--- a/src/HOL/Auth/Event.ML Wed Mar 17 18:01:41 1999 +0100
+++ b/src/HOL/Auth/Event.ML Thu Mar 18 10:41:00 1999 +0100
@@ -18,10 +18,10 @@
read_instantiate_sg (sign_of thy) [("H", "knows Spy evs")]);
-Goal "P(event_case sf nf gf ev) = \
+Goal "P(event_case sf gf nf ev) = \
\ ((ALL A B X. ev = Says A B X --> P(sf A B X)) & \
-\ (ALL A X. ev = Notes A X --> P(nf A X)) & \
-\ (ALL A X. ev = Gets A X --> P(gf A X)))";
+\ (ALL A X. ev = Gets A X --> P(gf A X)) & \
+\ (ALL A X. ev = Notes A X --> P(nf A X)))";
by (induct_tac "ev" 1);
by Auto_tac;
qed "expand_event_case";
--- 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))"