Theory KBO_Impl

(*
Author:  Christian Sternagel <c.sternagel@gmail.com> (2012-2015)
Author:  René Thiemann <rene.thiemann@uibk.ac.at> (2012-2015)
License: LGPL (see file COPYING.LESSER)
*)
theory KBO_Impl
imports
  KBO_More
  "Check-NT.Term_Order_Impl"
  Reduction_Order_Impl
  QTRS.Term_Impl
  "../Auxiliaries/Multiset_Code"
  QTRS.Map_Choice
begin

(* in the implementation, the precedence is determined by a mapping into naturals (0 has least prec.) *)
locale weight_fun_nat_prc =
  fixes w :: "'f × nat ⇒ nat"
  and w0 :: nat
  and prc :: "'f × nat ⇒ 'f × nat ⇒ bool × bool"
  and least :: "'f ⇒ bool"
  and scf :: "'f × nat ⇒ nat ⇒ nat"

sublocale weight_fun_nat_prc ⊆ kbo w w0 scf least "λ fn gm. fst (prc fn gm)" "λ fn gm. snd (prc fn gm)" .

context weight_fun_nat_prc
begin

definition kbo_impl where "kbo_impl ≡ kbo"

(* main difference to kbo from KBO.thy:
  - only one invocation of precedence function for two symbols 
*)
lemma kbo_impl: 
  "kbo_impl s t = (let wt = weight t; ws = weight s in if (vars_term_ms (SCF t) ⊆# vars_term_ms (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 g)) 
    | Fun f ss ⇒ case t of Var x ⇒ (True,True)
                 | Fun g ts ⇒ let p = prc (f,length ss) (g,length ts) in if fst p then (True,True) else if snd p then 
              lex_ext_unbounded kbo_impl ss ts else (False,False))
       else (False,False))" 
  unfolding kbo_code[of s t] kbo_impl_def Let_def by (rule refl)
end

declare weight_fun_nat_prc.kbo_impl_def[simp]

abbreviation kbo where "kbo ≡ weight_fun_nat_prc.kbo_impl"
declare weight_fun_nat_prc.kbo_impl[code]


(* for representing concrete instances of KBO, we define precedence, ... for finitely many
   symbols, the remainder obtains default values *)
type_synonym 'f prec_weight_repr = "(('f × nat) × (nat × nat × (nat list option))) list × nat"

fun shows_kbo_repr :: "('f :: show) prec_weight_repr ⇒ shows"
where
  "shows_kbo_repr (prs, w0) =
    shows ''KBO with the following precedence and weight function'' ∘ shows_nl ∘
    foldr (λ((f, n),(pr, w, scf)).
      shows ''precedence('' ∘ shows f ∘ shows ''['' ∘ shows n ∘ shows '']) = '' ∘ shows pr ∘ shows_nl) prs ∘ shows_nl ∘
    shows ''precedence(_) = 0'' ∘ shows_nl ∘
    shows ''and the following weight'' ∘ shows_nl ∘
    foldr (λ((f, n), (pr, w, scf)).
      shows ''weight('' ∘ shows f ∘ shows ''['' ∘ shows n ∘ shows '']) = '' ∘ shows w ∘ shows_nl) prs ∘ shows_nl ∘
    shows ''weight(_) = '' ∘ shows (Suc w0) ∘ shows_nl ∘
    shows ''w0 = '' ∘ shows w0 ∘ shows_nl ∘
    shows ''and the following subterm coefficient functions'' ∘ shows_nl ∘
    foldr (λ((f, n), (pr, w, scf)).
      shows ''scf('' ∘ shows f ∘ shows ''['' ∘ shows n ∘ shows '']) = '' ∘
      (if scf = None then shows ''all 1'' else shows (the scf)) ∘ shows_nl) prs ∘ shows_nl ∘
    shows ''scf(_) = all 1'' ∘ shows_nl"

definition scf_repr_to_scf :: "('f × nat ⇒ nat list option) ⇒ ('f × nat ⇒ nat ⇒ nat)" where
  "scf_repr_to_scf scf fn i ≡ case scf fn of None ⇒ 1 | Some xs ⇒ xs ! i"

fun check_scf_entry :: "('f :: show) × nat ⇒ nat list option ⇒ shows check" where
  "check_scf_entry fn None = succeed"
| "check_scf_entry (f,n) (Some es) = do {
     check (length es = n) (shows ''nr of entries should be '' +@+ shows n);
     check (∀ e ∈ set es. e > 0) (shows ''all entries must be non-zero'')
   } <+? (λ s. shows ''problem with subterm coefficients for '' +@+ shows (f,n) +@+ shows '': '' +@+ s +@+ shows_nl)"

definition prec_ext :: "('a ⇒ (nat × 'b) option) ⇒ ('a ⇒ 'a ⇒ bool × bool)"
  where "prec_ext prwm = (λ f g. case prwm f of
    Some pf ⇒ (case prwm g of Some pg ⇒ (fst pf > fst pg, fst pf ≥ fst pg) | None ⇒ (True, True))
    | None ⇒ (False,f=g))"

lemma prec_ext_measure:
  fixes prwm :: "('a ⇒ (nat × 'b) option)"
  defines "m ≡ fun_of_map_fun' prwm (λ _. 0) (Suc ∘ fst)"
  shows  "fst (prec_ext prwm fn gm) = (m fn > m gm)"
