src/HOL/Auth/Event.thy
changeset 53428 3083c611ec40
parent 46471 2289a3869c88
child 58305 57752a91eec4
     1.1 --- a/src/HOL/Auth/Event.thy	Fri Sep 06 10:56:40 2013 +0200
     1.2 +++ b/src/HOL/Auth/Event.thy	Fri Sep 06 10:56:40 2013 +0200
     1.3 @@ -48,7 +48,6 @@
     1.4               if A'=A then insert X (knows A evs) else knows A evs
     1.5           | Notes A' X    => 
     1.6               if A'=A then insert X (knows A evs) else knows A evs))"
     1.7 -
     1.8  (*
     1.9    Case A=Spy on the Gets event
    1.10    enforces the fact that if a message is received then it must have been sent,
    1.11 @@ -153,17 +152,6 @@
    1.12  
    1.13  subsection{*Knowledge of Agents*}
    1.14  
    1.15 -lemma knows_Says: "knows A (Says A B X # evs) = insert X (knows A evs)"
    1.16 -by simp
    1.17 -
    1.18 -lemma knows_Notes: "knows A (Notes A X # evs) = insert X (knows A evs)"
    1.19 -by simp
    1.20 -
    1.21 -lemma knows_Gets:
    1.22 -     "A \<noteq> Spy --> knows A (Gets A X # evs) = insert X (knows A evs)"
    1.23 -by simp
    1.24 -
    1.25 -
    1.26  lemma knows_subset_knows_Says: "knows A evs \<subseteq> knows A (Says A' B X # evs)"
    1.27  by (simp add: subset_insertI)
    1.28  
    1.29 @@ -260,7 +248,7 @@
    1.30  
    1.31  
    1.32  lemma knows_subset_knows_Cons: "knows A evs \<subseteq> knows A (e # evs)"
    1.33 -by (induct e, auto simp: knows_Cons)
    1.34 +by (cases e, auto simp: knows_Cons)
    1.35  
    1.36  lemma initState_subset_knows: "initState A \<subseteq> knows A evs"
    1.37  apply (induct_tac evs, simp)