# HG changeset patch
# User paulson
# Date 844937246 -7200
# Node ID b56425a385b9ac6acbba0f7f9e79629c4d209f84
# Parent  8659e3063a3054915a3fe822442205e5fadd1a95
Tidied some proofs: changed needed for de Morgan laws

diff -r 8659e3063a30 -r b56425a385b9 src/HOL/IOA/ABP/Correctness.ML
--- a/src/HOL/IOA/ABP/Correctness.ML	Thu Oct 10 10:46:14 1996 +0200
+++ b/src/HOL/IOA/ABP/Correctness.ML	Thu Oct 10 10:47:26 1996 +0200
@@ -137,19 +137,12 @@
 by (List.list.induct_tac "l" 1);
 by (Simp_tac 1);
 by (case_tac "list=[]" 1);
- by (asm_full_simp_tac (!simpset addsimps [reverse_Nil,reverse_Cons]) 1);
-by (rtac (expand_if RS ssubst) 1);
- by (Fast_tac 1);
- by (rtac impI 1);
-by (Simp_tac 1);
-by (cut_inst_tac [("l","list")] cons_not_nil 1);
- by (asm_full_simp_tac impl_ss 1);
- by (REPEAT (etac exE 1));
- by (hyp_subst_tac 1);
-by (asm_full_simp_tac (impl_ss addsimps [last_ind_on_first,l_iff_red_nil]) 1);
-by (rtac (expand_if RS ssubst) 1);
-by (rtac (expand_if RS ssubst) 1);
-by (asm_full_simp_tac impl_ss 1);
+by (cut_inst_tac [("l","list")] cons_not_nil 2);
+by (asm_full_simp_tac (!simpset setloop split_tac [expand_if]) 1);
+by (auto_tac (!claset, 
+	      impl_ss addsimps [last_ind_on_first,l_iff_red_nil] 
+                      setloop split_tac [expand_if]));
+by (asm_full_simp_tac (!simpset setloop split_tac [expand_if]) 1);
 qed"reduce_hd";
 
 
@@ -166,11 +159,9 @@
 by (rtac (expand_if RS ssubst) 1);
 by (rtac conjI 1);
 by (simp_tac (!simpset addsimps [and_de_morgan_and_absorbe]) 2);
-by (ALLGOALS (EVERY'[rtac impI,etac conjE,cut_inst_tac [("l","xs")] cons_not_nil,Asm_full_simp_tac]));
-by (REPEAT (etac exE 1));
-by (REPEAT (etac exE 2));
-by (REPEAT(hyp_subst_tac 2));
-by (ALLGOALS (Asm_full_simp_tac));
+by (Step_tac 1);
+by (ALLGOALS (cut_inst_tac [("l","xs")] cons_not_nil));
+by (Auto_tac());
 val reduce_tl =result();
 
 
diff -r 8659e3063a30 -r b56425a385b9 src/HOL/Integ/Integ.ML
--- a/src/HOL/Integ/Integ.ML	Thu Oct 10 10:46:14 1996 +0200
+++ b/src/HOL/Integ/Integ.ML	Thu Oct 10 10:47:26 1996 +0200
@@ -638,13 +638,7 @@
 by (asm_full_simp_tac
     (!simpset addsimps [zadd, zminus, Image_iff, Bex_def]) 1);
 by (res_inst_tac [("m1", "x+ya"), ("n1", "xa+y")] (less_linear RS disjE) 1);
-by (etac disjE 2);
-by (assume_tac 2);
-by (DEPTH_SOLVE
-    (swap_res_tac [exI] 1 THEN 
-     swap_res_tac [exI] 1 THEN 
-     etac conjI 1 THEN 
-     simp_tac (!simpset addsimps add_ac)  1));
+by (REPEAT (fast_tac (!claset addss (!simpset addsimps add_ac)) 1));
 qed "zless_linear";
 
 
diff -r 8659e3063a30 -r b56425a385b9 src/HOL/Lambda/Eta.ML
--- a/src/HOL/Lambda/Eta.ML	Thu Oct 10 10:46:14 1996 +0200
+++ b/src/HOL/Lambda/Eta.ML	Thu Oct 10 10:47:26 1996 +0200
@@ -185,17 +185,17 @@
 qed "decr_Fun";
 Addsimps [decr_Fun];
 
-goal Eta.thy "!i. ~free t (Suc i) --> decr t i = decr t (Suc i)";
+goal Eta.thy "!i. ~free t (Suc i) --> decr t (Suc i) = decr t i";
 by (db.induct_tac "t" 1);
-by (ALLGOALS(asm_simp_tac (addsplit (!simpset) addsimps [le_def, less_Suc_eq])));
-by (fast_tac HOL_cs 1);
-qed "decr_not_free";
+by (ALLGOALS
+    (asm_simp_tac (addsplit (!simpset) addsimps [le_def, less_Suc_eq])));
+qed_spec_mp "decr_not_free";
 Addsimps [decr_not_free];
 
 goal Eta.thy "!!s t. s -e> t ==> (!i. lift s i -e> lift t i)";
 by (etac eta.induct 1);
 by (ALLGOALS(asm_simp_tac (addsplit (!simpset) addsimps [decr_def])));
-by (asm_simp_tac (addsplit (!simpset) addsimps [subst_decr]) 1);
+by (asm_simp_tac (!simpset addsimps [subst_decr]) 1);
 qed_spec_mp "eta_lift";
 Addsimps [eta_lift];
 
diff -r 8659e3063a30 -r b56425a385b9 src/HOL/MiniML/W.ML
--- a/src/HOL/MiniML/W.ML	Thu Oct 10 10:46:14 1996 +0200
+++ b/src/HOL/MiniML/W.ML	Thu Oct 10 10:47:26 1996 +0200
@@ -217,6 +217,7 @@
   addss !simpset) 1); 
 qed_spec_mp "free_tv_W"; 
 
