--- a/doc-src/TutorialI/Protocol/Event.thy Sat Oct 17 01:05:59 2009 +0200
+++ b/doc-src/TutorialI/Protocol/Event.thy Sat Oct 17 14:43:18 2009 +0200
@@ -22,7 +22,7 @@
| Notes agent msg
consts
- bad :: "agent set" (*compromised agents*)
+ bad :: "agent set" -- {* compromised agents *}
knows :: "agent => event list => msg set"
@@ -43,19 +43,19 @@
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' \<in> 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 ev of
+ Says A' B X => insert X (knows Spy evs)
+ | Gets A' X => knows Spy evs
+ | Notes A' X =>
+ if A' \<in> 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
@@ -71,10 +71,10 @@
primrec
used_Nil: "used [] = (UN B. parts (initState B))"
used_Cons: "used (ev # evs) =
- (case ev of
- Says A B X => parts {X} \<union> used evs
- | Gets A X => used evs
- | Notes A X => parts {X} \<union> used evs)"
+ (case ev of
+ Says A B X => parts {X} \<union> used evs
+ | Gets A X => used evs
+ | Notes A X => parts {X} \<union> used evs)"
--{*The case for @{term Gets} seems anomalous, but @{term Gets} always
follows @{term Says} in real protocols. Seems difficult to change.
See @{text Gets_correct} in theory @{text "Guard/Extensions.thy"}. *}