Theory Ordered_Algebra

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

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 "<𝒜" 50) where "s <𝒜 t ≡ ∀α. ⟦s⟧α ⊏ ⟦t⟧α"
notation less_term (infix "<𝒜" 50)

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

lemma less_termI[intro]: "(⋀α :: 'v ⇒ 'a. ⟦s⟧α ⊏ ⟦t⟧α) ⟹ s <𝒜 t" by (auto simp: less_term_def)
lemma less_termE[elim]:
  assumes "s <𝒜 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" by (auto simp: less_eq_term_def)
lemma less_eq_termE[elim]:
  assumes "s ≤𝒜 t" and "(⋀α :: 'v ⇒ 'a. ⟦s⟧α ⊑ ⟦t⟧α) ⟹ thesis"
  shows "thesis" using assms by (auto simp: less_eq_term_def)

sublocale "term": ord "(≤𝒜)" "(<𝒜)".

notation(input) term.greater (infix ">𝒜" 50)
notation(input) term.greater_eq (infix "≥𝒜" 50)

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

lemma equiv_termI[intro]: "(⋀α :: 'v ⇒ 'a. ⟦s⟧α ≃ ⟦t⟧α) ⟹ s ≃𝒜 t" by auto
lemma equiv_termE[elim]:
  assumes "s ≃𝒜 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 <𝒜 s ⟹ t⋅σ <𝒜 s⋅σ"
  by (intro less_termI, auto simp: subst_eval)

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

end

locale ordered_algebra = ord_algebra + quasi_order
begin

sublocale "term": quasi_order "(≤𝒜)" "(<𝒜)"
  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 "(≤𝒜) :: ('f,'v) term ⇒ ('f,'v) term ⇒ bool" "(<𝒜)"
proof
  obtain v where "(v :: 'a) = v" by auto
  define α where "α ≡ λx :: 'v. v"
  fix P s
  assume *: "⋀s :: ('f,'v) term. (⋀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 <𝒜 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 (≤) (<) 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 "(≤)" "(<)" f using Cons(2).
    have "f (a # as) ≤ f (b # as)" using ab by auto
    also have "… ≤ f (b # bs)" using Cons(1) all len
      using weak_mono_Cons by blast
    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 (rule str_mono_Cons)
      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 (≥𝒜))"
 by (rule one_imp_ctxt_closed, auto intro: term.append_Cons_le_append_Cons)

lemma subst_closed_S: "subst.closed (rel_of (>𝒜))" by auto

lemma subst_closed_NS: "subst.closed (rel_of (≥𝒜))" by auto

lemma le_ctxt_closed[intro]: "s ≥𝒜 t ⟹ C⟨s⟩ ≥𝒜 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 (>𝒜)" "rel_of (≥𝒜)"
  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 "(≤𝒜)" "(<𝒜)" "(Fun f)"
  by (unfold_locales, intro less_termI, auto intro: append_Cons_less_append_Cons)

lemma ctxt_closed_S: "ctxt.closed (rel_of (>𝒜))"
  by (rule one_imp_ctxt_closed, auto intro: term.append_Cons_less_append_Cons)

lemma less_ctxt_closed[intro]: "s >𝒜 t ⟹ C⟨s⟩ >𝒜 C⟨t⟩"
  using ctxt.closedD[OF ctxt_closed_S] 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 ≥𝒜 r"
begin

lemma rrstep_imp_ge: assumes st: "(s,t) ∈ rrstep R" shows "s ≥𝒜 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 (≥𝒜)"
  using rrstep_imp_ge by auto

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

lemma rrsteps_subseteq_ge: "(rrstep R)* ⊆ rel_of (≥𝒜)"
  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 (>𝒜))" shows "SN(rrstep R)"
proof
  fix f
  assume 1: "chain (rrstep R) f"
  then have "chainp (≥𝒜) f" using rrstep_imp_ge by auto
  from term.chainp_ends_nonstrict[OF this]
  obtain n where "⋀i. i ≥ n ⟹ ¬ f i >𝒜 f (Suc i)" by auto
  with 1 have "⋀i. i ≥ n ⟹ (f i, f (Suc i)) ∈ rrstep R - rel_of (>𝒜)" by auto
  then have "chain (rrstep R - rel_of (>𝒜)) (λ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 >𝒜 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"
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 (>𝒜)"
  using rrstep_imp_greater by auto

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

lemma rrsteps_subseteq_greater: "(rrstep R)+ ⊆ rel_of (>𝒜)"
  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"
  using rstep_imp_ctxt_rrstep[OF st] rrstep_imp_ge by auto

lemma rstep_subseteq_ge: "rstep R ⊆ rel_of (≥𝒜)"
  using rstep_imp_ge by auto

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

lemma rsteps_subseteq_ge: "(rstep R)* ⊆ rel_of (≥𝒜)"
  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 (>𝒜))"
  shows "SN r"
proof
  fix f
  assume 1: "chain r f"
  have "r ⊆ rel_of (≥𝒜)" using rR rsteps_imp_ge by auto
  with 1 have "chainp (≥𝒜) f" by auto
  from term.chainp_ends_nonstrict[OF this]
  obtain n where "⋀i. i ≥ n ⟹ ¬ f i >𝒜 f (Suc i)" by auto
  with 1 have "⋀i. i ≥ n ⟹ (f i, f (Suc i)) ∈ r - rel_of (>𝒜)" by auto
  then have "chain (r - rel_of (>𝒜)) (λ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 (>𝒜))" 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 (>𝒜))" 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"
  using rstep_imp_ctxt_rrstep[OF st] rrstep_imp_greater by auto

lemma rsteps_imp_greater: "(s,t) ∈ (rstep R)+ ⟹ s >𝒜 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 (←*) (←+) 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 α) (←*) (←+) 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 (←*) (←+) 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 (←*) (←+) 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 <𝒜 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 ≃𝒜 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"
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 = "(=)" and less = "λx y. False"
  by (unfold_locales, auto)

sublocale ordered: equimodel
  where less_eq = "(=)" 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›


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

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