# HG changeset patch
# User paulson
# Date 1136387633 -3600
# Node ID ffce25f9aa7f7fa30ebd2ce7ec77e6b6e512c475
# Parent  cf0edebe540c4ed24176601eb5dd00384c95e875
a few more named lemmas

diff -r cf0edebe540c -r ffce25f9aa7f src/HOL/Auth/Event.thy
--- 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
diff -r cf0edebe540c -r ffce25f9aa7f src/HOL/Auth/OtwayRees.thy
--- 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]
diff -r cf0edebe540c -r ffce25f9aa7f src/HOL/Auth/Public.thy
--- 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) 
diff -r cf0edebe540c -r ffce25f9aa7f src/HOL/Auth/Yahalom.thy
--- 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.*}