proof
  assume s:"fst (prec_ext prwm fn gm)"
  from s[unfolded prec_ext_def] obtain pf where pf:"prwm fn = Some pf"
    by (metis (no_types, lifting) option.exhaust option.simps(4) prod.collapse prod.inject)
  show "m fn > m gm"
  proof(cases "prwm gm = None")
    case True
    with pf show "m fn > m gm" unfolding m_def by force
  next
    case False
    then obtain pg where pg:"prwm gm = Some pg" by auto
    from s[unfolded prec_ext_def pf pg option.cases] pf pg show "m fn > m gm" unfolding m_def by auto
  qed
next
  assume m:"m fn > m gm"
  from this[unfolded m_def] have pf:"prwm fn ≠ None"
    by (metis fun_of_map_fun'.simps not_less_zero option.simps(4))
  then obtain pf where pf:"prwm fn = Some pf" by auto
  show "fst (prec_ext prwm fn gm)" proof(cases "prwm gm = None")
    case False
    then obtain pg where pg:"prwm gm = Some pg" by auto
    from m[unfolded m_def] show ?thesis unfolding prec_ext_def pf pg option.cases using pf pg by force
  next
    case True
    show ?thesis unfolding prec_ext_def pf option.cases True by auto
  qed
qed

lemma prec_ext_weak_id: "fn = gm ⟹ snd (prec_ext prwm fn gm)"
 unfolding prec_ext_def by (cases "prwm fn", auto)

lemma prec_ext_weak_implies_measure:
  assumes "snd (prec_ext prwm fn gm)"
  shows "(fun_of_map_fun' prwm (λ _. 0) (Suc ∘ fst) fn ≥ fun_of_map_fun' prwm (λ _. 0) (Suc ∘ fst) gm)"
  using assms prec_ext_weak_id[of fn gm prwm] unfolding prec_ext_def option.cases
  by (cases "prwm fn", simp, cases "prwm gm", auto)
  
lemma prec_ext_measure_implies_weak:
  fixes prwm :: "('a ⇒ (nat × 'b) option)"
  defines "m ≡ fun_of_map_fun' prwm (λ _. 0) (Suc ∘ fst)"
  assumes pf:"prwm fn = Some pf" and m:"(m fn ≥ m gm)" shows "snd (prec_ext prwm fn gm)"
 using assms unfolding m_def prec_ext_def option.cases pf using pf by (cases "prwm gm", auto)

lemma prec_ext_trans: "trans {(fn, gm). snd (prec_ext prwm fn gm)}" (is "trans ?R")
proof -
  { fix fn gm hk
    assume 1:"snd (prec_ext prwm fn gm)" and 2:"snd (prec_ext prwm gm hk)"
    have "snd (prec_ext prwm fn hk)" proof (cases "prwm fn")
      case None
      from 1[unfolded prec_ext_def None option.cases] 2 show ?thesis by auto
    next
      case (Some pf)
      let ?m = "fun_of_map_fun' prwm (λ _. 0) (Suc ∘ fst)"
      from prec_ext_weak_implies_measure[OF 1] prec_ext_weak_implies_measure[OF 2] have "?m fn ≥ ?m hk" by auto
      from prec_ext_measure_implies_weak[OF Some this] show ?thesis by auto
    qed
  }
  thus ?thesis unfolding trans_def by fast
qed

lemma distinct_map_of:
  assumes distinct:"distinct (map (fst ∘ snd) prw)"
    and pwf:"map_of prw fn = Some pwf"
    and pwg:"map_of prw gm = Some pwg"
  shows "fn = gm ∨ fst pwf ≠ fst pwg"
proof -
  { assume diff:"fn ≠ gm"
    from distinct[unfolded distinct_map] have inj:"inj_on (fst ∘ snd) (set prw)" by auto
    from map_of_SomeD[OF pwf] map_of_SomeD[OF pwg] diff inj
     have "fst pwf ≠ fst pwg" using image_set[of snd prw] unfolding inj_on_def by force
  } thus ?thesis by auto
qed  

  
lemma total_prec_ext:
  fixes prw :: "(('f × nat) × nat × 'b) list"
  defines "p ≡ prec_ext (map_of prw)"
  assumes distinct:"distinct (map (fst ∘ snd) prw)"
    and fn:"fn ∈ set (map fst prw)"
    and gm:"gm ∈ set (map fst prw)"
  shows "fn = gm ∨ fst (p fn gm) ∨ fst (p gm fn)"
proof -
  { assume diff:"fn ≠ gm"
    let ?m = "fun_of_map_fun' (map_of prw) (λ _. 0) (Suc ∘ fst)"
    from fn obtain pwf where pwf:"map_of prw fn = Some pwf" using weak_map_of_SomeI[of fn _ prw] by fastforce
    from gm obtain pwg where pwg:"map_of prw gm = Some pwg" using weak_map_of_SomeI[of gm _ prw] by fastforce
    from distinct_map_of[OF distinct pwf pwg] pwf pwg diff
     have "fst (p fn gm) ∨ fst (p gm fn)" unfolding p_def prec_ext_measure by force
  } thus ?thesis by auto
qed
  
lemma prec_ext_rels:
  fixes prwm :: "('a ⇒ (nat × 'b) option)"
  defines "p ≡ prec_ext prwm"
  shows "fst (p fn gm) = (snd (p fn gm) ∧ ¬ snd (p gm fn))"
proof
  assume s:"fst (p fn gm)"
  note m = s[unfolded p_def prec_ext_measure]
  let ?m = "fun_of_map_fun' prwm (λ _. 0) (Suc ∘ fst)"
  have "(?m fn > ?m gm) ⟹ snd (prec_ext prwm fn gm)"
    using prec_ext_measure_implies_weak[of "prwm"] by (cases "prwm fn", auto)
  with prec_ext_weak_implies_measure[of prwm gm fn] m show "snd (p fn gm) ∧ ¬ snd (p gm fn)" unfolding p_def by auto
next
  assume w:"snd (p fn gm) ∧ ¬ snd (p gm fn)"
  let ?m = "fun_of_map_fun' prwm (λ _. 0) (Suc ∘ fst)"
  from w prec_ext_weak_implies_measure[of prwm fn gm] have m:"?m fn ≥ ?m gm" unfolding p_def by auto
  from w[unfolded p_def prec_ext_def] obtain pf where pf:"prwm fn = Some pf" by (cases "prwm fn", auto)
  show "fst (p fn gm)" proof (cases "prwm gm")
    case None
    from w show ?thesis unfolding p_def prec_ext_def pf None option.cases by auto
  next
    case (Some pg)
    from w show ?thesis unfolding p_def prec_ext_def pf Some option.cases by auto
  qed
qed

lemma prec_ext_strict_weak_total:
  fixes prw :: "(('f × nat) × nat × 'b) list"
  assumes distinct:"distinct (map (fst ∘ snd) prw)"
  shows "snd (prec_ext (map_of prw) fn gm) = (fst (prec_ext (map_of prw) fn gm) ∨ fn = gm)"
proof(cases "(map_of prw) fn")
  case None
  show ?thesis unfolding prec_ext_def None option.cases by auto
next
  case (Some pwf)
  note pwf = this
  show ?thesis proof(cases "(map_of prw) gm")
    case None
    show ?thesis unfolding prec_ext_def Some None option.cases by auto
  next
    case (Some pwg)
    from total_prec_ext[OF distinct] map_of_SomeD[OF pwf] map_of_SomeD[OF Some]
    have  "fn = gm ∨ fst (prec_ext (map_of prw) fn gm) ∨ fst (prec_ext (map_of prw) gm fn)"
      by (metis img_fst set_map)
    show ?thesis proof (cases "fn = gm")
      case True
      with prec_ext_weak_id[OF this, of "map_of prw"] show ?thesis by auto
    next
      case False
      with distinct_map_of[OF distinct pwf Some] have "fst pwf ≠ fst pwg" by auto
      with False show ?thesis  unfolding prec_ext_def pwf Some option.cases by force
    qed
  qed
qed
  
 
  
    
(* check whether partially defined prec and weight are admissible, convert to total weight and prec *)
definition
  prec_weight_repr_to_prec_weight_funs :: "('f :: key) prec_weight_repr ⇒ ('f × nat ⇒ 'f × nat ⇒ bool × bool) × ('f × nat ⇒ nat) × nat × 'f list × ('f × nat ⇒ nat list option)" 
where
  "prec_weight_repr_to_prec_weight_funs prw_w0 ≡
    let 
      (prw, w0) = prw_w0;
      prwm    = ceta_map_of prw;
      w_fun   = fun_of_map_fun' prwm (λ _. Suc w0) (fst o snd);
      p_fun   = prec_ext prwm;
      scf_fun = fun_of_map_fun' prwm (λ _. None) (snd o snd);
      fs      = map fst prw;
      cs      = filter (λ fn. snd fn = 0 ∧ w_fun fn = w0) fs;
      lcs     = map fst (filter (λ c. list_all (λ c'. snd (p_fun c' c)) cs) cs)
      in (p_fun, w_fun, w0, lcs, scf_fun)"

