Isabelle: Predecessor function

Question

I am not sure, but I think sometimes my proofs would be easier if I had a predecessor function, e.g., in case a variable is known not to be zero.

I don't know a good example, but perhaps here: { fix n have "(n::nat) > 0 ⟹ (∑i<n. f i) = Predecessor n" sorry }

Possibly because it is not a good idea, there is no predecessor function in the library.

Is there a way to simulate a predecessor function or similar?

I have thought of this example:

theorem dummy:
shows "1=1" (* dummy *)
proof-

  (* Predecessor function *)
  def pred == "λnum::nat. (∑i∈{ i . Suc i = num}. i)"

  {fix n :: nat
  from pred_def have "n>0 ⟹ Suc (pred n) = n" 
  apply(induct n)
  by simp_all
  }
  show ?thesis sorry
qed

Answer 1

Your definition is unnecessarily complicated. Why do you not just write

def pred ≡ "λn::nat. n - 1"

Then you can have

have [simp]: "⋀n. n > 0 ⟹ Suc (pred n) = n" by (simp add: pred_def)

In the case of 0, the pred function then simply returns 0 and Suc (pred 0) = 0 obviously doesn't hold. You could also define pred ≡ "λn. THE n'. Suc n' = n". That would return the unique natural number whose successor is n if such a number exists (i.e. if n > 0) and undefined (i.e. some natural number you know nothing about) otherwise. However, I would argue that in this case, it is much easier and sensible to just do pred ≡ λn::nat. n - 1.

I would suspect that in most cases, you can simply forgo the pred function and write n - 1; however, I do know that it is sometimes good to have the - 1 “protected” by a definition. In these cases, I usually def a variable n' as n - 1 and prove Suc n' = n – basically the same thing. In my opinion, seeing as proving this takes only one line, it does not really merit a definition of its own, such as this pred function, but one could make a reasonable case for it, I guess.

Another thing: I've noticed you use lemma "1 = 1" as some kind of dummy environment to do Isar proofs in. I would like to point out the existence of notepad, which exists precisely for that use case and that can be used as follows:

notepad
begin
  have "some fact" by something
end