Theory SN_Orders

theory SN_Orders
imports Abstract_Rewriting
(*  Title:       Executable multivariate polynomials
    Author:      Christian Sternagel <christian.sternagel@uibk.ac.at>
                 René Thiemann       <rene.thiemann@uibk.ac.at>
    Maintainer:  Christian Sternagel and René Thiemann
    License:     LGPL
*)

(*
Copyright 2010 Christian Sternagel and René Thiemann

This file is part of IsaFoR/CeTA.

IsaFoR/CeTA is free software: you can redistribute it and/or modify it under the
terms of the GNU Lesser General Public License as published by the Free Software
Foundation, either version 3 of the License, or (at your option) any later
version.

IsaFoR/CeTA is distributed in the hope that it will be useful, but WITHOUT ANY
WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A
PARTICULAR PURPOSE.  See the GNU Lesser General Public License for more details.

You should have received a copy of the GNU Lesser General Public License along
with IsaFoR/CeTA. If not, see <http://www.gnu.org/licenses/>.
*)

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