definition
  prec_weight_repr_to_prec_weight :: "('f :: {show,key}) prec_weight_repr ⇒ shows check × ('f × nat ⇒ 'f × nat ⇒ bool × bool) × ('f × nat ⇒ nat) × nat × 'f list × ('f × nat ⇒ nat ⇒ nat)" 
where
  "prec_weight_repr_to_prec_weight prw_w0 ≡
    let
      (p_fun, w_fun, w0, lcs, scf_fun) = prec_weight_repr_to_prec_weight_funs prw_w0;
      (prw, w0) = prw_w0;
      (*(prw, w0) = prw_w0;
      prwm    = ceta_map_of prw;
      w_fun   = fun_of_map_fun' prwm (λ _. Suc w0) (fst o snd);
      p_fun   = prec_ext prwm;
      scf_fun = fun_of_map_fun' prwm (λ _. None) (snd o snd);*)
      fs      = map fst prw;
      cw_okay = check_allm (λ fn. check (snd fn = 0 ⟶ w_fun fn ≥ w0) (shows ''weight of constant '' +@+ shows (fst fn) +@+ shows '' must be at least w0'')) (map fst prw);
      adm     = check_allm (λ fn. check (snd fn = 1 ⟶ w_fun fn = 0 ⟶ (list_all (snd ∘ (p_fun fn)) fs )) (shows ''unary symbol '' +@+ shows (fst fn) +@+ shows '' with weight 0 does not have maximal precedence'')) (map fst prw);
      scf_ok  = check_allm (λ fn. check_scf_entry fn (scf_fun fn)) (map fst prw);
      (*cs      = filter (λ fn. snd fn = 0 ∧ w_fun fn = w0) fs;
      lcs     = map fst (filter (λ c. list_all (λ c'. snd (p_fun c' c)) cs) cs);*)
      ok      = (do {
        check (w0 > 0) (shows ''w0 must be larger than 0'');
        adm;
        cw_okay;
        scf_ok
      })
      in (ok, p_fun, w_fun, w0, lcs, scf_repr_to_scf scf_fun)"

lemma prec_weight_repr_to_prec_weight: 
  assumes ok: "prec_weight_repr_to_prec_weight prw_w0 = (succeed,p,w,w0,lcs,scf_fun)"
  shows "admissible_kbo w w0 (λ fn gm. fst (p fn gm)) (λ fn gm. snd (p fn gm)) (λ c. c ∈ set lcs) scf_fun"
