Theory IsaFoR_Term

theory IsaFoR_Term
imports Derive Abstract_Substitution Unification Subsumption Wellorder_Extension Restricted_Predicates KBO
(*  Title:       Integration of IsaFoR Terms and the Knuth-Bendix Order
    Author:      Dmitriy Traytel <traytel at inf.ethz.ch>, 2014
    Author:      Anders Schlichtkrull <andschl at dtu.dk>, 2017
    Maintainer:  Anders Schlichtkrull <andschl at dtu.dk>
*)

section ‹Integration of \textsf{IsaFoR} Terms and the Knuth--Bendix Order›

text ‹
This theory implements the abstract interface for atoms and substitutions using
the \textsf{IsaFoR} library.
›

theory IsaFoR_Term
  imports
    Deriving.Derive
    Ordered_Resolution_Prover.Abstract_Substitution
    First_Order_Terms.Unification
    First_Order_Terms.Subsumption
    "HOL-Cardinals.Wellorder_Extension"
    Open_Induction.Restricted_Predicates
    Knuth_Bendix_Order.KBO
begin

hide_const (open) mgu

abbreviation subst_apply_literal ::
  "('f, 'v) term literal ⇒ ('f, 'v, 'w) gsubst ⇒ ('f, 'w) term literal" (infixl "⋅lit" 60) where
  "L ⋅lit σ ≡ map_literal (λA. A ⋅ σ) L"

definition subst_apply_clause ::
  "('f, 'v) term clause ⇒ ('f, 'v, 'w) gsubst ⇒ ('f, 'w) term clause" (infixl "⋅cls" 60) where
  "C ⋅cls σ = image_mset (λL. L ⋅lit σ) C"

abbreviation vars_lit :: "('f, 'v) term literal ⇒ 'v set" where
  "vars_lit L ≡ vars_term (atm_of L)"

definition vars_clause :: "('f, 'v) term clause ⇒ 'v set" where
  "vars_clause C = Union (set_mset (image_mset vars_lit C))"

definition vars_clause_list :: "('f, 'v) term clause list ⇒ 'v set" where
  "vars_clause_list Cs = Union (vars_clause ` set Cs) "

definition vars_partitioned :: "('f,'v) term clause list ⇒ bool" where
  "vars_partitioned Cs ⟷
   (∀i < length Cs. ∀j < length Cs. i ≠ j ⟶ (vars_clause (Cs ! i) ∩ vars_clause (Cs ! j)) = {})"

lemma vars_clause_mono: "S ⊆# C ⟹ vars_clause S ⊆ vars_clause C"
  unfolding vars_clause_def by auto

interpretation substitution_ops "(⋅)" Var "(∘s)" .

lemma is_ground_atm_is_ground_on_var:
  assumes "is_ground_atm (A ⋅ σ)" and "v ∈ vars_term A"
  shows "is_ground_atm (σ v)"
using assms proof (induction A)
  case (Var x)
  then show ?case by auto
next
  case (Fun f ts)
  then show ?case unfolding is_ground_atm_def
    by auto
qed

lemma is_ground_lit_is_ground_on_var:
  assumes ground_lit: "is_ground_lit (subst_lit L σ)" and v_in_L: "v ∈ vars_lit L"
  shows "is_ground_atm (σ v)"
proof -
  let ?A = "atm_of L"
  from v_in_L have A_p: "v ∈ vars_term ?A"
    by auto
  then have "is_ground_atm (?A ⋅ σ)"
    using ground_lit unfolding is_ground_lit_def by auto
  then show ?thesis
    using A_p is_ground_atm_is_ground_on_var by metis
qed

lemma is_ground_cls_is_ground_on_var:
  assumes
    ground_clause: "is_ground_cls (subst_cls C σ)" and
    v_in_C: "v ∈ vars_clause C"
  shows "is_ground_atm (σ v)"
proof -
  from v_in_C obtain L where L_p: "L ∈# C" "v ∈ vars_lit L"
    unfolding vars_clause_def by auto
  then have "is_ground_lit (subst_lit L σ)"
    using ground_clause unfolding is_ground_cls_def subst_cls_def by auto
  then show ?thesis
    using L_p is_ground_lit_is_ground_on_var by metis
qed

lemma is_ground_cls_list_is_ground_on_var:
  assumes ground_list: "is_ground_cls_list (subst_cls_list Cs σ)"
    and v_in_Cs: "v ∈ vars_clause_list Cs"
  shows "is_ground_atm (σ v)"
