tweaks
authorpaulson
Tue, 29 Apr 2003 12:36:49 +0200
changeset 13935 4822d9597d1e
parent 13934 8c23dea4648e
child 13936 d3671b878828
tweaks
src/HOL/Auth/Event.thy
src/HOL/Auth/NS_Shared.thy
src/HOL/Auth/Public.thy
src/HOL/Auth/Recur.thy
--- a/src/HOL/Auth/Event.thy	Tue Apr 29 12:36:40 2003 +0200
+++ b/src/HOL/Auth/Event.thy	Tue Apr 29 12:36:49 2003 +0200
@@ -73,10 +73,12 @@
   used_Nil:   "used []         = (UN B. parts (initState B))"
   used_Cons:  "used (ev # evs) =
 		     (case ev of
-			Says A B X => parts {X} \<union> (used evs)
+			Says A B X => parts {X} \<union> used evs
 		      | Gets A X   => used evs
-		      | Notes A X  => parts {X} \<union> (used evs))"
-
+		      | Notes A X  => parts {X} \<union> used evs)"
+    --{*The case for @{term Gets} seems anomalous, but @{term Gets} always
+        follows @{term Says} in real protocols.  Seems difficult to change.
+        See @{text Gets_correct} in theory @{text "Guard/Extensions.thy"}. *}
 
 lemma Notes_imp_used [rule_format]: "Notes A X \<in> set evs --> X \<in> used evs"
 apply (induct_tac evs)
