Re: [isabelle] "and similarly..."



Hi John,

the proofs look to me as if they are completely independent of HeadMap and TailMap. Hence, Isar allows you to abstract over them and prove both goals in one go:

next
  fix HeadOrTailMap
  assume "opt1 fN \<circ>  HeadOrTailMap g1 = HeadOrTailMap g2 \<circ>  fA"
     and "opt1 fN' \<circ>  HeadOrTailMap g2 = HeadOrTailMap g3 \<circ>  fA'"
  hence "opt1 fN' \<circ>  opt1 fN \<circ>  HeadOrTailMap g1 =
         HeadOrTailMap g3 \<circ>  fA' \<circ>  fA"
    using o_assoc[of "opt1 fN'" "opt1 fN" "HeadOrTailMap g1"]
    and o_assoc[of "opt1 fN'" "HeadOrTailMap g2" "fA"] by auto
  hence "opt1 (fN' \<circ>  fN) \<circ>  HeadOrTailMap g1 =
         HeadOrTailMap g3 \<circ>  (fA' \<circ>  fA)" (is ?thesis)
    using opt1_o[of "fN'" "fN"] by auto
  thus ?thesis and ?thesis by -
qed

In order to solve both goals, you still must state the "show" or "thus" part twice, which is why I introduced the ?thesis abbreviation.

Problems with distinct types might cause this approach to fail. In that case, you can state the above proof as a separate lemma X and then use

qed(erule (2) X)+

instead.

Hope this helps,
Andreas


Am 31.01.2012 16:57, schrieb John Wickerson:
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 auto
     thus "opt1 (fN' \<circ>  fN) \<circ>  HeadMap g1 = HeadMap g3 \<circ>  (fA' \<circ>  fA)"
       using opt1_o[of "fN'" "fN"] by auto
   next
     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 auto
     thus "opt1 (fN' \<circ>  fN) \<circ>  TailMap g1 = TailMap g3 \<circ>  (fA' \<circ>  fA)"
       using opt1_o[of "fN'" "fN"] by auto
   qed

The 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

--
Karlsruher Institut für Technologie
IPD Snelting

Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Adenauerring 20a, Geb. 50.41, Raum 031
76131 Karlsruhe

Telefon: +49 721 608-47399
Fax: +49 721 608-48457
E-Mail: andreas.lochbihler at kit.edu
http://pp.info.uni-karlsruhe.de
KIT - Universität des Landes Baden-Württemberg und nationales Forschungszentrum in der Helmholtz-Gemeinschaft





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