--- 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));
--- 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) & \
--- 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);