# HG changeset patch
# User paulson
# Date 850468728 -3600
# Node ID 4148aa5b00a2919cff9b18f4bae5d750f2171155
# Parent  490ffa16952ecb8529054814e1bf7d26a6fbffe3
Streamlined many proofs

diff -r 490ffa16952e -r 4148aa5b00a2 src/HOL/Auth/NS_Public.ML
--- 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
diff -r 490ffa16952e -r 4148aa5b00a2 src/HOL/Auth/NS_Public_Bad.ML
--- 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*)
diff -r 490ffa16952e -r 4148aa5b00a2 src/HOL/Auth/NS_Shared.ML
--- 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);