Theory Delta_Poly_Termination_Undecidable
section ‹Undecidability of Polynomial Termination using ‹δ›-Orders›
theory Delta_Poly_Termination_Undecidable
imports
Poly_Termination_Undecidable
begin
context poly_input
begin
definition y8 :: var where "y8 = 7"
definition y9 :: var where "y9 = 8"
text ‹Definition 6.3›
definition "lhs_Q = Fun f_sym [
q_t (h_t (Var y1)),
h_t (Var y2),
h_t (Var y3),
g_t (q_t (Var y4)) (h_t (h_t (h_t (Var y4)))),
q_t (Var y5),
a_t (Var y6) (Var y6),
Var y7,
Var y8,
h_t (a_t (encode_poly y9 p) (Var y9))]"
fun g_list :: "_ ⇒ (symbol,var)term" where
"g_list [] = z_t"
| "g_list ((f,n) # fs) = g_t (Fun f (replicate n z_t)) (g_list fs)"
definition symbol_list where "symbol_list = [(f_sym,9),(q_sym,1),(h_sym,1),(a_sym,2)] @ map (λ i. (v_sym i, 1)) V_list"
definition t_t :: "(symbol,var)term" where "t_t = (g_list ((z_sym,0) # symbol_list))"
definition "rhs_Q = Fun f_sym [
h_t (h_t (q_t (Var y1))),
g_t (Var y2) (Var y2),
Fun f_sym (replicate 9 (Var y3)),
q_t (g_t (Var y4) t_t),
a_t (Var y5) (Var y5),
q_t (Var y6),
a_t z_t (Var y7),
a_t (Var y8) z_t,
a_t (encode_poly y9 q) (Var y9)]"
definition Q where "Q = {(lhs_Q, rhs_Q)}"
definition F_Q where "F_Q = {(f_sym,9), (h_sym,1), (g_sym,2), (q_sym,1)} ∪ F"
lemma lhs_Q_F: "funas_term lhs_Q ⊆ F_Q"
proof -
from funas_encode_poly_p
show "funas_term lhs_Q ⊆ F_Q" unfolding lhs_Q_def by (auto simp: F_Q_def F_def)
qed
lemma g_list_F: "set zs ⊆ F_Q ⟹ funas_term (g_list zs) ⊆ F_Q"
proof (induct zs)
case Nil
thus ?case by (auto simp: F_Q_def F_def)
next
case (Cons fa ts)
then obtain f a where fa: "fa = (f,a)" and inF: "(f,a) ∈ F_Q" by (cases fa, auto)
have "{(g_sym,Suc (Suc 0)),(z_sym,0)} ⊆ F_Q" by (auto simp: F_Q_def F_def)
with Cons fa inF show ?case by auto
qed
lemma symbol_list: "set symbol_list ⊆ F_Q" unfolding symbol_list_def F_Q_def F_def using V_list by auto
lemma t_F: "funas_term t_t ⊆ F_Q"
unfolding t_t_def using g_list_F[OF symbol_list]
by (auto simp: F_Q_def F_def)
lemma vars_g_list[simp]: "vars_term (g_list zs) = {}"
by (induct zs, auto)
lemma vars_t: "vars_term t_t = {}"
unfolding t_t_def by simp
lemma rhs_Q_F: "funas_term rhs_Q ⊆ F_Q"
proof -
from funas_encode_poly_q
show "funas_term rhs_Q ⊆ F_Q" unfolding rhs_Q_def using t_F by (auto simp: F_Q_def F_def)
qed
context
fixes I :: "symbol ⇒ 'a :: linordered_field mpoly" and δ :: 'a and a3 a2 a1 a0 z0 v
assumes I: "I a_sym = Const a3 * PVar 0 * PVar 1 + Const a2 * PVar 0 + Const a1 * PVar 1 + Const a0"
"I z_sym = Const z0"
"I (v_sym i) = mpoly_of_poly 0 (v i)"
and a: "a3 > 0" "a2 > 0" "a1 > 0" "a0 ≥ 0"
and z: "z0 ≥ 0"
and v: "nneg_poly (v i)" "degree (v i) > 0"
begin
lemma nneg_combination: assumes "nneg_poly r"
shows "nneg_poly ([:a1, a3:] * r + [:a0, a2:])"
by (intro nneg_poly_add nneg_poly_mult assms, insert a, auto)
lemma degree_combination: assumes "nneg_poly r"
shows "degree ([:a1, a3:] * r + [:a0, a2:]) = Suc (degree r)"
using nneg_poly_degree_add_1[OF assms, OF a(1) a(2)] by auto
lemma degree_eval_encode_num: assumes c: "c ≥ 0"
shows "∃ p. mpoly_of_poly x p = poly_inter.eval I (encode_num x c) ∧ nneg_poly p ∧ int (degree p) = c"
proof -
interpret poly_inter UNIV I .
from assms obtain n where cn: "c = int n" by (metis nonneg_eq_int)
hence natc: "nat c = n" by auto
note [simp] = I
show ?thesis unfolding encode_num_def natc unfolding cn int_int_eq
proof (induct n)
case 0
show ?case using z by (auto simp: intro!: exI[of _ "[:z0:]"])
next
case (Suc n)
define t where "t = (((λt. Fun a_sym [TVar x, t]) ^^ n) (Fun z_sym []))"
from Suc obtain p where mp: "mpoly_of_poly x p = eval t"
and deg: "degree p = n" and p: "nneg_poly p" by (auto simp: t_def)
show ?case apply (simp add: t_def[symmetric])
apply (unfold deg[symmetric])
apply (intro exI[of _ "[: a1, a3:] * p + [:a0, a2:]"] conjI mpoly_extI degree_combination p nneg_combination)
by (simp add: mp insertion_add insertion_mult field_simps)
qed
qed
lemma degree_eval_encode_monom: assumes c: "c > 0"
and α: "α = (λ i. int (degree (v i)))"
shows "∃ p. mpoly_of_poly y p = poly_inter.eval I (encode_monom y m c) ∧ nneg_poly p ∧
int (degree p) = insertion α (mmonom m c) ∧ degree p > 0"
proof -
interpret poly_inter UNIV I .
define xes where "xes = var_list m"
from var_list[of m c]
have monom: "mmonom m c = Const c * (∏(x, e)← xes . PVar x ^ e) " unfolding xes_def .
show ?thesis unfolding encode_monom_def monom xes_def[symmetric]
proof (induct xes)
case Nil
show ?case using degree_eval_encode_num[of c y] c by auto
next
case (Cons xe xes)
obtain x e where xe: "xe = (x,e)" by force
define expr where "expr = rec_list (encode_num y c) (λa. case a of (i, e) ⇒ λ_. (λt. Fun (v_sym i) [t]) ^^ e)"
define exes where "exes = expr xes"
define ixes where "ixes = insertion α (Const c * (∏a← xes. case a of (x, a) ⇒ PVar x ^ a))"
have step: "expr (xe # xes) = ((λt. Fun (v_sym x) [t]) ^^ e) (exes)"
unfolding xe expr_def exes_def by auto
have step': "insertion α (Const c * (∏a←xe # xes. case a of (x, a) ⇒ PVar x ^ a))
= (α x)^e * ixes"
unfolding xe ixes_def by (simp add: insertion_mult insertion_power)
from Cons(1)[folded expr_def exes_def ixes_def] obtain p where
IH: "mpoly_of_poly y p = eval exes" "nneg_poly p"
"int (degree p) = ixes" "degree p > 0"
by auto
show ?case
unfolding expr_def[symmetric]
unfolding step step'
proof (induct e)
case 0
thus ?case using IH by auto
next
case (Suc e)
define rec where "rec = ((λt. Fun (v_sym x) [t]) ^^ e) exes"
from Suc[folded rec_def] obtain p where
IH: "mpoly_of_poly y p = eval rec" "nneg_poly p" "int (degree p) = α x ^ e * ixes" "degree p > 0" by auto
have "((λt. Fun (v_sym x) [t]) ^^ Suc e) exes = Fun (v_sym x) [rec]"
unfolding rec_def by simp
also have "eval … = substitute (λi. if i = 0 then eval ([rec] ! i) else 0) (poly_to_mpoly 0 (v x))"
by (simp add: I mpoly_of_poly_is_poly_to_mpoly)
also have "… = poly_to_mpoly y (v x ∘⇩p p)"
by (rule substitute_poly_to_mpoly, auto simp: IH(1)[symmetric] mpoly_of_poly_is_poly_to_mpoly)
finally have id: "eval (((λt. Fun (v_sym x) [t]) ^^ Suc e) exes) = poly_to_mpoly y (v x ∘⇩p p)" .
show ?case unfolding id mpoly_of_poly_is_poly_to_mpoly
proof (intro exI[of _ "v x ∘⇩p p"] conjI refl)
show "int (degree (v x ∘⇩p p)) = α x ^ Suc e * ixes"
unfolding degree_pcompose using IH(3) by (auto simp: α)
show "nneg_poly (v x ∘⇩p p)" using IH(2) v[of x]
by (intro nneg_poly_pcompose, insert IH, auto)
show "0 < degree (v x ∘⇩p p)" unfolding degree_pcompose using IH(4) v[of x] by auto
qed
qed
qed
qed
text ‹Lemma 6.2›
lemma degree_eval_encode_poly_generic: assumes "positive_poly r"
and α: "α = (λ i. int (degree (v i)))"
shows "∃ p. poly_to_mpoly x p = poly_inter.eval I (encode_poly x r) ∧ nneg_poly p ∧
int (degree p) = insertion α r"
proof -
interpret poly_inter UNIV I .
define mcs where "mcs = monom_list r"
from monom_list[of r] have r: "r = (∑(m, c)← mcs. mmonom m c)" unfolding mcs_def by auto
{
fix m c
assume mc: "(m,c) ∈ set mcs"
hence "c ≥ 0"
using monom_list_coeff assms unfolding mcs_def positive_poly_def by auto
moreover from mc have "c ≠ 0" unfolding mcs_def
by (transfer, auto)
ultimately have "c > 0" by auto
} note mcs = this
note [simp] = I
show ?thesis unfolding encode_poly_def mcs_def[symmetric] unfolding r insertion_sum_list map_map o_def
unfolding mpoly_of_poly_is_poly_to_mpoly[symmetric]
using mcs
proof (induct mcs)
case Nil
show ?case by (rule exI[of _ "[:z0:]"], insert z, auto)
next
case (Cons mc mcs)
define trm where "trm = rec_list (Fun z_sym []) (λa. case a of (m, c) ⇒ λ_ t. Fun a_sym [encode_monom x m c, t])"
define expr where "expr mcs = (∑x←mcs. insertion α (case x of (x, xa) ⇒ mmonom x xa))" for mcs
obtain m c where mc: "mc = (m,c)" by force
from Cons(2) mc have c: "c > 0" by auto
from degree_eval_encode_monom[OF this α, of x m]
obtain q where monom: "mpoly_of_poly x q = eval (encode_monom x m c)"
"nneg_poly q" "int (degree q) = insertion α (mmonom m c)"
and dq: "degree q > 0" by auto
from Cons(1)[folded trm_def expr_def, OF Cons(2)]
obtain p where IH: "mpoly_of_poly x p = eval (trm mcs)" "nneg_poly p" "int (degree p) = expr mcs" by force
have step: "trm (mc # mcs) = Fun a_sym [encode_monom x m c, trm mcs]"
unfolding mc trm_def by simp
have step': "expr (mc # mcs) = insertion α (mmonom m c) + expr mcs" unfolding mc expr_def by simp
have deg: "degree ([:a3:] * q * p + ([:a2:] * q + [:a1:] * p + [:a0:])) = degree p + degree q"
by (rule nneg_poly_degree_add, insert a IH monom, auto)
show ?case unfolding expr_def[symmetric] trm_def[symmetric]
unfolding step step'
unfolding IH(3)[symmetric] monom(3)[symmetric]
apply (intro exI[of _ "[:a3:] * q * p + [:a2:] * q + [:a1:] * p + [:a0:]"] conjI)
subgoal by (intro mpoly_extI, simp add: IH(1)[symmetric] monom(1)[symmetric] insertion_mult insertion_add)
subgoal by (intro nneg_poly_mult nneg_poly_add IH monom, insert a, auto)
subgoal using deg by (auto simp: ac_simps)
done
qed
qed
end
end
context delta_poly_inter
begin
lemma transp_gt_delta: "transp (λ x y. x ≥ y + δ)" using δ0
by (auto simp: transp_def)
lemma gt_delta_imp_ge: "y + δ ≤ x ⟹ y ≤ x" using δ0 by auto
lemma weakly_monotone_insertion: assumes mono: "monotone_poly (vars p) p"
and a: "assignment (a :: _ ⇒ 'a)"
and gt: "⋀ x. x ∈ vars p ⟹ a x + δ ≤ b x"
shows "insertion a p ≤ insertion b p"
using monotone_poly_wrt_insertion[OF transp_gt_delta gt_delta_imp_ge mono a, of b] gt δ0 by auto
text ‹Lemma 6.5›
lemma degree_partial_insertion_stays_constant: assumes mono: "monotone_poly (vars p) p"
shows "∃ a. assignment a ∧
(∀ b. (∀ y. a y + δ ≤ b y) ⟶ degree (partial_insertion a x p) = degree (partial_insertion b x p))"
using degree_partial_insertion_stays_constant_generic
[OF transp_gt_delta gt_delta_imp_ge poly_pinfty_ge mono, of δ x, simplified]
by metis
lemma degree_mono: assumes pos: "lead_coeff p ≥ (0 :: 'a)"
and le: "⋀ x. x ≥ c ⟹ poly p x ≤ poly q x"
shows "degree p ≤ degree q"
by (rule degree_mono_generic[OF poly_pinfty_ge assms])
lemma degree_mono': assumes "⋀ x. x ≥ c ⟹ (bnd :: 'a) ≤ poly p x ∧ poly p x ≤ poly q x"
shows "degree p ≤ degree q"
by (rule degree_mono'_generic[OF poly_pinfty_ge assms])
text ‹Lemma 6.6›
lemma subst_same_var_monotone_imp_same_degree:
assumes mono: "monotone_poly (vars p) (p :: 'a mpoly)"
and qp: "poly_to_mpoly x q = substitute (λi. PVar x) p"
shows "total_degree p = degree q"
proof (cases "total_degree p = 0")
case False
from False have p0: "p ≠ 0" by auto
obtain d where dq: "degree q = d" by blast
let ?mc = "(λ m. mmonom m (mcoeff p m))"
let ?cfs = "{m . mcoeff p m ≠ 0}"
let ?lc = "lead_coeff"
note fin = finite_coeff_support[of p]
define M where "M = total_degree p"
with False have M1: "M ≥ 1" by auto
from degree_monom_eq_total_degree[OF p0]
obtain mM where mM: "mcoeff p mM ≠ 0" "degree_monom mM = M" unfolding M_def by blast
from degree_substitute_same_var[of x p, folded M_def qp]
have dM: "d ≤ M" unfolding dq degree_poly_to_mpoly .
define p1 where "p1 = sum ?mc (?cfs ∩ {m. degree_monom m = M})"
define p2 where "p2 = sum ?mc (?cfs ∩ {m. degree_monom m < M})"
have "p = sum ?mc ?cfs"
by (rule mpoly_as_sum)
also have "?cfs = ?cfs ∩ {m. degree_monom m = M}
∪ ?cfs ∩ {m. degree_monom m ≠ M}" by auto
also have "?cfs ∩ {m. degree_monom m ≠ M} = ?cfs ∩ {m. degree_monom m < M}"
using degree_monon_le_total_degree[of p, folded M_def] by force
also have "sum ?mc (?cfs ∩ {m. degree_monom m = M} ∪ …) = p1 + p2" unfolding p1_def p2_def
using fin by (intro sum.union_disjoint, auto)
finally have p_split: "p = p1 + p2" .
have "total_degree p2 ≤ M - 1" unfolding p2_def
by (intro total_degree_sum_leI, subst total_degree_monom, auto)
also have "… < M" using M1 by auto
finally have deg_p': "total_degree p2 < M" by auto
have "p1 ≠ 0"
proof
assume "p1 = 0"
hence "p = p2" unfolding p_split by auto
hence "M = total_degree p2" unfolding M_def by simp
with deg_p' show False by auto
qed
with mpoly_ext_bounded_field[of "max 1 δ" p1 0] obtain b
where b: "⋀ v. b v ≥ max 1 δ" and bpm0: "insertion b p1 ≠ 0" by auto
from b have b1: "⋀ v. b v ≥ 1" and bδ: "⋀ v. b v ≥ δ" by auto
define c where "c = Max (insert 1 (b ` vars p)) + δ"
define X where "X = (0 :: nat)"
define pb where "pb p = mpoly_to_poly X (substitute (λ v. Const (b v) * PVar X) p)" for p
have c1: "c ≥ 1" unfolding c_def using vars_finite[of p] δ0 Max_ge[of _ "1 :: 'a"]
by (meson add_increasing2 finite.insertI finite_imageI insertI1 nless_le)
have varsX: "vars (substitute (λ v. Const (b v) * PVar X) p) ⊆ {X}" for p
by (intro vars_substitute order.trans[OF vars_mult], auto)
have pb: "substitute (λ v. Const (b v) * PVar X) p = poly_to_mpoly X (pb p)" for p
unfolding pb_def
by (rule mpoly_to_poly_inverse[symmetric, OF varsX])
have poly_pb: "poly (pb p) x = insertion (λv. b v * x) p" for x p
using arg_cong[OF pb, of "insertion (λ _. x)",
unfolded insertion_poly_to_mpoly]
by (auto simp: insertion_substitute insertion_mult)
define lb where "lb = insertion (λ _. 0) p"
{
fix x
have "poly (pb p) x = insertion (λv. b v * x) p" by fact
also have "… = insertion (λv. b v * x) p1 + insertion (λv. b v * x) p2" unfolding p_split
by (simp add: insertion_add)
also have "insertion (λv. b v * x) p1 = insertion b p1 * x^M"
unfolding p1_def insertion_sum insertion_mult insertion_monom sum_distrib_right
power_mult_distrib
proof (intro sum.cong[OF refl], goal_cases)
case (1 m)
from 1 have M: "M = degree_monom m" by auto
have "{ v. lookup m v ≠ 0} ⊆ keys m"
by (simp add: keys.rep_eq)
from finite_subset[OF this] have fin: "finite { v. lookup m v ≠ 0}" by auto
have "(∏v. b v ^ lookup m v * x ^ lookup m v)
= (∏v. b v ^ lookup m v) * (∏v. x ^ lookup m v)"
by (subst (1 2 3) Prod_any.expand_superset[OF fin])
(insert zero_less_iff_neq_zero, force simp: prod.distrib)+
also have "(∏v. x ^ lookup m v) = x ^ M" unfolding M degree_monom_def
by (smt (verit) Prod_any.conditionalize Prod_any.cong finite_keys in_keys_iff power_0 power_sum)
finally show ?case by simp
qed
also have "insertion (λv. b v * x) p2 = poly (pb p2) x" unfolding poly_pb ..
finally have "poly (pb p) x = poly (monom (insertion b p1) M + pb p2) x" by (simp add: poly_monom)
}
hence pbp_split: "pb p = monom (insertion b p1) M + pb p2" by blast
have "degree (pb p2) ≤ total_degree p2" unfolding pb_def
apply (subst degree_mpoly_to_poly)
apply (simp add: varsX)
by (rule degree_substitute_const_same_var)
also have "… < M" by fact
finally have deg_pbp2: "degree (pb p2) < M" .
have "degree (monom (insertion b p1) M) = M" using bpm0 by (rule degree_monom_eq)
with deg_pbp2 pbp_split have deg_pbp: "degree (pb p) = M" unfolding pbp_split
by (subst degree_add_eq_left, auto)
have "?lc (pb p) = insertion b p1" unfolding pbp_split
using deg_pbp2 bpm0 coeff_eq_0 deg_pbp pbp_split by auto
define bnd where "bnd = insertion (λ _. 0) p"
{
fix x :: 'a
assume x1: "x ≥ 1"
hence x: "x ≥ 0" by simp
have ass: "assignment (λ v. b v * x)" unfolding assignment_def using x b1
by (meson linorder_not_le mult_le_cancel_right1 order_trans)
have "poly (pb p) x = insertion (λv. b v * x) p" by fact
also have "insertion (λ v. b v * x) p ≤ insertion (λ v. c * x) p"
proof (rule weakly_monotone_insertion[OF mono ass])
fix v
assume v: "v ∈ vars p"
have "b v + δ ≤ c" unfolding c_def using vars_finite[of p] v Max_ge[of _ "b v"] by auto
thus "b v * x + δ ≤ c * x" using b[of v] x1 c1 δ0
by (smt (verit) c_def add_le_imp_le_right add_mono comm_semiring_class.distrib mult.commute mult_le_cancel_right1 mult_right_mono order.asym x)
qed
also have "… = poly q (c * x)" unfolding poly_to_mpoly_substitute_same[OF qp] ..
also have "… = poly (q ∘⇩p [:0, c:]) x" by (simp add: poly_pcompose ac_simps)
finally have ineq: "poly (pb p) x ≤ poly (q ∘⇩p [:0, c:]) x" .
have "bnd ≤ insertion (λv. b v * x) p" unfolding bnd_def
apply (intro weakly_monotone_insertion[OF mono])
subgoal by (simp add: assignment_def)
subgoal for v using bδ[of v] x1 δ0
by simp (metis dual_order.trans less_le_not_le mult_le_cancel_left1)
done
also have "… = poly (pb p) x" using poly_pb by auto
finally have "bnd ≤ poly (pb p) x" by auto
note this ineq
} note pb_approx = this
have "M = degree (pb p)" unfolding deg_pbp ..
also have "… ≤ degree (q ∘⇩p [:0, c:])"
by (intro degree_mono'[of 1 bnd], insert pb_approx, auto)
also have "… ≤ d" by (simp add: dq)
finally have deg_pbp: "M ≤ d" .
with dM have "M = d" by auto
thus ?thesis unfolding M_def dq .
next
case True
then obtain c where p: "p = Const c" using degree_0_imp_Const by blast
with qp have "poly_to_mpoly x q = p" by auto
thus ?thesis
by (metis True degree_Const degree_poly_to_mpoly p)
qed
lemma monotone_poly_partial_insertion:
assumes x: "x ∈ xs"
and mono: "monotone_poly xs p"
and ass: "assignment a"
shows "0 < degree (partial_insertion a x p)"
"lead_coeff (partial_insertion a x p) > 0"
"valid_poly p ⟹ y ≥ 0 ⟹ poly (partial_insertion a x p) y ≥ y - δ"
"valid_poly p ⟹ insertion a p ≥ a x - δ"
proof -
have 0: "1 ≤ inverse δ * δ" using δ0 by auto
define ceil_nat :: "'a ⇒ nat" where "ceil_nat x = nat (ceiling x)" for x
have 1: "x ≤ of_nat (ceil_nat x)" for x unfolding ceil_nat_def
by (simp add: of_nat_ceiling)
note main = monotone_poly_partial_insertion_generic[OF transp_gt_delta gt_delta_imp_ge poly_pinfty_ge refl δ0 0 1 x mono ass, simplified]
show "0 < degree (partial_insertion a x p)" "0 < lead_coeff (partial_insertion a x p)"
using main by auto
assume valid: "valid_poly p"
from main(3)[OF this] have estimation: "δ * of_nat y ≤ poly (partial_insertion a x p) (δ * of_nat y)" for y by auto
{
fix y :: 'a
assume y: "y ≥ 0"
with ass have ass': "assignment (a(x := y))" unfolding assignment_def by auto
from valid[unfolded valid_poly_def, rule_format, OF ass']
have ge0: "insertion (a(x := y)) p ≥ 0" by auto
have id: "poly (partial_insertion a x p) y = insertion (a(x := y)) p"
using insertion_partial_insertion[of x a "a(x:=y)" p] by auto
show "y - δ ≤ poly (partial_insertion a x p) y"
proof (cases "y ≥ δ")
case False
with ge0[folded id] y show ?thesis by auto
next
case True
define z where "z = y - δ"
from True have z0: "z ≥ 0" unfolding z_def by auto
define n where "n = nat (floor (z * inverse δ))"
have "δ * of_nat n ≤ z" unfolding n_def using δ0 z0
by (metis field_class.field_divide_inverse mult_of_nat_commute mult_zero_left of_nat_floor pos_le_divide_eq)
hence gt: "δ * of_nat n + δ ≤ y" unfolding z_def by auto
define b where "b = a(x := δ * of_nat n)"
have ass_b: "assignment b" using δ0 ass unfolding b_def assignment_def by auto
from mono[unfolded monotone_poly_wrt_def, rule_format, OF ass_b x, of y] gt
have gt: "insertion b p ≤ insertion (b(x := y)) p - δ" by (auto simp: b_def)
have "δ * of_nat n + δ ≥ z" unfolding n_def using δ0 z0
by (smt (verit, del_insts) comm_semiring_class.distrib field_class.field_divide_inverse floor_divide_upper inverse_nonnegative_iff_nonnegative mult.commute mult_cancel_left2 mult_nonneg_nonneg of_nat_nat order_less_le z_def z_def z_def zero_le_floor)
hence "y - 2 * δ ≤ δ * of_nat n" unfolding z_def by auto
also have "δ * of_nat n ≤ poly (partial_insertion a x p) (δ * of_nat n)"
by fact
also have "… = insertion b p" using insertion_partial_insertion[of x a b p]
by (auto simp: b_def)
also have "… ≤ insertion (b(x := y)) p - δ" by fact
also have "insertion (b(x := y)) p = poly (partial_insertion a x p) y"
using insertion_partial_insertion[of x a "b(x := y)" p]
by (auto simp: b_def)
finally show ?thesis by simp
qed
} note estimation = this
from ass have "a x ≥ 0" unfolding assignment_def by auto
from estimation[OF this] show "insertion a p ≥ a x - δ"
using insertion_partial_insertion[of x a a p] by auto
qed
end
context solvable_poly_problem
begin
context
assumes "SORT_CONSTRAINT('a :: floor_ceiling)"
begin
context
fixes h :: 'a
begin
fun IQ :: "symbol ⇒ 'a mpoly" where
"IQ f_sym = PVar 0 + PVar 1 + PVar 2 + PVar 3 + PVar 4 + PVar 5 + PVar 6 + PVar 7 + PVar 8"
| "IQ a_sym = PVar 0 * PVar 1 + PVar 0 + PVar 1"
| "IQ z_sym = 0"
| "IQ (v_sym i) = PVar 0 ^ (nat (α i))"
| "IQ q_sym = PVar 0 * PVar 0 + Const 2 * PVar 0"
| "IQ g_sym = PVar 0 + PVar 1"
| "IQ h_sym = Const h * PVar 0 + Const h"
| "IQ o_sym = 0"
interpretation interQ: poly_inter F_Q IQ "(λx y. x ≥ y + (1 :: 'a))" .
text ‹Lemma 6.2 specialized for this interpretation›
lemma degree_eval_encode_poly: assumes "positive_poly r"
shows "∃p. poly_to_mpoly y9 p = interQ.eval (encode_poly y9 r) ∧ nneg_poly p ∧ int (degree p) = insertion α r"
proof -
define v where "v i = (monom 1 (nat (α i)) :: 'a poly)" for i
define γ where "γ = (λi. int (degree (v i)))"
have nneg_v: "nneg_poly (v i)" "0 < degree (v i)" for i unfolding v_def using α1[of i]
by (auto simp: nneg_poly_def degree_monom_eq poly_monom)
have id: "int (Polynomial.degree (v i)) = α i" for i unfolding v_def
using α1[of i] by (auto simp: nneg_poly_def degree_monom_eq)
have "IQ (v_sym i) = mpoly_of_poly 0 (v i)" for i
unfolding v_def by (intro mpoly_extI, simp add: insertion_power poly_monom)
from degree_eval_encode_poly_generic[of IQ 1 1 1 0 0 v _ γ, OF _ _ this, simplified, OF nneg_v assms γ_def,
unfolded id]
show ?thesis by auto
qed
definition pp where "pp = (SOME pp. poly_to_mpoly y9 pp = interQ.eval (encode_poly y9 p) ∧ nneg_poly pp ∧ int (degree pp) = insertion α p)"
lemma pp: "interQ.eval (encode_poly y9 p) = poly_to_mpoly y9 pp"
"nneg_poly pp" "int (degree pp) = insertion α p"
using someI_ex[OF degree_eval_encode_poly[OF pq(1)], folded pp_def] by auto
definition qq where "qq = (SOME qq. poly_to_mpoly y9 qq = interQ.eval (encode_poly y9 q) ∧ nneg_poly qq ∧ int (degree qq) = insertion α q)"
lemma qq: "interQ.eval (encode_poly y9 q) = poly_to_mpoly y9 qq"
"nneg_poly qq" "int (degree qq) = insertion α q"
using someI_ex[OF degree_eval_encode_poly[OF pq(2)], folded qq_def] by auto
definition "ppp = pp * [:1,1:] + [:0,1:]"
definition "qqq = qq * [:1,1:] + [:0,1:]"
lemma degree_ppp: "int (degree ppp) = 1 + insertion α p"
unfolding ppp_def pp(3)[symmetric]
using nneg_poly_degree_add_1[OF pp(2), of 1 1 1 0] by simp
lemma degree_qqq: "int (degree qqq) = 1 + insertion α q"
unfolding qqq_def qq(3)[symmetric]
using nneg_poly_degree_add_1[OF qq(2), of 1 1 1 0] by simp
lemma ppp_qqq: "degree ppp ≥ degree qqq"
using degree_ppp degree_qqq α(2) by auto
lemma nneg_ppp: "nneg_poly ppp"
unfolding ppp_def
by (intro nneg_poly_add nneg_poly_mult pp, auto)
definition H where "H = (SOME H. ∀ h ≥ H. ∀x≥0. poly qqq x ≤ h * poly ppp x + h)"
lemma H: "h ≥ H ⟹ x ≥ 0 ⟹ poly qqq x ≤ h * poly ppp x + h"
proof -
from poly_degree_le_large_const[OF ppp_qqq nneg_poly_nneg[OF nneg_ppp]]
have "∃H. ∀h≥H. ∀x≥0. poly qqq x ≤ h * poly ppp x + h" by auto
from someI_ex[OF this, folded H_def]
show "h ≥ H ⟹ x ≥ 0 ⟹ poly qqq x ≤ h * poly ppp x + h" by auto
qed
end
definition h where "h = max 9 (H 1)"
lemma h: "h ≥ 1" unfolding h_def by auto
abbreviation I_Q where "I_Q ≡ IQ h"
interpretation inter_Q: poly_inter F_Q I_Q "(λx y. x ≥ y + (1 :: 'a))" .
text ‹Well-definedness of Interpretation in Theorem 6.4›
lemma valid_monotone_inter_Q:
"inter_Q.valid_monotone_poly_inter"
unfolding inter_Q.valid_monotone_poly_inter_def
proof (intro ballI)
note [simp] = insertion_add insertion_mult
fix fn
assume f: "fn ∈ F_Q"
then consider
(a) "fn = (a_sym,2)"
| (g) "fn = (g_sym,2)"
| (h) "fn = (h_sym,1)"
| (q) "fn = (q_sym,1)"
| (f) "fn = (f_sym,9)"
| (z) "fn = (z_sym,0)"
| (v) i where "fn = (v_sym i, 1)" "i ∈ V"
unfolding F_Q_def F_def by auto
thus "inter_Q.valid_monotone_poly fn"
proof cases
case *: a
have vars: "vars (PVar 0 * PVar 1 + PVar 0 + PVar 1 :: 'a mpoly) = {0,1}"
apply (intro vars_eqI)
subgoal by (intro vars_mult_subI vars_add_subI, auto)
subgoal for v by (intro exI[of _ "λ _. 1"] exI[of _ 0], auto)
done
show ?thesis unfolding inter_Q.valid_monotone_poly_def *
apply (intro allI impI, clarify, unfold IQ.simps vars valid_poly_def
monotone_poly_wrt_def
insertion_mult insertion_add insertion_Var,
intro conjI allI impI)
subgoal for α unfolding assignment_def by simp
subgoal for _ _ _ α x v
proof goal_cases
case 1
from assignmentD[OF 1(1)] have 0: "α 0 ≥ 0" "α 1 ≥ 0" by auto
from 1 have "x = 0 ∨ x = 1" by auto
thus ?case using 0 1(3) mult_right_mono[OF 1(3), of "α (x - 1)"]
by (auto simp: field_simps)
(smt (verit, ccfv_threshold) "1"(3) add.assoc add.commute add_increasing add_le_imp_le_right add_right_mono diff_ge_0_iff_ge le_add_diff_inverse2 mult_right_mono zero_less_one_class.zero_le_one)
qed
subgoal by auto
done
next
case *: f
have vars: "vars (PVar 0 + PVar 1 + PVar 2 + PVar 3 + PVar 4 + PVar 5 + PVar 6 + PVar 7 + PVar 8 :: 'a mpoly) = {0,1,2,3,4,5,6,7,8}"
apply (intro vars_eqI)
subgoal by (intro vars_mult_subI vars_add_subI, auto)
subgoal for v by (intro exI[of _ "λ _. 1"] exI[of _ 0], auto)
done
show ?thesis unfolding inter_Q.valid_monotone_poly_def *
apply (intro allI impI, clarify, unfold IQ.simps vars valid_poly_def
monotone_poly_wrt_def
insertion_mult insertion_add insertion_Var,
intro conjI allI impI)
subgoal for α unfolding assignment_def by simp
subgoal for _ _ _ α x v
proof goal_cases
case 1
hence "x ∈ {0,1,2,3,4,5,6,7,8}" by auto
thus ?case using 1(3) by auto
qed
subgoal by auto
done
next
case *: h
have vars: "vars (Const h * PVar 0 + Const h :: 'a mpoly) = {0}"
apply (intro vars_eqI)
subgoal by (intro vars_mult_subI vars_add_subI, auto)
subgoal for v using h by (intro exI[of _ "λ _. 1"] exI[of _ 0], auto)
done
show ?thesis unfolding inter_Q.valid_monotone_poly_def *
apply (intro allI impI, clarify, unfold IQ.simps vars valid_poly_def
monotone_poly_wrt_def
insertion_mult insertion_add insertion_Var,
intro conjI allI impI)
subgoal for α using h unfolding assignment_def by simp
subgoal for _ _ _ α x v
proof goal_cases
case 1
from assignmentD[OF 1(1), of 0]
show ?case using 1 h
by (auto simp: field_simps)
(smt (verit, ccfv_threshold) add.commute add_le_cancel_left distrib_left linordered_nonzero_semiring_class.zero_le_one mult.commute mult_cancel_left1 mult_left_mono nle_le order_trans)
qed
subgoal by auto
done
next
case z
thus ?thesis by (auto simp: inter_Q.valid_monotone_poly_def valid_poly_def monotone_poly_wrt_def)
next
case *: g
have vars: "vars (PVar 0 + PVar 1 :: 'a mpoly) = {0,1}"
apply (intro vars_eqI)
subgoal by (intro vars_mult_subI vars_add_subI, auto)
subgoal for v by (intro exI[of _ "λ _. 1"] exI[of _ 0], auto)
done
show ?thesis unfolding inter_Q.valid_monotone_poly_def *
apply (intro allI impI, clarify, unfold IQ.simps vars valid_poly_def
monotone_poly_wrt_def
insertion_mult insertion_add insertion_Var,
intro conjI allI impI)
subgoal for α unfolding assignment_def by simp
subgoal for _ _ _ α x v
proof goal_cases
case 1
hence "x ∈ {0,1}" by auto
thus ?case using 1(3) by auto
qed
subgoal by auto
done
next
case *: q
have vars: "vars (PVar 0 * PVar 0 + Const 2 * PVar 0 :: 'a mpoly) = {0}"
apply (intro vars_eqI)
subgoal by (intro vars_mult_subI vars_add_subI, auto)
subgoal for v by (intro exI[of _ "λ _. 1"] exI[of _ 2], auto)
done
show ?thesis unfolding inter_Q.valid_monotone_poly_def *
apply (intro allI impI, clarify, unfold IQ.simps vars valid_poly_def
monotone_poly_wrt_def
insertion_mult insertion_add insertion_Var,
intro conjI allI impI)
subgoal for α unfolding assignment_def by simp
subgoal for _ _ _ α x v
proof goal_cases
case 1
hence [simp]: "x = 0" by auto
from 1(1) have "α 0 ≥ 0" unfolding assignment_def by simp
thus ?case using 1(3)
by auto
(metis (no_types, opaque_lifting) add.assoc add_mono le_add_same_cancel1 mult_2 mult_mono order_trans zero_less_one_class.zero_le_one)
qed
subgoal by auto
done
next
case *: (v i)
from α[unfolded positive_interpr_def] have pos: "α i > 0" by auto
have vars: "vars ((PVar 0)^(nat (α i)):: 'a mpoly) = {0}"
apply (intro vars_eqI)
subgoal by (metis Preliminaries_on_Polynomials_1.vars_Var vars_power)
subgoal for v using pos apply (intro exI[of _ "λ _. 2"] exI[of _ 1])
by (auto simp: insertion_power)
(metis less_numeral_extra(4) one_less_numeral_iff one_less_power semiring_norm(76) zero_less_nat_eq)
done
show ?thesis unfolding inter_Q.valid_monotone_poly_def *
apply (intro allI impI, clarify, unfold IQ.simps vars valid_poly_def
monotone_poly_wrt_def
insertion_Var insertion_power,
intro conjI allI impI)
subgoal for _ _ _ β using pos unfolding assignment_def by simp
subgoal for _ _ _ β x v
proof goal_cases
case 1
hence [simp]: "x = 0" by auto
from 1(1) have b0: "β 0 ≥ 0" unfolding assignment_def by simp
from pos obtain k where nik: "nat (α i) = Suc k"
using gr0_implies_Suc zero_less_nat_eq by presburger
define b0 where "b0 = β 0"
have "β 0 ^ nat (α i) + 1 ≤ (β 0 + 1) ^ nat (α i)" using b0 unfolding nik b0_def[symmetric]
proof (induct k)
case (Suc k)
define sk where "sk = Suc k"
from Suc show ?case unfolding sk_def[symmetric]
by (auto simp: field_simps add_mono ordered_comm_semiring_class.comm_mult_left_mono)
qed auto
also have "… ≤ v ^ nat (α i)" using 1(3) by (simp add: b0 power_mono)
finally show ?case by simp
qed
subgoal by auto
done
qed
qed
lemma I_Q_delta_poly_inter: "delta_poly_inter F_Q I_Q (1 :: 'a)"
by (unfold_locales, rule valid_monotone_inter_Q, auto)
interpretation inter_Q: delta_poly_inter F_Q I_Q "1 :: 'a" by (rule I_Q_delta_poly_inter)
text ‹Orientation part of Theorem 6.4›
lemma orient_Q: "inter_Q.orient_rule (lhs_Q, rhs_Q)"
unfolding inter_Q.orient_rule_def split inter_Q.I'_is_insertion_eval
proof (intro allI impI)
fix x :: "_ ⇒ 'a"
assume "assignment x"
hence x: "x i ≥ 0" for i unfolding assignment_def by auto
have h9: "h ≥ 9" unfolding h_def by auto
define l where "l i = args (lhs_Q) ! i" for i
define r where "r i = args (rhs_Q) ! i" for i
let ?e = "inter_Q.eval"
let ?poly = "λ t. insertion x (?e t)"
note defs = l_def r_def lhs_Q_def rhs_Q_def
let ?nums = "[0,1,2,3,4,5,6,7,8] :: nat list"
note [simp] = insertion_add insertion_mult y1_def y2_def y3_def y4_def y5_def y6_def y7_def y8_def y9_def
have e_lhs: "?e lhs_Q = sum_list (map (λ i. (?e (l i))) ?nums)"
unfolding defs by simp
have e_rhs: "?e rhs_Q = sum_list (map (λ i. (?e (r i))) ?nums)"
unfolding defs by simp
have [simp]: "2 = (Const (2 :: 'a))"
by (metis mpoly_Const_1 mpoly_Const_add one_add_one)
have "?poly (r 0) = h^2 * ((x 0)^2 + 2 * x 0) + h^2 + h"
by (simp add: field_simps power2_eq_square defs)
also have "… ≤ (h * x 0 + h)^2 + 2 * (h * x 0 + h)" using h x[of 0]
by (simp add: field_simps power2_eq_square)
also have "… = ?poly (l 0)"
by (simp add: field_simps power2_eq_square defs)
finally have 1: "?poly (l 0) ≥ ?poly (r 0)" .
from h9 have h2: "h ≥ 2" by auto
have "?poly (r 1) = 2 * x 1"
by (simp add: field_simps defs)
also have "… ≤ h * x 1 + h" using mult_right_mono[OF h2 x[of 1]] h
by auto
also have "… = ?poly (l 1)"
by (simp add: field_simps power2_eq_square defs)
finally have 2: "?poly (l 1) ≥ ?poly (r 1)" .
have "?poly (r 2) + 1 = 9 * x 2 + 1" unfolding defs by simp
also have "… ≤ h * x 2 + h"
by (intro add_mono h mult_right_mono h9 x)
also have "… = ?poly (l 2)" unfolding defs by simp
finally have 3: "?poly (l 2) ≥ ?poly (r 2) + 1" .
have eval_vs: "insertion x (inter_Q.eval (g_list (map (λi. (v_sym i, Suc 0)) xs))) = 0"
for xs by (induct xs, auto simp: insertion_power α1)
have [simp]: "insertion x (inter_Q.eval t_t) = h" unfolding t_t_def symbol_list_def
by (simp add: eval_vs)
have "?poly (r 3) = (x 3 + h)^2 + 2 * (x 3 + h)"
by (simp add: field_simps power2_eq_square defs)
also have "… ≤ (x 3)^2 + 2 * x 3 + h^3*x 3 + h^3 + h^2 + h" (is "?l ≤ ?r")
proof -
have "2 * 1 ≤ h * h"
by (intro mult_mono, insert h2, auto)
hence hh: "h * h ≥ 2" by auto
have "?l ≤ ?r ⟷ 1 * h + (2 * h) * x 3 ≤ (h * h) * h + ((h * h) * h) * x 3"
by (auto simp: field_simps power2_eq_square defs power3_eq_cube)
also have "…"
by (intro add_mono mult_right_mono x, insert h hh, auto)
finally show ?thesis .
qed
also have "… = ?poly (l 3)"
by (simp add: field_simps power2_eq_square defs power3_eq_cube)
finally have 4: "?poly (l 3) ≥ ?poly (r 3)" .
have "?poly (r 4) = ((x 4)^2 + 2 * x 4)"
by (simp add: field_simps power2_eq_square defs)
also have "… = ?poly (l 4)"
by (simp add: field_simps power2_eq_square defs)
finally have 5: "?poly (l 4) ≥ ?poly (r 4)" by simp
have "?poly (r 5) = (x 5)^2 + 2 * x 5"
by (simp add: field_simps power2_eq_square defs)
also have "… = ?poly (l 5)"
by (simp add: field_simps power2_eq_square defs)
finally have 6: "?poly (l 5) ≥ ?poly (r 5)" by simp
have 7: "?poly (l 6) ≥ ?poly (r 6)" unfolding defs using h x[of 6]
by (simp add: add_increasing2 linorder_not_le mult_le_cancel_right1)
have 8: "?poly (l 7) ≥ ?poly (r 7)" unfolding defs using h x[of 7]
by (simp add: add_increasing2 linorder_not_le mult_le_cancel_right1)
have 9: "?poly (l 8) ≥ ?poly (r 8)"
proof -
have r: "?e (r 8) = poly_to_mpoly 8 (qqq h)"
unfolding defs qqq_def
by (simp add: qq[unfolded y9_def] algebra_simps smult_conv_mult_Const Const_mult flip: mpoly_of_poly_is_poly_to_mpoly)
have l: "?e (l 8) = poly_to_mpoly 8 ([:h:] * (ppp h) + [:h:])"
unfolding defs ppp_def
by (simp add: pp[unfolded y9_def] algebra_simps smult_conv_mult_Const Const_mult flip: mpoly_of_poly_is_poly_to_mpoly)
{
fix r
assume r: "r ∈ {p,q}"
with funas_encode_poly_p funas_encode_poly_q
have funas: "funas_term (encode_poly y9 r) ⊆ F" by auto
have "poly_inter.eval (IQ 1) (encode_poly y9 r) = inter_Q.eval (encode_poly y9 r)"
by (rule poly_inter_eval_cong, insert funas, auto simp: F_def)
} note encode_eq = this
have pp_eq: "pp h = pp 1" unfolding pp_def using encode_eq[of p] by auto
have qq_eq: "qq h = qq 1" unfolding qq_def using encode_eq[of q] by auto
have ppp_eq: "ppp h = ppp 1" unfolding ppp_def pp_eq ..
have qqq_eq: "qqq h = qqq 1" unfolding qqq_def qq_eq ..
have "H h = H 1" unfolding H_def ppp_eq qqq_eq ..
also have "… ≤ h" unfolding h_def by auto
finally have h: "h ≥ H h" .
show ?thesis unfolding l r using H[OF h x[of 8]] by simp
qed
have "?poly rhs_Q + 1 =
?poly (r 0) + ?poly (r 1) + (?poly (r 2) + 1) + ?poly (r 3) + ?poly (r 4) + ?poly (r 5) + ?poly (r 6) + ?poly (r 7) + ?poly (r 8)"
unfolding e_rhs by simp
also have "… ≤ ?poly (l 0) + ?poly (l 1) + ?poly (l 2) + ?poly (l 3) + ?poly (l 4) + ?poly (l 5) + ?poly (l 6) + ?poly (l 7) + ?poly (l 8)"
by (intro add_mono 1 2 3 4 5 6 7 8 9)
also have "… = ?poly lhs_Q"
unfolding e_lhs by simp
finally show "?poly rhs_Q + 1 ≤ ?poly lhs_Q" by auto
qed
end
end
context poly_input
begin
text ‹Theorem 6.4›
theorem solution_impl_delta_termination_of_Q:
assumes "positive_poly_problem p q"
shows "termination_by_delta_poly_interpretation (TYPE('a :: floor_ceiling)) F_Q Q"
proof -
interpret solvable_poly_problem
by (unfold_locales, fact)
interpret I: delta_poly_inter F_Q I_Q "(1 :: 'a)" by (rule I_Q_delta_poly_inter)
show ?thesis
unfolding termination_by_delta_poly_interpretation_def
proof (intro exI[of _ "1 :: 'a"] exI[of _ I_Q] conjI I_Q_delta_poly_inter)
show "I.termination_by_delta_interpretation Q"
unfolding I.termination_by_delta_interpretation_def Q_def
proof (clarify, intro conjI)
show "funas_term lhs_Q ∪ funas_term rhs_Q ⊆ F_Q" using lhs_Q_F rhs_Q_F by auto
show "I.orient_rule (lhs_Q, rhs_Q)" using orient_Q by simp
qed
qed
qed
end
context delta_poly_inter
begin
lemma insertion_eval_pos: assumes "funas_term t ⊆ F"
and "assignment α"
shows "insertion α (eval t) ≥ 0"
by (rule valid_imp_insertion_eval_pos[OF valid assms])
lemma monotone_poly_eval: assumes "funas_term t ⊆ F"
shows "monotone_poly (vars_term t) (eval t)" "vars (eval t) = vars_term t"
proof -
have "∃y. x + δ ≤ y" for x :: 'a by (intro exI[of _ "x + δ"], auto)
from monotone_poly_eval_generic[OF valid transp_gt_delta gt_delta_imp_ge this _ assms] δ0
show "monotone_poly (vars_term t) (eval t)" "vars (eval t) = vars_term t" by auto
qed
lemma monotone_linear_poly_to_coeffs: fixes p :: "'a mpoly"
assumes linear: "total_degree p ≤ 1"
and poly: "valid_poly p"
and mono: "monotone_poly {..<n} p"
and vars: "vars p = {..<n}"
shows "∃ c a. p = Const c + (∑i←[0..<n]. Const (a i) * PVar i)
∧ c ≥ 0 ∧ (∀ i < n. a i ≥ 1)"
proof -
have sum_zero: "(⋀ x. x ∈ set xs ⟹ x = 0) ⟹ sum_list (xs :: int list) = 0" for xs by (induct xs, auto)
from coefficients_of_linear_poly[OF linear] obtain c a vs
where p: "p = Const c + (∑i←vs. Const (a i) * PVar i)"
and vsd: "distinct vs" "set vs = vars p" "sorted_list_of_set (vars p) = vs"
and nz: "⋀ v. v ∈ set vs ⟹ a v ≠ 0"
and c: "c = mcoeff p 0"
and a: "⋀ i. a i = mcoeff p (monomial 1 i)" by blast
have vs: "vs = [0..<n]" unfolding vsd(3)[symmetric] unfolding vars
by (simp add: lessThan_atLeast0)
show ?thesis unfolding p vs
proof (intro exI conjI allI impI, rule refl)
show c: "c ≥ 0" using poly[unfolded valid_poly_def, rule_format, of "λ _. 0", unfolded p]
by (auto simp: coeff_add[symmetric] coeff_Const coeff_sum_list o_def coeff_Const_mult
coeff_Var monomial_0_iff assignment_def)
fix i
assume "i < n"
hence i: "i ∈ set vs" unfolding vs by auto
from nz[OF i] have a0: "a i ≠ 0" by auto
from split_list[OF i] obtain bef aft where vsi: "vs = bef @ [i] @ aft" by auto
with vsd(1) have i: "i ∉ set (bef @ aft)" by auto
define α where "α = (λ x :: var. 0 :: 'a)"
have "assignment α" unfolding assignment_def α_def using c by auto
from mono[unfolded monotone_poly_wrt_def, rule_format, OF this, of i δ] ‹i < n›
have "insertion α p + δ ≤ insertion (α(i := δ)) p" by (auto simp: α_def)
from this[unfolded p vsi insertion_add insertion_sum_list insertion_Const map_map o_def insertion_mult insertion_Var]
have "(∑x← bef @ aft. a x * α x) + δ ≤ (∑x←bef @ aft. a x * (α(i := δ)) x) + a i * δ"
by (auto simp: α_def)
also have "(∑x←bef @ aft. a x * (α(i := δ)) x) = (∑x←bef @ aft. a x * α x)"
by (subst map_cong[OF refl, of _ _ "λ x. a x * α x"], insert i, auto simp: α_def)
finally have "δ ≤ a i * δ" by auto
with δ0 show "a i ≥ 1" by simp
qed
qed
end
text ‹Lemma 6.7›
lemma criterion_for_degree_2: assumes qq_def: "qq = q ∘⇩p [:c, a:] - smult a q"
and dq: "degree q ≥ 2"
and ineq: "⋀ x :: 'a :: linordered_field. x ≥ 0 ⟹ poly qq x ≤ poly p x"
and dp: "degree p ≤ 1"
and a1: "a ≥ 1"
and lq0: "lead_coeff q > 0"
and c: "c > 0"
shows "degree q = 2" "a = 1"
proof -
have deg: "degree (q ∘⇩p [:c, a:]) = degree q"
unfolding degree_pcompose using a1 by simp
have coeff_dq: "coeff qq (degree q) = lead_coeff q * (a ^ degree q - a)"
apply (simp add: qq_def)
apply (subst deg[symmetric])
apply (subst lead_coeff_comp)
subgoal using a1 by simp
subgoal using a1 by (simp add: field_simps)
done
have deg_qq: "degree qq ≤ degree q" using deg
by (simp add: degree_diff_le qq_def)
{
assume "a ≠ 1"
with a1 have a1: "a > 1" by auto
hence "a ^ degree q > a ^ 1" using dq
by (metis add_strict_increasing linorder_not_less one_add_one power_le_imp_le_exp zero_less_one)
hence coeff: "coeff qq (degree q) > 0"
unfolding coeff_dq using dq by (auto intro!: mult_pos_pos lq0)
hence "degree qq ≥ degree q"
by (simp add: le_degree)
with deg_qq have eq: "degree qq = degree q" by auto
from coeff[folded eq] have lcqq: "lead_coeff qq > 0" by auto
from dq[folded eq] have "2 ≤ degree qq" by auto
also have "degree qq ≤ degree p" using ineq lcqq
by (metis Preliminaries_on_Polynomials_2.poly_pinfty_ge degree_mono_generic linorder_le_less_linear order_less_not_sym)
also have "… ≤ 1" by fact
finally have False by simp
}
thus a1: "a = 1" by auto
hence qq: "qq = q ∘⇩p [:c, 1:] - q" unfolding qq_def by auto
from coeff_dq[unfolded a1] have "coeff qq (degree q) = 0" by simp
with deg_qq dq have deq_qq: "degree qq < degree q"
using degree_less_if_less_eqI by fastforce
define m where "m = degree q"
define m1 where "m1 = m - 1"
from dq have mm1: "m = Suc m1" unfolding m1_def m_def by auto
define qi where "qi = coeff q"
define cf where "cf k i = (qi k * of_nat (k choose i) * c ^ (k - i))" for i k
define inner where "inner k = (∑i<k. monom (cf k i) i)" for k
define rem where "rem = (∑i< m1. monom (cf m i) i) + sum inner {..<m}"
{
fix x
define e where "e i k = of_nat (k choose i) * x ^ i * c ^ (k - i)" for k i
have "poly qq x = poly (q ∘⇩p [:c, 1:]) x - poly q x" unfolding qq by simp
also have "… = (∑k≤m. qi k * (x + c) ^ k) - (∑k≤m. qi k * x ^ k)" unfolding qi_def
by (subst (1 2) poly_as_sum_of_monoms[of q, symmetric, folded m_def])
(simp add: poly_sum poly_pcompose poly_monom ac_simps)
also have "… = (∑k≤m. qi k * (∑i≤k. e i k)) - (∑k≤m. qi k * x ^ k)"
by (subst binomial_ring, auto simp: e_def)
also have "… = (∑k≤m. qi k * (e k k + (∑i<k. e i k))) - (∑k≤m. qi k * x ^ k)"
by (intro arg_cong[of _ _ "λ x. x - _"] sum.cong refl arg_cong2[of _ _ _ _ "(*)"])
(metis add.commute lessThan_Suc_atMost sum.lessThan_Suc)
also have "… = (∑k≤m. qi k * e k k) + (∑k≤m. qi k * (∑i<k. e i k)) - (∑k≤m. qi k * x ^ k)"
by (simp add: field_simps sum.distrib)
also have "… = (∑k≤m. qi k * (∑i<k. e i k))"
unfolding e_def by simp
also have "… = poly (∑k≤m. inner k) x" unfolding e_def inner_def cf_def
by (simp add: poly_sum poly_monom ac_simps sum_distrib_left)
finally have "poly qq x = poly (sum inner {..m}) x" .
}
hence "qq = sum inner {..m}" by (intro poly_ext, auto)
also have "… = inner m + sum inner {..<m}"
by (metis add.commute lessThan_Suc_atMost sum.lessThan_Suc)
also have "inner m = monom (cf m m1) m1 + (∑i< m1. monom (cf m i) i)"
unfolding inner_def mm1 by simp
finally have qq: "qq = monom (cf m m1) m1 + rem" by (simp add: rem_def)
have cf_mm1: "cf m m1 > 0" unfolding cf_def
proof (intro mult_pos_pos)
show "0 < qi m" unfolding qi_def m_def by fact
show "0 < (of_nat (m choose m1) :: 'a)" unfolding mm1
by (simp add: add_strict_increasing)
show "0 < c ^ (m - m1)" using c by simp
qed
{
fix k
assume k: "k ≥ m1"
have "coeff rem k = (∑i<m. coeff (inner i) k)" using k
by (simp add: rem_def Polynomial.coeff_sum)
also have "… = 0"
proof (intro sum.neutral ballI)
fix i
show "i ∈ {..<m} ⟹ coeff (inner i) k = 0"
unfolding inner_def Polynomial.coeff_sum using k mm1
by auto
qed
finally have "coeff rem k = 0" .
} note zero = this
from cf_mm1 zero[of m1]
have qq_m1: "coeff qq m1 > 0" unfolding qq by auto
{
fix k
assume "k > m1"
with zero[of k] have "coeff qq k = 0" unfolding qq by auto
}
with qq_m1 have deg_qq: "degree qq = m1"
by (metis coeff_0 le_degree leading_coeff_0_iff order_less_le)
with qq_m1 have lc_qq: "lead_coeff qq > 0" by auto
from ineq lc_qq have "degree qq ≤ degree p"
by (metis Preliminaries_on_Polynomials_2.poly_pinfty_ge degree_mono_generic linorder_le_less_linear order_less_not_sym)
also have "… ≤ 1" by fact
finally have "m1 ≤ 1" unfolding deg_qq by simp
with mm1 have "m ≤ 2" by auto
hence "degree q ≤ 2" unfolding m_def by auto
with dq show "degree q = 2" by auto
qed
locale term_delta_poly_input = poly_input p q for p q +
fixes type_of_field :: "'a :: floor_ceiling itself"
assumes terminating_delta_poly: "termination_by_delta_poly_interpretation TYPE('a) F_Q Q"
begin
definition I where "I = (SOME I. ∃ δ. delta_poly_inter F_Q I (δ :: 'a) ∧
delta_poly_inter.termination_by_delta_interpretation F_Q I δ Q)"
definition δ where "δ = (SOME δ. delta_poly_inter F_Q I (δ :: 'a) ∧
delta_poly_inter.termination_by_delta_interpretation F_Q I δ Q)"
lemma I: "delta_poly_inter F_Q I δ" "delta_poly_inter.termination_by_delta_interpretation F_Q I