Add STRIP_ALL_THEN and CHOOSE_ALL_THEN

src/1/Tactic.sml

@@ -466,7 +466,7 @@ val CHECK_ASSUME_TAC: thm_tactic =
       FIRST [CONTR_TAC gth, ACCEPT_TAC gth, OPPOSITE_TAC gth,
              DISCARD_TAC gth, ASSUME_TAC gth]
 
-val STRIP_ASSUME_TAC = REPEAT_TCL STRIP_THM_THEN CHECK_ASSUME_TAC
+val STRIP_ASSUME_TAC = STRIP_ALL_THEN CHECK_ASSUME_TAC
 val strip_assume_tac = STRIP_ASSUME_TAC
 
 (*---------------------------------------------------------------------------*
@@ -487,10 +487,10 @@ val strip_assume_tac = STRIP_ASSUME_TAC
  *---------------------------------------------------------------------------*)
 
 val STRUCT_CASES_TAC =
-   REPEAT_TCL STRIP_THM_THEN (fn th => SUBST1_TAC th ORELSE ASSUME_TAC th)
+   STRIP_ALL_THEN (fn th => SUBST1_TAC th ORELSE ASSUME_TAC th)
 
 val FULL_STRUCT_CASES_TAC =
-   REPEAT_TCL STRIP_THM_THEN (fn th => SUBST_ALL_TAC th ORELSE ASSUME_TAC th)
+   STRIP_ALL_THEN (fn th => SUBST_ALL_TAC th ORELSE ASSUME_TAC th)
 
 (*---------------------------------------------------------------------------*
  * COND_CASES_TAC: tactic for doing a case split on the condition p          *

src/1/Thm_cont.sig

@@ -26,6 +26,7 @@ sig
   val X_CASES_THEN     : Term.term list list -> thm_tactical
   val CASES_THENL      : thm_tactic list -> thm_tactic
   val STRIP_THM_THEN   : thm_tactical
+  val STRIP_ALL_THEN   : thm_tactical
 
   val ANTE_RES_THEN    : thm_tactical
   val IMP_RES_THEN     : thm_tactic -> thm -> tactic

src/1/Thm_cont.sml

@@ -260,6 +260,61 @@ val CHOOSE_THEN: thm_tactical =
       end
       handle HOL_ERR _ => raise ERR "CHOOSE_THEN" ""
 
+(* same as REPEAT_TCL CHOOSE_THEN but faster *)
+local
+   fun varyAcc v (V, l) = let val v' = gen_variant Parse.is_constname "" V v in (v'::V, v'::l) end
+   (* There are actual cases where strip_exists differ from this function *)
+   fun strip_exists1 tm =
+   let fun dest_exist_opt tm = SOME (dest_exists tm) handle HOL_ERR _ => NONE
+       fun strip A tm =
+           case dest_exist_opt tm of
+               NONE => (List.rev A, tm)
+             | SOME (x,tm') => strip (x::A) tm'
+   in
+      strip [] tm
+   end
+in
+val CHOOSE_ALL_THEN: thm_tactical =
+   fn ttac => fn xth =>
+      let
+         val (hyp,conc) = dest_thm xth
+         val _ = if is_exists conc then () else raise ERR "CHOOSE_THEN" "not a exists"
+         val (vars,_) = strip_exists1 conc
+         val len = List.length vars
+         val arr = Array.array (len,false)
+         fun name_eq x y = (fst (dest_var x) = fst (dest_var y))
+         fun check_for_dupes i [] = ([],[])
+           | check_for_dupes i (x::xs) = (if op_mem name_eq x xs
+                                          then
+                                          let val _ = Array.update (arr,i,true)
+                                              val (dupl,notdup) = check_for_dupes (i + 1) xs
+                                          in
+                                            (x::dupl,notdup)
+                                          end
+                                          else
+                                          let val (dupl,notdup) = check_for_dupes (i + 1) xs
+                                          in (dupl,x::notdup)
+                                          end)
+         val (dups,vars) = check_for_dupes 0 vars
+         val vec = Array.vector arr
+
+      in
+         fn (g as (asl,w)) =>
+         let
+            val fvs = (free_varsl ((conc::hyp)@(w::asl)))
+            val vars = List.rev (snd (rev_itlist varyAcc vars (fvs,[])))
+            fun merge i dups vars = if i < Vector.length vec
+                                    then if Vector.sub (vec,i)
+                                         then (hd dups :: merge (i + 1) (tl dups) vars)
+                                         else (hd vars :: merge (i + 1) dups (tl vars))
+                                    else []
+            val vars = merge 0 dups vars
+         in
+            EVERY_TCL (map X_CHOOSE_THEN vars) ttac xth g
+         end
+         handle HOL_ERR _ => raise ERR "CHOOSE_THEN" ""
+      end
+end
 (*----------  Cases tactics   -------------*)
 
 (*---------------------------------------------------------------------------
@@ -289,14 +344,17 @@ fun X_CASES_THEN varsl ttac =
  * Version that chooses the y's as variants of the x's.                      *
  *---------------------------------------------------------------------------*)
 
-fun CASES_THENL ttacl = DISJ_CASES_THENL (map (REPEAT_TCL CHOOSE_THEN) ttacl)
+fun CASES_THENL ttacl = DISJ_CASES_THENL (map (CHOOSE_ALL_THEN) ttacl)
 
 (*---------------------------------------------------------------------------*
  * Tactical to strip off ONE disjunction, conjunction, or existential.       *
  *---------------------------------------------------------------------------*)
 
 val STRIP_THM_THEN = FIRST_TCL [CONJUNCTS_THEN, DISJ_CASES_THEN, CHOOSE_THEN]
 
+(* Same as STRIP_ALL_THEN but slightly faster *)
+val STRIP_ALL_THEN = REPEAT_TCL (FIRST_TCL [CONJUNCTS_THEN, DISJ_CASES_THEN, CHOOSE_ALL_THEN])
+
 
 (* ---------------------------------------------------------------------*)
 (* Resolve implicative assumptions with an antecedent                   *)

src/basicProof/BasicProvers.sml

@@ -66,12 +66,11 @@ fun name_eq s M = ((s = fst(dest_var M)) handle HOL_ERR _ => false)
  * of a SUBST1_TAC.                                                          *
  *---------------------------------------------------------------------------*)
 
-val VAR_INTRO_TAC = REPEAT_TCL STRIP_THM_THEN
+val VAR_INTRO_TAC = STRIP_ALL_THEN
                       (fn th => SUBST_ALL_TAC th ORELSE ASSUME_TAC th);
 
-val TERM_INTRO_TAC =
- REPEAT_TCL STRIP_THM_THEN
-     (fn th => TRY (SUBST_ALL_TAC th) THEN ASSUME_TAC th);
+val TERM_INTRO_TAC = STRIP_ALL_THEN
+                      (fn th => TRY (SUBST_ALL_TAC th) THEN ASSUME_TAC th);
 
 fun away gfrees0 bvlist =
   rev(fst

src/basicProof/Notes

@@ -225,7 +225,7 @@ fun STRIP_NAMED_TAC (g as (asl,w)) =
                DISCARD_TAC th, 
                ASSUME_NAMED_AUTO_REF_TAC vars th]
      val STRIP_ASSUME_NAMED_TAC = 
-         REPEAT_TCL STRIP_THM_THEN CHECK_ASSUME_NAMED_TAC
+         STRIP_ALL_THEN CHECK_ASSUME_NAMED_TAC
  in
    STRIP_GOAL_THEN STRIP_ASSUME_NAMED_TAC g
  end;

src/coalgebras/llistScript.sml

@@ -868,7 +868,7 @@ Proof
                                 (ll2 = LMAP (f o g) ll0)` THEN
   SIMP_TAC (srw_ss()) [] THEN REPEAT STRIP_TAC THENL [
     PROVE_TAC [],
-    REPEAT_TCL STRIP_THM_THEN SUBST_ALL_TAC
+    STRIP_ALL_THEN SUBST_ALL_TAC
       (Q.ISPEC `ll0:'c llist` llist_CASES) THEN
     FULL_SIMP_TAC (srw_ss()) [LMAP, LTL_THM, LHD_THM] THEN
     PROVE_TAC []
@@ -1045,7 +1045,7 @@ Proof
                           !ll. (ll1 = LMAP f ll) ==> LFINITE ll`
           THEN1 SRW_TAC [][] THEN
     HO_MATCH_MP_TAC LFINITE_INDUCTION THEN REPEAT STRIP_TAC THEN
-    REPEAT_TCL STRIP_THM_THEN SUBST_ALL_TAC (Q.SPEC `ll` llist_CASES) THEN
+    STRIP_ALL_THEN SUBST_ALL_TAC (Q.SPEC `ll` llist_CASES) THEN
     FULL_SIMP_TAC (srw_ss()) [LMAP, LFINITE_THM],
     Q.ID_SPEC_TAC `ll` THEN HO_MATCH_MP_TAC LFINITE_INDUCTION THEN
     SIMP_TAC (srw_ss()) [LFINITE_THM, LMAP]
@@ -1061,7 +1061,7 @@ Proof
                                     LFINITE ll1 /\ LFINITE ll2`
           THEN1 PROVE_TAC [] THEN
     HO_MATCH_MP_TAC LFINITE_STRONG_INDUCTION THEN REPEAT STRIP_TAC THEN
-    REPEAT_TCL STRIP_THM_THEN SUBST_ALL_TAC (Q.SPEC `ll1` llist_CASES) THEN
+    STRIP_ALL_THEN SUBST_ALL_TAC (Q.SPEC `ll1` llist_CASES) THEN
     FULL_SIMP_TAC (srw_ss()) [LFINITE_THM, LAPPEND] THEN
     PROVE_TAC [],
     REWRITE_TAC [GSYM AND_IMP_INTRO] THEN
@@ -1092,7 +1092,7 @@ Proof
   Q.EXISTS_TAC `\ll1 ll2. ~LFINITE ll2 /\  ?ll3. ll1 = LAPPEND ll2 ll3` THEN
   ASM_SIMP_TAC (srw_ss()) [] THEN REPEAT STRIP_TAC THENL [
     PROVE_TAC [],
-    REPEAT_TCL STRIP_THM_THEN SUBST_ALL_TAC (Q.SPEC `ll4` llist_CASES) THEN
+    STRIP_ALL_THEN SUBST_ALL_TAC (Q.SPEC `ll4` llist_CASES) THEN
     FULL_SIMP_TAC (srw_ss()) [LFINITE_THM, LAPPEND, LHD_THM, LTL_THM] THEN
     PROVE_TAC []
   ]

src/coalgebras/pathScript.sml

@@ -165,10 +165,10 @@ Proof
     Q.ISPECL_THEN [`p_2`,`p_2`] (STRIP_ASSUME_TAC o
                                  REWRITE_RULE []) LLIST_BISIMULATION THEN
     Q.EXISTS_TAC `R` THEN SRW_TAC [][] THEN
-    Q.ISPEC_THEN `p_2''` (REPEAT_TCL STRIP_THM_THEN SUBST_ALL_TAC)
+    Q.ISPEC_THEN `p_2''` (STRIP_ALL_THEN SUBST_ALL_TAC)
                  llist_CASES THEN
     SRW_TAC [][] THEN
-    Q.ISPEC_THEN `p_2'''` (REPEAT_TCL STRIP_THM_THEN SUBST_ALL_TAC)
+    Q.ISPEC_THEN `p_2'''` (STRIP_ALL_THEN SUBST_ALL_TAC)
                  llist_CASES THEN SRW_TAC [][]
     THENL [
       RES_TAC THEN FULL_SIMP_TAC (srw_ss()) [LHD_THM],
@@ -265,7 +265,7 @@ Proof
         THEN1 METIS_TAC [] THEN
   CONJ_TAC THEN HO_MATCH_MP_TAC finite_path_ind THEN
   SRW_TAC [][] THEN
-  Q.ISPEC_THEN `p0` (REPEAT_TCL STRIP_THM_THEN SUBST_ALL_TAC)
+  Q.ISPEC_THEN `p0` (STRIP_ALL_THEN SUBST_ALL_TAC)
                path_cases THEN
   FULL_SIMP_TAC (srw_ss()) [] THEN METIS_TAC []
 QED
@@ -1200,7 +1200,7 @@ Proof
   Q.EXISTS_TAC
     `\x y. ~finite x /\ (y = pgenerate (\n. el n x) (\n. nth_label n x))` THEN
   ASM_SIMP_TAC (srw_ss()) [] THEN REPEAT STRIP_TAC THEN
-  Q.SPEC_THEN `q1` (REPEAT_TCL STRIP_THM_THEN SUBST_ALL_TAC) path_cases THEN
+  Q.SPEC_THEN `q1` (STRIP_ALL_THEN SUBST_ALL_TAC) path_cases THEN
   FULL_SIMP_TAC (srw_ss()) [] THEN
   CONV_TAC (LAND_CONV (ONCE_REWRITE_CONV [pgenerate_def])) THEN
   SRW_TAC [][el_def, nth_label_def, combinTheory.o_DEF]
@@ -1282,7 +1282,7 @@ Proof
         `!p. (?p0. okpath R p0 /\ (p = pmap f g p0)) ==> okpath R p` THEN1
         METIS_TAC[] THEN
   HO_MATCH_MP_TAC okpath_co_ind THEN SRW_TAC [][] THEN
-  Q.SPEC_THEN `p0` (REPEAT_TCL STRIP_THM_THEN SUBST_ALL_TAC) path_cases THEN
+  Q.SPEC_THEN `p0` (STRIP_ALL_THEN SUBST_ALL_TAC) path_cases THEN
   FULL_SIMP_TAC (srw_ss()) [] THEN METIS_TAC []
 QED
 
@@ -1338,7 +1338,7 @@ Proof
                         !p1 p2. (p = plink p1 p2) ==> finite p1 /\ finite p2`
      THEN1 PROVE_TAC [] THEN CONJ_TAC THEN
   HO_MATCH_MP_TAC finite_path_ind THEN SRW_TAC [][] THEN
-  Q.SPEC_THEN `p1` (REPEAT_TCL STRIP_THM_THEN SUBST_ALL_TAC) path_cases THEN
+  Q.SPEC_THEN `p1` (STRIP_ALL_THEN SUBST_ALL_TAC) path_cases THEN
   FULL_SIMP_TAC (srw_ss()) [] THEN
   SRW_TAC [][] THEN PROVE_TAC []
 QED

src/integer/integerScript.sml

@@ -2101,7 +2101,7 @@ Theorem INT_MOD_BOUNDS:
                        else          0 <= p % q /\ p % q < q
 Proof
   REPEAT STRIP_TAC THEN ASM_SIMP_TAC int_ss [int_mod] THEN
-  REPEAT_TCL STRIP_THM_THEN ASSUME_TAC (Q.SPEC `q` INT_NUM_CASES) THEN
+  STRIP_ALL_THEN ASSUME_TAC (Q.SPEC `q` INT_NUM_CASES) THEN
   FIRST_X_ASSUM SUBST_ALL_TAC THENL [
     ASM_SIMP_TAC int_ss [INT_LT, INT_SUB_LE, INT_LT_SUB_RADD],
     ASM_SIMP_TAC int_ss [INT_NEG_LT0, INT_LT],
@@ -2791,7 +2791,7 @@ QED
 
 (* can now prove uniqueness of / and % *)
 fun case_tac s =
-    REPEAT_TCL STRIP_THM_THEN ASSUME_TAC (Q.SPEC [QUOTE s] INT_NUM_CASES) THEN
+    STRIP_ALL_THEN ASSUME_TAC (Q.SPEC [QUOTE s] INT_NUM_CASES) THEN
     FIRST_X_ASSUM SUBST_ALL_TAC THEN Q.ABBREV_TAC [QUOTE s, QUOTE " = n"] THEN
     POP_ASSUM (K ALL_TAC)
 

src/num/theories/WhileScript.sml

@@ -46,7 +46,7 @@ Proof
         ASM_REWRITE_TAC [FUNPOW, NOT_LESS_0],
         Q.X_GEN_TAC `m` THEN REPEAT STRIP_TAC THEN
         Q.SUBGOAL_THEN `m = 0` (fn th => REWRITE_TAC [th, FUNPOW]) THEN
-        Q.SPEC_THEN `m` (REPEAT_TCL STRIP_THM_THEN SUBST_ALL_TAC)
+        Q.SPEC_THEN `m` (STRIP_ALL_THEN SUBST_ALL_TAC)
                     num_CASES THEN
         REWRITE_TAC [] THEN
         FIRST_X_ASSUM (Q.SPEC_THEN `0` MP_TAC) THEN
@@ -58,7 +58,7 @@ Proof
         METIS_TAC [],
         Q.X_GEN_TAC `m` THEN REPEAT STRIP_TAC THEN
         Q.SUBGOAL_THEN `?p. m = SUC p` (CHOOSE_THEN SUBST_ALL_TAC) THENL [
-          Q.SPEC_THEN `m` (REPEAT_TCL STRIP_THM_THEN SUBST_ALL_TAC)
+          Q.SPEC_THEN `m` (STRIP_ALL_THEN SUBST_ALL_TAC)
                       num_CASES THEN
           FULL_SIMP_TAC bool_ss [FUNPOW] THEN METIS_TAC [],
           ALL_TAC

src/num/theories/arithmeticScript.sml

@@ -2379,7 +2379,7 @@ Proof
    REPEAT STRIP_TAC THEN
    IMP_RES_THEN (STRIP_ASSUME_TAC o SPEC (“k:num”)) DIVISION THEN
    FIRST_ASSUM (fn th => fn g => SUBST_OCCS_TAC [([2],th)] g) THEN
-   REPEAT_TCL STRIP_THM_THEN MP_TAC (SPEC (“n:num”) num_CASES) THENL
+   STRIP_ALL_THEN MP_TAC (SPEC (“n:num”) num_CASES) THENL
    [IMP_RES_TAC LESS_NOT_EQ THEN
     DISCH_THEN (ASSUME_TAC o SYM) THEN
     RES_TAC,
@@ -2518,7 +2518,7 @@ Theorem DIV_MULT:
   !n r. r < n ==> !q. (q*n + r) DIV n = q
 Proof
    REPEAT GEN_TAC THEN
-   REPEAT_TCL STRIP_THM_THEN SUBST1_TAC (SPEC (“n:num”) num_CASES) THENL
+   STRIP_ALL_THEN SUBST1_TAC (SPEC (“n:num”) num_CASES) THENL
    [REWRITE_TAC [NOT_LESS_0],
     REPEAT STRIP_TAC THEN
     MATCH_MP_TAC DIV_UNIQUE THEN
@@ -3566,7 +3566,7 @@ Proof
       Q.EXISTS_TAC `SUC m` THEN REWRITE_TAC [EXP] THEN
       POP_ASSUM SUBST_ALL_TAC THEN MATCH_MP_TAC MULT_INCREASES THEN
       ASM_REWRITE_TAC [] THEN
-      REPEAT_TCL STRIP_THM_THEN SUBST_ALL_TAC (Q.SPEC `b` num_CASES) THENL [
+      STRIP_ALL_THEN SUBST_ALL_TAC (Q.SPEC `b` num_CASES) THENL [
         IMP_RES_TAC NOT_LESS_0,
         REWRITE_TAC [GSYM NOT_ZERO_LT_ZERO, NOT_EXP_0]
       ]
@@ -3580,7 +3580,7 @@ Proof
   REPEAT GEN_TAC THEN STRUCT_CASES_TAC (Q.SPEC `m` num_CASES) THEN
   REWRITE_TAC [EXP, GSYM NOT_ZERO_LT_ZERO, ONE, NOT_SUC, MULT_EQ_0] THEN
   EQ_TAC THEN STRIP_TAC THENL [
-    REPEAT_TCL STRIP_THM_THEN SUBST_ALL_TAC (Q.SPEC `n` num_CASES) THEN
+    STRIP_ALL_THEN SUBST_ALL_TAC (Q.SPEC `n` num_CASES) THEN
     REWRITE_TAC [] THEN IMP_RES_TAC NOT_EXP_0,
     ASM_REWRITE_TAC []
   ]

src/num/theories/numeralScript.sml

@@ -387,7 +387,7 @@ Proof
     INDUCT_THEN (MATCH_MP relationTheory.WF_INDUCTION_THM WF_LESS)
                 STRIP_ASSUME_TAC THEN
     (* now do numeral cases on n *)
-    REPEAT_TCL STRIP_THM_THEN SUBST_ALL_TAC (SPEC_ALL bit_cases) THENL [
+    STRIP_ALL_THEN SUBST_ALL_TAC (SPEC_ALL bit_cases) THENL [
       ASM_SIMP_TAC bool_ss [],
       ASM_SIMP_TAC bool_ss [] THEN AP_TAC THEN AP_TAC THEN
       FIRST_ASSUM MATCH_MP_TAC THEN SIMP_TAC bool_ss [BIT1] THEN

src/pred_set/src/pred_setScript.sml

@@ -3548,7 +3548,7 @@ val CARD_SUBSET =
         IMP_RES_TAC CARD_DELETE THEN
         ASM_REWRITE_TAC [] THEN COND_CASES_TAC THENL
         [let val th = SPEC (“CARD (t:'a set)”) num_CASES
-         in REPEAT_TCL STRIP_THM_THEN SUBST_ALL_TAC th
+         in STRIP_ALL_THEN SUBST_ALL_TAC th
          end THENL
           [REWRITE_TAC [LESS_OR_EQ,LESS_0],
            REWRITE_TAC [SUC_SUB1,LESS_OR_EQ,LESS_MONO_EQ,INV_SUC_EQ]],

src/simp/src/congLib.sml

@@ -326,7 +326,7 @@ fun FULL_CONGRUENCE_SIMP_TAC cs ss l =
 
            (* differs only in that it doesn't call DISCARD_TAC *)
            val STRIP_ASSUME_TAC' =
-         REPEAT_TCL STRIP_THM_THEN
+         STRIP_ALL_THEN
                     (fn th => FIRST [CONTR_TAC th, ACCEPT_TAC th,
                                            ASSUME_TAC th])
      fun simp_asm (t,l') = CONGRUENCE_SIMP_RULE cs ss (l'@l) t::l'

src/simp/src/simpLib.sml

@@ -852,7 +852,7 @@ local
    val caa_tac =
        caa_tac0 false {elimvars = false, droptrues = false, strip = false,
                        oldestfirst = true}
-   val STRIP_ASSUME_TAC' = REPEAT_TCL STRIP_THM_THEN caa_tac
+   val STRIP_ASSUME_TAC' = STRIP_ALL_THEN caa_tac
    fun drop r =
       fn n =>
          POP_ASSUM_LIST
@@ -886,7 +886,7 @@ end
 fun stdcon (c : simptac_config) th =
     if #elimvars c andalso eliminable (concl th) then VSUBST_TAC th
     else
-      (if #strip c then REPEAT_TCL STRIP_THM_THEN else I)
+      (if #strip c then STRIP_ALL_THEN else I)
         (caa_tac0 (not (#oldestfirst c)) c)
         th