proof -
  from v_in_Cs obtain C where C_p: "C ∈ set Cs" "v ∈ vars_clause C"
    unfolding vars_clause_list_def by auto
  then have "is_ground_cls (subst_cls C σ)"
    using ground_list unfolding is_ground_cls_list_def subst_cls_list_def by auto
  then show ?thesis
    using C_p is_ground_cls_is_ground_on_var by metis
qed

lemma same_on_vars_lit:
  assumes "∀v ∈ vars_lit L. σ v = τ v"
  shows "subst_lit L σ = subst_lit L τ"
  using assms
proof (induction L)
  case (Pos x)
  then have "∀v ∈ vars_term x. σ v = τ v ⟹ subst_atm_abbrev x σ = subst_atm_abbrev x τ"
    using term_subst_eq by metis+
  then show ?case
    unfolding subst_lit_def using Pos by auto
next
  case (Neg x)
  then have "∀v ∈ vars_term x. σ v = τ v ⟹ subst_atm_abbrev x σ = subst_atm_abbrev x τ"
    using term_subst_eq by metis+
  then show ?case
    unfolding subst_lit_def using Neg by auto
qed

lemma in_list_of_mset_in_S:
  assumes "i < length (list_of_mset S)"
  shows "list_of_mset S ! i ∈# S"
proof -
  from assms have "list_of_mset S ! i ∈ set (list_of_mset S)"
    by auto
  then have "list_of_mset S ! i ∈# mset (list_of_mset S)"
    by (meson in_multiset_in_set)
  then show ?thesis
    by auto
qed

lemma same_on_vars_clause:
  assumes "∀v ∈ vars_clause S. σ v = τ v"
  shows "subst_cls S σ = subst_cls S τ"
  by (smt assms image_eqI image_mset_cong2 mem_simps(9) same_on_vars_lit set_image_mset
      subst_cls_def vars_clause_def)

lemma vars_partitioned_var_disjoint:
  assumes "vars_partitioned Cs"
  shows "var_disjoint Cs"
  unfolding var_disjoint_def
proof (intro allI impI)
  fix σs :: ‹('b ⇒ ('a, 'b) term) list›
  assume "length σs = length Cs"
  with assms[unfolded vars_partitioned_def] Fun_More.fun_merge[of "map vars_clause Cs" "nth σs"]
  obtain σ where
    σ_p: "∀i < length (map vars_clause Cs). ∀x ∈ map vars_clause Cs ! i. σ x = (σs ! i) x"
    by auto
  have "∀i < length Cs. ∀S. S ⊆# Cs ! i ⟶ subst_cls S (σs ! i) = subst_cls S σ"
  proof (rule, rule, rule, rule)
    fix i :: nat and S :: "('a, 'b) term literal multiset"
    assume
      "i < length Cs" and
      "S ⊆# Cs ! i"
    then have "∀v ∈ vars_clause S. (σs ! i) v = σ v"
      using vars_clause_mono[of S "Cs ! i"] σ_p by auto
    then show "subst_cls S (σs ! i) = subst_cls S σ"
      using same_on_vars_clause by auto
  qed
  then show "∃τ. ∀i<length Cs. ∀S. S ⊆# Cs ! i ⟶ subst_cls S (σs ! i) = subst_cls S τ"
    by auto
qed

lemma vars_in_instance_in_range_term:
  "vars_term (subst_atm_abbrev A σ) ⊆ Union (image vars_term (range σ))"
  by (induction A) auto

lemma vars_in_instance_in_range_lit: "vars_lit (subst_lit L σ) ⊆ Union (image vars_term (range σ))"
proof (induction L)
  case (Pos A)
  have "vars_term (A ⋅ σ) ⊆ Union (image vars_term (range σ))"
    using vars_in_instance_in_range_term[of A σ] by blast
  then show ?case by auto
next
  case (Neg A)
  have "vars_term (A ⋅ σ) ⊆ Union (image vars_term (range σ))"
    using vars_in_instance_in_range_term[of A σ] by blast
  then show ?case by auto
qed

lemma vars_in_instance_in_range_cls:
  "vars_clause (subst_cls C σ) ⊆ Union (image vars_term (range σ))"
  unfolding vars_clause_def subst_cls_def using vars_in_instance_in_range_lit[of _ σ] by auto

primrec renamings_apart :: "('f, nat) term clause list ⇒ (('f, nat) subst) list" where
  "renamings_apart [] = []"
| "renamings_apart (C # Cs) =
   (let σs = renamings_apart Cs in
      (λv. Var (v + Max (vars_clause_list (subst_cls_lists Cs σs) ∪ {0}) + 1)) # σs)"

definition var_map_of_subst :: "('f, nat) subst ⇒ nat ⇒ nat" where
  "var_map_of_subst σ v = the_Var (σ v)"

lemma len_renamings_apart: "length (renamings_apart Cs) = length Cs"
  by (induction Cs) (auto simp: Let_def)

lemma renamings_apart_is_Var: "∀σ ∈ set (renamings_apart Cs). ∀x. is_Var (σ x)"
  by (induction Cs) (auto simp: Let_def)

lemma renamings_apart_inj: "∀σ ∈ set (renamings_apart Cs). inj σ"
proof (induction Cs)
  case (Cons a Cs)
  then have "inj (λv. Var (Suc (v + Max (vars_clause_list
               (subst_cls_lists Cs (renamings_apart Cs)) ∪ {0}))))"
    by (meson add_right_imp_eq injI nat.inject term.inject(1))
  then show ?case
    using Cons by (auto simp: Let_def)
