# Theory Abstract-Rewriting.SN_Order_Carrier

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

(*
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
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"
show "0 * x = 0"
show "(0 :: arctic) ≠ 1"
show "x + 0 = x" by (cases x, auto simp: zero_arctic_def)
show "x ≥ x"
by (cases x, auto)
show "(1 :: arctic) ≥ 0"
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›

datatype 'a arctic_delta = MinInfty_delta | Num_arc_delta 'a

instantiation arctic_delta :: (ord) ord
begin
fun less_eq_arctic_delta :: "'a arctic_delta ⇒ 'a arctic_delta ⇒ bool" where
"less_eq_arctic_delta MinInfty_delta x = True"
| "less_eq_arctic_delta (Num_arc_delta _) MinInfty_delta = False"
| "less_eq_arctic_delta (Num_arc_delta y) (Num_arc_delta x) = (y ≤ x)"

fun less_arctic_delta :: "'a arctic_delta ⇒ 'a arctic_delta ⇒ bool" where
"less_arctic_delta MinInfty_delta x = True"
| "less_arctic_delta (Num_arc_delta _) MinInfty_delta = False"
| "less_arctic_delta (Num_arc_delta y) (Num_arc_delta x) = (y < x)"

instance ..
end

instantiation arctic_delta :: (linordered_field) ordered_semiring_1
begin
fun plus_arctic_delta :: "'a arctic_delta ⇒ 'a arctic_delta ⇒ 'a arctic_delta" where
"plus_arctic_delta MinInfty_delta y = y"
| "plus_arctic_delta x MinInfty_delta = x"
| "plus_arctic_delta (Num_arc_delta x) (Num_arc_delta y) = (Num_arc_delta (max x y))"

fun times_arctic_delta :: "'a arctic_delta ⇒ 'a arctic_delta ⇒ 'a arctic_delta" where
"times_arctic_delta MinInfty_delta y = MinInfty_delta"
| "times_arctic_delta x MinInfty_delta = MinInfty_delta"
| "times_arctic_delta (Num_arc_delta x) (Num_arc_delta y) = (Num_arc_delta (x + y))"

definition zero_arctic_delta :: "'a arctic_delta" where
"zero_arctic_delta = MinInfty_delta"

definition one_arctic_delta :: "'a arctic_delta" where
"one_arctic_delta = Num_arc_delta 0"

instance
proof
fix x y z :: "'a arctic_delta"
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_delta_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_delta_def)
show "x * 1 = x"
by (cases x, simp_all add: one_arctic_delta_def)
show "0 + x = x"
show "0 * x = 0"
show "(0 :: 'a arctic_delta) ≠ 1"
show "x + 0 = x" by (cases x, auto simp: zero_arctic_delta_def)
show "x ≥ x"
by (cases x, auto)
show "(1 :: 'a arctic_delta) ≥ 0"
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 :: "'a arctic_delta"
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 :: "'a arctic_delta"
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 :: "'a arctic_delta"
show "x ≥ y ⟹ 0 ≥ z ⟹ y * z ≥ x * z"
by (cases z, cases x, auto simp: zero_arctic_delta_def)
qed
end

text ‹x >d y is interpreted as y = -inf or (x,y != -inf and x >d y)›
fun gt_arctic_delta :: "'a :: floor_ceiling ⇒ 'a arctic_delta ⇒ 'a arctic_delta ⇒ bool"
where "gt_arctic_delta δ _ MinInfty_delta = True"
|  "gt_arctic_delta δ MinInfty_delta (Num_arc_delta _) = False"
|  "gt_arctic_delta δ (Num_arc_delta x) (Num_arc_delta y) = delta_gt δ x y"

fun get_arctic_delta_num :: "'a arctic_delta ⇒ 'a"
where "get_arctic_delta_num (Num_arc_delta n) = n"

fun pos_arctic_delta :: "('a :: floor_ceiling) arctic_delta ⇒ bool"
where "pos_arctic_delta MinInfty_delta = False"
| "pos_arctic_delta (Num_arc_delta n) = (0 ≤ n)"

