# HG changeset patch
# User nipkow
# Date 888676850 -3600
# Node ID 131989b78417ee8af2b877a5d7f52dedbf482377
# Parent  6328d427a3396160ab4b02b415352d6b37f661d7
Little reorganization. Loop tactics have names now.

diff -r 6328d427a339 -r 131989b78417 src/Provers/simplifier.ML
--- a/src/Provers/simplifier.ML	Sat Feb 28 15:40:03 1998 +0100
+++ b/src/Provers/simplifier.ML	Sat Feb 28 15:40:50 1998 +0100
@@ -22,14 +22,14 @@
   val rep_ss: simpset ->
    {mss: meta_simpset,
     subgoal_tac:        simpset -> int -> tactic,
-    loop_tac:                      int -> tactic,
+    loop_tacs:          (string * (int -> tactic))list,
            finish_tac: thm list -> int -> tactic,
     unsafe_finish_tac: thm list -> int -> tactic};
   val print_ss: simpset -> unit
   val print_simpset: theory -> unit
   val setsubgoaler: simpset *  (simpset -> int -> tactic) -> simpset
   val setloop:      simpset *             (int -> tactic) -> simpset
-  val addloop:      simpset *             (int -> tactic) -> simpset
+  val addloop:      simpset *  (string * (int -> tactic)) -> simpset
   val setSSolver:   simpset * (thm list -> int -> tactic) -> simpset
   val addSSolver:   simpset * (thm list -> int -> tactic) -> simpset
   val setSolver:    simpset * (thm list -> int -> tactic) -> simpset
@@ -102,16 +102,16 @@
   Simpset of {
     mss: meta_simpset,
     subgoal_tac:        simpset -> int -> tactic,
-    loop_tac:                      int -> tactic,
+    loop_tacs:          (string * (int -> tactic))list,
            finish_tac: thm list -> int -> tactic,
     unsafe_finish_tac: thm list -> int -> tactic};
 
