Theory Renaming_Interpretations

(*
Author:  Christian Sternagel <c.sternagel@gmail.com> (2014, 2015)
Author:  René Thiemann <rene.thiemann@uibk.ac.at> (2014, 2015)
License: LGPL (see file COPYING.LESSER)
*)

section ‹Renaming of Terms, Substitutions, TRSs, ...›

theory Renaming_Interpretations
imports
  "../Auxiliaries/Renaming"
  Trs
  Unification
begin

text ‹Turning a permutation into a substitution.›
abbreviation "sop π ≡ Var ∘ Rep_perm π"

fun permute_term :: "'v perm ⇒ ('f, 'v) term ⇒ ('f, 'v) term"
where
  "permute_term p (Var x) = Var (permute_atom p x)" |
  "permute_term p (Fun f ts) = Fun f (map (permute_term p) ts)"

interpretation term_pt: permutation_type permute_term
  by standard (induct_tac [!] x, auto simp: map_idI)

adhoc_overloading
  PERMUTE permute_term and
  FRESH term_pt.fresh term_pt.fresh_set

interpretation terms_pt: list_pt permute_term ..

adhoc_overloading
  PERMUTE terms_pt.permute_list and
  FRESH terms_pt.fresh

lemma supp_Var:
  fixes x :: "'v :: infinite"
  shows "term_pt.supp (Var x) = {x}"
  using infinite_UNIV
  by (auto simp: term_pt.supp_def swap_atom)

lemma permute_Fun:
  fixes p :: "('v :: infinite) perm"
  shows "p ∙ (Fun f ss) = Fun f (p ∙ ss)"
  by (induct ss) (simp)+

lemma supp_Fun':
  "term_pt.supp (Fun f ss) = permutation_type.supp (op ∙) ss"
  by (simp only: term_pt.supp_def terms_pt.supp_def permute_Fun) auto

