import Init.Data.Nat.Lemmas
import Init.Prelude
import Mathlib.Data.Nat.Basic
import Mathlib.Data.Nat.Dist
import Mathlib.Data.Set.Basic
import Mathlib.Data.Set.Defs
import Mathlib.Data.Set.Image
import Mathlib.Data.Set.Insert
import Mathlib.Data.Set.Lattice
import Mathlib.Order.Closure
import Mathlib.Order.Lattice
import Mathlib.Tactic.ApplyAt
import Mathlib.Tactic.SimpIntro
import Mathlib.Tactic.NthRewrite

-- Keys are integers
abbrev Key := Nat

-- Define constants
def all_symmetric : Bool := true -- true if all keys are symmetric

-- Define the inverse of a symmetric key
def invKey : Key → Key := fun k => k -- Placeholder definition

-- Specification for invKey
axiom invKey_spec : ∀ K : Key, invKey (invKey K) = K
axiom invKey_symmetric : all_symmetric → invKey = id

-- Define the set of symmetric keys
@[grind]
def symKeys : Set Key := { K | invKey K = K }

-- Define the datatype for agents
@[grind]
inductive Agent
  | Server : Agent
  | Friend : Nat → Agent
  | Spy : Agent

@[grind]
inductive Msg
  | Agent : Agent → Msg -- Agent names
  | Number : Nat → Msg -- Ordinary integers, timestamps, ...
  | Nonce : Nat → Msg -- Unguessable nonces
  | Key : Key → Msg -- Crypto keys
  | Hash : Msg → Msg -- Hashing
  | MPair : Msg → Msg → Msg -- Compound messages
  | Crypt : Key → Msg → Msg -- Encryption, public- or shared-key

namespace Msg
-- Define concrete syntax for message tuples
notation "⦃" x ", " y "⦄" => MPair x y
notation "⦃" x ", " y ", " z "⦄" => MPair x (MPair y z)
end Msg

open Msg
open Agent
-- Define HPair
def HPair (X Y : Msg) : Msg :=
  ⦃Hash ⦃X, Y⦄, Y⦄

notation "⦃" x ", " y "⦄ₕ" => HPair x y

-- Define keysFor
@[simp]
def keysFor (H : Set Msg) : Set Key :=
  invKey '' { K | ∃ X, Crypt K X ∈ H }

-- Define the inductive set `parts`
@[grind]
inductive parts (H : Set Msg) : Set Msg
  | inj {X : Msg} : X ∈ H → parts H X
  | fst {X Y : Msg} : ⦃X, Y⦄ ∈ parts H → parts H X
  | snd {X Y : Msg} : ⦃X, Y⦄ ∈ parts H → parts H Y
  | body {K : Key} {X : Msg} : Crypt K X ∈ parts H → parts H X

-- Monotonicity lemmas

/--
An `apply` tactic that also calls the assumptions
-/
syntax "aapply" term  : tactic
macro_rules
  |`(tactic| aapply $l:term) => `(tactic| apply $l <;> try assumption)

@[simp]
lemma parts_mono: Monotone parts := by
  intro _ _ h _ a
  induction a
  · apply parts.inj; aapply h
  · aapply parts.fst
  · aapply parts.snd
  · aapply parts.body

-- Equations for injective constructors
@[simp]
lemma Friend_image_eq {A : Set Nat} {x : Nat} :
  ((Friend x) ∈ Friend '' A) = (x ∈ A) := by
  simp

@[simp]
lemma Key_image_eq {A : Set Key} {x : Key} :
  (Key x ∈ Key '' A) = (x ∈ A) := by
  simp

@[simp]
lemma Nonce_Key_image_eq {A : Set Key} {x : Nat} :
  (Nonce x ∉ Key '' A) := by
  simp

