Theory Message

(*******************************************************************************

  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 ‹Theory of ASes and Messages for Security Protocols›

theory Message imports Keys "HOL-Library.Sublist" "HOL.Finite_Set" "HOL-Library.FSet"
begin

datatype msgterm =
    ε                                  ― ‹Empty message. Used for instance to denote non-existent interface›
  | AS as                              ― ‹Autonomous System identifier, i.e. agents. Note that AS is an alias of nat›
  | Num nat                            ― ‹Ordinary integers, timestamps, ...›
  | Key    key                         ― ‹Crypto keys›
  | Nonce  nonce                       ― ‹Unguessable nonces›
  | L      "msgterm list"              ― ‹Lists›
  | FS     "msgterm fset"              ― ‹Finite Sets. Used to represent XOR values.›
  | MPair  msgterm msgterm             ― ‹Compound messages›
  | Hash    msgterm                    ― ‹Hashing›
  | Crypt  key msgterm                 ― ‹Encryption, public- or shared-key›

text ‹Syntax sugar›
syntax
  "_MTuple" :: "['a, args] ⇒ 'a * 'b"       ("(2⟨_,/ _⟩)")

syntax (xsymbols)
  "_MTuple" :: "['a, args] ⇒ 'a * 'b"       ("(2⟨_,/ _⟩)")

translations
  "⟨x, y, z⟩" ⇌ "⟨x, ⟨y, z⟩⟩"
  "⟨x, y⟩"    ⇌ "CONST MPair x y"

syntax
  "_MHF" :: "['a, 'b , 'c, 'd, 'e] ⇒ 'a * 'b * 'c * 'd * 'e"  ("(5HF⊲_,/ _,/ _,/ _,/ _⊳)")

abbreviation
  Mac :: "[msgterm,msgterm] ⇒ msgterm"                       ("(4Mac[_] /_)" [0, 1000])
where
  ― ‹Message Y paired with a MAC computed with the help of X›
  "Mac[X] Y ≡ Hash ⟨X,Y⟩"

abbreviation macKey where "macKey a ≡ Key (macK a)"

definition
  keysFor :: "msgterm set ⇒ key set"
where
  ― ‹Keys useful to decrypt elements of a message set›
  "keysFor H ≡ invKey ` {K. ∃X. Crypt K X ∈ H}"

subsubsection ‹Inductive Definition of "All Parts" of a Message›

inductive_set
  parts :: "msgterm set ⇒ msgterm set"
  for H :: "msgterm set"
  where
    Inj [intro]: "X ∈ H ⟹ X ∈ parts H"
  | Fst:         "⟨X,_⟩ ∈ parts H ⟹ X ∈ parts H"
  | Snd:         "⟨_,Y⟩ ∈ parts H ⟹ Y ∈ parts H"
  | Lst:         "⟦ L xs ∈ parts H; X ∈ set xs ⟧ ⟹ X ∈ parts H"
  | FSt:          "⟦ FS xs ∈ parts H; X |∈| xs ⟧ ⟹ X ∈ parts H"
(*| Hd:          "L (X # xs) ∈ parts H ⟹ X ∈ parts H"
  | Tl:          "L (X # xs) ∈ parts H ⟹ L xs ∈ parts H" *)
  | Body:        "Crypt K X ∈ parts H ⟹ X ∈ parts H"


text ‹Monotonicity›
lemma parts_mono: "G ⊆ H ⟹ parts G ⊆ parts H"
apply auto
apply (erule parts.induct)
apply (blast dest: parts.Fst parts.Snd parts.Lst parts.FSt parts.Body)+
done


text ‹Equations hold because constructors are injective.›
lemma Other_image_eq [simp]: "(AS x ∈ AS`A) = (x:A)"
by auto

lemma Key_image_eq [simp]: "(Key x ∈ Key`A) = (x∈A)"
by auto

lemma AS_Key_image_eq [simp]: "(AS x ∉ Key`A)"
by auto

lemma Num_Key_image_eq [simp]: "(Num x ∉ Key`A)"
by auto

subsection ‹keysFor operator›

lemma keysFor_empty [simp]: "keysFor {} = {}"
by (unfold keysFor_def, blast)

lemma keysFor_Un [simp]: "keysFor (H ∪ H') = keysFor H ∪ keysFor H'"
by (unfold keysFor_def, blast)

lemma keysFor_UN [simp]: "keysFor (⋃i∈A. H i) = (⋃i∈A. keysFor (H i))"
by (unfold keysFor_def, blast)

text ‹Monotonicity›
lemma keysFor_mono: "G ⊆ H ⟹ keysFor G ⊆ 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 ⟨X,Y⟩ 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 ∈ H ⟹ invKey K ∈ keysFor H"
by (unfold keysFor_def, blast)


subsection ‹Inductive relation "parts"›

lemma MPair_parts:
  "⟦
    ⟨X,Y⟩ ∈ parts H;
    ⟦ X ∈ parts H; Y ∈ parts H ⟧ ⟹ P
   ⟧ ⟹ P"
by (blast dest: parts.Fst parts.Snd)

lemma L_parts:
  "⟦
    L l ∈ parts H;
    ⟦ set l ⊆ parts H ⟧ ⟹ P
   ⟧ ⟹ P"
  by (blast dest: parts.Lst)

lemma FS_parts:
  "⟦
    FS l ∈ parts H;
    ⟦ fset l ⊆ parts H ⟧ ⟹ P
   ⟧ ⟹ P"
  by (simp add: parts.FSt subsetI)
thm parts.FSt subsetI

declare MPair_parts [elim!] L_parts [elim!] FS_parts [elim] parts.Body [dest!]

text ‹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.›

lemma parts_increasing: "H ⊆ 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∈ parts{} ⟹ P"
by simp

text ‹WARNING: loops if H = {Y}, therefore must not be repeated!›
lemma parts_singleton: "X ∈ parts H ⟹ ∃Y ∈ H. X ∈ parts {Y}"
  apply (erule parts.induct, fast)
  using parts.FSt by blast+

lemma parts_singleton_set: "x ∈ parts {s . P s} ⟹ ∃Y. P Y ∧ x ∈ parts {Y}"
  by(auto dest: parts_singleton)

lemma parts_singleton_set_rev: "⟦x ∈ parts {Y}; P Y⟧ ⟹ x ∈ parts {s . P s}"
  by (induction rule: parts.induct)
     (blast dest: parts.Fst parts.Snd parts.Lst parts.FSt parts.Body)+

lemma parts_Hash: "⟦⋀t . t ∈ H ⟹ ∃t' . t = Hash t'⟧ ⟹ parts H = H"
  by (auto, erule parts.induct, fast+)

subsubsection ‹Unions›

lemma parts_Un_subset1: "parts G ∪ parts H ⊆ parts(G ∪ H)"
by (intro Un_least parts_mono Un_upper1 Un_upper2)

lemma parts_Un_subset2: "parts(G ∪ H) ⊆ parts G ∪ parts H"
  by (rule subsetI) (erule parts.induct, blast+)

lemma parts_Un [simp]: "parts(G ∪ H) = parts G ∪ parts H"
by (intro equalityI parts_Un_subset1 parts_Un_subset2)

lemma parts_insert: "parts (insert X H) = parts {X} ∪ parts H"
apply (subst insert_is_Un [of _ H])
apply (simp only: parts_Un)
done

text ‹TWO inserts to avoid looping.  This rewrite is better than nothing.
        Not suitable for Addsimps: its behaviour can be strange.›
lemma parts_insert2:
  "parts (insert X (insert Y H)) = parts {X} ∪ parts {Y} ∪ parts H"
apply (simp add: Un_assoc)
apply (simp add: parts_insert [symmetric])
done

(*needed?!*)
lemma parts_two: "⟦x ∈ parts {e1, e2}; x ∉ parts {e1}⟧⟹ x ∈ parts {e2}"
  by (simp add: parts_insert2)


text ‹Added to simplify arguments to parts, analz and synth.›


text ‹This allows @{text blast} to simplify occurrences of
        @{term "parts(G∪H)"} in the assumption.›
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) ⊆ parts(insert X H)"
by (blast intro: parts_mono [THEN [2] rev_subsetD])



