--- a/src/HOL/MiniML/W.ML Fri Oct 17 15:23:14 1997 +0200
+++ b/src/HOL/MiniML/W.ML Fri Oct 17 15:25:12 1997 +0200
@@ -18,7 +18,7 @@
"!A n S t m. W e A n = Some (S,t,m) --> n<=m";
by (expr.induct_tac "e" 1);
(* case Var(n) *)
-by (simp_tac (!simpset setloop (split_tac [expand_option_bind,expand_if])) 1);
+by (simp_tac (!simpset addsplits [expand_option_bind,expand_if]) 1);
by (strip_tac 1);
by (etac conjE 1);
by (etac conjE 1);
@@ -27,10 +27,10 @@
by (dtac sym 1);
by (Asm_full_simp_tac 1);
(* case Abs e *)
-by (simp_tac (!simpset setloop (split_tac [expand_option_bind])) 1);
+by (simp_tac (!simpset addsplits [expand_option_bind]) 1);
by (fast_tac (HOL_cs addDs [Suc_leD]) 1);
(* case App e1 e2 *)
-by (simp_tac (!simpset setloop (split_tac [expand_option_bind])) 1);
+by (simp_tac (!simpset addsplits [expand_option_bind]) 1);
by (strip_tac 1);
by (rename_tac "S t n1 S1 t1 n2 S2 S3 t2 m" 1);
by (eres_inst_tac [("x","A")] allE 1);
@@ -50,7 +50,7 @@
by (Asm_simp_tac 1);
by (Asm_simp_tac 1);
(* case LET e1 e2 *)
-by (simp_tac (!simpset setloop (split_tac [expand_option_bind])) 1);
+by (simp_tac (!simpset addsplits [expand_option_bind]) 1);
by (strip_tac 1);
by (rename_tac "A n1 S t2 m1 S2 t3 m2 S3 t1 m" 1);
by (REPEAT (etac conjE 1));
@@ -88,7 +88,7 @@
by (assume_tac 2);
by (rtac add_le_mono 1);
by (Simp_tac 1);
-by (simp_tac (!simpset setloop (split_tac [expand_if]) addsimps [max_def]) 1);
+by (simp_tac (!simpset addsplits [expand_if] addsimps [max_def]) 1);
by (strip_tac 1);
by (rtac new_tv_le 1);
by (mp_tac 2);
@@ -96,7 +96,7 @@
by (assume_tac 2);
by (rtac add_le_mono 1);
by (Simp_tac 1);
-by (simp_tac (!simpset setloop (split_tac [expand_if]) addsimps [max_def]) 1);
+by (simp_tac (!simpset addsplits [expand_if] addsimps [max_def]) 1);
by (strip_tac 1);
by (dtac not_leE 1);
by (rtac less_or_eq_imp_le 1);
@@ -111,7 +111,7 @@
\ new_tv m S & new_tv m t";
by (expr.induct_tac "e" 1);
(* case Var n *)
-by (simp_tac (!simpset setloop (split_tac [expand_option_bind,expand_if])) 1);
+by (simp_tac (!simpset addsplits [expand_option_bind,expand_if]) 1);
by (strip_tac 1);
by (REPEAT (etac conjE 1));
by (rtac conjI 1);
@@ -125,14 +125,14 @@
by (Asm_full_simp_tac 1);
(* case Abs e *)
by (simp_tac (!simpset addsimps [new_tv_subst,new_tv_Suc_list]
- setloop (split_tac [expand_option_bind])) 1);
+ addsplits [expand_option_bind]) 1);
by (strip_tac 1);
by (eres_inst_tac [("x","Suc n")] allE 1);
by (eres_inst_tac [("x","(FVar n)#A")] allE 1);
by (fast_tac (HOL_cs addss (!simpset
addsimps [new_tv_subst,new_tv_Suc_list])) 1);
(* case App e1 e2 *)
-by (simp_tac (!simpset setloop (split_tac [expand_option_bind])) 1);
+by (simp_tac (!simpset addsplits [expand_option_bind]) 1);
by (strip_tac 1);
by (rename_tac "S t n1 S1 t1 n2 S2 S3 t2 m" 1);
by (eres_inst_tac [("x","n")] allE 1);
@@ -174,7 +174,7 @@
[new_scheme_list_le,new_tv_subst_scheme_list,new_tv_le]
addss (!simpset)) 1);
(* case LET e1 e2 *)
-by (simp_tac (!simpset setloop (split_tac [expand_option_bind])) 1);
+by (simp_tac (!simpset addsplits [expand_option_bind]) 1);
by (strip_tac 1);
by (rename_tac "n1 A S1 t1 n2 S2 t2 m2 S t m" 1);
by (REPEAT (etac conjE 1));
@@ -239,7 +239,7 @@
by (expr.induct_tac "e" 1);
(* case Var n *)
by (simp_tac (!simpset addsimps
- [free_tv_subst] setloop (split_tac [expand_option_bind,expand_if])) 1);
+ [free_tv_subst] addsplits [expand_option_bind,expand_if]) 1);
by (strip_tac 1);
by (REPEAT (etac conjE 1));
by (hyp_subst_tac 1);
@@ -255,7 +255,7 @@
by (Asm_full_simp_tac 1);
(* case Abs e *)
by (asm_full_simp_tac (!simpset addsimps
- [free_tv_subst] setloop (split_tac [expand_option_bind]) delsimps all_simps) 1);
+ [free_tv_subst] addsplits [expand_option_bind] delsimps all_simps) 1);
by (strip_tac 1);
by (rename_tac "S t n1 S1 t1 m v" 1);
by (eres_inst_tac [("x","Suc n")] allE 1);
@@ -267,7 +267,7 @@
by (best_tac (HOL_cs addIs [cod_app_subst]
addss (!simpset addsimps [less_Suc_eq])) 1);
(* case App e1 e2 *)
-by (simp_tac (!simpset setloop (split_tac [expand_option_bind]) delsimps all_simps) 1);
+by (simp_tac (!simpset addsplits [expand_option_bind] delsimps all_simps) 1);
by (strip_tac 1);
by (rename_tac "S t n1 S1 t1 n2 S2 S3 t2 m v" 1);
by (eres_inst_tac [("x","n")] allE 1);
@@ -303,7 +303,7 @@
addEs [UnE]
addss !simpset) 1);
(* LET e1 e2 *)
-by (simp_tac (!simpset setloop (split_tac [expand_option_bind]) delsimps all_simps) 1);
+by (simp_tac (!simpset addsplits [expand_option_bind] delsimps all_simps) 1);
by (strip_tac 1);
by (rename_tac "nat A S1 t1 n2 S2 t2 m2 S t m v" 1);
by (eres_inst_tac [("x","nat")] allE 1);
@@ -338,7 +338,7 @@
"!A S t m n . new_tv n A --> Some (S,t,m) = W e A n --> $S A |- e :: t";
by (expr.induct_tac "e" 1);
(* case Var n *)
-by (asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
+by (asm_full_simp_tac (!simpset addsplits [expand_if]) 1);
by (strip_tac 1);
by (rtac has_type.VarI 1);
by (Simp_tac 1);
@@ -347,7 +347,7 @@
by (rtac refl 1);
(* case Abs e *)
by (asm_full_simp_tac (!simpset addsimps [app_subst_list]
- setloop (split_tac [expand_option_bind])) 1);
+ addsplits [expand_option_bind]) 1);
by (strip_tac 1);
by (eres_inst_tac [("x","(mk_scheme (TVar n)) # A")] allE 1);
by (Asm_full_simp_tac 1);
@@ -360,7 +360,7 @@
by (Asm_simp_tac 1);
by (assume_tac 1);
(* case App e1 e2 *)
-by (simp_tac (!simpset setloop (split_tac [expand_option_bind])) 1);
+by (simp_tac (!simpset addsplits [expand_option_bind]) 1);
by (strip_tac 1);
by (rename_tac "S1 t1 n1 S2 t2 n2 S3" 1);
by (res_inst_tac [("t2.0","$ S3 t2")] has_type.AppI 1);
@@ -392,7 +392,7 @@
by (mp_tac 1);
by (assume_tac 1);
(* case Let e1 e2 *)
-by (simp_tac (!simpset setloop (split_tac [expand_option_bind])) 1);
+by (simp_tac (!simpset addsplits [expand_option_bind]) 1);
by (strip_tac 1);
by (rename_tac "w q m1 S1 t1 m2 S2 t n2" 1);
by (res_inst_tac [("t1.0","$ S2 t1")] has_type.LETI 1);
@@ -469,8 +469,7 @@
by (expr.induct_tac "e" 1);
(* case Var n *)
by (strip_tac 1);
-by (simp_tac (!simpset addcongs [conj_cong]
- setloop (split_tac [expand_if])) 1);
+by (simp_tac (!simpset addcongs [conj_cong] addsplits [expand_if]) 1);
by (eresolve_tac has_type_casesE 1);
by (asm_full_simp_tac (!simpset addsimps [is_bound_typ_instance]) 1);
by (etac exE 1);
@@ -491,7 +490,7 @@
by (eres_inst_tac [("x","Suc n")] allE 1);
by (best_tac (HOL_cs addSDs [mk_scheme_injective]
addss (!simpset addcongs [conj_cong]
- setloop (split_tac [expand_option_bind]))) 1);
+ addsplits [expand_option_bind])) 1);
(** LEVEL 19 **)
(* case App e1 e2 *)
@@ -531,8 +530,7 @@
by (case_tac "na:free_tv Sa" 2);
(* n1 ~: free_tv S1 *)
by (forward_tac [not_free_impl_id] 3);
-by (asm_simp_tac (!simpset
- setloop (split_tac [expand_if])) 3);
+by (asm_simp_tac (!simpset addsplits [expand_if]) 3);
(* na : free_tv Sa *)
by (dres_inst_tac [("A1","$ S A")] (subst_comp_scheme_list RSN (2,trans)) 2);
by (dtac eq_subst_scheme_list_eq_free 2);
@@ -540,8 +538,7 @@
by (Asm_simp_tac 2);
by (case_tac "na:dom Sa" 2);
(* na ~: dom Sa *)
-by (asm_full_simp_tac (!simpset addsimps [dom_def]
- setloop (split_tac [expand_if])) 3);
+by (asm_full_simp_tac (!simpset addsimps [dom_def] addsplits [expand_if]) 3);
(* na : dom Sa *)
by (rtac eq_free_eq_subst_te 2);
by (strip_tac 2);
@@ -553,7 +550,7 @@
by (fast_tac (set_cs addDs [new_tv_W,new_tv_not_free_tv] addss
(!simpset addsimps [cod_def,free_tv_subst])) 3);
by (fast_tac (set_cs addss (!simpset addsimps [cod_def,free_tv_subst]
- setloop (split_tac [expand_if]))) 2);
+ addsplits [expand_if])) 2);
by (Simp_tac 2);
by (rtac eq_free_eq_subst_te 2);
by (strip_tac 2 );
@@ -564,16 +561,16 @@
by (fast_tac (HOL_cs addDs [new_scheme_list_le,new_tv_subst_scheme_list,new_tv_W,new_tv_not_free_tv]) 3);
by (case_tac "na: free_tv t - free_tv Sa" 2);
(* case na ~: free_tv t - free_tv Sa *)
-by ( asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 3);
+by ( asm_full_simp_tac (!simpset addsplits [expand_if]) 3);
by (Fast_tac 3);
(* case na : free_tv t - free_tv Sa *)
-by ( asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 2);
+by ( asm_full_simp_tac (!simpset addsplits [expand_if]) 2);
by (dres_inst_tac [("A1","$ S A")] (subst_comp_scheme_list RSN (2,trans)) 2);
by (dtac eq_subst_scheme_list_eq_free 2);
by (fast_tac (HOL_cs addIs [free_tv_W,free_tv_le_new_tv] addDs [new_tv_W]) 2);
(** LEVEL 75 **)
by (asm_full_simp_tac (!simpset addsimps [free_tv_subst,dom_def]) 2);
-by (asm_simp_tac (!simpset setloop (split_tac [expand_option_bind])) 1);
+by (asm_simp_tac (!simpset addsplits [expand_option_bind]) 1);
by (safe_tac HOL_cs );
by (dtac mgu_Some 1);
by ( fast_tac (HOL_cs addss !simpset) 1);
@@ -603,9 +600,9 @@
new_tv_not_free_tv]) 2);
by (case_tac "na: free_tv t - free_tv Sa" 1);
(* case na ~: free_tv t - free_tv Sa *)
-by (asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 2);
+by (asm_full_simp_tac (!simpset addsplits [expand_if]) 2);
(* case na : free_tv t - free_tv Sa *)
-by (asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
+by (asm_full_simp_tac (!simpset addsplits [expand_if]) 1);
by (dtac (free_tv_app_subst_scheme_list RS subsetD) 1);
by (fast_tac (set_cs addDs [codD,subst_comp_scheme_list RSN (2,trans),
eq_subst_scheme_list_eq_free] addss ((!simpset addsimps