Theory Renegar_Proofs

theory Renegar_Proofs
  imports Renegar_Algorithm
    BKR_Proofs
begin

(* Note that there is significant overlap between Renegar and BKR in general, so there is some
  similarity between this file and BKR_Proofs.thy
  The main difference is that the RHS vector in Renegar is different from the RHS vector in BKR 
  In BKR, all of the qs are assumed to be relatively prime to p. Renegar removes this assumption. 
  In general, the _R's on definition and lemma names in this file are to emphasize that we are 
  working with Renegar style.
*)

section "Tarski Queries Changed"

lemma construct_NofI_R_relation:
  fixes p:: "real poly"
  fixes I1:: "real poly list"
  fixes I2:: "real poly list"
  shows "construct_NofI_R p I1 I2 =
    construct_NofI (sum_list (map power2 (p # I1))) I2"
  unfolding construct_NofI_R_def construct_NofI_def
  by metis

lemma sum_list_map_power2:
  shows "sum_list (map power2 ls)  (0::real poly)"
  apply (induct ls)
  by auto

lemma sum_list_map_power2_poly:
  shows "poly (sum_list (map power2 (ls::real poly list))) x  (0::real)"
  apply (induct ls)
  by auto

lemma construct_NofI_R_prop_helper:
  fixes p:: "real poly"
  fixes I1:: "real poly list"
  fixes I2:: "real poly list"
  assumes nonzero: "p0"
  shows "construct_NofI_R p I1 I2 =
    rat_of_int (int (card {x. poly (sum_list (map (λx. x^2) (p # I1))) x = 0  poly (prod_list I2) x > 0}) - 
    int (card {x. poly (sum_list (map (λx. x^2) (p # I1))) x = 0   poly (prod_list I2) x < 0}))"
proof -
  show ?thesis unfolding construct_NofI_R_relation[of p I1 I2]
    apply (subst construct_NofI_prop[of _ I2])
     apply auto
    using assms sum_list_map_power2
    by (metis le_add_same_cancel1 power2_less_eq_zero_iff)
qed

lemma zer_iff:
  fixes p:: "real poly"
  fixes ls:: "real poly list"
  shows "poly (sum_list (map (λx. x^2) ls)) x = 0  (i  set ls. poly i x = 0)"
proof (induct ls)
  case Nil
  then show ?case by auto
next
  case (Cons a I1)
  then show ?case
    apply simp
    apply (subst add_nonneg_eq_0_iff)
    using zero_le_power2 apply blast
    using sum_list_map_power2_poly apply presburger
    by simp
qed

lemma construct_NofI_prop_R:
  fixes p:: "real poly"
  fixes I1:: "real poly list"
  fixes I2:: "real poly list"
  assumes nonzero: "p0"
  shows "construct_NofI_R p I1 I2 =
    rat_of_int (int (card {x. poly p x = 0  (q  set I1. poly q x = 0)  poly (prod_list I2) x > 0}) - 
    int (card {x. poly p x = 0   (q  set I1. poly q x = 0)  poly (prod_list I2) x < 0}))"
  unfolding construct_NofI_R_prop_helper[OF nonzero] 
  using zer_iff
  apply auto
  by (smt (verit, del_insts) Collect_cong sum_list_map_power2_poly zero_le_power2 zero_less_power2)

section "Matrix Equation"

definition map_sgas:: "rat list  rat list"
  where "map_sgas l = map (λr. (1 - r^2)) l"

definition z_R:: "(nat list*nat list)  rat list  rat"
  where "z_R index_list sign_asg  (prod_list (map (nth (map_sgas sign_asg)) (fst(index_list))))*(prod_list (map (nth sign_asg) (snd(index_list))))"

definition mtx_row_R:: "rat list list  (nat list * nat list)  rat list"
  where "mtx_row_R sign_list index_list  (map ((z_R index_list)) sign_list)"

definition matrix_A_R:: "rat list list   (nat list * nat list) list  rat mat" 
  where "matrix_A_R sign_list subset_list = 
    (mat_of_rows_list (length sign_list) (map (λi .(mtx_row_R sign_list i)) subset_list))"

definition all_list_constr_R:: "(nat list*nat list) list  nat  bool"
  where "all_list_constr_R L n  (x. List.member L x  (list_constr (fst x) n  list_constr (snd x) n))"

definition alt_matrix_A_R:: "rat list list  (nat list*nat list) list  rat mat"
  where "alt_matrix_A_R signs subsets = (mat (length subsets) (length signs) 
    (λ(i, j). z_R (subsets ! i) (signs ! j)))"

lemma alt_matrix_char_R: "alt_matrix_A_R signs subsets = matrix_A_R signs subsets"
proof - 
  have h0: "(i j. i < length subsets 
            j < length signs 
            map (λindex_list. map (z_R index_list) signs) subsets ! i ! j = z_R (subsets ! i) (signs ! j))"
  proof -
    fix i
    fix j
    assume i_lt: "i < length subsets"
    assume j_lt: "j < length signs"
    show "((map (λindex_list. map (z_R index_list) signs) subsets) ! i) ! j = z_R (subsets ! i) (signs ! j)"
    proof - 
      have h0: "(map (λindex_list. map (z_R index_list) signs) subsets) ! i =  map (z_R (subsets ! i)) signs" 
        using nth_map i_lt
        by blast
      then show ?thesis using nth_map j_lt
        by simp 
    qed
  qed
  have h: " mat (length subsets) (length signs) (λ(i, j). z_R (subsets ! i) (signs ! j)) =
    mat (length subsets) (length signs) (λ(i, y). map (λindex_list. map (z_R index_list) signs) subsets ! i ! y)"
    using h0 eq_matI[where A = "mat (length subsets) (length signs) (λ(i, j). z_R (subsets ! i) (signs ! j))",
        where B = "mat (length subsets) (length signs) (λ(i, y). map (λindex_list. map (z_R index_list) signs) subsets ! i ! y)"]
    by auto
  show ?thesis unfolding alt_matrix_A_R_def matrix_A_R_def mat_of_rows_list_def apply (auto) unfolding mtx_row_R_def
    using h  by blast
qed

lemma subsets_are_rows_R: "i < (length subsets). row (alt_matrix_A_R signs subsets) i  = vec (length signs) (λj. z_R (subsets ! i) (signs ! j))"
  unfolding row_def unfolding alt_matrix_A_R_def by auto

lemma signs_are_cols_R: "i < (length signs). col (alt_matrix_A_R signs subsets) i  = vec (length subsets) (λj. z_R (subsets ! j) (signs ! i))"
  unfolding col_def unfolding alt_matrix_A_R_def by auto

definition consistent_sign_vec::"real poly list  real  rat list"
  where "consistent_sign_vec qs x 
    map (λ q. if (poly q x > 0) then (1::rat) else (if (poly q x = 0) then (0::rat) else (-1::rat))) qs"

definition construct_lhs_vector_R:: "real poly  real poly list  rat list list   rat vec"
  where "construct_lhs_vector_R p qs signs                                                            
 vec_of_list (map (λw.  rat_of_int (int (length (filter (λv. v = w) (map (consistent_sign_vec qs) (characterize_root_list_p p)))))) signs)"

(* The ith entry of LHS vector is the number of (distinct) real zeros of p where the sign vector of 
   the qs is the ith entry of signs.*)

(* Putting all of the pieces of the construction together *)
definition satisfy_equation_R:: "real poly  real poly list  (nat list*nat list) list  rat list list  bool"
  where "satisfy_equation_R p qs subset_list sign_list =
        (mult_mat_vec (matrix_A_R sign_list subset_list) (construct_lhs_vector_R p qs sign_list) = (construct_rhs_vector_R p qs subset_list))"

(* Recharacterize the LHS vector *)
lemma construct_lhs_vector_clean_R:
  assumes "p  0"
  assumes "i < length signs"
  shows "(construct_lhs_vector_R p qs signs) $ i =
    card {x. poly p x = 0  ((consistent_sign_vec qs x) = (nth signs i))}"
proof -
  from poly_roots_finite[OF assms(1)] have "finite {x. poly p x = 0}" .
  then have eq: "(Collect
       ((λv. v = signs ! i) 
        consistent_sign_vec qs) 
      set (sorted_list_of_set
            {x. poly p x = 0})) =
    {x. poly p x = 0  consistent_sign_vec qs x = signs ! i}"
    by auto
  show ?thesis
    unfolding construct_lhs_vector_R_def vec_of_list_index characterize_root_list_p_def
    apply auto
    apply (subst nth_map[OF assms(2)])
    apply auto
    apply (subst distinct_length_filter)
     apply (auto) 
    using eq 
    by auto
qed

lemma construct_lhs_vector_cleaner_R:
  assumes "p  0"
  shows "(construct_lhs_vector_R p qs signs) =
   vec_of_list (map (λs. rat_of_int (card {x. poly p x = 0  ((consistent_sign_vec qs x) = s)})) signs)"
  apply (rule eq_vecI)
   apply (auto simp add:  construct_lhs_vector_clean_R[OF assms] )
   apply (simp add: vec_of_list_index)
  unfolding construct_lhs_vector_R_def
  using assms construct_lhs_vector_clean_R construct_lhs_vector_def apply auto[1]
   apply (simp add: construct_lhs_vector_R_def)
  by auto

(* Show that because our consistent sign vectors consist of 1, 0's, and -1's, z returns 1, 0, or -1 
  when applied to a consistent sign vector *)
lemma z_signs_R2:
  fixes I:: "nat list"
  fixes signs:: "rat list"
  assumes lf: "list_all (λi. i < length signs) I"
  assumes la:  "list_all (λs. s = 1  s = 0  s = -1) signs"
  shows "(prod_list (map (nth signs) I)) = 1 
  (prod_list (map (nth signs) I)) = 0 
  (prod_list (map (nth signs) I)) = -1" using assms
proof (induct I)
  case Nil
  then show ?case by auto
next
  case (Cons a I)
  moreover have eo: "signs ! a = 1  signs ! a = 0  signs ! a = -1" 
    using assms
    by (smt (verit, del_insts) calculation(2) list_all_length list_all_simps(1)) 
  have "prod_list (map ((!) (map_sgas signs)) (a # I)) = (1 - (signs ! a)^2)*prod_list (map ((!) (map_sgas signs)) (I))"
    unfolding map_sgas_def apply (auto)
    using calculation(2) by auto 
  then show ?case using eo
    using Cons.hyps calculation(2) la by auto 
qed

lemma z_signs_R1:
  fixes I:: "nat list"
  fixes signs:: "rat list"
  assumes lf: "list_all (λi. i < length signs) I"
  assumes la:  "list_all (λs. s = 1  s = 0  s = -1) signs"
  shows "(prod_list (map (nth (map_sgas signs)) I)) = 1 
(prod_list (map (nth (map_sgas signs)) I)) = 0" using assms
proof (induct I)
  case Nil
  then show ?case by auto
next
  case (Cons a I)
  moreover have "signs ! a = 1  signs ! a = 0  signs ! a = -1" 
    using assms
    by (smt (verit, best) calculation(2) list_all_length list_all_simps(1)) 
  then have eo: "1 - (signs ! a)^2 = 1  1 - (signs !a)^2 = 0"
    using cancel_comm_monoid_add_class.diff_cancel diff_zero by fastforce
  have "prod_list (map ((!) (map_sgas signs)) (a # I)) = (1 - (signs ! a)^2)*prod_list (map ((!) (map_sgas signs)) (I))"
    unfolding map_sgas_def apply (auto)
    using calculation(2) by auto 
  then show ?case using eo
    using Cons.hyps calculation(2) la by auto 
qed

lemma z_signs_R:
  fixes I:: "(nat list * nat list)"
  fixes signs:: "rat list"
  assumes lf: "list_all (λi. i < length signs) (fst(I))"
  assumes ls: "list_all (λi. i < length signs) (snd(I))"
  assumes la:  "list_all (λs. s = 1  s = 0  s = -1) signs"
  shows "(z_R I signs = 1)  (z_R I signs = 0)  (z_R I signs = -1)" 
  using assms z_signs_R2 z_signs_R1 unfolding z_R_def apply (auto)
  by (metis (no_types, lifting) mult_cancel_left1 mult_minus1_right)

lemma z_lemma_R:
  fixes I:: "nat list * nat list" 
  fixes sign:: "rat list"
  assumes consistent: "sign  set (characterize_consistent_signs_at_roots p qs)"
  assumes welldefined1: "list_constr (fst I) (length qs)"
  assumes welldefined2: "list_constr (snd I) (length qs)"
  shows "(z_R I sign = 1)  (z_R I sign = 0)  (z_R I sign = -1)"
proof (rule z_signs_R)
  have same: "length sign = length qs" using consistent
    using characterize_consistent_signs_at_roots_def signs_at_def by fastforce
  thus "(list_all (λi. i < length sign) (fst I))"
    using welldefined1  
    by (auto simp add: list_constr_def characterize_consistent_signs_at_roots_def consistent_sign_vec_copr_def)
  thus "(list_all (λi. i < length sign) (snd I))"
    using same welldefined2  
    by (auto simp add: list_constr_def characterize_consistent_signs_at_roots_def consistent_sign_vec_copr_def)
  show "list_all (λs. s = 1  s = 0  s = - 1) sign" using consistent
    apply (auto simp add: list.pred_map  characterize_consistent_signs_at_roots_def  consistent_sign_vec_def)
    using Ball_set
    by (simp add: list_all_length signs_at_def squash_def) 
qed

(* Show that all consistent sign vectors on roots of polynomials are in characterize_consistent_signs_at_roots  *)
lemma in_set_R: 
  fixes p:: "real poly"
  assumes nonzero: "p0"
  fixes qs:: "real poly list"
  fixes sign:: "rat list"
  fixes x:: "real"
  assumes root_p: "x  {x. poly p x = 0}"
  assumes sign_fix: "sign = consistent_sign_vec qs x"
  shows "sign  set (characterize_consistent_signs_at_roots p qs)" 
proof -
  have h1: "consistent_sign_vec qs x 
      set (remdups (map (signs_at qs) (sorted_list_of_set {x. poly p x = 0})))" 
    unfolding consistent_sign_vec_def signs_at_def squash_def
    using root_p nonzero poly_roots_finite set_sorted_list_of_set apply (auto)
    by (smt (verit, ccfv_SIG) Collect_cong comp_def image_eqI map_eq_conv mem_Collect_eq poly_roots_finite set_sorted_list_of_set) 
  thus ?thesis unfolding characterize_consistent_signs_at_roots_def characterize_root_list_p_def using sign_fix
    by blast
qed

lemma consistent_signs_prop_R:
  fixes p:: "real poly"
  assumes nonzero: "p0"
  fixes qs:: "real poly list"
  fixes sign:: "rat list"
  fixes x:: "real"
  assumes root_p: "x  {x. poly p x = 0}"
  assumes sign_fix: "sign = consistent_sign_vec qs x"
  shows  "list_all (λs. s = 1  s = 0  s = -1) sign"
  using assms unfolding consistent_sign_vec_def squash_def apply (auto)
  by (smt (z3) length_map list_all_length nth_map) 

(* The next few lemmas relate z_R to the signs of the product of subsets of polynomials of qs *)
lemma horiz_vector_helper_pos_ind_R1: 
  fixes p:: "real poly"
  assumes nonzero: "p0"
  fixes qs:: "real poly list"
  fixes I:: "nat list" 
  fixes sign:: "rat list"
  fixes x:: "real"
  assumes root_p: "x  {x. poly p x = 0}"
  assumes sign_fix: "sign = consistent_sign_vec qs x"
  assumes asm: "list_constr I (length qs)"
  shows "(prod_list (map (nth (map_sgas sign)) I)) = 1  
    (p  set (retrieve_polys qs I). poly p x = 0)"
  using asm
proof (induction "I")
  case Nil
  then show ?case unfolding map_sgas_def apply (auto)
    by (simp add: retrieve_polys_def)
next
  case (Cons a xa)
  then have same0: "(prod_list (map (nth (map_sgas sign)) xa)) = 1  
    (p  set (retrieve_polys qs xa). poly p x = 0)" unfolding list_constr_def by auto
  have welldef: "a < length qs" using Cons.prems assms unfolding list_constr_def by auto
  then have h: "prod_list (map ((!) (map_sgas sign)) (a#xa)) = (1 - (sign ! a)^2)*(prod_list (map ((!) (map_sgas sign)) (xa)))"
    unfolding map_sgas_def using assms apply (auto)
    by (metis (no_types, lifting) consistent_sign_vec_def length_map nth_map) 
  have "list_all (λs. s = 1  s = 0  s = -1) sign" using sign_fix unfolding consistent_sign_vec_def squash_def
    apply (auto)
    by (smt (z3) length_map list_all_length nth_map) 
  then have eo: "(prod_list (map ((!) (map_sgas sign)) (xa))) = 0  (prod_list (map ((!) (map_sgas sign)) (xa))) = 1"
    using z_signs_R1 assms Cons.prems consistent_sign_vec_def length_map list_all_simps(1) length_map list_all_length list_constr_def
    by (smt (verit, best))
  have "(sign ! a)^2 = 1  (sign ! a)^2 = 0" using sign_fix welldef  unfolding consistent_sign_vec_def 
    by auto
  then have s1: "(prod_list (map (nth (map_sgas sign)) (a#xa))) = 1  
    ((sign ! a)^2 = 0  (prod_list (map ((!) (map_sgas sign)) (xa))) = 1)"
    using eo h
    by (metis (mono_tags, opaque_lifting) cancel_comm_monoid_add_class.diff_cancel diff_zero mult.left_neutral mult_zero_left)
  have "(sign ! a)^2 = 0  (poly (qs ! a) x = 0)"
    using sign_fix unfolding consistent_sign_vec_def welldef apply (auto)
     apply (smt (z3) class_field.neg_1_not_0 class_field.zero_not_one nth_map welldef)
    by (smt (z3) nth_map welldef)
  then have same1:"(prod_list (map (nth (map_sgas sign)) (a#xa))) = 1  
    ((poly (qs ! a) x = 0)  (prod_list (map ((!) (map_sgas sign)) (xa))) = 1)" using s1 by auto
  have "set (retrieve_polys qs (a#xa)) = {(qs ! a)}  set (retrieve_polys qs xa)"
    by (metis (no_types, lifting) insert_is_Un list.simps(15) list.simps(9) retrieve_polys_def)
  then have same2:"(p  set (retrieve_polys qs (a#xa)). poly p x = 0) = ((poly (qs ! a) x = 0)
       (p  set (retrieve_polys qs (xa)). poly p x = 0))"
    by auto 
  then show ?case using same0 same1 same2 
      assms by auto
qed

lemma csv_length_same_as_qlist: 
  fixes p:: "real poly"
  assumes nonzero: "p0"
  fixes qs:: "real poly list"
  fixes sign:: "rat list"
  fixes x:: "real"
  assumes root_p: "x  {x. poly p x = 0}"
  assumes sign_fix: "sign = consistent_sign_vec qs x"
  shows "length sign = length qs" 
  using assms unfolding consistent_sign_vec_def by auto

lemma horiz_vector_helper_zer_ind_R2: 
  fixes p:: "real poly"
  assumes nonzero: "p0"
  fixes qs:: "real poly list"
  fixes I:: "nat list" 
  fixes sign:: "rat list"
  fixes x:: "real"
  assumes root_p: "x  {x. poly p x = 0}"
  assumes sign_fix: "sign = consistent_sign_vec qs x"
  assumes asm: "list_constr I (length qs)"
  shows "(prod_list (map (nth sign) I)) = 0  
    (poly (prod_list (retrieve_polys qs I)) x = 0)"
  using asm
proof (induction "I")
  case Nil
  then show ?case unfolding map_sgas_def apply (auto) unfolding retrieve_polys_def
    by auto next
  case (Cons a xa)
  have "poly (prod_list (retrieve_polys qs (a # xa))) x = (poly (qs ! a) x)*poly (prod_list (retrieve_polys qs (xa))) x"
    by (simp add: retrieve_polys_def)
  then show ?case using Cons.prems
    by (smt (z3) Cons.IH class_field.neg_1_not_0 class_field.zero_not_one consistent_sign_vec_def list.simps(9) list_all_simps(1) list_constr_def mult_eq_0_iff nth_map prod_list.Cons sign_fix) 
qed

lemma horiz_vector_helper_pos_ind_R2: 
  fixes p:: "real poly"
  assumes nonzero: "p0"
  fixes qs:: "real poly list"
  fixes I:: "nat list" 
  fixes sign:: "rat list"
  fixes x:: "real"
  assumes root_p: "x  {x. poly p x = 0}"
  assumes sign_fix: "sign = consistent_sign_vec qs x"
  assumes asm: "list_constr I (length qs)"
  shows "(prod_list (map (nth sign) I)) = 1  
    (poly (prod_list (retrieve_polys qs I)) x > 0)"
  using asm
proof (induction "I")
  case Nil
  then show ?case unfolding map_sgas_def apply (auto) unfolding retrieve_polys_def
    by auto next
  case (Cons a xa)
  then have ih: "(prod_list (map ((!) sign) xa) = 1) = (0 < poly (prod_list (retrieve_polys qs xa)) x)"
    unfolding list_constr_def by auto
  have lensame: "length sign = length qs" using sign_fix csv_length_same_as_qlist[of p x sign qs]
      nonzero root_p by auto
  have "poly (prod_list (retrieve_polys qs (a # xa))) x = (poly (qs ! a) x)*poly (prod_list (retrieve_polys qs (xa))) x"
    by (simp add: retrieve_polys_def)
  then have iff1: "(poly (prod_list (retrieve_polys qs (a#xa))) x > 0)  
      (((poly (qs ! a) x) > 0  poly (prod_list (retrieve_polys qs (xa))) x > 0)  
       ((poly (qs ! a) x) < 0  poly (prod_list (retrieve_polys qs (xa))) x < 0))"
    by (metis zero_less_mult_iff)
  have prodsame: "(prod_list (map (nth sign) (a#xa))) = (sign ! a)* (prod_list (map (nth sign) (xa)))"
    using lensame Cons.prems unfolding list_constr_def by auto
  have sagt: "sign ! a = 1  (poly (qs ! a) x) > 0" using assms unfolding consistent_sign_vec_def
    apply (auto)
     apply (smt (verit, best) Cons.prems list_all_simps(1) list_constr_def neg_equal_zero nth_map zero_neq_one)
    by (smt (verit, ccfv_threshold) Cons.prems list_all_simps(1) list_constr_def nth_map)
  have salt: "sign ! a = -1  (poly (qs ! a) x) < 0" using assms unfolding consistent_sign_vec_def
    apply (auto)
     apply (smt (verit, ccfv_SIG) Cons.prems less_minus_one_simps(1) less_minus_one_simps(3) list_all_simps(1) list_constr_def neg_0_less_iff_less nth_map)
    by (smt (verit, best) Cons.prems list_all_simps(1) list_constr_def nth_map)  
  have h1: "((poly (qs ! a) x) > 0  poly (prod_list (retrieve_polys qs (xa))) x > 0) 
       (prod_list (map (nth sign) (a#xa))) = 1" 
    using prodsame sagt ih by auto
  have eo: "(prod_list (map ((!) sign) xa) = 1)   (prod_list (map ((!) sign) xa) = 0)  
      (prod_list (map ((!) sign) xa) = -1)"
    using Cons.prems consistent_signs_prop_R lensame list_constr_def nonzero root_p sign_fix z_signs_R2 by auto
  have d1:"(prod_list (map ((!) sign) xa) = -1)  (0 > poly (prod_list (retrieve_polys qs xa)) x)"
  proof -
    assume "(prod_list (map ((!) sign) xa) = -1) "
    then show "(0 > poly (prod_list (retrieve_polys qs xa)) x)"
      using prodsame salt ih assms Cons.prems class_field.neg_1_not_0 equal_neg_zero horiz_vector_helper_zer_ind_R2 linorder_neqE_linordered_idom list_all_simps(1) list_constr_def
      apply (auto)
       apply (smt (verit, ccfv_threshold) class_field.neg_1_not_0 list.set_map list_all_length semidom_class.prod_list_zero_iff)
      by (smt (verit, ccfv_threshold) class_field.neg_1_not_0 list.set_map list_all_length semidom_class.prod_list_zero_iff)
  qed
  have d2: "(0 > poly (prod_list (retrieve_polys qs xa)) x)  (prod_list (map ((!) sign) xa) = -1)"
    using eo assms horiz_vector_helper_zer_ind_R2[where p = "p", where x = "x", where sign = "sign", where I ="I"]
    apply (auto)
    using ih apply force
    by (metis (full_types, lifting) Cons.prems class_field.neg_1_not_0 horiz_vector_helper_zer_ind_R2 ih imageI list.set_map list_all_simps(1) list_constr_def mem_Collect_eq neg_equal_0_iff_equal semidom_class.prod_list_zero_iff)  
  have "(prod_list (map ((!) sign) xa) = -1) = (0 > poly (prod_list (retrieve_polys qs xa)) x)"
    using d1 d2
    by blast       
  then have h2: "((poly (qs ! a) x) < 0  poly (prod_list (retrieve_polys qs (xa))) x < 0) 
      (prod_list (map (nth sign) (a#xa))) = 1"
    using prodsame salt ih by auto
  have h3: "(prod_list (map (nth sign) (a#xa))) = 1  (((poly (qs ! a) x) > 0  poly (prod_list (retrieve_polys qs (xa))) x > 0)  
       ((poly (qs ! a) x) < 0  poly (prod_list (retrieve_polys qs (xa))) x < 0))"
    using prodsame salt ih assms horiz_vector_helper_zer_ind_R2[where p = "p", where x = "x", where sign = "sign", where I ="I"]
    by (smt (verit, ccfv_threshold) Cons.prems poly (prod_list (retrieve_polys qs (a # xa))) x = poly (qs ! a) x * poly (prod_list (retrieve_polys qs xa)) x horiz_vector_helper_zer_ind_R2 mem_Collect_eq mult_cancel_left1 mult_not_zero sagt) 
  then show ?case using h1 h2 h3 iff1 Cons.prems by auto
qed

lemma horiz_vector_helper_pos_ind_R: 
  fixes p:: "real poly"
  assumes nonzero: "p0"
  fixes qs:: "real poly list"
  fixes I:: "nat list * nat list" 
  fixes sign:: "rat list"
  fixes x:: "real"
  assumes root_p: "x  {x. poly p x = 0}"
  assumes sign_fix: "sign = consistent_sign_vec qs x"
  assumes asm1: "list_constr (fst I) (length qs)"
  assumes asm2: "list_constr (snd I) (length qs)"
  shows "((p  set (retrieve_polys qs (fst I)). poly p x = 0)  (poly (prod_list (retrieve_polys qs (snd I))) x > 0))  (z_R I sign = 1)"
proof - 
  have len: "length sign = length qs" using sign_fix csv_length_same_as_qlist[of p x sign qs]
      nonzero root_p by auto
  have d1: "((p  set (retrieve_polys qs (fst I)). poly p x = 0)  (poly (prod_list (retrieve_polys qs (snd I))) x > 0))  (z_R I sign = 1)" 
    using assms horiz_vector_helper_pos_ind_R1[where p = "p", where qs = "qs", where sign = "sign", where x = "x", where I = "fst I"]
      horiz_vector_helper_pos_ind_R2[where p = "p", where qs = "qs", where sign = "sign", where x = "x", where I = "snd I"] unfolding z_R_def 
    by auto
  have d2: "(z_R I sign = 1)  ((p  set (retrieve_polys qs (fst I)). poly p x = 0)  (poly (prod_list (retrieve_polys qs (snd I))) x > 0))"
  proof - 
    have h1: "(z_R I sign = 1)  (p  set (retrieve_polys qs (fst I)). poly p x = 0)" 
    proof - 
      have "(prod_list (map (nth (map_sgas sign)) (fst I))) = 1  (prod_list (map (nth (map_sgas sign)) (fst I))) = 0" 
        using len consistent_signs_prop_R[where p = "p", where qs = "qs", where x = "x", where sign = "sign"] z_signs_R1[where signs = "sign", where I = "fst I"] assms 
        unfolding list_constr_def 
        by auto
      then show ?thesis
        using z_signs_R1[where signs = "sign", where I = "fst I"] horiz_vector_helper_pos_ind_R1[where sign = "sign", where I = "fst I", where p = "p", where x = "x"] assms 
        apply (auto)
        by (metis (mono_tags, opaque_lifting) prod_list (map ((!) (map_sgas sign)) (fst I)) = 1  prod_list (map ((!) (map_sgas sign)) (fst I)) = 0 mult_zero_left z_R_def) 
    qed
    then have h2: "(z_R I sign = 1)  (poly (prod_list (retrieve_polys qs (snd I))) x > 0)" 
      unfolding z_R_def using assms horiz_vector_helper_pos_ind_R2[where p = "p", where x = "x", where sign = "sign", where qs = "qs", where I ="snd I"]
      by (metis horiz_vector_helper_pos_ind_R1 mult.left_neutral)
    show ?thesis using h1 h2 by auto
  qed
  show ?thesis using d1 d2 by blast
qed

lemma horiz_vector_helper_pos_R: 
  fixes p:: "real poly"
  assumes nonzero: "p0"
  fixes qs:: "real poly list"
  fixes I:: "nat list*nat list" 
  fixes sign:: "rat list"
  fixes x:: "real"
  assumes root_p: "x  {x. poly p x = 0}"
  assumes sign_fix: "sign = consistent_sign_vec qs x"
  assumes welldefined1: "list_constr (fst I) (length qs)"
  assumes welldefined2: "list_constr (snd I) (length qs)"
  shows "((p  set (retrieve_polys qs (fst I)). poly p x = 0)  (poly (prod_list (retrieve_polys qs (snd I))) x > 0))  (z_R I sign = 1)"
  using horiz_vector_helper_pos_ind_R
  using  nonzero  root_p sign_fix welldefined1 welldefined2 by blast

lemma horiz_vector_helper_neg_R: 
  fixes p:: "real poly"
  assumes nonzero: "p0"
  fixes qs:: "real poly list"
  fixes I:: "nat list*nat list" 
  fixes sign:: "rat list"
  fixes x:: "real"
  assumes root_p: "x  {x. poly p x = 0}"
  assumes sign_fix: "sign = consistent_sign_vec qs x"
  assumes welldefined1: "list_constr (fst I) (length qs)"
  assumes welldefined2: "list_constr (snd I) (length qs)"
  shows "((p  set (retrieve_polys qs (fst I)). poly p x = 0)  (poly (prod_list (retrieve_polys qs (snd I))) x < 0))  (z_R I sign = -1)"
proof -
  have set_hyp: "sign  set (characterize_consistent_signs_at_roots p qs)" 
    using in_set_R[of p x sign qs] nonzero root_p sign_fix  by blast 
  have z_hyp: "((z_R I sign = 1)  (z_R I sign = 0)  (z_R I sign = -1))" 
    using welldefined1 welldefined2 set_hyp  z_lemma_R[where sign="sign", where I = "I", where p="p", where qs="qs"] by blast
  have d1: "((p  set (retrieve_polys qs (fst I)). poly p x = 0)  (poly (prod_list (retrieve_polys qs (snd I))) x < 0))  (z_R I sign = -1)"
    using horiz_vector_helper_pos_R
    using nonzero root_p sign_fix welldefined1 welldefined2
    by (smt (verit, ccfv_threshold) horiz_vector_helper_pos_ind_R1 horiz_vector_helper_zer_ind_R2 mem_Collect_eq mult_eq_0_iff z_R_def z_hyp) 
  have d2: "(z_R I sign = -1)  ((p  set (retrieve_polys qs (fst I)). poly p x = 0)  (poly (prod_list (retrieve_polys qs (snd I))) x < 0))" 
    using horiz_vector_helper_pos_ind_R1 horiz_vector_helper_zer_ind_R2 nonzero root_p sign_fix welldefined1 welldefined2
    by (smt (verit, ccfv_threshold) class_field.neg_1_not_0 consistent_sign_vec_def consistent_signs_prop_R equal_neg_zero horiz_vector_helper_pos_ind_R2 length_map list_all_length list_constr_def mem_Collect_eq mem_Collect_eq mult_cancel_left1 mult_not_zero retrieve_polys_def z_R_def z_signs_R1 zero_neq_one)
  then show ?thesis using d1 d2
    by linarith 
qed

lemma lhs_dot_rewrite:
  fixes p:: "real poly"
  fixes qs:: "real poly list"
  fixes I:: "nat list*nat list" 
  fixes signs:: "rat list list"
  assumes nonzero: "p0"
  shows
    "(vec_of_list (mtx_row_R signs I)  (construct_lhs_vector_R p qs signs)) =
   sum_list (map (λs. (z_R I s)  *  rat_of_int (card {x. poly p x = 0  consistent_sign_vec qs x = s})) signs)"
proof -
  have "p  0" using nonzero by auto
  from construct_lhs_vector_cleaner[OF this]
  have rhseq: "construct_lhs_vector_R p qs signs =
    vec_of_list
    (map (λs. rat_of_int (card {x. poly p x = 0  consistent_sign_vec qs x = s})) signs)"
    using construct_lhs_vector_cleaner_R nonzero by presburger
  have "(vec_of_list (mtx_row_R signs I)  (construct_lhs_vector_R p qs signs)) =    
    sum_list (map2 (*) (mtx_row_R signs I) (map (λs. rat_of_int (card {x. poly p x = 0  consistent_sign_vec qs x = s})) signs))"
    unfolding rhseq 
    apply (intro vec_of_list_dot_rewrite)
    by (auto simp add: mtx_row_R_def)
  thus ?thesis unfolding mtx_row_R_def
    using map2_map_map 
    by (auto simp add: map2_map_map)
qed

(* If we have a superset of the signs, we can drop to just the consistent ones *)
lemma construct_lhs_vector_drop_consistent_R:
  fixes p:: "real poly"
  fixes qs:: "real poly list"
  fixes I:: "nat list*nat list" 
  fixes signs:: "rat list list"
  assumes nonzero: "p0"
  assumes distinct_signs: "distinct signs"
  assumes all_info: "set (characterize_consistent_signs_at_roots p qs)  set(signs)"
  assumes welldefined1: "list_constr (fst I) (length qs)"
  assumes welldefined2: "list_constr (snd I) (length qs)"
  shows
    "(vec_of_list (mtx_row_R signs I)  (construct_lhs_vector_R p qs signs)) =
     (vec_of_list (mtx_row_R (characterize_consistent_signs_at_roots p qs) I) 
      (construct_lhs_vector_R p qs (characterize_consistent_signs_at_roots p qs)))"
proof - 
  have h0: " sgn. sgn  set signs  sgn  consistent_sign_vec qs ` set (characterize_root_list_p p)  
    0 < rat_of_nat (card  {xa. poly p xa = 0  consistent_sign_vec qs xa = sgn})  z_R I sgn = 0"
  proof - 
    have " sgn. sgn  set signs  sgn  consistent_sign_vec qs ` set (characterize_root_list_p p)  0 < rat_of_int (card
                  {xa. poly p xa = 0  consistent_sign_vec qs xa = sgn})  {xa. poly p xa = 0  consistent_sign_vec qs xa = sgn}  {}" 
      by fastforce
    then show ?thesis
    proof -
      { fix iis :: "rat list"
        have ff1: "0  p"
          using nonzero rsquarefree_def by blast
        obtain rr :: "(real  bool)  real" where
          ff2: "p. p (rr p)  Collect p = {}"
          by (metis Collect_empty_eq)
        { assume "is. is = iis  {r. poly p r = 0  consistent_sign_vec qs r = is}  {}"
          then have "is. consistent_sign_vec qs (rr (λr. poly p r = 0  consistent_sign_vec qs r = is)) = iis  {r. poly p r = 0  consistent_sign_vec qs r = is}  {}"
            using ff2
            by (metis (mono_tags, lifting))
          then have "r. poly p r = 0  consistent_sign_vec qs r = iis"
            using ff2
            by smt
          then have "iis  consistent_sign_vec qs ` set (sorted_list_of_set {r. poly p r = 0})"
            using ff1 poly_roots_finite
            by (metis (mono_tags) imageI mem_Collect_eq set_sorted_list_of_set) }
        then have "iis  set signs  iis  consistent_sign_vec qs ` set (characterize_root_list_p p)  ¬ 0 < rat_of_int (int (card {r. poly p r = 0  consistent_sign_vec qs r = iis}))"
          by (metis (no_types) sgn. sgn  set signs  sgn  consistent_sign_vec qs ` set (characterize_root_list_p p)  0 < rat_of_int (int (card {xa. poly p xa = 0  consistent_sign_vec qs xa = sgn}))  {xa. poly p xa = 0  consistent_sign_vec qs xa = sgn}  {} characterize_root_list_p_def) }
      then show ?thesis
        by fastforce
    qed
  qed
  then have " sgn. sgn  set signs  sgn  consistent_sign_vec qs ` set (characterize_root_list_p p)  ((0 = rat_of_nat (card
                  {xa. poly p xa = 0  consistent_sign_vec qs xa = sgn})  z_R I sgn = 0))"
    by auto
  then have hyp: " s. s  set signs  s  consistent_sign_vec qs ` set (characterize_root_list_p p)  (z_R I s * rat_of_nat (card {x. poly p x = 0  consistent_sign_vec qs x = s}) = 0)"
    by auto
  then have "(s set(signs). z_R I s * rat_of_nat (card {x. poly p x = 0  consistent_sign_vec qs x = s})) = 
        (s(set (signs)  (consistent_sign_vec qs ` set (characterize_root_list_p p))). z_R I s * rat_of_nat (card {x. poly p x = 0  consistent_sign_vec qs x = s}))"
  proof - 
    have "set(signs) =(set (signs)  (consistent_sign_vec qs ` set (characterize_root_list_p p))) 
              (set(signs)-(consistent_sign_vec qs ` set (characterize_root_list_p p)))"
      by blast
    then have sum_rewrite: "(s set(signs). z_R I s * rat_of_nat (card {x. poly p x = 0  consistent_sign_vec qs x = s})) =  
          (s (set (signs)  (consistent_sign_vec qs ` set (characterize_root_list_p p))) 
              (set(signs)-(consistent_sign_vec qs ` set (characterize_root_list_p p))). z_R I s * rat_of_nat (card {x. poly p x = 0  consistent_sign_vec qs x = s}))"
      by auto
    then have sum_split: "(s (set (signs)  (consistent_sign_vec qs ` set (characterize_root_list_p p))) 
              (set(signs)-(consistent_sign_vec qs ` set (characterize_root_list_p p))). z_R I s * rat_of_nat (card {x. poly p x = 0  consistent_sign_vec qs x = s}))
          = 
(s (set (signs)  (consistent_sign_vec qs ` set (characterize_root_list_p p))). z_R I s * rat_of_nat (card {x. poly p x = 0  consistent_sign_vec qs x = s}))
+ (s (set(signs)-(consistent_sign_vec qs ` set (characterize_root_list_p p))). z_R I s * rat_of_nat (card {x. poly p x = 0  consistent_sign_vec qs x = s}))"
      by (metis (no_types, lifting) List.finite_set sum.Int_Diff)
    have sum_zero: "(s (set(signs)-(consistent_sign_vec qs ` set (characterize_root_list_p p))). z_R I s * rat_of_nat (card {x. poly p x = 0  consistent_sign_vec qs x = s})) = 0"   
      using hyp
      by (simp add: hyp)      
    show ?thesis using sum_rewrite sum_split sum_zero by linarith
  qed
  then have set_eq: "set (remdups
           (map (consistent_sign_vec qs)
             (characterize_root_list_p p))) = set (signs)  (consistent_sign_vec qs ` set (characterize_root_list_p p))"
    using all_info apply (simp add: characterize_consistent_signs_at_roots_def subset_antisym)
    by (smt (z3) Int_subset_iff consistent_sign_vec_def list.set_map map_eq_conv o_apply signs_at_def squash_def subsetI subset_antisym)
  have hyp1: "(ssigns. z_R I s * rat_of_nat (card {x. poly p x = 0  consistent_sign_vec qs x = s})) = 
        (sset (signs). z_R I s * rat_of_nat (card {x. poly p x = 0  consistent_sign_vec qs x = s}))"
    using distinct_signs sum_list_distinct_conv_sum_set by blast
  have hyp2: "(sremdups
           (map (consistent_sign_vec qs)
             (characterize_root_list_p p)). z_R I s * rat_of_nat (card {x. poly p x = 0  consistent_sign_vec qs x = s}))
  = (s set (remdups
           (map (consistent_sign_vec qs)
             (characterize_root_list_p p))). z_R I s * rat_of_nat (card {x. poly p x = 0  consistent_sign_vec qs x = s}))"
    using sum_list_distinct_conv_sum_set by blast 
  have set_sum_eq: "(s(set (signs)  (consistent_sign_vec qs ` set (characterize_root_list_p p))). z_R I s * rat_of_nat (card {x. poly p x = 0  consistent_sign_vec qs x = s})) =
    (s set (remdups
           (map (consistent_sign_vec qs)
             (characterize_root_list_p p))). z_R I s * rat_of_nat (card {x. poly p x = 0  consistent_sign_vec qs x = s}))"
    using set_eq by auto
  then have "(ssigns. z_R I s * rat_of_nat (card {x. poly p x = 0  consistent_sign_vec qs x = s})) =
    (sremdups
           (map (consistent_sign_vec qs)
             (characterize_root_list_p p)). z_R I s * rat_of_nat (card {x. poly p x = 0  consistent_sign_vec qs x = s}))"
    using set_sum_eq hyp1 hyp2
    using (sset signs. z_R I s * rat_of_nat (card {x. poly p x = 0  consistent_sign_vec qs x = s})) = (sset signs  consistent_sign_vec qs ` set (characterize_root_list_p p). z_R I s * rat_of_nat (card {x. poly p x = 0  consistent_sign_vec qs x = s})) by linarith
  then have "consistent_sign_vec qs ` set (characterize_root_list_p p)  set signs 
    (p qss.
        characterize_consistent_signs_at_roots p qss =
        remdups (map (consistent_sign_vec qss) (characterize_root_list_p p))) 
    (ssigns. z_R I s * rat_of_nat (card {x. poly p x = 0  consistent_sign_vec qs x = s})) =
    (sremdups
           (map (consistent_sign_vec qs)
             (characterize_root_list_p p)). z_R I s * rat_of_nat (card {x. poly p x = 0  consistent_sign_vec qs x = s}))"
    by linarith
  then show ?thesis unfolding lhs_dot_rewrite[OF nonzero]
    apply (auto intro!: sum_list_distinct_filter simp add: distinct_signs  consistent_sign_vec_def characterize_consistent_signs_at_roots_def)
    using all_info consistent_sign_vec_def characterize_consistent_signs_at_roots_def
    by (smt (z3) list.set_map map_eq_conv o_apply set_remdups signs_at_def squash_def) 
qed

lemma matrix_equation_helper_step_R:
  fixes p:: "real poly"
  fixes qs:: "real poly list"
  fixes I:: "nat list*nat list" 
  fixes signs:: "rat list list"
  assumes nonzero: "p0"
  assumes distinct_signs: "distinct signs"
  assumes all_info: "set (characterize_consistent_signs_at_roots p qs)  set(signs)"
  assumes welldefined1: "list_constr (fst I) (length qs)"
  assumes welldefined2: "list_constr (snd I) (length qs)"
  shows "(vec_of_list (mtx_row_R signs I)  (construct_lhs_vector_R p qs signs)) =
   rat_of_int (card {x. poly p x = 0  (p  set (retrieve_polys qs (fst I)). poly p x = 0)  poly (prod_list (retrieve_polys qs (snd I))) x > 0}) -
   rat_of_int (card {x. poly p x = 0  (p  set (retrieve_polys qs (fst I)). poly p x = 0)  poly (prod_list (retrieve_polys qs (snd I))) x < 0})"
proof -
  have finset: "finite (set (map (consistent_sign_vec qs)  (characterize_root_list_p p)))" by auto
  let ?gt = "(set (map (consistent_sign_vec qs)  (characterize_root_list_p p))  {s. z_R I s = 1})"
  let ?lt = "  (set (map (consistent_sign_vec qs)  (characterize_root_list_p p))  {s. z_R I s = -1})"  
  let ?zer = "(set (map (consistent_sign_vec qs)  (characterize_root_list_p p))  {s. z_R I s = 0})"
  have eq: "set (map (consistent_sign_vec qs)  (characterize_root_list_p p)) = (?gt  ?lt)  ?zer"
  proof safe
    fix x
    assume h:"x  set (map (consistent_sign_vec qs) (characterize_root_list_p p))"
        "z_R I x  0" "z_R I x  - 1" 
    then have "x  set (characterize_consistent_signs_at_roots p qs)"
      unfolding characterize_consistent_signs_at_roots_def
      by (smt (verit, del_insts) characterize_consistent_signs_at_roots_def characterize_root_list_p_def imageE in_set_R nonzero poly_roots_finite set_map sorted_list_of_set(1))
    thus "z_R I x = 1"
      using h welldefined1 welldefined2 z_lemma_R by blast
  qed
  have sumeq: "(s(?gt?lt). z_R I s * rat_of_int (card {x. poly p x = 0  consistent_sign_vec qs x = s}))
  = (s?gt. z_R I s * rat_of_int (card {x. poly p x = 0  consistent_sign_vec qs x = s})) +
  (s?lt. z_R I s * rat_of_int (card {x. poly p x = 0  consistent_sign_vec qs x = s}))"
    apply (rule sum.union_disjoint) by auto
      (* First, drop the signs that are irrelevant *)
  from construct_lhs_vector_drop_consistent_R[OF assms(1-5)] have
    "vec_of_list (mtx_row_R signs I)  construct_lhs_vector_R p qs signs =
  vec_of_list (mtx_row_R (characterize_consistent_signs_at_roots p qs) I) 
  construct_lhs_vector_R p qs (characterize_consistent_signs_at_roots p qs)" .
    (* Now we split the sum *)
  from lhs_dot_rewrite[OF assms(1)]
  moreover have "... =
  (scharacterize_consistent_signs_at_roots p qs.
    z_R I s * rat_of_int (card {x. poly p x = 0  consistent_sign_vec qs x = s}))" .
  moreover have "... =
  (sset (map (consistent_sign_vec qs)  (characterize_root_list_p p)).
    z_R I s * rat_of_int (card {x. poly p x = 0  consistent_sign_vec qs x = s}))" unfolding characterize_consistent_signs_at_roots_def sum_code[symmetric]
    apply (auto)
    by (smt (verit, best) consistent_sign_vec_def list.set_map map_eq_conv o_apply signs_at_def squash_def sum.set_conv_list) 
  moreover have setc1:"... = 
  (s(?gt?lt). z_R I s * rat_of_int (card {x. poly p x = 0  consistent_sign_vec qs x = s})) +
    (s?zer. z_R I s * rat_of_int (card {x. poly p x = 0  consistent_sign_vec qs x = s})) "
    apply (subst eq) 
    apply (rule  sum.union_disjoint) by auto
  ultimately have setc: "... =
  (s?gt. z_R I s * rat_of_int (card {x. poly p x = 0  consistent_sign_vec qs x = s})) +
  (s?lt. z_R I s * rat_of_int (card {x. poly p x = 0  consistent_sign_vec qs x = s})) +
  (s?zer. z_R I s * rat_of_int (card {x. poly p x = 0  consistent_sign_vec qs x = s}))"
    using sumeq by auto
  have "s  ?zer. (z_R I s * rat_of_int (card {x. poly p x = 0  consistent_sign_vec qs x = s})) = 0"
    by auto
  then have obvzer: "(s?zer. z_R I s * rat_of_int (card {x. poly p x = 0  consistent_sign_vec qs x = s})) = 0"
    by auto
  (* Now recharacterize lt, gt*)
  have setroots: "set (characterize_root_list_p p) = {x. poly p x = 0}" unfolding characterize_root_list_p_def
    using poly_roots_finite nonzero rsquarefree_def set_sorted_list_of_set by blast    
  have *: "s. {x. poly p x = 0  consistent_sign_vec qs x = s} =
        {x {x. poly p x = 0}. consistent_sign_vec qs x = s}"
    by auto
  have e1: "(sconsistent_sign_vec qs ` {x. poly p x = 0}  {s. z_R I s = 1}.
       card {x. poly p x = 0  consistent_sign_vec qs x = s}) =
     (sum (λx. if (p  set (retrieve_polys qs (fst I)). poly p x = 0)  (poly (prod_list (retrieve_polys qs (snd I))) x) > 0 then 1 else 0) {x. poly p x = 0})"
    unfolding * apply (rule sum_multicount_gen)
    using finite (set (map (consistent_sign_vec qs) (characterize_root_list_p p))) setroots apply auto[1]
     apply (metis List.finite_set setroots)
  proof safe
    fix x
    assume rt: "poly p x = 0"
    then have 1: "{s  consistent_sign_vec qs ` {x. poly p x = 0}  {s. z_R I s = 1}. consistent_sign_vec qs x = s} =
      {s. z_R I s = 1  consistent_sign_vec qs x = s}"
      by auto
    have 2: "... = {s. (p  set (retrieve_polys qs (fst I)). poly p x = 0)  (0 < poly (prod_list (retrieve_polys qs (snd I))) x)   consistent_sign_vec qs x = s}"
      using horiz_vector_helper_pos_R assms welldefined1 welldefined2 rt by blast
    have 3: "... = (if (p  set (retrieve_polys qs (fst I)). poly p x = 0)  (0 < poly (prod_list (retrieve_polys qs (snd I))) x)  then {consistent_sign_vec qs x} else {})"
      by auto
    then have "card {s  consistent_sign_vec qs ` {x. poly p x = 0}  {s. z_R I s = 1}. consistent_sign_vec qs x = s} =
         (if ((p  set (retrieve_polys qs (fst I)). poly p x = 0)  0 < poly (prod_list  (retrieve_polys qs (snd I))) x)
          then 1 else 0)" using 1 2 3 by auto
    thus " card
          {s  consistent_sign_vec qs ` {x. poly p x = 0}  {s. z_R I s = 1}.
           consistent_sign_vec qs x = s} =
         (if (pset (retrieve_polys qs (fst I)). poly p x = 0) 
             0 < poly (prod_list (retrieve_polys qs (snd I))) x
          then 1 else 0)" 
      by auto
  qed

  have gtchr: "(s?gt. z_R I s * rat_of_int (card {x. poly p x = 0  consistent_sign_vec qs x = s})) =
    rat_of_int (card {x. poly p x = 0  (pset (retrieve_polys qs (fst I)). poly p x = 0)  0 < poly (prod_list (retrieve_polys qs (snd I))) x})"
    apply (auto simp add: setroots)
    apply (subst of_nat_sum[symmetric])
    apply (subst of_nat_eq_iff)
    apply (subst e1)
    apply (subst card_eq_sum)
    apply (rule sum.mono_neutral_cong_right)
       apply (metis List.finite_set setroots)
    by auto
  have e2: " (sconsistent_sign_vec qs ` {x. poly p x = 0}  {s. z_R I s = - 1}.
       card {x. poly p x = 0  consistent_sign_vec qs x = s}) =
     (sum (λx. if (pset (retrieve_polys qs (fst I)). poly p x = 0)  (poly (prod_list (retrieve_polys qs (snd I))) x) < 0 then 1 else 0) {x. poly p x = 0})"
    unfolding * apply (rule sum_multicount_gen)
    using finite (set (map (consistent_sign_vec qs) (characterize_root_list_p p))) setroots apply auto[1]
     apply (metis List.finite_set setroots)
  proof safe
    fix x
    assume rt: "poly p x = 0"
    then have 1: "{s  consistent_sign_vec qs ` {x. poly p x = 0}  {s. z_R I s = -1}. consistent_sign_vec qs x = s} =
      {s. z_R I s = -1  consistent_sign_vec qs x = s}"
      by auto
    have 2: "... = {s. ((pset (retrieve_polys qs (fst I)). poly p x = 0)  0 > poly (prod_list (retrieve_polys qs (snd I))) x)   consistent_sign_vec qs x = s}"
      using horiz_vector_helper_neg_R assms rt welldefined1 welldefined2 by blast
    have 3: "... = (if (pset (retrieve_polys qs (fst I)). poly p x = 0)  (0 > poly (prod_list (retrieve_polys qs (snd I))) x)  then {consistent_sign_vec qs x} else {})"
      by auto
    thus "card {s  consistent_sign_vec qs ` {x. poly p x = 0}  {s. z_R I s = -1}. consistent_sign_vec qs x = s} =
         (if (pset (retrieve_polys qs (fst I)). poly p x = 0)  0 > poly
                  (prod_list
                    (retrieve_polys qs (snd I)))
                  x
          then 1 else 0)" using 1 2 3 by auto
  qed
  have ltchr: "(s?lt. z_R I s * rat_of_int (card {x. poly p x = 0  consistent_sign_vec qs x = s})) =
    - rat_of_int (card {x. poly p x = 0  (pset (retrieve_polys qs (fst I)). poly p x = 0)  0 > poly (prod_list (retrieve_polys qs (snd I))) x})"
    apply (auto simp add: setroots sum_negf)
    apply (subst of_nat_sum[symmetric])
    apply (subst of_nat_eq_iff)
    apply (subst e2)
    apply (subst card_eq_sum)
    apply (rule sum.mono_neutral_cong_right)
       apply (metis List.finite_set setroots)
    by auto
  show ?thesis using gtchr ltchr obvzer setc
    using (scharacterize_consistent_signs_at_roots p qs. z_R I s * rat_of_int (int (card {x. poly p x = 0  consistent_sign_vec qs x = s}))) = (sset (map (consistent_sign_vec qs) (characterize_root_list_p p)). z_R I s * rat_of_int (int (card {x. poly p x = 0  consistent_sign_vec qs x = s}))) vec_of_list (mtx_row_R (characterize_consistent_signs_at_roots p qs) I)  construct_lhs_vector_R p qs (characterize_consistent_signs_at_roots p qs) = (scharacterize_consistent_signs_at_roots p qs. z_R I s * rat_of_int (int (card {x. poly p x = 0  consistent_sign_vec qs x = s}))) vec_of_list (mtx_row_R signs I)  construct_lhs_vector_R p qs signs = vec_of_list (mtx_row_R (characterize_consistent_signs_at_roots p qs) I)  construct_lhs_vector_R p qs (characterize_consistent_signs_at_roots p qs) setc1 by linarith
qed  

lemma matrix_equation_main_step_R:
  fixes p:: "real poly"
  fixes qs:: "real poly list"
  fixes I:: "nat list*nat list" 
  fixes signs:: "rat list list"
  assumes nonzero: "p0"
  assumes distinct_signs: "distinct signs"
  assumes all_info: "set (characterize_consistent_signs_at_roots p qs)  set(signs)"
  assumes welldefined1: "list_constr (fst I) (length qs)"
  assumes welldefined2: "list_constr (snd I) (length qs)"
  shows "(vec_of_list (mtx_row_R signs I) 
          (construct_lhs_vector_R p qs signs)) =  
    construct_NofI_R p (retrieve_polys qs (fst I)) (retrieve_polys qs (snd I))"
proof -
  show ?thesis
    unfolding construct_NofI_prop_R[OF nonzero]
    using matrix_equation_helper_step_R[OF assms]
    by linarith
qed

lemma mtx_row_length_R:
  "list_all (λr. length r = length signs) (map (mtx_row_R signs) ls)"
  apply (induction ls)
  by (auto simp add: mtx_row_R_def)

(* Shows that as long as we have a "basis" of sign assignments (see assumptions all_info, welldefined), 
  and some other mild assumptions on our inputs (given in nonzero, distinct_signs), the construction 
  will be satisfied *)
theorem matrix_equation_R:
  fixes p:: "real poly"
  fixes qs:: "real poly list"
  fixes subsets:: "(nat list*nat list) list" 
  fixes signs:: "rat list list"
  assumes nonzero: "p0"
  assumes distinct_signs: "distinct signs"
  assumes all_info: "set (characterize_consistent_signs_at_roots p qs)  set(signs)"
  assumes welldefined: "all_list_constr_R (subsets) (length qs)"
  shows "satisfy_equation_R p qs subsets signs"
  unfolding satisfy_equation_R_def matrix_A_R_def
    construct_lhs_vector_R_def construct_rhs_vector_R_def all_list_constr_R_def
  apply (subst mult_mat_vec_of_list)
    apply (auto simp add: mtx_row_length_R intro!: map_vec_vec_of_list_eq_intro)
  using matrix_equation_main_step_R[OF assms(1-3), unfolded construct_lhs_vector_R_def]
  using all_list_constr_R_def in_set_member welldefined by fastforce

(* Prettifying some theorems*)

lemma consistent_signs_at_roots_eq:
  assumes "p  0"
  shows "consistent_signs_at_roots p qs =
         set (characterize_consistent_signs_at_roots p qs)"
  unfolding consistent_signs_at_roots_def characterize_consistent_signs_at_roots_def
    characterize_root_list_p_def
  apply auto
   apply (subst set_sorted_list_of_set)
  using assms poly_roots_finite apply blast
  unfolding sgn_vec_def sgn_def signs_at_def squash_def o_def
  using roots_def apply auto[1]
    by (smt Collect_cong assms image_iff poly_roots_finite roots_def sorted_list_of_set(1))

abbreviation w_vec_R:: "real poly  real poly list  rat list list   rat vec"
  where "w_vec_R  construct_lhs_vector_R"

abbreviation v_vec_R:: "real poly  real poly list  (nat list*nat list) list  rat vec"
  where "v_vec_R  construct_rhs_vector_R"

abbreviation M_mat_R:: "rat list list  (nat list*nat list) list  rat mat"
  where "M_mat_R  matrix_A_R"

theorem matrix_equation_pretty:
  fixes subsets:: "(nat list*nat list) list"
  assumes "p0"
  assumes "distinct signs"
  assumes "consistent_signs_at_roots p qs  set signs"
  assumes "a b i. (a, b)  set ( subsets)  (i  set a  i  set b)  i < length qs"
  shows "M_mat_R signs subsets *v w_vec_R p qs signs = v_vec_R p qs subsets"
  unfolding satisfy_equation_R_def[symmetric]
  using matrix_equation_R[of p signs qs subsets] assms 
  using consistent_signs_at_roots_eq unfolding all_list_constr_R_def list_constr_def apply (auto)
  by (metis (no_types, lifting) Ball_set in_set_member)

section "Base Case"
definition satisfies_properties_R:: "real poly  real poly list  (nat list*nat list) list  rat list list  rat mat  bool"
  where "satisfies_properties_R p qs subsets signs matrix = 
  ( all_list_constr_R subsets (length qs)  well_def_signs (length qs) signs  distinct signs
   satisfy_equation_R p qs subsets signs   invertible_mat matrix   matrix = matrix_A_R signs subsets
   set (characterize_consistent_signs_at_roots p qs)  set(signs)
  )"

lemma mat_base_case_R:
  shows "matrix_A_R [[1],[0],[-1]] [([], []),([0], []),([], [0])] = (mat_of_rows_list 3 [[1,1,1], [0,1,0], [1,0,-1]])"
  unfolding matrix_A_R_def mtx_row_R_def z_R_def map_sgas_def apply (auto)
  by (simp add: numeral_3_eq_3)

lemma base_case_sgas_R:
  fixes q p:: "real poly"
  assumes nonzero: "p  0"
  shows "set (characterize_consistent_signs_at_roots p [q])  {[1],[0], [- 1]}"
  unfolding characterize_consistent_signs_at_roots_def signs_at_def  apply (auto)
  by (meson squash_def) 

lemma base_case_sgas_alt_R:
  fixes p:: "real poly"
  fixes qs:: "real poly list"
  assumes len1: "length qs = 1"
  assumes nonzero: "p  0"
  shows "set (characterize_consistent_signs_at_roots p qs)  {[1], [0], [- 1]}"
proof - 
  have ex_q: "(q::real poly). qs = [q]" 
    using len1    
    using length_Suc_conv[of qs 0] by auto
  then show ?thesis using base_case_sgas_R nonzero 
    by auto
qed

lemma base_case_satisfy_equation_R:
  fixes q p:: "real poly"
  assumes nonzero: "p  0"
  shows "satisfy_equation_R p [q] [([], []),([0], []),([], [0])] [[1],[0],[-1]] "
proof - 
  have h1: "set (characterize_consistent_signs_at_roots p [q])  {[1], [0],[- 1]}"
    using base_case_sgas_R assms by auto
  have h2: "all_list_constr_R [([], []),([0], []),([], [0])] (Suc 0)" unfolding all_list_constr_R_def
    by (simp add: list_constr_def member_def)
  then show ?thesis using matrix_equation_R[where p = "p", where qs = "[q]", where signs = "[[1],[0],[-1]] ", where subsets = "[([], []),([0], []),([], [0])]"]
      nonzero h1  h2 by auto
qed

lemma base_case_satisfy_equation_alt_R:
  fixes p:: "real poly"
  fixes qs:: "real poly list"
  assumes len1: "length qs = 1"
  assumes nonzero: "p  0"
  shows "satisfy_equation_R p qs [([], []),([0], []),([], [0])] [[1],[0],[-1]]"
proof - 
  have ex_q: "(q::real poly). qs = [q]" 
    using len1    
    using length_Suc_conv[of qs 0] by auto
  then show ?thesis using base_case_satisfy_equation_R nonzero
    by auto
qed

lemma base_case_matrix_eq:
  fixes q p:: "real poly"
  assumes nonzero: "p  0"
  shows "(mult_mat_vec (mat_of_rows_list 3 [[1,1,1], [0,1,0], [1,0,-1]]) (construct_lhs_vector_R p [q] [[1],[0],[-1]]) = 
    (construct_rhs_vector_R p [q] [([], []),([0], []),([], [0])]))"                      
  using mat_base_case_R base_case_satisfy_equation_R unfolding satisfy_equation_R_def
  by (simp add: nonzero)

lemma less_three: "(n::nat) < Suc (Suc (Suc 0))  n = 0  n = 1  n = 2"
  by auto

lemma inverse_mat_base_case_R:
  shows "inverts_mat (mat_of_rows_list 3  [[1/2, -1/2, 1/2], [0, 1, 0], [1/2, -1/2, -1/2]]::rat mat) (mat_of_rows_list 3 [[1,1,1], [0,1,0], [1,0,-1]]::rat mat)"
  unfolding inverts_mat_def mat_of_rows_list_def mat_eq_iff apply auto
  unfolding less_three by (auto simp add: scalar_prod_def)

lemma inverse_mat_base_case_2_R: 
  shows "inverts_mat (mat_of_rows_list 3 [[1,1,1], [0,1,0], [1,0,-1]]::rat mat) (mat_of_rows_list 3  [[1/2, -1/2, 1/2], [0, 1, 0], [1/2, -1/2, -1/2]]:: rat mat)"
  unfolding inverts_mat_def mat_of_rows_list_def mat_eq_iff apply auto
  unfolding less_three by (auto simp add: scalar_prod_def)

lemma base_case_invertible_mat_R: 
  shows "invertible_mat (matrix_A_R [[1],[0], [- 1]] [([], []),([0], []),([], [0])])"
  unfolding invertible_mat_def using inverse_mat_base_case_R inverse_mat_base_case_2_R
  apply (auto)
  apply (simp add: mat_base_case mat_of_rows_list_def)
  using mat_base_case_R by auto 

section "Inductive Step"

(***** Need some properties of smashing; smashing signs is just as it was in BKR *****)
subsection "Lemmas on smashing subsets "

definition subsets_first_component_list::"(nat list*nat list) list  nat list list"
  where "subsets_first_component_list I = map (λI. (fst I)) I"

definition subsets_second_component_list::"(nat list*nat list) list  nat list list"
  where "subsets_second_component_list I = map (λI. (snd I)) I"

definition smash_list_list::"('a list*'a list) list   ('a list*'a list) list  ('a list*'a list) list"
  where "smash_list_list s1 s2 = concat (map (λl1. map (λl2. (fst l1 @ fst l2, snd l1 @ snd l2)) s2) s1)"

lemma smash_list_list_property_set:
  fixes l1 l2 :: "('a list*'a list) list"
  fixes a b:: "nat"
  shows " (elem :: ('a list*'a list)). (elem  (set (smash_list_list l1 l2))  
    ( (elem1:: ('a list*'a list)).  (elem2:: ('a list*'a list)). 
      (elem1  set(l1)  elem2  set(l2)  elem = (fst elem1@ fst elem2, snd elem1 @ snd elem2))))"
proof clarsimp 
  fix a b 
  assume assum: "(a, b)  set (smash_list_list l1 l2)"
  show "aa ba. (aa, ba)  set l1  (ab bb. (ab, bb)  set l2  a = aa @ ab  b = ba @ bb)"
    using assum unfolding smash_list_list_def 
    apply (auto) by blast 
qed


lemma subsets_smash_property_R:
  fixes subsets1 subsets2 :: "(nat list*nat list) list"
  fixes n:: "nat"
  shows " (elem :: nat list*nat list). (List.member (subsets_smash_R n subsets1 subsets2) elem)  
    ( (elem1::nat list*nat list).  (elem2::nat list*nat list).
      (elem1  set(subsets1)  elem2  set(subsets2)  elem = ((fst elem1) @ (map ((+) n) (fst elem2)), (snd elem1) @ (map ((+) n) (snd elem2)))))"
proof -
  let ?fst_component2 = "subsets_first_component_list subsets2"
  let ?snd_component2 = "subsets_second_component_list subsets2"
  let ?new_subsets = "map (λI. ((map ((+) n)) (fst I),  (map ((+) n)) (snd I))) subsets2"
    (* a slightly unorthodox use of signs_smash, but it closes the proof *)
  have "subsets_smash_R n subsets1 subsets2 = smash_list_list subsets1 ?new_subsets" 
    unfolding subsets_smash_R_def smash_list_list_def apply (auto)
    by (simp add: comp_def) 
  then show ?thesis using smash_list_list_property_set[of subsets1 ?new_subsets] apply (auto)
    using imageE in_set_member set_map smash_list_list_property_set
    by (smt (z3) prod.exhaust_sel)
qed

(* If subsets for smaller systems are well-defined, then subsets for combined systems are, too *)
subsection "Well-defined subsets preserved when smashing"

lemma well_def_step_R: 
  fixes qs1 qs2 :: "real poly list"
  fixes subsets1 subsets2 :: "(nat list*nat list) list"
  assumes well_def_subsets1: "all_list_constr_R (subsets1) (length qs1)"
  assumes well_def_subsets2: "all_list_constr_R (subsets2) (length qs2)"
  shows "all_list_constr_R ((subsets_smash_R (length qs1) subsets1 subsets2))
     (length (qs1 @ qs2))"
proof - 
  let ?n = "(length qs1)"
  have h1: "elem.
     List.member (subsets_smash_R ?n subsets1 subsets2) elem 
     ( (elem1::nat list*nat list).  (elem2::nat list*nat list).
      (elem1  set(subsets1)  elem2  set(subsets2)  elem = ((fst elem1) @ (map ((+) ?n) (fst elem2)), (snd elem1) @ (map ((+) ?n) (snd elem2)))))"
    using