Theory PreSimplyTyped

theory PreSimplyTyped
imports Fresh Permutation
begin

type_synonym tvar = nat

datatype type =
  TUnit
| TVar tvar
| TArr type type
| TPair type type

datatype 'a ptrm =
  PUnit
| PVar 'a
| PApp "'a ptrm" "'a ptrm"
| PFn 'a type "'a ptrm"
| PPair "'a ptrm" "'a ptrm"
| PFst "'a ptrm"
| PSnd "'a ptrm"

fun ptrm_fvs :: "'a ptrm ⇒ 'a set" where
  "ptrm_fvs PUnit = {}"
| "ptrm_fvs (PVar x) = {x}"
| "ptrm_fvs (PApp A B) = ptrm_fvs A ∪ ptrm_fvs B"
| "ptrm_fvs (PFn x _ A) = ptrm_fvs A - {x}"
| "ptrm_fvs (PPair A B) = ptrm_fvs A ∪ ptrm_fvs B"
| "ptrm_fvs (PFst P) = ptrm_fvs P"
| "ptrm_fvs (PSnd P) = ptrm_fvs P"

fun ptrm_apply_prm :: "'a prm ⇒ 'a ptrm ⇒ 'a ptrm" (infixr ‹∙› 150) where
  "ptrm_apply_prm π PUnit = PUnit"
| "ptrm_apply_prm π (PVar x) = PVar (π $ x)"
| "ptrm_apply_prm π (PApp A B) = PApp (ptrm_apply_prm π A) (ptrm_apply_prm π B)"
| "ptrm_apply_prm π (PFn x T A) = PFn (π $ x) T (ptrm_apply_prm π A)"
| "ptrm_apply_prm π (PPair A B) = PPair (ptrm_apply_prm π A) (ptrm_apply_prm π B)"
| "ptrm_apply_prm π (PFst P) = PFst (ptrm_apply_prm π P)"
| "ptrm_apply_prm π (PSnd P) = PSnd (ptrm_apply_prm π P)"

inductive ptrm_alpha_equiv :: "'a ptrm ⇒ 'a ptrm ⇒ bool" (infix ‹≈› 100) where
  unit:       "PUnit ≈ PUnit"
| var:        "(PVar x) ≈ (PVar x)"
| app:        "⟦A ≈ B; C ≈ D⟧ ⟹ (PApp A C) ≈ (PApp B D)"
| fn1:        "A ≈ B ⟹ (PFn x T A) ≈ (PFn x T B)"
| fn2:        "⟦a ≠ b; A ≈ [a ↔ b] ∙ B; a ∉ ptrm_fvs B⟧ ⟹ (PFn a T A) ≈ (PFn b T B)"
| pair:       "⟦A ≈ B; C ≈ D⟧ ⟹ (PPair A C) ≈ (PPair B D)"
| fst:        "A ≈ B ⟹ PFst A ≈ PFst B"
| snd:        "A ≈ B ⟹ PSnd A ≈ PSnd B"

inductive_cases unitE: "PUnit ≈ Y"
inductive_cases varE:  "PVar x ≈ Y"
inductive_cases appE:  "PApp A B ≈ Y"
inductive_cases fnE:   "PFn x T A ≈ Y"
inductive_cases pairE: "PPair A B ≈ Y"
inductive_cases fstE:  "PFst P ≈ Y"
inductive_cases sndE:  "PSnd P ≈ Y"

lemma ptrm_prm_apply_id:
  shows "ε ∙ X = X"
by(induction X, simp_all add: prm_apply_id)

lemma ptrm_prm_apply_compose:
  shows "π ∙ σ ∙ X = (π ⋄ σ) ∙ X"
by(induction X, simp_all add: prm_apply_composition)

lemma ptrm_size_prm:
  shows "size X = size (π ∙ X)"
by(induction X, auto)

lemma ptrm_size_alpha_equiv:
  assumes "X ≈ Y"
  shows "size X = size Y"
using assms proof(induction rule: ptrm_alpha_equiv.induct)
  case (fn2 a b A B T)
    hence "size A = size B" using ptrm_size_prm by metis
    thus ?case by auto
  next
qed auto

lemma ptrm_fvs_finite:
  shows "finite (ptrm_fvs X)"
by(induction X, auto)

lemma ptrm_prm_fvs:
  shows "ptrm_fvs (π ∙ X) = π {$} ptrm_fvs X"
proof(induction X)
  case (PUnit)
    thus ?case unfolding prm_set_def by simp
  next
  case (PVar x)
    have "ptrm_fvs (π ∙ PVar x) = ptrm_fvs (PVar (π $ x))" by simp
    moreover have "... = {π $ x}" by simp
    moreover have "... = π {$} {x}" using prm_set_singleton by metis
    moreover have "... = π {$} ptrm_fvs (PVar x)" by simp
    ultimately show ?case by metis
  next
  case (PApp A B)
    have "ptrm_fvs (π ∙ PApp A B) = ptrm_fvs (PApp (π ∙ A) (π ∙ B))" by simp
    moreover have "... = ptrm_fvs (π ∙ A) ∪ ptrm_fvs (π ∙ B)" by simp
    moreover have "... = π {$} ptrm_fvs A ∪ π {$} ptrm_fvs B" using PApp.IH by metis
    moreover have "... = π {$} (ptrm_fvs A ∪ ptrm_fvs B)" using prm_set_distributes_union by metis
    moreover have "... = π {$} ptrm_fvs (PApp A B)" by simp
    ultimately show ?case by metis
  next
  case (PFn x T A)
    have "ptrm_fvs (π ∙ PFn x T A) = ptrm_fvs (PFn (π $ x) T (π ∙ A))" by simp
    moreover have "... = ptrm_fvs (π ∙ A) - {π $ x}" by simp
    moreover have "... = π {$} ptrm_fvs A - {π $ x}" using PFn.IH by metis
    moreover have "... = π {$} ptrm_fvs A - π {$} {x}" using prm_set_singleton by metis
    moreover have "... = π {$} (ptrm_fvs A - {x})" using prm_set_distributes_difference by metis
    moreover have "... = π {$} ptrm_fvs (PFn x T A)" by simp
    ultimately show ?case by metis
  next
  case (PPair A B)
    thus ?case
      using prm_set_distributes_union ptrm_apply_prm.simps(5) ptrm_fvs.simps(5)
      by fastforce
  next
  case (PFst P)
    thus ?case by auto
  next
  case (PSnd P)
    thus ?case by auto
  next
