Theory Ordered_Algebra

(*
Author:  Akihisa Yamada (2017)
License: LGPL (see file COPYING.LESSER)
*)
theory Ordered_Algebra
imports 
  Quasi_Order
  HOL.Lattices
begin

section {* F-Algebras *}

locale algebra = fixes I :: "'f ⇒ 'a list ⇒ 'a"
begin

fun eval :: "('f,'v) term ⇒ ('v ⇒ 'a) ⇒ 'a"
  where "eval (Var x) α = α x"
      | "eval (Fun f ss) α = I f (map (λs. eval s α) ss)"

notation eval ("⟦(_)⟧")

lemma eval_same_vars[intro]: "(⋀x. x ∈ vars_term t ⟹ α x = β x) ⟹ ⟦t⟧ α = ⟦t⟧ β"
  by(induct t, auto intro!:map_cong[OF refl] cong[of "I _"])

lemma subset_range_eval: "range α ⊆ range (λs. ⟦s⟧α)" (is "?l ⊆ ?r")
proof
  fix a assume "a ∈ ?l"
  then obtain v where "α v = a" by auto
  then show "a ∈ ?r" by (auto intro!: range_eqI[of _ _ "Var v"])
qed

definition constant_at where "constant_at f n i ≡
  ∀as b. i < n ⟶ length as = n ⟶ I f (as[i:=b]) = I f as"

lemma constant_atI:
  assumes "⋀as b. i < n ⟹ length as = n ⟹ I f (as[i:=b]) = I f as"
  shows "constant_at f n i" using assms by (auto simp: constant_at_def)

lemma constant_atD:
  "constant_at f n i ⟹ length as = n ⟹ I f (as[i:=b]) = I f as"
  by (auto simp: constant_at_def)

definition "constant_term_on s x ≡ ∀α a. ⟦s⟧(α(x:=a)) = ⟦s⟧α"

lemma constant_term_onI: assumes "⋀α a. ⟦s⟧(α(x:=a)) = ⟦s⟧α" shows "constant_term_on s x"
  using assms by (auto simp: constant_term_on_def)

lemma constant_term_onD:
  assumes "constant_term_on s x" shows "⟦s⟧(α(x:=a)) = ⟦s⟧α"
  using assms by (auto simp: constant_term_on_def)

lemma constant_term_onE:
  assumes "constant_term_on s x" and "(⋀α a. ⟦s⟧(α(x:=a)) = ⟦s⟧α) ⟹ thesis"
  shows thesis using assms by (auto simp: constant_term_on_def)

lemma constant_term_on_extra_var: "x ∉ vars_term s ⟹ constant_term_on s x"
  by (auto intro!: constant_term_onI)

lemma constant_term_on_eq:
  assumes "⟦s⟧ = ⟦t⟧" and "constant_term_on s x" shows "constant_term_on t x"
  using assms by (simp add: constant_term_on_def)

definition "constant_term s ≡ ∀x. constant_term_on s x"

lemma constant_termI: assumes "⋀x. constant_term_on s x" shows "constant_term s"
  using assms by (auto simp: constant_term_def)

lemma ground_imp_constant: "ground s ⟹ constant_term s"
  by (auto intro!: constant_termI constant_term_on_extra_var simp: ground_vars_term_empty)

end

declare algebra.eval.simps[code,simp]

lemma eval_map_term:
  "algebra.eval I (map_term ff fv t) α = algebra.eval (I ∘ ff) t (α ∘ fv)"
  by (induct t, auto intro: cong[of "I _"])

text {* In the term algebra, evaluation is substitution. *}

interpretation term_algebra: algebra Fun
  rewrites term_algebra_eval: "term_algebra.eval = op ⋅"
proof (intro ext)
  show "algebra.eval Fun s σ = s⋅σ" for s σ by (induct s, unfold algebra.eval.simps, auto)
qed

subsection {* Homomorphism *}

locale algebra_hom = source: algebra I + target: algebra I'
  for hom :: "'a ⇒ 'b" and I :: "'f ⇒ 'a list ⇒ 'a" and I' :: "'f ⇒ 'b list ⇒ 'b" +
  assumes hom: "⋀f as. hom (I f as) = I' f (map hom as)"
begin

lemma hom_eval: "hom (source.eval s α) = target.eval s (λx. hom (α x))"
  by (induct s, auto simp: hom intro: arg_cong[OF list.map_cong0])

end

context algebra begin

text {* Evaluation is a homomophism from the term algebra. *}

sublocale eval_hom: algebra_hom "(λs. ⟦s⟧α)" Fun I
  rewrites "algebra.eval Fun = op ⋅"
  by (unfold_locales, auto simp: term_algebra_eval)

lemmas subst_eval = eval_hom.hom_eval

end

(* a.k.a. subst_subst *)
thm term_algebra.subst_eval[folded subst_compose_def]

locale algebra_epim = algebra_hom +
  assumes surj: "surj hom"

text {* An algebra where every element has a representation: *}
locale algebra_constant = algebra I
  for I :: "'f ⇒ 'a list ⇒ 'a"
  and const :: "'a ⇒ ('f,'v) term" +
  assumes var_term_const[simp]: "⋀d. vars_term (const d) = {}"
      and eval_const[simp]: "⋀d α. ⟦const d⟧ α = d"

