src/HOL/Auth/Event.thy
changeset 32960 69916a850301
parent 32404 da3ca3c6ec81
child 37936 1e4c5015a72e
     1.1 --- a/src/HOL/Auth/Event.thy	Sat Oct 17 01:05:59 2009 +0200
     1.2 +++ b/src/HOL/Auth/Event.thy	Sat Oct 17 14:43:18 2009 +0200
     1.3 @@ -22,7 +22,7 @@
     1.4          | Notes agent       msg
     1.5         
     1.6  consts 
     1.7 -  bad    :: "agent set"				(*compromised agents*)
     1.8 +  bad    :: "agent set"                         -- {* compromised agents *}
     1.9    knows  :: "agent => event list => msg set"
    1.10  
    1.11  
    1.12 @@ -43,19 +43,19 @@
    1.13    knows_Cons:
    1.14      "knows A (ev # evs) =
    1.15         (if A = Spy then 
    1.16 -	(case ev of
    1.17 -	   Says A' B X => insert X (knows Spy evs)
    1.18 -	 | Gets A' X => knows Spy evs
    1.19 -	 | Notes A' X  => 
    1.20 -	     if A' \<in> bad then insert X (knows Spy evs) else knows Spy evs)
    1.21 -	else
    1.22 -	(case ev of
    1.23 -	   Says A' B X => 
    1.24 -	     if A'=A then insert X (knows A evs) else knows A evs
    1.25 -	 | Gets A' X    => 
    1.26 -	     if A'=A then insert X (knows A evs) else knows A evs
    1.27 -	 | Notes A' X    => 
    1.28 -	     if A'=A then insert X (knows A evs) else knows A evs))"
    1.29 +        (case ev of
    1.30 +           Says A' B X => insert X (knows Spy evs)
    1.31 +         | Gets A' X => knows Spy evs
    1.32 +         | Notes A' X  => 
    1.33 +             if A' \<in> bad then insert X (knows Spy evs) else knows Spy evs)
    1.34 +        else
    1.35 +        (case ev of
    1.36 +           Says A' B X => 
    1.37 +             if A'=A then insert X (knows A evs) else knows A evs
    1.38 +         | Gets A' X    => 
    1.39 +             if A'=A then insert X (knows A evs) else knows A evs
    1.40 +         | Notes A' X    => 
    1.41 +             if A'=A then insert X (knows A evs) else knows A evs))"
    1.42  
    1.43  (*
    1.44    Case A=Spy on the Gets event
    1.45 @@ -71,10 +71,10 @@
    1.46  primrec
    1.47    used_Nil:   "used []         = (UN B. parts (initState B))"
    1.48    used_Cons:  "used (ev # evs) =
    1.49 -		     (case ev of
    1.50 -			Says A B X => parts {X} \<union> used evs
    1.51 -		      | Gets A X   => used evs
    1.52 -		      | Notes A X  => parts {X} \<union> used evs)"
    1.53 +                     (case ev of
    1.54 +                        Says A B X => parts {X} \<union> used evs
    1.55 +                      | Gets A X   => used evs
    1.56 +                      | Notes A X  => parts {X} \<union> used evs)"
    1.57      --{*The case for @{term Gets} seems anomalous, but @{term Gets} always
    1.58          follows @{term Says} in real protocols.  Seems difficult to change.
    1.59          See @{text Gets_correct} in theory @{text "Guard/Extensions.thy"}. *}