Theory Idiomatic_Terms

(* Author: Joshua Schneider, ETH Zurich *)

subsection ‹Idiomatic terms -- Properties and operations›

theory Idiomatic_Terms
imports Combinators
begin

text ‹This theory proves the correctness of the normalisation algorithm for
  arbitrary applicative functors. We generalise the normal form using a framework
  for bracket abstraction algorithms. Both approaches justify lifting certain
  classes of equations. We model this as implications of term equivalences,
  where unlifting of idiomatic terms is expressed syntactically.›

subsubsection ‹Basic definitions›

datatype 'a itrm =
    Opaque 'a | Pure dB
  | IAp "'a itrm" "'a itrm" (infixl "⋄" 150)

primrec opaque :: "'a itrm ⇒ 'a list"
where
    "opaque (Opaque x) = [x]"
  | "opaque (Pure _) = []"
  | "opaque (f ⋄ x) = opaque f @ opaque x"

abbreviation "iorder x ≡ length (opaque x)"

inductive itrm_cong :: "('a itrm ⇒ 'a itrm ⇒ bool) ⇒ 'a itrm ⇒ 'a itrm ⇒ bool"
for R
where
    into_itrm_cong: "R x y ⟹ itrm_cong R x y"
  | pure_cong[intro]: "x ↔ y ⟹ itrm_cong R (Pure x) (Pure y)"
  | ap_cong: "itrm_cong R f f' ⟹ itrm_cong R x x' ⟹ itrm_cong R (f ⋄ x) (f' ⋄ x')"
  | itrm_refl[iff]: "itrm_cong R x x"
  | itrm_sym[sym]: "itrm_cong R x y ⟹ itrm_cong R y x"
  | itrm_trans[trans]: "itrm_cong R x y ⟹ itrm_cong R y z ⟹ itrm_cong R x z"

lemma ap_congL[intro]: "itrm_cong R f f' ⟹ itrm_cong R (f ⋄ x) (f' ⋄ x)"
by (blast intro: ap_cong)

lemma ap_congR[intro]: "itrm_cong R x x' ⟹ itrm_cong R (f ⋄ x) (f ⋄ x')"
by (blast intro: ap_cong)

text ‹Idiomatic terms are \emph{similar} iff they have the same structure, and all contained
  lambda terms are equivalent.›

abbreviation similar :: "'a itrm ⇒ 'a itrm ⇒ bool" (infixl "≅" 50)
where "x ≅ y ≡ itrm_cong (λ_ _. False) x y"

lemma pure_similarE:
  assumes "Pure x' ≅ y"
  obtains y' where "y = Pure y'" and "x' ↔ y'"
