Theory Sturm_Sequences.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"
  by (simp add: count_roots_between_correct)

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
    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 
            by (simp add: count_roots_between_correct)
    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}"
        by (metis infinite_Ioo less_add_one) 
      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}" 
        by (metis infinite_Ioo diff_add_cancel less_add_one) 
      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)"
  by (simp_all add: PR_TAG_def)

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)"
  by (simp_all add: PR_TAG_def)

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)"
  by (simp_all add: PR_TAG_def)



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)"
by (simp_all add: PR_TAG_def field_simps poly_monom power_add)

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