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" by auto
    hence "y ∉ fvs A" using ‹y ∉ fvs (Fn x T A)› fvs_simp(4) by force
    hence *: "([y ↔ z] ⋅ A)[y ::= M] = (A[z ::= M])" using "4.IH" by metis

    have "([y ↔ z] ⋅ Fn x T A)[y ::= M] = ((Fn ([y ↔ z] $ x) T ([y ↔ z] ⋅ A))[y ::= M])"
      using trm_prm_simp(4) by metis
    also have "... = ((Fn x T ([y ↔ z] ⋅ A))[y ::= M])"
      using prm_unit_inaction ‹x ≠ y› ‹x ≠ z› by metis
    also have "... = Fn x T (([y ↔ z] ⋅ A)[y ::= M])"
      using subst_simp_fn ‹x ≠ y› ‹x ∉ fvs M› by metis
    also have "... = Fn x T (A[z ::= M])" using * by metis
    also have "... = ((Fn x T A)[z ::= M])"
      using subst_simp_fn ‹x ≠ z› ‹x ∉ fvs M› by metis
    finally show ?case.
  next
  case (5 A B)
    from ‹y ∉ fvs (Pair A B)› have "y ∉ fvs A" "y ∉ fvs B" by (auto simp add: fvs_simp(5))
    hence "([y ↔ z] ⋅ A)[y ::= M] = (A[z ::= M])" "([y ↔ z] ⋅ B)[y ::= M] = (B[z ::= M])"
      using "5.IH" by metis+
    thus ?case using trm_prm_simp(5) subst_simp_pair by metis
  next
  case (6 P)
    from ‹y ∉ fvs (Fst P)› have "y ∉ fvs P" by (simp add: fvs_simp(6))
    hence "([y ↔ z] ⋅ P)[y ::= M] = (P[z ::= M])" using "6.IH" by metis
    thus ?case using trm_prm_simp(6) subst_simp_fst by metis
  next
  case (7 P)
    from ‹y ∉ fvs (Snd P)› have "y ∉ fvs P" by (simp add: fvs_simp(7))
    hence "([y ↔ z] ⋅ P)[y ::= M] = (P[z ::= M])" using "7.IH" by metis
    thus ?case using trm_prm_simp(7) subst_simp_snd by metis
  next
qed

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

  case 1
    thus ?case using subst_simp_unit by metis
  next
  case (2 x)
    consider "x = y" | "x = z" | "x ≠ y ∧ x ≠ z" by auto
    thus ?case proof(cases)
      case 1
        hence "x = y" "x ≠ z" using assms(1) by auto
        thus ?thesis using subst_simp_var1 subst_simp_var2 by metis
      next
      case 2
        hence "x ≠ y" "x = z" using assms(1) by auto
        thus ?thesis using subst_free ‹y ∉ fvs L› subst_simp_var1 subst_simp_var2 by metis
      next
      case 3
        then show ?thesis using subst_simp_var2 by metis
      next
    qed
  next
  case (3 A B)
    thus ?case using subst_simp_app by metis
  next
  case (4 x T A)
    hence *: "A[y ::= N][z ::= L] = (A[z ::= L][y ::= N[z ::= L]])" by blast
    from ‹x ∉ {y, z} ∪ fvs N ∪ fvs L› have "x ≠ y" "x ≠ z" "x ∉ fvs N" "x ∉ fvs L" by auto
    hence "x ∉ fvs (N[z ::= L])" using subst_fvs by auto
    
    have "(Fn x T A)[y ::= N][z ::= L] = Fn x T (A[y ::= N][z ::= L])"
      using subst_simp_fn ‹x ≠ y› ‹x ≠ z› ‹x ∉ fvs N› ‹x ∉ fvs L› by metis
    also have "... = Fn x T (A[z ::= L][y ::= N[z ::= L]])" using * by metis
    also have "... = ((Fn x T A)[z ::= L][y ::= N[z ::= L]])"
      using subst_simp_fn ‹x ≠ y› ‹x ≠ z› ‹x ∉ fvs (N[z ::= L])› ‹x ∉ fvs L› by metis
    finally show ?case.
  next
  case (5 A B)
    thus ?case using subst_simp_pair by metis
  next
  case (6 P)
    thus ?case using subst_simp_fst by metis
  next
  case (7 P)
    thus ?case using subst_simp_snd by metis
  next
qed

lemma typing_subst:
  assumes "Γ(z ↦ τ) ⊢ M : σ" "Γ ⊢ N : τ"
  shows "Γ ⊢ M[z ::= N] : σ"
using assms proof(induction M arbitrary: Γ σ rule: trm_strong_depth_induct[where S="{z} ∪ fvs N"])
  show "finite ({z} ∪ fvs N)" using fvs_finite by auto
  next

  case 1
    thus ?case using subst_simp_unit typing.tunit typing_unitE by metis
  next
  case (2 x)
    hence *: "(Γ(z ↦ τ)) x = Some σ" using typing_varE by metis

    consider "x = z" | "x ≠ z" by auto
    thus ?case proof(cases)
      case 1
        hence "(Γ(x ↦ τ)) x = Some σ" using * by metis
        hence "τ = σ" by auto
        thus ?thesis using ‹Γ ⊢ N : τ› subst_simp_var1 ‹x = z› by metis
      next
      case 2
        hence "Γ x = Some σ" using * by auto
        hence "Γ ⊢ Var x : σ" using typing.tvar by metis
        thus ?thesis using ‹x ≠ z› subst_simp_var2 by metis
      next
    qed
  next
  case (3 A B)
    have *: "depth A < depth (App A B) ∧ depth B < depth (App A B)"
      using depth_app by auto

    from ‹Γ(z ↦ τ) ⊢ App A B : σ› obtain σ' where
      "Γ(z ↦ τ) ⊢ A : (TArr σ' σ)"
      "Γ(z ↦ τ) ⊢ B : σ'"
      using typing_appE by metis
    hence
      "Γ ⊢ (A[z ::= N]) : (TArr σ' σ)"
      "Γ ⊢ (B[z ::= N]) : σ'"
      using 3 * by metis+
    hence "Γ ⊢ App (A[z ::= N]) (B[z ::= N]) : σ" using typing.tapp by metis
    thus ?case using subst_simp_app by metis
  next
  case (4 x T A)
    hence "x ≠ z" "x ∉ fvs N" by auto
    hence *: "Γ(x ↦ T) ⊢ N : τ" using typing_weaken 4 by metis
    have **: "depth A < depth (Fn x T A)" using depth_fn.

    from ‹Γ(z ↦ τ) ⊢ Fn x T A : σ› obtain σ' where
      "σ = TArr T σ'"
      "Γ(z ↦ τ, x ↦ T) ⊢ A : σ'"
      using typing_fnE by metis
    hence "Γ(x ↦ T, z ↦ τ) ⊢ A : σ'" using ‹x ≠ z› fun_upd_twist by metis
    hence "Γ(x ↦ T) ⊢ A[z ::= N] : σ'" using 4 * ** by metis
    hence "Γ ⊢ Fn x T (A[z ::= N]) : σ" using typing.tfn ‹σ = TArr T σ'› by metis
    thus ?case using ‹x ≠ z› ‹x ∉ fvs N› subst_simp_fn by metis
  next
  case (5 A B)
    from this obtain T S where "σ = TPair T S" "Γ(z ↦ τ) ⊢ A : T" "Γ(z ↦ τ) ⊢ B : S"
      using typing_pairE by metis
    moreover have "depth A < depth (Pair A B)" and "depth B < depth (Pair A B)"
      using depth_pair by auto
    ultimately have "Γ ⊢ A[z ::= N] : T" "Γ ⊢ B[z ::= N] : S" using 5 by metis+
    hence "Γ ⊢ Pair (A[z ::= N]) (B[z ::= N]) : σ" using ‹σ = TPair T S› typing.tpair by metis
    thus ?case using subst_simp_pair by metis
  next
  case (6 P)
    from this obtain σ' where "Γ(z ↦ τ) ⊢ P : (TPair σ σ')" using typing_fstE by metis
    moreover have "depth P < depth (Fst P)" using depth_fst by metis
    ultimately have "Γ ⊢ P[z ::= N] : (TPair σ σ')" using 6 by metis
    hence "Γ ⊢ Fst (P[z ::= N]) : σ" using typing.tfst by metis
    thus ?case using subst_simp_fst by metis
  next
  case (7 P)
    from this obtain σ' where "Γ(z ↦ τ) ⊢ P : (TPair σ' σ)" using typing_sndE by metis
    moreover have "depth P < depth (Snd P)" using depth_snd by metis
    ultimately have "Γ ⊢ P[z ::= N] : (TPair σ' σ)" using 7 by metis
    hence "Γ ⊢ Snd (P[z ::= N]) : σ" using typing.tsnd by metis
    thus ?case using subst_simp_snd by metis
  next
qed


inductive beta_reduction :: "'a trm ⇒ 'a trm ⇒ bool" ("_ →β _") where
  beta:  "(App (Fn x T A) M) →β (A[x ::= M])"
