src/HOL/Auth/Event.thy
changeset 13935 4822d9597d1e
parent 13926 6e62e5357a10
child 13956 8fe7e12290e1
     1.1 --- a/src/HOL/Auth/Event.thy	Tue Apr 29 12:36:40 2003 +0200
     1.2 +++ b/src/HOL/Auth/Event.thy	Tue Apr 29 12:36:49 2003 +0200
     1.3 @@ -73,10 +73,12 @@
     1.4    used_Nil:   "used []         = (UN B. parts (initState B))"
     1.5    used_Cons:  "used (ev # evs) =
     1.6  		     (case ev of
     1.7 -			Says A B X => parts {X} \<union> (used evs)
     1.8 +			Says A B X => parts {X} \<union> used evs
     1.9  		      | Gets A X   => used evs
    1.10 -		      | Notes A X  => parts {X} \<union> (used evs))"
    1.11 -
    1.12 +		      | Notes A X  => parts {X} \<union> used evs)"
    1.13 +    --{*The case for @{term Gets} seems anomalous, but @{term Gets} always
    1.14 +        follows @{term Says} in real protocols.  Seems difficult to change.
    1.15 +        See @{text Gets_correct} in theory @{text "Guard/Extensions.thy"}. *}
    1.16  
    1.17  lemma Notes_imp_used [rule_format]: "Notes A X \<in> set evs --> X \<in> used evs"
    1.18  apply (induct_tac evs)
    1.19 @@ -101,7 +103,7 @@
    1.20        = parts {X} \<union> parts (knows Spy evs)"}.  The general case loops.*)
    1.21  
    1.22  text{*This version won't loop with the simplifier.*}
    1.23 -lemmas parts_insert_knows_Spy = parts_insert [of _ "knows Spy evs", standard]
    1.24 +lemmas parts_insert_knows_A = parts_insert [of _ "knows A evs", standard]
    1.25  
    1.26  lemma knows_Spy_Says [simp]:
    1.27       "knows Spy (Says A B X # evs) = insert X (knows Spy evs)"
    1.28 @@ -118,15 +120,15 @@
    1.29  by simp
    1.30  
    1.31  lemma knows_Spy_subset_knows_Spy_Says:
    1.32 -     "knows Spy evs <= knows Spy (Says A B X # evs)"
    1.33 +     "knows Spy evs \<subseteq> knows Spy (Says A B X # evs)"
    1.34  by (simp add: subset_insertI)
    1.35  
    1.36  lemma knows_Spy_subset_knows_Spy_Notes:
    1.37 -     "knows Spy evs <= knows Spy (Notes A X # evs)"
    1.38 +     "knows Spy evs \<subseteq> knows Spy (Notes A X # evs)"
    1.39  by force
    1.40  
    1.41  lemma knows_Spy_subset_knows_Spy_Gets:
    1.42 -     "knows Spy evs <= knows Spy (Gets A X # evs)"
    1.43 +     "knows Spy evs \<subseteq> knows Spy (Gets A X # evs)"
    1.44  by (simp add: subset_insertI)
    1.45  
    1.46  text{*Spy sees what is sent on the traffic*}
    1.47 @@ -152,7 +154,7 @@
    1.48  text{*Compatibility for the old "spies" function*}
    1.49  lemmas spies_partsEs = knows_Spy_partsEs
    1.50  lemmas Says_imp_spies = Says_imp_knows_Spy
    1.51 -lemmas parts_insert_spies = parts_insert_knows_Spy
    1.52 +lemmas parts_insert_spies = parts_insert_knows_A [of _ Spy]
    1.53  
    1.54  
    1.55  subsection{*Knowledge of Agents*}
    1.56 @@ -168,17 +170,14 @@
    1.57  by simp
    1.58  
    1.59  
    1.60 -lemma knows_subset_knows_Says: "knows A evs <= knows A (Says A' B X # evs)"
    1.61 -apply (simp add: subset_insertI)
    1.62 -done
    1.63 +lemma knows_subset_knows_Says: "knows A evs \<subseteq> knows A (Says A' B X # evs)"
    1.64 +by (simp add: subset_insertI)
    1.65  
    1.66 -lemma knows_subset_knows_Notes: "knows A evs <= knows A (Notes A' X # evs)"
    1.67 -apply (simp add: subset_insertI)
    1.68 -done
    1.69 +lemma knows_subset_knows_Notes: "knows A evs \<subseteq> knows A (Notes A' X # evs)"
    1.70 +by (simp add: subset_insertI)
    1.71  
    1.72 -lemma knows_subset_knows_Gets: "knows A evs <= knows A (Gets A' X # evs)"
    1.73 -apply (simp add: subset_insertI)
    1.74 -done
    1.75 +lemma knows_subset_knows_Gets: "knows A evs \<subseteq> knows A (Gets A' X # evs)"
    1.76 +by (simp add: subset_insertI)
    1.77  
    1.78  text{*Agents know what they say*}
    1.79  lemma Says_imp_knows [rule_format]: "Says A B X \<in> set evs --> X \<in> knows A evs"
    1.80 @@ -224,27 +223,16 @@
    1.81  apply blast
    1.82  done
    1.83  
    1.84 -
    1.85 -
    1.86 -
    1.87 -text{*NOTE REMOVAL--laws above are cleaner, as they don't involve "case"*}
    1.88 -declare knows_Cons [simp del]
    1.89 -
    1.90 -
    1.91 -subsection{*Fresh Nonces*}
    1.92 -
    1.93 -lemma parts_knows_Spy_subset_used: "parts (knows Spy evs) <= used evs"
    1.94 -apply (induct_tac "evs")
    1.95 -apply (simp_all (no_asm_simp) add: parts_insert_knows_Spy split add: event.split)
    1.96 -apply blast+
    1.97 +lemma parts_knows_Spy_subset_used: "parts (knows Spy evs) \<subseteq> used evs"
    1.98 +apply (induct_tac "evs", force)  
    1.99 +apply (simp add: parts_insert_knows_A knows_Cons add: event.split, blast) 
   1.100  done
   1.101  
   1.102  lemmas usedI = parts_knows_Spy_subset_used [THEN subsetD, intro]
   1.103  
   1.104  lemma initState_into_used: "X \<in> parts (initState B) ==> X \<in> used evs"
   1.105  apply (induct_tac "evs")
   1.106 -apply (simp_all (no_asm_simp) add: parts_insert_knows_Spy split add: event.split)
   1.107 -apply blast
   1.108 +apply (simp_all add: parts_insert_knows_A split add: event.split, blast)
   1.109  done
   1.110  
   1.111  lemma used_Says [simp]: "used (Says A B X # evs) = parts{X} \<union> used evs"
   1.112 @@ -256,13 +244,14 @@
   1.113  lemma used_Gets [simp]: "used (Gets A X # evs) = used evs"
   1.114  by simp
   1.115  
   1.116 -lemma used_nil_subset: "used [] <= used evs"
   1.117 -apply (simp)
   1.118 +lemma used_nil_subset: "used [] \<subseteq> used evs"
   1.119 +apply simp
   1.120  apply (blast intro: initState_into_used)
   1.121  done
   1.122  
   1.123  text{*NOTE REMOVAL--laws above are cleaner, as they don't involve "case"*}
   1.124 -declare used_Nil [simp del] used_Cons [simp del]
   1.125 +declare knows_Cons [simp del]
   1.126 +        used_Nil [simp del] used_Cons [simp del]
   1.127  
   1.128  
   1.129  text{*For proving theorems of the form @{term "X \<notin> analz (knows Spy evs) --> P"}
   1.130 @@ -291,7 +280,7 @@
   1.131  lemma knows_subset_knows_Cons: "knows A evs \<subseteq> knows A (e # evs)"
   1.132  by (induct e, auto simp: knows_Cons)
   1.133  
   1.134 -lemma initState_subset_knows: "initState A <= knows A evs"
   1.135 +lemma initState_subset_knows: "initState A \<subseteq> knows A evs"
   1.136  apply (induct_tac evs, simp) 
   1.137  apply (blast intro: knows_subset_knows_Cons [THEN subsetD])
   1.138  done
   1.139 @@ -322,31 +311,17 @@
   1.140  val Notes_imp_used = thm "Notes_imp_used";
   1.141  val Says_imp_used = thm "Says_imp_used";
   1.142  val MPair_used = thm "MPair_used";
   1.143 -val parts_insert_knows_Spy = thm "parts_insert_knows_Spy";
   1.144 -val knows_Spy_Says = thm "knows_Spy_Says";
   1.145 -val knows_Spy_Notes = thm "knows_Spy_Notes";
   1.146 -val knows_Spy_Gets = thm "knows_Spy_Gets";
   1.147 -val knows_Spy_subset_knows_Spy_Says = thm "knows_Spy_subset_knows_Spy_Says";
   1.148 -val knows_Spy_subset_knows_Spy_Notes = thm "knows_Spy_subset_knows_Spy_Notes";
   1.149 -val knows_Spy_subset_knows_Spy_Gets = thm "knows_Spy_subset_knows_Spy_Gets";
   1.150  val Says_imp_knows_Spy = thm "Says_imp_knows_Spy";
   1.151  val Notes_imp_knows_Spy = thm "Notes_imp_knows_Spy";
   1.152  val knows_Spy_partsEs = thms "knows_Spy_partsEs";
   1.153  val spies_partsEs = thms "spies_partsEs";
   1.154  val Says_imp_spies = thm "Says_imp_spies";
   1.155  val parts_insert_spies = thm "parts_insert_spies";
   1.156 -val knows_Says = thm "knows_Says";
   1.157 -val knows_Notes = thm "knows_Notes";
   1.158 -val knows_Gets = thm "knows_Gets";
   1.159 -val knows_subset_knows_Says = thm "knows_subset_knows_Says";
   1.160 -val knows_subset_knows_Notes = thm "knows_subset_knows_Notes";
   1.161 -val knows_subset_knows_Gets = thm "knows_subset_knows_Gets";
   1.162  val Says_imp_knows = thm "Says_imp_knows";
   1.163  val Notes_imp_knows = thm "Notes_imp_knows";
   1.164  val Gets_imp_knows_agents = thm "Gets_imp_knows_agents";
   1.165  val knows_imp_Says_Gets_Notes_initState = thm "knows_imp_Says_Gets_Notes_initState";
   1.166  val knows_Spy_imp_Says_Notes_initState = thm "knows_Spy_imp_Says_Notes_initState";
   1.167 -val parts_knows_Spy_subset_used = thm "parts_knows_Spy_subset_used";
   1.168  val usedI = thm "usedI";
   1.169  val initState_into_used = thm "initState_into_used";
   1.170  val used_Says = thm "used_Says";
   1.171 @@ -361,6 +336,11 @@
   1.172  
   1.173  val synth_analz_mono = thm "synth_analz_mono";
   1.174  
   1.175 +val knows_Spy_subset_knows_Spy_Says = thm "knows_Spy_subset_knows_Spy_Says";
   1.176 +val knows_Spy_subset_knows_Spy_Notes = thm "knows_Spy_subset_knows_Spy_Notes";
   1.177 +val knows_Spy_subset_knows_Spy_Gets = thm "knows_Spy_subset_knows_Spy_Gets";
   1.178 +
   1.179 +
   1.180  val synth_analz_mono_contra_tac = 
   1.181    let val syan_impI = inst "P" "?Y \<notin> synth (analz (knows Spy ?evs))" impI
   1.182    in