src/HOL/Auth/Event.thy
changeset 6399 4a9040b85e2e
parent 6308 76f3865a2b1d
child 11104 f2024fed9f0c
--- a/src/HOL/Auth/Event.thy	Wed Mar 17 18:01:41 1999 +0100
+++ b/src/HOL/Auth/Event.thy	Thu Mar 18 10:41:00 1999 +0100
@@ -16,10 +16,10 @@
 consts  (*Initial states of agents -- parameter of the construction*)
   initState :: agent => msg set
 
-datatype  (*Messages--could add another constructor for agent knowledge*)
+datatype
   event = Says  agent agent msg
+        | Gets  agent       msg
         | Notes agent       msg
-        | Gets  agent       msg
        
 consts 
   bad    :: agent set        (*compromised agents*)
@@ -41,21 +41,22 @@
 
 primrec
   knows_Nil   "knows A []         = initState A"
-  knows_Cons  "knows A (ev # evs) =
-	        (if A = Spy then 
-                  (case ev of
-		    Says A' B X => insert X (knows Spy evs)
-		  | Notes A' X  => 
-                   if A' : bad then insert X (knows Spy evs) else knows Spy evs
-                  | Gets A' X => knows Spy evs)
-                 else
-                  (case ev of
-		    Says A' B X => 
-                      if A'=A then insert X (knows A evs) else knows A evs
-		  | Notes A' X    => 
-                      if A'=A then insert X (knows A evs) else knows A evs
-		  | Gets A' X    => 
-                      if A'=A then insert X (knows A evs) else knows A evs))"
+  knows_Cons
+    "knows A (ev # evs) =
+       (if A = Spy then 
+	(case ev of
+	   Says A' B X => insert X (knows Spy evs)
+	 | Gets A' X => knows Spy evs
+	 | Notes A' X  => 
+	     if A' : bad then insert X (knows Spy evs) else knows Spy evs)
+	else
+	(case ev of
+	   Says A' B X => 
+	     if A'=A then insert X (knows A evs) else knows A evs
+	 | Gets A' X    => 
+	     if A'=A then insert X (knows A evs) else knows A evs
+	 | Notes A' X    => 
+	     if A'=A then insert X (knows A evs) else knows A evs))"
 
 (*
   Case A=Spy on the Gets event
@@ -73,8 +74,8 @@
   used_Cons  "used (ev # evs) =
 	         (case ev of
 		    Says A B X => parts {X} Un (used evs)
-		  | Notes A X  => parts {X} Un (used evs)
-		  | Gets A X   => used evs)"
+		  | Gets A X   => used evs
+		  | Notes A X  => parts {X} Un (used evs))"