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
>> ...
>> goal:
>> No subgoals!
>> Failed to apply initial proof method:
>> goal (1 subgoal):
>>  1. P
>> variables:
>>   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"
where
  "simple5 x = x"
proof -
  show "eqvt simple5_graph_aux" by (simp add: eqvt_def simple5_graph_aux_def)
next
  fix x y assume "simple5_graph x y" show True by auto
next
  fix P x assume "â xa . x = xa â P" then show P by simp
next
  fix x xa assume "x = xa"
  from this show "x = xa" by assumption
qed

proves the lemma.

One thing is not clear: I get exclamation marks aside on the last two
assumption:

after

   assume "â xa . x = xa â P"

   Introduced fixed type variable(s): 'a in "x__"

and after

   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?

- Gergely




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.