qed

lemma ptrm_alpha_equiv_fvs:
  assumes "X ≈ Y"
  shows "ptrm_fvs X = ptrm_fvs Y"
using assms proof(induction rule: ptrm_alpha_equiv.induct)
  case (fn2 a b A B T)
    have "ptrm_fvs (PFn a T A) = ptrm_fvs A - {a}" by simp
    moreover have "... = ptrm_fvs ([a ↔ b] ∙ B) - {a}" using fn2.IH by metis
    moreover have "... = ([a ↔ b] {$} ptrm_fvs B) - {a}" using ptrm_prm_fvs by metis
    moreover have "... = ptrm_fvs B - {b}"  proof -
      consider "b ∈ ptrm_fvs B" | "b ∉ ptrm_fvs B" by auto
      thus ?thesis proof(cases)
        case 1
          have "[a ↔ b] {$} ptrm_fvs B - {a} = [b ↔ a] {$} ptrm_fvs B - {a}" using prm_unit_commutes by metis
          moreover have "... = ((ptrm_fvs B - {b}) ∪ {a}) - {a}"
            using prm_set_unit_action ‹b ∈ ptrm_fvs B› ‹a ∉ ptrm_fvs B› by metis
          moreover have "... = ptrm_fvs B - {b}" using ‹a ∉ ptrm_fvs B› ‹a ≠ b›
            using Diff_insert0 Diff_insert2 Un_insert_right insert_Diff1 insert_is_Un singletonI
              sup_bot.right_neutral by blast (* why?! *)
          ultimately show ?thesis by metis
        next
        case 2
          hence "[a ↔ b] {$} ptrm_fvs B - {a} = ptrm_fvs B - {a}"
            using prm_set_unit_inaction ‹a ∉ ptrm_fvs B› by metis
          moreover have "... = ptrm_fvs B" using ‹a ∉ ptrm_fvs B› by simp
          moreover have "... = ptrm_fvs B - {b}" using ‹b ∉ ptrm_fvs B› by simp
          ultimately show ?thesis by metis
        next
      qed
    qed
    moreover have "... = ptrm_fvs (PFn b T B)" by simp
    ultimately show ?case by metis
  next
qed auto

lemma ptrm_alpha_equiv_prm:
  assumes "X ≈ Y"
  shows "π ∙ X ≈ π ∙ Y"
using assms proof(induction rule: ptrm_alpha_equiv.induct)
  case (unit)
    thus ?case using ptrm_alpha_equiv.unit by simp
  next
  case (var x)
    thus ?case using ptrm_alpha_equiv.var by simp
  next
  case (app A B C D)
    thus ?case using ptrm_alpha_equiv.app by simp
  next
  case (fn1 A B x T)
    thus ?case using ptrm_alpha_equiv.fn1 by simp
  next
  case (fn2 a b A B T)
    have "π $ a ≠ π $ b" using ‹a ≠ b› using prm_apply_unequal by metis
    moreover have "π $ a ∉ ptrm_fvs (π ∙ B)" using ‹a ∉ ptrm_fvs B›
      using imageE prm_apply_unequal prm_set_def ptrm_prm_fvs by (metis (no_types, lifting))
    moreover have "π ∙ A ≈ [π $ a ↔ π $ b] ∙ π ∙ B"
      using fn2.IH prm_compose_push ptrm_prm_apply_compose by metis
    ultimately show ?case using ptrm_alpha_equiv.fn2 by simp
  next
  case (pair A B C D)
    thus ?case using ptrm_alpha_equiv.pair by simp
  next
  case (fst A B)
    thus ?case using ptrm_alpha_equiv.fst by simp
  next
  case (snd A B)
    thus ?case using ptrm_alpha_equiv.snd by simp
  next
qed

lemma ptrm_swp_transfer:
  shows "[a ↔ b] ∙ X ≈ Y ⟷ X ≈ [a ↔ b] ∙ Y"
proof -
  have 1: "[a ↔ b] ∙ X ≈ Y ⟹ X ≈ [a ↔ b] ∙ Y"
  proof -
    assume "[a ↔ b] ∙ X ≈ Y"
    hence "ε ∙ X ≈ [a ↔ b] ∙ Y"
      using ptrm_alpha_equiv_prm ptrm_prm_apply_compose prm_unit_involution by metis
    thus ?thesis using ptrm_prm_apply_id by metis
  qed
  have 2: "X ≈ [a ↔ b] ∙ Y ⟹ [a ↔ b] ∙ X ≈ Y"
  proof -
    assume "X ≈ [a ↔ b] ∙ Y"
    hence "[a ↔ b] ∙ X ≈ ε ∙ Y"
      using ptrm_alpha_equiv_prm ptrm_prm_apply_compose prm_unit_involution by metis
    thus ?thesis using ptrm_prm_apply_id by metis
  qed
  from 1 and 2 show "[a ↔ b] ∙ X ≈ Y ⟷ X ≈ [a ↔ b] ∙ Y" by blast
