import Init.Data.Nat.Lemmas
import Init.Prelude
import Lean
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
open Lean Elab Command Term Meta
open Parser.Tactic

-- Keys are integers
abbrev Key := Nat

-- Define the inverse of a symmetric key
class InvKey where
  invKey : Key → Key
  all_symmetric : Bool
  invKey_spec : ∀ K : Key,  invKey (invKey K) = K
  invKey_symmetric : all_symmetric → invKey = id

open InvKey

@[grind]
def symKeys [InvKey] : 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
def keysFor [InvKey] (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] : (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 [InvKey] : keysFor ∅ = ∅ := by
  simp[keysFor]

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

-- Monotonicity
lemma keysFor_mono [InvKey] : 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) [InvKey] :
    keysFor (insert (Agent A) H) = keysFor H := by
  simp[keysFor]

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

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

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

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

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

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

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

lemma Crypt_imp_invKey_keysFor {K : Key} {X : Msg} {H : Set Msg} [InvKey] :
    Crypt K X ∈ H → invKey K ∈ keysFor H := by
  intro h
  simp[invKey_eq,keysFor]
  exact ⟨_, h⟩
  
-- MPair_parts lemma
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
lemma parts_increasing {H : Set Msg} : H ⊆ parts H :=
  λ _ hx => parts.inj hx

