Theory Abstract-Rewriting.SN_Orders

(*  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