src/HOL/Auth/NS_Public_Bad.ML

 \     Crypt (pubK B) {|Nonce NA, Agent A|} : parts (sees lost Spy evs) --> \
 \     Crypt (pubK C) {|NA', Nonce NA|} ~: parts (sees lost Spy evs)";
 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
                       addEs  [nonce_not_seen_now]) 4);
 (*NS2*)
 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));
 
 
 (*Uniqueness for NS1: nonce NA identifies agents A and B*)
 goal thy 

 \      Crypt (pubK B) {|Nonce NA, Agent A|} : parts (sees lost Spy evs) --> \
 \      A=A' & B=B')";
 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
     REPEAT (fast_tac (!claset addSEs (nonce_not_seen_now::partsEs)) 3));
 (*Base*)
 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]
 	              addDs  [impOfSubs analz_subset_parts]
                       addss (!simpset)) 1);

 \ ==> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set_of_list evs \
 \     --> Nonce NA ~: analz (sees lost Spy evs)";
 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]
                       addEs  [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 4);
 (*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*)
 by (Step_tac 1);
 by (fast_tac (!claset addSEs partsEs
                       addSDs [new_nonces_not_seen, 
 			      Says_imp_sees_Spy' RS parts.Inj]) 2);

 \        Crypt (pubK B) {|Nonce NA, Agent A|} : parts (sees lost Spy evs) --> \
 \        Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set_of_list evs";
 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*)
 by (fast_tac (!claset addss (!simpset)) 1);
 qed_spec_mp "B_trusts_NS1";

 \      Crypt (pubK A) {|Nonce NA, Nonce NB|} : parts (sees lost Spy evs) --> \
 \      A=A' & NA=NA')";
 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
     REPEAT (fast_tac (!claset addSEs (nonce_not_seen_now::partsEs)) 3));
 (*Base*)
 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]
 	              addDs  [impOfSubs analz_subset_parts] 
 	              addss (!simpset)) 1);

 \     (ALL C. Says A C (Crypt (pubK C) (Nonce NB)) ~: set_of_list evs) --> \
 \     Nonce NB ~: analz (sees lost Spy evs)";
 by (etac ns_public.induct 1);
 by (ALLGOALS 
     (asm_simp_tac 
-     (!simpset addsimps ([analz_subset_parts RS contra_subsetD] @ 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));
+     (!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 spy_analz_tac);
 (*NS2 and NS3*)
 by (Step_tac 1);
 (*NS2*)
 by (fast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
                       addEs  [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 3);

 \ ==> Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set_of_list evs \
 \     --> Nonce NB ~: analz (sees lost Spy evs)";
 by (etac ns_public.induct 1);
 by (ALLGOALS 
     (asm_simp_tac 
-     (!simpset addsimps ([analz_subset_parts RS contra_subsetD] @ 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));
+     (!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 spy_analz_tac);
 (*NS2 and NS3*)
 by (Step_tac 1);
 (*NS2*)
 by (fast_tac (!claset addSEs partsEs
                       addSDs [new_nonces_not_seen,