subsubsection ‹Idempotence›

lemma parts_partsD [dest!]: "X∈ parts (parts H) ⟹ X∈ 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 ⊆ parts H) = (G ⊆ parts H)"
apply (rule iffI)
apply (iprover intro: subset_trans parts_increasing)
apply (frule parts_mono, simp)
done

subsubsection ‹Transitivity›
lemma parts_trans: "⟦ X∈ parts G;  G ⊆ parts H ⟧ ⟹ X∈ parts H"
by (drule parts_mono, blast)

subsubsection ‹Unions, revisited›
text ‹You can take the union of parts h for all h in H›
lemma parts_split: "parts H = ⋃ { parts {h} | h . h ∈ 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 ‹Cut›
lemma parts_cut:
  "⟦ Y∈ parts (insert X G);  X ∈ parts H ⟧ ⟹ Y ∈ parts (G ∪ H)"
by (blast intro: parts_trans)


lemma parts_cut_eq [simp]: "X ∈ parts H ⟹ parts (insert X H) = parts H"
by (force dest!: parts_cut intro: parts_insertI)


subsubsection ‹Rewrite rules for pulling out atomic messages›

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 ε H) = insert ε (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 ⟨X,Y⟩ H) =
    insert ⟨X,Y⟩ (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) ∪  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) ∪  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 ‹Parts of lists and finite sets.›

