*To*: Jens Doll <jd at cococo.de>*Subject*: Re: [isabelle] Length of Proofs*From*: Jeremy Dawson <jeremy at rsise.anu.edu.au>*Date*: Thu, 01 Nov 2012 17:59:23 +1100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <50921697.9090307@cococo.de>*References*: <50921697.9090307@cococo.de>*User-agent*: Thunderbird 2.0.0.24 (X11/20101027)

Jens,

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]) ;

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 ] ;

Cheers, Jeremy Dawson Jens Doll wrote:

Hello all,when viewing the file Vickrey.thy from Tim I almost fell from mychair. It has 22 pages of code and that seems to be a normal lengthfor Isabelle.Does anyone know how to shorten these artefacts or could someoneexplain to me why proofs have to be that long?Jens

**Follow-Ups**:**Re: [isabelle] Length of Proofs***From:*Christian Sternagel

**Re: [isabelle] Length of Proofs***From:*Makarius

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

- Previous by Date: [isabelle] Length of Proofs
- Next by Date: Re: [isabelle] Length of Proofs
- Previous by Thread: [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