qed

lemma ptrm_alpha_equiv_fvs_transfer:
  assumes "A ≈ [a ↔ b] ∙ B" and "a ∉ ptrm_fvs B"
  shows "b ∉ ptrm_fvs A"
proof -
  from ‹A ≈ [a ↔ b] ∙ B› have "[a ↔ b] ∙ A ≈ B" using ptrm_swp_transfer by metis
  hence "ptrm_fvs B = [a ↔ b] {$} ptrm_fvs A"
    using ptrm_alpha_equiv_fvs ptrm_prm_fvs by metis
  hence "a ∉ [a ↔ b] {$} ptrm_fvs A" using ‹a ∉ ptrm_fvs B› by metis
  hence "b ∉ [a ↔ b] {$} ([a ↔ b] {$} ptrm_fvs A)"
    using prm_set_notmembership prm_unit_action by metis
  thus ?thesis using prm_set_apply_compose prm_unit_involution prm_set_id by metis
qed

lemma ptrm_prm_agreement_equiv:
  assumes "⋀a. a ∈ ds π σ ⟹ a ∉ ptrm_fvs M"
  shows "π ∙ M ≈ σ ∙ M"
using assms proof(induction M arbitrary: π σ)
  case (PUnit)
    thus ?case using ptrm_alpha_equiv.unit by simp
  next
  case (PVar x)
    consider "x ∈ ds π σ" | "x ∉ ds π σ" by auto
    thus ?case proof(cases)
      case 1
        hence "x ∉ ptrm_fvs (PVar x)" using PVar.prems by blast
        thus ?thesis by simp
      next
      case 2
        hence "π $ x = σ $ x" using prm_disagreement_ext by metis
        thus ?thesis using ptrm_alpha_equiv.var by simp
      next
    qed
  next
  case (PApp A B)
    hence "π ∙ A ≈ σ ∙ A" and "π ∙ B ≈ σ ∙ B" by auto
    thus ?case using ptrm_alpha_equiv.app by auto
  next
  case (PFn x T A)
    consider "x ∉ ds π σ" | "x ∈ ds π σ" by auto
    thus ?case proof(cases)
      case 1
        hence *: "π $ x = σ $ x" using prm_disagreement_ext by metis
        have "⋀a. a ∈ ds π σ ⟹ a ∉ ptrm_fvs A"
        proof -
          fix a
          assume "a ∈ ds π σ"
          hence "a ∉ ptrm_fvs (PFn x T A)" using PFn.prems by metis
          hence "a = x ∨ a ∉ ptrm_fvs A" by auto
          thus "a ∉ ptrm_fvs A" using ‹a ∈ ds π σ› ‹x ∉ ds π σ› by auto
        qed
        thus ?thesis using PFn.IH * ptrm_alpha_equiv.fn1 ptrm_apply_prm.simps(3) by fastforce
      next
      case 2
        hence "π $ x ≠ σ $ x" using prm_disagreement_def CollectD by fastforce
        moreover have "π $ x ∉ ptrm_fvs (σ ∙ A)"
        proof -
          have "y ∈ (ptrm_fvs A) ⟹ π $ x ≠ σ $ y" for y
            using PFn ‹π $ x ≠ σ $ x› prm_apply_unequal prm_disagreement_ext ptrm_fvs.simps(4)
            by (metis Diff_iff empty_iff insert_iff)
          hence "π $ x ∉ σ {$} ptrm_fvs A" unfolding prm_set_def by auto
          thus ?thesis using ptrm_prm_fvs by metis
        qed
        moreover have "π ∙ A ≈ [π $ x ↔ σ $ x] ∙ σ ∙ A"
        proof -
          have "⋀a. a ∈ ds π ([π $ x ↔ σ $ x] ⋄ σ) ⟹ a ∉ ptrm_fvs A" proof -
            fix a
            assume *: "a ∈ ds π ([π $ x ↔ σ $ x] ⋄ σ)"
            hence "a ≠ x" using ‹π $ x ≠ σ $ x›
              using prm_apply_composition prm_disagreement_ext prm_unit_action prm_unit_commutes
              by metis
            hence "a ∈ ds π σ"
              using * prm_apply_composition prm_apply_unequal prm_disagreement_ext prm_unit_inaction
              by metis
            thus "a ∉ ptrm_fvs A" using ‹a ≠ x› PFn.prems by auto
          qed
          thus ?thesis using PFn by (simp add: ptrm_prm_apply_compose)
        qed
        ultimately show ?thesis using ptrm_alpha_equiv.fn2 by simp
      next    
    qed
  next
  case (PPair A B)
    hence "π ∙ A ≈ σ ∙ A" and "π ∙ B ≈ σ ∙ B" by auto
    thus ?case using ptrm_alpha_equiv.pair by auto
  next
  case (PFst P)
    hence "π ∙ P ≈ σ ∙ P" by auto
    thus ?case using ptrm_alpha_equiv.fst by auto
  next
  case (PSnd P)
    hence "π ∙ P ≈ σ ∙ P" by auto
    thus ?case using ptrm_alpha_equiv.snd by auto
  next
qed

lemma ptrm_prm_unit_inaction:
  assumes "a ∉ ptrm_fvs X" "b ∉ ptrm_fvs X"
  shows "[a ↔ b] ∙ X ≈ X"