-fun make_ss (mss, subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac) =
-  Simpset {mss = mss, subgoal_tac = subgoal_tac, loop_tac = loop_tac,
+fun make_ss (mss, subgoal_tac, loop_tacs, finish_tac, unsafe_finish_tac) =
+  Simpset {mss = mss, subgoal_tac = subgoal_tac, loop_tacs = loop_tacs,
     finish_tac = finish_tac, unsafe_finish_tac = unsafe_finish_tac};
 
 val empty_ss =
-  make_ss (Thm.empty_mss, K (K no_tac), K no_tac, K (K no_tac), K (K no_tac));
+  make_ss (Thm.empty_mss, K (K no_tac), [], K (K no_tac), K (K no_tac));
 
 fun rep_ss (Simpset args) = args;
 fun prems_of_ss (Simpset {mss, ...}) = Thm.prems_of_mss mss;
@@ -136,90 +136,89 @@
 
 (* extend simpsets *)
 
-fun (Simpset {mss, subgoal_tac = _, loop_tac, finish_tac, unsafe_finish_tac})
+fun (Simpset {mss, subgoal_tac = _, loop_tacs, finish_tac, unsafe_finish_tac})
     setsubgoaler subgoal_tac =
-  make_ss (mss, subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac);
+  make_ss (mss, subgoal_tac, loop_tacs, finish_tac, unsafe_finish_tac);
 
-fun (Simpset {mss, subgoal_tac, loop_tac = _, finish_tac, unsafe_finish_tac})
-    setloop loop_tac =
-  make_ss (mss, subgoal_tac, DETERM o loop_tac, finish_tac, unsafe_finish_tac);
+fun (Simpset {mss, subgoal_tac, loop_tacs = _, finish_tac, unsafe_finish_tac})
+    setloop tac =
+  make_ss (mss, subgoal_tac, [("",tac)], finish_tac, unsafe_finish_tac);
 
-fun (Simpset {mss, subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac})
-    addloop tac =
-  make_ss (mss, subgoal_tac, loop_tac ORELSE' (DETERM o tac), finish_tac, unsafe_finish_tac);
+fun (Simpset {mss, subgoal_tac, loop_tacs, finish_tac, unsafe_finish_tac})
+    addloop atac =
+  make_ss (mss, subgoal_tac, overwrite(loop_tacs,atac),
+           finish_tac, unsafe_finish_tac);
 
-fun (Simpset {mss, subgoal_tac, loop_tac, finish_tac = _, unsafe_finish_tac})
+fun (Simpset {mss, subgoal_tac, loop_tacs, finish_tac = _, unsafe_finish_tac})
     setSSolver finish_tac =
-  make_ss (mss, subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac);
+  make_ss (mss, subgoal_tac, loop_tacs, finish_tac, unsafe_finish_tac);
 
-fun (Simpset {mss, subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac})
+fun (Simpset {mss, subgoal_tac, loop_tacs, finish_tac, unsafe_finish_tac})
     addSSolver tac =
-  make_ss (mss, subgoal_tac, loop_tac, fn hyps => finish_tac hyps ORELSE' tac hyps,
+  make_ss (mss, subgoal_tac, loop_tacs, fn hyps => finish_tac hyps ORELSE' tac hyps,
     unsafe_finish_tac);
 
-fun (Simpset {mss, subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac = _})
+fun (Simpset {mss, subgoal_tac, loop_tacs, finish_tac, unsafe_finish_tac = _})
     setSolver unsafe_finish_tac =
-  make_ss (mss, subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac);
+  make_ss (mss, subgoal_tac, loop_tacs, finish_tac, unsafe_finish_tac);
 
-fun (Simpset {mss, subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac})
+fun (Simpset {mss, subgoal_tac, loop_tacs, finish_tac, unsafe_finish_tac})
     addSolver tac =
-  make_ss (mss, subgoal_tac, loop_tac, finish_tac,
+  make_ss (mss, subgoal_tac, loop_tacs, finish_tac,
     fn hyps => unsafe_finish_tac hyps ORELSE' tac hyps);
 
-fun (Simpset {mss, subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac})
+fun (Simpset {mss, subgoal_tac, loop_tacs, finish_tac, unsafe_finish_tac})
     setmksimps mk_simps =
   make_ss (Thm.set_mk_rews (mss, map (Thm.strip_shyps o Drule.zero_var_indexes) o mk_simps),
-    subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac);
+    subgoal_tac, loop_tacs, finish_tac, unsafe_finish_tac);
 
-fun (Simpset {mss, subgoal_tac, loop_tac,  finish_tac, unsafe_finish_tac})
+fun (Simpset {mss, subgoal_tac, loop_tacs,  finish_tac, unsafe_finish_tac})
     settermless termless =
-  make_ss (Thm.set_termless (mss, termless), subgoal_tac, loop_tac,
+  make_ss (Thm.set_termless (mss, termless), subgoal_tac, loop_tacs,
     finish_tac, unsafe_finish_tac);
 
-fun (Simpset {mss, subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac})
+fun (Simpset {mss, subgoal_tac, loop_tacs, finish_tac, unsafe_finish_tac})
     addsimps rews =
-  let val rews' = flat (map (Thm.mk_rews_of_mss mss) rews) in
-    make_ss (Thm.add_simps (mss, rews'), subgoal_tac, loop_tac,
-      finish_tac, unsafe_finish_tac)
-  end;
+  make_ss (Thm.add_simps (mss, rews), subgoal_tac, loop_tacs,
+           finish_tac, unsafe_finish_tac);
 
-fun (Simpset {mss, subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac})
+fun (Simpset {mss, subgoal_tac, loop_tacs, finish_tac, unsafe_finish_tac})
     delsimps rews =
-  let val rews' = flat (map (Thm.mk_rews_of_mss mss) rews) in
-    make_ss (Thm.del_simps (mss, rews'), subgoal_tac, loop_tac,
-      finish_tac, unsafe_finish_tac)
-  end;
+  make_ss (Thm.del_simps (mss, rews), subgoal_tac, loop_tacs,
+           finish_tac, unsafe_finish_tac);
 
-fun (Simpset {mss, subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac})
+fun (Simpset {mss, subgoal_tac, loop_tacs, finish_tac, unsafe_finish_tac})
     addeqcongs newcongs =
-  make_ss (Thm.add_congs (mss, newcongs), subgoal_tac, loop_tac,
+  make_ss (Thm.add_congs (mss, newcongs), subgoal_tac, loop_tacs,
     finish_tac, unsafe_finish_tac);
 
-fun (Simpset {mss, subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac})
+fun (Simpset {mss, subgoal_tac, loop_tacs, finish_tac, unsafe_finish_tac})
     deleqcongs oldcongs =
-  make_ss (Thm.del_congs (mss, oldcongs), subgoal_tac, loop_tac,
+  make_ss (Thm.del_congs (mss, oldcongs), subgoal_tac, loop_tacs,
     finish_tac, unsafe_finish_tac);
 
-fun (Simpset {mss, subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac})
+fun (Simpset {mss, subgoal_tac, loop_tacs, finish_tac, unsafe_finish_tac})
     addsimprocs simprocs =
   make_ss
     (Thm.add_simprocs (mss, map rep_simproc simprocs),
-      subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac);
+      subgoal_tac, loop_tacs, finish_tac, unsafe_finish_tac);
 
-fun (Simpset {mss, subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac})
+fun (Simpset {mss, subgoal_tac, loop_tacs, finish_tac, unsafe_finish_tac})
     delsimprocs simprocs =
   make_ss
     (Thm.del_simprocs (mss, map rep_simproc simprocs),
-      subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac);
+      subgoal_tac, loop_tacs, finish_tac, unsafe_finish_tac);
 
 
 (* merge simpsets *)	(*NOTE: ignores tactics of 2nd simpset*)
 
 fun merge_ss
-   (Simpset {mss = mss1, subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac},
-    Simpset {mss = mss2, ...}) =
-  make_ss (Thm.merge_mss (mss1, mss2),
-    subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac);
+   (Simpset {mss = mss1, loop_tacs = loop_tacs1,
+             subgoal_tac, finish_tac, unsafe_finish_tac},
+    Simpset {mss = mss2, loop_tacs = loop_tacs2, ...}) =
+  make_ss (Thm.merge_mss (mss1, mss2), subgoal_tac,
+           foldl overwrite (loop_tacs1,loop_tacs2),
+           finish_tac, unsafe_finish_tac);
 
 
 
@@ -278,24 +277,25 @@
 
 (** simplification tactics **)
 
-fun solve_all_tac (subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac) mss =
+fun solve_all_tac (subgoal_tac, loop_tacs, finish_tac, unsafe_finish_tac) mss =
   let
     val ss =
-      make_ss (mss, subgoal_tac, loop_tac, unsafe_finish_tac, unsafe_finish_tac);
+      make_ss (mss, subgoal_tac, loop_tacs, unsafe_finish_tac, unsafe_finish_tac);
     val solve1_tac = (subgoal_tac ss THEN_ALL_NEW (K no_tac)) 1
   in DEPTH_SOLVE solve1_tac end;
 
+fun loop_tac loop_tacs = FIRST'(map snd loop_tacs);
 
 (*not totally safe: may instantiate unknowns that appear also in other subgoals*)
 fun basic_gen_simp_tac mode =
-  fn (Simpset {mss, subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac}) =>
+  fn (Simpset {mss, subgoal_tac, loop_tacs, finish_tac, unsafe_finish_tac}) =>
     let
       fun simp_loop_tac i =
         asm_rewrite_goal_tac mode
-          (solve_all_tac (subgoal_tac,loop_tac,finish_tac,unsafe_finish_tac))
+          (solve_all_tac (subgoal_tac,loop_tacs,finish_tac,unsafe_finish_tac))
           mss i
         THEN (finish_tac (prems_of_mss mss) i ORELSE
-              TRY ((loop_tac THEN_ALL_NEW simp_loop_tac) i))
+              TRY ((loop_tac loop_tacs THEN_ALL_NEW simp_loop_tac) i))
     in simp_loop_tac end;
 
 fun gen_simp_tac mode (ss as Simpset {unsafe_finish_tac, ...}) =
@@ -321,9 +321,9 @@
 
 (** simplification meta rules **)
 
-fun simp mode (Simpset {mss, subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac}) thm =
+fun simp mode (Simpset {mss, subgoal_tac, loop_tacs, finish_tac, unsafe_finish_tac}) thm =
   let
-    val tacf = solve_all_tac (subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac);
+    val tacf = solve_all_tac (subgoal_tac, loop_tacs, finish_tac, unsafe_finish_tac);
     fun prover m th = apsome fst (Seq.pull (tacf m th));
   in
     Drule.rewrite_thm mode prover mss thm
diff -r 6328d427a339 -r 131989b78417 src/Provers/splitter.ML
--- a/src/Provers/splitter.ML	Sat Feb 28 15:40:03 1998 +0100
+++ b/src/Provers/splitter.ML	Sat Feb 28 15:40:50 1998 +0100
@@ -18,6 +18,8 @@
 
 local
 
+fun split_format_err() = error("Wrong format for split rule");
+
 fun mk_case_split_tac_2 iffD order =
 let
 
@@ -242,7 +244,6 @@
     term_lift_inst_rule (state, i, ixnTs, [((P2, T), abss (cntxt, Ts))], thm)
   end;
 
-
 (*****************************************************************************
    The split-tactic
    
@@ -256,8 +257,8 @@
             (case concl_of thm of _$(t as _$lhs)$_ =>
                (case strip_comb lhs of (Const(a,_),args) =>
                   (a,(thm,fastype_of t,length args))
-                | _ => error("Wrong format for split rule"))
-             | _ => error("Wrong format for split rule"))
+                | _ => split_format_err())
+             | _ => split_format_err())
       val cmap = map const splits;
       fun lift_tac Ts t p st = (rtac (inst_lift Ts t p st trlift i) i) st
       fun lift_split_tac st = st |>
@@ -278,6 +279,16 @@
 
 in split_tac end;
 
+(* FIXME: this junk is only HOL specific and should therefore not go here! *)
+(* const_of_split_thm is used in HOL/simpdata.ML *)
+
+fun const_of_split_thm thm =
+  (case concl_of thm of
+     Const("Trueprop",_) $ (Const("op =", _)$(Var _$t)$_) =>
+        (case strip_comb t of
+           (Const(a,_),_) => a
+         | _              => split_format_err())
+   | _ => split_format_err());
 
 fun mk_case_split_asm_tac split_tac 
 			  (disjE,conjE,exE,contrapos,contrapos2,notnotD) = 
@@ -292,13 +303,7 @@
 
 fun split_asm_tac []     = K no_tac
   | split_asm_tac splits = 
-  let fun const thm =
-            (case concl_of thm of Const ("Trueprop",_)$
-				 (Const ("op =", _)$(Var _$t)$_) =>
-               (case strip_comb t of (Const(a,_),_) => a
-                | _ => error("Wrong format for split rule"))
-             | _ =>    error("Wrong format for split rule"))
-      val cname_list = map const splits;
+  let val cname_list = map const_of_split_thm splits;
       fun is_case (a,_) = a mem cname_list;
       fun tac (t,i) = 
 	  let val n = find_index (exists_Const is_case) 
@@ -330,6 +335,8 @@
 
 in
 
+val const_of_split_thm = const_of_split_thm;
+
 fun mk_case_split_tac iffD = mk_case_split_tac_2 iffD int_ord;
 
 fun mk_case_split_inside_tac iffD = mk_case_split_tac_2 iffD (rev_order o int_ord);