lemma supp_Fun:
  "term_pt.supp (Fun f ss) = (⋃s∈set ss. term_pt.supp s)"
  by (simp add: supp_Fun')

lemma supp_vars_term_eq:
  fixes t :: "('f, 'v :: infinite) term"
  shows "term_pt.supp t = vars_term t"
by (induct t) (simp add: supp_Var supp_Fun)+

interpretation subst_conjugate_pt: fun_pt permute_atom permute_term ..

abbreviation "conjugate_subst ≡ subst_conjugate_pt.permute_fun"

lemma term_apply_subst_eqvt [eqvt]:
  "p ∙ (t ⋅ σ) = (p ∙ t) ⋅ (conjugate_subst p σ)"
  by (induct t) (simp add: subst_conjugate_pt.permute_fun_def)+

definition permute_subst :: "('v :: infinite) perm ⇒ ('f, 'v) subst ⇒ ('f, 'v) subst"
where
  "permute_subst π σ x = π ∙ σ x"

interpretation subst_pt: permutation_type permute_subst
  by standard (simp add: permute_subst_def [abs_def])+

adhoc_overloading
  PERMUTE "permute_subst" and
  FRESH subst_pt.fresh

fun permute_ctxt :: "'v perm ⇒ ('f, 'v) ctxt ⇒ ('f, 'v) ctxt"
where
  "permute_ctxt p □ = □" |
  "permute_ctxt p (More f ss1 C ss2) =
    More f (map (permute_term p) ss1) (permute_ctxt p C) (map (permute_term p) ss2)"

interpretation ctxt_pt: permutation_type permute_ctxt
  by standard (induct_tac [!] x, auto simp: map_idI)

adhoc_overloading
  PERMUTE permute_ctxt and
  FRESH ctxt_pt.fresh

lemma supp_Hole:
  "ctxt_pt.supp □ = {}"
  by (simp add: ctxt_pt.supp_def)

lemma permute_More:
  fixes p :: "('v :: infinite) perm"
  shows "p ∙ (More f ss1 C ss2) = More f (p ∙ ss1) (p ∙ C) (p ∙ ss2)"
  by (simp)

lemma supp_More':
  "ctxt_pt.supp (More f ss1 C ss2) =
    permutation_type.supp (op ∙) ss1 ∪ ctxt_pt.supp C ∪  permutation_type.supp (op ∙) ss2"
  by (simp only: ctxt_pt.supp_def terms_pt.supp_def) auto

lemma supp_More:
  "ctxt_pt.supp (More f ss1 C ss2) =
    (⋃s∈set ss1. term_pt.supp s) ∪ ctxt_pt.supp C ∪ (⋃s∈set ss2. term_pt.supp s)"
  by (simp add: supp_More')

lemma supp_vars_ctxt_eq:
  fixes C :: "('f, 'v :: infinite) ctxt"
  shows "ctxt_pt.supp C = vars_ctxt C"
  by (induct C) (auto simp: supp_Hole supp_More supp_vars_term_eq)

lemma term_apply_ctxt_eqvt [eqvt]:
  fixes p :: "('v :: infinite) perm"
  shows "p ∙ (C⟨t⟩) = (p ∙ C)⟨p ∙ t⟩"
  by (induct C) simp+

interpretation rule_pt: prod_pt permute_term permute_term ..
interpretation rules_pt: list_pt rule_pt.permute_prod ..

adhoc_overloading
  PERMUTE rule_pt.permute_prod rules_pt.permute_list and
  FRESH rule_pt.fresh rule_pt.fresh_set rules_pt.fresh rules_pt.fresh_set

lemma supp_vars_rule_eq:
  fixes r :: "('f, 'v :: infinite) rule"
  shows "rule_pt.supp r = vars_term (fst r) ∪ vars_term (snd r)"
  by (cases r) (simp add: supp_vars_term_eq)

interpretation trs_pt: rel_pt permute_term ..

adhoc_overloading
  PERMUTE trs_pt.permute_set and
  FRESH trs_pt.fresh

interpretation term_set_pt: set_pt permute_term ..

adhoc_overloading
  PERMUTE term_set_pt.permute_set and
  FRESH term_set_pt.fresh

lemma rule_mem_trs_iff [iff]:
  fixes p :: "('v :: infinite) perm" and R :: "('f, 'v) term rel"
  shows "(p ∙ s, p ∙ t) ∈ p ∙ R ⟷ (s, t) ∈ R"
unfolding rule_pt.permute_prod.simps [symmetric] trs_pt.mem_permute_iff ..

lemma inv_rule_mem_trs_simps [simp]:
  fixes p :: "('v :: infinite) perm" and R :: "('f, 'v) term rel"
  shows "(-p ∙ s, -p ∙ t) ∈ R ⟷ (s, t) ∈ p ∙ R"
    and "(s, t) ∈ -p ∙ R ⟷ (p ∙ s, p ∙ t) ∈ R"
  unfolding rule_pt.permute_prod.simps [symmetric]
  by (metis trs_pt.inv_mem_simps(1))
     (metis trs_pt.inv_mem_simps(2))

lemma symcl_trs_eqvt [eqvt]: "π ∙ R⇧↔ = (π ∙ R)⇧↔"
  apply (auto simp: eqvt)
  apply (meson converse_iff inv_rule_mem_trs_simps(1))
  by (meson converse.intros inv_rule_mem_trs_simps(1))

lemma term_apply_subst_Var_Rep_perm [simp]:
  "t ⋅ sop p = p ∙ t"
  by (induct t) (simp add: permute_atom_def)+

lemma rstep_permute_subset:
  "rstep (p ∙ R) ⊆ rstep R"
proof (rule subrelI)
  fix s t
  assume "(s, t) ∈ rstep (p ∙ R)"
  then show "(s, t) ∈ rstep R"
  proof (rule rstepE)
    fix l r C σ
    assume "(l, r) ∈ p ∙ R" and [simp]: "s = C⟨l ⋅ σ⟩" "t = C⟨r ⋅ σ⟩"
    then have "(-p ∙ l, -p ∙ r) ∈ R" by simp
    then have "((-p ∙ l) ⋅ sop p, (-p ∙ r) ⋅ sop p) ∈ rstep R" by blast
    then show "(s, t) ∈ rstep R" by auto
  qed
qed

text ‹The rewrite relation is invariant under variable renamings of the given TRS.›
lemma rstep_permute [simp]:
  "rstep (p ∙ R) = rstep R"
proof
  show "rstep (p ∙ R) ⊆ rstep R" by (rule rstep_permute_subset)
next
  have "rstep R = rstep (-p ∙ p ∙ R)" by simp
  also have "… ⊆ rstep (p ∙ R)" by (rule rstep_permute_subset)
  finally show "rstep R ⊆ rstep (p ∙ R)" .
qed

lemma permute_rstep_subset:
  "p ∙ rstep R ⊆ rstep R"
proof (rule subrelI)
  fix s t
  assume "(s, t) ∈ p ∙ rstep R"
  then have "(-p ∙ s, -p ∙ t) ∈ rstep R" by simp
  then show "(s, t) ∈ rstep R"
  proof (induct x≡"-p ∙ s" y≡"-p ∙ t")
    case (IH C σ l r)
    then have "(p ∙ l, p ∙ r) ∈ p ∙ R"
      and [simp]: "s = p ∙ C⟨l ⋅ σ⟩" "t = p ∙ C⟨r ⋅ σ⟩" by simp+
    then have "((p ∙ C)⟨(p ∙ l) ⋅ (conjugate_subst p σ)⟩,
                (p ∙ C)⟨(p ∙ r) ⋅ (conjugate_subst p σ)⟩) ∈ rstep (p ∙ R)" by blast
    then show "(s, t) ∈ rstep R" by (simp add: eqvt)
  qed
qed

lemma permute_rstep [simp]:
  "p ∙ rstep R = rstep R"
proof
  show "p ∙ rstep R ⊆ rstep R" by (rule permute_rstep_subset)
next
  have "rstep R = p ∙ -p ∙ rstep R" by simp
  also have "… ⊆ p ∙ rstep R"
    using permute_rstep_subset [of "-p" R] by auto
  finally show "rstep R ⊆ p ∙ rstep R" .
qed

lemma rstep_eqvt [eqvt]:
  "p ∙ rstep R = rstep (p ∙ R)"
  by simp

lemma rstep_imp_perm_rstep:
  "(s, t) ∈ rstep R ⟹ (p ∙ s, p ∙ t) ∈ rstep R"
  by (subst (asm) rule_mem_trs_iff [symmetric]) (simp add: eqvt)

lemma perm_rstep_imp_rstep:
  "(p ∙ s, p ∙ t) ∈ rstep R ⟹ (s, t) ∈ rstep R"
  by (subst (asm) rule_mem_trs_iff [symmetric, of _ _ _ "-p"]) (simp add: eqvt)

lemma rstep_permute_iff [iff]:
  "(p ∙ s, p ∙ t) ∈ rstep R ⟷ (s, t) ∈ rstep R"
  by (metis perm_rstep_imp_rstep rstep_imp_perm_rstep)

lemma term_apply_subst_Var_Abs_perm:
  "f ∈ perms ⟹ t ⋅ (Var ∘ f) = Abs_perm f ∙ t"
  by (metis Abs_perm_inverse term_apply_subst_Var_Rep_perm)

lemma finite_term_supp: "finite (term_pt.supp t)"
  unfolding supp_vars_term_eq
  by (induct t) simp+

lemma finite_rule_supp: "finite (rule_pt.supp (l, r))"
  by (simp add: finite_term_supp)

interpretation term_fs: finitely_supported permute_term
  by standard (rule finite_term_supp)

interpretation rule_fs: finitely_supported rule_pt.permute_prod
  by standard (auto simp: finite_rule_supp finite_term_supp)

lemma vars_rule_disjoint:
  fixes l r u v :: "('f, 'v :: infinite) term"
  shows "∃p. vars_rule (p ∙ (l, r)) ∩ vars_rule (u, v) = {}"
proof -
  from rule_fs.supp_fresh_set obtain p
    where "rule_pt.supp (p ∙ (l, r)) ♯ (u, v)" by blast
  from rule_pt.fresh_set_disjoint [OF this]
    show ?thesis
    by (auto simp: supp_vars_rule_eq vars_rule_def)
qed

lemma vars_term_eqvt [eqvt]:
  "π ∙ vars_term t = vars_term (π ∙ t)"
  by (simp add: supp_vars_term_eq [symmetric] eqvt)

lemma permute_term_subst_apply_term:
  "(π ∙ t) ⋅ σ = t ⋅ (σ ∘ Rep_perm π)"
  by (induct t) (simp_all add: permute_atom_def)

lemma permute_subst_subst_compose:
  "π ∙ σ = σ ∘⇩s sop π"
  by (rule ext) (simp add: subst_compose_def permute_subst_def)

lemma vars_rule_eqvt [eqvt]:
  "π ∙ vars_rule r = vars_rule (π ∙ r)"
  by (simp add: vars_rule_def) (metis rule_fs.supp_eqvt supp_vars_rule_eq)

lemma funposs_perm_simp [simp]:
  "funposs (π ∙ t) = funposs t"
  by (induct t) auto

lemma poss_perm_simp [simp]:
  "poss (π ∙ t) = poss t"
  by (induct t) auto

definition permute_pos :: "'a perm ⇒ pos ⇒ pos"
where
  "permute_pos π (p :: pos) = p"

interpretation pos_pure: pure permute_pos
  by standard (simp_all add: permute_pos_def)

adhoc_overloading
  PERMUTE permute_pos

interpretation pos_set_pt: set_pt permute_pos ..

adhoc_overloading
  PERMUTE pos_set_pt.permute_set

interpretation pos_set_pure: pure pos_set_pt.permute_set
  by standard (simp add: permute_pos_def pos_set_pt.permute_set_def)

lemma funposs_eqvt [eqvt]:
  "π ∙ funposs t = funposs (π ∙ t)"
  by simp

lemma poss_eqvt [eqvt]:
  "π ∙ poss t = poss (π ∙ t)"
  by simp

lemma subt_at_eqvt [eqvt]:
  "p ∈ poss t ⟹ π ∙ (t |_ p) = (π ∙ t) |_ p"
  by (induct t p rule: subt_at.induct)
     (auto simp del: subt_at_PCons_distr)

lemma subst_variants_id:
  assumes variants: "σ ∘⇩s σ' = τ" "τ ∘⇩s τ' = σ"
    and x: "x ∈ ⋃(vars_term ` σ ` V)" (is "x ∈ ?D")
  shows "(the_Var ∘ τ') ((the_Var ∘ σ') x) = x" (is "?τ' (?σ' x) = x")
proof -
  note * [simp] = subst_variants_imp_eq [OF variants]
  { fix y
    assume **: "x ∈ vars_term (σ y)"
    then have var: "is_Var (σ' x)"
      using variants_imp_is_Var [OF *] by simp
    have "⋀μ. μ x = Var x ∨ σ y ⋅ μ ≠ σ y"
      using ** by (metis subst_apply_term_empty term_subst_eq_rev)
    then have "⋀μ ν. (ν x) ⋅ μ = Var x ∨ σ y ⋅ ν ⋅ μ ≠ σ y"
      by (metis subst_apply_term.simps(1) subst_subst)
    then have "?τ' (?σ' x) = x"
      using var and * by (metis term.collapse(1) subst_apply_term.simps(1) term.sel(1) o_def) }
  then show ?thesis using x by auto
qed

lemma subst_variants_image_subset:
  assumes variants: "σ ∘⇩s σ' = τ" "τ ∘⇩s τ' = σ"
  shows "(the_Var ∘ σ') ` ⋃(vars_term ` σ ` V) ⊆ ⋃(vars_term ` τ ` V)"
  (is "?σ' ` ?S ⊆ ?T")
proof
  note * = subst_variants_imp_eq [OF variants]
  have subst_fun_range_subset: "?S ⊆ subst_fun_range σ" by (auto simp: subst_fun_range_def)
  note is_Var = subst_variants_imp_is_Var [OF variants]

  fix x⇩0
  assume "x⇩0 ∈ ?σ' ` ?S"
  then obtain x where **: "?σ' x = x⇩0" and "x ∈ ?S" by blast
  then obtain x' where "x ∈ vars_term (σ x')" and "x' ∈ V" by (auto)
  then have "σ x' ⊵ Var x" by (metis supteq_Var)
  then have "σ x' ⋅ σ' ⊵ σ' x" by auto
  then have "τ x' ⊵ σ' x" by (simp add: *)
  moreover
  from is_Var and subst_fun_range_subset and ‹x ∈ ?S› have "is_Var (σ' x)" by auto
  ultimately have "?σ' x ∈ vars_term (τ x')"
    by (metis term.collapse(1) comp_def subteq_Var_imp_in_vars_term)
  then have "?σ' x ∈ ?T" using ‹x' ∈ V› by (auto simp:)
  then show "x⇩0 ∈ ?T" unfolding ** .