qed auto

lemma finite_vars_clause[simp]: "finite (vars_clause x)"
  unfolding vars_clause_def by auto

lemma finite_vars_clause_list[simp]: "finite (vars_clause_list Cs)"
  unfolding vars_clause_list_def by (induction Cs) auto

lemma Suc_Max_notin_set: "finite X ⟹ Suc (v + Max (insert 0 X)) ∉ X"
  by (metis Max.boundedE Suc_n_not_le_n empty_iff finite.insertI le_add2 vimageE vimageI
      vimage_Suc_insert_0)

lemma vars_partitioned_Nil[simp]: "vars_partitioned []"
  unfolding vars_partitioned_def by auto

lemma subst_cls_lists_Nil[simp]: "subst_cls_lists Cs [] = []"
  unfolding subst_cls_lists_def by auto

lemma vars_clause_hd_partitioned_from_tl:
  assumes "Cs ≠[]"
  shows "vars_clause (hd (subst_cls_lists Cs (renamings_apart Cs)))
    ∩ vars_clause_list (tl (subst_cls_lists Cs (renamings_apart Cs))) = {}"
  using assms
proof (induction Cs)
  case (Cons C Cs)
  define σ' :: "nat ⇒ nat"
    where "σ' = (λv. (Suc (v + Max ((vars_clause_list (subst_cls_lists Cs
                        (renamings_apart Cs))) ∪ {0}))))"
  define σ :: "nat ⇒ ('a, nat) term"
    where "σ = (λv. Var (σ' v))"

  have "vars_clause (subst_cls C σ) ⊆ ⋃ (vars_term ` range σ)"
    using vars_in_instance_in_range_cls[of C "hd (renamings_apart (C # Cs))"] σ_def σ'_def
    by (auto simp: Let_def)
  moreover have "⋃ (vars_term ` range σ)
    ∩ vars_clause_list (subst_cls_lists Cs (renamings_apart Cs)) = {}"
  proof -
    have "range σ' ∩ vars_clause_list (subst_cls_lists Cs (renamings_apart Cs)) = {}"
      unfolding σ'_def using Suc_Max_notin_set by auto
    then show ?thesis
      unfolding σ_def σ'_def by auto
  qed
  ultimately have "vars_clause (subst_cls C σ)
     ∩ vars_clause_list (subst_cls_lists Cs (renamings_apart Cs)) = {}"
    by auto
  then show ?case
    unfolding σ_def σ'_def unfolding subst_cls_lists_def
    by (simp add: Let_def subst_cls_lists_def)
qed auto

