Re: [isabelle] Difficulties with Isar proofs and fix



Hi Denis,

I was not able to reproduce your example due to lack of notation (what is the <| ?).

Any way, to this kind of reasoning in Isar, you should use the "{" and "}" brackets. This is like a new sheet of paper you take and prove something new on it.

So something like
 proof
   fix T :: property
   assume T_st: "T : Prop" "T ~: [[S]]"

   obtain M where M_st: "M : Obs" "M <| T" sorry

{
   fix T' :: property
   assume T'_st: "T' : Prop" "M <| T'"

   hence "T' ~: [[ S ]]" sorry
   with T'_st have "T' : Prop & M <| T' --> T' ~: [[ S ]]" by blast
}
   hence "ALL T'. T' : Prop & M <| T' --> T' ~: [[ S ]]" ..


When you leave the context of the brackets, you will see that Isar already generalizes your result, i.e. the have "T' : Prop & M <| T' --> T' ~: [[ S ]]" *inside* the brackets, becomes

 "?T' : Prop & M <| ?T' --> ?T' ~: [[ S ]]"

i.e. generalized for arbitrary T' of type property.

Hope this helps.

Amine.

Denis Bueno wrote:
Hi all,

I'm having trouble with a proof skeleton that seems like it should
work (judging from what I've seen from the Isar tutorial and manual),
but I can't get it to, and I'm not sure why.

Basically I have a theorem whose conclusion is of the form: ALL x. ...
(EX y. ... (ALL z. ...)).  I would like to show this by fix'ing an
arbitrary x, exhibiting a y, and fix'ing an arbitrary z, then
satisfying the respective bodies of each quantification.  Something
similar is done as the last example in section 2.4 of the Isar
tutorial, and it is this example which I'm trying to emulate.

For what it's worth, I've already proved this theorem in a low-level
style with a bunch of apply's and tactics.  I'm trying to convert this
to a real Isar proof (not just one that embeds the apply-style proof).

theorem proposition_1_oif:
  assumes S_Prop: "S : Prop"
  and     S_SP:   "S : SP"
  shows   lift_S_SHP: "[[S]] : SHP"
apply (unfold SHP_def, unfold shp_def)
apply (simp)
(* at this point the goal is:
ALL T. T : Prop & T ~: [[ S ]] -->
           (EX M. M : Obs & M <| T & (ALL T'. T' : Prop & M <| T' -->
T' ~: [[ S ]]))
*)
proof
  fix T :: property
  assume T_st: "T : Prop" "T ~: [[S]]"

  obtain M where M_st: "M : Obs" "M <| T" sorry

  fix T' :: property
  assume T'_st: "T' : Prop" "M <| T'"

  hence "T' ~: [[ S ]]" sorry
  with T'_st have "T' : Prop & M <| T' --> T' ~: [[ S ]]" by blast
  hence "ALL T'. T' : Prop & M <| T' --> T' ~: [[ S ]]" ..

The last step in the proof fails.  I'm not sure why, since it seems to
me that using the T' fix'd at the beginning, along with its relevant
constraints, one should be able to show the last goal.  The informal
argument goes, "Since T' was arbitrary, we know that for *all such
T'*, such-and-such holds."

What have I done wrong?






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