qed

lemma subst_variants_imp_image_eq:
  assumes "σ ∘⇩s σ' = τ" and "τ ∘⇩s τ' = σ"
  shows "(the_Var ∘ σ') ` ⋃(vars_term ` σ ` V) = ⋃(vars_term ` τ ` V)"
  (is "?σ' ` ?S = ?T")
proof
  show "?σ' ` ?S ⊆ ?T"
    using subst_variants_image_subset [OF assms, of V] by (simp)
next
  let ?τ' = "the_Var ∘ τ'"
  have "?σ' ` ?τ' ` ?T ⊆ ?σ' ` ?S"
    using subst_variants_image_subset [OF assms(2, 1), of V] by (metis image_mono)
  moreover have "?σ' ` ?τ' ` ?T = ?T"
    using subst_variants_id [OF assms(2, 1), of _ V]
    by (auto simp: o_def) (metis, metis (full_types) UN_I image_eqI)
  ultimately show "?T ⊆ ?σ' ` ?S" by simp
qed

text ‹If two variables are substitution instances of each other, then they only differ
by a variable renaming.›
lemma subst_variants_imp_perm:
  fixes σ τ :: "('f, 'v :: infinite) subst"
  assumes variants: "σ ∘⇩s σ' = τ" "τ ∘⇩s τ' = σ"
    and finite: "finite (subst_domain σ)" "finite (subst_domain τ)"
  shows "∃π. π ∙ σ = τ"
