Re: [isabelle] writing an Isar proof for multiple subgoals
On 14 July 2015 at 20:09, Lars Noschinski <noschinl at in.tum.de> wrote:
> On 14.07.2015 11:19, Buday Gergely wrote:
>> I have a problem proving the third subgoal:
>> lemma "â (P::bool) (x::lam). (â xa. x = xa â P) â P"
>> proof -
>> fix P x assume "â xa. x = xa â P" show P by auto
>> No subgoals!
>> Failed to apply initial proof method:
>> goal (1 subgoal):
>> 1. P
>> P :: bool
> ... but auto failed to solve it. Notice the suspicious lack of "!!xa. x
> = xa" in the second part? That is because you did not feed the
> assumption into the show statement (which you could do e.g. using "then").
nominal_function simple5 :: "lam â lam"
"simple5 x = x"
show "eqvt simple5_graph_aux" by (simp add: eqvt_def simple5_graph_aux_def)
fix x y assume "simple5_graph x y" show True by auto
fix P x assume "â xa . x = xa â P" then show P by simp
fix x xa assume "x = xa"
from this show "x = xa" by assumption
proves the lemma.
One thing is not clear: I get exclamation marks aside on the last two
assume "â xa . x = xa â P"
Introduced fixed type variable(s): 'a in "x__"
assume "x = xa"
Introduced fixed type variable(s): 'a in "x__" or "xa__"
I guess I can ignore these for now but when could this be significant?
This archive was generated by a fusion of
Pipermail (Mailman edition) and