*To*: Denis Bueno <dbueno at gmail.com>*Subject*: Re: [isabelle] Difficulties with Isar proofs and fix*From*: Amine Chaieb <chaieb at in.tum.de>*Date*: Tue, 26 Feb 2008 11:27:39 +0100*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <6dbd4d000802251536r5123346ag9798ec984381e549@mail.gmail.com>*References*: <6dbd4d000802251536r5123346ag9798ec984381e549@mail.gmail.com>*Sender*: Amine Chaieb <chaieb.amine at googlemail.com>*User-agent*: Thunderbird 1.5.0.8 (Macintosh/20061025)

Hi Denis,

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

"?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?

**References**:**[isabelle] Difficulties with Isar proofs and fix***From:*Denis Bueno

- Previous by Date: [isabelle] Difficulties with Isar proofs and fix
- Next by Date: Re: [isabelle] Difficulties with Isar proofs and fix
- Previous by Thread: [isabelle] Difficulties with Isar proofs and fix
- Next by Thread: Re: [isabelle] Difficulties with Isar proofs and fix
- Cl-isabelle-users February 2008 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list