Theory Virtual_Substitution.OptimizationProofs

subsection "Optimization Proofs"
theory OptimizationProofs
  imports Optimizations
begin

lemma neg_nnf : "∀Γ. (¬ eval (nnf (Neg φ)) Γ) = eval (nnf φ) Γ"
  apply(induction φ)
           apply(simp_all)
  using aNeg_aEval apply blast
  using aNeg_aEval by blast

theorem eval_nnf : "∀Γ. eval φ Γ = eval (nnf φ) Γ"
  apply(induction φ)apply(simp_all) using neg_nnf by blast


theorem negation_free_nnf : "negation_free (nnf φ)"
proof(induction "depth φ" arbitrary : φ rule: nat_less_induct )
  case 1
  then show ?case
  proof(induction φ)
    case (And φ1 φ2)
    then show ?case apply simp
      by (metis less_Suc_eq_le max.cobounded1 max.cobounded2)
  next
    case (Or φ1 φ2)
    then show ?case apply simp
      by (metis less_Suc_eq_le max.cobounded1 max.cobounded2)
  next
    case (Neg φ)
    then show ?case proof (induction φ)
      case (And φ1 φ2)
      then show ?case apply simp
        by (metis less_Suc_eq max_less_iff_conj not_less_eq)
    next
      case (Or φ1 φ2)
      then show ?case apply simp
        by (metis less_Suc_eq max_less_iff_conj not_less_eq)
    next
      case (Neg φ)
      then show ?case
        by (metis Suc_eq_plus1 add_lessD1 depth.simps(6) lessI nnf.simps(12))
    qed auto
  qed auto
qed


lemma groupQuantifiers_eval : "eval F L = eval (groupQuantifiers F) L"
  apply(induction F arbitrary: L  rule:groupQuantifiers.induct) 
  unfolding doubleExist unwrapExist unwrapExist' unwrapExist'' doubleForall unwrapForall unwrapForall' unwrapForall''
  apply (auto)
  using doubleExist doubleExist unwrapExist unwrapExist' unwrapExist'' doubleForall unwrapForall unwrapForall' unwrapForall''  apply auto
  by metis+


theorem simp_atom_eval : "aEval a xs = eval (simp_atom a) xs"
proof(cases a)
  case (Less p)
  then show ?thesis by(cases "get_if_const p")(simp_all add:get_if_const_insertion)
next
  case (Eq p)
  then show ?thesis by(cases "get_if_const p")(simp_all add:get_if_const_insertion)
next
  case (Leq p)
  then show ?thesis by(cases "get_if_const p")(simp_all add:get_if_const_insertion)
next
  case (Neq p)
  then show ?thesis by(cases "get_if_const p")(simp_all add:get_if_const_insertion)
qed

lemma simpfm_eval : "∀L. eval φ L = eval (simpfm φ) L"
  apply(induction φ)
  apply(simp_all add: simp_atom_eval eval_and eval_or)
  using eval_neg by blast

lemma exQ_clearQuantifiers:
  assumes ExQ : "⋀xs. eval (clearQuantifiers φ) xs = eval φ xs"
  shows "eval (clearQuantifiers (ExQ φ)) xs = eval (ExQ φ) xs"
