--- a/src/HOL/Auth/Event.thy Wed Jan 04 10:28:31 2006 +0100
+++ b/src/HOL/Auth/Event.thy Wed Jan 04 16:13:53 2006 +0100
@@ -144,6 +144,8 @@
Says_imp_knows_Spy [THEN parts.Inj, THEN revcut_rl, standard]
parts.Body [THEN revcut_rl, standard]
+lemmas Says_imp_analz_Spy = Says_imp_knows_Spy [THEN analz.Inj]
+
text{*Compatibility for the old "spies" function*}
lemmas spies_partsEs = knows_Spy_partsEs
lemmas Says_imp_spies = Says_imp_knows_Spy
--- a/src/HOL/Auth/OtwayRees.thy Wed Jan 04 10:28:31 2006 +0100
+++ b/src/HOL/Auth/OtwayRees.thy Wed Jan 04 16:13:53 2006 +0100
@@ -81,7 +81,7 @@
==> Notes Spy {|Nonce NA, Nonce NB, Key K|} # evso : otway"
-declare Says_imp_knows_Spy [THEN analz.Inj, dest]
+declare Says_imp_analz_Spy [dest]
declare parts.Body [dest]
declare analz_into_parts [dest]
declare Fake_parts_insert_in_Un [dest]
--- a/src/HOL/Auth/Public.thy Wed Jan 04 10:28:31 2006 +0100
+++ b/src/HOL/Auth/Public.thy Wed Jan 04 16:13:53 2006 +0100
@@ -68,7 +68,7 @@
subsection{*Basic properties of @{term pubK} and @{term priK}*}
-lemma [iff]: "(publicKey b A = publicKey c A') = (b=c & A=A')"
+lemma publicKey_inject [iff]: "(publicKey b A = publicKey c A') = (b=c & A=A')"
by (blast dest!: injective_publicKey)
lemma not_symKeys_pubK [iff]: "publicKey b A \<notin> symKeys"
@@ -133,8 +133,9 @@
axioms
sym_shrK [iff]: "shrK X \<in> symKeys" --{*All shared keys are symmetric*}
-(*Injectiveness: Agents' long-term keys are distinct.*)
-declare inj_shrK [THEN inj_eq, iff]
+text{*Injectiveness: Agents' long-term keys are distinct.*}
+lemmas shrK_injective = inj_shrK [THEN inj_eq]
+declare shrK_injective [iff]
lemma invKey_shrK [simp]: "invKey (shrK A) = shrK A"
by (simp add: invKey_K)
--- a/src/HOL/Auth/Yahalom.thy Wed Jan 04 10:28:31 2006 +0100
+++ b/src/HOL/Auth/Yahalom.thy Wed Jan 04 16:13:53 2006 +0100
@@ -83,7 +83,7 @@
\<in> set evs"
-declare Says_imp_knows_Spy [THEN analz.Inj, dest]
+declare Says_imp_analz_Spy [dest]
declare parts.Body [dest]
declare Fake_parts_insert_in_Un [dest]
declare analz_into_parts [dest]
@@ -113,7 +113,8 @@
"[| Gets B X \<in> set evs; evs \<in> yahalom |] ==> X \<in> knows Spy evs"
by (blast dest!: Gets_imp_Says Says_imp_knows_Spy)
-declare Gets_imp_knows_Spy [THEN analz.Inj, dest]
+lemmas Gets_imp_analz_Spy = Gets_imp_knows_Spy [THEN analz.Inj]
+declare Gets_imp_analz_Spy [dest]
text{*Lets us treat YM4 using a similar argument as for the Fake case.*}