Theory SimplyTyped

theory SimplyTyped
imports PreSimplyTyped
begin

quotient_type 'a trm = "'a ptrm" / ptrm_alpha_equiv
proof(rule equivpI)
  show "reflp  ptrm_alpha_equiv" using ptrm_alpha_equiv_reflp.
  show "symp   ptrm_alpha_equiv" using ptrm_alpha_equiv_symp.
  show "transp ptrm_alpha_equiv" using ptrm_alpha_equiv_transp.
qed

lift_definition Unit :: "'a trm" is PUnit.
lift_definition Var :: "'a ⇒ 'a trm" is PVar.
lift_definition App :: "'a trm ⇒ 'a trm ⇒ 'a trm" is PApp using ptrm_alpha_equiv.app.
lift_definition Fn  :: "'a ⇒ type ⇒ 'a trm ⇒ 'a trm" is PFn using ptrm_alpha_equiv.fn1.
lift_definition Pair :: "'a trm ⇒ 'a trm ⇒ 'a trm" is PPair using ptrm_alpha_equiv.pair.
lift_definition Fst :: "'a trm ⇒ 'a trm" is PFst using ptrm_alpha_equiv.fst.
lift_definition Snd :: "'a trm ⇒ 'a trm" is PSnd using ptrm_alpha_equiv.snd.
lift_definition fvs :: "'a trm ⇒ 'a set" is ptrm_fvs using ptrm_alpha_equiv_fvs.
lift_definition prm :: "'a prm ⇒ 'a trm ⇒ 'a trm" (infixr "⋅" 150) is ptrm_apply_prm
  using ptrm_alpha_equiv_prm.
lift_definition depth :: "'a trm ⇒ nat" is size using ptrm_size_alpha_equiv.

lemma depth_prm:
  shows "depth (π ⋅ A) = depth A"
by(transfer, metis ptrm_size_prm)

lemma depth_app:
  shows "depth A < depth (App A B)" "depth B < depth (App A B)"
by(transfer, auto)+

lemma depth_fn:
  shows "depth A < depth (Fn x T A)"
by(transfer, auto)

lemma depth_pair:
  shows "depth A < depth (Pair A B)" "depth B < depth (Pair A B)"
by(transfer, auto)+

lemma depth_fst:
  shows "depth P < depth (Fst P)"
by(transfer, auto)

lemma depth_snd:
  shows "depth P < depth (Snd P)"
by(transfer, auto)
  
lemma unit_not_var:
  shows "Unit ≠ Var x"
proof(transfer)
  fix x :: 'a
  show "¬ PUnit ≈ PVar x"
  proof(rule classical)
    assume "¬¬ PUnit ≈ PVar x"
    hence False using unitE by fastforce
    thus ?thesis by blast
  qed
qed

lemma unit_not_app:
  shows "Unit ≠ App A B"
proof(transfer)
  fix A B :: "'a ptrm"
  show "¬ PUnit ≈ PApp A B"
  proof(rule classical)
    assume "¬¬ PUnit ≈ PApp A B"
    hence False using unitE by fastforce
    thus ?thesis by blast
  qed
qed

lemma unit_not_fn:
  shows "Unit ≠ Fn x T A"
proof(transfer)
  fix x :: 'a and T A
  show "¬ PUnit ≈ PFn x T A"
  proof(rule classical)
    assume "¬¬ PUnit ≈ PFn x T A"
    hence False using unitE by fastforce
    thus ?thesis by blast
  qed
qed

lemma unit_not_pair:
  shows "Unit ≠ Pair A B"
proof(transfer)
  fix A B :: "'a ptrm"
  show "¬ PUnit ≈ PPair A B"
  proof(rule classical)
    assume "¬¬ PUnit ≈ PPair A B"
    hence False using unitE by fastforce
    thus ?thesis by blast
  qed
qed

lemma unit_not_fst:
  shows "Unit ≠ Fst P"
proof(transfer)
  fix P :: "'a ptrm"
  show "¬ PUnit ≈ PFst P"
  proof(rule classical)
    assume "¬¬ PUnit ≈ PFst P"
    hence False using unitE by fastforce
    thus ?thesis by blast
  qed
qed

lemma unit_not_snd:
  shows "Unit ≠ Snd P"
proof(transfer)
  fix P :: "'a ptrm"
  show "¬ PUnit ≈ PSnd P"
  proof(rule classical)
    assume "¬¬ PUnit ≈ PSnd P"
    hence False using unitE by fastforce
    thus ?thesis by blast
  qed
qed

lemma var_not_app:
  shows "Var x ≠ App A B"
proof(transfer)
  fix x :: 'a and A B
  show "¬PVar x ≈ PApp A B"
  proof(rule classical)
    assume "¬¬PVar x ≈ PApp A B"
    hence False using varE by fastforce
    thus ?thesis by blast
  qed
qed

lemma var_not_fn:
  shows "Var x ≠ Fn y T A"
proof(transfer)
  fix x y :: 'a and T A
  show "¬PVar x ≈ PFn y T A"
  proof(rule classical)
    assume "¬¬PVar x ≈ PFn y T A" 
    hence False using varE by fastforce
    thus ?thesis by blast
  qed
qed

lemma var_not_pair:
  shows "Var x ≠ Pair A B"
proof(transfer)
  fix x :: 'a and A B
  show "¬PVar x ≈ PPair A B"
  proof(rule classical)
    assume "¬¬PVar x ≈ PPair A B"
    hence False using varE by fastforce
    thus ?thesis by blast
  qed
qed

lemma var_not_fst:
  shows "Var x ≠ Fst P"
proof(transfer)
  fix x :: 'a and P
  show "¬PVar x ≈ PFst P"
  proof(rule classical)
    assume "¬¬PVar x ≈ PFst P"
    hence False using varE by fastforce
    thus ?thesis by blast
  qed
qed

lemma var_not_snd:
  shows "Var x ≠ Snd P"
proof(transfer)
  fix x :: 'a and P
  show "¬PVar x ≈ PSnd P"
  proof(rule classical)
    assume "¬¬PVar x ≈ PSnd P"
    hence False using varE by fastforce
    thus ?thesis by blast
  qed
qed

lemma app_not_fn:
  shows "App A B ≠ Fn y T X"
proof(transfer)
  fix y :: 'a and A B T X
  show "¬PApp A B ≈ PFn y T X"
  proof(rule classical)
    assume "¬¬PApp A B ≈ PFn y T X"
    hence False using appE by auto
    thus ?thesis by blast
  qed
qed

lemma app_not_pair:
  shows "App A B ≠ Pair C D"
proof(transfer)
  fix A B C D :: "'a ptrm"
  show "¬PApp A B ≈ PPair C D"
  proof(rule classical)
    assume "¬¬PApp A B ≈ PPair C D"
    hence False using appE by auto
    thus ?thesis by blast
  qed
qed

lemma app_not_fst:
  shows "App A B ≠ Fst P"
proof(transfer)
  fix A B P :: "'a ptrm"
  show "¬PApp A B ≈ PFst P"
  proof(rule classical)
    assume "¬¬PApp A B ≈ PFst P"
    hence False using appE by auto
    thus ?thesis by blast
  qed
qed

lemma app_not_snd:
  shows "App A B ≠ Snd P"
proof(transfer)
  fix A B P :: "'a ptrm"
  show "¬PApp A B ≈ PSnd P"
  proof(rule classical)
    assume "¬¬PApp A B ≈ PSnd P"
    hence False using appE by auto
    thus ?thesis by blast
  qed
qed

lemma fn_not_pair:
  shows "Fn x T A ≠ Pair C D"
proof(transfer)
  fix x :: 'a and T A C D
  show "¬PFn x T A ≈ PPair C D"
  proof(rule classical)
    assume "¬¬PFn x T A ≈ PPair C D"
    hence False using fnE by fastforce
    thus ?thesis by blast
  qed
qed

lemma fn_not_fst:
  shows "Fn x T A ≠ Fst P"
proof(transfer)
  fix x :: 'a and T A P
  show "¬PFn x T A ≈ PFst P"
  proof(rule classical)
    assume "¬¬PFn x T A ≈ PFst P"
    hence False using fnE by fastforce
    thus ?thesis by blast
  qed
qed

lemma fn_not_snd:
  shows "Fn x T A ≠ Snd P"
