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

• To: John Wickerson <jpw48 at cam.ac.uk>
• Subject: Re: [isabelle] "and similarly..."
• From: Andreas Lochbihler <andreas.lochbihler at kit.edu>
• Date: Wed, 01 Feb 2012 08:52:55 +0100
• Cc: cl-isabelle-users at lists.cam.ac.uk
• User-agent: Mozilla/5.0 (X11; U; Linux x86_64; en-US; rv:1.9.2.24) Gecko/20111108 Thunderbird/3.1.16

```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
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)+

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
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.