proof -
  have "(⋀x. x ∈ ds [a ↔ b] ε ⟹ x ∉ ptrm_fvs X)"
  proof -
    fix x
    assume "x ∈ ds [a ↔ b] ε"
    hence "[a ↔ b] $ x ≠ ε $ x"
      unfolding prm_disagreement_def
      by auto
    hence "x = a ∨ x = b"
      using prm_apply_id prm_unit_inaction by metis
    thus "x ∉ ptrm_fvs X" using assms by auto
  qed
  hence "[a ↔ b] ∙ X ≈ ε ∙ X"
    using ptrm_prm_agreement_equiv by metis
  thus ?thesis using ptrm_prm_apply_id by metis
qed

lemma ptrm_alpha_equiv_reflexive:
  shows "M ≈ M"
by(induction M, auto simp add: ptrm_alpha_equiv.intros)

corollary ptrm_alpha_equiv_reflp:
  shows "reflp ptrm_alpha_equiv"
unfolding reflp_def using ptrm_alpha_equiv_reflexive by auto

lemma ptrm_alpha_equiv_symmetric:
  assumes "X ≈ Y"
  shows "Y ≈ X"
using assms proof(induction rule: ptrm_alpha_equiv.induct, auto simp add: ptrm_alpha_equiv.intros)
  case (fn2 a b A B T)
    have "b ≠ a" using ‹a ≠ b› by auto
    have "B ≈ [b ↔ a] ∙ A" using ‹[a ↔ b] ∙ B ≈ A›
      using ptrm_swp_transfer prm_unit_commutes by metis

    have "b ∉ ptrm_fvs A" using ‹a ∉ ptrm_fvs B› ‹A ≈ [a ↔ b] ∙ B› ‹a ≠ b›
      using ptrm_alpha_equiv_fvs_transfer by metis

    show ?case using ‹b ≠ a› ‹B ≈ [b ↔ a] ∙ A› ‹b ∉ ptrm_fvs A›
      using ptrm_alpha_equiv.fn2 by metis
  next
qed

corollary ptrm_alpha_equiv_symp:
  shows "symp ptrm_alpha_equiv"
unfolding symp_def using ptrm_alpha_equiv_symmetric by auto

lemma ptrm_alpha_equiv_transitive:
  assumes "X ≈ Y" and "Y ≈ Z"
  shows "X ≈ Z"
