src/HOL/Auth/NS_Public_Bad.ML

 qed_spec_mp "new_nonces_not_seen";
 Addsimps [new_nonces_not_seen];
 
 val nonce_not_seen_now = le_refl RSN (2, new_nonces_not_seen) RSN (2,rev_notE);
 
+fun analz_induct_tac i = 
+    etac ns_public.induct i	THEN
+    ALLGOALS (asm_simp_tac 
+	      (!simpset addsimps ([not_parts_not_analz] @ pushes)
+               setloop split_tac [expand_if]));
+
 
 (**** Authenticity properties obtained from NS2 ****)
 
 (*It is impossible to re-use a nonce in both NS1 and NS2, provided the nonce
   is secret.  (Honest users generate fresh nonces.)*)
 goal thy 
  "!!evs. evs : ns_public                       \
 \ ==> Nonce NA ~: analz (sees lost Spy evs) -->           \
 \     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 ([not_parts_not_analz] @ pushes)
-               setloop split_tac [expand_if])));
+by (analz_induct_tac 1);
 (*NS3*)
 by (fast_tac (!claset addSEs partsEs
                       addEs  [nonce_not_seen_now]) 4);
 (*NS2*)
 by (fast_tac (!claset addSEs partsEs

  "!!evs. evs : ns_public                                                    \
 \ ==> Nonce NA ~: analz (sees lost Spy evs) -->                             \
 \     (EX A' B'. ALL A B.                                                   \
 \      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 ([not_parts_not_analz] @ pushes)
-               setloop split_tac [expand_if])));
+by (analz_induct_tac 1);
 (*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);

  "!!evs. [| Crypt(pubK B)  {|Nonce NA, Agent A|}  : parts(sees lost Spy evs); \
 \           Crypt(pubK B') {|Nonce NA, Agent A'|} : parts(sees lost Spy evs); \
 \           Nonce NA ~: analz (sees lost Spy evs);                            \
 \           evs : ns_public |]                                                \
 \        ==> A=A' & B=B'";
-by (dtac lemma 1);
-by (mp_tac 1);
-by (REPEAT (etac exE 1));
-(*Duplicate the assumption*)
-by (forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl 1);
-by (fast_tac (!claset addSDs [spec]) 1);
+by (prove_unique_tac lemma 1);
 qed "unique_NA";
 
 
 (*Secrecy: Spy does not see the nonce sent in msg NS1 if A and B are secure*)
 goal thy 
  "!!evs. [| A ~: lost;  B ~: lost;  evs : ns_public |]   \
 \ ==> 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 ([not_parts_not_analz] @ pushes)
-               setloop split_tac [expand_if])));
+by (analz_induct_tac 1);
 (*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

 goal thy 
  "!!evs. [| A ~: lost;  B ~: lost;  evs : ns_public |]       \
 \ ==> Crypt (pubK A) {|Nonce NA, Nonce NB|} : parts (sees lost Spy evs) \
 \     --> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set_of_list evs \
 \     --> Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set_of_list evs";
-by (etac ns_public.induct 1);
+by (analz_induct_tac 1);
 by (ALLGOALS Asm_simp_tac);
 (*NS1*)
 by (fast_tac (!claset addSEs partsEs
                       addSDs [new_nonces_not_seen, 
 			      Says_imp_sees_Spy' RS parts.Inj]) 2);

 goal thy 
  "!!evs. evs : ns_public                   \
 \    ==> Nonce NA ~: analz (sees lost Spy evs) --> \
 \        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 ([not_parts_not_analz] @ pushes)
-               setloop split_tac [expand_if])));
+by (analz_induct_tac 1);
 (*Fake*)
 by (best_tac (!claset addSIs [disjI2]
 		      addSDs [impOfSubs Fake_parts_insert]
 		      addIs  [analz_insertI]
 		      addDs  [impOfSubs analz_subset_parts]

  "!!evs. evs : ns_public                                                    \
 \ ==> Nonce NB ~: analz (sees lost Spy evs) -->                             \
 \     (EX A' NA'. ALL A NA.                                                 \
 \      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 ([not_parts_not_analz] @ pushes)
-               setloop split_tac [expand_if])));
+by (analz_induct_tac 1);
 (*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);

  "!!evs. [| Crypt(pubK A) {|Nonce NA, Nonce NB|}  : parts(sees lost Spy evs); \
 \           Crypt(pubK A'){|Nonce NA', Nonce NB|} : parts(sees lost Spy evs); \
 \           Nonce NB ~: analz (sees lost Spy evs);                            \
 \           evs : ns_public |]                                                \
 \        ==> A=A' & NA=NA'";
-by (dtac lemma 1);
-by (mp_tac 1);
-by (REPEAT (etac exE 1));
-(*Duplicate the assumption*)
-by (forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl 1);
-by (fast_tac (!claset addSDs [spec]) 1);
+by (prove_unique_tac lemma 1);
 qed "unique_NB";
 
 
 (*NB remains secret PROVIDED Alice never responds with round 3*)
 goal thy 
  "!!evs. [| A ~: lost;  B ~: lost;  evs : ns_public |]   \
 \ ==> Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set_of_list evs --> \
 \     (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 ([not_parts_not_analz] @ pushes)
-               setloop split_tac [expand_if])));
+by (analz_induct_tac 1);
 (*NS1*)
 by (fast_tac (!claset addSEs partsEs
                       addSDs [new_nonces_not_seen, 
 			      Says_imp_sees_Spy' RS parts.Inj]) 2);
 (*Fake*)

 goal thy 
  "!!evs. [| A ~: lost;  B ~: lost;  evs : ns_public |]       \
 \ ==> Crypt (pubK B) (Nonce NB) : parts (sees lost Spy evs) \
 \     --> Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set_of_list evs \
 \     --> (EX C. Says A C (Crypt (pubK C) (Nonce NB)) : set_of_list evs)";
-by (etac ns_public.induct 1);
+by (analz_induct_tac 1);
 by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib])));
 by (ALLGOALS Asm_simp_tac);
 (*NS1*)
 by (fast_tac (!claset addSEs partsEs
                       addSDs [new_nonces_not_seen, 

 (*Can we strengthen the secrecy theorem?  NO*)
 goal thy 
  "!!evs. [| A ~: lost;  B ~: lost;  evs : ns_public |]   \
 \ ==> 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 ([not_parts_not_analz] @ pushes)
-               setloop split_tac [expand_if])));
+by (analz_induct_tac 1);
 (*NS1*)
 by (fast_tac (!claset addSEs partsEs
                       addSDs [new_nonces_not_seen, 
 			      Says_imp_sees_Spy' RS parts.Inj]) 2);
 (*Fake*)