Theory Virtual_Substitution.NegInfinityUni
theory NegInfinityUni
imports UniAtoms NegInfinity QE
begin
fun allZero' :: "real * real * real ⇒ atomUni fmUni" where
"allZero' (a,b,c) = AndUni(AndUni(AtomUni(EqUni(0,0,a))) (AtomUni(EqUni(0,0,b)))) (AtomUni(EqUni(0,0,c)))"
lemma convert_allZero :
assumes "convert_poly var p (xs'@x#xs) = Some p'"
assumes "length xs' = var"
shows "eval (allZero p var) (xs'@x#xs) = evalUni (allZero' p') x"
proof(cases p')
case (fields a b c)
then show ?thesis proof(cases "MPoly_Type.degree p var = 0")
case True
then show ?thesis
using assms fields
by(simp add:eval_list_conj isovar_greater_degree)
next
case False
then have nonzero : "MPoly_Type.degree p var ≠ 0" by auto
then show ?thesis
proof(cases "MPoly_Type.degree p var = 1")
case True
then show ?thesis
using assms fields
apply(simp add:eval_list_conj isovar_greater_degree)
by (metis)
next
case False
then have degree2 : "MPoly_Type.degree p var = 2" using degree_convert_eq[OF assms(1)] nonzero by auto
then show ?thesis
using assms
apply(simp add:eval_list_conj isovar_greater_degree)
using insertion_isovarspars_free list_update_code(2)
apply auto
by (metis One_nat_def Suc_1 less_2_cases less_Suc_eq numeral_3_eq_3)
qed
qed
qed
fun alternateNegInfinity' :: "real * real * real ⇒ atomUni fmUni" where
"alternateNegInfinity' (a,b,c) =
OrUni(AtomUni(LessUni(0,0,a)))(
AndUni(AtomUni(EqUni(0,0,a))) (
OrUni(AtomUni(LessUni(0,0,-b)))(
AndUni(AtomUni(EqUni(0,0,b)))(
AtomUni(LessUni(0,0,c))
))
))
"
lemma convert_alternateNegInfinity :
assumes "convert_poly var p (xs'@x#xs) = Some X"
assumes "length xs' = var"
shows "eval (alternateNegInfinity p var) (xs'@x#xs) = evalUni (alternateNegInfinity' X) x"
proof(cases X)
case (fields a b c)
then show ?thesis proof(cases "MPoly_Type.degree p var = 0")
case True
then show ?thesis
using assms
apply (simp add: isovar_greater_degree)
apply auto
apply (metis aEval.simps(2) eval.simps(1) eval_and eval_false eval_or mult_one_left)
by (metis aEval.simps(2) eval.simps(1) eval_or mult_one_left)
next
case False
then have nonzero : "MPoly_Type.degree p var ≠ 0" by auto
then show ?thesis
proof(cases "MPoly_Type.degree p var = 1")
case True
have letbind: "eval
(let a_n = isolate_variable_sparse p var (Suc 0)
in or (fm.Atom (Less (Const (- 1) * a_n)))
(and (fm.Atom (Eq a_n))
(let a_n = isolate_variable_sparse p var 0
in or (fm.Atom (Less (Const 1 * a_n))) (and (fm.Atom (Eq a_n)) FalseF))))
(xs'@x#xs) =
eval
(or (fm.Atom (Less (Const (- 1) * (isolate_variable_sparse p var (Suc 0)))))
(and (fm.Atom (Eq (isolate_variable_sparse p var (Suc 0))))
(or (fm.Atom (Less (Const 1 * (isolate_variable_sparse p var 0)))) (and (fm.Atom (Eq (isolate_variable_sparse p var 0))) FalseF))))
(xs'@x#xs)"
by meson
show ?thesis
using assms True unfolding fields
by (simp add: isovar_greater_degree letbind eval_or eval_and insertion_mult insertion_const)
next
case False
then have degree2 : "MPoly_Type.degree p var = 2" using degree_convert_eq[OF assms(1)] nonzero by auto
have "[0..<3] = [0,1,2]"
by (simp add: upt_rec)
then have unfold : " (foldl
(λF i. let a_n = isolate_variable_sparse p var i
in or (fm.Atom (Less ((if i mod 2 = 0 then Const 1 else Const (- 1)) * a_n)))
(and (fm.Atom (Eq a_n)) F))
FalseF [0..<3]) =
(let a_n = isolate_variable_sparse p var 2
in or (fm.Atom (Less ((Const 1) * a_n)))
(and (fm.Atom (Eq a_n))
(let a_n = isolate_variable_sparse p var (Suc 0)
in or (fm.Atom (Less (Const (- 1) * a_n)))
(and (fm.Atom (Eq a_n))
(let a_n = isolate_variable_sparse p var 0
in or (fm.Atom (Less (Const 1 * a_n))) (and (fm.Atom (Eq a_n)) FalseF))))))"
by auto
have letbind : "eval
(foldl
(λF i. let a_n = isolate_variable_sparse p var i
in or (fm.Atom (Less ((if i mod 2 = 0 then Const 1 else Const (- 1)) * a_n)))
(and (fm.Atom (Eq a_n)) F))
FalseF [0..<3]) (xs'@x#xs) =
eval
(or (fm.Atom (Less ( Const 1 * (isolate_variable_sparse p var 2))))
(and (fm.Atom (Eq (isolate_variable_sparse p var 2)))
(or (fm.Atom (Less (Const (- 1) * (isolate_variable_sparse p var (Suc 0)))))
(and (fm.Atom (Eq (isolate_variable_sparse p var (Suc 0))))
(or (fm.Atom (Less (Const 1 * (isolate_variable_sparse p var 0)))) (and (fm.Atom (Eq (isolate_variable_sparse p var 0))) FalseF))))))
(xs'@x#xs)" apply (simp add:unfold) by metis
show ?thesis
using degree2 assms unfolding fields by (simp add: isovar_greater_degree eval_or eval_and letbind insertion_mult insertion_const)
qed
qed
qed
fun substNegInfinityUni :: "atomUni ⇒ atomUni fmUni" where
"substNegInfinityUni (EqUni p) = allZero' p " |
"substNegInfinityUni (LessUni p) = alternateNegInfinity' p"|
"substNegInfinityUni (LeqUni p) = OrUni (alternateNegInfinity' p) (allZero' p)"|
"substNegInfinityUni (NeqUni p) = negUni (allZero' p)"
lemma convert_substNegInfinity :
assumes "convert_atom var A (xs'@x#xs) = Some(A')"
assumes "length xs' = var"
shows "eval (substNegInfinity var A) (xs'@x#xs) = evalUni (substNegInfinityUni A') x"
using assms
proof(cases A)
case (Less p)
have "∃X. convert_poly var p (xs' @ x # xs) = Some X" using assms Less apply(cases "MPoly_Type.degree p var < 3") by (simp_all)
then obtain X where X_def: "convert_poly var p (xs' @ x # xs) = Some X" by auto
then have A' : "A' = LessUni X" using assms Less apply(cases "MPoly_Type.degree p var < 3") by (simp_all)
show ?thesis unfolding Less substNegInfinity.simps
unfolding convert_alternateNegInfinity[OF X_def assms(2)] A'
apply(cases X) by simp
next
case (Eq p)
then show ?thesis using assms convert_allZero by auto
next
case (Leq p)
define p' where "p' = (case convert_poly var p (xs'@x#xs) of Some p' ⇒ p')"
have A'_simp : "A' = LeqUni p'"
using assms Leq
using p'_def by auto
have allZ : "eval (allZero p var) (xs'@x#xs) = evalUni (allZero' p') x" using convert_allZero
using Leq assms p'_def by auto
have altNeg : "eval (alternateNegInfinity p var) (xs'@x#xs) = evalUni (alternateNegInfinity' p') x" using convert_alternateNegInfinity
using Leq assms p'_def by auto
show ?thesis
unfolding Leq substNegInfinity.simps eval_Or A'_simp substNegInfinityUni.simps evalUni.simps
using allZ altNeg by auto
next
case (Neq p)
then show ?thesis using assms convert_allZero convert_neg by auto
qed
lemma change_eval_eq:
fixes x y:: "real"
assumes "((aEvalUni (EqUni(a,b,c)) x ≠ aEvalUni (EqUni(a,b,c)) y) ∧ x < y)"
shows "(∃w. x ≤ w ∧ w ≤ y ∧ a*w^2 + b*w + c = 0)"
using assms by auto
lemma change_eval_lt:
fixes x y:: "real"
assumes "((aEvalUni (LessUni (a,b,c)) x ≠ aEvalUni (LessUni (a,b,c)) y) ∧ x < y)"
shows "(∃w. x ≤ w ∧ w ≤ y ∧ a*w^2 + b*w + c = 0)"
proof -
let ?p = "[:c, b, a:]"
have "sign ?p x ≠ sign ?p y"
using assms unfolding sign_def
apply (simp add: distrib_left mult.commute mult.left_commute power2_eq_square)
by linarith
then have "(∃w ∈ (root_list ?p). x ≤ w ∧ w ≤ y)" using changes_sign
assms by auto
then obtain w where w_prop: "w ∈ (root_list ?p) ∧ x ≤ w ∧ w ≤ y" by auto
then have "a*w^2 + b*w + c = 0" unfolding root_list_def
using add.commute distrib_right mult.assoc mult.commute power2_eq_square
using quadratic_poly_eval by force
then show ?thesis using w_prop by auto
qed
lemma no_change_eval_lt:
fixes x y:: "real"
assumes "x < y"
assumes "¬(∃w. x ≤ w ∧ w ≤ y ∧ a*w^2 + b*w + c = 0)"
shows "((aEvalUni (LessUni (a,b,c)) x = aEvalUni (LessUni (a,b,c)) y))"
using change_eval_lt
using assms(1) assms(2) by blast
lemma change_eval_neq:
fixes x y:: "real"
assumes "((aEvalUni (NeqUni (a,b,c)) x ≠ aEvalUni (NeqUni (a,b,c)) y) ∧ x < y)"
shows "(∃w. x ≤ w ∧ w ≤ y ∧ a*w^2 + b*w + c = 0)"
using assms by auto
lemma change_eval_leq:
fixes x y:: "real"
assumes "((aEvalUni (LeqUni (a,b,c)) x ≠ aEvalUni (LeqUni (a,b,c)) y) ∧ x < y)"
shows "(∃w. x ≤ w ∧ w ≤ y ∧ a*w^2 + b*w + c = 0)"
proof -
let ?p = "[:c, b, a:]"
have "sign ?p x ≠ sign ?p y"
using assms unfolding sign_def
apply (simp add: distrib_left mult.commute mult.left_commute power2_eq_square)
by linarith
then have "(∃w ∈ (root_list ?p). x ≤ w ∧ w ≤ y)" using changes_sign
assms by auto
then obtain w where w_prop: "w ∈ (root_list ?p) ∧ x ≤ w ∧ w ≤ y" by auto
then have "a*w^2 + b*w + c = 0" unfolding root_list_def
using add.commute distrib_right mult.assoc mult.commute power2_eq_square
using quadratic_poly_eval by force
then show ?thesis using w_prop by auto
qed
lemma change_eval:
fixes x y:: "real"
fixes At:: "atomUni"
assumes xlt: "x < y"
assumes noteq: "((aEvalUni At) x ≠ aEvalUni (At) y)"
assumes "getPoly At = (a, b, c)"
shows "(∃w. x ≤ w ∧ w ≤ y ∧ a*w^2 + b*w + c = 0)"
proof -
have four_types: "At = (EqUni (a,b,c)) ∨ At = (LessUni (a,b,c)) ∨ At = (LeqUni (a,b,c)) ∨ At = (NeqUni (a,b,c))"
using getPoly.elims assms(3) by force
have eq_h: "At = (EqUni (a,b,c)) ⟶ (∃w. x ≤ w ∧ w ≤ y ∧ a*w^2 + b*w + c = 0)"
using assms(1) assms(2) change_eval_eq
by blast
have less_h: "At = (LessUni(a,b,c)) ⟶ (∃w. x ≤ w ∧ w ≤ y ∧ a*w^2 + b*w + c = 0)"
using change_eval_lt assms
by blast
have leq_h: "At = (LeqUni(a,b,c)) ⟶ (∃w. x ≤ w ∧ w ≤ y ∧ a*w^2 + b*w + c = 0)"
using change_eval_leq assms
by blast
have neq_h: "At = (NeqUni(a,b,c)) ⟶ (∃w. x ≤ w ∧ w ≤ y ∧ a*w^2 + b*w + c = 0)"
using change_eval_neq assms
by blast
show ?thesis
using four_types eq_h less_h leq_h neq_h
by blast
qed
lemma no_change_eval:
fixes x y:: "real"
assumes "getPoly At = (a, b, c)"
assumes "x < y"
assumes "¬(∃w. x ≤ w ∧ w ≤ y ∧ a*w^2 + b*w + c = 0)"
shows "((aEvalUni At) x = aEvalUni (At) y ∧ x < y)"
using change_eval
using assms(1) assms(2) assms(3) by blast
lemma same_eval'' :
assumes "getPoly At = (a, b, c)"
assumes nonz: "a ≠ 0 ∨ b ≠ 0 ∨ c ≠ 0"
shows "∃x. ∀y<x. (aEvalUni At y = aEvalUni At x)"
proof -
let ?p = "[:c, b, a:]"
have poly_eval: "∀y. poly ?p y = a*y^2 + b*y + c"
by (simp add: distrib_left power2_eq_square)
have "?p ≠ 0" using nonz by auto
then have "finite {y. poly ?p y = 0}"
using poly_roots_finite
by blast
then have "finite {y. c + (a * y⇧2 + b * y) = 0} ⟹
∀y. y * (b + y * a) = a * y⇧2 + b * y ⟹
finite {y. a * y⇧2 + b * y + c = 0}"
proof -
assume a1: "finite {y. c + (a * y⇧2 + b * y) = 0}"
have "∀x0. c + (a * x0⇧2 + b * x0) = a * x0⇧2 + b * x0 + c"
by simp
then show ?thesis
using a1 by presburger
qed
then have finset: "finite {y. a*y^2 + b*y + c = 0}"
using poly_eval
by (metis ‹finite {y. poly [:c, b, a:] y = 0}› poly_roots_set_same)
then have "∃x. (∀y. a*y^2 + b*y + c = 0 ⟶ x < y)"
proof -
let ?l = "sorted_list_of_set {y. a*y^2 + b*y + c = 0}"
have "∃x. x < ?l ! 0"
using infzeros nonz by blast
then obtain x where x_prop: "x < ?l! 0" by auto
then have "∀ y. List.member ?l y ⟶ x < y"
proof clarsimp
fix y
assume "List.member ?l y"
then have "∃n. n < length ?l ∧ ?l ! n = y"
by (meson in_set_conv_nth in_set_member)
then obtain n where n_prop: "n < length ?l ∧ ?l ! n = y"
by auto
have h: "∀n < length ?l. ?l ! n ≥ ?l !0" using sorted_iff_nth_mono
using sorted_sorted_list_of_set by blast
then have h: "y ≥ ?l ! 0" using n_prop by auto
then show "x < y" using x_prop by auto
qed
then show ?thesis
using finset set_sorted_list_of_set in_set_member
by (metis (mono_tags, lifting) mem_Collect_eq)
qed
then obtain x where x_prop: "(∀y. a*y^2 + b*y + c = 0 ⟶ x < y)" by auto
then have same_as: "∀y<x. (aEvalUni At y = aEvalUni At x)"
using no_change_eval change_eval assms by (smt (verit, ccfv_SIG))
then show ?thesis by auto
qed
lemma inequality_case : "(∃(x::real). ∀(y::real)<x. (a::real) * y⇧2 + (b::real) * y + (c::real) < 0) =
(a < 0 ∨ a = 0 ∧ (0 < b ∨ b = 0 ∧ c < 0))"
proof-
let ?At = "(LessUni (a, b, c))"
have firsth : "⋀x. (∀y<x. a * y⇧2 + b * y + c < 0 ⟹ a≤0)"
proof -
fix x
assume lt: "∀y<x. a * y⇧2 + b * y + c < 0"
have "∃w. ∀y < w. y^2 > (-b/a)*y - c/a" using ysq_dom_y_plus_coeff[where b = "-b/a", where c = "-c/a"]
by auto
then have gtdomhelp: "a > 0 ⟹ ∃w. ∀y < w. a*y^2 > a*((-b/a)*y - c/a)"
by auto
have "∀y. (a > 0 ⟶ a*((-b/a)*y - c/a) = -b*y - c)"
by (simp add: right_diff_distrib')
then have gtdom: "a > 0 ⟹ ∃w.∀y < w. a*y^2 > -b*y - c"
using gtdomhelp
by simp
then have " a > 0 ⟹ False"
proof -
assume "a > 0"
then have "∃w.∀y < w. a*y^2 > -b*y - c" using gtdom by auto
then obtain w where w_prop: "∀y < w. a*y^2 + b*y + c > 0"
by fastforce
let ?mn = "min w x - 1"
have gtz: "a*?mn^2 + b*?mn + c > 0" using w_prop
by auto
have ltz: "a*?mn^2 + b*?mn + c < 0" using lt by auto
then show "False" using gtz ltz by auto
qed
then show "a ≤ 0"
by fastforce
qed
have bleq0 : "⋀x. (∀y<x. b * y + c < 0 ⟹ b≥0)"
proof -
fix x
assume lt: "∀y<x. b * y + c < 0"
have gtdom: "b < 0 ⟹ ∃w.∀y < w. b*y > - c"
by (metis mult.commute neg_less_divide_eq)
then have "b < 0 ⟹ False"
proof -
assume "b < 0"
then have "∃w.∀y < w. b*y > - c" using gtdom by auto
then obtain w where w_prop: "∀y < w .b*y + c > 0"
by fastforce
let ?mn = "min w x - 1"
have gtz: "b*?mn + c > 0" using w_prop
by auto
have ltz: "b*?mn + c < 0" using lt by auto
then show "False" using gtz ltz by auto
qed
then show "b ≥ 0"
by fastforce
qed
have secondh: "⋀x. (∀y<x. a * y⇧2 + b * y + c < 0 ⟹ ¬ a < 0 ⟹ ¬ 0 < b ⟹ b = 0)"
using firsth bleq0
by (metis add.commute add.right_neutral less_eq_real_def mult_zero_class.mult_zero_left)
have thirdh : "⋀x. ∀y<x. a * y⇧2 + b * y + c < 0 ⟹ ¬ a < 0 ⟹ ¬ 0 < b ⟹ c < 0"
using firsth secondh add.commute add.right_neutral infzeros mult_zero_class.mult_zero_left not_numeral_le_zero order_refl
by (metis less_eq_real_def)
have fourthh : "a < 0 ⟹ ∃x. ∀y<x. a * y⇧2 + b * y + c < 0"
proof -
assume aleq: "a < 0"
have "∃(w::real). ∀(y::real). (y < w ⟶ y^2 > (-b/a)*y + (-c/a))"
using ysq_dom_y_plus_coeff[where b = "-b/a", where c = "-c/a"]
by blast
then have hyp:"∃(w::real). ∀(y::real). (y < w ⟶ a*y^2 ≤ a*(-b/a)*y + a*(-c/a))"
by (metis (no_types, opaque_lifting) ‹a < 0› distrib_left less_eq_real_def linorder_not_le mult.assoc mult_less_cancel_left)
have "∀y. a*(-b/a)*y + a*(-c/a) = -b*y -c"
using ‹a < 0› by auto
then have "∃(w::real). ∀(y::real). (y < w ⟶ a*y^2 ≤ -b*y - c)"
using hyp by auto
then have "∃(w::real). ∀(y::real). (y < w ⟶ a*y^2 + b*y + c ≤ 0)"
by (metis add.commute add_uminus_conv_diff le_diff_eq mult_minus_left real_add_le_0_iff)
then obtain w where w_prop: "∀(y::real). (y < w ⟶ a*y^2 + b*y + c ≤ 0)" by auto
have "∃x. ∀y < x. aEvalUni ?At x = aEvalUni ?At y" using same_eval''
proof -
have f1: "∀x0 x1. ((x0::real) < x1) = (¬ 0 ≤ x0 + - 1 * x1)"
by linarith
have "a ≠ 0"
using ‹a < 0› by force
then obtain rr :: "atomUni ⇒ real" where
"∀r. 0 ≤ r + - 1 * rr (LessUni (a, b, c)) ∨ aEvalUni (LessUni (a, b, c)) r = aEvalUni (LessUni (a, b, c)) (rr (LessUni (a, b, c)))"
using f1 by (metis getPoly.simps(4) same_eval'')
then show ?thesis
using f1 by meson
qed
then obtain x where x_prop: "∀y < x. aEvalUni ?At x = aEvalUni ?At y" by auto
let ?mn = "min x w - 1"
have "∀y < ?mn. aEvalUni ?At y = True ∨ aEvalUni ?At y = False"
using x_prop by auto
have "∀ y < ?mn. aEvalUni ?At y = False ⟶ a*y^2 + b*y + c ≥ 0"
by auto
then have "⋀y. ∀y<w. a * y⇧2 + b * y + c ≤ 0 ⟹
y < min x w - 1 ⟹
¬ a * y⇧2 + b * y + c < 0 ⟹
a * y⇧2 + b * y + c = 0"
proof -
fix y :: real
assume a1: "y < min x w - 1"
assume a2: "¬ a * y⇧2 + b * y + c < 0"
assume a3: "∀y<w. a * y⇧2 + b * y + c ≤ 0"
have "y < w"
using a1 by linarith
then show "a * y⇧2 + b * y + c = 0"
using a3 a2 less_eq_real_def by blast
qed
then have "∀ y < ?mn. aEvalUni ?At y = False ⟶ a*y^2 + b*y + c = 0"
using w_prop by auto
then have "∀ y < ?mn. aEvalUni ?At y = False ⟹ False" using infzeros aleq
by (metis power_zero_numeral zero_less_power2)
then have "∀ y < ?mn. aEvalUni ?At y = True"
proof -
{ fix rr :: real
have "∀r ra. (ra::real) < r ∨ ¬ ra < r + - 1"
by linarith
then have "¬ rr < min x w - 1 ∨ aEvalUni (LessUni (a, b, c)) rr"
by (metis (no_types) ‹∀y<min x w - 1. aEvalUni (LessUni (a, b, c)) y = False ⟹ False› ab_group_add_class.ab_diff_conv_add_uminus less_eq_real_def min_less_iff_disj not_le x_prop) }
then show ?thesis
by blast
qed
then show ?thesis by auto
qed
have fifthh : "b > 0 ⟹ ∃x. ∀y<x. b * y + c < 0"
proof-
assume bh : "b > 0"
show "∃x. ∀y<x. b * y + c < 0"
apply(rule exI[where x="-c/b"])
apply auto
using bh
by (simp add: mult.commute pos_less_minus_divide_eq)
qed
show ?thesis
apply(auto)
using firsth apply simp
using secondh apply simp
using thirdh apply simp
using fourthh apply simp
using fifthh by simp
qed
lemma inequality_case_geq : "(∃(x::real). ∀(y::real)<x. (a::real) * y⇧2 + (b::real) * y + (c::real) > 0) =
(a > 0 ∨ a = 0 ∧ (0 > b ∨ b = 0 ∧ c > 0))"
proof -
have s1: "∀y. - 1 * a * y⇧2 + - 1 * b * y + - 1 * c < 0 ⟷ a * y⇧2 + b * y + c > 0"
by auto
have s2: "(- 1 * a < 0 ∨ - 1 * a = 0 ∧ (0 < - 1 * b ∨ - 1 * b = 0 ∧ - 1 * c < 0)) ⟷
(a > 0 ∨ a = 0 ∧ (0 > b ∨ b = 0 ∧ c > 0)) "
by auto
have "(∃x. ∀y<x. - 1 * a * y⇧2 + - 1 * b * y + - 1 * c < 0) =
(- 1 * a < 0 ∨ - 1 * a = 0 ∧ (0 < - 1 * b ∨ - 1 * b = 0 ∧ - 1 * c < 0))"
using inequality_case[where a = "-1*a", where b = "-1*b", where c= "-1*c"]
by auto
then show ?thesis
using s1 s2 by auto
qed
lemma infinity_evalUni_LessUni : "(∃x. ∀y<x. aEvalUni (LessUni p) y) = (evalUni (substNegInfinityUni (LessUni p)) x)"
proof(cases p)
case (fields a b c)
show ?thesis
unfolding fields apply simp
using inequality_case[of a b c] .
qed
lemma infinity_evalUni_EqUni : "(∃x. ∀y<x. aEvalUni (EqUni p) y) = (evalUni (substNegInfinityUni (EqUni p)) x)"
proof(cases p)
case (fields a b c)
show ?thesis
using infzeros[of _ a b c] by(auto simp add: fields)
qed
lemma infinity_evalUni_NeqUni : "(∃x. ∀y<x. aEvalUni (NeqUni p) y) = (evalUni (substNegInfinityUni (NeqUni p)) x)"
proof(cases p)
case (fields a b c)
show ?thesis
unfolding fields apply simp
using inequality_case[of a b c]
using inequality_case_geq[of a b c]
by (metis less_numeral_extra(3) linorder_neqE_linordered_idom mult_eq_0_iff)
qed
lemma infinity_evalUni_LeqUni : "(∃x. ∀y<x. aEvalUni (LeqUni p) y) = (evalUni (substNegInfinityUni (LeqUni p)) x)"
proof(cases p)
case (fields a b c)
show ?thesis
unfolding fields apply simp
proof -
have h1: "((∃x. ∀y<x. a * y⇧2 + b * y + c < 0) ∨ (∃x. ∀y<x. a * y⇧2 + b * y + c = 0)) ⟶ (∃x. ∀y<x. a * y⇧2 + b * y + c ≤ 0)"
using less_eq_real_def
by auto
have h2: "(∃x. ∀y<x. a * y⇧2 + b * y + c ≤ 0) ⟹ ((∃x. ∀y<x. a * y⇧2 + b * y + c < 0) ∨ (∃x. ∀y<x. a * y⇧2 + b * y + c = 0))"
proof -
assume a1: "(∃x. ∀y<x. a * y⇧2 + b * y + c ≤ 0)"
have "¬(∃x. ∀y<x. a * y⇧2 + b * y + c = 0) ⟹ (∃x. ∀y<x. a * y⇧2 + b * y + c < 0) "
proof -
assume a2: "¬(∃x. ∀y<x. a * y⇧2 + b * y + c = 0)"
then have "a ≠ 0 ∨ b ≠ 0 ∨ c ≠ 0" by auto
then have "(a < 0 ∨ a = 0 ∧ (0 < b ∨ b = 0 ∧ c < 0))"
proof -
have x1: "a > 0 ⟹ False"
proof -
assume "a > 0"
then have "(∃(x::real). ∀(y::real)<x. (a::real) * y⇧2 + (b::real) * y + (c::real) > 0)" using inequality_case_geq
by auto
then show ?thesis
using a1
by (meson a2 linorder_not_le min_less_iff_conj)
qed
then have x2: "a = 0 ∧ 0 > b ⟹ False"
proof -
assume "a = 0 ∧ 0 > b"
then have "(∃(x::real). ∀(y::real)<x. (a::real) * y⇧2 + (b::real) * y + (c::real) > 0)" using inequality_case_geq
by blast
then show ?thesis
using a1
by (meson a2 linorder_not_le min_less_iff_conj)
qed
then have x3: "a = 0 ∧ b = 0 ∧ c > 0 ⟹ False "
using a1 a2 by auto
show ?thesis using x1 x2 x3
by (meson ‹a ≠ 0 ∨ b ≠ 0 ∨ c ≠ 0› linorder_neqE_linordered_idom)
qed
then show "(∃x. ∀y<x. a * y⇧2 + b * y + c < 0)" using inequality_case
by auto
qed
then show ?thesis
by auto
qed
have "(∃x. ∀y<x. a * y⇧2 + b * y + c ≤ 0) = (∃x. ∀y<x. a * y⇧2 + b * y + c < 0) ∨ (∃x. ∀y<x. a * y⇧2 + b * y + c = 0)"
using h1 h2 by auto
then show "(∃x. ∀y<x. a * y⇧2 + b * y + c ≤ 0) =
(a < 0 ∨ a = 0 ∧ (0 < b ∨ b = 0 ∧ c < 0) ∨ a = 0 ∧ b = 0 ∧ c = 0)"
using inequality_case[of a b c] infzeros[of _ a b c] by auto
qed
qed
text "This is the vertical translation for substNegInfinityUni where we represent the virtual
substution of negative infinity in the univariate case"
lemma infinity_evalUni :
shows "(∃x. ∀y<x. aEvalUni At y) = (evalUni (substNegInfinityUni At) x)"
proof(cases At)
case (LessUni p)
then show ?thesis using infinity_evalUni_LessUni by auto
next
case (EqUni p)
then show ?thesis using infinity_evalUni_EqUni by auto
next
case (LeqUni p)
then show ?thesis using infinity_evalUni_LeqUni by auto
next
case (NeqUni p)
then show ?thesis using infinity_evalUni_NeqUni by auto
qed
end