Theory SN_Orders
section ‹Strongly Normalizing Orders›
theory SN_Orders
imports Abstract_Rewriting
begin
text ‹
We define several classes of orders which are used to build ordered semirings.
Note that we do not use Isabelle's preorders since the condition
$x > y = x \geq y \wedge y \not\geq x$
is sometimes not applicable. E.g., for $\delta$-orders over the rationals
we have $0.2 \geq 0.1 \wedge 0.1 \not\geq 0.2$, but $0.2 >_\delta 0.1$ does not
hold if $\delta$ is larger than $0.1$.
›
class non_strict_order = ord +
assumes ge_refl: "x ≥ (x :: 'a)"
and ge_trans[trans]: "⟦x ≥ y; (y :: 'a) ≥ z⟧ ⟹ x ≥ z"
and max_comm: "max x y = max y x"
and max_ge_x[intro]: "max x y ≥ x"
and max_id: "x ≥ y ⟹ max x y = x"
and max_mono: "x ≥ y ⟹ max z x ≥ max z y"
begin
lemma max_ge_y[intro]: "max x y ≥ y"
unfolding max_comm[of x y] ..
lemma max_mono2: "x ≥ y ⟹ max x z ≥ max y z"
unfolding max_comm[of _ z] by (rule max_mono)
end
class ordered_ab_semigroup = non_strict_order + ab_semigroup_add + monoid_add +
assumes plus_left_mono: "x ≥ y ⟹ x + z ≥ y + z"
lemma plus_right_mono: "y ≥ (z :: 'a :: ordered_ab_semigroup) ⟹ x + y ≥ x + z"
by (simp add: add.commute[of x], rule plus_left_mono, auto)
class ordered_semiring_0 = ordered_ab_semigroup + semiring_0 +
assumes times_left_mono: "z ≥ 0 ⟹ x ≥ y ⟹ x * z ≥ y * z"
and times_right_mono: "x ≥ 0 ⟹ y ≥ z ⟹ x * y ≥ x * z"
and times_left_anti_mono: "x ≥ y ⟹ 0 ≥ z ⟹ y * z ≥ x * z"
class ordered_semiring_1 = ordered_semiring_0 + semiring_1 +
assumes one_ge_zero: "1 ≥ 0"
text ‹
We do not use a class to define order-pairs of a strict and a weak-order
since often we
have parametric strict orders, e.g. on rational numbers there are several orders
$>$ where $x > y = x \geq y + \delta$ for some parameter $\delta$
›
locale order_pair =
fixes gt :: "'a :: {non_strict_order,zero} ⇒ 'a ⇒ bool" (infix "≻" 50)
and default :: "'a"
assumes compat[trans]: "⟦x ≥ y; y ≻ z⟧ ⟹ x ≻ z"
and compat2[trans]: "⟦x ≻ y; y ≥ z⟧ ⟹ x ≻ z"
and gt_imp_ge: "x ≻ y ⟹ x ≥ y"
and default_ge_zero: "default ≥ 0"
begin
lemma gt_trans[trans]: "⟦x ≻ y; y ≻ z⟧ ⟹ x ≻ z"
by (rule compat[OF gt_imp_ge])
end
locale one_mono_ordered_semiring_1 = order_pair gt
for gt :: "'a :: ordered_semiring_1 ⇒ 'a ⇒ bool" (infix "≻" 50) +
assumes plus_gt_left_mono: "x ≻ y ⟹ x + z ≻ y + z"
and default_gt_zero: "default ≻ 0"
begin
lemma plus_gt_right_mono: "x ≻ y ⟹ a + x ≻ a + y"
unfolding add.commute[of a] by (rule plus_gt_left_mono)
lemma plus_gt_both_mono: "x ≻ y ⟹ a ≻ b ⟹ x + a ≻ y + b"
by (rule gt_trans[OF plus_gt_left_mono plus_gt_right_mono])
end
locale SN_one_mono_ordered_semiring_1 = one_mono_ordered_semiring_1 + order_pair +
assumes SN: "SN {(x,y) . y ≥ 0 ∧ x ≻ y}"
locale SN_strict_mono_ordered_semiring_1 = SN_one_mono_ordered_semiring_1 +
fixes mono :: "'a :: ordered_semiring_1 ⇒ bool"
assumes mono: "⟦mono x; y ≻ z; x ≥ 0⟧ ⟹ x * y ≻ x * z"
locale both_mono_ordered_semiring_1 = order_pair gt
for gt :: "'a :: ordered_semiring_1 ⇒ 'a ⇒ bool" (infix "≻" 50) +
fixes arc_pos :: "'a ⇒ bool"
assumes plus_gt_both_mono: "⟦x ≻ y; z ≻ u⟧ ⟹ x + z ≻ y + u"
and times_gt_left_mono: "x ≻ y ⟹ x * z ≻ y * z"
and times_gt_right_mono: "y ≻ z ⟹ x * y ≻ x * z"
and zero_leastI: "x ≻ 0"
and zero_leastII: "0 ≻ x ⟹ x = 0"
and zero_leastIII: "(x :: 'a) ≥ 0"
and arc_pos_one: "arc_pos (1 :: 'a)"
and arc_pos_default: "arc_pos default"
and arc_pos_zero: "¬ arc_pos 0"
and arc_pos_plus: "arc_pos x ⟹ arc_pos (x + y)"
and arc_pos_mult: "⟦arc_pos x; arc_pos y⟧ ⟹ arc_pos (x * y)"
and not_all_ge: "⋀ c d. arc_pos d ⟹ ∃ e. e ≥ 0 ∧ arc_pos e ∧ ¬ (c ≥ d * e)"
begin
lemma max0_id: "max 0 (x :: 'a) = x"
unfolding max_comm[of 0]
by (rule max_id[OF zero_leastIII])
end
locale SN_both_mono_ordered_semiring_1 = both_mono_ordered_semiring_1 +
assumes SN: "SN {(x,y) . arc_pos y ∧ x ≻ y}"
locale weak_SN_strict_mono_ordered_semiring_1 =
fixes weak_gt :: "'a :: ordered_semiring_1 ⇒ 'a ⇒ bool"
and default :: "'a"
and mono :: "'a ⇒ bool"
assumes weak_gt_mono: "∀ x y. (x,y) ∈ set xys ⟶ weak_gt x y ⟹ ∃ gt. SN_strict_mono_ordered_semiring_1 default gt mono ∧ (∀ x y. (x,y) ∈ set xys ⟶ gt x y)"
locale weak_SN_both_mono_ordered_semiring_1 =
fixes weak_gt :: "'a :: ordered_semiring_1 ⇒ 'a ⇒ bool"
and default :: "'a"
and arc_pos :: "'a ⇒ bool"
assumes weak_gt_both_mono: "∀ x y. (x,y) ∈ set xys ⟶ weak_gt x y ⟹ ∃ gt. SN_both_mono_ordered_semiring_1 default gt arc_pos ∧ (∀ x y. (x,y) ∈ set xys ⟶ gt x y)"
class poly_carrier = ordered_semiring_1 + comm_semiring_1
locale poly_order_carrier = SN_one_mono_ordered_semiring_1 default gt
for default :: "'a :: poly_carrier" and gt (infix "≻" 50) +
fixes power_mono :: "bool"
and discrete :: "bool"
assumes times_gt_mono: "⟦y ≻ z; x ≥ 1⟧ ⟹ y * x ≻ z * x"
and power_mono: "power_mono ⟹ x ≻ y ⟹ y ≥ 0 ⟹ n ≥ 1 ⟹ x ^ n ≻ y ^ n"
and discrete: "discrete ⟹ x ≥ y ⟹ ∃ k. x = (((+) 1)^^k) y"
class large_ordered_semiring_1 = poly_carrier +
assumes ex_large_of_nat: "∃ x. of_nat x ≥ y"
context ordered_semiring_1
begin
lemma pow_mono: assumes ab: "a ≥ b" and b: "b ≥ 0"
shows "a ^ n ≥ b ^ n ∧ b ^ n ≥ 0"
proof (induct n)
case 0
show ?case by (auto simp: ge_refl one_ge_zero)
next
case (Suc n)
hence abn: "a ^ n ≥ b ^ n" and bn: "b ^ n ≥ 0" by auto
have bsn: "b ^ Suc n ≥ 0" unfolding power_Suc
using times_left_mono[OF bn b] by auto
have "a ^ Suc n = a * a ^ n" unfolding power_Suc by simp
also have "... ≥ b * a ^ n"
by (rule times_left_mono[OF ge_trans[OF abn bn] ab])
also have "b * a ^ n ≥ b * b ^ n"
by (rule times_right_mono[OF b abn])
finally show ?case using bsn unfolding power_Suc by simp
qed
lemma pow_ge_zero[intro]: assumes a: "a ≥ (0 :: 'a)"
shows "a ^ n ≥ 0"
proof (induct n)
case 0
from one_ge_zero show ?case by simp
next
case (Suc n)
show ?case using times_left_mono[OF Suc a] by simp
qed
end
lemma of_nat_ge_zero[intro,simp]: "of_nat n ≥ (0 :: 'a :: ordered_semiring_1)"
proof (induct n)
case 0
show ?case by (simp add: ge_refl)
next
case (Suc n)
from plus_right_mono[OF Suc, of 1] have "of_nat (Suc n) ≥ (1 :: 'a)" by simp
also have "(1 :: 'a) ≥ 0" using one_ge_zero .
finally show ?case .
qed
lemma mult_ge_zero[intro]: "(a :: 'a :: ordered_semiring_1) ≥ 0 ⟹ b ≥ 0 ⟹ a * b ≥ 0"
using times_left_mono[of b 0 a] by auto
lemma pow_mono_one: assumes a: "a ≥ (1 :: 'a :: ordered_semiring_1)"
shows "a ^ n ≥ 1"
proof (induct n)
case (Suc n)
show ?case unfolding power_Suc
using ge_trans[OF times_right_mono[OF ge_trans[OF a one_ge_zero] Suc], of 1]
a
by (auto simp: field_simps)
qed (auto simp: ge_refl)
lemma pow_mono_exp: assumes a: "a ≥ (1 :: 'a :: ordered_semiring_1)"
shows "n ≥ m ⟹ a ^ n ≥ a ^ m"
proof (induct m arbitrary: n)
case 0
show ?case using pow_mono_one[OF a] by auto
next
case (Suc m nn)
then obtain n where nn: "nn = Suc n" by (cases nn, auto)
note Suc = Suc[unfolded nn]
hence rec: "a ^ n ≥ a ^ m" by auto
show ?case unfolding nn power_Suc
by (rule times_right_mono[OF ge_trans[OF a one_ge_zero] rec])
qed
lemma mult_ge_one[intro]: assumes a: "(a :: 'a :: ordered_semiring_1) ≥ 1"
and b: "b ≥ 1"
shows "a * b ≥ 1"
proof -
from ge_trans[OF b one_ge_zero] have b0: "b ≥ 0" .
from times_left_mono[OF b0 a] have "a * b ≥ b" by simp
from ge_trans[OF this b] show ?thesis .
qed
lemma sum_list_ge_mono: fixes as :: "('a :: ordered_semiring_0) list"
assumes "length as = length bs"
and "⋀ i. i < length bs ⟹ as ! i ≥ bs ! i"
shows "sum_list as ≥ sum_list bs"
using assms
proof (induct as arbitrary: bs)
case (Nil bs)
from Nil(1) show ?case by (simp add: ge_refl)
next
case (Cons a as bbs)
from Cons(2) obtain b bs where bbs: "bbs = b # bs" and len: "length as = length bs" by (cases bbs, auto)
note ge = Cons(3)[unfolded bbs]
{
fix i
assume "i < length bs"
hence "Suc i < length (b # bs)" by simp
from ge[OF this] have "as ! i ≥ bs ! i" by simp
}
from Cons(1)[OF len this] have IH: "sum_list as ≥ sum_list bs" .
from ge[of 0] have ab: "a ≥ b" by simp
from ge_trans[OF plus_left_mono[OF ab] plus_right_mono[OF IH]]
show ?case unfolding bbs by simp
qed
lemma sum_list_ge_0_nth: fixes xs :: "('a :: ordered_semiring_0)list"
assumes ge: "⋀ i. i < length xs ⟹ xs ! i ≥ 0"
shows "sum_list xs ≥ 0"
proof -
let ?l = "replicate (length xs) (0 :: 'a)"
have "length xs = length ?l" by simp
from sum_list_ge_mono[OF this] ge have "sum_list xs ≥ sum_list ?l" by simp
also have "sum_list ?l = 0" using sum_list_0[of ?l] by auto
finally show ?thesis .
qed
lemma sum_list_ge_0: fixes xs :: "('a :: ordered_semiring_0)list"
assumes ge: "⋀ x. x ∈ set xs ⟹ x ≥ 0"
shows "sum_list xs ≥ 0"
by (rule sum_list_ge_0_nth, insert ge[unfolded set_conv_nth], auto)
lemma foldr_max: "a ∈ set as ⟹ foldr max as b ≥ (a :: 'a :: ordered_ab_semigroup)"
proof (induct as arbitrary: b)
case Nil thus ?case by simp
next
case (Cons c as)
show ?case
proof (cases "a = c")
case True
show ?thesis unfolding True by auto
next
case False
with Cons have "foldr max as b ≥ a" by auto
from ge_trans[OF _ this] show ?thesis by auto
qed
qed
lemma of_nat_mono[intro]: assumes "n ≥ m" shows "(of_nat n :: 'a :: ordered_semiring_1) ≥ of_nat m"
proof -
let ?n = "of_nat :: nat ⇒ 'a"
from assms
show ?thesis
proof (induct m arbitrary: n)
case 0
show ?case by auto
next
case (Suc m nn)
then obtain n where nn: "nn = Suc n" by (cases nn, auto)
note Suc = Suc[unfolded nn]
hence rec: "?n n ≥ ?n m" by simp
show ?case unfolding nn of_nat_Suc
by (rule plus_right_mono[OF rec])
qed
qed
text ‹non infinitesmal is the same as in the CADE07 bounded increase paper›
definition non_inf :: "'a rel ⇒ bool"
where "non_inf r ≡ ∀ a f. ∃ i. (f i, f (Suc i)) ∉ r ∨ (f i, a) ∉ r"
lemma non_infI[intro]: assumes "⋀ a f. ⟦ ⋀ i. (f i, f (Suc i)) ∈ r⟧ ⟹ ∃ i. (f i, a) ∉ r"
shows "non_inf r"
using assms unfolding non_inf_def by blast
lemma non_infE[elim]: assumes "non_inf r" and "⋀ i. (f i, f (Suc i)) ∉ r ∨ (f i, a) ∉ r ⟹ P"
shows P
using assms unfolding non_inf_def by blast
lemma non_inf_image:
assumes ni: "non_inf r" and image: "⋀ a b. (a,b) ∈ s ⟹ (f a, f b) ∈ r"
shows "non_inf s"
proof
fix a g
assume s: "⋀ i. (g i, g (Suc i)) ∈ s"
define h where "h = f o g"
from image[OF s] have h: "⋀ i. (h i, h (Suc i)) ∈ r" unfolding h_def comp_def .
from non_infE[OF ni, of h] have "⋀ a. ∃ i. (h i, a) ∉ r" using h by blast
thus "∃i. (g i, a) ∉ s" using image unfolding h_def comp_def by blast
qed
lemma SN_imp_non_inf: "SN r ⟹ non_inf r"
by (intro non_infI, auto)
lemma non_inf_imp_SN_bound: "non_inf r ⟹ SN {(a,b). (b,c) ∈ r ∧ (a,b) ∈ r}"
by (rule, auto)
end