lemma arctic_delta_interpretation: assumes dpos: "δ > 0" shows "SN_both_mono_ordered_semiring_1 1 (gt_arctic_delta δ) pos_arctic_delta"
proof -
from delta_interpretation[OF dpos] interpret SN_strict_mono_ordered_semiring_1 δ "delta_gt δ" delta_mono by simp
show ?thesis
proof
fix x y z :: "'a arctic_delta"
assume "x ≥ y" and "gt_arctic_delta δ y z"
thus "gt_arctic_delta δ x z"
by (cases z, simp, cases y, simp, cases x, simp, simp add: compat)
next
fix x y z :: "'a arctic_delta"
assume "gt_arctic_delta δ x y" and "y ≥ z"
thus "gt_arctic_delta δ x z"
by (cases z, simp, cases y, simp, cases x, simp, simp add: compat2)
next
fix x y :: "'a arctic_delta"
assume "gt_arctic_delta δ x y"
thus "x ≥ y"
by (cases x, insert dpos, (cases y, auto simp: delta_gt_def)+)
next
fix x y z u
assume "gt_arctic_delta δ x y" and "gt_arctic_delta δ z u"
thus "gt_arctic_delta δ (x + z) (y + u)"
by (cases y, cases u, simp, cases z, simp, cases x, simp, simp add: delta_gt_def,
cases z, cases x, simp, cases u, simp, simp, cases x, simp, cases z, simp, cases u, simp add: delta_gt_def, simp add: delta_gt_def)
next
fix x y z
assume "gt_arctic_delta δ x y"
thus "gt_arctic_delta δ (x * z) (y * z)"
by (cases y, simp, cases z, simp, cases x, simp, simp add: plus_gt_left_mono)
next
fix x
assume "gt_arctic_delta δ 0 x"
thus "x = 0"
by (cases x, auto simp: zero_arctic_delta_def)
next
fix x
show "pos_arctic_delta 1" unfolding one_arctic_delta_def by simp
show "gt_arctic_delta δ x 0" unfolding zero_arctic_delta_def by simp
show "(1 :: 'a arctic_delta) ≥ 0" unfolding zero_arctic_delta_def by simp
show "x ≥ 0" unfolding zero_arctic_delta_def by simp
show "¬ pos_arctic_delta 0" unfolding zero_arctic_delta_def by simp
next
fix x y :: "'a arctic_delta"
assume "pos_arctic_delta x"
thus "pos_arctic_delta (x + y)" by (cases x, simp, cases y, auto)
next
fix x y :: "'a arctic_delta"
assume "pos_arctic_delta x" and "pos_arctic_delta y"
thus "pos_arctic_delta (x * y)" by (cases x, simp, cases y, auto)
next
show "SN {(x,y). pos_arctic_delta y ∧ gt_arctic_delta δ 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. gt_arctic_delta δ (f i) (f (Suc i)) ∧ pos_arctic_delta (f (Suc i)) " by auto
let ?g = "λ i. get_arctic_delta_num (f i)"
have "∀ i. ?g (Suc i) ≥ 0 ∧ delta_gt δ (?g i) (?g (Suc i))"
proof
fix i
from steps have i: "gt_arctic_delta δ (f i) (f (Suc i)) ∧ pos_arctic_delta (f (Suc i))" by auto
from i obtain n where fi: "f i = Num_arc_delta n" by (cases "f (Suc i)", simp, cases "f i", auto)
from i obtain m where fsi: "f (Suc i) = Num_arc_delta m" by (cases "f (Suc i)", auto)
with i have gz: "0 ≤ m" by simp
from i fi fsi have "delta_gt δ n m" by auto
with fi fsi gz
show "?g (Suc i) ≥ 0 ∧ delta_gt δ (?g i) (?g (Suc i))" by auto
qed
from this obtain g where "∀ i. g (Suc i) ≥ 0 ∧ delta_gt δ (g i) (g (Suc i))" by auto
hence "∃ f. f 0 = g 0 ∧ (∀ i. (f i, f (Suc i)) ∈ {(x,y). y ≥ 0 ∧ delta_gt δ x y})" by auto
with SN have False unfolding SN_defs by auto
}
thus ?thesis unfolding SN_defs by auto
qed
next
fix c d :: "'a arctic_delta"
assume "pos_arctic_delta d"
then obtain n where d: "d = Num_arc_delta n" and n: "0 ≤ n"
by (cases d, auto)
show "∃ e. e ≥ 0 ∧ pos_arctic_delta e ∧ ¬ c ≥ d * e"
proof (cases c)
case MinInfty_delta
show ?thesis
by (rule exI[of _ "Num_arc_delta 0"],
unfold d MinInfty_delta zero_arctic_delta_def, simp)
next
case (Num_arc_delta m)
show ?thesis
by (rule exI[of _ "Num_arc_delta (abs m  + 1)"], insert n,
unfold d Num_arc_delta zero_arctic_delta_def, simp)
qed
next
fix x y z
assume gt: "gt_arctic_delta δ y z"
{
fix x y z
assume gt: "delta_gt δ y z"
have "delta_gt δ (x + y) (x + z)"
using plus_gt_left_mono[OF gt] by (auto simp: field_simps)
}
with gt show "gt_arctic_delta δ (x * y) (x * z)"
by (cases x, simp, cases z, simp, cases y, simp_all)
qed
qed