lemma parts_list_set (*[simp]*):
  "parts (L`ls) =  (L`ls) ∪ (⋃l ∈ 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) ∪ H) =  (L`ls) ∪ (⋃l ∈ ls. parts ((set l))) ∪ 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) ∪ (⋃l ∈ 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 ‹suffix of parts›
lemma suffix_in_parts:
  "suffix (x#xs) ys ⟹ x ∈ parts {L ys}"
by (auto simp add: suffix_def)

lemma parts_L_set:
  "⟦x ∈ parts {L ys}; ys ∈ St⟧ ⟹ x ∈ 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:
  "⟦suffix (x#xs) ys; ys ∈ St⟧ ⟹ x ∈ parts (L`St)"
using parts_L_set suffix_in_parts
by blast

subsection ‹Inductive relation "analz"›

text ‹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.›

inductive_set
  analz :: "msgterm set ⇒ msgterm set"
  for H :: "msgterm set"
  where
    Inj [intro,simp] : "X ∈ H ⟹ X ∈ analz H"
  | Fst:               "⟨X,Y⟩ ∈ analz H ⟹ X ∈ analz H"
  | Snd:               "⟨X,Y⟩ ∈ analz H ⟹ Y ∈ analz H"
  | Lst:               "(L y) ∈ analz H  ⟹ x ∈ set (y) ⟹ x ∈ analz H "
  | FSt:               "⟦ FS xs ∈ analz H; X |∈| xs ⟧ ⟹ X ∈ analz H"
  | Decrypt [dest]:    "⟦ Crypt K X ∈ analz H; Key (invKey K) ∈ analz H ⟧ ⟹ X ∈ analz H"


text ‹Monotonicity; Lemma 1 of Lowe's paper›
lemma analz_mono: "G ⊆ H ⟹ analz(G) ⊆ 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 ‹Making it safe speeds up proofs›
lemma MPair_analz [elim!]:
  "⟦
    ⟨X,Y⟩ ∈ analz H;
    ⟦ X ∈ analz H; Y ∈ analz H ⟧ ⟹ P
   ⟧ ⟹ P"
by (blast dest: analz.Fst analz.Snd)

lemma L_analz [elim!]:
  "⟦
    L l ∈ analz H;
    ⟦ set l ⊆ analz H ⟧ ⟹ P
   ⟧ ⟹ P"
by (blast dest: analz.Lst analz.FSt)

lemma FS_analz [elim!]:
  "⟦
    FS l ∈ analz H;
    ⟦ fset l ⊆ analz H ⟧ ⟹ P
   ⟧ ⟹ P"
  by (simp add: analz.FSt subsetI)

thm parts.FSt subsetI
lemma analz_increasing: "H ⊆ analz(H)"
by blast

lemma analz_subset_parts: "analz H ⊆ parts H"
  by (rule subsetI) (erule analz.induct, blast+)


text ‹If there is no cryptography, then analz and parts is equivalent.›
lemma no_crypt_analz_is_parts:
  "¬ (∃ K X . Crypt K X ∈ parts A) ⟹ 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 ‹General equational properties›

lemma analz_empty [simp]: "analz {} = {}"
apply safe
apply (erule analz.induct, blast+)
done

text ‹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›
lemma analz_Un: "analz(G) ∪ analz(H) ⊆ analz(G ∪ H)"
by (intro Un_least analz_mono Un_upper1 Un_upper2)