proof -
  define x :: "'a itrm" where "x = Pure x'"
  from assms have "x ≅ y" unfolding x_def .
  then have "(∀x''. x = Pure x'' ⟶ (∃y'. y = Pure y' ∧ x'' ↔ y')) ∧
    (∀x''. y = Pure x'' ⟶ (∃y'. x = Pure y' ∧ x'' ↔ y'))"
  proof (induction)
    case pure_cong thus ?case by (auto intro: term_sym)
  next
    case itrm_trans thus ?case by (fastforce intro: term_trans)
  qed simp_all
  with that show thesis unfolding x_def by blast
qed

lemma opaque_similarE:
  assumes "Opaque x' ≅ y"
  obtains y' where "y = Opaque y'" and "x' = y'"
proof -
  define x :: "'a itrm" where "x = Opaque x'"
  from assms have "x ≅ y" unfolding x_def .
  then have "(∀x''. x = Opaque x'' ⟶ (∃y'. y = Opaque y' ∧ x'' = y')) ∧
    (∀x''. y = Opaque x'' ⟶ (∃y'. x = Opaque y' ∧ x'' = y'))"
  by induction fast+
  with that show thesis unfolding x_def by blast
qed

lemma ap_similarE:
  assumes "x1 ⋄ x2 ≅ y"
  obtains y1 y2 where "y = y1 ⋄ y2" and "x1 ≅ y1" and "x2 ≅ y2"
proof -
  from assms
  have "(∀x1' x2'. x1 ⋄ x2 = x1' ⋄ x2' ⟶ (∃y1 y2. y = y1 ⋄ y2 ∧ x1' ≅ y1 ∧ x2' ≅ y2)) ∧
    (∀x1' x2'. y = x1' ⋄ x2' ⟶ (∃y1 y2. x1 ⋄ x2 = y1 ⋄ y2 ∧ x1' ≅ y1 ∧ x2' ≅ y2))"
  proof (induction)
    case ap_cong thus ?case by (blast intro: itrm_sym)
  next
    case trans: itrm_trans thus ?case by (fastforce intro: itrm_trans)
  qed simp_all
  with that show thesis by blast
qed

text ‹The following relations define semantic equivalence of idiomatic terms.
  We consider equivalences that hold universally in all idioms, as well as arbitrary
  specialisations using additional laws.›

inductive idiom_rule :: "'a itrm ⇒ 'a itrm ⇒ bool"
where
    idiom_id: "idiom_rule (Pure ℐ ⋄ x) x"
  | idiom_comp: "idiom_rule (Pure ℬ ⋄ g ⋄ f ⋄ x) (g ⋄ (f ⋄ x))"
  | idiom_hom: "idiom_rule (Pure f ⋄ Pure x) (Pure (f ° x))"
  | idiom_xchng: "idiom_rule (f ⋄ Pure x) (Pure (𝒯 ° x) ⋄ f)"

abbreviation itrm_equiv :: "'a itrm ⇒ 'a itrm ⇒ bool" (infixl "≃" 50)
where "x ≃ y ≡ itrm_cong idiom_rule x y"

lemma idiom_rule_into_equiv: "idiom_rule x y ⟹ x ≃ y" ..

lemmas itrm_id = idiom_id[THEN idiom_rule_into_equiv]
lemmas itrm_comp = idiom_comp[THEN idiom_rule_into_equiv]
lemmas itrm_hom = idiom_hom[THEN idiom_rule_into_equiv]
lemmas itrm_xchng = idiom_xchng[THEN idiom_rule_into_equiv]

lemma similar_into_equiv: "x ≅ y ⟹ x ≃ y"
by (induction pred: itrm_cong) (auto intro: ap_cong itrm_sym itrm_trans)

lemma opaque_equiv: "x ≃ y ⟹ opaque x = opaque y"
proof (induction pred: itrm_cong)
  case (into_itrm_cong x y)
  thus ?case by induction auto
qed simp_all

lemma iorder_equiv: "x ≃ y ⟹ iorder x = iorder y"
by (auto dest: opaque_equiv)

locale special_idiom =
  fixes extra_rule :: "'a itrm ⇒ 'a itrm ⇒ bool"
begin

definition "idiom_ext_rule = sup idiom_rule extra_rule"

abbreviation itrm_ext_equiv :: "'a itrm ⇒ 'a itrm ⇒ bool" (infixl "≃⇧+" 50)
where "x ≃⇧+ y ≡ itrm_cong idiom_ext_rule x y"

lemma equiv_into_ext_equiv: "x ≃ y ⟹ x ≃⇧+ y"
unfolding idiom_ext_rule_def
by (induction pred: itrm_cong)
   (auto intro: into_itrm_cong ap_cong itrm_sym itrm_trans)

lemmas itrm_ext_id = itrm_id[THEN equiv_into_ext_equiv]
lemmas itrm_ext_comp = itrm_comp[THEN equiv_into_ext_equiv]
lemmas itrm_ext_hom = itrm_hom[THEN equiv_into_ext_equiv]
lemmas itrm_ext_xchng = itrm_xchng[THEN equiv_into_ext_equiv]

end


subsubsection ‹Syntactic unlifting›

paragraph ‹With generalisation of variables›

primrec unlift' :: "nat ⇒ 'a itrm ⇒ nat ⇒ dB"
where
    "unlift' n (Opaque _) i = Var i"
  | "unlift' n (Pure x) i = liftn n x 0"
  | "unlift' n (f ⋄ x) i = unlift' n f (i + iorder x) ° unlift' n x i"

abbreviation "unlift x ≡ (Abs^^iorder x) (unlift' (iorder x) x 0)"

lemma funpow_Suc_inside: "(f ^^ Suc n) x = (f ^^ n) (f x)"
using funpow_Suc_right unfolding comp_def by metis

lemma absn_cong[intro]: "s ↔ t ⟹ (Abs^^n) s ↔ (Abs^^n) t"
by (induction n) auto

lemma free_unlift: "free (unlift' n x i) j ⟹ j ≥ n ∨ (j ≥ i ∧ j < i + iorder x)"
proof (induction x arbitrary: i)
  case (Opaque x)
  thus ?case by simp
next
  case (Pure x)
  thus ?case using free_liftn by simp
next
  case (IAp x y)
  thus ?case by fastforce
qed

lemma unlift_subst: "j ≤ i ∧ j ≤ n ⟹ (unlift' (Suc n) t (Suc i))[s/j] = unlift' n t i"
proof (induction t arbitrary: i)
  case (Opaque x)
  thus ?case by simp
next
  case (Pure x)
  thus ?case using subst_liftn by simp
next
  case (IAp x y)
  hence "j ≤ i + iorder y" by simp
  with IAp show ?case by auto
qed

lemma unlift'_equiv: "x ≃ y ⟹ unlift' n x i ↔ unlift' n y i"
proof (induction arbitrary: n i pred: itrm_cong)
  case (into_itrm_cong x y) thus ?case
  proof induction
    case (idiom_id x)
    show ?case using I_equiv[symmetric] by simp
  next
    case (idiom_comp g f x)
    let ?G = "unlift' n g (i + iorder f + iorder x)"
    let ?F = "unlift' n f (i + iorder x)"
    let ?X = "unlift' n x i"
    have "unlift' n (g ⋄ (f ⋄ x)) i = ?G ° (?F ° ?X)"
      by (simp add: add.assoc)
    moreover have "unlift' n (Pure ℬ ⋄ g ⋄ f ⋄ x) i = ℬ ° ?G ° ?F ° ?X"
      by (simp add: add.commute add.left_commute)
    moreover have "?G ° (?F ° ?X) ↔ ℬ ° ?G ° ?F ° ?X" using B_equiv[symmetric] .
    ultimately show ?case by simp
  next
    case (idiom_hom f x)
    show ?case by auto
  next
    case (idiom_xchng f x)
    let ?F = "unlift' n f i"
    let ?X = "liftn n x 0"
    have "unlift' n (f ⋄ Pure x) i = ?F ° ?X" by simp
    moreover have "unlift' n (Pure (𝒯 ° x) ⋄ f) i = 𝒯 ° ?X ° ?F" by simp
    moreover have "?F ° ?X ↔ 𝒯 ° ?X ° ?F" using T_equiv[symmetric] .
    ultimately show ?case by simp
  qed
next
  case pure_cong
  thus ?case by (auto intro: equiv_liftn)
next
  case (ap_cong f f' x x')
  from ‹x ≃ x'› have iorder_eq: "iorder x = iorder x'" by (rule iorder_equiv)
  have "unlift' n (f ⋄ x) i = unlift' n f (i + iorder x) ° unlift' n x i" by simp
  moreover have "unlift' n (f' ⋄ x') i = unlift' n f' (i + iorder x) ° unlift' n x' i"
    using iorder_eq by simp
  ultimately show ?case using ap_cong.IH by (auto intro: equiv_app)
next
  case itrm_refl
  thus ?case by simp
next
  case itrm_sym
  thus ?case using term_sym by simp
next
  case itrm_trans
  thus ?case using term_trans by blast
qed

lemma unlift_equiv: "x ≃ y ⟹ unlift x ↔ unlift y"
proof -
  assume "x ≃ y"
  then have "unlift' (iorder y) x 0 ↔ unlift' (iorder y) y 0" by (rule unlift'_equiv)
  moreover from ‹x ≃ y› have "iorder x = iorder y" by (rule iorder_equiv)
  ultimately show ?thesis by auto
qed


paragraph ‹Preserving variables›

primrec unlift_vars :: "nat ⇒ nat itrm ⇒ dB"
where
    "unlift_vars n (Opaque i) = Var i"
  | "unlift_vars n (Pure x) = liftn n x 0"
  | "unlift_vars n (x ⋄ y) = unlift_vars n x ° unlift_vars n y"

lemma all_pure_unlift_vars: "opaque x = [] ⟹ x ≃ Pure (unlift_vars 0 x)"
proof (induction x)
  case (Opaque x) then show ?case by simp
next
  case (Pure x) then show ?case by simp
next
  case (IAp x y)
  then have no_opaque: "opaque x = []" "opaque y = []" by simp+
  then have unlift_ap: "unlift_vars 0 (x ⋄ y) = unlift_vars 0 x ° unlift_vars 0 y"
    by simp
  from no_opaque IAp.IH have "x ⋄ y ≃ Pure (unlift_vars 0 x) ⋄ Pure (unlift_vars 0 y)"
    by (blast intro: ap_cong)
  also have "... ≃ Pure (unlift_vars 0 x ° unlift_vars 0 y)" by (rule itrm_hom)
  also have "... = Pure (unlift_vars 0 (x ⋄ y))" by (simp only: unlift_ap)
  finally show ?case .
qed


subsubsection ‹Canonical forms›

inductive_set CF :: "'a itrm set"
where
    pure_cf[iff]: "Pure x ∈ CF"
  | ap_cf[intro]: "f ∈ CF ⟹ f ⋄ Opaque x ∈ CF"

primrec CF_pure :: "'a itrm ⇒ dB"
where
    "CF_pure (Opaque _) = undefined"
  | "CF_pure (Pure x) = x"
  | "CF_pure (x ⋄ _) = CF_pure x"

lemma ap_cfD1[dest]: "f ⋄ x ∈ CF ⟹ f ∈ CF"
by (rule CF.cases) auto

lemma ap_cfD2[dest]: "f ⋄ x ∈ CF ⟹ ∃x'. x = Opaque x'"
by (rule CF.cases) auto

lemma opaque_not_cf[simp]: "Opaque x ∈ CF ⟹ False"
by (rule CF.cases) auto

lemma cf_unlift:
  assumes "x ∈ CF"
    shows "CF_pure x ↔ unlift x"
using assms proof (induction set: CF)
  case (pure_cf x)
  show ?case by simp
next
  case (ap_cf f x)
  let ?n = "iorder f + 1"
  have "unlift (f ⋄ Opaque x) = (Abs^^?n) (unlift' ?n f 1 ° Var 0)"
    by simp
  also have "... = (Abs^^iorder f) (Abs (unlift' ?n f 1 ° Var 0))"
    using funpow_Suc_inside by simp
  also have "... ↔ unlift f" proof -
    have "¬ free (unlift' ?n f 1) 0" using free_unlift by fastforce
    hence "Abs (unlift' ?n f 1 ° Var 0) →⇩η (unlift' ?n f 1)[Var 0/0]" ..
    also have "... = unlift' (iorder f) f 0"
      using unlift_subst by (metis One_nat_def Suc_eq_plus1 le0)
    finally show ?thesis
      by (simp add: r_into_rtranclp absn_cong eta_into_equiv)
  qed
  finally show ?case
    using ap_cf.IH by (auto intro: term_sym term_trans)
qed

lemma cf_similarI:
  assumes "x ∈ CF" "y ∈ CF"
      and "opaque x = opaque y"
      and "CF_pure x ↔ CF_pure y"
    shows "x ≅ y"
using assms proof (induction arbitrary: y)
  case (pure_cf x)
  hence "opaque y = []" by auto
  with ‹y ∈ CF› obtain y' where "y = Pure y'" by cases auto
  with pure_cf.prems show ?case by auto
next
  case (ap_cf f x)
  from ‹opaque (f ⋄ Opaque x) = opaque y›
  obtain y1 y2 where "opaque y = y1 @ y2"
    and "opaque f = y1" and "[x] = y2" by fastforce
  from ‹[x] = y2› obtain y' where "y2 = [y']" and "x = y'"
    by auto
  with ‹y ∈ CF› and ‹opaque y = y1 @ y2› obtain g
    where "opaque g = y1" and y_split: "y = g ⋄ Opaque y'" "g ∈ CF" by cases auto
  with ap_cf.prems ‹opaque f = y1›
  have "opaque f = opaque g" "CF_pure f ↔ CF_pure g" by auto
  with ap_cf.IH ‹g ∈ CF› have "f ≅ g" by simp
  with ap_cf.prems y_split ‹x = y'› show ?case by (auto intro: ap_cong)
qed

lemma cf_similarD:
  assumes in_cf: "x ∈ CF" "y ∈ CF"
      and similar: "x ≅ y"
    shows "CF_pure x ↔ CF_pure y ∧ opaque x = opaque y"
using assms
by (blast intro!: similar_into_equiv opaque_equiv cf_unlift unlift_equiv
      intro: term_trans term_sym)

text ‹Equivalent idiomatic terms in canonical form are similar. This justifies speaking of a
  normal form.›

lemma cf_unique:
  assumes in_cf: "x ∈ CF" "y ∈ CF"
      and equiv: "x ≃ y"
    shows "x ≅ y"
using in_cf proof (rule cf_similarI)
  from equiv show "opaque x = opaque y" by (rule opaque_equiv)
next
  from equiv have "unlift x ↔ unlift y" by (rule unlift_equiv)
  thus "CF_pure x ↔ CF_pure y"
    using cf_unlift[OF in_cf(1)] cf_unlift[OF in_cf(2)]
    by (auto intro: term_sym term_trans)
qed


subsubsection ‹Normalisation of idiomatic terms›

primrec norm_pn :: "dB ⇒ 'a itrm ⇒ 'a itrm"
where
    "norm_pn f (Opaque x) = undefined"
  | "norm_pn f (Pure x) = Pure (f ° x)"
  | "norm_pn f (n ⋄ x) = norm_pn (ℬ ° f) n ⋄ x"

primrec norm_nn :: "'a itrm ⇒ 'a itrm ⇒ 'a itrm"
where
    "norm_nn n (Opaque x) = undefined"
  | "norm_nn n (Pure x) = norm_pn (𝒯 ° x) n"
  | "norm_nn n (n' ⋄ x) = norm_nn (norm_pn ℬ n) n' ⋄ x"

primrec norm :: "'a itrm ⇒ 'a itrm"
where
    "norm (Opaque x) = Pure ℐ ⋄ Opaque x"
  | "norm (Pure x) = Pure x"
  | "norm (f ⋄ x) = norm_nn (norm f) (norm x)"


lemma norm_pn_in_cf:
  assumes "x ∈ CF"
    shows "norm_pn f x ∈ CF"
using assms
by (induction x arbitrary: f) auto

lemma norm_nn_in_cf:
  assumes "n ∈ CF" "n' ∈ CF"
    shows "norm_nn n n' ∈ CF"
using assms(2,1)
by (induction n' arbitrary: n) (auto intro: norm_pn_in_cf)

lemma norm_in_cf: "norm x ∈ CF"
by (induction x) (auto intro: norm_nn_in_cf)


lemma norm_pn_equiv:
  assumes "x ∈ CF"
    shows "norm_pn f x ≃ Pure f ⋄ x"
using assms proof (induction x arbitrary: f)
  case (pure_cf x)
  have "Pure (f ° x) ≃ Pure f ⋄ Pure x" using itrm_hom[symmetric] .
  then show ?case by simp
next
  case (ap_cf n x)
  from ap_cf.IH have "norm_pn (ℬ ° f) n ≃ Pure (ℬ ° f) ⋄ n" .
  then have "norm_pn (ℬ ° f) n ⋄ Opaque x ≃ Pure (ℬ ° f) ⋄ n ⋄ Opaque x" ..
  also have "... ≃ Pure ℬ ⋄ Pure f ⋄ n ⋄ Opaque x"
    using itrm_hom[symmetric] by blast
  also have "... ≃ Pure f ⋄ (n ⋄ Opaque x)" using itrm_comp .
  finally show ?case by simp
qed

lemma norm_nn_equiv:
  assumes "n ∈ CF" "n' ∈ CF"
    shows "norm_nn n n' ≃ n ⋄ n'"
using assms(2,1) proof (induction n' arbitrary: n)
  case (pure_cf x)
  then have "norm_pn (𝒯 ° x) n ≃ Pure (𝒯 ° x) ⋄ n" by (rule norm_pn_equiv)
  also have "... ≃ n ⋄ Pure x" using itrm_xchng[symmetric] .
  finally show ?case by simp
next
  case (ap_cf n' x)
  have "norm_nn (norm_pn ℬ n) n' ⋄ Opaque x ≃ Pure ℬ ⋄ n ⋄ n' ⋄ Opaque x" proof
    from ‹n ∈ CF› have "norm_pn ℬ n ∈ CF" by (rule norm_pn_in_cf)
    with ap_cf.IH have "norm_nn (norm_pn ℬ n) n' ≃ norm_pn ℬ n ⋄ n'" .
    also have "... ≃ Pure ℬ ⋄ n ⋄ n'" using norm_pn_equiv ‹n ∈ CF› by blast
    finally show "norm_nn (norm_pn ℬ n) n' ≃ Pure ℬ ⋄ n ⋄ n'" .
  qed
  also have "... ≃ n ⋄ (n' ⋄ Opaque x)" using itrm_comp .
  finally show ?case by simp
qed

lemma norm_equiv: "norm x ≃ x"
proof (induction)
  case (Opaque x)
  have "Pure ℐ ⋄ Opaque x ≃ Opaque x" using itrm_id .
  then show ?case by simp
next
  case (Pure x)
  show ?case by simp
next
  case (IAp f x)
  have "norm f ∈ CF" and "norm x ∈ CF" by (rule norm_in_cf)+
  then have "norm_nn (norm f) (norm x) ≃ norm f ⋄ norm x"
    by (rule norm_nn_equiv)
  also have "... ≃ f ⋄ x" using IAp.IH ..
  finally show ?case by simp
qed

lemma normal_form: obtains n where "n ≃ x" and "n ∈ CF"
using norm_equiv norm_in_cf ..


subsubsection ‹Lifting with normal forms›

lemma nf_unlift:
  assumes equiv: "n ≃ x" and cf: "n ∈ CF"
    shows "CF_pure n ↔ unlift x"
proof -
  from cf have "CF_pure n ↔ unlift n" by (rule cf_unlift)
  also from equiv have "unlift n ↔ unlift x" by (rule unlift_equiv)
  finally show ?thesis .
qed

theorem nf_lifting:
  assumes opaque: "opaque x = opaque y"
      and base_eq: "unlift x ↔ unlift y"
    shows "x ≃ y"
proof -
  obtain n where nf_x: "n ≃ x" "n ∈ CF" by (rule normal_form)
  obtain n' where nf_y: "n' ≃ y" "n' ∈ CF" by (rule normal_form)

  from nf_x have "CF_pure n ↔ unlift x" by (rule nf_unlift)
  also note base_eq
  also from nf_y have "unlift y ↔ CF_pure n'" by (rule nf_unlift[THEN term_sym])
  finally have pure_eq: "CF_pure n ↔ CF_pure n'" .

  from nf_x(1) have "opaque n = opaque x" by (rule opaque_equiv)
  also note opaque
  also from nf_y(1) have "opaque y = opaque n'" by (rule opaque_equiv[THEN sym])
  finally have opaque_eq: "opaque n = opaque n'" .

  from nf_x(1) have "x ≃ n" ..
  also have "n ≃ n'"
    using nf_x nf_y pure_eq opaque_eq
    by (blast intro: similar_into_equiv cf_similarI)
  also from nf_y(1) have "n' ≃ y" .
  finally show "x ≃ y" .
qed


subsubsection ‹Bracket abstraction, twice›

paragraph ‹Preliminaries: Sequential application of variables›

definition frees :: "dB ⇒ nat set"
where [simp]: "frees t = {i. free t i}"

definition var_dist :: "nat list ⇒ dB ⇒ dB"
where "var_dist = fold (λi t. t ° Var i)"

lemma var_dist_Nil[simp]: "var_dist [] t = t"
unfolding var_dist_def by simp

lemma var_dist_Cons[simp]: "var_dist (v # vs) t = var_dist vs (t ° Var v)"
unfolding var_dist_def by simp

lemma var_dist_append1: "var_dist (vs @ [v]) t = var_dist vs t ° Var v"
unfolding var_dist_def by simp

lemma var_dist_frees: "frees (var_dist vs t) = frees t ∪ set vs"
by (induction vs arbitrary: t) auto

lemma var_dist_subst_lt:
  "∀v∈set vs. i < v ⟹ (var_dist vs s)[t/i] = var_dist (map (λv. v - 1) vs) (s[t/i])"
by (induction vs arbitrary: s) simp_all

lemma var_dist_subst_gt:
  "∀v∈set vs. v < i ⟹ (var_dist vs s)[t/i] = var_dist vs (s[t/i])"
by (induction vs arbitrary: s) simp_all

definition vsubst :: "nat ⇒ nat ⇒ nat ⇒ nat"
where "vsubst u v w = (if u < w then u else if u = w then v else u - 1)"

lemma vsubst_subst[simp]: "(Var u)[Var v/w] = Var (vsubst u v w)"
unfolding vsubst_def by simp

lemma vsubst_subst_lt[simp]: "u < w ⟹ vsubst u v w = u"
unfolding vsubst_def by simp

lemma var_dist_subst_Var:
  "(var_dist vs s)[Var i/j] = var_dist (map (λv. vsubst v i j) vs) (s[Var i/j])"
by (induction vs arbitrary: s) simp_all

lemma var_dist_cong: "s ↔ t ⟹ var_dist vs s ↔ var_dist vs t"
by (induction vs arbitrary: s t) auto


paragraph ‹Preliminaries: Eta reductions with permuted variables›

lemma absn_subst: "((Abs^^n) s)[t/k] = (Abs^^n) (s[liftn n t 0/k+n])"
by (induction n arbitrary: t k) (simp_all add: liftn_lift_swap)

lemma absn_beta_equiv: "(Abs^^Suc n) s ° t ↔ (Abs^^n) (s[liftn n t 0/n])"
proof -
  have "(Abs^^Suc n) s ° t = Abs ((Abs^^n) s) ° t" by simp
  also have "... ↔ ((Abs^^n) s)[t/0]" by (rule beta_into_equiv) (rule beta.beta)
  also have "... = (Abs^^n) (s[liftn n t 0/n])" by (simp add: absn_subst)
  finally show ?thesis .
qed

lemma absn_dist_eta: "(Abs^^n) (var_dist (rev [0..<n]) (liftn n t 0)) ↔ t"
proof (induction n)
  case 0 show ?case by simp
next
  case (Suc n)
  let ?dist_range = "λa k. var_dist (rev [a..<k]) (liftn k t 0)"
  have append: "rev [0..<Suc n] = rev [1..<Suc n] @ [0]" by (simp add: upt_rec)
  have dist_last: "?dist_range 0 (Suc n) = ?dist_range 1 (Suc n) ° Var 0"
    unfolding append var_dist_append1 ..

  have "¬ free (?dist_range 1 (Suc n)) 0" proof -
    have "frees (?dist_range 1 (Suc n)) = frees (liftn (Suc n) t 0) ∪ {1..n}"
      unfolding var_dist_frees by fastforce
    then have "0 ∉ frees (?dist_range 1 (Suc n))" by simp
    then show ?thesis by simp
  qed
  then have "Abs (?dist_range 0 (Suc n)) →⇩η (?dist_range 1 (Suc n))[Var 0/0]"
    unfolding dist_last by (rule eta)
  also have "... = var_dist (rev [0..<n]) ((liftn (Suc n) t 0)[Var 0/0])" proof -
    have "∀v∈set (rev [1..<Suc n]). 0 < v" by auto
    moreover have "rev [0..<n] = map (λv. v - 1) (rev [1..<Suc n])" by (induction n) simp_all
    ultimately show ?thesis by (simp only: var_dist_subst_lt)
  qed
  also have "... = ?dist_range 0 n" using subst_liftn[of 0 n 0 t "Var 0"] by simp
  finally have "Abs (?dist_range 0 (Suc n)) ↔ ?dist_range 0 n" ..
  then have "(Abs^^Suc n) (?dist_range 0 (Suc n)) ↔ (Abs^^n) (?dist_range 0 n)"
    unfolding funpow_Suc_inside by (rule absn_cong)
  also from Suc.IH have "... ↔ t" .
  finally show ?case .
qed

primrec strip_context :: "nat ⇒ dB ⇒ nat ⇒ dB"
where
    "strip_context n (Var i) k = (if i < k then Var i else Var (i - n))"
  | "strip_context n (Abs t) k = Abs (strip_context n t (Suc k))"
  | "strip_context n (s ° t) k = strip_context n s k ° strip_context n t k"

lemma strip_context_liftn: "strip_context n (liftn (m + n) t k) k = liftn m t k"
by (induction t arbitrary: k) simp_all

lemma liftn_strip_context:
  assumes "∀i∈frees t. i < k ∨ k + n ≤ i"
    shows "liftn n (strip_context n t k) k = t"
using assms proof (induction t arbitrary: k)
  case (Abs t)
  have "∀i∈frees t. i < Suc k ∨ Suc k + n ≤ i" proof
    fix i assume free: "i ∈ frees t"
    show "i < Suc k ∨ Suc k + n ≤ i" proof (cases "i > 0")
      assume "i > 0"
      with free Abs.prems have "i-1 < k ∨ k + n ≤ i-1" by simp
      then show ?thesis by arith
    qed simp
  qed
  with Abs.IH show ?case by simp
qed auto

lemma absn_dist_eta_free:
  assumes "∀i∈frees t. n ≤ i"
  shows "(Abs^^n) (var_dist (rev [0..<n]) t) ↔ strip_context n t 0" (is "?lhs t ↔ ?rhs")
proof -
  have "?lhs (liftn n ?rhs 0) ↔ ?rhs" by (rule absn_dist_eta)
  moreover have "liftn n ?rhs 0 = t"
    using assms by (auto intro: liftn_strip_context)
  ultimately show ?thesis by simp
qed

definition perm_vars :: "nat ⇒ nat list ⇒ bool"
where "perm_vars n vs ⟷ distinct vs ∧ set vs = {0..<n}"

lemma perm_vars_distinct: "perm_vars n vs ⟹ distinct vs"
unfolding perm_vars_def by simp

lemma perm_vars_length: "perm_vars n vs ⟹ length vs = n"
unfolding perm_vars_def using distinct_card by force

lemma perm_vars_lt: "perm_vars n vs ⟹ ∀i∈set vs. i < n"
unfolding perm_vars_def by simp

lemma perm_vars_nth_lt: "perm_vars n vs ⟹ i < n ⟹ vs ! i < n"
using perm_vars_length perm_vars_lt by simp

lemma perm_vars_inj_on_nth:
  assumes "perm_vars n vs"
    shows "inj_on (nth vs) {0..<n}"
proof (rule inj_onI)
  fix i j
  assume "i ∈ {0..<n}" and "j ∈ {0..<n}"
  with assms have "i < length vs" and "j < length vs"
    using perm_vars_length by simp+
  moreover from assms have "distinct vs" by (rule perm_vars_distinct)
  moreover assume "vs ! i = vs ! j"
  ultimately show "i = j" using nth_eq_iff_index_eq by blast
qed

abbreviation perm_vars_inv :: "nat ⇒ nat list ⇒ nat ⇒ nat"
where "perm_vars_inv n vs i ≡ the_inv_into {0..<n} ((!) vs) i"

lemma perm_vars_inv_nth:
  assumes "perm_vars n vs"
      and "i < n"
    shows "perm_vars_inv n vs (vs ! i) = i"
using assms by (auto intro: the_inv_into_f_f perm_vars_inj_on_nth)

lemma dist_perm_eta:
  assumes perm_vars: "perm_vars n vs"
  obtains vs' where "⋀t. ∀i∈frees t. n ≤ i ⟹
    (Abs^^n) (var_dist vs' ((Abs^^n) (var_dist vs (liftn n t 0)))) ↔ strip_context n t 0"
proof -
  define vsubsts where "vsubsts n vs' vs =
    map (λv.
      if v < n - length vs' then v
      else if v < n then vs' ! (n - v - 1) + (n - length vs')
      else v - length vs') vs" for n vs' vs

  let ?app_vars = "λt n vs' vs. var_dist vs' ((Abs^^n) (var_dist vs (liftn n t 0)))"
  {
    fix t :: dB and vs' :: "nat list"
    assume partial: "length vs' ≤ n"

    let ?m = "n - length vs'"
    have "?app_vars t n vs' vs ↔ (Abs^^?m) (var_dist (vsubsts n vs' vs) (liftn ?m t 0))"
    using partial proof (induction vs' arbitrary: vs n)
      case Nil
      then have "vsubsts n [] vs = vs" unfolding vsubsts_def by (auto intro: map_idI)
      then show ?case by simp
    next
      case (Cons v vs')
      define n' where "n' = n - 1"
      have Suc_n': "Suc n' = n" unfolding n'_def using Cons.prems by simp
      have vs'_length: "length vs' ≤ n'" unfolding n'_def using Cons.prems by simp
      let ?m' = "n' - length vs'"
      have m'_conv: "?m' = n - length (v # vs')" unfolding n'_def by simp

      have "?app_vars t n (v # vs') vs = ?app_vars t (Suc n') (v # vs') vs"
        unfolding Suc_n' ..
      also have "... ↔ var_dist vs' ((Abs^^Suc n') (var_dist vs (liftn (Suc n') t 0)) ° Var v)"
        unfolding var_dist_Cons ..
      also have "... ↔ ?app_vars t n' vs' (vsubsts n [v] vs)" proof (rule var_dist_cong)
        have "map (λvv. vsubst vv (v + n') n') vs = vsubsts n [v] vs"
          unfolding Suc_n'[symmetric] vsubsts_def vsubst_def
          by (auto cong: if_cong)
        then have "(var_dist vs (liftn (Suc n') t 0))[liftn n' (Var v) 0/n']
                  = var_dist (vsubsts n [v] vs) (liftn n' t 0)"
          using var_dist_subst_Var subst_liftn by simp
        then show "(Abs^^Suc n') (var_dist vs (liftn (Suc n') t 0)) ° Var v
                  ↔ (Abs^^n') (var_dist (vsubsts n [v] vs) (liftn n' t 0))"
          by (fastforce intro: absn_beta_equiv[THEN term_trans])
      qed
      also have "... ↔ (Abs^^?m') (var_dist (vsubsts n' vs' (vsubsts n [v] vs)) (liftn ?m' t 0))"
        using vs'_length Cons.IH by blast
      also have "... = (Abs^^?m') (var_dist (vsubsts n (v # vs') vs) (liftn ?m' t 0))"
      proof -
        have "vsubsts n' vs' (vsubsts (Suc n') [v] vs) = vsubsts (Suc n') (v # vs') vs"
          unfolding vsubsts_def
          using vs'_length [[linarith_split_limit=10]]
          by auto
        then show ?thesis unfolding Suc_n' by simp
      qed
      finally show ?case unfolding m'_conv .
    qed
  }
  note partial_appd = this

  define vs' where "vs' = map (λi. n - perm_vars_inv n vs (n - i - 1) - 1) [0..<n]"

  from perm_vars have vs_length: "length vs = n" by (rule perm_vars_length)
  have vs'_length: "length vs' = n" unfolding vs'_def by simp

  have "map (λv. vs' ! (n - v - 1)) vs = rev [0..<n]" proof -
    have "length vs = length (rev [0..<n])"
      unfolding vs_length by simp
    then have "list_all2 (λv v'. vs' ! (n - v - 1) = v') vs (rev [0..<n])" proof
      fix i assume "i < length vs"
      then have "i < n" unfolding vs_length .
      then have "vs ! i < n" using perm_vars perm_vars_nth_lt by simp
      with ‹i < n› have "vs' ! (n - vs ! i - 1) = n - perm_vars_inv n vs (vs ! i) - 1"
        unfolding vs'_def by simp
      also from ‹i < n› have "... = n - i - 1" using perm_vars perm_vars_inv_nth by simp
      also from ‹i < n› have "... = rev [0..<n] ! i" by (simp add: rev_nth)
      finally show "vs' ! (n - vs ! i - 1) = rev [0..<n] ! i" .
    qed
    then show ?thesis
      unfolding list.rel_eq[symmetric]
      using list.rel_map
      by auto
  qed
  then have vs'_vs: "vsubsts n vs' vs = rev [0..<n]"
    unfolding vsubsts_def vs'_length
    using perm_vars perm_vars_lt
    by (auto intro: map_ext[THEN trans])

  let ?appd_vars = "λt n. var_dist (rev [0..<n]) t"
  {
    fix t
    assume not_free: "∀i∈frees t. n ≤ i"
    have "?app_vars t n vs' vs ↔ ?appd_vars t n" for t
      using partial_appd[of vs'] vs'_length vs'_vs by simp
    then have "(Abs^^n) (?app_vars t n vs' vs) ↔ (Abs^^n) (?appd_vars t n)"
      by (rule absn_cong)
    also have "... ↔ strip_context n t 0"
      using not_free by (rule absn_dist_eta_free)
    finally have "(Abs^^n) (?app_vars t n vs' vs) ↔ strip_context n t 0" .
  }
  with that show ?thesis .
qed

lemma liftn_absn: "liftn n ((Abs^^m) t) k = (Abs^^m) (liftn n t (k + m))"
by (induction m arbitrary: k) auto

lemma liftn_var_dist_lt:
  "∀i∈set vs. i < k ⟹ liftn n (var_dist vs t) k = var_dist vs (liftn n t k)"
by (induction vs arbitrary: t) auto

lemma liftn_context_conv: "k ≤ k' ⟹ ∀i∈frees t. i < k ∨ k' ≤ i ⟹ liftn n t k = liftn n t k'"
proof (induction t arbitrary: k k')
  case (Abs t)
  have "∀i∈frees t. i < Suc k ∨ Suc k' ≤ i" proof
    fix i assume "i ∈ frees t"
    show "i < Suc k ∨ Suc k' ≤ i" proof (cases "i = 0")
      assume "i = 0" then show ?thesis by simp
    next
      assume "i ≠ 0"
      from Abs.prems(2) have "∀i. free t (Suc i) ⟶ i < k ∨ k' ≤ i" by auto
      then have "∀i. 0 < i ∧ free t i ⟶ i - 1 < k ∨ k' ≤ i - 1" by simp
      then have "∀i. 0 < i ∧ free t i ⟶ i < Suc k ∨ Suc k' ≤ i" by auto
      with ‹i ≠ 0› ‹i ∈ frees t› show ?thesis by simp
    qed
  qed
  with Abs.IH Abs.prems(1) show ?case by auto
qed auto

lemma liftn_liftn0: "∀i∈frees t. k ≤ i ⟹ liftn n t k = liftn n t 0"
using liftn_context_conv by auto

lemma dist_perm_eta_equiv:
  assumes perm_vars: "perm_vars n vs"
      and not_free: "∀i∈frees s. n ≤ i" "∀i∈frees t. n ≤ i"
      and perm_equiv: "(Abs^^n) (var_dist vs s) ↔ (Abs^^n) (var_dist vs t)"
    shows "strip_context n s 0 ↔ strip_context n t 0"
proof -
  from perm_vars have vs_lt_n: "∀i∈set vs. i < n" using perm_vars_lt by simp
  obtain vs' where
    etas: "⋀t. ∀i∈frees t. n ≤ i ⟹
          (Abs^^n) (var_dist vs' ((Abs^^n) (var_dist vs (liftn n t 0)))) ↔ strip_context n t 0"
    using perm_vars dist_perm_eta by blast

  have "strip_context n s 0 ↔ (Abs^^n) (var_dist vs' ((Abs^^n) (var_dist vs (liftn n s 0))))"
    using etas[THEN term_sym] not_free(1) .
  also have "... ↔ (Abs^^n) (var_dist vs' ((Abs^^n) (var_dist vs (liftn n t 0))))"
  proof (rule absn_cong, rule var_dist_cong)
    have "(Abs^^n) (var_dist vs (liftn n s 0)) = (Abs^^n) (var_dist vs (liftn n s n))"
      using not_free(1) liftn_liftn0[of s n] by simp
    also have "... = (Abs^^n) (liftn n (var_dist vs s) n)"
      using vs_lt_n liftn_var_dist_lt by simp
    also have "... = liftn n ((Abs^^n) (var_dist vs s)) 0"
      using liftn_absn by simp
    also have "... ↔ liftn n ((Abs^^n) (var_dist vs t)) 0"
      using perm_equiv by (rule equiv_liftn)
    also have "... = (Abs^^n) (liftn n (var_dist vs t) n)"
      using liftn_absn by simp
    also have "... = (Abs^^n) (var_dist vs (liftn n t n))"
      using vs_lt_n liftn_var_dist_lt by simp
    also have "... = (Abs^^n) (var_dist vs (liftn n t 0))"
      using not_free(2) liftn_liftn0[of t n] by simp
    finally show "(Abs^^n) (var_dist vs (liftn n s 0)) ↔ ..." .
  qed
  also have "... ↔ strip_context n t 0"
    using etas not_free(2) .
  finally show ?thesis .
qed


paragraph ‹General notion of bracket abstraction for lambda terms›

definition foldr_option :: "('a ⇒ 'b ⇒ 'b option) ⇒ 'a list ⇒ 'b ⇒ 'b option"
where "foldr_option f xs e = foldr (λa b. Option.bind b (f a)) xs (Some e)"

lemma bind_eq_SomeE:
  assumes "Option.bind x f = Some y"
  obtains x' where "x = Some x'" and "f x' = Some y"
using assms by (auto iff: bind_eq_Some_conv)

lemma foldr_option_Nil[simp]: "foldr_option f [] e = Some e"
unfolding foldr_option_def by simp

lemma foldr_option_Cons_SomeE:
  assumes "foldr_option f (x#xs) e = Some y"
  obtains y' where "foldr_option f xs e = Some y'" and "f x y' = Some y"
using assms unfolding foldr_option_def by (auto elim: bind_eq_SomeE)

locale bracket_abstraction =
  fixes term_bracket :: "nat ⇒ dB ⇒ dB option"
  assumes bracket_app: "term_bracket i s = Some s' ⟹ s' ° Var i ↔ s"
  assumes bracket_frees: "term_bracket i s = Some s' ⟹ frees s' = frees s - {i}"
begin

definition term_brackets :: "nat list ⇒ dB ⇒ dB option"
where "term_brackets = foldr_option term_bracket"

lemma term_brackets_Nil[simp]: "term_brackets [] t = Some t"
unfolding term_brackets_def by simp

lemma term_brackets_Cons_SomeE:
  assumes "term_brackets (v#vs) t = Some t'"
  obtains s' where "term_brackets vs t = Some s'" and "term_bracket v s' = Some t'"
using assms unfolding term_brackets_def by (elim foldr_option_Cons_SomeE)

lemma term_brackets_ConsI:
  assumes "term_brackets vs t = Some t'"
      and "term_bracket v t' = Some t''"
    shows "term_brackets (v#vs) t = Some t''"
using assms unfolding term_brackets_def foldr_option_def by simp

lemma term_brackets_dist:
  assumes "term_brackets vs t = Some t'"
    shows "var_dist vs t' ↔ t"
proof -
  from assms have "∀t''. t' ↔ t'' ⟶ var_dist vs t'' ↔ t"
  proof (induction vs arbitrary: t')
    case Nil then show ?case by (simp add: term_sym)
  next
    case (Cons v vs)
    from Cons.prems obtain u where
        inner: "term_brackets vs t = Some u" and
        step: "term_bracket v u = Some t'"
      by (auto elim: term_brackets_Cons_SomeE)
    from step have red1: "t' ° Var v ↔ u" by (rule bracket_app)
    show ?case proof rule+
      fix t'' assume "t' ↔ t''"
      with red1 have red: "t'' ° Var v ↔ u"
        using term_sym term_trans by blast
      have "var_dist (v # vs) t'' = var_dist vs (t'' ° Var v)" by simp
      also have "... ↔ t" using Cons.IH[OF inner] red[symmetric] by blast
      finally show "var_dist (v # vs) t'' ↔ t" .
    qed
  qed
  then show ?thesis by blast
qed

end (* locale bracket_abstraction *)


paragraph ‹Bracket abstraction for idiomatic terms›

text ‹We consider idiomatic terms with explicitly assigned variables.›

lemma strip_unlift_vars:
  assumes "opaque x = []"
  shows "strip_context n (unlift_vars n x) 0 = unlift_vars 0 x"
using assms by (induction x) (simp_all add: strip_context_liftn[where m=0, simplified])

lemma unlift_vars_frees: "∀i∈frees (unlift_vars n x). i ∈ set (opaque x) ∨ n ≤ i"
by (induction x) (auto simp add: free_liftn)

locale itrm_abstraction = special_idiom extra_rule for extra_rule :: "nat itrm ⇒ _" +
  fixes itrm_bracket :: "nat ⇒ nat itrm ⇒ nat itrm option"
  assumes itrm_bracket_ap: "itrm_bracket i x = Some x' ⟹ x' ⋄ Opaque i ≃⇧+ x"
  assumes itrm_bracket_opaque:
    "itrm_bracket i x = Some x' ⟹ set (opaque x') = set (opaque x) - {i}"
begin

definition "itrm_brackets = foldr_option itrm_bracket"

lemma itrm_brackets_Nil[simp]: "itrm_brackets [] x = Some x"
unfolding itrm_brackets_def by simp

lemma itrm_brackets_Cons_SomeE:
  assumes "itrm_brackets (v#vs) x = Some x'"
  obtains y' where "itrm_brackets vs x = Some y'" and "itrm_bracket v y' = Some x'"
using assms unfolding itrm_brackets_def by (elim foldr_option_Cons_SomeE)

definition "opaque_dist = fold (λi y. y ⋄ Opaque i)"

lemma opaque_dist_cong: "x ≃⇧+ y ⟹ opaque_dist vs x ≃⇧+ opaque_dist vs y"
unfolding opaque_dist_def
by (induction vs arbitrary: x y) (simp_all add: ap_congL)

lemma itrm_brackets_dist:
  assumes defined: "itrm_brackets vs x = Some x'"
    shows "opaque_dist vs x' ≃⇧+ x"
proof -
  define x'' where "x'' = x'"
  have "x' ≃⇧+ x''" unfolding x''_def ..
  with defined show "opaque_dist vs x'' ≃⇧+ x"
    unfolding opaque_dist_def
    proof (induction vs arbitrary: x' x'')
      case Nil then show ?case unfolding itrm_brackets_def by (simp add: itrm_sym)
    next
      case (Cons v vs)
      from Cons.prems(1) obtain y'
        where defined': "itrm_brackets vs x = Some y'"
          and "itrm_bracket v y' = Some x'"
        by (rule itrm_brackets_Cons_SomeE)
      then have "x' ⋄ Opaque v ≃⇧+ y'" by (elim itrm_bracket_ap)
      then have "x'' ⋄ Opaque v ≃⇧+ y'"
        using Cons.prems(2) by (blast intro: itrm_sym itrm_trans)
      note this[symmetric]
      with defined' have "fold (λi y. y ⋄ Opaque i) vs (x'' ⋄ Opaque v) ≃⇧+ x"
        using Cons.IH by blast
      then show ?case by simp
    qed
qed

lemma itrm_brackets_opaque:
  assumes "itrm_brackets vs x = Some x'"
    shows "set (opaque x') = set (opaque x) - set vs"
using assms proof (induction vs arbitrary: x')
  case Nil
  then show ?case unfolding itrm_brackets_def by simp
next
  case (Cons v vs)
  then show ?case
    by (auto elim: itrm_brackets_Cons_SomeE dest!: itrm_bracket_opaque)
qed

lemma itrm_brackets_all:
  assumes all_opaque: "set (opaque x) ⊆ set vs"
      and defined: "itrm_brackets vs x = Some x'"
    shows "opaque x' = []"
proof -
  from defined have "set (opaque x') = set (opaque x) - set vs"
    by (rule itrm_brackets_opaque)
  with all_opaque have "set (opaque x') = {}" by simp
  then show ?thesis by simp
qed

lemma itrm_brackets_all_unlift_vars:
  assumes all_opaque: "set (opaque x) ⊆ set vs"
      and defined: "itrm_brackets vs x = Some x'"
    shows "x' ≃⇧+ Pure (unlift_vars 0 x')"
proof (rule equiv_into_ext_equiv)
  from assms have "opaque x' = []" by (rule itrm_brackets_all)
  then show "x' ≃ Pure (unlift_vars 0 x')" by (rule all_pure_unlift_vars)
qed

end (* locale itrm_abstraction *)


subsubsection ‹Lifting with bracket abstraction›

locale lifted_bracket = bracket_abstraction + itrm_abstraction +
  assumes bracket_compat:
    "set (opaque x) ⊆ {0..<n} ⟹ i < n ⟹
      term_bracket i (unlift_vars n x) = map_option (unlift_vars n) (itrm_bracket i x)"
begin

lemma brackets_unlift_vars_swap:
  assumes all_opaque: "set (opaque x) ⊆ {0..<n}"
      and vs_bound: "set vs ⊆ {0..<n}"
      and defined: "itrm_brackets vs x = Some x'"
    shows "term_brackets vs (unlift_vars n x) = Some (unlift_vars n x')"
using vs_bound defined proof (induction vs arbitrary: x')
  case Nil
  then show ?case by simp
next
  case (Cons v vs)
  then obtain y'
    where ivs: "itrm_brackets vs x = Some y'"
      and iv: "itrm_bracket v y' = Some x'"
    by (elim itrm_brackets_Cons_SomeE)
  with Cons have "term_brackets vs (unlift_vars n x) = Some (unlift_vars n y')"
    by auto
  moreover {
    have "Some (unlift_vars n x') = map_option (unlift_vars n) (itrm_bracket v y')"
      unfolding iv by simp
    moreover have "set (opaque y') ⊆ {0..<n}"
      using all_opaque ivs by (auto dest: itrm_brackets_opaque)
    moreover have "v < n" using Cons.prems by simp
    ultimately have "term_bracket v (unlift_vars n y') = Some (unlift_vars n x')"
      using bracket_compat by auto
  }
  ultimately show ?case by (rule term_brackets_ConsI)
qed

theorem bracket_lifting:
  assumes all_vars: "set (opaque x) ∪ set (opaque y) ⊆ {0..<n}"
      and perm_vars: "perm_vars n vs"
      and defined: "itrm_brackets vs x = Some x'" "itrm_brackets vs y = Some y'"
      and base_eq: "(Abs^^n) (unlift_vars n x) ↔ (Abs^^n) (unlift_vars n y)"
    shows "x ≃⇧+ y"
proof -
  from perm_vars have set_vs: "set vs = {0..<n}"
    unfolding perm_vars_def by simp

  have x_swap: "term_brackets vs (unlift_vars n x) = Some (unlift_vars n x')"
    using all_vars set_vs defined(1) by (auto intro: brackets_unlift_vars_swap)
  have y_swap: "term_brackets vs (unlift_vars n y) = Some (unlift_vars n y')"
    using all_vars set_vs defined(2) by (auto intro: brackets_unlift_vars_swap)

  from all_vars have "set (opaque x) ⊆ set vs" unfolding set_vs by simp
  then have complete_x: "opaque x' = []"
    using defined(1) itrm_brackets_all by blast
  then have ux_frees: "∀i∈frees (unlift_vars n x'). n ≤ i"
    using unlift_vars_frees by fastforce

  from all_vars have "set (opaque y) ⊆ set vs" unfolding set_vs by simp
  then have complete_y: "opaque y' = []"
    using defined(2) itrm_brackets_all by blast
  then have uy_frees: "∀i∈frees (unlift_vars n y'). n ≤ i"
    using unlift_vars_frees by fastforce

  have "x ≃⇧+ opaque_dist vs x'"
    using defined(1) by (rule itrm_brackets_dist[symmetric])
  also have "... ≃⇧+ opaque_dist vs (Pure (unlift_vars 0 x'))"
    using all_vars set_vs defined(1)
    by (auto intro: opaque_dist_cong itrm_brackets_all_unlift_vars)
  also have "... ≃⇧+ opaque_dist vs (Pure (unlift_vars 0 y'))"
  proof (rule opaque_dist_cong, rule pure_cong)
    have "(Abs^^n) (var_dist vs (unlift_vars n x')) ↔ (Abs^^n) (unlift_vars n x)"
      using x_swap term_brackets_dist by auto
    also have "... ↔ (Abs^^n) (unlift_vars n y)" using base_eq .
    also have "... ↔ (Abs^^n) (var_dist vs (unlift_vars n y'))"
      using y_swap term_brackets_dist[THEN term_sym] by auto
    finally have "strip_context n (unlift_vars n x') 0 ↔ strip_context n (unlift_vars n y') 0"
      using perm_vars ux_frees uy_frees
      by (intro dist_perm_eta_equiv)
    then show "unlift_vars 0 x' ↔ unlift_vars 0 y'"
      using strip_unlift_vars complete_x complete_y by simp
  qed
  also have "... ≃⇧+ opaque_dist vs y'" proof (rule opaque_dist_cong)
    show "Pure (unlift_vars 0 y') ≃⇧+ y'"
      using all_vars set_vs defined(2) itrm_brackets_all_unlift_vars[THEN itrm_sym]
      by blast
  qed
  also have "... ≃⇧+ y" using defined(2) by (rule itrm_brackets_dist)
  finally show ?thesis .
qed

end (* locale lifted_bracket *)

end