proof -
  have id: "⋀ b. (b = succeed) = isOK(b)" by auto
  note defs = prec_weight_repr_to_prec_weight_def prec_weight_repr_to_prec_weight_funs_def
  obtain prw w0' where prw_w0: "prw_w0 = (prw,w0')" by force
  obtain cs where cs: "cs = filter (λ fn. snd fn = 0 ∧ w fn = w0') (map fst prw)" by auto
  with ok[unfolded defs prw_w0 Let_def split]
   have lcs:"lcs = map fst (filter (λ c. list_all (λ c'. snd (p c' c)) cs) cs)" by fast
  note ok' = ok[unfolded defs prw_w0 Let_def split]
  from ok' have w0': "w0' = w0" by simp
  note ok = ok'[unfolded w0']
  obtain fs where fs: "fs = set (map fst prw)" by auto
  note ok = ok[simplified, unfolded id, simplified]
  have w: "w = (λ fn. case map_of prw fn of Some pw ⇒ (fst o snd) pw | None ⇒ Suc w0)" 
    by (rule ext, insert ok, auto)
  from ok have p:"p = prec_ext (map_of prw)" by auto
  let ?scf = "(λ fn. case map_of prw fn of Some pw ⇒ (snd o snd) pw | None ⇒ None)"
  have scf: "scf_fun = scf_repr_to_scf ?scf"
    by (rule ext, insert ok, auto simp: scf_repr_to_scf_def)
  from ok have cw_okay: "⋀ fn. fn ∈ fs ⟹ snd fn = 0 ⟹ w fn ≥ w0" unfolding w fs by auto
  from ok have "⋀ fn. fn ∈ fs ⟹ snd fn = 1 ⟶ w fn = 0 ⟶ list_all (snd ∘ (p fn)) (map fst prw)"
    unfolding fs w set_map comp_apply by auto
  hence adm: "⋀ fn gm. fn ∈ fs ⟹ gm ∈ fs ⟹ snd fn = 1 ⟹ w fn = 0 ⟹ snd (p fn gm) "
    using fs unfolding list.pred_set by force
  from ok have w0: "w0 > 0" by simp
  let ?least = "λ c. c ∈ set lcs"
  {
    fix fn
    assume "fn ∉ fs"
    hence fn: "⋀ e. (fn,e) ∉ set prw" unfolding fs by force
    with map_of_SomeD[of prw fn] have l: "map_of prw fn = None" 
      by (cases "map_of prw fn", auto)
    hence "w fn = Suc w0 ∧ ?scf fn = None" unfolding p w by auto
  } note not_fs = this
  show ?thesis
  proof
    show "w0 > 0" by (rule w0)
  next    
    fix f
    show "w0 ≤ w (f,0)"
    proof (cases "(f,0) ∈ fs")
      case False
      from not_fs[OF this] show ?thesis by simp
    next
      case True
      from cw_okay[OF this] show ?thesis by simp
    qed
  next
    fix f
    have cmp:"⋀f. list_all (λc'. snd (p c' (f,0))) cs = (∀g. w (g,0) = w0 ⟶ snd (p (g,0) (f,0)))"
      unfolding cs fs list.pred_set set_filter using not_fs[unfolded fs] w0' by force
    show "?least f = (w (f,0) = w0 ∧ (∀ g. w (g,0) = w0 ⟶ snd (p (g,0) (f,0))))" (is "_ = ?r")
      unfolding lcs cmp[symmetric] cs using not_fs[unfolded fs] w0' by (cases "(f,0) ∈ fs", force+)
  next
    fix f g and n::nat
    assume wf:"w (f,1) = 0"
    with not_fs[of "(f,1)"] have f_fs:"(f,1) ∈ fs" by auto
    obtain pf where f_some:"map_of prw (f, 1) = Some pf"
      using weak_map_of_SomeI[of "(f,1)" _ prw] f_fs[unfolded fs] by fastforce
    show "snd(p (f,1) (g,n))" proof(cases "(g,n) ∈ fs")
      case False
      then have g_none:"map_of prw (g, n) = None" unfolding fs map_of_eq_None_iff by force
      from not_fs[OF False] show ?thesis unfolding p prec_ext_def g_none f_some by fastforce
    next
      case True
      from True have "p (g,n) ∈ set (map p (map fst prw))" unfolding fs by force
      from adm[OF f_fs True _ wf] show ?thesis by simp
    qed
  next
    fix f and n i :: nat
    assume i: "i < n"
    define scffn where "scffn = ?scf (f,n)"
    show "0 < scf_fun (f,n) i"
    proof (cases "map_of prw (f, n)")
      case None
      thus ?thesis unfolding scf scf_repr_to_scf_def by auto
    next
      case (Some e)
      define s where "s = (snd o snd) e"
      from map_of_SomeD[OF Some]
      have "((f,n),e) ∈ set prw" by force
      hence "isOK(check_scf_entry (f,n) (?scf (f,n)))"
        using ok by auto
      also have "?scf (f,n) = s" unfolding s_def Some by simp
      finally have ok: "isOK(check_scf_entry (f,n) s)" .
      show ?thesis unfolding scf scf_repr_to_scf_def Some option.simps s_def[symmetric]
        using ok i by (cases s, auto)
    qed
  next
    let ?m = "fun_of_map_fun' (map_of prw) (λ _. 0) (Suc ∘ fst)"
    show "SN {(fn, gm). fst (p fn gm)}" unfolding p prec_ext_measure
      using SN_inv_image[OF SN_nat_gt, unfolded inv_image_def, of ?m] by fast
  next
    show "⋀fn gm hk. snd (p fn gm) ⟹ snd (p gm hk) ⟹ snd (p fn hk)"
      using prec_ext_trans[unfolded trans_def, of "map_of prw"] unfolding p by blast
  next
    fix fn
    show "snd (p fn fn)" unfolding p prec_ext_def by (cases "map_of prw fn", auto)
  next
    from prec_ext_rels show "⋀fn gm. fst (p fn gm) = (snd (p fn gm) ∧ ¬ snd (p gm fn))" unfolding p by fast
  qed