-- parts_empty_aux lemma
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
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`
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

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

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
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_eq {h : X ∈ parts H}:
  parts (insert X H) = parts H :=
by
  simp[parts_insert];
  apply_rules [parts_subset_iff.mp, Set.singleton_subset_iff.mpr]
  
-- parts_element lemma
lemma parts_element:
  X ∈ parts H ↔ parts {X} ⊆ parts H
:= by
  constructor
  · intro h; apply_rules [ parts_subset_iff.mp, Set.singleton_subset_iff.mpr ]
  · intro h; aapply parts_subset_iff.mpr; simp

/--
A tactic that expands terms like `X ∈ parts H`
-/
syntax (name := expandPartsElement) "expand_parts_element" (ppSpace location) : tactic
macro_rules
  | `(tactic| expand_parts_element at $loc) =>
  `(tactic| rw[parts_element, Set.subset_def] at $loc; simp at $loc)

@[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_singleton_Agent :
  parts {Agent agt} = {Agent agt} := by
  rw[Set.singleton_def, parts_insert_Agent, parts_empty]

@[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_singleton_Nonce :
  parts {Nonce N} = {Nonce N} := by
  rw[Set.singleton_def, parts_insert_Nonce, parts_empty]
  
@[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_singleton_Number :
  parts {Number N} = {Number N} := by
  rw[Set.singleton_def, parts_insert_Number, parts_empty]

@[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_singleton_Key :
  parts {Key K} = {Key K} := by
  rw[Set.singleton_def, parts_insert_Key, parts_empty]

@[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_singleton_Hash :
  parts {Hash H} = {Hash H} := by
  rw[Set.singleton_def, parts_insert_Hash, parts_empty]

@[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_singleton_Crypt :
  parts {Crypt K X} = {Crypt K X} ∪ parts {X} := by
  rw[
    Set.singleton_def,
    parts_insert_Crypt,
    ←Set.singleton_def,
    Set.insert_union,
    Set.empty_union
  ]

@[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_singleton_MPair :
  parts {⦃X, Y⦄} = {⦃X, Y⦄} ∪ parts (insert X {Y}) := by
  rw[
    Set.singleton_def,
    parts_insert_MPair,
    ←Set.singleton_def,
    Set.insert_union,
    Set.empty_union
  ]

@[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 [InvKey] (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 [InvKey] : Monotone analz :=
by 
  intro _ _ h₁ _ 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} [InvKey] :
  ⦃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 [InvKey] {H : Set Msg} : H ⊆ analz H :=
  λ _ hx => analz.inj hx

lemma analz_into_parts {H : Set Msg} {X : Msg} [InvKey] : 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} [InvKey] : analz H ⊆ parts H :=
  λ _ hx => analz_into_parts hx

@[simp]
lemma analz_parts {H : Set Msg} [InvKey] : 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} [InvKey] :
  X ∉ parts H → X ∉ analz H :=
  λ h₁ h₂ => h₁ (analz_into_parts h₂)

@[simp]
lemma parts_analz {H : Set Msg} [InvKey] : 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} [InvKey] :
  insert X (analz H) ⊆ analz (insert X H) :=
by
  intro x hx
  cases hx with
  | inl h => apply analz.inj; left; assumption;
  | inr h => aapply analz_mono (Set.subset_insert _ _)

-- General equational properties

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


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

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

-- Rewrite rules for pulling out atomic messages

@[simp]
lemma analz_insert_Agent {H : Set Msg} {agt : Agent} [InvKey] :
  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} [InvKey] :
  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} [InvKey] :
  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} [InvKey] :
  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} [InvKey] :
  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} [InvKey] :
  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

@[simp]
lemma analz_insert_Decrypt [InvKey]
  { h : Key (invKey K) ∈ analz H  } :
  analz (insert (Crypt K X) H) = insert (Crypt K X) (analz (insert X H)) :=
by
  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

@[simp]
lemma analz_Crypt [InvKey]
  { h : (Key (invKey K) ∉ analz H)  } :
  (analz (insert (Crypt K X) H) = insert (Crypt K X) (analz H)) :=
by
  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} [InvKey] :
  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
  
lemma analz_insert_Crypt_element [InvKey] :
  M ∈ analz (insert (Crypt K X) H) ↔ 
  ((Key (invKey K) ∈ analz H ∧ M ∈ insert (Crypt K X) (analz (insert X H))) ∨
   (Key (invKey K) ∉ analz H ∧ M ∈ insert (Crypt K X) (analz H)))
:= by
  constructor
  · intro h; by_cases invK_in_H : Msg.Key (invKey K) ∈ analz H
    · left; rw[←analz_insert_Decrypt]; aapply And.intro; assumption
    · right; rw[←analz_Crypt]; aapply And.intro; assumption
  · intro h; rcases h with (⟨_, _⟩ | ⟨_, _⟩)
    · rw[analz_insert_Decrypt]; assumption; assumption
    · rw[analz_Crypt]; assumption; assumption

@[simp]
lemma analz_image_Key {N : Set Key} [InvKey] : 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

lemma analz_analzD [InvKey] {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₂
 
@[simp]
abbrev analzClosureOperator [InvKey] : ClosureOperator (Set Msg) :=
  ClosureOperator.mk'
  analz (analz_mono)
  (λ x ↦ @analz_increasing _ x)
  (λ x ↦ @analz_analzD _ x)

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

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

lemma analz_trans {G H : Set Msg} {X : Msg} [InvKey] :
  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} [InvKey] :
  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} [InvKey] :
  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} [InvKey] :
  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} [InvKey] :
  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} [InvKey] :
  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 [InvKey] {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 [InvKey] (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 [InvKey] : 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 [InvKey] {H : Set Msg} : H ⊆ synth H :=
  λ _ hx => synth.inj hx

-- Unions
lemma synth_union [InvKey] {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 [InvKey] {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
lemma synth_synthD [InvKey] {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 [InvKey] : ClosureOperator (Set Msg) :=
  ClosureOperator.mk' synth synth_mono 
  (λ x ↦ @synth_increasing _ x)
  (λ x ↦ @synth_synthD _ x)

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

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

@[simp]
lemma synth_trans [InvKey] {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 [InvKey] {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

lemma Crypt_synth_EK [InvKey] :
  (Crypt K X ∈ synth H) ↔
  (Crypt K X ∈ H ∨ ( Key K ∈ H ∧ X ∈ synth H)) :=
  by
  constructor
  · intro h; cases h <;> tauto
  · intro h; cases h
    · aapply synth.inj
    · apply synth.crypt <;> tauto

@[simp]
lemma Crypt_synth_eq [InvKey]
  { hK : Key K ∉ H } :
  (Crypt K X ∈ synth H ↔ Crypt K X ∈ H) :=
by
  constructor
  · intro h; simp[Crypt_synth_EK] at h; tauto
  · intro h; exact synth.inj h
  
@[simp]
lemma keysFor_synth [InvKey] {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

@[simp]
lemma Nonce_synth [InvKey] :
  Nonce NA ∈ synth H ↔ Nonce NA ∈ H
:= by
  constructor
  · intro h; cases h; assumption
  · aapply synth.inj
  
@[simp]
lemma Key_synth [InvKey] :
  Key K ∈ synth H ↔ Key K ∈ H
:= by
  constructor
  · intro h; cases h; assumption
  · aapply synth.inj
  
-- Combinations of parts, analz, and synth

@[simp]
lemma parts_synth [InvKey] {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 [InvKey] {G H : Set Msg} : analz (analz G ∪ H) = analz (G ∪ H) :=
by
  apply analz_cong
  · exact analz_idem
  · trivial

@[simp]
lemma analz_synth_Un [InvKey] {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 [InvKey] {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 [InvKey] {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 [InvKey] {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 [InvKey] {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 [InvKey] {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 [InvKey] {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 [InvKey] :
  ⦃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

@[simp]
lemma Crypt_synth_analz [InvKey]
  { h₁ : Key K ∈ analz H } 
  { h₂ : Key (invKey K) ∈ analz H } :
  ((Crypt K X ∈ synth (analz H)) ↔ X ∈ synth (analz H)) :=
  by
  constructor
  · intro h; cases h
    · apply synth.inj; aapply analz.decrypt
    · assumption
  · intro _; aapply synth.crypt

@[simp]
lemma Hash_synth_analz [InvKey] {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 [InvKey] {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]; grind

@[simp]
lemma analz_insert_HPair [InvKey] {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 [InvKey] {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, MPair_synth_analz]; 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 [InvKey] {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 [InvKey] {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 [InvKey] {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 [InvKey] {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 [InvKey] {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 [InvKey] {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