*To*: Denis Bueno <dbueno at gmail.com>*Subject*: Re: [isabelle] Difficulties with Isar proofs and fix*From*: Makarius <makarius at sketis.net>*Date*: Tue, 26 Feb 2008 11:40:38 +0100 (CET)*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <6dbd4d000802251536r5123346ag9798ec984381e549@mail.gmail.com>*References*: <6dbd4d000802251536r5123346ag9798ec984381e549@mail.gmail.com>

On Mon, 25 Feb 2008, Denis Bueno wrote: > 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. Here is your proof in Isar: lemma "ALL x :: 'a. EX y :: 'b. ALL z :: 'c. P x y z" proof fix a :: 'a def b == "t :: 'b" have "ALL z. P a b z" proof fix c show "P a b c" sorry qed then show "EX y. ALL z. P a y z" .. qed (Note that type constraints are needed here, because of the fully abstract formulation of the problem and sub-problems.) Isar is very ``puristic'' in the sense in being ignorant of predicate logic. The native way of expressing statements and proofs is via the Isabelle/Pure logical framework, which provides very powerful means to work with higher-order Natural Deduction rules. Maybe the paper http://www4.in.tum.de/~wenzelm/papers/isar-framework.pdf helps to understand the basic approach. In the above text there are certain situations where single introduction or elimination rules get involved; these are made explicit here: lemma "ALL x :: 'a. EX y :: 'b. ALL z :: 'c. P x y z" proof (rule allI) fix a :: 'a def b == "t :: 'b" have "ALL z. P a b z" proof (rule allI) fix c show "P a b c" sorry qed then show "EX y. ALL z. P a y z" by (rule exI) qed This is indeed a bit awkward, so one could blame Isar for not supporting ``standard'' logical connectives more directly. On the other hand, by making proper use of Pure principles, things work out smoothly not just for ALL/EX, but any concept you have introduced in your application. The idea is to derive intro/elim rules from your definitions, or even better let the system do it for you (using the 'inductive' package) as hinted in section 4.6 of the above article. > 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 ]]" .. If you provide a working theory, we can play with it a little. For the moment here are some general hints: * The abbreviations 'hence' for 'then have' and 'thus' for 'then show' are better avoided, because they demand much more typing. This paradox is explained by the experience that the goal prefixing often changes in proof development and massaging, e.g. 'then have' vs. 'from blah have' vs. 'with blubb have' etc. * Local facts can be referenced literally, e.g. `S : Prop` (with ASCII backquotes); no need to emulate the structure of statements in names like S_Prop. Makarius

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

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

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