qed

(* checking kbo constraints: invoke kbo, and throw error message if terms are not in relation *)                  
definition
  kbo_strict :: "('f × nat ⇒ 'f × nat ⇒ bool × bool) ⇒ ('f × nat ⇒ nat) ⇒ nat ⇒ ('f ⇒ bool) ⇒ ('f × nat ⇒ nat ⇒ nat) ⇒ ('f :: show,'v :: show)rule ⇒ shows check"
where
  "kbo_strict pr w w0 least scf ≡ λ(s, t). check (fst (kbo w w0 pr least scf s t)) (''could not orient '' +#+ shows s +@+ '' >KBO '' +#+ shows t +@+ shows_nl)"

lemma kbo_strict[simp]: "isOK (kbo_strict pr w w0 least scf st) = fst (kbo w w0 pr least scf (fst st) (snd st))" unfolding kbo_strict_def by (cases st, auto)


definition
  kbo_nstrict :: "('f × nat ⇒ 'f × nat ⇒ bool × bool) ⇒ ('f × nat ⇒ nat) ⇒ nat ⇒ ('f ⇒ bool) ⇒ ('f × nat ⇒ nat ⇒ nat) ⇒ ('f :: show,'v :: show)rule ⇒ shows check"
where
  "kbo_nstrict pr w w0 least scf ≡ λ(s, t). check (snd (kbo w w0 pr least scf s t)) (''could not orient '' +#+ shows s +@+ '' >=KBO '' +#+ shows t +@+ shows_nl)"

lemma kbo_nstrict[simp]: "isOK (kbo_nstrict pr w w0 least scf st) = snd (kbo w w0 pr least scf (fst st) (snd st))" unfolding kbo_nstrict_def by (cases st, auto)

fun create_KBO_redtriple :: "(('f :: show)prec_weight_repr ⇒ 'g prec_weight_repr) ⇒ 'f prec_weight_repr ⇒ ('g :: {show,key},'v :: show)redtriple"
where "create_KBO_redtriple f_to_g pr = (let (ch,p,w,w0,lcs,scf) = prec_weight_repr_to_prec_weight (f_to_g pr);
   ns = kbo_nstrict p w w0 (λc. c ∈ set lcs) scf;
   s =  kbo_strict p w w0 (λc. c ∈ set lcs) scf
    in
  ⦇ redtriple.valid = ch, 
    s = s, 
    ns = ns, 
    nst = ns, 
    af = full_af, 
    mono_af = full_af,
    mono = (λ _. succeed), 
    desc = shows_kbo_repr pr, 
    not_ws_ns = Some [],
    cpx = no_complexity_check⦈)"

(* register KBO as executable reduction triple *)
interpretation KBO_redpair: generic_redtriple_impl "create_KBO_redtriple (f_to_g :: ('f :: show)prec_weight_repr ⇒ ('g :: {show,key})prec_weight_repr)"
proof
  fix "prw" :: "'f prec_weight_repr"
   and s_list ns_list nst_list :: "('g,'v :: show)rule list"
  let ?rp = "create_KBO_redtriple f_to_g prw :: ('g,'v)redtriple"
  let ?af = "redtriple.af ?rp :: ('g af)"
  let ?af' = "redtriple.mono_af ?rp :: ('g af)"
  let ?pr = "prec_weight_repr_to_prec_weight (f_to_g prw)"
  let ?cpx = "redtriple.cpx ?rp"
  let ?cpx' = "λ cm cc. isOK(?cpx cm cc)"
  let ?all = "s_list @ ns_list @ nst_list"
  let ?ws = "redtriple.not_ws_ns ?rp"
  obtain ch "pr" w w0 lcs scf where id: "?pr = (ch,pr,w,w0,lcs,scf)" by (cases ?pr, force)
  assume valid: "isOK(redtriple.valid ?rp)"
   and stri: "isOK(check_allm (redtriple.s ?rp) s_list)"
   and nstri: "isOK (check_allm (redtriple.ns ?rp) ns_list)"
   and nstri_top: "isOK (check_allm (redtriple.nst ?rp) nst_list)"
  have af: "?af = full_af" "?af' = full_af" by (simp_all add: id Let_def)
  from valid have "isOK(ch)" by (simp add: id Let_def)
  hence ch: "ch = succeed" by (cases ch, auto)
  have cpx: "?cpx' = no_complexity" by (simp add: id Let_def)
  note id = id[unfolded ch cpx]
  let ?least = "λf. f ∈ set lcs"
  interpret admissible_kbo w w0 "λ fn gm. fst (pr fn gm)" "λ fn gm. snd (pr fn gm)" ?least scf
    by (rule prec_weight_repr_to_prec_weight[OF id])
  from kbo_redpair 
  interpret mono_ce_af_redtriple_order kbo_S kbo_NS kbo_NS full_af .
  show "∃ S NS NST. cpx_ce_af_redtriple_order S NS NST ?af ?af' ?cpx' 
    ∧ set s_list ⊆ S ∧ set ns_list ⊆ NS ∧ set nst_list ⊆ NST 
    ∧ not_ws_info NS (redtriple.not_ws_ns ?rp)
    ∧ (isOK (redtriple.mono ?rp ?all) ⟶ mono_ce_af_redtriple_order S NS NST ?af ∧ ctxt.closed S)"
    unfolding af cpx
  proof (intro exI conjI impI)
    show "cpx_ce_af_redtriple_order kbo_S kbo_NS kbo_NS full_af full_af no_complexity"
      by (unfold_locales, rule ctxt_closed_imp_af_monotone[OF kbo_S_mono])
    show "mono_ce_af_redtriple_order kbo_S kbo_NS kbo_NS full_af" ..
    show "ctxt.closed kbo_S" by (rule kbo_S_mono)
    show "set s_list ⊆ kbo_S" using stri by (force simp: Let_def id)
    show "set ns_list ⊆ kbo_NS" using nstri by (force simp: Let_def id)
    show "set nst_list ⊆ kbo_NS" using nstri_top by (force simp: Let_def id)
    show "not_ws_info kbo_NS ?ws" 
      by (simp add: id Let_def, intro allI ws_fun_argI kbo_NS_supteq, auto)
  qed
