# Theory Sturm_Method

```section ‹The ``sturm'' proof method›

(* Author: Manuel Eberl <manuel@pruvisto.org> *)
theory Sturm_Method
imports Sturm_Theorem
begin

subsection ‹Preliminary lemmas›

text ‹
In this subsection, we prove lemmas that reduce root counting and
related statements to simple, computable expressions using the
@{term "count_roots"} function family.
›

lemma poly_card_roots_less_leq:
"card {x. a < x ∧ x ≤ b ∧ poly p x = 0} = count_roots_between p a b"

lemma poly_card_roots_leq_leq:
"card {x. a ≤ x ∧ x ≤ b ∧ poly p x = 0} =
( count_roots_between p a b +
(if (a ≤ b ∧ poly p a = 0 ∧ p ≠ 0) ∨ (a = b ∧ p = 0) then 1 else 0))"
proof (cases "(a ≤ b ∧ poly p a = 0 ∧ p ≠ 0) ∨ (a = b ∧ p = 0)")
case False
note False' = this
thus ?thesis
proof (cases "p = 0")
case False
with False' have "poly p a ≠ 0 ∨ a > b" by auto
hence "{x. a ≤ x ∧ x ≤ b ∧ poly p x = 0} =
{x. a < x ∧ x ≤ b ∧ poly p x = 0}"
by (auto simp: less_eq_real_def)
thus ?thesis using poly_card_roots_less_leq False'
by (auto split: if_split_asm)
next
case True
have "{x. a ≤ x ∧ x ≤ b} = {a..b}"
"{x. a < x ∧ x ≤ b} = {a<..b}" by auto
with True False have "card {x. a < x ∧ x ≤ b} = 0" "card {x. a ≤ x ∧ x ≤ b} = 0"
by (auto simp add: card_eq_0_iff infinite_Ioc infinite_Icc)
with True False show ?thesis
using count_roots_between_correct by (simp add: )
qed
next
case True
note True' = this
have fin: "finite {x. a ≤ x ∧ x ≤ b ∧ poly p x = 0}"
proof (cases "p = 0")
case True
with True' have "a = b" by simp
hence "{x. a ≤ x ∧ x ≤ b ∧ poly p x = 0} = {b}" using True by auto
thus ?thesis by simp
next
case False
from poly_roots_finite[OF this] show ?thesis by fast
qed
with True have "{x. a ≤ x ∧ x ≤ b ∧ poly p x = 0} =
insert a {x. a < x ∧ x ≤ b ∧ poly p x = 0}" by auto
hence "card {x. a ≤ x ∧ x ≤ b ∧ poly p x = 0} =
Suc (card {x. a < x ∧ x ≤ b ∧ poly p x = 0})" using fin by force
thus ?thesis using True count_roots_between_correct by simp
qed

lemma poly_card_roots_less_less:
"card {x. a < x ∧ x < b ∧ poly p x = 0} =
( count_roots_between p a b -
(if poly p b = 0 ∧ a < b ∧ p ≠ 0 then 1 else 0))"
proof (cases "poly p b = 0 ∧ a < b ∧ p ≠ 0")
case False
note False' = this
show ?thesis
proof (cases "p = 0")
case True
have [simp]: "{x. a < x ∧ x < b} = {a<..<b}"
"{x. a < x ∧ x ≤ b} = {a<..b}" by auto
with True False have "card {x. a < x ∧ x ≤ b} = 0" "card {x. a < x ∧ x < b} = 0"
by (auto simp add: card_eq_0_iff infinite_Ioo infinite_Ioc)
with True False' show ?thesis
by (auto simp: count_roots_between_correct)
next
case False
with False' have "{x. a < x ∧ x < b ∧ poly p x = 0} =
{x. a < x ∧ x ≤ b ∧ poly p x = 0}"
by (auto simp: less_eq_real_def)
thus ?thesis using poly_card_roots_less_leq False by auto
qed
next
case True
with poly_roots_finite
have fin: "finite {x. a < x ∧ x < b ∧ poly p x = 0}" by fast
from True have "{x. a < x ∧ x ≤ b ∧ poly p x = 0} =
insert b {x. a < x ∧ x < b ∧ poly p x = 0}" by auto
hence "Suc (card {x. a < x ∧ x < b ∧ poly p x = 0}) =
card {x. a < x ∧ x ≤ b ∧ poly p x = 0}" using fin by force
also note count_roots_between_correct[symmetric]
finally show ?thesis using True by simp
qed

lemma poly_card_roots_leq_less:
"card {x::real. a ≤ x ∧ x < b ∧ poly p x = 0} =
( count_roots_between p a b +
(if p ≠ 0 ∧ a < b ∧ poly p a = 0 then 1 else 0) -
(if p ≠ 0 ∧ a < b ∧ poly p b = 0 then 1 else 0))"
proof (cases "p = 0 ∨ a ≥ b")
case True
note True' = this
show ?thesis
proof (cases "a ≥ b")
case False
hence "{x. a < x ∧ x ≤ b} = {a<..b}"
"{x. a ≤ x ∧ x < b} = {a..<b}" by auto
with True False have "card {x. a < x ∧ x ≤ b} = 0" "card {x. a ≤ x ∧ x < b} = 0"
by (auto simp add: card_eq_0_iff infinite_Ico infinite_Ioc)
with False True' show ?thesis
next
case True
with True' have "{x. a ≤ x ∧ x < b ∧ poly p x = 0} =
{x. a < x ∧ x ≤ b ∧ poly p x = 0}"
by (auto simp: less_eq_real_def)
thus ?thesis using poly_card_roots_less_leq True by simp
qed
next
case False
let ?A = "{x. a ≤ x ∧ x < b ∧ poly p x = 0}"
let ?B = "{x. a < x ∧ x ≤ b ∧ poly p x = 0}"
let ?C = "{x. x = b ∧ poly p x = 0}"
let ?D = "{x. x = a ∧ poly p a = 0}"
have CD_if: "?C = (if poly p b = 0 then {b} else {})"
"?D = (if poly p a = 0 then {a} else {})" by auto
from False poly_roots_finite
have [simp]: "finite ?A" "finite ?B" "finite ?C" "finite ?D"
by (fast, fast, simp_all)

from False have "?A = (?B ∪ ?D) - ?C" by (auto simp: less_eq_real_def)
with False have "card ?A = card ?B + (if poly p a = 0 then 1 else 0) -
(if poly p b = 0 then 1 else 0)" by (auto simp: CD_if)
also note count_roots_between_correct[symmetric]
finally show ?thesis using False by simp
qed

lemma poly_card_roots:
"card {x::real. poly p x = 0} = count_roots p"
using count_roots_correct by simp

lemma poly_no_roots:
"(∀x. poly p x ≠ 0) ⟷ ( p ≠ 0 ∧ count_roots p = 0)"
by (auto simp: count_roots_correct dest: poly_roots_finite)

lemma poly_pos:
"(∀x. poly p x > 0) ⟷ (
p ≠ 0 ∧ poly_inf p = 1 ∧ count_roots p = 0)"
by (simp only: Let_def poly_pos poly_no_roots, blast)

lemma poly_card_roots_greater:
"card {x::real. x > a ∧ poly p x = 0} = count_roots_above p a"
using count_roots_above_correct by simp

lemma poly_card_roots_leq:
"card {x::real. x ≤ a ∧ poly p x = 0} = count_roots_below p a"
using count_roots_below_correct by simp

lemma poly_card_roots_geq:
"card {x::real. x ≥ a ∧ poly p x = 0} = (
count_roots_above p a + (if poly p a = 0 ∧ p ≠ 0 then 1 else 0))"
proof (cases "poly p a = 0 ∧ p ≠ 0")
case False
hence "card {x. x ≥ a ∧ poly p x = 0} = card {x. x > a ∧ poly p x = 0}"
proof (cases rule: disjE)
assume "p = 0"
have "¬finite {a<..<a+1}"
moreover have "{a<..<a+1} ⊆ {x. x ≥ a ∧ poly p x = 0}"
"{a<..<a+1} ⊆ {x. x > a ∧ poly p x = 0}"
using ‹p = 0› by auto
ultimately have "¬finite {x. x ≥ a ∧ poly p x = 0}"
"¬finite {x. x > a ∧ poly p x = 0}"
by (auto dest!: finite_subset[of "{a<..<a+1}"] simp: infinite_Ioo)
thus ?thesis by simp
next
assume "poly p a ≠ 0"
hence "{x. x ≥ a ∧ poly p x = 0} = {x. x > a ∧ poly p x = 0}"
by (auto simp: less_eq_real_def)
thus ?thesis by simp
qed auto
thus ?thesis using False
by (auto intro: poly_card_roots_greater)
next
case True
hence "finite {x. x > a ∧ poly p x = 0}" using poly_roots_finite by force
moreover have "{x. x ≥ a ∧ poly p x = 0} =
insert a {x. x > a ∧ poly p x = 0}" using True by auto
ultimately have "card {x. x ≥ a ∧ poly p x = 0} =
Suc (card {x. x > a ∧ poly p x = 0})"
using card_insert_disjoint by auto
thus ?thesis using True by (auto intro: poly_card_roots_greater)
qed

lemma poly_card_roots_less:
"card {x::real. x < a ∧ poly p x = 0} =
(count_roots_below p a - (if poly p a = 0 ∧ p ≠ 0 then 1 else 0))"
proof (cases "poly p a = 0 ∧ p ≠ 0")
case False
hence "card {x. x < a ∧ poly p x = 0} = card {x. x ≤ a ∧ poly p x = 0}"
proof (cases rule: disjE)
assume "p = 0"
have "¬finite {a - 1<..<a}"
moreover have "{a - 1<..<a} ⊆ {x. x ≤ a ∧ poly p x = 0}"
"{a - 1<..<a} ⊆ {x. x < a ∧ poly p x = 0}"
using ‹p = 0› by auto
ultimately have "¬finite {x. x ≤ a ∧ poly p x = 0}"
"¬finite {x. x < a ∧ poly p x = 0}"
by (auto dest: finite_subset[of "{a - 1<..<a}"] simp: infinite_Ioo)
thus ?thesis by simp
next
assume "poly p a ≠ 0"
hence "{x. x < a ∧ poly p x = 0} = {x. x ≤ a ∧ poly p x = 0}"
by (auto simp: less_eq_real_def)
thus ?thesis by simp
qed auto
thus ?thesis using False
by (auto intro: poly_card_roots_leq)
next
case True
hence "finite {x. x < a ∧ poly p x = 0}" using poly_roots_finite by force
moreover have "{x. x ≤ a ∧ poly p x = 0} =
insert a {x. x < a ∧ poly p x = 0}" using True by auto
ultimately have "Suc (card {x. x < a ∧ poly p x = 0}) =
(card {x. x ≤ a ∧ poly p x = 0})"
using card_insert_disjoint by auto
also note count_roots_below_correct[symmetric]
finally show ?thesis using True by simp
qed

lemma poly_no_roots_less_leq:
"(∀x. a < x ∧ x ≤ b ⟶ poly p x ≠ 0) ⟷
((a ≥ b ∨ (p ≠ 0 ∧ count_roots_between p a b = 0)))"
by (auto simp: count_roots_between_correct card_eq_0_iff not_le
dest: poly_roots_finite)

lemma poly_pos_between_less_leq:
"(∀x. a < x ∧ x ≤ b ⟶ poly p x > 0) ⟷
((a ≥ b ∨ (p ≠ 0 ∧ poly p b > 0 ∧ count_roots_between p a b = 0)))"
by (simp only: poly_pos_between_less_leq Let_def
poly_no_roots_less_leq, blast)

lemma poly_no_roots_leq_leq:
"(∀x. a ≤ x ∧ x ≤ b ⟶ poly p x ≠ 0) ⟷
((a > b ∨ (p ≠ 0 ∧ poly p a ≠ 0 ∧ count_roots_between p a b = 0)))"
apply (intro iffI)
apply (force simp add: count_roots_between_correct card_eq_0_iff)
apply (elim conjE disjE, simp, intro allI)
apply (rename_tac x, case_tac "x = a")
apply (auto simp add: count_roots_between_correct card_eq_0_iff
dest: poly_roots_finite)
done

lemma poly_pos_between_leq_leq:
"(∀x. a ≤ x ∧ x ≤ b ⟶ poly p x > 0) ⟷
((a > b ∨ (p ≠ 0 ∧ poly p a > 0 ∧
count_roots_between p a b = 0)))"
by (simp only: poly_pos_between_leq_leq Let_def poly_no_roots_leq_leq, force)

lemma poly_no_roots_less_less:
"(∀x. a < x ∧ x < b ⟶ poly p x ≠ 0) ⟷
((a ≥ b ∨ p ≠ 0 ∧ count_roots_between p a b =
(if poly p b = 0 then 1 else 0)))"
proof (standard, goal_cases)
case A: 1
show ?case
proof (cases "a ≥ b")
case True
with A show ?thesis by simp
next
case False
with A have [simp]: "p ≠ 0" using dense[of a b] by auto
have B: "{x. a < x ∧ x ≤ b ∧ poly p x = 0} =
{x. a < x ∧ x < b ∧ poly p x = 0} ∪
(if poly p b = 0 then {b} else {})" using A False by auto
have "count_roots_between p a b =
card {x. a < x ∧ x < b ∧ poly p x = 0} +
(if poly p b = 0 then 1 else 0)"
by (subst count_roots_between_correct, subst B, subst card_Un_disjoint,
rule finite_subset[OF _ poly_roots_finite], blast, simp_all)
also from A have "{x. a < x ∧ x < b ∧ poly p x = 0} = {}" by simp
finally show ?thesis by auto
qed
next
case prems: 2
hence "card {x. a < x ∧ x < b ∧ poly p x = 0} = 0"
by (subst poly_card_roots_less_less, auto simp: count_roots_between_def)
thus ?case using prems
by (cases "p = 0", simp, subst (asm) card_eq_0_iff,
auto dest: poly_roots_finite)
qed

lemma poly_pos_between_less_less:
"(∀x. a < x ∧ x < b ⟶ poly p x > 0) ⟷
((a ≥ b ∨ (p ≠ 0 ∧ poly p ((a+b)/2) > 0 ∧
count_roots_between p a b = (if poly p b = 0 then 1 else 0))))"
by (simp only: poly_pos_between_less_less Let_def
poly_no_roots_less_less, blast)

lemma poly_no_roots_leq_less:
"(∀x. a ≤ x ∧ x < b ⟶ poly p x ≠ 0) ⟷
((a ≥ b ∨ p ≠ 0 ∧ poly p a ≠ 0 ∧ count_roots_between p a b =
(if a < b ∧ poly p b = 0 then 1 else 0)))"
proof (standard, goal_cases)
case prems: 1
hence "∀x. a < x ∧ x < b ⟶ poly p x ≠ 0" by simp
thus ?case using prems by (subst (asm) poly_no_roots_less_less, auto)
next
case prems: 2
hence "(b ≤ a ∨ p ≠ 0 ∧ count_roots_between p a b =
(if poly p b = 0 then 1 else 0))" by auto
thus ?case using prems unfolding Let_def
by (subst (asm) poly_no_roots_less_less[symmetric, unfolded Let_def],
auto split: if_split_asm simp: less_eq_real_def)
qed

lemma poly_pos_between_leq_less:
"(∀x. a ≤ x ∧ x < b ⟶ poly p x > 0) ⟷
((a ≥ b ∨ (p ≠ 0 ∧ poly p a > 0 ∧ count_roots_between p a b =
(if a < b ∧ poly p b = 0 then 1 else 0))))"
by (simp only: poly_pos_between_leq_less Let_def
poly_no_roots_leq_less, force)

lemma poly_no_roots_greater:
"(∀x. x > a ⟶ poly p x ≠ 0) ⟷
((p ≠ 0 ∧ count_roots_above p a = 0))"
proof-
have "∀x. ¬ a < x ⟹ False" by (metis gt_ex)
thus ?thesis by (auto simp: count_roots_above_correct card_eq_0_iff
intro: poly_roots_finite )
qed

lemma poly_pos_greater:
"(∀x. x > a ⟶ poly p x > 0) ⟷ (
p ≠ 0 ∧ poly_inf p = 1 ∧ count_roots_above p a = 0)"
unfolding Let_def
by (subst poly_pos_greater, subst poly_no_roots_greater, force)

lemma poly_no_roots_leq:
"(∀x. x ≤ a ⟶ poly p x ≠ 0) ⟷
( (p ≠ 0 ∧ count_roots_below p a = 0))"
by (auto simp: Let_def count_roots_below_correct card_eq_0_iff
intro: poly_roots_finite)

lemma poly_pos_leq:
"(∀x. x ≤ a ⟶ poly p x > 0) ⟷
( p ≠ 0 ∧ poly_neg_inf p = 1 ∧ count_roots_below p a = 0)"
by (simp only: poly_pos_leq Let_def poly_no_roots_leq, blast)

lemma poly_no_roots_geq:
"(∀x. x ≥ a ⟶ poly p x ≠ 0) ⟷
( (p ≠ 0 ∧ poly p a ≠ 0 ∧ count_roots_above p a = 0))"
proof (standard, goal_cases)
case prems: 1
hence "∀x>a. poly p x ≠ 0" by simp
thus ?case using prems by (subst (asm) poly_no_roots_greater, auto)
next
case prems: 2
hence "(p ≠ 0 ∧ count_roots_above p a = 0)" by simp
thus ?case using prems
by (subst (asm) poly_no_roots_greater[symmetric, unfolded Let_def],
auto simp: less_eq_real_def)
qed

lemma poly_pos_geq:
"(∀x. x ≥ a ⟶ poly p x > 0) ⟷
(p ≠ 0 ∧ poly_inf p = 1 ∧ poly p a ≠ 0 ∧ count_roots_above p a = 0)"
by (simp only: poly_pos_geq Let_def poly_no_roots_geq, blast)

lemma poly_no_roots_less:
"(∀x. x < a ⟶ poly p x ≠ 0) ⟷
((p ≠ 0 ∧ count_roots_below p a = (if poly p a = 0 then 1 else 0)))"
proof (standard, goal_cases)
case prems: 1
hence "{x. x ≤ a ∧ poly p x = 0} = (if poly p a = 0 then {a} else {})"
by (auto simp: less_eq_real_def)
moreover have "∀x. ¬ x < a ⟹ False" by (metis lt_ex)
ultimately show ?case using prems by (auto simp: count_roots_below_correct)
next
case prems: 2
have A: "{x. x ≤ a ∧ poly p x = 0} = {x. x < a ∧ poly p x = 0} ∪
(if poly p a = 0 then {a} else {})" by (auto simp: less_eq_real_def)
have "count_roots_below p a = card {x. x < a ∧ poly p x = 0} +
(if poly p a = 0 then 1 else 0)" using prems
by (subst count_roots_below_correct, subst A, subst card_Un_disjoint,
auto intro: poly_roots_finite)
with prems have "card {x. x < a ∧ poly p x = 0} = 0" by simp
thus ?case using prems
by (subst (asm) card_eq_0_iff, auto intro: poly_roots_finite)
qed

lemma poly_pos_less:
"(∀x. x < a ⟶ poly p x > 0) ⟷
(p ≠ 0 ∧ poly_neg_inf p = 1 ∧ count_roots_below p a =
(if poly p a = 0 then 1 else 0))"
by (simp only: poly_pos_less Let_def poly_no_roots_less, blast)

lemmas sturm_card_substs = poly_card_roots poly_card_roots_less_leq
poly_card_roots_leq_less poly_card_roots_less_less poly_card_roots_leq_leq
poly_card_roots_less poly_card_roots_leq poly_card_roots_greater
poly_card_roots_geq

lemmas sturm_prop_substs = poly_no_roots poly_no_roots_less_leq
poly_no_roots_leq_leq poly_no_roots_less_less poly_no_roots_leq_less
poly_no_roots_leq poly_no_roots_less poly_no_roots_geq
poly_no_roots_greater
poly_pos poly_pos_greater poly_pos_geq poly_pos_less poly_pos_leq
poly_pos_between_leq_less poly_pos_between_less_leq
poly_pos_between_leq_leq poly_pos_between_less_less

subsection ‹Reification›

text ‹
This subsection defines a number of equations to automatically convert
statements about roots of polynomials into a canonical form so that they
can be proven using the above substitutions.
›

definition "PR_TAG x ≡ x"

lemma sturm_id_PR_prio0:
"{x::real. P x} = {x::real. (PR_TAG P) x}"
"(∀x::real. f x < g x) = (∀x::real. PR_TAG (λx. f x < g x) x)"
"(∀x::real. P x) = (∀x::real. ¬(PR_TAG (λx. ¬P x)) x)"

lemma sturm_id_PR_prio1:
"{x::real. x < a ∧ P x} = {x::real. x < a ∧ (PR_TAG P) x}"
"{x::real. x ≤ a ∧ P x} = {x::real. x ≤ a ∧ (PR_TAG P) x}"
"{x::real. x ≥ b ∧ P x} = {x::real. x ≥ b ∧ (PR_TAG P) x}"
"{x::real. x > b ∧ P x} = {x::real. x > b ∧ (PR_TAG P) x}"
"(∀x::real < a. f x < g x) = (∀x::real < a. PR_TAG (λx. f x < g x) x)"
"(∀x::real ≤ a. f x < g x) = (∀x::real ≤ a. PR_TAG (λx. f x < g x) x)"
"(∀x::real > a. f x < g x) = (∀x::real > a. PR_TAG (λx. f x < g x) x)"
"(∀x::real ≥ a. f x < g x) = (∀x::real ≥ a. PR_TAG (λx. f x < g x) x)"
"(∀x::real < a. P x) = (∀x::real < a. ¬(PR_TAG (λx. ¬P x)) x)"
"(∀x::real > a. P x) = (∀x::real > a. ¬(PR_TAG (λx. ¬P x)) x)"
"(∀x::real ≤ a. P x) = (∀x::real ≤ a. ¬(PR_TAG (λx. ¬P x)) x)"
"(∀x::real ≥ a. P x) = (∀x::real ≥ a. ¬(PR_TAG (λx. ¬P x)) x)"

lemma sturm_id_PR_prio2:
"{x::real. x > a ∧ x ≤ b ∧ P x} =
{x::real. x > a ∧ x ≤ b ∧ PR_TAG P x}"
"{x::real. x ≥ a ∧ x ≤ b ∧ P x} =
{x::real. x ≥ a ∧ x ≤ b ∧ PR_TAG P x}"
"{x::real. x ≥ a ∧ x < b ∧ P x} =
{x::real. x ≥ a ∧ x < b ∧ PR_TAG P x}"
"{x::real. x > a ∧ x < b ∧ P x} =
{x::real. x > a ∧ x < b ∧ PR_TAG P x}"
"(∀x::real. a < x ∧ x ≤ b ⟶ f x < g x) =
(∀x::real. a < x ∧ x ≤ b ⟶ PR_TAG (λx. f x < g x) x)"
"(∀x::real. a ≤ x ∧ x ≤ b ⟶ f x < g x) =
(∀x::real. a ≤ x ∧ x ≤ b ⟶ PR_TAG (λx. f x < g x) x)"
"(∀x::real. a < x ∧ x < b ⟶ f x < g x) =
(∀x::real. a < x ∧ x < b ⟶ PR_TAG (λx. f x < g x) x)"
"(∀x::real. a ≤ x ∧ x < b ⟶ f x < g x) =
(∀x::real. a ≤ x ∧ x < b ⟶ PR_TAG (λx. f x < g x) x)"
"(∀x::real. a < x ∧ x ≤ b ⟶ P x) =
(∀x::real. a < x ∧ x ≤ b ⟶ ¬(PR_TAG (λx. ¬P x)) x)"
"(∀x::real. a ≤ x ∧ x ≤ b ⟶ P x) =
(∀x::real. a ≤ x ∧ x ≤ b ⟶ ¬(PR_TAG (λx. ¬P x)) x)"
"(∀x::real. a ≤ x ∧ x < b ⟶ P x) =
(∀x::real. a ≤ x ∧ x < b ⟶ ¬(PR_TAG (λx. ¬P x)) x)"
"(∀x::real. a < x ∧ x < b ⟶ P x) =
(∀x::real. a < x ∧ x < b ⟶ ¬(PR_TAG (λx. ¬P x)) x)"

lemma PR_TAG_intro_prio0:
fixes P :: "real ⇒ bool" and f :: "real ⇒ real"
shows
"PR_TAG P = P' ⟹ PR_TAG (λx. ¬(¬P x)) = P'"
"⟦PR_TAG P = (λx. poly p x = 0); PR_TAG Q = (λx. poly q x = 0)⟧
⟹ PR_TAG (λx. P x ∧ Q x) = (λx. poly (gcd p q) x = 0)" and
" ⟦PR_TAG P = (λx. poly p x = 0); PR_TAG Q = (λx. poly q x = 0)⟧
⟹ PR_TAG (λx. P x ∨ Q x) = (λx. poly (p*q) x = 0)" and

"⟦PR_TAG f = (λx. poly p x); PR_TAG g = (λx. poly q x)⟧
⟹ PR_TAG (λx. f x = g x) = (λx. poly (p-q) x = 0)"
"⟦PR_TAG f = (λx. poly p x); PR_TAG g = (λx. poly q x)⟧
⟹ PR_TAG (λx. f x ≠ g x) = (λx. poly (p-q) x ≠ 0)"
"⟦PR_TAG f = (λx. poly p x); PR_TAG g = (λx. poly q x)⟧
⟹ PR_TAG (λx. f x < g x) = (λx. poly (q-p) x > 0)"
"⟦PR_TAG f = (λx. poly p x); PR_TAG g = (λx. poly q x)⟧
⟹ PR_TAG (λx. f x ≤ g x) = (λx. poly (q-p) x ≥ 0)"

"PR_TAG f = (λx. poly p x) ⟹ PR_TAG (λx. -f x) = (λx. poly (-p) x)"
"⟦PR_TAG f = (λx. poly p x); PR_TAG g = (λx. poly q x)⟧
⟹ PR_TAG (λx. f x + g x) = (λx. poly (p+q) x)"
"⟦PR_TAG f = (λx. poly p x); PR_TAG g = (λx. poly q x)⟧
⟹ PR_TAG (λx. f x - g x) = (λx. poly (p-q) x)"
"⟦PR_TAG f = (λx. poly p x); PR_TAG g = (λx. poly q x)⟧
⟹ PR_TAG (λx. f x * g x) = (λx. poly (p*q) x)"
"PR_TAG f = (λx. poly p x) ⟹ PR_TAG (λx. (f x)^n) = (λx. poly (p^n) x)"
"PR_TAG (λx. poly p x :: real) = (λx. poly p x)"
"PR_TAG (λx. x::real) = (λx. poly [:0,1:] x)"
"PR_TAG (λx. a::real) = (λx. poly [:a:] x)"
by (simp_all add: PR_TAG_def poly_eq_0_iff_dvd field_simps)

lemma PR_TAG_intro_prio1:
fixes f :: "real ⇒ real"
shows
"PR_TAG f = (λx. poly p x) ⟹ PR_TAG (λx. f x = 0) = (λx. poly p x = 0)"
"PR_TAG f = (λx. poly p x) ⟹ PR_TAG (λx. f x ≠ 0) = (λx. poly p x ≠ 0)"
"PR_TAG f = (λx. poly p x) ⟹ PR_TAG (λx. 0 = f x) = (λx. poly p x = 0)"
"PR_TAG f = (λx. poly p x) ⟹ PR_TAG (λx. 0 ≠ f x) = (λx. poly p x ≠ 0)"
"PR_TAG f = (λx. poly p x) ⟹ PR_TAG (λx. f x ≥ 0) = (λx. poly p x ≥ 0)"
"PR_TAG f = (λx. poly p x) ⟹ PR_TAG (λx. f x > 0) = (λx. poly p x > 0)"
"PR_TAG f = (λx. poly p x) ⟹ PR_TAG (λx. f x ≤ 0) = (λx. poly (-p) x ≥ 0)"
"PR_TAG f = (λx. poly p x) ⟹ PR_TAG (λx. f x < 0) = (λx. poly (-p) x > 0)"
"PR_TAG f = (λx. poly p x) ⟹
PR_TAG (λx. 0 ≤ f x) = (λx. poly (-p) x ≤ 0)"
"PR_TAG f = (λx. poly p x) ⟹
PR_TAG (λx. 0 < f x) = (λx. poly (-p) x < 0)"
"PR_TAG f = (λx. poly p x)
⟹ PR_TAG (λx. a * f x) = (λx. poly (smult a p) x)"
"PR_TAG f = (λx. poly p x)
⟹ PR_TAG (λx. f x * a) = (λx. poly (smult a p) x)"
"PR_TAG f = (λx. poly p x)
⟹ PR_TAG (λx. f x / a) = (λx. poly (smult (inverse a) p) x)"
"PR_TAG (λx. x^n :: real) = (λx. poly (monom 1 n) x)"
by (simp_all add: PR_TAG_def field_simps poly_monom)

lemma PR_TAG_intro_prio2:
"PR_TAG (λx. 1 / b) = (λx. inverse b)"
"PR_TAG (λx. a / b) = (λx. a / b)"
"PR_TAG (λx. a / b * x^n :: real) = (λx. poly (monom (a/b) n) x)"
"PR_TAG (λx. x^n * a / b :: real) = (λx. poly (monom (a/b) n) x)"
"PR_TAG (λx. a * x^n :: real) = (λx. poly (monom a n) x)"
"PR_TAG (λx. x^n * a :: real) = (λx. poly (monom a n) x)"
"PR_TAG (λx. x^n / a :: real) = (λx. poly (monom (inverse a) n) x)"
(* TODO: can this be done more efficiently? I should think so. *)
"PR_TAG (λx. f x^(Suc (Suc 0)) :: real) = (λx. poly p x)
⟹ PR_TAG (λx. f x * f x :: real) = (λx. poly p x)"
"PR_TAG (λx. (f x)^Suc n :: real) = (λx. poly p x)
⟹ PR_TAG (λx. (f x)^n * f x :: real) = (λx. poly p x)"
"PR_TAG (λx. (f x)^Suc n :: real) = (λx. poly p x)
⟹ PR_TAG (λx. f x * (f x)^n :: real) = (λx. poly p x)"
"PR_TAG (λx. (f x)^(m+n) :: real) = (λx. poly p x)
⟹ PR_TAG (λx. (f x)^m * (f x)^n :: real) = (λx. poly p x)"

lemma sturm_meta_spec: "(⋀x::real. P x) ⟹ P x" by simp
lemma sturm_imp_conv:
"(a < x ⟶ x < b ⟶ c) ⟷ (a < x ∧ x < b ⟶ c)"
"(a ≤ x ⟶ x < b ⟶ c) ⟷ (a ≤ x ∧ x < b ⟶ c)"
"(a < x ⟶ x ≤ b ⟶ c) ⟷ (a < x ∧ x ≤ b ⟶ c)"
"(a ≤ x ⟶ x ≤ b ⟶ c) ⟷ (a ≤ x ∧ x ≤ b ⟶ c)"
"(x < b ⟶ a < x ⟶ c) ⟷ (a < x ∧ x < b ⟶ c)"
"(x < b ⟶ a ≤ x ⟶ c) ⟷ (a ≤ x ∧ x < b ⟶ c)"
"(x ≤ b ⟶ a < x ⟶ c) ⟷ (a < x ∧ x ≤ b ⟶ c)"
"(x ≤ b ⟶ a ≤ x ⟶ c) ⟷ (a ≤ x ∧ x ≤ b ⟶ c)"
by auto

subsection ‹Setup for the ``sturm'' method›

ML_file ‹sturm.ML›

method_setup sturm = ‹
Scan.succeed (fn ctxt => SIMPLE_METHOD' (Sturm.sturm_tac ctxt true))
›

end
```