theory Monotone_Algebra
imports
QTRS.Term_Order
begin
locale wf_algebra = SN_order_pair S NS for
NS S :: "'a rel" +
fixes A :: "'a set"
and I :: "'f ⇒ 'a list ⇒ 'a"
and "typ" :: "'v itself"
assumes I_A: "set as ⊆ A ⟹ I f as ∈ A"
and wm: "a ∈ A ⟹ b ∈ A ⟹ set (bef @ aft) ⊆ A
⟹ (a,b) ∈ NS ⟹ (I f (bef @ a # aft), I f (bef @ b # aft)) ∈ NS"
and S_imp_NS: "S ⊆ NS"
begin
fun eval :: "('v ⇒ 'a) ⇒ ('f,'v)term ⇒ 'a" where
"eval α (Var x) = α x"
| "eval α (Fun f ts) = I f (map (eval α) ts)"
lemma eval_A: assumes ran: "range α ⊆ A"
shows "eval α t ∈ A"
proof (induct t)
case Var thus ?case using ran by auto
next
case (Fun f ts)
thus ?case unfolding eval.simps by (intro I_A, auto)
qed
definition S_A :: "('f,'v)term rel" where
"S_A = {(s,t) . (∀ α. range α ⊆ A ⟶ (eval α s, eval α t) ∈ S)}"
definition NS_A :: "('f,'v)term rel" where
"NS_A = {(s,t) . (∀ α. range α ⊆ A ⟶ (eval α s, eval α t) ∈ NS)}"
lemma NS_A_I[intro]: assumes "⋀ α. range α ⊆ A ⟹ (eval α s, eval α t) ∈ NS"
shows "(s,t) ∈ NS_A" using assms unfolding NS_A_def by blast
lemma eval_subst: "eval α (t ⋅ δ) = eval (λ x. eval α (δ x)) t"
proof (induct t)
case (Fun f ts)
thus ?case unfolding subst_apply_term.simps eval.simps
by (intro arg_cong[of _ _ "I f"], auto)
qed simp
lemma S_NS_stable: assumes "((s,t)) ∈ {(s,t) . (∀ α. range α ⊆ A ⟶ (eval α s, eval α t) ∈ S_NS)}" (is "_ ∈ ?r")
shows "(s ⋅ (δ :: ('f,'v)subst), t ⋅ δ) ∈ ?r"
proof -
{
fix α :: "'v ⇒ 'a"
assume "range α ⊆ A"
hence "range (λ x. eval α (δ x)) ⊆ A" using eval_A[of α] by auto
}
thus ?thesis using assms by (auto simp: eval_subst)
qed
lemma S_A_stable: "(s,t) ∈ S_A ⟹ (s ⋅ δ, t ⋅ δ) ∈ S_A"
using S_NS_stable unfolding S_A_def .
lemma NS_A_stable: "(s,t) ∈ NS_A ⟹ (s ⋅ δ, t ⋅ δ) ∈ NS_A"
using S_NS_stable unfolding NS_A_def .
lemma NS_A_mono: assumes st: "(s,t) ∈ NS_A" shows "(Fun f (bef @ s # aft), Fun f (bef @ t # aft)) ∈ NS_A"
proof
fix α :: "'v ⇒ 'a"
assume ran: "range α ⊆ A"
from st ran have "(eval α s, eval α t) ∈ NS" unfolding NS_A_def by auto
from wm[OF eval_A eval_A _ this, of "map (eval α) bef" "map (eval α) aft" f] ran eval_A
show "(eval α (Fun f (bef @ s # aft)), eval α (Fun f (bef @ t # aft))) ∈ NS" by auto
qed
lemma NS_A_NS_A: "(x,y) ∈ NS_A ⟹ (y,z) ∈ NS_A ⟹ (x,z) ∈ NS_A"
using trans_NS_point unfolding NS_A_def by blast
lemma S_A_S_A: "(x,y) ∈ S_A ⟹ (y,z) ∈ S_A ⟹ (x,z) ∈ S_A"
using trans_S_point unfolding S_A_def by blast
lemma NS_A_S_A: "(x,y) ∈ NS_A ⟹ (y,z) ∈ S_A ⟹ (x,z) ∈ S_A"
using compat_NS_S unfolding S_A_def NS_A_def by blast
lemma S_A_NS_A: "(x,y) ∈ S_A ⟹ (y,z) ∈ NS_A ⟹ (x,z) ∈ S_A"
using compat_S_NS unfolding S_A_def NS_A_def by blast
lemma refl_NS_A: "(x,x) ∈ NS_A"
using refl_NS unfolding NS_A_def refl_on_def by blast
lemma S_A_imp_NS_A: "st ∈ S_A ⟹ st ∈ NS_A"
unfolding S_A_def NS_A_def using S_imp_NS by blast
lemma SN_S_A: "SN (S_A)"
proof
fix f
assume all: "∀ i. (f i, f (Suc i)) ∈ S_A"
def α ≡ "λ x :: 'v. I undefined []"
def g ≡ "λ i. eval α (f i)"
have "range α ⊆ A" using I_A[of Nil] unfolding α_def by auto
with all[unfolded S_A_def] have "⋀ i. (g i, g (Suc i)) ∈ S"
unfolding g_def by auto
with SN show False unfolding SN_defs by blast
qed
lemma redtriple_order: "redtriple_order S_A NS_A NS_A"
proof
show "SN S_A" using SN_S_A .
show "ctxt.closed NS_A" by (rule one_imp_ctxt_closed[OF NS_A_mono])
show "subst.closed S_A" using S_A_stable by auto
show "subst.closed NS_A" using NS_A_stable by auto
show "refl NS_A" using refl_NS_A unfolding refl_on_def by auto
show "trans S_A" using S_A_S_A unfolding trans_def by blast
show "trans NS_A" using NS_A_NS_A unfolding trans_def by blast
show "NS_A O S_A ⊆ S_A" using NS_A_S_A by blast
show "S_A O NS_A ⊆ S_A" using S_A_NS_A by blast
show "S_A ⊆ NS_A" using S_A_imp_NS_A by blast
qed
end
locale ws_wf_algebra = wf_algebra NS S A I "typ" for
NS S :: "'a rel" and A :: "'a set" and I :: "'f ⇒ 'a list ⇒ 'a" and "typ" :: "'v itself"
and σ :: "'f status" +
assumes ws: "i ∈ set (status σ (f,length ss)) ⟹ (I f ss, (ss ! i)) ∈ NS"
begin
lemma NS_A_arg: assumes i: "i ∈ set (status σ (f,length ts))"
shows "(Fun f ts, ts ! i) ∈ NS_A"
proof
fix α :: "'v ⇒ 'a"
assume "range α ⊆ A"
from i status[of σ f "length ts"] have ii: "i < length ts" by auto
hence id: "eval α (ts ! i) = (map (eval α) ts) ! i" by auto
show "(eval α (Fun f ts), eval α (ts ! i)) ∈ NS"
unfolding eval.simps id
by (rule ws, insert i, auto)
qed
lemma ws_redpair_order: "ws_redpair_order S_A NS_A σ"
proof -
interpret redtriple_order S_A NS_A NS_A by (rule redtriple_order)
show ?thesis
by (unfold_locales, insert NS_A_arg S_A_imp_NS_A, auto simp: ws_fun_arg_def)
qed
end
end