# HG changeset patch
# User nipkow
# Date 830180540 -7200
# Node ID e56cdf7117291dcda1a663f13070be990c4526bd
# Parent  8ead1fe65aad1973b1a8ba639fb013a4d4853dda
inserted Suc_less_eq explictly in a few proofs.
inserted o_def explictly in a few proofs because the new split_tac causes
fewer eta-expansions which some of the rewrites need.

Indented proof in I.ML

diff -r 8ead1fe65aad -r e56cdf711729 src/HOL/MiniML/I.ML
--- a/src/HOL/MiniML/I.ML	Fri Apr 19 11:33:24 1996 +0200
+++ b/src/HOL/MiniML/I.ML	Mon Apr 22 15:42:20 1996 +0200
@@ -1,45 +1,40 @@
 open I;
 
-Unify.trace_bound := 45;
-Unify.search_bound := 50;
-
 goal thy
   "! a m s s' t n.  \
 \    (new_tv m a & new_tv m s) --> I e a m s = Ok(s',t,n) -->   \
 \    ( ? r. W e ($ s a) m = Ok(r, $ s' t, n) & s' = ($ r o s) )";
 by (expr.induct_tac "e" 1);
 
-(* case Var n *)
-by (simp_tac (!simpset addsimps [app_subst_list]
-    setloop (split_tac [expand_if])) 1);
-by (fast_tac (HOL_cs addss !simpset) 1);
-
-(* case Abs e *)
-by (asm_full_simp_tac (!simpset setloop (split_tac [expand_bind])) 1);
-by (strip_tac 1);
-by (rtac conjI 1);
+  (* case Var n *)
+  by (simp_tac (!simpset addsimps [app_subst_list]
+      setloop (split_tac [expand_if])) 1);
+  by (fast_tac (HOL_cs addss !simpset) 1);
 
-by (strip_tac 1);
-by (REPEAT (etac allE 1));
-by (etac impE 1);
-by (fast_tac (HOL_cs addss (!simpset addsimps [new_tv_subst])) 2);
-by (fast_tac (HOL_cs addIs [new_tv_Suc_list RS mp,new_tv_subst_le,
-    less_imp_le,lessI]) 1); 
+ (* case Abs e *)
+ by (asm_full_simp_tac (!simpset setloop (split_tac [expand_bind])) 1);
+ by (strip_tac 1);
+ by (rtac conjI 1);
+  by (strip_tac 1);
+  by (REPEAT (etac allE 1));
+  by (etac impE 1);
+   by (fast_tac (HOL_cs addss (!simpset addsimps [new_tv_subst])) 2);
+  by (fast_tac (HOL_cs addIs [new_tv_Suc_list RS mp,new_tv_subst_le,
+                              less_imp_le,lessI]) 1); 
 
-by (strip_tac 1);
-by (REPEAT (etac allE 1));
-by (etac impE 1);
-by (fast_tac (HOL_cs addss (!simpset addsimps [new_tv_subst])) 2);
-by (fast_tac (HOL_cs addIs [new_tv_Suc_list RS mp,new_tv_subst_le,
-    less_imp_le,lessI]) 1); 
+ by (strip_tac 1);
+ by (REPEAT (etac allE 1));
+ by (etac impE 1);
+  by (fast_tac (HOL_cs addss (!simpset addsimps [new_tv_subst])) 2);
+ by (fast_tac (HOL_cs addIs [new_tv_Suc_list RS mp,new_tv_subst_le,
+                             less_imp_le,lessI]) 1);
 
 (* case App e1 e2 *)
 by (simp_tac (!simpset setloop (split_tac [expand_bind])) 1);
 by (strip_tac 1);
 by (rename_tac "s1' t1 n1 s2' t2 n2 sa" 1);
 by (rtac conjI 1);
-by (fast_tac (HOL_cs addss !simpset) 1);
-
+ by (fast_tac (HOL_cs addss !simpset) 1);
 by (strip_tac 1);
 by (rename_tac "s1 t1' n1'" 1);
 by (eres_inst_tac [("x","a")] allE 1);
@@ -54,70 +49,64 @@
 by (eres_inst_tac [("x","s2'")] allE 1);
 by (eres_inst_tac [("x","t2")] allE 1);
 by (eres_inst_tac [("x","n2")] allE 1);
-
 by (rtac conjI 1);
