CODEWITHSUNDEEP
isabelle
resu
resu

Reputation: 41

Instantiating theorems in Isabelle

Suppose some lemma, lets call it an_equation, proves that equation f(n)=n*n+1 holds for all odd natural numbers n (and f is some previously defined function).

How can I instantiate this lemma to concrete values of n, so that I can prove, say f(5)=5*5+1?

(There is the lemmas keyword, with which I can prove lemmas inst = an_equation[where n=5, simplified], but this is not quite what I what. What I want is 

lemma inst_new : "f(5) = 5*5+1"

but as there were scarcely any example around in the usual documentation thai I consult, I couldn't figure out how to prove this.)

Upvotes: 0

Views: 572

Answers (1)

Manuel Eberl
Manuel Eberl

Reputation: 8268

You can instantiate free variables in your theorem with the of and where attributes, e.g. an_equation[of 5] or an_equation[where n = 5]. You can also instantiate its assumptions, e.g. if you have a theorem called foo of the form P x ⟹ Q x and you have a theorem called bar of the form P 5, you can do foo[OF bar] to get the theorem Q 5.

You can inspect these instantiated with thm (e.g. thm foo[of 5]) and use them in a proof with using, from, etc.

Note that proof methods also instantiate theorems whenever needed, e.g. if you have, as above, the theorem foo stating that P n ⟹ Q n and you have the goal Q 5, you can do this:

lemma "Q 5"
  apply (rule foo)

Then the goal state will have one subgoal, namely P 5.

So, in your case, by (rule an_equation) should do the trick. Something like by (simp add: an_equation) or using an_equation by simp or using an_equation by blast would probably also work, but might be slightly less robust in general since the simplifier can do other stuff first and then the rule might not apply anymore.

Upvotes: 1

Related Questions