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



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

In your case what differs between the two cases is the choice of the constant (?) HeadMap or TailMap, to plug into a particular spot. You could no doubt work something out involving a variable ?XMap (in place of HeadMap or TailMap), a subgoal ?XMap = ?XMap, and resolve this with theorems such as
HeadMap = HeadMap (in one instance), or TailMap = TailMap (in the other).

Alternatively, what I have also done on occasions is to create different strings for use in subgoal_tac or similar

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

You have to be using the ML interface to Isabelle to do this - which, I understand, is what ML was originally designed for - and so is particularly well suited for.

Cheers,

Jeremy






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