# HG changeset patch
# User paulson
# Date 841912056 -7200
# Node ID 1badf0b0804084827fdbc9be2e8f3a8c597c385d
# Parent  78e5bfcbc1e95165d4c8efbf4ca236f3e46bab16
Simplified some proofs for compatibility with miniscoping

diff -r 78e5bfcbc1e9 -r 1badf0b08040 src/HOL/IOA/NTP/Correctness.ML
--- a/src/HOL/IOA/NTP/Correctness.ML	Thu Sep 05 10:23:55 1996 +0200
+++ b/src/HOL/IOA/NTP/Correctness.ML	Thu Sep 05 10:27:36 1996 +0200
@@ -81,8 +81,7 @@
 by(Action.action.induct_tac "a"  1);
 by(asm_simp_tac (ss' setloop (split_tac [expand_if])) 1);
 by(forward_tac [inv4] 1);
-by(asm_full_simp_tac (!simpset addsimps 
-                 [imp_ex_equiv,neq_Nil_conv,ex_all_equiv]) 1);
+by (fast_tac (!claset addss (!simpset addsimps [neq_Nil_conv])) 1);
 by(simp_tac ss' 1);
 by(simp_tac ss' 1);
 by(simp_tac ss' 1);
@@ -96,7 +95,7 @@
 by(forward_tac [inv2] 1);
 by (etac disjE 1);
 by(Asm_simp_tac 1);
-by(asm_full_simp_tac (!simpset addsimps [imp_ex_equiv,neq_Nil_conv,ex_all_equiv]) 1);
+by (fast_tac (!claset addss (!simpset addsimps [neq_Nil_conv])) 1);
 
 by(asm_simp_tac ss' 1);
 by(forward_tac [inv2] 1);
@@ -110,8 +109,7 @@
 
 by(case_tac "m = hd(sq(sen(s)))" 1);
 
-by(asm_full_simp_tac (!simpset addsimps 
-                     [imp_ex_equiv,neq_Nil_conv,ex_all_equiv]) 1);
+by (fast_tac (!claset addss (!simpset addsimps [neq_Nil_conv])) 1);
 
 by(Asm_full_simp_tac 1);
 by(fast_tac (!claset addSDs [add_leD1 RS leD]) 1);
diff -r 78e5bfcbc1e9 -r 1badf0b08040 src/HOL/IOA/meta_theory/IOA.ML
--- a/src/HOL/IOA/meta_theory/IOA.ML	Thu Sep 05 10:23:55 1996 +0200
+++ b/src/HOL/IOA/meta_theory/IOA.ML	Thu Sep 05 10:27:36 1996 +0200
@@ -59,7 +59,7 @@
 \                         %i.if i<Suc n then snd ex i else t)")] bexI 1);
   by(res_inst_tac [("x","Suc(n)")] exI 1);
   by(Simp_tac 1);
-  by(asm_simp_tac (!simpset (*delsimps [less_Suc_eq]*)) 1);
+  by(Asm_simp_tac 1);
   by(REPEAT(rtac allI 1));
   by(res_inst_tac [("m","na"),("n","n")] (make_elim less_linear) 1);
   be disjE 1;
diff -r 78e5bfcbc1e9 -r 1badf0b08040 src/HOL/IOA/meta_theory/Solve.ML
--- a/src/HOL/IOA/meta_theory/Solve.ML	Thu Sep 05 10:23:55 1996 +0200
+++ b/src/HOL/IOA/meta_theory/Solve.ML	Thu Sep 05 10:27:36 1996 +0200
@@ -88,7 +88,7 @@
 (* case 2: action sequence of || had Some(a) and 
            filtered sequence also       *)
 by (Asm_full_simp_tac 1);
- by (rtac impI 1);
+ by (strip_tac 1);
  by (REPEAT(hyp_subst_tac 1)); 
  by (Asm_full_simp_tac 1);
 (* case 3: action sequence pf || had Some(a) but
@@ -120,7 +120,7 @@
  by (REPEAT(etac exE 1));
  by (case_tac "y:actions(asig_of(C2))" 1);
  by (Asm_full_simp_tac 1);
- by (rtac impI 1);
+ by (strip_tac 1);
  by (REPEAT(hyp_subst_tac 1)); 
  by (Asm_full_simp_tac 1);
  by (Asm_full_simp_tac 1);
@@ -187,37 +187,10 @@
     par_def, starts_of_def,trans_of_def,rename_def]) 1);
 by (REPEAT(rtac allI 1));
 by (cut_inst_tac [("x","fst ex n")] opt_cases 1);
- by (etac disjE 1);
-(* case 1: action sequence of rename C had already a None *)
-by (Asm_full_simp_tac 1);
-(* case 2 *)
-by (REPEAT(etac exE 1));
-by (etac conjE 1);
-by (eres_inst_tac [("x","n")] allE 1);
-by (eres_inst_tac [("x","y")] allE 1);
-by (Asm_full_simp_tac 1);
-by (etac exE 1);
-by (etac conjE 1);
-by (dtac sym 1);
-by (dtac sym 1);
-by (dtac sym 1);
-by (Asm_full_simp_tac 1);
-by (safe_tac (!claset));
+by (Auto_tac());
 qed"reachable_rename_ioa";
 
 
-(* HOL Lemmata - must already exist ! *)
-goal HOL.thy  "(~(A|B)) =(~A&~B)";
- by (Fast_tac 1);
-val disj_demorgan = result();
-goal HOL.thy  "(~(A&B)) =(~A|~B)";
- by (Fast_tac 1);
-val conj_demorgan = result();
-goal HOL.thy  "(~(? x.P x)) =(! x. (~ (P x)))";
- by (Fast_tac 1);
-val neg_ex = result();
-
-
 goal Solve.thy "!!f.[| is_weak_pmap f C A |]\
 \                      ==> (is_weak_pmap f (rename C g) (rename A g))";
 by (asm_full_simp_tac (!simpset addsimps [is_weak_pmap_def]) 1);
@@ -253,14 +226,10 @@
 by (assume_tac 1);
 by (Asm_full_simp_tac 1);
 (* x is internal *)
-by (simp_tac (!simpset addsimps [disj_demorgan,neg_ex,conj_demorgan] addcongs [conj_cong]) 1);
+by (simp_tac (!simpset addsimps [de_Morgan_disj, de_Morgan_conj, not_ex] 
+	               addcongs [conj_cong]) 1);
 by (rtac impI 1);
 by (etac conjE 1);
 by (cut_inst_tac [("C","C"),("g","g"),("s","s")] reachable_rename_ioa 1);
-by (assume_tac 1);
-by (eres_inst_tac [("x","s")] allE 1);
-by (eres_inst_tac [("x","t")] allE 1);
-by (eres_inst_tac [("x","x")] allE 1);
-by (eres_inst_tac [("x","x")] allE 1);
-by (Asm_full_simp_tac 1);
+by (Auto_tac());
 qed"rename_through_pmap";