theory Quasi_Decreasingness
imports
Conditional_Rewriting
begin
definition "quasi_reductive_order R S ⟷
trans S ∧ SN S ∧
ctxt.closed S ∧
(∀ l r cs (σ :: ('f, 'v) subst). ((l, r), cs) ∈ R ⟶
(∀ i. i < length cs ⟶ (∀j < i. (fst (cs ! j) ⋅ σ, snd (cs ! j) ⋅ σ) ∈ S⇧=) ⟶
(l ⋅ σ, fst (cs ! i) ⋅ σ) ∈ (S ∪ {⊳})⇧+) ∧
((∀j < length cs. (fst (cs ! j) ⋅ σ, snd (cs ! j) ⋅ σ) ∈ S⇧=) ⟶ (l ⋅ σ, r ⋅ σ) ∈ S))"
definition "quasi_decreasing_order R S ⟷
(trans S ∧ SN S ∧
cstep R ⊆ S ∧ {⊳} ⊆ S ∧
(∀ l r cs (σ :: ('f, 'v) subst). ((l, r), cs) ∈ R ⟶
(∀ i. i < length cs ⟶ (∀j < i. (fst (cs ! j) ⋅ σ, snd (cs ! j) ⋅ σ) ∈ (cstep R)⇧* ) ⟶
(l ⋅ σ, fst (cs ! i) ⋅ σ) ∈ S)))"
definition "quasi_reductive R ⟷ (∃S. quasi_reductive_order R S)"
definition "quasi_decreasing R ⟷ (∃S. quasi_decreasing_order R S)"
lemma quasi_reductive_order_cstep:
assumes "quasi_reductive_order (R :: ('f, 'v) ctrs) S"
shows "cstep R ⊆ S"
proof -
from assms [unfolded quasi_reductive_order_def]
have trans: "trans S"
and mono: "ctxt.closed S"
and qr: "⋀ l r cs (σ :: ('f,'v)subst).
((l, r), cs) ∈ R ⟹
(∀j<length cs. (fst (cs ! j) ⋅ σ, snd (cs ! j) ⋅ σ) ∈ S^=) ⟹ (l ⋅ σ, r ⋅ σ) ∈ S" by auto
show "cstep R ⊆ S"
proof
fix s t
assume "(s,t) ∈ cstep R"
then obtain n where "(s,t) ∈ cstep_n R n" unfolding cstep_def by auto
thus "(s,t) ∈ S"
proof (induct n arbitrary: s t)
case (Suc n s t)
from Suc(2)
obtain l r cs C σ where lr: "((l,r),cs) ∈ R" and
cs: "⋀ s⇩i t⇩i. (s⇩i,t⇩i) ∈ set cs ⟹ (s⇩i ⋅ σ, t⇩i ⋅ σ) ∈ (cstep_n R n)⇧*"
and s: "s = C ⟨ l ⋅ σ ⟩" and t: "t = C ⟨ r ⋅ σ ⟩" by (blast elim: cstep_n_SucE)
note qr = qr[OF lr, of σ]
have "(l ⋅ σ, r ⋅ σ) ∈ S"
proof (rule qr[rule_format])
fix j
assume j: "j < length cs"
obtain sj tj where csj: "cs ! j = (sj,tj)" by force
from j have "(sj,tj) ∈ set cs" unfolding csj[symmetric] set_conv_nth by auto
from cs[OF this] have steps: "(sj ⋅ σ, tj ⋅ σ) ∈ (cstep_n R n)⇧*" .
{
fix s t
assume "(s,t) ∈ (cstep_n R n)⇧*"
hence "(s,t) ∈ S^="
proof (induct)
case (step t u)
from step(3) Suc(1)[OF step(2)] have "(s,u) ∈ S^= O S" by auto
thus "(s,u) ∈ S^=" using trans[unfolded trans_def] by blast
qed simp
}
from this[OF steps]
show "(fst (cs ! j) ⋅ σ, snd (cs ! j) ⋅ σ) ∈ S^=" unfolding csj by simp
qed
from ctxt.closedD[OF mono this, of C]
show ?case unfolding s t .
qed simp
qed
qed
lemma quasi_reductive_order_quasi_decreasing_order:
assumes qro: "quasi_reductive_order (R :: ('f, 'v) ctrs) S"
shows "quasi_decreasing_order R ((S ∪ {⊳})⇧+)"
proof -
let ?S = "(S ∪ {⊳})⇧+"
from quasi_reductive_order_cstep[OF qro] have "cstep R ⊆ S" by auto
hence "cstep R ⊆ ?S" by auto
from qro[unfolded quasi_reductive_order_def]
have trans: "trans S" and SN: "SN S"
and mono: "ctxt.closed S"
and decr: "⋀ l r cs i (σ :: ('f,'v)subst).
((l, r), cs) ∈ R ⟹
i < length cs ⟹
(∀j<i. (fst (cs ! j) ⋅ σ, snd (cs ! j) ⋅ σ) ∈ S⇧=) ⟹ (l ⋅ σ, fst (cs ! i) ⋅ σ) ∈ ?S"
by auto
from mono SN have "SN (S ∪ {⊳})" by (metis SN_imp_SN_union_supt)
hence "SN ?S" unfolding SN_trancl_SN_conv .
have "trans ?S" by simp
have "{⊳} ⊆ ?S" by auto
show ?thesis unfolding quasi_decreasing_order_def
proof (intro conjI, rule ‹trans ?S›, rule ‹SN ?S›, rule ‹cstep R ⊆ ?S›, rule ‹{⊳} ⊆ ?S›, intro allI impI)
fix l r cs σ i
assume lr: "((l,r), cs) ∈ R" and i: "i < length cs"
and args: "∀j<i. (fst (cs ! j) ⋅ σ, snd (cs ! j) ⋅ σ) ∈ (cstep R)⇧*"
show "(l ⋅ σ, fst (cs ! i) ⋅ σ) ∈ ?S"
proof (rule decr[OF lr i], intro allI impI)
fix j
assume "j < i"
with args have "(fst (cs ! j) ⋅ σ, snd (cs ! j) ⋅ σ) ∈ (cstep R)⇧*" by auto
also have "(cstep R)⇧* ⊆ S^*" by (rule rtrancl_mono[OF ‹cstep R ⊆ S›])
also have "S^* = (S^+)^=" by regexp
also have "S^+ = S" using trans by auto
finally show "(fst (cs ! j) ⋅ σ, snd (cs ! j) ⋅ σ) ∈ S^=" .
qed
qed
qed
lemma quasi_reductive_quasi_decreasing:
"quasi_reductive R ⟹ quasi_decreasing R"
unfolding quasi_reductive_def quasi_decreasing_def
using quasi_reductive_order_quasi_decreasing_order by blast
lemma quasi_decreasing_SN:
assumes qd: "quasi_decreasing R"
shows "SN (cstep R)"
proof -
from qd[unfolded quasi_decreasing_def] obtain S where "quasi_decreasing_order R S" by blast
from this[unfolded quasi_decreasing_order_def] have "SN S" and "cstep R ⊆ S" by auto
thus ?thesis
by (rule SN_subset)
qed
lemma quasi_reductive_SN:
"quasi_reductive R ⟹ SN (cstep R)"
by (rule quasi_decreasing_SN[OF quasi_reductive_quasi_decreasing])
lemma quasi_reductive_order_csteps:
assumes "quasi_reductive_order R S"
shows "(cstep R)⇧* ⊆ S⇧="
proof -
from assms have trans: "trans S" and RsubS: "cstep R ⊆ S"
using quasi_reductive_order_cstep [OF assms] by (auto simp: quasi_reductive_order_def)
have "(cstep R)⇧* ⊆ S^*" by (rule rtrancl_mono[OF RsubS])
also have "S^* = (S^+)^=" by regexp
also have "S^+ = S" using trans by auto
finally show ?thesis by blast
qed
lemma quasi_reductive_obtains_normalized_subst:
assumes "quasi_reductive_order R S"
obtains τ where "normalized R τ" and "∀x. (σ x, τ x) ∈ (cstep R)⇧*"
and "τ = (λx. some_NF (cstep R) (σ x))"
proof -
have *: "SN (cstep R)" using assms using quasi_reductive_SN quasi_reductive_def by auto
define τ where "τ ≡ λx. some_NF (cstep R) (σ x)"
{ fix x
from * have "(σ x, τ x) ∈ (cstep R)⇧*" unfolding τ_def by (simp add: SN_def some_NF)
then have "(σ x, τ x) ∈ (cstep R)⇧*" by auto
}
then have "∀x. (σ x, τ x) ∈ (cstep R)⇧*" by auto
moreover have "normalized R τ" by (auto simp: normalized_def) (metis SN_def * τ_def some_NF)
ultimately obtain τ where "normalized R τ" and "∀x. (σ x, τ x) ∈ (cstep R)⇧*"
and "τ = (λx. some_NF (cstep R) (σ x))" using τ_def by blast
then show ?thesis ..
qed
lemma quasi_decreasing_order_csteps:
assumes "quasi_decreasing_order R S"
shows "(cstep R)⇧* ⊆ S⇧="
proof -
from assms have trans: "trans S" and RsubS: "cstep R ⊆ S"
by (auto simp: quasi_decreasing_order_def)
have "(cstep R)⇧* ⊆ S^*" by (rule rtrancl_mono[OF RsubS])
also have "S^* = (S^+)^=" by regexp
also have "S^+ = S" using trans by auto
finally show ?thesis by blast
qed
lemma quasi_decreasing_order_conds_sat:
assumes qd: "quasi_decreasing_order R S"
and rule: "((l, r), cs) ∈ R"
and cs: "∀(s, t) ∈ set cs. (s ⋅ σ, t ⋅ σ) ∈ (cstep R)⇧*"
shows "∀i < length cs. (l ⋅ σ, fst (cs ! i) ⋅ σ) ∈ (S ∪ {⊳})⇧+"
proof -
from quasi_decreasing_order_csteps [OF qd] have "(cstep R)⇧* ⊆ S⇧=" .
moreover from qd [unfolded quasi_decreasing_order_def]
have *: "∀l r cs σ. ((l, r), cs) ∈ R ⟶
(∀i < length cs. (∀j < i. (fst (cs ! j) ⋅ σ, snd (cs ! j) ⋅ σ) ∈ (cstep R)⇧*) ⟶
(l ⋅ σ, fst (cs ! i) ⋅ σ) ∈ (S ∪ {⊳})⇧+)" by blast
ultimately have "∀(s, t) ∈ set cs. (s ⋅ σ, t ⋅ σ) ∈ (cstep R)⇧*" using cs by blast
then have "∀i < length cs. ∀j<i. (fst (cs ! j) ⋅ σ, snd (cs ! j) ⋅ σ) ∈ (cstep R)⇧*" by force
with * rule show ?thesis by auto
qed
lemma quasi_decreasing_obtains_normalized_subst:
assumes "quasi_decreasing_order R S"
obtains τ where "normalized R τ" and "∀x. (σ x, τ x) ∈ (cstep R)⇧*"
and "τ = (λx. some_NF (cstep R) (σ x))"
proof -
have *: "SN (cstep R)" using assms using quasi_decreasing_SN quasi_decreasing_def by auto
define τ where "τ ≡ λx. some_NF (cstep R) (σ x)"
{ fix x
from * have "(σ x, τ x) ∈ (cstep R)⇧*" unfolding τ_def by (simp add: SN_def some_NF)
then have "(σ x, τ x) ∈ (cstep R)⇧*" by auto
}
then have "∀x. (σ x, τ x) ∈ (cstep R)⇧*" by auto
moreover have "normalized R τ" by (auto simp: normalized_def) (metis SN_def * τ_def some_NF)
ultimately obtain τ where "normalized R τ" and "∀x. (σ x, τ x) ∈ (cstep R)⇧*"
and "τ = (λx. some_NF (cstep R) (σ x))" using τ_def by blast
then show ?thesis ..
qed
end