using assms proof(induction "size X" arbitrary: X Y Z rule: less_induct)
  fix X Y Z :: "'a ptrm"
  assume IH: "⋀K Y Z :: 'a ptrm. size K < size X ⟹ K ≈ Y ⟹ Y ≈ Z ⟹ K ≈ Z"
  assume "X ≈ Y" and "Y ≈ Z"
  show "X ≈ Z" proof(cases X)
    case (PUnit)
      hence "Y = PUnit" using ‹X ≈ Y› unitE by metis
      hence "Z = PUnit" using ‹Y ≈ Z› unitE by metis
      thus ?thesis using ptrm_alpha_equiv.unit ‹X = PUnit› by metis
    next
    case (PVar x)
      hence "PVar x ≈ Y" using ‹X ≈ Y› by auto
      hence "Y = PVar x" using varE by metis
      hence "PVar x ≈ Z" using ‹Y ≈ Z› by auto
      hence "Z = PVar x" using varE by metis
      thus ?thesis using ptrm_alpha_equiv.var ‹X = PVar x› by metis
    next
    case (PApp A B)
      obtain C D where "Y = PApp C D" and "A ≈ C" and "B ≈ D"
        using appE ‹X = PApp A B› ‹X ≈ Y› by metis
      hence "PApp C D ≈ Z" using ‹Y ≈ Z› by simp
      from this obtain E F where "Z = PApp E F" and "C ≈ E" and "D ≈ F" using appE by metis

      have "size A < size X" and "size B < size X" using ‹X = PApp A B› by auto
      hence "A ≈ E" and "B ≈ F" using IH ‹A ≈ C› ‹C ≈ E› ‹B ≈ D› ‹D ≈ F› by auto
      thus ?thesis using ‹X = PApp A B› ‹Z = PApp E F› ptrm_alpha_equiv.app by metis
    next
    case (PFn x T A)
      from this have X: "X = PFn x T A".
      hence *: "size A < size X" by auto

      obtain y B where "Y = PFn y T B"
        and Y_cases: "(x = y ∧ A ≈ B) ∨ (x ≠ y ∧ A ≈ [x ↔ y] ∙ B ∧ x ∉ ptrm_fvs B)"
        using fnE ‹X ≈ Y› ‹X = PFn x T A› by metis
      obtain z C where Z: "Z = PFn z T C"
        and Z_cases: "(y = z ∧ B ≈ C) ∨ (y ≠ z ∧ B ≈ [y ↔ z] ∙ C ∧ y ∉ ptrm_fvs C)"
        using fnE ‹Y ≈ Z› ‹Y = PFn y T B› by metis

      consider
        "x = y" "A ≈ B" and "y = z" "B ≈ C"
      | "x = y" "A ≈ B" and "y ≠ z" "B ≈ [y ↔ z] ∙ C" "y ∉ ptrm_fvs C"
      | "x ≠ y" "A ≈ [x ↔ y] ∙ B" "x ∉ ptrm_fvs B" and "y = z" "B ≈ C"
      | "x ≠ y" "A ≈ [x ↔ y] ∙ B" "x ∉ ptrm_fvs B" and "y ≠ z" "B ≈ [y ↔ z] ∙ C" "y ∉ ptrm_fvs C" and "x = z"
      | "x ≠ y" "A ≈ [x ↔ y] ∙ B" "x ∉ ptrm_fvs B" and "y ≠ z" "B ≈ [y ↔ z] ∙ C" "y ∉ ptrm_fvs C" and "x ≠ z"
        using Y_cases Z_cases by auto

      thus ?thesis proof(cases)
        case 1
          have "A ≈ C" using ‹A ≈ B› ‹B ≈ C› IH * by metis
          have "x = z" using ‹x = y› ‹y = z› by metis
          show ?thesis using ‹A ≈ C› ‹x = z› X Z
            using ptrm_alpha_equiv.fn1 by metis
        next
        case 2
          have "x ≠ z" using ‹x = y› ‹y ≠ z› by metis
          have "A ≈ [x ↔ z] ∙ C" using ‹A ≈ B› ‹B ≈ [y ↔ z] ∙ C› ‹x = y› IH * by metis
          have "x ∉ ptrm_fvs C" using ‹x = y› ‹y ∉ ptrm_fvs C› by metis
          thus ?thesis using ‹x ≠ z› ‹A ≈ [x ↔ z] ∙ C› ‹x ∉ ptrm_fvs C› X Z
            using ptrm_alpha_equiv.fn2 by metis
        next
        case 3
          have "x ≠ z" using ‹x ≠ y› ‹y = z› by metis
          have "[x ↔ y] ∙ B ≈ [x ↔ y] ∙ C" using ‹B ≈ C› ptrm_alpha_equiv_prm by metis
          have "A ≈ [x ↔ z] ∙ C"
            using ‹A ≈ [x ↔ y] ∙ B› ‹[x ↔ y] ∙ B ≈ [x ↔ y] ∙ C› ‹y = z› IH *
            by metis
          have "x ∉ ptrm_fvs C" using ‹B ≈ C› ‹x ∉ ptrm_fvs B› ptrm_alpha_equiv_fvs by metis
          thus ?thesis using ‹x ≠ z› ‹A ≈ [x ↔ z] ∙ C› ‹x ∉ ptrm_fvs C› X Z
            using ptrm_alpha_equiv.fn2 by metis
        next
        case 4
          have "[x ↔ y] ∙ B ≈ [x ↔ y] ∙ [y ↔ z] ∙ C"
            using ‹B ≈ [y ↔ z] ∙ C› ptrm_alpha_equiv_prm by metis
          hence "A ≈ [x ↔ y] ∙ [y ↔ z] ∙ C"
            using ‹A ≈ [x ↔ y] ∙ B› IH * by metis
          hence "A ≈ ([x ↔ y] ⋄ [y ↔ z]) ∙ C" using ptrm_prm_apply_compose by metis
          hence "A ≈ ([x ↔ y] ⋄ [y ↔ x]) ∙ C" using ‹x = z› by metis
          hence "A ≈ ([x ↔ y] ⋄ [x ↔ y]) ∙ C" using prm_unit_commutes by metis
          hence "A ≈ ε ∙ C" using ‹x = z› prm_unit_involution by metis
          hence "A ≈ C" using ptrm_prm_apply_id by metis

          thus ?thesis using ‹x = z› ‹A ≈ C› X Z
            using ptrm_alpha_equiv.fn1 by metis
        next
        case 5
          have "x ∉ ptrm_fvs C" proof -
            have "ptrm_fvs B = ptrm_fvs ([y ↔ z] ∙ C)"
              using ptrm_alpha_equiv_fvs ‹B ≈ [y ↔ z] ∙ C› by metis
            hence "x ∉ ptrm_fvs ([y ↔ z] ∙ C)" using ‹x ∉ ptrm_fvs B› by auto
            hence "x ∉ [y ↔ z] {$} ptrm_fvs C" using ptrm_prm_fvs by metis
            consider "z ∈ ptrm_fvs C" | "z ∉ ptrm_fvs C" by auto
            thus ?thesis proof(cases)
              case 1
                hence "[y ↔ z] {$} ptrm_fvs C = ptrm_fvs C - {z} ∪ {y}"
                  using prm_set_unit_action prm_unit_commutes
                  and ‹z ∈ ptrm_fvs C› ‹y ∉ ptrm_fvs C› by metis
                hence "x ∉ ptrm_fvs C - {z} ∪ {y}" using ‹x ∉ [y ↔ z] {$} ptrm_fvs C› by auto
                hence "x ∉ ptrm_fvs C - {z}" using ‹x ≠ y› by auto
                thus ?thesis using ‹x ≠ z› by auto
              next
              case 2
                hence "[y ↔ z] {$} ptrm_fvs C = ptrm_fvs C" using prm_set_unit_inaction ‹y ∉ ptrm_fvs C› by metis
                thus ?thesis using ‹x ∉ [y ↔ z] {$} ptrm_fvs C› by auto
              next
            qed
          qed

          have "A ≈ [x ↔ z] ∙ C" proof -
            have "A ≈ ([x ↔ y] ⋄ [y ↔ z]) ∙ C"
              using IH * ‹A ≈ [x ↔ y] ∙ B› ‹B ≈ [y ↔ z] ∙ C›
              and ptrm_alpha_equiv_prm ptrm_prm_apply_compose by metis

            have "([x ↔ y] ⋄ [y ↔ z]) ∙ C ≈ [x ↔ z] ∙ C" proof -
              have "ds ([x ↔ y] ⋄ [y ↔ z]) [x ↔ z] = {x, y}"
                using ‹x ≠ y› ‹y ≠ z› ‹x ≠ z› prm_disagreement_composition by metis

              hence "⋀a. a ∈ ds ([x ↔ y] ⋄ [y ↔ z]) [x ↔ z] ⟹ a ∉ ptrm_fvs C"
                using ‹x ∉ ptrm_fvs C› ‹y ∉ ptrm_fvs C›
                using Diff_iff Diff_insert_absorb insert_iff by auto
              thus ?thesis using ptrm_prm_agreement_equiv by metis
            qed

            thus ?thesis using IH *
              using ‹A ≈ ([x ↔ y] ⋄ [y ↔ z]) ∙ C› ‹([x ↔ y] ⋄ [y ↔ z]) ∙ C ≈ [x ↔ z] ∙ C›
              by metis
          qed

          show ?thesis using ‹x ≠ z› ‹A ≈ [x ↔ z] ∙ C› ‹x ∉ ptrm_fvs C› X Z
            using ptrm_alpha_equiv.fn2 by metis
        next
      qed
    next
    case (PPair A B)
      obtain C D where "Y = PPair C D" and "A ≈ C" and "B ≈ D"
        using pairE ‹X = PPair A B› ‹X ≈ Y› by metis
      hence "PPair C D ≈ Z" using ‹Y ≈ Z› by simp
      from this obtain E F where "Z = PPair E F" and "C ≈ E" and "D ≈ F" using pairE by metis

      have "size A < size X" and "size B < size X" using ‹X = PPair A B› by auto
      hence "A ≈ E" and "B ≈ F" using IH ‹A ≈ C› ‹C ≈ E› ‹B ≈ D› ‹D ≈ F› by auto
      thus ?thesis using ‹X = PPair A B› ‹Z = PPair E F› ptrm_alpha_equiv.pair by metis
    next
    case (PFst P)
      obtain Q where "Y = PFst Q" "P ≈ Q" using fstE ‹X = PFst P› ‹X ≈ Y› by metis
      obtain R where "Z = PFst R" "Q ≈ R" using fstE ‹Y = PFst Q› ‹Y ≈ Z› by metis

      have "size P < size X" using ‹X = PFst P› by auto
      hence "P ≈ R" using IH ‹P ≈ Q› ‹Q ≈ R› by metis
      thus ?thesis using ‹X = PFst P› ‹Z = PFst R› ptrm_alpha_equiv.fst by metis
    next
    case (PSnd P)
      obtain Q where "Y = PSnd Q" "P ≈ Q" using sndE ‹X = PSnd P› ‹X ≈ Y› by metis
      obtain R where "Z = PSnd R" "Q ≈ R" using sndE ‹Y = PSnd Q› ‹Y ≈ Z› by metis

      have "size P < size X" using ‹X = PSnd P› by auto
      hence "P ≈ R" using IH ‹P ≈ Q› ‹Q ≈ R› by metis
      thus ?thesis using ‹X = PSnd P› ‹Z = PSnd R› ptrm_alpha_equiv.snd by metis
    next
  qed
