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) 

     2.1 --- a/src/HOL/Auth/Shared.thy	Fri Sep 06 10:56:40 2013 +0200
     2.2 +++ b/src/HOL/Auth/Shared.thy	Fri Sep 06 10:56:40 2013 +0200
     2.3 @@ -251,6 +251,6 @@
     2.4      "for proving possibility theorems"
     2.5  
     2.6  lemma knows_subset_knows_Cons: "knows A evs <= knows A (e # evs)"
     2.7 -by (induct e) (auto simp: knows_Cons)
     2.8 +by (cases e) (auto simp: knows_Cons)
     2.9  
    2.10  end

     3.1 --- a/src/HOL/Auth/Smartcard/EventSC.thy	Fri Sep 06 10:56:40 2013 +0200
     3.2 +++ b/src/HOL/Auth/Smartcard/EventSC.thy	Fri Sep 06 10:56:40 2013 +0200
     3.3 @@ -1,6 +1,10 @@
     3.4  header{*Theory of Events for Security Protocols that use smartcards*}
     3.5  
     3.6 -theory EventSC imports "../Message" begin
     3.7 +theory EventSC
     3.8 +imports
     3.9 +  "../Message"
    3.10 +  "~~/src/HOL/Library/Simps_Case_Conv"
    3.11 +begin
    3.12  
    3.13  consts  (*Initial states of agents -- parameter of the construction*)
    3.14    initState :: "agent => msg set"
    3.15 @@ -46,7 +50,6 @@
    3.16    Card_Spy_not_cloned    [iff]: "Card Spy \<notin> cloned"
    3.17    apply blast done
    3.18  
    3.19 -
    3.20  primrec (*This definition is extended over the new events, subject to the 
    3.21            assumption of secure means*)
    3.22    knows   :: "agent => event list => msg set" (*agents' knowledge*) where
    3.23 @@ -244,16 +247,6 @@
    3.24  
    3.25  subsection{*Knowledge of Agents*}
    3.26  
    3.27 -lemma knows_Says: "knows A (Says A B X # evs) = insert X (knows A evs)"
    3.28 -by simp
    3.29 -
    3.30 -lemma knows_Notes: "knows A (Notes A X # evs) = insert X (knows A evs)"
    3.31 -by simp
    3.32 -
    3.33 -lemma knows_Gets:
    3.34 -      "A \<noteq> Spy \<longrightarrow> knows A (Gets A X # evs) = insert X (knows A evs)"
    3.35 -by simp
    3.36 -
    3.37  lemma knows_Inputs: "knows A (Inputs A C X # evs) = insert X (knows A evs)"
    3.38  by simp
    3.39  
    3.40 @@ -346,7 +339,7 @@
    3.41  
    3.42  lemma parts_knows_Spy_subset_used: "parts (knows Spy evs) \<subseteq> used evs"
    3.43  apply (induct_tac "evs", force)  
    3.44 -apply (simp add: parts_insert_knows_A knows_Cons add: event.split, blast) 
    3.45 +apply (simp add: parts_insert_knows_A add: event.split, blast)
    3.46  done
    3.47  
    3.48  lemmas usedI = parts_knows_Spy_subset_used [THEN subsetD, intro]
    3.49 @@ -356,26 +349,7 @@
    3.50  apply (simp_all add: parts_insert_knows_A split add: event.split, blast)
    3.51  done
    3.52  
    3.53 -lemma used_Says [simp]: "used (Says A B X # evs) = parts{X} \<union> used evs"
    3.54 -by simp
    3.55 -
    3.56 -lemma used_Notes [simp]: "used (Notes A X # evs) = parts{X} \<union> used evs"
    3.57 -by simp
    3.58 -
    3.59 -lemma used_Gets [simp]: "used (Gets A X # evs) = used evs"
    3.60 -by simp
    3.61 -
    3.62 -lemma used_Inputs [simp]: "used (Inputs A C X # evs) = parts{X} \<union> used evs"
    3.63 -by simp
    3.64 -
    3.65 -lemma used_C_Gets [simp]: "used (C_Gets C X # evs) = used evs"
    3.66 -by simp
    3.67 -
    3.68 -lemma used_Outpts [simp]: "used (Outpts C A X # evs) = parts{X} \<union> used evs"
    3.69 -by simp
    3.70 -
    3.71 -lemma used_A_Gets [simp]: "used (A_Gets A X # evs) = used evs"
    3.72 -by simp
    3.73 +simps_of_case used_Cons_simps[simp]: used_Cons
    3.74  
    3.75  lemma used_nil_subset: "used [] \<subseteq> used evs"
    3.76  apply simp
    3.77 @@ -422,7 +396,7 @@
    3.78  
    3.79  
    3.80  lemma knows_subset_knows_Cons: "knows A evs \<subseteq> knows A (e # evs)"
    3.81 -by (induct e, auto simp: knows_Cons)
    3.82 +by (cases e, auto simp: knows_Cons)
    3.83  
    3.84  lemma initState_subset_knows: "initState A \<subseteq> knows A evs"
    3.85  apply (induct_tac evs, simp) 

     4.1 --- a/src/HOL/Auth/Smartcard/Smartcard.thy	Fri Sep 06 10:56:40 2013 +0200
     4.2 +++ b/src/HOL/Auth/Smartcard/Smartcard.thy	Fri Sep 06 10:56:40 2013 +0200
     4.3 @@ -370,8 +370,7 @@
     4.4  fun possibility_tac ctxt =
     4.5     (REPEAT 
     4.6      (ALLGOALS (simp_tac (ctxt
     4.7 -      delsimps [@{thm used_Says}, @{thm used_Notes}, @{thm used_Gets},
     4.8 -        @{thm used_Inputs}, @{thm used_C_Gets}, @{thm used_Outpts}, @{thm used_A_Gets}]
     4.9 +      delsimps @{thms used_Cons_simps}
    4.10        setSolver safe_solver))
    4.11       THEN
    4.12       REPEAT_FIRST (eq_assume_tac ORELSE'