@@ -101,7 +103,7 @@
       = parts {X} \<union> parts (knows Spy evs)"}.  The general case loops.*)
 
 text{*This version won't loop with the simplifier.*}
-lemmas parts_insert_knows_Spy = parts_insert [of _ "knows Spy evs", standard]
+lemmas parts_insert_knows_A = parts_insert [of _ "knows A evs", standard]
 
 lemma knows_Spy_Says [simp]:
      "knows Spy (Says A B X # evs) = insert X (knows Spy evs)"
@@ -118,15 +120,15 @@
 by simp
 
 lemma knows_Spy_subset_knows_Spy_Says:
-     "knows Spy evs <= knows Spy (Says A B X # evs)"
+     "knows Spy evs \<subseteq> knows Spy (Says A B X # evs)"
 by (simp add: subset_insertI)
 
 lemma knows_Spy_subset_knows_Spy_Notes:
-     "knows Spy evs <= knows Spy (Notes A X # evs)"
+     "knows Spy evs \<subseteq> knows Spy (Notes A X # evs)"
 by force
 
 lemma knows_Spy_subset_knows_Spy_Gets:
-     "knows Spy evs <= knows Spy (Gets A X # evs)"
+     "knows Spy evs \<subseteq> knows Spy (Gets A X # evs)"
 by (simp add: subset_insertI)
 
 text{*Spy sees what is sent on the traffic*}
@@ -152,7 +154,7 @@
 text{*Compatibility for the old "spies" function*}
 lemmas spies_partsEs = knows_Spy_partsEs
 lemmas Says_imp_spies = Says_imp_knows_Spy
-lemmas parts_insert_spies = parts_insert_knows_Spy
+lemmas parts_insert_spies = parts_insert_knows_A [of _ Spy]
 
 
 subsection{*Knowledge of Agents*}
@@ -168,17 +170,14 @@
 by simp
 
 
-lemma knows_subset_knows_Says: "knows A evs <= knows A (Says A' B X # evs)"
-apply (simp add: subset_insertI)
-done
+lemma knows_subset_knows_Says: "knows A evs \<subseteq> knows A (Says A' B X # evs)"
+by (simp add: subset_insertI)
 
-lemma knows_subset_knows_Notes: "knows A evs <= knows A (Notes A' X # evs)"
-apply (simp add: subset_insertI)
-done
+lemma knows_subset_knows_Notes: "knows A evs \<subseteq> knows A (Notes A' X # evs)"
+by (simp add: subset_insertI)
 
-lemma knows_subset_knows_Gets: "knows A evs <= knows A (Gets A' X # evs)"
-apply (simp add: subset_insertI)
-done
+lemma knows_subset_knows_Gets: "knows A evs \<subseteq> knows A (Gets A' X # evs)"
+by (simp add: subset_insertI)
 
 text{*Agents know what they say*}
 lemma Says_imp_knows [rule_format]: "Says A B X \<in> set evs --> X \<in> knows A evs"
@@ -224,27 +223,16 @@
 apply blast
 done
 
-
-
-
-text{*NOTE REMOVAL--laws above are cleaner, as they don't involve "case"*}
-declare knows_Cons [simp del]
-
-
-subsection{*Fresh Nonces*}
-
-lemma parts_knows_Spy_subset_used: "parts (knows Spy evs) <= used evs"
-apply (induct_tac "evs")
-apply (simp_all (no_asm_simp) add: parts_insert_knows_Spy split add: event.split)
-apply blast+
+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) 
 done
 
 lemmas usedI = parts_knows_Spy_subset_used [THEN subsetD, intro]
 
 lemma initState_into_used: "X \<in> parts (initState B) ==> X \<in> used evs"
 apply (induct_tac "evs")
-apply (simp_all (no_asm_simp) add: parts_insert_knows_Spy split add: event.split)
-apply blast
+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"
@@ -256,13 +244,14 @@
 lemma used_Gets [simp]: "used (Gets A X # evs) = used evs"
 by simp
 
-lemma used_nil_subset: "used [] <= used evs"
-apply (simp)
+lemma used_nil_subset: "used [] \<subseteq> used evs"
+apply simp
 apply (blast intro: initState_into_used)
 done
 
 text{*NOTE REMOVAL--laws above are cleaner, as they don't involve "case"*}
-declare used_Nil [simp del] used_Cons [simp del]
+declare knows_Cons [simp del]
+        used_Nil [simp del] used_Cons [simp del]
 
 
 text{*For proving theorems of the form @{term "X \<notin> analz (knows Spy evs) --> P"}
@@ -291,7 +280,7 @@
 lemma knows_subset_knows_Cons: "knows A evs \<subseteq> knows A (e # evs)"
 by (induct e, auto simp: knows_Cons)
 
-lemma initState_subset_knows: "initState A <= knows A evs"
+lemma initState_subset_knows: "initState A \<subseteq> knows A evs"
 apply (induct_tac evs, simp) 
 apply (blast intro: knows_subset_knows_Cons [THEN subsetD])
 done
@@ -322,31 +311,17 @@
 val Notes_imp_used = thm "Notes_imp_used";
 val Says_imp_used = thm "Says_imp_used";
 val MPair_used = thm "MPair_used";
-val parts_insert_knows_Spy = thm "parts_insert_knows_Spy";
-val knows_Spy_Says = thm "knows_Spy_Says";
-val knows_Spy_Notes = thm "knows_Spy_Notes";
-val knows_Spy_Gets = thm "knows_Spy_Gets";
-val knows_Spy_subset_knows_Spy_Says = thm "knows_Spy_subset_knows_Spy_Says";
-val knows_Spy_subset_knows_Spy_Notes = thm "knows_Spy_subset_knows_Spy_Notes";
-val knows_Spy_subset_knows_Spy_Gets = thm "knows_Spy_subset_knows_Spy_Gets";
 val Says_imp_knows_Spy = thm "Says_imp_knows_Spy";
 val Notes_imp_knows_Spy = thm "Notes_imp_knows_Spy";
 val knows_Spy_partsEs = thms "knows_Spy_partsEs";
 val spies_partsEs = thms "spies_partsEs";
 val Says_imp_spies = thm "Says_imp_spies";
 val parts_insert_spies = thm "parts_insert_spies";
-val knows_Says = thm "knows_Says";
-val knows_Notes = thm "knows_Notes";
-val knows_Gets = thm "knows_Gets";
-val knows_subset_knows_Says = thm "knows_subset_knows_Says";
-val knows_subset_knows_Notes = thm "knows_subset_knows_Notes";
-val knows_subset_knows_Gets = thm "knows_subset_knows_Gets";
 val Says_imp_knows = thm "Says_imp_knows";
 val Notes_imp_knows = thm "Notes_imp_knows";
 val Gets_imp_knows_agents = thm "Gets_imp_knows_agents";
 val knows_imp_Says_Gets_Notes_initState = thm "knows_imp_Says_Gets_Notes_initState";
 val knows_Spy_imp_Says_Notes_initState = thm "knows_Spy_imp_Says_Notes_initState";
-val parts_knows_Spy_subset_used = thm "parts_knows_Spy_subset_used";
 val usedI = thm "usedI";
 val initState_into_used = thm "initState_into_used";
 val used_Says = thm "used_Says";
@@ -361,6 +336,11 @@
 
 val synth_analz_mono = thm "synth_analz_mono";
 
+val knows_Spy_subset_knows_Spy_Says = thm "knows_Spy_subset_knows_Spy_Says";
+val knows_Spy_subset_knows_Spy_Notes = thm "knows_Spy_subset_knows_Spy_Notes";
+val knows_Spy_subset_knows_Spy_Gets = thm "knows_Spy_subset_knows_Spy_Gets";
+
+
 val synth_analz_mono_contra_tac = 
   let val syan_impI = inst "P" "?Y \<notin> synth (analz (knows Spy ?evs))" impI
   in
--- a/src/HOL/Auth/NS_Shared.thy	Tue Apr 29 12:36:40 2003 +0200
+++ b/src/HOL/Auth/NS_Shared.thy	Tue Apr 29 12:36:49 2003 +0200
@@ -302,9 +302,9 @@
 apply (force dest!: Crypt_imp_keysFor)     
 txt{*NS3*}
 apply blast 
-txt{*NS4*}
-apply (blast dest!: B_trusts_NS3
-	     dest: Says_imp_knows_Spy [THEN analz.Inj]
+txt{*NS4*} 
+apply (blast dest: B_trusts_NS3
+	           Says_imp_knows_Spy [THEN analz.Inj]
                    Crypt_Spy_analz_bad unique_session_keys)
 done
 
@@ -334,7 +334,7 @@
 txt{*NS3*}
 apply blast
 txt{*NS4*}
-apply (blast dest!: B_trusts_NS3
+apply (blast dest: B_trusts_NS3
 	     dest: Says_imp_knows_Spy [THEN analz.Inj]
                    unique_session_keys Crypt_Spy_analz_bad)
 done
--- a/src/HOL/Auth/Public.thy	Tue Apr 29 12:36:40 2003 +0200
+++ b/src/HOL/Auth/Public.thy	Tue Apr 29 12:36:49 2003 +0200
@@ -176,9 +176,10 @@
        (Key ` range pubEK) \<union> (Key ` range pubSK)"
 
 
-
 text{*These lemmas allow reasoning about @{term "used evs"} rather than
-   @{term "knows Spy evs"}, which is useful when there are private Notes. *}
+   @{term "knows Spy evs"}, which is useful when there are private Notes. 
+   Because they depend upon the definition of @{term initState}, they cannot
+   be moved up.*}
 
 lemma used_parts_subset_parts [rule_format]:
      "\<forall>X \<in> used evs. parts {X} \<subseteq> used evs"
@@ -186,14 +187,10 @@
  prefer 2
  apply (simp add: used_Cons)
  apply (rule ballI)  
- apply (case_tac a, auto)
- apply (drule parts_cut, assumption, simp) 
- apply (drule parts_cut, assumption, simp) 
+ apply (case_tac a, auto)  
+apply (auto dest!: parts_cut) 
 txt{*Base case*}
-apply (simp add: used_Nil, clarify) 
-apply (rename_tac B) 
-apply (rule_tac x=B in exI) 
-apply (case_tac B, auto) 
+apply (simp add: used_Nil) 
 done
 
 lemma MPair_used_D: "{|X,Y|} \<in> used H ==> X \<in> used H & Y \<in> used H"
@@ -218,6 +215,9 @@
 lemma Crypt_notin_initState: "Crypt K X \<notin> parts (initState B)"
 by (induct B, auto)
 
+lemma Crypt_notin_used_empty [simp]: "Crypt K X \<notin> used []"
+by (simp add: Crypt_notin_initState used_Nil)
+
 
 (*** Basic properties of shrK ***)
 
--- a/src/HOL/Auth/Recur.thy	Tue Apr 29 12:36:40 2003 +0200
+++ b/src/HOL/Auth/Recur.thy	Tue Apr 29 12:36:49 2003 +0200
@@ -392,8 +392,8 @@
 apply blast
 txt{*Inductive step of respond*}
 apply (intro allI conjI impI, simp_all)
-txt{*by unicity, either B=Aa or B=A', a contradiction if B \<in> bad*}
-apply (blast dest: unique_session_keys [OF _ respond_certificate])
+txt{*by unicity, either B=Aa or B=A', a contradiction if B \<in> bad*}   
+apply (blast dest: unique_session_keys respond_certificate)
 apply (blast dest!: respond_certificate)
 apply (blast dest!: resp_analz_insert)
 done