qed

corollary ptrm_alpha_equiv_transp:
  shows "transp ptrm_alpha_equiv"
unfolding transp_def using ptrm_alpha_equiv_transitive by auto


type_synonym 'a typing_ctx = "'a ⇀ type"

fun ptrm_infer_type :: "'a typing_ctx ⇒ 'a ptrm ⇒ type option" where
  "ptrm_infer_type Γ PUnit = Some TUnit"
| "ptrm_infer_type Γ (PVar x) = Γ x"
| "ptrm_infer_type Γ (PApp A B) = (case (ptrm_infer_type Γ A, ptrm_infer_type Γ B) of
     (Some (TArr τ σ), Some τ') ⇒ (if τ = τ' then Some σ else None)
   | _ ⇒ None
   )"
| "ptrm_infer_type Γ (PFn x τ A) = (case ptrm_infer_type (Γ(x ↦ τ)) A of
     Some σ ⇒ Some (TArr τ σ)
   | None ⇒ None
   )"
| "ptrm_infer_type Γ (PPair A B) = (case (ptrm_infer_type Γ A, ptrm_infer_type Γ B) of
     (Some τ, Some σ) ⇒ Some (TPair τ σ)
   | _ ⇒ None
   )"
| "ptrm_infer_type Γ (PFst P) = (case ptrm_infer_type Γ P of
     (Some (TPair τ σ)) ⇒ Some τ
   | _ ⇒ None
   )"
| "ptrm_infer_type Γ (PSnd P) = (case ptrm_infer_type Γ P of
     (Some (TPair τ σ)) ⇒ Some σ
   | _ ⇒ None
   )"

lemma ptrm_infer_type_swp_types:
  assumes "a ≠ b"
  shows "ptrm_infer_type (Γ(a ↦ T, b ↦ S)) X = ptrm_infer_type (Γ(a ↦ S, b ↦ T)) ([a ↔ b] ∙ X)"
