Re: [isabelle] Interleave in Isabelle



On Thu, 14 Apr 2011, Johan Jeuring wrote:

We noticed that the Isabelle Reference Manual from 1999 mentions an interleaving construct for tactics, which has disappeared in the manual from 2011. Is there a particular reason for this?

It was probably dropped when renovating some of the more ancient manuals, because it was hardly ever used.

A grep through the sources and its history reveals the following:

  * Isabelle2011 provides Seq.interleave (in src/Pure/General/seq.ML)
    and INTLEAVE (in src/Pure/tactical.ML) but neither of them is used.

  * These operations have been there since the beginnings of recorded
    Isabelle history in 1993, see also http://isabelle.in.tum.de/repos/isabelle/annotate/957c887b89b5/src/Pure/tctical.ML#l102

  * In prehistoric Isabelle92 there is a single use of the tactical

val prems = goal ZF.thy
    "[| f: A->B;  g: C->D;  A Int C = 0  |] ==>  \
\    (f Un g) : (A Un C) -> (B Un D)";
     (*Contradiction if A Int C = 0, a:A, a:B*)
val [disjoint] = prems RL ([IntI] RLN (2, [equals0D]));
by (cut_facts_tac prems 1);
by (rtac PiI 1);
(*solve subgoal 2 first!!*)
by (DEPTH_SOLVE_1 (eresolve_tac [UnE, Pair_mem_PiE, sym, disjoint] 2
       INTLEAVE ares_tac [ex1I, apply_Pair RS UnI1, apply_Pair RS UnI2] 2));
by (REPEAT (eresolve_tac [asm_rl,UnE,rel_Un,PiE] 1));
val fun_disjoint_Un = result();

  * In Isabelle93 the same is proved like this, using the "Classical
    reasoner" (fast_tac):

val prems = goal ZF.thy
    "[| f: A->B;  g: C->D;  A Int C = 0  |] ==>  \
\    (f Un g) : (A Un C) -> (B Un D)";
     (*Contradiction if A Int C = 0, a:A, a:B*)
val [disjoint] = prems RL ([IntI] RLN (2, [equals0D]));
val Pair_UnE = read_instantiate [("c","<?a,?b>")] UnE; (* ignores x: A Un C *)
by (cut_facts_tac prems 1);
by (rtac PiI 1);
by (REPEAT (ares_tac [rel_Un, fun_is_rel] 1));
by (rtac ex_ex1I 1);
by (fast_tac (ZF_cs addDs [apply_Pair]) 1);
by (REPEAT_FIRST (eresolve_tac [asm_rl, Pair_UnE, sym RS trans]
             ORELSE' eresolve_tac [Pair_mem_PiE,disjoint] THEN' atac));
val fun_disjoint_Un = result();


We ask because we are working on a paper on interleaving strategies for solving exercises (with the goal to follow and comment upon student interactions), and Isabelle seems to be the only prover that has offered interleave.

These are just a few lines of rather obvious SML text. When I encountered it as a young student in 1993 it did not surprise me.


We can imagine that efficiency might be a reason to exclude it: the number of possibilities increases (more than) exponentially in the length of the arguments when interleaving is used.

Larry might remember what he did in 1992/1993. We do not have any formal history, because we started using CVS 1.0 only in summer 1993.

Often such generic strategies have been superseded by specific proof automation, such as the Classical Reasoner above.

Since tacticals are closely related to parser combinators, you might also look there in the literature what people did to improve worst-case complexities.


	Makarius





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