*To*: Johan Jeuring <johanj at cs.uu.nl>*Subject*: Re: [isabelle] Interleave in Isabelle*From*: Makarius <makarius at sketis.net>*Date*: Fri, 15 Apr 2011 20:34:23 +0200 (CEST)*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <A60093FC-86A6-4853-A863-3AEA0A182836@cs.uu.nl>*References*: <F811F2EF-B37C-4401-899A-8FCFE47382E5@cs.uu.nl> <A60093FC-86A6-4853-A863-3AEA0A182836@cs.uu.nl>*User-agent*: Alpine 1.10 (LNX 962 2008-03-14)

On Thu, 14 Apr 2011, Johan Jeuring wrote:

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

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]));

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 forsolving exercises (with the goal to follow and comment upon studentinteractions), and Isabelle seems to be the only prover that has offeredinterleave.

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

Makarius

**References**:**[isabelle] Interleave in Isabelle***From:*Johan Jeuring

- Previous by Date: [isabelle] EXTENDED DEADLINE : UML&FM'2011
- Next by Date: Re: [isabelle] apply proof method to all subgoals
- Previous by Thread: [isabelle] Interleave in Isabelle
- Next by Thread: [isabelle] tools on Isabelle.
- Cl-isabelle-users April 2011 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list