diff --git a/thys/BenOr_Kozen_Reif/BKR_Decision.thy b/thys/BenOr_Kozen_Reif/BKR_Decision.thy --- a/thys/BenOr_Kozen_Reif/BKR_Decision.thy +++ b/thys/BenOr_Kozen_Reif/BKR_Decision.thy @@ -1,2034 +1,2031 @@ theory BKR_Decision imports BKR_Algorithm "Berlekamp_Zassenhaus.Factorize_Rat_Poly" "Algebraic_Numbers.Real_Roots" "BKR_Proofs" "HOL.Deriv" begin section "Algorithm" subsection "Parsing" (* Formula type *) datatype 'a fml = And "'a fml" "'a fml" | Or "'a fml" "'a fml" | Gt 'a (* 'a > 0 *) | Geq 'a (* 'a \ 0 *) | Lt 'a (* 'a < 0 *) | Leq 'a (* 'a \ 0 *) | Eq 'a (* 'a = 0 *) | Neq 'a (* 'a \ 0 *) (* Evaluating a formula over a lookup semantics where 'a is nat *) primrec lookup_sem :: "nat fml \ ('a::linordered_field list) \ bool" where "lookup_sem (And l r) ls = (lookup_sem l ls \ lookup_sem r ls)" | "lookup_sem (Or l r) ls = (lookup_sem l ls \ lookup_sem r ls)" | "lookup_sem (Gt p) ls = (ls ! p > 0)" | "lookup_sem (Geq p) ls = (ls ! p \ 0)" | "lookup_sem (Lt p) ls = (ls ! p < 0)" | "lookup_sem (Leq p) ls = (ls ! p \ 0)" | "lookup_sem (Eq p) ls = (ls ! p = 0)" | "lookup_sem (Neq p) ls = (ls ! p \ 0)" (* (compute) all polynomials mentioned in a formula *) primrec poly_list :: "'a fml \ 'a list" where "poly_list (And l r) = poly_list l @ poly_list r" | "poly_list (Or l r) = poly_list l @ poly_list r" | "poly_list (Gt p) = [p]" | "poly_list (Geq p) = [p]" | "poly_list (Lt p) = [p]" | "poly_list (Leq p) = [p]" | "poly_list (Eq p) = [p]" | "poly_list (Neq p) = [p]" primrec index_of_aux :: "'a list \ 'a \ nat \ nat" where "index_of_aux [] y n = n" | "index_of_aux (x#xs) y n = (if x = y then n else index_of_aux xs y (n+1))" definition index_of :: "'a list \ 'a \ nat" where "index_of xs y = index_of_aux xs y 0" definition convert :: "'a fml \ (nat fml \ 'a list)" where "convert fml = ( let ps = remdups (poly_list fml) in (map_fml (index_of ps) fml, ps) )" subsection "Factoring" (* Makes sure the result of factorize_rat_poly is monic *) definition factorize_rat_poly_monic :: "rat poly \ (rat \ (rat poly \ nat) list)" where "factorize_rat_poly_monic p = ( let (c,fs) = factorize_rat_poly p ; lcs = prod_list (map (\(f,i). (lead_coeff f) ^ Suc i) fs) ; fs = map (\(f,i). (normalize f, i)) fs in (c * lcs,fs) )" (* Factoring an input list of polynomials *) definition factorize_polys :: "rat poly list \ (rat poly list \ (rat \ (nat \ nat) list) list)" where "factorize_polys ps = ( let fact_ps = map factorize_rat_poly_monic ps; factors = remdups (map fst (concat (map snd fact_ps))) ; data = map (\(c,fs). (c, map (\(f,pow). (index_of factors f, pow) ) fs)) fact_ps in (factors,data) )" (* After turning a polynomial into factors, this turns a sign condition on the factors into a sign condition for the polynomial *) definition undo_factorize :: "rat \ (nat \ nat) list \ rat list \ rat" where "undo_factorize cfs signs = squash (case cfs of (c,fs) \ (c * prod_list (map (\(f,pow). (signs ! f) ^ Suc pow) fs))) " definition undo_factorize_polys :: "(rat \ (nat \ nat) list) list \ rat list \ rat list" where "undo_factorize_polys ls signs = map (\l. undo_factorize l signs) ls" subsection "Auxiliary Polynomial" definition crb:: "real poly \ int" where "crb p = ceiling (2 + max_list_non_empty (map (\ i. norm (coeff p i)) [0 ..< degree p]) / norm (lead_coeff p))" (* Because we are using prod_list instead of lcm, it's important that this is called when ps is pairwise coprime. *) definition coprime_r :: "real poly list \ real poly" where "coprime_r ps = pderiv (prod_list ps) * ([:-(crb (prod_list ps)),1:]) * ([:(crb (prod_list ps)),1:])" subsection "Setting Up the Procedure" (* 0 indexed *) definition insertAt :: "nat \ 'a \ 'a list \ 'a list" where "insertAt n x ls = take n ls @ x # (drop n ls)" (* 0 indexed *) definition removeAt :: "nat \ 'a list \ 'a list" where "removeAt n ls = take n ls @ (drop (n+1) ls)" definition find_sgas_aux:: "real poly list \ rat list list" where "find_sgas_aux in_list = concat (map (\i. map (\v. insertAt i 0 v) (find_consistent_signs_at_roots (in_list ! i) (removeAt i in_list)) ) [0.. rat list list" where "find_sgas ps = ( let r = coprime_r ps in find_consistent_signs_at_roots r ps @ find_sgas_aux ps )" (* Putting the sign condition preprocessing together with BKR *) definition find_consistent_signs :: "rat poly list \ rat list list" where "find_consistent_signs ps = ( let (fs,data) = factorize_polys ps; sgas = find_sgas (map (map_poly of_rat) fs); rsgas = map (undo_factorize_polys data) sgas in (if fs = [] then [(map (\x. if poly x 0 < 0 then -1 else if poly x 0 = 0 then 0 else 1) ps)] else rsgas) )" subsection "Deciding Univariate Problems" definition decide_universal :: "rat poly fml \ bool" where [code]: "decide_universal fml = ( let (fml_struct,polys) = convert fml; conds = find_consistent_signs polys in list_all (lookup_sem fml_struct) conds )" definition decide_existential :: "rat poly fml \ bool" where [code]: "decide_existential fml = ( let (fml_struct,polys) = convert fml; conds = find_consistent_signs polys in find (lookup_sem fml_struct) conds \ None )" section "Proofs" subsection "Parsing and Semantics" (* Evaluating a formula where 'a is a real poly *) primrec real_sem :: "real poly fml \ real \ bool" where "real_sem (And l r) x = (real_sem l x \ real_sem r x)" | "real_sem (Or l r) x = (real_sem l x \ real_sem r x)" | "real_sem (Gt p) x = (poly p x > 0)" | "real_sem (Geq p) x = (poly p x \ 0)" | "real_sem (Lt p) x = (poly p x < 0)" | "real_sem (Leq p) x = (poly p x \ 0)" | "real_sem (Eq p) x = (poly p x = 0)" | "real_sem (Neq p) x = (poly p x \ 0)" (* Evaluating a formula where 'a is a rat poly *) primrec fml_sem :: "rat poly fml \ real \ bool" where "fml_sem (And l r) x = (fml_sem l x \ fml_sem r x)" | "fml_sem (Or l r) x = (fml_sem l x \ fml_sem r x)" | "fml_sem (Gt p) x = (rpoly p x > 0)" | "fml_sem (Geq p) x = (rpoly p x \ 0)" | "fml_sem (Lt p) x = (rpoly p x < 0)" | "fml_sem (Leq p) x = (rpoly p x \ 0)" | "fml_sem (Eq p) x = (rpoly p x = 0)" | "fml_sem (Neq p) x = (rpoly p x \ 0)" lemma poly_list_set_fml: shows "set (poly_list fml) = set_fml fml" apply (induction) by auto lemma convert_semantics_lem: assumes "\p. p \ set (poly_list fml) \ ls ! (index_of ps p) = rpoly p x" shows "fml_sem fml x = lookup_sem (map_fml (index_of ps) fml) ls" using assms apply (induct fml) by auto lemma index_of_aux_more: shows "index_of_aux ls p n \ n" apply (induct ls arbitrary: n) apply auto using Suc_leD by blast lemma index_of_aux_lookup: assumes "p \ set ls" shows "(index_of_aux ls p n) - n < length ls" "ls ! ((index_of_aux ls p n) - n) = p" using assms apply (induct ls arbitrary: n) apply auto apply (metis Suc_diff_Suc index_of_aux_more lessI less_Suc_eq_0_disj less_le_trans) by (metis Suc_diff_Suc index_of_aux_more lessI less_le_trans nth_Cons_Suc) lemma index_of_lookup: assumes "p \ set ls" shows "index_of ls p < length ls" "ls ! (index_of ls p) = p" apply (metis assms index_of_aux_lookup(1) index_of_def minus_nat.diff_0) by (metis assms index_of_aux_lookup(2) index_of_def minus_nat.diff_0) lemma convert_semantics: shows "fml_sem fml x = lookup_sem (fst (convert fml)) (map (\p. rpoly p x) (snd (convert fml)))" unfolding convert_def Let_def apply simp apply (intro convert_semantics_lem) by (simp add: index_of_lookup(1) index_of_lookup(2)) lemma convert_closed: shows "\i. i \ set_fml (fst (convert fml)) \ i < length (snd (convert fml))" unfolding convert_def Let_def apply (auto simp add: fml.set_map) by (simp add: index_of_lookup(1) poly_list_set_fml) (* Rational sign vector of polynomials qs with rational coefficients at x *) definition sign_vec::"rat poly list \ real \ rat list" where "sign_vec qs x \ map (squash \ (\p. rpoly p x)) qs" (* The set of all rational sign vectors for qs wrt the set S When S = UNIV, then this quantifies over all reals *) definition consistent_sign_vectors::"rat poly list \ real set \ rat list set" where "consistent_sign_vectors qs S = (sign_vec qs) ` S" lemma sign_vec_semantics: assumes "\i. i \ set_fml fml \ i < length ls" shows "lookup_sem fml (map (\p. rpoly p x) ls) = lookup_sem fml (sign_vec ls x)" using assms apply (induction) by (auto simp add: sign_vec_def squash_def) (* The universal and existential decision procedure is easy if we know the consistent sign vectors *) lemma universal_lookup_sem: assumes "\i. i \ set_fml fml \ i < length qs" assumes "set signs = consistent_sign_vectors qs UNIV" shows "(\x::real. lookup_sem fml (map (\p. rpoly p x) qs)) \ list_all (lookup_sem fml) signs" using assms(2) unfolding consistent_sign_vectors_def list_all_iff by (simp add: assms(1) sign_vec_semantics) lemma existential_lookup_sem: assumes "\i. i \ set_fml fml \ i < length qs" assumes "set signs = consistent_sign_vectors qs UNIV" shows "(\x::real. lookup_sem fml (map (\p. rpoly p x) qs)) \ find (lookup_sem fml) signs \ None" using assms(2) unfolding consistent_sign_vectors_def find_None_iff by (simp add: assms(1) sign_vec_semantics) subsection "Factoring Lemmas" (*definition real_factorize_list:: "rat poly list \ real poly list" where "real_factorize_list qs = map (map_poly of_rat) (fst(factorize_polys qs))" *) interpretation of_rat_poly_hom: map_poly_comm_semiring_hom of_rat.. interpretation of_rat_poly_hom: map_poly_comm_ring_hom of_rat.. interpretation of_rat_poly_hom: map_poly_idom_hom of_rat.. lemma finite_prod_map_of_rat_poly_hom: shows "poly (real_of_rat_poly (\(a,b)\s. f a b)) y = (\(a,b)\s. poly (real_of_rat_poly (f a b)) y)" apply (simp add: of_rat_poly_hom.hom_prod poly_prod) by (simp add: case_prod_app prod.case_distrib) lemma sign_vec_index_of: assumes "f \ set ftrs" shows "sign_vec ftrs x ! (index_of ftrs f) = squash (rpoly f x)" by (simp add: assms index_of_lookup(1) index_of_lookup(2) sign_vec_def) lemma squash_idem: shows "squash (squash x) = squash x" unfolding squash_def by auto lemma squash_mult: shows "squash ((a::real) * b) = squash a * squash b" unfolding squash_def apply auto using less_not_sym mult_neg_neg apply blast using mult_less_0_iff by blast lemma squash_prod_list: shows "squash (prod_list (ls::real list)) = prod_list (map squash ls)" apply (induction ls) unfolding squash_def apply auto apply (simp add: mult_less_0_iff) by (simp add: zero_less_mult_iff) lemma squash_pow: shows "squash ((x::real) ^ (y::nat)) = (squash x) ^ y" unfolding squash_def apply auto by (auto simp add: zero_less_power_eq) lemma squash_real_of_rat[simp]: shows "squash (real_of_rat x) = squash x" unfolding squash_def by auto lemma factorize_rat_poly_monic_irreducible_monic: assumes "factorize_rat_poly_monic f = (c,fs)" assumes "(fi,i) \ set fs" shows "irreducible fi \ monic fi" proof - obtain c' fs' where cfs: "factorize_rat_poly f = (c',fs')" by (meson surj_pair) then have fs: "fs = map (\(f,i). (normalize f, i)) fs'" using factorize_rat_poly_monic_def assms by auto obtain "fi'" where "(fi',i) \ set fs'" "fi = normalize fi'" using assms(2) unfolding fs by auto thus ?thesis using factorize_rat_poly irreducible_normalize_iff by (metis cfs monic_normalize not_irreducible_zero) qed lemma square_free_normalize: assumes "square_free p" shows "square_free (normalize p)" by (metis assms square_free_multD(3) unit_factor_mult_normalize) lemma coprime_normalize: assumes "coprime a b" shows "coprime (normalize a) b" using assms by auto lemma undo_normalize: shows "a = Polynomial.smult (unit_factor (lead_coeff a)) (normalize a)" by (metis add.right_neutral mult_pCons_right mult_zero_right normalize_mult_unit_factor pCons_0_hom.hom_zero unit_factor_poly_def) lemma finite_smult_distr: assumes "distinct fs" shows "(\(x,y)\set fs. Polynomial.smult ((f x y)::rat) (g x y)) = Polynomial.smult (\(x,y)\set fs. f x y) (\(x,y)\set fs. g x y)" using assms proof (induction fs) case Nil then show ?case by auto next case (Cons a fs) then show ?case apply auto using mult.commute mult_smult_right prod.case_distrib smult_smult split_cong split_conv by (simp add: Groups.mult_ac(2) split_beta) qed lemma normalize_coprime_degree: assumes "normalize (f::rat poly) = normalize g" assumes "coprime f g" shows "degree f = 0" proof - have "f dvd g" by (simp add: assms(1) associatedD2) then have "f dvd 1" using assms(2) associatedD1 by auto thus ?thesis using Missing_Polynomial_Factorial.is_unit_field_poly by blast qed lemma factorize_rat_poly_monic_square_free_factorization: assumes res: "factorize_rat_poly_monic f = (c,fs)" shows "square_free_factorization f (c,fs)" proof (unfold square_free_factorization_def split, intro conjI impI allI) obtain c' fs' where cfs: "factorize_rat_poly f = (c',fs')" by (meson surj_pair) then have fs: "fs = map (\(f,i). (normalize f, i)) fs'" using factorize_rat_poly_monic_def assms by auto have sq: "square_free_factorization f (c',fs')" using cfs factorize_rat_poly(1) by blast obtain lcs where lcs: "lcs = prod_list (map (\(f,i). lead_coeff f ^ Suc i) fs')" by force have c: "c = c' * lcs" using assms unfolding factorize_rat_poly_monic_def cfs Let_def lcs by auto show "f = 0 \ c = 0" using c cfs by auto show "f = 0 \ fs = []" using fs cfs by auto have dist: "distinct fs'" using sq square_free_factorizationD(5) by blast show dist2: "distinct fs" unfolding fs unfolding distinct_conv_nth apply auto proof - fix i j assume ij: "i < length fs'" "j < length fs'" "i \ j" assume eq: "(case fs' ! i of (f, x) \ (normalize f, x)) = (case fs' ! j of (f, x) \ (normalize f, x))" obtain f a where fa: "fs' ! i = (f,a)" by force obtain g where g: "fs' ! j = (g,a)" "normalize f = normalize g" using eq fa apply auto by (metis case_prod_conv prod.collapse prod.inject) have "f \ g" using dist ij fa g using nth_eq_iff_index_eq by fastforce then have "coprime f g" using square_free_factorizationD(3)[OF sq, of f a g a] fa g ij apply auto using nth_mem by force then have "degree f = 0" by (simp add: g(2) normalize_coprime_degree) thus False using fa ij(1) nth_mem sq square_free_factorizationD'(3) by fastforce qed have ceq: "c = c' * (\(a, i)\set fs'. (lead_coeff a) ^ Suc i)" using c lcs by (simp add: dist prod.distinct_set_conv_list) have fseq: " (\(a, i)\set fs. a ^ Suc i) = (\(a, i)\set fs'. (normalize a) ^ Suc i)" apply (subst prod.distinct_set_conv_list[OF dist]) apply (subst prod.distinct_set_conv_list[OF dist2]) unfolding fs apply (auto simp add: o_def ) by (metis (no_types, lifting) case_prod_conv old.prod.exhaust) have "f = Polynomial.smult c' (\(a, i)\set fs'. a ^ Suc i)" using sq square_free_factorizationD(1) by blast moreover have "... = Polynomial.smult c' (\(a, i)\set fs'. (Polynomial.smult ((unit_factor (lead_coeff a))) (normalize a)) ^ Suc i)" apply (subst undo_normalize[symmetric]) by auto moreover have "... = Polynomial.smult c' (\(a, i)\set fs'. (Polynomial.smult ((lead_coeff a) ^ Suc i) ((normalize a) ^ Suc i)))" apply (subst smult_power) by auto moreover have "... = Polynomial.smult c' (Polynomial.smult (\(a, i)\set fs'. ((lead_coeff a) ^ Suc i)) (\(a, i)\set fs'. (normalize a) ^ Suc i))" apply (subst finite_smult_distr) by (auto simp add: dist) moreover have "... = Polynomial.smult (c' * (\(a, i)\set fs'. (lead_coeff a) ^ Suc i)) (\(a, i)\set fs'. (normalize a) ^ Suc i)" using smult_smult by blast moreover have "... = Polynomial.smult c (\(a, i)\set fs. a ^ Suc i)" unfolding ceq fseq by auto ultimately show "f = Polynomial.smult c (\(a, i)\set fs. a ^ Suc i)" by auto fix a i assume ai: "(a,i) \ set fs" obtain a' where a': "(a',i) \ set fs'" "a = normalize a'" using ai unfolding fs by auto show "square_free a" using square_free_normalize a' using sq square_free_factorizationD(2) by blast show "0 < degree a" using degree_normalize a' using sq square_free_factorizationD'(3) by fastforce fix b j assume bj: "(b,j) \ set fs" "(a,i) \ (b,j)" obtain b' where b': "(b',j) \ set fs'" "b = normalize b'" using bj unfolding fs by auto show "algebraic_semidom_class.coprime a b" using a' b' apply auto using bj(2) sq square_free_factorizationD(3) by fastforce qed lemma undo_factorize_correct: assumes "factorize_rat_poly_monic p = (c,fs)" assumes "\f p. (f,p) \ set fs \ f \ set ftrs" shows "undo_factorize (c,map (\(f,pow). (index_of ftrs f, pow)) fs) (sign_vec ftrs x) = squash (rpoly p x)" proof - have p: "p = smult c (\(a, i)\ set fs. a ^ Suc i)" using assms(1) factorize_rat_poly_monic_square_free_factorization square_free_factorizationD(1) by blast have fs: "distinct fs" using assms(1) factorize_rat_poly_monic_square_free_factorization square_free_factorizationD(5) by blast have "rpoly p x = ((real_of_rat c) * rpoly (\(a, i)\ set fs. a ^ Suc i) x)" using p by (simp add: of_rat_hom.map_poly_hom_smult) moreover have "... = ((real_of_rat c) * rpoly (\ai\ set fs. case ai of (a,i) \ a ^ Suc i) x)" by blast moreover have "... = ((real_of_rat c) * (\ai\ set fs. case ai of (a,i) \ rpoly (a ^ Suc i) x))" by (simp add: finite_prod_map_of_rat_poly_hom) moreover have "... = ((real_of_rat c) * (\ai\ set fs. case ai of (a,i) \ (rpoly a x) ^ Suc i))" by (metis (mono_tags, lifting) of_rat_poly_hom.hom_power poly_hom.hom_power split_cong) moreover have "... = ((real_of_rat c) * (prod_list (map (\ai. case ai of (a,i) \ (rpoly a x) ^ Suc i) fs)))" by (simp add: fs prod.distinct_set_conv_list) ultimately have "rpoly p x = ((real_of_rat c) * (prod_list (map (\ai. case ai of (a,i) \ (rpoly a x) ^ Suc i) fs)))" by auto then have "squash (rpoly p x) = squash c * prod_list (map squash (map (\ai. case ai of (a,i) \ (rpoly a x) ^ Suc i) fs))" by (auto simp add: squash_mult squash_prod_list o_def) moreover have "... = squash c * prod_list (map (\ai. case ai of (a,i) \ squash ((rpoly a x) ^ Suc i)) fs)" apply (simp add: o_def) by (simp add: prod.case_distrib) ultimately have rp:"squash(rpoly p x) = squash c * prod_list (map (\ai. case ai of (a,i) \ squash (rpoly a x) ^ Suc i) fs)" using squash_pow by presburger have "undo_factorize (c, map (\(f, pow).(index_of ftrs f, pow)) fs) (sign_vec ftrs x) = squash (c * (\xa\fs. case xa of (f, y) \ sign_vec ftrs x ! index_of ftrs f ^ Suc y))" unfolding undo_factorize_def apply (auto simp add: o_def) by (metis (mono_tags, lifting) case_prod_conv old.prod.exhaust) moreover have "... = squash (c * (\xa\fs. case xa of (f, y) \ (squash (rpoly f x)) ^ Suc y))" using assms(2) sign_vec_index_of map_eq_conv split_cong apply (auto) by (smt map_eq_conv split_cong) ultimately show ?thesis using rp by (metis (mono_tags, lifting) of_rat_hom.hom_mult squash_idem squash_mult squash_real_of_rat) qed lemma length_sign_vec[simp]: shows "length (sign_vec ps x) = length ps" unfolding sign_vec_def by auto lemma factorize_polys_has_factors: assumes "factorize_polys ps = (ftrs,data)" assumes "p \ set ps" assumes "factorize_rat_poly_monic p = (c,fs)" shows "set (map fst fs) \ set ftrs" using assms unfolding factorize_polys_def Let_def apply auto by (metis UN_iff fst_conv image_eqI snd_conv) lemma factorize_polys_undo_factorize_polys: assumes "factorize_polys ps = (ftrs,data)" shows "undo_factorize_polys data (sign_vec ftrs x) = sign_vec ps x" unfolding list_eq_iff_nth_eq undo_factorize_polys_def apply auto proof - show leq:"length data = length ps" using assms unfolding factorize_polys_def by (auto simp add: Let_def) fix i assume il:"i < length data" obtain c fs where cfs: "factorize_rat_poly_monic (ps ! i) = (c,fs)" by (meson surj_pair) then have fsts:"set (map fst fs) \ set ftrs" using assms factorize_polys_has_factors il leq nth_mem by fastforce have *:"data ! i = (c,map (\(f,pow). (index_of ftrs f, pow)) fs)" using assms unfolding factorize_polys_def using cfs il by (auto simp add: Let_def cfs) have "undo_factorize (data ! i) (sign_vec ftrs x) = squash (rpoly (ps ! i) x)" unfolding * apply (subst undo_factorize_correct[of "ps ! i"]) apply (auto simp add: cfs) using fsts by auto thus "undo_factorize (data ! i) (sign_vec ftrs x) = sign_vec ps x ! i" using leq il sign_vec_def by auto qed lemma factorize_polys_irreducible_monic: assumes "factorize_polys ps = (fs,data)" shows "distinct fs" "\f. f \ set fs \ irreducible f \ monic f" using assms unfolding factorize_polys_def Let_def apply auto using factorize_rat_poly_monic_irreducible_monic apply (metis prod.collapse) using factorize_rat_poly_monic_irreducible_monic by (metis prod.collapse) lemma factorize_polys_square_free: assumes "factorize_polys ps = (fs,data)" shows "\f. f \ set fs \ square_free f" using assms factorize_polys_irreducible_monic(2) irreducible_imp_square_free by blast lemma irreducible_monic_coprime: assumes f: "monic f" "irreducible (f::rat poly)" assumes g: "monic g" "irreducible (g::rat poly)" assumes "f \ g" shows "coprime f g" by (metis (no_types, lifting) assms(5) coprime_0(2) coprime_def' f(1) f(2) g(1) g(2) irreducible_normalized_divisors normalize_dvd_iff normalize_idem normalize_monic) lemma factorize_polys_coprime: assumes "factorize_polys ps = (fs,data)" shows "\f g. f \ set fs \ g \ set fs \ f \ g \ coprime f g" using assms factorize_polys_irreducible_monic(2) irreducible_monic_coprime by auto lemma coprime_rat_poly_real_poly: assumes "coprime p (q::rat poly)" shows "coprime (real_of_rat_poly p) ((real_of_rat_poly q)::real poly)" by (metis assms gcd_dvd_1 of_rat_hom.map_poly_gcd of_rat_poly_hom.hom_dvd_1) lemma coprime_rat_poly_iff_coprimereal_poly: shows "coprime p (q::rat poly) \ coprime (real_of_rat_poly p) ((real_of_rat_poly q)::real poly)" proof - have forward: "coprime p (q::rat poly) \ coprime (real_of_rat_poly p) ((real_of_rat_poly q)::real poly)" using coprime_rat_poly_real_poly by auto have backward: "coprime (real_of_rat_poly p) ((real_of_rat_poly q)::real poly) \ coprime p (q::rat poly)" proof - assume copr_real: "comm_monoid_mult_class.coprime (real_of_rat_poly p) (real_of_rat_poly q)" have "degree (gcd p (q::rat poly)) > 0 \ False" proof - assume deg: "degree (gcd p (q::rat poly)) > 0" then have "\y. y dvd p \ y dvd q \ degree y > 0" by blast then obtain y where yprop: "y dvd p \ y dvd q \ degree y > 0" by auto then have "(real_of_rat_poly y) dvd (real_of_rat_poly p) \ (real_of_rat_poly y ) dvd (real_of_rat_poly q) \ degree y > 0" by simp then show "False" using copr_real apply (auto) by fastforce qed then show "comm_monoid_mult_class.coprime p (q::rat poly)" using comm_monoid_gcd_class.gcd_dvd_1 by (metis Missing_Polynomial_Factorial.is_unit_field_poly copr_real gcd_zero_iff' neq0_conv of_rat_poly_hom.hom_zero) qed show ?thesis using forward backward by auto qed lemma factorize_polys_map_distinct: assumes "factorize_polys ps = (fs,data)" assumes "fss = map real_of_rat_poly fs" shows "distinct fss" using factorize_polys_irreducible_monic[OF assms(1)] unfolding assms(2) apply (simp add: distinct_conv_nth) by (metis of_rat_eq_iff of_rat_hom.coeff_map_poly_hom poly_eqI) lemma factorize_polys_map_square_free: assumes "factorize_polys ps = (fs,data)" assumes "fss = map real_of_rat_poly fs" shows "\f. f \ set fss \ square_free f" using factorize_polys_square_free[OF assms(1)] using assms(2) field_hom_0'.square_free_map_poly of_rat_hom.field_hom_0'_axioms by auto lemma factorize_polys_map_coprime: assumes "factorize_polys ps = (fs,data)" assumes "fss = map real_of_rat_poly fs" shows "\f g. f \ set fss \ g \ set fss \ f \ g \ coprime f g" using factorize_polys_coprime[OF assms(1)] coprime_rat_poly_real_poly unfolding assms(2) by auto lemma coprime_prod_list: assumes "\p. p \ set ps \ p \ 0" assumes "coprime (prod_list ps) (q::real poly)" shows "\p. p \ set ps \ coprime p q" proof - fix p assume "p \ set ps" then obtain r where r: "prod_list ps = r * p" using remove1_retains_prod by blast show "coprime p q" apply (rule coprime_prod[of r 1]) using assms r apply auto by blast qed (* basically copied from square_free_factorizationD' *) lemma factorize_polys_square_free_prod_list: assumes "factorize_polys ps = (fs,data)" shows "square_free (prod_list fs)" proof (rule square_freeI) from factorize_polys_coprime[OF assms] have coprime: "\p q. p \ set fs \ q \ set fs \ p \ q \ coprime p q" . from factorize_polys_square_free[OF assms] have sq: "\p. p \ set fs \ square_free p" . thus "prod_list fs \ 0" unfolding prod_list_zero_iff using square_free_def by blast fix q assume "degree q > 0" "q * q dvd prod_list fs" from irreducible\<^sub>d_factor[OF this(1)] this(2) obtain q where irr: "irreducible q" and dvd: "q * q dvd prod_list fs" unfolding dvd_def by auto hence dvd': "q dvd prod_list fs" unfolding dvd_def by auto from irreducible_dvd_prod_list[OF irr dvd'] obtain b where mem: "b \ set fs" and dvd1: "q dvd b" by auto from dvd1 obtain k where b: "b = q * k" unfolding dvd_def by auto from split_list[OF mem] b obtain bs1 bs2 where bs: "fs = bs1 @ b # bs2" by auto from irr have q0: "q \ 0" and dq: "degree q > 0" unfolding irreducible\<^sub>d_def by auto have "square_free (q * k)" using sq b mem by auto from this[unfolded square_free_def, THEN conjunct2, rule_format, OF dq] have qk: "\ q dvd k" by simp from dvd[unfolded bs b] have "q * q dvd q * (k * prod_list (bs1 @ bs2))" by (auto simp: ac_simps) with q0 have "q dvd k * prod_list (bs1 @ bs2)" by auto with irr qk have "q dvd prod_list (bs1 @ bs2)" by auto from irreducible_dvd_prod_list[OF irr this] obtain b' where mem': "b' \ set (bs1 @ bs2)" and dvd2: "q dvd b'" by fastforce from dvd1 dvd2 have "q dvd gcd b b'" by auto with dq is_unit_iff_degree[OF q0] have cop: "\ coprime b b'" by force from mem' have "b' \ set fs" unfolding bs by auto have b': "b' = b" using coprime using \b' \ set fs\ cop mem by blast with mem' bs factorize_polys_irreducible_monic(1)[OF assms] show False by auto qed lemma factorize_polys_map_square_free_prod_list: assumes "factorize_polys ps = (fs,data)" assumes "fss = map real_of_rat_poly fs" shows "square_free (prod_list fss)" using factorize_polys_square_free_prod_list[OF assms(1)] unfolding assms(2) by (simp add: of_rat_hom.square_free_map_poly) lemma factorize_polys_map_coprime_pderiv: assumes "factorize_polys ps = (fs,data)" assumes "fss = map real_of_rat_poly fs" shows "\f. f \ set fss \ coprime f (pderiv (prod_list fss))" proof - fix f assume f: "f \ set fss" from factorize_polys_map_square_free[OF assms] have sq: "\p. p \ set fss \ square_free p" . have z: "\p. p \ set fss \ p \ 0" using sq square_free_def by blast have c: "coprime (prod_list fss) (pderiv (prod_list fss))" apply (simp add: separable_def[symmetric] square_free_iff_separable[symmetric]) using factorize_polys_map_square_free_prod_list[OF assms] . from coprime_prod_list[OF z c f] show "coprime f (pderiv (prod_list fss))" by auto qed definition pairwise_coprime_list:: "rat poly list \ bool" where "pairwise_coprime_list qs = (\m < length qs. \ n < length qs. m \ n \ coprime (qs ! n) (qs ! m))" (* Restating factorize_polys_map_coprime to match later definitions *) lemma coprime_factorize: fixes qs:: "rat poly list" shows "pairwise_coprime_list (fst(factorize_polys qs))" proof - let ?fs = "fst(factorize_polys qs)" have "(\m < length ?fs. \ n < length ?fs. m \ n \ coprime (?fs ! n) (?fs ! m))" proof clarsimp fix m n assume "m < length (fst (factorize_polys qs))" assume "n < length (fst (factorize_polys qs))" assume "m \ n" show " algebraic_semidom_class.coprime (fst (factorize_polys qs) ! n) (fst (factorize_polys qs) ! m)" by (metis \m < length (fst (factorize_polys qs))\ \m \ n\ \n < length (fst (factorize_polys qs))\ coprime_iff_coprime distinct_conv_nth factorize_polys_coprime factorize_polys_def factorize_polys_irreducible_monic(1) fstI nth_mem) qed then show ?thesis unfolding pairwise_coprime_list_def by auto qed lemma squarefree_factorization_degree: assumes "square_free_factorization p (c,fs)" shows "degree p = sum_list (map (\(f,c). (c+1) * degree f) fs)" proof - have "p = Polynomial.smult c (\(a, i)\set fs. a ^ Suc i)" using assms unfolding square_free_factorization_def by blast then have "degree p = degree (\(a, i)\set fs. a ^ Suc i)" using assms square_free_factorizationD(4) by fastforce also have "... = degree (prod_list (map (\(f,c). f ^ Suc c) fs))" by (metis assms prod.distinct_set_conv_list square_free_factorizationD(5)) also have "... = (\(a, i)\fs. degree (a ^ Suc i))" apply (subst degree_prod_list_eq) apply (auto simp add: o_def) using assms degree_0 square_free_factorizationD(2) apply blast using assms degree_0 square_free_factorizationD(2) apply blast by (simp add: prod.case_distrib) ultimately show ?thesis by (smt Polynomial.degree_power_eq add.commute assms degree_0 map_eq_conv plus_1_eq_Suc split_cong square_free_factorizationD(2)) qed subsection "Auxiliary Polynomial Lemmas" definition roots_of_coprime_r:: "real poly list \ real set" where "roots_of_coprime_r qs = {x. poly (coprime_r qs) x = 0}" lemma crb_lem_pos: fixes x:: "real" fixes p:: "real poly" assumes x: "poly p x = 0" assumes p: "p \ 0" shows "x < crb p" using cauchy_root_bound[of p x] apply (auto) unfolding crb_def apply (auto) using p x by linarith lemma crb_lem_neg: fixes x:: "real" fixes p:: "real poly" assumes x: "poly p x = 0" assumes p: "p \ 0" shows "x > -crb p" using cauchy_root_bound[of p x] apply (auto) unfolding crb_def apply (auto) using p x by linarith (* Show that the product of the polynomial list is 0 at x iff there is a polynomial in the list that is 0 at x *) lemma prod_zero: shows "\x . poly (prod_list (qs:: rat poly list)) x = 0 \ (\q \ set (qs). poly q x = 0)" apply auto using poly_prod_list_zero_iff apply blast using poly_prod_list_zero_iff by blast lemma coprime_r_zero1: "poly (coprime_r qs) (crb (prod_list qs)) = 0" by (simp add: coprime_r_def) lemma coprime_r_zero2: "poly (coprime_r qs) (-crb (prod_list qs)) = 0" by (simp add: coprime_r_def) lemma coprime_mult: fixes a:: "real poly" fixes b:: "real poly" fixes c:: "real poly" assumes "algebraic_semidom_class.coprime a b" assumes "algebraic_semidom_class.coprime a c" shows "algebraic_semidom_class.coprime a (b*c)" using assms(1) assms(2) by auto (* Will be needed when we call the BKR roots on coprime_r *) lemma coprime_r_coprime_prop: fixes ps:: "rat poly list" assumes "factorize_polys ps = (fs,data)" assumes "fss = map real_of_rat_poly fs" shows "\f. f \ set fss \ coprime f (coprime_r fss)" proof clarsimp fix f:: "real poly" assume f_in: "f \ set fss" have nonz_prod: "prod_list fss \ 0" using factorize_polys_map_square_free apply (auto) using assms(1) assms(2) square_free_def by fastforce have nonz_f: "f \ 0" using f_in factorize_polys_map_square_free apply (auto) using assms(1) assms(2) square_free_def by fastforce have copr_pderiv: "algebraic_semidom_class.coprime f (pderiv (prod_list fss))" using factorize_polys_map_coprime_pderiv apply (auto) using f_in assms(1) assms(2) by auto have z_iff: "\x. poly f x = 0 \ poly (prod_list fss) x = 0" using f_in apply (auto) using poly_prod_list_zero_iff by blast let ?inf_p = "[:-(crb (prod_list fss)),1:]::real poly" have copr_inf: "algebraic_semidom_class.coprime f ([:-(crb (prod_list fss)),1:])" proof - have zero_prop: "\x. poly ?inf_p x = 0 \ x = crb (prod_list fss)" by auto have "poly (prod_list fss) (crb (prod_list fss)) \ 0" proof - have h: "\x. poly (prod_list fss) x = 0 \ x < (crb (prod_list fss))" using nonz_prod crb_lem_pos[where p = "prod_list fss"] by auto then show ?thesis by auto qed then have nonzero: "poly f (crb (prod_list fss)) \ 0" using z_iff by auto then have "\(\x. poly f x = 0 \ poly ?inf_p x = 0)" by simp have is_unit_gcd: "is_unit (gcd ?inf_p f)" using prime_elem_imp_gcd_eq prime_elem_iff_irreducible linear_irreducible_field apply (auto) using nonzero proof - have f1: "\x0. - (x0::real) = - 1 * x0" by simp have "(1::real) \ 0" by auto then have "is_unit (gcd (pCons (- 1 * real_of_int (crb (prod_list fss))) 1) f)" using f1 by (metis (no_types) is_unit_gcd nonzero one_poly_eq_simps(1) poly_eq_0_iff_dvd prime_elem_imp_coprime prime_elem_linear_field_poly) then show "degree (gcd (pCons (- real_of_int (crb (prod_list fss))) 1) f) = 0" by simp qed then show ?thesis using is_unit_gcd by (metis gcd.commute gcd_eq_1_imp_coprime is_unit_gcd_iff) qed let ?ninf_p = "[:(crb (prod_list fss)),1:]::real poly" have copr_neg_inf: "algebraic_semidom_class.coprime f ([:(crb (prod_list fss)),1:])" proof - have h: "\x. poly f x = 0 \ poly (prod_list fss) x = 0" using f_in apply (auto) using poly_prod_list_zero_iff by blast have zero_prop: "\x. poly ?ninf_p x = 0 \ x = -crb (prod_list fss)" by auto have "poly (prod_list fss) (-crb (prod_list fss)) \ 0" proof - have h: "\x. poly (prod_list fss) x = 0 \ x > (-crb (prod_list fss))" using nonz_prod crb_lem_neg[where p = "prod_list fss"] by auto then show ?thesis by auto qed then have nonzero: "poly f (-crb (prod_list fss)) \ 0" using z_iff by auto then have "\(\x. poly f x = 0 \ poly ?ninf_p x = 0)" using zero_prop by auto have is_unit_gcd: "is_unit (gcd ?ninf_p f)" using prime_elem_imp_gcd_eq prime_elem_iff_irreducible linear_irreducible_field apply (auto) using nonzero proof - have f1: "(1::real) \ 0" by auto have "\ pCons (real_of_int (crb (prod_list fss))) 1 dvd f" using nonzero by auto then show "degree (gcd (pCons (real_of_int (crb (prod_list fss))) 1) f) = 0" using f1 by (metis (no_types) Missing_Polynomial_Factorial.is_unit_field_poly coprime_imp_gcd_eq_1 is_unit_gcd_iff one_poly_eq_simps(1) prime_elem_imp_coprime prime_elem_linear_field_poly) qed then show ?thesis using is_unit_gcd by (metis gcd.commute gcd_eq_1_imp_coprime is_unit_gcd_iff) qed show "algebraic_semidom_class.coprime f (coprime_r fss)" using copr_pderiv coprime_mult unfolding coprime_r_def using copr_inf copr_neg_inf by blast qed lemma coprime_r_nonzero: fixes ps:: "rat poly list" assumes "factorize_polys ps = (fs,data)" assumes nonempty_fs: "fs \ []" assumes fss_is: "fss = map real_of_rat_poly fs" shows "(coprime_r fss) \ 0" proof - have nonempty_fss: "fss \ []" using nonempty_fs fss_is by auto have deg_f: "\f \ set (fs). degree f > 0" using factorize_polys_irreducible_monic apply (auto) using assms(1) irreducible_degree_field by blast then have deg_fss: "\f \ set (fss). degree f > 0" using fss_is by simp then have fss_nonz: "\f \ set (fss). f \ 0" by auto have "fss \ [] \ ((\f \ set (fss). (degree f > 0 \ f \ 0)) \ degree (prod_list fss) > 0)" proof (induct fss) case Nil then show ?case by blast next case (Cons a fss) show ?case proof clarsimp assume z_lt: "0 < degree a" assume anonz: "a \ 0" assume fnonz: "\f\set fss. 0 < degree f \ f \ 0" have h: "degree (a * prod_list fss) = degree a + degree (prod_list fss) " using degree_mult_eq[where p = "a", where q = "prod_list fss"] anonz fnonz by auto then show "0 < degree (a * prod_list fss)" using z_lt Cons.hyps by auto qed qed then have "degree (prod_list fss) > 0" using nonempty_fss deg_fss fss_nonz by auto then have pderiv_nonzero: "pderiv (prod_list fss) \ 0" by (simp add: pderiv_eq_0_iff) have "(([:-(crb (prod_list fss)),1:]) * ([:(crb (prod_list fss)),1:])) \ 0" by auto then show ?thesis using pderiv_nonzero unfolding coprime_r_def apply (auto) by (metis offset_poly_eq_0_lemma right_minus_eq synthetic_div_unique_lemma) qed lemma Rolle_pderiv: fixes q:: "real poly" fixes x1 x2:: "real" shows "(x1 < x2 \ poly q x1 = 0 \ poly q x2 = 0) \ (\w. x1 < w \ w < x2 \ poly (pderiv q) w = 0)" using Rolle_deriv apply (auto) by (metis DERIV_unique Rolle continuous_at_imp_continuous_on poly_DERIV poly_differentiable poly_isCont) lemma coprime_r_roots_prop: fixes qs:: "real poly list" assumes pairwise_rel_prime: "\q1 q2. (q1 \ q2 \ (List.member qs q1) \ (List.member qs q2))\ coprime q1 q2" shows "\x1. \x2. ((x1 < x2 \ (\q1 \ set (qs). (poly q1 x1) = 0) \ (\q2\ set(qs). (poly q2 x2) = 0)) \ (\q. x1 < q \ q < x2 \ poly (coprime_r qs) q = 0))" proof clarsimp fix x1:: "real" fix x2:: "real" fix q1:: "real poly" fix q2:: "real poly" assume "x1 < x2" assume q1_in: "q1 \ set qs" assume q1_0: "poly q1 x1 = 0" assume q2_in: "q2 \ set qs" assume q2_0: "poly q2 x2 = 0" have prod_z_x1: "poly (prod_list qs) x1 = 0" using q1_in q1_0 using poly_prod_list_zero_iff by blast have prod_z_x2: "poly (prod_list qs) x2 = 0" using q2_in q2_0 using poly_prod_list_zero_iff by blast have "\w>x1. w < x2 \ poly (pderiv (prod_list qs)) w = 0" using Rolle_pderiv[where q = "prod_list qs"] prod_z_x1 prod_z_x2 using \x1 < x2\ by blast then obtain w where w_def: "w > x1 \w < x2 \ poly (pderiv (prod_list qs)) w = 0" by auto then have "poly (coprime_r qs) w = 0" unfolding coprime_r_def by simp then show "\q>x1. q < x2 \ poly (coprime_r qs) q = 0" using w_def by blast qed subsection "Setting Up the Procedure: Lemmas" definition has_no_zeros::"rat list \ bool" where "has_no_zeros l = (0 \ set l)" lemma hnz_prop: "has_no_zeros l \ \(\k < length l. l ! k = 0)" unfolding has_no_zeros_def by (simp add: in_set_conv_nth) definition cast_rat_list:: "rat poly list \ real poly list" where "cast_rat_list qs = map real_of_rat_poly qs" definition consistent_sign_vectors_r::"real poly list \ real set \ rat list set" where "consistent_sign_vectors_r qs S = (signs_at qs) ` S" lemma consistent_sign_vectors_consistent_sign_vectors_r: shows"consistent_sign_vectors_r (cast_rat_list qs) S = consistent_sign_vectors qs S" unfolding consistent_sign_vectors_r_def cast_rat_list_def consistent_sign_vectors_def sign_vec_def signs_at_def by auto (* Relies on coprime_rat_poly_real_poly *) lemma coprime_over_reals_coprime_over_rats: fixes qs:: "rat poly list" assumes csa_in: "csa \ (consistent_sign_vectors qs UNIV)" assumes p1p2: "p1\p2 \ p1 < length csa \ p2 < length csa \ csa ! p1 = 0 \ csa ! p2 = 0" shows "\ algebraic_semidom_class.coprime (nth qs p1) (nth qs p2) " proof - have isx: "\(x::real). csa = (sign_vec qs x)" using csa_in unfolding consistent_sign_vectors_def by auto then obtain x where havex: "csa = (sign_vec qs x)" by auto then have expolys: "poly (real_of_rat_poly (nth qs p1)) x = 0 \ poly (real_of_rat_poly (nth qs p2)) x = 0" using havex unfolding sign_vec_def squash_def by (smt class_field.neg_1_not_0 length_map map_map nth_map one_neq_zero p1p2) then have "\ coprime (real_of_rat_poly (nth qs p1)) ((real_of_rat_poly (nth qs p2))::real poly)" apply (auto) using coprime_poly_0 by blast then show ?thesis using coprime_rat_poly_real_poly by auto qed (* This and the following lemma are designed to show that if you have two sgas that aren't the same, there's a 0 in between! The proof uses IVT. It hones in on the component that's changed sign (either from 1 to {0, -1} or from -1 to {0, 1}) *) lemma zero_above: fixes qs:: "rat poly list" fixes x1:: "real" assumes hnz: "has_no_zeros (sign_vec qs x1)" shows "(\ x2 > x1. ((sign_vec qs x1) \ (sign_vec qs x2)) \ (\(r::real) > x1. (r \ x2 \ (\ q \ set(qs). rpoly q r = 0))))" proof clarsimp fix x2 assume x1_lt: "x1 < x2" assume diff_sign_vec: "sign_vec qs x1 \ sign_vec qs x2" then have "\q \ set qs. squash (rpoly q x1) \ squash (rpoly q x2)" unfolding sign_vec_def by simp then obtain q where q_prop: "q \ set qs \ squash (rpoly q x1) \ squash (rpoly q x2)" by auto then have q_in: "q \ set qs" by auto have poss1: "squash (rpoly q x1) = -1 \ squash (rpoly q x2) = 1 \ (\r>x1. r \ x2 \ (\q\set qs. rpoly q r = 0))" using poly_IVT_pos[of x1 x2] using x1_lt unfolding squash_def apply (auto) using q_prop by fastforce have poss2: "squash (rpoly q x1) = 1 \ squash (rpoly q x2) = -1 \ (\r>x1. r \ x2 \ (\q\set qs. rpoly q r = 0))" using poly_IVT_neg[of x1 x2] using x1_lt unfolding squash_def apply (auto) using q_prop by fastforce have poss3: "squash (rpoly q x2) = 0 \ (\r>x1. r \ x2 \ (\q\set qs. rpoly q r = 0))" using x1_lt unfolding squash_def apply (auto) using q_prop by blast have "(q \ set qs \ rpoly q x1 = 0) \ \has_no_zeros (sign_vec qs x1)" unfolding has_no_zeros_def sign_vec_def apply auto by (smt image_iff squash_def) have not_poss4: "squash (rpoly q x1) \ 0" using hnz q_in unfolding squash_def using \q \ set qs \ rpoly q x1 = 0 \ \ has_no_zeros (sign_vec qs x1)\ by auto then show "\r>x1. r \ x2 \ (\q\set qs. rpoly q r = 0)" using q_prop poss1 poss2 poss3 not_poss4 apply (auto) apply (meson squash_def) apply (metis squash_def) apply (metis squash_def) by (meson squash_def) qed lemma zero_below: fixes qs:: "rat poly list" fixes x1:: "real" assumes hnz: "has_no_zeros (sign_vec qs x1)" shows "\x2 < x1. ((sign_vec qs x1) \ (sign_vec qs x2)) \ (\(r::real) < x1. (r \ x2 \ (\ q \ set(qs). rpoly q r = 0)))" proof clarsimp fix x2 assume x1_gt: "x2 < x1" assume diff_sign_vec: "sign_vec qs x1 \ sign_vec qs x2" then have "\q \ set qs. squash (rpoly q x1) \ squash (rpoly q x2)" unfolding sign_vec_def by simp then obtain q where q_prop: "q \ set qs \ squash (rpoly q x1) \ squash (rpoly q x2)" by auto then have q_in: "q \ set qs" by auto have poss1: "squash (rpoly q x1) = -1 \ squash (rpoly q x2) = 1 \ (\r x2 \ (\ q \ set(qs). rpoly q r = 0)))" using poly_IVT_neg[of x2 x1] using x1_gt unfolding squash_def apply (auto) using q_prop by fastforce have poss2: "squash (rpoly q x1) = 1 \ squash (rpoly q x2) = -1 \ (\r x2 \ (\ q \ set(qs). rpoly q r = 0)))" using poly_IVT_pos[of x2 x1] using x1_gt unfolding squash_def apply (auto) using q_prop by fastforce have poss3: "squash (rpoly q x2) = 0 \ (\r x2 \ (\ q \ set(qs). rpoly q r = 0)))" using x1_gt unfolding squash_def apply (auto) using q_prop by blast have "(q \ set qs \ rpoly q x1 = 0) \ \has_no_zeros (sign_vec qs x1)" unfolding has_no_zeros_def sign_vec_def apply auto using image_iff squash_def by (smt image_iff squash_def) have not_poss4: "squash (rpoly q x1) \ 0" using hnz q_in unfolding squash_def using \q \ set qs \ rpoly q x1 = 0 \ \ has_no_zeros (sign_vec qs x1)\ by auto then show "(\r x2 \ (\ q \ set(qs). rpoly q r = 0)))" using q_prop poss1 poss2 poss3 not_poss4 apply (auto) apply (meson squash_def) apply (metis squash_def) apply (metis squash_def) by (meson squash_def) qed lemma sorted_list_lemma: fixes l:: "real list" fixes a b:: "real" fixes n:: "nat" assumes "a < b" assumes "(n + 1) < length l" - assumes strict_sort: "strict_sorted l" + assumes strict_sort: "sorted_wrt (<) l" assumes lt_a: "(l ! n) < a" assumes b_lt: "b < (l ! (n+1))" shows "\(\(x::real). (List.member l x \ a \ x \ x \ b))" proof - have sorted_hyp_var: "\q1 < length l. \q2 < length l. (q1 < q2 \ (l ! q1) < (l ! q2))" - apply (auto) - by (metis (no_types, lifting) strict_sort sorted_wrt_iff_nth_less strict_sorted_sorted_wrt) + using strict_sort by (auto simp: sorted_wrt_iff_nth_less) then have sorted_hyp_var2: "\q1 < length l. \q2 < length l. ((l ! q1) < (l ! q2)) \ q1 < q2" using linorder_neqE_nat by (metis Groups.add_ac(2) add_mono_thms_linordered_field(5) less_irrefl) have "(\(x::real). (List.member l x \ a \ x \ x \ b)) \ False" proof - assume "(\(x::real). (List.member l x \ a \ x \ x \ b))" then obtain x where x_prop: "List.member l x \ a \ x \ x \ b" by auto then have l_prop: "List.member l x \ (l ! n) < x \ x < (l ! (n+1))" using lt_a b_lt by auto have nth_l: "l ! n < x" using l_prop by auto have np1th_l: "x < l ! (n+1)" using l_prop by auto have "\k. k < length l \ nth l k = x" using l_prop by (meson in_set_member index_of_lookup(1) index_of_lookup(2)) then obtain k where k_prop: "k < length l \ nth l k = x" by auto have n_lt: "n < k" using nth_l sorted_hyp_var k_prop add_lessD1 assms(2) linorder_neqE_nat nat_SN.gt_trans by (meson sorted_hyp_var2) have k_gt: "k < n + 1" using sorted_hyp_var np1th_l k_prop using assms(2) sorted_hyp_var2 by blast show False using n_lt k_gt by auto qed then show ?thesis by auto qed (* This lemma shows that any zero of coprime_r is either between two roots or it's smaller than the least root (neg inf) or it's greater than the biggest root (pos inf). *) lemma roots_of_coprime_r_location_property: fixes qs:: "rat poly list" fixes sga:: "rat list" fixes zer_list assumes pairwise_rel_prime: "pairwise_coprime_list qs" assumes all_squarefree: "\q. q \ set qs \ rsquarefree q" assumes x1_prop: "sga = sign_vec qs x1" assumes hnz: "has_no_zeros sga" assumes zer_list_prop: "zer_list = sorted_list_of_set {(x::real). (\q \ set(qs). (rpoly q x = 0))}" shows "zer_list \ [] \ ((x1 < (zer_list ! 0)) \ (x1 > (zer_list ! (length zer_list - 1)) \ (\ n < (length zer_list - 1). x1 > (zer_list ! n) \ x1 < (zer_list ! (n+1)))))" proof - let ?zer_list = "sorted_list_of_set {(x::real). (\q \ set(qs). (rpoly q x = 0))} :: real list" show ?thesis proof - have "((\q. (List.member qs q) \ q \ 0) \ has_no_zeros (sign_vec qs x1)) \ \ List.member ?zer_list x1" proof (induct qs) case Nil then show ?case apply (auto) by (simp add: member_rec(2)) next case (Cons a qs) then show ?case proof clarsimp assume imp: "((\q. List.member qs q \ q \ 0) \ has_no_zeros (sign_vec qs x1) \ \ List.member (sorted_list_of_set {x. \q\set qs. rpoly q x = 0}) x1)" assume nonz: "\q. List.member (a # qs) q \ q \ 0" assume hnz: " has_no_zeros (sign_vec (a # qs) x1)" assume mem_list: "List.member (sorted_list_of_set {x. rpoly a x = 0 \ (\q\set qs. rpoly q x = 0)}) x1" have "has_no_zeros (sign_vec (a # qs) x1) \ has_no_zeros (sign_vec qs x1)" proof - assume hnz: "has_no_zeros (sign_vec (a # qs) x1)" have same_vec: "sign_vec (a # qs) x1 = ((if rpoly a x1 > 0 then 1 else if rpoly a x1 = 0 then 0 else -1) # sign_vec (qs) x1)" unfolding sign_vec_def squash_def by auto have "has_no_zeros ((if rpoly a x1 > 0 then 1 else if rpoly a x1 = 0 then 0 else -1) # sign_vec (qs) x1) \ has_no_zeros (sign_vec (qs) x1)" by (simp add: has_no_zeros_def) then show "has_no_zeros (sign_vec qs x1)" using hnz same_vec by auto qed then have nmem: "\ List.member (sorted_list_of_set {x. \q\set qs. rpoly q x = 0}) x1" using hnz nonz imp apply (auto) by (simp add: member_rec(1)) have "\q \set qs. q \ 0" using nonz using in_set_member apply (auto) by fastforce then have "\q \set qs. finite {x. rpoly q x = 0}" by (simp add: poly_roots_finite) then have fin_set: "finite {x. \q\set qs. rpoly q x = 0}" by auto have not_in: "x1 \ {x. \q\set qs. rpoly q x = 0}" using fin_set nmem set_sorted_list_of_set all_squarefree apply (auto) by (simp add: List.member_def \finite {x. \q\set qs. rpoly q x = 0}\) have x1_in: "x1 \ {x. rpoly a x = 0 \ (\q\set qs. rpoly q x = 0)}" using mem_list sorted_list_of_set proof - have f1: "\r R. ((r::real) \ R \ \ List.member (sorted_list_of_set R) r) \ infinite R" by (metis in_set_member set_sorted_list_of_set) have "finite {r. rpoly a (r::real) = 0}" by (metis (full_types) List.finite_set member_rec(1) nonz real_roots_of_rat_poly(1)) then show ?thesis using f1 \finite {x. \q\set qs. rpoly q x = 0}\ mem_list by fastforce qed have "rpoly a x1 \ 0" using hnz unfolding has_no_zeros_def sign_vec_def squash_def by auto then show "False" using not_in x1_in by auto qed qed then have non_mem: "\ List.member ?zer_list x1" using all_squarefree unfolding rsquarefree_def hnz apply (auto) using hnz x1_prop by (simp add: in_set_member) have "?zer_list \ [] \ ((x1 \ (?zer_list ! 0)) \ (x1 \ (?zer_list ! (length ?zer_list - 1)))) \ (\ n < (length ?zer_list - 1). x1 > (?zer_list ! n) \ x1 < (?zer_list ! (n+1)))" proof - assume "?zer_list \ []" assume x1_asm: "(x1 \ (?zer_list ! 0)) \ (x1 \ (?zer_list ! (length ?zer_list - 1)))" have nm1: "x1 \ ?zer_list ! 0" using non_mem using \sorted_list_of_set {x. \q\set qs. rpoly q x = 0} \ []\ in_set_member by (metis (no_types, lifting) in_set_conv_nth length_greater_0_conv) have nm2: "x1 \ ?zer_list ! (length ?zer_list -1)" using non_mem by (metis (no_types, lifting) One_nat_def \sorted_list_of_set {x. \q\set qs. rpoly q x = 0} \ []\ diff_Suc_less in_set_member length_greater_0_conv nth_mem) then have x_asm_var: "x1 > (?zer_list ! 0) \ x1 < ?zer_list ! (length ?zer_list -1)" using x1_asm nm1 nm2 by auto have "(\n. (n < (length ?zer_list - 1) \ x1 \ (?zer_list ! n) \ x1 \ (?zer_list ! (n+1)))) \ False" proof - assume assump: "(\n. (n < (length ?zer_list - 1) \ x1 \ (?zer_list ! n) \ x1 \ (?zer_list ! (n+1))))" have zer_case: "x1 \ ?zer_list ! 0" using x_asm_var by auto have all_n: "\ n. (n < (length ?zer_list - 1) \ x1 \ ?zer_list ! n) " proof - fix n show n_lt: "(n < (length ?zer_list - 1) \ x1 \ ?zer_list ! n)" proof (induct n) case 0 then show ?case using zer_case by blast next case (Suc n) then show ?case using assump using Suc_eq_plus1 Suc_lessD by presburger qed qed have "(length ?zer_list - 2) \ length ?zer_list -1" using diff_le_mono2 one_le_numeral by blast have "x1 \ ?zer_list ! (length ?zer_list - 1)" proof - have h1: "length ?zer_list = 1 \ x1 \ ?zer_list ! (length ?zer_list - 1)" using assump zer_case by auto have h2: "length ?zer_list > 1 \ x1 \ ?zer_list ! (length ?zer_list - 1)" using all_n assump apply (auto) by (metis (mono_tags, lifting) Suc_diff_Suc lessI) then show ?thesis using h1 h2 apply (auto) using zer_case by blast qed then show False using all_n x_asm_var by linarith qed then show ?thesis using x1_asm by (smt One_nat_def Suc_pred \sorted_list_of_set {x. \q\set qs. rpoly q x = 0} \ []\ in_set_member length_greater_0_conv less_SucI non_mem nth_mem) qed then have h1: "(?zer_list \ [] \ (x1 \ (?zer_list ! 0)) \ (x1 \ (?zer_list ! (length ?zer_list - 1))) \ (\ n < (length ?zer_list - 1). x1 > (?zer_list ! n) \ x1 < (?zer_list ! (n+1))))" by blast then show ?thesis apply (auto) using zer_list_prop not_less by auto qed qed (* This lemma is essentially saying that the zeros of coprime_r capture all relevant sample points. From roots_of_coprime_r_location_property, we know that any zero of coprime_r is either between two roots, or it's smaller than the least root (neg inf), or it's greater than the biggest root (pos inf). Then, since the polynomials have constant signs within those intervals, the zeros of coprime_r capture all the relevant information. *) lemma roots_of_coprime_r_capture_sgas_without_zeros: fixes qs:: "rat poly list" fixes sga:: "rat list" assumes pairwise_rel_prime: "pairwise_coprime_list qs" assumes all_squarefree: "\q. q \ set qs \ rsquarefree q" assumes ex_x1: "sga = sign_vec qs x1" assumes hnz: "has_no_zeros sga" shows "(\w \ (roots_of_coprime_r (cast_rat_list qs)). sga = (sign_vec qs w))" proof - obtain x1 where x1_prop: "sga = (sign_vec qs x1)" using ex_x1 by auto let ?zer_list = "sorted_list_of_set {(x::real). (\q \ set(qs). (rpoly q x = 0))} :: real list" - have strict_sorted_h: "strict_sorted ?zer_list" using sorted_sorted_list_of_set + have strict_sorted_h: "sorted_wrt (<) ?zer_list" using sorted_sorted_list_of_set strict_sorted_iff by auto then have sorted_hyp: "\q < length ?zer_list. (q + 1 < length ?zer_list) \ (?zer_list ! q) < (?zer_list ! (q +1))" - apply (auto) using lessI sorted_wrt_iff_nth_less strict_sorted_sorted_wrt - by (metis (no_types, lifting) length_sorted_list_of_set strict_sorted_h) + using strict_sorted_h by (auto simp: sorted_wrt_iff_nth_less) then have sorted_hyp_var: "\q1 < length ?zer_list. \q2 < length ?zer_list. (q1 < q2 \ (?zer_list ! q1) < (?zer_list ! q2))" - by (metis (no_types, lifting) sorted_wrt_iff_nth_less strict_sorted_h strict_sorted_sorted_wrt) + using sorted_wrt_iff_nth_less strict_sorted_h by blast then have sorted_hyp_var2: "\q1 < length ?zer_list. ((?zer_list ! q1)::real) \ (?zer_list ! (length ?zer_list - 1))" - apply (auto) - by (smt (z3) Suc_pred diff_less gr_implies_not0 less_SucE zero_less_Suc) + by (smt (verit, ccfv_SIG) One_nat_def Suc_pred bot_nat_0.extremum less_Suc_eq_le less_le not_less) have nonz_q: "\q \set qs. q \ 0" using all_squarefree unfolding rsquarefree_def using in_set_member by auto then have "\q \set qs. finite {x. rpoly q x = 0}" by (simp add: poly_roots_finite) then have fin_set: "finite {x. \q\set qs. rpoly q x = 0}" by auto have x1_and_roots: "?zer_list \ [] \ ((x1 < (?zer_list ! 0)) \ (x1 > (?zer_list ! (length ?zer_list - 1)) \ (\ n < (length ?zer_list - 1). x1 > (?zer_list ! n) \ x1 < (?zer_list ! (n+1)))))" using roots_of_coprime_r_location_property x1_prop assms by auto have x2gt: "\x2>x1. sign_vec qs x1 \ sign_vec qs x2 \ (\r>x1. r \ x2 \ (\q\set qs. rpoly q r = 0))" using hnz x1_prop zero_above[of qs x1] by auto have x2lt: "\x2 sign_vec qs x2 \ (\r r \ (\q\set qs. rpoly q r = 0))" using hnz x1_prop zero_below[of qs x1] by (auto) have triv_neg_inf_h: "?zer_list = [] \ sga = (sign_vec qs (-crb (prod_list (cast_rat_list qs))))" proof - assume empty_zer: "(?zer_list:: real list) = []" let ?zer_set = "{x. \q\set qs. rpoly q x = 0}:: real set" have fin_zer: "finite ?zer_set" using fin_set by auto have "finite ?zer_set \ (sorted_list_of_set ?zer_set = []) = (?zer_set = {})" using fin_zer sorted_list_of_set_eq_Nil_iff[where A = "?zer_set"] by auto then have "(sorted_list_of_set ?zer_set = []) = (?zer_set = {})" using fin_zer by auto then have nozers: "?zer_set = {}" using empty_zer by auto then have "\(\(r::real). (\(q::rat poly)\set qs. rpoly q r = 0))" using nozers by auto then have "\y. sign_vec qs x1 = sign_vec qs y" proof - fix y have gt_prop: "x1 > y \ sign_vec qs x1 = sign_vec qs y" using hnz x1_prop zero_below[of qs x1] apply (auto) using \\r. \q\set qs. rpoly q r = 0\ by blast have lt_prop: "x1 < y \ sign_vec qs x1 = sign_vec qs y" using zero_above[of qs x1] apply (auto) using \\r. \q\set qs. rpoly q r = 0\ x2gt by blast show ?thesis using gt_prop lt_prop apply (auto) apply (metis \\r. \q\set qs. rpoly q r = 0\ linorder_neqE_linordered_idom x2gt x2lt) using x2gt x2lt apply (auto) apply (metis \\r. \q\set qs. rpoly q r = 0\ linorder_neqE_linordered_idom) apply (metis \\r. \q\set qs. rpoly q r = 0\ linorder_neqE_linordered_idom) by (metis \\r. \q\set qs. rpoly q r = 0\ linorder_neqE_linordered_idom) qed then show ?thesis by (simp add: x1_prop) qed have neg_inf_h: "?zer_list \[] \ (x1 < (?zer_list ! 0) \ sga = (sign_vec qs (-crb (prod_list (cast_rat_list qs)))))" proof - let ?neg_crb = "-crb (prod_list (cast_rat_list qs))" assume len_nontriv: "?zer_list \[]" assume x1_lt: "x1 < ?zer_list ! 0" have r_gt: "\r. (\q\set qs. rpoly q r = 0) \ r \ (?zer_list ! 0)" proof clarsimp fix q::"rat poly" fix r:: "real" assume q_in: "q \ set qs" assume "rpoly q r = 0" then have "r \ {x. \q\set qs. rpoly q x = 0}" using q_in by auto then have "List.member (sorted_list_of_set {x. \q\set qs. rpoly q x = 0}) r" using in_set_member set_sorted_list_of_set fin_set apply (auto) by (smt \r \ {x. \q\set qs. rpoly q x = 0}\ fin_set in_set_member set_sorted_list_of_set) then show "sorted_list_of_set {x. \q\set qs. rpoly q x = 0} ! 0 \ r" using sorted_hyp_var by (metis (no_types, lifting) gr_implies_not0 in_set_conv_nth in_set_member not_less sorted_iff_nth_mono sorted_sorted_list_of_set) qed have prod_zer: "\x. (\q\set qs. rpoly q x = 0) \ (poly (prod_list (cast_rat_list qs)) x) = 0" using prod_list_zero_iff[where xs = "(cast_rat_list qs)"] unfolding cast_rat_list_def apply (auto) using nonz_q apply blast by (metis (no_types, hide_lams) image_eqI list.set_map of_rat_poly_hom.prod_list_map_hom poly_prod_list_zero_iff) have "?zer_list \[] \ List.member (sorted_list_of_set {x. \q\set qs. rpoly q x = 0}) (?zer_list ! 0)" using nth_Cons_0 apply (auto) by (meson gr0I in_set_member length_0_conv nth_mem) then have "?zer_list \[] \ (?zer_list ! 0) \ {x. \q\set qs. rpoly q x = 0}" using in_set_member[where x = "(sorted_list_of_set {x. \q\set qs. rpoly q x = 0} ! 0)", where xs = "sorted_list_of_set {x. \q\set qs. rpoly q x = 0}"] set_sorted_list_of_set fin_set by blast then have "?zer_list \[] \ (\q\set qs. rpoly q (?zer_list ! 0) = 0)" by blast then have poly_zer: "?zer_list \[] \ (poly (prod_list (cast_rat_list qs)) (?zer_list ! 0)) = 0" using prod_zer by auto have "\q. List.member (cast_rat_list qs) q \q \ 0" using nonz_q unfolding cast_rat_list_def using in_set_member imageE image_set map_poly_zero of_rat_eq_0_iff by smt then have "(prod_list (cast_rat_list qs)) \ 0" using prod_list_zero_iff in_set_member apply (auto) by fastforce then have crb_lt: "?zer_list \[] \ ?neg_crb < ?zer_list ! 0" using crb_lem_neg[where p = "(prod_list (cast_rat_list qs))", where x = "sorted_list_of_set {x. \q\set qs. rpoly q x = 0} ! 0"] apply (auto) using poly_zer by blast have crb_gt_x1: "?zer_list \[] \ (?neg_crb > x1 \ (sga \ (sign_vec qs ?neg_crb)) \ (\r>x1. r \ ?neg_crb \ (\q\set qs. rpoly q r = 0)))" using x2gt apply (auto) using crb_lt r_gt x1_prop by fastforce have crb_lt_x1: "?neg_crb < x1 \ (sga \ (sign_vec qs ?neg_crb)) \ (\r r \ (\q\set qs. rpoly q r = 0))" using x2lt apply (auto) using x1_lt r_gt x1_prop by fastforce show ?thesis using len_nontriv crb_gt_x1 crb_lt_x1 x1_lt crb_lt r_gt apply (auto) using x1_prop by blast qed have pos_inf_h: "?zer_list \ [] \ (x1 > (?zer_list ! (length ?zer_list - 1)) \ sga = (sign_vec qs (crb (prod_list (cast_rat_list qs)))))" proof - let ?pos_crb = "crb (prod_list (cast_rat_list qs))" assume len_nontriv: "?zer_list \[]" assume x1_lt: "x1 > ?zer_list ! (length ?zer_list - 1)" have r_gt: "\r. (\q\set qs. rpoly q r = 0) \ r \ (?zer_list ! (length ?zer_list - 1))" proof - fix r:: "real" assume q_in: "(\q\set qs. rpoly q r = 0)" then obtain q::"rat poly" where q_prop: "q \ set qs \ rpoly q r = 0" by auto then have "r \ {x. \q\set qs. rpoly q x = 0}" using q_in by auto then have "List.member (sorted_list_of_set {x. \q\set qs. rpoly q x = 0}) r" using in_set_member set_sorted_list_of_set fin_set by smt then have "\n < (length ?zer_list). r = ?zer_list ! n" by (metis (no_types, lifting) in_set_conv_nth in_set_member) then obtain n where n_prop: "n < length ?zer_list \ r = ?zer_list ! n" by auto then show "r \ (?zer_list ! (length ?zer_list - 1))" proof - have "\q1. q1 < length ?zer_list \ (?zer_list ! q1) \ (?zer_list ! (length ?zer_list - 1:: nat))" using sorted_hyp_var2 by auto then have "(?zer_list ! n) \ (?zer_list ! (length ?zer_list - 1))" using n_prop by auto then show ?thesis using n_prop by auto qed qed have prod_zer: "\x. (\q\set qs. rpoly q x = 0) \ (poly (prod_list (cast_rat_list qs)) x) = 0" using prod_list_zero_iff[where xs = "(cast_rat_list qs)"] unfolding cast_rat_list_def apply (auto) using nonz_q apply blast by (metis (no_types, hide_lams) image_eqI list.set_map of_rat_poly_hom.prod_list_map_hom poly_prod_list_zero_iff) have "?zer_list \[] \ List.member (sorted_list_of_set {x. \q\set qs. rpoly q x = 0}) (?zer_list ! (length ?zer_list -1))" using nth_Cons_0 apply (auto) by (metis (no_types, lifting) diff_less in_set_conv_nth in_set_member length_greater_0_conv length_sorted_list_of_set zero_less_Suc) then have "?zer_list \[] \ (?zer_list ! (length ?zer_list -1)) \ {x. \q\set qs. rpoly q x = 0}" using in_set_member[where x = "(sorted_list_of_set {x. \q\set qs. rpoly q x = 0} ! (length ?zer_list -1))", where xs = "sorted_list_of_set {x. \q\set qs. rpoly q x = 0}"] set_sorted_list_of_set fin_set by blast then have "?zer_list \[] \ (\q\set qs. rpoly q (?zer_list ! (length ?zer_list -1)) = 0)" by blast then have poly_zer: "?zer_list \[] \ (poly (prod_list (cast_rat_list qs)) (?zer_list ! (length ?zer_list -1))) = 0" using prod_zer by auto have "\q. List.member (cast_rat_list qs) q \q \ 0" using nonz_q unfolding cast_rat_list_def using in_set_member imageE image_set map_poly_zero of_rat_eq_0_iff by smt then have "(prod_list (cast_rat_list qs)) \ 0" using prod_list_zero_iff in_set_member apply (auto) by fastforce then have crb_lt: "?zer_list \[] \ ?pos_crb > ?zer_list ! (length ?zer_list -1)" using crb_lem_pos[where p = "(prod_list (cast_rat_list qs))", where x = "sorted_list_of_set {x. \q\set qs. rpoly q x = 0} ! (length ?zer_list -1)"] apply (auto) using poly_zer by simp have crb_gt_x1: "?zer_list \[] \ ((?pos_crb::real) > (x1::real) \ (sga \ (sign_vec (qs::rat poly list) (?pos_crb::real))) \ (\(r::real) ?pos_crb \ (\(q::rat poly)\set qs. rpoly q r = 0)))" using x2gt apply (auto) using crb_lt r_gt x1_prop using x1_lt by fastforce have crb_lt_x1: "?pos_crb < x1 \ (sga \ (sign_vec qs ?pos_crb)) \ (\r>x1. ?pos_crb \ r \ (\q\set qs. poly (real_of_rat_poly q) r = 0))" using x2lt apply (auto) using x1_lt r_gt x1_prop by (meson \prod_list (cast_rat_list qs) \ 0\ crb_lem_pos not_less prod_zer) show ?thesis using len_nontriv crb_gt_x1 crb_lt_x1 x1_lt crb_lt r_gt apply (auto) using x1_prop by blast qed have between_h: "(\ n < (length ?zer_list - 1). x1 > (?zer_list ! n) \ x1 < (?zer_list ! (n+1))) \ (\w \ (roots_of_coprime_r (cast_rat_list qs)). sga = (sign_vec qs w))" proof - assume "(\ n < (length ?zer_list - 1). x1 > (?zer_list ! n) \ x1 < (?zer_list ! (n+1)))" then obtain n where n_prop: "n < (length ?zer_list - 1) \ x1 > (?zer_list ! n) \ x1 < (?zer_list ! (n+1))" by auto have "\q1 q2. (q1 \ q2 \ (List.member (cast_rat_list qs) q1) \ (List.member (cast_rat_list qs) q2))\ coprime q1 q2" using pairwise_rel_prime coprime_rat_poly_iff_coprimereal_poly unfolding pairwise_coprime_list_def by (smt cast_rat_list_def imageE image_set in_set_conv_nth in_set_member) then have all_prop: "\x1. \x2. ((x1 < x2 \ (\q1 \ set (cast_rat_list(qs)). (poly q1 x1) = 0) \ (\q2\ set((cast_rat_list(qs))). (poly q2 x2) = 0)) \ (\q. x1 < q \ q < x2 \ poly (coprime_r (cast_rat_list qs)) q = 0))" using coprime_r_roots_prop by auto have exq1: "(\q1 \ set (cast_rat_list(qs)). (poly q1 (?zer_list ! n)) = 0)" unfolding cast_rat_list_def using n_prop apply (auto) by (smt (verit, ccfv_SIG) One_nat_def Suc_eq_plus1 Suc_lessD fin_set length_sorted_list_of_set less_diff_conv mem_Collect_eq nth_mem set_sorted_list_of_set) have exq2: "(\q2 \ set (cast_rat_list(qs)). (poly q2 (?zer_list ! (n+1))) = 0)" unfolding cast_rat_list_def using n_prop One_nat_def Suc_eq_plus1 fin_set less_diff_conv mem_Collect_eq nth_mem set_sorted_list_of_set by (smt (verit, ccfv_SIG) image_eqI set_map) have n_prop2: "(((?zer_list ! n) < (?zer_list ! (n+1)) \ (\q1 \ set (cast_rat_list(qs)). (poly q1 (?zer_list ! n)) = 0) \ (\q2\ set((cast_rat_list(qs))). (poly q2 (?zer_list ! (n+1))) = 0)))" using exq1 exq2 sorted_hyp n_prop by auto then have "(\q. (?zer_list ! n) < q \ q < (?zer_list ! (n+1)) \ poly (coprime_r (cast_rat_list qs)) q = 0)" using all_prop n_prop2 by auto then have "\w \ (roots_of_coprime_r (cast_rat_list qs)). (?zer_list ! n) < w \ w < (?zer_list ! (n+1))" apply (auto) using roots_of_coprime_r_def by auto then obtain w where w_prop: "w \ (roots_of_coprime_r (cast_rat_list qs)) \ (?zer_list ! n) < w \ w < (?zer_list ! (n+1))" by auto have n_lt1: "n < length ?zer_list" using n_prop using add_lessD1 less_diff_conv by blast have n_lt2: "n + 1 < length ?zer_list" using n_prop using less_diff_conv by blast have sorted_hyp_var3: "?zer_list ! n < ?zer_list ! (n + 1)" using sorted_hyp n_lt1 n_lt2 by auto then have helper: "w > x1 \ \(\(x::real). (List.member ?zer_list x \ x1 \ x \ x \ w))" using n_prop w_prop x1_prop strict_sorted_h sorted_list_lemma[where n = "n", where l = ?zer_list, where a = "x1", where b = "w"] sorted_hyp_var3 by auto have no_root1: "w > x1 \ \(\r>x1. r \ w \ (\q\set qs. rpoly q r = 0))" proof - assume "w > x1" then have nex: "\(\(x::real). (List.member ?zer_list x \ x1 \ x \ x \ w))" using helper by auto have "(\r>x1. r \ w \ (\q\set qs. rpoly q r = 0)) \ False" proof - assume "(\r>x1. r \ w \ (\q\set qs. rpoly q r = 0))" then obtain r where r_prop: "r > x1 \r \ w \(\q\set qs. rpoly q r = 0)" by auto then have "List.member ?zer_list r \x1 \ r \x1 \ w " by (smt fin_set in_set_member mem_Collect_eq set_sorted_list_of_set) then show ?thesis using nex r_prop by blast qed then show ?thesis by auto qed have helper2: "w < x1 \ \(\(x::real). (List.member ?zer_list x \ w \ x \ x \ x1))" using n_prop w_prop x1_prop strict_sorted_h sorted_list_lemma[where n = "n", where l = ?zer_list, where a = "w", where b = "x1"] sorted_hyp_var3 by auto have no_root2: "w < x1 \ \(\r r \ (\q\set qs. rpoly q r = 0))" proof - assume "w < x1" then have nex: "\(\(x::real). (List.member ?zer_list x \ w \ x \ x \ x1))" using helper2 by auto have "(\r r \ (\q\set qs. rpoly q r = 0)) \ False" proof - assume "(\r r\ (\q\set qs. rpoly q r = 0))" then obtain r where r_prop: "r < x1 \ w \ r \(\q\set qs. rpoly q r = 0)" by auto then have "List.member ?zer_list r \ w \ r \ r \ x1 " by (smt fin_set in_set_member mem_Collect_eq set_sorted_list_of_set) then show ?thesis using nex r_prop by blast qed then show ?thesis by auto qed then have w_gt: "w > x1 \ (sign_vec qs x1) = (sign_vec qs w)" using no_root1 n_prop x2gt by auto have w_lt: "w < x1 \ (sign_vec qs x1) = (sign_vec qs w)" using no_root2 n_prop x2lt by auto then have "sga = (sign_vec qs w)" using w_gt w_lt x1_prop by auto then show "(\w \ (roots_of_coprime_r (cast_rat_list qs)). sga = (sign_vec qs w))" using w_prop by auto qed show ?thesis using triv_neg_inf_h neg_inf_h pos_inf_h between_h x1_and_roots by (metis (mono_tags, lifting) coprime_r_zero1 coprime_r_zero2 mem_Collect_eq roots_of_coprime_r_def) qed (* This lemma heavily relies on the main BKR_Proofs result and also the lemma named roots_of_coprime_r_capture_sgas_without_zeros *) lemma find_csas_lemma_nozeros: fixes qs:: "rat poly list" assumes fs: "factorize_polys qs = (fs,data)" assumes "fs \ []" shows "(csa \ (consistent_sign_vectors fs UNIV) \ has_no_zeros csa) \ csa \ set (find_consistent_signs_at_roots (coprime_r (cast_rat_list fs)) (cast_rat_list fs))" proof - let ?new_l = "cast_rat_list fs" let ?copr = "coprime_r ?new_l" have copr_nonz: "?copr \ 0" using coprime_r_nonzero[OF assms(1-2)] unfolding cast_rat_list_def by auto have nontriv_list: "0 < length ?new_l" using assms cast_rat_list_def by (auto) have pairwise_cp: "(\q. q \ set ?new_l \ algebraic_semidom_class.coprime ?copr q)" using coprime_r_coprime_prop[OF assms(1)] apply (auto) by (metis cast_rat_list_def comm_monoid_mult_class.coprime_commute coprime_iff_coprime list.set_map) have set_fsga: "set(find_consistent_signs_at_roots ?copr ?new_l) = set(characterize_consistent_signs_at_roots ?copr ?new_l)" using find_consistent_signs_at_roots[OF copr_nonz pairwise_cp] by auto then have csa_in_hyp: "csa \ set (find_consistent_signs_at_roots ?copr ?new_l) \ csa \ set(characterize_consistent_signs_at_roots ?copr ?new_l)" by auto have forward: "(csa \ (consistent_sign_vectors fs UNIV) \ has_no_zeros csa) \ csa \ set(characterize_consistent_signs_at_roots ?copr ?new_l)" proof - assume csa_in: "(csa \ (consistent_sign_vectors fs UNIV) \ has_no_zeros csa)" have fin: "finite {x. poly (coprime_r (cast_rat_list fs)) x = 0}" using copr_nonz poly_roots_finite by (simp add: poly_roots_finite fs) have pcl: "pairwise_coprime_list fs" using coprime_factorize fs by (metis fst_conv) have sqf: "\q. q \ set fs \ rsquarefree q" using factorize_polys_square_free[OF assms(1)] by (metis square_free_rsquarefree) obtain x1 where x1:"csa = sign_vec fs x1" using consistent_sign_vectors_def csa_in by auto have hnz: "has_no_zeros csa" using csa_in by auto obtain w where w_prop: "w\roots_of_coprime_r (cast_rat_list fs)" "csa = sign_vec fs w" using roots_of_coprime_r_capture_sgas_without_zeros[OF pcl sqf x1 hnz] by auto have w_root: "poly (coprime_r (cast_rat_list fs)) w = 0" using w_prop by (simp add: roots_of_coprime_r_def) then have "w \ {x. poly (coprime_r (cast_rat_list fs)) x = 0}" by auto then have w_ins: "w \ set (characterize_root_list_p (coprime_r (cast_rat_list fs)))" using fin set_sorted_list_of_set[where A="{x. poly (coprime_r (cast_rat_list fs)) x = 0}"] unfolding characterize_root_list_p_def by auto have "map ((\x. if 0 < x then 1 else if x < 0 then - 1 else 0) \ (\p. rpoly p w)) fs = map ((\x. if 0 < x then 1 else - 1) \ (\p. rpoly p w)) fs" proof - have "\(\x \ set fs. rpoly x w = 0)" proof clarsimp fix x assume x_in: "x \ set fs" assume x_zer: "rpoly x w = 0" then have "\k < length fs. nth fs k = x" using x_in by (simp add: in_set_conv_nth) then obtain k where k_prop: "k < length fs \ fs ! k = x" by auto then have "(sign_vec fs w) ! k = 0" using x_zer apply (auto) unfolding sign_vec_def squash_def by auto then have "\ (has_no_zeros (sign_vec fs w))" apply (auto) by (simp add: hnz_prop k_prop) then show False using hnz unfolding sign_vec_def squash_def using \\ has_no_zeros (sign_vec fs w)\ w_prop(2) by blast qed then show ?thesis using hnz unfolding sign_vec_def squash_def by auto qed then have "map ((\x. if 0 < x then 1 else if x < 0 then - 1 else 0) \ (\p. rpoly p w)) fs = map (\q. if 0 < poly q w then 1 else - 1) (cast_rat_list fs)" unfolding cast_rat_list_def by auto then have "csa = map (\q. if 0 < poly q w then 1 else - 1) (cast_rat_list fs)" by (simp add: comp_def sign_vec_def squash_def w_prop(2)) then show ?thesis unfolding characterize_consistent_signs_at_roots_def apply (auto) unfolding signs_at_def using w_ins w_prop using consistent_sign_vectors_consistent_sign_vectors_r consistent_sign_vectors_def consistent_sign_vectors_r_def signs_at_def by force qed have backward: "csa \ set(characterize_consistent_signs_at_roots ?copr ?new_l) \ (csa \ (consistent_sign_vectors fs UNIV) \ has_no_zeros csa)" proof - assume csa_in: "csa \ set(characterize_consistent_signs_at_roots ?copr ?new_l)" have csa_in_old_set: "csa \ set (characterize_consistent_signs_at_roots_copr ?copr ?new_l)" using csa_list_copr_rel copr_nonz csa_in find_consistent_signs_at_roots_copr pairwise_cp set_fsga by auto have "\(x::real). \ (l::real poly list). rec_list True (\h T. If (h = 0) False) (map (\q. if 0 < poly q x then (1::rat) else (-1::rat)) l)" proof clarsimp fix x::"real" fix l::"real poly list" show " rec_list True (\h T. If (h = 0) False) (map (\q. if 0 < poly q x then (1::rat) else (-1::rat)) l) " proof (induct l) case Nil then show ?case by simp next case (Cons a l) then show ?case by auto qed qed then have "\x. rec_list True (\h T. If (h = 0) False) (map (\q. if 0 < poly q x then (1::rat) else - 1) (cast_rat_list fs))" by auto then have hnz: "has_no_zeros csa" using csa_in_old_set unfolding characterize_consistent_signs_at_roots_copr_def consistent_sign_vec_copr_def apply (auto) unfolding has_no_zeros_def by auto have "\w \ set(characterize_root_list_p ?copr). csa = consistent_sign_vec_copr ?new_l w" using csa_in_old_set using characterize_consistent_signs_at_roots_copr_def by auto then obtain w where w_prop: "w \ set (characterize_root_list_p ?copr) \ csa = consistent_sign_vec_copr ?new_l w" by auto then have "poly ?copr w = 0" unfolding characterize_root_list_p_def by (simp add: copr_nonz poly_roots_finite) then have copr_prop: "\p \ set(?new_l). poly p w \ 0" using w_prop coprime_r_coprime_prop apply (auto) by (meson coprime_poly_0 in_set_member pairwise_cp) then have "consistent_sign_vec_copr ?new_l w = sign_vec fs w" unfolding sign_vec_def squash_def consistent_sign_vec_copr_def cast_rat_list_def by auto then show ?thesis using hnz w_prop apply (auto) using consistent_sign_vectors_def by blast qed have "(csa \ (consistent_sign_vectors fs UNIV) \ has_no_zeros csa) \ csa \ set(characterize_consistent_signs_at_roots ?copr ?new_l)" using forward backward by blast then show ?thesis using csa_in_hyp by auto qed lemma range_eq: fixes a fixes b shows "a = b \ range a = range b" by simp lemma removeAt_distinct: shows "distinct fss \ distinct (removeAt i fss)" unfolding removeAt_def by (simp add: set_take_disj_set_drop_if_distinct) lemma consistent_signs_atw: assumes "\p. p \ set fs \ poly p x \ 0" shows "consistent_sign_vec_copr fs x = signs_at fs x" unfolding consistent_sign_vec_copr_def signs_at_def squash_def o_def by (simp add: assms) (* This could be an alternate (equivalent) definition *) lemma characterize_consistent_signs_at_roots_rw: assumes "p \ 0" assumes copr: "\q. q \ set fs \ coprime p q" shows "set (characterize_consistent_signs_at_roots p fs) = consistent_sign_vectors_r fs ({x. poly p x = 0})" by (simp add: assms(1) characterize_consistent_signs_at_roots_def consistent_sign_vectors_r_def poly_roots_finite characterize_root_list_p_def) lemma signs_at_insert: assumes "i \ length qs" shows "insertAt i (squash (poly p x)) (signs_at qs x) = signs_at (insertAt i p qs) x" unfolding insertAt_def signs_at_def o_def using assms take_map apply auto apply (subst drop_map) by simp lemma length_removeAt: assumes "i < length ls" shows "length (removeAt i ls) = length ls - 1" unfolding removeAt_def using assms by auto lemma insertAt_removeAt: assumes "i < length ls" shows "insertAt i (ls!i) (removeAt i ls) = ls" unfolding insertAt_def removeAt_def using assms apply auto by (simp add: Cons_nth_drop_Suc) lemma insertAt_nth: assumes "i \ length ls" shows "insertAt i n ls ! i = n" unfolding insertAt_def using assms by (simp add: nth_append_take) lemma length_signs_at[simp]: shows "length (signs_at qs x) = length qs" unfolding signs_at_def by auto lemma find_csa_at_index: assumes "i < length fss" assumes "\p q. p \ set fss \ q \ set fss \ p \ q \ coprime p q" assumes "\p. p \ set fss \ p \ 0" assumes "distinct fss" shows " set (map (\v. insertAt i 0 v) (find_consistent_signs_at_roots (fss ! i) (removeAt i fss))) = {v \ consistent_sign_vectors_r fss UNIV. v ! i = 0}" proof - from removeAt_distinct[OF assms(4)] have neq: "fss ! i \ 0" using assms by simp have cop: "\q. q \ set (removeAt i fss) \ coprime (fss ! i) q" using assms unfolding removeAt_def apply auto using dual_order.strict_trans find_first_unique image_iff less_imp_le_nat less_not_refl nth_image nth_mem apply (smt atLeastLessThan_iff dual_order.strict_trans find_first_unique image_iff less_imp_le_nat less_not_refl nth_image nth_mem) by (metis Cons_nth_drop_Suc distinct.simps(2) distinct_drop in_set_dropD nth_mem) from find_consistent_signs_at_roots[OF neq] have "set (find_consistent_signs_at_roots (fss ! i) (removeAt i fss)) = set (characterize_consistent_signs_at_roots (fss ! i) (removeAt i fss))" using cop by auto then have eq: "set (map (insertAt i 0) (find_consistent_signs_at_roots (fss ! i) (removeAt i fss))) = insertAt i 0 ` set (characterize_consistent_signs_at_roots (fss ! i) (removeAt i fss)) " by simp from characterize_consistent_signs_at_roots_rw[OF neq cop] have eq2: "set (characterize_consistent_signs_at_roots (fss ! i) (removeAt i fss)) = consistent_sign_vectors_r (removeAt i fss) {x. poly (fss ! i) x = 0}" . have ile: "i \ length (removeAt i fss)" using length_removeAt[OF assms(1)] assms(1) by linarith have 1: "\xb. poly (fss ! i) xb = 0 \ insertAt i 0 (signs_at (removeAt i fss) xb) \ range (signs_at fss)" proof - fix x assume "poly (fss ! i) x = 0" then have "insertAt i 0 (signs_at (removeAt i fss) x) = insertAt i (squash (poly (fss ! i) x)) (signs_at (removeAt i fss) x)" by (auto simp add: squash_def) also have "... = signs_at (insertAt i (fss ! i) (removeAt i fss)) x" apply (intro signs_at_insert) using length_removeAt[OF assms(1)] using assms(1) by linarith also have "... = signs_at fss x" unfolding insertAt_removeAt[OF assms(1)] by auto ultimately have *:"insertAt i 0 (signs_at (removeAt i fss) x) = signs_at fss x" by auto thus "insertAt i 0 (signs_at (removeAt i fss) x) \ range (signs_at fss)" by auto qed have 2: "\xa. signs_at fss xa ! i = 0 \ i \ length (removeAt i fss) \ signs_at fss xa \ insertAt i 0 ` signs_at (removeAt i fss) ` {x. poly (fss ! i) x = 0}" proof - fix x assume "signs_at fss x ! i = 0" then have z:"poly (fss ! i) x = 0" unfolding signs_at_def o_def squash_def by (smt assms(1) class_field.zero_not_one nth_map zero_neq_neg_one) then have "insertAt i 0 (signs_at (removeAt i fss) x) = insertAt i (squash (poly (fss ! i) x)) (signs_at (removeAt i fss) x)" by (auto simp add: squash_def) also have "... = signs_at (insertAt i (fss ! i) (removeAt i fss)) x" apply (intro signs_at_insert) using length_removeAt[OF assms(1)] using assms(1) by linarith also have "... = signs_at fss x" unfolding insertAt_removeAt[OF assms(1)] by auto ultimately have *:"insertAt i 0 (signs_at (removeAt i fss) x) = signs_at fss x" by auto thus "signs_at fss x \ insertAt i 0 ` signs_at (removeAt i fss) ` {x. poly (fss ! i) x = 0}" using z by (metis (mono_tags, lifting) mem_Collect_eq rev_image_eqI) qed have "insertAt i 0 ` consistent_sign_vectors_r (removeAt i fss) {x. poly (fss ! i) x = 0} = {v \ consistent_sign_vectors_r fss UNIV. v ! i = 0}" unfolding consistent_sign_vectors_r_def apply (auto simp add: 1) apply (subst insertAt_nth) using ile by (auto simp add: 2) thus ?thesis unfolding eq eq2 . qed lemma in_set_concat_map: assumes "i < length ls" assumes "x \ set (f (ls ! i))" shows "x \ set (concat (map f ls))" using assms by auto lemma find_csas_lemma_onezero_gen: fixes qs:: "rat poly list" assumes fs: "factorize_polys qs = (fs,data)" assumes fss: "fss = cast_rat_list fs" shows "(csa \ (consistent_sign_vectors_r fss UNIV) \ \(has_no_zeros csa)) \ csa \ set (find_sgas_aux fss)" proof - have a:"(\p q. p \ set fss \ q \ set fss \ p \ q \ coprime p q)" using cast_rat_list_def factorize_polys_map_coprime fs fss by blast have b:"(\p. p \ set fss \ p \ 0)" using factorize_polys_map_square_free_prod_list semidom_class.prod_list_zero_iff square_free_def using cast_rat_list_def fs fss by blast have c:"distinct fss" using factorize_polys_map_distinct[OF assms(1)] assms(2) unfolding cast_rat_list_def by auto have forwards: "csa \ (consistent_sign_vectors_r fss UNIV) \ \ (has_no_zeros csa) \ csa \ set (find_sgas_aux fss)" unfolding find_sgas_aux_def proof - assume csa: "csa \ (consistent_sign_vectors_r fss UNIV)" assume hnz: "\(has_no_zeros csa)" then obtain i where i: "i < length csa" "csa ! i = 0" unfolding hnz_prop by auto then have cin: "csa \ {v \ consistent_sign_vectors_r fss UNIV. v ! i = 0}" using csa by auto have 1:"i < length fss" using i csa unfolding consistent_sign_vectors_r_def by auto from find_csa_at_index[OF 1 a b c] have eq: "set (map (\v. insertAt i 0 v) (find_consistent_signs_at_roots (fss ! i) (removeAt i fss))) = {v \ consistent_sign_vectors_r fss UNIV. v ! i = 0}" by auto show "csa \ set (concat (map (\i. map (insertAt i 0) (find_consistent_signs_at_roots (fss ! i) (removeAt i fss))) [0.. set (find_sgas_aux fss) \ \ (has_no_zeros csa) \ csa \ (consistent_sign_vectors_r fss UNIV)" proof - assume *: "csa \ set (find_sgas_aux fss)" then obtain i where i: "i < length fss" "csa \ set (map (\v. insertAt i 0 v) (find_consistent_signs_at_roots (fss ! i) (removeAt i fss)))" unfolding find_sgas_aux_def by auto from find_csa_at_index[OF i(1) a b c] have eq: "set (map (\v. insertAt i 0 v) (find_consistent_signs_at_roots (fss ! i) (removeAt i fss))) = {v \ consistent_sign_vectors_r fss UNIV. v ! i = 0}" by auto have *: "csa \ {v \ consistent_sign_vectors_r fss UNIV. v ! i = 0}" using i eq by auto then have "length csa = length fss" unfolding consistent_sign_vectors_r_def by auto thus ?thesis unfolding has_no_zeros_def using * apply (auto simp add:in_set_conv_nth) using i(1) by auto qed show ?thesis using forwards backwards by blast qed lemma mem_append: "List.member (l1@l2) m \ (List.member l1 m \ List.member l2 m)" by (simp add: List.member_def) lemma same_sign_cond_rationals_reals: fixes qs:: "rat poly list" assumes lenh: "length (fst(factorize_polys qs)) > 0" shows "set(find_sgas (map (map_poly of_rat) (fst(factorize_polys qs)))) = consistent_sign_vectors (fst(factorize_polys qs)) UNIV" proof - let ?ftrs = "(fst(factorize_polys qs))" have pairwise_rel_prime: "pairwise_coprime_list (fst(factorize_polys qs))" using factorize_polys_coprime by (simp add: coprime_factorize) have all_squarefree:"\q. (List.member (fst(factorize_polys qs)) q) \ (rsquarefree q)" using factorize_polys_square_free by (metis in_set_member prod.collapse square_free_rsquarefree) have allnonzero: "\q. (List.member ?ftrs q) \ q \ 0" using all_squarefree apply (auto) using rsquarefree_def by blast have h1: "\ csa. (csa \ (consistent_sign_vectors ?ftrs UNIV) \ \ (has_no_zeros csa)) \ csa \ set (find_sgas_aux (cast_rat_list ?ftrs))" using lenh find_csas_lemma_onezero_gen pairwise_rel_prime allnonzero by (metis consistent_sign_vectors_consistent_sign_vectors_r eq_fst_iff) have h2: "\csa. (csa \ (consistent_sign_vectors ?ftrs UNIV) \ has_no_zeros csa) \ List.member (find_consistent_signs_at_roots (coprime_r (cast_rat_list ?ftrs)) (cast_rat_list ?ftrs)) csa" using lenh find_csas_lemma_nozeros pairwise_rel_prime allnonzero by (metis in_set_member length_greater_0_conv prod.collapse) have h3: "\ csa. List.member (find_sgas (map (map_poly of_rat) ?ftrs)) csa \ ((List.member (find_sgas_aux (cast_rat_list ?ftrs)) csa) \ (List.member (find_consistent_signs_at_roots (coprime_r (cast_rat_list ?ftrs)) (cast_rat_list ?ftrs)) csa))" unfolding find_sgas_def cast_rat_list_def using mem_append by metis have h4: "\ csa. List.member (find_sgas (map (map_poly of_rat) ?ftrs)) csa \ ((csa \ (consistent_sign_vectors ?ftrs UNIV) \ has_no_zeros csa) \ (csa \ (consistent_sign_vectors ?ftrs UNIV) \ \ (has_no_zeros csa)))" using h1 h2 h3 apply (auto) apply (simp add: in_set_member) by (simp add: in_set_member) have h5: "\csa. (csa \ (consistent_sign_vectors ?ftrs UNIV) \ has_no_zeros csa) \ (csa \ (consistent_sign_vectors ?ftrs UNIV) \ \ (has_no_zeros csa)) \ csa \ (consistent_sign_vectors ?ftrs UNIV)" by auto then have "\ csa. List.member (find_sgas (map (map_poly of_rat) ?ftrs)) csa \ csa \ (consistent_sign_vectors ?ftrs UNIV)" using h4 by blast then show ?thesis using in_set_member apply (auto) apply (simp add: in_set_member) by (simp add: in_set_member) qed lemma factorize_polys_undo_factorize_polys_set: assumes "factorize_polys ps = (ftrs,data)" assumes "sgas = find_sgas (map (map_poly of_rat) ftrs)" assumes sgas_set: "set (sgas) = consistent_sign_vectors ftrs UNIV" shows "set (map (undo_factorize_polys data) sgas) = consistent_sign_vectors ps UNIV" proof - have h: "\x. undo_factorize_polys data (sign_vec ftrs x) = sign_vec ps x" using factorize_polys_undo_factorize_polys by (simp add: assms(1)) have h1: "\x. sign_vec ps x \ set (map (undo_factorize_polys data) sgas)" using sgas_set by (metis UNIV_I consistent_sign_vectors_def h image_eqI image_set) then have subset_h: "consistent_sign_vectors ps UNIV \ set (map (undo_factorize_polys data) sgas)" unfolding consistent_sign_vectors_def by auto have supset_h: "consistent_sign_vectors ps UNIV \ set (map (undo_factorize_polys data) sgas)" proof - have "\ ele. ele \ set (map (undo_factorize_polys data) sgas) \ (\n < length sgas. ele = (undo_factorize_polys data (nth sgas n)))" using index_of_lookup(1) index_of_lookup(2) by fastforce then have "\ ele. ele \ set (map (undo_factorize_polys data) sgas) \ (\x. ele = (undo_factorize_polys data (sign_vec ftrs x)))" using sgas_set apply (auto) using consistent_sign_vectors_def by auto then show ?thesis using h using consistent_sign_vectors_def by auto qed show ?thesis using subset_h supset_h by blast qed lemma main_step_aux1: fixes qs:: "rat poly list" assumes empty: "(fst(factorize_polys qs)) = []" shows "set (find_consistent_signs qs) = consistent_sign_vectors qs UNIV" proof - have set_eq: "set (find_consistent_signs qs) = {(map (\x. if poly x 0 < 0 then -1 else if poly x 0 = 0 then 0 else 1) qs)}" using empty unfolding find_consistent_signs_def apply (auto) apply (metis fst_conv) by (metis prod.collapse) have deg_q_prop: "fst(factorize_polys qs) = [] \ (\q \set(qs). degree q = 0)" apply (rule ccontr) proof clarsimp fix q assume *:"fst(factorize_polys qs) = []" assume q: "q \ set qs" "0 < degree q" obtain arb where "factorize_rat_poly_monic q = (arb,[])" using * q unfolding factorize_polys_def apply (auto simp add:Let_def) by (metis prod.collapse) from squarefree_factorization_degree[OF factorize_rat_poly_monic_square_free_factorization[OF this]] have "degree q = 0" by auto thus False using q by auto qed have deg_q_cons: "(\q \set(qs). degree q = 0) \ (consistent_sign_vectors qs UNIV = {(map (\x. if poly x 0 < 0 then -1 else if poly x 0 = 0 then 0 else 1) qs)})" proof - assume deg_z: "(\q \set(qs). degree q = 0)" then have "\q \set(qs). \x y. poly q x = poly q y" apply (auto) by (meson constant_def constant_degree) then have csv: "consistent_sign_vectors qs UNIV = {sign_vec qs 0}" unfolding consistent_sign_vectors_def sign_vec_def apply (auto) apply (metis deg_z degree_0_id of_rat_hom.map_poly_hom_coeff_lift poly_0_coeff_0 poly_const_conv squash_real_of_rat) by (metis (mono_tags, lifting) class_semiring.add.one_closed comp_def image_iff list.map_cong0 of_rat_hom.poly_map_poly_0) have "sign_vec qs 0 = (map (\x. if poly x 0 < 0 then -1 else if poly x 0 = 0 then 0 else 1) qs)" unfolding sign_vec_def squash_def by auto then show "consistent_sign_vectors qs UNIV = {(map (\x. if poly x 0 < 0 then -1 else if poly x 0 = 0 then 0 else 1) qs)}" using csv by auto qed then show ?thesis using deg_q_prop deg_q_cons set_eq by (simp add: empty) qed lemma main_step_aux2: fixes qs:: "rat poly list" assumes lenh: "length (fst(factorize_polys qs)) > 0" shows "set (find_consistent_signs qs) = consistent_sign_vectors qs UNIV" proof - let ?fs = "fst(factorize_polys qs)" let ?data = "snd(factorize_polys qs)" let ?sgas = "find_sgas (map (map_poly of_rat) ?fs)" have h0: "set (?sgas) = consistent_sign_vectors ?fs UNIV" using lenh same_sign_cond_rationals_reals coprime_factorize by auto then have h1: "set (map (undo_factorize_polys ?data) ?sgas) = consistent_sign_vectors qs UNIV" using factorize_polys_undo_factorize_polys_set by simp then show ?thesis using lenh apply (auto) apply (smt case_prod_unfold find_consistent_signs_def h1 main_step_aux1) by (simp add: find_consistent_signs_def prod.case_eq_if) qed lemma main_step: fixes qs:: "rat poly list" shows "set (find_consistent_signs qs) = consistent_sign_vectors qs UNIV" using main_step_aux1 main_step_aux2 by auto subsection "Decision Procedure: Main Lemmas" lemma decide_univ_lem_helper: assumes "(fml_struct,polys) = convert fml" shows "(\x::real. lookup_sem fml_struct (map (\p. rpoly p x) polys)) \ (decide_universal fml)" using universal_lookup_sem main_step unfolding decide_universal_def apply (auto) apply (metis assms convert_closed fst_conv snd_conv) by (metis (full_types) assms convert_closed fst_conv snd_conv) lemma decide_exis_lem_helper: assumes "(fml_struct,polys) = convert fml" shows "(\x::real. lookup_sem fml_struct (map (\p. rpoly p x) polys)) \ (decide_existential fml)" using existential_lookup_sem main_step unfolding decide_existential_def apply (auto) apply (metis assms convert_closed fst_conv snd_conv) by (metis (full_types) assms convert_closed fst_conv snd_conv) theorem decision_procedure: shows "(\x::real. fml_sem fml x) \ (decide_universal fml)" "\x::real. fml_sem fml x \ (decide_existential fml)" using convert_semantics_lem decide_univ_lem_helper apply (auto) apply (simp add: convert_semantics) apply (metis convert_def convert_semantics fst_conv snd_conv) using convert_semantics_lem by (metis convert_def convert_semantics decide_exis_lem_helper fst_conv snd_conv) end \ No newline at end of file diff --git a/thys/BenOr_Kozen_Reif/More_Matrix.thy b/thys/BenOr_Kozen_Reif/More_Matrix.thy --- a/thys/BenOr_Kozen_Reif/More_Matrix.thy +++ b/thys/BenOr_Kozen_Reif/More_Matrix.thy @@ -1,2014 +1,2012 @@ theory More_Matrix imports "Jordan_Normal_Form.Matrix" "Jordan_Normal_Form.DL_Rank" "Jordan_Normal_Form.VS_Connect" "Jordan_Normal_Form.Gauss_Jordan_Elimination" begin section "Kronecker Product" definition kronecker_product :: "'a :: ring mat \ 'a mat \ 'a mat" where "kronecker_product A B = (let ra = dim_row A; ca = dim_col A; rb = dim_row B; cb = dim_col B in mat (ra*rb) (ca*cb) (\(i,j). A $$ (i div rb, j div cb) * B $$ (i mod rb, j mod cb) ))" lemma arith: assumes "d < a" assumes "c < b" shows "b*d+c < a*(b::nat)" proof - have "b*d+c < b*(d+1)" by (simp add: assms(2)) thus ?thesis by (metis One_nat_def Suc_leI add.right_neutral add_Suc_right assms(1) less_le_trans mult.commute mult_le_cancel2) qed lemma dim_kronecker[simp]: "dim_row (kronecker_product A B) = dim_row A * dim_row B" "dim_col (kronecker_product A B) = dim_col A * dim_col B" unfolding kronecker_product_def Let_def by auto lemma kronecker_inverse_index: assumes "r < dim_row A" "s < dim_col A" assumes "v < dim_row B" "w < dim_col B" shows "kronecker_product A B $$ (dim_row B*r+v, dim_col B*s+w) = A $$ (r,s) * B $$ (v,w)" proof - from arith[OF assms(1) assms(3)] have "dim_row B*r+v < dim_row A * dim_row B" . moreover from arith[OF assms(2) assms(4)] have "dim_col B * s + w < dim_col A * dim_col B" . ultimately show ?thesis unfolding kronecker_product_def Let_def using assms by auto qed lemma kronecker_distr_left: assumes "dim_row B = dim_row C" "dim_col B = dim_col C" shows "kronecker_product A (B+C) = kronecker_product A B + kronecker_product A C" unfolding kronecker_product_def Let_def using assms apply (auto simp add: mat_eq_iff) by (metis (no_types, lifting) distrib_left index_add_mat(1) mod_less_divisor mult_eq_0_iff neq0_conv not_less_zero) lemma kronecker_distr_right: assumes "dim_row B = dim_row C" "dim_col B = dim_col C" shows "kronecker_product (B+C) A = kronecker_product B A + kronecker_product C A" unfolding kronecker_product_def Let_def using assms by (auto simp add: mat_eq_iff less_mult_imp_div_less distrib_right) lemma index_mat_mod[simp]: "nr > 0 & nc > 0 \ mat nr nc f $$ (i mod nr,j mod nc) = f (i mod nr,j mod nc)" by auto lemma kronecker_assoc: shows "kronecker_product A (kronecker_product B C) = kronecker_product (kronecker_product A B) C" unfolding kronecker_product_def Let_def apply (case_tac "dim_row B * dim_row C > 0 & dim_col B * dim_col C > 0") apply (auto simp add: mat_eq_iff less_mult_imp_div_less) by (smt div_mult2_eq div_mult_mod_eq kronecker_inverse_index less_mult_imp_div_less linordered_semiring_strict_class.mult_pos_pos mod_less_divisor mod_mult2_eq mult.assoc mult.commute) lemma sum_sum_mod_div: "(\ia = 0::nat..ja = 0..ia = 0..ia. (ia div y, ia mod y)) {0.. {0.. (\ia. (ia div y, ia mod y)) ` {0.. {0.. (\ia. (ia div y, ia mod y)) ` {0..ia. (ia div y, ia mod y)) ` {0.. {0.. {0.. {0..ia. (ia div y, ia mod y)) ` {0..ia = 0::nat..ja = 0..(x, y)\{0.. {0..ia. (ia div y, ia mod y)"]) using 1 2 by auto qed (* Kronecker product distributes over matrix multiplication *) lemma kronecker_of_mult: assumes "dim_col (A :: 'a :: comm_ring mat) = dim_row C" assumes "dim_col B = dim_row D" shows "kronecker_product A B * kronecker_product C D = kronecker_product (A * C) (B * D)" unfolding kronecker_product_def Let_def mat_eq_iff proof clarsimp fix i j assume ij: "i < dim_row A * dim_row B" "j < dim_col C * dim_col D" have 1: "(A * C) $$ (i div dim_row B, j div dim_col D) = row A (i div dim_row B) \ col C (j div dim_col D)" using ij less_mult_imp_div_less by (auto intro!: index_mult_mat) have 2: "(B * D) $$ (i mod dim_row B, j mod dim_col D) = row B (i mod dim_row B) \ col D (j mod dim_col D)" using ij apply (auto intro!: index_mult_mat) using gr_implies_not0 apply fastforce using gr_implies_not0 by fastforce have 3: "\x. x < dim_row C * dim_row D \ A $$ (i div dim_row B, x div dim_row D) * B $$ (i mod dim_row B, x mod dim_row D) * (C $$ (x div dim_row D, j div dim_col D) * D $$ (x mod dim_row D, j mod dim_col D)) = row A (i div dim_row B) $ (x div dim_row D) * col C (j div dim_col D) $ (x div dim_row D) * (row B (i mod dim_row B) $ (x mod dim_row D) * col D (j mod dim_col D) $ (x mod dim_row D))" proof - fix x assume *:"x < dim_row C * dim_row D" have 1: "row A (i div dim_row B) $ (x div dim_row D) = A $$ (i div dim_row B, x div dim_row D)" by (simp add: * assms(1) less_mult_imp_div_less row_def) have 2: "row B (i mod dim_row B) $ (x mod dim_row D) = B $$ (i mod dim_row B, x mod dim_row D)" by (metis "*" assms(2) ij(1) index_row(1) mod_less_divisor nat_0_less_mult_iff neq0_conv not_less_zero) have 3: "col C (j div dim_col D) $ (x div dim_row D) = C $$ (x div dim_row D, j div dim_col D)" by (simp add: "*" ij(2) less_mult_imp_div_less) have 4: "col D (j mod dim_col D) $ (x mod dim_row D) = D $$ (x mod dim_row D, j mod dim_col D)" by (metis "*" Euclidean_Division.div_eq_0_iff gr_implies_not0 ij(2) index_col mod_div_trivial mult_not_zero) show "A $$ (i div dim_row B, x div dim_row D) * B $$ (i mod dim_row B, x mod dim_row D) * (C $$ (x div dim_row D, j div dim_col D) * D $$ (x mod dim_row D, j mod dim_col D)) = row A (i div dim_row B) $ (x div dim_row D) * col C (j div dim_col D) $ (x div dim_row D) * (row B (i mod dim_row B) $ (x mod dim_row D) * col D (j mod dim_col D) $ (x mod dim_row D))" unfolding 1 2 3 4 by (simp add: mult.assoc mult.left_commute) qed have *: "(A * C) $$ (i div dim_row B, j div dim_col D) * (B * D) $$ (i mod dim_row B, j mod dim_col D) = (\ia = 0..j. A $$ (i div dim_row B, j div dim_col B) * B $$ (i mod dim_row B, j mod dim_col B)) \ vec (dim_row C * dim_row D) (\i. C $$ (i div dim_row D, j div dim_col D) * D $$ (i mod dim_row D, j mod dim_col D)) = (A * C) $$ (i div dim_row B, j div dim_col D) * (B * D) $$ (i mod dim_row B, j mod dim_col D)" unfolding * scalar_prod_def by (auto simp add: assms sum_product sum_sum_mod_div intro!: sum.cong) qed lemma inverts_mat_length: assumes "square_mat A" "inverts_mat A B" "inverts_mat B A" shows "dim_row B = dim_row A" "dim_col B = dim_col A" apply (metis assms(1) assms(3) index_mult_mat(3) index_one_mat(3) inverts_mat_def square_mat.simps) by (metis assms(1) assms(2) index_mult_mat(3) index_one_mat(3) inverts_mat_def square_mat.simps) lemma less_mult_imp_mod_less: "m mod i < i" if "m < n * i" for m n i :: nat using gr_implies_not_zero that by fastforce lemma kronecker_one: shows "kronecker_product ((1\<^sub>m x)::'a :: ring_1 mat) (1\<^sub>m y) = 1\<^sub>m (x*y)" unfolding kronecker_product_def Let_def apply (auto simp add:mat_eq_iff less_mult_imp_div_less less_mult_imp_mod_less) by (metis div_mult_mod_eq) lemma kronecker_invertible: assumes "invertible_mat (A :: 'a :: comm_ring_1 mat)" "invertible_mat B" shows "invertible_mat (kronecker_product A B)" proof - obtain Ai where Ai: "inverts_mat A Ai" "inverts_mat Ai A" using assms invertible_mat_def by blast obtain Bi where Bi: "inverts_mat B Bi" "inverts_mat Bi B" using assms invertible_mat_def by blast have "square_mat (kronecker_product A B)" by (metis (no_types, lifting) assms(1) assms(2) dim_col_mat(1) dim_row_mat(1) invertible_mat_def kronecker_product_def square_mat.simps) moreover have "inverts_mat (kronecker_product A B) (kronecker_product Ai Bi)" using Ai Bi unfolding inverts_mat_def by (metis (no_types, lifting) dim_kronecker(1) index_mult_mat(3) index_one_mat(3) kronecker_of_mult kronecker_one) moreover have "inverts_mat (kronecker_product Ai Bi) (kronecker_product A B)" using Ai Bi unfolding inverts_mat_def by (metis (no_types, lifting) dim_kronecker(1) index_mult_mat(3) index_one_mat(3) kronecker_of_mult kronecker_one) ultimately show ?thesis unfolding invertible_mat_def by blast qed section "More DL Rank" (* conjugate matrices *) instantiation mat :: (conjugate) conjugate begin definition conjugate_mat :: "'a :: conjugate mat \ 'a mat" where "conjugate m = mat (dim_row m) (dim_col m) (\(i,j). conjugate (m $$ (i,j)))" lemma dim_row_conjugate[simp]: "dim_row (conjugate m) = dim_row m" unfolding conjugate_mat_def by auto lemma dim_col_conjugate[simp]: "dim_col (conjugate m) = dim_col m" unfolding conjugate_mat_def by auto lemma carrier_vec_conjugate[simp]: "m \ carrier_mat nr nc \ conjugate m \ carrier_mat nr nc" by (auto) lemma mat_index_conjugate[simp]: shows "i < dim_row m \ j < dim_col m \ conjugate m $$ (i,j) = conjugate (m $$ (i,j))" unfolding conjugate_mat_def by auto lemma row_conjugate[simp]: "i < dim_row m \ row (conjugate m) i = conjugate (row m i)" by (auto) lemma col_conjugate[simp]: "i < dim_col m \ col (conjugate m) i = conjugate (col m i)" by (auto) lemma rows_conjugate: "rows (conjugate m) = map conjugate (rows m)" by (simp add: list_eq_iff_nth_eq) lemma cols_conjugate: "cols (conjugate m) = map conjugate (cols m)" by (simp add: list_eq_iff_nth_eq) instance proof fix a b :: "'a mat" show "conjugate (conjugate a) = a" unfolding mat_eq_iff by auto let ?a = "conjugate a" let ?b = "conjugate b" show "conjugate a = conjugate b \ a = b" by (metis dim_col_conjugate dim_row_conjugate mat_index_conjugate conjugate_cancel_iff mat_eq_iff) qed end abbreviation conjugate_transpose :: "'a::conjugate mat \ 'a mat" where "conjugate_transpose A \ conjugate (A\<^sup>T)" notation conjugate_transpose ("(_\<^sup>H)" [1000]) lemma transpose_conjugate: shows "(conjugate A)\<^sup>T = A\<^sup>H" unfolding conjugate_mat_def by auto lemma vec_module_col_helper: fixes A:: "('a :: field) mat" shows "(0\<^sub>v (dim_row A) \ LinearCombinations.module.span class_ring \carrier = carrier_vec (dim_row A), mult = undefined, one = undefined, zero = 0\<^sub>v (dim_row A), add = (+), smult = (\\<^sub>v)\ (set (cols A)))" proof - have "\v. (0::'a) \\<^sub>v v + v = v" by auto then show "0\<^sub>v (dim_row A) \ LinearCombinations.module.span class_ring \carrier = carrier_vec (dim_row A), mult = undefined, one = undefined, zero = 0\<^sub>v (dim_row A), add = (+), smult = (\\<^sub>v)\ (set (cols A))" by (metis cols_dim module_vec_def right_zero_vec smult_carrier_vec vec_space.prod_in_span zero_carrier_vec) qed lemma vec_module_col_helper2: fixes A:: "('a :: field) mat" shows "\a x. x \ LinearCombinations.module.span class_ring \carrier = carrier_vec (dim_row A), mult = undefined, one = undefined, zero = 0\<^sub>v (dim_row A), add = (+), smult = (\\<^sub>v)\ (set (cols A)) \ (\a b v. (a + b) \\<^sub>v v = a \\<^sub>v v + b \\<^sub>v v) \ a \\<^sub>v x \ LinearCombinations.module.span class_ring \carrier = carrier_vec (dim_row A), mult = undefined, one = undefined, zero = 0\<^sub>v (dim_row A), add = (+), smult = (\\<^sub>v)\ (set (cols A))" proof - fix a :: 'a and x :: "'a vec" assume "x \ LinearCombinations.module.span class_ring \carrier = carrier_vec (dim_row A), mult = undefined, one = undefined, zero = 0\<^sub>v (dim_row A), add = (+), smult = (\\<^sub>v)\ (set (cols A))" then show "a \\<^sub>v x \ LinearCombinations.module.span class_ring \carrier = carrier_vec (dim_row A), mult = undefined, one = undefined, zero = 0\<^sub>v (dim_row A), add = (+), smult = (\\<^sub>v)\ (set (cols A))" by (metis (full_types) cols_dim idom_vec.smult_in_span module_vec_def) qed lemma vec_module_col: "module (class_ring :: 'a :: field ring) (module_vec TYPE('a) (dim_row A) \carrier := LinearCombinations.module.span class_ring (module_vec TYPE('a) (dim_row A)) (set (cols A))\)" proof - interpret abelian_group "module_vec TYPE('a) (dim_row A) \carrier := LinearCombinations.module.span class_ring (module_vec TYPE('a) (dim_row A)) (set (cols A))\" apply (unfold_locales) apply (auto simp add:module_vec_def) apply (metis cols_dim module_vec_def partial_object.select_convs(1) ring.simps(2) vec_vs vectorspace.span_add1) apply (metis assoc_add_vec cols_dim module_vec_def vec_space.cV vec_vs vectorspace.span_closed) using vec_module_col_helper[of A] apply (auto) apply (metis cols_dim left_zero_vec module_vec_def partial_object.select_convs(1) vec_vs vectorspace.span_closed) apply (metis cols_dim module_vec_def partial_object.select_convs(1) right_zero_vec vec_vs vectorspace.span_closed) apply (metis cols_dim comm_add_vec module_vec_def vec_space.cV vec_vs vectorspace.span_closed) unfolding Units_def apply auto by (smt cols_dim module_vec_def partial_object.select_convs(1) uminus_l_inv_vec uminus_r_inv_vec vec_space.vec_neg vec_vs vectorspace.span_closed vectorspace.span_neg) show ?thesis apply (unfold_locales) unfolding class_ring_simps apply auto unfolding module_vec_simps using add_smult_distrib_vec apply auto apply (auto simp add:module_vec_def) using vec_module_col_helper2 apply blast using cols_dim module_vec_def partial_object.select_convs(1) smult_add_distrib_vec vec_vs vectorspace.span_closed by (smt (z3)) qed (* The columns of a matrix form a vectorspace *) lemma vec_vs_col: "vectorspace (class_ring :: 'a :: field ring) (module_vec TYPE('a) (dim_row A) \carrier := LinearCombinations.module.span class_ring (module_vec TYPE('a) (dim_row A)) (set (cols A))\)" unfolding vectorspace_def using vec_module_col class_field by (auto simp: class_field_def) lemma cols_mat_mul_map: shows "cols (A * B) = map ((*\<^sub>v) A) (cols B)" unfolding list_eq_iff_nth_eq by auto lemma cols_mat_mul: shows "set (cols (A * B)) = (*\<^sub>v) A ` set (cols B)" by (simp add: cols_mat_mul_map) lemma set_obtain_sublist: assumes "S \ set ls" obtains ss where "distinct ss" "S = set ss" using assms finite_distinct_list infinite_super by blast lemma mul_mat_of_cols: assumes "A \ carrier_mat nr n" assumes "\j. j < length cs \ cs ! j \ carrier_vec n" shows "A * (mat_of_cols n cs) = mat_of_cols nr (map ((*\<^sub>v) A) cs)" unfolding mat_eq_iff using assms apply auto apply (subst mat_of_cols_index) by auto lemma helper: fixes x y z ::"'a :: {conjugatable_ring, comm_ring}" shows "x * (y * z) = y * x * z" by (simp add: mult.assoc mult.left_commute) lemma cscalar_prod_conjugate_transpose: fixes x y ::"'a :: {conjugatable_ring, comm_ring} vec" assumes "A \ carrier_mat nr nc" assumes "x \ carrier_vec nr" assumes "y \ carrier_vec nc" shows "x \c (A *\<^sub>v y) = (A\<^sup>H *\<^sub>v x) \c y" unfolding mult_mat_vec_def scalar_prod_def using assms apply (auto simp add: sum_distrib_left sum_distrib_right sum_conjugate conjugate_dist_mul) apply (subst sum.swap) by (meson helper mult.assoc mult.left_commute sum.cong) lemma mat_mul_conjugate_transpose_vec_eq_0: fixes v ::"'a :: {conjugatable_ordered_ring,semiring_no_zero_divisors,comm_ring} vec" assumes "A \ carrier_mat nr nc" assumes "v \ carrier_vec nr" assumes "A *\<^sub>v (A\<^sup>H *\<^sub>v v) = 0\<^sub>v nr" shows "A\<^sup>H *\<^sub>v v = 0\<^sub>v nc" proof - have "(A\<^sup>H *\<^sub>v v) \c (A\<^sup>H *\<^sub>v v) = (A *\<^sub>v (A\<^sup>H *\<^sub>v v)) \c v" by (metis (mono_tags, lifting) Matrix.carrier_vec_conjugate assms(1) assms(2) assms(3) carrier_matD(2) conjugate_zero_vec cscalar_prod_conjugate_transpose dim_row_conjugate index_transpose_mat(2) mult_mat_vec_def scalar_prod_left_zero scalar_prod_right_zero vec_carrier) also have "... = 0" by (simp add: assms(2) assms(3)) (* this step requires real entries *) ultimately have "(A\<^sup>H *\<^sub>v v) \c (A\<^sup>H *\<^sub>v v) = 0" by auto thus ?thesis apply (subst conjugate_square_eq_0_vec[symmetric]) using assms(1) carrier_dim_vec apply fastforce by auto qed lemma row_mat_of_cols: assumes "i < nr" shows "row (mat_of_cols nr ls) i = vec (length ls) (\j. (ls ! j) $i)" by (smt assms dim_vec eq_vecI index_row(1) index_row(2) index_vec mat_of_cols_carrier(2) mat_of_cols_carrier(3) mat_of_cols_index) lemma mat_of_cols_cons_mat_vec: fixes v ::"'a::comm_ring vec" assumes "v \ carrier_vec (length ls)" assumes "dim_vec a = nr" shows "mat_of_cols nr (a # ls) *\<^sub>v (vCons m v) = m \\<^sub>v a + mat_of_cols nr ls *\<^sub>v v" unfolding mult_mat_vec_def vec_eq_iff using assms by (auto simp add: row_mat_of_cols vec_Suc o_def mult.commute) lemma smult_vec_zero: fixes v ::"'a::ring vec" shows "0 \\<^sub>v v = 0\<^sub>v (dim_vec v)" unfolding smult_vec_def vec_eq_iff by (auto) lemma helper2: fixes A ::"'a::comm_ring mat" fixes v ::"'a vec" assumes "v \ carrier_vec (length ss)" assumes "\x. x \ set ls \ dim_vec x = nr" shows "mat_of_cols nr ss *\<^sub>v v = mat_of_cols nr (ls @ ss) *\<^sub>v (0\<^sub>v (length ls) @\<^sub>v v)" using assms(2) proof (induction ls) case Nil then show ?case by auto next case (Cons a ls) then show ?case apply (auto simp add:zero_vec_Suc) apply (subst mat_of_cols_cons_mat_vec) by (auto simp add:assms smult_vec_zero) qed lemma mat_of_cols_mult_mat_vec_permute_list: fixes v ::"'a::comm_ring list" assumes "f permutes {..v vec_of_list (permute_list f v) = mat_of_cols nr ss *\<^sub>v vec_of_list v" unfolding mat_of_cols_def mult_mat_vec_def vec_eq_iff scalar_prod_def proof clarsimp fix i assume "i < nr" from sum.permute[OF assms(1)] have "(\iaia. ss ! f ia $ i * v ! f ia) \ f) {..ia = 0..ia = 0..ia = 0..\g. sum g {.. f) {.. assms(2) comp_apply lessThan_atLeast0 sum.cong) show "(\ia = 0..j. permute_list f ss ! j $ i) $ ia * vec_of_list (permute_list f v) $ ia) = (\ia = 0..j. ss ! j $ i) $ ia * vec_of_list v $ ia)" using assms * by (auto simp add: permute_list_nth vec_of_list_index) qed (* permute everything in a subset of the indices to the back *) lemma subindex_permutation: assumes "distinct ss" "set ss \ {..i. i \ set ss) [0..i. i \ set ss) [0..i. i \ set ss) [0..i. i \ set ss) [0.. {..i. i \ set ss) [0.. set ls" obtains ids where "distinct ids" "set ids \ {.. {..ids. distinct ids \ set ids \ {.. ss = map ((!) ls) ids \ thesis) \ thesis" using 1 2 3 by blast qed lemma helper3: fixes A ::"'a::comm_ring mat" assumes A: "A \ carrier_mat nr nc" assumes ss:"distinct ss" "set ss \ set (cols A)" assumes "v \ carrier_vec (length ss)" obtains c where "mat_of_cols nr ss *\<^sub>v v = A *\<^sub>v c" "dim_vec c = nc" proof - from distinct_list_subset_nths[OF ss] obtain ids where ids: "distinct ids" "set ids \ {..x. x \ set ?ls \ dim_vec x = nr" using A by auto let ?cs1 = "(list_of_vec (0\<^sub>v (length ?ls) @\<^sub>v v))" from helper2[OF assms(4) ] have "mat_of_cols nr ss *\<^sub>v v = mat_of_cols nr (?ls @ ss) *\<^sub>v vec_of_list (?cs1)" using * by (metis vec_list) also have "... = mat_of_cols nr (permute_list f (?ls @ ss)) *\<^sub>v vec_of_list (permute_list f ?cs1)" apply (auto intro!: mat_of_cols_mult_mat_vec_permute_list[symmetric]) apply (metis cols_length f(1) f(2) length_append length_map length_permute_list) using assms(4) by auto also have "... = A *\<^sub>v vec_of_list (permute_list f ?cs1)" using f(2) assms by auto ultimately show "(\c. mat_of_cols nr ss *\<^sub>v v = A *\<^sub>v c \ dim_vec c = nc \ thesis) \ thesis" by (metis A assms(4) carrier_matD(2) carrier_vecD cols_length dim_vec_of_list f(2) index_append_vec(2) index_zero_vec(2) length_append length_list_of_vec length_permute_list) qed lemma mat_mul_conjugate_transpose_sub_vec_eq_0: fixes A ::"'a :: {conjugatable_ordered_ring,semiring_no_zero_divisors,comm_ring} mat" assumes "A \ carrier_mat nr nc" assumes "distinct ss" "set ss \ set (cols (A\<^sup>H))" assumes "v \ carrier_vec (length ss)" assumes "A *\<^sub>v (mat_of_cols nc ss *\<^sub>v v) = 0\<^sub>v nr" shows "(mat_of_cols nc ss *\<^sub>v v) = 0\<^sub>v nc" proof - have "A\<^sup>H \ carrier_mat nc nr" using assms(1) by auto from helper3[OF this assms(2-4)] obtain c where c: "mat_of_cols nc ss *\<^sub>v v = A\<^sup>H *\<^sub>v c" "dim_vec c = nr" by blast have 1: "c \ carrier_vec nr" using c carrier_vec_dim_vec by blast have 2: "A *\<^sub>v (A\<^sup>H *\<^sub>v c) = 0\<^sub>v nr" using c assms(5) by auto from mat_mul_conjugate_transpose_vec_eq_0[OF assms(1) 1 2] have "A\<^sup>H *\<^sub>v c = 0\<^sub>v nc" . thus ?thesis unfolding c(1)[symmetric] . qed lemma Units_invertible: fixes A:: "'a::semiring_1 mat" assumes "A \ Units (ring_mat TYPE('a) n b)" shows "invertible_mat A" using assms unfolding Units_def invertible_mat_def apply (auto simp add: ring_mat_def) using inverts_mat_def by blast lemma invertible_Units: fixes A:: "'a::semiring_1 mat" assumes "invertible_mat A" shows "A \ Units (ring_mat TYPE('a) (dim_row A) b)" using assms unfolding Units_def invertible_mat_def apply (auto simp add: ring_mat_def) by (metis assms carrier_mat_triv invertible_mat_def inverts_mat_def inverts_mat_length(1) inverts_mat_length(2)) lemma invertible_det: fixes A:: "'a::field mat" assumes "A \ carrier_mat n n" shows "invertible_mat A \ det A \ 0" apply auto using invertible_Units unit_imp_det_non_zero apply fastforce using assms by (auto intro!: Units_invertible det_non_zero_imp_unit) context vec_space begin lemma find_indices_distinct: assumes "distinct ss" assumes "i < length ss" shows "find_indices (ss ! i) ss = [i]" proof - have "set (find_indices (ss ! i) ss) = {i}" using assms apply auto by (simp add: assms(1) assms(2) nth_eq_iff_index_eq) thus ?thesis by (metis distinct.simps(2) distinct_find_indices empty_iff empty_set insert_iff list.exhaust list.simps(15)) qed lemma lin_indpt_lin_comb_list: assumes "distinct ss" assumes "lin_indpt (set ss)" assumes "set ss \ carrier_vec n" assumes "lincomb_list f ss = 0\<^sub>v n" assumes "i < length ss" shows "f i = 0" proof - from lincomb_list_as_lincomb[OF assms(3)] have "lincomb_list f ss = lincomb (mk_coeff ss f) (set ss)" . also have "... = lincomb (\v. sum f (set (find_indices v ss))) (set ss)" unfolding mk_coeff_def apply (subst R.sumlist_map_as_finsum) by (auto simp add: distinct_find_indices) ultimately have "lincomb_list f ss = lincomb (\v. sum f (set (find_indices v ss))) (set ss)" by auto then have *:"lincomb (\v. sum f (set (find_indices v ss))) (set ss) = 0\<^sub>v n" using assms(4) by auto have "finite (set ss)" by simp from not_lindepD[OF assms(2) this _ _ *] have "(\v. sum f (set (find_indices v ss))) \ set ss \ {0}" by auto from funcset_mem[OF this] have "sum f (set (find_indices (nth ss i) ss)) \ {0}" using assms(5) by auto thus ?thesis unfolding find_indices_distinct[OF assms(1) assms(5)] by auto qed (* Note: in this locale dim_row A = n, e.g.: lemma foo: assumes "dim_row A = n" shows "rank A = vec_space.rank (dim_row A) A" by (simp add: assms) *) lemma span_mat_mul_subset: assumes "A \ carrier_mat n d" assumes "B \ carrier_mat d nc" shows "span (set (cols (A * B))) \ span (set (cols A))" proof - have *: "\v. \ca. lincomb_list v (cols (A * B)) = lincomb_list ca (cols A)" proof - fix v have "lincomb_list v (cols (A * B)) = (A * B) *\<^sub>v vec nc v" apply (subst lincomb_list_as_mat_mult) apply (metis assms(1) carrier_dim_vec carrier_matD(1) cols_dim index_mult_mat(2) subset_code(1)) by (metis assms(1) assms(2) carrier_matD(1) carrier_matD(2) cols_length index_mult_mat(2) index_mult_mat(3) mat_of_cols_cols) also have "... = A *\<^sub>v (B *\<^sub>v vec nc v)" using assms(1) assms(2) by auto also have "... = lincomb_list (\i. (B *\<^sub>v vec nc v) $ i) (cols A)" apply (subst lincomb_list_as_mat_mult) using assms(1) carrier_dim_vec cols_dim apply blast by (metis assms(1) assms(2) carrier_matD(1) carrier_matD(2) cols_length dim_mult_mat_vec dim_vec eq_vecI index_vec mat_of_cols_cols) ultimately have "lincomb_list v (cols (A * B)) = lincomb_list (\i. (B *\<^sub>v vec nc v) $ i) (cols A)" by auto thus "\ca. lincomb_list v (cols (A * B)) = lincomb_list ca (cols A)" by auto qed show ?thesis apply (subst span_list_as_span[symmetric]) apply (metis assms(1) carrier_matD(1) cols_dim index_mult_mat(2)) apply (subst span_list_as_span[symmetric]) using assms(1) cols_dim apply blast by (auto simp add:span_list_def *) qed lemma rank_mat_mul_right: assumes "A \ carrier_mat n d" assumes "B \ carrier_mat d nc" shows "rank (A * B) \ rank A" proof - have "subspace class_ring (local.span (set (cols (A*B)))) (vs (local.span (set (cols A))))" unfolding subspace_def by (metis assms(1) assms(2) carrier_matD(1) cols_dim index_mult_mat(2) nested_submodules span_is_submodule vec_space.span_mat_mul_subset vec_vs_col) from vectorspace.subspace_dim[OF _ this] have "vectorspace.dim class_ring (vs (local.span (set (cols A))) \carrier := local.span (set (cols (A * B)))\) \ vectorspace.dim class_ring (vs (local.span (set (cols A))))" apply auto by (metis (no_types) assms(1) carrier_matD(1) fin_dim_span_cols index_mult_mat(2) mat_of_cols_carrier(1) mat_of_cols_cols vec_vs_col) thus ?thesis unfolding rank_def by auto qed lemma sumlist_drop: assumes "\v. v \ set ls \ dim_vec v = n" shows "sumlist ls = sumlist (filter (\v. v \ 0\<^sub>v n) ls)" using assms proof (induction ls) case Nil then show ?case by auto next case (Cons a ls) then show ?case using dim_sumlist by auto qed lemma lincomb_list_alt: shows "lincomb_list c s = sumlist (map2 (\i j. i \\<^sub>v s ! j) (map (\i. c i) [0..v. v \ set s \ dim_vec v = n" assumes "\i. i \ set ls \ i < length s" shows " sumlist (map2 (\i j. i \\<^sub>v s ! j) (map (\i. c i) ls) ls) = sumlist (map2 (\i j. i \\<^sub>v s ! j) (map (\i. c i) (filter (\i. c i \ 0) ls)) (filter (\i. c i \ 0) ls))" using assms(2) proof (induction ls) case Nil then show ?case by auto next case (Cons a s) then show ?case apply auto apply (subst smult_l_null) apply (simp add: assms(1) carrier_vecI) apply (subst left_zero_vec) apply (subst sumlist_carrier) apply auto by (metis (no_types, lifting) assms(1) carrier_dim_vec mem_Collect_eq nth_mem set_filter set_zip_rightD) qed lemma two_set: assumes "distinct ls" assumes "set ls = set [a,b]" assumes "a \ b" shows "ls = [a,b] \ ls = [b,a]" apply (cases ls) using assms(2) apply auto[1] proof - fix x xs assume ls:"ls = x # xs" obtain y ys where xs:"xs = y # ys" by (metis (no_types) \ls = x # xs\ assms(2) assms(3) list.set_cases list.set_intros(1) list.set_intros(2) set_ConsD) have 1:"x = a \ x = b" using \ls = x # xs\ assms(2) by auto have 2:"y = a \ y = b" using \ls = x # xs\ \xs = y # ys\ assms(2) by auto have 3:"ys = []" by (metis (no_types) \ls = x # xs\ \xs = y # ys\ assms(1) assms(2) distinct.simps(2) distinct_length_2_or_more in_set_member member_rec(2) neq_Nil_conv set_ConsD) show "ls = [a, b] \ ls = [b, a]" using ls xs 1 2 3 assms by auto qed lemma filter_disj_inds: assumes "i < length ls" "j < length ls" "i \ j" shows "filter (\ia. ia \ j \ ia = i) [0.. filter (\ia. ia \ j \ ia = i) [0..ia. ia = i \ ia = j) [0..ia. ia = i \ ia = j) [0..v. v \ set ls \ dim_vec v = n" assumes "\c. lincomb_list c ls = 0\<^sub>v n \ (\i. i < (length ls) \ c i = 0)" shows "distinct ls" unfolding distinct_conv_nth proof clarsimp fix i j assume ij: "i < length ls" "j < length ls" "i \ j" assume lsij: "ls ! i = ls ! j" have "lincomb_list (\k. if k = i then 1 else if k = j then -1 else 0) ls = (ls ! i) - (ls ! j)" unfolding lincomb_list_alt apply (subst lincomb_list_alt2[OF assms(1)]) apply auto using filter_disj_inds[OF ij] apply auto using ij(3) apply force using assms(1) ij(2) apply auto[1] using ij(3) apply blast using assms(1) ij(2) by auto also have "... = 0\<^sub>v n" unfolding lsij apply (rule minus_cancel_vec) using \j < length ls\ assms(1) using carrier_vec_dim_vec nth_mem by blast ultimately have "lincomb_list (\k. if k = i then 1 else if k = j then -1 else 0) ls = 0\<^sub>v n" by auto from assms(2)[OF this] show False using \i < length ls\ by auto qed end locale conjugatable_vec_space = vec_space f_ty n for f_ty::"'a::conjugatable_ordered_field itself" and n begin lemma transpose_rank_mul_conjugate_transpose: fixes A :: "'a mat" assumes "A \ carrier_mat n nc" shows "vec_space.rank nc A\<^sup>H \ rank (A * A\<^sup>H)" proof - have 1: "A\<^sup>H \ carrier_mat nc n" using assms by auto have 2: "A * A\<^sup>H \ carrier_mat n n" using assms by auto (* S is a maximal linearly independent set of rows A (or cols A\<^sup>T) *) let ?P = "(\T. T \ set (cols A\<^sup>H) \ module.lin_indpt class_ring (module_vec TYPE('a) nc) T)" have *:"\A. ?P A \ finite A \ card A \ n" proof clarsimp fix S assume S: "S \ set (cols A\<^sup>H)" have "card S \ card (set (cols A\<^sup>H))" using S using card_mono by blast also have "... \ length (cols A\<^sup>H)" using card_length by blast also have "... \ n" using assms by auto ultimately show "finite S \ card S \ n" by (meson List.finite_set S dual_order.trans finite_subset) qed have **:"?P {}" apply (subst module.lin_dep_def) by (auto simp add: vec_module) from maximal_exists[OF *] obtain S where S: "maximal S ?P" using ** by (metis (no_types, lifting)) (* Some properties of S *) from vec_space.rank_card_indpt[OF 1 S] have rankeq: "vec_space.rank nc A\<^sup>H = card S" . have s_hyp: "S \ set (cols A\<^sup>H)" using S unfolding maximal_def by simp have modhyp: "module.lin_indpt class_ring (module_vec TYPE('a) nc) S" using S unfolding maximal_def by simp (* switch to a list representation *) obtain ss where ss: "set ss = S" "distinct ss" by (metis (mono_tags) S maximal_def set_obtain_sublist) have ss2: "set (map ((*\<^sub>v) A) ss) = (*\<^sub>v) A ` S" by (simp add: ss(1)) have rw_hyp: "cols (mat_of_cols n (map ((*\<^sub>v) A) ss)) = cols (A * mat_of_cols nc ss)" unfolding cols_def apply (auto) using mat_vec_as_mat_mat_mult[of A n nc] by (metis (no_types, lifting) "1" assms carrier_matD(1) cols_dim mul_mat_of_cols nth_mem s_hyp ss(1) subset_code(1)) then have rw: "mat_of_cols n (map ((*\<^sub>v) A) ss) = A * mat_of_cols nc ss" by (metis assms carrier_matD(1) index_mult_mat(2) mat_of_cols_carrier(2) mat_of_cols_cols) have indpt: "\c. lincomb_list c (map ((*\<^sub>v) A) ss) = 0\<^sub>v n \ \i. (i < (length ss) \ c i = 0)" proof clarsimp fix c i assume *: "lincomb_list c (map ((*\<^sub>v) A) ss) = 0\<^sub>v n" assume i: "i < length ss" have "\w\set (map ((*\<^sub>v) A) ss). dim_vec w = n" using assms by auto from lincomb_list_as_mat_mult[OF this] have "A * mat_of_cols nc ss *\<^sub>v vec (length ss) c = 0\<^sub>v n" using * rw by auto then have hq: "A *\<^sub>v (mat_of_cols nc ss *\<^sub>v vec (length ss) c) = 0\<^sub>v n" by (metis assms assoc_mult_mat_vec mat_of_cols_carrier(1) vec_carrier) then have eq1: "(mat_of_cols nc ss *\<^sub>v vec (length ss) c) = 0\<^sub>v nc" apply (intro mat_mul_conjugate_transpose_sub_vec_eq_0) using assms ss s_hyp by auto (* Rewrite the inner vector back to a lincomb_list *) have dim_hyp2: "\w\set ss. dim_vec w = nc" using ss(1) s_hyp by (metis "1" carrier_matD(1) carrier_vecD cols_dim subsetD) from vec_module.lincomb_list_as_mat_mult[OF this, symmetric] have "mat_of_cols nc ss *\<^sub>v vec (length ss) c = module.lincomb_list (module_vec TYPE('a) nc) c ss" . then have "module.lincomb_list (module_vec TYPE('a) nc) c ss = 0\<^sub>v nc" using eq1 by auto from vec_space.lin_indpt_lin_comb_list[OF ss(2) _ _ this i] show "c i = 0" using modhyp ss s_hyp using "1" cols_dim by blast qed have distinct: "distinct (map ((*\<^sub>v) A) ss)" by (metis (no_types, lifting) assms carrier_matD(1) dim_mult_mat_vec imageE indpt length_map lincomb_list_indpt_distinct ss2) then have 3: "card S = card ((*\<^sub>v) A ` S)" by (metis ss distinct_card image_set length_map) then have 4: "(*\<^sub>v) A ` S \ set (cols (A * A\<^sup>H))" using cols_mat_mul \S \ set (cols A\<^sup>H)\ by blast have 5: "lin_indpt ((*\<^sub>v) A ` S)" proof clarsimp assume ld:"lin_dep ((*\<^sub>v) A ` S)" have *: "finite ((*\<^sub>v) A ` S)" by (metis List.finite_set ss2) have **: "(*\<^sub>v) A ` S \ carrier_vec n" using "2" "4" cols_dim by blast from finite_lin_dep[OF * ld **] obtain a v where a: "lincomb a ((*\<^sub>v) A ` S) = 0\<^sub>v n" and v: "v \ (*\<^sub>v) A ` S" "a v \ 0" by blast obtain i where i:"v = map ((*\<^sub>v) A) ss ! i" "i < length ss" using v unfolding ss2[symmetric] using find_first_le nth_find_first by force from ss2[symmetric] have "set (map ((*\<^sub>v) A) ss)\ carrier_vec n" using ** ss2 by auto from lincomb_as_lincomb_list_distinct[OF this distinct] have "lincomb_list (\i. a (map ((*\<^sub>v) A) ss ! i)) (map ((*\<^sub>v) A) ss) = 0\<^sub>v n" using a ss2 by auto from indpt[OF this] show False using v i by simp qed from rank_ge_card_indpt[OF 2 4 5] have "card ((*\<^sub>v) A ` S) \ rank (A * A\<^sup>H)" . thus ?thesis using rankeq 3 by linarith qed lemma conjugate_transpose_rank_le: assumes "A \ carrier_mat n nc" shows "vec_space.rank nc (A\<^sup>H) \ rank A" by (metis assms carrier_matD(2) carrier_mat_triv dim_row_conjugate dual_order.trans index_transpose_mat(2) rank_mat_mul_right transpose_rank_mul_conjugate_transpose) lemma conjugate_finsum: assumes f: "f : U \ carrier_vec n" shows "conjugate (finsum V f U) = finsum V (conjugate \ f) U" using f proof (induct U rule: infinite_finite_induct) case (infinite A) then show ?case by auto next case empty then show ?case by auto next case (insert u U) hence f: "f : U \ carrier_vec n" "f u : carrier_vec n" by auto then have cf: "conjugate \ f : U \ carrier_vec n" "(conjugate \ f) u : carrier_vec n" apply (simp add: Pi_iff) by (simp add: f(2)) then show ?case unfolding finsum_insert[OF insert(1) insert(2) f] unfolding finsum_insert[OF insert(1) insert(2) cf ] apply (subst conjugate_add_vec[of _ n]) using f(2) apply blast using M.finsum_closed f(1) apply blast by (simp add: comp_def f(1) insert.hyps(3)) qed lemma rank_conjugate_le: assumes A:"A \ carrier_mat n d" shows "rank (conjugate (A)) \ rank A" proof - (* S is a maximal linearly independent set of (conjugate A) *) let ?P = "(\T. T \ set (cols (conjugate A)) \ lin_indpt T)" have *:"\A. ?P A \ finite A \ card A \ d" by (metis List.finite_set assms card_length card_mono carrier_matD(2) cols_length dim_col_conjugate dual_order.trans rev_finite_subset) have **:"?P {}" by (simp add: finite_lin_indpt2) from maximal_exists[OF *] obtain S where S: "maximal S ?P" using ** by (metis (no_types, lifting)) have s_hyp: "S \ set (cols (conjugate A))" "lin_indpt S" using S unfolding maximal_def apply blast by (metis (no_types, lifting) S maximal_def) from rank_card_indpt[OF _ S, of d] have rankeq: "rank (conjugate A) = card S" using assms by auto have 1:"conjugate ` S \ set (cols A)" using S apply auto by (metis (no_types, lifting) cols_conjugate conjugate_id image_eqI in_mono list.set_map s_hyp(1)) have 2: "lin_indpt (conjugate ` S)" apply (rule ccontr) apply (auto simp add: lin_dep_def) proof - fix T c v assume T: "T \ conjugate ` S" "finite T" and lc:"lincomb c T = 0\<^sub>v n" and "v \ T" "c v \ 0" let ?T = "conjugate ` T" let ?c = "conjugate \ c \ conjugate" have 1: "finite ?T" using T by auto have 2: "?T \ S" using T by auto have 3: "?c \ ?T \ UNIV" by auto have "lincomb ?c ?T = (\\<^bsub>V\<^esub>x\T. conjugate (c x) \\<^sub>v conjugate x)" unfolding lincomb_def apply (subst finsum_reindex) apply auto apply (metis "2" carrier_vec_conjugate assms carrier_matD(1) cols_dim image_eqI s_hyp(1) subsetD) by (meson conjugate_cancel_iff inj_onI) also have "... = (\\<^bsub>V\<^esub>x\T. conjugate (c x \\<^sub>v x)) " by (simp add: conjugate_smult_vec) also have "... = conjugate (\\<^bsub>V\<^esub>x\T. (c x \\<^sub>v x))" apply(subst conjugate_finsum[of "\x.(c x \\<^sub>v x)" T]) apply (auto simp add:o_def) by (smt Matrix.carrier_vec_conjugate Pi_I' T(1) assms carrier_matD(1) cols_dim dim_row_conjugate imageE s_hyp(1) smult_carrier_vec subset_eq) also have "... = conjugate (lincomb c T)" using lincomb_def by presburger ultimately have "lincomb ?c ?T = conjugate (lincomb c T)" by auto then have 4:"lincomb ?c ?T = 0\<^sub>v n" using lc by auto from not_lindepD[OF s_hyp(2) 1 2 3 4] have "conjugate \ c \ conjugate \ conjugate ` T \ {0}" . then have "c v = 0" by (simp add: Pi_iff \v \ T\) thus False using \c v \ 0\ by auto qed from rank_ge_card_indpt[OF A 1 2] have 3:"card (conjugate ` S) \ rank A" . have 4: "card (conjugate ` S) = card S" apply (auto intro!: card_image) by (meson conjugate_cancel_iff inj_onI) show ?thesis using rankeq 3 4 by auto qed lemma rank_conjugate: assumes "A \ carrier_mat n d" shows "rank (conjugate A) = rank A" using rank_conjugate_le by (metis carrier_vec_conjugate assms conjugate_id dual_order.antisym) end (* exit the context *) lemma conjugate_transpose_rank: fixes A::"'a::{conjugatable_ordered_field} mat" shows "vec_space.rank (dim_row A) A = vec_space.rank (dim_col A) (A\<^sup>H)" using conjugatable_vec_space.conjugate_transpose_rank_le by (metis (no_types, lifting) Matrix.transpose_transpose carrier_matI conjugate_id dim_col_conjugate dual_order.antisym index_transpose_mat(2) transpose_conjugate) lemma transpose_rank: fixes A::"'a::{conjugatable_ordered_field} mat" shows "vec_space.rank (dim_row A) A = vec_space.rank (dim_col A) (A\<^sup>T)" by (metis carrier_mat_triv conjugatable_vec_space.rank_conjugate conjugate_transpose_rank index_transpose_mat(2)) lemma rank_mat_mul_left: fixes A::"'a::{conjugatable_ordered_field} mat" assumes "A \ carrier_mat n d" assumes "B \ carrier_mat d nc" shows "vec_space.rank n (A * B) \ vec_space.rank d B" by (metis (no_types, lifting) Matrix.transpose_transpose assms(1) assms(2) carrier_matD(1) carrier_matD(2) carrier_mat_triv conjugatable_vec_space.rank_conjugate conjugate_transpose_rank index_mult_mat(3) index_transpose_mat(3) transpose_mult vec_space.rank_mat_mul_right) section "Results on Invertibility" (* Extract specific columns of a matrix *) definition take_cols :: "'a mat \ nat list \ 'a mat" where "take_cols A inds = mat_of_cols (dim_row A) (map ((!) (cols A)) (filter ((>) (dim_col A)) inds))" definition take_cols_var :: "'a mat \ nat list \ 'a mat" where "take_cols_var A inds = mat_of_cols (dim_row A) (map ((!) (cols A)) (inds))" definition take_rows :: "'a mat \ nat list \ 'a mat" where "take_rows A inds = mat_of_rows (dim_col A) (map ((!) (rows A)) (filter ((>) (dim_row A)) inds))" lemma cong1: "x = y \ mat_of_cols n x = mat_of_cols n y" by auto lemma nth_filter: assumes "j < length (filter P ls)" shows "P ((filter P ls) ! j)" by (simp add: assms list_ball_nth) lemma take_cols_mat_mul: assumes "A \ carrier_mat nr n" assumes "B \ carrier_mat n nc" shows "A * take_cols B inds = take_cols (A * B) inds" proof - have "\j. j < length (map ((!) (cols B)) (filter ((>) nc) inds)) \ (map ((!) (cols B)) (filter ((>) nc) inds)) ! j \ carrier_vec n" using assms apply auto apply (subst cols_nth) using nth_filter by auto from mul_mat_of_cols[OF assms(1) this] have "A * take_cols B inds = mat_of_cols nr (map (\x. A *\<^sub>v cols B ! x) (filter ((>) (dim_col B)) inds))" unfolding take_cols_def using assms by (auto simp add: o_def) also have "... = take_cols (A * B) inds" - unfolding take_cols_def using assms apply (auto intro!: cong1) - by (simp add: mult_mat_vec_def) + unfolding take_cols_def using assms by (auto intro!: cong1) ultimately show ?thesis by auto qed lemma take_cols_carrier_mat: assumes "A \ carrier_mat nr nc" obtains n where "take_cols A inds \ carrier_mat nr n" unfolding take_cols_def using assms by fastforce lemma take_cols_carrier_mat_strict: assumes "A \ carrier_mat nr nc" assumes "\i. i \ set inds \ i < nc" shows "take_cols A inds \ carrier_mat nr (length inds)" unfolding take_cols_def using assms by auto lemma gauss_jordan_take_cols: assumes "gauss_jordan A (take_cols A inds) = (C,D)" shows "D = take_cols C inds" proof - obtain nr nc where A: "A \ carrier_mat nr nc" by auto from take_cols_carrier_mat[OF this] obtain n where B: "take_cols A inds \ carrier_mat nr n" by auto from gauss_jordan_transform[OF A B assms, of undefined] obtain P where PP:"P\Units (ring_mat TYPE('a) nr undefined)" and CD: "C = P * A" "D = P * take_cols A inds" by blast have P: "P \ carrier_mat nr nr" by (metis (no_types, lifting) Units_def PP mem_Collect_eq partial_object.select_convs(1) ring_mat_def) from take_cols_mat_mul[OF P A] have "P * take_cols A inds = take_cols (P * A) inds" . thus ?thesis using CD by blast qed lemma dim_col_take_cols: assumes "\j. j \ set inds \ j < dim_col A" shows "dim_col (take_cols A inds) = length inds" unfolding take_cols_def using assms by auto lemma dim_col_take_rows[simp]: shows "dim_col (take_rows A inds) = dim_col A" unfolding take_rows_def by auto lemma cols_take_cols_subset: shows "set (cols (take_cols A inds)) \ set (cols A)" unfolding take_cols_def apply (subst cols_mat_of_cols) apply auto using in_set_conv_nth by fastforce lemma dim_row_take_cols[simp]: shows "dim_row (take_cols A ls) = dim_row A" by (simp add: take_cols_def) lemma dim_row_append_rows[simp]: shows "dim_row (A @\<^sub>r B) = dim_row A + dim_row B" by (simp add: append_rows_def) lemma rows_inj: assumes "dim_col A = dim_col B" assumes "rows A = rows B" shows "A = B" unfolding mat_eq_iff apply auto apply (metis assms(2) length_rows) using assms(1) apply blast by (metis assms(1) assms(2) mat_of_rows_rows) lemma append_rows_index: assumes "dim_col A = dim_col B" assumes "i < dim_row A + dim_row B" assumes "j < dim_col A" shows "(A @\<^sub>r B) $$ (i,j) = (if i < dim_row A then A $$ (i,j) else B $$ (i-dim_row A,j))" unfolding append_rows_def apply (subst index_mat_four_block) using assms by auto lemma row_append_rows: assumes "dim_col A = dim_col B" assumes "i < dim_row A + dim_row B" shows "row (A @\<^sub>r B) i = (if i < dim_row A then row A i else row B (i-dim_row A))" unfolding vec_eq_iff using assms by (auto simp add: append_rows_def) lemma append_rows_mat_mul: assumes "dim_col A = dim_col B" shows "(A @\<^sub>r B) * C = A * C @\<^sub>r B * C" unfolding mat_eq_iff apply auto apply (simp add: append_rows_def) apply (subst index_mult_mat) apply auto apply (simp add: append_rows_def) apply (subst append_rows_index) apply auto apply (simp add: append_rows_def) apply (metis add.right_neutral append_rows_def assms index_mat_four_block(3) index_mult_mat(1) index_mult_mat(3) index_zero_mat(3) row_append_rows trans_less_add1) by (metis add_cancel_right_right add_diff_inverse_nat append_rows_def assms index_mat_four_block(3) index_mult_mat(1) index_mult_mat(3) index_zero_mat(3) nat_add_left_cancel_less row_append_rows) lemma cardlt: shows "card {i. i < (n::nat)} \ n" by simp lemma row_echelon_form_zero_rows: assumes row_ech: "row_echelon_form A" assumes dim_asm: "dim_col A \ dim_row A" shows "take_rows A [0..r 0\<^sub>m (dim_row A - length (pivot_positions A)) (dim_col A) = A" proof - have ex_pivot_fun: "\ f. pivot_fun A f (dim_col A)" using row_ech unfolding row_echelon_form_def by auto have len_help: "length (pivot_positions A) = card {i. i < dim_row A \ row A i \ 0\<^sub>v (dim_col A)}" using ex_pivot_fun pivot_positions[where A = "A",where nr = "dim_row A", where nc = "dim_col A"] by auto then have len_help2: "length (pivot_positions A) \ dim_row A" by (metis (no_types, lifting) card_mono cardlt finite_Collect_less_nat le_trans mem_Collect_eq subsetI) have fileq: "filter (\y. y < dim_row A) [0..< length (pivot_positions A)] = [0..n. card {i. i < n \ row A i \ 0\<^sub>v (dim_col A)} \ n" proof clarsimp fix n have h: "\x. x \ {i. i < n \ row A i \ 0\<^sub>v (dim_col A)} \ x\{.. row A i \ 0\<^sub>v (dim_col A)} \ {.. row A i \ 0\<^sub>v (dim_col A)}::nat) \ (card {.. row A i \ 0\<^sub>v (dim_col A)}::nat) \ (n::nat)" using h2 card_lessThan[of n] by auto qed then have pivot_len: "length (pivot_positions A) \ dim_row A " using len_help by simp have alt_char: "mat_of_rows (dim_col A) (map ((!) (rows A)) (filter (\y. y < dim_col A) [0..i j. i < dim_row A \ j < dim_col A \ i < dim_row (take_rows A [0.. take_rows A [0.. dim_row A" using pivot_len by auto have h1: "take_rows A [0..i < dim_row A\ j_lt) qed let ?nc = "dim_col A" let ?nr = "dim_row A" have h2: "\i j. i < dim_row A \ j < dim_col A \ \ i < dim_row (take_rows A [0.. 0\<^sub>m (dim_row A - length (pivot_positions A)) (dim_col A) $$ (i - dim_row (take_rows A [0.. i < dim_row (take_rows A [0..f. pivot_fun A f (dim_col A) \ f i = ?nc" proof - have half1: "\f. pivot_fun A f (dim_col A)" using assms unfolding row_echelon_form_def by blast have half2: "\f. pivot_fun A f (dim_col A) \ f i = ?nc " proof clarsimp fix f assume is_piv: "pivot_fun A f (dim_col A)" have len_pp: "length (pivot_positions A) = card {i. i < ?nr \ row A i \ 0\<^sub>v ?nc}" using is_piv pivot_positions[of A ?nr ?nc f] by auto have "\i. (i < ?nr \ row A i \ 0\<^sub>v ?nc) \ (i < ?nr \ f i \ ?nc)" using is_piv pivot_fun_zero_row_iff[of A f ?nc ?nr] by blast then have len_pp_var: "length (pivot_positions A) = card {i. i < ?nr \ f i \ ?nc}" using len_pp by auto have allj_hyp: "\j < ?nr. f j = ?nc \ ((Suc j) < ?nr \ f (Suc j) = ?nc)" using is_piv unfolding pivot_fun_def using lt_i by (metis le_antisym le_less) have if_then_bad: "f i \ ?nc \ (\j. j \ i \ f j \ ?nc)" proof clarsimp fix j assume not_i: "f i \ ?nc" assume j_leq: "j \ i" assume bad_asm: "f j = ?nc" have "\k. k \ j \ k < ?nr \ f k = ?nc" proof - fix k :: nat assume a1: "j \ k" assume a2: "k < dim_row A" have f3: "\n. \ n < dim_row A \ f n \ f j \ \ Suc n < dim_row A \ f (Suc n) = f j" using allj_hyp bad_asm by presburger obtain nn :: "nat \ nat \ (nat \ bool) \ nat" where f4: "\n na p nb nc. (\ n \ na \ Suc n \ Suc na) \ (\ p nb \ \ nc \ nb \ \ p (nn nc nb p) \ p nc) \ (\ p nb \ \ nc \ nb \ p nc \ p (Suc (nn nc nb p)))" using inc_induct order_refl by moura then have f5: "\p. \ p k \ p j \ p (Suc (nn j k p))" using a1 by presburger have f6: "\p. \ p k \ \ p (nn j k p) \ p j" using f4 a1 by meson { assume "nn j k (\n. n < dim_row A \ f n \ dim_col A) < dim_row A \ f (nn j k (\n. n < dim_row A \ f n \ dim_col A)) \ dim_col A" moreover { assume "(nn j k (\n. n < dim_row A \ f n \ dim_col A) < dim_row A \ f (nn j k (\n. n < dim_row A \ f n \ dim_col A)) \ dim_col A) \ (\ j < dim_row A \ f j = dim_col A)" then have "\ k < dim_row A \ f k = dim_col A" using f6 by (metis (mono_tags, lifting)) } ultimately have "(\ j < dim_row A \ f j = dim_col A) \ (\ Suc (nn j k (\n. n < dim_row A \ f n \ dim_col A)) < dim_row A \ f (Suc (nn j k (\n. n < dim_row A \ f n \ dim_col A))) = dim_col A) \ \ k < dim_row A \ f k = dim_col A" using bad_asm by blast } moreover { assume "(\ j < dim_row A \ f j = dim_col A) \ (\ Suc (nn j k (\n. n < dim_row A \ f n \ dim_col A)) < dim_row A \ f (Suc (nn j k (\n. n < dim_row A \ f n \ dim_col A))) = dim_col A)" then have "\ k < dim_row A \ f k = dim_col A" using f5 proof - have "\ (Suc (nn j k (\n. n < dim_row A \ f n \ dim_col A)) < dim_row A \ f (Suc (nn j k (\n. n < dim_row A \ f n \ dim_col A))) \ dim_col A) \ \ (j < dim_row A \ f j \ dim_col A)" using \(\ j < dim_row A \ f j = dim_col A) \ (\ Suc (nn j k (\n. n < dim_row A \ f n \ dim_col A)) < dim_row A \ f (Suc (nn j k (\n. n < dim_row A \ f n \ dim_col A))) = dim_col A)\ by linarith then have "\ (k < dim_row A \ f k \ dim_col A)" by (metis (mono_tags, lifting) a2 bad_asm f5 le_less) then show ?thesis by meson qed } ultimately show "f k = dim_col A" using f3 a2 by (metis (lifting) Suc_lessD bad_asm) qed then show "False" using lt_i not_i using j_leq by blast qed have "f i \ ?nc \ ({0.. {y. y < ?nr \ f y \ dim_col A})" proof - have h1: "f i \ dim_col A \ (\j\i. j < ?nr \ f j \ dim_col A)" using if_then_bad lt_i by auto then show ?thesis by auto qed then have gteq: "f i \ ?nc \ (card {i. i < ?nr \ f i \ dim_col A} \ (i+1))" using card_lessThan[of ?ip] card_mono[where B = "{i. i < ?nr \ f i \ dim_col A} ", where A = "{0.. length (pivot_positions A)" using not_lt clear by auto then show "f i = ?nc" using gteq len_pp_var by auto qed show ?thesis using half1 half2 by blast qed then have h1a: "row A i = 0\<^sub>v (dim_col A)" using pivot_fun_zero_row_iff[of A _ ?nc ?nr] using lt_i by blast then have h1: "A $$ (i, j) = 0" using index_row(1) lt_i lt_j by fastforce have h2a: "i - dim_row (take_rows A [0..m (dim_row A - length (pivot_positions A)) (dim_col A) $$ (i - dim_row (take_rows A [0..m (dim_row A - length (pivot_positions A)) (dim_col A) $$ (i - dim_row (take_rows A [0..i j. i < dim_row A \ j < dim_col A \ i < dim_row (take_rows A [0.. dim_row A" proof - have 1: "A \ carrier_mat (dim_row A) (dim_col A)" by auto obtain f where 2: "pivot_fun A f (dim_col A)" using assms row_echelon_form_def by blast from pivot_positions(4)[OF 1 2] have "length (pivot_positions A) = card {i. i < dim_row A \ row A i \ 0\<^sub>v (dim_col A)}" . also have "... \ card {i. i < dim_row A}" apply (rule card_mono) by auto ultimately show ?thesis by auto qed lemma rref_pivot_positions: assumes "row_echelon_form R" assumes R: "R \ carrier_mat nr nc" shows "\i j. (i,j) \ set (pivot_positions R) \ i < nr \ j < nc" proof - obtain f where f: "pivot_fun R f nc" using assms(1) assms(2) row_echelon_form_def by blast have *: "\i. i < nr \ f i \ nc" using f using R pivot_funD(1) by blast from pivot_positions[OF R f] have "set (pivot_positions R) = {(i, f i) |i. i < nr \ f i \ nc}" by auto then have **: "set (pivot_positions R) = {(i, f i) |i. i < nr \ f i < nc}" using * by fastforce fix i j assume "(i, j) \ set (pivot_positions R)" thus "i < nr \ j < nc" using ** by simp qed lemma pivot_fun_monoton: assumes pf: "pivot_fun A f (dim_col A)" assumes dr: "dim_row A = nr" shows "\ i. i < nr \ (\ k. ((k < nr \ i < k) \ f i \ f k))" proof - fix i assume "i < nr" show "(\ k. ((k < nr \ i < k) \ f i \ f k))" proof - fix k show "((k < nr \ i < k) \ f i \ f k)" proof (induct k) case 0 then show ?case by blast next case (Suc k) then show ?case by (smt dr le_less_trans less_Suc_eq less_imp_le_nat pf pivot_funD(1) pivot_funD(3)) qed qed qed lemma pivot_positions_contains: assumes row_ech: "row_echelon_form A" assumes dim_h: "dim_col A \ dim_row A" assumes "pivot_fun A f (dim_col A)" shows "\i < (length (pivot_positions A)). (i, f i) \ set (pivot_positions A)" proof - let ?nr = "dim_row A" let ?nc = "dim_col A" let ?pp = "pivot_positions A" have i_nr: "\i < (length ?pp). i < ?nr" using rref_pivot_positions assms using length_pivot_positions_dim_row less_le_trans by blast have i_nc: "\i < (length ?pp). f i < ?nc" proof clarsimp fix i assume i_lt: "i < length ?pp" have fis_nc: "f i = ?nc \ (\ k > i. k < ?nr \ f k = ?nc)" proof - assume is_nc: "f i = ?nc" show "(\ k > i. k < ?nr \ f k = ?nc)" proof clarsimp fix k assume k_gt: "k > i" assume k_lt: "k < ?nr" have fk_lt: "f k \ ?nc" using pivot_funD(1)[of A ?nr f ?nc k] k_lt apply (auto) using \pivot_fun A f (dim_col A)\ by blast show "f k = ?nc" using fk_lt is_nc k_gt k_lt assms pivot_fun_monoton[of A f ?nr i k] using \pivot_fun A f (dim_col A)\ by auto qed qed have ncimp: "f i = ?nc \ (\ k \i. k \ { i. i < ?nr \ row A i \ 0\<^sub>v ?nc})" proof - assume nchyp: "f i = ?nc" show "(\ k \i. k \ { i. i < ?nr \ row A i \ 0\<^sub>v ?nc})" proof clarsimp fix k assume i_lt: "i \ k" assume k_lt: "k < dim_row A" show "row A k = 0\<^sub>v (dim_col A) " using i_lt k_lt fis_nc using pivot_fun_zero_row_iff[of A f ?nc ?nr] using \pivot_fun A f (dim_col A)\ le_neq_implies_less nchyp by blast qed qed then have "f i = ?nc \ card { i. i < ?nr \ row A i \ 0\<^sub>v ?nc} \ i" proof - assume nchyp: "f i = ?nc" have h: "{ i. i < ?nr \ row A i \ 0\<^sub>v ?nc} \ {0.. row A i \ 0\<^sub>v ?nc} \ i" using card_lessThan using subset_eq_atLeast0_lessThan_card by blast qed then show "f i < ?nc" using i_lt pivot_positions(4)[of A ?nr ?nc f] apply (auto) by (metis \pivot_fun A f (dim_col A)\ i_nr le_neq_implies_less not_less pivot_funD(1)) qed then show ?thesis using pivot_positions(1) by (smt \pivot_fun A f (dim_col A)\ carrier_matI i_nr less_not_refl mem_Collect_eq) qed lemma pivot_positions_form_helper_1: shows "(a, b) \ set (pivot_positions_main_gen z A nr nc i j) \ i \ a" proof (induct i j rule: pivot_positions_main_gen.induct[of nr nc A z]) case (1 i j) then show ?case using pivot_positions_main_gen.simps[of z A nr nc i j] apply (auto) by (smt Suc_leD le_refl old.prod.inject set_ConsD) qed lemma pivot_positions_form_helper_2: - shows "strict_sorted (map fst (pivot_positions_main_gen z A nr nc i j))" + shows "sorted_wrt (<) (map fst (pivot_positions_main_gen z A nr nc i j))" proof (induct i j rule: pivot_positions_main_gen.induct[of nr nc A z]) case (1 i j) - then show ?case using pivot_positions_main_gen.simps[of z A nr nc i j] - apply (auto) using pivot_positions_form_helper_1 - by (simp add: pivot_positions_form_helper_1 Suc_le_lessD) + then show ?case using pivot_positions_main_gen.simps[of z A nr nc i j] + by (auto simp: pivot_positions_form_helper_1 Suc_le_lessD) qed lemma sorted_pivot_positions: - shows "strict_sorted (map fst (pivot_positions A))" + shows "sorted_wrt (<) (map fst (pivot_positions A))" using pivot_positions_form_helper_2 by (simp add: pivot_positions_form_helper_2 pivot_positions_gen_def) lemma pivot_positions_form: assumes row_ech: "row_echelon_form A" assumes dim_h: "dim_col A \ dim_row A" shows "\ i < (length (pivot_positions A)). fst ((pivot_positions A) ! i) = i" proof clarsimp let ?nr = "dim_row A" let ?nc = "dim_col A" let ?pp = "pivot_positions A :: (nat \ nat) list" fix i assume i_lt: "i < length (pivot_positions A)" have "\f. pivot_fun A f ?nc" using row_ech unfolding row_echelon_form_def by blast then obtain f where pf:"pivot_fun A f ?nc" by blast have all_f_in: "\i < (length ?pp). (i, f i) \ set ?pp" using pivot_positions_contains pf assms by blast have sorted_hyp: "\ (p::nat) (q::nat). p < (length ?pp) \ q < (length ?pp) \ p < q \ (fst (?pp ! p) < fst (?pp ! q))" proof - fix p::nat fix q::nat assume p_lt: "p < q" assume p_welldef: "p < (length ?pp)" assume q_welldef: "q < (length ?pp)" show "fst (?pp ! p) < fst (?pp ! q)" using sorted_pivot_positions p_lt p_welldef q_welldef apply (auto) by (smt find_first_unique length_map nat_less_le nth_map p_welldef sorted_nth_mono sorted_pivot_positions strict_sorted_iff) qed have h: "i < (length ?pp) \ fst (pivot_positions A ! i) = i" proof (induct i) case 0 have "\j. fst (pivot_positions A ! j) = 0" by (metis all_f_in fst_conv i_lt in_set_conv_nth length_greater_0_conv list.size(3) not_less0) then obtain j where jth:" fst (pivot_positions A ! j) = 0" by blast have "j \ 0 \ (fst (pivot_positions A ! 0) > 0 \ j \ 0)" using sorted_hyp apply (auto) by (metis all_f_in fst_conv i_lt in_set_conv_nth length_greater_0_conv list.size(3) neq0_conv not_less0) then show ?case using jth neq0_conv by blast next case (Suc i) have ind_h: "i < length (pivot_positions A) \ fst (pivot_positions A ! i) = i" using Suc.hyps by blast have thesis_h: "(Suc i) < length (pivot_positions A) \ fst (pivot_positions A ! (Suc i)) = (Suc i)" proof - assume suc_i_lt: "(Suc i) < length (pivot_positions A)" have fst_i_is: "fst (pivot_positions A ! i) = i" using suc_i_lt ind_h using Suc_lessD by blast have "(\j < (length ?pp). fst (pivot_positions A ! j) = (Suc i))" by (metis suc_i_lt all_f_in fst_conv in_set_conv_nth) then obtain j where jth: "j < (length ?pp) \ fst (pivot_positions A ! j) = (Suc i)" by blast have "j > i" using sorted_hyp apply (auto) by (metis Suc_lessD \fst (pivot_positions A ! i) = i\ jth less_not_refl linorder_neqE_nat n_not_Suc_n suc_i_lt) have "j > (Suc i) \ False" proof - assume j_gt: "j > (Suc i)" then have h1: "fst (pivot_positions A ! (Suc i)) > i" using fst_i_is sorted_pivot_positions using sorted_hyp suc_i_lt by force have "fst (pivot_positions A ! j) > fst (pivot_positions A ! (Suc i))" using jth j_gt sorted_hyp apply (auto) by fastforce then have h2: "fst (pivot_positions A ! (Suc i)) < (Suc i)" using jth by simp show "False" using h1 h2 using not_less_eq by blast qed show "fst (pivot_positions A ! (Suc i)) = (Suc i)" using Suc_lessI \Suc i < j \ False\ \i < j\ jth by blast qed then show ?case by blast qed then show "fst (pivot_positions A ! i) = i" using i_lt by auto qed lemma take_cols_pivot_eq: assumes row_ech: "row_echelon_form A" assumes dim_h: "dim_col A \ dim_row A" shows "take_cols A (map snd (pivot_positions A)) = 1\<^sub>m (length (pivot_positions A)) @\<^sub>r 0\<^sub>m (dim_row A - length (pivot_positions A)) (length (pivot_positions A))" proof - let ?nr = "dim_row A" let ?nc = "dim_col A" have h1: " dim_col (1\<^sub>m (length (pivot_positions A)) @\<^sub>r 0\<^sub>m (dim_row A - length (pivot_positions A)) (length (pivot_positions A))) = (length (pivot_positions A))" by (simp add: append_rows_def) have len_pivot: "length (pivot_positions A) = card {i. i < ?nr \ row A i \ 0\<^sub>v ?nc}" using row_ech pivot_positions(4) row_echelon_form_def by blast have pp_leq_nc: "\f. pivot_fun A f ?nc \ (\i < ?nr. f i \ ?nc)" unfolding pivot_fun_def by meson have pivot_set: "\f. pivot_fun A f ?nc \ set (pivot_positions A) = {(i, f i) | i. i < ?nr \ f i \ ?nc}" using row_ech row_echelon_form_def pivot_positions(1) by (smt (verit) Collect_cong carrier_matI) then have pivot_set_alt: "\f. pivot_fun A f ?nc \ set (pivot_positions A) = {(i, f i) | i. i < ?nr \ row A i \ 0\<^sub>v ?nc}" using pivot_positions pivot_fun_zero_row_iff Collect_cong carrier_mat_triv by (smt (verit, best)) have "\f. pivot_fun A f ?nc \ set (pivot_positions A) = {(i, f i) | i. f i \ ?nc \ i < ?nr \ f i \ ?nc}" using pivot_set pp_leq_nc by auto then have pivot_set_var: "\f. pivot_fun A f ?nc \ set (pivot_positions A) = {(i, f i) | i. i < ?nr \ f i < ?nc}" by auto have "length (map snd (pivot_positions A)) = card (set (map snd (pivot_positions A)))" using row_ech row_echelon_form_def pivot_positions(3) distinct_card[where xs = "map snd (pivot_positions A)"] by (metis carrier_mat_triv) then have "length (map snd (pivot_positions A)) = card (set (pivot_positions A))" by (metis card_distinct distinct_card distinct_map length_map) then have "length (map snd (pivot_positions A)) = card {i. i < ?nr \ row A i \ 0\<^sub>v ?nc}" using pivot_set_alt by (simp add: len_pivot) then have length_asm: "length (map snd (pivot_positions A)) = length (pivot_positions A)" using len_pivot by linarith then have "\a. List.member (map snd (pivot_positions A)) a \ a < dim_col A" proof clarsimp fix a assume a_in: "List.member (map snd (pivot_positions A)) a" have "\v \ set (pivot_positions A). a = snd v" using a_in in_set_member[where xs = "(pivot_positions A)"] apply (auto) by (metis in_set_impl_in_set_zip2 in_set_member length_map snd_conv zip_map_fst_snd) then show "a < dim_col A" using pivot_set_var in_set_member by auto qed then have h2b: "(filter (\y. y < dim_col A) (map snd (pivot_positions A))) = (map snd (pivot_positions A))" by (meson filter_True in_set_member) then have h2a: "length (map ((!) (cols A)) (filter (\y. y < dim_col A) (map snd (pivot_positions A)))) = length (pivot_positions A)" using length_asm by (simp add: h2b) then have h2: "length (pivot_positions A) \ dim_row A \ dim_col (take_cols A (map snd (pivot_positions A))) = (length (pivot_positions A))" unfolding take_cols_def using mat_of_cols_carrier by auto have h_len: "length (pivot_positions A) \ dim_row A \ dim_col (take_cols A (map snd (pivot_positions A))) = dim_col (1\<^sub>m (length (pivot_positions A)) @\<^sub>r 0\<^sub>m (dim_row A - length (pivot_positions A)) (length (pivot_positions A)))" using h1 h2 by (simp add: h1 assms length_pivot_positions_dim_row) have h2: "\i j. length (pivot_positions A) \ dim_row A \ i < dim_row A \ j < dim_col (1\<^sub>m (length (pivot_positions A)) @\<^sub>r 0\<^sub>m (dim_row A - length (pivot_positions A)) (length (pivot_positions A))) \ take_cols A (map snd (pivot_positions A)) $$ (i, j) = (1\<^sub>m (length (pivot_positions A)) @\<^sub>r 0\<^sub>m (dim_row A - length (pivot_positions A)) (length (pivot_positions A))) $$ (i, j)" proof - fix i fix j let ?pp = "(pivot_positions A)" assume len_lt: "length (pivot_positions A) \ dim_row A" assume i_lt: " i < dim_row A" assume j_lt: "j < dim_col (1\<^sub>m (length (pivot_positions A)) @\<^sub>r 0\<^sub>m (dim_row A - length (pivot_positions A)) (length (pivot_positions A)))" let ?w = "((map snd (pivot_positions A)) ! j)" have breaking_it_down: "mat_of_cols (dim_row A) (map ((!) (cols A)) (map snd (pivot_positions A))) $$ (i, j) = ((cols A) ! ?w) $ i" apply (auto) by (metis comp_apply h1 i_lt j_lt length_map mat_of_cols_index nth_map) have h1a: "i < (length ?pp) \ (mat_of_cols (dim_row A) (map ((!) (cols A)) (map snd (pivot_positions A))) $$ (i, j) = (1\<^sub>m (length (pivot_positions A))) $$ (i, j))" proof - (* need to, using row_ech, rely heavily on pivot_fun_def, that num_cols \ num_rows, and row_echelon form*) assume "i < (length ?pp)" have "\f. pivot_fun A f ?nc" using row_ech unfolding row_echelon_form_def by blast then obtain f where "pivot_fun A f ?nc" by blast have j_nc: "j < (length ?pp)" using j_lt by (simp add: h1) then have j_lt_nr: "j < ?nr" using dim_h using len_lt by linarith then have is_this_true: "(pivot_positions A) ! j = (j, f j)" using pivot_positions_form pivot_positions(1)[of A ?nr ?nc f] proof - have "pivot_positions A ! j \ set (pivot_positions A)" using j_nc nth_mem by blast then have "\n. pivot_positions A ! j = (n, f n) \ n < dim_row A \ f n \ dim_col A" using \\A \ carrier_mat (dim_row A) (dim_col A); pivot_fun A f (dim_col A)\ \ set (pivot_positions A) = {(i, f i) |i. i < dim_row A \ f i \ dim_col A}\ \pivot_fun A f (dim_col A)\ by blast then show ?thesis by (metis (no_types) \\A. \row_echelon_form A; dim_row A \ dim_col A\ \ \i dim_h fst_conv j_nc row_ech) qed then have w_is: "?w = f j" by (metis h1 j_lt nth_map snd_conv) have h0: "i = j \ ((cols A) ! ?w) $ i = 1" using w_is pivot_funD(4)[of A ?nr f ?nc i] by (metis \\a. List.member (map snd (pivot_positions A)) a \ a < dim_col A\ \i < length (pivot_positions A)\ \pivot_fun A f (dim_col A)\ cols_length i_lt in_set_member length_asm mat_of_cols_cols mat_of_cols_index nth_mem) have h1: "i \ j \ ((cols A) ! ?w) $ i = 0" using w_is pivot_funD(5) by (metis \\a. List.member (map snd (pivot_positions A)) a \ a < dim_col A\ \pivot_fun A f (dim_col A)\ cols_length h1 i_lt in_set_member j_lt len_lt length_asm less_le_trans mat_of_cols_cols mat_of_cols_index nth_mem) show "(mat_of_cols (dim_row A) (map ((!) (cols A)) (map snd (pivot_positions A))) $$ (i, j) = (1\<^sub>m (length (pivot_positions A))) $$ (i, j))" using h0 h1 breaking_it_down by (metis \i < length (pivot_positions A)\ h2 h_len index_one_mat(1) j_lt len_lt) qed have h1b: "i \ (length ?pp) \ (mat_of_cols (dim_row A) (map ((!) (cols A)) (map snd (pivot_positions A))) $$ (i, j) = 0)" proof - assume i_gt: "i \ (length ?pp)" have h0a: "((cols A) ! ((map snd (pivot_positions A)) ! j)) $ i = (row A i) $ ?w" by (metis \\a. List.member (map snd (pivot_positions A)) a \ a < dim_col A\ cols_length h1 i_lt in_set_member index_row(1) j_lt length_asm mat_of_cols_cols mat_of_cols_index nth_mem) have h0b: "take_rows A [0..r 0\<^sub>m (dim_row A - length (pivot_positions A)) (dim_col A) = A" using assms row_echelon_form_zero_rows[of A] by blast then have h0c: "(row A i) = 0\<^sub>v (dim_col A)" using i_gt using add_diff_cancel_right' add_less_cancel_left diff_is_0_eq' dim_col_take_rows dim_row_append_rows i_lt index_zero_mat(2) index_zero_mat(3) le_add_diff_inverse len_lt less_not_refl3 row_append_rows row_zero zero_less_diff by (smt add_diff_cancel_right' add_less_cancel_left diff_is_0_eq' dim_col_take_rows dim_row_append_rows i_lt index_zero_mat(2) index_zero_mat(3) le_add_diff_inverse len_lt less_not_refl3 row_append_rows row_zero zero_less_diff) then show ?thesis using h0a breaking_it_down apply (auto) by (metis \\a. List.member (map snd (pivot_positions A)) a \ a < dim_col A\ h1 in_set_member index_zero_vec(1) j_lt length_asm nth_mem) qed have h1: " mat_of_cols (dim_row A) (map ((!) (cols A)) (map snd (pivot_positions A))) $$ (i, j) = (1\<^sub>m (length (pivot_positions A)) @\<^sub>r 0\<^sub>m (dim_row A - length (pivot_positions A)) (length (pivot_positions A))) $$ (i, j) " using h1a h1b apply (auto) by (smt add_diff_inverse_nat add_less_cancel_left append_rows_index h1 i_lt index_one_mat(2) index_one_mat(3) index_zero_mat(1) index_zero_mat(2) index_zero_mat(3) j_lt len_lt not_less) then show "take_cols A (map snd (pivot_positions A)) $$ (i, j) = (1\<^sub>m (length (pivot_positions A)) @\<^sub>r 0\<^sub>m (dim_row A - length (pivot_positions A)) (length (pivot_positions A))) $$ (i, j)" unfolding take_cols_def by (simp add: h2b) qed show ?thesis unfolding mat_eq_iff using length_pivot_positions_dim_row[OF assms(1)] h_len h2 by auto qed lemma rref_right_mul: assumes "row_echelon_form A" assumes "dim_col A \ dim_row A" shows "take_cols A (map snd (pivot_positions A)) * take_rows A [0..m (length (pivot_positions A)) @\<^sub>r 0\<^sub>m (dim_row A - length (pivot_positions A)) (length (pivot_positions A))" . have 2: "take_cols A (map snd (pivot_positions A)) * take_rows A [0..r 0\<^sub>m (dim_row A - length (pivot_positions A)) (dim_col A)" unfolding 1 apply (auto simp add: append_rows_mat_mul) by (smt add_diff_cancel_right' assms diff_diff_cancel dim_col_take_rows dim_row_append_rows index_zero_mat(2) left_mult_one_mat' left_mult_zero_mat' length_pivot_positions_dim_row row_echelon_form_zero_rows) from row_echelon_form_zero_rows[OF assms] have "... = A" . thus ?thesis by (simp add: "2") qed context conjugatable_vec_space begin lemma lin_indpt_id: shows "lin_indpt (set (cols (1\<^sub>m n)::'a vec list))" proof - have *: "set (cols (1\<^sub>m n)) = set (rows (1\<^sub>m n))" by (metis cols_transpose transpose_one) have "det (1\<^sub>m n) \ 0" using det_one by auto from det_not_0_imp_lin_indpt_rows[OF _ this] have "lin_indpt (set (rows (1\<^sub>m n)))" using one_carrier_mat by blast thus ?thesis by (simp add: *) qed lemma lin_indpt_take_cols_id: shows "lin_indpt (set (cols (take_cols (1\<^sub>m n) inds)))" proof - have subset_h: "set (cols (take_cols (1\<^sub>m n) inds)) \ set (cols (1\<^sub>m n)::'a vec list)" using cols_take_cols_subset by blast then show ?thesis using lin_indpt_id subset_li_is_li by auto qed lemma cols_id_unit_vecs: shows "cols (1\<^sub>m d) = unit_vecs d" unfolding unit_vecs_def list_eq_iff_nth_eq by auto lemma distinct_cols_id: shows "distinct (cols (1\<^sub>m d)::'a vec list)" by (simp add: conjugatable_vec_space.cols_id_unit_vecs vec_space.unit_vecs_distinct) lemma distinct_map_nth: assumes "distinct ls" assumes "distinct inds" assumes "\j. j \ set inds \ j < length ls" shows "distinct (map ((!) ls) inds)" by (simp add: assms(1) assms(2) assms(3) distinct_map inj_on_nth) lemma distinct_take_cols_id: assumes "distinct inds" shows "distinct (cols (take_cols (1\<^sub>m n) inds) :: 'a vec list)" unfolding take_cols_def apply (subst cols_mat_of_cols) apply (auto intro!: distinct_map_nth simp add: distinct_cols_id) using assms distinct_filter by blast lemma rank_take_cols: assumes "distinct inds" shows "rank (take_cols (1\<^sub>m n) inds) = length (filter ((>) n) inds)" apply (subst lin_indpt_full_rank[of _ "length (filter ((>) n) inds)"]) apply (auto simp add: lin_indpt_take_cols_id) apply (metis (full_types) index_one_mat(2) index_one_mat(3) length_map mat_of_cols_carrier(1) take_cols_def) by (simp add: assms distinct_take_cols_id) lemma rank_mul_left_invertible_mat: fixes A::"'a mat" assumes "invertible_mat A" assumes "A \ carrier_mat n n" assumes "B \ carrier_mat n nc" shows "rank (A * B) = rank B" proof - obtain C where C: "inverts_mat A C" "inverts_mat C A" using assms invertible_mat_def by blast from C have ceq: "C * A = 1\<^sub>m n" by (metis assms(2) carrier_matD(2) index_mult_mat(3) index_one_mat(3) inverts_mat_def) then have *:"B = C*A*B" using assms(3) by auto from rank_mat_mul_left[OF assms(2-3)] have **: "rank (A*B) \ rank B" . have 1: "C \ carrier_mat n n" using C ceq by (metis assms(2) carrier_matD(1) carrier_matI index_mult_mat(3) index_one_mat(3) inverts_mat_def) have 2: "A * B \ carrier_mat n nc" using assms by auto have "rank B = rank (C* A * B)" using * by auto also have "... \ rank (A*B)" using rank_mat_mul_left[OF 1 2] using "1" assms(2) assms(3) by auto ultimately show ?thesis using ** by auto qed lemma invertible_take_cols_rank: fixes A::"'a mat" assumes "invertible_mat A" assumes "A \ carrier_mat n n" assumes "distinct inds" shows "rank (take_cols A inds) = length (filter ((>) n) inds)" proof - have " A = A * 1\<^sub>m n" using assms(2) by auto then have "take_cols A inds = A * take_cols (1\<^sub>m n) inds" by (metis assms(2) one_carrier_mat take_cols_mat_mul) then have "rank (take_cols A inds) = rank (take_cols (1\<^sub>m n) inds)" by (metis assms(1) assms(2) conjugatable_vec_space.rank_mul_left_invertible_mat one_carrier_mat take_cols_carrier_mat) thus ?thesis by (simp add: assms(3) conjugatable_vec_space.rank_take_cols) qed lemma rank_take_cols_leq: assumes R:"R \ carrier_mat n nc" shows "rank (take_cols R ls) \ rank R" proof - from take_cols_mat_mul[OF R] have "take_cols R ls = R * take_cols (1\<^sub>m nc) ls" by (metis assms one_carrier_mat right_mult_one_mat) thus ?thesis by (metis assms one_carrier_mat take_cols_carrier_mat vec_space.rank_mat_mul_right) qed lemma rank_take_cols_geq: assumes R:"R \ carrier_mat n nc" assumes t:"take_cols R ls \ carrier_mat n r" assumes B:"B \ carrier_mat r nc" assumes "R = (take_cols R ls) * B" shows "rank (take_cols R ls) \ rank R" by (metis B assms(4) t vec_space.rank_mat_mul_right) lemma rref_drop_pivots: assumes row_ech: "row_echelon_form R" assumes dims: "R \ carrier_mat n nc" assumes order: "nc \ n" shows "rank (take_cols R (map snd (pivot_positions R))) = rank R" proof - let ?B = "take_rows R [0..r. take_cols R (map snd (pivot_positions R)) \ carrier_mat n r \ ?B \ carrier_mat r nc" proof - have h1: "take_cols R (map snd (pivot_positions R)) \ carrier_mat n (length (pivot_positions R))" using assms by (metis in_set_impl_in_set_zip2 length_map rref_pivot_positions take_cols_carrier_mat_strict zip_map_fst_snd) have "\ f. pivot_fun R f nc" using row_ech unfolding row_echelon_form_def using dims by blast then have "length (pivot_positions R) = card {i. i < n \ row R i \ 0\<^sub>v nc}" using pivot_positions[of R n nc] using dims by auto then have "nc \ length (pivot_positions R)" using order using carrier_matD(1) dims dual_order.trans length_pivot_positions_dim_row row_ech by blast then have "dim_col R \ length (pivot_positions R)" using dims by auto then have h2: "?B \ carrier_mat (length (pivot_positions R)) nc" unfolding take_rows_def using dims by (smt atLeastLessThan_iff carrier_matD(2) filter_True le_eq_less_or_eq length_map length_pivot_positions_dim_row less_trans map_nth mat_of_cols_carrier(1) row_ech set_upt transpose_carrier_mat transpose_mat_of_rows) show ?thesis using h1 h2 by blast qed (* prove the other two dimensionality assumptions *) have "rank R \ rank (take_cols R (map snd (pivot_positions R)))" using dims ex_r rank_take_cols_geq[where R = "R", where B = "?B", where ls = "(map snd (pivot_positions R))", where nc = "nc"] using equa by blast thus ?thesis using assms(2) conjugatable_vec_space.rank_take_cols_leq le_antisym by blast qed lemma gjs_and_take_cols_var: fixes A::"'a mat" assumes A:"A \ carrier_mat n nc" assumes order: "nc \ n" shows "(take_cols A (map snd (pivot_positions (gauss_jordan_single A)))) = (take_cols_var A (map snd (pivot_positions (gauss_jordan_single A))))" proof - let ?gjs = "(gauss_jordan_single A)" have "\x. List.member (map snd (pivot_positions (gauss_jordan_single A))) x \ x \ dim_col A" using rref_pivot_positions gauss_jordan_single(3) carrier_matD(2) gauss_jordan_single(2) in_set_impl_in_set_zip2 in_set_member length_map less_irrefl less_trans not_le_imp_less zip_map_fst_snd by (smt A carrier_matD(2) gauss_jordan_single(2) in_set_impl_in_set_zip2 in_set_member length_map less_irrefl less_trans not_le_imp_less zip_map_fst_snd) then have "(filter (\y. y < dim_col A) (map snd (pivot_positions (gauss_jordan_single A)))) = (map snd (pivot_positions (gauss_jordan_single A)))" by (metis (no_types, lifting) A carrier_matD(2) filter_True gauss_jordan_single(2) gauss_jordan_single(3) in_set_impl_in_set_zip2 length_map rref_pivot_positions zip_map_fst_snd) then show ?thesis unfolding take_cols_def take_cols_var_def by simp qed lemma gauss_jordan_single_rank: fixes A::"'a mat" assumes A:"A \ carrier_mat n nc" assumes order: "nc \ n" shows "rank (take_cols A (map snd (pivot_positions (gauss_jordan_single A)))) = rank A" proof - let ?R = "gauss_jordan_single A" obtain P where P:"P\Units (ring_mat TYPE('a) n undefined)" and i: "?R = P * A" using gauss_jordan_transform[OF A] using A assms det_mult det_non_zero_imp_unit det_one gauss_jordan_single(4) mult_not_zero one_neq_zero by (smt A assms det_mult det_non_zero_imp_unit det_one gauss_jordan_single(4) mult_not_zero one_neq_zero) have pcarrier: "P \ carrier_mat n n" using P unfolding Units_def by (auto simp add: ring_mat_def) have "invertible_mat P" using P unfolding invertible_mat_def Units_def inverts_mat_def apply auto apply (simp add: ring_mat_simps(5)) by (metis index_mult_mat(2) index_one_mat(2) ring_mat_simps(1) ring_mat_simps(3)) then obtain Pi where Pi: "invertible_mat Pi" "Pi * P = 1\<^sub>m n" proof - assume a1: "\Pi. \invertible_mat Pi; Pi * P = 1\<^sub>m n\ \ thesis" have "dim_row P = n" by (metis (no_types) A assms(1) carrier_matD(1) gauss_jordan_single(2) i index_mult_mat(2)) then show ?thesis using a1 by (metis (no_types) \invertible_mat P\ index_mult_mat(3) index_one_mat(3) invertible_mat_def inverts_mat_def square_mat.simps) qed then have pi_carrier:"Pi \ carrier_mat n n" by (metis carrier_mat_triv index_mult_mat(2) index_one_mat(2) invertible_mat_def square_mat.simps) have R1:"row_echelon_form ?R" using assms(2) gauss_jordan_single(3) by blast have R2: "?R \ carrier_mat n nc" using A assms(2) gauss_jordan_single(2) by auto have Rcm: "take_cols ?R (map snd (pivot_positions ?R)) \ carrier_mat n (length (map snd (pivot_positions ?R)))" apply (rule take_cols_carrier_mat_strict[OF R2]) using rref_pivot_positions[OF R1 R2] by auto have "Pi * ?R = A" using i Pi by (smt A \invertible_mat P\ assoc_mult_mat carrier_mat_triv index_mult_mat(2) index_mult_mat(3) index_one_mat(3) invertible_mat_def left_mult_one_mat square_mat.simps) then have "rank (take_cols A (map snd (pivot_positions ?R))) = rank (take_cols (Pi * ?R) (map snd (pivot_positions ?R)))" by auto also have "... = rank ( Pi * take_cols ?R (map snd (pivot_positions ?R)))" by (metis A gauss_jordan_single(2) pi_carrier take_cols_mat_mul) also have "... = rank (take_cols ?R (map snd (pivot_positions ?R)))" by (intro rank_mul_left_invertible_mat[OF Pi(1) pi_carrier Rcm]) also have "... = rank ?R" using assms(2) conjugatable_vec_space.rref_drop_pivots gauss_jordan_single(3) using R1 R2 by blast ultimately show ?thesis using A \P \ carrier_mat n n\ \invertible_mat P\ conjugatable_vec_space.rank_mul_left_invertible_mat i by auto qed lemma lin_indpt_subset_cols: fixes A:: "'a mat" fixes B:: "'a vec set" assumes "A \ carrier_mat n n" assumes inv: "invertible_mat A" assumes "B \ set (cols A)" shows "lin_indpt B" proof - have "det A \ 0" using assms(1) inv invertible_det by blast then have "lin_indpt (set (rows A\<^sup>T))" using assms(1) idom_vec.lin_dep_cols_imp_det_0 by auto thus ?thesis using subset_li_is_li assms(3) by auto qed lemma rank_invertible_subset_cols: fixes A:: "'a mat" fixes B:: "'a vec list" assumes inv: "invertible_mat A" assumes A_square: "A \ carrier_mat n n" assumes set_sub: "set (B) \ set (cols A)" assumes dist_B: "distinct B" shows "rank (mat_of_cols n B) = length B" proof - let ?B_mat = "(mat_of_cols n B)" have h1: "lin_indpt (set(B))" using assms lin_indpt_subset_cols[of A] by auto have "set B \ carrier_vec n" using set_sub A_square cols_dim[of A] by auto then have cols_B: "cols (mat_of_cols n B) = B" using cols_mat_of_cols by auto then have "maximal (set B) (\T. T \ set (B) \ lin_indpt T)" using h1 by (simp add: maximal_def subset_antisym) then have h2: "maximal (set B) (\T. T \ set (cols (mat_of_cols n B)) \ lin_indpt T)" using cols_B by auto have h3: "rank (mat_of_cols n B) = card (set B)" using h1 h2 rank_card_indpt[of ?B_mat] using mat_of_cols_carrier(1) by blast then show ?thesis using assms distinct_card by auto qed end end \ No newline at end of file diff --git a/thys/BenOr_Kozen_Reif/Renegar_Decision.thy b/thys/BenOr_Kozen_Reif/Renegar_Decision.thy --- a/thys/BenOr_Kozen_Reif/Renegar_Decision.thy +++ b/thys/BenOr_Kozen_Reif/Renegar_Decision.thy @@ -1,809 +1,809 @@ theory Renegar_Decision imports "Renegar_Proofs" "BKR_Decision" begin (* Note that there is significant overlap between Renegar and BKR in general, so there is some similarity between this file and BKR_Decision.thy. However, there are also notable differences as Renegar and BKR use different auxiliary polynomials in their decision procedures. In general, the _R's on definition and lemma names in this file are to emphasize that we are working with Renegar style. *) section "Algorithm" (* The set of all rational sign vectors for qs wrt the set S When S = UNIV, then this quantifies over all reals *) definition consistent_sign_vectors_R::"real poly list \ real set \ rat list set" where "consistent_sign_vectors_R qs S = (consistent_sign_vec qs) ` S" primrec prod_list_var:: "real poly list \ real poly" where "prod_list_var [] = 1" | "prod_list_var (h#T) = (if h = 0 then (prod_list_var T) else (h* prod_list_var T))" primrec check_all_const_deg:: "real poly list \ bool" where "check_all_const_deg [] = True" | "check_all_const_deg (h#T) = (if degree h = 0 then (check_all_const_deg T) else False)" definition poly_f :: "real poly list \ real poly" where "poly_f ps = (if (check_all_const_deg ps = True) then [:0, 1:] else (pderiv (prod_list_var ps)) * (prod_list_var ps)* ([:-(crb (prod_list_var ps)),1:]) * ([:(crb (prod_list_var ps)),1:]))" definition find_consistent_signs_R :: "real poly list \ rat list list" where "find_consistent_signs_R ps = find_consistent_signs_at_roots_R (poly_f ps) ps" definition decide_universal_R :: "real poly fml \ bool" where [code]: "decide_universal_R fml = ( let (fml_struct,polys) = convert fml; conds = find_consistent_signs_R polys in list_all (lookup_sem fml_struct) conds )" definition decide_existential_R :: "real poly fml \ bool" where [code]: "decide_existential_R fml = ( let (fml_struct,polys) = convert fml; conds = find_consistent_signs_R polys in find (lookup_sem fml_struct) conds \ None )" subsection "Proofs" definition roots_of_poly_f:: "real poly list \ real set" where "roots_of_poly_f qs = {x. poly (poly_f qs) x = 0}" lemma prod_list_var_nonzero: shows "prod_list_var qs \ 0" proof (induct qs) case Nil then show ?case by auto next case (Cons a qs) then show ?case by auto qed lemma q_dvd_prod_list_var_prop: assumes "q \ set qs" assumes "q \ 0" shows "q dvd prod_list_var qs" using assms proof (induct qs) case Nil then show ?case by auto next case (Cons a qs) then have eo: "q = a \q \ set qs" by auto have c1: "q = a \ q dvd prod_list_var (a#qs)" proof - assume "q = a" then have "prod_list_var (a#qs) = q*(prod_list_var qs)" using Cons.prems unfolding prod_list_var_def by auto then show ?thesis using prod_list_var_nonzero[of qs] by auto qed have c2: "q \ set qs \ q dvd prod_list_var qs" using Cons.prems Cons.hyps unfolding prod_list_var_def by auto show ?case using eo c1 c2 by auto qed lemma check_all_const_deg_prop: shows "check_all_const_deg l = True \ (\p \ set(l). degree p = 0)" proof (induct l) case Nil then show ?case by auto next case (Cons a l) then show ?case by auto qed (* lemma prod_zero shows that the product of the polynomial list is 0 at x iff there is a polynomial in the list that is 0 at x *) lemma poly_f_nonzero: fixes qs :: "real poly list" shows "(poly_f qs) \ 0" proof - have eo: "(\p \ set qs. degree p = 0) \ (\p \ set qs. degree p > 0)" by auto have c1: "(\p \ set qs. degree p = 0) \ (poly_f qs) \ 0" unfolding poly_f_def using check_all_const_deg_prop by auto have c2: "(\p \ set qs. degree p > 0) \ (poly_f qs) \ 0" proof clarsimp fix q assume q_in: "q \ set qs" assume deg_q: "0 < degree q" assume contrad: "poly_f qs = 0" have nonconst: "check_all_const_deg qs = False" using deg_q check_all_const_deg_prop q_in by auto have h1: "prod_list_var qs \ 0" using prod_list_var_nonzero by auto then have "degree (prod_list_var qs) > 0" using q_in deg_q h1 proof (induct qs) case Nil then show ?case by auto next case (Cons a qs) have q_nonz: "q \ 0" using Cons.prems by auto have q_ins: "q \ set (a # qs) " using Cons.prems by auto then have "q = a \ q \ set qs" by auto then have eo: " q = a \ List.member qs q" using in_set_member[of q qs] by auto have degq: "degree q > 0" using Cons.prems by auto have h2: "(prod_list (a # qs)) = a* (prod_list qs)" by auto have isa: "q = a \ 0 < degree (prod_list_var (a # qs))" using h2 degree_mult_eq_0[where p = "q", where q = "prod_list_var qs"] Cons.prems by auto have inl: "List.member qs q \ 0 < degree (prod_list_var (a # qs))" proof - have nonzprod: "prod_list_var (a # qs) \ 0" using prod_list_var_nonzero by auto have "q dvd prod_list_var (a # qs)" using q_dvd_prod_list_var_prop[where q = "q", where qs = "(a#qs)"] q_nonz q_ins by auto then show ?thesis using divides_degree[where p = "q", where q = "prod_list_var (a # qs)"] nonzprod degq by auto qed then show ?case using eo isa by auto qed then have h2: "pderiv (prod_list_var qs) \ 0" using pderiv_eq_0_iff[where p = "prod_list_var qs"] by auto then have "pderiv (prod_list_var qs) * prod_list_var qs \ 0" using prod_list_var_nonzero h2 by auto then show "False" using contrad nonconst unfolding poly_f_def deg_q by (smt (z3) mult_eq_0_iff pCons_eq_0_iff) qed show ?thesis using eo c1 c2 by auto qed lemma poly_f_roots_prop_1: fixes qs:: "real poly list" assumes non_const: "check_all_const_deg qs = False" shows "\x1. \x2. ((x1 < x2 \ (\q1 \ set (qs). q1 \ 0 \ (poly q1 x1) = 0) \ (\q2\ set(qs). q2 \ 0 \ (poly q2 x2) = 0)) \ (\q. x1 < q \ q < x2 \ poly (poly_f qs) q = 0))" proof clarsimp fix x1:: "real" fix x2:: "real" fix q1:: "real poly" fix q2:: "real poly" assume "x1 < x2" assume q1_in: "q1 \ set qs" assume q1_0: "poly q1 x1 = 0" assume q1_nonz: "q1 \ 0" assume q2_in: "q2 \ set qs" assume q2_0: "poly q2 x2 = 0" assume q2_nonz: "q2 \ 0" have prod_z_x1: "poly (prod_list_var qs) x1 = 0" using q1_in q1_0 using q1_nonz q_dvd_prod_list_var_prop[of q1 qs] by auto have prod_z_x2: "poly (prod_list_var qs) x2 = 0" using q2_in q2_0 using q2_nonz q_dvd_prod_list_var_prop[of q2 qs] by auto have "\w>x1. w < x2 \ poly (pderiv (prod_list_var qs)) w = 0" using Rolle_pderiv[where q = "prod_list_var qs"] prod_z_x1 prod_z_x2 using \x1 < x2\ by blast then obtain w where w_def: "w > x1 \w < x2 \ poly (pderiv (prod_list_var qs)) w = 0" by auto then have "poly (poly_f qs) w = 0" unfolding poly_f_def using non_const by simp then show "\q>x1. q < x2 \ poly (poly_f qs) q = 0" using w_def by blast qed lemma main_step_aux1_R: fixes qs:: "real poly list" assumes non_const: "check_all_const_deg qs = True" shows "set (find_consistent_signs_R qs) = consistent_sign_vectors_R qs UNIV" proof - have poly_f_is: "poly_f qs = [:0, 1:]" unfolding poly_f_def using assms by auto have same: "set (find_consistent_signs_at_roots_R [:0, 1:] qs) = set (characterize_consistent_signs_at_roots [:0, 1:] qs)" using find_consistent_signs_at_roots_R[of "[:0, 1:]" qs] by auto have rech: "(sorted_list_of_set {x. poly ([:0, 1:]::real poly) x = 0}) = [0]" by auto have alldeg0: "(\p \ set qs. degree p = 0)" using non_const check_all_const_deg_prop by auto then have allconst: "\p \ set qs. (\(k::real). p = [:k:])" apply (auto) by (meson degree_eq_zeroE) then have allconstvar: "\p \ set qs. \(x::real). \(y::real). poly p x = poly p y" by fastforce have e1: "set (remdups (map (signs_at qs) [0])) \ consistent_sign_vectors_R qs UNIV" unfolding signs_at_def squash_def consistent_sign_vectors_R_def consistent_sign_vec_def apply (simp) by (smt (verit, best) class_ring.ring_simprules(2) comp_def image_iff length_map map_nth_eq_conv) have e2: "consistent_sign_vectors_R qs UNIV \ set (remdups (map (signs_at qs) [0])) " unfolding signs_at_def squash_def consistent_sign_vectors_R_def consistent_sign_vec_def apply (simp) using allconstvar by (smt (verit, best) comp_apply image_iff insert_iff map_eq_conv subsetI) have "set (remdups (map (signs_at qs) [0])) = consistent_sign_vectors_R qs UNIV" using e1 e2 by auto then have "set (characterize_consistent_signs_at_roots [:0, 1:] qs) = consistent_sign_vectors_R qs UNIV" unfolding characterize_consistent_signs_at_roots_def characterize_root_list_p_def using rech by auto then show ?thesis using same poly_f_is unfolding find_consistent_signs_R_def by auto qed lemma sorted_list_lemma_var: fixes l:: "real list" fixes x:: "real" assumes "length l > 1" - assumes strict_sort: "strict_sorted l" + assumes strict_sort: "sorted_wrt (<) l" assumes x_not_in: "\ (List.member l x)" assumes lt_a: "x > (l ! 0)" assumes b_lt: "x < (l ! (length l - 1))" shows "(\n. n < length l - 1 \ x > l ! n \ x < l !(n+1))" using assms proof (induct l) case Nil then show ?case by auto next case (Cons a l) have len_gteq: "length l \ 1" using Cons.prems(1) by (metis One_nat_def Suc_eq_plus1 list.size(4) not_le not_less_eq) have len_one: "length l = 1 \ (\n. n < length (a#l) - 1 \ x > (a#l) ! n \ x < (a#l) !(n+1))" proof - assume len_is: "length l = 1" then have "x > (a#l) ! 0 \ x < (a#l) !1 " using Cons.prems(4) Cons.prems(5) by auto then show "(\n. n < length (a#l) - 1 \ x > (a#l) ! n \ x < (a#l) !(n+1))" using len_is by auto qed have len_gt: "length l > 1 \ (\n. n < length (a#l) - 1 \ x > (a#l) ! n \ x < (a#l) !(n+1))" proof - assume len_gt_one: "length l > 1" have eo: "x \ l ! 0" using Cons.prems(3) apply (auto) by (metis One_nat_def Suc_lessD in_set_member len_gt_one member_rec(1) nth_mem) have c1: "x < l ! 0 \ (\n. n < length (a#l) - 1 \ x > (a#l) ! n \ x < (a#l) !(n+1)) " proof - assume xlt: "x < l !0" then have "x < (a#l) ! 1 " by simp then show ?thesis using Cons.prems(4) len_gt_one apply (auto) using Cons.prems(4) Suc_lessD by blast qed have c2: "x > l ! 0 \ (\n. n < length (a#l) - 1 \ x > (a#l) ! n \ x < (a#l) !(n+1)) " proof - assume asm: "x > l ! 0" have xlt_1: " x < l ! (length l - 1)" using Cons.prems(5) by (metis Cons.prems(1) One_nat_def add_diff_cancel_right' list.size(4) nth_Cons_pos zero_less_diff) - have ssl: "strict_sorted l " using Cons.prems(2) - using strict_sorted.simps(2) by blast + have ssl: "sorted_wrt (<) l " using Cons.prems(2) + using sorted_wrt.simps(2) by auto have " \ List.member l x" using Cons.prems(3) by (meson member_rec(1)) then have " \n x < l ! (n + 1)" using asm xlt_1 len_gt_one ssl Cons.hyps by auto then show ?thesis by (metis One_nat_def Suc_eq_plus1 diff_Suc_1 less_diff_conv list.size(4) nth_Cons_Suc) qed show "(\n. n < length (a#l) - 1 \ x > (a#l) ! n \ x < (a#l) !(n+1))" using eo c1 c2 by (meson linorder_neqE_linordered_idom) qed then show ?case using len_gteq len_one len_gt apply (auto) by (metis One_nat_def less_numeral_extra(1) linorder_neqE_nat not_less nth_Cons_0) qed (* We want to show that our auxiliary polynomial has roots in all relevant intervals: so it captures all of the zeros, and also it captures all of the points in between! *) lemma all_sample_points_prop: assumes is_not_const: "check_all_const_deg qs = False" assumes s_is: "S = (characterize_root_list_p (pderiv (prod_list_var qs) * (prod_list_var qs) * ([:-(crb (prod_list_var qs)),1:]) * ([:(crb (prod_list_var qs)),1:])))"(* properties about S*) shows "consistent_sign_vectors_R qs UNIV = consistent_sign_vectors_R qs (set S)" proof - let ?zer_list = "sorted_list_of_set {(x::real). (\q \ set(qs). (q \ 0 \ poly q x = 0))} :: real list" - have strict_sorted_h: "strict_sorted ?zer_list" using sorted_sorted_list_of_set + have strict_sorted_h: "sorted_wrt (<) ?zer_list" using sorted_sorted_list_of_set strict_sorted_iff by auto have poly_f_is: "poly_f qs = (pderiv (prod_list_var qs) * prod_list_var qs)* ([:-(crb (prod_list_var qs)),1:]) * ([:(crb (prod_list_var qs)),1:])" unfolding poly_f_def using is_not_const by auto then have set_S_char: "set S = ({x. poly (poly_f qs) x = 0}::real set)" using poly_roots_finite[of "poly_f qs"] set_sorted_list_of_set poly_f_nonzero[of qs] using s_is unfolding characterize_root_list_p_def by auto have difficult_direction: "consistent_sign_vectors_R qs UNIV \ consistent_sign_vectors_R qs (set S)" proof clarsimp fix x assume "x \ consistent_sign_vectors_R qs UNIV " then have "\y. x = (consistent_sign_vec qs y)" unfolding consistent_sign_vectors_R_def by auto then obtain y where y_prop: "x = consistent_sign_vec qs y" by auto then have "\ k \ (set S). consistent_sign_vec qs k = consistent_sign_vec qs y" proof - have c1: "(\q \ (set qs). q \ 0 \ poly q y = 0) \ (\ k \ (set S). consistent_sign_vec qs k = consistent_sign_vec qs y)" proof - assume "(\q \ (set qs). q \ 0 \ poly q y = 0)" then obtain q where "q \ (set qs) \ q \ 0 \ poly q y = 0" by auto then have "poly (prod_list_var qs) y = 0" using q_dvd_prod_list_var_prop[of q qs] by auto then have "poly (pderiv (prod_list_var qs) * (prod_list_var qs)*([:-(crb (prod_list_var qs)),1:]) * ([:(crb (prod_list_var qs)),1:])) y = 0" by auto then have "y \ (set S)" using s_is unfolding characterize_root_list_p_def proof - have "y \ {r. poly (pderiv (prod_list_var qs) * (prod_list_var qs)*([:-(crb (prod_list_var qs)),1:]) * ([:(crb (prod_list_var qs)),1:])) r = 0}" using \poly (pderiv (prod_list_var qs) * (prod_list_var qs)*([:-(crb (prod_list_var qs)),1:]) * ([:(crb (prod_list_var qs)),1:])) y = 0\ by force then show ?thesis by (metis characterize_root_list_p_def is_not_const poly_f_def poly_f_nonzero poly_roots_finite s_is set_sorted_list_of_set) qed then show "\ k \ (set S). consistent_sign_vec qs k = consistent_sign_vec qs y" by auto qed have len_gtz_prop: "length ?zer_list > 0 \ ((\w. w < length ?zer_list \ y = ?zer_list ! w) \ (y < ?zer_list ! 0) \ (y > ?zer_list ! (length ?zer_list - 1)) \ (\k < (length ?zer_list - 1). y > ?zer_list ! k \ y < ?zer_list ! (k+1)))" proof - let ?c = "(\w. w < length ?zer_list \ y = ?zer_list ! w) \ (y < ?zer_list ! 0) \ (y > ?zer_list ! (length ?zer_list - 1)) \ (\k < (length ?zer_list - 1). y > ?zer_list ! k \ y < ?zer_list ! (k+1))" have lis1: "length ?zer_list = 1 \ ?c" by auto have h1: "\(\w. w < length ?zer_list \ y = ?zer_list ! w) \ \ (List.member ?zer_list y)" by (metis (no_types, lifting) in_set_conv_nth in_set_member) have h2: "(length ?zer_list > 0 \ \(\w. w < length ?zer_list \ y = ?zer_list ! w) \ \ (y < ?zer_list ! 0)) \ y > ?zer_list ! 0" by auto have h3: "(length ?zer_list > 1 \ \(\w. w < length ?zer_list \ y = ?zer_list ! w) \ \ (y > ?zer_list ! (length ?zer_list - 1))) \ y < ?zer_list ! (length ?zer_list - 1)" apply (auto) by (smt (z3) diff_Suc_less gr_implies_not0 not_gr_zero) have "length ?zer_list > 1 \ \(\w. w < length ?zer_list \ y = ?zer_list ! w) \ \ (y < ?zer_list ! 0) \ \ (y > ?zer_list ! (length ?zer_list - 1)) \ (\k < (length ?zer_list - 1). y > ?zer_list ! k \ y < ?zer_list ! (k+1))" using h1 h2 h3 strict_sorted_h sorted_list_lemma_var[of ?zer_list y] using One_nat_def Suc_lessD by presburger then have lgt1: "length ?zer_list > 1 \ ?c" by auto then show ?thesis using lis1 lgt1 by (smt (z3) diff_is_0_eq' not_less) qed have neg_crb_in: "(- crb (prod_list_var qs)) \ set S" using set_S_char poly_f_is by auto have pos_crb_in: "(crb (prod_list_var qs)) \ set S" using set_S_char poly_f_is by auto have set_S_nonempty: "set S \ {}" using neg_crb_in by auto have finset: "finite {x. \q\set qs. q \ 0 \ poly q x = 0}" proof - have "\q \ set qs. q\ 0 \ finite {x. poly q x = 0} " using poly_roots_finite by auto then show ?thesis by auto qed have c2: "\(\q \ (set qs). q \ 0 \ poly q y = 0) \ \ k \ (set S). consistent_sign_vec qs k = consistent_sign_vec qs y" proof - assume "\(\q \ (set qs). q \ 0 \ poly q y = 0)" have c_c1: "length ?zer_list = 0 \ \ k \ (set S). consistent_sign_vec qs k = consistent_sign_vec qs y" proof - assume "length ?zer_list = 0" then have "\q \ set (qs). \ (x:: real). \(y::real). squash (poly q x) = squash (poly q y)" proof clarsimp fix q x y assume czer: "card {x. \q\set qs. q \ 0 \ poly q x = 0} = 0" assume qin: "q \ set qs" have fin_means_empty: "{x. \q\set qs. q \ 0 \ poly q x = 0} = {}" using finset czer by auto have qzer: "q = 0 \ squash (poly q x) = squash (poly q y)" by auto have qnonz: "q \ 0 \ squash (poly q x) = squash (poly q y)" proof - assume qnonz: "q \ 0" then have noroots: "{x. poly q x = 0} = {}" using qin finset using Collect_empty_eq fin_means_empty by auto have nonzsq1: "squash (poly q x) \ 0" using fin_means_empty qnonz czer qin unfolding squash_def by auto then have eo: "(poly q x) > 0 \ (poly q x) < 0" unfolding squash_def apply (auto) by presburger have eo1: "poly q x > 0 \ poly q y > 0" using noroots poly_IVT_pos[of y x q] poly_IVT_neg[of x y q] apply (auto) by (metis linorder_neqE_linordered_idom) have eo2: "poly q x < 0 \ poly q y < 0" using noroots poly_IVT_pos[of x y q] poly_IVT_neg[of y x q] apply (auto) by (metis linorder_neqE_linordered_idom) then show "squash (poly q x) = squash (poly q y)" using eo eo1 eo2 unfolding squash_def by auto qed show "squash (poly q x) = squash (poly q y)" using qzer qnonz by blast qed then have "\q \ set (qs). squash (poly q y) = squash (poly q (- crb (prod_list_var qs)))" by auto then show "\ k \ (set S). consistent_sign_vec qs k = consistent_sign_vec qs y" using neg_crb_in unfolding consistent_sign_vec_def squash_def apply (auto) by (metis (no_types, hide_lams) antisym_conv3 class_field.neg_1_not_0 equal_neg_zero less_irrefl of_int_minus) qed have c_c2: "length ?zer_list > 0 \ \ k \ (set S). consistent_sign_vec qs k = consistent_sign_vec qs y" proof - assume lengt: "length ?zer_list > 0" let ?t = " \ k \ (set S). consistent_sign_vec qs k = consistent_sign_vec qs y" have sg1: "(\w. w < length ?zer_list \ y = ?zer_list ! w) \ ?t" proof - assume "(\w. w < length ?zer_list \ y = ?zer_list ! w)" then obtain w where w_prop: "w < length ?zer_list \ y = ?zer_list ! w" by auto then have " y \ {x. \q\set qs. q \ 0 \ poly q x = 0}" using finset set_sorted_list_of_set[of "{x. \q\set qs. q \ 0 \ poly q x = 0}"] by (smt (verit, best) nth_mem) then have "y \ {x. poly (poly_f qs) x = 0}" using poly_f_is using \\ (\q\set qs. q \ 0 \ poly q y = 0)\ by blast then show ?thesis using set_S_char by blast qed have sg2: "(y < ?zer_list ! 0) \ ?t" proof - assume ylt: "y < ?zer_list ! 0" have ynonzat_some_qs: "\q \ (set qs). q \ 0 \ poly q y \ 0" proof clarsimp fix q assume q_in: "q \ set qs" assume qnonz: "q \ 0" assume "poly q y = 0" then have "y \ {x. \q\set qs. q \ 0 \ poly q x = 0}" using q_in qnonz by auto then have "List.member ?zer_list y" by (smt (verit, best) finset in_set_member mem_Collect_eq set_sorted_list_of_set) then have "y \ ?zer_list ! 0" using strict_sorted_h using \\ (\q\set qs. q \ 0 \ poly q y = 0)\ \poly q y = 0\ q_in qnonz by blast then show "False" using ylt by auto qed let ?ncrb = "(- crb (prod_list_var qs))" have "\x \ {x. \q\set qs. q \ 0 \ poly q x = 0}. poly (prod_list_var qs) x = 0" using q_dvd_prod_list_var_prop by fastforce then have "poly (prod_list_var qs) (sorted_list_of_set {x. \q\set qs. q \ 0 \ poly q x = 0} ! 0) = 0" using finset set_sorted_list_of_set by (metis (no_types, lifting) lengt nth_mem) then have ncrblt: "?ncrb < ?zer_list ! 0" using prod_list_var_nonzero crb_lem_neg[of "prod_list_var qs" "?zer_list ! 0"] by auto have qzerh: "\q \ (set qs). q = 0 \ squash (poly q ?ncrb) = squash (poly q y)" by auto have "\q \ (set qs). q \ 0 \ squash (poly q ?ncrb) = squash (poly q y)" proof clarsimp fix q assume q_in: "q \ set qs" assume qnonz: "q \ 0" have nonzylt:"\(\x \ y. poly q x = 0)" proof clarsimp fix x assume xlt: "x \ y" assume "poly q x = 0" then have "x \ {x. \q\set qs. q \ 0 \ poly q x = 0}" using q_in qnonz by auto then have "List.member ?zer_list x" by (smt (verit, best) finset in_set_member mem_Collect_eq set_sorted_list_of_set) then have "x \ ?zer_list ! 0" using strict_sorted_h by (metis (no_types, lifting) gr_implies_not0 in_set_conv_nth in_set_member not_less sorted_iff_nth_mono sorted_list_of_set(2)) then show "False" using xlt ylt by auto qed have nonzncrb:"\(\x \ (real_of_int ?ncrb). poly q x = 0)" proof clarsimp fix x assume xlt: "x \ - real_of_int (crb (prod_list_var qs))" assume "poly q x = 0" then have "x \ {x. \q\set qs. q \ 0 \ poly q x = 0}" using q_in qnonz by auto then have "List.member ?zer_list x" by (smt (verit, best) finset in_set_member mem_Collect_eq set_sorted_list_of_set) then have "x \ ?zer_list ! 0" using strict_sorted_h by (metis (no_types, lifting) gr_implies_not0 in_set_conv_nth in_set_member not_less sorted_iff_nth_mono sorted_list_of_set(2)) then show "False" using xlt ncrblt by auto qed have c1: " (poly q ?ncrb) > 0 \ (poly q y) > 0" proof - assume qncrbgt: "(poly q ?ncrb) > 0" then have eq: "?ncrb = y \ poly q y > 0 " by auto have gt: " ?ncrb > y \ poly q y > 0" using qncrbgt qnonz poly_IVT_pos[of y ?ncrb q] poly_IVT_neg[of ?ncrb y q] nonzncrb nonzylt apply (auto) by (meson less_eq_real_def linorder_neqE_linordered_idom) have lt: "?ncrb < y \ poly q y > 0" using qncrbgt using qnonz poly_IVT_pos[of y ?ncrb q] poly_IVT_neg[of ?ncrb y q] nonzncrb nonzylt apply (auto) by (meson less_eq_real_def linorder_neqE_linordered_idom) then show ?thesis using eq gt lt apply (auto) by (meson linorder_neqE_linordered_idom) qed have c2: "(poly q ?ncrb) < 0 \ (poly q y) < 0" using poly_IVT_pos[of ?ncrb y q] poly_IVT_neg[of y ?ncrb q] nonzncrb nonzylt apply (auto) by (metis less_eq_real_def linorder_neqE_linordered_idom) have eo: "(poly q ?ncrb) > 0 \ (poly q ?ncrb) < 0" using nonzncrb by auto then show "squash (poly q (- real_of_int (crb (prod_list_var qs)))) = squash (poly q y)" using c1 c2 by (smt (verit, ccfv_SIG) of_int_minus squash_def) qed then have "\q \ (set qs). squash (poly q ?ncrb) = squash (poly q y)" using qzerh by auto then have "consistent_sign_vec qs ?ncrb = consistent_sign_vec qs y" unfolding consistent_sign_vec_def squash_def by (smt (z3) map_eq_conv) then show ?thesis using neg_crb_in by auto qed have sg3: " (y > ?zer_list ! (length ?zer_list - 1)) \ ?t" proof - assume ygt: "y > ?zer_list ! (length ?zer_list - 1)" have ynonzat_some_qs: "\q \ (set qs). q \ 0 \ poly q y \ 0" proof clarsimp fix q assume q_in: "q \ set qs" assume qnonz: "q \ 0" assume "poly q y = 0" then have "y \ {x. \q\set qs. q \ 0 \ poly q x = 0}" using q_in qnonz by auto then have "List.member ?zer_list y" by (smt (verit, best) finset in_set_member mem_Collect_eq set_sorted_list_of_set) then have "y \ ?zer_list ! (length ?zer_list - 1)" using strict_sorted_h using \\ (\q\set qs. q \ 0 \ poly q y = 0)\ \poly q y = 0\ q_in qnonz by blast then show "False" using ygt by auto qed let ?crb = "crb (prod_list_var qs)" have "\x \ {x. \q\set qs. q \ 0 \ poly q x = 0}. poly (prod_list_var qs) x = 0" using q_dvd_prod_list_var_prop by fastforce then have "poly (prod_list_var qs) (sorted_list_of_set {x. \q\set qs. q \ 0 \ poly q x = 0} ! 0) = 0" using finset set_sorted_list_of_set by (metis (no_types, lifting) lengt nth_mem) then have crbgt: "?crb > ?zer_list ! (length ?zer_list - 1)" using prod_list_var_nonzero crb_lem_pos[of "prod_list_var qs" "?zer_list ! (length ?zer_list - 1)"] by (metis (no_types, lifting) \\x\{x. \q\set qs. q \ 0 \ poly q x = 0}. poly (prod_list_var qs) x = 0\ diff_less finset lengt less_numeral_extra(1) nth_mem set_sorted_list_of_set) have qzerh: "\q \ (set qs). q = 0 \ squash (poly q ?crb) = squash (poly q y)" by auto have "\q \ (set qs). q \ 0 \ squash (poly q ?crb) = squash (poly q y)" proof clarsimp fix q assume q_in: "q \ set qs" assume qnonz: "q \ 0" have nonzylt:"\(\x \ y. poly q x = 0)" proof clarsimp fix x assume xgt: "x \ y" assume "poly q x = 0" then have "x \ {x. \q\set qs. q \ 0 \ poly q x = 0}" using q_in qnonz by auto then have "List.member ?zer_list x" by (smt (verit, best) finset in_set_member mem_Collect_eq set_sorted_list_of_set) then have "x \ ?zer_list ! (length ?zer_list - 1)" using strict_sorted_h by (metis (no_types, lifting) One_nat_def Suc_leI Suc_pred diff_Suc_less in_set_conv_nth in_set_member lengt not_less sorted_iff_nth_mono sorted_list_of_set(2)) then show "False" using xgt ygt by auto qed have nonzcrb:"\(\x \ (real_of_int ?crb). poly q x = 0)" proof clarsimp fix x assume xgt: "x \ real_of_int (crb (prod_list_var qs))" assume "poly q x = 0" then have "x \ {x. \q\set qs. q \ 0 \ poly q x = 0}" using q_in qnonz by auto then have "List.member ?zer_list x" by (smt (verit, best) finset in_set_member mem_Collect_eq set_sorted_list_of_set) then have "x \ ?zer_list ! (length ?zer_list - 1)" using strict_sorted_h by (meson \\x\{x. \q\set qs. q \ 0 \ poly q x = 0}. poly (prod_list_var qs) x = 0\ \x \ {x. \q\set qs. q \ 0 \ poly q x = 0}\ crb_lem_pos not_less prod_list_var_nonzero xgt) then show "False" using xgt crbgt by auto qed have c1: " (poly q ?crb) > 0 \ (poly q y) > 0" proof - assume qcrbgt: "(poly q ?crb) > 0" then have eq: "?crb = y \ poly q y > 0 " by auto have gt: " ?crb > y \ poly q y > 0" using qcrbgt qnonz poly_IVT_pos[of y ?crb q] poly_IVT_neg[of ?crb y q] nonzcrb nonzylt apply (auto) by (meson less_eq_real_def linorder_neqE_linordered_idom) have lt: "?crb < y \ poly q y > 0" using qcrbgt using qnonz poly_IVT_pos[of y ?crb q] poly_IVT_neg[of ?crb y q] nonzcrb nonzylt apply (auto) by (meson less_eq_real_def linorder_neqE_linordered_idom) then show ?thesis using eq gt lt apply (auto) by (meson linorder_neqE_linordered_idom) qed have c2: "(poly q ?crb) < 0 \ (poly q y) < 0" using poly_IVT_pos[of ?crb y q] poly_IVT_neg[of y ?crb q] nonzcrb nonzylt apply (auto) by (metis less_eq_real_def linorder_neqE_linordered_idom) have eo: "(poly q ?crb) > 0 \ (poly q ?crb) < 0" using nonzcrb by auto then show "squash (poly q (real_of_int (crb (prod_list_var qs)))) = squash (poly q y)" using c1 c2 by (smt (verit, ccfv_SIG) of_int_minus squash_def) qed then have "\q \ (set qs). squash (poly q ?crb) = squash (poly q y)" using qzerh by auto then have "consistent_sign_vec qs ?crb = consistent_sign_vec qs y" unfolding consistent_sign_vec_def squash_def by (smt (z3) map_eq_conv) then show ?thesis using pos_crb_in by auto qed have sg4: " (\k < (length ?zer_list - 1). y > ?zer_list ! k \ y < ?zer_list ! (k+1)) \ ?t" proof - assume " (\k < (length ?zer_list - 1). y > ?zer_list ! k \ y < ?zer_list ! (k+1))" then obtain k where k_prop: "k < (length ?zer_list - 1) \ y > ?zer_list ! k \ y < ?zer_list ! (k+1)" by auto have ltk: "(?zer_list ! k) < (?zer_list ! (k+1)) " using strict_sorted_h using k_prop by linarith have q1e: "(\q1\set qs. q1 \ 0 \ poly q1 (?zer_list ! k) = 0)" by (smt (z3) One_nat_def Suc_lessD add.right_neutral add_Suc_right finset k_prop less_diff_conv mem_Collect_eq nth_mem set_sorted_list_of_set) have q2e: "(\q2\set qs. q2 \ 0 \ poly q2 (?zer_list ! (k + 1)) = 0)" by (smt (verit, del_insts) finset k_prop less_diff_conv mem_Collect_eq nth_mem set_sorted_list_of_set) then have "(\q>(?zer_list ! k). q < (?zer_list ! (k + 1)) \ poly (poly_f qs) q = 0)" using poly_f_roots_prop_1[of qs] q1e q2e ltk is_not_const by auto then have "\s \ set S. s > ?zer_list ! k \ s < ?zer_list ! (k+1)" using poly_f_is by (smt (z3) k_prop mem_Collect_eq set_S_char) then obtain s where s_prop: "s \ set S \ s > ?zer_list ! k \ s < ?zer_list ! (k+1)" by auto have qnon: "\q \ set qs. q\ 0 \ squash (poly q s) = squash (poly q y)" proof clarsimp fix q assume q_in: "q \ set qs" assume qnonz: "q \ 0" have sgt: "s > y \ squash (poly q s) = squash (poly q y)" proof - assume "s > y" then have "\x. List.member ?zer_list x \ y \ x \ x \ s" using sorted_list_lemma[of y s k ?zer_list] k_prop strict_sorted_h s_prop y_prop using less_diff_conv by blast then have nox: "\x. poly q x = 0 \ y \ x \ x \ s" using q_in qnonz by (metis (mono_tags, lifting) finset in_set_member mem_Collect_eq set_sorted_list_of_set) then have c1: "poly q s \ 0" using s_prop q_in qnonz by (metis (mono_tags, lifting) \y < s\ less_eq_real_def ) have c2: "poly q s > 0 \ poly q y > 0" using poly_IVT_pos poly_IVT_neg nox by (meson \y < s\ less_eq_real_def linorder_neqE_linordered_idom) have c3: "poly q s < 0 \ poly q y < 0" using poly_IVT_pos poly_IVT_neg nox by (meson \y < s\ less_eq_real_def linorder_neqE_linordered_idom) show ?thesis using c1 c2 c3 unfolding squash_def by auto qed have slt: "s < y \ squash (poly q s) = squash (poly q y)" proof - assume slt: "s < y" then have "\x. List.member ?zer_list x \ s \ x \ x \ y" using sorted_list_lemma[of s y k ?zer_list] k_prop strict_sorted_h s_prop y_prop using less_diff_conv by blast then have nox: "\x. poly q x = 0 \ s \ x \ x \ y" using q_in qnonz by (metis (mono_tags, lifting) finset in_set_member mem_Collect_eq set_sorted_list_of_set) then have c1: "poly q s \ 0" using s_prop q_in qnonz by (metis (mono_tags, lifting) \s < y\ less_eq_real_def ) have c2: "poly q s > 0 \ poly q y > 0" using poly_IVT_pos poly_IVT_neg nox by (meson \s < y\ less_eq_real_def linorder_neqE_linordered_idom) have c3: "poly q s < 0 \ poly q y < 0" using poly_IVT_pos poly_IVT_neg nox by (meson \s < y\ less_eq_real_def linorder_neqE_linordered_idom) show ?thesis using c1 c2 c3 unfolding squash_def by auto qed have "s = y \ squash (poly q s) = squash (poly q y)" by auto then show "squash (poly q s) = squash (poly q y)" using sgt slt by (meson linorder_neqE_linordered_idom) qed have "\q \ set qs. q= 0 \ squash (poly q s) = squash (poly q y)" by auto then have "\q \ set qs. squash (poly q s) = squash (poly q y)" using qnon by fastforce then show ?thesis using s_prop unfolding squash_def consistent_sign_vec_def apply (auto) by (metis (no_types, hide_lams) class_field.neg_1_not_0 equal_neg_zero less_irrefl linorder_neqE_linordered_idom) qed show ?thesis using lengt sg1 sg2 sg3 sg4 len_gtz_prop is_not_const by fastforce qed show "\ k \ (set S). consistent_sign_vec qs k = consistent_sign_vec qs y" using c_c1 c_c2 by auto qed show ?thesis using c1 c2 by auto qed then show "x \ consistent_sign_vectors_R qs (set S)" using y_prop unfolding consistent_sign_vectors_R_def by (metis imageI) qed have easy_direction: "consistent_sign_vectors_R qs (set S) \ consistent_sign_vectors_R qs UNIV " using consistent_sign_vectors_R_def by auto then show ?thesis using difficult_direction easy_direction by auto qed lemma main_step_aux2_R: fixes qs:: "real poly list" assumes is_not_const: "check_all_const_deg qs = False" shows "set (find_consistent_signs_R qs) = consistent_sign_vectors_R qs UNIV" proof - have poly_f_is: "poly_f qs = (pderiv (prod_list_var qs)) * (prod_list_var qs)* ([:-(crb (prod_list_var qs)),1:]) * ([:(crb (prod_list_var qs)),1:])" using is_not_const unfolding poly_f_def by auto let ?p = "(pderiv (prod_list_var qs)) * (prod_list_var qs)* ([:-(crb (prod_list_var qs)),1:]) * ([:(crb (prod_list_var qs)),1:])" let ?S = "characterize_root_list_p (pderiv (prod_list_var qs) * (prod_list_var qs) * ([:-(crb (prod_list_var qs)),1:]) * ([:(crb (prod_list_var qs)),1:]))" have "set (remdups (map (signs_at qs) ?S)) = consistent_sign_vectors_R qs (set ?S)" unfolding signs_at_def squash_def consistent_sign_vectors_R_def consistent_sign_vec_def by (smt (verit, best) comp_apply map_eq_conv set_map set_remdups) then have "set (characterize_consistent_signs_at_roots ?p qs) = consistent_sign_vectors_R qs UNIV" unfolding characterize_consistent_signs_at_roots_def using assms all_sample_points_prop[of qs] by auto then show ?thesis unfolding find_consistent_signs_R_def using find_consistent_signs_at_roots_R poly_f_is poly_f_nonzero[of qs] by auto qed lemma main_step_R: fixes qs:: "real poly list" shows "set (find_consistent_signs_R qs) = consistent_sign_vectors_R qs UNIV" using main_step_aux1_R main_step_aux2_R by auto (* The universal and existential decision procedure for real polys are easy if we know the consistent sign vectors *) lemma consistent_sign_vec_semantics_R: assumes "\i. i \ set_fml fml \ i < length ls" shows "lookup_sem fml (map (\p. poly p x) ls) = lookup_sem fml (consistent_sign_vec ls x)" using assms apply (induction) by (auto simp add: consistent_sign_vec_def) lemma universal_lookup_sem_R: assumes "\i. i \ set_fml fml \ i < length qs" assumes "set signs = consistent_sign_vectors_R qs UNIV" shows "(\x::real. lookup_sem fml (map (\p. poly p x) qs)) \ list_all (lookup_sem fml) signs" using assms(2) unfolding consistent_sign_vectors_R_def list_all_iff by (simp add: assms(1) consistent_sign_vec_semantics_R) lemma existential_lookup_sem_R: assumes "\i. i \ set_fml fml \ i < length qs" assumes "set signs = consistent_sign_vectors_R qs UNIV" shows "(\x::real. lookup_sem fml (map (\p. poly p x) qs)) \ find (lookup_sem fml) signs \ None" using assms(2) unfolding consistent_sign_vectors_R_def find_None_iff by (simp add: assms(1) consistent_sign_vec_semantics_R) lemma decide_univ_lem_helper_R: fixes fml:: "real poly fml" assumes "(fml_struct,polys) = convert fml" shows "(\x::real. lookup_sem fml_struct (map (\p. poly p x) polys)) \ (decide_universal_R fml)" using assms universal_lookup_sem_R main_step_R unfolding decide_universal_R_def apply (auto) apply (metis assms convert_closed fst_conv snd_conv) by (metis (full_types) assms convert_closed fst_conv snd_conv) lemma decide_exis_lem_helper_R: fixes fml:: "real poly fml" assumes "(fml_struct,polys) = convert fml" shows "(\x::real. lookup_sem fml_struct (map (\p. poly p x) polys)) \ (decide_existential_R fml)" using assms existential_lookup_sem_R main_step_R unfolding decide_existential_R_def apply (auto) apply (metis assms convert_closed fst_conv snd_conv) by (metis (full_types) assms convert_closed fst_conv snd_conv) lemma convert_semantics_lem_R: assumes "\p. p \ set (poly_list fml) \ ls ! (index_of ps p) = poly p x" shows "real_sem fml x = lookup_sem (map_fml (index_of ps) fml) ls" using assms apply (induct fml) by auto lemma convert_semantics_R: shows "real_sem fml x = lookup_sem (fst (convert fml)) (map (\p. poly p x) (snd (convert fml)))" unfolding convert_def Let_def apply simp apply (intro convert_semantics_lem_R) by (simp add: index_of_lookup(1) index_of_lookup(2)) (* Main result *) theorem decision_procedure_R: shows "(\x::real. real_sem fml x) \ (decide_universal_R fml)" "\x::real. real_sem fml x \ (decide_existential_R fml)" using convert_semantics_lem_R decide_univ_lem_helper_R apply (auto) apply (simp add: convert_semantics_R) apply (metis convert_def convert_semantics_R fst_conv snd_conv) using convert_semantics_lem_R by (metis convert_def convert_semantics_R decide_exis_lem_helper_R fst_conv snd_conv) end