Theory Functional_Ordered_Resolution_Prover.IsaFoR_Term

(*  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)

interpretation substitution "(⋅)" "Var :: _  ('f, nat) term" "(∘s)"
proof unfold_locales
  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
  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

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_renamings "(⋅)" "Var :: _  ('f, nat) term" "(∘s)" renamings_apart "Fun undefined"
proof unfold_locales
  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
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) [])"

lemma mgu_sets_is_imgu:
  fixes AAA :: "('a :: compare, nat) term set set" and σ :: "('a, nat) subst"
  assumes fin: "finite AAA" "AA  AAA. finite AA" and "mgu_sets AAA = Some σ"
  shows "is_imgu σ AAA"
proof -
  have "Unifiers.is_imgu σ (set (Pairs AAA))"
    using assms unify_sound unfolding mgu_sets_def by blast
  thus ?thesis
    unfolding Unifiers.is_imgu_def is_imgu_def unifiers_Pairs[OF fin]
    by simp
qed

interpretation mgu "(⋅)" "Var :: _  ('f :: compare, nat) term" "(∘s)" renamings_apart
  "Fun undefined" mgu_sets
proof unfold_locales
  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 σ"
  thus "is_mgu σ AAA"
    using mgu_sets_is_imgu 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

interpretation imgu "(⋅)" "Var :: _  ('f :: compare, nat) term" "(∘s)" renamings_apart
  "Fun undefined" mgu_sets
proof unfold_locales
  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 σ"
  thus "is_imgu σ AAA"
    by (rule mgu_sets_is_imgu)
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 irreflp_def
      intro: asympI 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: asympI 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