src/HOL/Auth/Event.thy
changeset 6399 4a9040b85e2e
parent 6308 76f3865a2b1d
child 11104 f2024fed9f0c
     1.1 --- a/src/HOL/Auth/Event.thy	Wed Mar 17 18:01:41 1999 +0100
     1.2 +++ b/src/HOL/Auth/Event.thy	Thu Mar 18 10:41:00 1999 +0100
     1.3 @@ -16,10 +16,10 @@
     1.4  consts  (*Initial states of agents -- parameter of the construction*)
     1.5    initState :: agent => msg set
     1.6  
     1.7 -datatype  (*Messages--could add another constructor for agent knowledge*)
     1.8 +datatype
     1.9    event = Says  agent agent msg
    1.10 +        | Gets  agent       msg
    1.11          | Notes agent       msg
    1.12 -        | Gets  agent       msg
    1.13         
    1.14  consts 
    1.15    bad    :: agent set        (*compromised agents*)
    1.16 @@ -41,21 +41,22 @@
    1.17  
    1.18  primrec
    1.19    knows_Nil   "knows A []         = initState A"
    1.20 -  knows_Cons  "knows A (ev # evs) =
    1.21 -	        (if A = Spy then 
    1.22 -                  (case ev of
    1.23 -		    Says A' B X => insert X (knows Spy evs)
    1.24 -		  | Notes A' X  => 
    1.25 -                   if A' : bad then insert X (knows Spy evs) else knows Spy evs
    1.26 -                  | Gets A' X => knows Spy evs)
    1.27 -                 else
    1.28 -                  (case ev of
    1.29 -		    Says A' B X => 
    1.30 -                      if A'=A then insert X (knows A evs) else knows A evs
    1.31 -		  | Notes A' X    => 
    1.32 -                      if A'=A then insert X (knows A evs) else knows A evs
    1.33 -		  | Gets A' X    => 
    1.34 -                      if A'=A then insert X (knows A evs) else knows A evs))"
    1.35 +  knows_Cons
    1.36 +    "knows A (ev # evs) =
    1.37 +       (if A = Spy then 
    1.38 +	(case ev of
    1.39 +	   Says A' B X => insert X (knows Spy evs)
    1.40 +	 | Gets A' X => knows Spy evs
    1.41 +	 | Notes A' X  => 
    1.42 +	     if A' : bad then insert X (knows Spy evs) else knows Spy evs)
    1.43 +	else
    1.44 +	(case ev of
    1.45 +	   Says A' B X => 
    1.46 +	     if A'=A then insert X (knows A evs) else knows A evs
    1.47 +	 | Gets A' X    => 
    1.48 +	     if A'=A then insert X (knows A evs) else knows A evs
    1.49 +	 | Notes A' X    => 
    1.50 +	     if A'=A then insert X (knows A evs) else knows A evs))"
    1.51  
    1.52  (*
    1.53    Case A=Spy on the Gets event
    1.54 @@ -73,8 +74,8 @@
    1.55    used_Cons  "used (ev # evs) =
    1.56  	         (case ev of
    1.57  		    Says A B X => parts {X} Un (used evs)
    1.58 -		  | Notes A X  => parts {X} Un (used evs)
    1.59 -		  | Gets A X   => used evs)"
    1.60 +		  | Gets A X   => used evs
    1.61 +		  | Notes A X  => parts {X} Un (used evs))"
    1.62  
    1.63  
    1.64