proof(transfer)
  fix x :: 'a and T A P
  show "¬PFn x T A ≈ PSnd P"
  proof(rule classical)
    assume "¬¬PFn x T A ≈ PSnd P"
    hence False using fnE by fastforce
    thus ?thesis by blast
  qed
qed

lemma pair_not_fst:
  shows "Pair A B ≠ Fst P"
proof(transfer)
  fix A B P :: "'a ptrm"
  show "¬PPair A B ≈ PFst P"
  proof(rule classical)
    assume "¬¬PPair A B ≈ PFst P"
    hence False using pairE by auto
    thus ?thesis by blast
  qed
qed

lemma pair_not_snd:
  shows "Pair A B ≠ Snd P"
proof(transfer)
  fix A B P :: "'a ptrm"
  show "¬PPair A B ≈ PSnd P"
  proof(rule classical)
    assume "¬¬PPair A B ≈ PSnd P"
    hence False using pairE by auto
    thus ?thesis by blast
  qed
qed

lemma fst_not_snd:
  shows "Fst P ≠ Snd Q"
proof(transfer)
  fix P Q :: "'a ptrm"
  show "¬PFst P ≈ PSnd Q"
  proof(rule classical)
    assume "¬¬PFst P ≈ PSnd Q"
    hence False using fstE by auto
    thus ?thesis by blast
  qed
qed

lemma trm_simp:
  shows
    "Var x = Var y ⟹ x = y"
    "App A B = App C D ⟹ A = C"
    "App A B = App C D ⟹ B = D"
    "Fn x T A = Fn y S B ⟹
      (x = y ∧ T = S ∧ A = B) ∨ (x ≠ y ∧ T = S ∧ x ∉ fvs B ∧ A = [x ↔ y] ⋅ B)"
    "Pair A B = Pair C D ⟹ A = C"
    "Pair A B = Pair C D ⟹ B = D"
    "Fst P = Fst Q ⟹ P = Q"
    "Snd P = Snd Q ⟹ P = Q"