subsection {* Quasi-Ordered Algebras *}

text
{* A quasi-ordered algebra is an F-algebra whose domain is quasi-ordered.
   We cannot use @{class quasi_order} as a class since later we want to use
   arbitrary order on terms which cannot be globally fixed. Local instantiation
   would alleviate the problem.
 *}

text {* Following is a syntactic locale where executable definitions should be made. *}
locale ord_algebra = ord less_eq less + algebra I
  for less_eq less :: "'a ⇒ 'a ⇒ bool"
  and I :: "'f ⇒ 'a list ⇒ 'a"
begin

interpretation ord_syntax.

text{* Base orderings are extended over terms in the standard way. *}

definition less_term (infix "⊏⇩t" 50) where "s ⊏⇩t t ≡ ∀α. ⟦s⟧α ⊏ ⟦t⟧α"
notation less_term (infix "⊏⇩t" 50)

definition less_eq_term (infix "⊑⇩t" 50) where "s ⊑⇩t t ≡ ∀α. ⟦s⟧α ⊑ ⟦t⟧α"
notation less_eq_term (infix "⊑⇩t" 50)

lemma less_termI[intro]: "(⋀α :: 'v ⇒ 'a. ⟦s⟧α ⊏ ⟦t⟧α) ⟹ s ⊏⇩t t" by (auto simp: less_term_def)
lemma less_termE[elim]:
  assumes "s ⊏⇩t t" and "(⋀α :: 'v ⇒ 'a. ⟦s⟧α ⊏ ⟦t⟧α) ⟹ thesis"
  shows "thesis" using assms by (auto simp: less_term_def)

lemma less_eq_termI[intro]: "(⋀α :: 'v ⇒ 'a. ⟦s⟧α ⊑ ⟦t⟧α) ⟹ s ⊑⇩t t" by (auto simp: less_eq_term_def)
lemma less_eq_termE[elim]:
  assumes "s ⊑⇩t t" and "(⋀α :: 'v ⇒ 'a. ⟦s⟧α ⊑ ⟦t⟧α) ⟹ thesis"
  shows "thesis" using assms by (auto simp: less_eq_term_def)

sublocale "term": ord "op ⊑⇩t" "op ⊏⇩t".

notation(input) term.greater (infix "⊐⇩t" 50)
notation(input) term.greater_eq (infix "⊒⇩t" 50)

notation term.equiv (infix "≃⇩t" 50)
notation term.equiv_class ("[_]⇩t")

lemma equiv_termI[intro]: "(⋀α :: 'v ⇒ 'a. ⟦s⟧α ≃ ⟦t⟧α) ⟹ s ≃⇩t t" by auto
lemma equiv_termE[elim]:
  assumes "s ≃⇩t t" and "(⋀α :: 'v ⇒ 'a. ⟦s⟧α ≃ ⟦t⟧α) ⟹ thesis"
  shows "thesis" using assms by auto

lemma less_term_stable[intro]: fixes σ :: "'v ⇒ ('f,'w) term" shows "t ⊏⇩t s ⟹ t⋅σ ⊏⇩t s⋅σ"
  by (intro less_termI, auto simp: subst_eval)

lemma less_eq_term_stable[intro]: fixes σ :: "'v ⇒ ('f,'w) term" shows "t ⊑⇩t s ⟹ t⋅σ ⊑⇩t s⋅σ"
  by (intro less_eq_termI, auto simp: subst_eval)

end

locale ordered_algebra = ord_algebra + quasi_order
begin

sublocale "term": quasi_order "op ⊑⇩t" "op ⊏⇩t"
  apply (unfold_locales, unfold less_term_def less_eq_term_def)
  apply (auto dest: order_trans less_trans le_less_trans less_le_trans less_imp_le)
  done

end

locale ordered_algebra_hom =
  algebra_hom hom I I' + ordered_algebra less_eq less I +
  target: ordered_algebra less_eq' less' I'
  for hom less_eq less I less_eq' less' I' +
  assumes le_hom: "less_eq a b ⟹ less_eq' (hom a) (hom b)"
    and less_hom: "less a b ⟹ less' (hom a) (hom b)"

locale ordered_algebra_epim = ordered_algebra_hom + algebra_epim

locale wf_algebra = ordered_algebra where I = I + wf_order
  for I :: "'f ⇒ 'a list ⇒ 'a"
begin

interpretation ord_syntax.

sublocale "term": wf_order "op ⊑⇩t :: ('f,'v) term ⇒ ('f,'v) term ⇒ bool" "op ⊏⇩t"
proof
  obtain v where "(v :: 'a) = v" by auto
  define α where "α ≡ λx :: 'v. v"
  fix P s
  assume *: "⋀s :: ('f,'v) term. (⋀t. t ⊏⇩t s ⟹ P t) ⟹ P s"
  then show "P s"
  proof(induct "⟦s⟧α" arbitrary: s rule: less_induct)
    case less show ?case
    proof (rule less(2))
      fix t assume ts: "t ⊏⇩t s"
      then have "⟦t⟧α ⊏ ⟦s⟧α" by auto
      from less(1)[OF this *] show "P t" by auto
    qed
  qed
