--- a/src/HOL/Auth/NS_Public.ML Fri Dec 13 10:17:35 1996 +0100
+++ b/src/HOL/Auth/NS_Public.ML Fri Dec 13 10:18:48 1996 +0100
@@ -114,7 +114,7 @@
by (etac ns_public.induct 1);
by (ALLGOALS
(asm_simp_tac
- (!simpset addsimps ([analz_subset_parts RS contra_subsetD] @ pushes)
+ (!simpset addsimps ([not_parts_not_analz] @ pushes)
setloop split_tac [expand_if])));
(*NS3*)
by (fast_tac (!claset addSEs partsEs
@@ -123,13 +123,12 @@
by (fast_tac (!claset addSEs partsEs
addEs [nonce_not_seen_now]) 3);
(*Fake*)
-by (best_tac (!claset addIs [impOfSubs (subset_insertI RS analz_mono)]
+by (best_tac (!claset addIs [analz_insertI]
addDs [impOfSubs analz_subset_parts,
impOfSubs Fake_parts_insert]
addss (!simpset)) 2);
(*Base*)
-by (fast_tac (!claset addDs [impOfSubs analz_subset_parts]
- addss (!simpset)) 1);
+by (fast_tac (!claset addss (!simpset)) 1);
bind_thm ("no_nonce_NS1_NS2", result() RSN (2, rev_mp) RSN (2, rev_mp));
@@ -143,7 +142,7 @@
by (etac ns_public.induct 1);
by (ALLGOALS
(asm_simp_tac
- (!simpset addsimps ([analz_subset_parts RS contra_subsetD] @ pushes)
+ (!simpset addsimps ([not_parts_not_analz] @ pushes)
setloop split_tac [expand_if])));
(*NS1*)
by (expand_case_tac "NA = ?y" 3 THEN
@@ -152,7 +151,7 @@
by (fast_tac (!claset addss (!simpset)) 1);
(*Fake*)
by (simp_tac (!simpset addsimps [all_conj_distrib,parts_insert_sees]) 1);
-by (step_tac (!claset addSIs [impOfSubs (subset_insertI RS analz_mono)]) 1);
+by (step_tac (!claset addSIs [analz_insertI]) 1);
by (ex_strip_tac 1);
by (best_tac (!claset delrules [conjI]
addSDs [impOfSubs Fake_parts_insert]
@@ -183,7 +182,7 @@
by (etac ns_public.induct 1);
by (ALLGOALS
(asm_simp_tac
- (!simpset addsimps ([analz_subset_parts RS contra_subsetD] @ pushes)
+ (!simpset addsimps ([not_parts_not_analz] @ pushes)
setloop split_tac [expand_if])));
(*NS3*)
by (fast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
@@ -193,7 +192,7 @@
addSDs [new_nonces_not_seen,
Says_imp_sees_Spy' RS parts.Inj]) 2);
(*Fake*)
-by (REPEAT_FIRST (rtac conjI ORELSE' spy_analz_tac));
+by (REPEAT_FIRST spy_analz_tac);
(*NS2*)
by (Step_tac 1);
by (fast_tac (!claset addSEs partsEs
@@ -252,12 +251,12 @@
by (etac ns_public.induct 1);
by (ALLGOALS
(asm_simp_tac
- (!simpset addsimps ([analz_subset_parts RS contra_subsetD] @ pushes)
+ (!simpset addsimps ([not_parts_not_analz] @ pushes)
setloop split_tac [expand_if])));
(*Fake*)
by (best_tac (!claset addSIs [disjI2]
addSDs [impOfSubs Fake_parts_insert]
- addIs [impOfSubs (subset_insertI RS analz_mono)]
+ addIs [analz_insertI]
addDs [impOfSubs analz_subset_parts]
addss (!simpset)) 2);
(*Base*)
@@ -280,7 +279,7 @@
by (etac ns_public.induct 1);
by (ALLGOALS
(asm_simp_tac
- (!simpset addsimps ([analz_subset_parts RS contra_subsetD] @ pushes)
+ (!simpset addsimps ([not_parts_not_analz] @ pushes)
setloop split_tac [expand_if])));
(*NS2*)
by (expand_case_tac "NB = ?y" 3 THEN
@@ -289,7 +288,7 @@
by (fast_tac (!claset addss (!simpset)) 1);
(*Fake*)
by (simp_tac (!simpset addsimps [all_conj_distrib,parts_insert_sees]) 1);
-by (step_tac (!claset addSIs [impOfSubs (subset_insertI RS analz_mono)]) 1);
+by (step_tac (!claset addSIs [analz_insertI]) 1);
by (ex_strip_tac 1);
by (best_tac (!claset delrules [conjI]
addSDs [impOfSubs Fake_parts_insert]
@@ -323,7 +322,7 @@
by (etac ns_public.induct 1);
by (ALLGOALS
(asm_simp_tac
- (!simpset addsimps ([analz_subset_parts RS contra_subsetD] @ pushes)
+ (!simpset addsimps ([not_parts_not_analz] @ pushes)
setloop split_tac [expand_if])));
(*NS3*)
by (fast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
@@ -333,7 +332,7 @@
addSDs [new_nonces_not_seen,
Says_imp_sees_Spy' RS parts.Inj]) 2);
(*Fake*)
-by (REPEAT_FIRST (rtac conjI ORELSE' spy_analz_tac));
+by (REPEAT_FIRST spy_analz_tac);
(*NS2*)
by (Step_tac 1);
by (fast_tac (!claset addSEs partsEs
--- a/src/HOL/Auth/NS_Public_Bad.ML Fri Dec 13 10:17:35 1996 +0100
+++ b/src/HOL/Auth/NS_Public_Bad.ML Fri Dec 13 10:18:48 1996 +0100
@@ -119,7 +119,7 @@
by (etac ns_public.induct 1);
by (ALLGOALS
(asm_simp_tac
- (!simpset addsimps ([analz_subset_parts RS contra_subsetD] @ pushes)
+ (!simpset addsimps ([not_parts_not_analz] @ pushes)
setloop split_tac [expand_if])));
(*NS3*)
by (fast_tac (!claset addSEs partsEs
@@ -128,13 +128,12 @@
by (fast_tac (!claset addSEs partsEs
addEs [nonce_not_seen_now]) 3);
(*Fake*)
-by (best_tac (!claset addIs [impOfSubs (subset_insertI RS analz_mono)]
+by (best_tac (!claset addIs [analz_insertI]
addDs [impOfSubs analz_subset_parts,
impOfSubs Fake_parts_insert]
addss (!simpset)) 2);
(*Base*)
-by (fast_tac (!claset addDs [impOfSubs analz_subset_parts]
- addss (!simpset)) 1);
+by (fast_tac (!claset addss (!simpset)) 1);
bind_thm ("no_nonce_NS1_NS2", result() RSN (2, rev_mp) RSN (2, rev_mp));
@@ -148,7 +147,7 @@
by (etac ns_public.induct 1);
by (ALLGOALS
(asm_simp_tac
- (!simpset addsimps ([analz_subset_parts RS contra_subsetD] @ pushes)
+ (!simpset addsimps ([not_parts_not_analz] @ pushes)
setloop split_tac [expand_if])));
(*NS1*)
by (expand_case_tac "NA = ?y" 3 THEN
@@ -157,7 +156,7 @@
by (fast_tac (!claset addss (!simpset)) 1);
(*Fake*)
by (simp_tac (!simpset addsimps [all_conj_distrib,parts_insert_sees]) 1);
-by (step_tac (!claset addSIs [impOfSubs (subset_insertI RS analz_mono)]) 1);
+by (step_tac (!claset addSIs [analz_insertI]) 1);
by (ex_strip_tac 1);
by (best_tac (!claset delrules [conjI]
addSDs [impOfSubs Fake_parts_insert]
@@ -188,7 +187,7 @@
by (etac ns_public.induct 1);
by (ALLGOALS
(asm_simp_tac
- (!simpset addsimps ([analz_subset_parts RS contra_subsetD] @ pushes)
+ (!simpset addsimps ([not_parts_not_analz] @ pushes)
setloop split_tac [expand_if])));
(*NS3*)
by (fast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
@@ -198,7 +197,7 @@
addSDs [new_nonces_not_seen,
Says_imp_sees_Spy' RS parts.Inj]) 2);
(*Fake*)
-by (REPEAT_FIRST (rtac conjI ORELSE' spy_analz_tac));
+by (REPEAT_FIRST spy_analz_tac);
(*NS2*)
by (Step_tac 1);
by (fast_tac (!claset addSEs partsEs
@@ -258,12 +257,12 @@
by (etac ns_public.induct 1);
by (ALLGOALS
(asm_simp_tac
- (!simpset addsimps ([analz_subset_parts RS contra_subsetD] @ pushes)
+ (!simpset addsimps ([not_parts_not_analz] @ pushes)
setloop split_tac [expand_if])));
(*Fake*)
by (best_tac (!claset addSIs [disjI2]
addSDs [impOfSubs Fake_parts_insert]
- addIs [impOfSubs (subset_insertI RS analz_mono)]
+ addIs [analz_insertI]
addDs [impOfSubs analz_subset_parts]
addss (!simpset)) 2);
(*Base*)
@@ -285,7 +284,7 @@
by (etac ns_public.induct 1);
by (ALLGOALS
(asm_simp_tac
- (!simpset addsimps ([analz_subset_parts RS contra_subsetD] @ pushes)
+ (!simpset addsimps ([not_parts_not_analz] @ pushes)
setloop split_tac [expand_if])));
(*NS2*)
by (expand_case_tac "NB = ?y" 3 THEN
@@ -294,7 +293,7 @@
by (fast_tac (!claset addss (!simpset)) 1);
(*Fake*)
by (simp_tac (!simpset addsimps [all_conj_distrib,parts_insert_sees]) 1);
-by (step_tac (!claset addSIs [impOfSubs (subset_insertI RS analz_mono)]) 1);
+by (step_tac (!claset addSIs [analz_insertI]) 1);
by (ex_strip_tac 1);
by (best_tac (!claset delrules [conjI]
addSDs [impOfSubs Fake_parts_insert]
@@ -326,14 +325,14 @@
by (etac ns_public.induct 1);
by (ALLGOALS
(asm_simp_tac
- (!simpset addsimps ([analz_subset_parts RS contra_subsetD] @ pushes)
+ (!simpset addsimps ([not_parts_not_analz] @ pushes)
setloop split_tac [expand_if])));
(*NS1*)
by (fast_tac (!claset addSEs partsEs
addSDs [new_nonces_not_seen,
Says_imp_sees_Spy' RS parts.Inj]) 2);
(*Fake*)
-by (REPEAT_FIRST (rtac conjI ORELSE' spy_analz_tac));
+by (REPEAT_FIRST spy_analz_tac);
(*NS2 and NS3*)
by (Step_tac 1);
(*NS2*)
@@ -411,14 +410,14 @@
by (etac ns_public.induct 1);
by (ALLGOALS
(asm_simp_tac
- (!simpset addsimps ([analz_subset_parts RS contra_subsetD] @ pushes)
+ (!simpset addsimps ([not_parts_not_analz] @ pushes)
setloop split_tac [expand_if])));
(*NS1*)
by (fast_tac (!claset addSEs partsEs
addSDs [new_nonces_not_seen,
Says_imp_sees_Spy' RS parts.Inj]) 2);
(*Fake*)
-by (REPEAT_FIRST (rtac conjI ORELSE' spy_analz_tac));
+by (REPEAT_FIRST spy_analz_tac);
(*NS2 and NS3*)
by (Step_tac 1);
(*NS2*)
--- a/src/HOL/Auth/NS_Shared.ML Fri Dec 13 10:17:35 1996 +0100
+++ b/src/HOL/Auth/NS_Shared.ML Fri Dec 13 10:18:48 1996 +0100
@@ -362,7 +362,7 @@
by analz_Fake_tac;
by (ALLGOALS
(asm_simp_tac
- (!simpset addsimps ([analz_subset_parts RS contra_subsetD,
+ (!simpset addsimps ([not_parts_not_analz,
analz_insert_Key_newK] @ pushes)
setloop split_tac [expand_if])));
(*NS2*)
@@ -370,7 +370,7 @@
addEs [Says_imp_old_keys RS less_irrefl]
addss (!simpset)) 2);
(*OR4, OR2, Fake*)
-by (REPEAT_FIRST (resolve_tac [conjI, impI] ORELSE' spy_analz_tac));
+by (REPEAT_FIRST spy_analz_tac);
(*NS3 and Oops subcases*) (**LEVEL 7 **)
by (step_tac (!claset delrules [impCE]) 1);
by (full_simp_tac (!simpset addsimps [all_conj_distrib]) 2);