+
 (* Completeness of W w.r.t. has_type *)
 goal thy
  "!s' a t' n. $s' a |- e :: t' --> new_tv n a -->     \
@@ -330,7 +331,7 @@
 by (dtac eq_subst_tel_eq_free 2);
 by (fast_tac (HOL_cs addIs [free_tv_W,free_tv_le_new_tv] addDs [new_tv_W]) 2);
 by (asm_full_simp_tac (!simpset addsimps [free_tv_subst,dom_def,de_Morgan_disj]) 2);
-
+(** LEVEL 74 **)
 by (asm_simp_tac (!simpset setloop (split_tac [expand_bind])) 1); 
 by (safe_tac HOL_cs );
 by (dtac mgu_Ok 1);
@@ -348,6 +349,7 @@
 by (res_inst_tac [("ts2","($ sa ($ s a))")] ((subst_comp_tel RS sym) RSN 
     (2,trans)) 1);
 by ( asm_full_simp_tac (!simpset addsimps [o_def,eq_sym_conv]) 1);
+(** LEVEL 90 **)
 by (rtac eq_free_eq_subst_tel 1);
 by ( safe_tac HOL_cs );
 by (subgoal_tac "ma ~= na" 1);
@@ -358,6 +360,7 @@
 by (( forw_inst_tac [("n","m")] (sym RSN (2,new_tv_W)) 2) THEN (atac 2));
 by (etac conjE 2);
 by (dtac (free_tv_app_subst_tel RS subsetD) 2);
+(** LEVEL 100 **)
 by (fast_tac (set_cs addDs [W_var_geD,new_tv_list_le,codD,
     new_tv_not_free_tv]) 2);
 by (case_tac "na: free_tv t - free_tv sa" 1);
@@ -367,8 +370,10 @@
 by (asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
 by (dtac (free_tv_app_subst_tel RS subsetD) 1);
 by (fast_tac (set_cs addDs [codD,subst_comp_tel RSN (2,trans),
-    eq_subst_tel_eq_free] addss ((!simpset addsimps 
-    [de_Morgan_disj,free_tv_subst,dom_def]))) 1);
+			    eq_subst_tel_eq_free] 
+       addss ((!simpset addsimps [de_Morgan_disj,free_tv_subst,dom_def]))) 1);
+(** LEVEL 106 **)
+by (Fast_tac 1);
 qed_spec_mp "W_complete_lemma";
 
 goal W.thy