qed

(* total_well_order_extension  *)
definition create_KBO_redord :: "(('f :: {show,key} × nat) × nat × nat × nat list option) list × nat ⇒
  ('f × nat) list ⇒  ('f, string) redord" 
where "create_KBO_redord pr fs = (let
 (ch,p,w,w0,lcs,scf) = prec_weight_repr_to_prec_weight pr;
   valid = (do {
     ch;
     check_same_set fs (map fst (fst pr)) <+? (λfs. shows '' signature does not match '');
     check (length lcs > 0) (shows ''there must be a minimal constant with weight w0'');
     check (distinct (map (fst ∘ snd)(fst pr))) (shows ''the given precedence is not injective'')
   })
  in 
  ⦇ redord.valid = valid,
    redord.less = (λ s t. fst (weight_fun_nat_prc.kbo_impl w w0 (λ f g. p f g) (λf. f ∈ set lcs) scf s t)),
    redord.min_const = lcs ! 0 ⦈)"

  
lemma ext_admissible_weight_fun_prc:
  assumes ok: "prec_weight_repr_to_prec_weight (prw,w0) = (succeed,p,w,w0,lcs,scf_fun)"
    and distinct:"distinct (map (fst ∘ snd) prw)"
    and s:"⋀ fn gm. fst(p fn gm) ⟹ (gm,fn) ∈ (S - Id)"
    and w:"⋀ fn gm. snd(p fn gm) ⟹ (gm,fn) ∈ S"
    and wo:"Well_order S"
    and univ:"Field S = UNIV"
  shows "admissible_kbo w w0 (λ fn gm. (gm,fn) ∈ (S - Id)) (λ fn gm. (gm,fn) ∈ S) (λf. f ∈ set lcs) scf_fun"
proof -
  from ok prec_weight_repr_to_prec_weight[OF ok] have 
    adm:"admissible_kbo w w0 (λ fn gm. fst (p fn gm)) (λ fn gm. snd (p fn gm)) (λ c. c ∈ set lcs) scf_fun" by auto
  note adm = adm[unfolded admissible_kbo_def]
  note pw_defs = prec_weight_repr_to_prec_weight_funs_def prec_weight_repr_to_prec_weight_def
  note ok = ok[unfolded pw_defs split Let_def]
  from ok have p:"p = prec_ext (map_of prw)" by auto
  from wo[unfolded well_order_on_def] have lin:"Linear_order S" by auto
  let ?F = "set (map fst prw)"
  let ?map = "map_of prw"
  let ?w = "(λ fn gm. (gm,fn) ∈ S)"
  let ?s = "(λ fn gm. (gm,fn) ∈ S - Id)"
  show ?thesis proof
    fix f g n
    assume wf0:"w (f,1) = 0"
    from adm wf0 w show "?w (f,1) (g,n)" by metis
  next
    fix f
    let ?lcs_cond = "λ wp. w (f,0) = w0 ∧ (∀g. w (g,0) = w0 ⟶ wp (g,0) (f,0))"
    show "f ∈ set lcs = ?lcs_cond ?w"
    proof
      assume f_lcs:"f ∈ set lcs"
      from adm f_lcs have "?lcs_cond (λ fn gm. snd (p fn gm))" by auto
      with w show "?lcs_cond ?w" by blast
    next
      assume fw0:"?lcs_cond ?w"
      from ok[unfolded Let_def] have "w (f,0) = fun_of_map_fun' ?map (λ _. Suc w0) (fst o snd) (f,0)" by auto
      from this fw0 obtain pwf where pwf:"?map (f,0) = Some pwf" by (cases "?map (f,0)", auto)
      from map_of_SomeD [OF this] have fF:"(f,0) ∈ ?F" by auto
      define cs where "cs = [fn←map fst prw . snd fn = 0 ∧ w fn = w0]"
      from fF fw0 have f_cs:"(f,0) ∈ set cs" unfolding cs_def by auto
      from ok have lcs:"lcs = map fst [c←cs. list_all (λc'. snd (p c' c)) cs]" unfolding cs_def by blast
      { fix c
        assume ccs:"(c,0) ∈ set cs"
        with fw0 have cf:"?w (c,0) (f, 0)" unfolding cs_def by auto
        from ccs have cF:"(c,0) ∈ ?F" unfolding cs_def by auto
        { assume "(c,0) = (f,0)"
          with prec_ext_weak_id have "snd (p (c,0) (f,0))" unfolding p by fast
        } note 1 = this
        { assume "fst (p (c,0) (f,0))"
          with prec_ext_strict_weak_total[OF distinct] have "snd (p (c,0) (f,0))" unfolding p by fast
        } note 2 = this
        { assume neq:"(c,0) ≠ (f,0)" and pfc:"fst (p (f,0) (c,0))"
          with s have sfc:"?s (f,0) (c,0)" by auto
          from Linear_order_in_diff_Id[OF lin, unfolded univ] sfc cf neq have False by blast
        }
        with 1 2 total_prec_ext[OF distinct cF fF] have "snd (p (c,0) (f,0))" unfolding p by auto
      }
      hence "list_all (λc'. snd (p c' (f,0))) cs" unfolding list_all_iff cs_def by simp
      with f_cs show "f ∈ set lcs" unfolding lcs by auto
    qed
  next
    from wo have wf_R: "wf (S - Id)" unfolding well_order_on_def by auto
    thus "SN {(fn,gm). (gm,fn) ∈ (S - Id)}" unfolding SN_iff_wf pair_set_inverse wf_def 
      by (metis (mono_tags, lifting) mem_Collect_eq split_conv)
  next
    from wo univ show "⋀fn. (fn,fn) ∈ S" unfolding well_order_on_def linear_order_on_def
        partial_order_on_def preorder_on_def refl_on_def by auto
  next
    from wo show "⋀fn gm hk. (gm,fn) ∈ S ⟹ (hk,gm) ∈ S ⟹ (hk,fn) ∈ S"
      unfolding well_order_on_def linear_order_on_def partial_order_on_def preorder_on_def trans_def
      by blast
  next
    from Linear_order_in_diff_Id[OF lin] univ
    show "⋀fn gm. ((gm,fn) ∈ S - Id) = ((gm,fn) ∈ S ∧ (fn,gm) ∉ S)" by blast
  qed (insert adm, auto)