proof -
  def D ≡ "subst_domain σ ∪ subst_domain τ"
  def D⇩σ ≡ "⋃(vars_term ` σ ` D)"
  def D⇩τ ≡ "⋃(vars_term ` τ ` D)"
  let ?σ' = "the_Var ∘ σ'"
  let ?τ' = "the_Var ∘ τ'"

  note * = subst_variants_imp_eq [OF variants]
  note is_Var = subst_variants_imp_is_Var [OF variants]

  have finite: "finite D⇩σ" using finite by (auto simp: D⇩σ_def D_def)
  have subst_fun_range_subset: "D⇩σ ⊆ subst_fun_range σ" by (auto simp: D⇩σ_def subst_fun_range_def)
  have id: "⋀x. x ∉ D ⟹ σ' x = Var x" "⋀x. x ∉ D ⟹ τ' x = Var x"
           "⋀x. x ∉ D ⟹ σ x = Var x" "⋀x. x ∉ D ⟹ τ x = Var x"
    using * by (auto simp: D_def subst_domain_def) (metis subst_apply_term.simps(1))+

  have "?σ' ` D⇩σ = D⇩τ"
    using subst_variants_imp_image_eq [OF variants] by (simp add: D⇩σ_def D⇩τ_def)
  moreover have "inj_on ?σ' D⇩σ"
    by (rule inj_on_inverseI [of _ "?τ'"]) (insert subst_variants_id [OF variants], simp add: D⇩σ_def)
  ultimately have "bij_betw ?σ' D⇩σ D⇩τ" by (auto simp: bij_betw_def)
  from bij_betw_extend [OF this, of UNIV] and finite obtain g
    where "finite {x. g x ≠ x}" and g_id: "(∀x∈UNIV - (D⇩σ ∪ D⇩τ). g x = x)"
      and g_eq: "∀x∈D⇩σ. g x = (the_Var ∘ σ') x" and "bij g" by blast
  then have perm: "g ∈ perms" by (auto simp: perms_def)
  have "Abs_perm g ∙ σ = τ"
  proof (rule ext)
    fix x
    have "Abs_perm g ∙ σ x = τ x"
    proof (cases "x ∈ D")
      assume "x ∈ D"
      then have "vars_term (σ x) ⊆ D⇩σ" by (auto simp: D⇩σ_def)
      with g_eq and term_subst_eq [of "σ x" "Var ∘ g" "σ'"]
        have "σ x ⋅ (Var ∘ g) = σ x ⋅ σ'"
        by auto (metis subst_fun_range_subset(1) term.collapse(1) is_Var(1) set_rev_mp)
      with perm and * show ?thesis by (simp add: term_apply_subst_Var_Abs_perm)
    next
      have "D⇩τ - D ⊆ D⇩σ - D"
      proof -
        have [simp]: "?τ' ` (D⇩τ - D) = D⇩τ - D"
          using id by auto (metis (full_types) DiffI imageI image_comp term.sel(1))
        have "?τ' ` (D⇩τ - D) ⊆ ?τ' ` D⇩τ" by blast
        also have "... ⊆ D⇩σ"
          using subst_variants_image_subset [OF variants(2, 1), of D] by (simp add: D⇩τ_def D⇩σ_def)
        finally show ?thesis by auto
      qed
      then have **: "D⇩τ - D⇩σ ⊆ D" by blast
      assume "x ∉ D"
      moreover then have "Abs_perm g ∙ x = x"
        using g_eq and id and g_id and perm and **
        by (cases "x ∈ D⇩σ") (auto simp: permute_atom_def Abs_perm_inverse)
      ultimately show ?thesis by (simp add: id)
    qed
    then show "(Abs_perm g ∙ σ) x = τ x" by (simp add: permute_subst_def)
  qed
  then show ?thesis ..
qed

lemma is_mgu_imp_perm:
  fixes E :: "('f, 'v :: infinite) equations"
  assumes mgu: "is_mgu σ E" "is_mgu τ E"
    and finite: "finite (subst_domain σ)" "finite (subst_domain τ)"
  shows "∃π. π ∙ σ = τ"
proof -
  obtain σ' τ' :: "('f, 'v) subst"
    where "σ ∘⇩s σ' = τ" and "τ ∘⇩s τ' = σ"
    using mgu by (auto simp: is_mgu_def unifiers_def) metis
  from subst_variants_imp_perm [OF this finite]
    show ?thesis .
qed

lemma unifiers_perm_simp [simp]:
  "π ∙ σ ∈ unifiers E ⟷ σ ∈ unifiers E"
  by (auto simp: unifiers_def permute_subst_subst_compose)

lemma inv_Rep_perm_simp [simp]:
  fixes x :: "'v :: infinite"
  shows "-π ∙ Rep_perm π x = x"
  by (simp add: permute_atom_def Rep_perm_uminus)
     (metis Rep_perm_uminus atom_pt.permute_minus_cancel(2) permute_atom_def)

lemma permute_subst_conjugate_subst [simp]:
  "(π ∙ σ) ∘⇩s conjugate_subst π τ = σ ∘⇩s (τ ∘⇩s (Var ∘ Rep_perm π))"
  apply (rule ext)
  apply (simp add: subst_conjugate_pt.permute_fun_def)
  apply (simp add: permute_subst_subst_compose ac_simps)
  apply (simp add: subst_compose_def)
done

text ‹Every renaming of an mgu is again an mgu.›
lemma is_mgu_perm:
  fixes E :: "('f, 'v :: infinite) equations"
  assumes "is_mgu σ E"
  shows "is_mgu (π ∙ σ) E"
proof (unfold is_mgu_def, intro conjI ballI)
  show "π ∙ σ ∈ unifiers E" using assms by (simp add: is_mgu_def)
