# HG changeset patch
# User paulson
# Date 850731224 -3600
# Node ID 6b6a92d05fb24cfbf9bfd5b7ec94cf5ef37bd505
# Parent  95f275c8476e58fe5fd95344da145c342ed2d37d
New tactics: prove_unique_tac and analz_induct_tac

diff -r 95f275c8476e -r 6b6a92d05fb2 src/HOL/Auth/NS_Public.ML
--- a/src/HOL/Auth/NS_Public.ML	Mon Dec 16 11:08:11 1996 +0100
+++ b/src/HOL/Auth/NS_Public.ML	Mon Dec 16 11:13:44 1996 +0100
@@ -101,6 +101,11 @@
 
 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 ****)
 
@@ -111,11 +116,7 @@
 \ ==> Nonce NA ~: analz (sees lost Spy evs) -->           \
 \     Crypt (pubK B) {|Nonce NA, Agent A|} : parts (sees lost Spy evs) --> \
 \     Crypt (pubK C) {|X, Nonce NA, Agent D|} ~: 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);
@@ -139,11 +140,7 @@
 \     (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));
@@ -179,11 +176,7 @@
  "!!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);
@@ -247,12 +240,7 @@
  "!!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])));
+\        Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set_of_list evs"; by (analz_induct_tac 1);
 (*Fake*)
 by (best_tac (!claset addSIs [disjI2]
 		      addSDs [impOfSubs Fake_parts_insert]
@@ -276,11 +264,7 @@
 \     (EX A' NA' B'. ALL A NA B.                                            \
 \      Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}   \
 \        : parts (sees lost Spy evs)  -->  A=A' & NA=NA' & 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);
 (*NS2*)
 by (expand_case_tac "NB = ?y" 3 THEN
     REPEAT (fast_tac (!claset addSEs (nonce_not_seen_now::partsEs)) 3));
@@ -304,12 +288,7 @@
 \           Nonce NB ~: analz (sees lost Spy evs);           \
 \           evs : ns_public |]                               \
 \        ==> A=A' & NA=NA' & 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_NB";
 
 
@@ -319,11 +298,7 @@
 \ ==> Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}) \
 \       : 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);
 (*NS3*)
 by (fast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
                       addDs  [unique_NB]) 4);
diff -r 95f275c8476e -r 6b6a92d05fb2 src/HOL/Auth/NS_Public_Bad.ML
--- a/src/HOL/Auth/NS_Public_Bad.ML	Mon Dec 16 11:08:11 1996 +0100
+++ b/src/HOL/Auth/NS_Public_Bad.ML	Mon Dec 16 11:13:44 1996 +0100
@@ -106,6 +106,12 @@
 
 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 ****)
 
@@ -116,11 +122,7 @@
 \ ==> 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);
@@ -144,11 +146,7 @@
 \     (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));
@@ -170,12 +168,7 @@
 \           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";
 
 
@@ -184,11 +177,7 @@
  "!!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);
@@ -215,7 +204,7 @@
 \ ==> 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
@@ -254,11 +243,7 @@
 \    ==> 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]
@@ -281,11 +266,7 @@
 \     (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));
@@ -307,12 +288,7 @@
 \           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";
 
 
@@ -322,11 +298,7 @@
 \ ==> 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, 
@@ -363,7 +335,7 @@
 \ ==> 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*)
@@ -407,11 +379,7 @@
  "!!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,