*To*: isabelle-users at cl.cam.ac.uk*Subject*: [isabelle] Difficulties with Isar proofs and fix*From*: "Denis Bueno" <dbueno at gmail.com>*Date*: Mon, 25 Feb 2008 18:36:52 -0500

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

**Follow-Ups**:**Re: [isabelle] Difficulties with Isar proofs and fix***From:*Amine Chaieb

**Re: [isabelle] Difficulties with Isar proofs and fix***From:*Makarius

- Previous by Date: [isabelle] Postdoctoral Fellowhships
- Next by Date: Re: [isabelle] Difficulties with Isar proofs and fix
- Previous by Thread: [isabelle] Postdoctoral Fellowhships
- 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