qed


interpretation KBO_redord: reduction_order_impl create_KBO_redord
proof
  fix fs :: "('f :: {show,key} × nat) list" and prw_w0 :: "(('f :: {show,key} × nat) × nat × nat × nat list option) list × nat"
  obtain prw w0 where prw_w0:"prw_w0 = (prw, w0)" by fastforce
  let ?ro = "create_KBO_redord prw_w0 fs"
  let ?F = "map fst prw"
  let ?map = "map_of prw"
  let ?min = "redord.min_const ?ro"
  let ?prw = "prec_weight_repr_to_prec_weight (prw, w0)"
  assume ok:"isOK(redord.valid ?ro)"
  note valid = this[unfolded prw_w0 create_KBO_redord_def]
  
  obtain ch pr w w0' lcs scf where id: "?prw = (ch,pr,w,w0',lcs,scf)" by (cases ?prw, force)
  then have w0':"w0' = w0" unfolding prec_weight_repr_to_prec_weight_def
    prec_weight_repr_to_prec_weight_funs_def prw_w0 Let_def by fast
  from valid have "isOK(check_same_set fs (map fst prw))" unfolding id Let_def split fst_conv by simp
  hence fs:"set ?F = set fs" by auto
  note valid = valid[unfolded id Let_def prw_w0 split] 
  from valid have ch_ok:"isOK(ch)" by auto
  let ?least = "λc. c ∈ (set lcs)"
  let ?prs = "λ fn gm. fst (pr fn gm)"
  let ?prw = "λ fn gm. snd (pr fn gm)"
  interpret kbo:admissible_kbo w w0 ?prs ?prw ?least scf
    using prec_weight_repr_to_prec_weight[of prw_w0, unfolded prw_w0 id w0'] ch_ok by auto
  let ?S = "λ s t. (s,t) ∈ kbo.kbo_S"
  let ?W = "?S⇧=⇧="
 
  (* S is a reduction order *)
  interpret reduction_order ?S proof
    show "SN {(x, y). (x, y) ∈ kbo.kbo_S}" using kbo.kbo_strongly_normalizing unfolding SN_defs by blast
  qed (insert kbo.S_ctxt kbo.S_trans kbo.S_subst, auto)

  (* S is F-ground total *)
  from id[unfolded prec_weight_repr_to_prec_weight_funs_def prec_weight_repr_to_prec_weight_def Let_def]
    have pr:"pr = prec_ext (map_of prw)" by auto
  from valid have distinct:"distinct (map (fst ∘ snd) prw)" by auto
  note prec_ftotal = total_prec_ext[OF this]
  from prec_ext_strict_weak_total[OF distinct]
    have pr_sw:"(λfn gm. snd (pr fn gm)) = (λfn gm. fst (pr fn gm))⇧=⇧=" unfolding pr by auto
  { fix s t :: "('f, 'x) term"
    assume fg:"funas_term s ⊆ set ?F" "ground s" "funas_term t ⊆ set ?F" "ground t"
    with kbo.S_ground_total[OF pr_sw, of "set ?F" s t] prec_ftotal 
      have oriented:"s = t ∨ ?S s t ∨ ?S t s" unfolding pr by simp
  }
  hence fgtotal: "⋀s t. fground (set ?F) s ⟹ fground (set ?F) t ⟹ s = t ∨ ?S s t ∨ ?S t s"
    unfolding fground_def by auto
  
  (* extend precedence to a total one *)
  let ?m = "fun_of_map_fun' (map_of prw) (λ _. 0) (Suc ∘ fst)"
  have sn:"SN {(fn, gm). fst (pr fn gm)}" (is "SN ?P") unfolding pr prec_ext_measure
    using SN_inv_image[OF SN_nat_gt, unfolded inv_image_def, of ?m] by fast
  from SN_imp_wf[OF sn] have wf:"wf {(gm,fn). ?prs fn gm}" by auto
  from wf total_well_order_extension obtain Pt where Pt:"{(gm,fn). ?prs fn gm} ⊆ Pt" and
    wo:"Well_order Pt" and univ:"Field Pt = (UNIV :: ('f × nat) set)" by metis
  let ?psx = "λ (fn :: 'f × nat) gm. (gm,fn) ∈ Pt - Id"
  let ?pwx = "λ fn gm. (gm,fn) ∈ Pt"
  from wo[unfolded well_order_on_def] have lin:"Linear_order Pt" by auto
  from Linear_order_in_diff_Id[OF this] univ have ptotal:"⋀fn gm. fn = gm ∨ ?psx fn gm ∨ ?psx gm fn" by blast
  from lin[unfolded linear_order_on_def partial_order_on_def preorder_on_def refl_on_def] univ
    have refl:"⋀x. (x,x) ∈ Pt" by blast
  
  (* there exists a ground-total extension of S *)
  from Pt wf_not_refl[OF wf] have ext_s:"⋀fn gm. ?prs fn gm ⟹ ?psx fn gm" by blast
  with ext_s prec_ext_strict_weak_total[OF distinct] refl
    have ext_w:"⋀fn gm. ?prw fn gm ⟹ ?pwx fn gm" unfolding pr by blast
  interpret kbox: admissible_kbo w w0 ?psx ?pwx ?least scf
    using ext_admissible_weight_fun_prc[OF _ distinct ext_s ext_w wo univ, of w0 pr w lcs scf] id ch_ok
    unfolding isOK_iff w0' by force
  have pr_swx:"?pwx = ?psx⇧=⇧=" by force
  
  (* S is a ground-total reduction order *)
  { fix s t
    assume ground:"ground (s :: ('f, 'x) term)" "ground (t :: ('f, 'x) term)"
    with kbox.S_ground_total[OF pr_swx, of UNIV] ptotal
      have total:"s = t ∨ kbox.S s t ∨ kbox.S t s" by blast
  } note gtotal = this
  interpret redordx:reduction_order kbox.S proof
    show "SN {(x, y). kbox.S x y}" using kbox.kbo_strongly_normalizing unfolding SN_defs by blast
  qed (insert kbox.S_ctxt kbox.S_trans kbox.S_subst, auto)
  interpret admx_gtredord:gtotal_reduction_order kbox.S using gtotal by unfold_locales
  from two_kbos.kbo_prec_mono[of ?least ?least ?prs ?psx ?prw ?pwx w w0 scf, OF _ ext_s ext_w]
  have ext:"(⋀s t. kbo.S s t ⟶ kbox.S s t)" by blast
  note pw_defs = prec_weight_repr_to_prec_weight_def prec_weight_repr_to_prec_weight_funs_def

  (* the minimal constant is in the signature *)
  obtain cs where cs: "cs = filter (λ fn. snd fn = 0 ∧ w fn = w0) ?F" by auto
  with ch_ok id[unfolded pw_defs prw_w0 Let_def split]
    have lcs:"lcs = map fst (filter (λ c. list_all (λ c'. snd (pr c' c)) cs) cs)" by fast
  hence min:"?min = lcs ! 0" unfolding prw_w0 create_KBO_redord_def w0' Let_def prw_w0 id by auto
  from valid have len:"length lcs > 0" unfolding lcs by auto
  from cs have const:"⋀c. c ∈ (set cs) ⟹ snd c = 0" by auto
  from cs have "set cs ⊆ set ?F" by auto
  with lcs const have "⋀c. c ∈ set lcs ⟹ (c,0) ∈ set ?F" by force
  from this[OF nth_mem[OF len]] have min_fs:"(?min,0) ∈ set ?F" unfolding min .

  (* the minimal constant is smaller than any other term *)
  have min_ext:"∀t. ground t ⟶ kbox.S⇧=⇧= t (Fun ?min [])" proof(rule, rule)
    fix t :: "('f, 'x) term"
    assume t:"ground t"
    let ?c = "Fun ?min [] :: ('f,'x)term"
    from len have "lcs ! 0 ∈ set lcs" by auto
    from kbox.NS_all_least[OF this] have ns:"kbox.NS t ?c" unfolding min .
    have "ground ?c" by auto
    from gtotal[OF t this] consider "t = ?c" | "kbox.S t ?c" | "kbox.S ?c t" by blast
    thus "kbox.S⇧=⇧= t ?c" using kbox.S_NS_compat[OF _ ns, of ?c] kbox.S_irrefl[of ?c] by auto
  qed
  
  (* combine to requirements for ordered rewriting *)
  let ?l = "redord.less ?ro"
  let ?c = "redord.min_const ?ro"
  let ?g = "(?c, 0) ∈ (set fs) ∧ reduction_order ?l ∧
            (∀s t. fground (set fs) s ∧ fground (set fs) t ⟶ s = t ∨ ?l s t ∨ ?l t s) ∧
            (∃lt. gtotal_reduction_order lt ∧ (∀s t. ?l s t ⟶ lt s t) ∧ (∀t. ground t ⟶ lt⇧=⇧= t (Fun ?c [])))"
  have less: "redord.less ?ro = ?S"
    unfolding create_KBO_redord_def prw_w0 id Let_def split by (auto simp: prw_w0 w0')
  from prw_w0 have prw:"prw = fst prw_w0" by auto
  from ok show ?g using min_fs fgtotal gtotal ‹reduction_order ?S› ‹gtotal_reduction_order kbox.S›
    ext min_ext unfolding less fs by auto
qed
  
end