section ‹Linear Polynomials›
theory Linear_Polynomial
imports
Show.Show
"Certification_Monads.Check_Monad"
"Abstract-Rewriting.Abstract_Rewriting"
Linear_Poly_Complexity
begin
type_synonym ('v, 'a) p_ass = "'v ⇒ 'a"
type_synonym ('v, 'a) p_vars = "('v × 'a) list"
datatype ('v,'a) l_poly = LPoly 'a "('v, 'a) p_vars"
fun get_nc_lpoly :: "('v, 'a) l_poly ⇒ ('v, 'a) p_vars"
where
"get_nc_lpoly (LPoly _ nc) = nc"
fun
lookup_rest :: "'a ⇒ ('a × 'b) list ⇒ ('b × ('a × 'b) list) option"
where
"lookup_rest x [] = None" |
"lookup_rest x ((y, c) # ycs) =
(if x = y then Some (c, ycs)
else
(case lookup_rest x ycs of
None ⇒ None
| Some (d, yccs) ⇒ Some (d, (y, c) # yccs)))"
lemma lookup_rest_set:
assumes "lookup_rest a ab = Some (b, ab')"
shows "set ab = insert (a, b) (set ab')"
using assms
proof (induct ab arbitrary: ab')
case (Cons entry ab)
obtain a' b' where entry: "entry = (a', b')" by force
note Cons = Cons[unfolded entry lookup_rest.simps]
show ?case
proof (cases "a' = a")
case True
with Cons show ?thesis unfolding entry by auto
next
case False
show ?thesis
proof (cases "lookup_rest a ab")
case (Some res)
obtain b'' ab'' where res: "res = (b'', ab'')" by force
from Cons(2) False have Some: "lookup_rest a ab = Some (b, ab'')"
and ab: "ab' = (a', b') # ab''" by (auto simp: Some res)
from Cons(1)[OF Some]
show ?thesis unfolding ab entry by auto
qed (insert Cons(2) False, auto)
qed
qed auto
context
fixes R :: "('a, 'b) partial_object_scheme" (structure)
begin
definition wf_ass :: "('v, 'a) p_ass ⇒ bool"
where
"wf_ass α ⟷ range α ⊆ carrier R"
definition wf_pvars :: "('v, 'a) p_vars ⇒ bool"
where
"wf_pvars vas ⟷ set (map snd vas) ⊆ carrier R"
fun wf_lpoly :: "('v, 'a) l_poly ⇒ bool" where
"wf_lpoly (LPoly a vas) ⟷ a ∈ carrier R ∧ wf_pvars vas"
end
context
fixes R :: "('a, 'b) monoid_scheme" (structure)
begin
fun list_prod :: "'a list ⇒ 'a" where
"list_prod [] = 𝟭"
| "list_prod (x # xs) = x ⊗ (list_prod xs)"
lemma wf_list_prod_gen:
assumes "𝟭 ∈ carrier G"
and "⋀ x y. x ∈ carrier G ⟹ y ∈ carrier G ⟹ x ⊗ y ∈ carrier G"
shows "set as ⊆ carrier G ⟹ list_prod as ∈ carrier G"
using assms by (induct as) auto
end
context
fixes R :: "('a, 'b) ring_scheme" (structure)
begin
definition coeffs_of_pvars :: "('v, 'a) p_vars ⇒ 'a list"
where
"coeffs_of_pvars vas = 𝟬 # map snd vas"
fun coeffs_of_lpoly :: "('v, 'a) l_poly ⇒ 'a list"
where
"coeffs_of_lpoly (LPoly a vas) = a # coeffs_of_pvars vas"
fun add_var :: "'v ⇒ 'a ⇒ ('v, 'a) p_vars ⇒ ('v, 'a) p_vars" where
"add_var x a [] = [(x, a)]"
| "add_var x a ((y, b) # vas) =
(if x = y then (let s = a ⊕ b in if s = 𝟬 then vas else (x, s) # vas)
else ((y, b) # add_var x a vas))"
fun sum_pvars :: "('v, 'a) p_vars ⇒ ('v, 'a) p_vars ⇒ ('v, 'a) p_vars" where
"sum_pvars [] vbs = vbs"
| "sum_pvars ((x, a) # vas) vbs =
(if a = 𝟬 then sum_pvars vas vbs
else sum_pvars vas (add_var x a vbs))"
fun sum_lpoly :: "('v, 'a) l_poly ⇒ ('v, 'a) l_poly ⇒ ('v, 'a) l_poly" where
"sum_lpoly (LPoly a vas) (LPoly b vbs) = LPoly (a ⊕ b) (sum_pvars vas vbs)"
fun mul_pvars :: "'a ⇒ ('v, 'a) p_vars ⇒ ('v, 'a) p_vars" where
"mul_pvars a [] = []"
| "mul_pvars a ((x, b) # vas) =
(let p = a ⊗ b;
res = mul_pvars a vas in
if p = 𝟬 then res else (x, p) # res)"
fun mul_lpoly :: "'a ⇒ ('v, 'a) l_poly ⇒ ('v, 'a) l_poly" where
"mul_lpoly a (LPoly b vas) = LPoly (a ⊗ b) (mul_pvars a vas)"
abbreviation c_lpoly :: "'a ⇒ ('v, 'a) l_poly" where
"c_lpoly c ≡ LPoly c []"
abbreviation zero_lpoly :: "('v, 'a) l_poly" where
"zero_lpoly ≡ c_lpoly 𝟬"
abbreviation lpoly_monoid :: "('v, 'a) l_poly monoid" where
"lpoly_monoid ≡ ⦇ carrier = Collect (wf_lpoly R), mult = sum_lpoly, one = zero_lpoly ⦈"
abbreviation list_sum where
"list_sum ≡ list_prod ⦇ carrier = carrier R, mult = op ⊕, one = 𝟬 ⦈"
abbreviation list_sum_lpoly where
"list_sum_lpoly ≡ list_prod lpoly_monoid"
end
definition (in semiring) zero_ass :: "('v, 'a) p_ass"
where
"zero_ass = (λ x. 𝟬)"
context monoid
begin
lemma wf_list_prod[simp,intro!]: "set as ⊆ carrier G ⟹ list_prod G as ∈ carrier G"
by (rule wf_list_prod_gen, auto)
lemma list_prod_one[simp]: "list_prod G (map (λ _. 𝟭) ts) = 𝟭"
by (induct ts, auto)
lemma list_prod_mono:
assumes rel1: "rel 𝟭 𝟭"
and rel_mono: "⋀ x y z u. rel x y ⟹ rel z u ⟹ x ∈ carrier G ⟹ y ∈ carrier G ⟹ z ∈ carrier G
⟹ u ∈ carrier G ⟹ rel (x ⊗ z) (y ⊗ u)"
shows "f ∈ set ts → carrier G ⟹ g ∈ set ts → carrier G ⟹ (⋀ t. t ∈ set ts ⟹ rel (f t) (g t))
⟹ rel (list_prod G (map f ts)) (list_prod G (map g ts))"
proof (induct ts)
case (Cons t ts)
show ?case
unfolding list_prod.simps list.simps by (rule rel_mono, insert Cons, auto)
qed (auto simp: rel1)
lemma pos_list_prod:
assumes rel1: "rel 𝟭 𝟭"
and rel_mono: "⋀ x y z u. rel x y ⟹ rel z u ⟹ x ∈ carrier G ⟹ y ∈ carrier G ⟹ z ∈ carrier G
⟹ u ∈ carrier G ⟹ rel (x ⊗ z) (y ⊗ u)"
and as: "set as ⊆ carrier G" "⋀ a. a ∈ set as ⟹ rel a 𝟭"
shows "rel (list_prod G as) 𝟭"
proof -
have "?thesis = rel (list_prod G (map id as)) (list_prod G (map (λ _. 𝟭) as))" by simp
also have "…"
by (rule list_prod_mono[of rel, OF rel1 rel_mono], insert as, auto)
finally show ?thesis .
qed
end
context semiring
begin
lemmas wf_list_sum = add.wf_list_prod
fun eval_pvars :: "('v, 'a) p_ass ⇒ ('v, 'a) p_vars ⇒ 'a" where
"eval_pvars _ [] = 𝟬"
| "eval_pvars α ((x, a) # vas) = (a ⊗ α x ⊕ eval_pvars α vas)"
fun eval_lpoly :: "('v, 'a) p_ass ⇒ ('v, 'a) l_poly ⇒ 'a" where
"eval_lpoly α (LPoly a vas) = a ⊕ eval_pvars α vas"
lemma wf_lpoly_coeff:
assumes wf: "wf_lpoly R p" and mem: "a ∈ set (coeffs_of_lpoly R p)"
shows "a ∈ carrier R"
proof -
obtain b as where p: "p = LPoly b as" by (cases p, auto)
note wf = wf[unfolded p, simplified]
show ?thesis
proof (cases "a = b")
case True
with wf show ?thesis by auto
next
case False
with mem[unfolded p] have mem: "a ∈ set (coeffs_of_pvars R as)" by auto
from wf have "wf_pvars R as" ..
with mem show ?thesis
proof (induct as)
case Nil
thus ?case unfolding coeffs_of_pvars_def by auto
next
case (Cons b bs)
show ?case
proof (cases "a = snd b")
case True
with Cons(3) show ?thesis unfolding wf_pvars_def by auto
next
case False
with Cons(2) have mem: "a ∈ set (coeffs_of_pvars R bs)" unfolding coeffs_of_pvars_def by auto
from False Cons(3) have wf: "wf_pvars R bs" unfolding wf_pvars_def by auto
from Cons(1)[OF mem wf] show ?thesis .
qed
qed
qed
qed
lemma wf_mul_pvars[simp]:
assumes wf_pvars: "wf_pvars R vas"
and wf_elem: "a ∈ carrier R"
shows "wf_pvars R (mul_pvars R a vas)"
using wf_pvars
unfolding wf_pvars_def
proof (induct vas)
case (Cons yb vas)
obtain y b where yb: "yb = (y,b)" by force
show ?case using yb Cons wf_elem by (auto simp: Let_def)
qed simp
lemma wf_add_var[simp]:
assumes wf_pvars: "wf_pvars R vas"
and [simp]: "a ∈ carrier R"
shows "wf_pvars R (add_var R x a vas)"
using wf_pvars
unfolding wf_pvars_def
proof (induct vas)
case (Cons yb vas)
obtain y b where yb: "yb = (y,b)" by force
show ?case using yb Cons by (auto simp: Let_def)
qed auto
lemma wf_sum_pvars[simp]:
assumes wf_pvars_a: "wf_pvars R vas"
and wf_pvars_b: "wf_pvars R vbs"
shows "wf_pvars R (sum_pvars R vas vbs)"
using wf_pvars_a wf_pvars_b
unfolding wf_pvars_def[where vas = vas]
proof (induct vas arbitrary: vbs)
case (Cons xa vas)
thus ?case by (cases xa, auto)
qed simp
lemma wf_eval_pvars[simp,intro]:
assumes wf_ass: "wf_ass R α"
and wf_pvars: "wf_pvars R vas"
shows "eval_pvars α vas ∈ carrier R"
using wf_pvars
unfolding wf_pvars_def
proof (induct vas)
case (Cons xa vas)
show ?case
proof (cases xa)
case (Pair x a)
from wf_ass have "α x ∈ carrier R" unfolding wf_ass_def by auto
with Pair Cons show ?thesis by auto
qed
qed simp
lemma mul_pvars_sound[simp]:
assumes wf_pvars: "wf_pvars R vas"
and wf_a: "a ∈ carrier R"
and wf_ass: "wf_ass R α"
shows "eval_pvars α (mul_pvars R a vas) = a ⊗ (eval_pvars α vas)"
using wf_pvars
proof (induct vas)
case Nil thus ?case by (simp add: wf_a)
next
case (Cons xb vas)
show ?case
proof (cases xb)
case (Pair x b)
with Cons have wf_b: "b ∈ carrier R" unfolding wf_pvars_def by auto
from Cons have wf_vas: "wf_pvars R vas" unfolding wf_pvars_def by auto
from wf_ass have wf_x: "α x ∈ carrier R" unfolding wf_ass_def by auto
note wf_eval = wf_eval_pvars[OF wf_ass wf_vas]
show ?thesis
proof (cases "a ⊗ b = 𝟬")
case True
with Pair Cons have "eval_pvars α (mul_pvars R a (xb # vas)) = eval_pvars α (mul_pvars R a vas)" by (simp add: Let_def)
also have "… = a ⊗ eval_pvars α vas" using Cons wf_vas wf_a by auto
also have "… = a ⊗ (b ⊗ α x) ⊕ …" unfolding m_assoc[OF wf_a wf_b wf_x,symmetric] True using wf_a wf_eval wf_x by algebra
also have "… = a ⊗ (b ⊗ α x ⊕ eval_pvars α vas)" using wf_vas wf_a wf_b wf_x wf_eval by algebra
finally show ?thesis using Pair by auto
next
case False
with Cons Pair have "eval_pvars α (mul_pvars R a (xb # vas)) = eval_pvars α ((x,a⊗b) # mul_pvars R a vas)" by (simp add: Let_def)
also have "… = a ⊗ (b ⊗ α x ⊕ eval_pvars α vas)" using Cons wf_vas wf_vas wf_a wf_b wf_x wf_ass wf_eval
by (auto, algebra)
finally show ?thesis using Pair by auto
qed
qed
qed
lemma add_var_sound[simp]:
assumes wf_pvars: "wf_pvars R vas"
and wf_a: "a ∈ carrier R"
and wf_ass: "wf_ass R α"
shows "eval_pvars α (add_var R x a vas) = a ⊗ α x ⊕ eval_pvars α vas"
using wf_pvars
proof (induct vas)
case (Cons yb vas)
show ?case
proof (cases yb)
case (Pair y b)
with Cons have wf_b: "b ∈ carrier R" unfolding wf_pvars_def by auto
from Cons have wf_vas: "wf_pvars R vas" unfolding wf_pvars_def by auto
from wf_ass have wf_x: "α x ∈ carrier R" unfolding wf_ass_def by auto
from wf_ass have wf_y: "α y ∈ carrier R" unfolding wf_ass_def by auto
note wf_eval = wf_eval_pvars[OF wf_ass wf_vas]
show ?thesis
proof (cases "x = y")
case True note oTrue = this
show ?thesis
proof (cases "a ⊕ b = 𝟬")
case True
with oTrue Pair have "eval_pvars α (add_var R x a (yb # vas)) = eval_pvars α (vas)" by (simp add: Let_def)
also have "… = (a ⊕ b) ⊗ α x ⊕ eval_pvars α vas" using True wf_x wf_ass wf_vas by auto
also have "… = a ⊗ α x ⊕ eval_pvars α ((y,b) # vas)" using wf_ass wf_x wf_vas wf_a wf_b wf_eval unfolding ‹x = y›
by (auto, algebra)
finally show ?thesis using Pair by auto
next
case False
with oTrue Pair have "eval_pvars α (add_var R x a (yb # vas)) = eval_pvars α ((x,a⊕b) # vas)" by (simp add: Let_def)
also have "… = (a ⊕ b) ⊗ α x ⊕ eval_pvars α vas" using True wf_x wf_ass wf_vas by auto
also have "… = a ⊗ α x ⊕ eval_pvars α ((y,b) # vas)" using wf_ass wf_x wf_vas wf_a wf_b wf_eval unfolding ‹x = y›
by (auto, algebra)
finally show ?thesis using Pair by auto
qed
next
case False
term group
with Pair False have "eval_pvars α (add_var R x a (yb # vas)) = eval_pvars α ((y,b) # (add_var R x a vas))" by (simp add: Let_def)
also have "… = b ⊗ α y ⊕ eval_pvars α (add_var R x a vas)" by auto
also have "… = b ⊗ α y ⊕ (a ⊗ α x ⊕ eval_pvars α vas)" using Cons wf_vas by auto
also have "… = a ⊗ α x ⊕ eval_pvars α ((y,b) # vas)" using wf_ass wf_x wf_y wf_vas wf_a wf_b wf_eval
by (auto, algebra)
finally show ?thesis using Pair by auto
qed
qed
qed simp
lemma sum_pvars_sound[simp]:
assumes wf_ass: "wf_ass R α"
and wf_pvars_a: "wf_pvars R vas"
and wf_pvars_b: "wf_pvars R vbs"
shows "eval_pvars α (sum_pvars R vas vbs) = eval_pvars α vas ⊕ eval_pvars α vbs"
using wf_pvars_a wf_pvars_b
proof (induct vas arbitrary: vbs)
case Nil thus ?case using wf_ass by auto
next
case (Cons xa vas)
obtain x a where xa: "xa = (x,a)" by force
with Cons wf_ass have wf: "wf_pvars R vas" "a ∈ carrier R" "α x ∈ carrier R"
unfolding wf_pvars_def wf_ass_def by auto
have "eval_pvars α vas ∈ carrier R" using wf_eval_pvars wf_ass wf by auto
note wf = wf this
show ?case
proof (cases "a = 𝟬")
case True
thus ?thesis using xa Cons wf by auto
next
case False
from wf Cons have "wf_pvars R (add_var R x a vbs)" by auto
with False show ?thesis
using xa Cons wf wf_eval_pvars[OF wf_ass Cons(3)] wf_ass by (auto, algebra)
qed
qed
lemma wf_sum_lpoly:
assumes wf_p: "wf_lpoly R p"
and wf_q: "wf_lpoly R q"
shows "wf_lpoly R (sum_lpoly R p q)"
using assms
by (cases p, cases q, auto)
lemma wf_mul_lpoly:
assumes wf_a: "a ∈ carrier R"
and wf_p: "wf_lpoly R p"
shows "wf_lpoly R (mul_lpoly R a p)"
using assms
by (cases p, auto)
lemma wf_eval_lpoly[simp, intro]:
assumes wf_ass: "wf_ass R α"
and wf_p: "wf_lpoly R p"
shows "eval_lpoly α p ∈ carrier R"
using assms by (cases p, auto)
lemma sum_poly_sound:
assumes wf_ass: "wf_ass R α"
and wf_p: "wf_lpoly R p"
and wf_q: "wf_lpoly R q"
shows "eval_lpoly α (sum_lpoly R p q) = eval_lpoly α p ⊕ eval_lpoly α q"
proof (cases p)
case (LPoly a vas) note oLPoly = this
show ?thesis
proof (cases q)
case (LPoly b vbs)
with oLPoly assms have "eval_pvars α vas ∈ carrier R" "eval_pvars α vbs ∈ carrier R" by auto
with LPoly oLPoly assms wf_eval_pvars[OF wf_ass] show ?thesis
by (auto, algebra)
qed
qed
lemma mul_poly_sound:
assumes wf_ass: "wf_ass R α"
and wf_a: "a ∈ carrier R"
and wf_p: "wf_lpoly R p"
shows "eval_lpoly α (mul_lpoly R a p) = a ⊗ eval_lpoly α p"
proof (cases p)
case (LPoly b vbs)
with wf_p have wfb: "b ∈ carrier R" and wfbs: "wf_pvars R vbs" by auto
from wf_ass wfbs wf_eval_pvars[OF wf_ass wfbs] wfb wf_a show ?thesis unfolding LPoly
by (auto, algebra)
qed
lemma wf_zero_ass[simp]: "wf_ass R zero_ass"
unfolding wf_ass_def zero_ass_def by auto
lemma lookup_rest_sound:
assumes lookup: "lookup_rest y vas = Some (a,vas')"
and wf_ass: "wf_ass R α"
and wf_vas: "wf_pvars R vas"
shows "eval_pvars α vas = a ⊗ α y ⊕ eval_pvars α vas' ∧ wf_pvars R vas' ∧ a ∈ carrier R"
using lookup wf_vas
proof (induct vas arbitrary: vas')
case (Cons xb vas)
show ?case
proof (cases xb)
case (Pair x b)
with Cons have wf_b: "b ∈ carrier R" and wf_vas: "wf_pvars R vas" and wf_x: "α x ∈ carrier R" using wf_ass unfolding wf_ass_def wf_pvars_def by auto
show ?thesis
proof (cases "x = y")
case True
with Pair Cons have "a = b ∧ vas' = vas" by auto
with wf_b wf_vas Pair True show ?thesis by auto
next
case False
show ?thesis
proof (cases "lookup_rest y vas")
case None
with Pair False have "lookup_rest y ((x,b) # vas) = None" by auto
with Cons Pair show ?thesis by simp
next
case (Some res)
show ?thesis
proof (cases res)
case (Pair c vbs)
with Some False ‹xb = (x,b)› have "lookup_rest y (xb # vas) = Some (c,(x,b) # vbs)" by simp
with Cons have ca: "c = a" and vas': "vas' = (x,b) # vbs" by auto
from Some Pair Cons ca wf_vas have rec: "eval_pvars α vas = a ⊗ α y ⊕ eval_pvars α vbs" and wf_vbs: "wf_pvars R vbs" and wf_a: "a ∈ carrier R" by auto
from wf_eval_pvars[OF wf_ass] wf_vbs have wf_evbs: "eval_pvars α vbs ∈ carrier R" by auto
from wf_ass have wf_y: "α y ∈ carrier R" unfolding wf_ass_def by auto
show ?thesis using ‹xb = (x,b)› wf_b vas' rec wf_evbs wf_vbs wf_a wf_y wf_ass wf_b wf_x
by (auto simp: wf_pvars_def, algebra)
qed
qed
qed
qed
qed simp
lemma wf_list_sum_lpoly: "set as ⊆ carrier (lpoly_monoid R) ⟹
list_sum_lpoly R as ∈ carrier (lpoly_monoid R)"
by (rule wf_list_prod_gen, insert wf_sum_lpoly, auto simp: wf_pvars_def)
end
context ordered_semiring
begin
definition pos_pvars :: "('v,'a)p_vars ⇒ bool" where
"pos_pvars vas ⟷ (∀ va ∈ set vas. snd va ≽ 𝟬)"
definition pos_coeffs :: "('v,'a)l_poly ⇒ bool" where
"pos_coeffs p = pos_pvars (get_nc_lpoly p)"
lemmas poly_simps = geq_refl
declare poly_simps[simp]
lemma plus_right_mono:
assumes ge: "y ≽ z" and carr: "x ∈ carrier R" "y ∈ carrier R" "z ∈ carrier R"
shows "x ⊕ y ≽ x ⊕ z"
proof -
have "?thesis = (y ⊕ x ≽ z ⊕ x)" using carr by algebra
also have "…" by (rule plus_left_mono[OF ge], insert carr, auto)
finally show ?thesis .
qed
lemma plus_left_right_mono: "⟦x ≽ y; z ≽ u; x ∈ carrier R; y ∈ carrier R; z ∈ carrier R; u ∈ carrier R⟧ ⟹ x ⊕ z ≽ y ⊕ u"
by (rule geq_trans[OF plus_left_mono plus_right_mono], auto)
lemma pos_list_sum: "(⋀ a. a ∈ set as ⟹ a ∈ carrier R ∧ a ≽ 𝟬) ⟹ list_sum R as ≽ 𝟬"
by (rule add.pos_list_prod[of "op ≽", OF geq_refl plus_left_right_mono], auto)
lemma list_sum_mono: "(⋀ t. t ∈ set ts ⟹ f t ≽ g t ∧ f t ∈ carrier R ∧ g t ∈ carrier R) ⟹
list_sum R (map f ts) ≽ list_sum R (map g ts)"
by (rule add.list_prod_mono[of "op ≽", OF geq_refl plus_left_right_mono], auto)
lemma sum_pos:
assumes "a ≽ 𝟬" and "b ≽ 𝟬" and "a ∈ carrier R" and "b ∈ carrier R"
shows "a ⊕ b ≽ 𝟬"
proof -
have "a ⊕ b ≽ 𝟬 ⊕ 𝟬" by (rule plus_left_right_mono, auto simp: assms)
thus ?thesis by auto
qed
lemma pos_mul_pvars:
assumes pos_vas: "pos_pvars vas"
and wf_vas: "wf_pvars R vas"
and pos_a: "a ≽ 𝟬"
and wf_a: "a ∈ carrier R"
shows "pos_pvars (mul_pvars R a vas)"
using pos_vas wf_vas unfolding pos_pvars_def
proof (induct vas)
case (Cons xb vas)
show ?case
proof (cases xb)
case (Pair x b)
with Cons have wf_b: "b ∈ carrier R" and pos_b: "b ≽ 𝟬" unfolding wf_pvars_def by auto
from Cons have "wf_pvars R vas" unfolding wf_pvars_def by auto
with Cons have rec: "∀ va ∈ set (mul_pvars R a vas). snd va ≽ 𝟬" by auto
show ?thesis
proof (cases "a ⊗ b = 𝟬")
case True
with Cons Pair have "mul_pvars R a (xb # vas) = mul_pvars R a vas" by (simp add: Let_def)
with rec show ?thesis by auto
next
case False
have "a ⊗ b ≽ 𝟬 ⊗ 𝟬" by (rule geq_trans[where y = "a ⊗ 𝟬"], rule times_right_mono, auto simp: wf_a pos_a pos_b wf_b)
hence pos_ab: "a ⊗ b ≽ 𝟬" by simp
from False Pair Cons have "mul_pvars R a (xb # vas) = (x,a⊗b) # mul_pvars R a vas" by (simp add: Let_def)
with rec pos_ab show ?thesis by auto
qed
qed
qed simp
declare mul_pvars.simps[simp del]
lemma pos_add_var:
assumes wf_pvars: "wf_pvars R vas"
and pos_pvars: "pos_pvars vas"
and wf_a: "a ∈ carrier R"
and pos_a: "a ≽ 𝟬"
shows "pos_pvars (add_var R x a vas)"
using wf_pvars pos_pvars unfolding pos_pvars_def
proof (induct vas)
case Nil thus ?case by (simp add: pos_a)
next
case (Cons yb vas)
show ?case
proof (cases yb)
case (Pair y b)
with Cons have wf_b: "b ∈ carrier R" and pos_b: "b ≽ 𝟬" unfolding wf_pvars_def by auto
from Cons have "wf_pvars R vas" unfolding wf_pvars_def by auto
with Cons have rec: "∀ va ∈ set (add_var R x a vas). snd va ≽ 𝟬" by auto
show ?thesis
proof (cases "x = y")
case True note oTrue = this
show ?thesis
proof (cases "a ⊕ b = 𝟬")
case True
with oTrue Pair have "add_var R x a (yb # vas) = vas" by (simp add: Let_def)
with Cons show ?thesis by auto
next
case False
with True Pair have id: "add_var R x a (yb # vas) = (x,a⊕b) # vas" by (simp add: Let_def)
have "a ⊕ b ≽ 𝟬 ⊕ 𝟬" by (rule plus_left_right_mono, auto simp: pos_a pos_b wf_a wf_b)
with Cons id show ?thesis by auto
qed
next
case False
with Pair have "add_var R x a (yb # vas) = (y,b) # (add_var R x a vas)" by (simp add: Let_def)
with pos_b rec show ?thesis by auto
qed
qed
qed
declare add_var.simps[simp del]
lemma pos_sum_pvars:
assumes pos_vas: "pos_pvars vas"
and wf_vas: "wf_pvars R vas"
and pos_vbs: "pos_pvars vbs"
and wf_vbs: "wf_pvars R vbs"
shows "pos_pvars (sum_pvars R vas vbs)"
using assms
proof (induct vas arbitrary: vbs)
case (Cons xa vas)
from Cons(2) Cons(3)
have wf_vas: "wf_pvars R vas" and pos_vas: "pos_pvars vas" unfolding wf_pvars_def pos_pvars_def by auto
show ?case
proof (cases xa)
case (Pair x a)
with Cons(2) Cons(3) have wf_a: "a ∈ carrier R" and pos_a: "a ≽ 𝟬" unfolding wf_pvars_def pos_pvars_def by auto
show ?thesis
proof (cases "a = 𝟬")
case True
thus ?thesis using Pair Cons(1)[OF pos_vas wf_vas Cons(4) Cons(5)] unfolding pos_pvars_def by auto
next
case False
from wf_a Cons have wf_xvbs: "wf_pvars R (add_var R x a vbs)" by auto
have "pos_pvars (add_var R x a vbs)" by (rule pos_add_var, auto simp: Cons wf_a pos_a)
with Cons wf_xvbs wf_vas pos_vas have "pos_pvars (sum_pvars R vas (add_var R x a vbs))" by auto
with False show ?thesis using Pair by auto
qed
qed
qed simp
declare sum_pvars.simps[simp del]
lemma pos_sum_lpoly:
assumes wf_p: "wf_lpoly R p"
and wf_q: "wf_lpoly R q"
and pos_p: "pos_coeffs p"
and pos_q: "pos_coeffs q"
shows "pos_coeffs (sum_lpoly R p q)"
using assms unfolding pos_coeffs_def
by (cases p, cases q, simp add: pos_sum_pvars)
lemma pos_mul_lpoly:
assumes wf_a: "a ∈ carrier R"
and pos_a: "a ≽ 𝟬"
and wf_p: "wf_lpoly R p"
and pos_p: "pos_coeffs p"
shows "pos_coeffs (mul_lpoly R a p)"
using assms unfolding pos_coeffs_def
by (cases p, simp add: pos_mul_pvars)
text ‹let us head for comparing polynomials now›
definition pos_ass :: "('v, 'a) p_ass ⇒ bool"
where
"pos_ass α ⟷ (∀ x. α x ≽ 𝟬)"
lemma pos_zero_ass[simp]: "pos_ass zero_ass"
unfolding pos_ass_def zero_ass_def by auto
definition poly_s :: "('v, 'a) l_poly rel"
where
"poly_s = {(p, q). ∀ α. wf_ass R α ∧ pos_ass α ⟶ eval_lpoly α p ≻ eval_lpoly α q}"
definition poly_ns :: "('v, 'a) l_poly rel"
where
"poly_ns = {(p, q) . ∀ α. wf_ass R α ∧ pos_ass α ⟶ eval_lpoly α p ≽ eval_lpoly α q}"
end
context
fixes R :: "('a :: show, 'b) ring_scheme" (structure)
begin
fun
check_pvars :: "('a ⇒ 'a ⇒ bool) ⇒ ('v, 'a) p_vars ⇒ ('v, 'a) p_vars ⇒ 'v check"
where
"check_pvars rel vas [] = check_allm (λva. check (rel (snd va) 𝟬) (fst va)) vas" |
"check_pvars rel vas ((x, b) # vbs) = do {
let (a', vas') =
(case lookup_rest x vas of
None ⇒ (𝟬, vas)
| Some (a, vas'') ⇒ (a, vas''));
check (rel a' b) x;
check_pvars rel vas' vbs
}"
fun
show_pvars :: "('v :: show, 'a :: show) p_vars ⇒ string list"
where
"show_pvars [] = []" |
"show_pvars ((x, c) # vas) =
(if c = 𝟭 then id else shows c) (show x) # show_pvars vas"
fun
shows_lpoly :: "('v :: show, 'a) l_poly ⇒ shows"
where
"shows_lpoly (LPoly c cs) =
(case show_pvars cs of
[] ⇒ shows c
| ss ⇒
(if c = 𝟬 then id
else (shows c +@+ shows_string '' + '')) +@+ shows_list_gen shows [] [] '' + '' [] ss)"
end
context
fixes R :: "('a :: show, 'b) ordered_semiring_scheme" (structure)
begin
fun
check_lpoly_ns :: "('v :: show, 'a) l_poly ⇒ ('v, 'a) l_poly ⇒ shows check"
where
"check_lpoly_ns (LPoly a vas) (LPoly b vbs) = do {
check (a ≽ b) (shows_string ''problem when comparing constant parts'');
check_pvars R (op ≽) vas vbs
<+? (λe. ''problem when comparing coefficients of variable '' +#+ shows e)
} <+? (λe. ''problem when comparing '' +#+ shows_lpoly R (LPoly a vas)
+@+ '' >= '' +#+ shows_lpoly R (LPoly b vbs) +@+ shows_nl +@+ e)"
end
context
fixes R :: "('a :: show, 'b) lpoly_order_semiring_scheme" (structure)
begin
fun
check_lpoly_s :: "('v :: show, 'a) l_poly ⇒ ('v, 'a) l_poly ⇒ shows check"
where
"check_lpoly_s (LPoly a vas) (LPoly b vbs) = do {
check (a ≻ b) (shows_string ''problem when comparing constant part'');
check_pvars R (if psm then op ≽ else op ≻) vas vbs
<+? (λx. ''problem when comparing coefficients of variable '' +#+ shows x)
} <+? (λs. ''problem when comparing '' +#+ shows_lpoly R (LPoly a vas)
+@+ '' > '' +#+ shows_lpoly R (LPoly b vbs) +@+ shows_nl +@+ s)"
end
context lpoly_order
begin
lemma check_pvars_sound:
assumes check: "isOK (check_pvars (R ⦇ gt := gt, bound := bnd ⦈) (op ≽) vas vbs)"
and wf_ass: "wf_ass R α"
and wf_vas: "wf_pvars R vas"
and wf_vbs: "wf_pvars R vbs"
and pos_ass: "pos_ass α"
shows "eval_pvars α vas ≽ eval_pvars α vbs"
using check wf_vas wf_vbs
proof (induct vbs arbitrary: vas)
case Nil
hence "∀ va ∈ set vas. (snd va ≽ 𝟬)" by auto
with ‹wf_pvars R vas› have "eval_pvars α vas ≽ 𝟬"
proof (induct vas)
case (Cons xa vas)
show ?case
proof (cases xa)
case (Pair x a)
with Cons have wf_a: "a ∈ carrier R" and wf_vas: "wf_pvars R vas" and pos: "a ≽ 𝟬" unfolding wf_pvars_def by auto
from wf_ass have wf_x: "α x ∈ carrier R" unfolding wf_ass_def by auto
have "a ⊗ α x ⊕ eval_pvars α vas ≽ 𝟬 ⊕ eval_pvars α vas"
proof (rule plus_left_mono)
have posx: "α x ≽ 𝟬" using pos_ass unfolding pos_ass_def by auto
have ge1: "a ⊗ α x ≽ 𝟬 ⊗ α x" by (rule times_left_mono, auto simp: pos posx wf_x wf_a)
have ge2: "… ≽ 𝟬 ⊗ 𝟬" by (rule times_right_mono, auto simp: posx wf_x)
have "a ⊗ α x ≽ 𝟬 ⊗ 𝟬" by (rule geq_trans[where y = "𝟬 ⊗ α x"], auto simp only: ge1 ge2, auto simp: wf_x wf_a)
thus "a ⊗ α x ≽ 𝟬" by auto
qed (auto simp: wf_a wf_ass wf_x wf_vas)
hence ge1: "a ⊗ α x ⊕ eval_pvars α vas ≽ eval_pvars α vas" using wf_vas wf_ass by auto
have ge2: "… ≽ 𝟬" using Pair Cons wf_vas by auto
have "a ⊗ α x ⊕ eval_pvars α vas ≽ 𝟬"
by (rule geq_trans[where y = "eval_pvars α vas"], auto simp only: ge1 ge2,
auto simp: wf_a wf_x wf_ass wf_vas)
thus ?thesis using Pair by auto
qed
qed simp
thus ?case by auto
next
case (Cons yb vbs)
let ?R = "R ⦇ gt := gt, bound := bnd ⦈"
show ?case
proof (cases yb)
case (Pair y b) note oPair = this
with Cons have wf_b: "b ∈ carrier R" and wf_y: "α y ∈ carrier R" and pos_y: "α y ≽ 𝟬" and wf_vbs: "wf_pvars R vbs"
using wf_ass pos_ass unfolding wf_ass_def pos_ass_def wf_pvars_def by auto
show ?thesis
proof (cases "lookup_rest y vas")
case None
with Cons Pair wf_vbs have rec: "eval_pvars α vas ≽ eval_pvars α vbs" (is "?l ≽ ?r") and small_b: "𝟬 ≽ b" by auto
have "𝟬 ⊗ α y ≽ b ⊗ α y" by (rule times_left_mono, auto simp: wf_b wf_y small_b pos_y)
hence ge: "𝟬 ≽ b ⊗ α y" using wf_y by auto
have "𝟬 ⊕ ?l ≽ b ⊗ α y ⊕ ?r" by (rule plus_left_right_mono, auto simp: rec wf_ass wf_vbs wf_b wf_y Cons ge)
with Cons wf_ass Pair None show ?thesis by auto
next
case (Some avas)
show ?thesis
proof (cases avas)
case (Pair a vas')
with Some Cons oPair have lookup: "lookup_rest y vas = Some (a,vas')" and check: "isOK(check_pvars ?R op ≽ vas' vbs)" and ab: "a ≽ b" by auto
have lookupRes: "eval_pvars α vas = a ⊗ α y ⊕ eval_pvars α vas' ∧ wf_pvars R vas' ∧ a ∈ carrier R"
by (rule lookup_rest_sound[OF lookup wf_ass ‹wf_pvars R vas›])
with Cons check wf_vbs have rec: "eval_pvars α vas' ≽ eval_pvars α vbs" (is "?l ≽ ?r") by auto
have "a ⊗ α y ⊕ ?l ≽ b ⊗ α y ⊕ ?r"
by (rule plus_left_right_mono, rule times_left_mono, auto simp: rec lookupRes wf_ass wf_vbs wf_y wf_b ab pos_y)
with lookupRes Pair Some oPair show ?thesis by auto
qed
qed
qed
qed
lemma check_pvars_gt_sound:
assumes check: "isOK(check_pvars (R ⦇ gt := gt, bound := bnd ⦈) wgt vas vbs)"
and wgt_imp_gt: "⋀ a b. (a,b) ∈ set (coeffs_of_pvars (R ⦇ gt := gt, bound := bnd ⦈) vas) × set (coeffs_of_pvars (R ⦇ gt := gt, bound := bnd ⦈) vbs)
⟹ a ∈ carrier R ⟹ b ∈ carrier R ⟹ wgt a b ⟹ a ≻ b"
and wf_ass: "wf_ass R α"
and wf_vas: "wf_pvars R vas"
and wf_vbs: "wf_pvars R vbs"
and pos_ass: "pos_ass α"
and mode: "¬ psm"
shows "eval_pvars α vas ≻ eval_pvars α vbs"
using check wgt_imp_gt wf_vas wf_vbs
proof (induct vbs arbitrary: vas)
case Nil
have "eval_pvars α Nil = 𝟬" by auto
thus ?case by (auto simp: zero_leastI mode wf_ass ‹wf_pvars R vas›)
next
case (Cons yb vbs)
let ?R = "R ⦇ gt := gt, bound := bnd ⦈"
show ?case
proof (cases yb)
case (Pair y b) note oPair = this
with Cons have wf_b: "b ∈ carrier R" and wf_y: "α y ∈ carrier R" and pos_y: "α y ≽ 𝟬" and wf_vbs: "wf_pvars R vbs"
using wf_ass pos_ass unfolding wf_ass_def pos_ass_def wf_pvars_def by auto
note coeff = coeffs_of_pvars_def
have "set (coeffs_of_pvars ?R (yb # vbs)) = {b} ∪ set (coeffs_of_pvars ?R vbs)"
unfolding Pair coeff by auto
note coeffs = Cons(3)[unfolded this]
show ?thesis
proof (cases "lookup_rest y vas")
case None
from coeffs have "⋀ a b. (a, b) ∈ set (coeffs_of_pvars ?R vas) × set (coeffs_of_pvars ?R vbs)
⟹ a ∈ carrier R ⟹ b ∈ carrier R ⟹ wgt a b ⟹ a ≻ b"
by auto
from Cons(1)[OF _ this] None Cons
Pair wf_vbs have rec: "eval_pvars α vas ≻ eval_pvars α vbs" and small_b: "wgt 𝟬 b" by auto
from coeffs[unfolded coeff] small_b wf_b have "𝟬 ≻ b" by auto
from this wf_b have "b = 𝟬" using zero_leastII mode by auto
with rec Pair wf_b wf_vbs wf_y wf_ass show ?thesis by auto
next
case (Some avas)
show ?thesis
proof (cases avas)
case (Pair a vas')
with Some oPair Cons have lookup: "lookup_rest y vas = Some (a,vas')" and check: "isOK(check_pvars ?R wgt vas' vbs)" and ab: "wgt a b" by auto
from Cons(4)[unfolded wf_pvars_def] lookup_rest_set[OF lookup] have wf_a: "a ∈ carrier R" by auto
from lookup_rest_set[OF lookup] coeffs[unfolded coeff] ab wf_a wf_b have ab: "a ≻ b" by auto
from lookup_rest_set[OF lookup] have "set (coeffs_of_pvars ?R vas') ⊆ set (coeffs_of_pvars ?R vas)"
unfolding coeff by auto
with coeffs have "⋀ a b. (a, b) ∈ set (coeffs_of_pvars ?R vas') × set (coeffs_of_pvars ?R vbs) ⟹ a ∈ carrier R ⟹ b ∈ carrier R ⟹ wgt a b ⟹ a ≻ b" by auto
note IH = Cons(1)[OF check this]
have lookupRes: "eval_pvars α vas = a ⊗ α y ⊕ eval_pvars α vas' ∧ wf_pvars R vas' ∧ a ∈ carrier R"
by (rule lookup_rest_sound[OF lookup wf_ass ‹wf_pvars R vas›])
with IH check wf_vbs have gt: "eval_pvars α vas' ≻ eval_pvars α vbs" (is "?l ≻ ?r") by auto
show ?thesis
proof (cases "α y = 𝟬")
case False
have "a ⊗ α y ⊕ ?l ≻ b ⊗ α y ⊕ ?r"
by (rule plus_gt_both_mono, rule times_gt_left_mono[OF ab], auto simp: lookupRes wf_b wf_y wf_ass wf_vbs mode gt)
with lookupRes Some Pair oPair Cons show ?thesis by auto
next
case True
hence "a ⊗ α y ⊕ ?l = ?l" and "b ⊗ α y ⊕ ?r = ?r" by (auto simp: wf_y lookupRes wf_ass wf_b wf_vbs)
with gt lookupRes True Some Pair oPair Cons show ?thesis by auto
qed
qed
qed
qed
qed
lemma check_lpoly_ns_sound:
assumes check: "isOK (check_lpoly_ns (R ⦇ gt := gt, bound := bnd ⦈) p q)"
and wf_p: "wf_lpoly R p"
and wf_q: "wf_lpoly R q"
shows "(p, q) ∈ poly_ns"
proof (cases p)
case (LPoly a vas) note oLPoly = this
let ?R = "R ⦇ gt := gt, bound := bnd ⦈"
show ?thesis
proof (cases q)
case (LPoly b vbs)
with oLPoly assms have ab: "a ≽ b" and pvars: "isOK(check_pvars ?R op ≽ vas vbs)" and
wf_a: "a ∈ carrier R" and wf_b: "b ∈ carrier R" and wf_vas: "wf_pvars R vas" and wf_vbs: "wf_pvars R vbs"
by auto
{
fix α
have "wf_ass R α ∧ pos_ass α ⟶ (a ⊕ (eval_pvars α vas)) ≽ (b ⊕ (eval_pvars α vbs))" (is "?ass ⟶ ?goal")
proof
assume ass: ?ass
show ?goal
by (rule plus_left_right_mono[OF _ check_pvars_sound[OF pvars]],
insert wf_a wf_b ass wf_vas wf_vbs ab, auto)
qed
}
hence "(LPoly a vas, LPoly b vbs) ∈ poly_ns" unfolding poly_ns_def
by auto
with LPoly oLPoly show ?thesis by auto
qed
qed
lemma plus_gt_left_mono2:
assumes xy: "(x :: 'a) ≻ y" and zu: "(z :: 'a) ≽ u"
and carr: "x ∈ carrier R" "y ∈ carrier R" "z ∈ carrier R" "u ∈ carrier R"
and psm: psm
shows "(x :: 'a) ⊕ z ≻ y ⊕ u"
proof -
have "x ⊕ z ≻ y ⊕ z" by (rule plus_gt_left_mono[OF xy psm], insert carr, auto)
also have "… = z ⊕ y" using carr by algebra
finally have one: "x ⊕ z ≻ z ⊕ y" .
have "z ⊕ y ≽ u ⊕ y" by (rule plus_left_mono[OF zu], insert carr, auto)
also have "… = y ⊕ u" using carr by algebra
finally have two: "z ⊕ y ≽ y ⊕ u" .
show ?thesis
by (rule compat2[OF one two], insert carr, auto)
qed
lemma check_lpoly_s_sound:
assumes check: "isOK (check_lpoly_s (R ⦇ gt := wgt, bound := bnd ⦈) p q)"
and wf_p: "wf_lpoly R p"
and wf_q: "wf_lpoly R q"
and weak_gt: "⋀ a b. (a,b) ∈ set (coeffs_of_lpoly (R ⦇ gt := wgt, bound := bnd ⦈) p) × set (coeffs_of_lpoly (R ⦇ gt := wgt, bound := bnd ⦈) q)
⟹ a ∈ carrier R ⟹ b ∈ carrier R ⟹ wgt a b ⟹ a ∈ carrier R ⟹ b ∈ carrier R ⟹ a ≻ b"
shows "(p,q) ∈ poly_s"
proof (cases p)
case (LPoly a vas) note oLPoly = this
let ?R = "R ⦇ gt := wgt, bound := bnd ⦈"
let ?wgt = "if psm then op ≽ else wgt"
show ?thesis
proof (cases q)
case (LPoly b vbs)
with oLPoly wf_p wf_q check weak_gt[of a b] have ab: "a ≻ b" and ppvars: "isOK(check_pvars ?R ?wgt vas vbs)" and
wf_a: "a ∈ carrier R" and wf_b: "b ∈ carrier R" and wf_vas: "wf_pvars R vas" and wf_vbs: "wf_pvars R vbs" by auto
{
fix α
have "wf_ass R α ∧ pos_ass α ⟶ (a ⊕ (eval_pvars α vas)) ≻ (b ⊕ (eval_pvars α vbs))" (is "?ass ⟶ ?goal")
proof
assume ass: ?ass
show ?goal
proof (cases psm)
case True
with ppvars have pvars: "isOK(check_pvars ?R op ≽ vas vbs)" by auto
show ?goal
by (rule plus_gt_left_mono2[OF _ check_pvars_sound[OF pvars]], insert
ass pvars wf_vas wf_vbs True wf_a wf_b ab, auto)
next
case False
with ppvars have pvars: "isOK(check_pvars ?R wgt vas vbs)" by auto
have gt: "eval_pvars α vas ≻ eval_pvars α vbs"
by (rule check_pvars_gt_sound[OF pvars weak_gt], insert False LPoly oLPoly ass wf_vas wf_vbs, auto)
show ?thesis
by (rule plus_gt_both_mono[OF ab gt], auto simp: wf_a wf_b ass wf_vas wf_vbs False)
qed
qed
}
hence "(LPoly a vas, LPoly b vbs) ∈ poly_s" unfolding poly_s_def by auto
with LPoly oLPoly show ?thesis by auto
qed
qed
declare check_lpoly_ns.simps[simp del]
declare check_lpoly_s.simps[simp del]
end
context lpoly_order
begin
lemmas poly_order_simps = one_geq_zero default_geq_zero arc_pos_plus arc_pos_mult arc_pos_max0 arc_pos_default
declare poly_simps [simp del]
end
end