[isabelle] Difficulties with Isar proofs and fix
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).
assumes S_Prop: "S : Prop"
and S_SP: "S : SP"
shows lift_S_SHP: "[[S]] : SHP"
apply (unfold SHP_def, unfold shp_def)
(* 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