qed

end

locale weak_mono = quasi_order +
  fixes f
  assumes append_Cons_le_append_Cons:
    "⋀a b ls rs. less_eq a b ⟹ less_eq (f (ls @ a # rs)) (f (ls @ b # rs))"
begin

interpretation ord_syntax.

lemma Cons_le_Cons[intro,simp]: "a ⊑ b ⟹ f (a#as) ⊑ f (b#as)"
  using append_Cons_le_append_Cons[of _ _ "[]"] by auto

lemma weak_mono_Cons: "weak_mono less_eq less (λas. f (a#as))"
  using append_Cons_le_append_Cons[of _ _ "a#_"] by (unfold_locales, auto)

lemma weak_mono_append_left: "weak_mono less_eq less (λas. f (cs@as))"
  using append_Cons_le_append_Cons[of _ _ "cs@_"] by (unfold_locales, auto)

lemma weak_mono_append_right: "weak_mono less_eq less (λas. f (as@cs))"
  using append_Cons_le_append_Cons by (unfold_locales, auto)

end

lemma (in quasi_order) weak_mono_iff_all_le:
  "weak_mono (op ≤) (op <) f ⟷
   (∀as bs. length as = length bs ⟶ (∀i < length as. as ! i ≤ bs ! i) ⟶ f as ≤ f bs)"
  (is "?l ⟷ ?r")
proof(intro iffI impI allI)
  fix as bs
  assume "?l" and "length as = length bs" and "∀i < length as. as ! i ≤ bs ! i"
  then show "f as ≤ f bs"
  proof (induct as arbitrary: bs f)
    case (Cons a as bbs)
    then obtain b bs
      where bbs: "bbs = b#bs"
        and ab: "a ≤ b"
        and all: "∀i < length as. as ! i ≤ bs ! i"
        and len: "length as = length bs"
      by (atomize(full), cases bbs, auto)
    interpret weak_mono "(op ≤)" "(op <)" f using Cons(2).
    have "f (a # as) ≤ f (b # as)" using ab by auto
    also have "… ≤ f (b # bs)"
      apply (rule Cons(1)) apply fact using all len by auto
    finally show ?case unfolding bbs.
  qed simp
next
  assume r: ?r
  show ?l
  proof (unfold_locales, intro r[rule_format] allI impI)
    fix a b ls rs
    assume ab: "a ≤ b"
    fix i assume i: "i < length (ls @ a # rs)"
    show " (ls @ a # rs) ! i ≤ (ls @ b # rs) ! i"
      by(cases i "length ls" rule: linorder_cases, auto simp: ab nth_append)
  qed auto
qed

lemmas(in weak_mono) weak_mono_all_le = weak_mono_axioms[unfolded weak_mono_iff_all_le, rule_format]

locale str_mono = weak_mono +
  assumes append_Cons_less_append_Cons:
    "⋀ls rs a b. less a b ⟹ less (f (ls @ a # rs)) (f (ls @ b # rs))"
begin

interpretation ord_syntax.

lemma Cons_less_Cons[intro,simp]: "a ⊏ b ⟹ f (a#as) ⊏ f (b#as)"
  using append_Cons_less_append_Cons[of _ _ "[]"] by auto

lemma str_mono_Cons: "str_mono less_eq less (λas. f (a#as))"
  using append_Cons_le_append_Cons[of _ _ "a#_"] append_Cons_less_append_Cons[of _ _ "a#_"]
  by (unfold_locales, auto)

lemma str_mono_append_left: "str_mono less_eq less (λas. f (cs@as))"
  using append_Cons_le_append_Cons[of _ _ "cs@_"] append_Cons_less_append_Cons[of _ _ "cs@_"]
  by (unfold_locales, auto)

lemma str_mono_append_right: "str_mono less_eq less (λas. f (as@cs))"
  using append_Cons_le_append_Cons append_Cons_less_append_Cons by (unfold_locales, auto)

end

context weak_mono begin

interpretation ord_syntax.

lemma str_mono_iff_all_le_ex_less:
  "str_mono less_eq less f ⟷
  (∀as bs. length as = length bs ⟶
    (∀i < length as. as ! i ⊑ bs ! i) ⟶
    (∃i < length as. as ! i ⊏ bs ! i) ⟶ f as ⊏ f bs)" (is "?l ⟷ ?r")
