Re: [isabelle] Length of Proofs


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,
   (* 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.


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?


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.