a few more named lemmas
authorpaulson
Wed Jan 04 16:13:53 2006 +0100 (2006-01-04)
changeset 18570ffce25f9aa7f
parent 18569 cf0edebe540c
child 18571 4927aa1feb23
a few more named lemmas
src/HOL/Auth/Event.thy
src/HOL/Auth/OtwayRees.thy
src/HOL/Auth/Public.thy
src/HOL/Auth/Yahalom.thy
     1.1 --- a/src/HOL/Auth/Event.thy	Wed Jan 04 10:28:31 2006 +0100
     1.2 +++ b/src/HOL/Auth/Event.thy	Wed Jan 04 16:13:53 2006 +0100
     1.3 @@ -144,6 +144,8 @@
     1.4       Says_imp_knows_Spy [THEN parts.Inj, THEN revcut_rl, standard] 
     1.5       parts.Body [THEN revcut_rl, standard]
     1.6  
     1.7 +lemmas Says_imp_analz_Spy = Says_imp_knows_Spy [THEN analz.Inj]
     1.8 +
     1.9  text{*Compatibility for the old "spies" function*}
    1.10  lemmas spies_partsEs = knows_Spy_partsEs
    1.11  lemmas Says_imp_spies = Says_imp_knows_Spy
     2.1 --- a/src/HOL/Auth/OtwayRees.thy	Wed Jan 04 10:28:31 2006 +0100
     2.2 +++ b/src/HOL/Auth/OtwayRees.thy	Wed Jan 04 16:13:53 2006 +0100
     2.3 @@ -81,7 +81,7 @@
     2.4            ==> Notes Spy {|Nonce NA, Nonce NB, Key K|} # evso : otway"
     2.5  
     2.6  
     2.7 -declare Says_imp_knows_Spy [THEN analz.Inj, dest]
     2.8 +declare Says_imp_analz_Spy [dest]
     2.9  declare parts.Body  [dest]
    2.10  declare analz_into_parts [dest]
    2.11  declare Fake_parts_insert_in_Un  [dest]
     3.1 --- a/src/HOL/Auth/Public.thy	Wed Jan 04 10:28:31 2006 +0100
     3.2 +++ b/src/HOL/Auth/Public.thy	Wed Jan 04 16:13:53 2006 +0100
     3.3 @@ -68,7 +68,7 @@
     3.4  
     3.5  subsection{*Basic properties of @{term pubK} and @{term priK}*}
     3.6  
     3.7 -lemma [iff]: "(publicKey b A = publicKey c A') = (b=c & A=A')"
     3.8 +lemma publicKey_inject [iff]: "(publicKey b A = publicKey c A') = (b=c & A=A')"
     3.9  by (blast dest!: injective_publicKey) 
    3.10  
    3.11  lemma not_symKeys_pubK [iff]: "publicKey b A \<notin> symKeys"
    3.12 @@ -133,8 +133,9 @@
    3.13  axioms
    3.14    sym_shrK [iff]: "shrK X \<in> symKeys" --{*All shared keys are symmetric*}
    3.15  
    3.16 -(*Injectiveness: Agents' long-term keys are distinct.*)
    3.17 -declare inj_shrK [THEN inj_eq, iff]
    3.18 +text{*Injectiveness: Agents' long-term keys are distinct.*}
    3.19 +lemmas shrK_injective = inj_shrK [THEN inj_eq]
    3.20 +declare shrK_injective [iff]
    3.21  
    3.22  lemma invKey_shrK [simp]: "invKey (shrK A) = shrK A"
    3.23  by (simp add: invKey_K) 
     4.1 --- a/src/HOL/Auth/Yahalom.thy	Wed Jan 04 10:28:31 2006 +0100
     4.2 +++ b/src/HOL/Auth/Yahalom.thy	Wed Jan 04 16:13:53 2006 +0100
     4.3 @@ -83,7 +83,7 @@
     4.4           \<in> set evs"
     4.5  
     4.6  
     4.7 -declare Says_imp_knows_Spy [THEN analz.Inj, dest]
     4.8 +declare Says_imp_analz_Spy [dest]
     4.9  declare parts.Body  [dest]
    4.10  declare Fake_parts_insert_in_Un  [dest]
    4.11  declare analz_into_parts [dest]
    4.12 @@ -113,7 +113,8 @@
    4.13       "[| Gets B X \<in> set evs; evs \<in> yahalom |]  ==> X \<in> knows Spy evs"
    4.14  by (blast dest!: Gets_imp_Says Says_imp_knows_Spy)
    4.15  
    4.16 -declare Gets_imp_knows_Spy [THEN analz.Inj, dest]
    4.17 +lemmas Gets_imp_analz_Spy = Gets_imp_knows_Spy [THEN analz.Inj]
    4.18 +declare Gets_imp_analz_Spy [dest]
    4.19  
    4.20  
    4.21  text{*Lets us treat YM4 using a similar argument as for the Fake case.*}