-- Lemma: Inverse of keys
@[simp]
lemma invKey_eq (K K' : Key) : (invKey K = invKey K') ↔ (K = K') := by
  apply Iff.intro
  case mp =>
    intro h
    rw [←invKey_spec K, ←invKey_spec K', h]
  case mpr =>
    intro h
    rw [h]

-- Lemmas for the `keysFor` operator
@[simp]
lemma keysFor_empty : keysFor ∅ = ∅ := by
  simp

@[simp]
lemma keysFor_union (H H' : Set Msg) : keysFor (H ∪ H') = keysFor H ∪ keysFor H' := by
  simp
  ext
  constructor
  · intro h; simp_all; grind
  · intro h; simp_all; grind

-- Monotonicity
@[simp]
lemma keysFor_mono: Monotone keysFor := by
  simp_intro _ _ sub _ h
  rcases h with ⟨K, ⟨⟨X, _⟩, _⟩⟩ ; exists K; apply And.intro
  · exists X; aapply sub
  · assumption

-- Lemmas for `keysFor` with specific message types
@[simp]
lemma keysFor_insert_Agent (A : Agent) (H : Set Msg) :
    keysFor (insert (Agent A) H) = keysFor H := by
  simp

@[simp]
lemma keysFor_insert_Nonce (N : Nat) (H : Set Msg) :
    keysFor (insert (Nonce N) H) = keysFor H := by
  simp

@[simp]
lemma keysFor_insert_Number (N : Nat) (H : Set Msg) :
    keysFor (insert (Msg.Hash (Nonce N)) H) = keysFor H := by
  simp

@[simp]
lemma keysFor_insert_Key (K : Key) (H : Set Msg) :
    keysFor (insert (Key K) H) = keysFor H := by
  simp

@[simp]
lemma keysFor_insert_Hash (X : Msg) (H : Set Msg) :
    keysFor (insert (Hash X) H) = keysFor H := by
  simp

@[simp]
lemma keysFor_insert_MPair (X Y : Msg) (H : Set Msg) :
    keysFor (insert ⦃X, Y⦄ H) = keysFor H := by
  simp

@[simp]
lemma keysFor_insert_Crypt (K : Key) (X : Msg) (H : Set Msg) :
    keysFor (insert (Crypt K X) H) = insert (invKey K) (keysFor H) := by
  simp[insert,Set.insert,invKey]
  ext
  grind

@[simp]
lemma keysFor_image_Key (E : Set Key) : keysFor (Key '' E) = ∅ := by
  simp

@[simp]
lemma Crypt_imp_invKey_keysFor (K : Key) (X : Msg) (H : Set Msg) :
    Crypt K X ∈ H → invKey K ∈ keysFor H := by
  intro h
  simp
  exact ⟨_, h⟩

-- MPair_parts lemma
@[simp]
lemma MPair_parts {H : Set Msg} {X Y : Msg} { P : Prop} :
  ⦃X, Y⦄ ∈ parts H → (parts H X  → parts H Y → P) → P :=
by
  grind

-- parts_increasing lemma
@[simp]
lemma parts_increasing {H : Set Msg} : H ⊆ parts H :=
  λ _ hx => parts.inj hx

-- parts_empty_aux lemma
@[simp]
lemma parts_empty_aux {X : Msg} : parts ∅ X → False :=
by
  intro h
  induction h <;> assumption

-- parts_empty lemma
@[simp]
lemma parts_empty : parts ∅ = ∅ :=
  Set.eq_empty_of_forall_notMem @parts_empty_aux

-- parts_emptyE lemma
lemma parts_emptyE {X : Msg} {P: Prop} : X ∈ parts ∅ → P :=
  λ h => False.elim (parts_empty_aux h)

-- parts_singleton lemma
lemma parts_singleton {H : Set Msg} {X : Msg} :
  X ∈ parts H → ∃ Y ∈ H, X ∈ parts {Y} :=
by
  intro h
  induction h with
  | inj h => exact ⟨_, h, parts.inj (Set.mem_singleton _)⟩
  | fst _ ih => rcases ih with ⟨Z, ⟨l, r⟩⟩; exists Z; and_intros; apply l; apply parts.fst; exact r
  | snd _ ih => rcases ih with ⟨Z, ⟨l, r⟩⟩; exists Z; and_intros; apply l; apply parts.snd; exact r
  | body _ ih => rcases ih with ⟨Z, ⟨l, r⟩⟩; exists Z; and_intros; apply l; apply parts.body; exact r

-- parts_union lemma
@[simp]
lemma parts_union {G H : Set Msg} : parts (G ∪ H) = parts G ∪ parts H :=
by
  apply Set.ext
  intro X
  constructor
  · intro h
    induction h with
    | inj h => cases h with
      | inl hG => exact Or.inl (parts.inj hG)
      | inr hH => exact Or.inr (parts.inj hH)
    | fst h ih => cases ih with
      | inl hG => exact Or.inl (parts.fst hG)
      | inr hH => exact Or.inr (parts.fst hH)
    | snd h ih => cases ih with
      | inl hG => exact Or.inl (parts.snd hG)
      | inr hH => exact Or.inr (parts.snd hH)
    | body h ih => cases ih with
      | inl hG => exact Or.inl (parts.body hG)
      | inr hH => exact Or.inr (parts.body hH)
  · intro h
    cases h with
    | inl hG => induction hG with
      | inj hG => exact parts.inj (Or.inl hG)
      | fst h ih => exact parts.fst ih
      | snd h ih => exact parts.snd ih
      | body h ih => exact parts.body ih
    | inr hH => induction hH with
      | inj hH => exact parts.inj (Or.inr hH)
      | fst h ih => exact parts.fst ih
      | snd h ih => exact parts.snd ih
      | body h ih => exact parts.body ih

-- parts_insert lemma
@[simp]
lemma parts_insert {X : Msg} {H : Set Msg} :
  parts (insert X H) = parts {X} ∪ parts H :=
by
  rw [Set.insert_eq, parts_union]

-- parts_insert2 lemma
@[simp]
lemma parts_insert2 {X Y : Msg} {H : Set Msg} :
  parts (insert X (insert Y H)) = parts {X} ∪ parts {Y} ∪ parts H :=
by
rw [Set.insert_eq, Set.insert_eq, parts_union, parts_union]
grind

-- parts_image lemma
@[simp]
lemma parts_image {f : Msg → Msg} {A : Set Msg} :
  parts (f '' A) = ⋃ x ∈ A, parts {f x} :=
by
  apply Set.ext
  intro X
  constructor
  · intro h
    induction h with
    | inj h => rcases h with ⟨a, ha, rfl⟩; exact Set.mem_biUnion ha (parts.inj (Set.mem_singleton _))
    | fst _ ih => simp_all; rcases ih with ⟨W, ⟨_, r⟩⟩; apply parts.fst at r; exists W;
    | snd _ ih => simp_all; rcases ih with ⟨W, ⟨_, r⟩⟩; apply parts.snd at r; exists W;
    | body _ ih => simp_all; rcases ih with ⟨K, ⟨_, r⟩⟩; apply parts.body at r; exists K;
  · intro h
    simp_all
    rcases h with ⟨W, ⟨_, r⟩⟩; induction r with
      | inj a => simp_all; apply parts.inj; exists W;
      | fst _ ih => exact parts.fst ih
      | snd _ ih => exact parts.snd ih
      | body _ ih => exact parts.body ih

-- parts_insert_subset lemma
@[simp]
lemma parts_insert_subset {X : Msg} {H : Set Msg} :
  insert X (parts H) ⊆ parts (insert X H) :=
by
  intro x hx
  cases hx with
  | inl h => simp_all; left; apply parts.inj; simp;
  | inr h => induction h with
    | inj h => exact parts.inj (Set.mem_insert_of_mem _ h)
    | fst h ih => exact parts.fst ih
    | snd h ih => exact parts.snd ih
    | body h ih => exact parts.body ih


-- Idempotence and transitivity lemmas for `parts`
@[simp]
lemma parts_partsD {H : Set Msg} : parts (parts H) ⊆ parts H :=
by
  intro x h
  induction h
  · assumption
  · aapply parts.fst
  · aapply parts.snd
  · aapply parts.body

abbrev partsClosureOperator : ClosureOperator (Set Msg) :=
  ClosureOperator.mk' parts parts_mono @parts_increasing @parts_partsD

@[simp]
lemma parts_idem {H : Set Msg} : parts (parts H) = parts H :=
  by apply partsClosureOperator.idempotent

@[simp]
lemma parts_subset_iff {G H : Set Msg} : (G ⊆ parts H) ↔ (parts G ⊆ parts H) :=
by apply partsClosureOperator.le_closure_iff

@[simp]
lemma parts_trans {G H : Set Msg} {X : Msg} :
  X ∈ parts G → G ⊆ parts H → X ∈ parts H :=
by intro a b; apply parts_mono at b; rw[parts_idem] at b; apply b; apply a;

-- Cut lemma
@[simp]
lemma parts_cut {G H : Set Msg} {X Y : Msg} :
  Y ∈ parts (insert X G) → X ∈ parts H → Y ∈ parts (G ∪ H) :=
by
  intro a b; rw[parts_union]; rw[parts_insert] at a; cases a <;> grind[parts_trans]
  
@[simp]
lemma parts_cut_mono {G H : Set Msg} {X : Msg} :
  X ∈ parts H → parts (insert X G) ⊆ parts (G ∪ H) :=
by grind[parts_cut]

@[simp]
lemma parts_insert_Agent {H : Set Msg} {agt : Agent} :
  parts (insert (Agent agt) H) = insert (Agent agt) (parts H) :=
by
  ext
  constructor
  · intro h; rw[parts_insert] at h; cases h with
    | inl h => induction h with
      | inj => simp_all
      | fst _ a_ih => cases a_ih; contradiction; right; aapply parts.fst
      | snd _ a_ih => cases a_ih; contradiction; right; aapply parts.snd
      | body _ a_ih => cases a_ih; contradiction; right; aapply parts.body
    | inr h => right; assumption
  · apply parts_insert_subset

@[simp]
lemma parts_insert_Nonce {H : Set Msg} {N : Nat} :
  parts (insert (Nonce N) H) = insert (Nonce N) (parts H) :=
by
  ext
  constructor
  · intro h; rw[parts_insert] at h; cases h with
    | inl h => induction h with
      | inj => simp_all
      | fst _ a_ih => cases a_ih; contradiction; right; aapply parts.fst
      | snd _ a_ih => cases a_ih; contradiction; right; aapply parts.snd
      | body _ a_ih => cases a_ih; contradiction; right; aapply parts.body
    | inr h => right; assumption
  · apply parts_insert_subset

@[simp]
lemma parts_insert_Number {H : Set Msg} {N : Nat} :
  parts (insert (Number N) H) = insert (Number N) (parts H) :=
by
  ext
  constructor
  · intro h; rw[parts_insert] at h; cases h with
    | inl h => induction h with
      | inj => simp_all
      | fst _ a_ih => cases a_ih; contradiction; right; aapply parts.fst
      | snd _ a_ih => cases a_ih; contradiction; right; aapply parts.snd
      | body _ a_ih => cases a_ih; contradiction; right; aapply parts.body
    | inr h => right; assumption
  · apply parts_insert_subset

@[simp]
lemma parts_insert_Key {H : Set Msg} {K : Key} :
  parts (insert (Key K) H) = insert (Key K) (parts H) :=
by
  ext
  constructor
  · intro h; rw[parts_insert] at h; cases h with
    | inl h => induction h with
      | inj => simp_all
      | fst _ a_ih => cases a_ih; contradiction; right; aapply parts.fst
      | snd _ a_ih => cases a_ih; contradiction; right; aapply parts.snd
      | body _ a_ih => cases a_ih; contradiction; right; aapply parts.body
    | inr h => right; assumption
  · apply parts_insert_subset

@[simp]
lemma parts_insert_Hash {H : Set Msg} {X : Msg} :
  parts (insert (Hash X) H) = insert (Hash X) (parts H) :=
by
  ext
  constructor
  · intro h; rw[parts_insert] at h; cases h with
    | inl h => induction h with
      | inj => simp_all
      | fst _ a_ih => cases a_ih; contradiction; right; aapply parts.fst
      | snd _ a_ih => cases a_ih; contradiction; right; aapply parts.snd
      | body _ a_ih => cases a_ih; contradiction; right; aapply parts.body
    | inr h => right; assumption
  · apply parts_insert_subset

@[simp]
lemma parts_insert_Crypt {H : Set Msg} {K : Key} {X : Msg} :
  parts (insert (Crypt K X) H) = insert (Crypt K X) (parts (insert X H)) :=
by
  ext x
  constructor
  · intro h; rw[parts_insert] at h; cases h with
    | inl h => induction h with
      | inj => left; assumption;
      | fst _ a_ih => cases a_ih; contradiction; right; aapply parts.fst
      | snd _ a_ih => cases a_ih; contradiction; right; aapply parts.snd
      | body _ a_ih => cases a_ih with
        | inl => simp_all; right; left; apply parts_increasing; trivial;
        | inr h => apply parts.body at h; right; exact h;
    | inr => right; simp; right; assumption;
  · intro h; cases h with
    | inl => apply parts.inj; left; assumption
    | inr h => 
      apply (parts_cut (G := H) (H := {Crypt K X}) (X := X) (Y := x)) at h 
      rw[←Set.singleton_union, Set.union_comm]
      apply h
      apply parts.body (K := K) (X := X)
      apply parts.inj
      trivial
      
@[simp]
lemma parts_insert_MPair {H: Set Msg} {X Y : Msg} :
  parts (insert ⦃X, Y⦄ H) = insert ⦃X, Y⦄ (parts (insert X (insert Y H))) :=
by 
  ext x
  constructor;
  · intro h; rw[parts_insert] at h; cases h with
    | inl h => induction h with
      | inj => simp_all;
      | @fst A B _ a_ih => cases a_ih with
        | inl h => cases h; right; apply parts.inj; left; trivial
        | inr h => right; aapply parts.fst;
      | @snd A B _ a_ih => cases a_ih with
        | inl h => cases h; right; apply parts.inj; right; left; trivial;
        | inr h => right; aapply parts.snd;
      | body _ a_ih => cases a_ih; contradiction; right; aapply parts.body
    | inr h => simp; right; right; right; assumption;
  · intro h; cases h with
    | inl => rw[parts_insert]; left; apply parts.inj; assumption;
    | inr h => simp_all; cases h with
      | inl h => 
        left;
        apply parts_trans ( H := {⦃X, Y⦄}) at h;
        simp at h;
        apply h;
        apply parts.fst;
        apply parts.inj;
        trivial;
      | inr h => cases h with
        | inl h => 
            left;
            apply parts_trans ( H := {⦃X, Y⦄}) at h;
            simp at h;
            apply h;
            apply parts.snd;
            apply parts.inj;
            trivial;
        | inr => right; assumption;

@[simp]
lemma parts_image_Key {N : Set Key} : parts (Key '' N) = Key '' N :=
by 
  ext
  constructor
  · intro a; simp; induction a <;> simp_all;
  · simp; intro y _ _; apply parts.inj; simp; exists y;

-- In any message, there is an upper bound N on its greatest nonce.
lemma msg_Nonce_supply {msg : Msg} : ∃ N, ∀ n, N ≤ n → Nonce n ∉ parts {msg} :=
by
  induction msg with
  | Agent a => exists 0;
               have ins_agt := parts_insert_Agent (H := {}) (agt := a);
               simp_all
  | Number a => exists 0;
                have ins_number := parts_insert_Number (H := {}) (N := a);
                simp_all;
  | Nonce n => exists n.succ;
               intro _ _ _;
               have ins_nonce := parts_insert_Nonce (H := {}) (N := n);
               simp_all;
  | Key k => exists 0;
             have ins_key := parts_insert_Key (H := {}) (K := k);
             simp_all;
  | Hash X ih => exists 0;
                 have ins_hash := parts_insert_Hash (H := {}) (X := X);
                 simp_all;
  | MPair X Y ihX ihY =>
    rcases ihX with ⟨wX, hH⟩;
    cases ihY with
    | intro wY hY => exists Nat.max wX wY; intro n h₁ h₂;
                     have ins_mpair := parts_insert_MPair (H := {}) (X := X) (Y := Y);
                     simp_all;
  | Crypt K X ih => rcases ih with ⟨N, h⟩; exists N;
                    have ins_crypt := parts_insert_Crypt (H := {}) (K := K) (X := X);
                    simp_all;

-- Inductive relation "analz"
inductive analz (H : Set Msg) : Set Msg
  | inj {X : Msg} : X ∈ H → analz H X
  | fst {X Y : Msg} : ⦃X, Y⦄ ∈ analz H → analz H X
  | snd {X Y : Msg} : ⦃X, Y⦄ ∈ analz H → analz H Y
  | decrypt {K : Key} {X : Msg} :
      Crypt K X ∈ analz H → Key (invKey K) ∈ analz H → analz H X

-- Monotonicity
lemma analz_mono : Monotone analz :=
by 
  intro A B h₁ X h₂
  induction h₂ with
  | inj h => exact analz.inj (h₁ h)
  | fst h ih => exact analz.fst ih
  | snd h ih => exact analz.snd ih
  | decrypt h₁ h₂ ih₁ ih₂ => exact analz.decrypt ih₁ ih₂

-- Making it safe speeds up proofs
@[simp]
lemma MPair_analz {H : Set Msg} {X Y : Msg} {P : Prop} :
  ⦃X, Y⦄ ∈ analz H → (analz H X → analz H Y → P) → P :=
by
  intro h ih
  apply ih
  · apply analz.fst h
  · apply analz.snd h

@[simp]
lemma analz_increasing {H : Set Msg} : H ⊆ analz H :=
  λ _ hx => analz.inj hx

lemma analz_into_parts {H : Set Msg} {X : Msg} : X ∈ analz H → X ∈ parts H :=
by
  intro h
  induction h with
  | inj h => aapply parts.inj
  | fst _ ih => aapply parts.fst
  | snd _ ih => aapply parts.snd
  | decrypt _ _ ih₁ => aapply parts.body

lemma analz_subset_parts {H : Set Msg} : analz H ⊆ parts H :=
  λ _ hx => analz_into_parts hx

@[simp]
lemma analz_parts {H : Set Msg} : analz (parts H) = parts H :=
by
  ext X; constructor
  · intro h; induction h with
    | inj => assumption;
    | fst => aapply parts.fst;
    | snd => aapply parts.snd;
    | decrypt => aapply parts.body;
  · apply analz_increasing;

lemma not_parts_not_analz {H : Set Msg} {X : Msg} :
  X ∉ parts H → X ∉ analz H :=
  λ h₁ h₂ => h₁ (analz_into_parts h₂)

@[simp]
lemma parts_analz {H : Set Msg} : parts (analz H) = parts H :=
  by 
    ext; constructor;
    · intro h; induction h with
      | inj => aapply analz_subset_parts
      | fst => aapply parts.fst
      | snd => aapply parts.snd
      | body => aapply parts.body
    · apply parts_mono; apply analz_increasing;

@[simp]
lemma analz_insertI {X : Msg} {H : Set Msg} :
  insert X (analz H) ⊆ analz (insert X H) :=
by
  intro x hx
  cases hx with
  | inl h => apply analz.inj; left; assumption;
  | inr h => exact analz_mono (Set.subset_insert _ _) h

-- General equational properties

@[simp]
lemma analz_empty : analz ∅ = ∅ :=
by 
  ext; constructor;
  · intro h; induction h <;> contradiction;
  · apply analz_increasing


@[simp]
lemma analz_union {G H : Set Msg} : analz G ∪ analz H ⊆ analz (G ∪ H) :=
  by
    intro x hx
    cases hx with
    | inl hG => exact analz_mono (Set.subset_union_left) hG; 
    | inr hH => exact analz_mono (Set.subset_union_right) hH

lemma analz_insert {X : Msg} {H : Set Msg} :
  insert X (analz H) ⊆ analz (insert X H) :=
  by
    intro x hx
    cases hx with
    | inl h => apply analz.inj; left; assumption
    | inr h => exact analz_mono (Set.subset_insert _ _) h

-- Rewrite rules for pulling out atomic messages

@[simp]
lemma analz_insert_Agent {H : Set Msg} {agt : Agent} :
  analz (insert (Agent agt) H) = insert (Agent agt) (analz H) :=
  by
    ext
    constructor
    · intro h
      induction h with
      | inj h => cases h with
        | inl h => exact Or.inl h
        | inr h => exact Or.inr (analz.inj h)
      | fst _ ih => right; cases ih; contradiction; aapply analz.fst;
      | snd _ ih => right; cases ih; contradiction; aapply analz.snd;
      | decrypt _ _ ih₁ ih₂ => right; cases ih₁; contradiction;
                               cases ih₂; contradiction;
                               aapply analz.decrypt;
    · apply analz_insert

@[simp]
lemma analz_insert_Nonce {H : Set Msg} {N : Nat} :
  analz (insert (Nonce N) H) = insert (Nonce N) (analz H) :=
  by
    ext
    constructor
    · intro h
      induction h with
      | inj h => cases h with
        | inl h => exact Or.inl h
        | inr h => exact Or.inr (analz.inj h)
      | fst _ ih => right; cases ih; contradiction; aapply analz.fst;
      | snd _ ih => right; cases ih; contradiction; aapply analz.snd;
      | decrypt _ _ ih₁ ih₂ => right; cases ih₁; contradiction;
                               cases ih₂; contradiction;
                               aapply analz.decrypt;
    · apply analz_insert

@[simp]
lemma analz_insert_Number {H : Set Msg} {N : Nat} :
  analz (insert (Number N) H) = insert (Number N) (analz H) :=
  by
    ext
    constructor
    · intro h
      induction h with
      | inj h => cases h with
        | inl h => exact Or.inl h
        | inr h => exact Or.inr (analz.inj h)
      | fst _ ih => right; cases ih; contradiction; aapply analz.fst;
      | snd _ ih => right; cases ih; contradiction; aapply analz.snd;
      | decrypt _ _ ih₁ ih₂ => right; cases ih₁; contradiction;
                               cases ih₂; contradiction;
                               aapply analz.decrypt;
    · apply analz_insert

@[simp]
lemma analz_insert_Hash {H : Set Msg} {X : Msg} :
  analz (insert (Hash X) H) = insert (Hash X) (analz H) :=
  by
    ext
    constructor
    · intro h
      induction h with
      | inj h => cases h with
        | inl h => exact Or.inl h
        | inr h => exact Or.inr (analz.inj h)
      | fst _ ih => right; cases ih; contradiction; aapply analz.fst;
      | snd _ ih => right; cases ih; contradiction; aapply analz.snd;
      | decrypt _ _ ih₁ ih₂ => right; cases ih₁; contradiction;
                               cases ih₂; contradiction;
                               aapply analz.decrypt;
    · apply analz_insert

@[simp]
lemma analz_insert_Key {H : Set Msg} {K : Key} :
  K ∉ keysFor (analz H) →
  analz (insert (Key K) H) = insert (Key K) (analz H) :=
  by
    intro hK
    ext x
    constructor
    · intro h
      induction h with
      | inj h => cases h with
        | inl h => exact Or.inl h
        | inr h => exact Or.inr (analz.inj h)
      | fst _ ih => right; cases ih; contradiction; aapply analz.fst;
      | snd _ ih => right; cases ih; contradiction; aapply analz.snd;
      | @decrypt _ _ _ _ ih₁ ih₂ =>
      right
      cases ih₂ with
      | inl h => simp at h; simp at ih₁; apply Crypt_imp_invKey_keysFor at ih₁
                 rw[h] at ih₁; contradiction;
      | inr => cases ih₁; simp_all; aapply analz.decrypt
    · apply analz_insert

@[simp]
lemma analz_insert_MPair {H : Set Msg} {X Y : Msg} :
  analz (insert ⦃X, Y⦄ H) = insert ⦃X, Y⦄ (analz (insert X (insert Y H))) :=
  by
    ext
    constructor
    · intro h
      induction h with
      | inj h => cases h with
        | inl h => exact Or.inl h
        | inr => right; apply analz.inj; right; right; assumption
      | fst _ ih => right; cases ih
                    · simp_all; apply analz.inj; left; trivial
                    · aapply analz.fst
      | snd _ ih => right; cases ih
                    · simp_all; apply analz.inj; right; left; trivial
                    · aapply analz.snd
      | decrypt h₁ h₂ ih₁ ih₂ =>
      right
      cases ih₂; contradiction
      cases ih₁; contradiction
      aapply analz.decrypt
    · intro h
      cases h with
      | inl => apply analz.inj; left; trivial
      | inr h => induction h with
        | inj a => cases a with
          | inl h => apply analz.fst; apply analz.inj; left; rw[h]
          | inr h => cases h with
            | inl h => apply analz.snd; apply analz.inj; left; rw[h]
            | inr => apply analz.inj; right; assumption
        | fst => aapply analz.fst
        | snd => aapply analz.snd
        | decrypt => aapply analz.decrypt

lemma analz_insert_Decrypt {H : Set Msg} {K : Key} {X : Msg} :
  Key (invKey K) ∈ analz H →
  analz (insert (Crypt K X) H) = insert (Crypt K X) (analz (insert X H)) :=
by
  intro
  ext
  constructor
  · intro h
    induction h with
    | inj h => cases h with
      | inl => left; assumption;
      | inr => right; apply analz.inj; right; assumption
    | fst _ ih => right; cases ih; contradiction; aapply analz.fst
    | snd _ ih => right; cases ih; contradiction; aapply analz.snd
    | decrypt _ _ ih₁ ih₂ => cases ih₁ with
      | inl h => right; apply analz.inj; left; simp_all
      | inr => right; cases ih₂; contradiction; aapply analz.decrypt
  · intro h
    cases h with
    | inl h => apply analz.inj; left; assumption
    | inr h => induction h with
      | inj a => cases a with
        | inl h => apply analz.decrypt; apply analz.inj; left; rw[h]
                   apply analz_mono; apply Set.subset_insert; assumption
        | inr => apply analz.inj; right; assumption
      | fst => aapply analz.fst
      | snd => aapply analz.snd
      | decrypt => aapply analz.decrypt

-- TODO split into two lemmata
@[simp]
lemma analz_Crypt {H : Set Msg} {K : Key} {X : Msg} :
  (Key (invKey K) ∉ analz H) →
  (analz (insert (Crypt K X) H) = insert (Crypt K X) (analz H)) :=
by
  intro h
  ext
  constructor
  · intro a; induction a with
    | inj a => cases a; left; assumption; right; aapply analz.inj
    | fst _ a_ih => cases a_ih; contradiction; right; aapply analz.fst
    | snd _ a_ih => cases a_ih; contradiction; right; aapply analz.snd
    | decrypt h₁ h₂ ih₁ ih₂ =>
    cases ih₂; contradiction 
    cases ih₁; simp_all; right; aapply analz.decrypt
  · intro a; cases a with
    | inl => apply analz.inj; left; assumption
    | inr => apply analz_mono; apply Set.subset_insert; assumption
          
-- This rule supposes "for the sake of argument" that we have the key.
lemma analz_insert_Crypt_subset {H : Set Msg} {K : Key} {X : Msg} :
  analz (insert (Crypt K X) H) ⊆ insert (Crypt K X) (analz (insert X H)) :=
by
  intro Y h
  induction h with
  | inj h => cases h with
    | inl => left; assumption
    | inr => right; apply analz.inj; right; assumption
  | fst _ ih => right; cases ih; contradiction; aapply analz.fst
  | snd _ ih => right; cases ih; contradiction; aapply analz.snd
  | decrypt _ _ ih₁ ih₂ =>
  right
  cases ih₂; contradiction
  cases ih₁ with
  | inl => simp_all; apply analz.inj; left; trivial
  | inr => aapply analz.decrypt

@[simp]
lemma analz_image_Key {N : Set Key} : analz (Key '' N) = Key '' N :=
by
  apply Set.ext
  intro X
  constructor
  · intro h
    induction h <;> simp_all
  · intro h
    rcases h with ⟨k, hk, rfl⟩
    exact analz.inj ⟨k, hk, rfl⟩

-- Idempotence and transitivity

@[simp]
lemma analz_analzD {H : Set Msg} {X : Msg} : X ∈ analz (analz H) → X ∈ analz H :=
by
  intro h
  induction h with
  | inj h => exact h
  | fst h ih => exact analz.fst ih
  | snd h ih => exact analz.snd ih
  | decrypt h₁ h₂ ih₁ ih₂ => exact analz.decrypt ih₁ ih₂
 
abbrev analzClosureOperator : ClosureOperator (Set Msg) :=
  ClosureOperator.mk' analz analz_mono @analz_increasing @analz_analzD

@[simp]
lemma analz_idem {H : Set Msg} : analz (analz H) = analz H :=
  by apply analzClosureOperator.idempotent

@[simp]
lemma analz_subset_iff {G H : Set Msg} : (G ⊆ analz H) ↔ (analz G ⊆ analz H) :=
  by apply analzClosureOperator.le_closure_iff

@[simp]
lemma analz_trans {G H : Set Msg} {X : Msg} :
  X ∈ analz G → G ⊆ analz H → X ∈ analz H :=
by
  intro hG hGH
  apply analz_mono at hGH; rw [ analz_idem ] at hGH; apply hGH; assumption;

-- Cut; Lemma 2 of Lowe
@[simp]
lemma analz_cut {H : Set Msg} {X Y : Msg} :
  Y ∈ analz (insert X H) → X ∈ analz H → Y ∈ analz H :=
by
  intro hY _
  apply analz_trans; apply hY
  intro a h; cases h; simp_all; aapply analz.inj

-- Simplification of messages involving forwarding of unknown components
@[simp]
lemma analz_insert_eq {H : Set Msg} {X : Msg} :
  X ∈ analz H → analz (insert X H) = analz H :=
by
  intro
  ext
  constructor
  · intro; aapply analz_cut
  · apply analz_mono; apply Set.subset_insert

-- A congruence rule for "analz"
@[simp]
lemma analz_subset_cong {G G' H H' : Set Msg} :
  analz G ⊆ analz G' → analz H ⊆ analz H' → analz (G ∪ H) ⊆ analz (G' ∪ H') :=
by
  intro hG hH
  have a_sub := analz_subset_iff (G := G ∪ H) (H := G' ∪ H')
  apply a_sub.mp
  apply subset_trans (b := analz G ∪ analz H)
  apply Set.union_subset_union (h₁ := @analz_increasing (H := G)) (h₂ := @analz_increasing (H := H))
  apply subset_trans (b := analz G' ∪ analz H')
  apply Set.union_subset_union (h₁ := hG) (h₂ := hH)
  apply analz_union

lemma analz_cong {G G' H H' : Set Msg} :
  analz G = analz G' → analz H = analz H' → analz (G ∪ H) = analz (G' ∪ H') :=
by
  intro hG hH
  ext
  constructor
  · apply analz_subset_cong; aapply Eq.subset; aapply Eq.subset
  · apply analz_subset_cong; rw[Eq.comm] at hG; aapply Eq.subset; rw[Eq.comm] at hH; aapply Eq.subset


lemma analz_insert_cong {H H' : Set Msg} {X : Msg} :
  analz H = analz H' → analz (insert X H) = analz (insert X H') :=
by
  intro hH
  rw [Set.insert_eq, Set.insert_eq]
  exact analz_cong rfl hH

-- If there are no pairs or encryptions, then analz does nothing
lemma analz_trivial {H : Set Msg} :
  (∀ X Y, ⦃X, Y⦄ ∉ H) → (∀ X K, Crypt K X ∉ H) → analz H = H :=
by
  intro hPairs hCrypts
  apply Set.ext
  intro X
  constructor
  · intro h
    induction h with
    | inj h => exact h
    | fst => simp_all
    | snd => simp_all
    | decrypt h₁ _ _ => simp_all
  · exact analz.inj

-- Inductive relation "synth"

inductive synth (H : Set Msg) : Set Msg
  | inj {X : Msg} : X ∈ H → synth H X
  | agent {agt : Agent} : synth H (Agent agt)
  | number {n : Nat} : synth H (Number n)
  | hash {X : Msg} : synth H X → synth H (Hash X)
  | mpair {X Y : Msg} : synth H X → synth H Y → synth H ⦃X, Y⦄
  | crypt {K : Key} {X : Msg} : synth H X → Key K ∈ H → synth H (Crypt K X)

-- Monotonicity
lemma synth_mono : Monotone synth := by
  intro _ _ h _ hx
  induction hx with
  | inj hG => exact synth.inj (h hG)
  | agent => exact synth.agent
  | number => exact synth.number
  | hash _ ih => exact synth.hash ih
  | mpair _ _ ihX ihY => exact synth.mpair ihX ihY
  | crypt => aapply synth.crypt; aapply h 

-- Simplification rules for `synth`
@[simp]
lemma synth_increasing {H : Set Msg} : H ⊆ synth H :=
  λ _ hx => synth.inj hx

-- Unions
lemma synth_union {G H : Set Msg} : synth G ∪ synth H ⊆ synth (G ∪ H) :=
by
  intro x hx
  cases hx with
  | inl hG => exact synth_mono (Set.subset_union_left) hG
  | inr hH => exact synth_mono (Set.subset_union_right) hH

lemma synth_insert {X : Msg} {H : Set Msg} :
  insert X (synth H) ⊆ synth (insert X H) :=
by
  intro x hx
  cases hx with
  | inl h => apply synth.inj; left; assumption
  | inr h => exact synth_mono (Set.subset_insert _ _) h

-- Idempotence and transitivity
@[simp]
lemma synth_synthD {H : Set Msg} {X : Msg} : X ∈ synth (synth H) → X ∈ synth H :=
by
  intro h
  induction h with
  | inj h => exact h
  | agent => exact synth.agent
  | number => exact synth.number
  | hash _ ih => exact synth.hash ih
  | mpair _ _ ihX ihY => exact synth.mpair ihX ihY
  | crypt _ a => cases a; aapply synth.crypt;
  
abbrev synthClosureOperator : ClosureOperator (Set Msg) :=
  ClosureOperator.mk' synth synth_mono @synth_increasing @synth_synthD

@[simp]
lemma synth_idem {H : Set Msg} : synth (synth H) = synth H :=
  by apply synthClosureOperator.idempotent

@[simp]
lemma synth_subset_iff {G H : Set Msg} : (G ⊆ synth H) ↔ (synth G ⊆ synth H) :=
by apply synthClosureOperator.le_closure_iff

@[simp, grind]
lemma synth_trans {G H : Set Msg} {X : Msg} :
  X ∈ synth G → G ⊆ synth H → X ∈ synth H :=
by
  intro hG hGH; apply synth_mono at hGH; rw[synth_idem] at hGH; apply hGH; apply hG

-- Cut; Lemma 2 of Lowe
@[simp]
lemma synth_cut {H : Set Msg} {X Y : Msg} :
  Y ∈ synth (insert X H) → X ∈ synth H → Y ∈ synth H :=
by
  intro hY hX; apply synth_trans; apply hY
  intro a h; cases h; simp_all; aapply synth.inj

@[simp]
lemma Crypt_synth_eq {H : Set Msg} {K : Key} {X : Msg} :
  Key K ∉ H → (Crypt K X ∈ synth H ↔ Crypt K X ∈ H) :=
by
  intro hK
  constructor
  · intro h
    cases h; assumption; contradiction
  · intro h
    exact synth.inj h

@[simp]
lemma keysFor_synth {H : Set Msg} :
  keysFor (synth H) = keysFor H ∪ invKey '' {K | Key K ∈ H} :=
by
  ext K
  simp
  constructor
  · intro h
    rcases h with ⟨Y, ⟨⟨X, h⟩, _⟩⟩;
    cases h with
    | inj h => left; exists Y; apply And.intro; exists X; assumption
    | crypt _ _ => right; exists Y
  · intro h; cases h with
  | inl h =>  cases h with
    | intro Y h =>
    exists Y; rcases h with ⟨⟨X, _⟩, _⟩;
    apply And.intro
    · exists X; aapply synth.inj
    · assumption
  | inr h =>
    rcases h with ⟨Y, ⟨_, _⟩⟩;
    exists Y; apply And.intro
    · exists Number 0; aapply synth.crypt; apply synth.number
    · assumption


-- Combinations of parts, analz, and synth

@[simp]
lemma parts_synth {H : Set Msg} : parts (synth H) = parts H ∪ synth H :=
by
  apply Set.ext
  intro X
  constructor
  · intro h
    induction h with
    | inj => right; assumption
    | fst _ ih => cases ih with
      | inl => left; aapply parts.fst
      | inr h => cases h
                 · left; apply parts.fst; aapply parts.inj; 
                 · right; assumption
    | snd _ ih => cases ih with
      | inl => left; aapply parts.snd
      | inr h => cases h
                 · left; apply parts.snd; aapply parts.inj; 
                 · right; assumption
    | body h ih => cases ih with
      | inl h => left; aapply parts.body
      | inr h => cases h
                 · left; aapply parts.body; aapply parts.inj
                 · right; assumption
  · intro h
    cases h with
    | inl h =>
    apply parts_mono
    · apply synth_increasing
    · assumption
    | inr h => exact parts.inj h

@[simp]
lemma analz_analz_Un {G H : Set Msg} : analz (analz G ∪ H) = analz (G ∪ H) :=
by
  apply analz_cong
  · exact analz_idem
  · trivial

@[simp]
lemma analz_synth_Un {G H : Set Msg} : analz (synth G ∪ H) = analz (G ∪ H) ∪ synth G :=
by
  ext
  constructor
  · intro h; induction h with
    | inj a => cases a
               · right; assumption
               · left; apply analz.inj; right; assumption
    | fst _ ih =>
    cases ih with
        | inl => left; aapply analz.fst
        | inr h => 
        cases h
        · left; apply analz.fst; apply analz.inj; left; assumption
        · right; assumption
    | snd _ ih => 
    cases ih with
        | inl => left; aapply analz.snd
        | inr h => 
        cases h
        · left; apply analz.snd; apply analz.inj; left; assumption
        · right; assumption
    | decrypt _ _ ih₁ ih₂ =>
    cases ih₂ with
    | inl => cases ih₁ with
      | inl => left; aapply analz.decrypt
      | inr h => cases h
                 · left; aapply analz.decrypt; apply analz.inj; left; assumption
                 · right; assumption
    | inr h => cases h; cases ih₁ with
      | inl => left; aapply analz.decrypt; apply analz.inj; left; assumption
      | inr h => cases h
                 · left; aapply analz.decrypt <;> (apply analz.inj; left; assumption)
                 · right; assumption
  · apply sup_le (a := analz (G ∪ H)) (b := synth G) (c := analz ( synth G ∪ H ))
    · apply analz_mono; apply Set.union_subset_union; apply synth_increasing; trivial
    · apply analz_subset_iff.mpr; apply analz_mono; exact le_sup_left

@[simp]
lemma analz_synth {H : Set Msg} : analz (synth H) = analz H ∪ synth H :=
  by have asu := analz_synth_Un (G := H) (H := ∅); simp_all

-- For reasoning about the Fake rule in traces

lemma parts_insert_subset_Un {G H : Set Msg} {X : Msg} :
  X ∈ G → parts (insert X H) ⊆ parts G ∪ parts H :=
by
  intro hX
  rw [Set.insert_eq, parts_union]
  apply Set.union_subset_union
  · apply parts_mono; simp_all
  · trivial

lemma Fake_parts_insert {H : Set Msg} {X : Msg} :
  X ∈ synth (analz H) → parts (insert X H) ⊆ synth (analz H) ∪ parts H :=
by
  intro hX
  rw [parts_insert]
  apply sup_le
  · apply subset_trans (b := synth (analz H) ∪ parts (analz H))
    · rw [Set.union_comm, ←parts_synth]; apply parts_mono; simp; assumption
    · rw [parts_analz]
  · apply le_sup_of_le_right; trivial

lemma Fake_parts_insert_in_Un {H : Set Msg} {X Z : Msg} :
  Z ∈ parts (insert X H) → X ∈ synth (analz H) → Z ∈ synth (analz H) ∪ parts H :=
by
  intro hZ hX
  exact Set.mem_of_subset_of_mem (Fake_parts_insert hX) hZ

lemma Fake_analz_insert {G H : Set Msg} {X : Msg} :
  X ∈ synth (analz G) → analz (insert X H) ⊆ synth (analz G) ∪ analz (G ∪ H) :=
by
  intro
  apply subset_trans (b := analz (synth (analz G) ∪ H))
  · apply analz_mono; rw[Set.insert_eq]; apply Set.union_subset_union; simp_all; trivial;
  · rw[analz_synth_Un, Set.union_comm, analz_analz_Un]

@[simp]
lemma analz_conj_parts {H : Set Msg} {X : Msg} :
  (X ∈ analz H ∧ X ∈ parts H) ↔ X ∈ analz H :=
  by
    constructor
    · intro h
      exact h.1
    · intro h
      exact ⟨h, analz_subset_parts h⟩

@[simp]
lemma analz_disj_parts {H : Set Msg} {X : Msg} :
  (X ∈ analz H ∨ X ∈ parts H) ↔ X ∈ parts H :=
  by
    constructor
    · intro h
      cases h with
      | inl h => apply analz_conj_parts.mpr at h; cases h; assumption
      | inr h => assumption
    · intro h
      exact Or.inr h

@[simp]
lemma MPair_synth_analz {H : Set Msg} {X Y : Msg} :
  ⦃X, Y⦄ ∈ synth (analz H) ↔ X ∈ synth (analz H) ∧ Y ∈ synth (analz H) :=
  by
    constructor
    · intro h; cases h
      · apply And.intro
        · apply synth.inj; aapply analz.fst
        · apply synth.inj; aapply analz.snd
      · apply And.intro <;> assumption
    · intro h; exact synth.mpair h.1 h.2

lemma Crypt_synth_analz {H : Set Msg} {K : Key} {X : Msg} :
  Key K ∈ analz H → Key (invKey K) ∈ analz H → ((Crypt K X ∈ synth (analz H)) ↔ X ∈ synth (analz H)) :=
  by
  intro _ _
  constructor
  · intro h; cases h
    · apply synth.inj; aapply analz.decrypt
    · assumption
  · intro _; aapply synth.crypt

@[simp]
lemma Hash_synth_analz {H : Set Msg} {X Y : Msg} :
  X ∉ synth (analz H) → ((Hash ⦃X, Y⦄ ∈ synth (analz H)) ↔ Hash ⦃X, Y⦄ ∈ analz H) :=
  by
  intro _
  constructor
  · intro h; cases h with
    | inj => assumption
    | hash h => cases h with
      | inj a => apply analz.fst at a; apply synth.inj at a; contradiction
      | mpair => contradiction
  · intro h; aapply synth.inj

-- HPair: a combination of Hash and MPair

-- Freeness

@[simp]
lemma Agent_neq_HPair {A : Agent} {X Y : Msg} : Agent A ≠ ⦃X, Y⦄ₕ :=
  by simp [HPair]

@[simp]
lemma Nonce_neq_HPair {N : Nat} {X Y : Msg} : Nonce N ≠ ⦃X, Y⦄ₕ :=
  by simp [HPair]

@[simp]
lemma Number_neq_HPair {N : Nat} {X Y : Msg} : Number N ≠ ⦃X, Y⦄ₕ :=
  by simp [HPair]

@[simp]
lemma Key_neq_HPair {K : Key} {X Y : Msg} : Key K ≠ ⦃X, Y⦄ₕ :=
  by simp [HPair]

@[simp]
lemma Hash_neq_HPair {Z X Y : Msg} : Hash Z ≠ ⦃X, Y⦄ₕ :=
  by simp [HPair]

@[simp]
lemma Crypt_neq_HPair {K : Key} {X' X Y : Msg} : Crypt K X' ≠ ⦃X, Y⦄ₕ :=
  by simp [HPair]

@[simp]
lemma HPair_eq {X' Y' X Y : Msg} : (⦃X', Y'⦄ₕ = ⦃X, Y⦄ₕ) ↔ (X' = X ∧ Y' = Y) :=
  by simp [HPair]

@[simp]
lemma MPair_eq_HPair {X' Y' X Y : Msg} : (⦃X', Y'⦄ = ⦃X, Y⦄ₕ) ↔ (X' = Hash ⦃X, Y⦄ ∧ Y' = Y) :=
  by simp [HPair]

@[simp]
lemma HPair_eq_MPair {X' Y' X Y : Msg} : (⦃X, Y⦄ₕ = ⦃X', Y'⦄) ↔ (X' = Hash ⦃X, Y⦄ ∧ Y' = Y) :=
  by simp [HPair]; nth_rw 1 [Eq.comm]; nth_rw 2 [Eq.comm]

-- Specialized laws, proved in terms of those for Hash and MPair

@[simp]
lemma keysFor_insert_HPair {H : Set Msg} {X Y : Msg} :
  keysFor (insert (⦃X, Y⦄ₕ) H) = keysFor H :=
  by simp [HPair]

@[simp]
lemma parts_insert_HPair {H : Set Msg} {X Y : Msg} :
  parts (insert (⦃X, Y⦄ₕ) H) = insert (⦃X, Y⦄ₕ) (insert (Hash ⦃X, Y⦄) (parts (insert Y H))) :=
by
  simp [HPair]; rw[←Set.union_empty (a:= {⦃Hash ⦃X, Y⦄, Y⦄}), ←Set.insert_eq, parts_insert_MPair, parts_insert_Hash]
  rw[Set.insert_eq, Set.insert_eq, Set.insert_eq, Set.insert_eq, Set.insert_eq]
  rw[Set.union_empty]; simp only [Set.union_assoc]

@[simp]
lemma analz_insert_HPair {H : Set Msg} {X Y : Msg} :
  analz (insert (⦃X, Y⦄ₕ) H) = insert (⦃X, Y⦄ₕ) (insert (Hash ⦃X, Y⦄) (analz (insert Y H))) :=
  by simp [HPair]

@[simp]
lemma HPair_synth_analz {H : Set Msg} {X Y : Msg} :
  X ∉ synth (analz H) →
  ((⦃X, Y⦄ₕ ∈ synth (analz H)) ↔ (Hash ⦃X, Y⦄ ∈ analz H ∧ Y ∈ synth (analz H))) :=
by
  intro _; simp [HPair]; intro _; constructor
  · intro h; cases h with
    | inj => assumption
    | hash a => cases a with
      | inj a => apply analz.fst at a; apply synth.inj at a; contradiction
      | mpair => contradiction
  · intro _; aapply synth.inj

-- We do NOT want Crypt... messages broken up in protocols!!
-- TODO rewrite this
attribute [-simp] parts.body

-- Rewrites to push in Key and Crypt messages, so that other messages can
-- be pulled out using the `analz_insert` rules

lemma pushKeysAgent {K : Key} {C : Agent} {H : Set Msg}:
  insert (Key K) (insert (Agent C) H) = insert (Agent C) (insert (Key K) H) :=
  by simp [Set.insert_comm]

lemma pushKeysNumber {K : Key} {N : Nat} {H : Set Msg}:
  insert (Key K) (insert (Number N) H) = insert (Number N) (insert (Key K) H) :=
  by simp [Set.insert_comm]

lemma pushKeysNonce {K : Key} {N : Nat} {H : Set Msg}:
  insert (Key K) (insert (Nonce N) H) = insert (Nonce N) (insert (Key K) H) :=
  by simp [Set.insert_comm]

lemma pushKeysHash {K : Key} {X : Msg} {H : Set Msg}:
  insert (Key K) (insert (Hash X) H) = insert (Hash X) (insert (Key K) H) :=
  by simp [Set.insert_comm]

lemma pushKeysMPair {K : Key} {X Y : Msg} {H : Set Msg}:
  insert (Key K) (insert ⦃X, Y⦄ H) = insert ⦃X, Y⦄ (insert (Key K) H) :=
  by simp [Set.insert_comm]

lemma pushKeysCrypt {K K' : Key} {X : Msg} {H : Set Msg}:
  insert (Key K) (insert (Crypt K' X) H) = insert (Crypt K' X) (insert (Key K) H) :=
  by simp [Set.insert_comm]

lemma pushCryptsAgent {X : Msg} {K : Key} {C : Agent} {H : Set Msg} :
  insert (Crypt K X) (insert (Agent C) H) = insert (Agent C) (insert (Crypt K X) H) :=
  by simp [Set.insert_comm]

lemma pushCryptsNonce {X : Msg} {K : Key} {N : Nat} {H : Set Msg} :
  insert (Crypt K X) (insert (Nonce N) H) = insert (Nonce N) (insert (Crypt K X) H) :=
  by simp [Set.insert_comm]

lemma pushCryptsNumber {X : Msg} {K : Key} {N : Nat} {H : Set Msg} :
  insert (Crypt K X) (insert (Number N) H) = insert (Number N) (insert (Crypt K X) H) :=
  by simp [Set.insert_comm]

lemma pushCryptsHash {X X' : Msg} {K : Key} {H : Set Msg} :
  insert (Crypt K X) (insert (Hash X') H) = insert (Hash X') (insert (Crypt K X) H) :=
  by simp [Set.insert_comm]

lemma pushCryptsMPair {X X' Y : Msg} {K : Key} {H : Set Msg} :
  insert (Crypt K X) (insert ⦃X', Y⦄ H) = insert ⦃X', Y⦄ (insert (Crypt K X) H) :=
  by simp [Set.insert_comm]

-- The set of key-free messages

inductive keyfree : Set Msg
  | agent {A : Agent} : keyfree (Agent A)
  | number {N : Nat} : keyfree (Number N)
  | nonce {N : Nat} : keyfree (Nonce N)
  | hash {X : Msg} : keyfree (Hash X)
  | mpair {X Y : Msg} : keyfree X → keyfree Y → keyfree ⦃X, Y⦄
  | crypt {K : Key} {X : Msg} : keyfree X → keyfree (Crypt K X)

-- Inductive cases
lemma keyfree_KeyE {K : Key} : ¬keyfree (Key K) :=
  by intro h; cases h

lemma keyfree_MPairEL {X Y : Msg} : keyfree ⦃X, Y⦄ → keyfree X :=
  by intro h; cases h; assumption

lemma keyfree_MPairER {X Y : Msg} : keyfree ⦃X, Y⦄ → keyfree Y :=
  by intro h; cases h; assumption

lemma keyfree_CryptE {K : Key} {X : Msg} : keyfree (Crypt K X) → keyfree X :=
  by intro h; cases h; assumption

-- Parts of key-free messages remain key-free
lemma parts_keyfree : parts keyfree ⊆ keyfree :=
by
  intro X h
  induction h with
  | inj => assumption
  | fst => aapply keyfree_MPairEL
  | snd => aapply keyfree_MPairER
  | body => aapply 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 {G H : Set Msg} {X : Msg} :
  X ∈ analz (G ∪ H) → G ⊆ keyfree → X ∈ parts G ∪ analz H :=
by
  intro hG hKeyFree
  induction hG with
  | inj h => cases h with
    | inl hG => exact Or.inl (parts.inj hG)
    | inr hH => exact Or.inr (analz.inj hH)
  | fst _ ih =>
  cases ih
  · left; aapply parts.fst
  · right; aapply analz.fst
  | snd _ ih => 
  cases ih
  · left; aapply parts.snd
  · right; aapply analz.snd
  | @decrypt K _ h₁ h₂ ih₁ ih₂ => cases ih₂ with
    | inl h => apply parts_mono at hKeyFree
               apply subset_trans (c := keyfree) at hKeyFree
               have pkf := parts_keyfree
               apply hKeyFree at pkf
               apply pkf at h
               have kf_k := keyfree_KeyE (K := invKey K)
               contradiction
    | inr =>
    cases ih₁
    · left; aapply parts.body
    · right; aapply analz.decrypt

-- Crypt and Hash are not in the image of Key
@[simp]
lemma Crypt_notin_image_Key {K : Key} {X : Msg} {A : Set Key} : Crypt K X ∉ Key '' A :=
  by simp

@[simp]
lemma Hash_notin_image_Key {X : Msg} {A : Set Key} : Hash X ∉ Key '' A :=
  by simp

-- Monotonicity of `synth` over `analz`
lemma synth_analz_mono {G H : Set Msg} : G ⊆ H → synth (analz G) ⊆ synth (analz H) :=
  λ h => synth_mono (analz_mono h)

-- Simplification for Fake cases
@[simp]
lemma Fake_analz_eq {H : Set Msg} {X : Msg} :
  X ∈ synth (analz H) → synth (analz (insert X H)) = synth (analz H) :=
by
  intro hX
  ext
  constructor
  · apply synth_subset_iff.mp
    apply subset_trans (b := synth (analz H) ∪ analz H)
    · apply Fake_analz_insert (G := H) (H := H) (X := X) at hX
      rw[Set.union_self] at hX
      assumption
    · apply sup_le_iff.mpr; apply And.intro
      · trivial
      · exact synth_increasing
  · apply synth_analz_mono; simp

-- Generalizations of `analz_insert_eq`
lemma gen_analz_insert_eq {H G : Set Msg} {X : Msg} :
  X ∈ analz H → H ⊆ G → analz (insert X G) = analz G :=
by
  intro hX hSubset
  apply Set.ext
  intro Y
  constructor
  · intro h
    induction h with
    | inj h => cases h with
      | inl hX' => apply analz_mono at hSubset; apply hSubset at hX; rw[hX']; assumption
      | inr hG => aapply analz.inj
    | fst h ih => exact analz.fst ih
    | snd h ih => exact analz.snd ih
    | decrypt h₁ h₂ ih₁ ih₂ => exact analz.decrypt ih₁ ih₂
  · intro h
    exact analz_mono (Set.subset_insert _ _) h

lemma synth_analz_insert_eq {H G : Set Msg} {X : Msg} {K : Key} :
  X ∈ synth (analz H) → H ⊆ G → ((Key K ∈ analz (insert X G)) ↔ (Key K ∈ analz G)) :=
by
  intro h₁ h₂
  constructor
  · induction h₁ with
    | inj a => apply gen_analz_insert_eq (G := G) at a; apply a at h₂; simp[h₂]
    | agent => rw [analz_insert_Agent]; intro h; cases h; contradiction; assumption
    | number => rw [analz_insert_Number]; intro h; cases h; contradiction; assumption
    | hash => rw [analz_insert_Hash]; intro h; cases h; contradiction; assumption
    | @mpair _ Y h₁ _ _ ih₂ => rw [analz_insert_MPair]; intro h; cases h with
      | inl => contradiction 
      | inr h => apply Fake_analz_insert (H := insert Y G) at h₁; apply h₁ at h;
                 cases h with
        | inl h => cases h; aapply analz_mono
        | inr h => apply ih₂; have b := h₂; apply subset_trans (c := insert Y G) at b
                   have c := Set.subset_insert (x := Y) (s := G)
                   apply b at c
                   apply sup_le (a := H) (b := insert Y G) (c := insert Y G) at c
                   have e := le_refl (a := insert Y G)
                   apply c at e
                   apply analz_mono at e
                   aapply e
    | crypt b a a_ih => intro h; apply a_ih; apply analz_insert_Crypt_subset at h
                        cases h; contradiction; assumption
  · apply analz_mono; apply Set.subset_insert

  

-- Fake parts for single messages
lemma Fake_parts_sing {H : Set Msg} {X : Msg} :
  X ∈ synth (analz H) → parts {X} ⊆ synth (analz H) ∪ parts H :=
by
  intro h
  rw[Set.singleton_def]
  apply subset_trans (b := parts (insert X H))
  · apply parts_mono; simp
  · aapply Fake_parts_insert