Theory Virtual_Substitution.EliminateVariable

subsection "Lemmas of the elimVar function"

theory EliminateVariable
  imports LinearCase QuadraticCase  "HOL-Library.Quadratic_Discriminant"
begin




lemma elimVar_eq :
  assumes hlength : "length xs = var"
  assumes in_list : "Eq p  set(L)"
  assumes low_pow : "MPoly_Type.degree p var = 1  MPoly_Type.degree p var = 2"
  shows "((x. eval (list_conj (map fm.Atom L @ F)) (xs @ x # Γ)) =
    ((x. eval (elimVar var L F (Eq p)) (xs @ x # Γ))) (x. aEval (Eq p) (xs @ x # Γ)))"
proof-

  { fix x
    define A where "A = (isolate_variable_sparse p var 2)"
    define B where "B = (isolate_variable_sparse p var 1)"
    define C where "C = (isolate_variable_sparse p var 0)"
    have freeA : "var  vars A"
      unfolding A_def
      by (simp add: not_in_isovarspar)
    have freeB : "var  vars B"
      unfolding B_def
      by (simp add: not_in_isovarspar)
    have freeC : "var  vars C"
      unfolding C_def
      by (simp add: not_in_isovarspar)
    assume "eval (list_conj (map fm.Atom L @ F)) (xs @ x # Γ)"
    then have h : "(aset L. aEval a (xs @ x # Γ))  (fset F. eval f (xs @ x # Γ))"
      apply(simp add:eval_list_conj)
      by (meson Un_iff eval.simps(1) image_eqI)
    define X where "X=xs@x#Γ"
    have Xlength : "length X > var"
      using X_def hlength by auto
    define Aval where "Aval = insertion (nth_default 0 (list_update X var x)) A"
    define Bval where "Bval = insertion (nth_default 0 (list_update X var x)) B"
    define Cval where "Cval = insertion (nth_default 0 (list_update X var x)) C"
    have hinsert : "(xs @ x # Γ)[var := x] = (xs @ x #Γ)"
      using hlength by auto
    have allAval : "x. insertion (nth_default 0 (xs @ x # Γ)) A = Aval"
      using Aval_def
      using not_contains_insertion[where var="var", where p = "A", OF freeA, where L = "xs @ x #Γ", where x="x", where val="Aval"]
      unfolding X_def hinsert using hlength by auto
    have allBval : "x. insertion (nth_default 0 (xs @ x # Γ)) B = Bval"
      using Bval_def
      using not_contains_insertion[where var="var", where p = "B", OF freeB, where L = "xs @ x #Γ", where x="x", where val="Bval"]
      unfolding X_def hinsert using hlength by auto
    have allCval : "x. insertion (nth_default 0 (xs @ x # Γ)) C = Cval"
      using Cval_def
      using not_contains_insertion[where var="var", where p = "C", OF freeC, where L = "xs @ x #Γ", where x="x", where val="Cval"]
      unfolding X_def hinsert using hlength by auto
    have insertion_p : "insertion (nth_default 0 X) p = 0"
      using in_list h aEval.simps(1) X_def by fastforce
    have express_p : "p = A * Var var ^ 2 + B * Var var + C"
      using express_poly[OF low_pow] unfolding A_def B_def C_def
      by fastforce
    have insertion_p' : "Aval *x^2+Bval *x+Cval = 0"
      using express_p insertion_p unfolding Aval_def Bval_def Cval_def X_def hinsert
      apply(simp add: insertion_add insertion_mult insertion_pow)
      using  insertion_var by (metis X_def Xlength hinsert) 
    have biglemma : "
       ((Aval = 0 
        Bval  0 
        (fset L. aEval (linear_substitution var (-C) B f) (xs @ x # Γ))  
        (fset F. eval (linear_substitution_fm var (-C) B f) (xs @ x # Γ)) 
        Aval  0 
        insertion (nth_default 0 (xs @ x # Γ)) 4 * 
        Aval *
        Cval
         (Bval)2 
        ((fset L. eval (quadratic_sub var (- B) 1 (B2 - 4 * A * C) (2 * A) f) (xs @ x # Γ))
         (fset F. eval (quadratic_sub_fm var (- B) 1 (B2 - 4 * A * C) (2 * A) f) (xs @ x # Γ)) 
         (fset L. eval (quadratic_sub var (- B) (-1) (B2 - 4 * A * C) (2 * A) f) (xs @ x # Γ)) 
         (fset F. eval (quadratic_sub_fm var (- B) (-1) (B2 - 4 * A * C) (2 * A) f) (xs @ x # Γ))) 
        Aval = 0 
        Bval = 0 
        Cval = 0))"
    proof(cases "Aval=0")
      case True
      then have aval0 : "Aval=0" by simp
      show ?thesis proof(cases "Bval=0")
        case True
        then have bval0 :  "Bval=0" by simp
        have h : "eval (list_conj (map fm.Atom L @ F)) (xs @ x # Γ)"
          using hlength h unfolding X_def
          using eval (list_conj (map fm.Atom L @ F)) (xs @ x # Γ) by blast
        show ?thesis proof(cases "Cval=0")
          case True
          show ?thesis                                  
            by(simp add:aval0 True bval0)
        next
          case False
          show ?thesis
            using insertion_p' aval0 bval0 False by(simp)
        qed
      next
        case False
        have bh : "insertion (nth_default 0 (X[var := - Cval / Bval])) B = Bval"
          using allBval unfolding X_def
          using Bval_def X_def freeB not_contains_insertion by blast
        have ch : "insertion (nth_default 0 (X[var := - Cval / Bval])) C = Cval"
          using allCval unfolding X_def
          using Cval_def X_def freeC not_contains_insertion by blast
        have xh : "x=-Cval/Bval"
        proof-
          have "Bval*x+Cval = 0"
            using insertion_p' aval0
            by simp
          then show ?thesis using False
            by (smt nonzero_mult_div_cancel_left)
        qed
        have freecneg : "var  vars (-C)" using freeC not_in_neg by auto
        have h1:  "(aset L. aEval (linear_substitution var (-C) (B) a) (X[var := x]))"
          using h xh Bval_def Cval_def False LinearCase.linear[OF Xlength False freecneg freeB, of "-Cval"] freeB freeC freecneg
          by (metis X_def hinsert insertion_neg)
        have h2 : "fset F. eval (linear_substitution_fm var (-C) B f) (X[var := x])"
          using h xh Bval_def Cval_def False LinearCase.linear_fm[OF Xlength False freecneg freeB, of "-Cval"] freeB freeC
          by (metis X_def hinsert insertion_neg)
        show ?thesis using h1 h2 apply(simp add:aval0 False)
          using X_def hlength
          using hinsert by auto
      qed
    next
      case False
      then have aval0 : "Aval 0" by simp
      have h4 : "insertion (nth_default 0 (X[var := x])) 4 = 4"
        using insertion_const[where f = "(nth_default 0 (X[var := x]))", where c="4"]
        by (metis MPoly_Type.insertion_one insertion_add numeral_Bit0 one_add_one)
      show ?thesis proof(cases "4 * Aval * Cval  Bval2")
        case True
        have h1a : "varvars(-B)"
          by(simp add: freeB not_in_neg)
        have h1b : "varvars(1::real mpoly)"
          using isolate_var_one not_in_isovarspar by blast
        have h1c : "varvars(-1::real mpoly)"
          by(simp add: h1b not_in_neg)
        have h1d : "varvars(4::real mpoly)"
          by (metis h1b not_in_add numeral_Bit0 one_add_one)
        have h1e : "varvars(B^2-4*A*C)" 
          by(simp add: freeB h1d freeA freeC not_in_mult not_in_pow not_in_sub)
        have h1f : "varvars(2::real mpoly)"
          using h1b not_in_add by fastforce
        have h1g : "varvars(2*A)"
          by(simp add: freeA h1f not_in_mult)
        have h1h : "freeIn var (quadratic_sub var (-B) (1) (B^2-4*A*C) (2*A) a)"
          using free_in_quad h1a h1b h1e h1g by blast
        have h1i : "freeIn var (quadratic_sub var (-B) (-1) (B^2-4*A*C) (2*A) a)"
          using free_in_quad h1a h1c h1e h1g by blast 
        have h2 : "2*Aval  0" using aval0 by auto
        have h3 : "0  (Bval^2-4*Aval*Cval)" using True by auto
        have h4a : "var  vars 4"
          by (metis monom_numeral notInKeys_notInVars not_in_add not_in_isovarspar not_in_pow one_add_one power.simps(1) rel_simps(76) vars_monom_keys) 
        have h4 : "var  vars (B^2-4*A*C)" by(simp add: h4a freeA freeB freeC not_in_pow not_in_mult not_in_sub)  
        have h5 : "x. insertion (nth_default 0 (list_update X var x)) (-B) = -Bval " 
          using allBval apply(simp add: insertion_neg)
          by (simp add: B_def Bval_def insertion_isovarspars_free)
        have h6 : "x. insertion (nth_default 0 (list_update X var x)) 1 = 1" by simp
        have h6a : "x. insertion (nth_default 0 (list_update X var x)) (-1) = (-1)" using h6 by (simp add: insertion_neg) 
        have h7a : "x. insertion (nth_default 0 (list_update X var x)) 4 = 4" by (metis h6 insertion_add numeral_Bit0 one_add_one)
        have h7b : "var  vars(4*A*C)" using freeA freeC by (simp add: h4a not_in_mult) 
        have h7c : "var  vars(B^2)" using freeB not_in_pow by auto
        have h7 : "x. insertion (nth_default 0 (list_update X var x)) (B^2-4*A*C) = (Bval^2-4*Aval*Cval)"
          using h7a allAval allBval allCval unfolding X_def  using hlength 
          apply (simp add: insertion_mult insertion_sub power2_eq_square)
          by (metis A_def Aval_def Bval_def C_def Cval_def X_def freeB insertion_isovarspars_free not_contains_insertion)
        have h8a : "x. insertion (nth_default 0 (list_update X var x)) 2 = 2" by (metis h6 insertion_add one_add_one)
        have h8 : "x. insertion (nth_default 0 (list_update X var x)) (2*A) = (2*Aval)"
          apply(simp add: allAval h8a insertion_mult)
          by (simp add: A_def Aval_def insertion_isovarspars_free)

        have h1 : "- Bval2 + 4 * Aval * Cval  0"
          using True by simp
        have xh : "x = (- Bval + sqrt (Bval2 - 4 * Aval * Cval)) / (2 * Aval)x=(- Bval - sqrt (Bval2 - 4 * Aval * Cval)) / (2 * Aval)"
          using insertion_p' aval0 h1
            discriminant_iff unfolding discrim_def by blast
        have p1 : "x = (- Bval + sqrt (Bval2 - 4 * Aval * Cval)) / (2 * Aval)  
                                                            ((a set L. eval (quadratic_sub var (-B) 1 (B^2-4*A*C) (2*A) a) (X[var := x]))
                                                      (a set F. eval (quadratic_sub_fm var (-B) 1 (B^2-4*A*C) (2*A) a) (X[var := x])))"
        proof-
          assume x_def : "x = (- Bval + sqrt (Bval2 - 4 * Aval * Cval)) / (2 * Aval)"
          then have h : "(aset L. aEval a (X[var := (- Bval + sqrt (Bval2 - 4 * Aval * Cval)) / (2 * Aval)]))  (fset F. eval f (X[var := (- Bval + sqrt (Bval2 - 4 * Aval * Cval)) / (2 * Aval)]))"
            using h
            using X_def hinsert by auto
          { fix a
            assume in_list : "a set L"
            have "eval (quadratic_sub var (- B) 1 (B2 - 4 * A * C) (2 * A) a) (X[var := x])"
              using free_in_quad[where a="-B",where b="1", where c="(B^2-4*A*C)", where d="2*A",where var="var",OF h1a h1b h1e h1g]
              using quadratic_sub[where a="-B",where b="1", where c="(B^2-4*A*C)", where d="2*A",where var="var", where L="X", OF Xlength,
                  where Dv="2*Aval", OF h2, where Cv="(Bval^2-4*Aval*Cval)", OF h3, where Av="-Bval", OF h4 h5, where Bv="1", OF h6 h7 h8]
                  h in_list
              using var_not_in_eval by fastforce 

          }
          then have left : "(aset L. eval (quadratic_sub var (- B) 1 (B2 - 4 * A * C) (2 * A) a) (X[var := x]))"
            by simp


          { fix a
            assume in_list : "a set F"
            have "eval (quadratic_sub_fm var (- B) 1 (B2 - 4 * A * C) (2 * A) a) (X[var := x])"
              using free_in_quad_fm[where a="-B",where b="1", where c="(B^2-4*A*C)", where d="2*A",where var="var",OF h1a h1b h1e h1g]
              using quadratic_sub_fm[where a="-B",where b="1", where c="(B^2-4*A*C)", where d="2*A",where var="var", where L="X", OF Xlength,
                  where Dv="2*Aval", OF h2, where Cv="(Bval^2-4*Aval*Cval)", OF h3, where Av="-Bval", OF h4 h5, where Bv="1", OF h6 h7 h8]
                  h in_list
              using var_not_in_eval by fastforce 

          }
          then have right : "(aset F. eval (quadratic_sub_fm var (- B) 1 (B2 - 4 * A * C) (2 * A) a) (X[var := x]))"
            by simp
          show ?thesis
            using right left by simp
        qed

        have p2 : "x = (- Bval - sqrt (Bval2 - 4 * Aval * Cval)) / (2 * Aval)  
                                                            ((a set L. eval (quadratic_sub var (-B) (-1) (B^2-4*A*C) (2*A) a) (X[var := x]))
                                                      (a set F. eval (quadratic_sub_fm var (-B) (-1) (B^2-4*A*C) (2*A) a) (X[var := x])))"
        proof -
          assume x_def : "x = (- Bval - sqrt (Bval2 - 4 * Aval * Cval)) / (2 * Aval)"
          then have h : "(aset L. aEval a (X[var := (- Bval - sqrt (Bval2 - 4 * Aval * Cval)) / (2 * Aval)]))  (fset F. eval f (X[var := (- Bval - sqrt (Bval2 - 4 * Aval * Cval)) / (2 * Aval)]))"
            using h
            using X_def hinsert by auto
          then have "(aset L. aEval a (X[var := (- Bval - sqrt (Bval2 - 4 * Aval * Cval)) / (2 * Aval)]))  (fset F. eval f (X[var := (- Bval - sqrt (Bval2 - 4 * Aval * Cval)) / (2 * Aval)]))"
            using h  by simp
          { fix a
            assume in_list : "a set L"
            have "eval (quadratic_sub var (- B) (-1) (B2 - 4 * A * C) (2 * A) a) (X[var := x])"
              using free_in_quad[where a="-B",where b="-1", where c="(B^2-4*A*C)", where d="2*A",where var="var",OF h1a h1c h1e h1g]
              using quadratic_sub[where a="-B",where b="-1", where c="(B^2-4*A*C)", where d="2*A",where var="var", where L="X", OF Xlength,
                  where Dv="2*Aval", OF h2, where Cv="(Bval^2-4*Aval*Cval)", OF h3, where Av="-Bval", OF h4 h5, where Bv="-1", OF h6a h7 h8]
                  h in_list
              using var_not_in_eval by fastforce 

          }
          then have left : "(aset L. eval (quadratic_sub var (- B) (-1) (B2 - 4 * A * C) (2 * A) a) (X[var := x]))"
            by simp


          { fix a
            assume in_list : "a set F"
            have "eval (quadratic_sub_fm var (- B) (-1) (B2 - 4 * A * C) (2 * A) a) (X[var := x])"
              using free_in_quad_fm[where a="-B",where b="-1", where c="(B^2-4*A*C)", where d="2*A",where var="var",OF h1a h1c h1e h1g]
              using quadratic_sub_fm[where a="-B",where b="-1", where c="(B^2-4*A*C)", where d="2*A",where var="var", where L="X", OF Xlength,
                  where Dv="2*Aval", OF h2, where Cv="(Bval^2-4*Aval*Cval)", OF h3, where Av="-Bval", OF h4 h5, where Bv="-1", OF h6a h7 h8]
                  h in_list
              using var_not_in_eval by fastforce 

          }
          then have right : "(aset F. eval (quadratic_sub_fm var (- B) (-1) (B2 - 4 * A * C) (2 * A) a) (X[var := x]))"
            by simp
          show ?thesis
            using right left by simp
        qed
        have subst4 : "insertion (nth_default 0 (xs @ x # Γ)) 4 = 4" using h7a hlength X_def by auto 
        have disj: "(aset L. eval (quadratic_sub var (- B) 1 (B2 - 4 * A * C) (2 * A) a) (xs @ x # Γ)) 
                                                            (aset F. eval (quadratic_sub_fm var (- B) 1 (B2 - 4 * A * C) (2 * A) a) (xs @ x # Γ))  
                                                            (aset L. eval (quadratic_sub var (- B) (-1) (B2 - 4 * A * C) (2 * A) a) (xs @ x # Γ)) 
                                                            (aset F. eval (quadratic_sub_fm var (- B) (-1) (B2 - 4 * A * C) (2 * A) a) (xs @ x # Γ))"
          using xh p1 p2
          unfolding X_def hinsert  by blast
        show ?thesis apply(simp add: aval0 True h7a subst4) using disj
          unfolding X_def hinsert by auto
      next
        case False
        then have det : "0 < - Bval2 + 4 * Aval * Cval"
          by simp
        show ?thesis apply(simp add: aval0 False h4) using discriminant_negative unfolding discrim_def
          using insertion_p'
          using aval0 det by auto 
      qed
    qed
    have "(x.
       (insertion (nth_default 0 (xs @ x # Γ)) A = 0 
        insertion (nth_default 0 (xs @ x # Γ)) B  0 
        (fset L. aEval (linear_substitution var (-C) (B) f) (xs @ x # Γ))  
        (fset F. eval (linear_substitution_fm var (-C) B f) (xs @ x # Γ)) 
        insertion (nth_default 0 (xs @ x # Γ)) A  0 
        insertion (nth_default 0 (xs @ x # Γ)) 4 * 
        insertion (nth_default 0 (xs @ x # Γ)) A *
        insertion (nth_default 0 (xs @ x # Γ)) C
         (insertion (nth_default 0 (xs @ x # Γ)) B)2 
        ((fset L. eval (quadratic_sub var (- B) 1 (B2 - 4 * A * C) (2 * A) f) (xs @ x # Γ))
         (fset F. eval (quadratic_sub_fm var (- B) 1 (B2 - 4 * A * C) (2 * A) f) (xs @ x # Γ)) 
         (fset L. eval (quadratic_sub var (- B) (-1) (B2 - 4 * A * C) (2 * A) f) (xs @ x # Γ)) 
         (fset F. eval (quadratic_sub_fm var (- B) (-1) (B2 - 4 * A * C) (2 * A) f) (xs @ x # Γ)))) 
        (Aval = 0 
        Bval = 0 
        Cval = 0))"
      apply(rule exI[where x=x])
      using biglemma
      using allAval allBval allCval unfolding A_def B_def C_def Aval_def Bval_def Cval_def X_def hinsert
      by auto
    then obtain x where x : "(insertion (nth_default 0 (xs @ x # Γ)) A = 0 
        insertion (nth_default 0 (xs @ x # Γ)) B  0 
        (fset L. aEval (linear_substitution var (-C) (B) f) (xs @ x # Γ))  
        (fset F. eval (linear_substitution_fm var (-C) B f) (xs @ x # Γ)) 
        insertion (nth_default 0 (xs @ x # Γ)) A  0 
        insertion (nth_default 0 (xs @ x # Γ)) 4 * 
        insertion (nth_default 0 (xs @ x # Γ)) A *
        insertion (nth_default 0 (xs @ x # Γ)) C
         (insertion (nth_default 0 (xs @ x # Γ)) B)2 
        ((fset L. eval (quadratic_sub var (- B) 1 (B2 - 4 * A * C) (2 * A) f) (xs @ x # Γ))
         (fset F. eval (quadratic_sub_fm var (- B) 1 (B2 - 4 * A * C) (2 * A) f) (xs @ x # Γ)) 
         (fset L. eval (quadratic_sub var (- B) (-1) (B2 - 4 * A * C) (2 * A) f) (xs @ x # Γ)) 
         (fset F. eval (quadratic_sub_fm var (- B) (-1) (B2 - 4 * A * C) (2 * A) f) (xs @ x # Γ)))) 
        (Aval = 0 
        Bval = 0 
        Cval = 0)" by auto
    have h : "(x. eval (elimVar var L F (Eq p)) (xs @ x # Γ))(Aval = 0  Bval = 0  Cval = 0)"
    proof(cases "(Aval = 0  Bval = 0  Cval = 0)")
      case True
      then show ?thesis by simp
    next
      case False
      have "(x. eval (elimVar var L F (Eq p)) (xs @ x # Γ))"
        apply(rule exI[where x=x])
        apply(simp add: eval_list_conj insertion_mult insertion_sub insertion_pow insertion_add 
            del:  quadratic_sub.simps linear_substitution.simps quadratic_sub_fm.simps linear_substitution_fm.simps)
        unfolding A_def[symmetric] B_def[symmetric] C_def[symmetric] One_nat_def[symmetric] X_def[symmetric]
        using hlength x
        by (auto simp add:False)
      then show ?thesis by auto
    qed
    have "(x. eval (elimVar var L F (Eq p)) (xs @ x # Γ))(x. aEval (Eq p) (xs@ x# Γ))"
    proof(cases "(x. eval (elimVar var L F (Eq p)) (xs @ x # Γ))")
      case True
      then show ?thesis by auto
    next
      case False
      then have "(Aval = 0  Bval = 0  Cval = 0)"
        using h by auto
      then have "(x. aEval (Eq p) (xs @ x # Γ))"
        unfolding express_p
        apply(simp add:insertion_add insertion_mult insertion_pow)
        using allAval allBval allCval by auto 
      then show ?thesis by auto
    qed
  }
  then have left : "(x. eval (list_conj (map fm.Atom L @ F)) (xs @ x # Γ)) 
                        ((x. eval (elimVar var L F (Eq p)) (xs @ x # Γ))(x. aEval (Eq p) (xs@ x# Γ)))"
    by blast


  {
    assume hlength : "length (xs::real list) = var"
    define A where "A = (isolate_variable_sparse p var 2)"
    define B where "B = (isolate_variable_sparse p var 1)"
    define C where "C = (isolate_variable_sparse p var 0)"
    have freeA : "var  vars A"
      unfolding A_def
      by (simp add: not_in_isovarspar)
    have freeB : "var  vars B"
      unfolding B_def
      by (simp add: not_in_isovarspar)
    have freeC : "var  vars C"
      unfolding C_def
      by (simp add: not_in_isovarspar)
    have express_p : "p = A*(Var var)^2+B*(Var var)+C"
      using express_poly[OF low_pow] unfolding A_def B_def C_def
      by fastforce
    assume h : "(x. (eval (elimVar var L F (Eq p)) (list_update (xs@x#Γ) var x)))"
    fix x
    define X where "X=xs@x#Γ"
    have Xlength : "length X > var"
      using X_def hlength by auto
    define Aval where "Aval = insertion (nth_default 0 (list_update X var x)) A"
    define Bval where "Bval = insertion (nth_default 0 (list_update X var x)) B"
    define Cval where "Cval = insertion (nth_default 0 (list_update X var x)) C"
    have allAval : "x. insertion (nth_default 0 (list_update X var x)) A = Aval"
      using freeA Aval_def
      using not_contains_insertion by blast
    have allBval : "x. insertion (nth_default 0 (list_update X var x)) B = Bval"
      using freeB Bval_def
      using not_contains_insertion by blast
    have allCval : "x. insertion (nth_default 0 (list_update X var x)) C = Cval"
      using freeC Cval_def
      using not_contains_insertion by blast
    assume "(eval (elimVar var L F (Eq p)) (list_update (xs@x#Γ) var x))"
    then have h : "(eval (elimVar var L F (Eq p)) (list_update X var x))"
      unfolding X_def .

    have "(Aval = 0  Bval  0 
          (f(λa. Atom(linear_substitution var (-C) B a)) ` set L 
             linear_substitution_fm var (-C) B `
             set F.
            eval f (X[var := x])) 
          Aval  0 
          insertion (nth_default 0 (X[var := x])) 4 * Aval * Cval   Bval2 
          ((f(quadratic_sub var (-B) 1 (B^2-4*A*C) (2*A)) `
             set L 
             (quadratic_sub_fm var (-B) 1 (B^2-4*A*C) (2*A)) `
             set F.
            eval f (X[var := x]))
          (f(quadratic_sub var (-B) (-1) (B^2-4*A*C) (2*A)) `
             set L 
             (quadratic_sub_fm var (-B) (-1) (B^2-4*A*C) (2*A)) `
             set F.
            eval f (X[var := x]))
          ))"
      unfolding Aval_def Bval_def Cval_def A_def B_def C_def
      using h by(simp add: eval_list_conj insertion_mult insertion_sub insertion_pow insertion_add insertion_var Xlength)
    then have h : "(Aval = 0  Bval  0 
                            ((a set L. aEval (linear_substitution var (-C) B a) (X[var := x])) 
                            (a set F. eval (linear_substitution_fm var (-C) B a) (X[var := x]))) 
                            Aval  0  insertion (nth_default 0 (X[var := x])) 4 * Aval * Cval  Bval2 
                            (((a set L. eval (quadratic_sub var (-B) 1 (B^2-4*A*C) (2*A) a) (X[var := x]))
                            (a set F. eval (quadratic_sub_fm var (-B) 1 (B^2-4*A*C) (2*A) a) (X[var := x])))
                            ((a set L. eval (quadratic_sub var (-B) (-1) (B^2-4*A*C) (2*A) a) (X[var := x]))
                            (a set F. eval (quadratic_sub_fm var (-B) (-1) (B^2-4*A*C) (2*A) a) (X[var := x])))))
                          "
      apply(cases "Aval = 0 ")
      apply auto
      by (meson Un_iff eval.simps(1) imageI)
    have h : "(x. ((aset L . aEval a ((xs@x#Γ)[var := x]))  (fset F. eval f ((xs@x#Γ)[var := x]))))(Aval=0Bval=0Cval=0)"
    proof(cases "Aval=0")
      case True
      then have aval0 : "Aval=0"
        by simp
      show ?thesis proof(cases "Bval = 0")
        case True
        then have bval0 : "Bval = 0" by simp
        show ?thesis proof(cases "Cval=0")
          case True
          then show ?thesis using aval0 bval0 True by auto
        next
          case False
          then show ?thesis using h by(simp add:aval0 bval0 False)
        qed 
      next
        case False
        have hb :  "insertion (nth_default 0 (X[var := - Cval / Bval])) B = Bval"
          using allBval by simp
        have hc : "insertion (nth_default 0 (X[var := - Cval / Bval])) (-C) = -Cval"
          using allCval
          by (simp add: insertion_neg) 
        have freecneg : "varvars(-C)" using freeC not_in_neg by auto
        have p1 : "(aset L. aEval a ((xs @ x # Γ)[var := - Cval / Bval]))"
          using h apply(simp add: False aval0)
          using linear[OF Xlength False freecneg freeB hc hb]
            list_update_length var_not_in_linear[OF freecneg freeB]
          unfolding X_def using hlength
          by (metis divide_minus_left)

        have p2 : "(aset F. eval a ((xs @ x # Γ)[var := - Cval / Bval]))"
          using h apply(simp add: False aval0)
          using linear_fm[OF Xlength False freecneg freeB hc hb]
            list_update_length var_not_in_linear_fm[OF freecneg freeB]
          unfolding X_def using hlength var_not_in_eval
          by (metis divide_minus_left linear_substitution_fm.elims linear_substitution_fm_helper.elims)
        show ?thesis 
          using p1 p2 hlength by fastforce
      qed
    next
      case False
      then have aval0 : "Aval  0"
        by simp
      have h4 : "insertion (nth_default 0 (X[var := x])) 4 = 4"
        using insertion_const[where f = "(nth_default 0 (X[var := x]))", where c="4"]
        by (metis MPoly_Type.insertion_one insertion_add numeral_Bit0 one_add_one)
      show ?thesis proof(cases "4 * Aval * Cval  Bval2")
        case True
        then have h1 :  "- Bval2 + 4 * Aval * Cval  0"
          by simp
        have h : "(((a set L. eval (quadratic_sub var (-B) 1 (B^2-4*A*C) (2*A) a) (X[var := x]))
                        (a set F. eval (quadratic_sub_fm var (-B) 1 (B^2-4*A*C) (2*A) a) (X[var := x])))
                        ((a set L. eval (quadratic_sub var (-B) (-1) (B^2-4*A*C) (2*A) a) (X[var := x]))
                        (a set F. eval (quadratic_sub_fm var (-B) (-1) (B^2-4*A*C) (2*A) a) (X[var := x]))))"
          using h by(simp add: h1 aval0)
        have h1a : "varvars(-B)"
          by(simp add: freeB not_in_neg)
        have h1b : "varvars(1::real mpoly)"
          using isolate_var_one not_in_isovarspar by blast
        have h1c : "varvars(-1::real mpoly)"
          by(simp add: h1b not_in_neg)
        have h1d : "varvars(4::real mpoly)"
          by (metis h1b not_in_add numeral_Bit0 one_add_one)
        have h1e : "varvars(B^2-4*A*C)" 
          by(simp add: freeB h1d freeA freeC not_in_mult not_in_pow not_in_sub)
        have h1f : "varvars(2::real mpoly)"
          using h1b not_in_add by fastforce
        have h1g : "varvars(2*A)"
          by(simp add: freeA h1f not_in_mult)
        have h1h : "freeIn var (quadratic_sub var (-B) (1) (B^2-4*A*C) (2*A) a)"
          using free_in_quad h1a h1b h1e h1g by blast
        have h1i : "freeIn var (quadratic_sub var (-B) (-1) (B^2-4*A*C) (2*A) a)"
          using free_in_quad h1a h1c h1e h1g by blast 
        have h2 : "2*Aval  0" using aval0 by auto
        have h3 : "0  (Bval^2-4*Aval*Cval)" using True by auto
        have h4a : "var  vars 4"
          by (metis monom_numeral notInKeys_notInVars not_in_add not_in_isovarspar not_in_pow one_add_one power.simps(1) rel_simps(76) vars_monom_keys) 
        have h4 : "var  vars (B^2-4*A*C)" by(simp add: h4a freeA freeB freeC not_in_pow not_in_mult not_in_sub)  
        have h5 : "x. insertion (nth_default 0 (list_update X var x)) (-B) = -Bval " using allBval by(simp add: insertion_neg)
        have h6 : "x. insertion (nth_default 0 (list_update X var x)) 1 = 1" by simp
        have h6a : "x. insertion (nth_default 0 (list_update X var x)) (-1) = (-1)" using h6 by (simp add: insertion_neg) 
        have h7a : "x. insertion (nth_default 0 (list_update X var x)) 4 = 4" by (metis h6 insertion_add numeral_Bit0 one_add_one)
        have h7b : "var  vars(4*A*C)" using freeA freeC by (simp add: h4a not_in_mult) 
        have h7c : "var  vars(B^2)" using freeB not_in_pow by auto
        have h7 : "x. insertion (nth_default 0 (list_update X var x)) (B^2-4*A*C) = (Bval^2-4*Aval*Cval)"
          by (simp add: h7a allAval allBval allCval insertion_mult insertion_sub power2_eq_square)
        have h8a : "x. insertion (nth_default 0 (list_update X var x)) 2 = 2" by (metis h6 insertion_add one_add_one)
        have h8 : "x. insertion (nth_default 0 (list_update X var x)) (2*A) = (2*Aval)" by(simp add: allAval h8a insertion_mult)

        have p1 : "(a set L. eval (quadratic_sub var (-B) 1 (B^2-4*A*C) (2*A) a) (X[var := x]))
                        (a set F. eval (quadratic_sub_fm var (-B) 1 (B^2-4*A*C) (2*A) a) (X[var := x]))
                           x. length xs = var  ((aset L . aEval a ((xs@x#Γ)[var := x]))  (fset F. eval f ((xs@x#Γ)[var := x])))"
        proof-
          assume p1 : "(a set L. eval (quadratic_sub var (-B) 1 (B^2-4*A*C) (2*A) a) (X[var := x]))"
          assume p2 : "(a set F. eval (quadratic_sub_fm var (-B) 1 (B^2-4*A*C) (2*A) a) (X[var := x]))"
          show ?thesis
            using free_in_quad[where a="-B",where b="1", where c="(B^2-4*A*C)", where d="2*A",where var="var",OF h1a h1b h1e h1g]
            using quadratic_sub[where a="-B",where b="1", where c="(B^2-4*A*C)", where d="2*A",where var="var", where L="X", OF Xlength,
                where Dv="2*Aval", OF h2, where Cv="(Bval^2-4*Aval*Cval)", OF h3, where Av="-Bval", OF h4 h5, where Bv="1", OF h6 h7 h8]
            using free_in_quad_fm[where a="-B",where b="1", where c="(B^2-4*A*C)", where d="2*A",where var="var",OF h1a h1b h1e h1g]
            using quadratic_sub_fm[where a="-B",where b="1", where c="(B^2-4*A*C)", where d="2*A",where var="var", where L="X", OF Xlength,
                where Dv="2*Aval", OF h2, where Cv="(Bval^2-4*Aval*Cval)", OF h3, where Av="-Bval", OF h4 h5, where Bv="1", OF h6 h7 h8]
                p1 p2
            using var_not_in_eval
            by (metis X_def hlength list_update_length)
        qed
        have p2 : "(a set L. eval (quadratic_sub var (-B) (-1) (B^2-4*A*C) (2*A) a) (X[var := x]))
                        (a set F. eval (quadratic_sub_fm var (-B) (-1) (B^2-4*A*C) (2*A) a) (X[var := x]))
                          x. length xs = var  ((aset L . aEval a ((xs@x#Γ)[var := x]))  (fset F. eval f ((xs@x#Γ)[var := x])))"
          using free_in_quad[where a="-B",where b="-1", where c="(B^2-4*A*C)", where d="2*A",where var="var",OF h1a h1c h1e h1g]
          using quadratic_sub[where a="-B",where b="-1", where c="(B^2-4*A*C)", where d="2*A",where var="var", where L="X", OF Xlength,
              where Dv="2*Aval", OF h2, where Cv="(Bval^2-4*Aval*Cval)", OF h3, where Av="-Bval", OF h4 h5, where Bv="-1", OF h6a h7 h8]

          using free_in_quad_fm[where a="-B",where b="-1", where c="(B^2-4*A*C)", where d="2*A",where var="var",OF h1a h1c h1e h1g]
          using quadratic_sub_fm[where a="-B",where b="-1", where c="(B^2-4*A*C)", where d="2*A",where var="var", where L="X", OF Xlength,
              where Dv="2*Aval", OF h2, where Cv="(Bval^2-4*Aval*Cval)", OF h3, where Av="-Bval", OF h4 h5, where Bv="-1", OF h6a h7 h8]

          using var_not_in_eval by (metis X_def hlength list_update_length)
        then show ?thesis
          using h p1 p2 by blast
      next
        case False
        then show ?thesis using h by(simp add: aval0 False h4)
      qed
    qed
    have "(x.((aset L . aEval a ((xs@x#Γ)[var := x]))  (fset F. eval f ((xs@x#Γ)[var := x]))))(x. aEval (Eq p) (xs @ x#Γ))"
    proof(cases "(x.((aset L . aEval a ((xs@x#Γ)[var := x]))  (fset F. eval f ((xs@x#Γ)[var := x]))))")
      case True
      then show ?thesis by auto
    next
      case False
      then have "Aval=0Bval=0Cval=0" using h by auto
      then have "(x. aEval (Eq p) (xs @ x # Γ))"
        unfolding express_p apply(simp add:insertion_add insertion_mult insertion_pow)
        using allAval allBval allCval hlength unfolding X_def by auto
      then show ?thesis by auto
    qed
  }


  then have right : "(x. eval (elimVar var L F (Eq p)) (xs @ x # Γ)) 
               ((x. eval (list_conj (map fm.Atom L @ F)) (xs @ x # Γ))(x. aEval (Eq p) (xs @ x # Γ)))"
    by (smt UnE eval.simps(1) eval_list_conj hlength imageE list_update_length set_append set_map)


  show ?thesis using right left by blast
qed

text "simply states that the variable is free in the equality case of the elimVar function"
lemma freeIn_elimVar_eq : "freeIn var (elimVar var L F (Eq p))"
proof-
  have h4 : "var  vars(4:: real mpoly)" using var_not_in_Const
    by (metis (full_types) isolate_var_one monom_numeral not_in_isovarspar numeral_One vars_monom_keys zero_neq_numeral)
  have hlinear: "fset(map (λa. Atom(linear_substitution var (-isolate_variable_sparse p var 0) (isolate_variable_sparse p var (Suc 0)) a)) L @
        map (linear_substitution_fm var (-isolate_variable_sparse p var 0) (isolate_variable_sparse p var (Suc 0)))
         F). freeIn var f" 
    using
      var_not_in_linear[where c="(isolate_variable_sparse p var (Suc 0))", where b="(- isolate_variable_sparse p var 0)", where var="var"]
      var_not_in_linear_fm[where c="(isolate_variable_sparse p var (Suc 0))", where b="(-isolate_variable_sparse p var 0)", where var="var"]
      not_in_isovarspar not_in_neg by auto
  have freeA : "var  vars (- isolate_variable_sparse p var (Suc 0))"
    using not_in_isovarspar not_in_neg by auto
  have freeB1 : "var  vars (1::real mpoly)"
    by (metis h4 monom_numeral monom_one notInKeys_notInVars vars_monom_keys zero_neq_numeral)
  have freeC : "var  vars (((isolate_variable_sparse p var (Suc 0))2 -
                    4 * isolate_variable_sparse p var 2 * isolate_variable_sparse p var 0))"
    using not_in_isovarspar not_in_pow not_in_sub not_in_mult h4 by auto
  have freeD : "var  vars ((2 * isolate_variable_sparse p var 2))"
    using not_in_isovarspar not_in_mult
    by (metis mult_2 not_in_add) 
  have freeB2 : "varvars (-1::real mpoly)"
    using freeB1 not_in_neg by auto
  have quadratic1 : "fset(map (quadratic_sub var (- isolate_variable_sparse p var (Suc 0)) 1
              ((isolate_variable_sparse p var (Suc 0))2 -
               4 * isolate_variable_sparse p var 2 * isolate_variable_sparse p var 0)
              (2 * isolate_variable_sparse p var 2))
         L @
        map (quadratic_sub_fm var (- isolate_variable_sparse p var (Suc 0)) 1
              ((isolate_variable_sparse p var (Suc 0))2 -
               4 * isolate_variable_sparse p var 2 * isolate_variable_sparse p var 0)
              (2 * isolate_variable_sparse p var 2))
         F). freeIn var f" 
    using free_in_quad[OF freeA freeB1 freeC freeD]
      free_in_quad_fm[OF freeA freeB1 freeC freeD] by auto
  have quadratic2 : "fset(map (quadratic_sub var (- isolate_variable_sparse p var (Suc 0)) (-1)
              ((isolate_variable_sparse p var (Suc 0))2 -
               4 * isolate_variable_sparse p var 2 * isolate_variable_sparse p var 0)
              (2 * isolate_variable_sparse p var 2))
         L @
        map (quadratic_sub_fm var (- isolate_variable_sparse p var (Suc 0)) (-1)
              ((isolate_variable_sparse p var (Suc 0))2 -
               4 * isolate_variable_sparse p var 2 * isolate_variable_sparse p var 0)
              (2 * isolate_variable_sparse p var 2))
         F). freeIn var f"
    using free_in_quad[OF freeA freeB2 freeC freeD]
      free_in_quad_fm[OF freeA freeB2 freeC freeD] by auto
  show ?thesis
    using not_in_mult not_in_add h4 not_in_pow not_in_sub freeIn_list_conj not_in_isovarspar hlinear quadratic1 quadratic2
    by simp
qed


text "Theorem 20.2 in the textbook"
lemma elimVar_eq_2 :
  assumes hlength : "length xs = var"
  assumes in_list : "Eq p  set(L)"
  assumes low_pow : "MPoly_Type.degree p var = 1  MPoly_Type.degree p var = 2"
  assumes nonzero : "x. 
              insertion (nth_default 0 (xs @ x # Γ)) (isolate_variable_sparse p var 2)  0
             insertion (nth_default 0 (xs @ x # Γ)) (isolate_variable_sparse p var 1)  0
             insertion (nth_default 0 (xs @ x # Γ)) (isolate_variable_sparse p var 0)  0" (is ?non0)
  shows "(x. eval (list_conj (map fm.Atom L @ F)) (xs @ x # Γ)) =
         (x. eval (elimVar var L F (Eq p)) (xs @ x # Γ))"
proof-
  define A where "A = (isolate_variable_sparse p var 2)"
  define B where "B = (isolate_variable_sparse p var 1)"
  define C where "C = (isolate_variable_sparse p var 0)"
  have freeA : "var  vars A"
    unfolding A_def
    by (simp add: not_in_isovarspar)
  have freeB : "var  vars B"
    unfolding B_def
    by (simp add: not_in_isovarspar)
  have freeC : "var  vars C"
    unfolding C_def
    by (simp add: not_in_isovarspar)
  have express_p : "p = A*(Var var)^2+B*(Var var)+C"
    using express_poly[OF low_pow] unfolding A_def B_def C_def
    by fastforce
  have af : "isolate_variable_sparse p var 2 = A"
    using A_def by auto
  have bf : "isolate_variable_sparse p var (Suc 0) = B"
    using B_def by auto
  have cf : "isolate_variable_sparse p var 0 = C"
    using C_def by auto
  have xlength : "x. (insertion (nth_default 0 (xs @ x # Γ)) (Var var))= x" 
    using hlength insertion_var
    by (metis add.commute add_strict_increasing length_append length_greater_0_conv list.distinct(1) list_update_id nth_append_length order_refl)
  fix x
  define c where "c i = (insertion (nth_default 0 (xs @ x # Γ)) (isolate_variable_sparse p var i))" for i
  have c2 : "x. insertion (nth_default 0 (xs @ x # Γ)) A = c 2" 
    using freeA apply(simp add: A_def c_def)
    by (simp add: hlength insertion_lowerPoly1)
  have c1 : "x. insertion (nth_default 0 (xs @ x # Γ)) B = c 1"
    using freeB apply(simp add: B_def c_def)
    by (simp add: hlength insertion_lowerPoly1)
  have c0 : "x. insertion (nth_default 0 (xs @ x # Γ)) C = c 0"
    using freeC apply(simp add: C_def c_def)
    by (simp add: hlength insertion_lowerPoly1)
  have sum : "x. c 2 * x2 + c (Suc 0) * x + c 0 = (i2. c i * x ^ i)"
    by (simp add: numerals(2))
  have "(x. aEval (Eq p) (xs @ x # Γ)) = (¬?non0)"
    apply(simp add : af bf cf)
    unfolding express_p apply(simp add:insertion_add insertion_mult insertion_pow xlength)
    apply(simp add:c2 c1 c0)
    apply(simp add: sum)
    using polyfun_eq_0[where c="c", where n="2"]
    using sum by auto
  then have "¬(x. aEval (Eq p) (xs @ x Γ))"
    using nonzero by auto
  then show ?thesis
    using disjE[OF elimVar_eq[OF hlength in_list, where F="F", where Γ="Γ"], where R="?thesis"]
    using (x. aEval (Eq p) (xs @ x # Γ)) = (¬ (x. insertion (nth_default 0 (xs @ x # Γ)) (isolate_variable_sparse p var 2)  0  insertion (nth_default 0 (xs @ x # Γ)) (isolate_variable_sparse p var 1)  0  insertion (nth_default 0 (xs @ x # Γ)) (isolate_variable_sparse p var 0)  0)) low_pow nonzero by blast
qed



end