theory Matrix_Poly
imports
"Abstract-Rewriting.SN_Order_Carrier"
Jordan_Normal_Form.Matrix_Complexity
Show.Show_Instances
Linear_Poly_Order
Jordan_Normal_Form_Complexity_Approximation
Poly_Order
begin
subsection ‹Standard linear polynomial interpretations›
text ‹We can take standard linear polynomials using +, *, ... from type class
as carrier operations.›
definition class_complexity :: "'a :: ordered_semiring_1 ⇒ nat ⇒ shows check"
where
"class_complexity a deg = (check (a ≤ 1) (shows ''value is larger than 1''))"
definition
class_lpoly_order ::
"'a :: ordered_semiring_1 ⇒ ('a ⇒ bool) ⇒ ('a :: ordered_semiring_1 ⇒ 'a ⇒ bool) ⇒
'a lpoly_order_semiring"
where
"class_lpoly_order def mon gtt = class_ordered_semiring (TYPE('a)) gtt ⦇
plus_single_mono = True,
default = def,
arcpos = (λ _. True),
checkmono = mon,
bound = (λ _. 0), (* does not matter, will be overwritten *)
check_complexity = class_complexity,
description = ''polynomial interpretation''
⦈"
lemma class_lpoly_order:
fixes d :: "'a :: {show, large_real_ordered_semiring_1}"
and check_carrier :: "shows check"
assumes check_carrier: "isOK check_carrier ⟹ weak_complexity_linear_poly_order_carrier weak_gt d mon"
shows "linear_poly_order_impl (class_lpoly_order d mon (weak_gt :: 'a ⇒ 'a ⇒ bool)) (check_carrier)"
proof
note class_mono = times_left_mono times_right_mono
fix I :: "('f, 'a) lpoly_interL" and as :: "('a × 'a) list"
assume check: "isOK check_carrier"
interpret weak_complexity_linear_poly_order_carrier weak_gt d mon by (rule check_carrier[OF check])
let ?as = "filter (λ (a, b). weak_gt a b) as :: ('a × 'a) list"
have "∀ m1 m2. (m1, m2) ∈ set ?as ⟶ weak_gt m1 m2" by auto
from weak_gt_mono[of ?as, OF this] obtain gt bnd
where mono: "mono_matrix_carrier gt d bnd mon" and
weak_gt: "⋀ m1 m2. (m1, m2) ∈ set ?as ⟹ gt m1 m2" by auto
interpret mono_matrix_carrier gt d bnd mon by fact
let ?gt = gt
let ?bnd = bnd
let ?mono = mon
note d = class_lpoly_order_def class_ordered_semiring_def class_semiring_def
let ?D = "class_lpoly_order d mon weak_gt"
let ?C = "?D⦇gt := ?gt, bound := ?bnd⦈"
from class_ordered_semiring[of "⦇
plus_single_mono = True,
default = d,
arcpos = (λ _. True),
checkmono = ?mono,
bound = ?bnd,
check_complexity = class_complexity,
description = ''polynomial interpretation''⦈"]
interpret ordered_semiring ?C
unfolding d by simp
interpret lpoly_order ?C
by (unfold_locales, unfold d, auto intro:
SN default_ge_zero plus_gt_left_mono plus_gt_both_mono)
have lpoly_order: "lpoly_order ?C" by fact
show "∃gta bnd.
lpoly_order (?D⦇gt := gta, bound := bnd⦈) ∧
(∀(a, b)∈set as. a ∈ carrier ?D ⟶ b ∈ carrier ?D ⟶
a ≻⇘?D⇙ b ⟶ gta a b) ∧
(psm⇘?D⇙ ⟶ complexity_linear_poly_order_carrier (?D⦇gt := gta, bound := bnd⦈))"
proof (intro exI conjI impI, rule lpoly_order)
show "∀(a, b)∈set as. a ∈ carrier ?D ⟶ b ∈ carrier ?D ⟶
a ≻⇘?D⇙ b ⟶ ?gt a b" using weak_gt unfolding d by auto
{
fix bc bcv bd :: 'a and deg
assume bc0: "bc ≥ 0" and bcv0: "bcv ≥ 0" and bd0: "bd ≥ 0"
and comp: "isOK(class_complexity bc deg)"
from comp[unfolded class_complexity_def]
have bc1: "bc ≤ 1" by (auto split: if_splits)
let ?b = "bnd (bcv * bd)"
let ?g = "λ _ :: nat. ?b"
have mono: "⋀ g. g ∈ O_of (Comp_Poly 0) ⟹ g ∈ O_of (Comp_Poly deg)"
using O_of_poly_mono_deg[of 0 deg] by auto
have "∃g. g ∈ O_of (Comp_Poly deg) ∧
(∀n. bnd (bcv * (bd * bc (^)⇘?C⇙ n)) ≤ g n)"
proof (intro exI[of _ ?g] conjI allI, rule mono, rule O_of_polyI[of _ 0 _ ?b], simp)
fix n :: nat
have id: "bc (^)⇘?C⇙ n = bc ^ n"
by (induct n, unfold nat_pow_0 nat_pow_Suc, auto simp: field_simps d)
have "… ≤ 1"
proof (induct n)
case 0
show ?case by (simp add: ge_refl)
next
case (Suc n)
from ge_trans[OF class_mono(2)[OF one_ge_zero bc1] class_mono(1)[OF bc0 Suc]]
show ?case by (simp add: field_simps)
qed
from class_mono(2)[OF _ this, of "bcv * bd"]
have "bcv * (bd * bc ^ n) ≤ bcv * bd" using bcv0 bd0 by (auto simp: field_simps)
from bound_mono[OF this]
show "bnd (bcv * (bd * bc (^)⇘?C⇙ n)) ≤ ?b" unfolding id .
qed
} note main = this
show "complexity_linear_poly_order_carrier ?C"
by (unfold_locales, insert main, unfold d, auto simp: field_simps intro: bound_mono bound_plus default_gt_zero bound mono)
qed
qed
subsection ‹Arctic linear polynomial interpretations›
text ‹We can take arctic operations from type class as carrier operations.›
definition class_arc_complexity :: "'a ⇒ nat ⇒ shows check"
where
"class_arc_complexity a deg = error (shows ''complexity for arctic semirings not supported'')"
definition
class_arc_lpoly_order ::
"'a :: ordered_semiring_1 ⇒ ('a ⇒ bool) ⇒ ('a :: ordered_semiring_1 ⇒ 'a ⇒ bool) ⇒
'a lpoly_order_semiring"
where
"class_arc_lpoly_order def apos gtt = class_ordered_semiring (TYPE('a)) gtt ⦇
plus_single_mono = False,
default = def,
arcpos = apos,
checkmono = (λ _. False),
bound = (λ _. 0),
check_complexity = class_arc_complexity,
description = ''polynomial interpretation over arctic semiring''
⦈"
lemma class_arc_lpoly_order:
fixes d :: "'a :: {show, ordered_semiring_1}"
assumes "weak_SN_both_mono_ordered_semiring_1 weak_gt d arc_pos"
shows "linear_poly_order_impl (class_arc_lpoly_order d arc_pos (weak_gt :: 'a ⇒ 'a ⇒ bool)) check_carrier"
proof
fix I :: "('f, 'a) lpoly_interL" and as :: "('a × 'a) list"
interpret weak_SN_both_mono_ordered_semiring_1 weak_gt d arc_pos by fact
let ?as = "filter (λ (a, b). weak_gt a b) as :: ('a × 'a) list"
have "∀ m1 m2. (m1, m2) ∈ set ?as ⟶ weak_gt m1 m2" by auto
from weak_gt_both_mono[of ?as, OF this] obtain gt
where mono: "SN_both_mono_ordered_semiring_1 d gt arc_pos" and
weak_gt: "⋀ m1 m2. (m1, m2) ∈ set ?as ⟹ gt m1 m2" by auto
interpret SN_both_mono_ordered_semiring_1 d gt arc_pos by fact
note [simp] = gt_imp_ge[OF zero_leastI]
let ?gt = gt
let ?bnd = "λ _ :: 'a. 0"
let ?mono = "λ _. False"
note d = class_arc_lpoly_order_def class_ordered_semiring_def class_semiring_def
let ?D = "class_arc_lpoly_order d arc_pos weak_gt"
let ?C = "?D⦇gt := ?gt, bound := ?bnd⦈"
from class_ordered_semiring[of "⦇
plus_single_mono = False,
default = d,
arcpos = arc_pos,
checkmono = ?mono,
bound = ?bnd,
check_complexity = class_arc_complexity,
description = ''polynomial interpretation over arctic semiring''⦈"]
interpret ordered_semiring ?C
unfolding d by simp
interpret lpoly_order ?C
by (unfold_locales, unfold d, insert SN not_all_ge, auto simp: arc_pos_zero max0_id intro:
default_ge_zero plus_gt_both_mono arc_pos_one arc_pos_default
arc_pos_plus arc_pos_mult not_all_ge zero_leastI zero_leastII zero_leastIII
times_gt_left_mono times_gt_right_mono)
have lpoly_order: "lpoly_order ?C" by fact
show "∃gta bnd.
lpoly_order (?D⦇gt := gta, bound := bnd⦈) ∧
(∀(a, b)∈set as. a ∈ carrier ?D ⟶ b ∈ carrier ?D ⟶
a ≻⇘?D⇙ b ⟶ gta a b) ∧
(psm⇘?D⇙ ⟶ complexity_linear_poly_order_carrier (?D⦇gt := gta, bound := bnd⦈))"
proof (intro exI conjI impI, rule lpoly_order)
show "∀(a, b)∈set as. a ∈ carrier ?D ⟶ b ∈ carrier ?D ⟶
a ≻⇘?D⇙ b ⟶ ?gt a b" using weak_gt unfolding d by auto
qed (auto simp: d)
qed
subsection ‹Matrix interpretations›
text ‹We can take standard matrix operations as carrier operations.›
definition mat_complexity :: "nat ⇒ 'a :: large_real_ordered_semiring_1 mat ⇒ nat ⇒ shows check"
where
"mat_complexity n M d ≡ mat_estimate_complexity_jb (Suc d) M"
definition
mat_lpoly_order ::
"nat ⇒ nat ⇒ 'a :: large_real_ordered_semiring_1 ⇒ ('a ⇒ bool) ⇒
('a ⇒ 'a ⇒ bool) ⇒
('a mat) lpoly_order_semiring"
where
"mat_lpoly_order n sd def mon gtt = mat_ordered_semiring n sd gtt ⦇
plus_single_mono = True,
default = mat_default def n,
arcpos = (λ _. True),
checkmono = mat_mono mon sd,
bound = (λ _. 0), (* does not matter, will be overwritten *)
check_complexity = mat_complexity n,
description = ''matrix interpretation''
⦈"
definition check_dimensions :: "nat ⇒ nat ⇒ shows check ⇒ shows check"
where
"check_dimensions n sd c = do {
c;
check (sd ≤ n ∧ sd > 0)
(shows ''strict dimension must be at least 1 and less than total dimension'')
}"
lemma mat_lpoly_order:
fixes d :: "'a :: {show, large_real_ordered_semiring_1}"
and check_carrier :: "shows check"
assumes check_carrier: "isOK (check_carrier) ⟹ weak_complexity_linear_poly_order_carrier weak_gt d mon"
shows "linear_poly_order_impl (mat_lpoly_order n sd d mon (weak_gt :: 'a ⇒ 'a ⇒ bool)) (check_dimensions n sd check_carrier)"
proof
fix I :: "('f, 'a mat) lpoly_interL" and as :: "('a mat × 'a mat) list"
assume check: "isOK (check_dimensions n sd check_carrier)"
note check = check[unfolded check_dimensions_def, simplified]
from check have sd_n: "sd ≤ n" and sd_pos: "sd > 0" and check: "isOK(check_carrier)" by auto
interpret weak_complexity_linear_poly_order_carrier weak_gt d mon by (rule check_carrier[OF check])
let ?as = "filter (λ (a,b). weak_mat_gt sd a b) as :: ('a mat × 'a mat) list"
have "⋀m1 m2.
m1 ∈ carrier_mat n n ⟹ m2 ∈ carrier_mat n n ⟹ (m1, m2) ∈ set ?as ⟹
weak_mat_gt sd m1 m2" by auto
from weak_mat_gt_mono[OF sd_n, of ?as, OF this] obtain gt bnd
where mono: "mono_matrix_carrier gt d bnd mon" and
weak_gt: "⋀ m1 m2. m1 ∈ carrier_mat n n ⟹ m2 ∈ carrier_mat n n ⟹ (m1, m2) ∈ set ?as ⟹
mat_gt gt sd m1 m2" by blast
interpret mono_matrix_carrier gt d bnd mon by fact
let ?gt = "mat_gt gt sd"
let ?bnd = "λ m :: 'a mat. bnd (sum_mat m)"
let ?mono = "mat_mono mon sd"
note d = mat_lpoly_order_def mat_ordered_semiring_def ring_mat_def
let ?D = "mat_lpoly_order n sd d mon weak_gt"
let ?C = "?D⦇gt := ?gt, bound := ?bnd⦈"
from mat_ordered_semiring[OF sd_n, of "⦇
plus_single_mono = True,
default = default⇩m d n,
arcpos = (λ _. True),
checkmono = ?mono,
bound = ?bnd,
check_complexity = mat_complexity n,
description = ''matrix interpretation''⦈"]
interpret ordered_semiring ?C
unfolding d by simp
interpret lpoly_order ?C
by (unfold_locales, unfold d, insert mat_gt_SN[OF sd_n],
auto intro: mat_default_ge_0
mat_plus_gt_left_mono[OF sd_n]
mat_gt_ge_mono[OF sd_n])
have lpoly_order: "lpoly_order ?C" by fact
show "∃gta bnd.
lpoly_order (?D⦇gt := gta, bound := bnd⦈) ∧
(∀(a, b)∈set as. a ∈ carrier ?D ⟶ b ∈ carrier ?D ⟶
a ≻⇘?D⇙ b ⟶ gta a b) ∧
(psm⇘?D⇙ ⟶ complexity_linear_poly_order_carrier (?D⦇gt := gta, bound := bnd⦈))"
proof (intro exI conjI impI, rule lpoly_order)
show "∀(a, b)∈set as. a ∈ carrier ?D ⟶ b ∈ carrier ?D ⟶
a ≻⇘?D⇙ b ⟶ ?gt a b" using weak_gt unfolding d by auto
next
{
fix bc bcv bd :: "'a mat" and deg
assume bc: "bc ∈ carrier_mat n n" and bcv: "bcv ∈ carrier_mat n n" and bd: "bd ∈ carrier_mat n n"
and bc0: "bc ≥⇩m 0⇩m n n" and bcv0: "bcv ≥⇩m 0⇩m n n" and bd0: "bd ≥⇩m 0⇩m n n"
and comp: "isOK(mat_complexity n bc deg)"
let ?b = "λ nn. bnd (sum_mat (bd * ((bc ^⇩m nn) * bcv)))"
from comp[unfolded mat_complexity_def]
have ok: "isOK(mat_estimate_complexity_jb (Suc deg) bc)" by auto
from mat_estimate_complexity_jb_sum_mat_prod[OF ok bc bd bcv refl] obtain c where
bnd: "⋀ k. k > 0 ⟹ sum_mat (bd * (bc ^⇩m k * bcv)) ≤ c * of_nat k ^ deg" by auto
{
fix k
assume "k > (0 :: nat)"
from bound_mono[OF bnd[OF this]] have "?b k ≤ bnd (c * of_nat k ^ deg)" by auto
also have "… ≤ bnd c * of_nat k ^ deg"
by (rule bound_pow_of_nat)
finally have "?b k ≤ bnd c * of_nat k ^ deg" .
}
then obtain c where main: "⋀ k. k > 0 ⟹ ?b k ≤ c * k ^ deg" by auto
let ?gp = "λ nn. c * nn ^ deg"
let ?g = "λ nn. ?gp nn + ?b 0"
{
fix n
have "?b n ≤ ?g n"
proof (cases n)
case (Suc m)
hence "n > 0" by simp
from main[OF this] show ?thesis by simp
qed auto
}
hence main: "∀ nn. ?b nn ≤ ?g nn" by auto
have deg: "?g ∈ O_of (Comp_Poly deg)"
by (rule O_of_polyI[of _ c _ "?b 0"], simp)
have "∃g. g ∈ O_of (Comp_Poly deg) ∧
(∀na. bnd (sum_mat (bd * (bc (^)⇘?C⇙ na * bcv))) ≤ g na)"
by (intro exI conjI, rule deg, insert main,
unfold pow_mat_ring_pow[OF bc, of _ ?C],
unfold d nat_pow_def, auto)
} note main1 = this
{
fix m :: "'a mat"
let ?m = "λ x. (x :: 'a mat) ∈ carrier_mat n n"
let ?R = "{(x,y). ?m x ∧ ?m y ∧ y ≥⇩m 0⇩m n n ∧ mat_gt gt sd x y}"
let ?f = "λ m. sum_mat m"
let ?fR = "{(x,y). y ≥ 0 ∧ gt x y}"
{
fix x y
assume "(x,y) ∈ ?R"
hence x: "?m x" and y: "?m y" and ge: "y ≥⇩m 0⇩m n n" and gt: "mat_gt gt sd x y" by auto
from sum_mat_mono_gt[OF sd_n x y gt] sum_mat_mono[OF y _ ge]
have "(?f x, ?f y) ∈ ?fR" by simp
} note step = this
have "deriv_bound ?R m (?bnd m)"
by (rule deriv_bound_image[of _ sum_mat, OF bound], insert step, auto)
} note main2 = this
show "complexity_linear_poly_order_carrier ?C"
by (unfold_locales, insert main1 main2, unfold d, auto simp: sum_mat_add
intro:
mat_default_gt_mat0[OF sd_pos sd_n] mat_mono[OF sd_n]
bound_plus bound_mono[OF sum_mat_mono])
qed
qed
subsection ‹Arctic matrix interpretations›
text ‹We can take arctic matrix operations as carrier operations.›
definition mat_arc_complexity :: "'a ⇒ nat ⇒ shows check"
where
"mat_arc_complexity m deg = error (shows ''complexity for arctic matrices not supported'')"
definition
mat_arc_lpoly_order ::
"nat ⇒ 'a :: ordered_semiring_1 ⇒ ('a ⇒ bool) ⇒ ('a :: ordered_semiring_1 ⇒ 'a ⇒ bool) ⇒
('a mat) lpoly_order_semiring"
where
"mat_arc_lpoly_order n def apos gtt = mat_both_ordered_semiring n gtt ⦇
plus_single_mono = False,
default = mat_default def n,
arcpos = mat_arc_posI apos,
checkmono = (λ _. False),
bound = (λ _. 0),
check_complexity = mat_arc_complexity,
description = ''arctic matrix interpretation''
⦈"
definition check_arc_dimension :: "nat ⇒ shows check"
where
"check_arc_dimension n = check (n > 0) (shows ''dimension must be at least 1'')"
lemma mat_arc_lpoly_order:
fixes default :: "'a :: {show, ordered_semiring_1}"
assumes "weak_SN_both_mono_ordered_semiring_1 weak_gt default arc_pos"
shows "linear_poly_order_impl (mat_arc_lpoly_order n default arc_pos weak_gt) (check_arc_dimension n)"
proof
fix as :: "('a mat × 'a mat) list"
assume check: "isOK (check_arc_dimension n)"
note check = check[unfolded check_arc_dimension_def, simplified]
from check have n_pos: "n > 0" by simp
interpret weak_SN_both_mono_ordered_semiring_1 weak_gt default arc_pos by fact
let ?as = "filter (λ (A,B). A ∈ carrier_mat n n ∧ B ∈ carrier_mat n n ∧ weak_mat_gt_arc A B) as"
have AB': "set ?as ⊆ carrier_mat n n × carrier_mat n n" by auto
have "∀(A,B) ∈ set ?as. weak_mat_gt_arc A B" by auto
from weak_mat_gt_both_mono[OF AB']
obtain gt
where mono: "SN_both_mono_ordered_semiring_1 default gt arc_pos"
and weak_gt: "∀(A,B) ∈ set ?as. mat_comp_all gt A B" by auto
interpret SN_both_mono_ordered_semiring_1 default gt arc_pos by fact
let ?gt = "mat_comp_all gt"
let ?bnd = "λ m. 0"
note d = mat_arc_lpoly_order_def
mat_both_ordered_semiring_def ring_mat_def lpoly_order_semiring.simps
partial_object.simps ordered_semiring.simps
let ?D = "mat_arc_lpoly_order n default arc_pos weak_gt"
let ?C = "?D⦇gt := ?gt, bound := ?bnd⦈"
from mat_both_ordered_semiring[OF n_pos, of "⦇
plus_single_mono = False,
default = mat_default default n,
arcpos = mat_arc_pos,
checkmono = (λ _. False),
bound = ?bnd,
check_complexity = mat_arc_complexity,
description = ''arctic matrix interpretation''⦈"]
interpret ordered_semiring ?C
unfolding d by (simp add: mat_ordered_semiring_def ring_mat_def)
{
fix m :: "'a mat"
assume m: "m ∈ carrier_mat n n"
note mat_max_id[OF mat0_leastIII[OF this] this zero_carrier_mat]
} note mat_max[simp] = this
interpret lpoly_order ?C
by (unfold_locales, unfold d,
auto simp: mat_arc_pos_zero[OF n_pos] mat_max_0_id
intro: mat_gt_arc_plus_mono mat_gt_arc_mult_left_mono
mat_gt_arc_mult_right_mono mat0_leastI mat0_leastII
SN_subset[OF mat_gt_arc_SN[OF n_pos]] mat_default_ge_0
mat_arc_pos_plus[OF n_pos] mat_arc_pos_mult[OF n_pos]
mat_arc_pos_mat_default[OF n_pos] mat_arc_pos_one[OF n_pos]
mat_not_all_ge[OF n_pos])
have lpoly_order: "lpoly_order ?C" by fact
show "∃gta bnd.
lpoly_order (?D⦇gt := gta, bound := bnd⦈) ∧
(∀(a, b)∈set as. a ∈ carrier ?D ⟶ b ∈ carrier ?D ⟶
a ≻⇘?D⇙ b ⟶ gta a b) ∧
(psm⇘?D⇙ ⟶ complexity_linear_poly_order_carrier (?D⦇gt := gta, bound := bnd⦈))"
apply (intro exI conjI impI ballI2)
apply (rule lpoly_order)
unfolding d using weak_gt by auto
qed
abbreviation int_mat_redtriple where
"int_mat_redtriple n sd ≡
create_poly_redtriple (mat_lpoly_order n sd 1 int_mono (λx y. y < x))
(check_dimensions n sd succeed)"
abbreviation int_redtriple where
"int_redtriple ≡
create_poly_redtriple (class_lpoly_order 1 int_mono (λx y. y < x))
succeed"
lemma int_mat_redtriple:
"generic_redtriple_impl (int_mat_redtriple n sd)"
by (rule create_poly_redtriple[OF mat_lpoly_order[OF int_weak_complexity]])
lemma int_redtriple:
"generic_redtriple_impl (int_redtriple)"
by (rule create_poly_redtriple[OF class_lpoly_order[OF int_weak_complexity]])
lemma delta_cpx_poly_order_carrier:
fixes d :: "'a :: {show, large_real_ordered_semiring_1, floor_ceiling}"
assumes d: "d > 0"
shows "cpx_poly_order_carrier d (delta_gt d) (1 ≤ d) False (delta_bound d)"
proof -
let ?nat = "delta_bound d"
from delta_complexity[OF d] have "mono_matrix_carrier (delta_gt d) d ?nat delta_mono" by simp
interpret mono_matrix_carrier "delta_gt d" d ?nat delta_mono by fact
from delta_poly[OF d] have "poly_order_carrier d (delta_gt d) (1 ≤ d) False" by simp
interpret poly_order_carrier d "delta_gt d" "1 ≤ d" False by fact
show ?thesis ..
qed
lemma delta_non_inf_poly_order_carrier:
fixes d :: "'a :: {show, large_real_ordered_semiring_1, floor_ceiling}"
assumes d: "d > 0"
shows "non_inf_poly_order_carrier d (delta_gt d) (1 ≤ d) False"
proof -
interpret cpx_poly_order_carrier d "delta_gt d" "1 ≤ d" False "delta_bound d"
by (rule delta_cpx_poly_order_carrier[OF d])
show ?thesis
by (unfold_locales, insert non_inf_delta_gt[OF d], auto simp: mult_right_mono_neg delta_gt_def)
qed
definition
check_def_pos: "check_def_pos d = check (d > 0) (shows ''default value must be positive'')"
lemma delta_weak_complexity:
assumes d0: "isOK(check_def_pos def)"
shows "weak_complexity_linear_poly_order_carrier op > def delta_mono"
by (rule delta_weak_complexity_carrier, insert d0, auto simp: check_def_pos)
abbreviation delta_mat_redtriple where
"delta_mat_redtriple n sd d ≡
create_poly_redtriple (mat_lpoly_order n sd d delta_mono op >)
(check_dimensions n sd (check_def_pos d))"
abbreviation delta_redtriple where
"delta_redtriple d ≡
create_poly_redtriple (class_lpoly_order d delta_mono op >)
(check_def_pos d)"
abbreviation delta_nl_redtriple where
"delta_nl_redtriple d ≡
create_nlpoly_redtriple (check_def_pos d) d (delta_gt d) (1 ≤ d) False"
abbreviation delta_non_inf_order where
"delta_non_inf_order d s ≡
create_nlpoly_non_inf_order (check_def_pos d) d (delta_gt d) (1 ≤ d) False s"
context
fixes d :: "'a :: {floor_ceiling,large_real_ordered_semiring_1,show}"
begin
lemma delta_mat_redtriple: "generic_redtriple_impl (delta_mat_redtriple n sd d)"
by (rule create_poly_redtriple[OF mat_lpoly_order[OF delta_weak_complexity]])
lemma delta_redtriple: "generic_redtriple_impl (delta_redtriple d)"
by (rule create_poly_redtriple[OF class_lpoly_order[OF delta_weak_complexity]])
lemma delta_nl_redtriple: "generic_redtriple_impl (delta_nl_redtriple d)"
by (rule poly_order_carrier_to_generic_redtriple_impl[OF delta_cpx_poly_order_carrier], simp add: check_def_pos)
lemma delta_non_inf_order: "generic_non_inf_order_impl (delta_non_inf_order d s)"
by (rule non_inf_poly_order_carrier_to_generic_non_inf_order[OF delta_non_inf_poly_order_carrier],
simp add: check_def_pos)
end
section ‹The arctic integers and rationals can be used as carrier›
abbreviation arctic_mat_redtriple where
"arctic_mat_redtriple n ≡
create_poly_redtriple (mat_arc_lpoly_order n 1 pos_arctic op >)
(check_arc_dimension n)"
lemma arctic_mat_redtriple: "generic_redtriple_impl (arctic_mat_redtriple n)"
by (rule create_poly_redtriple[OF mat_arc_lpoly_order[OF arctic_weak_carrier]])
abbreviation arctic_redtriple where
"arctic_redtriple ≡
create_poly_redtriple (class_arc_lpoly_order 1 pos_arctic op >)
succeed"
lemma arctic_redtriple: "generic_redtriple_impl (arctic_redtriple)"
by (rule create_poly_redtriple[OF class_arc_lpoly_order[OF arctic_weak_carrier]])
abbreviation arctic_delta_mat_redtriple where
"arctic_delta_mat_redtriple n ≡
create_poly_redtriple (mat_arc_lpoly_order n 1 pos_arctic_delta weak_gt_arctic_delta)
(check_arc_dimension n)"
lemma arctic_delta_mat_redtriple: "generic_redtriple_impl (arctic_delta_mat_redtriple n)"
by (rule create_poly_redtriple[OF mat_arc_lpoly_order[OF arctic_delta_weak_carrier]])
abbreviation arctic_delta_redtriple where
"arctic_delta_redtriple ≡
create_poly_redtriple (class_arc_lpoly_order 1 pos_arctic_delta weak_gt_arctic_delta)
succeed"
lemma arctic_delta_redtriple: "generic_redtriple_impl (arctic_delta_redtriple)"
by (rule create_poly_redtriple[OF class_arc_lpoly_order[OF arctic_delta_weak_carrier]])
end