CODEWITHSUNDEEP
isabelleisar
Luiz Martins
Luiz Martins

Reputation: 1724

How to use the base case assumption when proving with 'induct' in Isabelle

Say I'm proving a theorem that assumes "n ≥ m" (both are natural numbers), and I apply induction on n. In the base case, the assumption is that "n = 0". With these two, we can conclude that, in the base case, "m = 0".

However, I'm having trouble in using the statement "n = 0":

lemma foo:
  assumes "(n::nat) ≥ (m::nat)"
  shows ...
proof (induct n)
  case 0
  have "m = 0" using <I don't know what to put here> assms by simp
  ...
qed

I've tried using "n = 0", but it appears to be an "Undefined fact". I've also tried adding it as an assumption, but to no avail. Nonetheless, it is clear that it is an implicit assumption when analyzing the base case.

So, how may I use the assumption of the base case directly in my proof?

Upvotes: 0

Views: 208

Answers (1)

Manuel Eberl
Manuel Eberl

Reputation: 8278

Any assumptions that you need to be part of the induction need to be part of the proof state when you call induct. In particular, that should be all assumptions that contain the thing you do the induction over (i.e. all the ones that contain n in your case).

You should therefore do a using assms before the proof. Then 0 ≥ m will be available to you in the base case, under the name "0.prems" (or just 0 for all of these plus the induction hypothesis, which in this case doesn't exist).

Upvotes: 2

Related Questions