theory Non_Inf_Order
imports
TRS.Trs
Knuth_Bendix_Order.Order_Pair
"Abstract-Rewriting.SN_Order_Carrier"
begin
text ‹We define non infinitesmal orders and related notions
as in the CADE07 "Bounded Increase" paper.›
text ‹for monotonicity, we do not use 0, 1, -1, and 2 as in CADE07, but a dedicated datatype›
datatype dependance = Ignore | Increase | Decrease | Wild
type_synonym 'f dep = "('f × nat) ⇒ nat ⇒ dependance"
fun rel_dep :: "'a rel ⇒ dependance ⇒ 'a rel" (infix "^^^" 52) where
"_ ^^^ Ignore = {}"
| "r ^^^ Increase = r"
| "r ^^^ Decrease = (r ^-1)"
| "r ^^^ Wild = (r^<->)"
lemma rel_dep_mono: "r1 ⊆ r2 ⟹ r1 ^^^ k ⊆ r2 ^^^ k"
by (cases k, auto)
fun invert_dep :: "dependance ⇒ dependance" where
"invert_dep Increase = Decrease"
| "invert_dep Decrease = Increase"
| "invert_dep d = d"
lemma rel_dep_invert_mono: "r1^-1 ⊆ r2 ⟹ r1 ^^^ invert_dep k ⊆ r2 ^^^ k"
by (cases k, auto)
text ‹for compatibility (monotonicity) we only consider F-terms, not all terms as in CADE07›
definition dep_compat :: "'f sig ⇒ ('f, 'v) term rel ⇒ 'f dep ⇒ bool" where
"dep_compat F r π ⟷ (∀ f bef s t aft. ⋃(funas_term ` ({s,t} ∪ set bef ∪ set aft)) ⊆ F ⟶
{(s,t)} ^^^ π (f,Suc (length bef + length aft)) (length bef) ⊆ r ⟶ (Fun f (bef @ s # aft), Fun f (bef @ t # aft)) ∈ r)"
lemma dep_compatE[elim]: assumes dep: "dep_compat F r π" shows "funas_args_term (Fun f (bef @ s # aft)) ⊆ F ⟹ funas_term t ⊆ F ⟹
{(s,t)} ^^^ π (f,Suc (length bef + length aft)) (length bef) ⊆ r
⟹ (Fun f (bef @ s # aft), Fun f (bef @ t # aft)) ∈ r"
unfolding funas_args_term_def
by (rule dep[unfolded dep_compat_def, rule_format, of s t bef aft f], force+)
lemma dep_compatI[intro]: assumes "⋀ f bef s t aft.
⟦⋀ u. u ∈ {s,t} ∪ set bef ∪ set aft ⟹ funas_term u ⊆ F⟧ ⟹
{(s,t)} ^^^ π (f,Suc (length bef + length aft)) (length bef) ⊆ r
⟹ (Fun f (bef @ s # aft), Fun f (bef @ t # aft)) ∈ r"
shows "dep_compat F r π"
unfolding dep_compat_def
by (intro allI impI, rule assms, auto)
text ‹F-stability (closure under F-substitutions) is the same as in CADE07›
definition F_subst_closed :: "'f sig ⇒ ('f, 'v) trs ⇒ bool" where
"F_subst_closed F r ⟷
(∀ σ s t. ⋃(funas_term ` range σ) ⊆ F ⟶ (s,t) ∈ r ⟶ (s ⋅ σ, t ⋅ σ) ∈ r)"
lemma F_subst_closedI[intro]:
assumes "⋀ σ s t. ⋃(funas_term ` range σ) ⊆ F ⟹ (s,t) ∈ r ⟹ (s ⋅ σ, t ⋅ σ) ∈ r"
shows "F_subst_closed F r" using assms unfolding F_subst_closed_def by blast
lemma F_subst_closedD[elim]: "F_subst_closed F r ⟹ ⋃(funas_term ` range σ) ⊆ F ⟹ (s,t) ∈ r ⟹ (s ⋅ σ, t ⋅ σ) ∈ r"
unfolding F_subst_closed_def by auto
lemma F_subst_closed_UNIV:
"F_subst_closed F r ⟹ F = UNIV ⟹ subst.closed r" unfolding F_subst_closed_def
using subst.closedI[of r] by auto
text ‹a locale to have all nice properties together›
locale non_inf_order = Order_Pair.order_pair S NS for S NS :: "'a rel" +
assumes non_inf: "non_inf S"
begin
lemma chain_split: fixes f :: "'b seq" and m :: "'b ⇒ 'a"
assumes fS: "fS ⊆ {i. (m (f i), m (f (Suc i))) ∈ S}"
and fB: "fB ⊆ {i. (m (f i), a) ∈ NS ∪ S}"
and decr: "⋀ i. (m (f i), m (f (Suc i))) ∈ NS ∪ S"
shows "(∀⇩∞ j. j ∉ fS) ∨ (∀⇩∞ j. j ∉ fB)"
proof (cases "(∃⇩∞ i. i ∈ fS) ∧ (∃⇩∞ i. i ∈ fB)")
case False
then show ?thesis unfolding INFM_nat_le MOST_nat_le by blast
next
case True
define g where "g = (λ i. m (f i))"
from decr have orient': "⋀ i. (g i, g (Suc i)) ∈ NS ∪ S" unfolding g_def by auto
have Ps': "⋀ i. i ∈ fS ⟹ (g i, g (Suc i)) ∈ S" using fS unfolding g_def by auto
have Pb': "⋀ i. i ∈ fB ⟹ (g i, a) ∈ NS ∪ S" using fB unfolding g_def by auto
from decr have orient': "⋀ i. (g i, g (Suc i)) ∈ NS ∪ S" unfolding g_def by auto
{
fix i j :: nat
assume "i ≤ j"
then have "j = (j - i) + i" by arith
then obtain k where j: "j = k + i" by blast
have "(g i, g j) ∈ (NS ∪ S)^*" unfolding j
proof (induct k)
case (Suc k)
with orient'[of "k + i"] have "(g i, g (Suc k + i)) ∈ (NS ∪ S)^* O (NS ∪ S)" by auto
then show ?case by regexp
qed simp
} note NS = this
let ?P = "λ i. (g i, g (Suc i)) ∈ S"
from True have infm: "INFM i. ?P i" using fS unfolding g_def INFM_nat_le by blast
interpret infinitely_many ?P
by (unfold_locales, rule infm)
let ?i = "λ i. index i"
define v where "v = (λ i. g (?i i))"
{
fix i
from index_p[of i] have S: "(v i, g (Suc (?i i))) ∈ S" unfolding v_def .
from index_ordered[of i] have "Suc (?i i) ≤ ?i (Suc i)" by simp
from compat_rtrancl[OF S NS[OF this]] have vv: "(v i, v (Suc i)) ∈ S" unfolding v_def .
from True obtain j where ji: "j ≥ ?i (Suc i)" and Pb: "j ∈ fB" unfolding INFM_nat_le by auto
from fB Pb have *: "(g j, a) ∈ NS ∪ S" unfolding g_def by auto
from compat_rtrancl[OF vv[unfolded v_def] NS[OF ji]] have "(v i, g j) ∈ S" unfolding v_def .
with * compat_S_NS_point trans_S_point
have "(v i, a) ∈ S" by blast
then have "(v i, v (Suc i)) ∈ S" and "(v i, a) ∈ S" using vv by blast+
}
with non_infE[OF non_inf, of v a] have False by blast
then show ?thesis ..
qed
end
definition "bound_on b s = {(x,y). (x,b) ∈ s ∧ (x,y) ∈ s}"
definition "bound_on_le b s ns = {(x,y). (x,b) ∈ ns ∧ (x,y) ∈ s}"
lemma (in non_inf_order) bound_on_SN_generic: "SN (bound_on_le bnd S (NS ∪ S))"
proof -
have sn: "SN {(a, b). (b, bnd) ∈ S ∧ (a, b) ∈ S}" by (rule non_inf_imp_SN_bound[OF non_inf])
show ?thesis proof(rule SN_onI) fix f
assume "∀i. (f i, f (Suc i)) ∈ bound_on_le bnd S (NS ∪ S)"
then have all:"⋀i. (f i, f (Suc i)) ∈ {(x,y). (y,bnd) ∈ NS ∪ S ∧ (x,y) ∈ S}"
unfolding bound_on_le_def by auto
then have s:"⋀ i. (f i, f (Suc i)) ∈ S"
and b:"⋀ i. (f (Suc i),bnd) ∈ NS ∪ S" by auto
from sn[unfolded SN_defs]
obtain i where i:"(f i, f (Suc i)) ∉ {(a, b). (b, bnd) ∈ S ∧ (a, b) ∈ S}" by auto
then have "(f (Suc i), bnd) ∉ S" using s by auto
then have "(f (Suc i), f (Suc (Suc i))) ∉ {(x,y). (y,bnd) ∈ NS ∪ S ∧ (x,y) ∈ S}"
using compat_S_NS_point trans_S_point by blast
then show False using all by auto
qed
qed
lemma (in non_inf_order) bound_on_SN: "SN (bound_on bnd S)"
by (rule SN_subset[OF bound_on_SN_generic], auto simp: bound_on_def bound_on_le_def)
lemma (in non_inf_order) bound_on_le_SN: "SN (bound_on_le bnd S NS)"
by (rule SN_subset[OF bound_on_SN_generic], auto simp: bound_on_le_def)
lemma (in Order_Pair.compat_pair) compat_pair_bound_on:
shows "Order_Pair.compat_pair (bound_on bnd S) NS"
by (unfold_locales, auto simp: bound_on_def dest: compat_NS_S_point compat_S_NS_point)
lemma (in Order_Pair.pre_order_pair) pre_order_pair_bound_on:
shows "Order_Pair.pre_order_pair (bound_on bnd S) NS"
by (unfold_locales, auto simp: bound_on_def intro: transI refl_NS dest: transD trans_NS_point trans_S_point)
lemma (in Order_Pair.order_pair) order_pair_bound_on:
shows "Order_Pair.order_pair (bound_on bnd S) NS"
by (unfold Order_Pair.order_pair_def, auto intro: compat_pair_bound_on pre_order_pair_bound_on)
lemma (in non_inf_order) SN_order_pair_bound_on:
shows "Order_Pair.SN_order_pair (bound_on bnd S) NS"
by (unfold SN_order_pair_def SN_ars_def, intro conjI order_pair_bound_on bound_on_SN)
lemma(in Order_Pair.order_pair) order_pair_union: "Order_Pair.order_pair S (NS ∪ S)"
by (unfold_locales, auto dest: compat_NS_S_point compat_S_NS_point trans_S_point trans_NS_point intro: trans_S refl_onI refl_NS_point transI)
lemma(in SN_order_pair) SN_order_pair_union: shows "SN_order_pair S (NS ∪ S)"
proof-
interpret Order_Pair.order_pair S "NS ∪ S" by (rule order_pair_union)
show ?thesis..
qed
lemma(in non_inf_order) non_inf_union: shows "non_inf_order S (NS ∪ S)"
proof-
interpret Order_Pair.order_pair S "NS ∪ S" by (fact order_pair_union)
show ?thesis by (unfold_locales, fact non_inf)
qed
lemma(in Order_Pair.order_pair) order_pair_inv_image: "Order_Pair.order_pair (inv_image S f) (inv_image NS f)"
by (unfold_locales, auto intro!: refl_onI refl_NS_point transI dest: trans_S_point trans_NS_point compat_NS_S_point compat_S_NS_point)
lemma non_inf_inv_image: "non_inf S ⟹ non_inf (inv_image S f)" by fastforce
lemma(in non_inf_order) non_inf_order_inv_image: "non_inf_order (inv_image S f) (inv_image NS f)"
proof-
interpret Order_Pair.order_pair "inv_image S f" "inv_image NS f" by (fact order_pair_inv_image)
from non_inf_inv_image[OF non_inf] show ?thesis by unfold_locales
qed
locale non_inf_order_trs = non_inf_order S NS
for S :: "('f,'v)trs"
and NS :: "('f,'v)trs" +
fixes F :: "'f sig"
and π :: "'f dep"
assumes stable_NS: "F_subst_closed F NS"
and stable_S: "F_subst_closed F S"
and dep_compat_NS: "dep_compat F NS π"
end