proof -
  show "Var x = Var y ⟹ x = y" by (transfer, insert ptrm.inject varE, fastforce)
  show "App A B = App C D ⟹ A = C" by (transfer, insert ptrm.inject appE, auto)
  show "App A B = App C D ⟹ B = D" by (transfer, insert ptrm.inject appE, auto)
  show "Pair A B = Pair C D ⟹ A = C" by (transfer, insert ptrm.inject pairE, auto)
  show "Pair A B = Pair C D ⟹ B = D" by (transfer, insert ptrm.inject pairE, auto)
  show "Fst P = Fst Q ⟹ P = Q" by (transfer, insert ptrm.inject fstE, auto)
  show "Snd P = Snd Q ⟹ P = Q" by (transfer, insert ptrm.inject sndE, auto)
  show "Fn x T A = Fn y S B ⟹
      (x = y ∧ T = S ∧ A = B) ∨ (x ≠ y ∧ T = S ∧ x ∉ fvs B ∧ A = [x ↔ y] ⋅ B)"
  proof(transfer')
    fix x y :: 'a and T S :: type and A B :: "'a ptrm"
    assume *: "PFn x T A ≈ PFn y S B"
    thus "x = y ∧ T = S ∧ A ≈ B ∨ x ≠ y ∧ T = S ∧ x ∉ ptrm_fvs B ∧ A ≈ [x ↔ y] ∙ B"
    proof(induction rule: fnE[where x=x and T=T and A=A and Y="PFn y S B"], metis *)
      case (2 C)
        thus ?case by simp
      next
      case (3 z C)
        thus ?case by simp
      next
    qed
  qed
qed

lemma fn_eq:
  assumes "x ≠ y" "x ∉ fvs B" "A = [x ↔ y] ⋅ B"
  shows "Fn x T A = Fn y T B"
using assms by(transfer', metis ptrm_alpha_equiv.fn2)

lemma trm_prm_simp:
  shows
    "π ⋅ Unit = Unit"
    "π ⋅ Var x = Var (π $ x)"
    "π ⋅ App A B = App (π ⋅ A) (π ⋅ B)"
    "π ⋅ Fn x T A = Fn (π $ x) T (π ⋅ A)"
    "π ⋅ Pair A B = Pair (π ⋅ A) (π ⋅ B)"
    "π ⋅ Fst P = Fst (π ⋅ P)"
    "π ⋅ Snd P = Snd (π ⋅ P)"
  apply (transfer, auto simp add: ptrm_alpha_equiv_reflexive)
  apply (transfer', auto simp add: ptrm_alpha_equiv_reflexive)
  apply ((transfer, auto simp add: ptrm_alpha_equiv_reflexive)+)
done

lemma trm_prm_apply_compose:
  shows "π ⋅ σ ⋅ A = (π ⋄ σ) ⋅ A"
by(transfer', metis ptrm_prm_apply_compose ptrm_alpha_equiv_reflexive)

lemma fvs_finite:
  shows "finite (fvs M)"
by(transfer, metis ptrm_fvs_finite)

lemma fvs_simp:
  shows
    "fvs Unit = {}" and
    "fvs (Var x) = {x}"
    "fvs (App A B) = fvs A ∪ fvs B"
    "fvs (Fn x T A) = fvs A - {x}"
    "fvs (Pair A B) = fvs A ∪ fvs B"
    "fvs (Fst P) = fvs P"
    "fvs (Snd P) = fvs P"
by((transfer, simp)+)

lemma var_prm_action:
  shows "[a ↔ b] ⋅ Var a = Var b"
by(transfer', simp add: prm_unit_action ptrm_alpha_equiv.intros)

lemma var_prm_inaction:
  assumes "a ≠ x" "b ≠ x"
  shows "[a ↔ b] ⋅ Var x = Var x"
using assms by(transfer', simp add: prm_unit_inaction ptrm_alpha_equiv.intros)

lemma trm_prm_apply_id:
  shows "ε ⋅ M = M"
by(transfer', auto simp add: ptrm_prm_apply_id)

lemma trm_prm_unit_inaction:
  assumes "a ∉ fvs X" "b ∉ fvs X"
  shows "[a ↔ b] ⋅ X = X"
using assms by(transfer', metis ptrm_prm_unit_inaction)

lemma trm_prm_agreement_equiv:
  assumes "⋀a. a ∈ ds π σ ⟹ a ∉ fvs M"
  shows "π ⋅ M = σ ⋅ M"
using assms by(transfer, metis ptrm_prm_agreement_equiv)

lemma trm_induct:
  fixes P :: "'a trm ⇒ bool"
  assumes
    "P Unit"
    "⋀x. P (Var x)"
    "⋀A B. ⟦P A; P B⟧ ⟹ P (App A B)"
    "⋀x T A. P A ⟹ P (Fn x T A)"
    "⋀A B. ⟦P A; P B⟧ ⟹ P (Pair A B)"
    "⋀A. P A ⟹ P (Fst A)"
    "⋀A. P A ⟹ P (Snd A)"
  shows "P M"
proof -
  have "⋀X. P (abs_trm X)"
  proof(rule ptrm.induct)
    show "P (abs_trm PUnit)"
      using assms(1) Unit.abs_eq by metis
    show "P (abs_trm (PVar x))" for x
      using assms(2) Var.abs_eq by metis
    show "⟦P (abs_trm A); P (abs_trm B)⟧ ⟹ P (abs_trm (PApp A B))" for A B
      using assms(3) App.abs_eq by metis
    show "P (abs_trm A) ⟹ P (abs_trm (PFn x T A))" for x T A
      using assms(4) Fn.abs_eq by metis
    show "⟦P (abs_trm A); P (abs_trm B)⟧ ⟹ P (abs_trm (PPair A B))" for A B
      using assms(5) Pair.abs_eq by metis
    show "P (abs_trm A) ⟹ P (abs_trm (PFst A))" for A
      using assms(6) Fst.abs_eq by metis
    show "P (abs_trm A) ⟹ P (abs_trm (PSnd A))" for A
      using assms(7) Snd.abs_eq by metis
  qed
  thus ?thesis using trm.abs_induct by auto
qed

lemma trm_cases:
  assumes
    "M = Unit ⟹ P M"
    "⋀x. M = Var x ⟹ P M"
    "⋀A B. M = App A B ⟹ P M"
    "⋀x T A. M = Fn x T A ⟹ P M"
    "⋀A B. M = Pair A B ⟹ P M"
    "⋀A. M = Fst A ⟹ P M"
    "⋀A. M = Snd A ⟹ P M"
  shows "P M"
using assms by(induction rule: trm_induct, auto)

lemma trm_depth_induct:
  assumes
    "P Unit"
    "⋀x. P (Var x)"
    "⋀A B. ⟦⋀K. depth K < depth (App A B) ⟹ P K⟧ ⟹ P (App A B)"
    "⋀M x T A. (⋀K. depth K < depth (Fn x T A) ⟹ P K) ⟹ P (Fn x T A)"
    "⋀A B. ⟦⋀K. depth K < depth (Pair A B) ⟹ P K⟧ ⟹ P (Pair A B)"
    "⋀A. ⟦⋀K. depth K < depth (Fst A) ⟹ P K⟧ ⟹ P (Fst A)"
    "⋀A. ⟦⋀K. depth K < depth (Snd A) ⟹ P K⟧ ⟹ P (Snd A)"
  shows "P M"
proof(induction "depth M" arbitrary: M rule: less_induct)
  fix M :: "'a trm"
  assume IH: "depth K < depth M ⟹ P K" for K
  hence
    "         M = Unit ⟹    P M"
    "⋀x.     M = Var x ⟹    P M"
    "⋀A B.   M = App A B ⟹  P M"
    "⋀x T A. M = Fn x T A ⟹ P M"
    "⋀A B.   M = Pair A B ⟹  P M"
    "⋀A.     M = Fst A ⟹  P M"
    "⋀A.     M = Snd A ⟹  P M"
    using assms by blast+
  thus "P M" using trm_cases[where M=M] by blast
qed

context fresh begin

lemma fresh_fn:
  fixes x :: 'a and S :: "'a set"
  assumes "finite S"
  shows "∃y B. y ∉ S ∧ B = [y ↔ x] ⋅ A ∧ (Fn x T A = Fn y T B)"
proof -
  have *: "finite ({x} ∪ fvs A ∪ S)" using fvs_finite assms by auto
  obtain y where "y = fresh_in ({x} ∪ fvs A ∪ S)" by auto
  hence "y ∉ ({x} ∪ fvs A ∪ S)" using fresh_axioms * unfolding class.fresh_def by metis
  hence "y ≠ x" "y ∉ fvs A" "y ∉ S" by auto

  obtain B where B: "B = [y ↔ x] ⋅ A" by auto
  hence "Fn x T A = Fn y T B" using fn_eq ‹y ≠ x› ‹y ∉ fvs A› by metis
  thus ?thesis using ‹y ≠ x› ‹y ∉ S› B by metis
qed

lemma trm_strong_induct:
  fixes P :: "'a set ⇒ 'a trm ⇒ bool"
  assumes
    "P S Unit"
    "⋀x. P S (Var x)"
    "⋀A B. ⟦P S A; P S B⟧ ⟹ P S (App A B)"
    "⋀x T. x ∉ S ⟹ (⋀A. P S A ⟹ P S (Fn x T A))"
    "⋀A B. ⟦P S A; P S B⟧ ⟹ P S (Pair A B)"
    "⋀A. P S A ⟹ P S (Fst A)"
    "⋀A. P S A ⟹ P S (Snd A)"
    "finite S"
  shows "P S M"
proof -
  have "⋀π. P S (π ⋅ M)"
  proof(induction M rule: trm_induct)
    case 1
      thus ?case using assms(1) trm_prm_simp(1) by metis
    next
    case (2 x)
      thus ?case using assms(2) trm_prm_simp(2) by metis
    next
    case (3 A B)
      thus ?case using assms(3) trm_prm_simp(3) by metis
    next
    case (4 x T A)
      have "finite S" "finite (fvs (π ⋅ A))" "finite {π $ x}"
        using ‹finite S› fvs_finite by auto
      hence "finite (S ∪ fvs (π ⋅ A) ∪ {π $ x})" by auto
      
      obtain y where "y = fresh_in (S ∪ fvs (π ⋅ A) ∪ {π $ x})" by auto
      hence "y ∉ S ∪ fvs (π ⋅ A) ∪ {π $ x}" using fresh_axioms unfolding class.fresh_def
        using ‹finite (S ∪ fvs (π ⋅ A) ∪ {π $ x})› by metis
      hence "y ≠ π $ x" "y ∉ fvs (π ⋅ A)" "y ∉ S" by auto
      hence *: "⋀A. P S A ⟹ P S (Fn y T A)" using assms(4) by metis
  
      have "P S (([y ↔ π $ x] ⋄ π) ⋅ A)" using 4 by metis
      hence "P S (Fn y T (([y ↔ π $ x] ⋄ π) ⋅ A))" using * by metis
      moreover have "(Fn y T (([y ↔ π $ x] ⋄ π) ⋅ A)) = Fn (π $ x) T (π ⋅ A)"
        using trm_prm_apply_compose fn_eq ‹y ≠ π $ x› ‹y ∉ fvs (π ⋅ A)› by metis
      ultimately show ?case using trm_prm_simp(4) by metis
    next
    case (5 A B)
      thus ?case using assms(5) trm_prm_simp(5) by metis
    next
    case (6 A)
      thus ?case using assms(6) trm_prm_simp(6) by metis
    next
    case (7 A)
      thus ?case using assms(7) trm_prm_simp(7) by metis
    next
  qed
  hence "P S (ε ⋅ M)" by metis
  thus "P S M" using trm_prm_apply_id by metis
qed

lemma trm_strong_cases:
  fixes P :: "'a set ⇒ 'a trm ⇒ bool"
  assumes
    "         M = Unit    ⟹ P S M"
    "⋀x.     M = Var x    ⟹ P S M"
    "⋀A B.   M = App A B  ⟹ P S M"
    "⋀x T A. M = Fn x T A ⟹ x ∉ S ⟹ P S M"
    "⋀A B.   M = Pair A B ⟹ P S M"
    "⋀A.     M = Fst A    ⟹ P S M"
    "⋀A.     M = Snd A    ⟹ P S M"
    "finite S"
  shows "P S M"
using assms by(induction S M rule: trm_strong_induct, metis+)

lemma trm_strong_depth_induct:
  fixes P :: "'a set ⇒ 'a trm ⇒ bool"
  assumes
    "P S Unit"
    "⋀x. P S (Var x)"
    "⋀A B. ⟦⋀K. depth K < depth (App A B) ⟹ P S K⟧ ⟹ P S (App A B)"
    "⋀x T. x ∉ S ⟹ (⋀A. (⋀K. depth K < depth (Fn x T A) ⟹ P S K) ⟹ P S (Fn x T A))"
    "⋀A B. ⟦⋀K. depth K < depth (Pair A B) ⟹ P S K⟧ ⟹ P S (Pair A B)"
    "⋀A. ⟦⋀K. depth K < depth (Fst A) ⟹ P S K⟧ ⟹ P S (Fst A)"
    "⋀A. ⟦⋀K. depth K < depth (Snd A) ⟹ P S K⟧ ⟹ P S (Snd A)"
    "finite S"
  shows "P S M"
proof(induction "depth M" arbitrary: M rule: less_induct)
  fix M :: "'a trm"
  assume IH: "depth K < depth M ⟹ P S K" for K
  hence
    "         M = Unit    ⟹ P S M"
    "⋀x.     M = Var x    ⟹ P S M"
    "⋀A B.   M = App A B  ⟹ P S M"
    "⋀x T A. M = Fn x T A ⟹ x ∉ S ⟹ P S M"
    "⋀A B.   M = Pair A B ⟹ P S M"
    "⋀A.     M = Fst A    ⟹ P S M"
    "⋀A.     M = Snd A    ⟹ P S M"
    "finite S"
    using assms IH by metis+
  thus "P S M" using trm_strong_cases[where M=M] by blast
qed

lemma trm_prm_fvs:
  shows "fvs (π ⋅ M) = π {$} fvs M"
by(transfer, metis ptrm_prm_fvs)

inductive typing :: "'a typing_ctx ⇒ 'a trm ⇒ type ⇒ bool" ("_ ⊢ _ : _") where
  tunit: "Γ ⊢ Unit : TUnit"
| tvar:  "Γ x = Some τ ⟹ Γ ⊢ Var x : τ"
| tapp:  "⟦Γ ⊢ f : (TArr τ σ); Γ ⊢ x : τ⟧ ⟹ Γ ⊢ App f x : σ"
| tfn:   "Γ(x ↦ τ) ⊢ A : σ ⟹ Γ ⊢ Fn x τ A : (TArr τ σ)"
| tpair: "⟦Γ ⊢ A : τ; Γ ⊢ B : σ⟧ ⟹ Γ ⊢ Pair A B : (TPair τ σ)"
| tfst:  "Γ ⊢ P : (TPair τ σ) ⟹ Γ ⊢ Fst P : τ"
| tsnd:  "Γ ⊢ P : (TPair τ σ) ⟹ Γ ⊢ Snd P : σ"

lemma typing_prm:
  assumes "Γ ⊢ M : τ" "⋀y. y ∈ fvs M ⟹ Γ y = Δ (π $ y)"
  shows "Δ ⊢ π ⋅ M : τ"
using assms proof(induction arbitrary: Δ rule: typing.induct)
  case (tunit Γ)
    thus ?case using typing.tunit trm_prm_simp(1) by metis
  next
  case (tvar Γ x τ)
    thus ?case using typing.tvar trm_prm_simp(2) fvs_simp(2) singletonI by metis
  next
  case (tapp Γ A τ σ B)
    thus ?case using typing.tapp trm_prm_simp(3) fvs_simp(3) UnCI by metis
  next
  case (tfn Γ x τ A σ)
    have "y ∈ fvs A ⟹ (Γ(x ↦ τ)) y = (Δ(π $ x ↦ τ)) (π $ y)" for y
    proof(cases "y = x")
      case True
        thus ?thesis using fun_upd_apply by simp
      next
      case False
        assume "y ∈ fvs A"
        hence "y ∈ fvs (Fn x τ A)" using fvs_simp(4) ‹y ≠ x› DiffI singletonD by fastforce
        hence "Γ y = Δ (π $ y)" using tfn.prems by metis
        thus ?thesis by (simp add: prm_apply_unequal)
      next
    qed
    hence "Δ(π $ x ↦ τ) ⊢ π ⋅ A : σ" using tfn.IH by metis
    thus ?case using trm_prm_simp(4) typing.tfn by metis
  next
  case (tpair Γ A B)
    thus ?case using typing.tpair trm_prm_simp(5) fvs_simp(5) UnCI by metis
  next
  case (tfst Γ P τ σ)
    thus ?case using typing.tfst trm_prm_simp(6) fvs_simp(6) by metis
  next
  case (tsnd Γ P τ σ)
    thus ?case using typing.tsnd trm_prm_simp(7) fvs_simp(7) by metis
  next
qed

lemma typing_swp:
  assumes "Γ(a ↦ σ) ⊢ M : τ" "b ∉ fvs M"
  shows "Γ(b ↦ σ) ⊢ [a ↔ b] ⋅ M : τ"
proof -
  have "y ∈ fvs M ⟹ (Γ(a ↦ σ)) y  = (Γ(b ↦ σ)) ([a ↔ b] $ y)" for y
  proof -
    assume "y ∈ fvs M"
    hence "y ≠ b" using assms(2) by auto
    consider "y = a" | "y ≠ a" by auto
    thus "(Γ(a ↦ σ)) y  = (Γ(b ↦ σ)) ([a ↔ b] $ y)"
    by(cases, simp add: prm_unit_action, simp add: prm_unit_inaction ‹y ≠ b›)
  qed
  thus ?thesis using typing_prm assms(1) by metis
qed

lemma typing_unitE:
  assumes "Γ ⊢ Unit : τ"
  shows "τ = TUnit"
using assms
  apply cases
  apply blast
  apply (auto simp add: unit_not_var unit_not_app unit_not_fn unit_not_pair unit_not_fst unit_not_snd)
done

lemma typing_varE:
  assumes "Γ ⊢ Var x : τ"
  shows "Γ x = Some τ"
using assms
  apply cases
  prefer 2
  apply (metis trm_simp(1))
  apply (metis unit_not_var)
  apply (auto simp add: var_not_app var_not_fn var_not_pair var_not_fst var_not_snd)
done

lemma typing_appE:
  assumes "Γ ⊢ App A B : σ"
  shows "∃τ. (Γ ⊢ A : (TArr τ σ)) ∧ (Γ ⊢ B : τ)"
using assms
  apply cases
  prefer 3
  apply (metis trm_simp(2, 3))
  apply (metis unit_not_app)
  apply (metis var_not_app)
  apply (auto simp add: app_not_fn app_not_pair app_not_fst app_not_snd)
done

lemma typing_fnE:
  assumes "Γ ⊢ Fn x T A : θ"
  shows "∃σ. θ = (TArr T σ) ∧ (Γ(x ↦ T) ⊢ A : σ)"
using assms proof(cases)
  case (tfn y S B σ)
    from this consider
      "x = y ∧ T = S ∧ A = B" | "x ≠ y ∧ T = S ∧ x ∉ fvs B ∧ A = [x ↔ y] ⋅ B"
      using trm_simp(4) by metis
    thus ?thesis proof(cases)
      case 1
        thus ?thesis using tfn by metis
      next
      case 2
        thus ?thesis using tfn typing_swp prm_unit_commutes by metis
      next
    qed
  next
qed (
  metis unit_not_fn,
  metis var_not_fn,
  metis app_not_fn,
  metis fn_not_pair,
  metis fn_not_fst,
  metis fn_not_snd
)

lemma typing_pairE:
  assumes "Γ ⊢ Pair A B : θ"
  shows "∃τ σ. θ = (TPair τ σ) ∧ (Γ ⊢ A : τ) ∧ (Γ ⊢ B : σ)"
using assms proof(cases)
  case (tpair A τ B σ)
    thus ?thesis using trm_simp(5) trm_simp(6) by blast
  next
qed (
  metis unit_not_pair,
  metis var_not_pair,
  metis app_not_pair,
  metis fn_not_pair,
  metis pair_not_fst,
  metis pair_not_snd
)

lemma typing_fstE:
  assumes "Γ ⊢ Fst P : τ"
  shows "∃σ. (Γ ⊢ P : (TPair τ σ))"
using assms proof(cases)
  case (tfst P σ)
    thus ?thesis using trm_simp(7) by blast
  next
qed (
  metis unit_not_fst,
  metis var_not_fst,
  metis app_not_fst,
  metis fn_not_fst,
  metis pair_not_fst,
  metis fst_not_snd
)

lemma typing_sndE:
  assumes "Γ ⊢ Snd P : σ"
  shows "∃τ. (Γ ⊢ P : (TPair τ σ))"
using assms proof(cases)
  case (tsnd P σ)
    thus ?thesis using trm_simp(8) by blast
  next
qed (
  metis unit_not_snd,
  metis var_not_snd,
  metis app_not_snd,
  metis fn_not_snd,
  metis pair_not_snd,
  metis fst_not_snd
)

theorem typing_weaken:
  assumes "Γ ⊢ M : τ" "y ∉ fvs M"
  shows "Γ(y ↦ σ) ⊢ M : τ"
using assms proof(induction rule: typing.induct)
  case (tunit Γ)
    thus ?case using typing.tunit by metis
  next
  case (tvar Γ x τ)
    hence "y ≠ x" using fvs_simp(2) singletonI by force
    hence "(Γ(y ↦ σ)) x = Some τ" using tvar.hyps fun_upd_apply by simp
    thus ?case using typing.tvar by metis
  next
  case (tapp Γ f τ τ' x)
    from ‹y ∉ fvs (App f x)› have "y ∉ fvs f" "y ∉ fvs x" using fvs_simp(3) Un_iff by force+
    hence "Γ(y ↦ σ) ⊢ f : (TArr τ τ')" "Γ(y ↦ σ) ⊢ x : τ" using tapp.IH by metis+
    thus ?case using typing.tapp by metis
  next
  case (tfn Γ x τ A τ')
    from ‹y ∉ fvs (Fn x τ A)› consider "y = x" | "y ≠ x ∧ y ∉ fvs A"
      using fvs_simp(4) DiffI empty_iff insert_iff by fastforce
    thus ?case proof(cases)
      case 1
        hence "(Γ(y ↦ σ, x ↦ τ)) ⊢ A : τ'" using tfn.hyps fun_upd_upd by simp
        thus ?thesis using typing.tfn by metis
      next
      case 2
        hence "y ≠ x" "y ∉ fvs A" by auto
        hence "Γ(x ↦ τ, y ↦ σ) ⊢ A : τ'" using tfn.IH by metis
        hence "Γ(y ↦ σ, x ↦ τ) ⊢ A : τ'" using ‹y ≠ x› fun_upd_twist by metis
        thus ?thesis using typing.tfn by metis
      next
    qed
  next
  case (tpair Γ A τ B σ)
    thus ?case using typing.tpair fvs_simp(5) UnCI by metis
  next
  case (tfst Γ P τ σ)
    thus ?case using typing.tfst fvs_simp(6) by metis
  next
  case (tsnd Γ P τ σ)
    thus ?case using typing.tsnd fvs_simp(7) by metis
  next
qed


lift_definition infer :: "'a typing_ctx ⇒ 'a trm ⇒ type option" is ptrm_infer_type
using ptrm_infer_type_alpha_equiv.

export_code infer fresh_nat_inst.fresh_in_nat in Haskell

lemma infer_simp:
  shows
    "infer Γ Unit = Some TUnit"
    "infer Γ (Var x) = Γ x"
    "infer Γ (App A B) = (case (infer Γ A, infer Γ B) of
       (Some (TArr τ σ), Some τ') ⇒ (if τ = τ' then Some σ else None)
     | _ ⇒ None
     )"
    "infer Γ (Fn x τ A) = (case infer (Γ(x ↦ τ)) A of
       Some σ ⇒ Some (TArr τ σ)
     | None ⇒ None
    )"
    "infer Γ (Pair A B) = (case (infer Γ A, infer Γ B) of
       (Some τ, Some σ) ⇒ Some (TPair τ σ)
     | _ ⇒ None
     )"
    "infer Γ (Fst P) = (case infer Γ P of
       (Some (TPair τ σ)) ⇒ Some τ
     | _ ⇒ None
     )"
    "infer Γ (Snd P) = (case infer Γ P of
       (Some (TPair τ σ)) ⇒ Some σ
     | _ ⇒ None
     )"
by((transfer, simp)+)

lemma infer_unitE:
  assumes "infer Γ Unit = Some τ"
  shows "τ = TUnit"
using assms by(transfer, simp)

lemma infer_varE:
  assumes "infer Γ (Var x) = Some τ"
  shows "Γ x = Some τ"
using assms by(transfer, simp)

lemma infer_appE:
  assumes "infer Γ (App A B) = Some τ"
  shows "∃σ. infer Γ A = Some (TArr σ τ) ∧ infer Γ B = Some σ"
using assms proof(transfer)
  fix Γ :: "'a typing_ctx" and A B τ
  assume H: "ptrm_infer_type Γ (PApp A B) = Some τ"

  have "ptrm_infer_type Γ A ≠ None"
  proof(rule classical, auto)
    assume "ptrm_infer_type Γ A = None"
    hence "ptrm_infer_type Γ (PApp A B) = None" by auto
    thus False using H by auto
  qed
  from this obtain T where *: "ptrm_infer_type Γ A = Some T" by auto

  have "T ≠ TVar x" for x
  proof(rule classical, auto)
    fix x
    assume "T = TVar x"
    hence "ptrm_infer_type Γ A = Some (TVar x)" using * by metis
    hence "ptrm_infer_type Γ (PApp A B) = None" by simp
    thus False using H by auto
  qed
  moreover have "T ≠ TUnit"
  proof(rule classical, auto)
    fix x
    assume "T = TUnit"
    hence "ptrm_infer_type Γ A = Some TUnit" using * by metis
    hence "ptrm_infer_type Γ (PApp A B) = None" by simp
    thus False using H by auto
  qed
  moreover have "T ≠ TPair τ σ" for τ σ
  proof(rule classical, auto)
    fix τ σ
    assume "T = TPair τ σ"
    hence "ptrm_infer_type Γ A = Some (TPair τ σ)" using * by metis
    hence "ptrm_infer_type Γ (PApp A B) = None" by simp
    thus False using H by auto
  qed
  ultimately obtain σ τ' where "T = TArr σ τ'" by(cases T, blast, auto)
  hence *: "ptrm_infer_type Γ A = Some (TArr σ τ')" using * by metis

  have "ptrm_infer_type Γ B ≠ None"
  proof(rule classical, auto)
    assume "ptrm_infer_type Γ B = None"
    hence "ptrm_infer_type Γ (PApp A B) = None" using * by auto
    thus False using H by auto
  qed
  from this obtain σ' where **: "ptrm_infer_type Γ B = Some σ'" by auto

  have "σ = σ'"
  proof(rule classical)
    assume "σ ≠ σ'"
    hence "ptrm_infer_type Γ (PApp A B) = None" using * ** by simp
    hence False using H by auto
    thus "σ = σ'" by blast
  qed
  hence **: "ptrm_infer_type Γ B = Some σ" using ** by auto

  have "ptrm_infer_type Γ (PApp A B) = Some τ'" using * ** by auto
  hence "τ = τ'" using H by auto
  hence *: "ptrm_infer_type Γ A = Some (TArr σ τ)" using * by auto

  show "∃σ. ptrm_infer_type Γ A = Some (TArr σ τ) ∧ ptrm_infer_type Γ B = Some σ"
    using * ** by auto
qed

lemma infer_fnE:
  assumes "infer Γ (Fn x T A) = Some τ"
  shows "∃σ. τ = TArr T σ ∧ infer (Γ(x ↦ T)) A = Some σ"
using assms proof(transfer)
  fix x :: 'a and Γ T A τ
  assume H: "ptrm_infer_type Γ (PFn x T A) = Some τ"

  have "ptrm_infer_type (Γ(x ↦ T)) A ≠ None"
  proof(rule classical, auto)
    assume "ptrm_infer_type (Γ(x ↦ T)) A = None"
    hence "ptrm_infer_type Γ (PFn x T A) = None" by auto
    thus False using H by auto
  qed
  from this obtain σ where *: "ptrm_infer_type (Γ(x ↦ T)) A = Some σ" by auto

  have "ptrm_infer_type Γ (PFn x T A) = Some (TArr T σ)" using * by auto
  hence "τ = TArr T σ" using H by auto
  thus "∃σ. τ = TArr T σ ∧ ptrm_infer_type (Γ(x ↦ T)) A = Some σ"
    using * by auto
qed

lemma infer_pairE:
  assumes "infer Γ (Pair A B) = Some τ"
  shows "∃T S. τ = TPair T S ∧ infer Γ A = Some T ∧ infer Γ B = Some S"
using assms proof(transfer)
  fix A B :: "'a ptrm" and Γ τ
  assume H: "ptrm_infer_type Γ (PPair A B) = Some τ"

  have "ptrm_infer_type Γ A ≠ None"
  proof(rule classical, auto)
    assume "ptrm_infer_type Γ A = None"
    hence "ptrm_infer_type Γ (PPair A B) = None" by auto
    thus False using H by auto
  qed
  moreover have "ptrm_infer_type Γ B ≠ None"
  proof(rule classical, auto)
    assume "ptrm_infer_type Γ B = None"
    hence "ptrm_infer_type Γ (PPair A B) = None" by (simp add: option.case_eq_if)
    thus False using H by auto
  qed
  ultimately obtain T S
    where "τ = TPair T S" "ptrm_infer_type Γ A = Some T" "ptrm_infer_type Γ B = Some S"
    using H by auto
  thus "∃T S. τ = TPair T S ∧ ptrm_infer_type Γ A = Some T ∧ ptrm_infer_type Γ B = Some S" by auto
qed

lemma infer_fstE:
  assumes "infer Γ (Fst P) = Some τ"
  shows "∃T S. infer Γ P = Some (TPair T S) ∧ τ = T"
using assms proof(transfer)
  fix P :: "'a ptrm" and Γ τ
  assume H: "ptrm_infer_type Γ (PFst P) = Some τ"

  have "ptrm_infer_type Γ P ≠ None"
  proof(rule classical, auto)
    assume "ptrm_infer_type Γ P = None"
    thus False using H by simp
  qed
  moreover have "ptrm_infer_type Γ P ≠ Some TUnit"
  proof(rule classical, auto)
    assume "ptrm_infer_type Γ P = Some TUnit"
    thus False using H by simp
  qed
  moreover have "ptrm_infer_type Γ P ≠ Some (TVar x)" for x
  proof(rule classical, auto)
    assume "ptrm_infer_type Γ P = Some (TVar x)"
    thus False using H by simp
  qed
  moreover have "ptrm_infer_type Γ P ≠ Some (TArr T S)" for T S
  proof(rule classical, auto)
    assume "ptrm_infer_type Γ P = Some (TArr T S)"
    thus False using H by simp
  qed
  ultimately obtain T S where
    "ptrm_infer_type Γ P = Some (TPair T S)"
    using type.distinct type.exhaust option.exhaust by metis
  moreover hence "ptrm_infer_type Γ (PFst P) = Some T" by simp
  ultimately show "∃T S. ptrm_infer_type Γ P = Some (TPair T S) ∧ τ = T"
    using H by auto
qed

lemma infer_sndE:
  assumes "infer Γ (Snd P) = Some τ"
  shows "∃T S. infer Γ P = Some (TPair T S) ∧ τ = S"
using assms proof(transfer)
  fix P :: "'a ptrm" and Γ τ
  assume H: "ptrm_infer_type Γ (PSnd P) = Some τ"

  have "ptrm_infer_type Γ P ≠ None"
  proof(rule classical, auto)
    assume "ptrm_infer_type Γ P = None"
    thus False using H by simp
  qed
  moreover have "ptrm_infer_type Γ P ≠ Some TUnit"
  proof(rule classical, auto)
    assume "ptrm_infer_type Γ P = Some TUnit"
    thus False using H by simp
  qed
  moreover have "ptrm_infer_type Γ P ≠ Some (TVar x)" for x
  proof(rule classical, auto)
    assume "ptrm_infer_type Γ P = Some (TVar x)"
    thus False using H by simp
  qed
  moreover have "ptrm_infer_type Γ P ≠ Some (TArr T S)" for T S
  proof(rule classical, auto)
    assume "ptrm_infer_type Γ P = Some (TArr T S)"
    thus False using H by simp
  qed
  ultimately obtain T S where
    "ptrm_infer_type Γ P = Some (TPair T S)"
    using type.distinct type.exhaust option.exhaust by metis
  moreover hence "ptrm_infer_type Γ (PSnd P) = Some S" by simp
  ultimately show "∃T S. ptrm_infer_type Γ P = Some (TPair T S) ∧ τ = S"
    using H by auto
qed

lemma infer_sound:
  assumes "infer Γ M = Some τ"
  shows "Γ ⊢ M : τ"
using assms proof(induction M arbitrary: Γ τ rule: trm_induct)
  case 1
    thus ?case using infer_unitE typing.tunit by metis
  next
  case (2 x)
    hence "Γ x = Some τ" using infer_varE by metis
    thus ?case using typing.tvar by metis
  next
  case (3 A B)
    from ‹infer Γ (App A B) = Some τ› obtain σ
      where "infer Γ A = Some (TArr σ τ)" and "infer Γ B = Some σ"
      using infer_appE by metis
    thus ?case using "3.IH" typing.tapp by metis
  next
  case (4 x T A Γ τ)
    from ‹infer Γ (Fn x T A) = Some τ› obtain σ
      where "τ = TArr T σ" and "infer (Γ(x ↦ T)) A = Some σ"
      using infer_fnE by metis
    thus ?case using "4.IH" typing.tfn by metis
  next
  case (5 A B Γ τ)
    thus ?case using typing.tpair infer_pairE by metis
  next
  case (6 P Γ τ)
    thus ?case using typing.tfst infer_fstE by metis
  next
  case (7 P Γ τ)
    thus ?case using typing.tsnd infer_sndE by metis
  next
qed

lemma infer_complete:
  assumes "Γ ⊢ M : τ"
  shows "infer Γ M = Some τ"
using assms proof(induction)
  case (tfn Γ x τ A σ)
    thus ?case by (simp add: infer_simp(4) tfn.IH)
  next
qed (auto simp add: infer_simp)

theorem infer_valid:
  shows "(Γ ⊢ M : τ) = (infer Γ M = Some τ)"
using infer_sound infer_complete by blast

inductive substitutes :: "'a trm ⇒ 'a ⇒ 'a trm ⇒ 'a trm ⇒ bool" where
  unit: "substitutes Unit y M Unit"
| var1: "x = y ⟹ substitutes (Var x) y M M"
| var2: "x ≠ y ⟹ substitutes (Var x) y M (Var x)"
| app:  "⟦substitutes A x M A'; substitutes B x M B'⟧ ⟹ substitutes (App A B) x M (App A' B')"
| fn:   "⟦x ≠ y; y ∉ fvs M; substitutes A x M A'⟧ ⟹ substitutes (Fn y T A) x M (Fn y T A')"
| pair: "⟦substitutes A x M A'; substitutes B x M B'⟧ ⟹ substitutes (Pair A B) x M (Pair A' B')"
| fst:  "substitutes P x M P' ⟹ substitutes (Fst P) x M (Fst P')"
| snd:  "substitutes P x M P' ⟹ substitutes (Snd P) x M (Snd P')"

lemma substitutes_prm:
  assumes "substitutes A x M A'"
  shows "substitutes (π ⋅ A) (π $ x) (π ⋅ M) (π ⋅ A')"
using assms proof(induction)
  case (unit y M)
    thus ?case using substitutes.unit trm_prm_simp(1) by metis
  case (var1 x y M)
    thus ?case using substitutes.var1 trm_prm_simp(2) by metis
  next
  case (var2 x y M)
    thus ?case using substitutes.var2 trm_prm_simp(2) prm_apply_unequal by metis
  next
  case (app A x M A' B B')
    thus ?case using substitutes.app trm_prm_simp(3) by metis
  next
  case (fn x y M A A' T)
    thus ?case
      using substitutes.fn trm_prm_simp(4) prm_apply_unequal prm_set_notmembership trm_prm_fvs
      by metis
  next
  case (pair A x M A' B B')
    thus ?case using substitutes.pair trm_prm_simp(5) by metis
  next
  case (fst P x M P')
    thus ?case using substitutes.fst trm_prm_simp(6) by metis
  next
  case (snd P x M P')
    thus ?case using substitutes.snd trm_prm_simp(7) by metis
  next
qed

lemma substitutes_fvs:
  assumes "substitutes A x M A'"
  shows "fvs A' ⊆ fvs A - {x} ∪ fvs M"
using assms proof(induction)
  case (unit y M)
    thus ?case using fvs_simp(1) by auto
  case (var1 x y M)
    thus ?case by auto
  next
  case (var2 x y M)
    thus ?case
      using fvs_simp(2) Un_subset_iff Un_upper2 insert_Diff_if insert_is_Un singletonD sup_commute
      by metis
  next
  case (app A x M A' B B')
    hence "fvs A' ∪ fvs B' ⊆ (fvs A - {x} ∪ fvs M) ∪ (fvs B - {x} ∪ fvs M)" by auto
    hence "fvs A' ∪ fvs B' ⊆ (fvs A ∪ fvs B) - {x} ∪ fvs M" by auto
    thus ?case using fvs_simp(3) by metis
  next
  case (fn x y M A A' T)
    hence "fvs A' - {y} ⊆ fvs A - {y} - {x} ∪ fvs M" by auto
    thus ?case using fvs_simp(4) by metis
  next
  case (pair A x M A' B B')
    hence "fvs A' ∪ fvs B' ⊆ (fvs A - {x} ∪ fvs M) ∪ (fvs B - {x} ∪ fvs M)" by auto
    hence "fvs A' ∪ fvs B' ⊆ (fvs A ∪ fvs B) - {x} ∪ fvs M" by auto
    thus ?case using fvs_simp(5) by metis
  next
  case (fst P x M P')
    thus ?case using fvs_simp(6) by fastforce
  next
  case (snd P x M P')
    thus ?case using fvs_simp(7) by fastforce
  next
qed

inductive_cases substitutes_unitE': "substitutes Unit y M X"
lemma substitutes_unitE:
  assumes "substitutes Unit y M X"
  shows "X = Unit"
by(
  rule substitutes_unitE'[where y=y and M=M and X=X],
  metis assms,
  auto simp add: unit_not_var unit_not_app unit_not_fn unit_not_pair unit_not_fst unit_not_snd
)

inductive_cases substitutes_varE': "substitutes (Var x) y M X"
lemma substitutes_varE:
  assumes "substitutes (Var x) y M X"
  shows "(x = y ∧ M = X) ∨ (x ≠ y ∧ X = Var x)"
by(
  rule substitutes_varE'[where x=x and y=y and M=M and X=X],
  metis assms,
  metis unit_not_var,
  metis trm_simp(1),
  metis trm_simp(1),
  auto simp add: var_not_app var_not_fn var_not_pair var_not_fst var_not_snd
)

inductive_cases substitutes_appE': "substitutes (App A B) x M X"
lemma substitutes_appE:
  assumes "substitutes (App A B) x M X"
  shows "∃A' B'. substitutes A x M A' ∧ substitutes B x M B' ∧ X = App A' B'"
by(
  cases rule: substitutes_appE'[where A=A and B=B and x=x and M=M and X=X],
  metis assms,
  metis unit_not_app,
  metis var_not_app,
  metis var_not_app,
  metis trm_simp(2,3),
  auto simp add: app_not_fn app_not_pair app_not_fst app_not_snd
)

inductive_cases substitutes_fnE': "substitutes (Fn y T A) x M X"
lemma substitutes_fnE:
  assumes "substitutes (Fn y T A) x M X" "y ≠ x" "y ∉ fvs M"
  shows "∃A'. substitutes A x M A' ∧ X = Fn y T A'"
using assms proof(induction rule: substitutes_fnE'[where y=y and T=T and A=A and x=x and M=M and X=X])
  case (6 z B B' S)
    consider "y = z ∧ T = S ∧ A = B" | "y ≠ z ∧ T = S ∧ y ∉ fvs B ∧ A = [y ↔ z] ⋅ B"
      using ‹Fn y T A = Fn z S B› trm_simp(4) by metis
    thus ?case proof(cases)
      case 1
        thus ?thesis using 6 by metis
      next
      case 2
        hence "y ≠ z" "T = S" "y ∉ fvs B" "A = [y ↔ z] ⋅ B" by auto
        have "substitutes ([y ↔ z] ⋅ B) ([y ↔ z] $ x) ([y ↔ z] ⋅ M) ([y ↔ z] ⋅ B')"
          using substitutes_prm ‹substitutes B x M B'› by metis
        hence "substitutes A ([y ↔ z] $ x) ([y ↔ z] ⋅ M) ([y ↔ z] ⋅ B')"
          using ‹A = [y ↔ z] ⋅ B› by metis
        hence "substitutes A x ([y ↔ z] ⋅ M) ([y ↔ z] ⋅ B')"
          using ‹y ≠ x› ‹x ≠ z› prm_unit_inaction by metis
        hence *: "substitutes A x M ([y ↔ z] ⋅ B')"
          using ‹y ∉ fvs M› ‹z ∉ fvs M› trm_prm_unit_inaction by metis

        have "y ∉ fvs B'"
          using
            substitutes_fvs ‹substitutes B x M B'› ‹y ∉ fvs B› ‹y ∉ fvs M›
            Diff_subset UnE rev_subsetD
          by blast
        hence "X = Fn y T ([y ↔ z] ⋅ B')"
          using ‹X = Fn z S B'› ‹y ≠ z› ‹T = S› fn_eq
          by metis

        thus ?thesis using * by auto
      next
    qed      
  next
qed (
  metis assms(1),
  metis unit_not_fn,
  metis var_not_fn,
  metis var_not_fn,
  metis app_not_fn,
  metis fn_not_pair,
  metis fn_not_fst,
  metis fn_not_snd
)

inductive_cases substitutes_pairE': "substitutes (Pair A B) x M X"
lemma substitutes_pairE:
  assumes "substitutes (Pair A B) x M X"
  shows "∃A' B'. substitutes A x M A' ∧ substitutes B x M B' ∧ X = Pair A' B'"
proof(cases rule: substitutes_pairE'[where A=A and B=B and x=x and M=M and X=X])
  case (7 A A' B B')
    thus ?thesis using trm_simp(5) trm_simp(6) by blast
  next
qed (
  metis assms,
  metis unit_not_pair,
  metis var_not_pair,
  metis var_not_pair,
  metis app_not_pair,
  metis fn_not_pair,
  metis pair_not_fst,
  metis pair_not_snd
)

inductive_cases substitutes_fstE': "substitutes (Fst P) x M X"
lemma substitutes_fstE:
  assumes "substitutes (Fst P) x M X"
  shows "∃P'. substitutes P x M P' ∧ X = Fst P'"
proof(cases rule: substitutes_fstE'[where P=P and x=x and M=M and X=X])
  case (8 P P')
    thus ?thesis using trm_simp(7) by blast
  next
qed (
  metis assms,
  metis unit_not_fst,
  metis var_not_fst,
  metis var_not_fst,
  metis app_not_fst,
  metis fn_not_fst,
  metis pair_not_fst,
  metis fst_not_snd
)

inductive_cases substitutes_sndE': "substitutes (Snd P) x M X"
lemma substitutes_sndE:
  assumes "substitutes (Snd P) x M X"
  shows "∃P'. substitutes P x M P' ∧ X = Snd P'"
proof(cases rule: substitutes_sndE'[where P=P and x=x and M=M and X=X])
  case (9 P P')
    thus ?thesis using trm_simp(8) by blast
  next
qed (
  metis assms,
  metis unit_not_snd,
  metis var_not_snd,
  metis var_not_snd,
  metis app_not_snd,
  metis fn_not_snd,
  metis pair_not_snd,
  metis fst_not_snd
)

lemma substitutes_total:
  shows "∃X. substitutes A x M X"
proof(induction A rule: trm_strong_induct[where S="{x} ∪ fvs M"])
  show "finite ({x} ∪ fvs M)" using fvs_finite by auto
  next

  case 1
    obtain X :: "'a trm" where "X = Unit" by auto
    thus ?case using substitutes.unit by metis
  next
  case (2 y)
    consider "x = y" | "x ≠ y" by auto
    thus ?case proof(cases)
      case 1
        obtain X where "X = M" by auto
        hence "substitutes (Var y) x M X" using ‹x = y› substitutes.var1 by metis
        thus ?thesis by auto
      next
      case 2
        obtain X where "X = (Var y)" by auto
        hence "substitutes (Var y) x M X" using ‹x ≠ y› substitutes.var2 by metis
        thus ?thesis by auto
      next
    qed
  next
  case (3 A B)
    from this obtain A' B' where A': "substitutes A x M A'" and B': "substitutes B x M B'" by auto
    obtain X where "X = App A' B'" by auto
    hence "substitutes (App A B) x M X" using A' B' substitutes.app by metis
    thus ?case by auto
  next
  case (4 y T A)
    from this obtain A' where A': "substitutes A x M A'" by auto
    from ‹y ∉ ({x} ∪ fvs M)› have "y ≠ x" "y ∉ fvs M" by auto
    obtain X where "X = Fn y T A'" by auto
    hence "substitutes (Fn y T A) x M X" using substitutes.fn ‹y ≠ x› ‹y ∉ fvs M› A' by metis
    thus ?case by auto
  next
  case (5 A B)
    from this obtain A' B' where "substitutes A x M A'" "substitutes B x M B'" by auto
    from this obtain X where "X = Pair A' B'" by auto
    hence "substitutes (Pair A B) x M X"
      using substitutes.pair ‹substitutes A x M A'› ‹substitutes B x M B'›
      by metis
    thus ?case by auto
  next
  case (6 P)
    from this obtain P' where "substitutes P x M P'" by auto
    from this obtain X where "X = Fst P'" by auto
    hence "substitutes (Fst P) x M X" using substitutes.fst ‹substitutes P x M P'› by metis
    thus ?case by auto
  next
  case (7 P)
    from this obtain P' where "substitutes P x M P'" by auto
    from this obtain X where "X = Snd P'" by auto
    hence "substitutes (Snd P) x M X" using substitutes.snd ‹substitutes P x M P'› by metis
    thus ?case by auto
  next
qed

lemma substitutes_unique:
  assumes "substitutes A x M B" "substitutes A x M C"
  shows "B = C"
using assms proof(induction A arbitrary: B C rule: trm_strong_induct[where S="{x} ∪ fvs M"])
  show "finite ({x} ∪ fvs M)" using fvs_finite by auto
  next

  case 1
    thus ?case using substitutes_unitE by metis
  next
  case (2 y)
    thus ?case using substitutes_varE by metis
  next
  case (3 X Y)
    thus ?case using substitutes_appE by metis
  next
  case (4 y T A)
    hence "y ≠ x" and "y ∉ fvs M" by auto
    thus ?case using 4 substitutes_fnE by metis
  next
  case (5 A B C D)
    thus ?case using substitutes_pairE by metis
  next
  case (6 P Q R)
    thus ?case using substitutes_fstE by metis
  next
  case (7 P Q R)
    thus ?case using substitutes_sndE by metis
  next
qed

lemma substitutes_function:
  shows "∃! X. substitutes A x M X"
using substitutes_total substitutes_unique by metis

definition subst :: "'a trm ⇒ 'a ⇒ 'a trm ⇒ 'a trm" ("_[_ ::= _]") where
  "subst A x M ≡ (THE X. substitutes A x M X)"

lemma subst_simp_unit:
  shows "Unit[x ::= M] = Unit"
unfolding subst_def by(rule, metis substitutes.unit, metis substitutes_function substitutes.unit)

lemma subst_simp_var1:
  shows "(Var x)[x ::= M] = M"
unfolding subst_def by(rule, metis substitutes.var1, metis substitutes_function substitutes.var1)

lemma subst_simp_var2:
  assumes "x ≠ y"
  shows "(Var x)[y ::= M] = Var x"
unfolding subst_def by(
  rule,
  metis substitutes.var2 assms,
  metis substitutes_function substitutes.var2 assms
)

lemma subst_simp_app:
  shows "(App A B)[x ::= M] = App (A[x ::= M]) (B[x ::= M])"
unfolding subst_def proof
  obtain A' B' where A': "A' = (A[x ::= M])" and B': "B' = (B[x ::= M])" by auto
  hence "substitutes A x M A'" "substitutes B x M B'"
    unfolding subst_def
    using substitutes_function theI by metis+
  hence "substitutes (App A B) x M (App A' B')" using substitutes.app by metis
  thus *: "substitutes (App A B) x M (App (THE X. substitutes A x M X) (THE X. substitutes B x M X))"
    using A' B' unfolding subst_def by metis

  fix X
  assume "substitutes (App A B) x M X"
  thus "X = App (THE X. substitutes A x M X) (THE X. substitutes B x M X)"
    using substitutes_function * by metis
qed

lemma subst_simp_fn:
  assumes "x ≠ y" "y ∉ fvs M"
  shows "(Fn y T A)[x ::= M] = Fn y T (A[x ::= M])"
unfolding subst_def proof
  obtain A' where A': "A' = (A[x ::= M])" by auto
  hence "substitutes A x M A'" unfolding subst_def using substitutes_function theI by metis
  hence "substitutes (Fn y T A) x M (Fn y T A')" using substitutes.fn assms by metis
  thus *: "substitutes (Fn y T A) x M (Fn y T (THE X. substitutes A x M X))"
    using A' unfolding subst_def by metis

  fix X
  assume "substitutes (Fn y T A) x M X"
  thus "X = Fn y T (THE X. substitutes A x M X)" using substitutes_function * by metis
qed

lemma subst_simp_pair:
  shows "(Pair A B)[x ::= M] = Pair (A[x ::= M]) (B[x ::= M])"
unfolding subst_def proof
  obtain A' B' where A': "A' = (A[x ::= M])" and B': "B' = (B[x ::= M])" by auto
  hence "substitutes A x M A'" "substitutes B x M B'"
    unfolding subst_def using substitutes_function theI by metis+
  hence "substitutes (Pair A B) x M (Pair A' B')" using substitutes.pair by metis
  thus *: "substitutes (Pair A B) x M (Pair (THE X. substitutes A x M X) (THE X. substitutes B x M X))"
    using A' B' unfolding subst_def by metis

  fix X
  assume "substitutes (Pair A B) x M X"
  thus "X = Pair (THE X. substitutes A x M X) (THE X. substitutes B x M X)"
    using substitutes_function * by metis
qed

lemma subst_simp_fst:
  shows "(Fst P)[x ::= M] = Fst (P[x ::= M])"
unfolding subst_def proof
  obtain P' where P': "P' = (P[x ::= M])" by auto
  hence "substitutes P x M P'" unfolding subst_def using substitutes_function theI by metis
  hence "substitutes (Fst P) x M (Fst P')" using substitutes.fst by metis
  thus *: "substitutes (Fst P) x M (Fst (THE X. substitutes P x M X))"
    using P' unfolding subst_def by metis

  fix X
  assume "substitutes (Fst P) x M X"
  thus "X = Fst (THE X. substitutes P x M X)" using substitutes_function * by metis
qed

lemma subst_simp_snd:
  shows "(Snd P)[x ::= M] = Snd (P[x ::= M])"
unfolding subst_def proof
  obtain P' where P': "P' = (P[x ::= M])" by auto
  hence "substitutes P x M P'" unfolding subst_def using substitutes_function theI by metis
  hence "substitutes (Snd P) x M (Snd P')" using substitutes.snd by metis
  thus *: "substitutes (Snd P) x M (Snd (THE X. substitutes P x M X))"
    using P' unfolding subst_def by metis

  fix X
  assume "substitutes (Snd P) x M X"
  thus "X = Snd (THE X. substitutes P x M X)" using substitutes_function * by metis
qed

lemma subst_prm:
  shows "(π ⋅ (M[z ::= N])) = ((π ⋅ M)[π $ z ::= π ⋅ N])"
unfolding subst_def using substitutes_prm substitutes_function the1_equality by (metis (full_types))

lemma subst_fvs:
  shows "fvs (M[z ::= N]) ⊆ (fvs M - {z}) ∪ fvs N"
unfolding subst_def using substitutes_fvs substitutes_function theI2 by metis

lemma subst_free:
  assumes "y ∉ fvs M"
  shows "M[y ::= N] = M"
using assms proof(induction M rule: trm_strong_induct[where S="{y} ∪ fvs N"])
  show "finite ({y} ∪ fvs N)" using fvs_finite by auto

  case 1
    thus ?case using subst_simp_unit by metis
  next
  case (2 x)
    thus ?case using subst_simp_var2 by (simp add: fvs_simp)
  next
  case (3 A B)
    thus ?case using subst_simp_app by (simp add: fvs_simp)
  next
  case (4 x T A)
    hence "y ≠ x" "x ∉ fvs N" by auto
    
    have "y ∉ fvs A - {x}" using ‹y ≠ x› ‹y ∉ fvs (Fn x T A)› fvs_simp(4) by metis
    hence "y ∉ fvs A" using ‹y ≠ x› by auto
    hence "A[y ::= N] = A" using "4.IH" by blast
    thus ?case using ‹y ≠ x› ‹y ∉ fvs A› ‹x ∉ fvs N› subst_simp_fn by metis
  next
  case (5 A B)
    thus ?case using subst_simp_pair by (simp add: fvs_simp)
  next
  case (6 P)
    thus ?case using subst_simp_fst by (simp add: fvs_simp)
  next
  case (7 P)
    thus ?case using subst_simp_snd by (simp add: fvs_simp)
  next
qed

lemma subst_swp:
  assumes "y ∉ fvs A"
  shows "([y ↔ z] ⋅ A)[y ::= M] = (A[z ::= M])"
using assms proof(induction A rule: trm_strong_induct[where S="{y, z} ∪ fvs M"])
  show "finite ({y, z} ∪ fvs M)" using fvs_finite by auto
  next

  case 1
    thus ?case using trm_prm_simp(1) subst_simp_unit by metis
  next
  case (2 x)
    hence "y ≠ x" using fvs_simp(2) by force
    consider "x = z" | "x ≠ z" by auto
    thus ?case proof(cases)
      case 1
        thus ?thesis using subst_simp_var1 trm_prm_simp(2) prm_unit_action prm_unit_commutes by metis
      next
      case 2
        thus ?thesis using subst_simp_var2 trm_prm_simp(2) prm_unit_inaction ‹y ≠ x› by metis
      next
    qed
  next
  case (3 A B)
    from ‹y ∉ fvs (App A B)› have "y ∉ fvs A" "y ∉ fvs B" by (auto simp add: fvs_simp(3))
    thus ?case using "3.IH" subst_simp_app trm_prm_simp(3) by metis
  next
  case (4 x T A)
    hence "x ≠ y" "x ≠ z" "x ∉ fvs M"