proof (intro iffI allI impI)
  fix as bs
  assume ?l and "length as = length bs" and "∀i < length as. as ! i ⊑ bs ! i"
  and "∃i < length as. as ! i ⊏ bs ! i"
  then show "f as ⊏ f bs"
  proof (induct as arbitrary: bs f)
    case Nil then show ?case by auto
  next
    case (Cons a as bbs)
    from Cons.prems obtain b bs
      where bbs[simp]: "bbs = b#bs"
        and len: "length as = length bs"
      by (atomize(full), cases bbs, auto)
    from Cons.prems
    have ab: "a ⊑ b"
      and all: "∀i < length as. as ! i ⊑ bs ! i"
      and some: "a ⊏ b ∨ (∃i < length as. as ! i ⊏ bs ! i)" by (auto simp: ex_Suc_conv)
    interpret str_mono where f = f using Cons.prems(1) .
    from some show ?case
    proof (elim disjE)
      assume ab: "a ⊏ b"
      interpret str_mono where f = "λcs. f (a#cs)" by fact
      have "f (a#as) ⊑ f (a#bs)" using all len by (simp add: weak_mono_all_le)
      also have "… ⊏ f (b#bs)" using ab by auto
      finally show ?thesis by simp
    next
      assume "∃i < length as. as ! i ⊏ bs ! i"
      from Cons.hyps[OF _ len all this, of "λcs. f (a#cs)"] str_mono_Cons
      have "f (a # as) ⊏ f (a # bs)" by auto
      also have "… ⊑ f (b # bs)" using ab by auto
      finally show ?thesis by simp
    qed
  qed
next
  assume r: ?r
  show ?l
    apply unfold_locales apply (intro r[rule_format])
    apply simp
    apply (metis append_Cons_nth_not_middle eq_imp_le less_imp_le nth_append_length)
    by (metis add_Suc_right length_Cons length_append less_add_Suc1 nth_append_length)
qed

end

lemmas(in str_mono) str_mono_all_le_ex_less =
  str_mono_axioms[unfolded str_mono_iff_all_le_ex_less, rule_format]

subsection {* Weakly monotone algebra *}

locale weak_mono_algebra = ordered_algebra +
  assumes weak_mono: "⋀f. weak_mono less_eq less (I f)"
begin

interpretation ord_syntax.

sublocale weak_mono where f = "I f" by (fact weak_mono)

sublocale "term": weak_mono less_eq_term less_term "Fun f"
  by (unfold_locales, intro less_eq_termI, auto intro: append_Cons_le_append_Cons)

lemma ctxt_closed_NS: "ctxt.closed (rel_of op ⊒⇩t)"
 by (rule one_imp_ctxt_closed, auto intro: term.append_Cons_le_append_Cons)

lemma subst_closed_S: "subst.closed (rel_of op ⊐⇩t)" by auto

lemma subst_closed_NS: "subst.closed (rel_of op ⊒⇩t)" by auto

lemma le_ctxt_closed[intro]: "s ⊒⇩t t ⟹ C⟨s⟩ ⊒⇩t C⟨t⟩"
  using ctxt.closedD[OF ctxt_closed_NS] by auto

lemma eval_le_eval: "∀v ∈ vars_term s. α v ⊑ β v ⟹ ⟦s⟧α ⊑ ⟦s⟧β"
proof (induct s)
  case (Var v) then show ?case by auto
next
  case IH: (Fun f ss)
  { fix i assume i: "i < length ss"
    then have "vars_term (ss!i) ⊆ vars_term (Fun f ss)" by fastforce
    with IH(2) have *: "v ∈ vars_term (ss!i) ⟹ α v ⊑ β v" for v by blast
    with i have "⟦ss ! i⟧α ⊑ ⟦ss ! i⟧β" by(intro IH(1), auto)
  }
  then show ?case by(auto intro: weak_mono_all_le)
qed

end

locale wf_weak_mono_algebra = weak_mono_algebra + wf_order
begin

sublocale wf_algebra..

sublocale redpair: redpair_order "rel_of op ⊐⇩t" "rel_of op ⊒⇩t"
  using SN ctxt_closed_NS subst_closed_S subst_closed_NS by unfold_locales

end


locale mono_algebra = weak_mono_algebra +
  assumes str_mono: "str_mono less_eq less (I f)"
begin

interpretation ord_syntax.

sublocale str_mono where f = "I f" by (fact str_mono)

sublocale "term": str_mono "op ⊑⇩t" "op ⊏⇩t" "(Fun f)"
  by (unfold_locales, intro less_termI, auto intro: append_Cons_less_append_Cons)

lemma ctxt_closed_S: "ctxt.closed (rel_of op ⊐⇩t)"
  by (rule one_imp_ctxt_closed, auto intro: term.append_Cons_less_append_Cons)

lemma less_ctxt_closed[intro]: "s ⊐⇩t t ⟹ C⟨s⟩ ⊐⇩t C⟨t⟩"
  using ctxt.closedD[OF ctxt_closed_S] by auto

(* TODO: Move *)
lemma upt_append_upt: "i ≤ j ⟹ j ≤ k ⟹ [i..<j] @ [j..<k] = [i..<k]"
  using upt_add_eq_append[of i j "k - j"] by auto

lemma eval_less_eval:
  assumes "∀v ∈ vars_term s. α v ⊑ β v"
    and "∃v ∈ vars_term s. α v ⊏ β v"
  shows "⟦s⟧α ⊏ ⟦s⟧β"
proof (insert assms, induct s)
  case (Var v)
  then show ?case by auto