lemma vars_partitioned_renamings_apart: "vars_partitioned (subst_cls_lists Cs (renamings_apart Cs))"
proof (induction Cs)
  case (Cons C Cs)
  {
    fix i :: nat and j :: nat
    assume ij:
      "i < Suc (length Cs)"
      "j < i"
    have "vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) ∩
        vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) =
        {}"
    proof (cases i; cases j)
      fix j' :: nat
      assume i'j':
        "i = 0"
        "j = Suc j'"
      then show "vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) ∩
        vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) =
        {}"
        using ij by auto
    next
      fix i' :: nat
      assume i'j':
        "i = Suc i'"
        "j = 0"
      have disjoin_C_Cs: "vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! 0) ∩
        vars_clause_list ((subst_cls_lists Cs (renamings_apart Cs))) = {}"
        using vars_clause_hd_partitioned_from_tl[of "C # Cs"]
        by (simp add: Let_def subst_cls_lists_def)
      {
        fix x
        assume asm: "x ∈ vars_clause (subst_cls_lists Cs (renamings_apart Cs) ! i')"
        then have "(subst_cls_lists Cs (renamings_apart Cs) ! i')
          ∈ set (subst_cls_lists Cs (renamings_apart Cs))"
          using i'j' ij unfolding subst_cls_lists_def
          by (metis Suc_less_SucD length_map len_renamings_apart length_zip min_less_iff_conj
              nth_mem)
        moreover from asm have
          "x ∈ vars_clause (subst_cls_lists Cs (renamings_apart Cs) ! i')"
          using i'j' ij
          unfolding subst_cls_lists_def by simp
        ultimately have "∃D ∈ set (subst_cls_lists Cs (renamings_apart Cs)). x ∈ vars_clause D"
            by auto
      }
      then have "vars_clause (subst_cls_lists Cs (renamings_apart Cs) ! i')
        ⊆ Union (set (map vars_clause ((subst_cls_lists Cs (renamings_apart Cs)))))"
        by auto
      then have "vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! 0) ∩
        vars_clause (subst_cls_lists Cs (renamings_apart Cs) ! i') =
        {}" using disjoin_C_Cs unfolding vars_clause_list_def by auto
      moreover
      have "subst_cls_lists Cs (renamings_apart Cs) ! i' =
        subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i"
        using i'j' ij unfolding subst_cls_lists_def by (simp add: Let_def)
      ultimately
      show "vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) ∩
        vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) =
        {}"
        using i'j' by (simp add: Int_commute)
    next
      fix i' :: nat and j' :: nat
      assume i'j':
        "i = Suc i'"
        "j = Suc j'"
      have "i'<length (subst_cls_lists Cs (renamings_apart Cs))"
        using ij i'j' unfolding subst_cls_lists_def by (auto simp: len_renamings_apart)
      moreover
      have "j'<length (subst_cls_lists Cs (renamings_apart Cs))"
        using ij i'j' unfolding subst_cls_lists_def by (auto simp: len_renamings_apart)
      moreover
      have "i' ≠ j'"
        using ‹i = Suc i'› ‹j = Suc j'› ij by blast
      ultimately
      have "vars_clause (subst_cls_lists Cs (renamings_apart Cs) ! i') ∩
          vars_clause (subst_cls_lists Cs (renamings_apart Cs) ! j') =
          {}"
        using Cons unfolding vars_partitioned_def by auto
      then show "vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) ∩
        vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) =
        {}"
        unfolding i'j'
        by (simp add: subst_cls_lists_def Let_def)
    next
      assume
        ‹i = 0› and
        ‹j = 0›
      then show ‹vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) ∩
        vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) =
        {}› using ij by auto
    qed
  }
  then show ?case
    unfolding vars_partitioned_def
    by (metis (no_types, lifting) Int_commute Suc_lessI len_renamings_apart length_map
        length_nth_simps(2) length_zip min.idem nat.inject not_less_eq subst_cls_lists_def)
qed auto

interpretation substitution "(⋅)" "Var :: _ ⇒ ('f, nat) term" "(∘s)" renamings_apart "Fun undefined"
proof (standard)
  show "⋀A. A ⋅ Var = A"
    by auto
next
  show "⋀A τ σ. A ⋅ τ ∘s σ = A ⋅ τ ⋅ σ"
    by auto
next
  show "⋀σ τ. (⋀A. A ⋅ σ = A ⋅ τ) ⟹ σ = τ"
    by (simp add: subst_term_eqI)
next
  fix C :: "('f, nat) term clause"
  fix σ
  assume "is_ground_cls (subst_cls C σ)"
  then have ground_atms_σ: "⋀v. v ∈ vars_clause C ⟹ is_ground_atm (σ v)"
    by (meson is_ground_cls_is_ground_on_var)

  define some_ground_trm :: "('f, nat) term" where "some_ground_trm = (Fun undefined [])"
  have ground_trm: "is_ground_atm some_ground_trm"
    unfolding is_ground_atm_def some_ground_trm_def by auto
  define τ where "τ = (λv. if v ∈ vars_clause C then σ v else some_ground_trm)"
  then have τ_σ: "∀v ∈ vars_clause C. σ v = τ v"
    unfolding τ_def by auto

  have all_ground_τ: "is_ground_atm (τ v)" for v
  proof (cases "v ∈ vars_clause C")
    case True
    then show ?thesis
      using ground_atms_σ τ_σ by auto
  next
    case False
    then show ?thesis
      unfolding τ_def using ground_trm by auto
  qed
  have "is_ground_subst τ"
    unfolding is_ground_subst_def
  proof
    fix A
    show "is_ground_atm (subst_atm_abbrev A τ)"
    proof (induction A)
      case (Var v)
      then show ?case using all_ground_τ by auto
    next
      case (Fun f As)
      then show ?case using all_ground_τ
        by (simp add: is_ground_atm_def)
    qed
  qed
  moreover have "∀v ∈ vars_clause C. σ v = τ v"
    using τ_σ unfolding vars_clause_list_def
    by blast
  then have "subst_cls C σ = subst_cls C τ"
    using same_on_vars_clause by auto
  ultimately show "∃τ. is_ground_subst τ ∧ subst_cls C τ = subst_cls C σ"
    by auto
