[isabelle] "and similarly..."



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




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