Theory First_Order_Clause.IsaFoR_KBO

(* TODO: 
   Beginning taken from "Functional_Ordered_Resolution_Prover.IsaFoR_Term"
   Try to rename Name clash, such that a copy is not needed *)
theory IsaFoR_KBO
  imports
    Knuth_Bendix_Order.KBO
    
    VeriComp.Well_founded

    IsaFoR_Nonground_Clause_With_Equality
    IsaFoR_Nonground_Context
    Nonground_Order_With_Equality

    (* TODO: Find out why this needs to be imported here already to have available for KBO *)
    Selection_Function_Select_Max
begin

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!: 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: "Term.ground s ⟹ Term.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

subsection‹Setup weights for nat›

abbreviation pr_strict :: "('f :: wellorder × nat) ⇒ _ ⇒ bool" where
  "pr_strict ≡ lex_prodp ((<) :: 'f ⇒ 'f ⇒ bool) ((<) :: nat ⇒ nat ⇒ bool)"

lemma wfp_pr_strict: "wfp pr_strict"
  by (simp add: lex_prodp_wfP)

abbreviation least where
  "least x ≡ ∀y. x ≤ y"

abbreviation weights where 
  "weights ≡ ⦇w =  λ_. 1, w0 = 1, pr_strict = pr_strict¯¯, least = least, scf = λ_ _. 1⦈"

instantiation nat :: weighted begin

definition weights_nat :: "nat weights" where
  "weights_nat ≡ weights"

instance
proof -

  have "SN {(fn  :: nat × nat, gm). fst gm < fst fn ∨ fst gm = fst fn ∧ snd gm < snd fn}"
  proof (fold lex_prodp_def, rule wf_imp_SN)
  
    show "wf ({(fn, gm). pr_strict gm fn}¯)"
      using wfp_pr_strict
      by (simp add: converse_def wfp_def)
  qed

  then show "OFCLASS(nat, weighted_class)"
    by (intro_classes, unfold weights_nat_def lex_prodp_def admissible_kbo_def) 
       (auto simp: order.order_iff_strict)
qed

end

subsection‹Interpret non-ground order with KBO›

interpretation KBO: context_compatible_nonground_order where
  lesst = "less_kbo :: ('f :: weighted,'v) term ⇒ ('f,'v) term ⇒ bool" and
  comp_subst = "(∘s)" and Var = Var and term_subst = "(⋅)" and term_vars = term.vars and
  compose_context = "(∘c)" and term_from_ground = term.from_ground and
  term_to_ground = term.to_ground and map_context = map_args_actxt and
  to_ground_context_map = map_args_actxt and from_ground_context_map = map_args_actxt and
  context_to_set = set2_actxt and hole = □ and apply_context = ctxt_apply_term and 
  occurences = occurences and ground_hole = □ and apply_ground_context = apply_ground_context and
  compose_ground_context = "(∘c)" and ground_context_map = map_args_actxt and
  ground_context_to_set = set2_actxt 
proof unfold_locales
   show "transp less_kbo"
    using KBO.S_trans
    unfolding transp_def less_kbo_def
    by blast
next
  show "asymp less_kbo"
    using wfp_imp_asymp wfP_less_kbo
    by blast
next
  show "wfp_on (range term.from_ground) less_kbo"
    using wfp_on_subset[OF wfP_less_kbo subset_UNIV] .
next
  show "totalp_on (range term.from_ground) less_kbo"
    using less_kbo_gtotal
    unfolding totalp_on_def Term.ground_vars_term_empty term.is_ground_iff_range_from_ground
    by blast
next
  fix
    c :: "('f, 'v) context" and
    t1 t2 :: "('f, 'v) term"
 
  assume "less_kbo t1 t2"

  then show "less_kbo c⟨t1⟩ c⟨t2⟩"
    unfolding less_kbo_def
    by (rule KBO.S_ctxt)
next
  fix
    t1 t2 :: "('f, 'v) term" and
    γ :: "('f, 'v) subst"

  assume "less_kbo t1 t2"

  then show "less_kbo (t1 ⋅ γ) (t2 ⋅ γ)"
    by (rule less_kbo_subst)
next
  fix t and c :: "('f, 'v) context"
  assume "c ≠ □"

  then show "less_kbo t c⟨t⟩"
    unfolding less_kbo_def
    by (intro KBO.S_supt nectxt_imp_supt_ctxt)
qed

end