diff --git a/thys/Inductive_Confidentiality/DolevYao/Message.thy b/thys/Inductive_Confidentiality/DolevYao/Message.thy
--- a/thys/Inductive_Confidentiality/DolevYao/Message.thy
+++ b/thys/Inductive_Confidentiality/DolevYao/Message.thy
@@ -1,926 +1,914 @@
 (*  Title:      HOL/Auth/Message.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1996  University of Cambridge
 
 Datatypes of agents and messages;
 Inductive relations "parts", "analz" and "synth"
 *)
 
 section\<open>Theory of Agents and Messages for Security Protocols against Dolev-Yao\<close>
 
 theory Message
 imports Main
 begin
 
 (*Needed occasionally with spy_analz_tac, e.g. in analz_insert_Key_newK*)
 lemma [simp] : "A \<union> (B \<union> A) = B \<union> A"
 by blast
 
 type_synonym
   key = nat
 
 consts
   all_symmetric :: bool        \<comment> \<open>true if all keys are symmetric\<close>
   invKey        :: "key=>key"  \<comment> \<open>inverse of a symmetric key\<close>
 
 specification (invKey)
   invKey [simp]: "invKey (invKey K) = K"
   invKey_symmetric: "all_symmetric --> invKey = id"
     by (rule exI [of _ id], auto)
 
 
 text\<open>The inverse of a symmetric key is itself; that of a public key
       is the private key and vice versa\<close>
 
 definition symKeys :: "key set" where
   "symKeys == {K. invKey K = K}"
 
 datatype  \<comment> \<open>We allow any number of friendly agents\<close>
   agent = Server | Friend nat | Spy
 
 datatype
      msg = Agent  agent     \<comment> \<open>Agent names\<close>
          | Number nat       \<comment> \<open>Ordinary integers, timestamps, ...\<close>
          | Nonce  nat       \<comment> \<open>Unguessable nonces\<close>
          | Key    key       \<comment> \<open>Crypto keys\<close>
          | Hash   msg       \<comment> \<open>Hashing\<close>
          | MPair  msg msg   \<comment> \<open>Compound messages\<close>
          | Crypt  key msg   \<comment> \<open>Encryption, public- or shared-key\<close>
 
 
 text\<open>Concrete syntax: messages appear as \<open>\<lbrace>A,B,NA\<rbrace>\<close>, etc...\<close>
 syntax
   "_MTuple" :: "['a, args] => 'a * 'b"  ("(2\<lbrace>_,/ _\<rbrace>)")
 translations
   "\<lbrace>x, y, z\<rbrace>"   == "\<lbrace>x, \<lbrace>y, z\<rbrace>\<rbrace>"
   "\<lbrace>x, y\<rbrace>"      == "CONST MPair x y"
 
 
 definition HPair :: "[msg,msg] => msg" ("(4Hash[_] /_)" [0, 1000]) where
     \<comment> \<open>Message Y paired with a MAC computed with the help of X\<close>
     "Hash[X] Y == \<lbrace> Hash\<lbrace>X,Y\<rbrace>, Y\<rbrace>"
 
 definition keysFor :: "msg set => key set" where
     \<comment> \<open>Keys useful to decrypt elements of a message set\<close>
   "keysFor H == invKey ` {K. \<exists>X. Crypt K X \<in> H}"
 
 
 subsection\<open>Inductive definition of all parts of a message\<close>
 
 inductive_set
   parts :: "msg set => msg set"
   for H :: "msg set"
   where
     Inj [intro]:               "X \<in> H ==> X \<in> parts H"
   | Fst:         "\<lbrace>X,Y\<rbrace>   \<in> parts H ==> X \<in> parts H"
   | Snd:         "\<lbrace>X,Y\<rbrace>   \<in> parts H ==> Y \<in> parts H"
   | Body:        "Crypt K X \<in> parts H ==> X \<in> parts H"
 
 
 text\<open>Monotonicity\<close>
 lemma parts_mono: "G \<subseteq> H ==> parts(G) \<subseteq> parts(H)"
 apply auto
 apply (erule parts.induct)
 apply (blast dest: parts.Fst parts.Snd parts.Body)+
 done
 
 
 text\<open>Equations hold because constructors are injective.\<close>
 lemma Friend_image_eq [simp]: "(Friend x \<in> Friend`A) = (x:A)"
 by auto
 
 lemma Key_image_eq [simp]: "(Key x \<in> Key`A) = (x\<in>A)"
 by auto
 
 lemma Nonce_Key_image_eq [simp]: "(Nonce x \<notin> Key`A)"
 by auto
 
 
 subsection\<open>Inverse of keys\<close>
 
 lemma invKey_eq [simp]: "(invKey K = invKey K') = (K=K')"
 by (metis invKey)
 
 
 subsection\<open>keysFor operator\<close>
 
 lemma keysFor_empty [simp]: "keysFor {} = {}"
 by (unfold keysFor_def, blast)
 
 lemma keysFor_Un [simp]: "keysFor (H \<union> H') = keysFor H \<union> keysFor H'"
 by (unfold keysFor_def, blast)
 
 lemma keysFor_UN [simp]: "keysFor (\<Union>i\<in>A. H i) = (\<Union>i\<in>A. keysFor (H i))"
 by (unfold keysFor_def, blast)
 
 text\<open>Monotonicity\<close>
 lemma keysFor_mono: "G \<subseteq> H ==> keysFor(G) \<subseteq> keysFor(H)"
 by (unfold keysFor_def, blast)
 
 lemma keysFor_insert_Agent [simp]: "keysFor (insert (Agent A) H) = keysFor H"
 by (unfold keysFor_def, auto)
 
 lemma keysFor_insert_Nonce [simp]: "keysFor (insert (Nonce N) H) = keysFor H"
 by (unfold keysFor_def, auto)
 
 lemma keysFor_insert_Number [simp]: "keysFor (insert (Number N) H) = keysFor H"
 by (unfold keysFor_def, auto)
 
 lemma keysFor_insert_Key [simp]: "keysFor (insert (Key K) H) = keysFor H"
 by (unfold keysFor_def, auto)
 
 lemma keysFor_insert_Hash [simp]: "keysFor (insert (Hash X) H) = keysFor H"
 by (unfold keysFor_def, auto)
 
 lemma keysFor_insert_MPair [simp]: "keysFor (insert \<lbrace>X,Y\<rbrace> H) = keysFor H"
 by (unfold keysFor_def, auto)
 
 lemma keysFor_insert_Crypt [simp]:
     "keysFor (insert (Crypt K X) H) = insert (invKey K) (keysFor H)"
 by (unfold keysFor_def, auto)
 
 lemma keysFor_image_Key [simp]: "keysFor (Key`E) = {}"
 by (unfold keysFor_def, auto)
 
 lemma Crypt_imp_invKey_keysFor: "Crypt K X \<in> H ==> invKey K \<in> keysFor H"
 by (unfold keysFor_def, blast)
 
 
 subsection\<open>Inductive relation "parts"\<close>
 
 lemma MPair_parts:
      "[| \<lbrace>X,Y\<rbrace> \<in> parts H;
          [| X \<in> parts H; Y \<in> parts H |] ==> P |] ==> P"
 by (blast dest: parts.Fst parts.Snd)
 
 declare MPair_parts [elim!]  parts.Body [dest!]
 text\<open>NB These two rules are UNSAFE in the formal sense, as they discard the
      compound message.  They work well on THIS FILE.
   \<open>MPair_parts\<close> is left as SAFE because it speeds up proofs.
   The Crypt rule is normally kept UNSAFE to avoid breaking up certificates.\<close>
 
 lemma parts_increasing: "H \<subseteq> parts(H)"
 by blast
 
 lemmas parts_insertI = subset_insertI [THEN parts_mono, THEN subsetD]
 
 lemma parts_empty [simp]: "parts{} = {}"
 apply safe
 apply (erule parts.induct, blast+)
 done
 
 lemma parts_emptyE [elim!]: "X\<in> parts{} ==> P"
 by simp
 
 text\<open>WARNING: loops if H = {Y}, therefore must not be repeated!\<close>
 lemma parts_singleton: "X\<in> parts H ==> \<exists>Y\<in>H. X\<in> parts {Y}"
 by (erule parts.induct, fast+)
 
 
 subsubsection\<open>Unions\<close>
 
 lemma parts_Un_subset1: "parts(G) \<union> parts(H) \<subseteq> parts(G \<union> H)"
 by (intro Un_least parts_mono Un_upper1 Un_upper2)
 
 lemma parts_Un_subset2: "parts(G \<union> H) \<subseteq> parts(G) \<union> parts(H)"
 apply (rule subsetI)
 apply (erule parts.induct, blast+)
 done
 
 lemma parts_Un [simp]: "parts(G \<union> H) = parts(G) \<union> parts(H)"
 by (intro equalityI parts_Un_subset1 parts_Un_subset2)
 
 lemma parts_insert: "parts (insert X H) = parts {X} \<union> parts H"
 by (metis insert_is_Un parts_Un)
 
 text\<open>TWO inserts to avoid looping.  This rewrite is better than nothing.
   Not suitable for Addsimps: its behaviour can be strange.\<close>
 lemma parts_insert2:
      "parts (insert X (insert Y H)) = parts {X} \<union> parts {Y} \<union> parts H"
 by (metis Un_commute Un_empty_right Un_insert_right insert_is_Un parts_Un)
 