next
  fix τ :: "('f, 'v) subst"
  assume "τ ∈ unifiers E"
  then obtain γ :: "('f, 'v) subst"
    where "τ = σ ∘⇩s γ" using assms by (auto simp: is_mgu_def)
  then have "τ ∘⇩s sop π = (π ∙ σ) ∘⇩s conjugate_subst π γ"
    by (simp add: ac_simps)
  then have "τ ∘⇩s sop π ∘⇩s sop (-π) =
    (π ∙ σ) ∘⇩s conjugate_subst π γ ∘⇩s sop (-π)" by simp
  then have "τ = (π ∙ σ) ∘⇩s conjugate_subst π γ ∘⇩s sop (-π)"
    by (simp add: subst_compose_def)
  then have "τ = (π ∙ σ) ∘⇩s (conjugate_subst π γ ∘⇩s sop (-π))"
    unfolding subst_compose_assoc .
  then show "∃γ::('f, 'v) subst. τ = (π ∙ σ) ∘⇩s γ" by blast
qed

lemma Rep_perm_image:
  "Rep_perm π ` A = π ∙ A"
  by (metis atom_set_pt.permute_set_eq_image image_cong permute_atom_def)

(*Can this be proved abstractly, i.e.,
"finite (supp a) ==> ALL x : supp a. p ∙ x = p' ∙ x ==> p ∙ a = p' ∙ a"?*)
lemma vars_term_perm_eq:
  assumes "∀x∈vars_term t. π ∙ x = π' ∙ x"
  shows "π ∙ t = π' ∙ t"
  using assms by (induct t) simp_all

lemma vars_rule_perm_eq:
  assumes "∀x∈vars_rule r. π ∙ x = π' ∙ x"
  shows "π ∙ r = π' ∙ r"
  using assms by (cases r) (auto simp: vars_rule_def vars_term_perm_eq eqvt)

lemma rule_variants_imp_perm:
  assumes disj: "vars_rule (π⇩1 ∙ r) ∩ vars_rule (π⇩2 ∙ r') = {}" (is "?V ∩ ?V' = {}")
                "vars_rule (π⇩3 ∙ r) ∩ vars_rule (π⇩4 ∙ r') = {}" (is "?W ∩ ?W' = {}")
  shows "∃π. π ∙ π⇩3 ∙ r = π⇩1 ∙ r ∧ π ∙ π⇩4 ∙ r' = π⇩2 ∙ r'"
