src/HOL/Auth/Guard/Guard_Public.thy
changeset 35416 d8d7d1b785af
parent 20217 25b068a99d2b
child 35418 83b0f75810f0
     1.1 --- a/src/HOL/Auth/Guard/Guard_Public.thy	Wed Feb 24 11:55:52 2010 +0100
     1.2 +++ b/src/HOL/Auth/Guard/Guard_Public.thy	Mon Mar 01 13:40:23 2010 +0100
     1.3 @@ -19,7 +19,7 @@
     1.4  
     1.5  subsubsection{*signature*}
     1.6  
     1.7 -constdefs sign :: "agent => msg => msg"
     1.8 +definition sign :: "agent => msg => msg" where
     1.9  "sign A X == {|Agent A, X, Crypt (priK A) (Hash X)|}"
    1.10  
    1.11  lemma sign_inj [iff]: "(sign A X = sign A' X') = (A=A' & X=X')"
    1.12 @@ -27,7 +27,7 @@
    1.13  
    1.14  subsubsection{*agent associated to a key*}
    1.15  
    1.16 -constdefs agt :: "key => agent"
    1.17 +definition agt :: "key => agent" where
    1.18  "agt K == @A. K = priK A | K = pubK A"
    1.19  
    1.20  lemma agt_priK [simp]: "agt (priK A) = A"
    1.21 @@ -57,7 +57,7 @@
    1.22  
    1.23  subsubsection{*sets of private keys*}
    1.24  
    1.25 -constdefs priK_set :: "key set => bool"
    1.26 +definition priK_set :: "key set => bool" where
    1.27  "priK_set Ks == ALL K. K:Ks --> (EX A. K = priK A)"
    1.28  
    1.29  lemma in_priK_set: "[| priK_set Ks; K:Ks |] ==> EX A. K = priK A"
    1.30 @@ -71,7 +71,7 @@
    1.31  
    1.32  subsubsection{*sets of good keys*}
    1.33  
    1.34 -constdefs good :: "key set => bool"
    1.35 +definition good :: "key set => bool" where
    1.36  "good Ks == ALL K. K:Ks --> agt K ~:bad"
    1.37  
    1.38  lemma in_good: "[| good Ks; K:Ks |] ==> agt K ~:bad"
    1.39 @@ -99,7 +99,7 @@
    1.40  
    1.41  subsubsection{*function giving a new nonce*}
    1.42  
    1.43 -constdefs new :: "event list => nat"
    1.44 +definition new :: "event list => nat" where
    1.45  "new evs == Suc (greatest evs)"
    1.46  
    1.47  lemma new_isnt_used [iff]: "Nonce (new evs) ~:used evs"
    1.48 @@ -151,7 +151,7 @@
    1.49  
    1.50  subsubsection{*regular protocols*}
    1.51  
    1.52 -constdefs regular :: "event list set => bool"
    1.53 +definition regular :: "event list set => bool" where
    1.54  "regular p == ALL evs A. evs:p --> (Key (priK A):parts (spies evs)) = (A:bad)"
    1.55  
    1.56  lemma priK_parts_iff_bad [simp]: "[| evs:p; regular p |] ==>