proof-
  define φ' where "φ' = clearQuantifiers φ"
  have h : "freeIn 0 φ' ⟹ (eval (lowerFm 0 1 φ') xs = eval (ExQ φ') xs)"
    using eval_lowerFm by simp
  have "eval (clearQuantifiers (ExQ φ)) xs = 
      eval (if freeIn 0 φ' then lowerFm 0 1 φ' else ExQ φ') xs"
    using φ'_def by simp
  also have "... = eval (ExQ φ) xs"
    apply(cases "freeIn 0 φ'")
    using h ExQ φ'_def by(simp_all)
  finally show ?thesis
    by simp
qed

lemma allQ_clearQuantifiers :
  assumes AllQ : "⋀xs. eval (clearQuantifiers φ) xs = eval φ xs"
  shows "eval (clearQuantifiers (AllQ φ)) xs = eval (AllQ φ) xs"
proof-
  define φ' where "φ' = clearQuantifiers φ"
  have "freeIn 0 φ' ⟹ (eval (ExQ φ') xs) = eval (AllQ φ') xs"
    by (simp add: var_not_in_eval2)
  then have h : "freeIn 0 φ' ⟹ (eval (lowerFm 0 1 φ') xs = eval (AllQ φ') xs)"
    using eval_lowerFm by simp
  have "eval (clearQuantifiers (AllQ φ)) xs = 
      eval (if freeIn 0 φ' then lowerFm 0 1 φ' else AllQ φ') xs"
    using φ'_def by simp
  also have "... = eval (AllQ φ) xs"
    apply(cases "freeIn 0 φ'")
    using h AllQ φ'_def by(simp_all)
  finally show ?thesis 
    by simp
qed

lemma clearQuantifiers_eval : "eval (clearQuantifiers φ) xs = eval φ xs"
proof(induction φ arbitrary : xs)
  case (Atom x)
  then show ?case using simp_atom_eval by simp
next
  case (And φ1 φ2)
  then show ?case using eval_and by simp
next
  case (Or φ1 φ2)
  then show ?case using eval_or by simp
next
  case (Neg φ)
  then show ?case using eval_neg by auto
next
  case (ExQ φ)
  then show ?case using exQ_clearQuantifiers by simp
next
  case (AllQ φ)
  then show ?case using allQ_clearQuantifiers by simp
next
  case (ExN x1 φ)
  then show ?case proof(induction x1 arbitrary:φ)
    case 0
    then show ?case by auto
  next
    case (Suc x1)
    show ?case
      using Suc(1)[of "ExQ φ", OF exQ_clearQuantifiers[OF Suc(2)]]
      apply simp
      using Suc_eq_plus1 ‹eval (clearQuantifiers (ExN x1 (ExQ φ))) xs = eval (ExN x1 (ExQ φ)) xs› eval.simps(10) unwrapExist' by presburger
  qed
next
  case (AllN x1 φ)
  then show ?case proof(induction x1 arbitrary:φ)
    case 0
    then show ?case by auto
  next
    case (Suc x1)
    show ?case
      using Suc(1)[of "AllQ φ", OF allQ_clearQuantifiers[OF Suc(2)]]
      apply simp
      using unwrapForall' by force
  qed
qed auto

lemma  push_forall_eval_AllQ : "∀xs. eval (AllQ φ) xs = eval (push_forall (AllQ φ)) xs"
proof(induction φ)
  case TrueF
  then show ?case by simp
next
  case FalseF
  then show ?case by simp
next
  case (Atom x)
  then show ?case
    using aEval_lowerAtom eval.simps(1) eval.simps(8) push_forall.simps(11) by presburger
next
  case (And φ1 φ2)
  {fix xs
    have "eval (AllQ (And φ1 φ2)) xs = (∀x. eval φ1 (x#xs) ∧ eval φ2 (x#xs))"
      by simp
    also have "... = ((∀x. eval φ1 (x#xs)) ∧ (∀x. eval φ2 (x#xs)))"
      by blast
    also have "... = eval (push_forall (AllQ (And φ1 φ2))) xs"
      using And eval_and by(simp)
    finally have "eval (AllQ (And φ1 φ2)) xs = eval (push_forall (AllQ (And φ1 φ2))) xs"
      by simp
  }
  then show ?case by simp 
next
  case (Or φ1 φ2)
  then show ?case proof(cases "freeIn 0 φ1")
    case True
    then have h : "freeIn 0 φ1"
      by simp
    then show ?thesis proof(cases "freeIn 0 φ2")
      case True
      {fix xs
        have "∃x. eval φ1 (x # xs) = eval (lowerFm 0 1 φ1) xs"
          using eval_lowerFm h eval.simps(7) by blast 
        then have h1 : "∀x. eval φ1 (x # xs) = eval (lowerFm 0 1 φ1) xs"
          using h var_not_in_eval2 by blast
        have "∃x. eval φ2 (x # xs) = eval (lowerFm 0 1 φ2) xs"
          using eval_lowerFm True eval.simps(7) by blast 
        then have h2 : "∀x. eval φ2 (x # xs) = eval (lowerFm 0 1 φ2) xs"
          using True var_not_in_eval2 by blast
        have "eval (AllQ (Or φ1 φ2)) xs = eval (push_forall (AllQ (Or φ1 φ2))) xs"
          by(simp add:h h1 h2 True eval_or)
      }
      then show ?thesis by simp
    next
      case False
      {fix xs
        have "∃x. eval φ1 (x # xs) = eval (lowerFm 0 1 φ1) xs"
          using eval_lowerFm h eval.simps(7) by blast 
        then have "∀x. eval φ1 (x # xs) = eval (lowerFm 0 1 φ1) xs"
          using True var_not_in_eval2 by blast
        then have "eval (AllQ (Or φ1 φ2)) xs = eval (push_forall (AllQ (Or φ1 φ2))) xs"
          by(simp add:h False eval_or)
      }
      then show ?thesis by simp
    qed
  next
    case False
    then have h : "¬freeIn 0 φ1"
      by simp
    then show ?thesis proof(cases "freeIn 0 φ2")
      case True
      {fix xs
        have "∃x. eval φ2 (x # xs) = eval (lowerFm 0 1 φ2) xs"
          using eval_lowerFm True eval.simps(7) by blast 
        then have "∀x. eval φ2 (x # xs) = eval (lowerFm 0 1 φ2) xs"
          using True var_not_in_eval2 by blast
        then have "eval (AllQ (Or φ1 φ2)) xs = eval (push_forall (AllQ (Or φ1 φ2))) xs"
          by(simp add:h True eval_or)
      }
      then show ?thesis by simp
    next
      case False
      then show ?thesis by(simp add:h False eval_or)
    qed
  qed
next
  case (Neg φ)
  {fix xs
    have "freeIn 0 (Neg φ) ⟹ (eval (ExQ (Neg φ)) xs) = eval (AllQ (Neg φ)) xs"
      using var_not_in_eval2 eval.simps(7) eval.simps(8) by blast
    then have h : "freeIn 0 (Neg φ) ⟹ (eval (lowerFm 0 1 (Neg φ)) xs = eval (AllQ (Neg φ)) xs)"
      using eval_lowerFm by blast
    have "eval (push_forall (AllQ (Neg φ))) xs = 
      eval (if freeIn 0 (Neg φ) then lowerFm 0 1 (Neg φ) else AllQ (Neg φ)) xs"
      by simp
    also have "... = eval (AllQ (Neg φ)) xs"
      apply(cases "freeIn 0 (Neg φ)")
      using h  by(simp_all)
    finally have "eval (push_forall (AllQ (Neg φ))) xs = eval (AllQ (Neg φ)) xs"
      by simp
  }
  then show ?case by simp
next
  case (ExQ φ)
  {fix xs
    have "freeIn 0 (ExQ φ) ⟹ (eval (ExQ (ExQ φ)) xs) = eval (AllQ (ExQ φ)) xs"
      using var_not_in_eval2 eval.simps(7) eval.simps(8) by blast
    then have h : "freeIn 0 (ExQ φ) ⟹ (eval (lowerFm 0 1 (ExQ φ)) xs = eval (AllQ (ExQ φ)) xs)"
      using eval_lowerFm by blast
    have "eval (push_forall (AllQ (ExQ φ))) xs = 
      eval (if freeIn 0 (ExQ φ) then lowerFm 0 1 (ExQ φ) else AllQ (ExQ φ)) xs"
      by simp
    also have "... = eval (AllQ (ExQ φ)) xs"
      apply(cases "freeIn 0 (ExQ φ)")
      using h  by(simp_all)
    finally have "eval (push_forall (AllQ (ExQ φ))) xs = eval (AllQ (ExQ φ)) xs"
      by simp
  }
  then show ?case by simp
next
  case (AllQ φ)
  {fix xs
    have "freeIn 0 (AllQ φ) ⟹ (eval (ExQ (AllQ φ)) xs) = eval (AllQ (AllQ φ)) xs"
      using var_not_in_eval2 eval.simps(7) eval.simps(8) by blast
    then have h : "freeIn 0 (AllQ φ) ⟹ (eval (lowerFm 0 1 (AllQ φ)) xs = eval (AllQ (AllQ φ)) xs)"
      using eval_lowerFm by blast
    have "eval (push_forall (AllQ (AllQ φ))) xs = 
      eval (if freeIn 0 (AllQ φ) then lowerFm 0 1 (AllQ φ) else AllQ (AllQ φ)) xs"
      by simp
    also have "... = eval (AllQ (AllQ φ)) xs"
      apply(cases "freeIn 0 (AllQ φ)")
      using h AllQ  by(simp_all)
    finally have "eval (push_forall (AllQ (AllQ φ))) xs = eval (AllQ (AllQ φ)) xs"
      by simp
  }
  then show ?case by simp
next
  case (ExN x1 φ)
  then show ?case
    using eval.simps(7) eval.simps(8) eval_lowerFm push_forall.simps(17) var_not_in_eval2 by presburger
next
  case (AllN x1 φ)
  then show ?case
    using eval.simps(7) eval.simps(8) eval_lowerFm push_forall.simps(18) var_not_in_eval2 by presburger
qed

lemma push_forall_eval : "∀xs. eval φ xs = eval (push_forall φ) xs"
proof(induction φ)
  case (Atom x)
  then show ?case using simp_atom_eval by simp
next
  case (And φ1 φ2)
  then show ?case using eval_and by auto
next
  case (Or φ1 φ2)
  then show ?case using eval_or by auto
next
  case (Neg φ)
  then show ?case using eval_neg by auto
next
  case (AllQ φ)
  then show ?case using push_forall_eval_AllQ by blast 
next
  case (ExN x1 φ)
  then show ?case
    using eval.simps(10) push_forall.simps(7) by presburger
qed auto

lemma map_fm_binders_negation_free : 
  assumes "negation_free φ"
  shows "negation_free (map_fm_binders f φ n)"
  using assms apply(induction φ arbitrary : n) by auto

lemma negation_free_and : 
  assumes "negation_free φ"
  assumes "negation_free ψ"
  shows "negation_free (and φ ψ)"
  using assms unfolding and_def by simp 

lemma negation_free_or : 
  assumes "negation_free φ"
  assumes "negation_free ψ"
  shows "negation_free (or φ ψ)"
  using assms unfolding or_def by simp 

lemma push_forall_negation_free_all :
  assumes "negation_free φ"
  shows "negation_free (push_forall (AllQ φ))"
  using assms proof(induction φ)
  case (And φ1 φ2)
  show ?case apply auto
    apply(rule negation_free_and)
    using And by auto
next
  case (Or φ1 φ2)
  show ?case
    apply auto
    apply(rule negation_free_or)   
    using Or map_fm_binders_negation_free negation_free_or by auto
next
  case (ExQ φ)
  then show ?case using map_fm_binders_negation_free by auto
next
  case (AllQ φ)
  then show ?case using map_fm_binders_negation_free by auto
next
  case (ExN x1 φ)
  then show ?case using map_fm_binders_negation_free by auto
next
  case (AllN x1 φ)
  then show ?case using map_fm_binders_negation_free by auto
qed auto

lemma push_forall_negation_free : 
  assumes "negation_free φ"  
  shows "negation_free(push_forall φ)"
  using assms proof(induction φ)
  case (Atom A)
  then show ?case apply(cases A) by auto
next
  case (And φ1 φ2)
  then show ?case by (auto simp add: and_def)
next
  case (Or φ1 φ2)
  then show ?case by (auto simp add: or_def)
next
  case (AllQ φ)
  then show ?case using push_forall_negation_free_all by auto
qed auto


lemma to_list_insertion: "insertion f p = sum_list [insertion f term * (f v) ^ i. (term,i)←(to_list v p)]"
proof-
  have h1 :  "insertion f p = insertion f (∑i≤MPoly_Type.degree p v. isolate_variable_sparse p v i * Var v ^ i)"
    using sum_over_zero by auto
  have h2 : "insertion f (Var v) = f v" by (auto simp: monomials_Var coeff_Var insertion_code)
  define d where "d = MPoly_Type.degree p v"
  define g where "g = (λx. insertion f (isolate_variable_sparse p v x) * f v ^ x)"
  have h3 : "insertion f (isolate_variable_sparse p v d) * f v ^ d = g d" using g_def by auto
  show ?thesis unfolding h1
      insertion_sum' insertion_mult insertion_pow h2 apply auto unfolding d_def[symmetric] g_def[symmetric]
      h3  proof(induction d)
    case 0
    then show ?case by auto
  next
    case (Suc d)
    show ?case
      apply (auto simp add: Suc ) unfolding g_def by auto
  qed
qed

lemma to_list_p: "p = sum_list [term * (Var v) ^ i. (term,i)←(to_list v p)]"
proof-
  define d where "d = MPoly_Type.degree p v"
  have "(∑i≤MPoly_Type.degree p v. isolate_variable_sparse p v i * Var v ^ i) = (∑(term, i)←to_list v p. term * Var v ^ i)"
    unfolding to_list.simps d_def[symmetric] apply(induction d) by auto
  then show ?thesis 
    using sum_over_zero[of p v]
    by auto
qed


fun chophelper :: "(real mpoly * nat) list ⇒ (real mpoly * nat) list ⇒ (real mpoly * nat) list * (real mpoly * nat) list" where
  "chophelper [] L = (L,[])"|
  "chophelper ((p,i)#L) R = (if p=0 then chophelper L (R @ [(p,i)]) else (R,(p,i)#L))"

lemma preserve :
  assumes "(a,b)=chophelper L L'"
  shows "a@b=L'@L"
  using assms
proof(induction L arbitrary : a b L')
  case Nil
  then show ?case using assms by auto
next
  case (Cons A L)
  then show ?case proof(cases A)
    case (Pair p i)
    show ?thesis using Cons unfolding Pair apply(cases "p=0") by auto
  qed
qed
lemma compare : 
  assumes "(a,b)=chophelper L L'"
  shows "chop L = b"
  using assms
proof(induction L arbitrary : a b L')
  case Nil
  then show ?case by auto
next
  case (Cons A L)
  then show ?case proof(cases A)
    case (Pair p i)
    show ?thesis using Cons unfolding Pair apply(cases "p=0") by auto
  qed
qed
lemma allzero:
  assumes "∀(p,i)∈set(L'). p=0"
  assumes "(a,b)=chophelper L L'"
  shows "∀(p,i)∈set(a). p=0"
  using assms proof(induction L arbitrary : a b L')
  case Nil
  then show ?case by auto
next
  case (Cons t L)
  then show ?case
  proof(cases t)
    case (Pair p i)
    show ?thesis proof(cases "p=0")
      case True
      have h1: "∀x∈set (L' @ [(0, i)]). case x of (p, i) ⇒ p = 0"
        using Cons(2) by auto
      show ?thesis using Cons(1)[OF h1] Cons(3) True unfolding Pair by auto
    next
      case False
      then show ?thesis using Cons unfolding Pair by auto
    qed
  qed
qed 

lemma separate:
  assumes "(a,b)=chophelper (to_list v p) []"
  shows "insertion f p = sum_list [insertion f term * (f v) ^ i. (term,i)←a] + sum_list [insertion f term * (f v) ^ i. (term,i)←b]"
  using to_list_insertion[of f p v]  preserve[OF assms, symmetric] unfolding List.append.left_neutral
  by (simp del: to_list.simps)

lemma chopped : 
  assumes "(a,b)=chophelper (to_list v p) []"
  shows "insertion f p = sum_list [insertion f term * (f v) ^ i. (term,i)←b]"
proof-
  have h1 : "∀(p, i)∈set []. p = 0" by auto
  have "(∑(term, i)←a. insertion f term * f v ^ i) = 0"
    using allzero[OF h1 assms] proof(induction a)
    case Nil
    then show ?case by auto
  next
    case (Cons a1 a2)
    then show ?case
      apply(cases a1) by simp
  qed 
  then show ?thesis using separate[OF assms, of f] by auto
qed

lemma insertion_chop : 
  shows "insertion f p = sum_list [insertion f term * (f v) ^ i. (term,i)←(chop (to_list v p))]" 
proof(cases "chophelper (to_list v p) []")
  case (Pair a b)
  show ?thesis using chopped[OF Pair[symmetric], of f] unfolding compare[OF Pair[symmetric], symmetric] .
qed

lemma sorted : "sorted_wrt (λ(_,i).λ(_,i'). i<i') (to_list v p)"
proof -
  define d  where "d = MPoly_Type.degree p v"
  show ?thesis unfolding to_list.simps d_def[symmetric] 
  proof(induction d)
    case 0
    then show ?case by auto
  next
    case (Suc d)
    have h : "(map (λx. (isolate_variable_sparse p v x, x)) [0..<Suc d + 1]) = 
        (map (λx. (isolate_variable_sparse p v x, x)) [0..<Suc d]) @ [(isolate_variable_sparse p v (Suc d), (Suc d))]"
      by auto
    show ?case
      unfolding sorted_wrt_append h
      using Suc
      by auto
  qed
qed

lemma sublist : "sublist (chop L) L"
proof(induction L)
  case Nil
  then show ?case by auto
next
  case (Cons a L)
  then show ?case proof(cases a)
    case (Pair a b)
    show ?thesis using Cons unfolding Pair apply auto
      by (simp add: sublist_Cons_right)
  qed
qed



lemma move_exp :
  assumes "(p',i)#L = (chop (to_list v p))"
  shows "insertion f p = sum_list [insertion f term * (f v) ^ (d-i). (term,d)←(chop (to_list v p))] * (f v)^i" 
proof-
  have h : "sorted_wrt (λ(_, i) (_, y). i < y) (chop (to_list v p))"
  proof-
    define L where "L = to_list v p"
    show ?thesis using sublist[of "to_list v p"] sorted[of v p] unfolding L_def[symmetric]
      by (metis sorted_wrt_append sublist_def)
  qed
  then have "∀(term,d)∈set(chop (to_list v p)). d≥i"
    unfolding assms[symmetric]  by fastforce
  then have simp : "∀(term,d)∈set(chop(to_list v p)). f v ^ (d - i) * f v ^ i = f v ^ d"
    unfolding semiring_normalization_rules(26) by(auto simp del: to_list.simps)
  have "insertion f p = sum_list [insertion f term * (f v) ^ i. (term,i)←(chop (to_list v p))]" using insertion_chop[of f p v] .
  also have "...= (∑(term, d)←chop (to_list v p). insertion f term * f v ^ (d-i) * f v ^ i)" 
    using simp
    by (smt Pair_inject case_prodE map_eq_conv mult.assoc split_cong) 
  also have "... =  (∑(term, d)←chop (to_list v p). insertion f term * f v ^ (d - i)) * f v ^ i"
  proof-
    define d where "d = chop(to_list v p)"
    define a where "a = f v ^ i"
    define b where "b = (λ(term, d). insertion f term * f v ^ (d - i))"
    have h : "(∑(term, d)←d. insertion f term * f v ^ (d - i) * a) = (∑(term, d)←d. b (term,d) * a)"
      using b_def by auto
    show ?thesis unfolding d_def[symmetric] a_def[symmetric]  b_def[symmetric] h  apply(induction d) apply simp apply auto
      by (simp add: ring_class.ring_distribs(2))
  qed
  finally show ?thesis by auto
qed

lemma insert_Var_Zero : "insertion f (Var v) = f v"
  unfolding insertion_code monomials_Var apply auto
  unfolding coeff_Var by simp


lemma decreasePower_insertion :
  assumes "decreasePower v p = (p',i)"
  shows "insertion f p = insertion f p'* (f v)^i"
proof(cases "chop (to_list v p)")
  case Nil
  then show ?thesis
    using assms by auto
next
  case (Cons a list)
  then show ?thesis
  proof(cases a)
    case (Pair coef i')
    have i'_def : "i'=i" using Cons assms Pair by auto
    have chop: "chop (to_list v p) = (coef, i) # list" using Cons assms unfolding i'_def Pair by auto
    have p'_def :  "p' = (∑(term, x)←chop (to_list v p). term * Var v ^ (x - i))"
      using assms Cons Pair by auto 
    have p'_insertion : "insertion f p' = (∑(term, x)←chop (to_list v p). insertion f term * f v ^ (x - i))"
    proof-
      define d where "d = chop (to_list v p)"
      have "insertion f p' = insertion f (∑(term, x)←chop (to_list v p). term * Var v ^ (x - i))" using p'_def by auto
      also have "... = (∑(term, x)←chop (to_list v p).  insertion f (term * Var v ^ (x - i)))" 
        unfolding d_def[symmetric] apply(induction d) apply simp apply(simp add:insertion_add) by auto
      also have "... = (∑(term, x)←chop (to_list v p). insertion f term * f v ^ (x - i))" unfolding insertion_mult insertion_pow insert_Var_Zero by auto
      finally show ?thesis by auto
    qed
    have h : "(coef, i') # list = chop (to_list v p)"  using Cons unfolding Pair by auto
    show ?thesis unfolding p'_insertion
      using move_exp[OF h, of f] unfolding i'_def .
  qed
qed 


lemma unpower_eval: "eval (unpower v φ) L = eval φ L"
proof(induction φ arbitrary: v L)
  case TrueF
  then show ?case by auto
next
  case FalseF
  then show ?case by auto
next
  case (Atom At)
  then show ?case proof(cases At)
    case (Less p)
    obtain q i where h: "decreasePower v p = (q, i)"
      using prod.exhaust_sel by blast
    have p : "⋀f. insertion f p = insertion f q* (f v)^i"
      using decreasePower_insertion[OF h] by auto
    show ?thesis
    proof(cases "i=0")
      case True
      then show ?thesis unfolding Less unpower.simps h  by auto
    next
      case False
      obtain x where x_def : "Suc x = i" using False
        using not0_implies_Suc by auto 
      have h1 : "i mod 2 = 0 ⟹
    (insertion (nth_default 0 L) q < 0 ∧
     insertion (nth_default 0 L) (Var v) ≠ 0) =
    (insertion (nth_default 0 L) q * nth_default 0 L v ^ i < 0)"
      proof -
        assume "i mod 2 = 0"
        then have "∀r. ¬ (r::real) ^ i < 0"
          by presburger
        then show ?thesis
          by (metis ‹⋀thesis. (⋀x. Suc x = i ⟹ thesis) ⟹ thesis› insert_Var_Zero linorder_neqE_linordered_idom mult_less_0_iff power_0_Suc power_eq_0_iff)
      qed
      show ?thesis
        unfolding Less unpower.simps h x_def [symmetric] apply simp
        unfolding x_def p apply (cases ‹even i›)
        using h1 apply (auto simp add: insertion_neg insert_Var_Zero mult_less_0_iff not_less zero_less_mult_iff elim: oddE)
        done
    qed 
  next
    case (Eq p)
    obtain q i where h: "decreasePower v p = (q, i)"
      using prod.exhaust_sel by blast
    have p : "⋀f. insertion f p = insertion f q* (f v)^i"
      using decreasePower_insertion[OF h] by auto
    show ?thesis unfolding Eq unpower.simps h apply simp apply(cases i) apply simp
      apply simp unfolding p apply simp
      by (metis insert_Var_Zero)
  next
    case (Leq p)
    obtain q i where h: "decreasePower v p = (q, i)"
      using prod.exhaust_sel by blast
    have p : "⋀f. insertion f p = insertion f q* (f v)^i"
      using decreasePower_insertion[OF h] by auto
    show ?thesis
    proof(cases "i=0")
      case True
      then show ?thesis unfolding Leq unpower.simps h  by auto
    next
      case False
      obtain x where x_def : "Suc x = i" using False
        using not0_implies_Suc by auto 
      define a where "a = insertion (nth_default 0 L) q"
      define x' where "x' = nth_default 0 L v"
      show ?thesis unfolding Leq unpower.simps h x_def[symmetric] apply simp
        unfolding x_def p apply(cases "i mod 2 = 0") unfolding insert_Var_Zero insertion_mult insertion_pow insertion_neg apply simp_all
        unfolding a_def[symmetric] x'_def[symmetric]
      proof-
        assume "i mod 2 = 0"
        then have "x' ^ i ≥0"
          by (simp add: ‹i mod 2 = 0› even_iff_mod_2_eq_zero zero_le_even_power) 
        then show "(a ≤ 0 ∨ x' = 0) = (a * x' ^ i ≤ 0)"
          using Rings.ordered_semiring_0_class.mult_nonpos_nonneg[of a "x'^i"]
          apply auto
          unfolding Rings.linordered_ring_strict_class.mult_le_0_iff
          apply auto
          by (simp add: False power_0_left)
      next
        assume h:  "i mod 2 = Suc 0"
        show "(a = 0 ∨ a < 0 ∧ 0 ≤ x' ∨ 0 < a ∧ x' ≤ 0) = (a * x' ^ i ≤ 0)"
          using h
          by (smt even_iff_mod_2_eq_zero mult_less_cancel_right mult_neg_neg mult_nonneg_nonpos mult_pos_pos not_mod2_eq_Suc_0_eq_0 power_0_Suc x_def zero_le_power_eq zero_less_mult_pos2 zero_less_power)
      qed
    qed 
  next
    case (Neq p)
    obtain q i where h: "decreasePower v p = (q, i)"
      using prod.exhaust_sel by blast
    have p : "⋀f. insertion f p = insertion f q* (f v)^i"
      using decreasePower_insertion[OF h] by auto
    show ?thesis unfolding Neq unpower.simps h apply simp apply(cases i) apply simp
      apply simp unfolding p apply simp
      by (metis insert_Var_Zero)
  qed
qed auto

lemma to_list_filter: "p = sum_list [term * (Var v) ^ i. (term,i)←((filter (λ(x,_). x≠0) (to_list v p)))]"
proof-
  define L where "L = to_list v p"
  have "(∑(term, i)←to_list v p. term * Var v ^ i) = (∑(term, i)←filter (λ(x, _). x ≠ 0) (to_list v p). term * Var v ^ i)"
    unfolding L_def[symmetric] apply(induction L) by auto
  then show ?thesis
    using to_list_p[of p v] by auto
qed

end