-by (strip_tac 1);
-by (mp_tac 1);
-by (mp_tac 1);
-by (etac exE 1);
-by (etac conjE 1);
-by (etac impE 1);
-by ((forward_tac [new_tv_subst_tel] 1) THEN (atac 1)); 
-by ((dres_inst_tac [("a","$ s a")] new_tv_W 1) THEN (atac 1));
-by (fast_tac (HOL_cs addDs [sym RS W_var_geD,new_tv_subst_le,new_tv_list_le] 
-    addss !simpset) 1);
-by (fast_tac (HOL_cs addss (!simpset addsimps [subst_comp_tel])) 1);
-
+ by (strip_tac 1);
+ by (mp_tac 1);
+ by (mp_tac 1);
+ by (etac exE 1);
+ by (etac conjE 1);
+ by (etac impE 1);
+  by ((forward_tac [new_tv_subst_tel] 1) THEN (atac 1)); 
+  by ((dres_inst_tac [("a","$ s a")] new_tv_W 1) THEN (atac 1));
+  by (fast_tac (HOL_cs addDs [sym RS W_var_geD,new_tv_subst_le,new_tv_list_le] 
+                       addss !simpset) 1);
+ by (fast_tac (HOL_cs addss (!simpset addsimps [subst_comp_tel])) 1);
 by (strip_tac 1);
 by (rename_tac "s2 t2' n2'" 1);
 by (rtac conjI 1);
+ by (strip_tac 1);
+ by (mp_tac 1);
+ by (mp_tac 1);
+ by (etac exE 1);
+ by (etac conjE 1);
+ by (etac impE 1);
+  by ((forward_tac [new_tv_subst_tel] 1) THEN (atac 1)); 
+  by ((dres_inst_tac [("a","$ s a")] new_tv_W 1) THEN (atac 1));
+  by (fast_tac (HOL_cs addDs [sym RS W_var_geD,new_tv_subst_le,new_tv_list_le] 
+                       addss !simpset) 1);
+ by (fast_tac (HOL_cs addss (!simpset addsimps [subst_comp_tel,subst_comp_te])) 1);
 by (strip_tac 1);
 by (mp_tac 1);
 by (mp_tac 1);
 by (etac exE 1);
 by (etac conjE 1);
 by (etac impE 1);
-by ((forward_tac [new_tv_subst_tel] 1) THEN (atac 1)); 
-by ((dres_inst_tac [("a","$ s a")] new_tv_W 1) THEN (atac 1));
-by (fast_tac (HOL_cs addDs [sym RS W_var_geD,new_tv_subst_le,new_tv_list_le] 
-    addss !simpset) 1);
-by (fast_tac (HOL_cs addss (!simpset addsimps [subst_comp_tel,subst_comp_te])) 1);
-
-by (strip_tac 1);
-by (mp_tac 1);
-by (mp_tac 1);
-by (etac exE 1);
-by (etac conjE 1);
-by (etac impE 1);
-by ((forward_tac [new_tv_subst_tel] 1) THEN (atac 1)); 
-by ((dres_inst_tac [("a","$ s a")] new_tv_W 1) THEN (atac 1));
-by (fast_tac (HOL_cs addDs [sym RS W_var_geD,new_tv_subst_le,new_tv_list_le] 
-    addss !simpset) 1);
-
+ by ((forward_tac [new_tv_subst_tel] 1) THEN (atac 1)); 
+ by ((dres_inst_tac [("a","$ s a")] new_tv_W 1) THEN (atac 1));
+ by (fast_tac (HOL_cs addDs [sym RS W_var_geD,new_tv_subst_le,new_tv_list_le] 
+                      addss !simpset) 1);
 by (mp_tac 1);
 by (REPEAT (eresolve_tac [exE,conjE] 1));
-by (REPEAT 
-    ((asm_full_simp_tac (!simpset addsimps [subst_comp_tel,subst_comp_te]) 1) THEN
-     (REPEAT (etac conjE 1)) THEN (hyp_subst_tac 1) ));
+by (REPEAT(EVERY1
+     [asm_full_simp_tac (!simpset addsimps [subst_comp_tel,subst_comp_te]),
+      REPEAT o etac conjE, hyp_subst_tac]));
 by (rtac exI 1);
 by (safe_tac HOL_cs);
-by (fast_tac HOL_cs 1);
-by (Simp_tac 2);
-
+  by (fast_tac HOL_cs 1);
+ by (simp_tac (!simpset addsimps [o_def,subst_comp_te]) 2);
 by (subgoal_tac "new_tv n2 s & new_tv n2 r & new_tv n2 ra" 1);
-by (asm_full_simp_tac (!simpset addsimps [new_tv_subst]) 1);
+ by (asm_full_simp_tac (!simpset addsimps [new_tv_subst]) 1);
 by ((forward_tac [new_tv_subst_tel] 1) THEN (atac 1));
 by ((dres_inst_tac [("a","$ s a")] new_tv_W 1) THEN (atac 1));
 by (safe_tac HOL_cs);