| app1:  "A →β A' ⟹ (App A B) →β (App A' B)"
| app2:  "B →β B' ⟹ (App A B) →β (App A B')"
| fn:    "A →β A' ⟹ (Fn x T A) →β (Fn x T A')"
| pair1: "A →β A' ⟹ (Pair A B) →β (Pair A' B)"
| pair2: "B →β B' ⟹ (Pair A B) →β (Pair A B')"
| fst1:  "P →β P' ⟹ (Fst P) →β (Fst P')"
| fst2:  "(Fst (Pair A B)) →β A" 
| snd1:  "P →β P' ⟹ (Snd P) →β (Snd P')"
| snd2:  "(Snd (Pair A B)) →β B"

lemma beta_reduction_fvs:
  assumes "M →β M'"
  shows "fvs M' ⊆ fvs M"
using assms proof(induction)
  case (beta x T A M)
    thus ?case using fvs_simp(3) fvs_simp(4) subst_fvs by metis
  next
  case (app1 A A' B)
    hence "fvs A' ∪ fvs B ⊆ fvs A ∪ fvs B" by auto
    thus ?case using fvs_simp(3) by metis
  next
  case (app2 B B' A)
    hence "fvs A ∪ fvs B' ⊆ fvs A ∪ fvs B" by auto
    thus ?case using fvs_simp(3) by metis
  next
  case (fn A A' x T)
    hence "fvs A' - {x} ⊆ fvs A - {x}" by auto
    thus ?case using fvs_simp(4) by metis
  next
  case (pair1 A A' B)
    hence "fvs A' ∪ fvs B ⊆ fvs A ∪ fvs B" by auto
    thus ?case using fvs_simp(5) by metis
  next
  case (pair2 B B' A)
    hence "fvs A ∪ fvs B' ⊆ fvs A ∪ fvs B" by auto
    thus ?case using fvs_simp(5) by metis
  next
  case (fst1 P P')
    thus ?case using fvs_simp(6) by metis
  next
  case (fst2 A B)
    thus ?case using fvs_simp(5, 6) by force
  next    
  case (snd1 P P')
    thus ?case using fvs_simp(7) by metis
  next
  case (snd2 A B)
    thus ?case using fvs_simp(5, 7) by force
  next
qed

lemma beta_reduction_prm:
  assumes "M →β M'"
  shows "(π ⋅ M) →β (π ⋅ M')"
using assms by(induction, auto simp add: beta_reduction.intros trm_prm_simp subst_prm)

lemma beta_reduction_left_unitE:
  assumes "Unit →β M'"
  shows "False"
using assms by(cases, auto simp add: unit_not_app unit_not_fn unit_not_pair unit_not_fst unit_not_snd)

lemma beta_reduction_left_varE:
  assumes "(Var x) →β M'"
  shows "False"
using assms by(cases, auto simp add: var_not_app var_not_fn var_not_pair var_not_fst var_not_snd)

lemma beta_reduction_left_appE:
  assumes "(App A B) →β M'"
  shows "
    (∃x T X. A = (Fn x T X) ∧ M' = (X[x ::= B])) ∨
    (∃A'. (A →β A') ∧ M' = App A' B) ∨
    (∃B'. (B →β B') ∧ M' = App A B')
  "
using assms by(
  cases,
  metis trm_simp(2, 3),
  metis trm_simp(2, 3),
  metis trm_simp(2, 3),
  auto simp add: app_not_fn app_not_pair app_not_fst app_not_snd
)

lemma beta_reduction_left_fnE:
  assumes "(Fn x T A) →β M'"
  shows "∃A'. (A →β A') ∧ M' = (Fn x T A')"
using assms proof(cases)
  case (fn B B' y S)
    consider "x = y ∧ T = S ∧ A = B" | "x ≠ y ∧ T = S ∧ x ∉ fvs B ∧ A = [x ↔ y] ⋅ B"
      using trm_simp(4) ‹Fn x T A = Fn y S B› by metis
    thus ?thesis proof(cases)
      case 1
        thus ?thesis using fn by auto
      next
      case 2
        thus ?thesis using fn beta_reduction_fvs beta_reduction_prm fn_eq by fastforce
      next
    qed
  next
qed (
  metis app_not_fn,
  metis app_not_fn,
  metis app_not_fn,
  auto simp add: fn_not_pair fn_not_fst fn_not_snd
)

lemma beta_reduction_left_pairE:
  assumes "(Pair A B) →β M'"
  shows "(∃A'. (A →β A') ∧ M' = (Pair A' B)) ∨ (∃B'. (B →β B') ∧ M' = (Pair A B'))"
using assms
  apply cases
  prefer 5
  apply (metis trm_simp(5, 6))
  prefer 5
  apply (metis trm_simp(5, 6))
  apply (metis app_not_pair, metis app_not_pair, metis app_not_pair, metis fn_not_pair, metis pair_not_fst, metis pair_not_fst, metis pair_not_snd, metis pair_not_snd)
done

lemma beta_reduction_left_fstE:
  assumes "(Fst P) →β M'"
  shows "(∃P'. (P →β P') ∧ M' = (Fst P')) ∨ (∃A B. P = (Pair A B) ∧ M' = A)"
using assms proof(cases)
  case (fst1 P P')
    thus ?thesis using trm_simp(7) by blast
  next
  case (fst2 B)
    thus ?thesis using trm_simp(7) by blast
  next
qed (
  metis app_not_fst,
  metis app_not_fst,
  metis app_not_fst,
  metis fn_not_fst,
  metis pair_not_fst,
  metis pair_not_fst,
  metis fst_not_snd,
  metis fst_not_snd
)

lemma beta_reduction_left_sndE:
  assumes "(Snd P) →β M'"
  shows "(∃P'. (P →β P') ∧ M' = (Snd P')) ∨ (∃A B. P = Pair A B ∧ M' = B)"
using assms proof(cases)
  case (snd1 P P')
    thus ?thesis using trm_simp(8) by blast
  next
  case (snd2 A)
    thus ?thesis using trm_simp(8) by blast
  next
qed (
  metis app_not_snd,
  metis app_not_snd,
  metis app_not_snd,
  metis fn_not_snd,
  metis pair_not_snd,
  metis pair_not_snd,
  metis fst_not_snd,
  metis fst_not_snd
)
  
lemma preservation':
  assumes "Γ ⊢ M : τ" and "M →β M'"
  shows "Γ ⊢ M' : τ"
using assms proof(induction arbitrary: M' rule: typing.induct)
  case (tunit Γ)
    thus ?case using beta_reduction_left_unitE by metis
  next
  case (tvar Γ x τ)
    thus ?case using beta_reduction_left_varE by metis
  next
  case (tapp Γ A τ σ B M')
    from ‹(App A B) →β M'› consider
      "(∃x T X. A = (Fn x T X) ∧ M' = (X[x ::= B]))" |
      "(∃A'. (A →β A') ∧ M' = App A' B)" |
      "(∃B'. (B →β B') ∧ M' = App A B')" using beta_reduction_left_appE by metis

    thus ?case proof(cases)
      case 1
        from this obtain x T X where "A = Fn x T X" and *: "M' = (X[x ::= B])" by auto

        have "Γ(x ↦ τ) ⊢ X : σ" using typing_fnE ‹Γ ⊢ A : (TArr τ σ)› ‹A = Fn x T X› type.inject
          by blast
        hence "Γ ⊢ (X[x ::= B]) : σ" using typing_subst ‹Γ ⊢ B : τ› by metis
        thus ?thesis using * by auto
      next
      case 2
        from this obtain A' where "A →β A'" and *: "M' = (App A' B)" by auto
        hence "Γ ⊢ A' : (TArr τ σ)" using tapp.IH(1) by metis
        hence "Γ ⊢ (App A' B) : σ" using ‹Γ ⊢ B : τ› typing.tapp by metis
        thus ?thesis using * by auto
      next
      case 3
        from this obtain B' where "B →β B'" and *: "M' = (App A B')" by auto
        hence "Γ ⊢ B' : τ" using tapp.IH(2) by metis
        hence "Γ ⊢ (App A B') : σ" using ‹Γ ⊢ A : (TArr τ σ)› typing.tapp by metis
        thus ?thesis using * by auto
      next
    qed
  next
  case (tfn Γ x T A σ)
    from this obtain A' where "A →β A'" and *: "M' = (Fn x T A')"
      using beta_reduction_left_fnE by metis
    hence "Γ(x ↦ T) ⊢ A' : σ" using tfn.IH by metis
    hence "Γ ⊢ (Fn x T A') : (TArr T σ)" using typing.tfn by metis
    thus ?case using * by auto
  next
  case (tpair Γ A τ B σ)
    from this consider
      "∃A'. (A →β A') ∧ M' = (Pair A' B)"
    | "∃B'. (B →β B') ∧ M' = (Pair A B')"
      using beta_reduction_left_pairE by metis
    thus ?case proof(cases)
      case 1
        from this obtain A' where "A →β A'" and "M' = Pair A' B" by auto
        thus ?thesis using tpair typing.tpair by metis
      next
      case 2
        from this obtain B' where "B →β B'" and "M' = Pair A B'" by auto
        thus ?thesis using tpair typing.tpair by metis
      next
    qed
  next
  case (tfst Γ P τ σ)
    from this consider
      "∃P'. (P →β P') ∧ M' = Fst P'"
    | "∃A B. P = Pair A B ∧ M' = A" using beta_reduction_left_fstE by metis
    thus ?case proof(cases)
      case 1
        from this obtain P' where "P →β P'" and "M' = Fst P'" by auto
        thus ?thesis using tfst typing.tfst by metis
      next
      case 2
        from this obtain A B where "P = Pair A B" and "M' = A" by auto
        thus ?thesis using ‹Γ ⊢ P : (TPair τ σ)› typing_pairE by blast
      next
    qed
  next
  case (tsnd Γ P τ σ)
    from this consider
      "∃P'. (P →β P') ∧ M' = Snd P'"
    | "∃A B. P = Pair A B ∧ M' = B" using beta_reduction_left_sndE by metis
    thus ?case proof(cases)
      case 1
        from this obtain P' where "P →β P'" and "M' = Snd P'" by auto
        thus ?thesis using tsnd typing.tsnd by metis
      next
      case 2
        from this obtain A B where "P = Pair A B" and "M' = B" by auto
        thus ?thesis using ‹Γ ⊢ P : (TPair τ σ)› typing_pairE by blast
      next
    qed
  next  
qed

inductive NF :: "'a trm ⇒ bool" where
  unit: "NF Unit"
| var: "NF (Var x)"
| app: "⟦A ≠ Fn x T A'; NF A; NF B⟧ ⟹ NF (App A B)"
| fn: "NF A ⟹ NF (Fn x T A)"
| pair: "⟦NF A; NF B⟧ ⟹ NF (Pair A B)"
| fst: "⟦P ≠ Pair A B; NF P⟧ ⟹ NF (Fst P)"
| snd: "⟦P ≠ Pair A B; NF P⟧ ⟹ NF (Snd P)"

theorem progress:
  assumes "Γ ⊢ M : τ"
  shows "NF M ∨ (∃M'. (M →β M'))"
using assms proof(induction M arbitrary: Γ τ rule: trm_induct)
  case 1
    thus ?case using NF.unit by metis
  next
  case (2 x)
    thus ?case using NF.var by metis
  next
  case (3 A B)
    from ‹Γ ⊢ App A B : τ› obtain σ
      where "Γ ⊢ A : (TArr σ τ)" and "Γ ⊢ B : σ"
      using typing_appE by metis
    hence A: "NF A ∨ (∃A'. (A →β A'))" and B: "NF B ∨ (∃B'. (B →β B'))"
      using "3.IH" by auto

    consider "NF B" | "∃B'. (B →β B')" using B by auto
    thus ?case proof(cases)
      case 1
        consider "NF A" | "∃A'. (A →β A')" using A by auto
        thus ?thesis proof(cases)
          case 1
            consider "∃x T A'. A = Fn x T A'" | "∄x T A'. A = Fn x T A'" by auto
            thus ?thesis proof(cases)
              case 1
                from this obtain x T A' where "A = Fn x T A'" by auto
                hence "(App A B) →β (A'[x ::= B])" using beta_reduction.beta by metis
                thus ?thesis by blast
              next
              case 2
                thus ?thesis using ‹NF A› ‹NF B› NF.app by metis
              next
            qed
          next
          case 2
            thus ?thesis using beta_reduction.app1 by metis
          next
        qed
      next
      case 2
        thus ?thesis using beta_reduction.app2 by metis
      next
    qed
  next
  case (4 x T A)
    from ‹Γ ⊢ Fn x T A : τ› obtain σ
      where "τ = TArr T σ" and "Γ(x ↦ T) ⊢ A : σ"
      using typing_fnE by metis
    from ‹Γ(x ↦ T) ⊢ A : σ› consider "NF A" | "∃A'. (A →β A')"
      using "4.IH" by metis

    thus ?case proof(cases)
      case 1
        thus ?thesis using NF.fn by metis
      next
      case 2
        from this obtain A' where "A →β A'" by auto
        obtain M' where "M' = Fn x T A'" by auto
        hence "(Fn x T A) →β M'" using ‹A →β A'› beta_reduction.fn by metis
        thus ?thesis by auto
      next
    qed
  next
  case (5 A B)
    thus ?case using typing_pairE beta_reduction.pair1 beta_reduction.pair2 NF.pair by meson
  next
  case (6 P)
    from this consider "NF P" | "∃P'. (P →β P')" using typing_fstE by metis
    thus ?case proof(cases)  
      case 1
        consider "∃A B. P = Pair A B" | "∄A B. P = Pair A B" by auto
        thus ?thesis proof(cases)
          case 1
            from this obtain A B where "P = Pair A B" by auto
            hence "(Fst P) →β A" using beta_reduction.fst2 by metis
            thus ?thesis by auto
          next
          case 2
            thus ?thesis using ‹NF P› NF.fst by metis
          next
        qed
      next
      case 2
        thus ?thesis using beta_reduction.fst1 by metis
      next
    qed
  next  
  case (7 P)
    from this consider "NF P" | "∃P'. (P →β P')" using typing_sndE by metis
    thus ?case proof(cases)  
      case 1
        consider "∃A B. P = Pair A B" | "∄A B. P = Pair A B" by auto
        thus ?thesis proof(cases)
          case 1
            from this obtain A B where "P = Pair A B" by auto
            hence "(Snd P) →β B" using beta_reduction.snd2 by metis
            thus ?thesis by auto
          next
          case 2
            thus ?thesis using ‹NF P› NF.snd by metis
          next
        qed
      next
      case 2
        thus ?thesis using beta_reduction.snd1 by metis
      next
    qed
  next  
qed

inductive beta_reduces :: "'a trm ⇒ 'a trm ⇒ bool" ("_ →β⇧* _") where
  reflexive:  "M →β⇧* M"
| transitive: "⟦M →β⇧* M'; M' →β M''⟧ ⟹ M →β⇧* M''"

lemma beta_reduces_composition:
  assumes "A' →β⇧* A''" and "A →β⇧* A'"
  shows "A →β⇧* A''"
using assms proof(induction)
  case (reflexive B)
    thus ?case.
  next
  case (transitive B B' B'')
    thus ?case using beta_reduces.transitive by metis
  next
qed

lemma beta_reduces_fvs:
  assumes "A →β⇧* A'"
  shows "fvs A' ⊆ fvs A"
using assms proof(induction)
  case (reflexive M)
    thus ?case by auto
  next
  case (transitive M M' M'')
    hence "fvs M'' ⊆ fvs M'" using beta_reduction_fvs by metis
    thus ?case using ‹fvs M' ⊆ fvs M› by auto
  next
qed

lemma beta_reduces_app_left:
  assumes "A →β⇧* A'"
  shows "(App A B) →β⇧* (App A' B)"
using assms proof(induction)
  case (reflexive A)
    thus ?case using beta_reduces.reflexive.
  next
  case (transitive A A' A'')
    thus ?case using beta_reduces.transitive beta_reduction.app1 by metis
  next
qed

lemma beta_reduces_app_right:
  assumes "B →β⇧* B'"
  shows "(App A B) →β⇧* (App A B')"
using assms proof(induction)
  case (reflexive B)
    thus ?case using beta_reduces.reflexive.
  next
  case (transitive B B' B'')
    thus ?case using beta_reduces.transitive beta_reduction.app2 by metis
  next
qed

lemma beta_reduces_fn:
  assumes "A →β⇧* A'"
  shows "(Fn x T A) →β⇧* (Fn x T A')"
using assms proof(induction)
  case (reflexive A)
    thus ?case using beta_reduces.reflexive.
  next
  case (transitive A A' A'')
    thus ?case using beta_reduces.transitive beta_reduction.fn by metis
  next
qed

lemma beta_reduces_pair_left:
  assumes "A →β⇧* A'"
  shows "(Pair A B) →β⇧* (Pair A' B)"
using assms proof(induction)
  case (reflexive M)
    thus ?case using beta_reduces.reflexive.
  next
  case (transitive M M' M'')
    thus ?case using beta_reduces.transitive beta_reduction.pair1 by metis
  next  
qed

lemma beta_reduces_pair_right:
  assumes "B →β⇧* B'"
  shows "(Pair A B) →β⇧* (Pair A B')"
using assms proof(induction)
  case (reflexive M)
    thus ?case using beta_reduces.reflexive.
  next
  case (transitive M M' M'')
    thus ?case using beta_reduces.transitive beta_reduction.pair2 by metis
  next  
qed

lemma beta_reduces_fst:
  assumes "P →β⇧* P'"
  shows "(Fst P) →β⇧* (Fst P')"
using assms proof(induction)
  case (reflexive M)
    thus ?case using beta_reduces.reflexive.
  next
  case (transitive M M' M'')
    thus ?case using beta_reduces.transitive beta_reduction.fst1 by metis
  next
qed

lemma beta_reduces_snd:
  assumes "P →β⇧* P'"
  shows "(Snd P) →β⇧* (Snd P')"
using assms proof(induction)
  case (reflexive M)
    thus ?case using beta_reduces.reflexive.
  next
  case (transitive M M' M'')
    thus ?case using beta_reduces.transitive beta_reduction.snd1 by metis
  next
qed
  
theorem preservation:
  assumes "M →β⇧* M'" "Γ ⊢ M : τ"
  shows "Γ ⊢ M' : τ"
using assms proof(induction)
  case (reflexive M)
    thus ?case.
  next
  case (transitive M M' M'')
    thus ?case using preservation' by metis
  next
qed

theorem safety:
  assumes "M →β⇧* M'" "Γ ⊢ M : τ"
  shows "NF M' ∨ (∃M''. (M' →β M''))"
using assms proof(induction)
  case (reflexive M)
    thus ?case using progress by metis
  next
  case (transitive M M' M'')
    hence "Γ ⊢ M' : τ" using preservation by metis
    hence "Γ ⊢ M'' : τ" using preservation' ‹M' →β M''› by metis
    thus ?case using progress by metis
  next
qed

inductive parallel_reduction :: "'a trm ⇒ 'a trm ⇒ bool" ("_ >> _") where
  refl: "A >> A"
| beta: "⟦A >> A'; B >> B'⟧ ⟹ (App (Fn x T A) B) >> (A'[x ::= B'])"
| eta:  "A >> A' ⟹ (Fn x T A) >> (Fn x T A')"
| app:  "⟦A >> A'; B >> B'⟧ ⟹ (App A B) >> (App A' B')"
| pair: "⟦A >> A'; B >> B'⟧ ⟹ (Pair A B) >> (Pair A' B')"
| fst1: "P >> P' ⟹ (Fst P) >> (Fst P')"
| fst2: "A >> A' ⟹ (Fst (Pair A B)) >> A'"
| snd1: "P >> P' ⟹ (Snd P) >> (Snd P')"
| snd2: "B >> B' ⟹ (Snd (Pair A B)) >> B'"

lemma parallel_reduction_prm:
  assumes "A >> A'"
  shows "(π ⋅ A) >> (π ⋅ A')"
using assms
  apply induction
  apply (rule parallel_reduction.refl)
  apply (metis parallel_reduction.beta subst_prm trm_prm_simp(3, 4))
  apply (metis parallel_reduction.eta trm_prm_simp(4))
  apply (metis parallel_reduction.app trm_prm_simp(3))
  apply (metis parallel_reduction.pair trm_prm_simp(5))
  apply (metis parallel_reduction.fst1 trm_prm_simp(6))
  apply (metis parallel_reduction.fst2 trm_prm_simp(5, 6))
  apply (metis parallel_reduction.snd1 trm_prm_simp(7))
  apply (metis parallel_reduction.snd2 trm_prm_simp(5, 7))
done

lemma parallel_reduction_fvs:
  assumes "A >> A'"
  shows "fvs A' ⊆ fvs A"
using assms proof(induction)
  case (refl A)
    thus ?case by auto
  next
  case (beta A A' B B' x T)
    have *:"fvs (App (Fn x T A) B) = fvs A - {x} ∪ fvs B" using fvs_simp(3, 4) by metis
    have "fvs (A'[x ::= B']) ⊆ fvs A' - {x} ∪ fvs B'" using subst_fvs.
    also have "... ⊆ fvs A - {x} ∪ fvs B" using beta.IH by auto
    finally show ?case using fvs_simp(3, 4) by metis
  next
  case (eta A A' x T)
    thus ?case using fvs_simp(4) Un_Diff subset_Un_eq by metis
  next
  case (app A A' B B')
    thus ?case using fvs_simp(3) Un_mono by metis
  next
  case (pair A A' B B')
    thus ?case using fvs_simp(5) Un_mono by metis
  next
  case (fst1 P P')
    thus ?case using fvs_simp(6) by force
  next
  case (fst2 A A' B)
    thus ?case using fvs_simp(5, 6) by force
  next
  case (snd1 P P')
    thus ?case using fvs_simp(7) by force
  next
  case (snd2 B B' A)
    thus ?case using fvs_simp(5, 7) by force
  next
qed

inductive_cases parallel_reduction_unitE': "Unit >> A"
lemma parallel_reduction_unitE:
  assumes "Unit >> A"
  shows "A = Unit"
using assms
  apply (rule parallel_reduction_unitE'[where A=A])
  apply blast
  apply (auto simp add: unit_not_app unit_not_fn unit_not_pair unit_not_fst unit_not_snd)
done

inductive_cases parallel_reduction_varE': "(Var x) >> A"
lemma parallel_reduction_varE:
  assumes "(Var x) >> A"
  shows "A = Var x"
using assms
  apply (rule parallel_reduction_varE'[where x=x and A=A])
  apply blast
  apply (auto simp add: var_not_app var_not_fn var_not_pair var_not_fst var_not_snd)
done

inductive_cases parallel_reduction_fnE': "(Fn x T A) >> X"
lemma parallel_reduction_fnE:
  assumes "(Fn x T A) >> X"
  shows "X = Fn x T A ∨ (∃A'. (A >> A') ∧ X = Fn x T A')"
using assms proof(induction rule: parallel_reduction_fnE'[where x=x and T=T and A=A and X=X])
  case (4 B B' y S)
    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 ?case proof(cases)
      case 1
        hence "x = y" "T = S" "A = B" by auto
        thus ?thesis using 4 by metis
      next
      case 2
        hence "x ≠ y" "T = S" "x ∉ fvs B" "A = [x ↔ y] ⋅ B" by auto
        hence "x ∉ fvs B'" "A >> ([x ↔ y] ⋅ B')"
          using parallel_reduction_fvs parallel_reduction_prm ‹B >> B'› by auto
        thus ?thesis using fn_eq ‹X = Fn y S B'› ‹x ≠ y› ‹T = S› by metis
      next
    qed
  next
qed (
  metis assms,
  blast,
  metis app_not_fn,
  metis app_not_fn,
  metis fn_not_pair,
  metis fn_not_fst,
  metis fn_not_fst,
  metis fn_not_snd,
  metis fn_not_snd
)

inductive_cases parallel_reduction_redexE': "(App (Fn x T A) B) >> X"
lemma parallel_reduction_redexE:
  assumes "(App (Fn x T A) B) >> X"
  shows "
    (X = App (Fn x T A) B) ∨
    (∃A' B'. (A >> A') ∧ (B >> B') ∧ X = (A'[x ::= B'])) ∨
    (∃A' B'. ((Fn x T A) >> (Fn x T A')) ∧ (B >> B') ∧ X = (App (Fn x T A') B'))
  "
using assms proof(induction rule: parallel_reduction_redexE'[where x=x and T=T and A=A and B=B and X=X])
  case (5 C C' D D')
    from ‹App (Fn x T A) B = App C D› have C: "C = Fn x T A" and D: "D = B"
      by (metis trm_simp(2), metis trm_simp(3))
    from C and ‹C >> C'› obtain A' where C': "C' = Fn x T A'"
      using parallel_reduction_fnE by metis
    thus ?thesis using C C' D ‹C >> C'› ‹D >> D'› ‹X = App C' D'› by metis
  next
  case (3 C C' D D' y S)
    from ‹App (Fn x T A) B = App (Fn y S C) D› have "Fn x T A = Fn y S C" and B: "B = D"
      by (metis trm_simp(2), metis trm_simp(3))
    from this consider
      "x = y ∧ T = S ∧ A = C"
    | "x ≠ y ∧ T = S ∧ A = [x ↔ y] ⋅ C ∧ x ∉ fvs C"
      using trm_simp(4) by metis
    thus ?case proof(cases)
      case 1
        thus ?thesis using ‹C >> C'› ‹X = (C'[y ::= D'])› ‹D >> D'› B by metis
      next
      case 2
        hence "x ≠ y" "T = S" and A: "A = [x ↔ y] ⋅ C" "x ∉ fvs C" by auto
        have "x ∉ fvs C'" using parallel_reduction_fvs ‹x ∉ fvs C› ‹C >> C'› by force
        
        have "A >> ([x ↔ y] ⋅ C')"
          using parallel_reduction_prm ‹C >> C'› A by metis
        moreover have "X = (([x ↔ y] ⋅ C')[x ::= D'])"
          using ‹X = (C'[y ::= D'])› subst_swp ‹x ∉ fvs C'› by metis
        ultimately show ?thesis using ‹D >> D'› B by metis
      next
    qed
  next
qed (
  metis assms,
  blast,
  metis app_not_fn,
  metis app_not_pair,
  metis app_not_fst,
  metis app_not_fst,
  metis app_not_snd,
  metis app_not_snd
)

inductive_cases parallel_reduction_nonredexE': "(App A B) >> X"
lemma parallel_reduction_nonredexE:
  assumes "(App A B) >> X" and "⋀x T A'. A ≠ Fn x T A'"
  shows "∃A' B'. (A >> A') ∧ (B >> B') ∧ X = (App A' B')"
using assms proof(induction rule: parallel_reduction_nonredexE'[where A=A and B=B and X=X])
  case (5 C C' D D')
    hence "A = C" "B = D" using trm_simp(2, 3) by auto
    thus ?case using ‹C >> C'› ‹D >> D'› ‹X = App C' D'› by metis
  next
qed (
  metis assms(1),
  metis parallel_reduction.refl,
  metis trm_simp(2, 3) assms(2),
  metis app_not_fn,
  metis app_not_pair,
  metis app_not_fst,
  metis app_not_fst,
  metis app_not_snd,
  metis app_not_snd
)

inductive_cases parallel_reduction_pairE': "(Pair A B) >> X"
lemma parallel_reduction_pairE:
  assumes "(Pair A B) >> X"
  shows "∃A' B'. (A >> A') ∧ (B >> B') ∧ (X = Pair A' B')"
using assms proof(induction rule: parallel_reduction_pairE'[where A=A and B=B and X=X])
  case 2
    thus ?case using parallel_reduction.refl by blast
  next
  case (6 A A' B B')
    thus ?case using parallel_reduction.pair trm_simp(5, 6) by fastforce
  next
qed (
  metis assms,
  metis app_not_pair,
  metis fn_not_pair,
  metis app_not_pair,
  metis pair_not_fst,
  metis pair_not_fst,
  metis pair_not_snd,
  metis pair_not_snd
)

inductive_cases parallel_reduction_fstE': "(Fst P) >> X"
lemma parallel_reduction_fstE:
  assumes "(Fst P) >> X"
  shows "(∃P'. (P >> P') ∧ X = (Fst P')) ∨ (∃A A' B. (P = Pair A B) ∧ (A >> A') ∧ X = A')"
using assms proof(induction rule: parallel_reduction_fstE'[where P=P and X=X])
  case (7 P P')
    thus ?case using parallel_reduction.fst1 trm_simp(7) by metis
  next
  case (8 A B)
    thus ?case using parallel_reduction.fst2 trm_simp(7) by metis
  next
qed (
  metis assms,
  insert parallel_reduction.refl, metis,
  metis app_not_fst,
  metis fn_not_fst,
  metis app_not_fst,
  metis pair_not_fst,
  metis fst_not_snd,
  metis fst_not_snd
)

inductive_cases parallel_reduction_sndE': "(Snd P) >> X"
lemma parallel_reduction_sndE:
  assumes "(Snd P) >> X"
  shows "(∃P'. (P >> P') ∧ X = (Snd P')) ∨ (∃A B B'. (P = Pair A B) ∧ (B >> B') ∧ X = B')"
using assms proof(induction rule: parallel_reduction_sndE'[where P=P and X=X])
  case (9 P P')
    thus ?case using parallel_reduction.snd1 trm_simp(8) by metis
  next
  case (10 A B)
    thus ?case using parallel_reduction.snd2 trm_simp(8) by metis
  next
qed (
  metis assms,
  insert parallel_reduction.refl, metis,
  metis app_not_snd,
  metis fn_not_snd,
  metis app_not_snd,
  metis pair_not_snd,
  metis fst_not_snd,
  metis fst_not_snd
)

lemma parallel_reduction_subst_inner:
  assumes "M >> M'"
  shows "X[z ::= M] >> (X[z ::= M'])"
using assms proof(induction X rule: trm_strong_induct[where S="{z} ∪ fvs M ∪ fvs M'"])
  show "finite ({z} ∪ fvs M ∪ fvs M')" using fvs_finite by auto

  case 1
    thus ?case using subst_simp_unit parallel_reduction.refl by metis
  next
  case (2 x)
    thus ?case by(cases "x = z", metis subst_simp_var1, metis subst_simp_var2 parallel_reduction.refl)
  next
  case (3 A B)
    thus ?case using subst_simp_app parallel_reduction.app by metis
  next
  case (4 x T A)
    hence "x ≠ z" "x ∉ fvs M" "x ∉ fvs M'" by auto
    thus ?case using 4 subst_simp_fn parallel_reduction.eta by metis
  next
  case (5 A B)
    thus ?case using subst_simp_pair parallel_reduction.pair by metis
  next
  case (6 P)
    thus ?case using subst_simp_fst parallel_reduction.fst1 by metis
  next
  case (7 P)
    thus ?case using subst_simp_snd parallel_reduction.snd1 by metis
  next
qed

lemma parallel_reduction_subst:
  assumes "X >> X'" "M >> M'"
  shows "X[z ::= M] >> (X'[z ::= M'])"
using assms proof(induction X arbitrary: X' rule: trm_strong_depth_induct[where S="{z} ∪ fvs M ∪ fvs M'"])
  show "finite ({z} ∪ fvs M ∪ fvs M')" using fvs_finite by auto
  next

  case 1
    hence "X' = Unit" using parallel_reduction_unitE by metis
    thus ?case using parallel_reduction.refl subst_simp_unit by metis
  next
  case (2 x)
    hence "X' = Var x" using parallel_reduction_varE by metis
    thus ?case using parallel_reduction_subst_inner ‹M >> M'› by metis
  next
  case (3 C D)
    consider "∃x T A. C = Fn x T A" | "∄x T A. C = Fn x T A" by metis
    thus ?case proof(cases)
      case 1
        from this obtain x T A where C: "C = Fn x T A" by auto
        have "depth C < depth (App C D)" "depth D < depth (App C D)"
          using depth_app by auto

        consider
          "X' = App (Fn x T A) D"
        | "∃A' D'. ((Fn x T A) >> (Fn x T A')) ∧ (D >> D') ∧ X' = (App (Fn x T A') D')" 
        | "∃A' D'. (A >> A') ∧ (D >> D') ∧ X' = (A'[x ::= D'])"
        using parallel_reduction_redexE ‹(App C D) >> X'› C by metis
        thus ?thesis proof(cases)
          case 1
            thus ?thesis using parallel_reduction_subst_inner ‹M >> M'› C by metis
          next
          case 2
            from this obtain A' D'
              where "(Fn x T A) >> (Fn x T A')" "D >> D'" and X': "X' = App (Fn x T A') D'"
              by auto
            have *: "((Fn x T A)[z ::= M]) >> ((Fn x T A')[z ::= M'])"
              using "3.IH" ‹depth C < depth (App C D)› C ‹(Fn x T A) >> (Fn x T A')› ‹M >> M'›
              by metis
            have **: "(D[z ::= M]) >> (D'[z ::= M'])"
              using "3.IH" ‹depth D < depth (App C D)› ‹D >> D'› ‹M >> M'›
              by metis

            have "(App C D)[z ::= M] = App ((Fn x T A)[z ::= M]) (D[z ::= M])"
              using subst_simp_app C by metis
            moreover have "... >> (App ((Fn x T A')[z ::= M']) (D'[z ::= M']))"
              using * ** parallel_reduction.app by metis
            moreover have "... = ((App (Fn x T A') D')[z ::= M'])"
              using subst_simp_app by metis
            moreover have "... = (X'[z ::= M'])"
              using X' by metis
            ultimately show ?thesis by metis
          next
          case 3
            from this obtain A' D' where "A >> A'" "D >> D'" and X': "X' = (A'[x ::= D'])"
              by auto

            have "depth A < depth (App C D)"
              using C depth_app depth_fn dual_order.strict_trans by fastforce

            have "finite ({z} ∪ fvs M ∪ fvs M' ∪ fvs A')" using fvs_finite by auto
            from this obtain y
              where "y ∉ {z} ∪ fvs M ∪ fvs M' ∪ fvs A'" and C: "C = Fn y T ([y ↔ x] ⋅ A)"
              using fresh_fn C by metis
            hence "y ≠ z" "y ∉ fvs M" "y ∉ fvs M'" "y ∉ fvs A'" by auto
            have "([y ↔ x] ⋅ A) >> ([y ↔ x] ⋅ A')" using parallel_reduction_prm ‹A >> A'› by metis
            hence *: "([y ↔ x] ⋅ A)[z ::= M] >> (([y ↔ x] ⋅ A')[z ::= M'])"
              using "3.IH" ‹depth A < depth (App C D)› depth_prm
              using ‹([y ↔ x] ⋅ A) >> ([y ↔ x] ⋅A')› ‹M >> M'› by metis
            have **: "(D[z ::= M]) >> (D'[z ::= M'])"
              using "3.IH" ‹depth D < depth (App C D)› ‹D >> D'› ‹M >> M'›
              by metis

            have "(App C D)[z ::= M] = (App ((Fn y T ([y ↔ x] ⋅ A))[z ::= M]) (D[z ::= M]))"
              using C subst_simp_app by metis
            moreover have "... = (App (Fn y T (([y ↔ x] ⋅ A)[z ::= M])) (D[z ::= M]))"
              using ‹y ≠ z› ‹y ∉ fvs M› subst_simp_fn by metis
            moreover have "... >> (([y ↔ x] ⋅ A')[z ::= M'][y ::= D'[z ::= M']])"
              using parallel_reduction.beta * ** by metis
            moreover have "... = (([y ↔ x] ⋅ A')[y ::= D'][z ::= M'])"
              using barendregt ‹y ≠ z› ‹y ∉ fvs M'› by metis
            moreover have "... = (A'[x ::= D'][z ::= M'])"
              using subst_swp ‹y ∉ fvs A'› by metis
            moreover have "... = (X'[z ::= M'])" using X' by metis
            ultimately show ?thesis by metis
          next
        qed
      next
      case 2
        from this obtain C' D' where "C >> C'" "D >> D'" and X': "X' = App C' D'"
          using parallel_reduction_nonredexE ‹(App C D) >> X'› by metis

        have "depth C < depth (App C D)" "depth D < depth (App C D)"
          using depth_app by auto
        hence *: "(C[z ::= M]) >> (C'[z ::= M'])" and **: "(D[z ::= M]) >> (D'[z ::= M'])"
          using "3.IH" ‹C >> C'› ‹D >> D'› ‹M >> M'› by metis+

        have "(App C D)[z ::= M] = App (C[z ::= M]) (D[z ::= M])"
          using subst_simp_app by metis
        moreover have "... >> (App (C'[z ::= M']) (D'[z ::= M']))"
          using parallel_reduction.app * ** by metis
        moreover have "... = ((App C' D')[z ::= M'])"
          using subst_simp_app by metis
        moreover have "... = (X'[z ::= M'])" using X' by metis
        ultimately show ?thesis by metis
      next
    qed
  next
  case (4 x T A)
    hence "x ≠ z" "x ∉ fvs M" "x ∉ fvs M'"
      by auto

    from ‹(Fn x T A) >> X'› consider
      "X' = Fn x T A"
    | "∃A'. (A >> A') ∧ X' = Fn x T A'" using parallel_reduction_fnE by metis
    thus ?case proof(cases)
      case 1
        thus ?thesis using parallel_reduction_subst_inner ‹M >> M'› by metis
      next
      case 2
        from this obtain A' where "A >> A'" and X': "X' = Fn x T A'" by auto

        hence *: "(A[z ::= M]) >> (A'[z ::= M'])"
          using "4.IH" depth_fn ‹A >> A'› ‹M >> M'› by metis

        have "((Fn x T A)[z ::= M]) = (Fn x T (A[z ::= M]))"
          using subst_simp_fn ‹x ≠ z› ‹x ∉ fvs M› by metis
        moreover have "... >> (Fn x T (A'[z ::= M']))"
          using parallel_reduction.eta * by metis
        moreover have "... = ((Fn x T A')[z ::= M'])"
          using subst_simp_fn ‹x ≠ z› ‹x ∉ fvs M'› by metis
        moreover have "... = (X'[z ::= M'])"
          using X' by metis
        ultimately show ?thesis by metis
      next
    qed
  next
  case (5 A B)
    from ‹(Pair A B) >> X'› consider
      "X' = Pair A B"
    | "∃A' B'. (A >> A') ∧ (B >> B') ∧ X' = Pair A' B'"
      using parallel_reduction_pairE by metis
    thus ?case proof(cases)
      case 1
        thus ?thesis using parallel_reduction_subst_inner ‹M >> M'› by metis
      next
      case 2
        from this obtain A' B' where "A >> A'" "B >> B'" and X': "X' = Pair A' B'" by auto

        have *: "(A[z ::= M]) >> (A'[z ::= M'])" and **: "(B[z ::= M]) >> (B'[z ::= M'])"
          using "5.IH" ‹A >> A'› ‹B >> B'› ‹M >> M'› by (metis depth_pair(1), metis depth_pair(2))

        have "(Pair A B)[z ::= M] = (Pair (A[z ::= M]) (B[z ::= M]))"
          using subst_simp_pair by metis
        moreover have "... >> (Pair (A'[z ::= M']) (B'[z ::= M']))"
          using parallel_reduction.pair * ** by metis
        moreover have "... = ((Pair A' B')[z ::= M'])"
          using subst_simp_pair by metis
        moreover have "... = (X'[z ::= M'])" using X' by metis
        ultimately show ?thesis by metis
      next
    qed
  next
  case (6 P)
    from ‹(Fst P) >> X'› consider
      "∃P'. (P >> P') ∧ X' = Fst P'"
    | "∃A A' B. P = Pair A B ∧ (A >> A') ∧ X' = A'"
      using parallel_reduction_fstE by metis
    thus ?case proof(cases)
      case 1
        from this obtain P' where "P >> P'" and X': "X' = Fst P'" by auto

        have *: "(P[z ::= M]) >> (P'[z ::= M'])"
          using "6.IH" depth_fst ‹P >> P'› ‹M >> M'› by metis

        have "(Fst P)[z ::= M] = Fst (P[z ::= M])"
          using subst_simp_fst by metis
        moreover have "... >> (Fst (P'[z ::= M']))"
          using parallel_reduction.fst1 * by metis
        moreover have "... = ((Fst P')[z ::= M'])"
          using subst_simp_fst by metis
        moreover have "... = (X'[z ::= M'])" using X' by metis
        ultimately show ?thesis by metis
      next
      case 2
        from this obtain A A' B where P: "P = Pair A B" "A >> A'" and X': "X' = A'" by auto

        have "depth A < depth (Fst P)"
          using P depth_fst depth_pair dual_order.strict_trans by fastforce
        hence *: "(A[z ::= M]) >> (A'[z ::= M'])"
          using "6.IH" ‹A >> A'› ‹M >> M'› by metis

        have "(Fst P)[z ::= M] = (Fst (Pair (A[z ::= M]) (B[z ::= M])))"
          using P subst_simp_fst subst_simp_pair by metis
        moreover have "... >> (A'[z ::= M'])"
          using parallel_reduction.fst2 * by metis
        moreover have "... = (X'[z ::= M'])"
          using X' by metis
        ultimately show ?thesis by metis
      next
    qed
  next
  case (7 P)
    from ‹(Snd P) >> X'› consider
      "∃P'. (P >> P') ∧ X' = Snd P'"
    | "∃A B B'. P = Pair A B ∧ (B >> B') ∧ X' = B'"
      using parallel_reduction_sndE by metis
    thus ?case proof(cases)
      case 1
        from this obtain P' where "P >> P'" and X': "X' = Snd P'" by auto

        have *: "(P[z ::= M]) >> (P'[z ::= M'])"
          using "7.IH" depth_snd ‹P >> P'› ‹M >> M'› by metis

        have "(Snd P)[z ::= M] = Snd (P[z ::= M])"
          using subst_simp_snd by metis
        moreover have "... >> (Snd (P'[z ::= M']))"
          using parallel_reduction.snd1 * by metis
        moreover have "... = ((Snd P')[z ::= M'])"
          using subst_simp_snd by metis
        moreover have "... = (X'[z ::= M'])" using X' by metis
        ultimately show ?thesis by metis
      next
      case 2
        from this obtain A B B' where P: "P = Pair A B" "B >> B'" and X': "X' = B'" by auto

        have "depth B < depth (Snd P)"
          using P depth_snd depth_pair dual_order.strict_trans by fastforce
        hence *: "(B[z ::= M]) >> (B'[z ::= M'])"
          using "7.IH" ‹B >> B'› ‹M >> M'› by metis

        have "(Snd P)[z ::= M] = (Snd (Pair (A[z ::= M]) (B[z ::= M])))"
          using P subst_simp_snd subst_simp_pair by metis
        moreover have "... >> (B'[z ::= M'])"
          using parallel_reduction.snd2 * by metis
        moreover have "... = (X'[z ::= M'])"
          using X' by metis
        ultimately show ?thesis by metis
      next
    qed
  next
qed

inductive complete_development :: "'a trm ⇒ 'a trm ⇒ bool" ("_ >>> _") where
  unit: "Unit >>> Unit"
| var:  "(Var x) >>> (Var x)"
| beta: "⟦A >>> A'; B >>> B'⟧ ⟹ (App (Fn x T A) B) >>> (A'[x ::= B'])"
| eta:  "A >>> A' ⟹ (Fn x T A) >>> (Fn x T A')"
| app:  "⟦A >>> A'; B >>> B'; (⋀x T M. A ≠ Fn x T M)⟧ ⟹ (App A B) >>> (App A' B')"
| pair: "⟦A >>> A'; B >>> B'⟧ ⟹ (Pair A B) >>> (Pair A' B')"
| fst1: "⟦P >>> P'; (⋀A B. P ≠ Pair A B)⟧ ⟹ (Fst P) >>> (Fst P')"
| fst2: "A >>> A' ⟹ (Fst (Pair A B)) >>> A'"
| snd1: "⟦P >>> P'; (⋀A B. P ≠ Pair A B)⟧ ⟹ (Snd P) >>> (Snd P')"
| snd2: "B >>> B' ⟹ (Snd (Pair A B)) >>> B'"

lemma not_fn_prm:
  assumes "⋀x T M. A ≠ Fn x T M"
  shows "π ⋅ A ≠ Fn x T M"
proof(rule classical)
  fix x T M
  obtain π' where *: "π' = prm_inv π" by auto
  assume "¬(π ⋅ A ≠ Fn x T M)"
  hence "π ⋅ A = Fn x T M" by blast
  hence "π' ⋅ (π ⋅ A) = π' ⋅ Fn x T M" by fastforce
  hence "(π' ⋄ π) ⋅ A = π' ⋅ Fn x T M"
    using trm_prm_apply_compose by metis
  hence "A = π' ⋅ Fn x T M"
    using * prm_inv_compose trm_prm_apply_id by metis
  hence "A = Fn (π' $ x) T (π' ⋅ M)" using trm_prm_simp(4) by metis
  hence False using assms by blast
  thus ?thesis by blast
qed

lemma not_pair_prm:
  assumes "⋀A B. P ≠ Pair A B"
  shows "π ⋅ P ≠ Pair A B"
proof(rule classical)
  fix A B
  obtain π' where *: "π' = prm_inv π" by auto
  assume "¬(π ⋅ P ≠ Pair A B)"
  hence "π ⋅ P = Pair A B" by blast
  hence "π' ⋅ π ⋅ P = π' ⋅ (Pair A B)" by fastforce
  hence "(π' ⋄ π) ⋅ P = π' ⋅ (Pair A B)"
    using trm_prm_apply_compose by metis
  hence "P = π' ⋅ (Pair A B)"
    using * prm_inv_compose trm_prm_apply_id by metis
  hence "P = Pair (π' ⋅ A) (π' ⋅ B)" using trm_prm_simp(5) by metis
  hence False using assms by blast
  thus ?thesis by blast
qed

lemma complete_development_prm:
  assumes "A >>> A'"
  shows "(π ⋅ A) >>> (π ⋅ A')"
using assms proof(induction)
  case unit
    thus ?case using complete_development.unit trm_prm_simp(1) by metis
  next
  case (var x)
    thus ?case using complete_development.var trm_prm_simp(2) by metis
  next
  case (beta A A' B B' x T)
    thus ?case using complete_development.beta subst_prm trm_prm_simp(3, 4) by metis
  next
  case (eta A A' x T)
    thus ?case using complete_development.eta trm_prm_simp(4) by metis
  next
  case (app A A' B B')
    thus ?case using complete_development.app by (simp add: trm_prm_simp(3) not_fn_prm)
  next
  case (pair A A' B B')
    thus ?case using complete_development.pair trm_prm_simp(5) by metis
  next
  case (fst1 P P')
    hence "π ⋅ P ≠ Pair A B" for A B using not_pair_prm by metis
    thus ?case using trm_prm_simp(6) fst1.IH complete_development.fst1 by metis
  next
  case (fst2 A A' B)
    thus ?case using trm_prm_simp(5, 6) complete_development.fst2 by metis
  next
  case (snd1 P P')
    hence "π ⋅ P ≠ Pair A B" for A B using not_pair_prm by metis
    thus ?case using trm_prm_simp(7) snd1.IH complete_development.snd1 by metis
  next
  case (snd2 B B' A)
    thus ?case using trm_prm_simp(5, 7) complete_development.snd2 by metis
  next
qed

lemma complete_development_fvs:
  assumes "A >>> A'"
  shows "fvs A' ⊆ fvs A"
using assms proof(induction)
  case unit
    thus ?case using fvs_simp by auto
  next
  case (var x)
    thus ?case using fvs_simp by auto
  next
  case (beta A A' B B' x T)
    have "fvs (A'[x ::= B']) ⊆ fvs A' - {x} ∪ fvs B'" using subst_fvs.
    also have "... ⊆ fvs A - {x} ∪ fvs B" using beta.IH by auto
    also have "... ⊆ fvs (Fn x T A) ∪ fvs B" using fvs_simp(4) subset_refl by force
    also have "... ⊆ fvs (App (Fn x T A) B)" using fvs_simp(3) subset_refl by force
    finally show ?case.
  next
  case (eta A A' x T)
    thus ?case using fvs_simp(4) using Un_Diff subset_Un_eq by (metis (no_types, lifting))
  next
  case (app A A' B B')
    thus ?case using fvs_simp(3) Un_mono by metis
  next
  case (pair A A' B B')
    thus ?case using fvs_simp(5) Un_mono by metis
  next
  case (fst1 P P')
    thus ?case using fvs_simp(6) by force
  next
  case (fst2 A A' B)
    thus ?case by (simp add: fvs_simp(5, 6) sup.coboundedI1)
  next
  case (snd1 P P')
    thus ?case using fvs_simp(7) by fastforce
  next
  case (snd2 B B' A)
    thus ?case using fvs_simp(5, 7) by fastforce
  next
qed

lemma complete_development_fnE:
  assumes "(Fn x T A) >>> X"
  shows "∃A'. (A >>> A') ∧ X = Fn x T A'"
using assms proof(cases)
  case (eta B B' y S)
    hence "T = S" using trm_simp(4) by metis
    from eta consider "x = y ∧ A = B" | "x ≠ y ∧ x ∉ fvs B ∧ A = [x ↔ y] ⋅ B"
      using trm_simp(4) by metis
    thus ?thesis proof(cases)
      case 1
        hence "x = y" and "A = B" by auto
        obtain A' where "A' = B'" by auto
        hence "A >>> A'" and "X = Fn x T A'" using eta ‹A = B› ‹x = y› ‹T = S› by auto
        thus ?thesis by auto
      next
      case 2
        hence "x ≠ y" "x ∉ fvs B" and A: "A = [x ↔ y] ⋅ B" by auto
        hence "x ∉ fvs B'" using ‹B >>> B'› complete_development_fvs by auto
        obtain A' where A': "A' = [x ↔ y] ⋅ B'" by auto
        hence "A >>> A'" using A ‹B >>> B'› complete_development_prm by auto
        have "X = Fn x T A'"
          using fn_eq ‹x ≠ y› ‹x ∉ fvs B'› A' ‹X = Fn y S B'› ‹T = S› by metis
        thus ?thesis using ‹A >>> A'› by auto
      next
    qed
  next
qed (
  metis unit_not_fn,
  metis var_not_fn,
  metis app_not_fn,
  metis app_not_fn,
  metis fn_not_pair,
  metis fn_not_fst,
  metis fn_not_fst,
  metis fn_not_snd,
  metis fn_not_snd
)

lemma complete_development_pairE:
  assumes "(Pair A B) >>> X"
  shows "∃A' B'. (A >>> A') ∧ (B >>> B') ∧ X = Pair A' B'"
using assms
  apply cases
  apply (metis unit_not_pair, metis var_not_pair, metis app_not_pair, metis fn_not_pair, metis app_not_pair)
  apply (metis trm_simp(5, 6))
  apply (metis pair_not_fst, metis pair_not_fst, metis pair_not_snd, metis pair_not_snd)
done

lemma complete_development_exists:
  shows "∃X. (A >>> X)"
proof(induction A rule: trm_induct)
  case 1
    obtain X :: "'a trm" where "X = Unit" by auto
    hence "Unit >>> X" using complete_development.unit by metis
    thus ?case by auto
  next
  case (2 x)
    obtain X where "X = Var x" by auto
    hence "(Var x) >>> X" using complete_development.var by metis
    thus ?case by auto
  next
  case (3 A B)
    from this obtain A' B' where A': "A >>> A'" and B': "B >>> B'" by auto
    consider "(∃x T M. A = Fn x T M)" | "¬(∃x T M. A = Fn x T M)" by auto
    thus ?case proof(cases)
      case 1
        from this obtain x T M where A: "A = Fn x T M" by auto
        from this obtain M' where "A' = Fn x T M'" and "M >>> M'"
          using complete_development_fnE A' by metis
        obtain X where "X = (M'[x ::= B'])" by auto
        hence "(App A B) >>> X"
          using complete_development.beta ‹M >>> M'› B' A by metis
        thus ?thesis by auto
      next
      case 2
        thus ?thesis using complete_development.app A' B' by metis
      next
    qed
  next
  case (4 x T A)
    from this obtain A' where A': "A >>> A'" by auto
    obtain X where "X = Fn x T A'" by auto
    hence "(Fn x T A) >>> X" using complete_development.eta A' by metis
    thus ?case by auto
  next
  case (5 A B)
    thus ?case using complete_development.pair by blast
  next
  case (6 P)
    consider "∃A B. P = Pair A B" | "∄A B. P = Pair A B" by auto
    thus ?case proof(cases)
      case 1
        from this obtain A B X where "P = Pair A B" "P >>> X" using 6 by auto
        from this obtain A' B' where "A >>> A'" "B >>> B'" "X = Pair A' B'"
          using complete_development_pairE by metis
        thus ?thesis using complete_development.fst2 ‹P = Pair A B› by metis
      next
      case 2
        thus ?thesis using complete_development.fst1 6 by blast
      next
    qed
  next
  case (7 P)
    consider "∃A B. P = Pair A B" | "∄A B. P = Pair A B" by auto
    thus ?case proof(cases)
      case 1
        from this obtain A B X where "P = Pair A B" "P >>> X" using 7 by auto
        from this obtain A' B' where "A >>> A'" "B >>> B'" "X = Pair A' B'"
          using complete_development_pairE by metis
        thus ?thesis using complete_development.snd2 ‹P = Pair A B› by metis
      next
      case 2
        thus ?thesis using complete_development.snd1 7 by blast
      next
    qed
  next
qed

lemma complete_development_triangle:
  assumes "A >>> D" "A >> B"
  shows "B >> D"
using assms proof(induction arbitrary: B rule: complete_development.induct)
  case unit
    thus ?case using parallel_reduction_unitE parallel_reduction.refl by metis
  next
  case (var x)
    thus ?case using parallel_reduction_varE parallel_reduction.refl by metis
  next
  case (beta A A' C C' x T)
    hence "A >> A'" "C >> C'" using parallel_reduction.refl by metis+
    from ‹(App (Fn x T A) C) >> B› consider
        "B = App (Fn x T A) C"
      | "∃A'' C''. (A >> A'') ∧ (C >> C'') ∧ B = (A''[x ::= C''])"
      | "∃A'' C''. ((Fn x T A) >> (Fn x T A'')) ∧ (C >> C'') ∧ B = (App (Fn x T A'') C'')"
      using parallel_reduction_redexE by metis
    thus ?case proof(cases)
      case 1
        thus ?thesis using parallel_reduction.beta ‹A >> A'› ‹C >> C'› by metis
      next
      case 2
        from this obtain A'' C'' where "A >> A''" "C >> C''" and B: "B = (A''[x ::= C''])" by auto
        hence "A'' >> A'" "C'' >> C'" using beta.IH by metis+
        thus ?thesis using B parallel_reduction_subst by metis
      next
      case 3
        from this obtain A'' C''
          where "(Fn x T A) >> (Fn x T A'')" "C >> C''" and B: "B = App (Fn x T A'') C''"
          by auto
        hence "C'' >> C'" using beta.IH by metis
        have "A'' >> A'"
        proof -
          thm parallel_reduction_fnE
          from ‹(Fn x T A) >> (Fn x T A'')› consider
            "Fn x T A = Fn x T A''"
          | "∃A'''. (A >> A''') ∧ Fn x T A'' = Fn x T A'''"
            using parallel_reduction_fnE by metis
          hence "A >> A''" proof(cases)
            case 1
              hence "A = A''" using trm_simp(4) by metis
              thus ?thesis using parallel_reduction.refl by metis
            next
            case 2
              from this obtain A''' where "A >> A'''" "Fn x T A'' = Fn x T A'''" by auto
              thus ?thesis using trm_simp(4) by metis
            next
          qed
          thus ?thesis using beta.IH by metis
        qed
        thus ?thesis using B ‹C'' >> C'› parallel_reduction.beta by metis
      next
    qed
  next
  case (eta A A' x T B)
    from this consider
      "B = Fn x T A"
    | "∃A''. (A >> A'') ∧ B = Fn x T A''" using parallel_reduction_fnE by metis
    thus ?case proof(cases)
      case 1
        thus ?thesis using eta.IH parallel_reduction.refl parallel_reduction.eta by metis
      next
      case 2
        from this obtain A'' where "A >> A''" and "B = Fn x T A''" by auto
        thus ?thesis using eta.IH parallel_reduction.eta by metis
      next
    qed
  next
  case (app A A' C C')
    from this obtain A'' C'' where "A >> A''" "C >> C''" and B: "B = App A'' C''"
      using parallel_reduction_nonredexE by metis
    hence "A'' >> A'" "C'' >> C'" using app.IH by metis+
    thus ?case using B parallel_reduction.app by metis
  next
  case (pair A A' C C')
    from ‹(Pair A C) >> B› and parallel_reduction_pairE obtain A'' C'' where
      "A >> A''" "C >> C''" "B = Pair A'' C''" by metis
    thus ?case using pair.IH parallel_reduction.pair by metis
  next
  case (fst1 P P')
    from this obtain P'' where "P >> P''" "B = Fst P''"
      using parallel_reduction_fstE by blast
    thus ?case using fst1.IH parallel_reduction.fst1 by metis
  next
  case (fst2 A A' C B)
    from this consider
      "∃P''. ((Pair A C) >> P'') ∧ B = Fst P''"
    | "∃A''. (A >> A'') ∧ (B = A'')"
      using parallel_reduction_fstE[where P="(Pair A C)" and X=B] using trm_simp(5) by metis
    thus ?case proof(cases)
      case 1
        from this obtain P'' where "(Pair A C) >> P''" and "B = Fst P''" by auto
        from this obtain A'' C'' where "P'' = Pair A'' C''" "A >> A''" "C >> C''"
          using parallel_reduction_pairE by metis
        thus ?thesis using fst2 parallel_reduction.fst2 ‹B = Fst P''› by metis
      next
      case 2
        from this obtain A'' where "A >> A''" "B = A''" by metis
        thus ?thesis using fst2 by metis
      next
    qed
  next
  case (snd1 P P')
    from this obtain P'' where "P >> P''" "B = Snd P''"
      using parallel_reduction_sndE by blast
    thus ?case using snd1.IH parallel_reduction.snd1 by metis
  next
  case (snd2 C A' A B)
    from this consider
      "∃P''. ((Pair A C) >> P'') ∧ B = Snd P''"
    | "∃C''. (C >> C'') ∧ (B = C'')"
      using parallel_reduction_sndE[where P="(Pair A C)" and X=B] using trm_simp(5, 6) by metis
    thus ?case proof(cases)
      case 1
        from this obtain P'' where "(Pair A C) >> P''" and "B = Snd P''" by auto
        from this obtain A'' C'' where "P'' = Pair A'' C''" "A >> A''" "C >> C''"
          using parallel_reduction_pairE by metis
        thus ?thesis using snd2 parallel_reduction.snd2 ‹B = Snd P''› by metis
      next
      case 2
        from this obtain C'' where "C >> C''" "B = C''" by metis
        thus ?thesis using snd2 by metis
      next
    qed
  next
qed

lemma parallel_reduction_diamond:
  assumes "A >> B" "A >> C"
  shows "∃D. (B >> D) ∧ (C >> D)"
proof -
  obtain D where "A >>> D" using complete_development_exists by metis
  hence "(B >> D) ∧ (C >> D)" using complete_development_triangle assms by auto
  thus ?thesis by blast
qed

inductive parallel_reduces :: "'a trm ⇒ 'a trm ⇒ bool" ("_ >>⇧* _") where
  reflexive: "A >>⇧* A"
| transitive: "⟦A >>⇧* A'; A' >> A''⟧ ⟹ A >>⇧* A''"

lemma parallel_reduces_diamond':
  assumes "A >>⇧* C" "A >> B"
  shows "∃D. (B >>⇧* D) ∧ (C >> D)"
using assms proof(induction)
  case (reflexive A)
    thus ?case using parallel_reduces.reflexive by metis
  next
  case (transitive A A' A'')
    from this obtain C where "B >>⇧* C" "A' >> C" by metis
    from ‹A' >> C› ‹A' >> A''› obtain D where "C >> D" "A'' >> D"
      using parallel_reduction_diamond by metis
    thus ?case using parallel_reduces.transitive ‹B >>⇧* C› by metis
  next
qed

lemma parallel_reduces_diamond:
  assumes "A >>⇧* B" "A >>⇧* C"
  shows "∃D. (B >>⇧* D) ∧ (C >>⇧* D)"
using assms proof(induction)
  case (reflexive A)
    thus ?case using parallel_reduces.reflexive by metis
  next
  case (transitive A A' A'')
    from this obtain C' where "A' >>⇧* C'" "C >>⇧* C'" by metis
    from this obtain D where "A'' >>⇧* D" "C' >> D"
      using ‹A' >> A''› ‹A' >>⇧* C'› parallel_reduces_diamond' by metis
    thus ?case using parallel_reduces.transitive ‹C >>⇧* C'› by metis
  next
qed

lemma beta_reduction_is_parallel_reduction:
  assumes "A →β B"
  shows "A >> B"
using assms
  apply induction
  apply (metis parallel_reduction.beta parallel_reduction.refl)
  apply (metis parallel_reduction.app parallel_reduction.refl)
  apply (metis parallel_reduction.app parallel_reduction.refl)
  apply (metis parallel_reduction.eta)
  apply (metis parallel_reduction.pair parallel_reduction.refl)
  apply (metis parallel_reduction.pair parallel_reduction.refl)
  apply (metis parallel_reduction.fst1)
  apply (metis parallel_reduction.fst2 parallel_reduction.refl)
  apply (metis parallel_reduction.snd1)
  apply (metis parallel_reduction.snd2 parallel_reduction.refl)
done

lemma parallel_reduction_is_beta_reduction:
  assumes "A >> B"
  shows "A →β⇧* B"
using assms proof(induction)
  case (refl A)
    thus ?case using beta_reduces.reflexive.
  next
  case (beta A A' B B' x T)
    hence "(App (Fn x T A) B) →β⇧* (App (Fn x T A') B')"
      using ‹A →β⇧* A'›
      beta_reduces_fn beta_reduces_app_left beta_reduces_app_right beta_reduces_composition
      by metis
    moreover have "(App (Fn x T A') B') →β (A'[x ::= B'])"
      using beta_reduction.beta.
    ultimately show ?case using beta_reduces.transitive by metis
  next
  case (eta A A' x T)
    thus ?case using beta_reduces_fn by metis
  next
  case (app A A' B B')
    thus ?case using beta_reduces_app_left beta_reduces_app_right beta_reduces_composition by metis
  next
  case (pair A A' B B')
    thus ?case using beta_reduces_pair_left beta_reduces_pair_right beta_reduces_composition by metis
  next
  case (fst1 P P')
    thus ?case using beta_reduces_fst by metis
  next
  case (fst2 A A' B)
    thus ?case
      using beta_reduces_pair_left beta_reduction.fst2 beta_reduces.intros beta_reduces_composition
      by blast
  next
  case (snd1 P P')
    thus ?case using beta_reduces_snd by metis
  next
  case (snd2 B B' A)
    thus ?case
      using beta_reduces_pair_left beta_reduction.snd2 beta_reduces.intros beta_reduces_composition
      by blast
  next
qed

lemma parallel_beta_reduces_equivalent:
  shows "(A >>⇧* B) = (A →β⇧* B)"
proof -
  have →: "(A >>⇧* B) ⟹ (A →β⇧* B)"
  proof(induction rule: parallel_reduces.induct)
    case (reflexive A)
      thus ?case using beta_reduces.reflexive.
    next
    case (transitive A A' A'')
      thus ?case using beta_reduces_composition parallel_reduction_is_beta_reduction by metis
    next
  qed

  have ←: "(A →β⇧* B) ⟹ (A >>⇧* B)"
  proof(induction rule: beta_reduces.induct)
    case (reflexive A)
      thus ?case using parallel_reduces.reflexive.
    next
    case (transitive A A' A'')
      thus ?case using parallel_reduces.transitive beta_reduction_is_parallel_reduction by metis
    next
  qed

  from ←→ show "(A >>⇧* B) = (A →β⇧* B)" by blast
qed

theorem confluence:
  assumes "A →β⇧* B" "A →β⇧* C"
  shows "∃D. (B →β⇧* D) ∧ (C →β⇧* D)"
proof -
  from assms have "A >>⇧* B" "A >>⇧* C" using parallel_beta_reduces_equivalent by metis+
  hence "∃D. (B >>⇧* D) ∧ (C >>⇧* D)" using parallel_reduces_diamond by metis
  thus "∃D. (B →β⇧* D) ∧ (C →β⇧* D)" using parallel_beta_reduces_equivalent by metis
qed

end
end