*To*: Denis Bueno <dbueno at gmail.com>*Subject*: Re: [isabelle] Difficulties with Isar proofs and fix*From*: Makarius <makarius at sketis.net>*Date*: Wed, 27 Feb 2008 12:04:53 +0100 (CET)*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <6dbd4d000802260950g129b82ebt46a0373cd18335d5@mail.gmail.com>*References*: <6dbd4d000802251536r5123346ag9798ec984381e549@mail.gmail.com> <Pine.LNX.4.63.0802261119030.7354@atbroy101.informatik.tu-muenchen.de> <6dbd4d000802260903g1e1d1fefj5b98b35b9f98579c@mail.gmail.com> <6dbd4d000802260950g129b82ebt46a0373cd18335d5@mail.gmail.com>

On Tue, 26 Feb 2008, Denis Bueno wrote: > > Thank you all for your replies. While I digest them, attached is the > > theory, so that you can play with it. It requires the LList2 library > > (lazy, infinite lists) available at > > http://afp.sourceforge.net/entries/Lazy-Lists-II.shtml. I'd > > appreciate any comments on my theory. > > Well, I've completed the theorem I was having trouble with. It is > quite a bit longer than the apply-style proof, though much clearer. > Any comments that would help me improve its readability and > conciseness are welcome. I've started to look at your proofs, which are quite impressive as your second attempt in Isar reasoning only. One reason why things turn out a bit long is the general strategy of reducing things to predicate logic first, exposing it in the text, and then blasting your way through the thicked of quantifiers. Even in your apply scripts, there have been these unfoldings of Pow_def, subset_def etc. followed by blast. By proving derived natural deduction rules (and declaring them to the system as intro/elim, simp/iff etc.) you can work more smoothly without the detour through the object-logic. This simplifies both apply scripts and Isar texts. Moreover, in proper Isar you can usually avoid extra ``boiler plate statements'' like ``have EX x. P x'' before continuing to ``obtain x where P x'' --- the latter alone is usually sufficient. Here is a concrete example from your proof of theorem proposition_1_oif: fix T :: property assume T_st: "T : Prop" "T ~: [[S]]" have t_is: "EX t:T. t ~: S" proof - from T_st have T_not_under_S: "~(T <= S)" unfolding property_lift_def by blast thus ?thesis unfolding subset_def by blast qed then obtain t where t_st: "t : T" "t ~: S" .. Here t_is is only ever used to obtain the subsequent t. The above hava/obtain part can be simplified as follows: from `T ~: [[S]]` have "~ T <= S" by (simp add: property_lift_def) then obtain t where t_st: "t : T" "t ~: S" by blast In fact you can also finish the obtain directly in one blow: from `T ~: [[S]]` obtain t where t_st: "t : T" "t ~: S" by (auto simp add: property_lift_def) (Here I've merely applied the heuristic that auto somehow combines simp and blast.) Isar is better at exploiting the power of automated reasoning than apply scripts, because the effect can be limited to clearly delimited sub-problems. Readability should also be kept in mind, of course. The challenge (and high art) in composing good Isar proofs is to expose just the relevant bits in the text, and manage to get it accepted by the proof tools. Makarius

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

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

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

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

- Previous by Date: [isabelle] Setting up a non-standard induction
- Next by Date: [isabelle] CMCS 08: final call for short contributions
- 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