--- 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);
--- 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,