using assms proof(induction X arbitrary: T S Γ)
  case (PUnit)
    thus ?case by simp
  next
  case (PVar x)
    consider "x = a" | "x = b" | "x ≠ a ∧ x ≠ b" by auto
    thus ?case proof(cases)
      assume "x = a"
      thus ?thesis using ‹a ≠ b› by (simp add: prm_unit_action)
      next

      assume "x = b"
      thus ?thesis using ‹a ≠ b›
        using prm_unit_action prm_unit_commutes fun_upd_same fun_upd_twist
        by (metis ptrm_apply_prm.simps(2) ptrm_infer_type.simps(2))
      next

      assume "x ≠ a ∧ x ≠ b"
      thus ?thesis by (simp add: prm_unit_inaction)
      next
    qed
  next
  case (PApp A B)
    thus ?case by simp
  next
  case (PFn x τ A)
    hence *:
      "ptrm_infer_type (Γ(a ↦ T, b ↦ S)) A = ptrm_infer_type (Γ(a ↦ S, b ↦ T)) ([a ↔ b] ∙ A)"
      for T S Γ
      by metis

    consider "x = a" | "x = b" | "x ≠ a ∧ x ≠ b" by auto
    thus ?case proof(cases)
      case 1
        hence
          "ptrm_infer_type (Γ(a ↦ S, b ↦ T)) ([a ↔ b] ∙ PFn x τ A)
         = ptrm_infer_type (Γ(a ↦ S, b ↦ T)) (PFn b τ ([a ↔ b] ∙ A))"
          using prm_unit_action ptrm_apply_prm.simps(4) by metis
        moreover have "... = (case ptrm_infer_type (Γ(a ↦ S, b ↦ τ)) ([a ↔ b] ∙ A) of None ⇒ None | Some σ ⇒ Some (TArr τ σ))"
          by simp
        moreover have "... = (case ptrm_infer_type (Γ(a ↦ τ, b ↦ S)) A of None ⇒ None | Some σ ⇒ Some (TArr τ σ))"
          using * by metis
        moreover have "... = (case ptrm_infer_type (Γ(b ↦ S, a ↦ T, a ↦ τ)) A of None ⇒ None | Some σ ⇒ Some (TArr τ σ))"
          using ‹a ≠ b› fun_upd_twist fun_upd_upd by metis
        moreover have "... = ptrm_infer_type (Γ(b ↦ S, a ↦ T)) (PFn x τ A)"
          using ‹x = a› by simp
        moreover have "... = ptrm_infer_type (Γ(a ↦ T, b ↦ S)) (PFn x τ A)"
          using ‹a ≠ b› fun_upd_twist by metis
        ultimately show ?thesis by metis
      next
      case 2
        hence
          "ptrm_infer_type (Γ(a ↦ S, b ↦ T)) ([a ↔ b] ∙ PFn x τ A)
         = ptrm_infer_type (Γ(a ↦ S, b ↦ T)) (PFn a τ ([a ↔ b] ∙ A))"
          using prm_unit_action prm_unit_commutes ptrm_apply_prm.simps(4) by metis
        moreover have "... = (case ptrm_infer_type (Γ(a ↦ S, b ↦ T, a ↦ τ)) ([a ↔ b] ∙ A) of None ⇒ None | Some σ ⇒ Some (TArr τ σ))"
          by simp
        moreover have "... = (case ptrm_infer_type (Γ(a ↦ τ, b ↦ T)) ([a ↔ b] ∙ A) of None ⇒ None | Some σ ⇒ Some (TArr τ σ))"
          using fun_upd_upd fun_upd_twist ‹a ≠ b› by metis
        moreover have "... = (case ptrm_infer_type (Γ(a ↦ T, b ↦ τ)) A of None ⇒ None | Some σ ⇒ Some (TArr τ σ))"
          using * by metis
        moreover have "... = (case ptrm_infer_type (Γ(a ↦ T, b ↦ S, b ↦ τ)) A of None ⇒ None | Some σ ⇒ Some (TArr τ σ))"
          using ‹a ≠ b› fun_upd_upd by metis
        moreover have "... = ptrm_infer_type (Γ(b ↦ S, a ↦ T)) (PFn x τ A)"
          using ‹x = b› by simp
        moreover have "... = ptrm_infer_type (Γ(a ↦ T, b ↦ S)) (PFn x τ A)"
          using ‹a ≠ b› fun_upd_twist by metis
        ultimately show ?thesis by metis
      next
      case 3
        hence "x ≠ a" "x ≠ b" by auto
        hence
          "ptrm_infer_type (Γ(a ↦ S, b ↦ T)) ([a ↔ b] ∙ PFn x τ A)
         = ptrm_infer_type (Γ(a ↦ S, b ↦ T)) (PFn x τ ([a ↔ b] ∙ A))"
          by (simp add: prm_unit_inaction)
        moreover have "... = (case ptrm_infer_type (Γ(a ↦ S, b ↦ T, x ↦ τ)) ([a ↔ b] ∙ A) of None ⇒ None | Some σ ⇒ Some (TArr τ σ))"
          by simp
        moreover have "... = (case ptrm_infer_type (Γ(x ↦ τ, a ↦ S, b ↦ T)) ([a ↔ b] ∙ A) of None ⇒ None | Some σ ⇒ Some (TArr τ σ))"
          using ‹x ≠ a› ‹x ≠ b› fun_upd_twist by metis
        moreover have "... = (case ptrm_infer_type (Γ(x ↦ τ, a ↦ T, b ↦ S)) A of None ⇒ None | Some σ ⇒ Some (TArr τ σ))"
          using * by metis
        moreover have "... = (case ptrm_infer_type (Γ(a ↦ T, b ↦ S, x ↦ τ)) A of None ⇒ None | Some σ ⇒ Some (TArr τ σ))"
          using ‹x ≠ a› ‹x ≠ b› fun_upd_twist by metis
        moreover have "... = ptrm_infer_type (Γ(a ↦ T, b ↦ S)) (PFn x τ A)" by simp
        ultimately show ?thesis by metis
      next
    qed
  next
  case (PPair A B)
    thus ?case by simp
  next
  case (PFst P)
    thus ?case by simp
  next
  case (PSnd P)
    thus ?case by simp
  next
qed

lemma ptrm_infer_type_swp:
  assumes "a ≠ b" "b ∉ ptrm_fvs X"
  shows "ptrm_infer_type (Γ(a ↦ τ)) X = ptrm_infer_type (Γ(b ↦ τ)) ([a ↔ b] ∙ X)"