-lemma parts_UN_subset1: "(\<Union>x\<in>A. parts(H x)) \<subseteq> parts(\<Union>x\<in>A. H x)"
-by (intro UN_least parts_mono UN_upper)
-
-lemma parts_UN_subset2: "parts(\<Union>x\<in>A. H x) \<subseteq> (\<Union>x\<in>A. parts(H x))"
-apply (rule subsetI)
-apply (erule parts.induct, blast+)
-done
-
-lemma parts_UN [simp]: "parts(\<Union>x\<in>A. H x) = (\<Union>x\<in>A. parts(H x))"
-by (intro equalityI parts_UN_subset1 parts_UN_subset2)
-
-text\<open>Added to simplify arguments to parts, analz and synth.
-  NOTE: the UN versions are no longer used!\<close>
+text\<open>Added to simplify arguments to parts, analz and synth.\<close>
 
 
 text\<open>This allows \<open>blast\<close> to simplify occurrences of
   @{term "parts(G\<union>H)"} in the assumption.\<close>
 lemmas in_parts_UnE = parts_Un [THEN equalityD1, THEN subsetD, THEN UnE]
 declare in_parts_UnE [elim!]
 
 
 lemma parts_insert_subset: "insert X (parts H) \<subseteq> parts(insert X H)"
 by (blast intro: parts_mono [THEN [2] rev_subsetD])
 
 subsubsection\<open>Idempotence and transitivity\<close>
 
 lemma parts_partsD [dest!]: "X\<in> parts (parts H) ==> X\<in> parts H"
 by (erule parts.induct, blast+)
 
 lemma parts_idem [simp]: "parts (parts H) = parts H"
 by blast
 
 lemma parts_subset_iff [simp]: "(parts G \<subseteq> parts H) = (G \<subseteq> parts H)"
 by (metis parts_idem parts_increasing parts_mono subset_trans)
 
 lemma parts_trans: "[| X\<in> parts G;  G \<subseteq> parts H |] ==> X\<in> parts H"
 by (metis parts_subset_iff subsetD)
 
 text\<open>Cut\<close>
 lemma parts_cut:
      "[| Y\<in> parts (insert X G);  X\<in> parts H |] ==> Y\<in> parts (G \<union> H)"
 by (blast intro: parts_trans)
 
 lemma parts_cut_eq [simp]: "X\<in> parts H ==> parts (insert X H) = parts H"
 by (metis insert_absorb parts_idem parts_insert)
 
 
 subsubsection\<open>Rewrite rules for pulling out atomic messages\<close>
 
 lemmas parts_insert_eq_I = equalityI [OF subsetI parts_insert_subset]
 
 
 lemma parts_insert_Agent [simp]:
      "parts (insert (Agent agt) H) = insert (Agent agt) (parts H)"
 apply (rule parts_insert_eq_I)
 apply (erule parts.induct, auto)
 done
 
 lemma parts_insert_Nonce [simp]:
      "parts (insert (Nonce N) H) = insert (Nonce N) (parts H)"
 apply (rule parts_insert_eq_I)
 apply (erule parts.induct, auto)
 done
 
 lemma parts_insert_Number [simp]:
      "parts (insert (Number N) H) = insert (Number N) (parts H)"
 apply (rule parts_insert_eq_I)
 apply (erule parts.induct, auto)
 done
 
 lemma parts_insert_Key [simp]:
      "parts (insert (Key K) H) = insert (Key K) (parts H)"
 apply (rule parts_insert_eq_I)
 apply (erule parts.induct, auto)
 done
 
 lemma parts_insert_Hash [simp]:
      "parts (insert (Hash X) H) = insert (Hash X) (parts H)"
 apply (rule parts_insert_eq_I)
 apply (erule parts.induct, auto)
 done
 
 lemma parts_insert_Crypt [simp]:
      "parts (insert (Crypt K X) H) = insert (Crypt K X) (parts (insert X H))"
 apply (rule equalityI)
 apply (rule subsetI)
 apply (erule parts.induct, auto)
 apply (blast intro: parts.Body)
 done
 
 lemma parts_insert_MPair [simp]:
      "parts (insert \<lbrace>X,Y\<rbrace> H) =
           insert \<lbrace>X,Y\<rbrace> (parts (insert X (insert Y H)))"
 apply (rule equalityI)
 apply (rule subsetI)
 apply (erule parts.induct, auto)
 apply (blast intro: parts.Fst parts.Snd)+
 done
 
 lemma parts_image_Key [simp]: "parts (Key`N) = Key`N"
 apply auto
 apply (erule parts.induct, auto)
 done
 
 
 text\<open>In any message, there is an upper bound N on its greatest nonce.\<close>
 lemma msg_Nonce_supply: "\<exists>N. \<forall>n. N\<le>n --> Nonce n \<notin> parts {msg}"
 apply (induct msg)
 apply (simp_all (no_asm_simp) add: exI parts_insert2)
 txt\<open>Nonce case\<close>
 apply (metis Suc_n_not_le_n)
 txt\<open>MPair case: metis works out the necessary sum itself!\<close>
 apply (metis le_trans nat_le_linear)
 done
 
 
 subsection\<open>Inductive relation "analz"\<close>
 
 text\<open>Inductive definition of "analz" -- what can be broken down from a set of
     messages, including keys.  A form of downward closure.  Pairs can
     be taken apart; messages decrypted with known keys.\<close>
 
 inductive_set
   analz :: "msg set => msg set"
   for H :: "msg set"
   where
     Inj [intro,simp] :    "X \<in> H ==> X \<in> analz H"
   | Fst:     "\<lbrace>X,Y\<rbrace> \<in> analz H ==> X \<in> analz H"
   | Snd:     "\<lbrace>X,Y\<rbrace> \<in> analz H ==> Y \<in> analz H"
   | Decrypt [dest]:
              "[|Crypt K X \<in> analz H; Key(invKey K): analz H|] ==> X \<in> analz H"
 
 
 text\<open>Monotonicity; Lemma 1 of Lowe's paper\<close>
 lemma analz_mono: "G\<subseteq>H ==> analz(G) \<subseteq> analz(H)"
 apply auto
 apply (erule analz.induct)
 apply (auto dest: analz.Fst analz.Snd)
 done
 
 text\<open>Making it safe speeds up proofs\<close>
 lemma MPair_analz [elim!]:
      "[| \<lbrace>X,Y\<rbrace> \<in> analz H;
              [| X \<in> analz H; Y \<in> analz H |] ==> P
           |] ==> P"
 by (blast dest: analz.Fst analz.Snd)
 
 lemma analz_increasing: "H \<subseteq> analz(H)"
 by blast
 
 lemma analz_subset_parts: "analz H \<subseteq> parts H"
 apply (rule subsetI)
 apply (erule analz.induct, blast+)
 done
 
 lemmas analz_into_parts = analz_subset_parts [THEN subsetD]
 
 lemmas not_parts_not_analz = analz_subset_parts [THEN contra_subsetD]
 
 
 lemma parts_analz [simp]: "parts (analz H) = parts H"
 by (metis analz_increasing analz_subset_parts equalityI parts_mono parts_subset_iff)
 
 lemma analz_parts [simp]: "analz (parts H) = parts H"
 apply auto
 apply (erule analz.induct, auto)
 done
 
 lemmas analz_insertI = subset_insertI [THEN analz_mono, THEN [2] rev_subsetD]
 
 subsubsection\<open>General equational properties\<close>
 
 lemma analz_empty [simp]: "analz{} = {}"
 apply safe
 apply (erule analz.induct, blast+)
 done
 
 text\<open>Converse fails: we can analz more from the union than from the
   separate parts, as a key in one might decrypt a message in the other\<close>
 lemma analz_Un: "analz(G) \<union> analz(H) \<subseteq> analz(G \<union> H)"
 by (intro Un_least analz_mono Un_upper1 Un_upper2)
 
 lemma analz_insert: "insert X (analz H) \<subseteq> analz(insert X H)"
 by (blast intro: analz_mono [THEN [2] rev_subsetD])
 
 subsubsection\<open>Rewrite rules for pulling out atomic messages\<close>
 
 lemmas analz_insert_eq_I = equalityI [OF subsetI analz_insert]
 
 lemma analz_insert_Agent [simp]:
      "analz (insert (Agent agt) H) = insert (Agent agt) (analz H)"
 apply (rule analz_insert_eq_I)
 apply (erule analz.induct, auto)
 done
 
 lemma analz_insert_Nonce [simp]:
      "analz (insert (Nonce N) H) = insert (Nonce N) (analz H)"
 apply (rule analz_insert_eq_I)
 apply (erule analz.induct, auto)
 done
 
 lemma analz_insert_Number [simp]:
      "analz (insert (Number N) H) = insert (Number N) (analz H)"
 apply (rule analz_insert_eq_I)
 apply (erule analz.induct, auto)
 done
 
 lemma analz_insert_Hash [simp]:
      "analz (insert (Hash X) H) = insert (Hash X) (analz H)"
 apply (rule analz_insert_eq_I)
 apply (erule analz.induct, auto)
 done
 
 text\<open>Can only pull out Keys if they are not needed to decrypt the rest\<close>
 lemma analz_insert_Key [simp]:
     "K \<notin> keysFor (analz H) ==>
           analz (insert (Key K) H) = insert (Key K) (analz H)"
 apply (unfold keysFor_def)
 apply (rule analz_insert_eq_I)
 apply (erule analz.induct, auto)
 done
 
 lemma analz_insert_MPair [simp]:
      "analz (insert \<lbrace>X,Y\<rbrace> H) =
           insert \<lbrace>X,Y\<rbrace> (analz (insert X (insert Y H)))"
 apply (rule equalityI)
 apply (rule subsetI)
 apply (erule analz.induct, auto)
 apply (erule analz.induct)
 apply (blast intro: analz.Fst analz.Snd)+
 done
 
 text\<open>Can pull out enCrypted message if the Key is not known\<close>
 lemma analz_insert_Crypt:
      "Key (invKey K) \<notin> analz H
       ==> analz (insert (Crypt K X) H) = insert (Crypt K X) (analz H)"
 apply (rule analz_insert_eq_I)
 apply (erule analz.induct, auto)
 
 done
 
 lemma lemma1: "Key (invKey K) \<in> analz H ==>
                analz (insert (Crypt K X) H) \<subseteq>
                insert (Crypt K X) (analz (insert X H))"
 apply (rule subsetI)
 apply (erule_tac x = x in analz.induct, auto)
 done
 
 lemma lemma2: "Key (invKey K) \<in> analz H ==>
                insert (Crypt K X) (analz (insert X H)) \<subseteq>
                analz (insert (Crypt K X) H)"
 apply auto
 apply (erule_tac x = x in analz.induct, auto)
 apply (blast intro: analz_insertI analz.Decrypt)
 done
 
 lemma analz_insert_Decrypt:
      "Key (invKey K) \<in> analz H ==>
                analz (insert (Crypt K X) H) =
                insert (Crypt K X) (analz (insert X H))"
 by (intro equalityI lemma1 lemma2)
 
 text\<open>Case analysis: either the message is secure, or it is not! Effective,
 but can cause subgoals to blow up! Use with \<open>if_split\<close>; apparently
 \<open>split_tac\<close> does not cope with patterns such as @{term"analz (insert
 (Crypt K X) H)"}\<close>
 lemma analz_Crypt_if [simp]:
      "analz (insert (Crypt K X) H) =
           (if (Key (invKey K) \<in> analz H)
            then insert (Crypt K X) (analz (insert X H))
            else insert (Crypt K X) (analz H))"
 by (simp add: analz_insert_Crypt analz_insert_Decrypt)
 
 
 text\<open>This rule supposes "for the sake of argument" that we have the key.\<close>
 lemma analz_insert_Crypt_subset:
      "analz (insert (Crypt K X) H) \<subseteq>
            insert (Crypt K X) (analz (insert X H))"
 apply (rule subsetI)
 apply (erule analz.induct, auto)
 done
 
 
 lemma analz_image_Key [simp]: "analz (Key`N) = Key`N"
 apply auto
 apply (erule analz.induct, auto)
 done
 
 
 subsubsection\<open>Idempotence and transitivity\<close>
 
 lemma analz_analzD [dest!]: "X\<in> analz (analz H) ==> X\<in> analz H"
 by (erule analz.induct, blast+)
 
 lemma analz_idem [simp]: "analz (analz H) = analz H"
 by blast
 
 lemma analz_subset_iff [simp]: "(analz G \<subseteq> analz H) = (G \<subseteq> analz H)"
 by (metis analz_idem analz_increasing analz_mono subset_trans)
 
 lemma analz_trans: "[| X\<in> analz G;  G \<subseteq> analz H |] ==> X\<in> analz H"
 by (drule analz_mono, blast)
 
 text\<open>Cut; Lemma 2 of Lowe\<close>
 lemma analz_cut: "[| Y\<in> analz (insert X H);  X\<in> analz H |] ==> Y\<in> analz H"
 by (erule analz_trans, blast)
 
 (*Cut can be proved easily by induction on
    "Y: analz (insert X H) ==> X: analz H --> Y: analz H"
 *)
 
 text\<open>This rewrite rule helps in the simplification of messages that involve
   the forwarding of unknown components (X).  Without it, removing occurrences
   of X can be very complicated.\<close>
 lemma analz_insert_eq: "X\<in> analz H ==> analz (insert X H) = analz H"
 by (metis analz_cut analz_insert_eq_I insert_absorb)
 
 
 text\<open>A congruence rule for "analz"\<close>
 
 lemma analz_subset_cong:
      "[| analz G \<subseteq> analz G'; analz H \<subseteq> analz H' |]
       ==> analz (G \<union> H) \<subseteq> analz (G' \<union> H')"
 by (metis Un_mono analz_Un analz_subset_iff subset_trans)
 
 lemma analz_cong:
      "[| analz G = analz G'; analz H = analz H' |]
       ==> analz (G \<union> H) = analz (G' \<union> H')"
 by (intro equalityI analz_subset_cong, simp_all)
 
 lemma analz_insert_cong:
      "analz H = analz H' ==> analz(insert X H) = analz(insert X H')"
 by (force simp only: insert_def intro!: analz_cong)
 
 text\<open>If there are no pairs or encryptions then analz does nothing\<close>
 lemma analz_trivial:
      "[| \<forall>X Y. \<lbrace>X,Y\<rbrace> \<notin> H;  \<forall>X K. Crypt K X \<notin> H |] ==> analz H = H"
 apply safe
 apply (erule analz.induct, blast+)
 done
 
 
 subsection\<open>Inductive relation "synth"\<close>
 
 text\<open>Inductive definition of "synth" -- what can be built up from a set of
     messages.  A form of upward closure.  Pairs can be built, messages
     encrypted with known keys.  Agent names are public domain.
     Numbers can be guessed, but Nonces cannot be.\<close>
 
 inductive_set
   synth :: "msg set => msg set"
   for H :: "msg set"
   where
     Inj    [intro]:   "X \<in> H ==> X \<in> synth H"
   | Agent  [intro]:   "Agent agt \<in> synth H"
   | Number [intro]:   "Number n  \<in> synth H"
   | Hash   [intro]:   "X \<in> synth H ==> Hash X \<in> synth H"
   | MPair  [intro]:   "[|X \<in> synth H;  Y \<in> synth H|] ==> \<lbrace>X,Y\<rbrace> \<in> synth H"
   | Crypt  [intro]:   "[|X \<in> synth H;  Key(K) \<in> H|] ==> Crypt K X \<in> synth H"
 
 text\<open>Monotonicity\<close>
 lemma synth_mono: "G\<subseteq>H ==> synth(G) \<subseteq> synth(H)"
   by (auto, erule synth.induct, auto)
 
 text\<open>NO \<open>Agent_synth\<close>, as any Agent name can be synthesized.
   The same holds for @{term Number}\<close>
 
 inductive_simps synth_simps [iff]:
  "Nonce n \<in> synth H"
  "Key K \<in> synth H"
  "Hash X \<in> synth H"
  "\<lbrace>X,Y\<rbrace> \<in> synth H"
  "Crypt K X \<in> synth H"
 
 lemma synth_increasing: "H \<subseteq> synth(H)"
 by blast
 
 subsubsection\<open>Unions\<close>
 
 text\<open>Converse fails: we can synth more from the union than from the
   separate parts, building a compound message using elements of each.\<close>
 lemma synth_Un: "synth(G) \<union> synth(H) \<subseteq> synth(G \<union> H)"
 by (intro Un_least synth_mono Un_upper1 Un_upper2)
 
 lemma synth_insert: "insert X (synth H) \<subseteq> synth(insert X H)"
 by (blast intro: synth_mono [THEN [2] rev_subsetD])
 
 subsubsection\<open>Idempotence and transitivity\<close>
 
 lemma synth_synthD [dest!]: "X\<in> synth (synth H) ==> X\<in> synth H"
 by (erule synth.induct, auto)
 
 lemma synth_idem: "synth (synth H) = synth H"
 by blast
 
 lemma synth_subset_iff [simp]: "(synth G \<subseteq> synth H) = (G \<subseteq> synth H)"
 by (metis subset_trans synth_idem synth_increasing synth_mono)
 
 lemma synth_trans: "[| X\<in> synth G;  G \<subseteq> synth H |] ==> X\<in> synth H"
 by (drule synth_mono, blast)
 
 text\<open>Cut; Lemma 2 of Lowe\<close>
 lemma synth_cut: "[| Y\<in> synth (insert X H);  X\<in> synth H |] ==> Y\<in> synth H"
 by (erule synth_trans, blast)
 
 lemma Agent_synth [simp]: "Agent A \<in> synth H"
 by blast
 
 lemma Number_synth [simp]: "Number n \<in> synth H"
 by blast
 
 lemma Nonce_synth_eq [simp]: "(Nonce N \<in> synth H) = (Nonce N \<in> H)"
 by blast
 
 lemma Key_synth_eq [simp]: "(Key K \<in> synth H) = (Key K \<in> H)"
 by blast
 
 lemma Crypt_synth_eq [simp]:
      "Key K \<notin> H ==> (Crypt K X \<in> synth H) = (Crypt K X \<in> H)"
 by blast
 
 
 lemma keysFor_synth [simp]:
     "keysFor (synth H) = keysFor H \<union> invKey`{K. Key K \<in> H}"
 by (unfold keysFor_def, blast)
 
 
 subsubsection\<open>Combinations of parts, analz and synth\<close>
 
 lemma parts_synth [simp]: "parts (synth H) = parts H \<union> synth H"
 apply (rule equalityI)
 apply (rule subsetI)
 apply (erule parts.induct)
 apply (blast intro: synth_increasing [THEN parts_mono, THEN subsetD]
                     parts.Fst parts.Snd parts.Body)+
 done
 
 lemma analz_analz_Un [simp]: "analz (analz G \<union> H) = analz (G \<union> H)"
 apply (intro equalityI analz_subset_cong)+
 apply simp_all
 done
 
 lemma analz_synth_Un [simp]: "analz (synth G \<union> H) = analz (G \<union> H) \<union> synth G"
 apply (rule equalityI)
 apply (rule subsetI)
 apply (erule analz.induct)
 prefer 5 apply (blast intro: analz_mono [THEN [2] rev_subsetD])
 apply (blast intro: analz.Fst analz.Snd analz.Decrypt)+
 done
 
 lemma analz_synth [simp]: "analz (synth H) = analz H \<union> synth H"
 by (metis Un_empty_right analz_synth_Un)
 
 
 subsubsection\<open>For reasoning about the Fake rule in traces\<close>
 
 lemma parts_insert_subset_Un: "X\<in> G ==> parts(insert X H) \<subseteq> parts G \<union> parts H"
 by (metis UnCI Un_upper2 insert_subset parts_Un parts_mono)
 
 text\<open>More specifically for Fake. See also \<open>Fake_parts_sing\<close> below\<close>
 lemma Fake_parts_insert:
      "X \<in> synth (analz H) ==>
       parts (insert X H) \<subseteq> synth (analz H) \<union> parts H"
 by (metis Un_commute analz_increasing insert_subset parts_analz parts_mono
           parts_synth synth_mono synth_subset_iff)
 
 lemma Fake_parts_insert_in_Un:
      "[|Z \<in> parts (insert X H);  X: synth (analz H)|]
       ==> Z \<in>  synth (analz H) \<union> parts H"
 by (metis Fake_parts_insert subsetD)
 
 text\<open>@{term H} is sometimes @{term"Key ` KK \<union> spies evs"}, so can't put
   @{term "G=H"}.\<close>
 lemma Fake_analz_insert:
      "X\<in> synth (analz G) ==>
       analz (insert X H) \<subseteq> synth (analz G) \<union> analz (G \<union> H)"
 apply (rule subsetI)
 apply (subgoal_tac "x \<in> analz (synth (analz G) \<union> H)", force)
 apply (blast intro: analz_mono [THEN [2] rev_subsetD] analz_mono [THEN synth_mono, THEN [2] rev_subsetD])
 done
 
 lemma analz_conj_parts [simp]:
      "(X \<in> analz H \<and> X \<in> parts H) = (X \<in> analz H)"
 by (blast intro: analz_subset_parts [THEN subsetD])
 
 lemma analz_disj_parts [simp]:
      "(X \<in> analz H | X \<in> parts H) = (X \<in> parts H)"
 by (blast intro: analz_subset_parts [THEN subsetD])
 
 text\<open>Without this equation, other rules for synth and analz would yield
   redundant cases\<close>
 lemma MPair_synth_analz [iff]:
      "(\<lbrace>X,Y\<rbrace> \<in> synth (analz H)) =
       (X \<in> synth (analz H) \<and> Y \<in> synth (analz H))"
 by blast
 
 lemma Crypt_synth_analz:
      "[| Key K \<in> analz H;  Key (invKey K) \<in> analz H |]
        ==> (Crypt K X \<in> synth (analz H)) = (X \<in> synth (analz H))"
 by blast
 
 
 lemma Hash_synth_analz [simp]:
      "X \<notin> synth (analz H)
       ==> (Hash\<lbrace>X,Y\<rbrace> \<in> synth (analz H)) = (Hash\<lbrace>X,Y\<rbrace> \<in> analz H)"
 by blast
 
 
 subsection\<open>HPair: a combination of Hash and MPair\<close>
 
 subsubsection\<open>Freeness\<close>
 
 lemma Agent_neq_HPair: "Agent A ~= Hash[X] Y"
 by (unfold HPair_def, simp)
 
 lemma Nonce_neq_HPair: "Nonce N ~= Hash[X] Y"
 by (unfold HPair_def, simp)
 
 lemma Number_neq_HPair: "Number N ~= Hash[X] Y"
 by (unfold HPair_def, simp)
 
 lemma Key_neq_HPair: "Key K ~= Hash[X] Y"
 by (unfold HPair_def, simp)
 
 lemma Hash_neq_HPair: "Hash Z ~= Hash[X] Y"
 by (unfold HPair_def, simp)
 
 lemma Crypt_neq_HPair: "Crypt K X' ~= Hash[X] Y"
 by (unfold HPair_def, simp)
 
 lemmas HPair_neqs = Agent_neq_HPair Nonce_neq_HPair Number_neq_HPair
                     Key_neq_HPair Hash_neq_HPair Crypt_neq_HPair
 
 declare HPair_neqs [iff]
 declare HPair_neqs [symmetric, iff]
 
 lemma HPair_eq [iff]: "(Hash[X'] Y' = Hash[X] Y) = (X' = X \<and> Y'=Y)"
 by (simp add: HPair_def)
 
 lemma MPair_eq_HPair [iff]:
      "(\<lbrace>X',Y'\<rbrace> = Hash[X] Y) = (X' = Hash\<lbrace>X,Y\<rbrace> \<and> Y'=Y)"
 by (simp add: HPair_def)
 
 lemma HPair_eq_MPair [iff]:
      "(Hash[X] Y = \<lbrace>X',Y'\<rbrace>) = (X' = Hash\<lbrace>X,Y\<rbrace> \<and> Y'=Y)"
 by (auto simp add: HPair_def)
 
 
 subsubsection\<open>Specialized laws, proved in terms of those for Hash and MPair\<close>
 
 lemma keysFor_insert_HPair [simp]: "keysFor (insert (Hash[X] Y) H) = keysFor H"
 by (simp add: HPair_def)
 
 lemma parts_insert_HPair [simp]:
     "parts (insert (Hash[X] Y) H) =
      insert (Hash[X] Y) (insert (Hash\<lbrace>X,Y\<rbrace>) (parts (insert Y H)))"
 by (simp add: HPair_def)
 
 lemma analz_insert_HPair [simp]:
     "analz (insert (Hash[X] Y) H) =
      insert (Hash[X] Y) (insert (Hash\<lbrace>X,Y\<rbrace>) (analz (insert Y H)))"
 by (simp add: HPair_def)
 
 lemma HPair_synth_analz [simp]:
      "X \<notin> synth (analz H)
     ==> (Hash[X] Y \<in> synth (analz H)) =
         (Hash \<lbrace>X, Y\<rbrace> \<in> analz H \<and> Y \<in> synth (analz H))"
 by (auto simp add: HPair_def)
 
 
 text\<open>We do NOT want Crypt... messages broken up in protocols!!\<close>
 declare parts.Body [rule del]
 
 
 text\<open>Rewrites to push in Key and Crypt messages, so that other messages can
     be pulled out using the \<open>analz_insert\<close> rules\<close>
 
 lemmas pushKeys =
   insert_commute [of "Key K" "Agent C"]
   insert_commute [of "Key K" "Nonce N"]
   insert_commute [of "Key K" "Number N"]
   insert_commute [of "Key K" "Hash X"]
   insert_commute [of "Key K" "MPair X Y"]
   insert_commute [of "Key K" "Crypt X K'"]
   for K C N X Y K'
 
 lemmas pushCrypts =
   insert_commute [of "Crypt X K" "Agent C"]
   insert_commute [of "Crypt X K" "Agent C"]
   insert_commute [of "Crypt X K" "Nonce N"]
   insert_commute [of "Crypt X K" "Number N"]
   insert_commute [of "Crypt X K" "Hash X'"]
   insert_commute [of "Crypt X K" "MPair X' Y"]
   for X K C N X' Y
 
 text\<open>Cannot be added with \<open>[simp]\<close> -- messages should not always be
   re-ordered.\<close>
 lemmas pushes = pushKeys pushCrypts
 
 
 subsection\<open>The set of key-free messages\<close>
 
 (*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|] ==> \<lbrace>X,Y\<rbrace> \<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: "\<lbrace>X,Y\<rbrace> \<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 parts_Un parts_keyfree UnI2)
 done
 
 subsection\<open>Tactics useful for many protocol proofs\<close>
 ML
 \<open>
 (*Analysis of Fake cases.  Also works for messages that forward unknown parts,
   but this application is no longer necessary if analz_insert_eq is used.
   DEPENDS UPON "X" REFERRING TO THE FRADULENT MESSAGE *)
 
 fun impOfSubs th = th RSN (2, @{thm rev_subsetD})
 
 (*Apply rules to break down assumptions of the form
   Y \<in> parts(insert X H)  and  Y \<in> analz(insert X H)
 *)
 fun Fake_insert_tac ctxt =
     dresolve_tac ctxt [impOfSubs @{thm Fake_analz_insert},
                   impOfSubs @{thm Fake_parts_insert}] THEN'
     eresolve_tac ctxt [asm_rl, @{thm synth.Inj}];
 
 fun Fake_insert_simp_tac ctxt i =
   REPEAT (Fake_insert_tac ctxt i) THEN asm_full_simp_tac ctxt i;
 
 fun atomic_spy_analz_tac ctxt =
   SELECT_GOAL
    (Fake_insert_simp_tac ctxt 1 THEN
     IF_UNSOLVED
       (Blast.depth_tac
         (ctxt addIs [@{thm analz_insertI}, impOfSubs @{thm analz_subset_parts}]) 4 1));
 
 fun spy_analz_tac ctxt i =
   DETERM
    (SELECT_GOAL
      (EVERY
       [  (*push in occurrences of X...*)
        (REPEAT o CHANGED)
          (Rule_Insts.res_inst_tac ctxt [((("x", 1), Position.none), "X")] []
           (insert_commute RS ssubst) 1),
        (*...allowing further simplifications*)
        simp_tac ctxt 1,
        REPEAT (FIRSTGOAL (resolve_tac ctxt [allI,impI,notI,conjI,iffI])),
        DEPTH_SOLVE (atomic_spy_analz_tac ctxt 1)]) i);
 \<close>
 
 text\<open>By default only \<open>o_apply\<close> is built-in.  But in the presence of
 eta-expansion this means that some terms displayed as @{term "f o g"} will be
 rewritten, and others will not!\<close>
 declare o_def [simp]
 
 
 lemma Crypt_notin_image_Key [simp]: "Crypt K X \<notin> Key ` A"
 by auto
 
 lemma Hash_notin_image_Key [simp] :"Hash X \<notin> Key ` A"
 by auto
 
 lemma synth_analz_mono: "G\<subseteq>H ==> synth (analz(G)) \<subseteq> synth (analz(H))"
 by (iprover intro: synth_mono analz_mono)
 
 lemma Fake_analz_eq [simp]:
      "X \<in> synth(analz H) ==> synth (analz (insert X H)) = synth (analz H)"
 by (metis Fake_analz_insert Un_absorb Un_absorb1 Un_commute
           subset_insertI synth_analz_mono synth_increasing synth_subset_iff)
 
 text\<open>Two generalizations of \<open>analz_insert_eq\<close>\<close>
 lemma gen_analz_insert_eq [rule_format]:
      "X \<in> analz H ==> \<forall>G. H \<subseteq> G --> analz (insert X G) = analz G"
 by (blast intro: analz_cut analz_insertI analz_mono [THEN [2] rev_subsetD])
 
 lemma synth_analz_insert_eq [rule_format]:
      "X \<in> synth (analz H)
       ==> \<forall>G. H \<subseteq> G --> (Key K \<in> analz (insert X G)) = (Key K \<in> analz G)"
 apply (erule synth.induct)
 apply (simp_all add: gen_analz_insert_eq subset_trans [OF _ subset_insertI])
 done
 
 lemma Fake_parts_sing:
      "X \<in> synth (analz H) ==> parts{X} \<subseteq> synth (analz H) \<union> parts H"
 by (metis Fake_parts_insert empty_subsetI insert_mono parts_mono subset_trans)
 
 lemmas Fake_parts_sing_imp_Un = Fake_parts_sing [THEN [2] rev_subsetD]
 
 method_setup spy_analz = \<open>
     Scan.succeed (SIMPLE_METHOD' o spy_analz_tac)\<close>
     "for proving the Fake case when analz is involved"
 
 method_setup atomic_spy_analz = \<open>
     Scan.succeed (SIMPLE_METHOD' o atomic_spy_analz_tac)\<close>
     "for debugging spy_analz"
 
 method_setup Fake_insert_simp = \<open>
     Scan.succeed (SIMPLE_METHOD' o Fake_insert_simp_tac)\<close>
     "for debugging spy_analz"
 
 end
diff --git a/thys/Inductive_Confidentiality/GeneralAttacker/MessageGA.thy b/thys/Inductive_Confidentiality/GeneralAttacker/MessageGA.thy
--- a/thys/Inductive_Confidentiality/GeneralAttacker/MessageGA.thy
+++ b/thys/Inductive_Confidentiality/GeneralAttacker/MessageGA.thy
@@ -1,919 +1,907 @@
 section\<open>Theory of Agents and Messages for Security Protocols against the General Attacker\<close>
 
 theory MessageGA imports Main begin
 
 (*Needed occasionally with spy_analz_tac, e.g. in analz_insert_Key_newK*)
 lemma [simp] : "A \<union> (B \<union> A) = B \<union> A"
 by blast
 
 type_synonym
   key = nat
 
 consts
   all_symmetric :: bool        \<comment> \<open>true if all keys are symmetric\<close>
   invKey        :: "key=>key"  \<comment> \<open>inverse of a symmetric key\<close>
 
 specification (invKey)
   invKey [simp]: "invKey (invKey K) = K"
   invKey_symmetric: "all_symmetric \<longrightarrow> invKey = id"
     by (rule exI [of _ id], auto)
 
 
 text\<open>The inverse of a symmetric key is itself; that of a public key
       is the private key and vice versa\<close>
 
 definition symKeys :: "key set" where
   "symKeys == {K. invKey K = K}"
 
 datatype  \<comment> \<open>We only allow for any number of friendly agents\<close>
   agent = Friend nat
 
 datatype
      msg = Agent  agent     \<comment> \<open>Agent names\<close>
          | Number nat       \<comment> \<open>Ordinary integers, timestamps, ...\<close>
          | Nonce  nat       \<comment> \<open>Unguessable nonces\<close>
          | Key    key       \<comment> \<open>Crypto keys\<close>
          | Hash   msg       \<comment> \<open>Hashing\<close>
          | MPair  msg msg   \<comment> \<open>Compound messages\<close>
          | Crypt  key msg   \<comment> \<open>Encryption, public- or shared-key\<close>
 
 
 text\<open>Concrete syntax: messages appear as \<open>\<lbrace>A,B,NA\<rbrace>\<close>, etc...\<close>
 syntax
   "_MTuple"      :: "['a, args] => 'a * 'b"       ("(2\<lbrace>_,/ _\<rbrace>)")
 translations
   "\<lbrace>x, y, z\<rbrace>"   == "\<lbrace>x, \<lbrace>y, z\<rbrace>\<rbrace>"
   "\<lbrace>x, y\<rbrace>"      == "CONST MPair x y"
 
 
 definition HPair :: "[msg,msg] => msg" ("(4Hash[_] /_)" [0, 1000]) where
     \<comment> \<open>Message Y paired with a MAC computed with the help of X\<close>
     "Hash[X] Y == \<lbrace> Hash\<lbrace>X,Y\<rbrace>, Y\<rbrace>"
 
 definition keysFor :: "msg set => key set" where
     \<comment> \<open>Keys useful to decrypt elements of a message set\<close>
   "keysFor H == invKey ` {K. \<exists>X. Crypt K X \<in> H}"
 
 
 subsection\<open>Inductive definition of all parts of a message\<close>
 
 inductive_set
   parts :: "msg set => msg set"
   for H :: "msg set"
   where
     Inj [intro]:               "X \<in> H \<Longrightarrow> X \<in> parts H"
   | Fst:         "\<lbrace>X,Y\<rbrace>   \<in> parts H \<Longrightarrow> X \<in> parts H"
   | Snd:         "\<lbrace>X,Y\<rbrace>   \<in> parts H \<Longrightarrow> Y \<in> parts H"
   | Body:        "Crypt K X \<in> parts H \<Longrightarrow> X \<in> parts H"
 
 
 text\<open>Monotonicity\<close>
 lemma parts_mono: "G \<subseteq> H \<Longrightarrow> parts(G) \<subseteq> parts(H)"
 apply auto
 apply (erule parts.induct)
 apply (blast dest: parts.Fst parts.Snd parts.Body)+
 done
 
 
 text\<open>Equations hold because constructors are injective.\<close>
 lemma Friend_image_eq [simp]: "(Friend x \<in> Friend`A) = (x:A)"
 by auto
 
 lemma Key_image_eq [simp]: "(Key x \<in> Key`A) = (x\<in>A)"
 by auto
 
 lemma Nonce_Key_image_eq [simp]: "(Nonce x \<notin> Key`A)"
 by auto
 
 
 subsection\<open>Inverse of keys\<close>
 
 lemma invKey_eq [simp]: "(invKey K = invKey K') = (K=K')"
 by (metis invKey)
 
 
 subsection\<open>keysFor operator\<close>
 
 lemma keysFor_empty [simp]: "keysFor {} = {}"
 by (unfold keysFor_def, blast)
 
 lemma keysFor_Un [simp]: "keysFor (H \<union> H') = keysFor H \<union> keysFor H'"
 by (unfold keysFor_def, blast)
 
 lemma keysFor_UN [simp]: "keysFor (\<Union>i\<in>A. H i) = (\<Union>i\<in>A. keysFor (H i))"
 by (unfold keysFor_def, blast)
 
 text\<open>Monotonicity\<close>
 lemma keysFor_mono: "G \<subseteq> H \<Longrightarrow> keysFor(G) \<subseteq> keysFor(H)"
 by (unfold keysFor_def, blast)
 
 lemma keysFor_insert_Agent [simp]: "keysFor (insert (Agent A) H) = keysFor H"
 by (unfold keysFor_def, auto)
 
 lemma keysFor_insert_Nonce [simp]: "keysFor (insert (Nonce N) H) = keysFor H"
 by (unfold keysFor_def, auto)
 
 lemma keysFor_insert_Number [simp]: "keysFor (insert (Number N) H) = keysFor H"
 by (unfold keysFor_def, auto)
 
 lemma keysFor_insert_Key [simp]: "keysFor (insert (Key K) H) = keysFor H"
 by (unfold keysFor_def, auto)
 
 lemma keysFor_insert_Hash [simp]: "keysFor (insert (Hash X) H) = keysFor H"
 by (unfold keysFor_def, auto)
 
 lemma keysFor_insert_MPair [simp]: "keysFor (insert \<lbrace>X,Y\<rbrace> H) = keysFor H"
 by (unfold keysFor_def, auto)
 
 lemma keysFor_insert_Crypt [simp]:
     "keysFor (insert (Crypt K X) H) = insert (invKey K) (keysFor H)"
 by (unfold keysFor_def, auto)
 
 lemma keysFor_image_Key [simp]: "keysFor (Key`E) = {}"
 by (unfold keysFor_def, auto)
 
 lemma Crypt_imp_invKey_keysFor: "Crypt K X \<in> H \<Longrightarrow> invKey K \<in> keysFor H"
 by (unfold keysFor_def, blast)
 
 
 subsection\<open>Inductive relation "parts"\<close>
 
 lemma MPair_parts:
      "[| \<lbrace>X,Y\<rbrace> \<in> parts H;
          [| X \<in> parts H; Y \<in> parts H |] ==> P |] ==> P"
 by (blast dest: parts.Fst parts.Snd)
 
 declare MPair_parts [elim!]  parts.Body [dest!]
 text\<open>NB These two rules are UNSAFE in the formal sense, as they discard the
      compound message.  They work well on THIS FILE.
   \<open>MPair_parts\<close> is left as SAFE because it speeds up proofs.
   The Crypt rule is normally kept UNSAFE to avoid breaking up certificates.\<close>
 
 lemma parts_increasing: "H \<subseteq> parts(H)"
 by blast
 
 lemmas parts_insertI = subset_insertI [THEN parts_mono, THEN subsetD]
 
 lemma parts_empty [simp]: "parts{} = {}"
 apply safe
 apply (erule parts.induct, blast+)
 done
 
 lemma parts_emptyE [elim!]: "X\<in> parts{} \<Longrightarrow> P"
 by simp
 
 text\<open>WARNING: loops if H = {Y}, therefore must not be repeated!\<close>
 lemma parts_singleton: "X\<in> parts H \<Longrightarrow> \<exists>Y\<in>H. X\<in> parts {Y}"
 by (erule parts.induct, fast+)
 
 
 subsubsection\<open>Unions\<close>
 
 lemma parts_Un_subset1: "parts(G) \<union> parts(H) \<subseteq> parts(G \<union> H)"
 by (intro Un_least parts_mono Un_upper1 Un_upper2)
 
 lemma parts_Un_subset2: "parts(G \<union> H) \<subseteq> parts(G) \<union> parts(H)"
 apply (rule subsetI)
 apply (erule parts.induct, blast+)
 done
 
 lemma parts_Un [simp]: "parts(G \<union> H) = parts(G) \<union> parts(H)"
 by (intro equalityI parts_Un_subset1 parts_Un_subset2)
 
 lemma parts_insert: "parts (insert X H) = parts {X} \<union> parts H"
 by (metis insert_is_Un parts_Un)
 
 text\<open>TWO inserts to avoid looping.  This rewrite is better than nothing.
   Not suitable for Addsimps: its behaviour can be strange.\<close>
 lemma parts_insert2:
      "parts (insert X (insert Y H)) = parts {X} \<union> parts {Y} \<union> parts H"
 by (metis Un_commute Un_empty_right Un_insert_right insert_is_Un parts_Un)
 
-lemma parts_UN_subset1: "(\<Union>x\<in>A. parts(H x)) \<subseteq> parts(\<Union>x\<in>A. H x)"
-by (intro UN_least parts_mono UN_upper)
-
-lemma parts_UN_subset2: "parts(\<Union>x\<in>A. H x) \<subseteq> (\<Union>x\<in>A. parts(H x))"
-apply (rule subsetI)
-apply (erule parts.induct, blast+)
-done
-
-lemma parts_UN [simp]: "parts(\<Union>x\<in>A. H x) = (\<Union>x\<in>A. parts(H x))"
-by (intro equalityI parts_UN_subset1 parts_UN_subset2)
-
-text\<open>Added to simplify arguments to parts, analz and synth.
-  NOTE: the UN versions are no longer used!\<close>
+text\<open>Added to simplify arguments to parts, analz and synth.\<close>
 
 
 text\<open>This allows \<open>blast\<close> to simplify occurrences of
   @{term "parts(G\<union>H)"} in the assumption.\<close>
 lemmas in_parts_UnE = parts_Un [THEN equalityD1, THEN subsetD, THEN UnE]
 declare in_parts_UnE [elim!]
 
 
 lemma parts_insert_subset: "insert X (parts H) \<subseteq> parts(insert X H)"
 by (blast intro: parts_mono [THEN [2] rev_subsetD])
 
 subsubsection\<open>Idempotence and transitivity\<close>
 
 lemma parts_partsD [dest!]: "X \<in> parts (parts H) \<Longrightarrow> X\<in> parts H"
 by (erule parts.induct, blast+)
 
 lemma parts_idem [simp]: "parts (parts H) = parts H"
 by blast
 
 lemma parts_subset_iff [simp]: "(parts G \<subseteq> parts H) = (G \<subseteq> parts H)"
 by (metis parts_idem parts_increasing parts_mono subset_trans)
 
 lemma parts_trans: "[| X \<in> parts G;  G \<subseteq> parts H |] ==> X\<in> parts H"
 by (drule parts_mono, blast)
 
 text\<open>Cut\<close>
 lemma parts_cut:
      "[| Y\<in> parts (insert X G);  X \<in> parts H |] ==> Y\<in> parts (G \<union> H)"
 by (blast intro: parts_trans)
 
 
 lemma parts_cut_eq [simp]: "X \<in> parts H \<Longrightarrow> parts (insert X H) = parts H"
 by (force dest!: parts_cut intro: parts_insertI)
 
 
 subsubsection\<open>Rewrite rules for pulling out atomic messages\<close>
 
 lemmas parts_insert_eq_I = equalityI [OF subsetI parts_insert_subset]
 
 
 lemma parts_insert_Agent [simp]:
      "parts (insert (Agent agt) H) = insert (Agent agt) (parts H)"
 apply (rule parts_insert_eq_I)
 apply (erule parts.induct, auto)
 done
 
 lemma parts_insert_Nonce [simp]:
      "parts (insert (Nonce N) H) = insert (Nonce N) (parts H)"
 apply (rule parts_insert_eq_I)
 apply (erule parts.induct, auto)
 done
 
 lemma parts_insert_Number [simp]:
      "parts (insert (Number N) H) = insert (Number N) (parts H)"
 apply (rule parts_insert_eq_I)
 apply (erule parts.induct, auto)
 done
 
 lemma parts_insert_Key [simp]:
      "parts (insert (Key K) H) = insert (Key K) (parts H)"
 apply (rule parts_insert_eq_I)
 apply (erule parts.induct, auto)
 done
 
 lemma parts_insert_Hash [simp]:
      "parts (insert (Hash X) H) = insert (Hash X) (parts H)"
 apply (rule parts_insert_eq_I)
 apply (erule parts.induct, auto)
 done
 
 lemma parts_insert_Crypt [simp]:
      "parts (insert (Crypt K X) H) = insert (Crypt K X) (parts (insert X H))"
 apply (rule equalityI)
 apply (rule subsetI)
 apply (erule parts.induct, auto)
 apply (blast intro: parts.Body)
 done
 
 lemma parts_insert_MPair [simp]:
      "parts (insert \<lbrace>X,Y\<rbrace> H) =
           insert \<lbrace>X,Y\<rbrace> (parts (insert X (insert Y H)))"
 apply (rule equalityI)
 apply (rule subsetI)
 apply (erule parts.induct, auto)
 apply (blast intro: parts.Fst parts.Snd)+
 done
 
 lemma parts_image_Key [simp]: "parts (Key`N) = Key`N"
 apply auto
 apply (erule parts.induct, auto)
 done
 
 
 text\<open>In any message, there is an upper bound N on its greatest nonce.\<close>
 lemma msg_Nonce_supply: "\<exists>N. \<forall>n. N\<le>n \<longrightarrow> Nonce n \<notin> parts {msg}"
 apply (induct msg)
 apply (simp_all (no_asm_simp) add: exI parts_insert2)
 txt\<open>Nonce case\<close>
 apply (metis Suc_n_not_le_n)
 txt\<open>MPair case: metis works out the necessary sum itself!\<close>
 apply (metis le_trans nat_le_linear)
 done
 
 
 subsection\<open>Inductive relation "analz"\<close>
 
 text\<open>Inductive definition of "analz" -- what can be broken down from a set of
     messages, including keys.  A form of downward closure.  Pairs can
     be taken apart; messages decrypted with known keys.\<close>
 
 inductive_set
   analz :: "msg set => msg set"
   for H :: "msg set"
   where
     Inj [intro,simp] :    "X \<in> H \<Longrightarrow> X \<in> analz H"
   | Fst:     "\<lbrace>X,Y\<rbrace> \<in> analz H \<Longrightarrow> X \<in> analz H"
   | Snd:     "\<lbrace>X,Y\<rbrace> \<in> analz H \<Longrightarrow> Y \<in> analz H"
   | Decrypt [dest]:
              "[|Crypt K X \<in> analz H; Key(invKey K): analz H|] ==> X \<in> analz H"
 
 
 text\<open>Monotonicity; Lemma 1 of Lowe's paper\<close>
 lemma analz_mono: "G\<subseteq>H \<Longrightarrow> analz(G) \<subseteq> analz(H)"
 apply auto
 apply (erule analz.induct)
 apply (auto dest: analz.Fst analz.Snd)
 done
 
 text\<open>Making it safe speeds up proofs\<close>
 lemma MPair_analz [elim!]:
      "[| \<lbrace>X,Y\<rbrace> \<in> analz H;
              [| X \<in> analz H; Y \<in> analz H |] ==> P
           |] ==> P"
 by (blast dest: analz.Fst analz.Snd)
 
 lemma analz_increasing: "H \<subseteq> analz(H)"
 by blast
 
 lemma analz_subset_parts: "analz H \<subseteq> parts H"
 apply (rule subsetI)
 apply (erule analz.induct, blast+)
 done
 
 lemmas analz_into_parts = analz_subset_parts [THEN subsetD]
 
 lemmas not_parts_not_analz = analz_subset_parts [THEN contra_subsetD]
 
 
 lemma parts_analz [simp]: "parts (analz H) = parts H"
 by (metis analz_increasing analz_subset_parts equalityI parts_mono parts_subset_iff)
 
 lemma analz_parts [simp]: "analz (parts H) = parts H"
 apply auto
 apply (erule analz.induct, auto)
 done
 
 lemmas analz_insertI = subset_insertI [THEN analz_mono, THEN [2] rev_subsetD]
 
 subsubsection\<open>General equational properties\<close>
 
 lemma analz_empty [simp]: "analz{} = {}"
 apply safe
 apply (erule analz.induct, blast+)
 done
 
 text\<open>Converse fails: we can analz more from the union than from the
   separate parts, as a key in one might decrypt a message in the other\<close>
 lemma analz_Un: "analz(G) \<union> analz(H) \<subseteq> analz(G \<union> H)"
 by (intro Un_least analz_mono Un_upper1 Un_upper2)
 
 lemma analz_insert: "insert X (analz H) \<subseteq> analz(insert X H)"
 by (blast intro: analz_mono [THEN [2] rev_subsetD])
 
 subsubsection\<open>Rewrite rules for pulling out atomic messages\<close>
 
 lemmas analz_insert_eq_I = equalityI [OF subsetI analz_insert]
 
 lemma analz_insert_Agent [simp]:
      "analz (insert (Agent agt) H) = insert (Agent agt) (analz H)"
 apply (rule analz_insert_eq_I)
 apply (erule analz.induct, auto)
 done
 
 lemma analz_insert_Nonce [simp]:
      "analz (insert (Nonce N) H) = insert (Nonce N) (analz H)"
 apply (rule analz_insert_eq_I)
 apply (erule analz.induct, auto)
 done
 
 lemma analz_insert_Number [simp]:
      "analz (insert (Number N) H) = insert (Number N) (analz H)"
 apply (rule analz_insert_eq_I)
 apply (erule analz.induct, auto)
 done
 
 lemma analz_insert_Hash [simp]:
      "analz (insert (Hash X) H) = insert (Hash X) (analz H)"
 apply (rule analz_insert_eq_I)
 apply (erule analz.induct, auto)
 done
 
 text\<open>Can only pull out Keys if they are not needed to decrypt the rest\<close>
 lemma analz_insert_Key [simp]:
     "K \<notin> keysFor (analz H) \<Longrightarrow>
           analz (insert (Key K) H) = insert (Key K) (analz H)"
 apply (unfold keysFor_def)
 apply (rule analz_insert_eq_I)
 apply (erule analz.induct, auto)
 done
 
 lemma analz_insert_MPair [simp]:
      "analz (insert \<lbrace>X,Y\<rbrace> H) =
           insert \<lbrace>X,Y\<rbrace> (analz (insert X (insert Y H)))"
 apply (rule equalityI)
 apply (rule subsetI)
 apply (erule analz.induct, auto)
 apply (erule analz.induct)
 apply (blast intro: analz.Fst analz.Snd)+
 done
 
 text\<open>Can pull out enCrypted message if the Key is not known\<close>
 lemma analz_insert_Crypt:
      "Key (invKey K) \<notin> analz H
       \<Longrightarrow> analz (insert (Crypt K X) H) = insert (Crypt K X) (analz H)"
 apply (rule analz_insert_eq_I)
 apply (erule analz.induct, auto)
 
 done
 
 lemma lemma1: "Key (invKey K) \<in> analz H \<Longrightarrow>
                analz (insert (Crypt K X) H) \<subseteq>
                insert (Crypt K X) (analz (insert X H))"
 apply (rule subsetI)
 apply (erule_tac x = x in analz.induct, auto)
 done
 
 lemma lemma2: "Key (invKey K) \<in> analz H \<Longrightarrow>
                insert (Crypt K X) (analz (insert X H)) \<subseteq>
                analz (insert (Crypt K X) H)"
 apply auto
 apply (erule_tac x = x in analz.induct, auto)
 apply (blast intro: analz_insertI analz.Decrypt)
 done
 
 lemma analz_insert_Decrypt:
      "Key (invKey K) \<in> analz H \<Longrightarrow>
                analz (insert (Crypt K X) H) =
                insert (Crypt K X) (analz (insert X H))"
 by (intro equalityI lemma1 lemma2)
 
 text\<open>Case analysis: either the message is secure, or it is not! Effective,
 but can cause subgoals to blow up! Use with \<open>if_split\<close>; apparently
 \<open>split_tac\<close> does not cope with patterns such as @{term"analz (insert
 (Crypt K X) H)"}\<close>
 lemma analz_Crypt_if [simp]:
      "analz (insert (Crypt K X) H) =
           (if (Key (invKey K) \<in> analz H)
            then insert (Crypt K X) (analz (insert X H))
            else insert (Crypt K X) (analz H))"
 by (simp add: analz_insert_Crypt analz_insert_Decrypt)
 
 
 text\<open>This rule supposes "for the sake of argument" that we have the key.\<close>
 lemma analz_insert_Crypt_subset:
      "analz (insert (Crypt K X) H) \<subseteq>
            insert (Crypt K X) (analz (insert X H))"
 apply (rule subsetI)
 apply (erule analz.induct, auto)
 done
 
 
 lemma analz_image_Key [simp]: "analz (Key`N) = Key`N"
 apply auto
 apply (erule analz.induct, auto)
 done
 
 
 subsubsection\<open>Idempotence and transitivity\<close>
 
 lemma analz_analzD [dest!]: "X\<in> analz (analz H) \<Longrightarrow> X \<in> analz H"
 by (erule analz.induct, blast+)
 
 lemma analz_idem [simp]: "analz (analz H) = analz H"
 by blast
 
 lemma analz_subset_iff [simp]: "(analz G \<subseteq> analz H) = (G \<subseteq> analz H)"
 by (metis analz_idem analz_increasing analz_mono subset_trans)
 
 lemma analz_trans: "[| X\<in> analz G;  G \<subseteq> analz H |] ==> X\<in> analz H"
 by (drule analz_mono, blast)
 
 text\<open>Cut; Lemma 2 of Lowe\<close>
 lemma analz_cut: "[| Y\<in> analz (insert X H);  X\<in> analz H |] ==> Y\<in> analz H"
 by (erule analz_trans, blast)
 
 (*Cut can be proved easily by induction on
    "Y: analz (insert X H) \<Longrightarrow> X: analz H \<longrightarrow> Y: analz H"
 *)
 
 text\<open>This rewrite rule helps in the simplification of messages that involve
   the forwarding of unknown components (X).  Without it, removing occurrences
   of X can be very complicated.\<close>
 lemma analz_insert_eq: "X \<in> analz H \<Longrightarrow> analz (insert X H) = analz H"
 by (blast intro: analz_cut analz_insertI)
 
 
 text\<open>A congruence rule for "analz"\<close>
 
 lemma analz_subset_cong:
      "[| analz G \<subseteq> analz G'; analz H \<subseteq> analz H' |]
       ==> analz (G \<union> H) \<subseteq> analz (G' \<union> H')"
 apply simp
 apply (iprover intro: conjI subset_trans analz_mono Un_upper1 Un_upper2)
 done
 
 lemma analz_cong:
      "[| analz G = analz G'; analz H = analz H' |]
       ==> analz (G \<union> H) = analz (G' \<union> H')"
 by (intro equalityI analz_subset_cong, simp_all)
 
 lemma analz_insert_cong:
      "analz H = analz H' \<Longrightarrow> analz(insert X H) = analz(insert X H')"
 by (force simp only: insert_def intro!: analz_cong)
 
 text\<open>If there are no pairs or encryptions then analz does nothing\<close>
 lemma analz_trivial:
      "[| \<forall>X Y. \<lbrace>X,Y\<rbrace> \<notin> H;  \<forall>X K. Crypt K X \<notin> H |] ==> analz H = H"
 apply safe
 apply (erule analz.induct, blast+)
 done
 
 
 subsection\<open>Inductive relation "synth"\<close>
 
 text\<open>Inductive definition of "synth" -- what can be built up from a set of
     messages.  A form of upward closure.  Pairs can be built, messages
     encrypted with known keys.  Agent names are public domain.
     Numbers can be guessed, but Nonces cannot be.\<close>
 
 inductive_set
   synth :: "msg set => msg set"
   for H :: "msg set"
   where
     Inj    [intro]:   "X \<in> H \<Longrightarrow> X \<in> synth H"
   | Agent  [intro]:   "Agent agt \<in> synth H"
   | Number [intro]:   "Number n  \<in> synth H"
   | Hash   [intro]:   "X \<in> synth H \<Longrightarrow> Hash X \<in> synth H"
   | MPair  [intro]:   "[|X \<in> synth H;  Y \<in> synth H|] ==> \<lbrace>X,Y\<rbrace> \<in> synth H"
   | Crypt  [intro]:   "[|X \<in> synth H;  Key(K) \<in> H|] ==> Crypt K X \<in> synth H"
 
 text\<open>Monotonicity\<close>
 lemma synth_mono: "G\<subseteq>H \<Longrightarrow> synth(G) \<subseteq> synth(H)"
   by (auto, erule synth.induct, auto)
 
 text\<open>NO \<open>Agent_synth\<close>, as any Agent name can be synthesized.
   The same holds for @{term Number}\<close>
 
 inductive_simps synth_simps [iff]:
  "Nonce n \<in> synth H"
  "Key K \<in> synth H"
  "Hash X \<in> synth H"
  "\<lbrace>X,Y\<rbrace> \<in> synth H"
  "Crypt K X \<in> synth H"
 
 lemma synth_increasing: "H \<subseteq> synth(H)"
 by blast
 
 subsubsection\<open>Unions\<close>
 
 text\<open>Converse fails: we can synth more from the union than from the
   separate parts, building a compound message using elements of each.\<close>
 lemma synth_Un: "synth(G) \<union> synth(H) \<subseteq> synth(G \<union> H)"
 by (intro Un_least synth_mono Un_upper1 Un_upper2)
 
 lemma synth_insert: "insert X (synth H) \<subseteq> synth(insert X H)"
 by (blast intro: synth_mono [THEN [2] rev_subsetD])
 
 subsubsection\<open>Idempotence and transitivity\<close>
 
 lemma synth_synthD [dest!]: "X \<in> synth (synth H) \<Longrightarrow> X\<in> synth H"
 by (erule synth.induct, auto)
 
 lemma synth_idem: "synth (synth H) = synth H"
 by blast
 
 lemma synth_subset_iff [simp]: "(synth G \<subseteq> synth H) = (G \<subseteq> synth H)"
 by (metis subset_trans synth_idem synth_increasing synth_mono)
 
 lemma synth_trans: "[| X\<in> synth G;  G \<subseteq> synth H |] ==> X\<in> synth H"
 by (drule synth_mono, blast)
 
 text\<open>Cut; Lemma 2 of Lowe\<close>
 lemma synth_cut: "[| Y\<in> synth (insert X H);  X\<in> synth H |] ==> Y\<in> synth H"
 by (erule synth_trans, blast)
 
 lemma Agent_synth [simp]: "Agent A \<in> synth H"
 by blast
 
 lemma Number_synth [simp]: "Number n \<in> synth H"
 by blast
 
 lemma Nonce_synth_eq [simp]: "(Nonce N \<in> synth H) = (Nonce N \<in> H)"
 by blast
 
 lemma Key_synth_eq [simp]: "(Key K \<in> synth H) = (Key K \<in> H)"
 by blast
 
 lemma Crypt_synth_eq [simp]:
      "Key K \<notin> H \<Longrightarrow> (Crypt K X \<in> synth H) = (Crypt K X \<in> H)"
 by blast
 
 
 lemma keysFor_synth [simp]:
     "keysFor (synth H) = keysFor H \<union> invKey`{K. Key K \<in> H}"
 by (unfold keysFor_def, blast)
 
 
 subsubsection\<open>Combinations of parts, analz and synth\<close>
 
 lemma parts_synth [simp]: "parts (synth H) = parts H \<union> synth H"
 apply (rule equalityI)
 apply (rule subsetI)
 apply (erule parts.induct)
 apply (blast intro: synth_increasing [THEN parts_mono, THEN subsetD]
                     parts.Fst parts.Snd parts.Body)+
 done
 
 lemma analz_analz_Un [simp]: "analz (analz G \<union> H) = analz (G \<union> H)"
 apply (intro equalityI analz_subset_cong)+
 apply simp_all
 done
 
 lemma analz_synth_Un [simp]: "analz (synth G \<union> H) = analz (G \<union> H) \<union> synth G"
 apply (rule equalityI)
 apply (rule subsetI)
 apply (erule analz.induct)
 prefer 5 apply (blast intro: analz_mono [THEN [2] rev_subsetD])
 apply (blast intro: analz.Fst analz.Snd analz.Decrypt)+
 done
 
 lemma analz_synth [simp]: "analz (synth H) = analz H \<union> synth H"
 by (metis Un_empty_right analz_synth_Un)
 
 
 subsubsection\<open>For reasoning about the Fake rule in traces\<close>
 
 lemma parts_insert_subset_Un: "X \<in> G \<Longrightarrow> parts(insert X H) \<subseteq> parts G \<union> parts H"
 by (metis UnCI Un_upper2 insert_subset parts_Un parts_mono)
 
 text\<open>More specifically for Fake. See also \<open>Fake_parts_sing\<close> below\<close>
 lemma Fake_parts_insert:
      "X \<in> synth (analz H) \<Longrightarrow>
       parts (insert X H) \<subseteq> synth (analz H) \<union> parts H"
 by (metis Un_commute analz_increasing insert_subset parts_analz parts_mono
           parts_synth synth_mono synth_subset_iff)
 
 lemma Fake_parts_insert_in_Un:
      "[|Z \<in> parts (insert X H);  X: synth (analz H)|]
       ==> Z \<in>  synth (analz H) \<union> parts H"
 by (metis Fake_parts_insert subsetD)
 
 text\<open>@{term H} is sometimes @{term"Key ` KK \<union> spies evs"}, so can't put
   @{term "G=H"}.\<close>
 lemma Fake_analz_insert:
      "X\<in> synth (analz G) \<Longrightarrow>
       analz (insert X H) \<subseteq> synth (analz G) \<union> analz (G \<union> H)"
 apply (rule subsetI)
 apply (subgoal_tac "x \<in> analz (synth (analz G) \<union> H)", force)
 apply (blast intro: analz_mono [THEN [2] rev_subsetD] analz_mono [THEN synth_mono, THEN [2] rev_subsetD])
 done
 
 lemma analz_conj_parts [simp]:
      "(X \<in> analz H \<and> X \<in> parts H) = (X \<in> analz H)"
 by (blast intro: analz_subset_parts [THEN subsetD])
 
 lemma analz_disj_parts [simp]:
      "(X \<in> analz H | X \<in> parts H) = (X \<in> parts H)"
 by (blast intro: analz_subset_parts [THEN subsetD])
 
 text\<open>Without this equation, other rules for synth and analz would yield
   redundant cases\<close>
 lemma MPair_synth_analz [iff]:
      "(\<lbrace>X,Y\<rbrace> \<in> synth (analz H)) =
       (X \<in> synth (analz H) \<and> Y \<in> synth (analz H))"
 by blast
 
 lemma Crypt_synth_analz:
      "[| Key K \<in> analz H;  Key (invKey K) \<in> analz H |]
        ==> (Crypt K X \<in> synth (analz H)) = (X \<in> synth (analz H))"
 by blast
 
 
 lemma Hash_synth_analz [simp]:
      "X \<notin> synth (analz H)
       \<Longrightarrow> (Hash\<lbrace>X,Y\<rbrace> \<in> synth (analz H)) = (Hash\<lbrace>X,Y\<rbrace> \<in> analz H)"
 by blast
 
 
 subsection\<open>HPair: a combination of Hash and MPair\<close>
 
 subsubsection\<open>Freeness\<close>
 
 lemma Agent_neq_HPair: "Agent A ~= Hash[X] Y"
 by (unfold HPair_def, simp)
 
 lemma Nonce_neq_HPair: "Nonce N ~= Hash[X] Y"
 by (unfold HPair_def, simp)
 
 lemma Number_neq_HPair: "Number N ~= Hash[X] Y"
 by (unfold HPair_def, simp)
 
 lemma Key_neq_HPair: "Key K ~= Hash[X] Y"
 by (unfold HPair_def, simp)
 
 lemma Hash_neq_HPair: "Hash Z ~= Hash[X] Y"
 by (unfold HPair_def, simp)
 
 lemma Crypt_neq_HPair: "Crypt K X' ~= Hash[X] Y"
 by (unfold HPair_def, simp)
 
 lemmas HPair_neqs = Agent_neq_HPair Nonce_neq_HPair Number_neq_HPair
                     Key_neq_HPair Hash_neq_HPair Crypt_neq_HPair
 
 declare HPair_neqs [iff]
 declare HPair_neqs [symmetric, iff]
 
 lemma HPair_eq [iff]: "(Hash[X'] Y' = Hash[X] Y) = (X' = X \<and> Y'=Y)"
 by (simp add: HPair_def)
 
 lemma MPair_eq_HPair [iff]:
      "(\<lbrace>X',Y'\<rbrace> = Hash[X] Y) = (X' = Hash\<lbrace>X,Y\<rbrace> \<and> Y'=Y)"
 by (simp add: HPair_def)
 
 lemma HPair_eq_MPair [iff]:
      "(Hash[X] Y = \<lbrace>X',Y'\<rbrace>) = (X' = Hash\<lbrace>X,Y\<rbrace> \<and> Y'=Y)"
 by (auto simp add: HPair_def)
 
 
 subsubsection\<open>Specialized laws, proved in terms of those for Hash and MPair\<close>
 
 lemma keysFor_insert_HPair [simp]: "keysFor (insert (Hash[X] Y) H) = keysFor H"
 by (simp add: HPair_def)
 
 lemma parts_insert_HPair [simp]:
     "parts (insert (Hash[X] Y) H) =
      insert (Hash[X] Y) (insert (Hash\<lbrace>X,Y\<rbrace>) (parts (insert Y H)))"
 by (simp add: HPair_def)
 
 lemma analz_insert_HPair [simp]:
     "analz (insert (Hash[X] Y) H) =
      insert (Hash[X] Y) (insert (Hash\<lbrace>X,Y\<rbrace>) (analz (insert Y H)))"
 by (simp add: HPair_def)
 
 lemma HPair_synth_analz [simp]:
      "X \<notin> synth (analz H)
     \<Longrightarrow> (Hash[X] Y \<in> synth (analz H)) =
         (Hash \<lbrace>X, Y\<rbrace> \<in> analz H \<and> Y \<in> synth (analz H))"
 by (auto simp add: HPair_def)
 
 
 text\<open>We do NOT want Crypt... messages broken up in protocols!!\<close>
 declare parts.Body [rule del]
 
 
 text\<open>Rewrites to push in Key and Crypt messages, so that other messages can
     be pulled out using the \<open>analz_insert\<close> rules\<close>
 
 lemmas pushKeys =
   insert_commute [of "Key K" "Agent C"]
   insert_commute [of "Key K" "Nonce N"]
   insert_commute [of "Key K" "Number N"]
   insert_commute [of "Key K" "Hash X"]
   insert_commute [of "Key K" "MPair X Y"]
   insert_commute [of "Key K" "Crypt X K'"]
   for K C N X Y K'
 
 lemmas pushCrypts =
   insert_commute [of "Crypt X K" "Agent C"]
   insert_commute [of "Crypt X K" "Agent C"]
   insert_commute [of "Crypt X K" "Nonce N"]
   insert_commute [of "Crypt X K" "Number N"]
   insert_commute [of "Crypt X K" "Hash X'"]
   insert_commute [of "Crypt X K" "MPair X' Y"]
   for X K C N X' Y
 
 text\<open>Cannot be added with \<open>[simp]\<close> -- messages should not always be
   re-ordered.\<close>
 lemmas pushes = pushKeys pushCrypts
 
 
 subsection\<open>The set of key-free messages\<close>
 
 (*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|] ==> \<lbrace>X,Y\<rbrace> \<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: "\<lbrace>X,Y\<rbrace> \<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 parts_Un parts_keyfree UnI2)
 done
 
 subsection\<open>Tactics useful for many protocol proofs\<close>
 ML
 \<open>
 (*Analysis of Fake cases.  Also works for messages that forward unknown parts,
   but this application is no longer necessary if analz_insert_eq is used.
   DEPENDS UPON "X" REFERRING TO THE FRADULENT MESSAGE *)
 
 fun impOfSubs th = th RSN (2, @{thm rev_subsetD})
 
 (*Apply rules to break down assumptions of the form
   Y \<in> parts(insert X H)  and  Y \<in> analz(insert X H)
 *)
 fun Fake_insert_tac ctxt =
     dresolve_tac ctxt [impOfSubs @{thm Fake_analz_insert},
                   impOfSubs @{thm Fake_parts_insert}] THEN'
     eresolve_tac ctxt [asm_rl, @{thm synth.Inj}];
 
 fun Fake_insert_simp_tac ctxt i =
   REPEAT (Fake_insert_tac ctxt i) THEN asm_full_simp_tac ctxt i;
 
 fun atomic_spy_analz_tac ctxt =
   SELECT_GOAL
    (Fake_insert_simp_tac ctxt 1 THEN
     IF_UNSOLVED
       (Blast.depth_tac
         (ctxt addIs [@{thm analz_insertI}, impOfSubs @{thm analz_subset_parts}]) 4 1));
 
 fun spy_analz_tac ctxt i =
   DETERM
    (SELECT_GOAL
      (EVERY
       [  (*push in occurrences of X...*)
        (REPEAT o CHANGED)
          (Rule_Insts.res_inst_tac ctxt [((("x", 1), Position.none), "X")] []
           (insert_commute RS ssubst) 1),
        (*...allowing further simplifications*)
        simp_tac ctxt 1,
        REPEAT (FIRSTGOAL (resolve_tac ctxt [allI,impI,notI,conjI,iffI])),
        DEPTH_SOLVE (atomic_spy_analz_tac ctxt 1)]) i);
 \<close>
 
 text\<open>By default only \<open>o_apply\<close> is built-in.  But in the presence of
 eta-expansion this means that some terms displayed as @{term "f o g"} will be
 rewritten, and others will not!\<close>
 declare o_def [simp]
 
 
 lemma Crypt_notin_image_Key [simp]: "Crypt K X \<notin> Key ` A"
 by auto
 
 lemma Hash_notin_image_Key [simp] :"Hash X \<notin> Key ` A"
 by auto
 
 lemma synth_analz_mono: "G\<subseteq>H \<Longrightarrow> synth (analz(G)) \<subseteq> synth (analz(H))"
 by (iprover intro: synth_mono analz_mono)
 
 lemma Fake_analz_eq [simp]:
      "X \<in> synth(analz H) \<Longrightarrow> synth (analz (insert X H)) = synth (analz H)"
 by (metis Fake_analz_insert Un_absorb Un_absorb1 Un_commute
           subset_insertI synth_analz_mono synth_increasing synth_subset_iff)
 
 text\<open>Two generalizations of \<open>analz_insert_eq\<close>\<close>
 lemma gen_analz_insert_eq [rule_format]:
      "X \<in> analz H \<Longrightarrow> \<forall>G. H \<subseteq> G \<longrightarrow> analz (insert X G) = analz G"
 by (blast intro: analz_cut analz_insertI analz_mono [THEN [2] rev_subsetD])
 
 lemma synth_analz_insert_eq [rule_format]:
      "X \<in> synth (analz H)
       \<Longrightarrow> \<forall> G. H \<subseteq> G \<longrightarrow> (Key K \<in> analz (insert X G)) = (Key K \<in> analz G)"
 apply (erule synth.induct)
 apply (simp_all add: gen_analz_insert_eq subset_trans [OF _ subset_insertI])
 done
 
 lemma Fake_parts_sing:
      "X \<in> synth (analz H) \<Longrightarrow> parts{X} \<subseteq> synth (analz H) \<union> parts H"
 by (metis Fake_parts_insert empty_subsetI insert_mono parts_mono subset_trans)
 
 lemmas Fake_parts_sing_imp_Un = Fake_parts_sing [THEN [2] rev_subsetD]
 
 method_setup spy_analz = \<open>
     Scan.succeed (SIMPLE_METHOD' o spy_analz_tac)\<close>
     "for proving the Fake case when analz is involved"
 
 method_setup atomic_spy_analz = \<open>
     Scan.succeed (SIMPLE_METHOD' o atomic_spy_analz_tac)\<close>
     "for debugging spy_analz"
 
 method_setup Fake_insert_simp = \<open>
     Scan.succeed (SIMPLE_METHOD' o Fake_insert_simp_tac)\<close>
     "for debugging spy_analz"
 
 end
diff --git a/thys/Inductive_Confidentiality/GeneralAttacker/PublicGA.thy b/thys/Inductive_Confidentiality/GeneralAttacker/PublicGA.thy
--- a/thys/Inductive_Confidentiality/GeneralAttacker/PublicGA.thy
+++ b/thys/Inductive_Confidentiality/GeneralAttacker/PublicGA.thy
@@ -1,412 +1,410 @@
 section\<open>Theory of Cryptographic Keys for Security Protocols against the General Attacker\<close>
 
 theory PublicGA imports EventGA begin
 
 lemma invKey_K: "K \<in> symKeys \<Longrightarrow> invKey K = K"
 by (simp add: symKeys_def)
 
 subsection\<open>Asymmetric Keys\<close>
 
 datatype keymode = Signature | Encryption
 
 consts
   publicKey :: "[keymode,agent] => key"
 
 abbreviation
   pubEK :: "agent => key" where
   "pubEK == publicKey Encryption"
 
 abbreviation
   pubSK :: "agent => key" where
   "pubSK == publicKey Signature"
 
 abbreviation
   privateKey :: "[keymode, agent] => key" where
   "privateKey b A == invKey (publicKey b A)"
 
 abbreviation
   (*BEWARE!! priEK, priSK DON'T WORK with inj, range, image, etc.*)
   priEK :: "agent => key" where
   "priEK A == privateKey Encryption A"
 
 abbreviation
   priSK :: "agent => key" where
   "priSK A == privateKey Signature A"
 
 
 text\<open>These abbreviations give backward compatibility.  They represent the
 simple situation where the signature and encryption keys are the same.\<close>
 
 abbreviation
   pubK :: "agent => key" where
   "pubK A == pubEK A"
 
 abbreviation
   priK :: "agent => key" where
   "priK A == invKey (pubEK A)"
 
 
 text\<open>By freeness of agents, no two agents have the same key.  Since
   @{term "True\<noteq>False"}, no agent has identical signing and encryption keys\<close>
 specification (publicKey)
   injective_publicKey:
     "publicKey b A = publicKey c A' \<Longrightarrow> b=c \<and> A=A'"
    apply (rule exI [of _ 
        "%b A. 2 * case_agent (\<lambda>n. n + 2) A + case_keymode 0 1 b"])
    apply (auto simp add: inj_on_def split: agent.split keymode.split)
    apply presburger
    apply presburger
    done                       
 
 
 axiomatization where
   (*No private key equals any public key (essential to ensure that private
     keys are private!) *)
   privateKey_neq_publicKey [iff]: "privateKey b A \<noteq> publicKey c A'"
 
 lemmas publicKey_neq_privateKey = privateKey_neq_publicKey [THEN not_sym]
 declare publicKey_neq_privateKey [iff]
 
 
 subsection\<open>Basic properties of @{term pubK} and @{term priK}\<close>
 
 lemma publicKey_inject [iff]: "(publicKey b A = publicKey c A') = (b=c \<and> A=A')"
 by (blast dest!: injective_publicKey) 
 
 lemma not_symKeys_pubK [iff]: "publicKey b A \<notin> symKeys"
 by (simp add: symKeys_def)
 
 lemma not_symKeys_priK [iff]: "privateKey b A \<notin> symKeys"
 by (simp add: symKeys_def)
 
 lemma symKey_neq_priEK: "K \<in> symKeys \<Longrightarrow> K \<noteq> priEK A"
 by auto
 
 lemma symKeys_neq_imp_neq: "(K \<in> symKeys) \<noteq> (K' \<in> symKeys) \<Longrightarrow> K \<noteq> K'"
 by blast
 
 lemma symKeys_invKey_iff [iff]: "(invKey K \<in> symKeys) = (K \<in> symKeys)"
 by (unfold symKeys_def, auto)
 
 lemma analz_symKeys_Decrypt:
      "[| Crypt K X \<in> analz H;  K \<in> symKeys;  Key K \<in> analz H |]  
       ==> X \<in> analz H"
 by (auto simp add: symKeys_def)
 
 
 
 subsection\<open>"Image" equations that hold for injective functions\<close>
 
 lemma invKey_image_eq [simp]: "(invKey x \<in> invKey`A) = (x \<in> A)"
 by auto
 
 (*holds because invKey is injective*)
 lemma publicKey_image_eq [simp]:
      "(publicKey b x \<in> publicKey c ` AA) = (b=c \<and> x \<in> AA)"
 by auto
 
 lemma privateKey_notin_image_publicKey [simp]: "privateKey b x \<notin> publicKey c ` AA"
 by auto
 
 lemma privateKey_image_eq [simp]:
      "(privateKey b A \<in> invKey ` publicKey c ` AS) = (b=c \<and> A\<in>AS)"
 by auto
 
 lemma publicKey_notin_image_privateKey [simp]: "publicKey b A \<notin> invKey ` publicKey c ` AS"
 by auto
 
 
 subsection\<open>Symmetric Keys\<close>
 
 text\<open>For some protocols, it is convenient to equip agents with symmetric as
 well as asymmetric keys.  The theory \<open>Shared\<close> assumes that all keys
 are symmetric.\<close>
 
 consts
   shrK    :: "agent => key"    \<comment> \<open>long-term shared keys\<close>
 
 specification (shrK)
   inj_shrK: "inj shrK"
   \<comment> \<open>No two agents have the same long-term key\<close>
    apply (rule exI [of _ "case_agent (\<lambda>n. n + 2)"]) 
    apply (simp add: inj_on_def split: agent.split) 
    done
 
 axiomatization where
   sym_shrK [iff]: "shrK X \<in> symKeys" \<comment> \<open>All shared keys are symmetric\<close>
 
 text\<open>Injectiveness: Agents' long-term keys are distinct.\<close>
 lemmas shrK_injective = inj_shrK [THEN inj_eq]
 declare shrK_injective [iff]
 
 lemma invKey_shrK [simp]: "invKey (shrK A) = shrK A"
 by (simp add: invKey_K) 
 
 lemma analz_shrK_Decrypt:
      "[| Crypt (shrK A) X \<in> analz H; Key(shrK A) \<in> analz H |] ==> X \<in> analz H"
 by auto
 
 lemma analz_Decrypt':
      "[| Crypt K X \<in> analz H; K \<in> symKeys; Key K \<in> analz H |] ==> X \<in> analz H"
 by (auto simp add: invKey_K)
 
 lemma priK_neq_shrK [iff]: "shrK A \<noteq> privateKey b C"
 by (simp add: symKeys_neq_imp_neq)
 
 lemmas shrK_neq_priK = priK_neq_shrK [THEN not_sym]
 declare shrK_neq_priK [simp]
 
 lemma pubK_neq_shrK [iff]: "shrK A \<noteq> publicKey b C"
 by (simp add: symKeys_neq_imp_neq)
 
 lemmas shrK_neq_pubK = pubK_neq_shrK [THEN not_sym]
 declare shrK_neq_pubK [simp]
 
 lemma priEK_noteq_shrK [simp]: "priEK A \<noteq> shrK B" 
 by auto
 
 lemma publicKey_notin_image_shrK [simp]: "publicKey b x \<notin> shrK ` AA"
 by auto
 
 lemma privateKey_notin_image_shrK [simp]: "privateKey b x \<notin> shrK ` AA"
 by auto
 
 lemma shrK_notin_image_publicKey [simp]: "shrK x \<notin> publicKey b ` AA"
 by auto
 
 lemma shrK_notin_image_privateKey [simp]: "shrK x \<notin> invKey ` publicKey b ` AA" 
 by auto
 
 lemma shrK_image_eq [simp]: "(shrK x \<in> shrK ` AA) = (x \<in> AA)"
 by auto
 
 text\<open>For some reason, moving this up can make some proofs loop!\<close>
 declare invKey_K [simp]
 
 
 subsection\<open>Initial States of Agents\<close>
 
 overloading
   initState \<equiv> initState
 begin
 
 primrec initState where
 
   initState_Friend:
     "initState (Friend i) =    
        {Key (priEK (Friend i)), Key (priSK (Friend i)), Key (shrK (Friend i))} \<union> 
        (Key ` range pubEK) \<union> (Key ` range pubSK)"
 end
 
 
 lemma used_parts_subset_parts [rule_format]:
      "\<forall>X \<in> used evs. parts {X} \<subseteq> used evs"
 apply (induct evs) 
  prefer 2
- apply (simp add: used_Cons)
- apply (rule ballI)  
- apply (case_tac a, auto)  
-apply (auto dest!: parts_cut) 
+ apply (simp add: used_Cons split: event.split)
+ apply (metis Un_iff empty_subsetI insert_subset le_supI1 le_supI2 parts_subset_iff)
 txt\<open>Base case\<close>
-apply (simp add: used_Nil) 
+apply (auto dest!: parts_cut simp add: used_Nil) 
 done
 
 lemma MPair_used_D: "\<lbrace>X,Y\<rbrace> \<in> used H \<Longrightarrow> X \<in> used H \<and> Y \<in> used H"
 by (drule used_parts_subset_parts, simp, blast)
 
 text\<open>There was a similar theorem in Event.thy, so perhaps this one can
   be moved up if proved directly by induction.\<close>
 lemma MPair_used [elim!]:
      "[| \<lbrace>X,Y\<rbrace> \<in> used H;
          [| X \<in> used H; Y \<in> used H |] ==> P |] 
       ==> P"
 by (blast dest: MPair_used_D) 
 
 
 text\<open>Rewrites should not refer to  @{term "initState(Friend i)"} because
   that expression is not in normal form.\<close>
 
 lemma keysFor_parts_initState [simp]: "keysFor (parts (initState C)) = {}"
 apply (unfold keysFor_def)
 apply (induct_tac "C")
 apply (auto intro: range_eqI)
 done
 
 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 ***)
 
 (*Agents see their own shared keys!*)
 lemma shrK_in_initState [iff]: "Key (shrK A) \<in> initState A"
 by (induct_tac "A", auto)
 
 lemma shrK_in_knows [iff]: "Key (shrK A) \<in> knows A evs"
 by (simp add: initState_subset_knows [THEN subsetD])
 
 lemma shrK_in_used [iff]: "Key (shrK A) \<in> used evs"
 by (rule initState_into_used, blast)
 
 
 (** Fresh keys never clash with long-term shared keys **)
 
 (*Used in parts_induct_tac and analz_Fake_tac to distinguish session keys
   from long-term shared keys*)
 lemma Key_not_used [simp]: "Key K \<notin> used evs \<Longrightarrow> K \<notin> range shrK"
 by blast
 
 lemma shrK_neq: "Key K \<notin> used evs \<Longrightarrow> shrK B \<noteq> K"
 by blast
 
 lemmas neq_shrK = shrK_neq [THEN not_sym]
 declare neq_shrK [simp]
 
 
 subsection\<open>Function @{term "knows Spy"}\<close>
 
 lemma not_SignatureE [elim!]: "b \<noteq> Signature \<Longrightarrow> b = Encryption"
   by (cases b, auto) 
 
 text\<open>Agents see their own private keys!\<close>
 lemma priK_in_initState [iff]: "Key (privateKey b A) \<in> initState A"
   by (cases A, auto)
 
 text\<open>Agents see all public keys!\<close>
 lemma publicKey_in_initState [iff]: "Key (publicKey b A) \<in> initState B"
   by (cases B, auto) 
 
 text\<open>All public keys are visible\<close>
 lemma spies_pubK [iff]: "Key (publicKey b A) \<in> knows B evs"
 apply (induct_tac "evs")
 apply (auto simp add: imageI knows_Cons split: event.split)
 done
 
 
 lemmas analz_spies_pubK = spies_pubK [THEN analz.Inj]
 declare analz_spies_pubK [iff]
 
 (*Note: there never is at this stage a lemma about what an agent cannot know*)
 
 lemma publicKey_into_used [iff] :"Key (publicKey b A) \<in> used evs"
 apply (rule initState_into_used)
 apply (rule publicKey_in_initState [THEN parts.Inj])
 done
 
 lemma privateKey_into_used [iff]: "Key (privateKey b A) \<in> used evs"
 apply(rule initState_into_used)
 apply(rule priK_in_initState [THEN parts.Inj])
 done
 
 lemma Crypt_analz_bad:
      "[| Crypt (shrK A) X \<in> analz (knows A evs) |]  
       ==> X \<in> analz (knows A evs)"
 by force
 
 
 subsection\<open>Fresh Nonces\<close>
 
 lemma Nonce_notin_initState [iff]: "Nonce N \<notin> parts (initState B)"
 by (induct_tac "B", auto)
 
 lemma Nonce_notin_used_empty [simp]: "Nonce N \<notin> used []"
 by (simp add: used_Nil)
 
 
 subsection\<open>Supply fresh nonces for possibility theorems\<close>
 
 text\<open>In any trace, there is an upper bound N on the greatest nonce in use\<close>
 lemma Nonce_supply_lemma: "\<exists>N. \<forall>n. N\<le>n \<longrightarrow> Nonce n \<notin> used evs"
 apply (induct_tac "evs")
 apply (rule_tac x = 0 in exI)
 apply (simp_all (no_asm_simp) add: used_Cons split: event.split)
 apply safe
 apply (rule msg_Nonce_supply [THEN exE], blast elim!: add_leE)+
 done
 
 lemma Nonce_supply1: "\<exists>N. Nonce N \<notin> used evs"
 by (rule Nonce_supply_lemma [THEN exE], blast)
 
 lemma Nonce_supply: "Nonce (SOME N. Nonce N \<notin> used evs) \<notin> used evs"
 apply (rule Nonce_supply_lemma [THEN exE])
 apply (rule someI, fast)
 done
 
 subsection\<open>Specialized Rewriting for Theorems About @{term analz} and Image\<close>
 
 lemma insert_Key_singleton: "insert (Key K) H = Key ` {K} \<union> H"
 by blast
 
 lemma insert_Key_image: "insert (Key K) (Key`KK \<union> C) = Key ` (insert K KK) \<union> C"
 by blast
 
 
 lemma Crypt_imp_keysFor :"[|Crypt K X \<in> H; K \<in> symKeys|] ==> K \<in> keysFor H"
 by (drule Crypt_imp_invKey_keysFor, simp)
 
 text\<open>Lemma for the trivial direction of the if-and-only-if of the 
 Session Key Compromise Theorem\<close>
 lemma analz_image_freshK_lemma:
      "(Key K \<in> analz (Key`nE \<union> H)) \<longrightarrow> (K \<in> nE | Key K \<in> analz H)  \<Longrightarrow>  
          (Key K \<in> analz (Key`nE \<union> H)) = (K \<in> nE | Key K \<in> analz H)"
 by (blast intro: analz_mono [THEN [2] rev_subsetD])
 
 lemmas analz_image_freshK_simps =
        simp_thms mem_simps \<comment> \<open>these two allow its use with @{text "only:"}\<close>
        disj_comms 
        image_insert [THEN sym] image_Un [THEN sym] empty_subsetI insert_subset
        analz_insert_eq Un_upper2 [THEN analz_mono, THEN subsetD]
        insert_Key_singleton 
        Key_not_used insert_Key_image Un_assoc [THEN sym]
 
 ML \<open>
 structure Public =
 struct
 
 val analz_image_freshK_ss =
   simpset_of (@{context}
     delsimps [image_insert, image_Un]
     delsimps [@{thm imp_disjL}]    (*reduces blow-up*)
     addsimps @{thms analz_image_freshK_simps})
 
 (*Tactic for possibility theorems*)
 fun possibility_tac ctxt =
     REPEAT (*omit used_Says so that Nonces start from different traces!*)
     (ALLGOALS (simp_tac (ctxt delsimps [@{thm used_Says}]))
      THEN
      REPEAT_FIRST (eq_assume_tac ORELSE' 
                    resolve_tac ctxt [refl, conjI, @{thm Nonce_supply}]))
 
 (*For harder protocols (such as Recur) where we have to set up some
   nonces and keys initially*)
 fun basic_possibility_tac ctxt =
     REPEAT 
     (ALLGOALS (asm_simp_tac (ctxt setSolver safe_solver))
      THEN
      REPEAT_FIRST (resolve_tac ctxt [refl, conjI]))
 
 end
 \<close>
 
 method_setup analz_freshK = \<open>
     Scan.succeed (fn ctxt =>
      (SIMPLE_METHOD
       (EVERY [REPEAT_FIRST (resolve_tac ctxt [allI, ballI, impI]),
           REPEAT_FIRST (resolve_tac ctxt @{thms analz_image_freshK_lemma}),
           ALLGOALS (asm_simp_tac (put_simpset Public.analz_image_freshK_ss ctxt))])))\<close>
     "for proving the Session Key Compromise theorem"
 
 
 subsection\<open>Specialized Methods for Possibility Theorems\<close>
 
 method_setup possibility = \<open>
     Scan.succeed (SIMPLE_METHOD o Public.possibility_tac)\<close>
     "for proving possibility theorems"
 
 method_setup basic_possibility = \<open>
     Scan.succeed (SIMPLE_METHOD o Public.basic_possibility_tac)\<close>
     "for proving possibility theorems"
 
 end
diff --git a/thys/IsaNet/infrastructure/Message.thy b/thys/IsaNet/infrastructure/Message.thy
--- a/thys/IsaNet/infrastructure/Message.thy
+++ b/thys/IsaNet/infrastructure/Message.thy
@@ -1,1203 +1,1191 @@
 (*******************************************************************************
 
   Title:      HOL/Auth/Message
   Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
   Copyright   1996  University of Cambridge
 
   Datatypes of agents and messages;
   Inductive relations "parts", "analz" and "synth"
 
 ********************************************************************************
 
   Edited:  Tobias Klenze, ETH Zurich <tobias.klenze@inf.ethz.ch>
            Christoph Sprenger, ETH Zurich <sprenger@inf.ethz.ch>
 
   Integrated and adapted for security protocol refinement and to add a constructor for finite sets.
 
 *******************************************************************************)
 
 section \<open>Theory of ASes and Messages for Security Protocols\<close>
 
 theory Message imports Keys "HOL-Library.Sublist" "HOL.Finite_Set" "HOL-Library.FSet"
 begin
 
 datatype msgterm =
     \<epsilon>                                  \<comment> \<open>Empty message. Used for instance to denote non-existent interface\<close>
   | AS as                              \<comment> \<open>Autonomous System identifier, i.e. agents. Note that AS is an alias of nat\<close>
   | Num nat                            \<comment> \<open>Ordinary integers, timestamps, ...\<close>
   | Key    key                         \<comment> \<open>Crypto keys\<close>
   | Nonce  nonce                       \<comment> \<open>Unguessable nonces\<close>
   | L      "msgterm list"              \<comment> \<open>Lists\<close>
   | FS     "msgterm fset"              \<comment> \<open>Finite Sets. Used to represent XOR values.\<close>
   | MPair  msgterm msgterm             \<comment> \<open>Compound messages\<close>
   | Hash    msgterm                    \<comment> \<open>Hashing\<close>
   | Crypt  key msgterm                 \<comment> \<open>Encryption, public- or shared-key\<close>
 
 text \<open>Syntax sugar\<close>
 syntax
   "_MTuple" :: "['a, args] \<Rightarrow> 'a * 'b"       ("(2\<langle>_,/ _\<rangle>)")
 
 syntax (xsymbols)
   "_MTuple" :: "['a, args] \<Rightarrow> 'a * 'b"       ("(2\<langle>_,/ _\<rangle>)")
 
 translations
   "\<langle>x, y, z\<rangle>" \<rightleftharpoons> "\<langle>x, \<langle>y, z\<rangle>\<rangle>"
   "\<langle>x, y\<rangle>"    \<rightleftharpoons> "CONST MPair x y"
 
 syntax
   "_MHF" :: "['a, 'b , 'c, 'd, 'e] \<Rightarrow> 'a * 'b * 'c * 'd * 'e"  ("(5HF\<lhd>_,/ _,/ _,/ _,/ _\<rhd>)")
 
 abbreviation
   Mac :: "[msgterm,msgterm] \<Rightarrow> msgterm"                       ("(4Mac[_] /_)" [0, 1000])
 where
   \<comment> \<open>Message Y paired with a MAC computed with the help of X\<close>
   "Mac[X] Y \<equiv> Hash \<langle>X,Y\<rangle>"
 
 abbreviation macKey where "macKey a \<equiv> Key (macK a)"
 
 definition
   keysFor :: "msgterm set \<Rightarrow> key set"
 where
   \<comment> \<open>Keys useful to decrypt elements of a message set\<close>
   "keysFor H \<equiv> invKey ` {K. \<exists>X. Crypt K X \<in> H}"
 
 subsubsection \<open>Inductive Definition of "All Parts" of a Message\<close>
 
 inductive_set
   parts :: "msgterm set \<Rightarrow> msgterm set"
   for H :: "msgterm set"
   where
     Inj [intro]: "X \<in> H \<Longrightarrow> X \<in> parts H"
   | Fst:         "\<langle>X,_\<rangle> \<in> parts H \<Longrightarrow> X \<in> parts H"
   | Snd:         "\<langle>_,Y\<rangle> \<in> parts H \<Longrightarrow> Y \<in> parts H"
   | Lst:         "\<lbrakk> L xs \<in> parts H; X \<in> set xs \<rbrakk> \<Longrightarrow> X \<in> parts H"
   | FSt:          "\<lbrakk> FS xs \<in> parts H; X |\<in>| xs \<rbrakk> \<Longrightarrow> X \<in> parts H"
 (*| Hd:          "L (X # xs) \<in> parts H \<Longrightarrow> X \<in> parts H"
   | Tl:          "L (X # xs) \<in> parts H \<Longrightarrow> L xs \<in> parts H" *)
   | Body:        "Crypt K X \<in> parts H \<Longrightarrow> X \<in> parts H"
 
 
 text \<open>Monotonicity\<close>
 lemma parts_mono: "G \<subseteq> H \<Longrightarrow> parts G \<subseteq> parts H"
 apply auto
 apply (erule parts.induct)
 apply (blast dest: parts.Fst parts.Snd parts.Lst parts.FSt parts.Body)+
 done
 
 
 text \<open>Equations hold because constructors are injective.\<close>
 lemma Other_image_eq [simp]: "(AS x \<in> AS`A) = (x:A)"
 by auto
 
 lemma Key_image_eq [simp]: "(Key x \<in> Key`A) = (x\<in>A)"
 by auto
 
 lemma AS_Key_image_eq [simp]: "(AS x \<notin> Key`A)"
 by auto
 
 lemma Num_Key_image_eq [simp]: "(Num x \<notin> Key`A)"
 by auto
 
 subsection \<open>keysFor operator\<close>
 
 lemma keysFor_empty [simp]: "keysFor {} = {}"
 by (unfold keysFor_def, blast)
 
 lemma keysFor_Un [simp]: "keysFor (H \<union> H') = keysFor H \<union> keysFor H'"
 by (unfold keysFor_def, blast)
 
 lemma keysFor_UN [simp]: "keysFor (\<Union>i\<in>A. H i) = (\<Union>i\<in>A. keysFor (H i))"
 by (unfold keysFor_def, blast)
 
 text \<open>Monotonicity\<close>
 lemma keysFor_mono: "G \<subseteq> H \<Longrightarrow> keysFor G \<subseteq> keysFor H"
 by (unfold keysFor_def, blast)
 
 lemma keysFor_insert_AS [simp]: "keysFor (insert (AS A) H) = keysFor H"
 by (unfold keysFor_def, auto)
 
 lemma keysFor_insert_Num [simp]: "keysFor (insert (Num N) H) = keysFor H"
 by (unfold keysFor_def, auto)
 
 lemma keysFor_insert_Key [simp]: "keysFor (insert (Key K) H) = keysFor H"
 by (unfold keysFor_def, auto)
 
 lemma keysFor_insert_Nonce [simp]: "keysFor (insert (Nonce n) H) = keysFor H"
 by (unfold keysFor_def, auto)
 
 lemma keysFor_insert_L [simp]: "keysFor (insert (L X) H) = keysFor H"
 by (unfold keysFor_def, auto)
 
 lemma keysFor_insert_FS [simp]: "keysFor (insert (FS X) H) = keysFor H"
 by (unfold keysFor_def, auto)
 
 lemma keysFor_insert_Hash [simp]: "keysFor (insert (Hash X) H) = keysFor H"
 by (unfold keysFor_def, auto)
 
 lemma keysFor_insert_MPair [simp]: "keysFor (insert \<langle>X,Y\<rangle> H) = keysFor H"
 by (unfold keysFor_def, auto)
 
 lemma keysFor_insert_Crypt [simp]:
   "keysFor (insert (Crypt K X) H) = insert (invKey K) (keysFor H)"
 by (unfold keysFor_def, auto)
 
 lemma keysFor_image_Key [simp]: "keysFor (Key`E) = {}"
 by (unfold keysFor_def, auto)
 
 lemma Crypt_imp_invKey_keysFor: "Crypt K X \<in> H \<Longrightarrow> invKey K \<in> keysFor H"
 by (unfold keysFor_def, blast)
 
 
 subsection \<open>Inductive relation "parts"\<close>
 
 lemma MPair_parts:
   "\<lbrakk>
     \<langle>X,Y\<rangle> \<in> parts H;
     \<lbrakk> X \<in> parts H; Y \<in> parts H \<rbrakk> \<Longrightarrow> P
    \<rbrakk> \<Longrightarrow> P"
 by (blast dest: parts.Fst parts.Snd)
 
 lemma L_parts:
   "\<lbrakk>
     L l \<in> parts H;
     \<lbrakk> set l \<subseteq> parts H \<rbrakk> \<Longrightarrow> P
    \<rbrakk> \<Longrightarrow> P"
   by (blast dest: parts.Lst)
 
 lemma FS_parts:
   "\<lbrakk>
     FS l \<in> parts H;
     \<lbrakk> fset l \<subseteq> parts H \<rbrakk> \<Longrightarrow> P
    \<rbrakk> \<Longrightarrow> P"
   by (simp add: fmember_iff_member_fset parts.FSt subsetI)
 thm fmember_iff_member_fset parts.FSt subsetI
 
 declare fmember_iff_member_fset[simp]
 declare MPair_parts [elim!] L_parts [elim!] FS_parts [elim] parts.Body [dest!]
 
 text \<open>NB These two rules are UNSAFE in the formal sense, as they discard the
         compound message.  They work well on THIS FILE.
         @{text MPair_parts} is left as SAFE because it speeds up proofs.
         The Crypt rule is normally kept UNSAFE to avoid breaking up certificates.\<close>
 
 lemma parts_increasing: "H \<subseteq> parts H"
 by blast
 
 lemmas parts_insertI = subset_insertI [THEN parts_mono, THEN subsetD]
 
 lemma parts_empty [simp]: "parts{} = {}"
 apply safe
 apply (erule parts.induct, blast+)
 done
 
 lemma parts_emptyE [elim!]: "X\<in> parts{} \<Longrightarrow> P"
 by simp
 
 text \<open>WARNING: loops if H = {Y}, therefore must not be repeated!\<close>
 lemma parts_singleton: "X \<in> parts H \<Longrightarrow> \<exists>Y \<in> H. X \<in> parts {Y}"
   apply (erule parts.induct, fast)
   using parts.FSt by blast+
 
 lemma parts_singleton_set: "x \<in> parts {s . P s} \<Longrightarrow> \<exists>Y. P Y \<and> x \<in> parts {Y}"
   by(auto dest: parts_singleton)
 
 lemma parts_singleton_set_rev: "\<lbrakk>x \<in> parts {Y}; P Y\<rbrakk> \<Longrightarrow> x \<in> parts {s . P s}"
   by (induction rule: parts.induct)
      (blast dest: parts.Fst parts.Snd parts.Lst parts.FSt parts.Body)+
 
 lemma parts_Hash: "\<lbrakk>\<And>t . t \<in> H \<Longrightarrow> \<exists>t' . t = Hash t'\<rbrakk> \<Longrightarrow> parts H = H"
   by (auto, erule parts.induct, fast+)
 
 subsubsection \<open>Unions\<close>
 
 lemma parts_Un_subset1: "parts G \<union> parts H \<subseteq> parts(G \<union> H)"
 by (intro Un_least parts_mono Un_upper1 Un_upper2)
 
 lemma parts_Un_subset2: "parts(G \<union> H) \<subseteq> parts G \<union> parts H"
 apply (rule subsetI)
   apply (erule parts.induct, blast+)
   using parts.FSt by auto
 
 lemma parts_Un [simp]: "parts(G \<union> H) = parts G \<union> parts H"
 by (intro equalityI parts_Un_subset1 parts_Un_subset2)
 
 lemma parts_insert: "parts (insert X H) = parts {X} \<union> parts H"
 apply (subst insert_is_Un [of _ H])
 apply (simp only: parts_Un)
 done
 
 text \<open>TWO inserts to avoid looping.  This rewrite is better than nothing.
         Not suitable for Addsimps: its behaviour can be strange.\<close>
 lemma parts_insert2:
   "parts (insert X (insert Y H)) = parts {X} \<union> parts {Y} \<union> parts H"
 apply (simp add: Un_assoc)
 apply (simp add: parts_insert [symmetric])
 done
 
 (*needed?!*)
 lemma parts_two: "\<lbrakk>x \<in> parts {e1, e2}; x \<notin> parts {e1}\<rbrakk>\<Longrightarrow> x \<in> parts {e2}"
   by (simp add: parts_insert2)
 
-lemma parts_UN_subset1: "(\<Union>x\<in>A. parts(H x)) \<subseteq> parts(\<Union>x\<in>A. H x)"
-by (intro UN_least parts_mono UN_upper)
 
-lemma parts_UN_subset2: "parts(\<Union>x\<in>A. H x) \<subseteq> (\<Union>x\<in>A. parts(H x))"
-apply (rule subsetI)
-  apply (erule parts.induct)
-  using parts.FSt by auto
-
-lemma parts_UN [simp]: "parts(\<Union>x\<in>A. H x) = (\<Union>x\<in>A. parts(H x))"
-by (intro equalityI parts_UN_subset1 parts_UN_subset2)
-
-
-text \<open>Added to simplify arguments to parts, analz and synth.
-        NOTE: the UN versions are no longer used!\<close>
+text \<open>Added to simplify arguments to parts, analz and synth.\<close>
 
 
 text \<open>This allows @{text blast} to simplify occurrences of
         @{term "parts(G\<union>H)"} in the assumption.\<close>
 lemmas in_parts_UnE = parts_Un [THEN equalityD1, THEN subsetD, THEN UnE]
 declare in_parts_UnE [elim!]
 
 
 lemma parts_insert_subset: "insert X (parts H) \<subseteq> parts(insert X H)"
 by (blast intro: parts_mono [THEN [2] rev_subsetD])
 
 
 
 subsubsection \<open>Idempotence\<close>
 
 lemma parts_partsD [dest!]: "X\<in> parts (parts H) \<Longrightarrow> X\<in> parts H"
   apply (erule parts.induct, blast+)
   using parts.FSt by auto
 
 lemma parts_idem [simp]: "parts (parts H) = parts H"
 by blast
 
 lemma parts_subset_iff [simp]: "(parts G \<subseteq> parts H) = (G \<subseteq> parts H)"
 apply (rule iffI)
 apply (iprover intro: subset_trans parts_increasing)
 apply (frule parts_mono, simp)
 done
 
 subsubsection \<open>Transitivity\<close>
 lemma parts_trans: "\<lbrakk> X\<in> parts G;  G \<subseteq> parts H \<rbrakk> \<Longrightarrow> X\<in> parts H"
 by (drule parts_mono, blast)
 
 subsubsection \<open>Unions, revisited\<close>
 text \<open>You can take the union of parts h for all h in H\<close>
 lemma parts_split: "parts H = \<Union> { parts {h} | h . h \<in> H}"
 apply auto
 apply (erule parts.induct)
 apply (blast dest: parts.Fst parts.Snd parts.Lst parts.FSt parts.Body)+
 using parts_trans apply blast
 done
 
 text \<open>Cut\<close>
 lemma parts_cut:
   "\<lbrakk> Y\<in> parts (insert X G);  X \<in> parts H \<rbrakk> \<Longrightarrow> Y \<in> parts (G \<union> H)"
 by (blast intro: parts_trans)
 
 
 lemma parts_cut_eq [simp]: "X \<in> parts H \<Longrightarrow> parts (insert X H) = parts H"
 by (force dest!: parts_cut intro: parts_insertI)
 
 
 subsubsection \<open>Rewrite rules for pulling out atomic messages\<close>
 
 lemmas parts_insert_eq_I = equalityI [OF subsetI parts_insert_subset]
 
 
 lemma parts_insert_AS [simp]:
   "parts (insert (AS agt) H) = insert (AS agt) (parts H)"
 apply (rule parts_insert_eq_I)
 by (erule parts.induct, auto elim!: FS_parts)
 
 lemma parts_insert_Epsilon [simp]:
   "parts (insert \<epsilon> H) = insert \<epsilon> (parts H)"
 apply (rule parts_insert_eq_I)
   by (erule parts.induct, auto)
 
 lemma parts_insert_Num [simp]:
   "parts (insert (Num N) H) = insert (Num N) (parts H)"
 apply (rule parts_insert_eq_I)
 by (erule parts.induct, auto)
 
 lemma parts_insert_Key [simp]:
   "parts (insert (Key K) H) = insert (Key K) (parts H)"
 apply (rule parts_insert_eq_I)
 by (erule parts.induct, auto)
 
 lemma parts_insert_Nonce [simp]:
   "parts (insert (Nonce n) H) = insert (Nonce n) (parts H)"
 apply (rule parts_insert_eq_I)
 by (erule parts.induct, auto)
 
 lemma parts_insert_Hash [simp]:
   "parts (insert (Hash X) H) = insert (Hash X) (parts H)"
 apply (rule parts_insert_eq_I)
 by (erule parts.induct, auto)
 
 lemma parts_insert_Crypt [simp]:
   "parts (insert (Crypt K X) H) = insert (Crypt K X) (parts (insert X H))"
 apply (rule equalityI)
 apply (rule subsetI)
 apply (erule parts.induct, auto)
 by (blast intro: parts.Body)
 
 lemma parts_insert_MPair [simp]:
   "parts (insert \<langle>X,Y\<rangle> H) =
     insert \<langle>X,Y\<rangle> (parts (insert X (insert Y H)))"
 apply (rule equalityI)
 apply (rule subsetI)
 apply (erule parts.induct, auto)
 by (blast intro: parts.Fst parts.Snd)+
 
 lemma parts_insert_L [simp]:
   "parts (insert (L xs) H) =
     insert (L xs) (parts ((set xs) \<union>  H))"
 apply (rule equalityI)
 apply (rule subsetI)
 apply (erule parts.induct, auto)
 by (blast intro: parts.Lst)+
 
 lemma parts_insert_FS [simp]:
   "parts (insert (FS xs) H) =
     insert (FS xs) (parts ((fset xs) \<union>  H))"
 apply (rule equalityI)
 apply (rule subsetI)
 apply (erule parts.induct, auto)
 by (auto intro: parts.FSt)+
 
 lemma parts_image_Key [simp]: "parts (Key`N) = Key`N"
 apply auto
 apply (erule parts.induct, auto)
 done
 
 
 text \<open>Parts of lists and finite sets.\<close>
 
 lemma parts_list_set (*[simp]*):
   "parts (L`ls) =  (L`ls) \<union> (\<Union>l \<in> ls. parts (set l)) "
 apply (rule equalityI, rule subsetI)
 apply (erule parts.induct, auto)
 by (meson L_parts image_subset_iff parts_increasing parts_trans)
 
 lemma parts_insert_list_set (*[simp]*):
   "parts ((L`ls) \<union> H) =  (L`ls) \<union> (\<Union>l \<in> ls. parts ((set l))) \<union> parts H"
 apply (rule equalityI, rule subsetI)
 by (erule parts.induct, auto simp add: parts_list_set)
 
 (*needed?!*)
 lemma parts_fset_set (*[simp]*):
   "parts (FS`ls) =  (FS`ls) \<union> (\<Union>l \<in> ls. parts (fset l)) "
 apply (rule equalityI, rule subsetI)
 apply (erule parts.induct, auto)
 by (meson FS_parts image_subset_iff parts_increasing parts_trans)
 
 subsubsection \<open>suffix of parts\<close>
 lemma suffix_in_parts:
   "suffix (x#xs) ys \<Longrightarrow> x \<in> parts {L ys}"
 by (auto simp add: suffix_def)
 
 lemma parts_L_set:
   "\<lbrakk>x \<in> parts {L ys}; ys \<in> St\<rbrakk> \<Longrightarrow> x \<in> parts (L`St)"
 by (metis (no_types, lifting) image_insert insert_iff mk_disjoint_insert parts.Inj
     parts_cut_eq parts_insert parts_insert2)
 
 lemma suffix_in_parts_set:
   "\<lbrakk>suffix (x#xs) ys; ys \<in> St\<rbrakk> \<Longrightarrow> x \<in> parts (L`St)"
 using parts_L_set suffix_in_parts
 by blast
 
 subsection \<open>Inductive relation "analz"\<close>
 
 text \<open>Inductive definition of "analz" -- what can be broken down from a set of
         messages, including keys.  A form of downward closure.  Pairs can
         be taken apart; messages decrypted with known keys.\<close>
 
 inductive_set
   analz :: "msgterm set \<Rightarrow> msgterm set"
   for H :: "msgterm set"
   where
     Inj [intro,simp] : "X \<in> H \<Longrightarrow> X \<in> analz H"
   | Fst:               "\<langle>X,Y\<rangle> \<in> analz H \<Longrightarrow> X \<in> analz H"
   | Snd:               "\<langle>X,Y\<rangle> \<in> analz H \<Longrightarrow> Y \<in> analz H"
   | Lst:               "(L y) \<in> analz H  \<Longrightarrow> x \<in> set (y) \<Longrightarrow> x \<in> analz H "
   | FSt:               "\<lbrakk> FS xs \<in> analz H; X |\<in>| xs \<rbrakk> \<Longrightarrow> X \<in> analz H"
   | Decrypt [dest]:    "\<lbrakk> Crypt K X \<in> analz H; Key (invKey K) \<in> analz H \<rbrakk> \<Longrightarrow> X \<in> analz H"
 
 
 text \<open>Monotonicity; Lemma 1 of Lowe's paper\<close>
 lemma analz_mono: "G \<subseteq> H \<Longrightarrow> analz(G) \<subseteq> analz(H)"
 apply auto
 apply (erule analz.induct)
 apply (auto dest: analz.Fst analz.Snd analz.Lst analz.FSt )
 done
 
 lemmas analz_monotonic = analz_mono [THEN [2] rev_subsetD]
 
 text \<open>Making it safe speeds up proofs\<close>
 lemma MPair_analz [elim!]:
   "\<lbrakk>
     \<langle>X,Y\<rangle> \<in> analz H;
     \<lbrakk> X \<in> analz H; Y \<in> analz H \<rbrakk> \<Longrightarrow> P
    \<rbrakk> \<Longrightarrow> P"
 by (blast dest: analz.Fst analz.Snd)
 
 lemma L_analz [elim!]:
   "\<lbrakk>
     L l \<in> analz H;
     \<lbrakk> set l \<subseteq> analz H \<rbrakk> \<Longrightarrow> P
    \<rbrakk> \<Longrightarrow> P"
 by (blast dest: analz.Lst analz.FSt)
 
 lemma FS_analz [elim!]:
   "\<lbrakk>
     FS l \<in> analz H;
     \<lbrakk> fset l \<subseteq> analz H \<rbrakk> \<Longrightarrow> P
    \<rbrakk> \<Longrightarrow> P"
   by (simp add: fmember_iff_member_fset analz.FSt subsetI)
 
 thm fmember_iff_member_fset parts.FSt subsetI
 lemma analz_increasing: "H \<subseteq> analz(H)"
 by blast
 
 lemma analz_subset_parts: "analz H \<subseteq> parts H"
 apply (rule subsetI)
   apply (erule analz.induct, blast+)
   apply auto
 done
 
 
 text \<open>If there is no cryptography, then analz and parts is equivalent.\<close>
 lemma no_crypt_analz_is_parts:
   "\<not> (\<exists> K X . Crypt K X \<in> parts A) \<Longrightarrow> analz A = parts A"
 apply (rule equalityI, simp add: analz_subset_parts)
 apply (rule subsetI)
 by (erule parts.induct, blast+, auto)
 
 lemmas analz_into_parts = analz_subset_parts [THEN subsetD]
 
 lemmas not_parts_not_analz = analz_subset_parts [THEN contra_subsetD]
 
 
 lemma parts_analz [simp]: "parts (analz H) = parts H"
 apply (rule equalityI)
 apply (rule analz_subset_parts [THEN parts_mono, THEN subset_trans], simp)
 apply (blast intro: analz_increasing [THEN parts_mono, THEN subsetD])
 done
 
 lemma analz_parts [simp]: "analz (parts H) = parts H"
 apply auto
 apply (erule analz.induct, auto)
 done
 
 lemmas analz_insertI = subset_insertI [THEN analz_mono, THEN [2] rev_subsetD]
 
 subsubsection \<open>General equational properties\<close>
 
 lemma analz_empty [simp]: "analz {} = {}"
 apply safe
 apply (erule analz.induct, blast+)
 done
 
 text \<open>Converse fails: we can analz more from the union than from the
         separate parts, as a key in one might decrypt a message in the other\<close>
 lemma analz_Un: "analz(G) \<union> analz(H) \<subseteq> analz(G \<union> H)"
 by (intro Un_least analz_mono Un_upper1 Un_upper2)
 
 lemma analz_insert: "insert X (analz H) \<subseteq> analz(insert X H)"
 by (blast intro: analz_mono [THEN [2] rev_subsetD])
 
 subsubsection \<open>Rewrite rules for pulling out atomic messages\<close>
 
 lemmas analz_insert_eq_I = equalityI [OF subsetI analz_insert]
 
 lemma analz_insert_AS [simp]:
   "analz (insert (AS agt) H) = insert (AS agt) (analz H)"
 apply (rule analz_insert_eq_I)
 by (erule analz.induct, auto)
 
 lemma analz_insert_Num [simp]:
   "analz (insert (Num N) H) = insert (Num N) (analz H)"
 apply (rule analz_insert_eq_I)
 by (erule analz.induct, auto)
 
 text \<open>Can only pull out Keys if they are not needed to decrypt the rest\<close>
 lemma analz_insert_Key [simp]:
   "K \<notin> keysFor (analz H) \<Longrightarrow>
     analz (insert (Key K) H) = insert (Key K) (analz H)"
 apply (unfold keysFor_def)
 apply (rule analz_insert_eq_I)
 by (erule analz.induct, auto)
 
 lemma analz_insert_LEmpty [simp]:
   "analz (insert (L []) H) = insert (L []) (analz H)"
 apply (rule analz_insert_eq_I)
 by (erule analz.induct, auto)
 
 
 lemma analz_insert_L [simp]:
   "analz (insert (L l) H) = insert (L l) (analz (set l \<union> H))"
 apply (rule equalityI)
 apply (rule subsetI)
 apply (erule analz.induct, auto)
 apply (erule analz.induct, auto)
 using analz.Inj by blast
 
 lemma analz_insert_FS [simp]:
   "analz (insert (FS l) H) = insert (FS l) (analz (fset l \<union> H))"
 apply (rule equalityI)
 apply (rule subsetI)
 apply (erule analz.induct, auto)
 apply (erule analz.induct, auto)
 using analz.Inj by blast
 
 lemma "L[] \<in> analz {L[L[]]}"
 using analz.Inj by simp
 
 lemma analz_insert_Hash [simp]:
   "analz (insert (Hash X) H) = insert (Hash X) (analz H)"
 apply (rule analz_insert_eq_I)
 by (erule analz.induct, auto)
 
 lemma analz_insert_MPair [simp]:
   "analz (insert \<langle>X,Y\<rangle> H) =
     insert \<langle>X,Y\<rangle> (analz (insert X (insert Y H)))"
 apply (rule equalityI)
 apply (rule subsetI)
 apply (erule analz.induct, auto)
 apply (erule analz.induct, auto)
 using Fst Snd analz.Inj insertI1
 by (metis)+
 
 
 text \<open>Can pull out enCrypted message if the Key is not known\<close>
 lemma analz_insert_Crypt:
   "Key (invKey K) \<notin> analz H
     \<Longrightarrow> analz (insert (Crypt K X) H) = insert (Crypt K X) (analz H)"
 apply (rule analz_insert_eq_I)
 by (erule analz.induct, auto)
 
 lemma analz_insert_Decrypt1:
   "Key (invKey K) \<in> analz H \<Longrightarrow>
     analz (insert (Crypt K X) H) \<subseteq>
     insert (Crypt K X) (analz (insert X H))"
 apply (rule subsetI)
 by (erule_tac x = x in analz.induct, auto)
 
 lemma analz_insert_Decrypt2:
   "Key (invKey K) \<in> analz H \<Longrightarrow>
     insert (Crypt K X) (analz (insert X H)) \<subseteq>
     analz (insert (Crypt K X) H)"
 apply auto
 apply (erule_tac x = x in analz.induct, auto)
 by (blast intro: analz_insertI analz.Decrypt)
 
 lemma analz_insert_Decrypt:
   "Key (invKey K) \<in> analz H \<Longrightarrow>
     analz (insert (Crypt K X) H) =
     insert (Crypt K X) (analz (insert X H))"
 by (intro equalityI analz_insert_Decrypt1 analz_insert_Decrypt2)
 
 text \<open>Case analysis: either the message is secure, or it is not! Effective,
         but can cause subgoals to blow up! Use with @{text "split_if"}; apparently
         @{text "split_tac"} does not cope with patterns such as @{term"analz (insert
         (Crypt K X) H)"}\<close>
 lemma analz_Crypt_if [simp]:
   "analz (insert (Crypt K X) H) =
     (if (Key (invKey K) \<in> analz H)
      then insert (Crypt K X) (analz (insert X H))
      else insert (Crypt K X) (analz H))"
 by (simp add: analz_insert_Crypt analz_insert_Decrypt)
 
 
 text \<open>This rule supposes "for the sake of argument" that we have the key.\<close>
 lemma analz_insert_Crypt_subset:
   "analz (insert (Crypt K X) H) \<subseteq>
     insert (Crypt K X) (analz (insert X H))"
 apply (rule subsetI)
 by (erule analz.induct, auto)
 
 lemma analz_image_Key [simp]: "analz (Key`N) = Key`N"
 apply auto
 apply (erule analz.induct, auto)
 done
 
 
 subsubsection \<open>Idempotence and transitivity\<close>
 
 lemma analz_analzD [dest!]: "X\<in> analz (analz H) \<Longrightarrow> X\<in> analz H"
 by (erule analz.induct, auto)
 
 lemma analz_idem [simp]: "analz (analz H) = analz H"
 by blast
 
 lemma analz_subset_iff [simp]: "(analz G \<subseteq> analz H) = (G \<subseteq> analz H)"
 apply (rule iffI)
 apply (iprover intro: subset_trans analz_increasing)
 apply (frule analz_mono, simp)
 done
 
 lemma analz_trans: "\<lbrakk> X\<in> analz G;  G \<subseteq> analz H \<rbrakk> \<Longrightarrow> X\<in> analz H"
 by (drule analz_mono, blast)
 
 text \<open>Cut; Lemma 2 of Lowe\<close>
 lemma analz_cut: "\<lbrakk> Y\<in> analz (insert X H);  X\<in> analz H \<rbrakk> \<Longrightarrow> Y\<in> analz H"
 by (erule analz_trans, blast)
 
 (*Cut can be proved easily by induction on
    "Y: analz (insert X H) \<Longrightarrow> X: analz H --> Y: analz H"
 *)
 
 text \<open>This rewrite rule helps in the simplification of messages that involve
         the forwarding of unknown components (X).  Without it, removing occurrences
         of X can be very complicated.\<close>
 lemma analz_insert_eq: "X\<in> analz H \<Longrightarrow> analz (insert X H) = analz H"
 by (blast intro: analz_cut analz_insertI)
 
 
 text \<open>A congruence rule for "analz"\<close>
 
 lemma analz_subset_cong:
   "\<lbrakk> analz G \<subseteq> analz G'; analz H \<subseteq> analz H' \<rbrakk>
     \<Longrightarrow> analz (G \<union> H) \<subseteq> analz (G' \<union> H')"
 apply simp
 apply (iprover intro: conjI subset_trans analz_mono Un_upper1 Un_upper2)
 done
 
 lemma analz_cong:
   "\<lbrakk> analz G = analz G'; analz H = analz H' \<rbrakk>
     \<Longrightarrow> analz (G \<union> H) = analz (G' \<union> H')"
 by (intro equalityI analz_subset_cong, simp_all)
 
 lemma analz_insert_cong:
   "analz H = analz H' \<Longrightarrow> analz(insert X H) = analz(insert X H')"
 by (force simp only: insert_def intro!: analz_cong)
 
 text \<open>If there are no pairs, lists or encryptions then analz does nothing\<close>
 (*needed?*)
 lemma analz_trivial:
   "\<lbrakk>
     \<forall>X Y. \<langle>X,Y\<rangle> \<notin> H; \<forall>xs. L xs \<notin> H; \<forall>xs. FS xs \<notin> H;
     \<forall>X K. Crypt K X \<notin> H
    \<rbrakk> \<Longrightarrow> analz H = H"
 apply safe
 by (erule analz.induct, auto)
 
 text \<open>These two are obsolete (with a single Spy) but cost little to prove...\<close>
 lemma analz_UN_analz_lemma:
   "X\<in> analz (\<Union>i\<in>A. analz (H i)) \<Longrightarrow> X\<in> analz (\<Union>i\<in>A. H i)"
 apply (erule analz.induct)
 by (auto intro: analz_mono [THEN [2] rev_subsetD])
 
 lemma analz_UN_analz [simp]: "analz (\<Union>i\<in>A. analz (H i)) = analz (\<Union>i\<in>A. H i)"
 by (blast intro: analz_UN_analz_lemma analz_mono [THEN [2] rev_subsetD])
 
 
 subsubsection \<open>Lemmas assuming absense of keys\<close>
 text \<open>If there are no keys in analz H, you can take the union of analz h for all h in H\<close>
 
 lemma analz_split:
   "\<not>(\<exists> K . Key K \<in> analz H)
     \<Longrightarrow> analz H = \<Union> { analz {h} | h . h \<in> H}"
 apply auto
 subgoal
   apply (erule analz.induct)
   apply (auto dest: analz.Fst analz.Snd analz.Lst analz.FSt)
 done
   apply (erule analz.induct)
   apply (auto dest: analz.Fst analz.Snd analz.Lst analz.FSt)
 done
 
 lemma analz_Un_eq:
   assumes "\<not>(\<exists> K . Key K \<in> analz H)" and "\<not>(\<exists> K . Key K \<in> analz G)"
   shows "analz (H \<union> G) = analz H \<union> analz G"
 apply (intro equalityI, rule subsetI)
 apply (erule analz.induct)
 using assms by auto
 
 lemma analz_Un_eq_Crypt:
   assumes "\<not>(\<exists> K . Key K \<in> analz G)" and "\<not>(\<exists> K X . Crypt K X \<in> analz G)"
   shows "analz (H \<union> G) = analz H \<union> analz G"
 apply (intro equalityI, rule subsetI)
 apply (erule analz.induct)
 using assms by auto
 
 lemma analz_list_set (*[simp]*):
   "\<not>(\<exists> K . Key K \<in> analz (L`ls))
     \<Longrightarrow> analz (L`ls) =  (L`ls) \<union> (\<Union>l \<in> ls. analz (set l)) "
 apply (rule equalityI, rule subsetI)
 apply (erule analz.induct, auto)
 using L_analz image_subset_iff analz_increasing analz_trans by metis
 
 lemma analz_fset_set (*[simp]*):
   "\<not>(\<exists> K . Key K \<in> analz (FS`ls))
     \<Longrightarrow> analz (FS`ls) =  (FS`ls) \<union> (\<Union>l \<in> ls. analz (fset l)) "
 apply (rule equalityI, rule subsetI)
 apply (erule analz.induct, auto)
 using FS_analz image_subset_iff analz_increasing analz_trans by metis
 
 
 subsection \<open>Inductive relation "synth"\<close>
 
 text \<open>Inductive definition of "synth" -- what can be built up from a set of
         messages.  A form of upward closure.  Pairs can be built, messages
         encrypted with known keys.  AS names are public domain.
         Nums can be guessed, but Nonces cannot be.\<close>
 
 inductive_set
   synth :: "msgterm set \<Rightarrow> msgterm set"
   for H :: "msgterm set"
   where
     Inj    [intro]:   "X \<in> H \<Longrightarrow> X \<in> synth H"
   | \<epsilon>  [simp,intro!]:   "\<epsilon> \<in> synth H"
   | AS  [simp,intro!]:   "AS agt \<in> synth H"
   | Num [simp,intro!]:   "Num n  \<in> synth H"
   | Lst [intro]:      "\<lbrakk> \<And>x . x \<in> set xs \<Longrightarrow> x \<in> synth H \<rbrakk> \<Longrightarrow> L xs \<in> synth H"
-  | FSt [intro]:      "\<lbrakk> \<And>x . x \<in> fset xs \<Longrightarrow> x \<in> synth H; 
-                         \<And>x ys . x \<in> fset xs \<Longrightarrow> x \<noteq> FS ys \<rbrakk> 
+  | FSt [intro]:      "\<lbrakk> \<And>x . x \<in> fset xs \<Longrightarrow> x \<in> synth H;
+                         \<And>x ys . x \<in> fset xs \<Longrightarrow> x \<noteq> FS ys \<rbrakk>
                       \<Longrightarrow> FS xs \<in> synth H"
   | Hash   [intro]:   "X \<in> synth H \<Longrightarrow> Hash X \<in> synth H"
   | MPair  [intro]:   "\<lbrakk> X \<in> synth H;  Y \<in> synth H \<rbrakk> \<Longrightarrow> \<langle>X,Y\<rangle> \<in> synth H"
   | Crypt  [intro]:   "\<lbrakk> X \<in> synth H;  Key K \<in> H \<rbrakk> \<Longrightarrow> Crypt K X \<in> synth H"
 
 
 (*removed fcard xs \<noteq> Suc 0 from FSt premise*)
 
 
 text \<open>Monotonicity\<close>
 lemma synth_mono: "G \<subseteq> H \<Longrightarrow> synth(G) \<subseteq> synth(H)"
   apply (auto, erule synth.induct, auto)
   by blast
 
 text \<open>NO @{text AS_synth}, as any AS name can be synthesized.
         The same holds for @{term Num}\<close>
 inductive_cases Key_synth   [elim!]: "Key K \<in> synth H"
 inductive_cases Nonce_synth [elim!]: "Nonce n \<in> synth H"
 inductive_cases Hash_synth  [elim!]: "Hash X \<in> synth H"
 inductive_cases MPair_synth [elim!]: "\<langle>X,Y\<rangle> \<in> synth H"
 inductive_cases L_synth     [elim!]: "L X \<in> synth H"
 inductive_cases FS_synth    [elim!]: "FS X \<in> synth H"
 inductive_cases Crypt_synth [elim!]: "Crypt K X \<in> synth H"
 
 lemma synth_increasing: "H \<subseteq> synth(H)"
 by blast
 
 lemma synth_analz_self: "x \<in> H \<Longrightarrow> x \<in> synth (analz H)"
   by blast
 
 subsubsection \<open>Unions\<close>
 
 text \<open>Converse fails: we can synth more from the union than from the
         separate parts, building a compound message using elements of each.\<close>
 lemma synth_Un: "synth(G) \<union> synth(H) \<subseteq> synth(G \<union> H)"
 by (intro Un_least synth_mono Un_upper1 Un_upper2)
 
 lemma synth_insert: "insert X (synth H) \<subseteq> synth(insert X H)"
 by (blast intro: synth_mono [THEN [2] rev_subsetD])
 
 subsubsection \<open>Idempotence and transitivity\<close>
 
 lemma synth_synthD [dest!]: "X\<in> synth (synth H) \<Longrightarrow> X \<in> synth H"
 apply (erule synth.induct, blast)
 apply auto by blast
 
 lemma synth_idem: "synth (synth H) = synth H"
 by blast
 
 lemma synth_subset_iff [simp]: "(synth G \<subseteq> synth H) = (G \<subseteq> synth H)"
 apply (rule iffI)
 apply (iprover intro: subset_trans synth_increasing)
 apply (frule synth_mono, simp add: synth_idem)
 done
 
 lemma synth_trans: "\<lbrakk> X\<in> synth G;  G \<subseteq> synth H \<rbrakk> \<Longrightarrow> X\<in> synth H"
 by (drule synth_mono, blast)
 
 text \<open>Cut; Lemma 2 of Lowe\<close>
 lemma synth_cut: "\<lbrakk> Y\<in> synth (insert X H);  X\<in> synth H \<rbrakk> \<Longrightarrow> Y\<in> synth H"
 by (erule synth_trans, blast)
 
 lemma Nonce_synth_eq [simp]: "(Nonce N \<in> synth H) = (Nonce N \<in> H)"
 by blast
 
 lemma Key_synth_eq [simp]: "(Key K \<in> synth H) = (Key K \<in> H)"
 by blast
 
 lemma Crypt_synth_eq [simp]:
   "Key K \<notin> H \<Longrightarrow> (Crypt K X \<in> synth H) = (Crypt K X \<in> H)"
 by blast
 
 
 lemma keysFor_synth [simp]:
   "keysFor (synth H) = keysFor H \<union> invKey`{K. Key K \<in> H}"
 by (unfold keysFor_def, blast)
 
 lemma L_cons_synth [simp]:
   "(set xs \<subseteq> H) \<Longrightarrow> (L xs \<in> synth H)"
 by auto
 
 lemma FS_cons_synth [simp]:
   "\<lbrakk>fset xs \<subseteq> H; \<And>x ys. x \<in> fset xs \<Longrightarrow> x \<noteq> FS ys; fcard xs \<noteq> Suc 0 \<rbrakk> \<Longrightarrow> (FS xs \<in> synth H)"
 by auto
 
 subsubsection \<open>Combinations of parts, analz and synth\<close>
 
 lemma parts_synth [simp]: "parts (synth H) = parts H \<union> synth H"
 proof (safe del: UnCI)
   fix X
   assume "X \<in> parts (synth H)"
   thus "X \<in> parts H \<union> synth H"
   by (induct rule: parts.induct)
      (auto intro: parts.Fst parts.Snd parts.Lst parts.FSt parts.Body)
 next
   fix X
   assume "X \<in> parts H"
   thus "X \<in> parts (synth H)"
   by (induction rule: parts.induct)
      (auto intro: parts.Fst parts.Snd  parts.Lst parts.FSt parts.Body)
 next
   fix X
   assume "X \<in> synth H"
   thus "X \<in> parts (synth H)"
     apply (induction rule: synth.induct)
     apply(auto intro: parts.Fst parts.Snd  parts.Lst parts.FSt parts.Body)
     by blast
 qed
 
 
 lemma analz_analz_Un [simp]: "analz (analz G \<union> H) = analz (G \<union> H)"
 apply (intro equalityI analz_subset_cong)+
 apply simp_all
 done
 
 lemma analz_synth_Un [simp]: "analz (synth G \<union> H) = analz (G \<union> H) \<union> synth G"
 proof (safe del: UnCI)
   fix X
   assume "X \<in> analz (synth G \<union> H)"
   thus "X \<in> analz (G \<union> H) \<union> synth G"
   by (induction rule: analz.induct)
      (auto intro: analz.Fst analz.Snd analz.Lst analz.FSt analz.Decrypt)
 qed (auto elim: analz_mono [THEN [2] rev_subsetD])
 
 lemma analz_synth [simp]: "analz (synth H) = analz H \<union> synth H"
 apply (cut_tac H = "{}" in analz_synth_Un)
 apply (simp (no_asm_use))
 done
 
 lemma analz_Un_analz [simp]: "analz (G \<union> analz H) = analz (G \<union> H)"
 by (subst Un_commute, auto)+
 
 lemma analz_synth_Un2 [simp]: "analz (G \<union> synth H) = analz (G \<union> H) \<union> synth H"
 by (subst Un_commute, auto)+
 
 
 subsubsection \<open>For reasoning about the Fake rule in traces\<close>
 
 lemma parts_insert_subset_Un: "X\<in> G \<Longrightarrow> parts(insert X H) \<subseteq> parts G \<union> parts H"
 by (rule subset_trans [OF parts_mono parts_Un_subset2], blast)
 
 text \<open>More specifically for Fake.  Very occasionally we could do with a version
   of the form  @{term"parts{X} \<subseteq> synth (analz H) \<union> parts H"}\<close>
 lemma Fake_parts_insert:
   "X \<in> synth (analz H) \<Longrightarrow>
     parts (insert X H) \<subseteq> synth (analz H) \<union> parts H"
 apply (drule parts_insert_subset_Un)
 apply (simp (no_asm_use))
 apply blast
 done
 
 lemma Fake_parts_insert_in_Un:
   "\<lbrakk>Z \<in> parts (insert X H);  X \<in> synth (analz H)\<rbrakk>
     \<Longrightarrow> Z \<in>  synth (analz H) \<union> parts H"
 by (blast dest: Fake_parts_insert  [THEN subsetD, dest])
 
 text \<open>@{term H} is sometimes @{term"Key ` KK \<union> spies evs"}, so can't put @{term "G=H"}.\<close>
 lemma Fake_analz_insert:
   "X\<in> synth (analz G) \<Longrightarrow>
     analz (insert X H) \<subseteq> synth (analz G) \<union> analz (G \<union> H)"
 apply (rule subsetI)
 apply (subgoal_tac "x \<in> analz (synth (analz G) \<union> H) ")
 prefer 2
   apply (blast intro: analz_mono [THEN [2] rev_subsetD]
                       analz_mono [THEN synth_mono, THEN [2] rev_subsetD])
 apply (simp (no_asm_use))
 apply blast
 done
 
 lemma analz_conj_parts [simp]:
   "(X \<in> analz H & X \<in> parts H) = (X \<in> analz H)"
 by (blast intro: analz_subset_parts [THEN subsetD])
 
 lemma analz_disj_parts [simp]:
   "(X \<in> analz H | X \<in> parts H) = (X \<in> parts H)"
 by (blast intro: analz_subset_parts [THEN subsetD])
 
 text \<open>Without this equation, other rules for synth and analz would yield
         redundant cases\<close>
 lemma MPair_synth_analz [iff]:
   "(\<langle>X,Y\<rangle> \<in> synth (analz H)) =
     (X \<in> synth (analz H) & Y \<in> synth (analz H))"
 by blast
 
 lemma L_cons_synth_analz [iff]:
   "(L xs \<in> synth (analz H)) =
     (set xs \<subseteq> synth (analz H))"
 by blast
 
 lemma L_cons_synth_parts [iff]:
   "(L xs \<in> synth (parts H)) =
     (set xs \<subseteq> synth (parts H))"
 by blast
 
 lemma FS_cons_synth_analz [iff]:
-  "\<lbrakk>\<And>x ys . x \<in> fset xs \<Longrightarrow> x \<noteq> FS ys; fcard xs \<noteq> Suc 0 \<rbrakk> \<Longrightarrow> 
+  "\<lbrakk>\<And>x ys . x \<in> fset xs \<Longrightarrow> x \<noteq> FS ys; fcard xs \<noteq> Suc 0 \<rbrakk> \<Longrightarrow>
     (FS xs \<in> synth (analz H)) =
     (fset xs \<subseteq> synth (analz H))"
 by blast
 
 lemma FS_cons_synth_parts [iff]:
-  "\<lbrakk>\<And>x ys . x \<in> fset xs \<Longrightarrow> x \<noteq> FS ys; fcard xs \<noteq> Suc 0 \<rbrakk> \<Longrightarrow> 
+  "\<lbrakk>\<And>x ys . x \<in> fset xs \<Longrightarrow> x \<noteq> FS ys; fcard xs \<noteq> Suc 0 \<rbrakk> \<Longrightarrow>
     (FS xs \<in> synth (parts H)) =
     (fset xs \<subseteq> synth (parts H))"
 by blast
 
 lemma Crypt_synth_analz:
   "\<lbrakk> Key K \<in> analz H;  Key (invKey K) \<in> analz H \<rbrakk>
     \<Longrightarrow> (Crypt K X \<in> synth (analz H)) = (X \<in> synth (analz H))"
 by blast
 
 lemma Hash_synth_analz [simp]:
   "X \<notin> synth (analz H)
     \<Longrightarrow> (Hash\<langle>X,Y\<rangle> \<in> synth (analz H)) = (Hash\<langle>X,Y\<rangle> \<in> analz H)"
 by blast
 
 
 subsection \<open>HPair: a combination of Hash and MPair\<close>
 
 text \<open>We do NOT want Crypt... messages broken up in protocols!!\<close>
 declare parts.Body [rule del]
 
 
 text \<open>Rewrites to push in Key and Crypt messages, so that other messages can
         be pulled out using the @{text analz_insert} rules\<close>
 
 (*needed?*)
 lemmas pushKeys =
   insert_commute [of "Key K" "AS C" for K C]
   insert_commute [of "Key K" "Nonce N" for K N]
   insert_commute [of "Key K" "Num N" for K N]
   insert_commute [of "Key K" "Hash X" for K X]
   insert_commute [of "Key K" "MPair X Y" for K X Y]
   insert_commute [of "Key K" "Crypt X K'" for K K' X]
 
 (*needed?*)
 lemmas pushCrypts =
   insert_commute [of "Crypt X K" "AS C" for X K C]
   insert_commute [of "Crypt X K" "AS C" for X K C]
   insert_commute [of "Crypt X K" "Nonce N" for X K N]
   insert_commute [of "Crypt X K" "Num N"  for X K N]
   insert_commute [of "Crypt X K" "Hash X'"  for X K X']
   insert_commute [of "Crypt X K" "MPair X' Y"  for X K X' Y]
 
 text \<open>Cannot be added with @{text "[simp]"} -- messages should not always be
         re-ordered.\<close>
 lemmas pushes = pushKeys pushCrypts
 
 text \<open>By default only @{text o_apply} is built-in.  But in the presence of
         eta-expansion this means that some terms displayed as @{term "f o g"} will be
         rewritten, and others will not!\<close>
 declare o_def [simp]
 
 
 lemma Crypt_notin_image_Key [simp]: "Crypt K X \<notin> Key ` A"
 by auto
 
 lemma Hash_notin_image_Key [simp] :"Hash X \<notin> Key ` A"
 by auto
 
 lemma synth_analz_mono: "G\<subseteq>H \<Longrightarrow> synth (analz(G)) \<subseteq> synth (analz(H))"
 by (iprover intro: synth_mono analz_mono)
 
 lemma synth_parts_mono: "G\<subseteq>H \<Longrightarrow> synth (parts G) \<subseteq> synth (parts H)"
 by (iprover intro: synth_mono parts_mono)
 
 lemma Fake_analz_eq [simp]:
   "X \<in> synth(analz H) \<Longrightarrow> synth (analz (insert X H)) = synth (analz H)"
 apply (drule Fake_analz_insert[of _ _ "H"])
 apply (simp add: synth_increasing[THEN Un_absorb2])
 apply (drule synth_mono)
 apply (simp add: synth_idem)
 apply (rule equalityI)
 apply (simp add: )
 apply (rule synth_analz_mono, blast)
 done
 
 text \<open>Two generalizations of @{text analz_insert_eq}\<close>
 lemma gen_analz_insert_eq [rule_format]:
   "X \<in> analz H \<Longrightarrow> ALL G. H \<subseteq> G --> analz (insert X G) = analz G"
 by (blast intro: analz_cut analz_insertI analz_mono [THEN [2] rev_subsetD])
 
 lemma Fake_parts_sing:
   "X \<in> synth (analz H) \<Longrightarrow> parts{X} \<subseteq> synth (analz H) \<union> parts H"
 apply (rule subset_trans)
  apply (erule_tac [2] Fake_parts_insert)
 apply (rule parts_mono, blast)
 done
 
 lemmas Fake_parts_sing_imp_Un = Fake_parts_sing [THEN [2] rev_subsetD]
 
 text \<open>For some reason, moving this up can make some proofs loop!\<close>
 declare invKey_K [simp]
 
 
 lemma synth_analz_insert:
   assumes "analz H \<subseteq> synth (analz H')"
   shows "analz (insert X H) \<subseteq> synth (analz (insert X H'))"
 proof
   fix x
   assume "x \<in> analz (insert X H)"
   then have "x \<in> analz (insert X (synth (analz H')))"
     using assms by (meson analz_increasing analz_monotonic insert_mono)
   then show "x \<in> synth (analz (insert X H'))"
-    by (metis (no_types) Un_iff analz_idem analz_insert analz_monotonic analz_synth synth.Inj 
+    by (metis (no_types) Un_iff analz_idem analz_insert analz_monotonic analz_synth synth.Inj
         synth_insert synth_mono)
 qed
 
 lemma synth_parts_insert:
   assumes "parts H \<subseteq> synth (parts H')"
   shows "parts (insert X H) \<subseteq> synth (parts (insert X H'))"
 proof
   fix x
   assume "x \<in> parts (insert X H)"
   then have "x \<in> parts (insert X (synth (parts H')))"
     using assms parts_increasing
     by (metis UnE UnI1 analz_monotonic analz_parts parts_insert parts_insertI)
   then show "x \<in> synth (parts (insert X H'))"
   using Un_iff parts_idem parts_insert parts_synth synth.Inj
   by (metis Un_subset_iff synth_increasing synth_trans)
 qed
 
 
 lemma parts_insert_subset_impl:
   "\<lbrakk>x \<in> parts (insert a G); x \<in> parts G \<Longrightarrow> x \<in> synth (parts H); a \<in> synth (parts H)\<rbrakk>
     \<Longrightarrow> x \<in> synth (parts H)"
 using Fake_parts_sing in_parts_UnE insert_is_Un
           parts_idem parts_synth subsetCE sup.absorb2 synth_idem synth_increasing
 by (metis (no_types, lifting) analz_parts)
 
 lemma synth_parts_subset_elem:
   "\<lbrakk>A \<subseteq> synth (parts B); x \<in> parts A\<rbrakk> \<Longrightarrow> x \<in> synth (parts B)"
 by (meson parts_emptyE parts_insert_subset_impl parts_singleton subset_iff)
 
 lemma synth_parts_subset:
   "A \<subseteq> synth (parts B) \<Longrightarrow> parts A \<subseteq> synth (parts B)"
 by (auto simp add: synth_parts_subset_elem)
 
 
 lemma parts_synth_parts[simp]: "parts (synth (parts H)) = synth (parts H)"
 by auto
 
 lemma synth_parts_trans:
   assumes "A \<subseteq> synth (parts B)" and "B \<subseteq> synth (parts C)"
   shows "A \<subseteq> synth (parts C)"
 using assms by (metis order_trans parts_synth_parts synth_idem synth_parts_mono)
 
 lemma synth_parts_trans_elem:
   assumes "x \<in> A" and "A \<subseteq> synth (parts B)" and "B \<subseteq> synth (parts C)"
   shows "x \<in> synth (parts C)"
 using synth_parts_trans assms by auto
 
 lemma synth_un_parts_split:
   assumes "x \<in> synth (parts A \<union> parts B)"
     and "\<And>x . x \<in> A \<Longrightarrow> x \<in> synth (parts C)"
     and "\<And>x . x \<in> B \<Longrightarrow> x \<in> synth (parts C)"
   shows "x \<in> synth (parts C)"
 proof -
   have "parts A \<subseteq> synth (parts C)" "parts B \<subseteq> synth (parts C)"
     using assms(2) assms(3) synth_parts_subset by blast+
   then have "x \<in> synth (synth (parts C) \<union> synth (parts C))" using assms(1)
     using synth_trans by auto
   then show ?thesis by auto
 qed
 
 
 subsubsection \<open>Normalization of Messages\<close>
-text\<open>Prevent FS from being contained directly in other FS. 
+text\<open>Prevent FS from being contained directly in other FS.
 For instance, a term @{term "FS {| FS {| Num 0 |}, Num 0 |}"} is
 not normalized, whereas @{term "FS {| Hash (FS {| Num 0 |}), Num 0 |}"} is normalized.\<close>
 
 
 inductive normalized :: "msgterm \<Rightarrow> bool" where
     \<epsilon>  [simp,intro!]:    "normalized \<epsilon>"
   | AS  [simp,intro!]:   "normalized (AS agt)"
   | Num [simp,intro!]:   "normalized (Num n)"
   | Key [simp,intro!]:   "normalized (Key n)"
   | Nonce [simp,intro!]:  "normalized (Nonce n)"
   | Lst [intro]:      "\<lbrakk> \<And>x . x \<in> set xs \<Longrightarrow> normalized x \<rbrakk> \<Longrightarrow> normalized (L xs)"
-  | FSt [intro]:      "\<lbrakk> \<And>x . x \<in> fset xs \<Longrightarrow> normalized x;  
-                         \<And>x ys . x \<in> fset xs \<Longrightarrow> x \<noteq> FS ys \<rbrakk> 
+  | FSt [intro]:      "\<lbrakk> \<And>x . x \<in> fset xs \<Longrightarrow> normalized x;
+                         \<And>x ys . x \<in> fset xs \<Longrightarrow> x \<noteq> FS ys \<rbrakk>
                       \<Longrightarrow> normalized (FS xs)"
   | Hash   [intro]:   "normalized X \<Longrightarrow> normalized (Hash X)"
   | MPair  [intro]:   "\<lbrakk> normalized X; normalized Y \<rbrakk> \<Longrightarrow> normalized \<langle>X,Y\<rangle>"
   | Crypt  [intro]:   "\<lbrakk> normalized X \<rbrakk> \<Longrightarrow> normalized (Crypt K X)"
 
 thm normalized.simps
 find_theorems normalized
 
 text\<open>Examples\<close>
 lemma "normalized (FS {| Hash (FS {| Num 0 |}), Num 0 |})" by fastforce
 lemma "\<not> normalized (FS {| FS {| Num 0 |}, Num 0 |})" by (auto elim: normalized.cases)
 
 
 subsubsection\<open>Closure of @{text "normalized"} under @{text "parts"}, @{text "analz"} and @{text "synth"}\<close>
 
 text\<open>All synthesized terms are normalized (since @{text "synth"} prevents directly nested FSets).\<close>
 lemma normalized_synth[elim!]: "\<lbrakk>t \<in> synth H; \<And>t. t \<in> H \<Longrightarrow> normalized t\<rbrakk> \<Longrightarrow> normalized t"
   by(induction t, auto 3 4)
 
 lemma normalized_parts[elim!]: "\<lbrakk>t \<in> parts H; \<And>t. t \<in> H \<Longrightarrow> normalized t\<rbrakk> \<Longrightarrow> normalized t"
   by(induction t rule: parts.induct)
     (auto elim: normalized.cases)
 
 lemma normalized_analz[elim!]: "\<lbrakk>t \<in> analz H; \<And>t. t \<in> H \<Longrightarrow> normalized t\<rbrakk> \<Longrightarrow> normalized t"
   by(induction t rule: analz.induct)
     (auto elim: normalized.cases)
 
 subsubsection\<open>Properties of @{text "normalized"}\<close>
 
 lemma normalized_FS[elim]: "\<lbrakk>normalized (FS xs); x |\<in>| xs\<rbrakk> \<Longrightarrow> normalized x"
   by(auto simp add: normalized.simps[of "FS xs"])
 
 lemma normalized_FS_FS[elim]: "\<lbrakk>normalized (FS xs); x |\<in>| xs; x = FS ys\<rbrakk> \<Longrightarrow> False"
   by(auto simp add: normalized.simps[of "FS xs"])
 
 lemma normalized_subset: "\<lbrakk>normalized (FS xs); ys |\<subseteq>| xs\<rbrakk> \<Longrightarrow> normalized (FS ys)"
   by (auto intro!: normalized.FSt)
 
 lemma normalized_insert[elim!]: "normalized (FS (finsert x xs)) \<Longrightarrow> normalized (FS xs)"
-  by(auto elim!: normalized_subset) 
+  by(auto elim!: normalized_subset)
 
-lemma normalized_union: 
+lemma normalized_union:
   assumes "normalized (FS xs)" "normalized (FS ys)" "zs |\<subseteq>| xs |\<union>| ys"
   shows "normalized (FS zs)"
   using assms by(auto intro!: normalized.FSt)
 
-lemma normalized_minus[elim]: 
-  assumes "normalized (FS (ys |-| xs))" "normalized (FS xs)" 
+lemma normalized_minus[elim]:
+  assumes "normalized (FS (ys |-| xs))" "normalized (FS xs)"
   shows "normalized (FS ys)"
   using normalized_union assms by blast
 
 
 subsubsection\<open>Lemmas that do not use @{text "normalized"}, but are helpful in proving its properties\<close>
 lemma FS_mono: "\<lbrakk>zs_s = finsert (f (FS zs_s)) zs_b; \<And> x. size (f x) > size x\<rbrakk> \<Longrightarrow> False"
-  by (metis (no_types) add.right_neutral add_Suc_right finite_fset finsert.rep_eq less_add_Suc1 
+  by (metis (no_types) add.right_neutral add_Suc_right finite_fset finsert.rep_eq less_add_Suc1
       msgterm.size(17) not_less_eq size_fset_simps sum.insert_remove)
 
 lemma FS_contr: "\<lbrakk>zs = f (FS {|zs|}); \<And> x. size (f x) > size x\<rbrakk> \<Longrightarrow> False"
   using FS_mono by blast
 
 
 end
diff --git a/thys/Key_Agreement_Strong_Adversaries/Message_derivation.thy b/thys/Key_Agreement_Strong_Adversaries/Message_derivation.thy
--- a/thys/Key_Agreement_Strong_Adversaries/Message_derivation.thy
+++ b/thys/Key_Agreement_Strong_Adversaries/Message_derivation.thy
@@ -1,708 +1,700 @@
 (*******************************************************************************
 
   Project: Refining Authenticated Key Agreement with Strong Adversaries
 
   Module:  Message_derivation.thy (Isabelle/HOL 2016-1)
   ID:      $Id: Message_derivation.thy 132885 2016-12-23 18:41:32Z csprenge $
   Author:  Joseph Lallemand, INRIA Nancy <joseph.lallemand@loria.fr>
            Christoph Sprenger, ETH Zurich <sprenger@inf.ethz.ch>
-  
+
   A theory of message derivations (analz, synth, parts).
   Based on Larry Paulson's theory HOL/Auth/Message.thy, but extended with
   - composed keys
   - including ephemeral asymmetric keys
   - Diffie-Hellman exponentiation and associated equational theory
 
   Copyright (c) 2015-2016 Joseph Lallemand and Christoph Sprenger
   Licence: LGPL
 
 *******************************************************************************)
 
-section \<open>Message theory\<close> 
+section \<open>Message theory\<close>
 
 theory Message_derivation
 imports Messages
 begin
 
 text \<open>This theory is adapted from Larry Paulson's original Message theory.\<close>
 
 
 (****************************************************************************************)
 subsection \<open>Message composition\<close>
 (****************************************************************************************)
 
 text \<open>Dolev-Yao message synthesis.\<close>
 
 inductive_set
-  synth :: "msg set \<Rightarrow> msg set"   
+  synth :: "msg set \<Rightarrow> msg set"
   for H :: "msg set"
   where
     Ax [intro]: "X \<in> H \<Longrightarrow> X \<in> synth H"
   | Agent [simp, intro]: "Agent A \<in> synth H"
   | Number [simp, intro]: "Number n \<in> synth H"
   | NonceA [simp, intro]: "NonceA n \<in> synth H"
   | EpubKA [simp, intro]: "epubKA n \<in> synth H"
   | EpriKA [simp, intro]: "epriKA n \<in> synth H"
   | Hash [intro]: "X \<in> synth H \<Longrightarrow> Hash X \<in> synth H"
   | Pair [intro]: "X \<in> synth H \<Longrightarrow> Y \<in> synth H \<Longrightarrow> (Pair X Y) \<in> synth H"
   | Enc [intro]: "X \<in> synth H \<Longrightarrow> Y \<in> synth H \<Longrightarrow> (Enc X Y) \<in> synth H"
   | Aenc [intro]: "X \<in> synth H \<Longrightarrow> Y \<in> synth H \<Longrightarrow> (Aenc X Y) \<in> synth H"
   | Sign [intro]: "X \<in> synth H \<Longrightarrow> Y \<in> synth H \<Longrightarrow> Sign X Y \<in> synth H"
   | Exp [intro]: "X \<in> synth H \<Longrightarrow> Y \<in> synth H \<Longrightarrow> (Exp X Y) \<in> synth H"
 
 
 text \<open>Lemmas about Dolev-Yao message synthesis.\<close>
 
 lemma synth_mono [mono_set]: "G \<subseteq> H \<Longrightarrow> synth G \<subseteq> synth H"
-  by (auto, erule synth.induct, auto) 
+  by (auto, erule synth.induct, auto)
 
 lemmas synth_monotone = synth_mono [THEN [2] rev_subsetD]
 
 \<comment> \<open>\<open>[elim!]\<close> slows down certain proofs, e.g., \<open>\<lbrakk> synth H \<inter> B \<subseteq> {} \<rbrakk> \<Longrightarrow> P\<close>\<close>
 inductive_cases NonceF_synth: "NonceF n \<in> synth H"
 inductive_cases LtK_synth: "LtK K \<in> synth H"
 inductive_cases EpubKF_synth: "epubKF K \<in> synth H"
 inductive_cases EpriKF_synth: "epriKF K \<in> synth H"
 inductive_cases Hash_synth: "Hash X \<in> synth H"
 inductive_cases Pair_synth: "Pair X Y \<in> synth H"
 inductive_cases Enc_synth: "Enc X K \<in> synth H"
 inductive_cases Aenc_synth: "Aenc X K \<in> synth H"
 inductive_cases Sign_synth: "Sign X K \<in> synth H"
 inductive_cases Tag_synth: "Tag t \<in> synth H"
 
 lemma EpriK_synth [elim]: "epriK K \<in> synth H \<Longrightarrow>
        epriK K \<in> H \<or> (\<exists> N. epriK K = epriKA N)"
 by (cases K, auto elim: EpriKF_synth)
 
 lemma EpubK_synth [elim]: "epubK K \<in> synth H \<Longrightarrow>
        epubK K \<in> H \<or> (\<exists> N. epubK K = epubKA N)"
 by (cases K, auto elim: EpubKF_synth)
 
-lemmas synth_inversion [elim] = 
-  NonceF_synth LtK_synth EpubKF_synth EpriKF_synth Hash_synth Pair_synth 
+lemmas synth_inversion [elim] =
+  NonceF_synth LtK_synth EpubKF_synth EpriKF_synth Hash_synth Pair_synth
   Enc_synth Aenc_synth Sign_synth Tag_synth
 
 
 lemma synth_increasing: "H \<subseteq> synth H"
 by blast
 
 lemma synth_Int1: "x \<in> synth (A \<inter> B) \<Longrightarrow> x \<in> synth A "
   by (erule synth.induct) (auto)
 
 lemma synth_Int2: "x \<in> synth (A \<inter> B) \<Longrightarrow> x \<in> synth B"
   by (erule synth.induct) (auto)
 
 lemma synth_Int: "x \<in> synth (A \<inter> B) \<Longrightarrow> x \<in> synth A \<inter> synth B"
   by (blast intro: synth_Int1 synth_Int2)
 
 lemma synth_Un: "synth G \<union> synth H \<subseteq> synth (G \<union> H)"
 by (intro Un_least synth_mono Un_upper1 Un_upper2)
 
 lemma synth_insert: "insert X (synth H) \<subseteq> synth (insert X H)"
 by (blast intro: synth_mono [THEN [2] rev_subsetD])
 
 lemma synth_synthD [dest!]: "X \<in> synth (synth H) \<Longrightarrow> X \<in> synth H"
 by (erule synth.induct, blast+)
 
 lemma synth_idem [simp]: "synth (synth H) = synth H"
 by blast
 
 lemma synth_subset_iff: "synth G \<subseteq> synth H \<longleftrightarrow> G \<subseteq> synth H"
 by (blast dest: synth_mono)
 
 lemma synth_trans: "\<lbrakk> X \<in> synth G; G \<subseteq> synth H \<rbrakk> \<Longrightarrow> X \<in> synth H"
 by (drule synth_mono, blast)
 
 lemma synth_cut: "\<lbrakk> Y \<in> synth (insert X H); X \<in> synth H \<rbrakk> \<Longrightarrow> Y \<in> synth H"
 by (erule synth_trans, blast)
 
 
 lemma Nonce_synth_eq [simp]: "(NonceF N \<in> synth H) = (NonceF N \<in> H)"
 by blast
 
 lemma LtK_synth_eq [simp]: "(LtK K \<in> synth H) = (LtK K \<in> H)"
 by blast
 
 lemma EpubKF_synth_eq [simp]: "(epubKF K \<in> synth H) = (epubKF K \<in> H)"
 by blast
 
 lemma EpriKF_synth_eq [simp]: "(epriKF K \<in> synth H) = (epriKF K \<in> H)"
 by blast
 
 lemma Enc_synth_eq1 [simp]:
      "K \<notin> synth H \<Longrightarrow> (Enc X K \<in> synth H) = (Enc X K \<in> H)"
 by blast
 
 lemma Enc_synth_eq2 [simp]:
      "X \<notin> synth H \<Longrightarrow> (Enc X K \<in> synth H) = (Enc X K \<in> H)"
 by blast
 
 lemma Aenc_synth_eq1 [simp]:
      "K \<notin> synth H \<Longrightarrow> (Aenc X K \<in> synth H) = (Aenc X K \<in> H)"
 by blast
 
 lemma Aenc_synth_eq2 [simp]:
      "X \<notin> synth H \<Longrightarrow> (Aenc X K \<in> synth H) = (Aenc X K \<in> H)"
 by blast
 
 lemma Sign_synth_eq1 [simp]:
      "K \<notin> synth H \<Longrightarrow> (Sign X K \<in> synth H) = (Sign X K \<in> H)"
 by blast
 
 lemma Sign_synth_eq2 [simp]:
      "X \<notin> synth H \<Longrightarrow> (Sign X K \<in> synth H) = (Sign X K \<in> H)"
 by blast
 
 (****************************************************************************************)
 subsection \<open>Message decomposition\<close>
 (****************************************************************************************)
 
 text \<open>Dolev-Yao message decomposition using known keys.\<close>
 
 inductive_set
   analz :: "msg set \<Rightarrow> msg set"
   for H :: "msg set"
   where
     Ax [intro]: "X \<in> H \<Longrightarrow> X \<in> analz H"
   | Fst: "Pair X Y \<in> analz H \<Longrightarrow> X \<in> analz H"
   | Snd: "Pair X Y \<in> analz H \<Longrightarrow> Y \<in> analz H"
-  | Dec [dest]: 
+  | Dec [dest]:
       "\<lbrakk> Enc X Y \<in> analz H; Y \<in> synth (analz H) \<rbrakk> \<Longrightarrow> X \<in> analz H"
-  | Adec_lt [dest]: 
+  | Adec_lt [dest]:
       "\<lbrakk> Aenc X (LtK (publK Y)) \<in> analz H; priK Y \<in> analz H \<rbrakk> \<Longrightarrow> X \<in> analz H"
-  | Adec_eph [dest]: 
+  | Adec_eph [dest]:
       "\<lbrakk> Aenc X (EphK (epublK Y)) \<in> analz H; epriK Y \<in> synth (analz H) \<rbrakk> \<Longrightarrow> X \<in> analz H"
-  | Sign_getmsg [dest]: 
+  | Sign_getmsg [dest]:
       "Sign X (priK Y) \<in> analz H \<Longrightarrow> pubK Y \<in> analz H \<Longrightarrow> X \<in> analz H"
 
 
 text \<open>Lemmas about Dolev-Yao message decomposition.\<close>
 
 lemma analz_mono: "G \<subseteq> H \<Longrightarrow> analz(G) \<subseteq> analz(H)"
 by (safe, erule analz.induct) (auto dest: Fst Snd synth_Int2)
 
 lemmas analz_monotone = analz_mono [THEN [2] rev_subsetD]
 
 
 lemma Pair_analz [elim!]:
   "\<lbrakk> Pair X Y \<in> analz H; \<lbrakk> X \<in> analz H; Y \<in> analz H \<rbrakk> \<Longrightarrow> P \<rbrakk> \<Longrightarrow> P"
 by (blast dest: analz.Fst analz.Snd)
 
 
 lemma analz_empty [simp]: "analz {} = {}"
 by (safe, erule analz.induct) (blast+)
 
 lemma analz_increasing: "H \<subseteq> analz(H)"
 by auto
 
 lemma analz_analzD [dest!]: "X \<in> analz (analz H) \<Longrightarrow> X \<in> analz H"
 by (induction X rule: analz.induct) (auto dest: synth_monotone)
 
 lemma analz_idem [simp]: "analz (analz H) = analz H"
 by auto
 
 
 lemma analz_Un: "analz G \<union> analz H \<subseteq> analz (G \<union> H)"
 by (intro Un_least analz_mono Un_upper1 Un_upper2)
 
 lemma analz_insertI: "X \<in> analz H \<Longrightarrow> X \<in> analz (insert Y H)"
 by (blast intro: analz_monotone)
 
 lemma analz_insert: "insert X (analz H) \<subseteq> analz (insert X H)"
 by (blast intro: analz_monotone)
 
 lemmas analz_insert_eq_I = equalityI [OF subsetI analz_insert]
 
 
 lemma analz_subset_iff [simp]: "analz G \<subseteq> analz H \<longleftrightarrow> G \<subseteq> analz H"
 by (blast dest: analz_mono)
 
 lemma analz_trans: "X \<in> analz G \<Longrightarrow>  G \<subseteq> analz H \<Longrightarrow> X \<in> analz H"
 by (drule analz_mono) blast
 
 lemma analz_cut: "Y \<in> analz (insert X H) \<Longrightarrow>  X \<in> analz H \<Longrightarrow> Y \<in> analz H"
 by (erule analz_trans) blast
 
 lemma analz_insert_eq: "X \<in> analz H \<Longrightarrow> analz (insert X H) = analz H"
 by (blast intro: analz_cut analz_insertI)
 
 
 lemma analz_subset_cong:
   "analz G \<subseteq> analz G' \<Longrightarrow>
-   analz H \<subseteq> analz H' \<Longrightarrow> 
+   analz H \<subseteq> analz H' \<Longrightarrow>
    analz (G \<union> H) \<subseteq> analz (G' \<union> H')"
 apply simp
-apply (iprover intro: conjI subset_trans analz_mono Un_upper1 Un_upper2) 
+apply (iprover intro: conjI subset_trans analz_mono Un_upper1 Un_upper2)
 done
 
 lemma analz_cong:
   "analz G = analz G' \<Longrightarrow>
    analz H = analz H' \<Longrightarrow>
    analz (G \<union> H) = analz (G' \<union> H')"
-by (intro equalityI analz_subset_cong, simp_all) 
+by (intro equalityI analz_subset_cong, simp_all)
 
 lemma analz_insert_cong:
   "analz H = analz H' \<Longrightarrow>
    analz (insert X H) = analz (insert X H')"
 by (force simp only: insert_def intro!: analz_cong)
 
 lemma analz_trivial:
   "\<forall>X Y. Pair X Y \<notin> H \<Longrightarrow>
    \<forall>X Y. Enc X Y \<notin> H \<Longrightarrow>
    \<forall>X Y. Aenc X Y \<notin> H \<Longrightarrow>
    \<forall>X Y. Sign X Y \<notin> H \<Longrightarrow>
    analz H = H"
 apply safe
 apply (erule analz.induct, blast+)
 done
 
 
 lemma analz_analz_Un [simp]: "analz (analz G \<union> H) = analz (G \<union> H)"
 apply (intro equalityI analz_subset_cong)+
 apply simp_all
 done
 
 lemma analz_Un_analz [simp]: "analz (G \<union> analz H) = analz (G \<union> H)"
 by (subst Un_commute, auto)+
 
 
-text \<open>Lemmas about analz and insert.\<close> 
+text \<open>Lemmas about analz and insert.\<close>
 
 lemma analz_insert_Agent [simp]:
   "analz (insert (Agent A) H) = insert (Agent A) (analz H)"
-apply (rule analz_insert_eq_I) 
+apply (rule analz_insert_eq_I)
 apply (erule analz.induct)
 thm analz.induct
 apply fastforce
 apply fastforce
 apply fastforce
 defer 1
 apply fastforce
 defer 1
 apply fastforce
 
 apply (rename_tac x X Y)
 apply (subgoal_tac "Y \<in> synth (analz H)", auto)
 apply (thin_tac "Enc X Y \<in> Z" for Z)+
 apply (drule synth_Int2, auto)
 apply (erule synth.induct, auto)
 
 apply (rename_tac X Y)
 apply (subgoal_tac "epriK Y \<in> synth (analz H)", auto)
 apply (thin_tac "Aenc X (epubK Y) \<in> Z" for Z)+
 apply (erule synth.induct, auto)
 done
 
 
 
 (****************************************************************************************)
 subsection \<open>Lemmas about combined composition/decomposition\<close>
 (****************************************************************************************)
 
 lemma synth_analz_incr: "H \<subseteq> synth (analz H)"
 by auto
 
-lemmas synth_analz_increasing = synth_analz_incr [THEN [2] rev_subsetD] 
+lemmas synth_analz_increasing = synth_analz_incr [THEN [2] rev_subsetD]
 
 lemma synth_analz_mono: "G \<subseteq> H \<Longrightarrow> synth (analz G) \<subseteq> synth (analz H)"
 by (blast intro!: analz_mono synth_mono)
 
 lemmas synth_analz_monotone = synth_analz_mono [THEN [2] rev_subsetD]
 
-lemma lem1: 
-  "Y \<in> synth (analz (synth G \<union> H) \<inter> (analz (G \<union> H) \<union> synth G)) 
+lemma lem1:
+  "Y \<in> synth (analz (synth G \<union> H) \<inter> (analz (G \<union> H) \<union> synth G))
 \<Longrightarrow> Y \<in> synth (analz (G \<union> H))"
 apply (rule subsetD, auto simp add: synth_subset_iff intro: analz_increasing synth_monotone)
 done
 
 lemma lem2: "{a. a \<in> analz (G \<union> H) \<or> a \<in> synth G} = analz (G \<union> H) \<union> synth G" by auto
 
 lemma analz_synth_Un: "analz (synth G \<union> H) = analz (G \<union> H) \<union> synth G"
 proof (intro equalityI subsetI)
   fix x
-  assume "x \<in> analz (synth G \<union> H)" 
+  assume "x \<in> analz (synth G \<union> H)"
   thus "x \<in> analz (G \<union> H) \<union> synth G"
   by (induction x rule: analz.induct)
-     (auto simp add: lem2 intro: analz_monotone Fst Snd Dec Adec_eph Adec_lt Sign_getmsg 
+     (auto simp add: lem2 intro: analz_monotone Fst Snd Dec Adec_eph Adec_lt Sign_getmsg
            dest: lem1)
-next 
+next
   fix x
-  assume "x \<in> analz (G \<union> H) \<union> synth G" 
-  thus "x \<in> analz (synth G \<union> H)" 
-    by (blast intro: analz_monotone) 
+  assume "x \<in> analz (G \<union> H) \<union> synth G"
+  thus "x \<in> analz (synth G \<union> H)"
+    by (blast intro: analz_monotone)
 qed
 
 
 lemma analz_synth: "analz (synth H) = analz H \<union> synth H"
 by (rule analz_synth_Un [where H="{}", simplified])
 
 
 lemma analz_synth_Un2 [simp]: "analz (G \<union> synth H) = analz (G \<union> H) \<union> synth H"
 by (subst Un_commute, auto simp add: analz_synth_Un)+
 
 
 lemma synth_analz_synth [simp]: "synth (analz (synth H)) = synth (analz H)"
 by (auto del:subsetI) (auto simp add: synth_subset_iff analz_synth)
 
 lemma analz_synth_analz [simp]: "analz (synth (analz H)) = synth (analz H)"
 by (auto simp add: analz_synth)
 
 lemma synth_analz_idem [simp]: "synth (analz (synth (analz H))) = synth (analz H)"
 by (simp only: analz_synth_analz) simp
 
 
-lemma insert_subset_synth_analz [simp]: 
+lemma insert_subset_synth_analz [simp]:
   "X \<in> synth (analz H) \<Longrightarrow> insert X H \<subseteq> synth (analz H)"
 by auto
 
 
-lemma synth_analz_insert [simp]: 
+lemma synth_analz_insert [simp]:
   assumes "X \<in> synth (analz H)"
   shows "synth (analz (insert X H)) = synth (analz H)"
 using assms
 proof (intro equalityI subsetI)
   fix Z
   assume "Z \<in> synth (analz (insert X H))"
-  hence "Z \<in> synth (analz (synth (analz H)))" using assms 
+  hence "Z \<in> synth (analz (synth (analz H)))" using assms
     by - (erule synth_analz_monotone, rule insert_subset_synth_analz)
   thus "Z \<in> synth (analz H)" using assms by simp
 qed (auto intro: synth_analz_monotone)
 
 
 (****************************************************************************************)
 subsection \<open>Accessible message parts\<close>
 (****************************************************************************************)
 
 text \<open>Accessible message parts: all subterms that are in principle extractable
 by the Dolev-Yao attacker, i.e., provided he knows all keys. Note that keys in
 key positions and messages under hashes are not message parts in this sense.\<close>
 
 inductive_set
   parts :: "msg set => msg set"
   for H :: "msg set"
 where
     Inj [intro]: "X \<in> H \<Longrightarrow> X \<in> parts H"
   | Fst [intro]: "Pair X Y \<in> parts H \<Longrightarrow> X \<in> parts H"
   | Snd [intro]: "Pair X Y \<in> parts H \<Longrightarrow> Y \<in> parts H"
   | Dec [intro]: "Enc X Y \<in> parts H \<Longrightarrow> X \<in> parts H"
   | Adec [intro]: "Aenc X Y \<in> parts H \<Longrightarrow> X \<in> parts H"
   | Sign_getmsg [intro]: "Sign X Y \<in> parts H \<Longrightarrow> X \<in> parts H"
 
 
 text \<open>Lemmas about accessible message parts.\<close>
 
 lemma parts_mono [mono_set]: "G \<subseteq> H \<Longrightarrow> parts G \<subseteq> parts H"
 by (auto, erule parts.induct, auto)
 
 lemmas parts_monotone = parts_mono [THEN [2] rev_subsetD]
 
 
 lemma Pair_parts [elim]:
   "\<lbrakk> Pair X Y \<in> parts H; \<lbrakk> X \<in> parts H; Y \<in> parts H \<rbrakk> \<Longrightarrow> P \<rbrakk> \<Longrightarrow> P"
-by blast 
+by blast
 
 
 lemma parts_increasing: "H \<subseteq> parts H"
 by blast
 
 lemmas parts_insertI = subset_insertI [THEN parts_mono, THEN subsetD]
 
 lemma parts_empty [simp]: "parts {} = {}"
 by (safe, erule parts.induct, auto)
 
 lemma parts_atomic [simp]: "atomic x \<Longrightarrow> parts {x} = {x}"
 by (auto, erule parts.induct, auto)
- 
-lemma parts_InsecTag [simp]: "parts {Tag t} = {Tag t}" 
+
+lemma parts_InsecTag [simp]: "parts {Tag t} = {Tag t}"
 by (safe, erule parts.induct) (auto)
 
 lemma parts_emptyE [elim!]: "X \<in> parts {} \<Longrightarrow> P"
 by simp
 
 lemma parts_Tags [simp]:
   "parts Tags = Tags"
-by (rule, rule, erule parts.induct, auto) 
+by (rule, rule, erule parts.induct, auto)
 
 lemma parts_singleton: "X \<in> parts H \<Longrightarrow> \<exists> Y\<in>H. X \<in> parts {Y}"
 by (erule parts.induct, blast+)
 
 lemma parts_Agents [simp]:
   "parts (Agent` G) = Agent` G"
 by (auto elim: parts.induct)
 
 lemma parts_Un [simp]: "parts (G \<union> H) = parts G \<union> parts H"
-proof 
+proof
   show "parts (G \<union> H) \<subseteq> parts G \<union> parts H"
     by (rule, erule parts.induct) (auto)
-next 
-  show "parts G \<union> parts H \<subseteq> parts (G \<union> H)" 
+next
+  show "parts G \<union> parts H \<subseteq> parts (G \<union> H)"
     by (intro Un_least parts_mono Un_upper1 Un_upper2)
-qed 
+qed
 
-lemma parts_insert_subset_Un: 
-  assumes "X \<in> G" 
+lemma parts_insert_subset_Un:
+  assumes "X \<in> G"
   shows "parts (insert X H) \<subseteq> parts G \<union> parts H"
 proof -
-  from assms have "parts (insert X H) \<subseteq> parts (G \<union> H)" by (blast intro!: parts_mono) 
+  from assms have "parts (insert X H) \<subseteq> parts (G \<union> H)" by (blast intro!: parts_mono)
   thus ?thesis by simp
-qed 
+qed
 
 lemma parts_insert: "parts (insert X H) = parts {X} \<union> parts H"
 by (blast intro!: parts_insert_subset_Un intro: parts_monotone)
 
 lemma parts_insert2:
   "parts (insert X (insert Y H)) = parts {X} \<union> parts {Y} \<union> parts H"
 apply (simp add: Un_assoc)
 apply (simp add: parts_insert [symmetric])
 done
 
 
-lemma parts_UN [simp]: "parts (\<Union>x\<in>A. H x) = (\<Union>x\<in>A. parts(H x))" (is "?X = ?Y")
-proof 
-  show "?X \<subseteq> ?Y" by (rule subsetI, erule parts.induct) (blast+)
-next 
-  show "?Y \<subseteq> ?X" by (intro UN_least parts_mono UN_upper)
-qed
-
-
-lemmas in_parts_UnE [elim!] = parts_Un [THEN equalityD1, THEN subsetD, THEN UnE] 
+lemmas in_parts_UnE [elim!] = parts_Un [THEN equalityD1, THEN subsetD, THEN UnE]
 
 
 lemma parts_insert_subset: "insert X (parts H) \<subseteq> parts (insert X H)"
 by (blast intro: parts_mono [THEN [2] rev_subsetD])
 
 
 lemma parts_partsD [dest!]: "X \<in> parts (parts H) \<Longrightarrow> X \<in> parts H"
 by (erule parts.induct, blast+)
 
 lemma parts_idem [simp]: "parts (parts H) = parts H"
 by blast
 
 lemma parts_subset_iff [simp]: "(parts G \<subseteq> parts H) \<longleftrightarrow> (G \<subseteq> parts H)"
 by (blast dest: parts_mono)
 
 lemma parts_trans: "X \<in> parts G \<Longrightarrow>  G \<subseteq> parts H \<Longrightarrow> X \<in> parts H"
 by (drule parts_mono, blast)
 
 
 lemma parts_cut:
-  "Y \<in> parts (insert X G) \<Longrightarrow>  X \<in> parts H \<Longrightarrow> Y \<in> parts (G \<union> H)" 
+  "Y \<in> parts (insert X G) \<Longrightarrow>  X \<in> parts H \<Longrightarrow> Y \<in> parts (G \<union> H)"
 by (blast intro: parts_trans)
 
 
 lemma parts_cut_eq [simp]: "X \<in> parts H \<Longrightarrow> parts (insert X H) = parts H"
 by (force dest!: parts_cut intro: parts_insertI)
 
 
 lemmas parts_insert_eq_I = equalityI [OF subsetI parts_insert_subset]
 
 
 lemma parts_insert_Agent [simp]:
   "parts (insert (Agent agt) H) = insert (Agent agt) (parts H)"
 by (rule parts_insert_eq_I, erule parts.induct, auto)
 
 lemma parts_insert_Nonce [simp]:
   "parts (insert (Nonce N) H) = insert (Nonce N) (parts H)"
 by (rule parts_insert_eq_I, erule parts.induct, auto)
 
 lemma parts_insert_Number [simp]:
   "parts (insert (Number N) H) = insert (Number N) (parts H)"
 by (rule parts_insert_eq_I, erule parts.induct, auto)
 
 lemma parts_insert_LtK [simp]:
   "parts (insert (LtK K) H) = insert (LtK K) (parts H)"
 by (rule parts_insert_eq_I, erule parts.induct, auto)
 
 lemma parts_insert_Hash [simp]:
   "parts (insert (Hash X) H) = insert (Hash X) (parts H)"
 by (rule parts_insert_eq_I, erule parts.induct, auto)
 
 
 lemma parts_insert_Enc [simp]:
   "parts (insert (Enc X Y) H) = insert (Enc X Y) (parts {X} \<union> parts H)"
 apply (rule equalityI)
 apply (rule subsetI)
 apply (erule parts.induct, auto)
 done
 
 lemma parts_insert_Aenc [simp]:
   "parts (insert (Aenc X Y) H) = insert (Aenc X Y) (parts {X} \<union> parts H)"
 apply (rule equalityI)
 apply (rule subsetI)
 apply (erule parts.induct, auto)
 done
 
 lemma parts_insert_Sign [simp]:
   "parts (insert (Sign X Y) H) = insert (Sign X Y) (parts {X} \<union> parts H)"
 apply (rule equalityI)
 apply (rule subsetI)
 apply (erule parts.induct, auto)
 done
 
 lemma parts_insert_Pair [simp]:
   "parts (insert (Pair X Y) H) = insert (Pair X Y) (parts {X} \<union> parts {Y} \<union> parts H)"
 apply (rule equalityI)
 apply (rule subsetI)
 apply (erule parts.induct, auto)
 done
 
 
 subsubsection \<open>Lemmas about combinations with composition and decomposition\<close>
 (****************************************************************************************)
 
 lemma analz_subset_parts: "analz H \<subseteq> parts H"
 apply (rule subsetI)
 apply (erule analz.induct, blast+)
 done
 
 lemmas analz_into_parts [simp] = analz_subset_parts [THEN subsetD]
 
 lemmas not_parts_not_analz = analz_subset_parts [THEN contra_subsetD]
 
 
 lemma parts_analz [simp]: "parts (analz H) = parts H"
 apply (rule equalityI)
 apply (rule analz_subset_parts [THEN parts_mono, THEN subset_trans], simp)
 apply (blast intro: analz_increasing [THEN parts_mono, THEN subsetD])
 done
 
 lemma analz_parts [simp]: "analz (parts H) = parts H"
 apply auto
 apply (erule analz.induct, auto)
 done
 
 
 lemma parts_synth [simp]: "parts (synth H) = parts H \<union> synth H"
 apply (rule equalityI)
 apply (rule subsetI)
 apply (erule parts.induct)
 apply (blast intro: synth_increasing [THEN parts_mono, THEN subsetD] )+
 done
 
 lemma Fake_parts_insert:
   "X \<in> synth (analz H) \<Longrightarrow> parts (insert X H) \<subseteq> synth (analz H) \<union> parts H"
 apply (drule parts_insert_subset_Un)
 apply (simp (no_asm_use))
 apply blast
 done
 
 lemma Fake_parts_insert_in_Un:
   "Z \<in> parts (insert X H) \<Longrightarrow>
    X \<in> synth (analz H) \<Longrightarrow>
    Z \<in>  synth (analz H) \<union> parts H"
 by (blast dest: Fake_parts_insert [THEN subsetD, dest])
 
 
 lemma analz_conj_parts [simp]:
   "X \<in> analz H \<and> X \<in> parts H \<longleftrightarrow> X \<in> analz H"
 by (blast intro: analz_subset_parts [THEN subsetD])
 
 lemma analz_disj_parts [simp]:
   "X \<in> analz H \<or> X \<in> parts H \<longleftrightarrow> X \<in> parts H"
 by (blast intro: analz_subset_parts [THEN subsetD])
 
 
 (****************************************************************************************)
 subsection \<open>More lemmas about combinations of closures\<close>
 (****************************************************************************************)
 
 text \<open>Combinations of @{term synth} and @{term analz}.\<close>
 
 lemma Pair_synth_analz [simp]:
   "Pair X Y \<in> synth (analz H) \<longleftrightarrow> X \<in> synth (analz H) \<and> Y \<in> synth (analz H)"
 by blast
 
 lemma Enc_synth_analz:
   "Y \<in> synth (analz H) \<Longrightarrow>
    (Enc X Y \<in> synth (analz H)) \<longleftrightarrow> (X \<in> synth (analz H))"
 by blast
 
 lemma Hash_synth_analz [simp]:
   "X \<notin> synth (analz H) \<Longrightarrow>
    (Hash (Pair X Y) \<in> synth (analz H)) \<longleftrightarrow> (Hash (Pair X Y) \<in> analz H)"
 by blast
 
 
 lemma gen_analz_insert_eq:
   "\<lbrakk> X \<in> analz G; G \<subseteq> H \<rbrakk> \<Longrightarrow> analz (insert X H) = analz H"
 by (blast intro: analz_cut analz_insertI analz_monotone)
 
 lemma synth_analz_insert_eq:
   "\<lbrakk> X \<in> synth (analz G); G \<subseteq> H \<rbrakk> \<Longrightarrow> synth (analz (insert X H)) = synth (analz H)"
 by (blast intro!: synth_analz_insert synth_analz_monotone)
 
 lemma Fake_parts_sing:
   "X \<in> synth (analz H) \<Longrightarrow> parts {X} \<subseteq> synth (analz H) \<union> parts H"
 apply (rule subset_trans)
 apply (erule_tac [2] Fake_parts_insert)
 apply (rule parts_mono, blast)
 done
 
 lemmas Fake_parts_sing_imp_Un = Fake_parts_sing [THEN [2] rev_subsetD]
 
 
-lemma analz_hash_nonce [simp]: 
+lemma analz_hash_nonce [simp]:
   "analz {M. \<exists>N. M = Hash (Nonce N)} = {M. \<exists>N. M = Hash (Nonce N)}"
 by (auto, rule analz.induct, auto)
 
-lemma synth_analz_hash_nonce [simp]: 
+lemma synth_analz_hash_nonce [simp]:
   "NonceF N \<notin> synth (analz {M. \<exists>N. M = Hash (Nonce N)})"
 by auto
 
 lemma synth_analz_idem_mono:
   "S \<subseteq> synth (analz S') \<Longrightarrow> synth (analz S) \<subseteq> synth (analz S')"
 by (frule synth_analz_mono, auto)
 
 lemmas synth_analz_idem_monoI =
   synth_analz_idem_mono [THEN [2] rev_subsetD]
 
 
 
 lemma analz_synth_subset:
   "analz X \<subseteq> synth (analz X') \<Longrightarrow>
    analz Y \<subseteq> synth (analz Y') \<Longrightarrow>
    analz (X \<union> Y) \<subseteq> synth (analz (X' \<union> Y'))"
 proof -
   assume "analz X \<subseteq> synth (analz X')"
   then have HX:"analz X \<subseteq> analz (synth (analz X'))" by blast
   assume "analz Y \<subseteq> synth (analz Y')"
   then have HY:"analz Y \<subseteq> analz (synth (analz Y'))" by blast
-  from analz_subset_cong [OF HX HY] 
+  from analz_subset_cong [OF HX HY]
   have "analz (X \<union> Y) \<subseteq> analz (synth (analz X') \<union> synth (analz Y'))"
     by blast
   also have "... \<subseteq> analz (synth (analz X' \<union> analz Y'))"
     by (intro analz_mono synth_Un)
   also have "... \<subseteq> analz (synth (analz (X' \<union> Y')))"
     by (intro synth_mono analz_mono analz_Un)
   also have "... \<subseteq> synth (analz (X' \<union> Y'))"
     by auto
   finally show "analz (X \<union> Y) \<subseteq> synth (analz (X' \<union> Y'))"
     by auto
 qed
 
 
 lemma analz_synth_subset_Un1 :
   "analz X \<subseteq> synth (analz X') \<Longrightarrow> analz (X \<union> Y) \<subseteq> synth (analz (X' \<union> Y))"
 using analz_synth_subset by blast
 
 lemma analz_synth_subset_Un2 :
   "analz X \<subseteq> synth (analz X') \<Longrightarrow> analz (Y \<union> X) \<subseteq> synth (analz (Y \<union> X'))"
 using analz_synth_subset by blast
 
 lemma analz_synth_insert:
   "analz X \<subseteq> synth (analz X') \<Longrightarrow> analz (insert Y X) \<subseteq> synth (analz (insert Y X'))"
 by (metis analz_synth_subset_Un2 insert_def)
 
 lemma Fake_analz_insert_Un:
-  assumes "Y \<in> analz (insert X H)" and "X \<in> synth (analz G)" 
+  assumes "Y \<in> analz (insert X H)" and "X \<in> synth (analz G)"
   shows "Y \<in> synth (analz G) \<union> analz (G \<union> H)"
 proof -
   from assms have "Y \<in> analz (synth (analz G) \<union> H)"
-    by (blast intro: analz_mono [THEN [2] rev_subsetD] 
+    by (blast intro: analz_mono [THEN [2] rev_subsetD]
                      analz_mono [THEN synth_mono, THEN [2] rev_subsetD])
-  thus ?thesis by (simp add: sup.commute) 
+  thus ?thesis by (simp add: sup.commute)
 qed
 
 
 
 end
diff --git a/thys/Security_Protocol_Refinement/Refinement/Message.thy b/thys/Security_Protocol_Refinement/Refinement/Message.thy
--- a/thys/Security_Protocol_Refinement/Refinement/Message.thy
+++ b/thys/Security_Protocol_Refinement/Refinement/Message.thy
@@ -1,878 +1,866 @@
 (*******************************************************************************
 
   Title:      HOL/Auth/Message
   Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
   Copyright   1996  University of Cambridge
 
   Datatypes of agents and messages;
   Inductive relations "parts", "analz" and "synth"
 
 ********************************************************************************
 
   Module:  Refinement/Message.thy (Isabelle/HOL 2016-1)
   ID:      $Id: Message.thy 133856 2017-03-20 18:05:54Z csprenge $
   Edited:  Christoph Sprenger <sprenger@inf.ethz.ch>, ETH Zurich
 
   Integrated and adapted for security protocol refinement
 
 *******************************************************************************)
 
 section \<open>Theory of Agents and Messages for Security Protocols\<close>
 
 theory Message imports Keys begin
 
 (*Needed occasionally with spy_analz_tac, e.g. in analz_insert_Key_newK*)
 lemma Un_idem_collapse [simp]: "A \<union> (B \<union> A) = B \<union> A"
 by blast
 
 datatype
      msg = Agent  agent     \<comment> \<open>Agent names\<close>
          | Number nat       \<comment> \<open>Ordinary integers, timestamps, ...\<close>
          | Nonce  nonce     \<comment> \<open>Unguessable nonces\<close>
          | Key    key       \<comment> \<open>Crypto keys\<close>
          | Hash   msg       \<comment> \<open>Hashing\<close>
          | MPair  msg msg   \<comment> \<open>Compound messages\<close>
          | Crypt  key msg   \<comment> \<open>Encryption, public- or shared-key\<close>
 
 
 text\<open>Concrete syntax: messages appear as \<open>\<lbrace>A,B,NA\<rbrace>\<close>, etc...\<close>
 
 syntax
   "_MTuple"      :: "['a, args] => 'a * 'b"       ("(2\<lbrace>_,/ _\<rbrace>)")
 translations
   "\<lbrace>x, y, z\<rbrace>"   == "\<lbrace>x, \<lbrace>y, z\<rbrace>\<rbrace>"
   "\<lbrace>x, y\<rbrace>"      == "CONST MPair x y"
 
 
 definition
   HPair :: "[msg,msg] \<Rightarrow> msg"                       ("(4Hash[_] /_)" [0, 1000])
 where
   \<comment> \<open>Message Y paired with a MAC computed with the help of X\<close>
   "Hash[X] Y \<equiv> \<lbrace>Hash\<lbrace>X,Y\<rbrace>, Y\<rbrace>"
 
 definition
   keysFor :: "msg set \<Rightarrow> key set"
 where
     \<comment> \<open>Keys useful to decrypt elements of a message set\<close>
   "keysFor H \<equiv> invKey ` {K. \<exists>X. Crypt K X \<in> H}"
 
 
 subsubsection\<open>Inductive Definition of All Parts" of a Message\<close>
 
 inductive_set
   parts :: "msg set => msg set"
   for H :: "msg set"
   where
     Inj [intro]:               "X \<in> H ==> X \<in> parts H"
   | Fst:         "\<lbrace>X,Y\<rbrace>   \<in> parts H ==> X \<in> parts H"
   | Snd:         "\<lbrace>X,Y\<rbrace>   \<in> parts H ==> Y \<in> parts H"
   | Body:        "Crypt K X \<in> parts H ==> X \<in> parts H"
 
 
 text\<open>Monotonicity\<close>
 lemma parts_mono: "G \<subseteq> H ==> parts(G) \<subseteq> parts(H)"
 apply auto
 apply (erule parts.induct)
 apply (blast dest: parts.Fst parts.Snd parts.Body)+
 done
 
 
 text\<open>Equations hold because constructors are injective.\<close>
 lemma Other_image_eq [simp]: "(Agent x \<in> Agent`A) = (x:A)"
 by auto
 
 lemma Key_image_eq [simp]: "(Key x \<in> Key`A) = (x\<in>A)"
 by auto
 
 lemma Nonce_Key_image_eq [simp]: "(Nonce x \<notin> Key`A)"
 by auto
 
 
 
 subsection\<open>keysFor operator\<close>
 
 lemma keysFor_empty [simp]: "keysFor {} = {}"
 by (unfold keysFor_def, blast)
 
 lemma keysFor_Un [simp]: "keysFor (H \<union> H') = keysFor H \<union> keysFor H'"
 by (unfold keysFor_def, blast)
 
 lemma keysFor_UN [simp]: "keysFor (\<Union>i\<in>A. H i) = (\<Union>i\<in>A. keysFor (H i))"
 by (unfold keysFor_def, blast)
 
 text\<open>Monotonicity\<close>
 lemma keysFor_mono: "G \<subseteq> H ==> keysFor(G) \<subseteq> keysFor(H)"
 by (unfold keysFor_def, blast)
 
 lemma keysFor_insert_Agent [simp]: "keysFor (insert (Agent A) H) = keysFor H"
 by (unfold keysFor_def, auto)
 
 lemma keysFor_insert_Nonce [simp]: "keysFor (insert (Nonce N) H) = keysFor H"
 by (unfold keysFor_def, auto)
 
 lemma keysFor_insert_Number [simp]: "keysFor (insert (Number N) H) = keysFor H"
 by (unfold keysFor_def, auto)
 
 lemma keysFor_insert_Key [simp]: "keysFor (insert (Key K) H) = keysFor H"
 by (unfold keysFor_def, auto)
 
 lemma keysFor_insert_Hash [simp]: "keysFor (insert (Hash X) H) = keysFor H"
 by (unfold keysFor_def, auto)
 
 lemma keysFor_insert_MPair [simp]: "keysFor (insert \<lbrace>X,Y\<rbrace> H) = keysFor H"
 by (unfold keysFor_def, auto)
 
 lemma keysFor_insert_Crypt [simp]:
     "keysFor (insert (Crypt K X) H) = insert (invKey K) (keysFor H)"
 by (unfold keysFor_def, auto)
 
 lemma keysFor_image_Key [simp]: "keysFor (Key`E) = {}"
 by (unfold keysFor_def, auto)
 
 lemma Crypt_imp_invKey_keysFor: "Crypt K X \<in> H ==> invKey K \<in> keysFor H"
 by (unfold keysFor_def, blast)
 
 
 subsection\<open>Inductive relation "parts"\<close>
 
 lemma MPair_parts:
      "[| \<lbrace>X,Y\<rbrace> \<in> parts H;
          [| X \<in> parts H; Y \<in> parts H |] ==> P |] ==> P"
 by (blast dest: parts.Fst parts.Snd)
 
 declare MPair_parts [elim!]  parts.Body [dest!]
 text\<open>NB These two rules are UNSAFE in the formal sense, as they discard the
      compound message.  They work well on THIS FILE.
   \<open>MPair_parts\<close> is left as SAFE because it speeds up proofs.
   The Crypt rule is normally kept UNSAFE to avoid breaking up certificates.\<close>
 
 lemma parts_increasing: "H \<subseteq> parts(H)"
 by blast
 
 lemmas parts_insertI = subset_insertI [THEN parts_mono, THEN subsetD]
 
 lemma parts_empty [simp]: "parts{} = {}"
 apply safe
 apply (erule parts.induct, blast+)
 done
 
 lemma parts_emptyE [elim!]: "X\<in> parts{} ==> P"
 by simp
 
 text\<open>WARNING: loops if H = {Y}, therefore must not be repeated!\<close>
 lemma parts_singleton: "X\<in> parts H ==> \<exists>Y\<in>H. X\<in> parts {Y}"
 by (erule parts.induct, fast+)
 
 
 subsubsection\<open>Unions\<close>
 
 lemma parts_Un_subset1: "parts(G) \<union> parts(H) \<subseteq> parts(G \<union> H)"
 by (intro Un_least parts_mono Un_upper1 Un_upper2)
 
 lemma parts_Un_subset2: "parts(G \<union> H) \<subseteq> parts(G) \<union> parts(H)"
 apply (rule subsetI)
 apply (erule parts.induct, blast+)
 done
 
 lemma parts_Un [simp]: "parts(G \<union> H) = parts(G) \<union> parts(H)"
 by (intro equalityI parts_Un_subset1 parts_Un_subset2)
 
 lemma parts_insert: "parts (insert X H) = parts {X} \<union> parts H"
 apply (subst insert_is_Un [of _ H])
 apply (simp only: parts_Un)
 done
 
 text\<open>TWO inserts to avoid looping.  This rewrite is better than nothing.
   Not suitable for Addsimps: its behaviour can be strange.\<close>
 lemma parts_insert2:
      "parts (insert X (insert Y H)) = parts {X} \<union> parts {Y} \<union> parts H"
 apply (simp add: Un_assoc)
 apply (simp add: parts_insert [symmetric])
 done
 
-lemma parts_UN_subset1: "(\<Union>x\<in>A. parts(H x)) \<subseteq> parts(\<Union>x\<in>A. H x)"
-by (intro UN_least parts_mono UN_upper)
-
-lemma parts_UN_subset2: "parts(\<Union>x\<in>A. H x) \<subseteq> (\<Union>x\<in>A. parts(H x))"
-apply (rule subsetI)
-apply (erule parts.induct, blast+)
-done
-
-lemma parts_UN [simp]: "parts(\<Union>x\<in>A. H x) = (\<Union>x\<in>A. parts(H x))"
-by (intro equalityI parts_UN_subset1 parts_UN_subset2)
-
-text\<open>Added to simplify arguments to parts, analz and synth.
-  NOTE: the UN versions are no longer used!\<close>
+text\<open>Added to simplify arguments to parts, analz and synth.\<close>
 
 
 text\<open>This allows \<open>blast\<close> to simplify occurrences of
   @{term "parts(G\<union>H)"} in the assumption.\<close>
 lemmas in_parts_UnE = parts_Un [THEN equalityD1, THEN subsetD, THEN UnE]
 declare in_parts_UnE [elim!]
 
 
 lemma parts_insert_subset: "insert X (parts H) \<subseteq> parts(insert X H)"
 by (blast intro: parts_mono [THEN [2] rev_subsetD])
 
 subsubsection\<open>Idempotence and transitivity\<close>
 
 lemma parts_partsD [dest!]: "X\<in> parts (parts H) ==> X\<in> parts H"
 by (erule parts.induct, blast+)
 
 lemma parts_idem [simp]: "parts (parts H) = parts H"
 by blast
 
 lemma parts_subset_iff [simp]: "(parts G \<subseteq> parts H) = (G \<subseteq> parts H)"
 apply (rule iffI)
 apply (iprover intro: subset_trans parts_increasing)
 apply (frule parts_mono, simp)
 done
 
 lemma parts_trans: "[| X\<in> parts G;  G \<subseteq> parts H |] ==> X\<in> parts H"
 by (drule parts_mono, blast)
 
 text\<open>Cut\<close>
 lemma parts_cut:
      "[| Y\<in> parts (insert X G);  X\<in> parts H |] ==> Y\<in> parts (G \<union> H)"
 by (blast intro: parts_trans)
 
 
 lemma parts_cut_eq [simp]: "X\<in> parts H ==> parts (insert X H) = parts H"
 by (force dest!: parts_cut intro: parts_insertI)
 
 
 subsubsection\<open>Rewrite rules for pulling out atomic messages\<close>
 
 lemmas parts_insert_eq_I = equalityI [OF subsetI parts_insert_subset]
 
 
 lemma parts_insert_Agent [simp]:
      "parts (insert (Agent agt) H) = insert (Agent agt) (parts H)"
 apply (rule parts_insert_eq_I)
 apply (erule parts.induct, auto)
 done
 
 lemma parts_insert_Nonce [simp]:
      "parts (insert (Nonce N) H) = insert (Nonce N) (parts H)"
 apply (rule parts_insert_eq_I)
 apply (erule parts.induct, auto)
 done
 
 lemma parts_insert_Number [simp]:
      "parts (insert (Number N) H) = insert (Number N) (parts H)"
 apply (rule parts_insert_eq_I)
 apply (erule parts.induct, auto)
 done
 
 lemma parts_insert_Key [simp]:
      "parts (insert (Key K) H) = insert (Key K) (parts H)"
 apply (rule parts_insert_eq_I)
 apply (erule parts.induct, auto)
 done
 
 lemma parts_insert_Hash [simp]:
      "parts (insert (Hash X) H) = insert (Hash X) (parts H)"
 apply (rule parts_insert_eq_I)
 apply (erule parts.induct, auto)
 done
 
 lemma parts_insert_Crypt [simp]:
      "parts (insert (Crypt K X) H) = insert (Crypt K X) (parts (insert X H))"
 apply (rule equalityI)
 apply (rule subsetI)
 apply (erule parts.induct, auto)
 apply (blast intro: parts.Body)
 done
 
 lemma parts_insert_MPair [simp]:
      "parts (insert \<lbrace>X,Y\<rbrace> H) =
           insert \<lbrace>X,Y\<rbrace> (parts (insert X (insert Y H)))"
 apply (rule equalityI)
 apply (rule subsetI)
 apply (erule parts.induct, auto)
 apply (blast intro: parts.Fst parts.Snd)+
 done
 
 lemma parts_image_Key [simp]: "parts (Key`N) = Key`N"
 apply auto
 apply (erule parts.induct, auto)
 done
 
 
 text\<open>In any message, there is an upper bound N on its greatest nonce.\<close>
 (*
 lemma msg_Nonce_supply: "\<exists>N. \<forall>n. N\<le>n --> Nonce n \<notin> parts {msg}"
 apply (induct msg)
 apply (simp_all (no_asm_simp) add: exI parts_insert2)
  txt{*MPair case: blast works out the necessary sum itself!*}
  prefer 2 apply auto apply (blast elim!: add_leE)
 txt{*Nonce case*}
 apply (rule_tac x = "N + Suc nat" in exI, auto)
 done
 *)
 
 
 subsection\<open>Inductive relation "analz"\<close>
 
 text\<open>Inductive definition of "analz" -- what can be broken down from a set of
     messages, including keys.  A form of downward closure.  Pairs can
     be taken apart; messages decrypted with known keys.\<close>
 
 inductive_set
   analz :: "msg set => msg set"
   for H :: "msg set"
   where
     Inj [intro,simp] :    "X \<in> H ==> X \<in> analz H"
   | Fst:     "\<lbrace>X,Y\<rbrace> \<in> analz H ==> X \<in> analz H"
   | Snd:     "\<lbrace>X,Y\<rbrace> \<in> analz H ==> Y \<in> analz H"
   | Decrypt [dest]:
              "[|Crypt K X \<in> analz H; Key(invKey K): analz H|] ==> X \<in> analz H"
 
 
 text\<open>Monotonicity; Lemma 1 of Lowe's paper\<close>
 lemma analz_mono: "G\<subseteq>H ==> analz(G) \<subseteq> analz(H)"
 apply auto
 apply (erule analz.induct)
 apply (auto dest: analz.Fst analz.Snd)
 done
 
 lemmas analz_monotonic = analz_mono [THEN [2] rev_subsetD]
 
 text\<open>Making it safe speeds up proofs\<close>
 lemma MPair_analz [elim!]:
      "[| \<lbrace>X,Y\<rbrace> \<in> analz H;
              [| X \<in> analz H; Y \<in> analz H |] ==> P
           |] ==> P"
 by (blast dest: analz.Fst analz.Snd)
 
 lemma analz_increasing: "H \<subseteq> analz(H)"
 by blast
 
 lemma analz_subset_parts: "analz H \<subseteq> parts H"
 apply (rule subsetI)
 apply (erule analz.induct, blast+)
 done
 
 lemmas analz_into_parts = analz_subset_parts [THEN subsetD]
 
 lemmas not_parts_not_analz = analz_subset_parts [THEN contra_subsetD]
 
 
 lemma parts_analz [simp]: "parts (analz H) = parts H"
 apply (rule equalityI)
 apply (rule analz_subset_parts [THEN parts_mono, THEN subset_trans], simp)
 apply (blast intro: analz_increasing [THEN parts_mono, THEN subsetD])
 done
 
 lemma analz_parts [simp]: "analz (parts H) = parts H"
 apply auto
 apply (erule analz.induct, auto)
 done
 
 lemmas analz_insertI = subset_insertI [THEN analz_mono, THEN [2] rev_subsetD]
 
 subsubsection\<open>General equational properties\<close>
 
 lemma analz_empty [simp]: "analz{} = {}"
 apply safe
 apply (erule analz.induct, blast+)
 done
 
 text\<open>Converse fails: we can analz more from the union than from the
   separate parts, as a key in one might decrypt a message in the other\<close>
 lemma analz_Un: "analz(G) \<union> analz(H) \<subseteq> analz(G \<union> H)"
 by (intro Un_least analz_mono Un_upper1 Un_upper2)
 
 lemma analz_insert: "insert X (analz H) \<subseteq> analz(insert X H)"
 by (blast intro: analz_mono [THEN [2] rev_subsetD])
 
 subsubsection\<open>Rewrite rules for pulling out atomic messages\<close>
 
 lemmas analz_insert_eq_I = equalityI [OF subsetI analz_insert]
 
 lemma analz_insert_Agent [simp]:
      "analz (insert (Agent agt) H) = insert (Agent agt) (analz H)"
 apply (rule analz_insert_eq_I)
 apply (erule analz.induct, auto)
 done
 
 lemma analz_insert_Nonce [simp]:
      "analz (insert (Nonce N) H) = insert (Nonce N) (analz H)"
 apply (rule analz_insert_eq_I)
 apply (erule analz.induct, auto)
 done
 
 lemma analz_insert_Number [simp]:
      "analz (insert (Number N) H) = insert (Number N) (analz H)"
 apply (rule analz_insert_eq_I)
 apply (erule analz.induct, auto)
 done
 
 lemma analz_insert_Hash [simp]:
      "analz (insert (Hash X) H) = insert (Hash X) (analz H)"
 apply (rule analz_insert_eq_I)
 apply (erule analz.induct, auto)
 done
 
 text\<open>Can only pull out Keys if they are not needed to decrypt the rest\<close>
 lemma analz_insert_Key [simp]:
     "K \<notin> keysFor (analz H) ==>
           analz (insert (Key K) H) = insert (Key K) (analz H)"
 apply (unfold keysFor_def)
 apply (rule analz_insert_eq_I)
 apply (erule analz.induct, auto)
 done
 
 lemma analz_insert_MPair [simp]:
      "analz (insert \<lbrace>X,Y\<rbrace> H) =
           insert \<lbrace>X,Y\<rbrace> (analz (insert X (insert Y H)))"
 apply (rule equalityI)
 apply (rule subsetI)
 apply (erule analz.induct, auto)
 apply (erule analz.induct)
 apply (blast intro: analz.Fst analz.Snd)+
 done
 
 text\<open>Can pull out enCrypted message if the Key is not known\<close>
 lemma analz_insert_Crypt:
      "Key (invKey K) \<notin> analz H
       ==> analz (insert (Crypt K X) H) = insert (Crypt K X) (analz H)"
 apply (rule analz_insert_eq_I)
 apply (erule analz.induct, auto)
 
 done
 
 lemma lemma1: "Key (invKey K) \<in> analz H ==>
                analz (insert (Crypt K X) H) \<subseteq>
                insert (Crypt K X) (analz (insert X H))"
 apply (rule subsetI)
 apply (erule_tac x = x in analz.induct, auto)
 done
 
 lemma lemma2: "Key (invKey K) \<in> analz H ==>
                insert (Crypt K X) (analz (insert X H)) \<subseteq>
                analz (insert (Crypt K X) H)"
 apply auto
 apply (erule_tac x = x in analz.induct, auto)
 apply (blast intro: analz_insertI analz.Decrypt)
 done
 
 lemma analz_insert_Decrypt:
      "Key (invKey K) \<in> analz H ==>
                analz (insert (Crypt K X) H) =
                insert (Crypt K X) (analz (insert X H))"
 by (intro equalityI lemma1 lemma2)
 
 text\<open>Case analysis: either the message is secure, or it is not! Effective,
 but can cause subgoals to blow up! Use with \<open>split_if\<close>; apparently
 \<open>split_tac\<close> does not cope with patterns such as @{term"analz (insert
 (Crypt K X) H)"}\<close>
 lemma analz_Crypt_if [simp]:
      "analz (insert (Crypt K X) H) =
           (if (Key (invKey K) \<in> analz H)
            then insert (Crypt K X) (analz (insert X H))
            else insert (Crypt K X) (analz H))"
 by (simp add: analz_insert_Crypt analz_insert_Decrypt)
 
 
 text\<open>This rule supposes "for the sake of argument" that we have the key.\<close>
 lemma analz_insert_Crypt_subset:
      "analz (insert (Crypt K X) H) \<subseteq>
            insert (Crypt K X) (analz (insert X H))"
 apply (rule subsetI)
 apply (erule analz.induct, auto)
 done
 
 
 lemma analz_image_Key [simp]: "analz (Key`N) = Key`N"
 apply auto
 apply (erule analz.induct, auto)
 done
 
 
 subsubsection\<open>Idempotence and transitivity\<close>
 
 lemma analz_analzD [dest!]: "X\<in> analz (analz H) ==> X\<in> analz H"
 by (erule analz.induct, blast+)
 
 lemma analz_idem [simp]: "analz (analz H) = analz H"
 by blast
 
 lemma analz_subset_iff [simp]: "(analz G \<subseteq> analz H) = (G \<subseteq> analz H)"
 apply (rule iffI)
 apply (iprover intro: subset_trans analz_increasing)
 apply (frule analz_mono, simp)
 done
 
 lemma analz_trans: "[| X\<in> analz G;  G \<subseteq> analz H |] ==> X\<in> analz H"
 by (drule analz_mono, blast)
 
 text\<open>Cut; Lemma 2 of Lowe\<close>
 lemma analz_cut: "[| Y\<in> analz (insert X H);  X\<in> analz H |] ==> Y\<in> analz H"
 by (erule analz_trans, blast)
 
 (*Cut can be proved easily by induction on
    "Y: analz (insert X H) ==> X: analz H --> Y: analz H"
 *)
 
 text\<open>This rewrite rule helps in the simplification of messages that involve
   the forwarding of unknown components (X).  Without it, removing occurrences
   of X can be very complicated.\<close>
 lemma analz_insert_eq: "X\<in> analz H ==> analz (insert X H) = analz H"
 by (blast intro: analz_cut analz_insertI)
 
 
 text\<open>A congruence rule for "analz"\<close>
 
 lemma analz_subset_cong:
      "[| analz G \<subseteq> analz G'; analz H \<subseteq> analz H' |]
       ==> analz (G \<union> H) \<subseteq> analz (G' \<union> H')"
 apply simp
 apply (iprover intro: conjI subset_trans analz_mono Un_upper1 Un_upper2)
 done
 
 lemma analz_cong:
      "[| analz G = analz G'; analz H = analz H' |]
       ==> analz (G \<union> H) = analz (G' \<union> H')"
 by (intro equalityI analz_subset_cong, simp_all)
 
 lemma analz_insert_cong:
      "analz H = analz H' ==> analz(insert X H) = analz(insert X H')"
 by (force simp only: insert_def intro!: analz_cong)
 
 text\<open>If there are no pairs or encryptions then analz does nothing\<close>
 lemma analz_trivial:
      "[| \<forall>X Y. \<lbrace>X,Y\<rbrace> \<notin> H;  \<forall>X K. Crypt K X \<notin> H |] ==> analz H = H"
 apply safe
 apply (erule analz.induct, blast+)
 done
 
 
 subsection\<open>Inductive relation "synth"\<close>
 
 text\<open>Inductive definition of "synth" -- what can be built up from a set of
     messages.  A form of upward closure.  Pairs can be built, messages
     encrypted with known keys.  Agent names are public domain.
     Numbers can be guessed, but Nonces cannot be.\<close>
 
 inductive_set
   synth :: "msg set => msg set"
   for H :: "msg set"
   where
     Inj    [intro]:   "X \<in> H ==> X \<in> synth H"
   | Agent  [intro]:   "Agent agt \<in> synth H"
   | Number [intro]:   "Number n  \<in> synth H"
   | Hash   [intro]:   "X \<in> synth H ==> Hash X \<in> synth H"
   | MPair  [intro]:   "[|X \<in> synth H;  Y \<in> synth H|] ==> \<lbrace>X,Y\<rbrace> \<in> synth H"
   | Crypt  [intro]:   "[|X \<in> synth H;  Key(K) \<in> H|] ==> Crypt K X \<in> synth H"
 
 text\<open>Monotonicity\<close>
 lemma synth_mono: "G\<subseteq>H ==> synth(G) \<subseteq> synth(H)"
   by (auto, erule synth.induct, auto)
 
 text\<open>NO \<open>Agent_synth\<close>, as any Agent name can be synthesized.
   The same holds for @{term Number}\<close>
 inductive_cases Nonce_synth [elim!]: "Nonce n \<in> synth H"
 inductive_cases Key_synth   [elim!]: "Key K \<in> synth H"
 inductive_cases Hash_synth  [elim!]: "Hash X \<in> synth H"
 inductive_cases MPair_synth [elim!]: "\<lbrace>X,Y\<rbrace> \<in> synth H"
 inductive_cases Crypt_synth [elim!]: "Crypt K X \<in> synth H"
 
 
 lemma synth_increasing: "H \<subseteq> synth(H)"
 by blast
 
 subsubsection\<open>Unions\<close>
 
 text\<open>Converse fails: we can synth more from the union than from the
   separate parts, building a compound message using elements of each.\<close>
 lemma synth_Un: "synth(G) \<union> synth(H) \<subseteq> synth(G \<union> H)"
 by (intro Un_least synth_mono Un_upper1 Un_upper2)
 
 lemma synth_insert: "insert X (synth H) \<subseteq> synth(insert X H)"
 by (blast intro: synth_mono [THEN [2] rev_subsetD])
 
 subsubsection\<open>Idempotence and transitivity\<close>
 
 lemma synth_synthD [dest!]: "X\<in> synth (synth H) ==> X\<in> synth H"
 by (erule synth.induct, blast+)
 
 lemma synth_idem: "synth (synth H) = synth H"
 by blast
 
 lemma synth_subset_iff [simp]: "(synth G \<subseteq> synth H) = (G \<subseteq> synth H)"
 apply (rule iffI)
 apply (iprover intro: subset_trans synth_increasing)
 apply (frule synth_mono, simp add: synth_idem)
 done
 
 lemma synth_trans: "[| X\<in> synth G;  G \<subseteq> synth H |] ==> X\<in> synth H"
 by (drule synth_mono, blast)
 
 text\<open>Cut; Lemma 2 of Lowe\<close>
 lemma synth_cut: "[| Y\<in> synth (insert X H);  X\<in> synth H |] ==> Y\<in> synth H"
 by (erule synth_trans, blast)
 
 lemma Agent_synth [simp]: "Agent A \<in> synth H"
 by blast
 
 lemma Number_synth [simp]: "Number n \<in> synth H"
 by blast
 
 lemma Nonce_synth_eq [simp]: "(Nonce N \<in> synth H) = (Nonce N \<in> H)"
 by blast
 
 lemma Key_synth_eq [simp]: "(Key K \<in> synth H) = (Key K \<in> H)"
 by blast
 
 lemma Crypt_synth_eq [simp]:
      "Key K \<notin> H ==> (Crypt K X \<in> synth H) = (Crypt K X \<in> H)"
 by blast
 
 
 lemma keysFor_synth [simp]:
     "keysFor (synth H) = keysFor H \<union> invKey`{K. Key K \<in> H}"
 by (unfold keysFor_def, blast)
 
 
 subsubsection\<open>Combinations of parts, analz and synth\<close>
 
 lemma parts_synth [simp]: "parts (synth H) = parts H \<union> synth H"
 apply (rule equalityI)
 apply (rule subsetI)
 apply (erule parts.induct)
 apply (blast intro: synth_increasing [THEN parts_mono, THEN subsetD]
                     parts.Fst parts.Snd parts.Body)+
 done
 
 lemma analz_analz_Un [simp]: "analz (analz G \<union> H) = analz (G \<union> H)"
 apply (intro equalityI analz_subset_cong)+
 apply simp_all
 done
 
 lemma analz_synth_Un [simp]: "analz (synth G \<union> H) = analz (G \<union> H) \<union> synth G"
 apply (rule equalityI)
 apply (rule subsetI)
 apply (erule analz.induct)
 prefer 5 apply (blast intro: analz_mono [THEN [2] rev_subsetD])
 apply (blast intro: analz.Fst analz.Snd analz.Decrypt)+
 done
 
 lemma analz_synth [simp]: "analz (synth H) = analz H \<union> synth H"
 apply (cut_tac H = "{}" in analz_synth_Un)
 apply (simp (no_asm_use))
 done
 
 text \<open>chsp: added\<close>
 
 lemma analz_Un_analz [simp]: "analz (G \<union> analz H) = analz (G \<union> H)"
 by (subst Un_commute, auto)+
 
 lemma analz_synth_Un2 [simp]: "analz (G \<union> synth H) = analz (G \<union> H) \<union> synth H"
 by (subst Un_commute, auto)+
 
 
 subsubsection\<open>For reasoning about the Fake rule in traces\<close>
 
 lemma parts_insert_subset_Un: "X\<in> G ==> parts(insert X H) \<subseteq> parts G \<union> parts H"
 by (rule subset_trans [OF parts_mono parts_Un_subset2], blast)
 
 text\<open>More specifically for Fake.  Very occasionally we could do with a version
   of the form  @{term"parts{X} \<subseteq> synth (analz H) \<union> parts H"}\<close>
 lemma Fake_parts_insert:
      "X \<in> synth (analz H) ==>
       parts (insert X H) \<subseteq> synth (analz H) \<union> parts H"
 apply (drule parts_insert_subset_Un)
 apply (simp (no_asm_use))
 apply blast
 done
 
 lemma Fake_parts_insert_in_Un:
      "[|Z \<in> parts (insert X H);  X \<in> synth (analz H)|]
       ==> Z \<in>  synth (analz H) \<union> parts H"
 by (blast dest: Fake_parts_insert  [THEN subsetD, dest])
 
 text\<open>@{term H} is sometimes @{term"Key ` KK \<union> spies evs"}, so can't put
   @{term "G=H"}.\<close>
 lemma Fake_analz_insert:
      "X\<in> synth (analz G) ==>
       analz (insert X H) \<subseteq> synth (analz G) \<union> analz (G \<union> H)"
 apply (rule subsetI)
 apply (subgoal_tac "x \<in> analz (synth (analz G) \<union> H) ")
 prefer 2
   apply (blast intro: analz_mono [THEN [2] rev_subsetD]
                       analz_mono [THEN synth_mono, THEN [2] rev_subsetD])
 apply (simp (no_asm_use))
 apply blast
 done
 
 lemma analz_conj_parts [simp]:
      "(X \<in> analz H & X \<in> parts H) = (X \<in> analz H)"
 by (blast intro: analz_subset_parts [THEN subsetD])
 
 lemma analz_disj_parts [simp]:
      "(X \<in> analz H | X \<in> parts H) = (X \<in> parts H)"
 by (blast intro: analz_subset_parts [THEN subsetD])
 
 text\<open>Without this equation, other rules for synth and analz would yield
   redundant cases\<close>
 lemma MPair_synth_analz [iff]:
      "(\<lbrace>X,Y\<rbrace> \<in> synth (analz H)) =
       (X \<in> synth (analz H) & Y \<in> synth (analz H))"
 by blast
 
 lemma Crypt_synth_analz:
      "[| Key K \<in> analz H;  Key (invKey K) \<in> analz H |]
        ==> (Crypt K X \<in> synth (analz H)) = (X \<in> synth (analz H))"
 by blast
 
 
 lemma Hash_synth_analz [simp]:
      "X \<notin> synth (analz H)
       ==> (Hash\<lbrace>X,Y\<rbrace> \<in> synth (analz H)) = (Hash\<lbrace>X,Y\<rbrace> \<in> analz H)"
 by blast
 
 
 subsection\<open>HPair: a combination of Hash and MPair\<close>
 
 subsubsection\<open>Freeness\<close>
 
 lemma Agent_neq_HPair: "Agent A ~= Hash[X] Y"
 by (unfold HPair_def, simp)
 
 lemma Nonce_neq_HPair: "Nonce N ~= Hash[X] Y"
 by (unfold HPair_def, simp)
 
 lemma Number_neq_HPair: "Number N ~= Hash[X] Y"
 by (unfold HPair_def, simp)
 
 lemma Key_neq_HPair: "Key K ~= Hash[X] Y"
 by (unfold HPair_def, simp)
 
 lemma Hash_neq_HPair: "Hash Z ~= Hash[X] Y"
 by (unfold HPair_def, simp)
 
 lemma Crypt_neq_HPair: "Crypt K X' ~= Hash[X] Y"
 by (unfold HPair_def, simp)
 
 lemmas HPair_neqs = Agent_neq_HPair Nonce_neq_HPair Number_neq_HPair
                     Key_neq_HPair Hash_neq_HPair Crypt_neq_HPair
 
 declare HPair_neqs [iff]
 declare HPair_neqs [symmetric, iff]
 
 lemma HPair_eq [iff]: "(Hash[X'] Y' = Hash[X] Y) = (X' = X & Y'=Y)"
 by (simp add: HPair_def)
 
 lemma MPair_eq_HPair [iff]:
      "(\<lbrace>X',Y'\<rbrace> = Hash[X] Y) = (X' = Hash\<lbrace>X,Y\<rbrace> & Y'=Y)"
 by (simp add: HPair_def)
 
 lemma HPair_eq_MPair [iff]:
      "(Hash[X] Y = \<lbrace>X',Y'\<rbrace>) = (X' = Hash\<lbrace>X,Y\<rbrace> & Y'=Y)"
 by (auto simp add: HPair_def)
 
 
 subsubsection\<open>Specialized laws, proved in terms of those for Hash and MPair\<close>
 
 lemma keysFor_insert_HPair [simp]: "keysFor (insert (Hash[X] Y) H) = keysFor H"
 by (simp add: HPair_def)
 
 lemma parts_insert_HPair [simp]:
     "parts (insert (Hash[X] Y) H) =
      insert (Hash[X] Y) (insert (Hash\<lbrace>X,Y\<rbrace>) (parts (insert Y H)))"
 by (simp add: HPair_def)
 
 lemma analz_insert_HPair [simp]:
     "analz (insert (Hash[X] Y) H) =
      insert (Hash[X] Y) (insert (Hash\<lbrace>X,Y\<rbrace>) (analz (insert Y H)))"
 by (simp add: HPair_def)
 
 lemma HPair_synth_analz [simp]:
      "X \<notin> synth (analz H)
     ==> (Hash[X] Y \<in> synth (analz H)) =
         (Hash\<lbrace>X, Y\<rbrace> \<in> analz H & Y \<in> synth (analz H))"
 by (simp add: HPair_def)
 
 
 text\<open>We do NOT want Crypt... messages broken up in protocols!!\<close>
 declare parts.Body [rule del]
 
 
 text\<open>Rewrites to push in Key and Crypt messages, so that other messages can
     be pulled out using the \<open>analz_insert\<close> rules\<close>
 
 lemmas pushKeys =
   insert_commute [of "Key K" "Agent C" for K C]
   insert_commute [of "Key K" "Nonce N" for K N]
   insert_commute [of "Key K" "Number N" for K N]
   insert_commute [of "Key K" "Hash X" for K X]
   insert_commute [of "Key K" "MPair X Y" for K X Y]
   insert_commute [of "Key K" "Crypt X K'" for K K' X]
 
 lemmas pushCrypts =
   insert_commute [of "Crypt X K" "Agent C" for X K C]
   insert_commute [of "Crypt X K" "Agent C" for X K C]
   insert_commute [of "Crypt X K" "Nonce N" for X K N]
   insert_commute [of "Crypt X K" "Number N"  for X K N]
   insert_commute [of "Crypt X K" "Hash X'"  for X K X']
   insert_commute [of "Crypt X K" "MPair X' Y"  for X K X' Y]
 
 text\<open>Cannot be added with \<open>[simp]\<close> -- messages should not always be
   re-ordered.\<close>
 lemmas pushes = pushKeys pushCrypts
 
 
 text\<open>By default only \<open>o_apply\<close> is built-in.  But in the presence of
 eta-expansion this means that some terms displayed as @{term "f o g"} will be
 rewritten, and others will not!\<close>
 declare o_def [simp]
 
 
 lemma Crypt_notin_image_Key [simp]: "Crypt K X \<notin> Key ` A"
 by auto
 
 lemma Hash_notin_image_Key [simp] :"Hash X \<notin> Key ` A"
 by auto
 
 lemma synth_analz_mono: "G\<subseteq>H ==> synth (analz(G)) \<subseteq> synth (analz(H))"
 by (iprover intro: synth_mono analz_mono)
 
 lemma Fake_analz_eq [simp]:
      "X \<in> synth(analz H) ==> synth (analz (insert X H)) = synth (analz H)"
 apply (drule Fake_analz_insert[of _ _ "H"])
 apply (simp add: synth_increasing[THEN Un_absorb2])
 apply (drule synth_mono)
 apply (simp add: synth_idem)
 apply (rule equalityI)
 apply simp
 apply (rule synth_analz_mono, blast)
 done
 
 text\<open>Two generalizations of \<open>analz_insert_eq\<close>\<close>
 lemma gen_analz_insert_eq [rule_format]:
      "X \<in> analz H ==> ALL G. H \<subseteq> G --> analz (insert X G) = analz G"
 by (blast intro: analz_cut analz_insertI analz_mono [THEN [2] rev_subsetD])
 
 lemma synth_analz_insert_eq [rule_format]:
      "X \<in> synth (analz H)
       ==> ALL G. H \<subseteq> G --> (Key K \<in> analz (insert X G)) = (Key K \<in> analz G)"
 apply (erule synth.induct)
 apply (simp_all add: gen_analz_insert_eq subset_trans [OF _ subset_insertI])
 done
 
 lemma Fake_parts_sing:
      "X \<in> synth (analz H) ==> parts{X} \<subseteq> synth (analz H) \<union> parts H"
 apply (rule subset_trans)
  apply (erule_tac [2] Fake_parts_insert)
 apply (rule parts_mono, blast)
 done
 
 lemmas Fake_parts_sing_imp_Un = Fake_parts_sing [THEN [2] rev_subsetD]
 
 
 text\<open>For some reason, moving this up can make some proofs loop!\<close>
 declare invKey_K [simp]
 
 
 end