Taming meta implication in Isar proofs

Question

Proving a simple theorem I came across meta-level implications in the proof. Is it OK to have them or could they be avoided? If I should handle them, is this the right way to do so?

theory Sandbox
imports Main
begin

lemma "(x::nat) > 0 ∨ x = 0"
proof (cases x)
  assume "x = 0"
  show "0 < x ∨ x = 0" by (auto)
next
  have "x = Suc n ⟹ 0 < x" by (simp only: Nat.zero_less_Suc)
  then have "x = Suc n ⟹ 0 < x ∨ x = 0" by (auto)
  then show "⋀nat. x = Suc nat ⟹ 0 < x ∨ x = 0" by (auto)
qed

end

I guess this could be proved more easily but I wanted to have a structured proof.

Answer 1

In principle meta-implication ==> is nothing to be avoided (in fact its the "native" way to express inference rules in Isabelle). There is a canonical way that often allows us to avoid meta-implication when writing Isar proofs. E.g., for a general goal

"!!x. A ==> B"

we can write in Isar

fix x
assume "A"
...
show "B"

For your specific example, when looking at it in Isabelle/jEdit you might notice that the n of the second case is highlighted. The reason is that it is a free variable. While this is not a problem per se, it is more canonical to fix such variables locally (like the typical statement "for an arbitrary but fixed ..." in textbooks). E.g.,

next
  fix n
  assume "x = Suc n"
  then have "0 < x" by (simp only: Nat.zero_less_Suc)
  then show "0 < x ∨ x = 0" ..
qed

Here it can again be seen how fix/assume/show in Isar corresponds to the actual goal, i.e.,

1. ⋀nat. x = Suc nat ⟹ 0 < x ∨ x = 0