using assms proof(induction X arbitrary: τ Γ)
  case (PUnit)
    thus ?case by simp
  next
  case (PVar x)
    hence "x ≠ b" by simp
    consider "x = a" | "x ≠ a" by auto
    thus ?case proof(cases)
      case 1
        hence "[a ↔ b] ∙ (PVar x) = PVar b"
        and   "ptrm_infer_type (Γ(a ↦ τ)) (PVar x) = Some τ" using prm_unit_action by auto
        thus ?thesis by auto
      next

      case 2
        hence *: "[a ↔ b] ∙ PVar x = PVar x" using ‹x ≠ b› prm_unit_inaction by simp
        consider "∃σ. Γ x = Some σ" | "Γ x = None" by auto
        thus ?thesis proof(cases)
          assume "∃σ. Γ x = Some σ"
          from this obtain σ where "Γ x = Some σ" by auto
          thus ?thesis using * ‹x ≠ a› ‹x ≠ b› by auto
          next
  
          assume "Γ x = None"
          thus ?thesis using * ‹x ≠ a› ‹x ≠ b› by auto
        qed
      next
    qed
  next
  case (PApp A B)
    have "b ∉ ptrm_fvs A" and "b ∉ ptrm_fvs B" using PApp.prems by auto
    hence "ptrm_infer_type (Γ(a ↦ τ)) A = ptrm_infer_type (Γ(b ↦ τ)) ([a ↔ b] ∙ A)"
    and   "ptrm_infer_type (Γ(a ↦ τ)) B = ptrm_infer_type (Γ(b ↦ τ)) ([a ↔ b] ∙ B)"
      using PApp.IH assms by metis+
    
    thus ?case by (metis ptrm_apply_prm.simps(3) ptrm_infer_type.simps(3))
  next
  case (PFn x σ A)
    consider "b ≠ x ∧ b ∉ ptrm_fvs A" | "b = x" using PFn.prems by auto
    thus ?case proof(cases)
      case 1
        hence "b ≠ x" "b ∉ ptrm_fvs A" by auto
        hence *: "⋀τ Γ. ptrm_infer_type (Γ(a ↦ τ)) A = ptrm_infer_type (Γ(b ↦ τ)) ([a ↔ b] ∙ A)"
          using PFn.IH assms by metis
        consider "a = x" | "a ≠ x" by auto
        thus ?thesis proof(cases)
          case 1
            hence "ptrm_infer_type (Γ(a ↦ τ)) (PFn x σ A) = ptrm_infer_type (Γ(a ↦ τ)) (PFn a σ A)"
            and "
              ptrm_infer_type (Γ(b ↦ τ)) ([a ↔ b] ∙ PFn x σ A) =
              ptrm_infer_type (Γ(b ↦ τ)) (PFn b σ ([a ↔ b] ∙ A))"
            by (auto simp add: prm_unit_action)
            thus ?thesis using * ptrm_infer_type.simps(4) fun_upd_upd by metis
          next
  
          case 2
            hence
              "ptrm_infer_type (Γ(b ↦ τ)) ([a ↔ b] ∙ PFn x σ A)
             = ptrm_infer_type (Γ(b ↦ τ)) (PFn x σ ([a ↔ b] ∙ A))"
              using ‹b ≠ x› by (simp add: prm_unit_inaction)
            moreover have "... = (case ptrm_infer_type (Γ(b ↦ τ, x ↦ σ)) ([a ↔ b] ∙ A) of None ⇒ None | Some σ' ⇒ Some (TArr σ σ'))"
              by simp
            moreover have "... = (case ptrm_infer_type (Γ(x ↦ σ, b ↦ τ)) ([a ↔ b] ∙ A) of None ⇒ None | Some σ' ⇒ Some (TArr σ σ'))"
              using ‹b ≠ x› fun_upd_twist by metis
            moreover have "... = (case ptrm_infer_type (Γ(x ↦ σ, a ↦ τ)) A of None ⇒ None | Some σ' ⇒ Some (TArr σ σ'))"
              using * by metis
            moreover have "... = (case ptrm_infer_type (Γ(a ↦ τ, x ↦ σ)) A of None ⇒ None | Some σ' ⇒ Some (TArr σ σ'))"
              using ‹a ≠ x› fun_upd_twist by metis
            moreover have "... = ptrm_infer_type (Γ(a ↦ τ)) (PFn x σ A)"
              by simp
            ultimately show ?thesis by metis
          next
        qed
      next

      case 2
        hence "a ≠ x" using assms by auto
        have "
          ptrm_infer_type (Γ(a ↦ τ, b ↦ σ)) A =
          ptrm_infer_type (Γ(b ↦ τ, a ↦ σ)) ([a ↔ b] ∙ A)
        " using ptrm_infer_type_swp_types using ‹a ≠ b› fun_upd_twist by metis
        thus ?thesis
          using ‹b = x› prm_unit_action prm_unit_commutes
          using ptrm_infer_type.simps(4) ptrm_apply_prm.simps(4) by metis
      next
    qed
  next
  case (PPair A B)
    thus ?case by simp
  next
  case (PFst P)
    thus ?case by simp
  next
  case (PSnd P)
    thus ?case by simp
  next
qed

lemma ptrm_infer_type_alpha_equiv:
  assumes "X ≈ Y"
  shows "ptrm_infer_type Γ X = ptrm_infer_type Γ Y"
using assms proof(induction arbitrary: Γ)
  case (fn2 a b A B T Γ)
    hence "ptrm_infer_type (Γ(a ↦ T)) A = ptrm_infer_type (Γ(b ↦ T)) B"
      using ptrm_infer_type_swp prm_unit_commutes by metis
    thus ?case by simp
  next
qed auto

end