# HG changeset patch
# User noschinl
# Date 1378457800 -7200
# Node ID 3083c611ec40c241c05b98da9bada0b787df71ff
# Parent  415354b68f0c8eb57689508a103cc0598d60a968
use case_of_simps

diff -r 415354b68f0c -r 3083c611ec40 src/HOL/Auth/Event.thy
--- a/src/HOL/Auth/Event.thy	Fri Sep 06 10:56:40 2013 +0200
+++ b/src/HOL/Auth/Event.thy	Fri Sep 06 10:56:40 2013 +0200
@@ -48,7 +48,6 @@
              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
   enforces the fact that if a message is received then it must have been sent,
@@ -153,17 +152,6 @@
 
 subsection{*Knowledge of Agents*}
 
-lemma knows_Says: "knows A (Says A B X # evs) = insert X (knows A evs)"
-by simp
-
-lemma knows_Notes: "knows A (Notes A X # evs) = insert X (knows A evs)"
-by simp
-
-lemma knows_Gets:
-     "A \<noteq> Spy --> knows A (Gets A X # evs) = insert X (knows A evs)"
-by simp
-
-
 lemma knows_subset_knows_Says: "knows A evs \<subseteq> knows A (Says A' B X # evs)"
 by (simp add: subset_insertI)
 
@@ -260,7 +248,7 @@
 
 
 lemma knows_subset_knows_Cons: "knows A evs \<subseteq> knows A (e # evs)"
-by (induct e, auto simp: knows_Cons)
+by (cases e, auto simp: knows_Cons)
 
 lemma initState_subset_knows: "initState A \<subseteq> knows A evs"
 apply (induct_tac evs, simp) 
diff -r 415354b68f0c -r 3083c611ec40 src/HOL/Auth/Shared.thy
--- a/src/HOL/Auth/Shared.thy	Fri Sep 06 10:56:40 2013 +0200
+++ b/src/HOL/Auth/Shared.thy	Fri Sep 06 10:56:40 2013 +0200
@@ -251,6 +251,6 @@
     "for proving possibility theorems"
 
 lemma knows_subset_knows_Cons: "knows A evs <= knows A (e # evs)"
-by (induct e) (auto simp: knows_Cons)
+by (cases e) (auto simp: knows_Cons)
 
 end
diff -r 415354b68f0c -r 3083c611ec40 src/HOL/Auth/Smartcard/EventSC.thy
--- a/src/HOL/Auth/Smartcard/EventSC.thy	Fri Sep 06 10:56:40 2013 +0200
+++ b/src/HOL/Auth/Smartcard/EventSC.thy	Fri Sep 06 10:56:40 2013 +0200
@@ -1,6 +1,10 @@
 header{*Theory of Events for Security Protocols that use smartcards*}
 
-theory EventSC imports "../Message" begin
+theory EventSC
+imports
+  "../Message"
+  "~~/src/HOL/Library/Simps_Case_Conv"
+begin
 
 consts  (*Initial states of agents -- parameter of the construction*)
   initState :: "agent => msg set"
@@ -46,7 +50,6 @@
   Card_Spy_not_cloned    [iff]: "Card Spy \<notin> cloned"
   apply blast done
 
-
 primrec (*This definition is extended over the new events, subject to the 
           assumption of secure means*)
   knows   :: "agent => event list => msg set" (*agents' knowledge*) where
@@ -244,16 +247,6 @@
 
 subsection{*Knowledge of Agents*}
 
-lemma knows_Says: "knows A (Says A B X # evs) = insert X (knows A evs)"
-by simp
-
-lemma knows_Notes: "knows A (Notes A X # evs) = insert X (knows A evs)"
-by simp
-
-lemma knows_Gets:
-      "A \<noteq> Spy \<longrightarrow> knows A (Gets A X # evs) = insert X (knows A evs)"
-by simp
-
 lemma knows_Inputs: "knows A (Inputs A C X # evs) = insert X (knows A evs)"
 by simp
 
@@ -346,7 +339,7 @@
 
 lemma parts_knows_Spy_subset_used: "parts (knows Spy evs) \<subseteq> used evs"
 apply (induct_tac "evs", force)  
-apply (simp add: parts_insert_knows_A knows_Cons add: event.split, blast) 
+apply (simp add: parts_insert_knows_A add: event.split, blast)
 done
 
 lemmas usedI = parts_knows_Spy_subset_used [THEN subsetD, intro]
@@ -356,26 +349,7 @@
 apply (simp_all add: parts_insert_knows_A split add: event.split, blast)
 done
 
-lemma used_Says [simp]: "used (Says A B X # evs) = parts{X} \<union> used evs"
-by simp
-
-lemma used_Notes [simp]: "used (Notes A X # evs) = parts{X} \<union> used evs"
-by simp
-
-lemma used_Gets [simp]: "used (Gets A X # evs) = used evs"
-by simp
-
-lemma used_Inputs [simp]: "used (Inputs A C X # evs) = parts{X} \<union> used evs"
-by simp
-
-lemma used_C_Gets [simp]: "used (C_Gets C X # evs) = used evs"
-by simp
-
-lemma used_Outpts [simp]: "used (Outpts C A X # evs) = parts{X} \<union> used evs"
-by simp
-
-lemma used_A_Gets [simp]: "used (A_Gets A X # evs) = used evs"
-by simp
+simps_of_case used_Cons_simps[simp]: used_Cons
 
 lemma used_nil_subset: "used [] \<subseteq> used evs"
 apply simp
@@ -422,7 +396,7 @@
 
 
 lemma knows_subset_knows_Cons: "knows A evs \<subseteq> knows A (e # evs)"
-by (induct e, auto simp: knows_Cons)
+by (cases e, auto simp: knows_Cons)
 
 lemma initState_subset_knows: "initState A \<subseteq> knows A evs"
 apply (induct_tac evs, simp) 
diff -r 415354b68f0c -r 3083c611ec40 src/HOL/Auth/Smartcard/Smartcard.thy
--- a/src/HOL/Auth/Smartcard/Smartcard.thy	Fri Sep 06 10:56:40 2013 +0200
+++ b/src/HOL/Auth/Smartcard/Smartcard.thy	Fri Sep 06 10:56:40 2013 +0200
@@ -370,8 +370,7 @@
 fun possibility_tac ctxt =
    (REPEAT 
     (ALLGOALS (simp_tac (ctxt
-      delsimps [@{thm used_Says}, @{thm used_Notes}, @{thm used_Gets},
-        @{thm used_Inputs}, @{thm used_C_Gets}, @{thm used_Outpts}, @{thm used_A_Gets}]
+      delsimps @{thms used_Cons_simps}
       setSolver safe_solver))
      THEN
      REPEAT_FIRST (eq_assume_tac ORELSE'