# HG changeset patch
# User paulson
# Date 962182150 -7200
# Node ID 74d403974c8da59a163c8091e3198edcfce64341
# Parent  f46f407080f8d8e986794307ba9177f2cd0b6c24
tidied

diff -r f46f407080f8 -r 74d403974c8d src/HOL/Auth/Yahalom.ML
--- a/src/HOL/Auth/Yahalom.ML	Wed Jun 28 10:48:27 2000 +0200
+++ b/src/HOL/Auth/Yahalom.ML	Wed Jun 28 10:49:10 2000 +0200
@@ -492,9 +492,8 @@
 	                 [analz_insert_eq, analz_insert_freshK])));
 (*Prove YM3 by showing that no NB can also be an NA*)
 by (blast_tac (claset() addDs [Says_imp_knows_Spy RS parts.Inj]
-	                addSEs [MPair_parts]
-		        addDs  [no_nonce_YM1_YM2, Gets_imp_Says,
-				Says_unique_NB]) 4);
+	                addSEs [no_nonce_YM1_YM2, MPair_parts]
+		        addDs  [Gets_imp_Says, Says_unique_NB]) 4);
 (*YM2: similar freshness reasoning*) 
 by (blast_tac (claset() addSEs partsEs
 		        addDs  [Gets_imp_Says,
@@ -527,9 +526,9 @@
 (*case NB ~= NBa*)
 by (asm_simp_tac (simpset() addsimps [single_Nonce_secrecy]) 1);
 by (Clarify_tac 1);
-by (blast_tac (claset() addSEs [MPair_parts]
-		        addDs  [Says_imp_knows_Spy RS parts.Inj, 
-			        no_nonce_YM1_YM2 (*to prove NB~=NAa*) ]) 1);
+by (blast_tac (claset() addSEs [MPair_parts, no_nonce_YM1_YM2]
+                                             (*to prove NB~=NAa*)
+		        addDs  [Says_imp_knows_Spy RS parts.Inj]) 1);
 bind_thm ("Spy_not_see_NB", result() RSN(2,rev_mp) RSN(2,rev_mp));
 
 
diff -r f46f407080f8 -r 74d403974c8d src/HOL/IOA/IOA.ML
--- a/src/HOL/IOA/IOA.ML	Wed Jun 28 10:48:27 2000 +0200
+++ b/src/HOL/IOA/IOA.ML	Wed Jun 28 10:49:10 2000 +0200
@@ -8,8 +8,6 @@
 
 Addsimps [Let_def];
 
-open IOA Asig;
-
 val ioa_projections = [asig_of_def, starts_of_def, trans_of_def];
 
 val exec_rws = [executions_def,is_execution_fragment_def];
@@ -65,13 +63,8 @@
    by (Simp_tac 1);
   by (Asm_full_simp_tac 1);
   by (rtac allI 1);
-  by (res_inst_tac [("m","na"),("n","n")] (make_elim less_linear) 1);
-  by (etac disjE 1);
-   by (asm_simp_tac (simpset() addsimps [less_Suc_eq]) 1);
-  by (etac disjE 1);
-   by (Asm_simp_tac 1);
-  by (ftac less_not_sym 1);
-  by (asm_simp_tac (simpset() addsimps [less_not_refl2,less_Suc_eq]) 1);
+  by (cut_inst_tac [("m","na"),("n","n")] less_linear 1);
+  by Auto_tac;
 qed "reachable_n";
 
 val [p1,p2] = goalw IOA.thy [invariant_def]
@@ -94,7 +87,7 @@
 
 val [p1,p2] = goal IOA.thy
  "[| !!s. s : starts_of(A) ==> P(s); \
-\   !!s t a. reachable A s ==> P(s) --> (s,a,t):trans_of(A) --> P(t) \
+\    !!s t a. reachable A s ==> P(s) --> (s,a,t):trans_of(A) --> P(t) \
 \ |] ==> invariant A P";
   by (fast_tac (claset() addSIs [invariantI] addSDs [p1,p2]) 1);
 qed "invariantI1";
@@ -137,8 +130,9 @@
 \  (if a:actions(asig_of(D)) then                                            \
 \     (snd(snd(snd(s))),a,snd(snd(snd(t)))):trans_of(D)                      \
 \   else snd(snd(snd(t)))=snd(snd(snd(s)))))";
-  by (simp_tac (simpset() addsimps ([par_def,actions_asig_comp,Pair_fst_snd_eq]@
-                            ioa_projections)) 1);
+  (*SLOW*)
+  by (simp_tac (simpset() addsimps ([par_def,actions_asig_comp,Pair_fst_snd_eq]
+                                    @ ioa_projections)) 1);
 qed "trans_of_par4";
 
 Goal "starts_of(restrict ioa acts) = starts_of(ioa) &     \
diff -r f46f407080f8 -r 74d403974c8d src/HOL/ex/set.ML
--- a/src/HOL/ex/set.ML	Wed Jun 28 10:48:27 2000 +0200
+++ b/src/HOL/ex/set.ML	Wed Jun 28 10:49:10 2000 +0200
@@ -48,7 +48,7 @@
 
 (*** A unique fixpoint theorem --- fast/best/meson all fail ***)
 
-Goal "?!x. f(g(x))=x ==> ?!y. g(f(y))=y";
+Goal "EX! x. f(g(x))=x ==> EX! y. g(f(y))=y";
 by (EVERY1[etac ex1E, rtac ex1I, etac arg_cong,
           rtac subst, atac, etac allE, rtac arg_cong, etac mp, etac arg_cong]);
 qed "";
@@ -56,13 +56,13 @@
 
 (*** Cantor's Theorem: There is no surjection from a set to its powerset. ***)
 
-Goal "~ (? f:: 'a=>'a set. ! S. ? x. f(x) = S)";
+Goal "~ (EX f:: 'a=>'a set. ALL S. EX x. f(x) = S)";
 (*requires best-first search because it is undirectional*)
 by (best_tac (claset() addSEs [equalityCE]) 1);
 qed "cantor1";
 
 (*This form displays the diagonal term*)
-Goal "! f:: 'a=>'a set. ! x. f(x) ~= ?S(f)";
+Goal "ALL f:: 'a=>'a set. ALL x. f(x) ~= ?S(f)";
 by (best_tac (claset() addSEs [equalityCE]) 1);
 uresult();
 
@@ -97,19 +97,18 @@
 \        h = (%z. if z:X then f(z) else g(z)) |]       \
 \     ==> inj(h) & surj(h)";
 by (asm_simp_tac (simpset() addsimps [surj_if_then_else]) 1);
-   (*PROOF FAILED if inj_onD*)
-by (blast_tac (claset() addDs [disj_lemma, sym RSN (2,disj_lemma)]) 1);
+by (blast_tac (claset() addDs [disj_lemma, sym]) 1);
 qed "bij_if_then_else";
 
-Goal "? X. X = - (g``(- (f``X)))";
+Goal "EX X. X = - (g``(- (f``X)))";
 by (rtac exI 1);
 by (rtac lfp_Tarski 1);
 by (REPEAT (ares_tac [monoI, image_mono, Compl_anti_mono] 1));
 qed "decomposition";
 
 val [injf,injg] = goal (the_context ())
-   "[| inj (f:: 'a=>'b);  inj (g:: 'b=>'a) |] ==> \
-\   ? h:: 'a=>'b. inj(h) & surj(h)";
+   "[| inj (f:: 'a=>'b);  inj (g:: 'b=>'a) |] \
+\   ==> EX h:: 'a=>'b. inj(h) & surj(h)";
 by (rtac (decomposition RS exE) 1);
 by (rtac exI 1);
 by (rtac bij_if_then_else 1);