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 * y2 + b * y) = 0} 
    y. y * (b + y * a) = a * y2 + b * y 
    finite {y. a * y2 + b * y + c = 0}"
  proof -
    assume a1: "finite {y. c + (a * y2 + b * y) = 0}"
    have "x0. c + (a * x02 + b * x0) = a * x02 + 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) * y2 + (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 * y2 + b * y + c < 0  a0)"
  proof -
    fix x
    assume lt: "y<x. a * y2 + 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  b0)"
  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 * y2 + 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 * y2 + 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 * y2 + 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 * y2 + b * y + c  0 
         y < min x w - 1 
         ¬ a * y2 + b * y + c < 0 
         a * y2 + b * y + c = 0"
    proof -
      fix y :: real
      assume a1: "y < min x w - 1"
      assume a2: "¬ a * y2 + b * y + c < 0"
      assume a3: "y<w. a * y2 + b * y + c  0"
      have "y < w"
        using a1 by linarith
      then show "a * y2 + 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) * y2 + (b::real) * y + (c::real) > 0) =
    (a > 0  a = 0  (0 > b  b = 0  c > 0))"
proof - 
  have s1: "y. - 1 * a * y2 + - 1 * b * y + - 1 * c < 0   a * y2 +  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 * y2 + - 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 * y2 + b * y + c < 0)  (x. y<x. a * y2 + b * y + c = 0))  (x. y<x. a * y2 + b * y + c  0)"
      using less_eq_real_def
      by auto
    have h2: "(x. y<x. a * y2 + b * y + c  0)  ((x. y<x. a * y2 + b * y + c < 0)  (x. y<x. a * y2 + b * y + c = 0))"
    proof -
      assume a1: "(x. y<x. a * y2 + b * y + c  0)"
      have "¬(x. y<x. a * y2 + b * y + c = 0)  (x. y<x. a * y2 + b * y + c < 0) " 
      proof - 
        assume a2: "¬(x. y<x. a * y2 + 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) * y2 + (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) * y2 + (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 * y2 + b * y + c < 0)" using inequality_case
          by auto
      qed
      then show ?thesis
        by auto
    qed
    have "(x. y<x. a * y2 + b * y + c  0) = (x. y<x. a * y2 + b * y + c < 0)  (x. y<x. a * y2 + b * y + c = 0)"
      using h1 h2 by auto
    then show "(x. y<x. a * y2 + 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