lemma analz_insert: "insert X (analz H) ⊆ analz(insert X H)"
by (blast intro: analz_mono [THEN [2] rev_subsetD])

subsubsection ‹Rewrite rules for pulling out atomic messages›

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 ‹Can only pull out Keys if they are not needed to decrypt the rest›
lemma analz_insert_Key [simp]:
  "K ∉ keysFor (analz H) ⟹
    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 ∪ 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 ∪ H))"
apply (rule equalityI)
apply (rule subsetI)
apply (erule analz.induct, auto)
apply (erule analz.induct, auto)
using analz.Inj by blast

lemma "L[] ∈ 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 ⟨X,Y⟩ H) =
    insert ⟨X,Y⟩ (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 ‹Can pull out enCrypted message if the Key is not known›
lemma analz_insert_Crypt:
  "Key (invKey K) ∉ analz H
    ⟹ 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) ∈ analz H ⟹
    analz (insert (Crypt K X) H) ⊆
    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) ∈ analz H ⟹
    insert (Crypt K X) (analz (insert X H)) ⊆
    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) ∈ analz H ⟹
    analz (insert (Crypt K X) H) =
    insert (Crypt K X) (analz (insert X H))"
by (intro equalityI analz_insert_Decrypt1 analz_insert_Decrypt2)

