# 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
```