keyfree: The set of key-free messages (and associated theorems)

--- a/src/HOL/Auth/Message.thy	Mon Jun 27 09:42:46 2011 +0200
+++ b/src/HOL/Auth/Message.thy	Tue Jun 28 12:47:32 2011 +0100
@@ -811,6 +811,39 @@
 lemmas pushes = pushKeys pushCrypts
 
 
+subsection{*The set of key-free messages*}
+
+(*Note that even the encryption of a key-free message remains key-free.
+  This concept is valuable because of the theorem analz_keyfree_into_Un, proved below. *)
+
+inductive_set
+  keyfree :: "msg set"
+  where
+    Agent:  "Agent A \<in> keyfree"
+  | Number: "Number N \<in> keyfree"
+  | Nonce:  "Nonce N \<in> keyfree"
+  | Hash:   "Hash X \<in> keyfree"
+  | MPair:  "[|X \<in> keyfree;  Y \<in> keyfree|] ==> {|X,Y|} \<in> keyfree"
+  | Crypt:  "[|X \<in> keyfree|] ==> Crypt K X \<in> keyfree"
+
+
+declare keyfree.intros [intro] 
+
+inductive_cases keyfree_KeyE: "Key K \<in> keyfree"
+inductive_cases keyfree_MPairE: "{|X,Y|} \<in> keyfree"
+inductive_cases keyfree_CryptE: "Crypt K X \<in> keyfree"
+
+lemma parts_keyfree: "parts (keyfree) \<subseteq> keyfree"
+  by (clarify, erule parts.induct, auto elim!: keyfree_KeyE keyfree_MPairE keyfree_CryptE)
+
+(*The key-free part of a set of messages can be removed from the scope of the analz operator.*)
+lemma analz_keyfree_into_Un: "\<lbrakk>X \<in> analz (G \<union> H); G \<subseteq> keyfree\<rbrakk> \<Longrightarrow> X \<in> parts G \<union> analz H"
+apply (erule analz.induct, auto)
+apply (blast dest:parts.Body)
+apply (blast dest: parts.Body)
+apply (metis Un_absorb2 keyfree_KeyE mem_def parts_Un parts_keyfree sup1I2)
+done
+
 subsection{*Tactics useful for many protocol proofs*}
 ML
 {*