text ‹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)"}›
lemma analz_Crypt_if [simp]:
  "analz (insert (Crypt K X) H) =
    (if (Key (invKey K) ∈ 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 ‹This rule supposes "for the sake of argument" that we have the key.›
lemma analz_insert_Crypt_subset:
  "analz (insert (Crypt K X) H) ⊆
    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 ‹Idempotence and transitivity›

lemma analz_analzD [dest!]: "X∈ analz (analz H) ⟹ X∈ 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 ⊆ analz H) = (G ⊆ analz H)"
apply (rule iffI)
apply (iprover intro: subset_trans analz_increasing)
apply (frule analz_mono, simp)
done

lemma analz_trans: "⟦ X∈ analz G;  G ⊆ analz H ⟧ ⟹ X∈ analz H"
by (drule analz_mono, blast)

text ‹Cut; Lemma 2 of Lowe›
lemma analz_cut: "⟦ Y∈ analz (insert X H);  X∈ analz H ⟧ ⟹ Y∈ 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 ‹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.›
lemma analz_insert_eq: "X∈ analz H ⟹ analz (insert X H) = analz H"
by (blast intro: analz_cut analz_insertI)


text ‹A congruence rule for "analz"›

lemma analz_subset_cong:
  "⟦ analz G ⊆ analz G'; analz H ⊆ analz H' ⟧
    ⟹ analz (G ∪ H) ⊆ analz (G' ∪ 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 ∪ H) = analz (G' ∪ 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 ‹If there are no pairs, lists or encryptions then analz does nothing›
(*needed?*)
lemma analz_trivial:
  "⟦
    ∀X Y. ⟨X,Y⟩ ∉ H; ∀xs. L xs ∉ H; ∀xs. FS xs ∉ H;
    ∀X K. Crypt K X ∉ H
   ⟧ ⟹ analz H = H"
apply safe
by (erule analz.induct, auto)

text ‹These two are obsolete (with a single Spy) but cost little to prove...›
lemma analz_UN_analz_lemma:
  "X∈ analz (⋃i∈A. analz (H i)) ⟹ X∈ analz (⋃i∈A. H i)"
apply (erule analz.induct)
by (auto intro: analz_mono [THEN [2] rev_subsetD])

lemma analz_UN_analz [simp]: "analz (⋃i∈A. analz (H i)) = analz (⋃i∈A. H i)"
by (blast intro: analz_UN_analz_lemma analz_mono [THEN [2] rev_subsetD])


subsubsection ‹Lemmas assuming absense of keys›
text ‹If there are no keys in analz H, you can take the union of analz h for all h in H›

lemma analz_split:
  "¬(∃ K . Key K ∈ analz H)
    ⟹ analz H = ⋃ { analz {h} | h . h ∈ 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 "¬(∃ K . Key K ∈ analz H)" and "¬(∃ K . Key K ∈ analz G)"
  shows "analz (H ∪ G) = analz H ∪ analz G"
apply (intro equalityI, rule subsetI)
apply (erule analz.induct)
using assms by auto

lemma analz_Un_eq_Crypt:
  assumes "¬(∃ K . Key K ∈ analz G)" and "¬(∃ K X . Crypt K X ∈ analz G)"
  shows "analz (H ∪ G) = analz H ∪ analz G"
apply (intro equalityI, rule subsetI)
apply (erule analz.induct)
using assms by auto

lemma analz_list_set (*[simp]*):
  "¬(∃ K . Key K ∈ analz (L`ls))
    ⟹ analz (L`ls) =  (L`ls) ∪ (⋃l ∈ 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]*):
  "¬(∃ K . Key K ∈ analz (FS`ls))
    ⟹ analz (FS`ls) =  (FS`ls) ∪ (⋃l ∈ 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 ‹Inductive relation "synth"›

text ‹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.›

inductive_set
  synth :: "msgterm set ⇒ msgterm set"
  for H :: "msgterm set"
  where
    Inj    [intro]:   "X ∈ H ⟹ X ∈ synth H"
  | ε  [simp,intro!]:   "ε ∈ synth H"
  | AS  [simp,intro!]:   "AS agt ∈ synth H"
  | Num [simp,intro!]:   "Num n  ∈ synth H"
  | Lst [intro]:      "⟦ ⋀x . x ∈ set xs ⟹ x ∈ synth H ⟧ ⟹ L xs ∈ synth H"
  | FSt [intro]:      "⟦ ⋀x . x ∈ fset xs ⟹ x ∈ synth H;
                         ⋀x ys . x ∈ fset xs ⟹ x ≠ FS ys ⟧
                      ⟹ FS xs ∈ synth H"
  | Hash   [intro]:   "X ∈ synth H ⟹ Hash X ∈ synth H"
  | MPair  [intro]:   "⟦ X ∈ synth H;  Y ∈ synth H ⟧ ⟹ ⟨X,Y⟩ ∈ synth H"
  | Crypt  [intro]:   "⟦ X ∈ synth H;  Key K ∈ H ⟧ ⟹ Crypt K X ∈ synth H"


(*removed fcard xs ≠ Suc 0 from FSt premise*)


text ‹Monotonicity›
lemma synth_mono: "G ⊆ H ⟹ synth(G) ⊆ synth(H)"
  apply (auto, erule synth.induct, auto)
  by blast

text ‹NO @{text AS_synth}, as any AS name can be synthesized.
        The same holds for @{term Num}›
inductive_cases Key_synth   [elim!]: "Key K ∈ synth H"
inductive_cases Nonce_synth [elim!]: "Nonce n ∈ synth H"
inductive_cases Hash_synth  [elim!]: "Hash X ∈ synth H"
inductive_cases MPair_synth [elim!]: "⟨X,Y⟩ ∈ synth H"
inductive_cases L_synth     [elim!]: "L X ∈ synth H"
inductive_cases FS_synth    [elim!]: "FS X ∈ synth H"
inductive_cases Crypt_synth [elim!]: "Crypt K X ∈ synth H"

lemma synth_increasing: "H ⊆ synth(H)"
by blast

lemma synth_analz_self: "x ∈ H ⟹ x ∈ synth (analz H)"
  by blast

subsubsection ‹Unions›

text ‹Converse fails: we can synth more from the union than from the
        separate parts, building a compound message using elements of each.›
lemma synth_Un: "synth(G) ∪ synth(H) ⊆ synth(G ∪ H)"
by (intro Un_least synth_mono Un_upper1 Un_upper2)

lemma synth_insert: "insert X (synth H) ⊆ synth(insert X H)"
by (blast intro: synth_mono [THEN [2] rev_subsetD])

subsubsection ‹Idempotence and transitivity›

lemma synth_synthD [dest!]: "X∈ synth (synth H) ⟹ X ∈ 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 ⊆ synth H) = (G ⊆ 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∈ synth G;  G ⊆ synth H ⟧ ⟹ X∈ synth H"
by (drule synth_mono, blast)

text ‹Cut; Lemma 2 of Lowe›
lemma synth_cut: "⟦ Y∈ synth (insert X H);  X∈ synth H ⟧ ⟹ Y∈ synth H"
by (erule synth_trans, blast)

lemma Nonce_synth_eq [simp]: "(Nonce N ∈ synth H) = (Nonce N ∈ H)"
by blast

lemma Key_synth_eq [simp]: "(Key K ∈ synth H) = (Key K ∈ H)"
by blast

lemma Crypt_synth_eq [simp]:
  "Key K ∉ H ⟹ (Crypt K X ∈ synth H) = (Crypt K X ∈ H)"
by blast


lemma keysFor_synth [simp]:
  "keysFor (synth H) = keysFor H ∪ invKey`{K. Key K ∈ H}"
by (unfold keysFor_def, blast)

lemma L_cons_synth [simp]:
  "(set xs ⊆ H) ⟹ (L xs ∈ synth H)"
by auto

lemma FS_cons_synth [simp]:
  "⟦fset xs ⊆ H; ⋀x ys. x ∈ fset xs ⟹ x ≠ FS ys; fcard xs ≠ Suc 0 ⟧ ⟹ (FS xs ∈ synth H)"
by auto

subsubsection ‹Combinations of parts, analz and synth›

lemma parts_synth [simp]: "parts (synth H) = parts H ∪ synth H"
proof (safe del: UnCI)
  fix X
  assume "X ∈ parts (synth H)"
  thus "X ∈ parts H ∪ synth H"
  by (induct rule: parts.induct)
     (auto intro: parts.Fst parts.Snd parts.Lst parts.FSt parts.Body)
next
  fix X
  assume "X ∈ parts H"
  thus "X ∈ 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 ∈ synth H"
  thus "X ∈ 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 ∪ H) = analz (G ∪ H)"
apply (intro equalityI analz_subset_cong)+
apply simp_all
done

lemma analz_synth_Un [simp]: "analz (synth G ∪ H) = analz (G ∪ H) ∪ synth G"
proof (safe del: UnCI)
  fix X
  assume "X ∈ analz (synth G ∪ H)"
  thus "X ∈ analz (G ∪ H) ∪ 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 ∪ synth H"
apply (cut_tac H = "{}" in analz_synth_Un)
apply (simp (no_asm_use))
done

lemma analz_Un_analz [simp]: "analz (G ∪ analz H) = analz (G ∪ H)"
by (subst Un_commute, auto)+

lemma analz_synth_Un2 [simp]: "analz (G ∪ synth H) = analz (G ∪ H) ∪ synth H"
by (subst Un_commute, auto)+


subsubsection ‹For reasoning about the Fake rule in traces›

lemma parts_insert_subset_Un: "X∈ G ⟹ parts(insert X H) ⊆ parts G ∪ parts H"
by (rule subset_trans [OF parts_mono parts_Un_subset2], blast)

text ‹More specifically for Fake.  Very occasionally we could do with a version
  of the form  @{term"parts{X} ⊆ synth (analz H) ∪ parts H"}›
lemma Fake_parts_insert:
  "X ∈ synth (analz H) ⟹
    parts (insert X H) ⊆ synth (analz H) ∪ parts H"
apply (drule parts_insert_subset_Un)
apply (simp (no_asm_use))
apply blast
done

lemma Fake_parts_insert_in_Un:
  "⟦Z ∈ parts (insert X H);  X ∈ synth (analz H)⟧
    ⟹ Z ∈  synth (analz H) ∪ parts H"
by (blast dest: Fake_parts_insert  [THEN subsetD, dest])

text ‹@{term H} is sometimes @{term"Key ` KK ∪ spies evs"}, so can't put @{term "G=H"}.›
lemma Fake_analz_insert:
  "X∈ synth (analz G) ⟹
    analz (insert X H) ⊆ synth (analz G) ∪ analz (G ∪ H)"
apply (rule subsetI)
apply (subgoal_tac "x ∈ analz (synth (analz G) ∪ 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 ∈ analz H & X ∈ parts H) = (X ∈ analz H)"
by (blast intro: analz_subset_parts [THEN subsetD])

lemma analz_disj_parts [simp]:
  "(X ∈ analz H | X ∈ parts H) = (X ∈ parts H)"
by (blast intro: analz_subset_parts [THEN subsetD])

text ‹Without this equation, other rules for synth and analz would yield
        redundant cases›
lemma MPair_synth_analz [iff]:
  "(⟨X,Y⟩ ∈ synth (analz H)) =
    (X ∈ synth (analz H) & Y ∈ synth (analz H))"
by blast

lemma L_cons_synth_analz [iff]:
  "(L xs ∈ synth (analz H)) =
    (set xs ⊆ synth (analz H))"
by blast

lemma L_cons_synth_parts [iff]:
  "(L xs ∈ synth (parts H)) =
    (set xs ⊆ synth (parts H))"
by blast

lemma FS_cons_synth_analz [iff]:
  "⟦⋀x ys . x ∈ fset xs ⟹ x ≠ FS ys; fcard xs ≠ Suc 0 ⟧ ⟹
    (FS xs ∈ synth (analz H)) =
    (fset xs ⊆ synth (analz H))"
by blast

lemma FS_cons_synth_parts [iff]:
  "⟦⋀x ys . x ∈ fset xs ⟹ x ≠ FS ys; fcard xs ≠ Suc 0 ⟧ ⟹
    (FS xs ∈ synth (parts H)) =
    (fset xs ⊆ synth (parts H))"
by blast

lemma Crypt_synth_analz:
  "⟦ Key K ∈ analz H;  Key (invKey K) ∈ analz H ⟧
    ⟹ (Crypt K X ∈ synth (analz H)) = (X ∈ synth (analz H))"
by blast

lemma Hash_synth_analz [simp]:
  "X ∉ synth (analz H)
    ⟹ (Hash⟨X,Y⟩ ∈ synth (analz H)) = (Hash⟨X,Y⟩ ∈ analz H)"
by blast


subsection ‹HPair: a combination of Hash and MPair›

text ‹We do NOT want Crypt... messages broken up in protocols!!›
declare parts.Body [rule del]


text ‹Rewrites to push in Key and Crypt messages, so that other messages can
        be pulled out using the @{text analz_insert} rules›

(*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 ‹Cannot be added with @{text "[simp]"} -- messages should not always be
        re-ordered.›
lemmas pushes = pushKeys pushCrypts

text ‹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!›
declare o_def [simp]


lemma Crypt_notin_image_Key [simp]: "Crypt K X ∉ Key ` A"
by auto

lemma Hash_notin_image_Key [simp] :"Hash X ∉ Key ` A"
by auto

lemma synth_analz_mono: "G⊆H ⟹ synth (analz(G)) ⊆ synth (analz(H))"
by (iprover intro: synth_mono analz_mono)

lemma synth_parts_mono: "G⊆H ⟹ synth (parts G) ⊆ synth (parts H)"
by (iprover intro: synth_mono parts_mono)

lemma Fake_analz_eq [simp]:
  "X ∈ 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 add: )
apply (rule synth_analz_mono, blast)
done

text ‹Two generalizations of @{text analz_insert_eq}›
lemma gen_analz_insert_eq [rule_format]:
  "X ∈ analz H ⟹ ALL G. H ⊆ 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 ∈ synth (analz H) ⟹ parts{X} ⊆ synth (analz H) ∪ 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 ‹For some reason, moving this up can make some proofs loop!›
declare invKey_K [simp]


lemma synth_analz_insert:
  assumes "analz H ⊆ synth (analz H')"
  shows "analz (insert X H) ⊆ synth (analz (insert X H'))"
proof
  fix x
  assume "x ∈ analz (insert X H)"
  then have "x ∈ analz (insert X (synth (analz H')))"
    using assms by (meson analz_increasing analz_monotonic insert_mono)
  then show "x ∈ synth (analz (insert X H'))"
    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 ⊆ synth (parts H')"
  shows "parts (insert X H) ⊆ synth (parts (insert X H'))"
proof
  fix x
  assume "x ∈ parts (insert X H)"
  then have "x ∈ 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 ∈ 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:
  "⟦x ∈ parts (insert a G); x ∈ parts G ⟹ x ∈ synth (parts H); a ∈ synth (parts H)⟧
    ⟹ x ∈ 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:
  "⟦A ⊆ synth (parts B); x ∈ parts A⟧ ⟹ x ∈ synth (parts B)"
by (meson parts_emptyE parts_insert_subset_impl parts_singleton subset_iff)

lemma synth_parts_subset:
  "A ⊆ synth (parts B) ⟹ parts A ⊆ 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 ⊆ synth (parts B)" and "B ⊆ synth (parts C)"
  shows "A ⊆ synth (parts C)"
using assms by (metis order_trans parts_synth_parts synth_idem synth_parts_mono)

lemma synth_parts_trans_elem:
  assumes "x ∈ A" and "A ⊆ synth (parts B)" and "B ⊆ synth (parts C)"
  shows "x ∈ synth (parts C)"
using synth_parts_trans assms by auto

lemma synth_un_parts_split:
  assumes "x ∈ synth (parts A ∪ parts B)"
    and "⋀x . x ∈ A ⟹ x ∈ synth (parts C)"
    and "⋀x . x ∈ B ⟹ x ∈ synth (parts C)"
  shows "x ∈ synth (parts C)"
proof -
  have "parts A ⊆ synth (parts C)" "parts B ⊆ synth (parts C)"
    using assms(2) assms(3) synth_parts_subset by blast+
  then have "x ∈ synth (synth (parts C) ∪ synth (parts C))" using assms(1)
    using synth_trans by auto
  then show ?thesis by auto
qed


subsubsection ‹Normalization of Messages›
text‹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.›


inductive normalized :: "msgterm ⇒ bool" where
    ε  [simp,intro!]:    "normalized ε"
  | 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]:      "⟦ ⋀x . x ∈ set xs ⟹ normalized x ⟧ ⟹ normalized (L xs)"
  | FSt [intro]:      "⟦ ⋀x . x ∈ fset xs ⟹ normalized x;
                         ⋀x ys . x ∈ fset xs ⟹ x ≠ FS ys ⟧
                      ⟹ normalized (FS xs)"
  | Hash   [intro]:   "normalized X ⟹ normalized (Hash X)"
  | MPair  [intro]:   "⟦ normalized X; normalized Y ⟧ ⟹ normalized ⟨X,Y⟩"
  | Crypt  [intro]:   "⟦ normalized X ⟧ ⟹ normalized (Crypt K X)"

thm normalized.simps
find_theorems normalized

text‹Examples›
lemma "normalized (FS {| Hash (FS {| Num 0 |}), Num 0 |})" by fastforce
lemma "¬ normalized (FS {| FS {| Num 0 |}, Num 0 |})" by (auto elim: normalized.cases)


subsubsection‹Closure of @{text "normalized"} under @{text "parts"}, @{text "analz"} and @{text "synth"}›

text‹All synthesized terms are normalized (since @{text "synth"} prevents directly nested FSets).›
lemma normalized_synth[elim!]: "⟦t ∈ synth H; ⋀t. t ∈ H ⟹ normalized t⟧ ⟹ normalized t"
  by(induction t, auto 3 4)

lemma normalized_parts[elim!]: "⟦t ∈ parts H; ⋀t. t ∈ H ⟹ normalized t⟧ ⟹ normalized t"
  by(induction t rule: parts.induct)
    (auto elim: normalized.cases)

lemma normalized_analz[elim!]: "⟦t ∈ analz H; ⋀t. t ∈ H ⟹ normalized t⟧ ⟹ normalized t"
  by(induction t rule: analz.induct)
    (auto elim: normalized.cases)

subsubsection‹Properties of @{text "normalized"}›

lemma normalized_FS[elim]: "⟦normalized (FS xs); x |∈| xs⟧ ⟹ normalized x"
  by(auto simp add: normalized.simps[of "FS xs"])

lemma normalized_FS_FS[elim]: "⟦normalized (FS xs); x |∈| xs; x = FS ys⟧ ⟹ False"
  by(auto simp add: normalized.simps[of "FS xs"])

lemma normalized_subset: "⟦normalized (FS xs); ys |⊆| xs⟧ ⟹ normalized (FS ys)"
  by (auto intro!: normalized.FSt)

lemma normalized_insert[elim!]: "normalized (FS (finsert x xs)) ⟹ normalized (FS xs)"
  by(auto elim!: normalized_subset)

lemma normalized_union:
  assumes "normalized (FS xs)" "normalized (FS ys)" "zs |⊆| xs |∪| ys"
  shows "normalized (FS zs)"
  using assms by(auto intro!: normalized.FSt)

lemma normalized_minus[elim]:
  assumes "normalized (FS (ys |-| xs))" "normalized (FS xs)"
  shows "normalized (FS ys)"
  using normalized_union assms by blast


subsubsection‹Lemmas that do not use @{text "normalized"}, but are helpful in proving its properties›
lemma FS_mono: "⟦zs_s = finsert (f (FS zs_s)) zs_b; ⋀ x. size (f x) > size x⟧ ⟹ False"
  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: "⟦zs = f (FS {|zs|}); ⋀ x. size (f x) > size x⟧ ⟹ False"
  using FS_mono by blast


end