next
  case (Fun f ss)
  from Fun.prems
  obtain i where i: "i < length ss" and "∃v ∈ vars_term (ss!i). α v ⊏ β v"
    by (metis term.sel(4) var_imp_var_of_arg)
  with Fun have ex: "⟦ss!i⟧α ⊏ ⟦ss!i⟧β" by auto
  have "∀t ∈ set ss. ⟦t⟧α ⊑ ⟦t⟧β" using Fun by (auto intro: eval_le_eval)
  with i ex show ?case by (auto intro!: str_mono_all_le_ex_less)
qed

end

locale wf_mono_algebra = mono_algebra + wf_order
begin
  sublocale wf_weak_mono_algebra..
end

section {* Models *}

lemma subst_closed_rrstep: "subst.closed r ⟹ rrstep r = r"
  apply (intro equalityI subrelI)
  apply (force elim: rrstepE)
  apply (force intro: rrstepI[of _ _ _ _ Var])
  done

subsection {* Non-Monotone Models *}

locale quasi_root_model = ordered_algebra where I = I
  for I :: "'f ⇒ 'a list ⇒ 'a" +
  fixes R :: "('f,'v) trs"
  assumes R_imp_ge: "(l,r) ∈ R ⟹ l ⊒⇩t r"
begin

lemma rrstep_imp_ge: assumes st: "(s,t) ∈ rrstep R" shows "s ⊒⇩t t"
proof-
  from st obtain σ l r where s: "s = l⋅σ" and t: "t = r⋅σ" and lr: "(l,r) ∈ R" by (auto simp:rrstep_def')
  show ?thesis by (auto simp: s t intro: R_imp_ge lr)
qed

lemma rrstep_subseteq_ge: "rrstep R ⊆ rel_of op ⊒⇩t"
  using rrstep_imp_ge by auto

lemma rrsteps_imp_ge: "(s,t) ∈ (rrstep R)⇧* ⟹ s ⊒⇩t t"
  by (induct rule: rtrancl_induct, auto dest: rrstep_imp_ge term.order_trans)

lemma rrsteps_subseteq_ge: "(rrstep R)⇧* ⊆ rel_of op ⊒⇩t"
  using rrsteps_imp_ge by auto

end

locale wf_quasi_root_model = quasi_root_model + wf_order
begin

sublocale wf_algebra..

lemma SN_rrstep_minus_greater:
  assumes "SN (rrstep R - rel_of op ⊐⇩t)" shows "SN(rrstep R)"
proof
  fix f
  assume 1: "chain (rrstep R) f"
  then have "chainp (op ⊒⇩t) f" using rrstep_imp_ge by auto
  from term.chainp_ends_nonstrict[OF this]
  obtain n where "⋀i. i ≥ n ⟹ ¬ f i ⊐⇩t f (Suc i)" by auto
  with 1 have "⋀i. i ≥ n ⟹ (f i, f (Suc i)) ∈ rrstep R - rel_of op ⊐⇩t" by auto
  then have "chain (rrstep R - rel_of op ⊐⇩t) (λi. f (n+i))" by auto
  from chain_imp_not_SN_on[OF this] assms
  show False by fast
qed

end

locale strict_root_model = ordered_algebra where I = I
  for I :: "'f ⇒ 'a list ⇒ 'a" +
  fixes R :: "('f,'v) trs"
  assumes R_imp_greater: "(l,r) ∈ R ⟹ l ⊐⇩t r"
begin

sublocale quasi_root_model using R_imp_greater by (unfold_locales, auto dest: term.less_imp_le)

lemma rrstep_imp_greater: assumes st: "(s,t) ∈ rrstep R" shows "s ⊐⇩t t"
proof-
  from st obtain σ l r where s: "s = l⋅σ" and t: "t = r⋅σ" and lr: "(l,r) ∈ R" by (auto simp:rrstep_def')
  show ?thesis by (auto simp: s t intro: R_imp_greater lr)
qed

lemma rrstep_subseteq_greater: "rrstep R ⊆ rel_of op ⊐⇩t"
  using rrstep_imp_greater by auto

lemma rrsteps_imp_greater: "(s,t) ∈ (rrstep R)⇧+ ⟹ s ⊐⇩t t"
  by (induct rule: trancl_induct, auto dest: rrstep_imp_greater term.less_trans)

lemma rrsteps_subseteq_greater: "(rrstep R)⇧+ ⊆ rel_of op ⊐⇩t"
  using rrsteps_imp_greater by auto

end

locale wf_root_model = strict_root_model + wf_algebra
begin

sublocale wf_quasi_root_model..

lemma SN_rrstep: "SN (rrstep R)" by (rule SN_rrstep_minus_greater, auto intro: rrstep_imp_greater)

end

lemma rstep_imp_ctxt_rrstep: "(s,t) ∈ rstep R ⟹ ∃(s',t') ∈ rrstep R. ∃C. s = C⟨s'⟩ ∧ t = C⟨t'⟩"
  by force

subsection {* Monotone Models for Rewriting *}

locale quasi_model = quasi_root_model + weak_mono_algebra
begin

lemma rstep_imp_ge: assumes st: "(s,t) ∈ rstep R" shows "s ⊒⇩t t"
  using rstep_imp_ctxt_rrstep[OF st] rrstep_imp_ge by auto

lemma rstep_subseteq_ge: "rstep R ⊆ rel_of op ⊒⇩t"
  using rstep_imp_ge by auto

lemma rsteps_imp_ge: "(s,t) ∈ (rstep R)⇧* ⟹ s ⊒⇩t t"
  by (induct rule: rtrancl_induct, auto dest: rstep_imp_ge term.order_trans)

lemma rsteps_subseteq_ge: "(rstep R)⇧* ⊆ rel_of op ⊒⇩t"
  using rsteps_imp_ge by auto

end


locale wf_quasi_model = quasi_model + wf_quasi_root_model
begin

lemma SN_minus_greater:
  assumes rR: "r ⊆ (rstep R)⇧*"
  assumes SN: "SN (r - rel_of op ⊐⇩t)"
  shows "SN r"
proof
  fix f
  assume 1: "chain r f"
  have "r ⊆ rel_of op ⊒⇩t" using rR rsteps_imp_ge by auto
  with 1 have "chainp (op ⊒⇩t) f" by auto
  from term.chainp_ends_nonstrict[OF this]
  obtain n where "⋀i. i ≥ n ⟹ ¬ f i ⊐⇩t f (Suc i)" by auto
  with 1 have "⋀i. i ≥ n ⟹ (f i, f (Suc i)) ∈ r - rel_of op ⊐⇩t" by auto
  then have "chain (r - rel_of op ⊐⇩t) (λi. f (n+i))" by auto
  from chain_imp_not_SN_on[OF this] SN_on_subset2[OF _ SN]
  show False by auto
qed

text {* Relative rule removal: *}
lemma SN_rstep_minus_greater:
  assumes "SN (rstep R - rel_of op ⊐⇩t)" shows "SN (rstep R)"
  by (rule SN_minus_greater, insert assms, auto)

text {* Reduction pair processor: *}
lemma SN_relto_rrstep_rstep_minus_greater:
  assumes "SN (relto (rrstep R) (rstep R) - rel_of op ⊐⇩t)" shows "SN (relto (rrstep R) (rstep R))"
    by (rule SN_minus_greater[OF _ assms], auto dest: rrstep_imp_rstep)

end

locale strict_model = strict_root_model + mono_algebra
begin

sublocale quasi_model using R_imp_greater term.less_imp_le by (unfold_locales, auto)

lemma rstep_imp_greater: assumes st: "(s,t) ∈ rstep R" shows "s ⊐⇩t t"
  using rstep_imp_ctxt_rrstep[OF st] rrstep_imp_greater by auto

lemma rsteps_imp_greater: "(s,t) ∈ (rstep R)⇧+ ⟹ s ⊐⇩t t"
  by (induct rule: trancl_induct, auto dest:rstep_imp_greater term.less_trans)

end

locale wf_model = strict_model + wf_order
begin

sublocale wf_quasi_model..
sublocale wf_mono_algebra..

text {* A well-founded model proves termination. *}
lemma SN_rstep: "SN (rstep R)"
  by (rule SN_rstep_minus_greater, auto intro: rstep_imp_greater)

end

subsection {* Rewrite Algebra *}

text {* A TRS induces a monotone algebra w.r.t. rewriting. *}

locale rewrite_algebra = fixes R :: "('f,'v) trs"
begin

abbreviation less_eq (infix "←⇧*" 50) where "t ←⇧* s ≡ (s,t) ∈ (rstep R)⇧*"
abbreviation less (infix "←⇧+" 50) where "t ←⇧+ s ≡ (s,t) ∈ (rstep R)⇧+"

sublocale ord less_eq less
  rewrites "rel_of less_eq = ((rstep R)⇧*)¯"
    and "rel_of less = ((rstep R)⇧+)¯"
    and "rel_of greater_eq = (rstep R)⇧*"
    and "rel_of greater = (rstep R)⇧+"
  by auto

notation less_eq (infix "←⇧*" 50)
notation less (infix "←⇧+" 50)
notation greater_eq (infix "→⇧*" 50)
notation greater (infix "→⇧+" 50)
notation equiv (infix "↔⇧*" 50)

sublocale mono_algebra less_eq less Fun
  using ctxt_closed_rsteps[of R] ctxt.closed_trancl[OF ctxt_closed_rstep[of R]]
  by (unfold_locales, auto simp: dest: ctxt_closed_one)

lemma less_term_is_less[simp]: "less_term = less"
  using subst.closed_trancl[OF subst_closed_rstep[of R]]
  by (unfold less_term_def, auto intro!: ext elim: allE[of _ Var] simp: term_algebra_eval)

lemma le_term_is_le[simp]: "less_eq_term = less_eq"
  using subst.closed_rtrancl[OF subst_closed_rstep[of R]]
  by (unfold less_eq_term_def, auto intro!: ext elim: allE[of _ Var] simp: term_algebra_eval)

(* rsteps_subst_closed is derived *)
thm less_term_stable[where 'v='v and 'w='v, simplified]

sublocale strict_model less_eq less Fun by (unfold_locales, auto)

text {*
  To any model of @{term R}, there is a homomorphism from the term algebra.
*}
proposition strict_model_imp_hom:
  assumes model: "strict_model (less_eq' :: 'b ⇒ _) less' I' R"
  shows "∃hom. ordered_algebra_hom hom (op ←⇧*) (op ←⇧+) Fun less_eq' less' I'"
proof-
  interpret target: strict_model less_eq' less' I' R using model.
  have "ordered_algebra_hom (λs. target.eval s α) (op ←⇧*) (op ←⇧+) Fun less_eq' less' I'" for α
    by (unfold_locales, auto dest: target.rsteps_imp_ge target.rsteps_imp_greater)
  then show ?thesis by auto
qed

text {*
  Further, if there is enough variables, then the model is a homomorphic image of the term algebra.
*}
theorem strict_model_imp_epim:
  assumes surj: "surj (α :: 'v ⇒ 'b)" (* there should be enough variables *)
      and model: "strict_model (less_eq' :: 'b ⇒ _) less' I' R"
  defines "hom ≡ λs. algebra.eval I' s α"
  shows "ordered_algebra_epim hom (op ←⇧*) (op ←⇧+) Fun less_eq' less' I'"
proof-
  interpret target: strict_model less_eq' less' I' R using model.
  from surj have "surj hom" using target.subset_range_eval[of α] by (auto simp: hom_def)
  then show "ordered_algebra_epim hom (op ←⇧*) (op ←⇧+) Fun less_eq' less' I'"
    by (unfold_locales, auto dest: target.rsteps_imp_ge target.rsteps_imp_greater simp: hom_def)
qed

end

text {* The next theorem is due to Zantema (JSC 1994): a TRS is terminating if and only if
  there is a well-founded model for it.
  In paper we don't restrict the domain of interpretations but in Isabelle/HOL we have to.
*}
proposition ex_wf_model_iff_terminating:
  fixes R :: "('f,'v) trs"
  shows "(∃less_eq less :: ('f,'v) term ⇒ _. ∃ I. wf_model less_eq less I R) ⟷ SN (rstep R)" (is "?l ⟷ ?r")
proof
  assume ?l
  then obtain less_eq less :: "('f,'v) term ⇒ _" and I where "wf_model less_eq less I R" by auto
  then interpret wf_model less_eq less I R by auto
  from SN_rstep show ?r.
next
  interpret rewrite_algebra R.
  assume ?r
  then have "SN ((rstep R)⇧+)" by (rule SN_on_trancl)
  from SN_induct[OF this]
  have "wf_model less_eq less Fun R" by (unfold_locales, auto)
  then show ?l by auto
qed

text {* Ordering in the rewrite algebra of R is preserved in any strict model of R. *}

definition models_less
  where "models_less (ty :: 'a itself) R t s ⟷
  (∀less_eq less :: 'a ⇒ _. ∀ I. strict_model less_eq less I R ⟶ ord_algebra.less_term less I t s)"

lemma(in strict_model) models_lessD:
  assumes "models_less (TYPE('a)) R t s" shows "t ⊏⇩t s"
  using assms strict_model_axioms by (auto simp: models_less_def)

lemma models_less_imp_rsteps:
  assumes "models_less (TYPE(('f,'v) term)) (R::('f,'v) trs) t s"
  shows "(s,t) ∈ (rstep R)⇧+"
proof-
  interpret rewrite_algebra R.
  from models_lessD[OF assms] show ?thesis by auto
qed

lemma rsteps_imp_models_less:
  assumes st: "(s,t) ∈ (rstep R)⇧+"
  shows "models_less (TYPE('a)) R t s"
proof (unfold models_less_def, intro allI impI)
  interpret rewrite_algebra R.
  fix less_eq less and I :: "_ ⇒ 'a list ⇒ 'a"
  assume "strict_model less_eq less I R"
  then interpret target: strict_model less_eq less I R.
  from target.rsteps_imp_greater[OF st]
  show "target.less_term t s" by auto
qed

subsection {* Models for Equational Theories *}

locale equimodel = weak_mono_algebra where I = I
  for I :: "'f ⇒ 'a list ⇒ 'a" +
  fixes E :: "('f,'v) trs"
  assumes E_imp_equiv: "(l,r) ∈ E ⟹ l ≃⇩t r"
begin

sublocale quasi_model where R = "E⇧↔"
  by (unfold_locales, insert E_imp_equiv, auto)

lemma conversion_imp_equiv: assumes "(s,t) ∈ (rstep E)⇧↔⇧*" shows "s ≃⇩t t"
proof-
  note * = rsteps_imp_ge[unfolded rstep_simps(5), folded conversion_def]
  from *[OF assms[unfolded conversion_inv[of s t]]] *[OF assms]
  show ?thesis by auto
qed

end

locale model = algebra I for I :: "'f ⇒ 'a list ⇒ 'a" and E :: "('f,'v) trs" +
  assumes E_imp_eq: "(l,r) ∈ E ⟹ ⟦l⟧ = ⟦r⟧"
begin

interpretation ordered: ordered_algebra
  where less_eq = "op =" and less = "λx y. False"
  by (unfold_locales, auto)

sublocale ordered: equimodel
  where less_eq = "op =" and less = "λx y. False"
  by (unfold_locales, auto simp: E_imp_eq)

lemma conversion_imp_eq: assumes "(s,t) ∈ (rstep E)⇧↔⇧*" shows "⟦s⟧ = ⟦t⟧"
  using ordered.conversion_imp_equiv[OF assms] by auto

end


subsection {* Encoding algebras *}

text {*
 Here we ``encode'' an $F$-algebra into a $G$-algebra, where $G$ is supposed to be established
 small signature like the semiring signature.
 Each function symbol $f \in F$ of arity $n$ is encoded as a term in $T(G,{0..<n})$.
*}

subsubsection {* Syntactic Encodings *}

locale pre_encoding =
  fixes E :: "'f ⇒ nat ⇒ ('g, nat) term"
begin

text {* These "pre" locales are needed only for (unconditional) cord equations. *}

abbreviation(input) I where "I f ss ≡ E f (length ss) ⋅ (nth ss)"

sublocale algebra I.

end

locale pre_encoded_algebra = target: algebra I + encoder: pre_encoding E
  for I :: "'g ⇒ 'a list ⇒ 'a"
  and E :: "'f ⇒ nat ⇒ ('g, nat) term"
begin

abbreviation encode :: "('f,'v) term ⇒ ('g,'v) term" where "encode s ≡ encoder.eval s Var"

abbreviation IE :: "'f ⇒ 'a list ⇒ 'a" where "IE f vs ≡ target.eval (E f (length vs)) (nth vs)"

sublocale algebra IE.

lemma constant_at_via_encoding:
  assumes "target.constant_term_on (E f n) i"
  shows "constant_at f n i"
proof (intro constant_atI)
  fix as :: "'a list" and b
  assume 1: "i < n" and 2: "length as = n"
  then have [simp]: "op ! (as [i := b]) = (λj. if i = j then b else as ! j)" by auto
  from target.constant_term_onD[OF assms, of "λj. as ! j" b, symmetric]
  show "target.eval (E f (length (as[i := b]))) (op ! (as[i := b])) =
    target.eval (E f (length as)) (op ! as)" by (auto simp: fun_upd_def 2)
qed

definition "constant_positions f n ≡ [i ← [0..<n]. i ∉ vars_term (E f n)]"

lemma constant_positions: "i ∈ set (constant_positions f n) ⟹ constant_at f n i"
  apply (rule constant_at_via_encoding)
  apply (rule target.constant_term_on_extra_var)
  by (auto simp: constant_positions_def)

end

locale pre_encoded_ord_algebra =
  ord less_eq less + pre_encoded_algebra I E
  for less_eq less :: "'a ⇒ 'a ⇒ bool"
  and I :: "'g ⇒ 'a list ⇒ 'a"
  and E :: "'f ⇒ nat ⇒ ('g, nat) term"
begin

sublocale target: ord_algebra.

sublocale ord_algebra where I = IE.

end

subsubsection {* Well-Formed Encodings *}

locale encoding = pre_encoding +
  assumes var_domain: "i ∈ vars_term (E f n) ⟹ i < n"

locale encoded_algebra = pre_encoded_algebra + encoder: encoding
begin

sublocale algebra_hom "λt. target.eval t α" "encoder.I" IE
  apply unfold_locales
  by (auto simp: target.eval_hom.hom_eval encoder.var_domain)

lemma eval_via_encoding [simp]: "target.eval (encode s) = ⟦s⟧"
  by (intro ext, induct s, auto simp: target.eval_hom.hom_eval encoder.var_domain)

end

locale encoded_ordered_algebra = quasi_order + pre_encoded_ord_algebra + encoded_algebra
begin

sublocale target: ordered_algebra..

sublocale ordered_algebra where I = IE..

end

locale encoded_wf_algebra = wf_order + encoded_ordered_algebra
begin

sublocale target: wf_algebra by (unfold_locales, fact less_induct)

sublocale wf_algebra where I = IE..

end


locale encoded_weak_mono_algebra = encoded_ordered_algebra +
  target: weak_mono_algebra
begin

sublocale weak_mono where f = "IE f"
  using encoder.var_domain
  by (auto simp: weak_mono_iff_all_le intro: target.eval_le_eval)

sublocale weak_mono_algebra where I = IE..

end

locale encoded_mono_algebra = encoded_ordered_algebra +
  target: mono_algebra +
  assumes mono_vars: "i < n ⟹ i ∈ vars_term (E f n)"
begin

interpretation ord_syntax.

sublocale encoded_weak_mono_algebra ..

sublocale str_mono where f = "IE f"
  apply (unfold str_mono_iff_all_le_ex_less)
  using encoder.var_domain mono_vars
  by (auto intro!: target.eval_less_eval)

sublocale mono_algebra where I = IE..

end

locale encoded_wf_weak_mono_algebra =
  encoded_weak_mono_algebra + wf_order
begin

sublocale encoded_wf_algebra..

sublocale wf_weak_mono_algebra where I = IE..

end

locale encoded_wf_mono_algebra =
  encoded_mono_algebra + wf_order
begin

sublocale encoded_wf_weak_mono_algebra..

sublocale wf_mono_algebra where I = IE..

end

end