next
  fix Cs :: "('f, nat) term clause list"
  show "length (renamings_apart Cs) = length Cs"
    using len_renamings_apart by auto
next
  fix Cs :: "('f, nat) term clause list"
  fix ρ ::  "nat ⇒ ('f, nat) Term.term"
  assume ρ_renaming: "ρ ∈ set (renamings_apart Cs)"
  {
    have inj_is_renaming:
      "⋀σ :: ('f, nat) subst. (⋀x. is_Var (σ x)) ⟹ inj σ ⟹ is_renaming σ"
    proof -
      fix σ :: "('f, nat) subst"
      fix x
      assume is_var_σ: "⋀x. is_Var (σ x)"
      assume inj_σ: "inj σ"
      define σ' where "σ' = var_map_of_subst σ"
      have σ: "σ = Var ∘ σ'"
        unfolding σ'_def var_map_of_subst_def using is_var_σ by auto

      from is_var_σ inj_σ have "inj σ'"
        unfolding is_renaming_def unfolding subst_domain_def inj_on_def σ'_def var_map_of_subst_def
         by (metis term.collapse(1))
      then have "inv σ' ∘ σ' = id"
        using inv_o_cancel[of σ'] by simp
      then have "Var ∘ (inv σ' ∘ σ') = Var"
        by simp
      then have "∀x. (Var ∘ (inv σ' ∘ σ')) x = Var x"
        by metis
      then have "∀x. ((Var ∘ σ') ∘s (Var ∘ (inv σ'))) x = Var x"
        unfolding subst_compose_def by auto
      then have "σ ∘s (Var ∘ (inv σ')) = Var"
        using σ by auto
      then show "is_renaming σ"
        unfolding is_renaming_def by blast
    qed
    then have "∀σ ∈ (set (renamings_apart Cs)). is_renaming σ"
      using renamings_apart_is_Var renamings_apart_inj by blast
  }
  then show "is_renaming ρ"
    using ρ_renaming by auto
next
  fix Cs :: "('f, nat) term clause list"
  have "vars_partitioned (subst_cls_lists Cs (renamings_apart Cs))"
    using vars_partitioned_renamings_apart by auto
  then show "var_disjoint (subst_cls_lists Cs (renamings_apart Cs))"
    using vars_partitioned_var_disjoint by auto
next
  show "⋀σ As Bs. Fun undefined As ⋅ σ = Fun undefined Bs ⟷ map (λA. A ⋅ σ) As = Bs"
    by simp
next
  show "wfP (strictly_generalizes_atm :: ('f, 'v) term ⇒ _ ⇒ _)"
    unfolding wfP_def
    by (rule wf_subset[OF wf_subsumes])
      (auto simp: strictly_generalizes_atm_def generalizes_atm_def term_subsumable.subsumes_def
        subsumeseq_term.simps)
qed

fun pairs :: "'a list ⇒ ('a × 'a) list" where
  "pairs (x # y # xs) = (x, y) # pairs (y # xs)" |
  "pairs _ = []"

derive compare "term"
derive compare "literal"

lemma class_linorder_compare: "class.linorder (le_of_comp compare) (lt_of_comp compare)"
  apply standard
      apply (simp_all add: lt_of_comp_def le_of_comp_def split: order.splits)
     apply (metis comparator.sym comparator_compare invert_order.simps(1) order.distinct(5))
    apply (metis comparator_compare comparator_def order.distinct(5))
   apply (metis comparator.sym comparator_compare invert_order.simps(1) order.distinct(5))
  by (metis comparator.sym comparator_compare invert_order.simps(2) order.distinct(5))

context begin
interpretation compare_linorder: linorder
  "le_of_comp compare"
  "lt_of_comp compare"
  by (rule class_linorder_compare)

definition Pairs where
  "Pairs AAA = concat (compare_linorder.sorted_list_of_set
     ((pairs ∘ compare_linorder.sorted_list_of_set) ` AAA))"

lemma unifies_all_pairs_iff:
  "(∀p ∈ set (pairs xs). fst p ⋅ σ = snd p ⋅ σ) ⟷ (∀a ∈ set xs. ∀b ∈ set xs. a ⋅ σ = b ⋅ σ)"
proof (induct xs rule: pairs.induct)
  case (1 x y xs)
  then show ?case
    unfolding pairs.simps list.set ball_Un ball_simps simp_thms fst_conv snd_conv by metis
qed simp_all

lemma in_pair_in_set:
  assumes "(A,B) ∈ set ((pairs As))"
  shows "A ∈ set As ∧ B ∈ set As"
  using assms
proof (induction As)
  case (Cons A As)
  note Cons_outer = this
  show ?case
  proof (cases As)
    case Nil
    then show ?thesis
      using Cons_outer by auto
  next
    case (Cons B As')
    then show ?thesis using Cons_outer by auto
  qed
qed auto

lemma in_pairs_sorted_list_of_set_in_set:
  assumes
    "finite AAA"
    "∀AA ∈ AAA. finite AA"
    "AB_pairs ∈ (pairs ∘ compare_linorder.sorted_list_of_set) ` AAA" and
    "(A :: _ :: compare, B) ∈ set AB_pairs"
  shows "∃AA. AA ∈ AAA ∧ A ∈ AA ∧ B ∈ AA"
proof -
  from assms have "AB_pairs ∈ (pairs ∘ compare_linorder.sorted_list_of_set) ` AAA"
    by auto
  then obtain AA where
    AA_p: "AA ∈ AAA ∧ (pairs ∘ compare_linorder.sorted_list_of_set) AA = AB_pairs"
    by auto
  have "(A, B) ∈ set (pairs (compare_linorder.sorted_list_of_set AA))"
    using AA_p[] assms(4) by auto
  then have "A ∈ set (compare_linorder.sorted_list_of_set AA)" and
    "B ∈ set (compare_linorder.sorted_list_of_set AA)"
    using in_pair_in_set[of A] by auto
  then show ?thesis
    using assms(2) AA_p by auto
qed

lemma unifiers_Pairs:
  assumes
    "finite AAA" and
    "∀AA ∈ AAA. finite AA"
  shows "unifiers (set (Pairs AAA)) = {σ. is_unifiers σ AAA}"
proof (rule; rule)
  fix σ :: "('a, 'b) subst"
  assume asm: "σ ∈ unifiers (set (Pairs AAA))"
  have "⋀AA. AA ∈ AAA ⟹ card (AA ⋅set σ) ≤ Suc 0"
  proof -
    fix AA :: "('a, 'b) term set"
    assume asm': "AA ∈ AAA"
    then have "∀p ∈ set (pairs (compare_linorder.sorted_list_of_set AA)).
      subst_atm_abbrev (fst p) σ = subst_atm_abbrev (snd p) σ"
      using assms asm unfolding Pairs_def by auto
    then have "∀A ∈ AA. ∀B ∈ AA. subst_atm_abbrev A σ = subst_atm_abbrev B σ"
      using assms asm' unfolding unifies_all_pairs_iff
      using compare_linorder.sorted_list_of_set by blast
    then show "card (AA ⋅set σ) ≤ Suc 0"
      by (smt imageE card.empty card_Suc_eq card_mono finite.intros(1) finite_insert le_SucI
           singletonI subsetI)
  qed
  then show "σ ∈ {σ. is_unifiers σ AAA}"
    using assms by (auto simp: is_unifiers_def is_unifier_def subst_atms_def)
next
  fix σ :: "('a, 'b) subst"
  assume asm: "σ ∈ {σ. is_unifiers σ AAA}"

  {
    fix AB_pairs A B
    assume
      "AB_pairs ∈ set (compare_linorder.sorted_list_of_set
         ((pairs ∘ compare_linorder.sorted_list_of_set) ` AAA))" and
      "(A, B) ∈ set AB_pairs"
    then have "∃AA. AA ∈ AAA ∧ A ∈ AA ∧ B ∈ AA"
      using assms by (simp add: in_pairs_sorted_list_of_set_in_set)
    then obtain AA where
     a: "AA ∈ AAA" "A ∈ AA" "B ∈ AA"
      by blast
    from a assms asm have card_AA_σ: "card (AA ⋅set σ) ≤ Suc 0"
      unfolding is_unifiers_def is_unifier_def subst_atms_def by auto
    have "subst_atm_abbrev A σ = subst_atm_abbrev B σ"
    proof (cases "card (AA ⋅set σ) = Suc 0")
      case True
      moreover
      have "subst_atm_abbrev A σ ∈ AA ⋅set σ"
        using a assms asm card_AA_σ by auto
      moreover
      have "subst_atm_abbrev B σ ∈ AA ⋅set σ"
        using a assms asm card_AA_σ by auto
      ultimately
      show ?thesis
        using a assms asm card_AA_σ by (metis (no_types, lifting) card_Suc_eq singletonD)
    next
      case False
      then have "card (AA ⋅set σ) = 0"
        using a assms asm card_AA_σ
        by arith
      then show ?thesis
        using a assms asm card_AA_σ by auto
    qed
  }
  then show "σ ∈ unifiers (set (Pairs AAA))"
    unfolding Pairs_def unifiers_def by auto
qed

end

definition "mgu_sets AAA = map_option subst_of (unify (Pairs AAA) [])"

interpretation mgu "(⋅)" "Var :: _ ⇒ ('f :: compare, nat) term" "(∘s)" "Fun undefined"
  renamings_apart mgu_sets
proof
  fix AAA :: "('a :: compare, nat) term set set" and σ :: "('a, nat) subst"
  assume fin: "finite AAA" "∀AA ∈ AAA. finite AA" and "mgu_sets AAA = Some σ"
  then have "is_imgu σ (set (Pairs AAA))"
    using unify_sound unfolding mgu_sets_def by blast
  then show "is_mgu σ AAA"
    unfolding is_imgu_def is_mgu_def unifiers_Pairs[OF fin] by auto
next
  fix AAA :: "('a :: compare, nat) term set set" and σ :: "('a, nat) subst"
  assume fin: "finite AAA" "∀AA ∈ AAA. finite AA" and "is_unifiers σ AAA"
  then have "σ ∈ unifiers (set (Pairs AAA))"
    unfolding is_mgu_def unifiers_Pairs[OF fin] by auto
  then show "∃τ. mgu_sets AAA = Some τ"
    using unify_complete unfolding mgu_sets_def by blast
qed

derive linorder prod
derive linorder list

text ‹
This part extends and integrates and the Knuth--Bendix order defined in
\textsf{IsaFoR}.
›

record 'f weights =
  w :: "'f × nat ⇒ nat"
  w0 :: nat
  pr_strict :: "'f × nat ⇒ 'f × nat ⇒ bool"
  least :: "'f ⇒ bool"
  scf :: "'f × nat ⇒ nat ⇒ nat"

class weighted =
  fixes weights :: "'a weights"
  assumes weights_adm:
    "admissible_kbo
       (w weights) (w0 weights) (pr_strict weights) ((pr_strict weights)==) (least weights) (scf weights)"
  and pr_strict_total: "fi = gj ∨ pr_strict weights fi gj ∨ pr_strict weights gj fi"
  and pr_strict_asymp: "asymp (pr_strict weights)"
  and scf_ok: "i < n ⟹ scf weights (f, n) i ≤ 1"

instantiation unit :: weighted begin

definition weights_unit :: "unit weights" where "weights_unit =
  ⦇w = Suc ∘ snd, w0 = 1, pr_strict = λ(_, n) (_, m). n > m, least = λ_. True, scf = λ_ _. 1⦈"

instance
  by (intro_classes, unfold_locales) (auto simp: weights_unit_def SN_iff_wf asymp.simps irreflp_def
      intro!: wf_subset[OF wf_inv_image[OF wf], of _ snd])
end

global_interpretation KBO:
  admissible_kbo
    "w (weights :: 'f :: weighted weights)" "w0 (weights :: 'f :: weighted weights)"
    "pr_strict weights" "((pr_strict weights)==)" "least weights" "scf weights"
    defines weight = KBO.weight
    and kbo = KBO.kbo
  by (simp add: weights_adm)

lemma kbo_code[code]: "kbo s t =
  (let wt = weight t; ws = weight s in
  if vars_term_ms (KBO.SCF t) ⊆# vars_term_ms (KBO.SCF s) ∧ wt ≤ ws
  then
    (if wt < ws then (True, True)
    else
      (case s of
        Var y ⇒ (False, case t of Var x ⇒ True | Fun g ts ⇒ ts = [] ∧ least weights g)
      | Fun f ss ⇒
          (case t of
            Var x ⇒ (True, True)
          | Fun g ts ⇒
              if pr_strict weights (f, length ss) (g, length ts) then (True, True)
              else if (f, length ss) = (g, length ts) then lex_ext_unbounded kbo ss ts
              else (False, False))))
  else (False, False))"
  by (subst KBO.kbo.simps) (auto simp: Let_def split: term.splits)

definition "less_kbo s t = fst (kbo t s)"

lemma less_kbo_gtotal: "ground s ⟹ ground t ⟹ s = t ∨ less_kbo s t ∨ less_kbo t s"
  unfolding less_kbo_def using KBO.S_ground_total by (metis pr_strict_total subset_UNIV)

lemma less_kbo_subst:
  fixes σ :: "('f :: weighted, 'v) subst"
  shows "less_kbo s t ⟹ less_kbo (s ⋅ σ) (t ⋅ σ)"
  unfolding less_kbo_def by (rule KBO.S_subst)

lemma wfP_less_kbo: "wfP less_kbo"
proof -
  have "SN {(x, y). fst (kbo x y)}"
    using pr_strict_asymp by (fastforce simp: asymp.simps irreflp_def intro!: KBO.S_SN scf_ok)
  then show ?thesis
    unfolding SN_iff_wf wfP_def by (rule wf_subset) (auto simp: less_kbo_def)
qed

instantiation "term" :: (weighted, type) linorder begin

definition "leq_term = (SOME leq. {(s,t). less_kbo s t} ⊆ leq ∧ Well_order leq ∧ Field leq = UNIV)"

lemma less_trm_extension: "{(s,t). less_kbo s t} ⊆ leq_term"
  unfolding leq_term_def
  by (rule someI2_ex[OF total_well_order_extension[OF wfP_less_kbo[unfolded wfP_def]]]) auto

lemma less_trm_well_order: "well_order leq_term"
  unfolding leq_term_def
  by (rule someI2_ex[OF total_well_order_extension[OF wfP_less_kbo[unfolded wfP_def]]]) auto

definition less_eq_term :: "('a :: weighted, 'b) term ⇒ _ ⇒ bool" where
  "less_eq_term = in_rel leq_term"
definition less_term :: "('a :: weighted, 'b) term ⇒ _ ⇒ bool" where
  "less_term s t = strict (≤) s t"

lemma leq_term_minus_Id: "leq_term - Id = {(x,y). x < y}"
  using less_trm_well_order
  unfolding well_order_on_def linear_order_on_def partial_order_on_def antisym_def less_term_def less_eq_term_def
  by auto

lemma less_term_alt: "(<) = in_rel (leq_term - Id)"
  by (simp add: in_rel_Collect_case_prod_eq leq_term_minus_Id)

instance
proof (standard, goal_cases less_less_eq refl trans antisym total)
  case (less_less_eq x y)
  then show ?case unfolding less_term_def ..
next
case (refl x)
  then show ?case using less_trm_well_order
    unfolding well_order_on_def linear_order_on_def partial_order_on_def preorder_on_def refl_on_def
      less_eq_term_def by auto
next
case (trans x y z)
  then show ?case using less_trm_well_order
    unfolding well_order_on_def linear_order_on_def partial_order_on_def preorder_on_def trans_def
      less_eq_term_def by auto
next
  case (antisym x y)
  then show ?case using less_trm_well_order
    unfolding well_order_on_def linear_order_on_def partial_order_on_def antisym_def
      less_eq_term_def by auto
next
  case (total x y)
  then show ?case using less_trm_well_order
    unfolding well_order_on_def linear_order_on_def partial_order_on_def preorder_on_def refl_on_def
      Relation.total_on_def less_eq_term_def by (cases "x = y") auto
qed

end

instantiation "term" :: (weighted, type) wellorder begin
instance
  using less_trm_well_order[unfolded well_order_on_def wf_def leq_term_minus_Id, THEN conjunct2]
  by intro_classes (atomize, auto)
end

lemma ground_less_less_kbo: "ground s ⟹ ground t ⟹ s < t ⟹ less_kbo s t"
  using less_kbo_gtotal[of s t] less_trm_extension
  by (auto simp: less_term_def less_eq_term_def)

lemma less_kbo_less: "less_kbo s t ⟹ s < t"
  using less_trm_extension
  by (auto simp: less_term_alt less_kbo_def KBO.S_irrefl)

lemma is_ground_atm_ground: "is_ground_atm t ⟷ ground t"
  unfolding is_ground_atm_def
  by (induct t) (fastforce simp: in_set_conv_nth list_eq_iff_nth_eq)+

end