fun weak_gt_arctic_delta :: "('a :: floor_ceiling) arctic_delta ⇒ 'a arctic_delta ⇒ bool"
where "weak_gt_arctic_delta _ MinInfty_delta = True"
|  "weak_gt_arctic_delta MinInfty_delta (Num_arc_delta _) = False"
|  "weak_gt_arctic_delta (Num_arc_delta x) (Num_arc_delta y) = (x > y)"

interpretation weak_arctic_delta_SN: weak_SN_both_mono_ordered_semiring_1 weak_gt_arctic_delta 1 pos_arctic_delta
proof
fix xys
assume orient: "∀ x y. (x,y) ∈ set xys ⟶ weak_gt_arctic_delta x y"
obtain xysp where xysp: "xysp = map (λ (ax, ay). (case ax of Num_arc_delta x ⇒ x , case ay of Num_arc_delta y ⇒ y)) (filter (λ (ax,ay). ax ≠ MinInfty_delta ∧ ay ≠ MinInfty_delta) xys)"
(is "_ = map ?f _")
by auto
have "∀ x y. (x,y) ∈ set xysp ⟶ x > y"
proof (intro allI impI)
fix x y
assume "(x,y) ∈ set xysp"
with xysp obtain ax ay where "(ax,ay) ∈ set xys" and "ax ≠ MinInfty_delta" and "ay ≠ MinInfty_delta" and "(x,y) = ?f (ax,ay)" by auto
hence "(Num_arc_delta x, Num_arc_delta y) ∈ set xys" by (cases ax, simp, cases ay, auto)
with orient show "x > y" by force
qed
with delta_minimal_delta[of xysp] obtain δ where dpos: "δ > 0" and orient2: "⋀ x y. (x, y) ∈ set xysp ⟹ delta_gt δ x y" by auto
have orient: "∀ x y. (x,y) ∈ set xys ⟶ gt_arctic_delta δ x y"
proof(intro allI impI)
fix ax ay
assume axay: "(ax,ay) ∈ set xys"
with orient have orient: "weak_gt_arctic_delta ax ay" by auto
show "gt_arctic_delta δ ax ay"
proof (cases ay, simp)
case (Num_arc_delta y) note ay = this
show ?thesis
proof (cases ax)
case MinInfty_delta
with ay orient show ?thesis by auto
next
case (Num_arc_delta x) note ax = this
from ax ay axay have "(x,y) ∈ set xysp" unfolding xysp by force
from ax ay orient2[OF this] show ?thesis by simp
qed
qed
qed
show "∃gt. SN_both_mono_ordered_semiring_1 1 gt pos_arctic_delta ∧ (∀x y. (x, y) ∈ set xys ⟶ gt x y)"
by (intro exI conjI, rule arctic_delta_interpretation[OF dpos], rule orient)
qed

end
```