(* Title: Executable multivariate polynomials Author: Christian Sternagel <christian.sternagel@uibk.ac.at> Rene Thiemann <rene.thiemann@uibk.ac.at> Maintainer: Christian Sternagel and Rene 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 ‹Carriers of Strongly Normalizing Orders› theory SN_Order_Carrier imports SN_Orders HOL.Rat begin text ‹ This theory shows that standard semirings can be used in combination with polynomials, e.g. the naturals, integers, and arbitrary Archemedean fields by using delta-orders. It also contains the arctic integers and arctic delta-orders where 0 is -infty, 1 is zero, + is max and * is plus. › subsection ‹The standard semiring over the naturals› instantiation nat :: large_ordered_semiring_1 begin instance by (intro_classes, auto) end definition nat_mono :: "nat ⇒ bool" where "nat_mono x ≡ x ≠ 0" interpretation nat_SN: SN_strict_mono_ordered_semiring_1 1 "(>) :: nat ⇒ nat ⇒ bool" nat_mono by (unfold_locales, insert SN_nat_gt, auto simp: nat_mono_def) interpretation nat_poly: poly_order_carrier 1 "(>) :: nat ⇒ nat ⇒ bool" True discrete proof (unfold_locales) fix x y :: nat assume ge: "x ≥ y" obtain k where k: "x - y = k" by auto show "∃ k. x = ((+) 1 ^^ k) y" proof (rule exI[of _ k]) from ge k have "x = k + y" by simp also have "… = ((+) 1 ^^ k) y" by (induct k, auto) finally show "x = ((+) 1 ^^ k) y" . qed qed (auto simp: field_simps power_strict_mono) subsection ‹The standard semiring over the Archimedean fields using delta-orderings› definition delta_gt :: "'a :: floor_ceiling ⇒ 'a ⇒ 'a ⇒ bool" where "delta_gt δ ≡ (λ x y. x - y ≥ δ)" lemma non_inf_delta_gt: assumes delta: "δ > 0" shows "non_inf {(a,b) . delta_gt δ a b}" (is "non_inf ?r") proof let ?gt = "delta_gt δ" fix a :: 'a and f assume "⋀ i. (f i, f (Suc i)) ∈ ?r" hence gt: "⋀ i. ?gt (f i) (f (Suc i))" by simp { fix i have "f i ≤ f 0 - δ * of_nat i" proof (induct i) case (Suc i) thus ?case using gt[of i, unfolded delta_gt_def] by (auto simp: field_simps) qed simp } note fi = this { fix r :: 'a have "of_nat (nat (ceiling r)) ≥ r" by (metis ceiling_le_zero le_of_int_ceiling less_le_not_le nat_0_iff not_less of_nat_0 of_nat_nat) } note ceil_elim = this define i where "i = nat (ceiling ((f 0 - a) / δ))" from fi[of i] have "f i - f 0 ≤ - δ * of_nat (nat (ceiling ((f 0 - a) / δ)))" unfolding i_def by simp also have "… ≤ - δ * ((f 0 - a) / δ)" using ceil_elim[of "(f 0 - a) / δ"] delta by (metis le_imp_neg_le minus_mult_commute mult_le_cancel_left_pos) also have "… = - f 0 + a" using delta by auto also have "… < - f 0 + a + δ" using delta by auto finally have "¬ ?gt (f i) a" unfolding delta_gt_def by arith thus "∃ i. (f i, a) ∉ ?r" by blast qed lemma delta_gt_SN: assumes dpos: "δ > 0" shows "SN {(x,y). 0 ≤ y ∧ delta_gt δ x y}" proof - from non_inf_imp_SN_bound[OF non_inf_delta_gt[OF dpos], of "- δ"] show ?thesis unfolding delta_gt_def by auto qed definition delta_mono :: "'a :: floor_ceiling ⇒ bool" where "delta_mono x ≡ x ≥ 1" subclass (in floor_ceiling) large_ordered_semiring_1 proof fix x :: 'a from ex_le_of_int[of x] obtain z where x: "x ≤ of_int z" by auto have "z ≤ int (nat z)" by auto with x have "x ≤ of_int (int (nat z))" by (metis (full_types) le_cases of_int_0_le_iff of_int_of_nat_eq of_nat_0_le_iff of_nat_nat order_trans) also have "… = of_nat (nat z)" unfolding of_int_of_nat_eq .. finally show "∃ y. x ≤ of_nat y" by blast qed (auto simp: mult_right_mono mult_left_mono mult_right_mono_neg max_def) lemma delta_interpretation: assumes dpos: "δ > 0" and default: "δ ≤ def" shows "SN_strict_mono_ordered_semiring_1 def (delta_gt δ) delta_mono" proof - from dpos default have defz: "0 ≤ def" by auto show ?thesis proof (unfold_locales) show "SN {(x,y). y ≥ 0 ∧ delta_gt δ x y}" by (rule delta_gt_SN[OF dpos]) next fix x y z :: 'a assume "delta_mono x" and yz: "delta_gt δ y z" hence x: "1 ≤ x" unfolding delta_mono_def by simp have "∃ d > 0. delta_gt δ = (λ x y. d ≤ x - y)" by (rule exI[of _ δ], auto simp: dpos delta_gt_def) from this obtain d where d: "0 < d" and rat: "delta_gt δ = (λ x y. d ≤ x - y)" by auto from yz have yzd: "d ≤ y - z" by (simp add: rat) show "delta_gt δ (x * y) (x * z)" proof (simp only: rat) let ?p = "(x - 1) * (y - z)" from x have x1: "0 ≤ x - 1" by auto from yzd d have yz0: "0 ≤ y - z" by auto have "0 ≤ ?p" by (rule mult_nonneg_nonneg[OF x1 yz0]) have "x * y - x * z = x * (y - z)" using right_diff_distrib[of x y z] by auto also have "… = ((x - 1) + 1) * (y - z)" by auto also have "… = ?p + 1 * ( y - z)" by (rule ring_distribs(2)) also have "… = ?p + (y - z)" by simp also have "… ≥ (0 + d)" using yzd ‹0 ≤ ?p› by auto finally show "d ≤ x * y - x * z" by auto qed qed (insert dpos, auto simp: delta_gt_def default defz) qed lemma delta_poly: assumes dpos: "δ > 0" and default: "δ ≤ def" shows "poly_order_carrier def (delta_gt δ) (1 ≤ δ) False" proof - from delta_interpretation[OF dpos default] interpret SN_strict_mono_ordered_semiring_1 "def" "delta_gt δ" delta_mono . interpret poly_order_carrier "def" "delta_gt δ" False False proof(unfold_locales) fix y z x :: 'a assume gt: "delta_gt δ y z" and ge: "x ≥ 1" from ge have ge: "x ≥ 0" and m: "delta_mono x" unfolding delta_mono_def by auto show "delta_gt δ (y * x) (z * x)" using mono[OF m gt ge] by (auto simp: field_simps) next fix x y :: 'a and n :: nat assume False thus "delta_gt δ (x ^ n) (y ^ n)" .. next fix x y :: 'a assume False thus "∃ k. x = ((+) 1 ^^ k) y" by simp qed show ?thesis proof(unfold_locales) fix x y :: 'a and n :: nat assume one: "1 ≤ δ" and gt: "delta_gt δ x y" and y: "y ≥ 0" and n: "1 ≤ n" then obtain p where n: "n = Suc p" and x: "x ≥ 1" and y2: "0 ≤ y" and xy: "x ≥ y" by (cases n, auto simp: delta_gt_def) show "delta_gt δ (x ^ n) (y ^ n)" proof (simp only: n, induct p, simp add: gt) case (Suc p) from times_gt_mono[OF this x] have one: "delta_gt δ (x ^ Suc (Suc p)) (x * y ^ Suc p)" by (auto simp: field_simps) also have "… ≥ y * y ^ Suc p" by (rule times_left_mono[OF _ xy], auto simp: zero_le_power[OF y2, of "Suc p", simplified]) finally show ?case by auto qed next fix x y :: 'a assume False thus "∃ k. x = ((+) 1 ^^ k) y" by simp qed (rule times_gt_mono, auto) qed lemma delta_minimal_delta: assumes "⋀ x y. (x,y) ∈ set xys ⟹ x > y" shows "∃ δ > 0. ∀ x y. (x,y) ∈ set xys ⟶ delta_gt δ x y" using assms proof (induct xys) case Nil show ?case by (rule exI[of _ 1], auto) next case (Cons xy xys) show ?case proof (cases xy) case (Pair x y) with Cons have "x > y" by auto then obtain d1 where "d1 = x - y" and d1pos: "d1 > 0" and "d1 ≤ x - y" by auto hence xy: "delta_gt d1 x y" unfolding delta_gt_def by auto from Cons obtain d2 where d2pos: "d2 > 0" and xys: "∀ x y. (x, y) ∈ set xys ⟶ delta_gt d2 x y" by auto obtain d where d: "d = min d1 d2" by auto with d1pos d2pos xy have dpos: "d > 0" and "delta_gt d x y" unfolding delta_gt_def by auto with xys d Pair have "∀ x y. (x,y) ∈ set (xy # xys) ⟶ delta_gt d x y" unfolding delta_gt_def by force with dpos show ?thesis by auto qed qed interpretation weak_delta_SN: weak_SN_strict_mono_ordered_semiring_1 "(>)" 1 delta_mono proof fix xysp :: "('a × 'a) list" assume orient: "∀ x y. (x,y) ∈ set xysp ⟶ x > y" obtain xys where xsy: "xys = (1,0) # xysp" by auto with orient have "⋀ x y. (x,y) ∈ set xys ⟹ x > y" by auto with delta_minimal_delta have "∃ δ > 0. ∀ x y. (x,y) ∈ set xys ⟶ delta_gt δ x y" by auto then obtain δ where dpos: "δ > 0" and orient: "⋀ x y. (x,y) ∈ set xys ⟹ delta_gt δ x y" by auto from orient have orient1: "∀ x y. (x,y) ∈ set xysp ⟶ delta_gt δ x y" and orient2: "delta_gt δ 1 0" unfolding xsy by auto from orient2 have oned: "δ ≤ 1" unfolding delta_gt_def by auto show " ∃gt. SN_strict_mono_ordered_semiring_1 1 gt delta_mono ∧ (∀x y. (x, y) ∈ set xysp ⟶ gt x y)" by (intro exI conjI, rule delta_interpretation[OF dpos oned], rule orient1) qed subsection ‹The standard semiring over the integers› definition int_mono :: "int ⇒ bool" where "int_mono x ≡ x ≥ 1" instantiation int :: large_ordered_semiring_1 begin instance proof fix y :: int show "∃ x. of_nat x ≥ y" by (rule exI[of _ "nat y"], simp) qed (auto simp: mult_right_mono mult_left_mono mult_right_mono_neg) end lemma non_inf_int_gt: "non_inf {(a,b :: int) . a > b}" (is "non_inf ?r") by (rule non_inf_image[OF non_inf_delta_gt, of 1 _ rat_of_int], auto simp: delta_gt_def) interpretation int_SN: SN_strict_mono_ordered_semiring_1 1 "(>) :: int ⇒ int ⇒ bool" int_mono proof (unfold_locales) have [simp]: "⋀ x :: int . (-1 < x) = (0 ≤ x)" by auto show "SN {(x,y). y ≥ 0 ∧ (y :: int) < x}" using non_inf_imp_SN_bound[OF non_inf_int_gt, of "-1"] by auto qed (auto simp: mult_strict_left_mono int_mono_def) interpretation int_poly: poly_order_carrier 1 "(>) :: int ⇒ int ⇒ bool" True discrete proof (unfold_locales) fix x y :: int assume ge: "x ≥ y" then obtain k where k: "x - y = k" and kp: "0 ≤ k" by auto then obtain nk where nk: "nk = nat k" and k: "x - y = int nk" by auto show "∃ k. x = ((+) 1 ^^ k) y" proof (rule exI[of _ nk]) from k have "x = int nk + y" by simp also have "… = ((+) 1 ^^ nk) y" by (induct nk, auto) finally show "x = ((+) 1 ^^ nk) y" . qed qed (auto simp: field_simps power_strict_mono) subsection ‹The arctic semiring over the integers› text ‹plus is interpreted as max, times is interpreted as plus, 0 is -infinity, 1 is 0› datatype arctic = MinInfty | Num_arc int instantiation arctic :: ord begin fun less_eq_arctic :: "arctic ⇒ arctic ⇒ bool" where "less_eq_arctic MinInfty x = True" | "less_eq_arctic (Num_arc _) MinInfty = False" | "less_eq_arctic (Num_arc y) (Num_arc x) = (y ≤ x)" fun less_arctic :: "arctic ⇒ arctic ⇒ bool" where "less_arctic MinInfty x = True" | "less_arctic (Num_arc _) MinInfty = False" | "less_arctic (Num_arc y) (Num_arc x) = (y < x)" instance .. end instantiation arctic :: ordered_semiring_1 begin fun plus_arctic :: "arctic ⇒ arctic ⇒ arctic" where "plus_arctic MinInfty y = y" | "plus_arctic x MinInfty = x" | "plus_arctic (Num_arc x) (Num_arc y) = (Num_arc (max x y))" fun times_arctic :: "arctic ⇒ arctic ⇒ arctic" where "times_arctic MinInfty y = MinInfty" | "times_arctic x MinInfty = MinInfty" | "times_arctic (Num_arc x) (Num_arc y) = (Num_arc (x + y))" definition zero_arctic :: arctic where "zero_arctic = MinInfty" definition one_arctic :: arctic where "one_arctic = Num_arc 0" instance proof fix x y z :: arctic show "x + y = y + x" by (cases x, cases y, auto, cases y, auto) show "(x + y) + z = x + (y + z)" by (cases x, auto, cases y, auto, cases z, auto) show "(x * y) * z = x * (y * z)" by (cases x, auto, cases y, auto, cases z, auto) show "x * 0 = 0" by (cases x, auto simp: zero_arctic_def) show "x * (y + z) = x * y + x * z" by (cases x, auto, cases y, auto, cases z, auto) show "(x + y) * z = x * z + y * z" by (cases x, auto, cases y, cases z, auto, cases z, auto) show "1 * x = x" by (cases x, simp_all add: one_arctic_def) show "x * 1 = x" by (cases x, simp_all add: one_arctic_def) show "0 + x = x" by (simp add: zero_arctic_def) show "0 * x = 0" by (simp add: zero_arctic_def) show "(0 :: arctic) ≠ 1" by (simp add: zero_arctic_def one_arctic_def) show "x + 0 = x" by (cases x, auto simp: zero_arctic_def) show "x ≥ x" by (cases x, auto) show "(1 :: arctic) ≥ 0" by (simp add: zero_arctic_def one_arctic_def) show "max x y = max y x" unfolding max_def by (cases x, (cases y, auto)+) show "max x y ≥ x" unfolding max_def by (cases x, (cases y, auto)+) assume ge: "x ≥ y" from ge show "x + z ≥ y + z" by (cases x, cases y, cases z, auto, cases y, cases z, auto, cases z, auto) from ge show "x * z ≥ y * z" by (cases x, cases y, cases z, auto, cases y, cases z, auto, cases z, auto) from ge show "max x y = x" unfolding max_def by (cases x, (cases y, auto)+) from ge show "max z x ≥ max z y" unfolding max_def by (cases z, cases x, auto, cases x, (cases y, auto)+) next fix x y z :: arctic assume "x ≥ y" and "y ≥ z" thus "x ≥ z" by (cases x, cases y, auto, cases y, cases z, auto, cases z, auto) next fix x y z :: arctic assume "y ≥ z" thus "x * y ≥ x * z" by (cases x, cases y, cases z, auto, cases y, cases z, auto, cases z, auto) next fix x y z :: arctic show "x ≥ y ⟹ 0 ≥ z ⟹ y * z ≥ x * z" by (cases z, cases x, auto simp: zero_arctic_def) qed end fun get_arctic_num :: "arctic ⇒ int" where "get_arctic_num (Num_arc n) = n" fun pos_arctic :: "arctic ⇒ bool" where "pos_arctic MinInfty = False" | "pos_arctic (Num_arc n) = (0 <= n)" interpretation arctic_SN: SN_both_mono_ordered_semiring_1 1 "(>)" pos_arctic proof fix x y z :: arctic assume "x ≥ y" and "y > z" thus "x > z" by (cases z, simp, cases y, simp, cases x, auto) next fix x y z :: arctic assume "x > y" and "y ≥ z" thus "x > z" by (cases z, simp, cases y, simp, cases x, auto) next fix x y z :: arctic assume "x > y" thus "x ≥ y" by (cases x, (cases y, auto)+) next fix x y z u :: arctic assume "x > y" and "z > u" thus "x + z > y + u" by (cases y, cases u, simp, cases z, auto, cases x, auto, cases u, auto, cases z, auto, cases x, auto, cases x, auto, cases z, auto, cases x, auto) next fix x y z :: arctic assume "x > y" thus "x * z > y * z" by (cases y, simp, cases z, simp, cases x, auto) next fix x :: arctic assume "0 > x" thus "x = 0" by (cases x, auto simp: zero_arctic_def) next fix x :: arctic show "pos_arctic 1" unfolding one_arctic_def by simp show "x > 0" unfolding zero_arctic_def by simp show "(1 :: arctic) ≥ 0" unfolding zero_arctic_def by simp show "x ≥ 0" unfolding zero_arctic_def by simp show "¬ pos_arctic 0" unfolding zero_arctic_def by simp next fix x y assume "pos_arctic x" thus "pos_arctic (x + y)" by (cases x, simp, cases y, auto) next fix x y assume "pos_arctic x" and "pos_arctic y" thus "pos_arctic (x * y)" by (cases x, simp, cases y, auto) next show "SN {(x,y). pos_arctic y ∧ x > y}" (is "SN ?rel") proof - { fix x assume "∃ f . f 0 = x ∧ (∀ i. (f i, f (Suc i)) ∈ ?rel)" from this obtain f where "f 0 = x" and seq: "∀ i. (f i, f (Suc i)) ∈ ?rel" by auto from seq have steps: "∀ i. f i > f (Suc i) ∧ pos_arctic (f (Suc i)) " by auto let ?g = "λ i. get_arctic_num (f i)" have "∀ i. ?g (Suc i) ≥ 0 ∧ ?g i > ?g (Suc i)" proof fix i from steps have i: "f i > f (Suc i) ∧ pos_arctic (f (Suc i))" by auto from i obtain n where fi: "f i = Num_arc n" by (cases "f (Suc i)", simp, cases "f i", auto) from i obtain m where fsi: "f (Suc i) = Num_arc m" by (cases "f (Suc i)", auto) with i have gz: "0 ≤ m" by simp from i fi fsi have "n > m" by auto with fi fsi gz show "?g (Suc i) ≥ 0 ∧ ?g i > ?g (Suc i)" by auto qed from this obtain g where "∀ i. g (Suc i) ≥ 0 ∧ ((>) :: int ⇒ int ⇒ bool) (g i) (g (Suc i))" by auto hence "∃ f. f 0 = g 0 ∧ (∀ i. (f i, f (Suc i)) ∈ {(x,y). y ≥ 0 ∧ x > y})" by auto with int_SN.SN have False unfolding SN_defs by auto } thus ?thesis unfolding SN_defs by auto qed next fix y z x :: arctic assume "y > z" thus "x * y > x * z" by (cases x, simp, cases z, simp, cases y, auto) next fix c d assume "pos_arctic d" then obtain n where d: "d = Num_arc n" and n: "0 ≤ n" by (cases d, auto) show "∃ e. e ≥ 0 ∧ pos_arctic e ∧ ¬ c ≥ d * e" proof (cases c) case MinInfty show ?thesis by (rule exI[of _ "Num_arc 0"], unfold d MinInfty zero_arctic_def, simp) next case (Num_arc m) show ?thesis by (rule exI[of _ "Num_arc (abs m + 1)"], insert n, unfold d Num_arc zero_arctic_def, simp) qed qed subsection ‹The arctic semiring over an arbitrary archimedean field› text ‹completely analogous to the integers, where one has to use delta-orderings›