theory Linear_Poly_Complexity
imports
QTRS.Complexity
"Certification_Monads.Check_Monad"
"Matrix.Ordered_Semiring"
begin
record 'a lpoly_order_semiring = "'a ordered_semiring" +
plus_single_mono :: "bool" ("psmı")
default :: 'a
arcpos :: "'a ⇒ bool" ("arc'_posı")
checkmono :: "'a ⇒ bool" ("check'_monoı")
bound :: "'a ⇒ nat"
check_complexity :: "'a ⇒ nat ⇒ shows check"
description :: "string"
locale lpoly_order = ordered_semiring R for R :: "('a :: show) lpoly_order_semiring" (structure) +
assumes plus_gt_left_mono: "⟦x ≻ y; psm; x ∈ carrier R; y ∈ carrier R; z ∈ carrier R⟧ ⟹ x ⊕ z ≻ y ⊕ z"
and plus_gt_both_mono: "⟦x ≻ y; z ≻ u; x ∈ carrier R; y ∈ carrier R; z ∈ carrier R; u ∈ carrier R⟧ ⟹ x ⊕ z ≻ y ⊕ u"
and times_gt_left_mono: "⟦x ≻ y; ¬ psm; x ∈ carrier R; y ∈ carrier R; z ∈ carrier R⟧ ⟹ x ⊗ z ≻ y ⊗ z"
and times_gt_right_mono: "⟦x ≻ y; ¬ psm; x ∈ carrier R; y ∈ carrier R; z ∈ carrier R⟧ ⟹ z ⊗ x ≻ z ⊗ y"
and zero_leastI: "⟦¬ psm; x ∈ carrier R⟧ ⟹ x ≻ 𝟬"
and zero_leastII: "⟦𝟬 ≻ x; ¬ psm; x ∈ carrier R⟧ ⟹ x = 𝟬"
and SN: "SN {(x,y) . x ∈ carrier R ∧ y ∈ carrier R ∧ y ≽ 𝟬 ∧ arc_pos y ∧ x ≻ y}"
and wf_default[simp, intro]: "default R ∈ carrier R"
and default_geq_zero: "default R ≽ 𝟬"
and arc_pos_plus: "⟦arc_pos x; x ∈ carrier R; y ∈ carrier R⟧ ⟹ arc_pos (x ⊕ y)"
and arc_pos_mult: "⟦arc_pos x; arc_pos y; x ∈ carrier R; y ∈ carrier R⟧ ⟹ arc_pos (x ⊗ y)"
and arc_pos_max0: "x ∈ carrier R ⟹ arc_pos (Max 𝟬 x) = arc_pos x"
and arc_pos_default: "arc_pos (default R)"
and arc_pos_one: "arc_pos 𝟭"
and arc_pos_zero: "¬ psm ⟹ ¬ arc_pos 𝟬"
and not_all_ge: "⋀ x y. ¬ psm ⟹ x ∈ carrier R ⟹ y ∈ carrier R ⟹ arc_pos y
⟹ ∃ z. z ∈ carrier R ∧ z ≽ 𝟬 ∧ arc_pos z ∧ ¬ x ≽ (y ⊗ z)"
begin
lemma max0_npsm_id: assumes psm: "¬ psm"
and x: "x ∈ carrier R"
shows "Max 𝟬 x = x"
unfolding max_comm[OF zero_closed x]
by (rule max_id[OF _ _ gt_imp_ge[OF zero_leastI[OF psm]]], insert x, auto)
end
locale mono_linear_poly_order_carrier = lpoly_order +
assumes plus_single_mono: "psm"
and check_mono: "⟦check_mono x; y ≻ z; x ≽ 𝟬; x ∈ carrier R; y ∈ carrier R; z ∈ carrier R⟧ ⟹ x ⊗ y ≻ x ⊗ z"
and default_gt_zero: "default R ≻ 𝟬"
and arc_pos_True: "arc_pos x"
locale complexity_linear_poly_order_carrier = mono_linear_poly_order_carrier +
assumes bound: "deriv_bound {(x,y) . (x :: 'a :: show) ∈ carrier R ∧ y ∈ carrier R ∧ y ≽ 𝟬 ∧ arc_pos y ∧ x ≻ y} x (bound R x)"
and bound_plus: "x ∈ carrier R ⟹ y ∈ carrier R ⟹ bound R (x ⊕ y) ≤ bound R x + bound R y"
and bound_0[simp]: "bound R 𝟬 = 0"
and bound_mono: "x ≽ y ⟹ x ∈ carrier R ⟹ y ∈ carrier R ⟹ bound R x ≥ bound R y"
and complexity_cond: "bc ∈ carrier R ⟹ bcv ∈ carrier R ⟹ bd ∈ carrier R ⟹
bc ≽ 𝟬 ⟹ bcv ≽ 𝟬 ⟹ bd ≽ 𝟬 ⟹
isOK(check_complexity R bc deg) ⟹
∃ g. g ∈ O_of (Comp_Poly deg) ∧ (∀ n. bound R (bd ⊗ (bc (^) n ⊗ bcv)) ≤ g n)"
end