src/HOL/Auth/Event.thy
changeset 14200 d8598e24f8fa
parent 14126 28824746d046
child 16417 9bc16273c2d4
     1.1 --- a/src/HOL/Auth/Event.thy	Tue Sep 23 15:40:27 2003 +0200
     1.2 +++ b/src/HOL/Auth/Event.thy	Tue Sep 23 15:41:33 2003 +0200
     1.3 @@ -35,13 +35,10 @@
     1.4  
     1.5  text{*Spy has access to his own key for spoof messages, but Server is secure*}
     1.6  specification (bad)
     1.7 -  bad_properties: "Spy \<in> bad & Server \<notin> bad"
     1.8 +  Spy_in_bad     [iff]: "Spy \<in> bad"
     1.9 +  Server_not_bad [iff]: "Server \<notin> bad"
    1.10      by (rule exI [of _ "{Spy}"], simp)
    1.11  
    1.12 -lemmas Spy_in_bad = bad_properties [THEN conjunct1, iff]
    1.13 -lemmas Server_not_bad = bad_properties [THEN conjunct2, iff]
    1.14 -
    1.15 -
    1.16  primrec
    1.17    knows_Nil:   "knows A [] = initState A"
    1.18    knows_Cons:
    1.19 @@ -111,8 +108,8 @@
    1.20       "knows Spy (Says A B X # evs) = insert X (knows Spy evs)"
    1.21  by simp
    1.22  
    1.23 -text{*The point of letting the Spy see "bad" agents' notes is to prevent
    1.24 -  redundant case-splits on whether A=Spy and whether A:bad*}
    1.25 +text{*Letting the Spy see "bad" agents' notes avoids redundant case-splits
    1.26 +      on whether @{term "A=Spy"} and whether @{term "A\<in>bad"}*}
    1.27  lemma knows_Spy_Notes [simp]:
    1.28       "knows Spy (Notes A X # evs) =  
    1.29            (if A:bad then insert X (knows Spy evs) else knows Spy evs)"