proof -
  let ?f = "Rep_perm (π⇩1 + -π⇩3)"
  let ?g = "Rep_perm (π⇩2 + -π⇩4)"
  have "bij ?f" by (metis bij_Rep_perm)
  then have bij: "bij_betw ?f ?W (?f ` ?W)" by (auto elim: bij_betw_subset)
  have "bij ?g" by (metis bij_Rep_perm)
  then have bij': "bij_betw ?g ?W' (?g ` ?W')" by (auto elim: bij_betw_subset)
  def f ≡ "λx. if x ∈ vars_rule (π⇩3 ∙ r) then ?f x else x"
  def g ≡ "λx. if x ∈ vars_rule (π⇩4 ∙ r') then ?g x else x"
  def h ≡ "λx. if x ∈ vars_rule (π⇩3 ∙ r) then f x else if x ∈ vars_rule (π⇩4 ∙ r') then g x else x"
  have bij: "bij_betw f ?W (f ` ?W)" using bij by (auto simp: f_def bij_betw_def inj_on_def)
  have bij': "bij_betw g ?W' (g ` ?W')" using bij' by (auto simp: g_def bij_betw_def inj_on_def)
  have *: "f ` ?W' = ?W'" "g ` ?W = ?W" using disj(2) by (auto simp: f_def g_def)
  have **: "h ` ?W' = g ` ?W'" "h ` ?W = f ` ?W" using disj(2) by (auto simp: h_def)
  have ***: "f ` ?W = ?V" "g ` ?W' = ?V'" using disj by (auto simp: f_def g_def eqvt Rep_perm_image)
  have "bij_betw h ?W ?V"
    using bij by (auto simp: *** bij_betw_def h_def inj_on_def)
  moreover have "bij_betw h ?W' ?V'"
    using bij' and disj
    apply (auto simp add: * ** *** bij_betw_def h_def inj_on_def)
    apply (metis "***"(2) imageI)
    apply (metis "***"(2) Compl_eq Diff_eq Diff_triv Int_absorb Int_commute)+
  done
  moreover have "h ` ?W ∩ h ` ?W' = {}"
    unfolding ** *** using disj(1) .
  ultimately have "bij_betw h (?W ∪ ?W') (?V ∪ ?V')"
    using  bij_betw_combine [of h ?W ?V ?W' ?V']
    unfolding ** *** by blast
  from conjI [THEN bij_betw_extend [OF this, of UNIV, simplified], OF finite_vars_rule finite_vars_rule]
    obtain b
    where "finite {x. b x ≠ x}"
    and neq: "∀x∈UNIV - ((?W ∪ ?W') ∪ (?V ∪ ?V')). b x = x"
    and eq: "∀x∈?W ∪ ?W'. b x = h x"
    and "bij b"
    by auto
  then have perm: "b ∈ perms" by (auto simp: perms_def)
  have "Abs_perm b ∙ π⇩3 ∙ r = π⇩1 ∙ r"
  proof -
    have "Abs_perm b ∙ π⇩3 ∙ r = Abs_perm ?f ∙ π⇩3 ∙ r"
    apply (rule vars_rule_perm_eq)
    apply (insert eq perm)
    apply (simp add: h_def f_def g_def Abs_perm_inverse Rep_perm permute_atom_def split: if_splits)
    done
    also have "… = π⇩1 ∙ r" by (simp add: Rep_perm_inverse)
    finally show ?thesis .
  qed
  moreover have "Abs_perm b ∙ π⇩4 ∙ r' = π⇩2 ∙ r'"
  proof -
    have "Abs_perm b ∙ π⇩4 ∙ r' = Abs_perm ?g ∙ π⇩4 ∙ r'"
    apply (rule vars_rule_perm_eq)
    apply (insert eq perm disj)
    apply (auto simp add: h_def f_def g_def Abs_perm_inverse Rep_perm permute_atom_def split: if_splits)
    done
    also have "… = π⇩2 ∙ r'" by (simp add: Rep_perm_inverse)
    finally show ?thesis .
  qed
  ultimately show ?thesis by blast
qed

lemma poss_perm_prod_simps [simp]:
  "poss (fst (π ∙ r)) = poss (fst r)"
  "poss (snd (π ∙ r)) = poss (snd r)"
  by (case_tac [!] r) (auto simp: eqvt)

lemma ctxt_of_pos_term_eqvt [eqvt]:
  assumes "p ∈ poss t"
  shows "π ∙ (ctxt_of_pos_term p t) = ctxt_of_pos_term p (π ∙ t)"
  using assms by (induct t arbitrary: p) (auto simp: take_map drop_map)

lemma finite_subst_domain_sop:
  "finite (subst_domain (sop π))"
  by (auto simp: subst_domain_def finite_Rep_perm)

lemma funposs_perm_iff [simp]:
  "p ∈ funposs (π ∙ t) ⟷ p ∈ funposs t"
  by (induct t) auto

lemma perm_rstep_conv [simp]:
  "π ∙ p ∈ rstep R ⟷ p ∈ rstep R"
  by (metis rstep_eqvt rstep_permute trs_pt.mem_permute_iff)

lemma perm_rstep_perm:
  assumes "(π ∙ s, t) ∈ rstep R"
  shows "∃u. t = π ∙ u"
  using assms by (metis term_pt.permute_minus_cancel(1))

lemma perm_rsteps_perm:
  assumes "(π ∙ s, t) ∈ (rstep R)⇧*"
  shows "∃u. t = π ∙ u"
  using assms by (metis term_pt.permute_minus_cancel(1))

lemma perm_rsteps_conv [simp]:
  "π ∙ p ∈ (rstep R)⇧* ⟷ p ∈ (rstep R)⇧*"
  by (metis perm_rstep_conv rstep_rtrancl_idemp)

lemma perm_join_conv [simp]:
  "π ∙ p ∈ (rstep R)⇧↓ ⟷ p ∈ (rstep R)⇧↓" (is "?L = ?R")
proof
  assume "?L"
  then obtain u
    where "(fst (π ∙ p), u) ∈ (rstep R)⇧*" and "(snd (π ∙ p), u) ∈ (rstep R)⇧*"
    by (metis joinE surjective_pairing)
  moreover then obtain v
    where [simp]: "u = π ∙ v" by (auto dest: perm_rsteps_perm simp: eqvt [symmetric])
  ultimately have "(fst p, v) ∈ (rstep R)⇧*" and "(snd p, v) ∈ (rstep R)⇧*"
    by (simp_all add: eqvt [symmetric])
  then show "?R" by (metis joinI surjective_pairing)
next
  assume "?R"
  then obtain u
    where "(fst p, u) ∈ (rstep R)⇧*" and "(snd p, u) ∈ (rstep R)⇧*"
    by (metis joinE surjective_pairing)
  then have "π ∙ (fst p, u) ∈ (rstep R)⇧*" and "π ∙ (snd p, u) ∈ (rstep R)⇧*" by auto
  then show "?L" by (metis joinI rule_pt.permute_prod_eqvt surjective_pairing)
qed

lemma permuted_rule_in_variants:
  assumes "(p ∙ s, p ∙ t) ∈ R"
  shows "(s, t) ∈ rule_pt.variants `` R"
  using assms
  by (auto simp: rule_pt.variants_def)
     (metis rule_pt.permute_minus_cancel(2) rule_pt.permute_prod.simps)

lemma in_funposs_eqvt:
  assumes "p ∈ funposs t"
  shows "p ∈ funposs (π ∙ t)"
  using assms by (induct t arbitrary: p) auto

text ‹Lists have an infinite universe.›
instance list :: (type) infinite by standard (rule infinite_UNIV_listI)

text ‹Two terms are variants iff they are substitution instances of each other.›
lemma term_variants_iff:
  fixes s t :: "('f, 'v :: infinite) term"
  shows "(∃π. π ∙ s = t) ⟷ (∃(σ :: ('f, 'v) subst) (τ :: ('f, 'v) subst). s ⋅ σ = t ∧ t ⋅ τ = s)"
  (is "?L = ?R")
proof
  assume "?L"
  then obtain π where *: "π ∙ s = t" ..
  have "s ⋅ (Var ∘ Rep_perm π) = t" by (simp add: *)
  moreover have "t ⋅ (Var ∘ Rep_perm (-π)) = s" by (simp add: * [symmetric])
  ultimately show "?R" by blast
next
  assume "?R"
  then obtain σ τ :: "('f, 'v) subst"
    where variants: "s ⋅ σ = t" "t ⋅ τ = s" by blast
  from variants_imp_bij_betw_vars [OF variants]
    have "bij_betw (the_Var ∘ σ) (vars_term s) (vars_term t)" .
  from bij_betw_extend [OF this, of UNIV] obtain g :: "'v ⇒ 'v"
    where "finite {x. g x ≠ x}" and *: "∀x∈vars_term s. g x = (the_Var ∘ σ) x" and "bij g" by auto
  then have "g ∈ perms" by (simp add: perms_def)
  then have **: "s ⋅ (Var ∘ g) = Abs_perm g ∙ s" by (rule term_apply_subst_Var_Abs_perm)
  from * have "∀x∈vars_term s. (Var ∘ g) x = σ x"
    using variants_imp_is_Var [OF variants] by simp
  from term_subst_eq_conv [THEN iffD2, OF this]
    show "?L" unfolding variants and ** ..
qed

lemma rstep_pos_permute [simp]:
  "rstep_pos (π ∙ R) p = rstep_pos R p"
proof
  show "rstep_pos (π ∙ R) p ⊆ rstep_pos R p"
  proof (rule subrelI)
    fix s t
    assume "(s, t) ∈ rstep_pos (π ∙ R) p"
    then show "(s, t) ∈ rstep_pos R p"
    proof (cases)
      fix l r σ
      assume "(l, r) ∈ π ∙ R"
        and [simp]: "s |_ p = l ⋅ σ" "t = (ctxt_of_pos_term p s)⟨r ⋅ σ⟩"
        and p: "p ∈ poss s"
      then have "(-π ∙ l, -π ∙ r) ∈ -π ∙ π ∙ R" by simp
      then have "(-π ∙ l, -π ∙ r) ∈ R" by simp
      from rstep_pos.intros [OF this p, of "sop π ∘⇩s σ"]
        show "(s, t) ∈ rstep_pos R p" by simp
    qed
  qed
next
  show "rstep_pos R p ⊆ rstep_pos (π ∙ R) p"
  proof (rule subrelI)
    fix s t
    assume "(s, t) ∈ rstep_pos R p"
    then show "(s, t) ∈ rstep_pos (π ∙ R) p"
    proof (cases)
      fix l r σ
      assume "(l, r) ∈ R" and [simp]: "s |_ p = l ⋅ σ" "t = (ctxt_of_pos_term p s)⟨r ⋅ σ⟩"
        and p: "p ∈ poss s"
      then have "(π ∙ l, π ∙ r) ∈ π ∙ R" by simp
      from rstep_pos.intros [OF this p, of "sop (-π) ∘⇩s σ"]
        show "(s, t) ∈ rstep_pos (π ∙ R) p" by simp
    qed
  qed
qed

lemma rstep_pos_subset_permute_rstep_pos:
  "rstep_pos R p ⊆ π ∙ rstep_pos R p"
proof (rule subrelI)
  fix s t
  assume "(s, t) ∈ rstep_pos R p"
  then have "(s, t) ∈ rstep_pos (π ∙ R) p" by auto
  then show "(s, t) ∈ π ∙ rstep_pos R p"
  proof (cases)
    case (rule l r σ)
    then have p: "p ∈ poss (-π ∙ s)"
      and *: "- π ∙ s |_ p = -π ∙ l ⋅ sop π ∘⇩s σ ∘⇩s sop (-π)" by (auto simp: eqvt [symmetric])
    have "(l, r) ∈ π ∙ R" by fact
    then have "(π ∙ (-π) ∙ l, π ∙ (-π) ∙ r) ∈ π ∙ R" by simp+
    then have "(-π ∙ l, -π ∙ r) ∈ R" by simp
    from rstep_pos.intros [OF this p *] and p
      show ?thesis unfolding rule by (auto simp: eqvt [symmetric])
  qed
qed

lemma rstep_pos_eqvt [eqvt]:
  "π ∙ rstep_pos R p = rstep_pos (π ∙ R) p"
proof
  show "rstep_pos (π ∙ R) p ⊆ π ∙ rstep_pos R p"
    using rstep_pos_subset_permute_rstep_pos by simp
next
  from rstep_pos_subset_permute_rstep_pos [of R p "-π"]
    have "π ∙ rstep_pos R p ⊆ π ∙ -π ∙ rstep_pos R p" by (metis trs_pt.permute_set_subset)
  then show "π ∙ rstep_pos R p ⊆ rstep_pos (π ∙ R) p" by simp
qed

lemma perm_rstep_pos_conv [simp]:
  "π ∙ r ∈ rstep_pos R p ⟷ r ∈ rstep_pos R p"
  by (metis rstep_pos_eqvt rstep_pos_permute trs_pt.mem_permute_iff)

lemma is_partition_map_vars_term_permute [simp]:
  "is_partition (map (vars_term ∘ op ∙ π) xs) ⟷ is_partition (map vars_term xs)"
by (auto simp add: is_partition_def eqvt [symmetric])

lemma linear_term_permute [simp]:
  "linear_term (π ∙ t) ⟷ linear_term t"
by (induction t) (auto)

lemma ground_permute [simp]:
  "ground (π ∙ t) ⟷ ground t"
by (induction t) (auto)

lemma funas_term_permute [simp]:
  "funas_term (π ∙ t) = funas_term t"
by (induction t) (auto)

lemma in_NF_rstep_permute [simp]:
  "π ∙ t ∈ NF (rstep R) ⟷ t ∈ NF (rstep R)"
by (metis NF_instance term_variants_iff)

lemma Id_trs_eqvt [simp]: "π ∙ (Id :: ('f, 'v :: infinite) trs) = Id"
by (auto simp: inv_rule_mem_trs_simps [where p = π, symmetric])

lemma supteq_eqvt [simp]:
  fixes π :: "('v :: infinite) perm"
  shows "π ∙ {⊵} = {⊵}"
proof (intro equalityI subrelI)
  fix s t :: "('f, 'v) term" assume "(s, t) ∈ π ∙ {⊵}"
  then have "-π ∙ s ⊵ -π ∙ t" by auto
  then have "(-π ∙ s) ⋅ sop π ⊵ (-π ∙ t) ⋅ sop π" by (blast intro: supteq_subst)
  then show "s ⊵ t" by simp
next
  fix s t :: "('f, 'v) term" assume "s ⊵ t"
  from supteq_subst [OF this, of "sop (-π)"] show "(s, t) ∈ π ∙ {⊵}" by simp
qed

lemma supt_eqvt [simp]:
  "π ∙ {⊳} = {⊳}"
  by (simp add: supt_supteq_set_conv eqvt)



lemma mgu_imp_mgu_var_disjoint:
  fixes v⇩x v⇩y :: "'v::infinite ⇒ 'v" and s t :: "('f, 'v) term"
  assumes μ: "mgu s t = Some μ"
    and ren: "inj v⇩x" "inj v⇩y" "range v⇩x ∩ range v⇩y = {}"
    and disj: "V ∩ W = {}"
    and vars_term: "vars_term s ⊆ V" "vars_term t ⊆ W"
    and finite: "finite V" "finite W"
  shows "∃μ'.
    (∃π.
      (∀x ∈ V. μ x = (sop π⇩1 ∘⇩s (μ' ∘ v⇩x) ∘⇩s sop (-π)) x) ∧
      (∀x ∈ W. μ x = (sop π⇩2 ∘⇩s (μ' ∘ v⇩y) ∘⇩s sop (-π)) x)) ∧
    mgu ((π⇩1 ∙ s) ⋅ (Var ∘ v⇩x)) ((π⇩2 ∙ t) ⋅ (Var ∘ v⇩y)) = Some μ'" (is "∃μ'. _ ∧ mgu ?sv ?tv = _")
proof -
  define h where "h x = (if x ∈ V then v⇩x (Rep_perm π⇩1 x) else v⇩y (Rep_perm π⇩2 x))" for x
  have "inj_on h (V ∪ W)"
    using disj and ren(3)
    apply (unfold inj_on_def)
    apply (auto simp: h_def dest!: injD [OF ‹inj v⇩x›] injD [OF ‹inj v⇩y›] split: if_splits)
    apply (metis inv_Rep_perm_simp)+
    done
  from inj_on_imp_bij_betw [OF this] have "bij_betw h (V ∪ W) (h ` (V ∪ W))" .
  from bij_betw_extend [OF this subset_UNIV subset_UNIV]
    obtain f where "f ∈ perms" and f: "∀x ∈ V ∪ W. f x = h x"
    using finite by (auto simp: perms_def)
  define π and μ' where "π = Abs_perm f" and "μ' = sop (-π) ∘⇩s μ"
  have "finite (subst_domain μ)"
    using mgu_subst_domain [OF μ] and finite and vars_term by (auto intro: finite_subset)
  moreover have "{x. Rep_perm (- π) x ≠ x} = {x. Rep_perm π x ≠ x}"
    using ‹f ∈ perms›
    apply (auto simp: π_def perms_def)
    apply (metis inv_Rep_perm_simp permute_atom_def)+
    done
  moreover then have "finite (subst_domain (Var ∘ Rep_perm (- π)))"
    using ‹f ∈ perms› by (auto simp: subst_domain_def π_def Abs_perm_inverse perms_def)
  ultimately have finite: "finite (subst_domain μ')"
    by (auto simp: μ'_def subst_domain_subst_compose)

  let ?s = "π⇩1 ∙ s" and ?t = "π⇩2 ∙ t"

  have "?sv = s ⋅ sop π⇩1 ∘⇩s (Var ∘ v⇩x)" by simp
  also have "… = s ⋅ sop π"
    using f and ‹f ∈ perms› and vars_term and disj unfolding term_subst_eq_conv
    by (auto simp: π_def h_def Abs_perm_inverse subst_compose)
  finally have sv: "?sv = π ∙ s" by simp

  have "?tv = t ⋅ sop π⇩2 ∘⇩s (Var ∘ v⇩y)" by simp
  also have "… = t ⋅ sop π"
    using f and ‹f ∈ perms› and vars_term and disj unfolding term_subst_eq_conv
    apply (auto simp: π_def h_def Abs_perm_inverse subst_compose split: if_splits)
    by (metis Un_iff disjoint_iff_not_equal set_rev_mp)
  finally have tv: "?tv = π ∙ t" by simp

  have eq: "s ⋅ μ = t ⋅ μ" using mgu_sound [OF ‹mgu s t = Some μ›] by (auto simp: is_imgu_def)
  then have eq': "?sv ⋅ μ' = ?tv ⋅ μ'" by (simp add: sv tv μ'_def)

  then obtain μ'' where μ'': "mgu ?sv ?tv = Some μ''" using mgu_complete by (auto simp: unifiers_def)
  from mgu_sound [OF this] have eq'': "?sv ⋅ μ'' = ?tv ⋅ μ''"
    and mgu'': "is_mgu μ'' {(?sv, ?tv)}" by (auto simp: is_mgu_def is_imgu_def)

  { fix τ :: "('f, 'v) subst" assume *: "?sv ⋅ τ = ?tv ⋅ τ"
    then have "s ⋅ sop π ∘⇩s τ = t ⋅ sop π ∘⇩s τ" by (simp add: sv tv)
    with mgu_sound [OF μ, THEN is_imgu_imp_is_mgu] obtain δ where "sop π ∘⇩s τ = μ ∘⇩s δ"
      unfolding is_mgu_def unifiers_def by force
    then have "sop (-π) ∘⇩s sop π ∘⇩s τ = sop (-π) ∘⇩s μ ∘⇩s δ" by (auto simp: subst_compose_assoc)
    then have "τ = μ' ∘⇩s δ"
      by (auto simp: μ'_def subst_compose_def)
      (metis atom_pt.permute_minus_cancel(1) permute_atom_def)
    then have "∃γ. τ = μ' ∘⇩s γ" by blast }
  then have "is_mgu μ' {(?sv, ?tv)}" using eq' by (auto simp: is_mgu_def unifiers_def)
  with eq'' obtain γ where "μ'' = μ' ∘⇩s γ" by (auto simp: is_mgu_def unifiers_def)
  moreover obtain δ where "μ' = μ'' ∘⇩s δ" using eq' and mgu'' by (auto simp: is_mgu_def unifiers_def)
  ultimately obtain π' where *: "μ'' = π' ∙ μ'"
    using subst_variants_imp_perm [OF _ _ finite mgu_finite_subst_domain [OF μ''], of γ δ] by metis
  have "∀x ∈ V. μ x = (sop π⇩1 ∘⇩s (μ'' ∘ v⇩x) ∘⇩s sop (-π')) x"
    using f
    apply (auto simp: * μ'_def subst_compose_def permute_subst_def π_def h_def split: if_splits)
    by (metis Abs_perm_inverse Rep_perm_uminus Un_iff ‹f ∈ perms› bij_Rep_perm bij_is_inj inv_f_eq)
  moreover have "∀x ∈ W. μ x = (sop π⇩2 ∘⇩s (μ'' ∘ v⇩y) ∘⇩s sop (-π')) x"
    using f and disj
    apply (auto simp: * μ'_def subst_compose_def permute_subst_def π_def h_def split: if_splits)
    by (metis Abs_perm_inverse Rep_perm_uminus Un_iff ‹f ∈ perms› bij_Rep_perm bij_is_inj disjoint_iff_not_equal inv_f_eq)
  ultimately show ?thesis using μ'' by blast
qed

end