*To*: John Wickerson <jpw48 at cam.ac.uk>*Subject*: Re: [isabelle] "and similarly..."*From*: Jeremy Dawson <jeremy at rsise.anu.edu.au>*Date*: Wed, 01 Feb 2012 10:03:29 +1100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <A49A52D0-C544-488B-8B82-A224DA214AD5@cam.ac.uk>*References*: <A49A52D0-C544-488B-8B82-A224DA214AD5@cam.ac.uk>*User-agent*: Thunderbird 2.0.0.24 (X11/20101027)

John Wickerson wrote:

Hello, Is there a feature in Isabelle that corresponds to writing "and similarly" in an informal pen-and-paper proof? Specifically, here is a fragment of my proof script:...next assume "opt1 fN \<circ> HeadMap g1 = HeadMap g2 \<circ> fA" and "opt1 fN' \<circ> HeadMap g2 = HeadMap g3 \<circ> fA'" hence "opt1 fN' \<circ> opt1 fN \<circ> HeadMap g1 = HeadMap g3 \<circ> fA' \<circ> fA"using o_assoc[of "opt1 fN'" "opt1 fN" "HeadMap g1"]and o_assoc[of "opt1 fN'" "HeadMap g2" "fA"] by autothus "opt1 (fN' \<circ> fN) \<circ> HeadMap g1 = HeadMap g3 \<circ> (fA' \<circ> fA)"using opt1_o[of "fN'" "fN"] by autonext assume "opt1 fN \<circ> TailMap g1 = TailMap g2 \<circ> fA" and "opt1 fN' \<circ> TailMap g2 = TailMap g3 \<circ> fA'" hence "opt1 fN' \<circ> opt1 fN \<circ> TailMap g1 = TailMap g3 \<circ> fA' \<circ> fA"using o_assoc[of "opt1 fN'" "opt1 fN" "TailMap g1"]and o_assoc[of "opt1 fN'" "TailMap g2" "fA"] by autothus "opt1 (fN' \<circ> fN) \<circ> TailMap g1 = TailMap g3 \<circ> (fA' \<circ> fA)"using opt1_o[of "fN'" "fN"] by autoqedThe two blocks here are identical, except one uses "HeadMap" where the other uses "TailMap". (HeadMap and TailMap are both record constructors.) Is there a neat way to remove the duplication here?Thanks very much, John

John, Where what varies is the choice of theorem you could get something like (and this sort of thing is absolutely routine in my work): fun mtacs XMap = [ ... ] : tactic list ; Then use, one time, (EVERY (mtacs HeadMapThm)) and the other time (EVERY (mtacs TailMapThm)).

HeadMap = HeadMap (in one instance), or TailMap = TailMap (in the other).

fun string1 XMapstr = .... ^ XMapstr ^ .... and use string1 "HeadMap" or string1 "TailMap"

Cheers, Jeremy

**References**:**[isabelle] "and similarly..."***From:*John Wickerson

- Previous by Date: Re: [isabelle] "and similarly..."
- Previous by Thread: Re: [isabelle] "and similarly..."
- Cl-isabelle-users January 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