-by (fast_tac (HOL_cs addDs [sym RS W_var_geD,new_tv_subst_le,new_tv_list_le] 
-    addss !simpset) 1);
-by (fast_tac (HOL_cs addDs [sym RS W_var_geD,new_tv_subst_le,new_tv_list_le] 
-    addss !simpset) 1);
+  by (fast_tac (HOL_cs addDs[sym RS W_var_geD,new_tv_subst_le,new_tv_list_le] 
+                       addss !simpset) 1);
+ by (fast_tac (HOL_cs addDs [sym RS W_var_geD,new_tv_subst_le,new_tv_list_le] 
+                      addss !simpset) 1);
 by (dres_inst_tac [("e","expr1")] (sym RS W_var_geD) 1);
 by ((dtac new_tv_subst_tel 1) THEN (atac 1));
 by ((dres_inst_tac [("ts","$ s a")] new_tv_list_le 1) THEN (atac 1));
 by ((dtac new_tv_subst_tel 1) THEN (atac 1));
 by (fast_tac (HOL_cs addDs [new_tv_W] addss 
     (!simpset addsimps [subst_comp_tel])) 1);
-
 qed_spec_mp "I_correct_wrt_W";
diff -r 8ead1fe65aad -r e56cdf711729 src/HOL/MiniML/W.ML
--- a/src/HOL/MiniML/W.ML	Fri Apr 19 11:33:24 1996 +0200
+++ b/src/HOL/MiniML/W.ML	Mon Apr 22 15:42:20 1996 +0200
@@ -12,7 +12,7 @@
 (* stronger version of Suc_leD *)
 goalw Nat.thy [le_def] 
         "!!m. Suc m <= n ==> m < n";
-by (Asm_full_simp_tac 1);
+by (asm_full_simp_tac (!simpset addsimps [less_Suc_eq]) 1);
 by (cut_facts_tac [less_linear] 1);
 by (fast_tac HOL_cs 1);
 qed "Suc_le_lessD";
@@ -42,7 +42,7 @@
 by (simp_tac (HOL_ss addsimps [subst_comp_tel RS sym]) 1);
 by ( (rtac has_type_cl_sub 1) THEN (rtac has_type_cl_sub 1));
 by (asm_full_simp_tac (!simpset addsimps [eq_sym_conv]) 1);
-by (asm_full_simp_tac (!simpset addsimps [subst_comp_tel RS sym,has_type_cl_sub,eq_sym_conv]) 1);
+by (asm_full_simp_tac (!simpset addsimps [subst_comp_tel RS sym,o_def,has_type_cl_sub,eq_sym_conv]) 1);
 qed_spec_mp "W_correct";
 
 val has_type_casesE = map(has_type.mk_cases expr.simps)
@@ -77,7 +77,7 @@
 by (etac conjE 1);
 by (res_inst_tac [("j","na")] le_trans 1); 
 by (Asm_simp_tac 1);
-by (asm_simp_tac (!simpset addsimps [Suc_leD]) 1);
+by (Asm_simp_tac 1);
 qed_spec_mp "W_var_ge";
 
 Addsimps [W_var_ge];
@@ -128,7 +128,7 @@
 by (eres_inst_tac [("x","sa")] allE 1);
 by (eres_inst_tac [("x","ta")] allE 1);
 by (eres_inst_tac [("x","nb")] allE 1);
-by( asm_full_simp_tac (!simpset addsimps [rotate_Ok]) 1);
+by( asm_full_simp_tac (!simpset addsimps [o_def,rotate_Ok]) 1);
 by (rtac conjI 1);
 by (rtac new_tv_subst_comp_2 1);
 by (rtac new_tv_subst_comp_2 1);
@@ -177,7 +177,8 @@
 by (eres_inst_tac [("x","t")] allE 1);
 by (eres_inst_tac [("x","na")] allE 1);
 by (eres_inst_tac [("x","v")] allE 1);
-by (fast_tac (HOL_cs addIs [cod_app_subst] addss !simpset) 1);
+by (fast_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_bind])) 1);
@@ -197,7 +198,7 @@
 by (eres_inst_tac [("x","nb")] allE 1);
 by (eres_inst_tac [("x","v")] allE 1);
 by (safe_tac (empty_cs addSIs [conjI,impI] addSEs [conjE]) ); 
-by (asm_full_simp_tac (!simpset addsimps [rotate_Ok]) 1);
+by (asm_full_simp_tac (!simpset addsimps [rotate_Ok,o_def]) 1);
 by (dtac W_var_geD 1);
 by (dtac W_var_geD 1);
 by ( (forward_tac [less_le_trans] 1) THEN (assume_tac 1) );