[isabelle] Difficulties with Isar proofs and fix

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 ]]))
  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.