*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Length of Proofs*From*: Christian Sternagel <c-sterna at jaist.ac.jp>*Date*: Thu, 01 Nov 2012 16:28:52 +0900*In-reply-to*: <50921DCB.6050502@rsise.anu.edu.au>*References*: <50921697.9090307@cococo.de> <50921DCB.6050502@rsise.anu.edu.au>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:16.0) Gecko/20121016 Thunderbird/16.0.1

cheers chris On 11/01/2012 03:59 PM, Jeremy Dawson wrote:

Jens, I don't know if this is a factor in this particular set of proofs, but often a particular sequence of proof steps is reused repeatedly. In such a case it is advantageous not to have to write them all down repeatedly, but to reuse them. The Standard ML interface to Isabelle is ideally suited to this purpose. Unfortunately its use has become actively discouraged in recent years. To illustrate, here are some bits of a proof script of mine which makes good use of the Standard ML interface. fun mctrtac sg st = FIRST [ atac sg, (match_tac [mstrctr.ctr] sg), ((resolve_tac [mstrctr.Comma, mstrctr.Star] THEN_ALL_NEW mctrtac) sg), (rtac mstrctr.same sg) ] st ; fun dvi_ctr_tacs dths = [ (rtac ex_conjI), (rtac mseqctr.I), mctrtac, mctrtac, (eresolve_tac [der_asm, dd1th] THEN_ALL_NEW resolve_tac dths THEN_ALL_NEW ssai_tac) ] ; fun init_dvi_ctr_tacs dths = [ (* ensure only desired occurrence of rule is expanded *) Clarsimp_tac, dtac trans, (clarsimp_tac (cesimps rule_defs)), rtac refl, Clarsimp_tac, (SELECT_GOAL (EVERY [ (* split up say F delible from (X,Y),Z |- W into cases: F (with stars) is X,Y or Z, or F is delible from X,Y,Z or W *) (REPEAT_SOME (eresolve_tac [mseqctr.elim, mstrctr_CommaR, mstrctr_StarR, mstrctr_IR] THEN_ALL_NEW Clarsimp_tac)), (* when deletion to substituted variable in rule *) TRYALL (EVERY' (dvi_ctr_tacs dths)) ])) ] ; fun xstacs th = [ (rtac ex_conjI 1), (etac dd1th 2), ((rtac th THEN_ALL_NEW ssai_tac) 2), (rtac mseqctr.I 1), mctrtac 1, mctrtac 1 ] ; val th = rdp (tn [dca1, dppsA, dica1, dassoc]) ; in the above, each additional theorem in the list of arguments to tn involves several proof steps val ctr_assoc_tacs = [ (EVERY' (init_dvi_ctr_tacs [dassoc]) 1), (EVERY (xstacs ([dassoc, dassoc] MRS duA2))), (EVERY (xstacs th)) ] ; (and twelve more rather like ctr_assoc_tacs, just a bit different) val ctr_tacs = [ EVERY init_ctr_tacs, EVERY ctr_assoc_tacs, EVERY ctr_ica1_tacs, EVERY ctr_ica2_tacs, EVERY ctr_ics1_tacs, EVERY ctr_ics2_tacs, (EVERY' (init_dvi_ctr_tacs [dastars]) 1), (EVERY' (init_dvi_ctr_tacs [dassA]) 1), EVERY ctr_ca1_tacs, EVERY ctr_ca2_tacs, EVERY ctr_cs1_tacs, EVERY ctr_cs2_tacs, EVERY ctr_rstars_tacs, EVERY ctr_rssA_tacs ] ; If I had written this out in the modern style (using Isar) the above would expand to thousands, probably tens of thousands, of lines of code. Cheers, Jeremy Dawson Jens Doll wrote:Hello all, when viewing the file Vickrey.thy from Tim I almost fell from my chair. It has 22 pages of code and that seems to be a normal length for Isabelle. Does anyone know how to shorten these artefacts or could someone explain to me why proofs have to be that long? Jens

**References**:**[isabelle] Length of Proofs***From:*Jens Doll

**Re: [isabelle] Length of Proofs***From:*Jeremy Dawson

- Previous by Date: Re: [isabelle] Length of Proofs
- Next by Date: Re: [isabelle] Print proof of theorem
- Previous by Thread: Re: [isabelle] Length of Proofs
- Next by Thread: Re: [isabelle] Length of Proofs
- Cl-isabelle-users November 2012 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