--- a/CONTRIBUTORS Tue Apr 30 21:04:08 2019 +0100
+++ b/CONTRIBUTORS Tue Apr 30 21:04:21 2019 +0100
@@ -10,7 +10,7 @@
Homology and supporting lemmas on topology and group theory
* April 2019: Paulo de Vilhena and Martin Baillon
- Group theory developments towards proving algebraic closure
+ Group theory developments, esp. algebraic closure of a field
* February/March 2019: Makarius Wenzel
Stateless management of export artifacts in the Isabelle/HOL code generator.
--- a/NEWS Tue Apr 30 21:04:08 2019 +0100
+++ b/NEWS Tue Apr 30 21:04:21 2019 +0100
@@ -266,7 +266,7 @@
at the level of abstract topological spaces.
* Session HOL-Algebra: Free abelian groups, etc., ported from HOL Light;
-proofs towards algebraic closure by de Vilhena and Baillon.
+ algebraic closure of a field by de Vilhena and Baillon.
* Session HOL-Homology has been added. It is a port of HOL Light's
homology library, with new proofs of "invariance of domain" and related
--- a/src/HOL/Algebra/Algebraic_Closure.thy Tue Apr 30 21:04:08 2019 +0100
+++ b/src/HOL/Algebra/Algebraic_Closure.thy Tue Apr 30 21:04:21 2019 +0100
@@ -5,7 +5,7 @@
*)
theory Algebraic_Closure
- imports Indexed_Polynomials Polynomial_Divisibility Pred_Zorn Finite_Extensions
+ imports Indexed_Polynomials Polynomial_Divisibility Finite_Extensions
begin
@@ -21,28 +21,24 @@
\<lparr> mult := (\<lambda>a \<in> carrier R. \<lambda>b \<in> carrier R. a \<otimes>\<^bsub>R\<^esub> b),
add := (\<lambda>a \<in> carrier R. \<lambda>b \<in> carrier R. a \<oplus>\<^bsub>R\<^esub> b) \<rparr>"
-definition (in ring) \<sigma> :: "'a list \<Rightarrow> (('a list multiset) \<Rightarrow> 'a) list"
+definition (in ring) \<sigma> :: "'a list \<Rightarrow> ((('a list \<times> nat) multiset) \<Rightarrow> 'a) list"
where "\<sigma> P = map indexed_const P"
-definition (in ring) extensions :: "(('a list multiset) \<Rightarrow> 'a) ring set"
+definition (in ring) extensions :: "((('a list \<times> nat) multiset) \<Rightarrow> 'a) ring set"
where "extensions \<equiv> { L \<comment> \<open>such that\<close>.
\<comment> \<open>i\<close> (field L) \<and>
\<comment> \<open>ii\<close> (indexed_const \<in> ring_hom R L) \<and>
\<comment> \<open>iii\<close> (\<forall>\<P> \<in> carrier L. carrier_coeff \<P>) \<and>
- \<comment> \<open>iv\<close> (\<forall>\<P> \<in> carrier L. \<forall>P \<in> carrier (poly_ring R).
- \<not> index_free \<P> P \<longrightarrow> \<X>\<^bsub>P\<^esub> \<in> carrier L \<and> (ring.eval L) (\<sigma> P) \<X>\<^bsub>P\<^esub> = \<zero>\<^bsub>L\<^esub>) }"
+ \<comment> \<open>iv\<close> (\<forall>\<P> \<in> carrier L. \<forall>P \<in> carrier (poly_ring R). \<forall>i.
+ \<not> index_free \<P> (P, i) \<longrightarrow>
+ \<X>\<^bsub>(P, i)\<^esub> \<in> carrier L \<and> (ring.eval L) (\<sigma> P) \<X>\<^bsub>(P, i)\<^esub> = \<zero>\<^bsub>L\<^esub>) }"
-abbreviation (in ring) restrict_extensions :: "(('a list multiset) \<Rightarrow> 'a) ring set" ("\<S>")
+abbreviation (in ring) restrict_extensions :: "((('a list \<times> nat) multiset) \<Rightarrow> 'a) ring set" ("\<S>")
where "\<S> \<equiv> law_restrict ` extensions"
subsection \<open>Basic Properties\<close>
-(* ========== *)
-lemma (in field) is_ring: "ring R"
- using ring_axioms .
-(* ========== *)
-
lemma law_restrict_carrier: "carrier (law_restrict R) = carrier R"
by (simp add: law_restrict_def ring.defs)
@@ -135,15 +131,15 @@
lemma (in ring) iso_incl_antisym:
assumes "A \<in> \<S>" "B \<in> \<S>" and "A \<lesssim> B" "B \<lesssim> A" shows "A = B"
proof -
- obtain A' B' :: "('a list multiset \<Rightarrow> 'a) ring"
+ obtain A' B' :: "(('a list \<times> nat) multiset \<Rightarrow> 'a) ring"
where A: "A = law_restrict A'" "ring A'" and B: "B = law_restrict B'" "ring B'"
using assms(1-2) field.is_ring by (auto simp add: extensions_def)
thus ?thesis
using law_restrict_iso_imp_eq iso_incl_antisym_aux[OF assms(3-4)] by simp
qed
-lemma (in ring) iso_incl_partial_order: "partial_order_on \<S> (rel_of (\<lesssim>) \<S>)"
- using iso_incl_refl iso_incl_trans iso_incl_antisym by (rule partial_order_on_rel_ofI)
+lemma (in ring) iso_incl_partial_order: "partial_order_on \<S> (relation_of (\<lesssim>) \<S>)"
+ using iso_incl_refl iso_incl_trans iso_incl_antisym by (rule partial_order_on_relation_ofI)
lemma iso_inclE:
assumes "ring A" and "ring B" and "A \<lesssim> B" shows "ring_hom_ring A B id"
@@ -174,14 +170,14 @@
show "indexed_const \<in> ring_hom R (image_ring indexed_const R)"
using inj_imp_image_ring_iso[OF indexed_const_inj_on] unfolding ring_iso_def by auto
next
- fix \<P> :: "('a list multiset) \<Rightarrow> 'a" and P
+ fix \<P> :: "(('a list \<times> nat) multiset) \<Rightarrow> 'a" and P and i
assume "\<P> \<in> carrier (image_ring indexed_const R)"
then obtain k where "k \<in> carrier R" and "\<P> = indexed_const k"
unfolding image_ring_carrier by blast
- hence "index_free \<P> P" for P
+ hence "index_free \<P> (P, i)" for P i
unfolding index_free_def indexed_const_def by auto
- thus "\<not> index_free \<P> P \<Longrightarrow> \<X>\<^bsub>P\<^esub> \<in> carrier (image_ring indexed_const R)"
- and "\<not> index_free \<P> P \<Longrightarrow> ring.eval (image_ring indexed_const R) (\<sigma> P) \<X>\<^bsub>P\<^esub> = \<zero>\<^bsub>image_ring indexed_const R\<^esub>"
+ thus "\<not> index_free \<P> (P, i) \<Longrightarrow> \<X>\<^bsub>(P, i)\<^esub> \<in> carrier (image_ring indexed_const R)"
+ and "\<not> index_free \<P> (P, i) \<Longrightarrow> ring.eval (image_ring indexed_const R) (\<sigma> P) \<X>\<^bsub>(P, i)\<^esub> = \<zero>\<^bsub>image_ring indexed_const R\<^esub>"
by auto
from \<open>k \<in> carrier R\<close> and \<open>\<P> = indexed_const k\<close> show "carrier_coeff \<P>"
unfolding indexed_const_def carrier_coeff_def by auto
@@ -371,77 +367,77 @@
subsection \<open>Zorn\<close>
lemma (in ring) exists_core_chain:
- assumes "C \<in> Chains (rel_of (\<lesssim>) \<S>)" obtains C' where "C' \<subseteq> extensions" and "C = law_restrict ` C'"
- using Chains_rel_of[OF assms] by (meson subset_image_iff)
+ assumes "C \<in> Chains (relation_of (\<lesssim>) \<S>)" obtains C' where "C' \<subseteq> extensions" and "C = law_restrict ` C'"
+ using Chains_relation_of[OF assms] by (meson subset_image_iff)
lemma (in ring) core_chain_is_chain:
- assumes "law_restrict ` C \<in> Chains (rel_of (\<lesssim>) \<S>)" shows "\<And>R S. \<lbrakk> R \<in> C; S \<in> C \<rbrakk> \<Longrightarrow> R \<lesssim> S \<or> S \<lesssim> R"
+ assumes "law_restrict ` C \<in> Chains (relation_of (\<lesssim>) \<S>)" shows "\<And>R S. \<lbrakk> R \<in> C; S \<in> C \<rbrakk> \<Longrightarrow> R \<lesssim> S \<or> S \<lesssim> R"
proof -
fix R S assume "R \<in> C" and "S \<in> C" thus "R \<lesssim> S \<or> S \<lesssim> R"
- using assms(1) unfolding iso_incl_hom[of R] iso_incl_hom[of S] Chains_def by auto
+ using assms(1) unfolding iso_incl_hom[of R] iso_incl_hom[of S] Chains_def relation_of_def
+ by auto
qed
lemma (in field) exists_maximal_extension:
shows "\<exists>M \<in> \<S>. \<forall>L \<in> \<S>. M \<lesssim> L \<longrightarrow> L = M"
proof (rule predicate_Zorn[OF iso_incl_partial_order])
- show "\<forall>C \<in> Chains (rel_of (\<lesssim>) \<S>). \<exists>L \<in> \<S>. \<forall>R \<in> C. R \<lesssim> L"
- proof
- fix C assume C: "C \<in> Chains (rel_of (\<lesssim>) \<S>)"
- show "\<exists>L \<in> \<S>. \<forall>R \<in> C. R \<lesssim> L"
- proof (cases)
- assume "C = {}" thus ?thesis
- using extensions_non_empty by auto
- next
- assume "C \<noteq> {}"
- from \<open>C \<in> Chains (rel_of (\<lesssim>) \<S>)\<close>
- obtain C' where C': "C' \<subseteq> extensions" "C = law_restrict ` C'"
- using exists_core_chain by auto
- with \<open>C \<noteq> {}\<close> obtain S where S: "S \<in> C'" and "C' \<noteq> {}"
- by auto
+ fix C assume C: "C \<in> Chains (relation_of (\<lesssim>) \<S>)"
+ show "\<exists>L \<in> \<S>. \<forall>R \<in> C. R \<lesssim> L"
+ proof (cases)
+ assume "C = {}" thus ?thesis
+ using extensions_non_empty by auto
+ next
+ assume "C \<noteq> {}"
+ from \<open>C \<in> Chains (relation_of (\<lesssim>) \<S>)\<close>
+ obtain C' where C': "C' \<subseteq> extensions" "C = law_restrict ` C'"
+ using exists_core_chain by auto
+ with \<open>C \<noteq> {}\<close> obtain S where S: "S \<in> C'" and "C' \<noteq> {}"
+ by auto
- have core_chain: "\<And>R. R \<in> C' \<Longrightarrow> field R" "\<And>R S. \<lbrakk> R \<in> C'; S \<in> C' \<rbrakk> \<Longrightarrow> R \<lesssim> S \<or> S \<lesssim> R"
- using core_chain_is_chain[of C'] C' C unfolding extensions_def by auto
- from \<open>C' \<noteq> {}\<close> interpret Union: field "union_ring C'"
- using union_ring_is_field[OF core_chain] C'(1) by blast
+ have core_chain: "\<And>R. R \<in> C' \<Longrightarrow> field R" "\<And>R S. \<lbrakk> R \<in> C'; S \<in> C' \<rbrakk> \<Longrightarrow> R \<lesssim> S \<or> S \<lesssim> R"
+ using core_chain_is_chain[of C'] C' C unfolding extensions_def by auto
+ from \<open>C' \<noteq> {}\<close> interpret Union: field "union_ring C'"
+ using union_ring_is_field[OF core_chain] C'(1) by blast
- have "union_ring C' \<in> extensions"
- proof (auto simp add: extensions_def)
- show "field (union_ring C')"
- using Union.field_axioms .
- next
- from \<open>S \<in> C'\<close> have "indexed_const \<in> ring_hom R S"
- using C'(1) unfolding extensions_def by auto
- thus "indexed_const \<in> ring_hom R (union_ring C')"
- using ring_hom_trans[of _ R S id] union_ring_is_upper_bound[OF core_chain S]
- unfolding iso_incl.simps by auto
- next
- show "a \<in> carrier (union_ring C') \<Longrightarrow> carrier_coeff a" for a
- using C'(1) unfolding union_ring_carrier extensions_def by auto
- next
- fix \<P> P
- assume "\<P> \<in> carrier (union_ring C')" and P: "P \<in> carrier (poly_ring R)" "\<not> index_free \<P> P"
- from \<open>\<P> \<in> carrier (union_ring C')\<close> obtain T where T: "T \<in> C'" "\<P> \<in> carrier T"
- using exists_superset_carrier[of C' "{ \<P> }"] core_chain by auto
- hence "\<X>\<^bsub>P\<^esub> \<in> carrier T" and "(ring.eval T) (\<sigma> P) \<X>\<^bsub>P\<^esub> = \<zero>\<^bsub>T\<^esub>"
- and field: "field T" and hom: "indexed_const \<in> ring_hom R T"
- using P C'(1) unfolding extensions_def by auto
- with \<open>T \<in> C'\<close> show "\<X>\<^bsub>P\<^esub> \<in> carrier (union_ring C')"
- unfolding union_ring_carrier by auto
- have "set P \<subseteq> carrier R"
- using P(1) unfolding sym[OF univ_poly_carrier] polynomial_def by auto
- hence "set (\<sigma> P) \<subseteq> carrier T"
- using ring_hom_memE(1)[OF hom] unfolding \<sigma>_def by (induct P) (auto)
- with \<open>\<X>\<^bsub>P\<^esub> \<in> carrier T\<close> and \<open>(ring.eval T) (\<sigma> P) \<X>\<^bsub>P\<^esub> = \<zero>\<^bsub>T\<^esub>\<close>
- show "(ring.eval (union_ring C')) (\<sigma> P) \<X>\<^bsub>P\<^esub> = \<zero>\<^bsub>union_ring C'\<^esub>"
- using iso_incl_imp_same_eval[OF field.is_ring[OF field] Union.is_ring
- union_ring_is_upper_bound[OF core_chain T(1)]] same_one_same_zero(2)[OF core_chain T(1)]
- by auto
- qed
- moreover have "R \<lesssim> law_restrict (union_ring C')" if "R \<in> C" for R
- using that union_ring_is_upper_bound[OF core_chain] iso_incl_hom unfolding C' by auto
- ultimately show ?thesis
- by blast
+ have "union_ring C' \<in> extensions"
+ proof (auto simp add: extensions_def)
+ show "field (union_ring C')"
+ using Union.field_axioms .
+ next
+ from \<open>S \<in> C'\<close> have "indexed_const \<in> ring_hom R S"
+ using C'(1) unfolding extensions_def by auto
+ thus "indexed_const \<in> ring_hom R (union_ring C')"
+ using ring_hom_trans[of _ R S id] union_ring_is_upper_bound[OF core_chain S]
+ unfolding iso_incl.simps by auto
+ next
+ show "a \<in> carrier (union_ring C') \<Longrightarrow> carrier_coeff a" for a
+ using C'(1) unfolding union_ring_carrier extensions_def by auto
+ next
+ fix \<P> P i
+ assume "\<P> \<in> carrier (union_ring C')"
+ and P: "P \<in> carrier (poly_ring R)"
+ and not_index_free: "\<not> index_free \<P> (P, i)"
+ from \<open>\<P> \<in> carrier (union_ring C')\<close> obtain T where T: "T \<in> C'" "\<P> \<in> carrier T"
+ using exists_superset_carrier[of C' "{ \<P> }"] core_chain by auto
+ hence "\<X>\<^bsub>(P, i)\<^esub> \<in> carrier T" and "(ring.eval T) (\<sigma> P) \<X>\<^bsub>(P, i)\<^esub> = \<zero>\<^bsub>T\<^esub>"
+ and field: "field T" and hom: "indexed_const \<in> ring_hom R T"
+ using P not_index_free C'(1) unfolding extensions_def by auto
+ with \<open>T \<in> C'\<close> show "\<X>\<^bsub>(P, i)\<^esub> \<in> carrier (union_ring C')"
+ unfolding union_ring_carrier by auto
+ have "set P \<subseteq> carrier R"
+ using P unfolding sym[OF univ_poly_carrier] polynomial_def by auto
+ hence "set (\<sigma> P) \<subseteq> carrier T"
+ using ring_hom_memE(1)[OF hom] unfolding \<sigma>_def by (induct P) (auto)
+ with \<open>\<X>\<^bsub>(P, i)\<^esub> \<in> carrier T\<close> and \<open>(ring.eval T) (\<sigma> P) \<X>\<^bsub>(P, i)\<^esub> = \<zero>\<^bsub>T\<^esub>\<close>
+ show "(ring.eval (union_ring C')) (\<sigma> P) \<X>\<^bsub>(P, i)\<^esub> = \<zero>\<^bsub>union_ring C'\<^esub>"
+ using iso_incl_imp_same_eval[OF field.is_ring[OF field] Union.is_ring
+ union_ring_is_upper_bound[OF core_chain T(1)]] same_one_same_zero(2)[OF core_chain T(1)]
+ by auto
qed
+ moreover have "R \<lesssim> law_restrict (union_ring C')" if "R \<in> C" for R
+ using that union_ring_is_upper_bound[OF core_chain] iso_incl_hom unfolding C' by auto
+ ultimately show ?thesis
+ by blast
qed
qed
@@ -485,44 +481,57 @@
using S.univ_poly_consistent[OF subfieldE(1)[OF img_is_subfield(2)[OF assms]]] by simp
qed
+
lemma (in field) exists_root:
assumes "M \<in> extensions" and "\<And>L. \<lbrakk> L \<in> extensions; M \<lesssim> L \<rbrakk> \<Longrightarrow> law_restrict L = law_restrict M"
- and "P \<in> carrier (poly_ring R)" and "degree P > 0"
- shows "\<exists>x \<in> carrier M. (ring.eval M) (\<sigma> P) x = \<zero>\<^bsub>M\<^esub>"
+ and "P \<in> carrier (poly_ring R)"
+ shows "(ring.splitted M) (\<sigma> P)"
proof (rule ccontr)
from \<open>M \<in> extensions\<close> interpret M: field M + Hom: ring_hom_ring R M "indexed_const"
using ring_hom_ringI2[OF ring_axioms field.is_ring] unfolding extensions_def by auto
interpret UP: principal_domain "poly_ring M"
using M.univ_poly_is_principal[OF M.carrier_is_subfield] .
- assume no_roots: "\<not> (\<exists>x \<in> carrier M. M.eval (\<sigma> P) x = \<zero>\<^bsub>M\<^esub>)"
+ assume not_splitted: "\<not> (ring.splitted M) (\<sigma> P)"
have "(\<sigma> P) \<in> carrier (poly_ring M)"
using polynomial_hom[OF Hom.homh field_axioms M.field_axioms assms(3)] unfolding \<sigma>_def by simp
- moreover have "(\<sigma> P) \<notin> Units (poly_ring M)" and "(\<sigma> P) \<noteq> \<zero>\<^bsub>poly_ring M\<^esub>"
- using assms(4) unfolding M.univ_poly_carrier_units \<sigma>_def univ_poly_zero by auto
- ultimately obtain Q
+ then obtain Q
where Q: "Q \<in> carrier (poly_ring M)" "pirreducible\<^bsub>M\<^esub> (carrier M) Q" "Q pdivides\<^bsub>M\<^esub> (\<sigma> P)"
- using UP.exists_irreducible_divisor[of "\<sigma> P"] unfolding pdivides_def by blast
+ and degree_gt: "degree Q > 1"
+ using M.trivial_factors_imp_splitted[of "\<sigma> P"] not_splitted by force
+
+ from \<open>(\<sigma> P) \<in> carrier (poly_ring M)\<close> have "(\<sigma> P) \<noteq> []"
+ using M.degree_zero_imp_splitted[of "\<sigma> P"] not_splitted unfolding \<sigma>_def by auto
- have hyps:
+ have "\<exists>i. \<forall>\<P> \<in> carrier M. index_free \<P> (P, i)"
+ proof (rule ccontr)
+ assume "\<nexists>i. \<forall>\<P> \<in> carrier M. index_free \<P> (P, i)"
+ then have "\<X>\<^bsub>(P, i)\<^esub> \<in> carrier M" and "(ring.eval M) (\<sigma> P) \<X>\<^bsub>(P, i)\<^esub> = \<zero>\<^bsub>M\<^esub>" for i
+ using assms(1,3) unfolding extensions_def by blast+
+ with \<open>(\<sigma> P) \<noteq> []\<close> have "((\<lambda>i :: nat. \<X>\<^bsub>(P, i)\<^esub>) ` UNIV) \<subseteq> { a. (ring.is_root M) (\<sigma> P) a }"
+ unfolding M.is_root_def by auto
+ moreover have "inj (\<lambda>i :: nat. \<X>\<^bsub>(P, i)\<^esub>)"
+ unfolding indexed_var_def indexed_const_def indexed_pmult_def inj_def
+ by (metis (no_types, lifting) add_mset_eq_singleton_iff diff_single_eq_union
+ multi_member_last prod.inject zero_not_one)
+ hence "infinite ((\<lambda>i :: nat. \<X>\<^bsub>(P, i)\<^esub>) ` UNIV)"
+ unfolding infinite_iff_countable_subset by auto
+ ultimately have "infinite { a. (ring.is_root M) (\<sigma> P) a }"
+ using finite_subset by auto
+ with \<open>(\<sigma> P) \<in> carrier (poly_ring M)\<close> show False
+ using M.finite_number_of_roots by simp
+ qed
+ then obtain i :: nat where "\<forall>\<P> \<in> carrier M. index_free \<P> (P, i)"
+ by blast
+
+ then have hyps:
\<comment> \<open>i\<close> "field M"
\<comment> \<open>ii\<close> "\<And>\<P>. \<P> \<in> carrier M \<Longrightarrow> carrier_coeff \<P>"
- \<comment> \<open>iii\<close> "\<And>\<P>. \<P> \<in> carrier M \<Longrightarrow> index_free \<P> P"
+ \<comment> \<open>iii\<close> "\<And>\<P>. \<P> \<in> carrier M \<Longrightarrow> index_free \<P> (P, i)"
\<comment> \<open>iv\<close> "\<zero>\<^bsub>M\<^esub> = indexed_const \<zero>"
- using assms(1,3) no_roots unfolding extensions_def by auto
- have degree_gt: "degree Q > 1"
- proof (rule ccontr)
- assume "\<not> degree Q > 1" hence "degree Q = 1"
- using M.pirreducible_degree[OF M.carrier_is_subfield Q(1-2)] by simp
- then obtain x where "x \<in> carrier M" and "M.eval Q x = \<zero>\<^bsub>M\<^esub>"
- using M.degree_one_root[OF M.carrier_is_subfield Q(1)] M.add.inv_closed by blast
- hence "M.eval (\<sigma> P) x = \<zero>\<^bsub>M\<^esub>"
- using M.pdivides_imp_root_sharing[OF Q(1,3)] by simp
- with \<open>x \<in> carrier M\<close> show False
- using no_roots by simp
- qed
+ using assms(1,3) unfolding extensions_def by auto
- define image_poly where "image_poly = image_ring (eval_pmod M P Q) (poly_ring M)"
+ define image_poly where "image_poly = image_ring (eval_pmod M (P, i) Q) (poly_ring M)"
with \<open>degree Q > 1\<close> have "M \<lesssim> image_poly"
using image_poly_iso_incl[OF hyps Q(1)] by auto
moreover have is_field: "field image_poly"
@@ -530,7 +539,7 @@
moreover have "image_poly \<in> extensions"
proof (auto simp add: extensions_def is_field)
fix \<P> assume "\<P> \<in> carrier image_poly"
- then obtain R where \<P>: "\<P> = eval_pmod M P Q R" and "R \<in> carrier (poly_ring M)"
+ then obtain R where \<P>: "\<P> = eval_pmod M (P, i) Q R" and "R \<in> carrier (poly_ring M)"
unfolding image_poly_def image_ring_carrier by auto
hence "M.pmod R Q \<in> carrier (poly_ring M)"
using M.long_division_closed(2)[OF M.carrier_is_subfield _ Q(1)] by simp
@@ -545,32 +554,32 @@
from \<open>M \<lesssim> image_poly\<close> interpret Id: ring_hom_ring M image_poly id
using iso_inclE[OF M.ring_axioms field.is_ring[OF is_field]] by simp
- fix \<P> S
- assume A: "\<P> \<in> carrier image_poly" "\<not> index_free \<P> S" "S \<in> carrier (poly_ring R)"
- have "\<X>\<^bsub>S\<^esub> \<in> carrier image_poly \<and> Id.eval (\<sigma> S) \<X>\<^bsub>S\<^esub> = \<zero>\<^bsub>image_poly\<^esub>"
+ fix \<P> S j
+ assume A: "\<P> \<in> carrier image_poly" "\<not> index_free \<P> (S, j)" "S \<in> carrier (poly_ring R)"
+ have "\<X>\<^bsub>(S, j)\<^esub> \<in> carrier image_poly \<and> Id.eval (\<sigma> S) \<X>\<^bsub>(S, j)\<^esub> = \<zero>\<^bsub>image_poly\<^esub>"
proof (cases)
- assume "P \<noteq> S"
- then obtain Q' where "Q' \<in> carrier M" and "\<not> index_free Q' S"
+ assume "(P, i) \<noteq> (S, j)"
+ then obtain Q' where "Q' \<in> carrier M" and "\<not> index_free Q' (S, j)"
using A(1) image_poly_index_free[OF hyps Q(1) _ A(2)] unfolding image_poly_def by auto
- hence "\<X>\<^bsub>S\<^esub> \<in> carrier M" and "M.eval (\<sigma> S) \<X>\<^bsub>S\<^esub> = \<zero>\<^bsub>M\<^esub>"
+ hence "\<X>\<^bsub>(S, j)\<^esub> \<in> carrier M" and "M.eval (\<sigma> S) \<X>\<^bsub>(S, j)\<^esub> = \<zero>\<^bsub>M\<^esub>"
using assms(1) A(3) unfolding extensions_def by auto
moreover have "\<sigma> S \<in> carrier (poly_ring M)"
using polynomial_hom[OF Hom.homh field_axioms M.field_axioms A(3)] unfolding \<sigma>_def .
ultimately show ?thesis
using Id.eval_hom[OF M.carrier_is_subring] Id.hom_closed Id.hom_zero by auto
next
- assume "\<not> P \<noteq> S" hence S: "P = S"
+ assume "\<not> (P, i) \<noteq> (S, j)" hence S: "(P, i) = (S, j)"
by simp
have poly_hom: "R \<in> carrier (poly_ring image_poly)" if "R \<in> carrier (poly_ring M)" for R
using polynomial_hom[OF Id.homh M.field_axioms is_field that] by simp
- have "\<X>\<^bsub>S\<^esub> \<in> carrier image_poly"
+ have "\<X>\<^bsub>(S, j)\<^esub> \<in> carrier image_poly"
using eval_pmod_var(2)[OF hyps Hom.homh Q(1) degree_gt] unfolding image_poly_def S by simp
- moreover have "Id.eval Q \<X>\<^bsub>S\<^esub> = \<zero>\<^bsub>image_poly\<^esub>"
+ moreover have "Id.eval Q \<X>\<^bsub>(S, j)\<^esub> = \<zero>\<^bsub>image_poly\<^esub>"
using image_poly_eval_indexed_var[OF hyps Hom.homh Q(1) degree_gt Q(2)] unfolding image_poly_def S by simp
moreover have "Q pdivides\<^bsub>image_poly\<^esub> (\<sigma> S)"
proof -
obtain R where R: "R \<in> carrier (poly_ring M)" "\<sigma> S = Q \<otimes>\<^bsub>poly_ring M\<^esub> R"
- using Q(3) unfolding S pdivides_def by auto
+ using Q(3) S unfolding pdivides_def by auto
moreover have "set Q \<subseteq> carrier M" and "set R \<subseteq> carrier M"
using Q(1) R(1) unfolding sym[OF univ_poly_carrier] polynomial_def by auto
ultimately have "Id.normalize (\<sigma> S) = Q \<otimes>\<^bsub>poly_ring image_poly\<^esub> R"
@@ -590,28 +599,27 @@
ultimately show ?thesis
using domain.pdivides_imp_root_sharing[OF field.axioms(1)[OF is_field], of Q] by auto
qed
- thus "\<X>\<^bsub>S\<^esub> \<in> carrier image_poly" and "Id.eval (\<sigma> S) \<X>\<^bsub>S\<^esub> = \<zero>\<^bsub>image_poly\<^esub>"
+ thus "\<X>\<^bsub>(S, j)\<^esub> \<in> carrier image_poly" and "Id.eval (\<sigma> S) \<X>\<^bsub>(S, j)\<^esub> = \<zero>\<^bsub>image_poly\<^esub>"
by auto
qed
ultimately have "law_restrict M = law_restrict image_poly"
using assms(2) by simp
hence "carrier M = carrier image_poly"
unfolding law_restrict_def by (simp add:ring.defs)
- moreover have "\<X>\<^bsub>P\<^esub> \<in> carrier image_poly"
+ moreover have "\<X>\<^bsub>(P, i)\<^esub> \<in> carrier image_poly"
using eval_pmod_var(2)[OF hyps Hom.homh Q(1) degree_gt] unfolding image_poly_def by simp
- moreover have "\<X>\<^bsub>P\<^esub> \<notin> carrier M"
- using indexed_var_not_index_free[of P] hyps(3) by blast
+ moreover have "\<X>\<^bsub>(P, i)\<^esub> \<notin> carrier M"
+ using indexed_var_not_index_free[of "(P, i)"] hyps(3) by blast
ultimately show False by simp
qed
lemma (in field) exists_extension_with_roots:
- shows "\<exists>L \<in> extensions. \<forall>P \<in> carrier (poly_ring R).
- degree P > 0 \<longrightarrow> (\<exists>x \<in> carrier L. (ring.eval L) (\<sigma> P) x = \<zero>\<^bsub>L\<^esub>)"
+ shows "\<exists>L \<in> extensions. \<forall>P \<in> carrier (poly_ring R). (ring.splitted L) (\<sigma> P)"
proof -
obtain M where "M \<in> extensions" and "\<forall>L \<in> extensions. M \<lesssim> L \<longrightarrow> law_restrict L = law_restrict M"
using exists_maximal_extension iso_incl_hom by blast
thus ?thesis
- using exists_root[of M] by auto
+ using exists_root[of M] by auto
qed
@@ -619,17 +627,16 @@
locale algebraic_closure = field L + subfield K L for L (structure) and K +
assumes algebraic_extension: "x \<in> carrier L \<Longrightarrow> (algebraic over K) x"
- and roots_over_subfield: "\<lbrakk> P \<in> carrier (K[X]); degree P > 0 \<rbrakk> \<Longrightarrow> \<exists>x \<in> carrier L. eval P x = \<zero>\<^bsub>L\<^esub>"
+ and roots_over_subfield: "P \<in> carrier (K[X]) \<Longrightarrow> splitted P"
locale algebraically_closed = field L for L (structure) +
- assumes roots_over_carrier: "\<lbrakk> P \<in> carrier (poly_ring L); degree P > 0 \<rbrakk> \<Longrightarrow> \<exists>x \<in> carrier L. eval P x = \<zero>\<^bsub>L\<^esub>"
+ assumes roots_over_carrier: "P \<in> carrier (poly_ring L) \<Longrightarrow> splitted P"
-definition (in field) closure :: "(('a list) multiset \<Rightarrow> 'a) ring" ("\<Omega>")
- where "closure = (SOME L \<comment> \<open>such that\<close>.
+definition (in field) alg_closure :: "(('a list \<times> nat) multiset \<Rightarrow> 'a) ring"
+ where "alg_closure = (SOME L \<comment> \<open>such that\<close>.
\<comment> \<open>i\<close> algebraic_closure L (indexed_const ` (carrier R)) \<and>
\<comment> \<open>ii\<close> indexed_const \<in> ring_hom R L)"
-
lemma algebraic_hom:
assumes "h \<in> ring_hom R S" and "field R" and "field S" and "subfield K R" and "x \<in> carrier R"
shows "((ring.algebraic R) over K) x \<Longrightarrow> ((ring.algebraic S) over (h ` K)) (h x)"
@@ -648,12 +655,11 @@
qed
lemma (in field) exists_closure:
- obtains L :: "(('a list multiset) \<Rightarrow> 'a) ring"
+ obtains L :: "((('a list \<times> nat) multiset) \<Rightarrow> 'a) ring"
where "algebraic_closure L (indexed_const ` (carrier R))" and "indexed_const \<in> ring_hom R L"
proof -
obtain L where "L \<in> extensions"
- and roots: "\<And>P. \<lbrakk> P \<in> carrier (poly_ring R); degree P > 0 \<rbrakk> \<Longrightarrow>
- \<exists>x \<in> carrier L. (ring.eval L) (\<sigma> P) x = \<zero>\<^bsub>L\<^esub>"
+ and roots: "\<And>P. P \<in> carrier (poly_ring R) \<Longrightarrow> (ring.splitted L) (\<sigma> P)"
using exists_extension_with_roots by auto
let ?K = "indexed_const ` (carrier R)"
@@ -685,7 +691,7 @@
next
show "?K \<subseteq> carrier ?M"
proof
- fix x :: "('a list multiset) \<Rightarrow> 'a"
+ fix x :: "(('a list \<times> nat) multiset) \<Rightarrow> 'a"
assume "x \<in> ?K"
hence "x \<in> carrier L"
using ring_hom_memE(1)[OF ring_hom_ring.homh[OF hom]] by auto
@@ -700,54 +706,126 @@
proof (intro algebraic_closure.intro[OF M is_subfield])
have "(Id.R.algebraic over ?K) x" if "x \<in> carrier ?M" for x
using that Id.S.algebraic_consistent[OF subfieldE(1)[OF set_of_algs]] by simp
- moreover have "\<exists>x \<in> carrier ?M. Id.R.eval P x = \<zero>\<^bsub>?M\<^esub>"
- if "P \<in> carrier (?K[X]\<^bsub>?M\<^esub>)" and "degree P > 0" for P
+ moreover have "Id.R.splitted P" if "P \<in> carrier (?K[X]\<^bsub>?M\<^esub>)" for P
proof -
- from \<open>P \<in> carrier (?K[X]\<^bsub>?M\<^esub>)\<close> have "P \<in> carrier (?K[X]\<^bsub>L\<^esub>)"
- unfolding Id.S.univ_poly_consistent[OF subfieldE(1)[OF set_of_algs]] .
- hence "set P \<subseteq> ?K"
- unfolding sym[OF univ_poly_carrier] polynomial_def by auto
- hence "\<exists>Q. set Q \<subseteq> carrier R \<and> P = \<sigma> Q"
- proof (induct P, simp add: \<sigma>_def)
- case (Cons p P)
- then obtain q Q where "q \<in> carrier R" "set Q \<subseteq> carrier R" and "\<sigma> Q = P""indexed_const q = p"
- unfolding \<sigma>_def by auto
- hence "set (q # Q) \<subseteq> carrier R" and "\<sigma> (q # Q) = (p # P)"
- unfolding \<sigma>_def by auto
- thus ?case
- by metis
- qed
- then obtain Q where "set Q \<subseteq> carrier R" and "\<sigma> Q = P"
- by auto
- moreover have "lead_coeff Q \<noteq> \<zero>"
- proof (rule ccontr)
- assume "\<not> lead_coeff Q \<noteq> \<zero>" then have "lead_coeff Q = \<zero>"
+ from \<open>P \<in> carrier (?K[X]\<^bsub>?M\<^esub>)\<close> have "P \<in> carrier (poly_ring ?M)"
+ using Id.R.carrier_polynomial_shell[OF subfieldE(1)[OF is_subfield]] by simp
+ show ?thesis
+ proof (cases "degree P = 0")
+ case True with \<open>P \<in> carrier (poly_ring ?M)\<close> show ?thesis
+ using domain.degree_zero_imp_splitted[OF field.axioms(1)[OF M]]
+ by fastforce
+ next
+ case False then have "degree P > 0"
by simp
- with \<open>\<sigma> Q = P\<close> and \<open>degree P > 0\<close> have "lead_coeff P = indexed_const \<zero>"
- unfolding \<sigma>_def by (metis diff_0_eq_0 length_map less_irrefl_nat list.map_sel(1) list.size(3))
- hence "lead_coeff P = \<zero>\<^bsub>L\<^esub>"
- using ring_hom_zero[OF ring_hom_ring.homh ring_hom_ring.axioms(1-2)] hom by auto
- with \<open>degree P > 0\<close> have "\<not> P \<in> carrier (?K[X]\<^bsub>?M\<^esub>)"
+ from \<open>P \<in> carrier (?K[X]\<^bsub>?M\<^esub>)\<close> have "P \<in> carrier (?K[X]\<^bsub>L\<^esub>)"
+ unfolding Id.S.univ_poly_consistent[OF subfieldE(1)[OF set_of_algs]] .
+ hence "set P \<subseteq> ?K"
+ unfolding sym[OF univ_poly_carrier] polynomial_def by auto
+ hence "\<exists>Q. set Q \<subseteq> carrier R \<and> P = \<sigma> Q"
+ proof (induct P, simp add: \<sigma>_def)
+ case (Cons p P)
+ then obtain q Q where "q \<in> carrier R" "set Q \<subseteq> carrier R"
+ and "\<sigma> Q = P" "indexed_const q = p"
+ unfolding \<sigma>_def by auto
+ hence "set (q # Q) \<subseteq> carrier R" and "\<sigma> (q # Q) = (p # P)"
+ unfolding \<sigma>_def by auto
+ thus ?case
+ by metis
+ qed
+ then obtain Q where "set Q \<subseteq> carrier R" and "\<sigma> Q = P"
+ by auto
+ moreover have "lead_coeff Q \<noteq> \<zero>"
+ proof (rule ccontr)
+ assume "\<not> lead_coeff Q \<noteq> \<zero>" then have "lead_coeff Q = \<zero>"
+ by simp
+ with \<open>\<sigma> Q = P\<close> and \<open>degree P > 0\<close> have "lead_coeff P = indexed_const \<zero>"
+ unfolding \<sigma>_def by (metis diff_0_eq_0 length_map less_irrefl_nat list.map_sel(1) list.size(3))
+ hence "lead_coeff P = \<zero>\<^bsub>L\<^esub>"
+ using ring_hom_zero[OF ring_hom_ring.homh ring_hom_ring.axioms(1-2)] hom by auto
+ with \<open>degree P > 0\<close> have "\<not> P \<in> carrier (?K[X]\<^bsub>?M\<^esub>)"
+ unfolding sym[OF univ_poly_carrier] polynomial_def by auto
+ with \<open>P \<in> carrier (?K[X]\<^bsub>?M\<^esub>)\<close> show False
+ by simp
+ qed
+ ultimately have "Q \<in> carrier (poly_ring R)"
unfolding sym[OF univ_poly_carrier] polynomial_def by auto
- with \<open>P \<in> carrier (?K[X]\<^bsub>?M\<^esub>)\<close> show False
- by simp
+ with \<open>\<sigma> Q = P\<close> have "Id.S.splitted P"
+ using roots[of Q] by simp
+
+ from \<open>P \<in> carrier (poly_ring ?M)\<close> show ?thesis
+ proof (rule field.trivial_factors_imp_splitted[OF M])
+ fix R
+ assume R: "R \<in> carrier (poly_ring ?M)" "pirreducible\<^bsub>?M\<^esub> (carrier ?M) R" and "R pdivides\<^bsub>?M\<^esub> P"
+
+ from \<open>P \<in> carrier (poly_ring ?M)\<close> and \<open>R \<in> carrier (poly_ring ?M)\<close>
+ have "P \<in> carrier ((?set_of_algs)[X]\<^bsub>L\<^esub>)" and "R \<in> carrier ((?set_of_algs)[X]\<^bsub>L\<^esub>)"
+ unfolding Id.S.univ_poly_consistent[OF subfieldE(1)[OF set_of_algs]] by auto
+ hence in_carrier: "P \<in> carrier (poly_ring L)" "R \<in> carrier (poly_ring L)"
+ using Id.S.carrier_polynomial_shell[OF subfieldE(1)[OF set_of_algs]] by auto
+
+ from \<open>R pdivides\<^bsub>?M\<^esub> P\<close> have "R divides\<^bsub>((?set_of_algs)[X]\<^bsub>L\<^esub>)\<^esub> P"
+ unfolding pdivides_def Id.S.univ_poly_consistent[OF subfieldE(1)[OF set_of_algs]]
+ by simp
+ with \<open>P \<in> carrier ((?set_of_algs)[X]\<^bsub>L\<^esub>)\<close> and \<open>R \<in> carrier ((?set_of_algs)[X]\<^bsub>L\<^esub>)\<close>
+ have "R pdivides\<^bsub>L\<^esub> P"
+ using domain.pdivides_iff_shell[OF field.axioms(1)[OF L] set_of_algs, of R P] by simp
+ with \<open>Id.S.splitted P\<close> and \<open>degree P \<noteq> 0\<close> have "Id.S.splitted R"
+ using field.pdivides_imp_splitted[OF L in_carrier(2,1)] by fastforce
+ show "degree R \<le> 1"
+ proof (cases "Id.S.roots R = {#}")
+ case True with \<open>Id.S.splitted R\<close> show ?thesis
+ unfolding Id.S.splitted_def by simp
+ next
+ case False with \<open>R \<in> carrier (poly_ring L)\<close>
+ obtain a where "a \<in> carrier L" and "a \<in># Id.S.roots R"
+ and "[ \<one>\<^bsub>L\<^esub>, \<ominus>\<^bsub>L\<^esub> a ] \<in> carrier (poly_ring L)" and pdiv: "[ \<one>\<^bsub>L\<^esub>, \<ominus>\<^bsub>L\<^esub> a ] pdivides\<^bsub>L\<^esub> R"
+ using domain.not_empty_rootsE[OF field.axioms(1)[OF L], of R] by blast
+
+ from \<open>P \<in> carrier (?K[X]\<^bsub>L\<^esub>)\<close>
+ have "(Id.S.algebraic over ?K) a"
+ proof (rule Id.S.algebraicI)
+ from \<open>degree P \<noteq> 0\<close> show "P \<noteq> []"
+ by auto
+ next
+ from \<open>a \<in># Id.S.roots R\<close> and \<open>R \<in> carrier (poly_ring L)\<close>
+ have "Id.S.eval R a = \<zero>\<^bsub>L\<^esub>"
+ using domain.roots_mem_iff_is_root[OF field.axioms(1)[OF L]]
+ unfolding Id.S.is_root_def by auto
+ with \<open>R pdivides\<^bsub>L\<^esub> P\<close> and \<open>a \<in> carrier L\<close> show "Id.S.eval P a = \<zero>\<^bsub>L\<^esub>"
+ using domain.pdivides_imp_root_sharing[OF field.axioms(1)[OF L] in_carrier(2)] by simp
+ qed
+ with \<open>a \<in> carrier L\<close> have "a \<in> ?set_of_algs"
+ by simp
+ hence "[ \<one>\<^bsub>L\<^esub>, \<ominus>\<^bsub>L\<^esub> a ] \<in> carrier ((?set_of_algs)[X]\<^bsub>L\<^esub>)"
+ using subringE(3,5)[of ?set_of_algs L] subfieldE(1,6)[OF set_of_algs]
+ unfolding sym[OF univ_poly_carrier] polynomial_def by simp
+ hence "[ \<one>\<^bsub>L\<^esub>, \<ominus>\<^bsub>L\<^esub> a ] \<in> carrier (poly_ring ?M)"
+ unfolding Id.S.univ_poly_consistent[OF subfieldE(1)[OF set_of_algs]] by simp
+
+ from \<open>[ \<one>\<^bsub>L\<^esub>, \<ominus>\<^bsub>L\<^esub> a ] \<in> carrier ((?set_of_algs)[X]\<^bsub>L\<^esub>)\<close>
+ and \<open>R \<in> carrier ((?set_of_algs)[X]\<^bsub>L\<^esub>)\<close>
+ have "[ \<one>\<^bsub>L\<^esub>, \<ominus>\<^bsub>L\<^esub> a ] divides\<^bsub>(?set_of_algs)[X]\<^bsub>L\<^esub>\<^esub> R"
+ using pdiv domain.pdivides_iff_shell[OF field.axioms(1)[OF L] set_of_algs] by simp
+ hence "[ \<one>\<^bsub>L\<^esub>, \<ominus>\<^bsub>L\<^esub> a ] divides\<^bsub>poly_ring ?M\<^esub> R"
+ unfolding pdivides_def Id.S.univ_poly_consistent[OF subfieldE(1)[OF set_of_algs]]
+ by simp
+
+ have "[ \<one>\<^bsub>L\<^esub>, \<ominus>\<^bsub>L\<^esub> a ] \<notin> Units (poly_ring ?M)"
+ using Id.R.univ_poly_units[OF field.carrier_is_subfield[OF M]] by force
+ with \<open>[ \<one>\<^bsub>L\<^esub>, \<ominus>\<^bsub>L\<^esub> a ] \<in> carrier (poly_ring ?M)\<close> and \<open>R \<in> carrier (poly_ring ?M)\<close>
+ and \<open>[ \<one>\<^bsub>L\<^esub>, \<ominus>\<^bsub>L\<^esub> a ] divides\<^bsub>poly_ring ?M\<^esub> R\<close>
+ have "[ \<one>\<^bsub>L\<^esub>, \<ominus>\<^bsub>L\<^esub> a ] \<sim>\<^bsub>poly_ring ?M\<^esub> R"
+ using Id.R.divides_pirreducible_condition[OF R(2)] by auto
+ with \<open>[ \<one>\<^bsub>L\<^esub>, \<ominus>\<^bsub>L\<^esub> a ] \<in> carrier (poly_ring ?M)\<close> and \<open>R \<in> carrier (poly_ring ?M)\<close>
+ have "degree R = 1"
+ using domain.associated_polynomials_imp_same_length[OF field.axioms(1)[OF M]
+ Id.R.carrier_is_subring, of "[ \<one>\<^bsub>L\<^esub>, \<ominus>\<^bsub>L\<^esub> a ]" R] by force
+ thus ?thesis
+ by simp
+ qed
+ qed
qed
- ultimately have "Q \<in> carrier (poly_ring R)"
- unfolding sym[OF univ_poly_carrier] polynomial_def by auto
- moreover from \<open>degree P > 0\<close> and \<open>\<sigma> Q = P\<close> have "degree Q > 0"
- unfolding \<sigma>_def by auto
- ultimately obtain x where "x \<in> carrier L" and "Id.S.eval P x = \<zero>\<^bsub>L\<^esub>"
- using roots[of Q] unfolding \<open>\<sigma> Q = P\<close> by auto
- hence "Id.R.eval P x = \<zero>\<^bsub>?M\<^esub>"
- unfolding Id.S.eval_consistent[OF subfieldE(1)[OF set_of_algs]] by simp
- moreover from \<open>degree P > 0\<close> have "P \<noteq> []"
- by auto
- with \<open>P \<in> carrier (?K[X]\<^bsub>L\<^esub>)\<close> and \<open>Id.S.eval P x = \<zero>\<^bsub>L\<^esub>\<close> have "(Id.S.algebraic over ?K) x"
- using Id.S.non_trivial_ker_imp_algebraic[of ?K x] unfolding a_kernel_def' by auto
- with \<open>x \<in> carrier L\<close> have "x \<in> carrier ?M"
- by auto
- ultimately show ?thesis
- by auto
qed
ultimately show "algebraic_closure_axioms ?M ?K"
unfolding algebraic_closure_axioms_def by auto
@@ -759,10 +837,178 @@
using that by auto
qed
-lemma (in field) closureE:
- shows "algebraic_closure \<Omega> (indexed_const ` (carrier R))" and "indexed_const \<in> ring_hom R \<Omega>"
- using exists_closure unfolding closure_def
+lemma (in field) alg_closureE:
+ shows "algebraic_closure alg_closure (indexed_const ` (carrier R))"
+ and "indexed_const \<in> ring_hom R alg_closure"
+ using exists_closure unfolding alg_closure_def
by (metis (mono_tags, lifting) someI2)+
+lemma (in field) algebraically_closedI':
+ assumes "\<And>p. \<lbrakk> p \<in> carrier (poly_ring R); degree p > 1 \<rbrakk> \<Longrightarrow> splitted p"
+ shows "algebraically_closed R"
+proof
+ fix p assume "p \<in> carrier (poly_ring R)" show "splitted p"
+ proof (cases "degree p \<le> 1")
+ case True with \<open>p \<in> carrier (poly_ring R)\<close> show ?thesis
+ using degree_zero_imp_splitted degree_one_imp_splitted by fastforce
+ next
+ case False with \<open>p \<in> carrier (poly_ring R)\<close> show ?thesis
+ using assms by fastforce
+ qed
+qed
+
+lemma (in field) algebraically_closedI:
+ assumes "\<And>p. \<lbrakk> p \<in> carrier (poly_ring R); degree p > 1 \<rbrakk> \<Longrightarrow> \<exists>x \<in> carrier R. eval p x = \<zero>"
+ shows "algebraically_closed R"
+proof
+ fix p assume "p \<in> carrier (poly_ring R)" thus "splitted p"
+ proof (induction "degree p" arbitrary: p rule: less_induct)
+ case less show ?case
+ proof (cases "degree p \<le> 1")
+ case True with \<open>p \<in> carrier (poly_ring R)\<close> show ?thesis
+ using degree_zero_imp_splitted degree_one_imp_splitted by fastforce
+ next
+ case False then have "degree p > 1"
+ by simp
+ with \<open>p \<in> carrier (poly_ring R)\<close> have "roots p \<noteq> {#}"
+ using assms[of p] roots_mem_iff_is_root[of p] unfolding is_root_def by force
+ then obtain a where a: "a \<in> carrier R" "a \<in># roots p"
+ and pdiv: "[ \<one>, \<ominus> a ] pdivides p" and in_carrier: "[ \<one>, \<ominus> a ] \<in> carrier (poly_ring R)"
+ using less(2) by blast
+ then obtain q where q: "q \<in> carrier (poly_ring R)" and p: "p = [ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> q"
+ unfolding pdivides_def by blast
+ with \<open>degree p > 1\<close> have not_zero: "q \<noteq> []" and "p \<noteq> []"
+ using domain.integral_iff[OF univ_poly_is_domain[OF carrier_is_subring] in_carrier, of q]
+ by (auto simp add: univ_poly_zero[of R "carrier R"])
+ hence deg: "degree p = Suc (degree q)"
+ using poly_mult_degree_eq[OF carrier_is_subring] in_carrier q p
+ unfolding univ_poly_carrier sym[OF univ_poly_mult[of R "carrier R"]] by auto
+ hence "splitted q"
+ using less(1)[OF _ q] by simp
+ moreover have "roots p = add_mset a (roots q)"
+ using poly_mult_degree_one_monic_imp_same_roots[OF a(1) q not_zero] p by simp
+ ultimately show ?thesis
+ unfolding splitted_def deg by simp
+ qed
+ qed
+qed
+
+sublocale algebraic_closure \<subseteq> algebraically_closed
+proof (rule algebraically_closedI')
+ fix P assume in_carrier: "P \<in> carrier (poly_ring L)" and gt_one: "degree P > 1"
+ then have gt_zero: "degree P > 0"
+ by simp
+
+ define A where "A = finite_extension K P"
+
+ from \<open>P \<in> carrier (poly_ring L)\<close> have "set P \<subseteq> carrier L"
+ by (simp add: polynomial_incl univ_poly_carrier)
+ hence A: "subfield A L" and P: "P \<in> carrier (A[X])"
+ using finite_extension_mem[OF subfieldE(1)[OF subfield_axioms], of P] in_carrier
+ algebraic_extension finite_extension_is_subfield[OF subfield_axioms, of P]
+ unfolding sym[OF A_def] sym[OF univ_poly_carrier] polynomial_def by auto
+ from \<open>set P \<subseteq> carrier L\<close> have incl: "K \<subseteq> A"
+ using finite_extension_incl[OF subfieldE(3)[OF subfield_axioms]] unfolding A_def by simp
+
+ interpret UP_K: domain "K[X]"
+ using univ_poly_is_domain[OF subfieldE(1)[OF subfield_axioms]] .
+ interpret UP_A: domain "A[X]"
+ using univ_poly_is_domain[OF subfieldE(1)[OF A]] .
+ interpret Rupt: ring "Rupt A P"
+ unfolding rupture_def using ideal.quotient_is_ring[OF UP_A.cgenideal_ideal[OF P]] .
+ interpret Hom: ring_hom_ring "L \<lparr> carrier := A \<rparr>" "Rupt A P" "rupture_surj A P \<circ> poly_of_const"
+ using ring_hom_ringI2[OF subring_is_ring[OF subfieldE(1)] Rupt.ring_axioms
+ rupture_surj_norm_is_hom[OF subfieldE(1) P]] A by simp
+ let ?h = "rupture_surj A P \<circ> poly_of_const"
+
+ have h_simp: "rupture_surj A P ` poly_of_const ` E = ?h ` E" for E
+ by auto
+ hence aux_lemmas:
+ "subfield (rupture_surj A P ` poly_of_const ` K) (Rupt A P)"
+ "subfield (rupture_surj A P ` poly_of_const ` A) (Rupt A P)"
+ using Hom.img_is_subfield(2)[OF _ rupture_one_not_zero[OF A P gt_zero]]
+ ring.subfield_iff(1)[OF subring_is_ring[OF subfieldE(1)[OF A]]]
+ subfield_iff(2)[OF subfield_axioms] subfield_iff(2)[OF A] incl
+ by auto
+
+ have "carrier (K[X]) \<subseteq> carrier (A[X])"
+ using subsetI[of "carrier (K[X])" "carrier (A[X])"] incl
+ unfolding sym[OF univ_poly_carrier] polynomial_def by auto
+ hence "id \<in> ring_hom (K[X]) (A[X])"
+ unfolding ring_hom_def unfolding univ_poly_mult univ_poly_add univ_poly_one by (simp add: subsetD)
+ hence "rupture_surj A P \<in> ring_hom (K[X]) (Rupt A P)"
+ using ring_hom_trans[OF _ rupture_surj_hom(1)[OF subfieldE(1)[OF A] P], of id] by simp
+ then interpret Hom': ring_hom_ring "K[X]" "Rupt A P" "rupture_surj A P"
+ using ring_hom_ringI2[OF UP_K.ring_axioms Rupt.ring_axioms] by simp
+
+ from \<open>id \<in> ring_hom (K[X]) (A[X])\<close> have Id: "ring_hom_ring (K[X]) (A[X]) id"
+ using ring_hom_ringI2[OF UP_K.ring_axioms UP_A.ring_axioms] by simp
+ hence "subalgebra (poly_of_const ` K) (carrier (K[X])) (A[X])"
+ using ring_hom_ring.img_is_subalgebra[OF Id _ UP_K.carrier_is_subalgebra[OF subfieldE(3)]]
+ univ_poly_subfield_of_consts[OF subfield_axioms] by auto
+
+ moreover from \<open>carrier (K[X]) \<subseteq> carrier (A[X])\<close> have "poly_of_const ` K \<subseteq> carrier (A[X])"
+ using subfieldE(3)[OF univ_poly_subfield_of_consts[OF subfield_axioms]] by simp
+
+ ultimately
+ have "subalgebra (rupture_surj A P ` poly_of_const ` K) (rupture_surj A P ` carrier (K[X])) (Rupt A P)"
+ using ring_hom_ring.img_is_subalgebra[OF rupture_surj_hom(2)[OF subfieldE(1)[OF A] P]] by simp
+
+ moreover have "Rupt.finite_dimension (rupture_surj A P ` poly_of_const ` K) (carrier (Rupt A P))"
+ proof (intro Rupt.telescopic_base_dim(1)[where
+ ?K = "rupture_surj A P ` poly_of_const ` K" and
+ ?F = "rupture_surj A P ` poly_of_const ` A" and
+ ?E = "carrier (Rupt A P)", OF aux_lemmas])
+ show "Rupt.finite_dimension (rupture_surj A P ` poly_of_const ` A) (carrier (Rupt A P))"
+ using Rupt.finite_dimensionI[OF rupture_dimension[OF A P gt_zero]] .
+ next
+ let ?h = "rupture_surj A P \<circ> poly_of_const"
+
+ from \<open>set P \<subseteq> carrier L\<close> have "finite_dimension K A"
+ using finite_extension_finite_dimension(1)[OF subfield_axioms, of P] algebraic_extension
+ unfolding A_def by auto
+ then obtain Us where Us: "set Us \<subseteq> carrier L" "A = Span K Us"
+ using exists_base subfield_axioms by blast
+ hence "?h ` A = Rupt.Span (?h ` K) (map ?h Us)"
+ using Hom.Span_hom[of K Us] incl Span_base_incl[OF subfield_axioms, of Us]
+ unfolding Span_consistent[OF subfieldE(1)[OF A]] by simp
+ moreover have "set (map ?h Us) \<subseteq> carrier (Rupt A P)"
+ using Span_base_incl[OF subfield_axioms Us(1)] ring_hom_memE(1)[OF Hom.homh]
+ unfolding sym[OF Us(2)] by auto
+ ultimately
+ show "Rupt.finite_dimension (rupture_surj A P ` poly_of_const ` K) (rupture_surj A P ` poly_of_const ` A)"
+ using Rupt.Span_finite_dimension[OF aux_lemmas(1)] unfolding h_simp by simp
+ qed
+
+ moreover have "rupture_surj A P ` carrier (A[X]) = carrier (Rupt A P)"
+ unfolding rupture_def FactRing_def A_RCOSETS_def' by auto
+ with \<open>carrier (K[X]) \<subseteq> carrier (A[X])\<close> have "rupture_surj A P ` carrier (K[X]) \<subseteq> carrier (Rupt A P)"
+ by auto
+
+ ultimately
+ have "Rupt.finite_dimension (rupture_surj A P ` poly_of_const ` K) (rupture_surj A P ` carrier (K[X]))"
+ using Rupt.subalbegra_incl_imp_finite_dimension[OF aux_lemmas(1)] by simp
+
+ hence "\<not> inj_on (rupture_surj A P) (carrier (K[X]))"
+ using Hom'.infinite_dimension_hom[OF _ rupture_one_not_zero[OF A P gt_zero] _
+ UP_K.carrier_is_subalgebra[OF subfieldE(3)] univ_poly_infinite_dimension[OF subfield_axioms]]
+ univ_poly_subfield_of_consts[OF subfield_axioms]
+ by auto
+ then obtain Q where Q: "Q \<in> carrier (K[X])" "Q \<noteq> []" and "rupture_surj A P Q = \<zero>\<^bsub>Rupt A P\<^esub>"
+ using Hom'.trivial_ker_imp_inj Hom'.hom_zero unfolding a_kernel_def' univ_poly_zero by blast
+ with \<open>carrier (K[X]) \<subseteq> carrier (A[X])\<close> have "Q \<in> PIdl\<^bsub>A[X]\<^esub> P"
+ using ideal.rcos_const_imp_mem[OF UP_A.cgenideal_ideal[OF P]]
+ unfolding rupture_def FactRing_def by auto
+ then obtain R where "R \<in> carrier (A[X])" and "Q = R \<otimes>\<^bsub>A[X]\<^esub> P"
+ unfolding cgenideal_def by blast
+ with \<open>P \<in> carrier (A[X])\<close> have "P pdivides Q"
+ using dividesI[of _ "A[X]"] UP_A.m_comm pdivides_iff_shell[OF A] by simp
+ thus "splitted P"
+ using pdivides_imp_splitted[OF in_carrier
+ carrier_polynomial_shell[OF subfieldE(1)[OF subfield_axioms] Q(1)] Q(2)
+ roots_over_subfield[OF Q(1)]] Q
+ by simp
+qed
+
end
-
+
--- a/src/HOL/Algebra/Divisibility.thy Tue Apr 30 21:04:08 2019 +0100
+++ b/src/HOL/Algebra/Divisibility.thy Tue Apr 30 21:04:21 2019 +0100
@@ -398,12 +398,12 @@
subsubsection \<open>Multiplication and associativity\<close>
-lemma (in monoid_cancel) mult_cong_r:
+lemma (in monoid) mult_cong_r:
assumes "b \<sim> b'" "a \<in> carrier G" "b \<in> carrier G" "b' \<in> carrier G"
shows "a \<otimes> b \<sim> a \<otimes> b'"
by (meson assms associated_def divides_mult_lI)
-lemma (in comm_monoid_cancel) mult_cong_l:
+lemma (in comm_monoid) mult_cong_l:
assumes "a \<sim> a'" "a \<in> carrier G" "a' \<in> carrier G" "b \<in> carrier G"
shows "a \<otimes> b \<sim> a' \<otimes> b"
using assms m_comm mult_cong_r by auto
@@ -723,6 +723,11 @@
qed
qed
+lemma divides_irreducible_condition:
+ assumes "irreducible G r" and "a \<in> carrier G"
+ shows "a divides\<^bsub>G\<^esub> r \<Longrightarrow> a \<in> Units G \<or> a \<sim>\<^bsub>G\<^esub> r"
+ using assms unfolding irreducible_def properfactor_def associated_def
+ by (cases "r divides\<^bsub>G\<^esub> a", auto)
subsubsection \<open>Prime elements\<close>
@@ -775,6 +780,36 @@
using A(1) Units_one_closed b'(1) unit_factor by presburger
qed
+lemma (in comm_monoid_cancel) prime_pow_divides_iff:
+ assumes "p \<in> carrier G" "a \<in> carrier G" "b \<in> carrier G" and "prime G p" and "\<not> (p divides a)"
+ shows "(p [^] (n :: nat)) divides (a \<otimes> b) \<longleftrightarrow> (p [^] n) divides b"
+proof
+ assume "(p [^] n) divides b" thus "(p [^] n) divides (a \<otimes> b)"
+ using divides_prod_l[of "p [^] n" b a] assms by simp
+next
+ assume "(p [^] n) divides (a \<otimes> b)" thus "(p [^] n) divides b"
+ proof (induction n)
+ case 0 with \<open>b \<in> carrier G\<close> show ?case
+ by (simp add: unit_divides)
+ next
+ case (Suc n)
+ hence "(p [^] n) divides (a \<otimes> b)" and "(p [^] n) divides b"
+ using assms(1) divides_prod_r by auto
+ with \<open>(p [^] (Suc n)) divides (a \<otimes> b)\<close> obtain c d
+ where c: "c \<in> carrier G" and "b = (p [^] n) \<otimes> c"
+ and d: "d \<in> carrier G" and "a \<otimes> b = (p [^] (Suc n)) \<otimes> d"
+ using assms by blast
+ hence "(p [^] n) \<otimes> (a \<otimes> c) = (p [^] n) \<otimes> (p \<otimes> d)"
+ using assms by (simp add: m_assoc m_lcomm)
+ hence "a \<otimes> c = p \<otimes> d"
+ using c d assms(1) assms(2) l_cancel by blast
+ with \<open>\<not> (p divides a)\<close> and \<open>prime G p\<close> have "p divides c"
+ by (metis assms(2) c d dividesI' prime_divides)
+ with \<open>b = (p [^] n) \<otimes> c\<close> show ?case
+ using assms(1) c by simp
+ qed
+qed
+
subsection \<open>Factorization and Factorial Monoids\<close>
--- a/src/HOL/Algebra/Finite_Extensions.thy Tue Apr 30 21:04:08 2019 +0100
+++ b/src/HOL/Algebra/Finite_Extensions.thy Tue Apr 30 21:04:21 2019 +0100
@@ -293,8 +293,11 @@
using assms(1) lin(2) unfolding polynomial_def by auto
hence "eval (normalize (p @ [ k2 ])) x = k1 \<otimes> x \<oplus> k2"
using eval_append_aux[of p k2 x] eval_normalize[of "p @ [ k2 ]" x] assms(2) p(3) by auto
- thus ?case
- using normalize_gives_polynomial[of "p @ [ k2 ]"] polynomial_incl[OF p(2)] lin(2)
+ moreover have "set (p @ [k2]) \<subseteq> K"
+ using polynomial_incl[OF p(2)] \<open>k2 \<in> K\<close> by auto
+ then have "local.normalize (p @ [k2]) \<in> carrier (K [X])"
+ using normalize_gives_polynomial univ_poly_carrier by blast
+ ultimately show ?case
unfolding univ_poly_carrier by force
qed
qed
@@ -720,91 +723,4 @@
qed
qed
-
-(*
-proposition (in domain) finite_extension_is_subfield:
- assumes "subfield K R" "set xs \<subseteq> carrier R"
- shows "subfield (finite_extension K xs) R \<longleftrightarrow> (algebraic_set over K) (set xs)"
-proof
- have "(\<And>x. x \<in> set xs \<Longrightarrow> (algebraic over K) x) \<Longrightarrow> subfield (finite_extension K xs) R"
- using simple_extension_is_subfield algebraic_mono assms
- by (induct xs) (auto, metis finite_extension.simps finite_extension_incl subring_props(1))
- thus "(algebraic_set over K) (set xs) \<Longrightarrow> subfield (finite_extension K xs) R"
- unfolding algebraic_set_def over_def by auto
-next
- { fix x xs
- assume x: "x \<in> carrier R" and xs: "set xs \<subseteq> carrier R"
- and is_subfield: "subfield (finite_extension K (x # xs)) R"
- hence "(algebraic over K) x" sorry }
-
- assume "subfield (finite_extension K xs) R" thus "(algebraic_set over K) (set xs)"
- using assms(2)
- proof (induct xs)
- case Nil thus ?case
- unfolding algebraic_set_def over_def by simp
- next
- case (Cons x xs)
- have "(algebraic over K) x"
- using simple_extension_subfield_imp_algebraic[OF
- finite_extension_is_subring[of K xs], of x]
-
- then show ?case sorry
- qed
-qed
-*)
-
-(*
-lemma (in ring) transcendental_imp_trivial_ker:
- assumes "x \<in> carrier R"
- shows "(transcendental over K) x \<Longrightarrow> (\<And>p. \<lbrakk> polynomial R p; set p \<subseteq> K \<rbrakk> \<Longrightarrow> eval p x = \<zero> \<Longrightarrow> p = [])"
-proof -
- fix p assume "(transcendental over K) x" "polynomial R p" "eval p x = \<zero>" "set p \<subseteq> K"
- moreover have "eval [] x = \<zero>" and "polynomial R []"
- using assms zero_is_polynomial by auto
- ultimately show "p = []"
- unfolding over_def transcendental_def inj_on_def by auto
-qed
-
-lemma (in domain) trivial_ker_imp_transcendental:
- assumes "subring K R" and "x \<in> carrier R"
- shows "(\<And>p. \<lbrakk> polynomial R p; set p \<subseteq> K \<rbrakk> \<Longrightarrow> eval p x = \<zero> \<Longrightarrow> p = []) \<Longrightarrow> (transcendental over K) x"
-proof -
- assume "\<And>p. \<lbrakk> polynomial R p; set p \<subseteq> K \<rbrakk> \<Longrightarrow> eval p x = \<zero> \<Longrightarrow> p = []"
- hence "a_kernel (univ_poly (R \<lparr> carrier := K \<rparr>)) R (\<lambda>p. local.eval p x) = { [] }"
- unfolding a_kernel_def' univ_poly_subring_def'[OF assms(1)] by auto
- moreover have "[] = \<zero>\<^bsub>(univ_poly (R \<lparr> carrier := K \<rparr>))\<^esub>"
- unfolding univ_poly_def by auto
- ultimately have "inj_on (\<lambda>p. local.eval p x) (carrier (univ_poly (R \<lparr> carrier := K \<rparr>)))"
- using ring_hom_ring.trivial_ker_imp_inj[OF eval_ring_hom[OF assms]] by auto
- thus "(transcendental over K) x"
- unfolding over_def transcendental_def univ_poly_subring_def'[OF assms(1)] by simp
-qed
-
-lemma (in ring) non_trivial_ker_imp_algebraic:
- assumes "x \<in> carrier R"
- and "p \<noteq> []" "polynomial R p" "set p \<subseteq> K" "eval p x = \<zero>"
- shows "(algebraic over K) x"
- using transcendental_imp_trivial_ker[OF assms(1) _ assms(3-5)] assms(2)
- unfolding over_def algebraic_def by auto
-
-lemma (in domain) algebraic_imp_non_trivial_ker:
- assumes "subring K R" "x \<in> carrier R"
- shows "(algebraic over K) x \<Longrightarrow> (\<exists>p \<noteq> []. polynomial R p \<and> set p \<subseteq> K \<and> eval p x = \<zero>)"
- using trivial_ker_imp_transcendental[OF assms]
- unfolding over_def algebraic_def by auto
-
-lemma (in domain) algebraic_iff:
- assumes "subring K R" "x \<in> carrier R"
- shows "(algebraic over K) x \<longleftrightarrow> (\<exists>p \<noteq> []. polynomial R p \<and> set p \<subseteq> K \<and> eval p x = \<zero>)"
- using non_trivial_ker_imp_algebraic[OF assms(2)] algebraic_imp_non_trivial_ker[OF assms] by auto
-*)
-
-
-(*
-lemma (in field)
- assumes "subfield K R"
- shows "subfield (simple_extension K x) R \<longleftrightarrow> (algebraic over K) x"
- sorry
-
-*)
end
\ No newline at end of file
--- a/src/HOL/Algebra/Ideal.thy Tue Apr 30 21:04:08 2019 +0100
+++ b/src/HOL/Algebra/Ideal.thy Tue Apr 30 21:04:21 2019 +0100
@@ -193,7 +193,7 @@
qed
-subsection \<open>General Ideal Properies\<close>
+subsection \<open>General Ideal Properties\<close>
lemma (in ideal) one_imp_carrier:
assumes I_one_closed: "\<one> \<in> I"
@@ -210,6 +210,30 @@
shows "i \<in> carrier R"
using iI by (rule a_Hcarr)
+lemma (in ring) quotient_eq_iff_same_a_r_cos:
+ assumes "ideal I R" and "a \<in> carrier R" and "b \<in> carrier R"
+ shows "a \<ominus> b \<in> I \<longleftrightarrow> I +> a = I +> b"
+proof
+ assume "I +> a = I +> b"
+ then obtain i where "i \<in> I" and "\<zero> \<oplus> a = i \<oplus> b"
+ using additive_subgroup.zero_closed[OF ideal.axioms(1)[OF assms(1)]] assms(2)
+ unfolding a_r_coset_def' by blast
+ hence "a \<ominus> b = i"
+ using assms(2-3) by (metis a_minus_def add.inv_solve_right assms(1) ideal.Icarr l_zero)
+ with \<open>i \<in> I\<close> show "a \<ominus> b \<in> I"
+ by simp
+next
+ assume "a \<ominus> b \<in> I"
+ then obtain i where "i \<in> I" and "a = i \<oplus> b"
+ using ideal.Icarr[OF assms(1)] assms(2-3)
+ by (metis a_minus_def add.inv_solve_right)
+ hence "I +> a = (I +> i) +> b"
+ using ideal.Icarr[OF assms(1)] assms(3)
+ by (simp add: a_coset_add_assoc subsetI)
+ with \<open>i \<in> I\<close> show "I +> a = I +> b"
+ using a_rcos_zero[OF assms(1)] by simp
+qed
+
subsection \<open>Intersection of Ideals\<close>
--- a/src/HOL/Algebra/Polynomial_Divisibility.thy Tue Apr 30 21:04:08 2019 +0100
+++ b/src/HOL/Algebra/Polynomial_Divisibility.thy Tue Apr 30 21:04:21 2019 +0100
@@ -122,6 +122,11 @@
using field.univ_poly_carrier_units[OF subfield_iff(2)[OF assms]]
univ_poly_consistent[OF subfieldE(1)[OF assms]] by auto
+lemma (in domain) univ_poly_units':
+ assumes "subfield K R" shows "p \<in> Units (K[X]) \<longleftrightarrow> p \<in> carrier (K[X]) \<and> p \<noteq> [] \<and> degree p = 0"
+ unfolding univ_poly_units[OF assms] sym[OF univ_poly_carrier] polynomial_def
+ by (auto, metis hd_in_set le_0_eq le_Suc_eq length_0_conv length_Suc_conv list.sel(1) subsetD)
+
corollary (in domain) rupture_one_not_zero:
assumes "subfield K R" and "p \<in> carrier (K[X])" and "degree p > 0"
shows "\<one>\<^bsub>Rupt K p\<^esub> \<noteq> \<zero>\<^bsub>Rupt K p\<^esub>"
@@ -727,12 +732,286 @@
unfolding univ_poly_units[OF assms(1)] by auto
corollary (in domain) associated_polynomials_imp_same_length: (* stronger than "imp_same_degree" *)
- assumes "subfield K R" and "p \<in> carrier (K[X])" "q \<in> carrier (K[X])"
+ assumes "subring K R" and "p \<in> carrier (K[X])" and "q \<in> carrier (K[X])"
shows "p \<sim>\<^bsub>K[X]\<^esub> q \<Longrightarrow> length p = length q"
- unfolding associated_polynomials_iff[OF assms]
- using poly_mult_const(1)[OF subfieldE(1)[OF assms(1)],of q] assms(3)
- by (auto simp add: univ_poly_carrier univ_poly_mult simp del: poly_mult.simps)
+proof -
+ { fix p q
+ assume p: "p \<in> carrier (K[X])" and q: "q \<in> carrier (K[X])" and "p \<sim>\<^bsub>K[X]\<^esub> q"
+ have "length p \<le> length q"
+ proof (cases "q = []")
+ case True with \<open>p \<sim>\<^bsub>K[X]\<^esub> q\<close> have "p = []"
+ unfolding associated_def True factor_def univ_poly_def by auto
+ thus ?thesis
+ using True by simp
+ next
+ case False
+ from \<open>p \<sim>\<^bsub>K[X]\<^esub> q\<close> have "p divides\<^bsub>K [X]\<^esub> q"
+ unfolding associated_def by simp
+ hence "p divides\<^bsub>poly_ring R\<^esub> q"
+ using carrier_polynomial[OF assms(1)]
+ unfolding factor_def univ_poly_carrier univ_poly_mult by auto
+ with \<open>q \<noteq> []\<close> have "degree p \<le> degree q"
+ using pdivides_imp_degree_le[OF assms(1) p q] unfolding pdivides_def by simp
+ with \<open>q \<noteq> []\<close> show ?thesis
+ by (cases "p = []", auto simp add: Suc_leI le_diff_iff)
+ qed
+ } note aux_lemma = this
+
+ interpret UP: domain "K[X]"
+ using univ_poly_is_domain[OF assms(1)] .
+
+ assume "p \<sim>\<^bsub>K[X]\<^esub> q" thus ?thesis
+ using aux_lemma[OF assms(2-3)] aux_lemma[OF assms(3,2) UP.associated_sym] by simp
+qed
+
+lemma (in ring) divides_pirreducible_condition:
+ assumes "pirreducible K q" and "p \<in> carrier (K[X])"
+ shows "p divides\<^bsub>K[X]\<^esub> q \<Longrightarrow> p \<in> Units (K[X]) \<or> p \<sim>\<^bsub>K[X]\<^esub> q"
+ using divides_irreducible_condition[of "K[X]" q p] assms
+ unfolding ring_irreducible_def by auto
+
+subsection \<open>Polynomial Power\<close>
+
+lemma (in domain) polynomial_pow_not_zero:
+ assumes "p \<in> carrier (poly_ring R)" and "p \<noteq> []"
+ shows "p [^]\<^bsub>poly_ring R\<^esub> (n::nat) \<noteq> []"
+proof -
+ interpret UP: domain "poly_ring R"
+ using univ_poly_is_domain[OF carrier_is_subring] .
+
+ from assms UP.integral show ?thesis
+ unfolding sym[OF univ_poly_zero[of R "carrier R"]]
+ by (induction n, auto)
+qed
+
+lemma (in domain) subring_polynomial_pow_not_zero:
+ assumes "subring K R" and "p \<in> carrier (K[X])" and "p \<noteq> []"
+ shows "p [^]\<^bsub>K[X]\<^esub> (n::nat) \<noteq> []"
+ using domain.polynomial_pow_not_zero[OF subring_is_domain, of K p n] assms
+ unfolding univ_poly_consistent[OF assms(1)] by simp
+
+lemma (in domain) polynomial_pow_degree:
+ assumes "p \<in> carrier (poly_ring R)"
+ shows "degree (p [^]\<^bsub>poly_ring R\<^esub> n) = n * degree p"
+proof -
+ interpret UP: domain "poly_ring R"
+ using univ_poly_is_domain[OF carrier_is_subring] .
+
+ show ?thesis
+ proof (induction n)
+ case 0 thus ?case
+ using UP.nat_pow_0 unfolding univ_poly_one by auto
+ next
+ let ?ppow = "\<lambda>n. p [^]\<^bsub>poly_ring R\<^esub> n"
+ case (Suc n) thus ?case
+ proof (cases "p = []")
+ case True thus ?thesis
+ using univ_poly_zero[of R "carrier R"] UP.r_null assms by auto
+ next
+ case False
+ hence "?ppow n \<in> carrier (poly_ring R)" and "?ppow n \<noteq> []" and "p \<noteq> []"
+ using polynomial_pow_not_zero[of p n] assms by (auto simp add: univ_poly_one)
+ thus ?thesis
+ using poly_mult_degree_eq[OF carrier_is_subring, of "?ppow n" p] Suc assms
+ unfolding univ_poly_carrier univ_poly_zero
+ by (auto simp add: add.commute univ_poly_mult)
+ qed
+ qed
+qed
+
+lemma (in domain) subring_polynomial_pow_degree:
+ assumes "subring K R" and "p \<in> carrier (K[X])"
+ shows "degree (p [^]\<^bsub>K[X]\<^esub> n) = n * degree p"
+ using domain.polynomial_pow_degree[OF subring_is_domain, of K p n] assms
+ unfolding univ_poly_consistent[OF assms(1)] by simp
+
+lemma (in domain) polynomial_pow_division:
+ assumes "p \<in> carrier (poly_ring R)" and "(n::nat) \<le> m"
+ shows "(p [^]\<^bsub>poly_ring R\<^esub> n) pdivides (p [^]\<^bsub>poly_ring R\<^esub> m)"
+proof -
+ interpret UP: domain "poly_ring R"
+ using univ_poly_is_domain[OF carrier_is_subring] .
+
+ let ?ppow = "\<lambda>n. p [^]\<^bsub>poly_ring R\<^esub> n"
+
+ have "?ppow n \<otimes>\<^bsub>poly_ring R\<^esub> ?ppow k = ?ppow (n + k)" for k
+ using assms(1) by (simp add: UP.nat_pow_mult)
+ thus ?thesis
+ using dividesI[of "?ppow (m - n)" "poly_ring R" "?ppow m" "?ppow n"] assms
+ unfolding pdivides_def by auto
+qed
+
+lemma (in domain) subring_polynomial_pow_division:
+ assumes "subring K R" and "p \<in> carrier (K[X])" and "(n::nat) \<le> m"
+ shows "(p [^]\<^bsub>K[X]\<^esub> n) divides\<^bsub>K[X]\<^esub> (p [^]\<^bsub>K[X]\<^esub> m)"
+ using domain.polynomial_pow_division[OF subring_is_domain, of K p n m] assms
+ unfolding univ_poly_consistent[OF assms(1)] pdivides_def by simp
+lemma (in domain) pirreducible_pow_pdivides_iff:
+ assumes "subfield K R" "p \<in> carrier (K[X])" "q \<in> carrier (K[X])" "r \<in> carrier (K[X])"
+ and "pirreducible K p" and "\<not> (p pdivides q)"
+ shows "(p [^]\<^bsub>K[X]\<^esub> (n :: nat)) pdivides (q \<otimes>\<^bsub>K[X]\<^esub> r) \<longleftrightarrow> (p [^]\<^bsub>K[X]\<^esub> n) pdivides r"
+proof -
+ interpret UP: principal_domain "K[X]"
+ using univ_poly_is_principal[OF assms(1)] .
+ show ?thesis
+ proof (cases "r = []")
+ case True with \<open>q \<in> carrier (K[X])\<close> have "q \<otimes>\<^bsub>K[X]\<^esub> r = []" and "r = []"
+ unfolding sym[OF univ_poly_zero[of R K]] by auto
+ thus ?thesis
+ using pdivides_zero[OF subfieldE(1),of K] assms by auto
+ next
+ case False then have not_zero: "p \<noteq> []" "q \<noteq> []" "r \<noteq> []" "q \<otimes>\<^bsub>K[X]\<^esub> r \<noteq> []"
+ using subfieldE(1) pdivides_zero[OF _ assms(2)] assms(1-2,5-6) pirreducibleE(1)
+ UP.integral_iff[OF assms(3-4)] univ_poly_zero[of R K] by auto
+ from \<open>p \<noteq> []\<close>
+ have ppow: "p [^]\<^bsub>K[X]\<^esub> (n :: nat) \<noteq> []" "p [^]\<^bsub>K[X]\<^esub> (n :: nat) \<in> carrier (K[X])"
+ using subring_polynomial_pow_not_zero[OF subfieldE(1)] assms(1-2) by auto
+ have not_pdiv: "\<not> (p divides\<^bsub>mult_of (K[X])\<^esub> q)"
+ using assms(6) pdivides_iff_shell[OF assms(1-3)] unfolding pdivides_def by auto
+ have prime: "prime (mult_of (K[X])) p"
+ using assms(5) pprime_iff_pirreducible[OF assms(1-2)]
+ unfolding sym[OF UP.prime_eq_prime_mult[OF assms(2)]] ring_prime_def by simp
+ have "a pdivides b \<longleftrightarrow> a divides\<^bsub>mult_of (K[X])\<^esub> b"
+ if "a \<in> carrier (K[X])" "a \<noteq> \<zero>\<^bsub>K[X]\<^esub>" "b \<in> carrier (K[X])" "b \<noteq> \<zero>\<^bsub>K[X]\<^esub>" for a b
+ using that UP.divides_imp_divides_mult[of a b] divides_mult_imp_divides[of "K[X]" a b]
+ unfolding pdivides_iff_shell[OF assms(1) that(1,3)] by blast
+ thus ?thesis
+ using UP.mult_of.prime_pow_divides_iff[OF _ _ _ prime not_pdiv, of r] ppow not_zero assms(2-4)
+ unfolding nat_pow_mult_of carrier_mult_of mult_mult_of sym[OF univ_poly_zero[of R K]]
+ by (metis DiffI UP.m_closed singletonD)
+ qed
+qed
+
+lemma (in domain) subring_degree_one_imp_pirreducible:
+ assumes "subring K R" and "a \<in> Units (R \<lparr> carrier := K \<rparr>)" and "b \<in> K"
+ shows "pirreducible K [ a, b ]"
+proof (rule pirreducibleI[OF assms(1)])
+ have "a \<in> K" and "a \<noteq> \<zero>"
+ using assms(2) subringE(1)[OF assms(1)] unfolding Units_def by auto
+ thus "[ a, b ] \<in> carrier (K[X])" and "[ a, b ] \<noteq> []" and "[ a, b ] \<notin> Units (K [X])"
+ using univ_poly_units_incl[OF assms(1)] assms(2-3)
+ unfolding sym[OF univ_poly_carrier] polynomial_def by auto
+next
+ interpret UP: domain "K[X]"
+ using univ_poly_is_domain[OF assms(1)] .
+
+ { fix q r
+ assume q: "q \<in> carrier (K[X])" and r: "r \<in> carrier (K[X])" and "[ a, b ] = q \<otimes>\<^bsub>K[X]\<^esub> r"
+ hence not_zero: "q \<noteq> []" "r \<noteq> []"
+ by (metis UP.integral_iff list.distinct(1) univ_poly_zero)+
+ have "degree (q \<otimes>\<^bsub>K[X]\<^esub> r) = degree q + degree r"
+ using not_zero poly_mult_degree_eq[OF assms(1)] q r
+ by (simp add: univ_poly_carrier univ_poly_mult)
+ with sym[OF \<open>[ a, b ] = q \<otimes>\<^bsub>K[X]\<^esub> r\<close>] have "degree q + degree r = 1" and "q \<noteq> []" "r \<noteq> []"
+ using not_zero by auto
+ } note aux_lemma1 = this
+
+ { fix q r
+ assume q: "q \<in> carrier (K[X])" "q \<noteq> []" and r: "r \<in> carrier (K[X])" "r \<noteq> []"
+ and "[ a, b ] = q \<otimes>\<^bsub>K[X]\<^esub> r" and "degree q = 1" and "degree r = 0"
+ hence "length q = Suc (Suc 0)" and "length r = Suc 0"
+ by (linarith, metis add.right_neutral add_eq_if length_0_conv)
+ from \<open>length q = Suc (Suc 0)\<close> obtain c d where q_def: "q = [ c, d ]"
+ by (metis length_0_conv length_Cons list.exhaust nat.inject)
+ from \<open>length r = Suc 0\<close> obtain e where r_def: "r = [ e ]"
+ by (metis length_0_conv length_Suc_conv)
+ from \<open>r = [ e ]\<close> and \<open>q = [ c, d ]\<close>
+ have c: "c \<in> K" "c \<noteq> \<zero>" and d: "d \<in> K" and e: "e \<in> K" "e \<noteq> \<zero>"
+ using r q subringE(1)[OF assms(1)] unfolding sym[OF univ_poly_carrier] polynomial_def by auto
+ with sym[OF \<open>[ a, b ] = q \<otimes>\<^bsub>K[X]\<^esub> r\<close>] have "a = c \<otimes> e"
+ using poly_mult_lead_coeff[OF assms(1), of q r]
+ unfolding polynomial_def sym[OF univ_poly_mult[of R K]] r_def q_def by auto
+ obtain inv_a where a: "a \<in> K" and inv_a: "inv_a \<in> K" "a \<otimes> inv_a = \<one>" "inv_a \<otimes> a = \<one>"
+ using assms(2) unfolding Units_def by auto
+ hence "a \<noteq> \<zero>" and "inv_a \<noteq> \<zero>"
+ using subringE(1)[OF assms(1)] integral_iff by auto
+ with \<open>c \<in> K\<close> and \<open>c \<noteq> \<zero>\<close> have in_carrier: "[ c \<otimes> inv_a ] \<in> carrier (K[X])"
+ using subringE(1,6)[OF assms(1)] inv_a integral
+ unfolding sym[OF univ_poly_carrier] polynomial_def
+ by (auto, meson subsetD)
+ moreover have "[ c \<otimes> inv_a ] \<otimes>\<^bsub>K[X]\<^esub> r = [ \<one> ]"
+ using \<open>a = c \<otimes> e\<close> a inv_a c e subsetD[OF subringE(1)[OF assms(1)]]
+ unfolding r_def univ_poly_mult by (auto) (simp add: m_assoc m_lcomm integral_iff)+
+ ultimately have "r \<in> Units (K[X])"
+ using r(1) UP.m_comm[OF in_carrier r(1)] unfolding sym[OF univ_poly_one[of R K]] Units_def by auto
+ } note aux_lemma2 = this
+
+ fix q r
+ assume q: "q \<in> carrier (K[X])" and r: "r \<in> carrier (K[X])" and qr: "[ a, b ] = q \<otimes>\<^bsub>K[X]\<^esub> r"
+ thus "q \<in> Units (K[X]) \<or> r \<in> Units (K[X])"
+ using aux_lemma1[OF q r qr] aux_lemma2[of q r] aux_lemma2[of r q] UP.m_comm add_is_1 by auto
+qed
+
+lemma (in domain) degree_one_imp_pirreducible:
+ assumes "subfield K R" and "p \<in> carrier (K[X])" and "degree p = 1"
+ shows "pirreducible K p"
+proof -
+ from \<open>degree p = 1\<close> have "length p = Suc (Suc 0)"
+ by simp
+ then obtain a b where p: "p = [ a, b ]"
+ by (metis length_0_conv length_Suc_conv)
+ with \<open>p \<in> carrier (K[X])\<close> show ?thesis
+ using subring_degree_one_imp_pirreducible[OF subfieldE(1)[OF assms(1)], of a b]
+ subfield.subfield_Units[OF assms(1)]
+ unfolding sym[OF univ_poly_carrier] polynomial_def by auto
+qed
+
+lemma (in ring) degree_oneE[elim]:
+ assumes "p \<in> carrier (K[X])" and "degree p = 1"
+ and "\<And>a b. \<lbrakk> a \<in> K; a \<noteq> \<zero>; b \<in> K; p = [ a, b ] \<rbrakk> \<Longrightarrow> P"
+ shows P
+proof -
+ from \<open>degree p = 1\<close> have "length p = Suc (Suc 0)"
+ by simp
+ then obtain a b where "p = [ a, b ]"
+ by (metis length_0_conv length_Cons nat.inject neq_Nil_conv)
+ with \<open>p \<in> carrier (K[X])\<close> have "a \<in> K" and "a \<noteq> \<zero>" and "b \<in> K"
+ unfolding sym[OF univ_poly_carrier] polynomial_def by auto
+ with \<open>p = [ a, b ]\<close> show ?thesis
+ using assms(3) by simp
+qed
+
+lemma (in domain) subring_degree_one_associatedI:
+ assumes "subring K R" and "a \<in> K" "a' \<in> K" and "b \<in> K" and "a \<otimes> a' = \<one>"
+ shows "[ a , b ] \<sim>\<^bsub>K[X]\<^esub> [ \<one>, a' \<otimes> b ]"
+proof -
+ from \<open>a \<otimes> a' = \<one>\<close> have not_zero: "a \<noteq> \<zero>" "a' \<noteq> \<zero>"
+ using subringE(1)[OF assms(1)] assms(2-3) by auto
+ hence "[ a, b ] = [ a ] \<otimes>\<^bsub>K[X]\<^esub> [ \<one>, a' \<otimes> b ]"
+ using assms(2-4)[THEN subsetD[OF subringE(1)[OF assms(1)]]] assms(5) m_assoc
+ unfolding univ_poly_mult by fastforce
+ moreover have "[ a, b ] \<in> carrier (K[X])" and "[ \<one>, a' \<otimes> b ] \<in> carrier (K[X])"
+ using subringE(1,3,6)[OF assms(1)] not_zero one_not_zero assms
+ unfolding sym[OF univ_poly_carrier] polynomial_def by auto
+ moreover have "[ a ] \<in> Units (K[X])"
+ proof -
+ from \<open>a \<noteq> \<zero>\<close> and \<open>a' \<noteq> \<zero>\<close> have "[ a ] \<in> carrier (K[X])" and "[ a' ] \<in> carrier (K[X])"
+ using assms(2-3) unfolding sym[OF univ_poly_carrier] polynomial_def by auto
+ moreover have "a' \<otimes> a = \<one>"
+ using subsetD[OF subringE(1)[OF assms(1)]] assms m_comm by simp
+ hence "[ a ] \<otimes>\<^bsub>K[X]\<^esub> [ a' ] = [ \<one> ]" and "[ a' ] \<otimes>\<^bsub>K[X]\<^esub> [ a ] = [ \<one> ]"
+ using assms unfolding univ_poly_mult by auto
+ ultimately show ?thesis
+ unfolding sym[OF univ_poly_one[of R K]] Units_def by blast
+ qed
+ ultimately show ?thesis
+ using domain.ring_associated_iff[OF univ_poly_is_domain[OF assms(1)]] by blast
+qed
+
+lemma (in domain) degree_one_associatedI:
+ assumes "subfield K R" and "p \<in> carrier (K[X])" and "degree p = 1"
+ shows "p \<sim>\<^bsub>K[X]\<^esub> [ \<one>, inv (lead_coeff p) \<otimes> (const_term p) ]"
+proof -
+ from \<open>p \<in> carrier (K[X])\<close> and \<open>degree p = 1\<close>
+ obtain a b where "p = [ a, b ]" and "a \<in> K" "a \<noteq> \<zero>" and "b \<in> K"
+ by auto
+ thus ?thesis
+ using subring_degree_one_associatedI[OF subfieldE(1)[OF assms(1)]]
+ subfield_m_inv[OF assms(1)] subsetD[OF subfieldE(3)[OF assms(1)]]
+ unfolding const_term_def
+ by auto
+qed
subsection \<open>Ideals\<close>
@@ -772,6 +1051,8 @@
have "\<And>r. \<lbrakk> r \<in> carrier (K[X]); lead_coeff r = \<one>; I = PIdl\<^bsub>K[X]\<^esub> r \<rbrakk> \<Longrightarrow> r = p"
proof -
fix r assume r: "r \<in> carrier (K[X])" "lead_coeff r = \<one>" "I = PIdl\<^bsub>K[X]\<^esub> r"
+ have "subring K R"
+ by (simp add: \<open>subfield K R\<close> subfieldE(1))
obtain k where k: "k \<in> K - { \<zero> }" "r = [ k ] \<otimes>\<^bsub>K[X]\<^esub> p"
using UP.associated_iff_same_ideal[OF r(1) in_carrier] PIdl_p r(3)
associated_polynomials_iff[OF assms(1) r(1) in_carrier]
@@ -780,7 +1061,7 @@
unfolding polynomial_def by simp
moreover have "p \<noteq> []"
using not_nil UP.associated_iff_same_ideal[OF in_carrier q(1)] q(2) PIdl_p
- associated_polynomials_imp_same_length[OF assms(1) in_carrier q(1)] by auto
+ associated_polynomials_imp_same_length[OF \<open>subring K R\<close> in_carrier q(1)] by auto
ultimately have "lead_coeff r = k \<otimes> (lead_coeff p)"
using poly_mult_lead_coeff[OF subfieldE(1)[OF assms(1)]] in_carrier k(2)
unfolding univ_poly_def by (auto simp del: poly_mult.simps)
@@ -855,6 +1136,26 @@
subsection \<open>Roots and Multiplicity\<close>
+definition (in ring) is_root :: "'a list \<Rightarrow> 'a \<Rightarrow> bool"
+ where "is_root p x \<longleftrightarrow> (x \<in> carrier R \<and> eval p x = \<zero> \<and> p \<noteq> [])"
+
+definition (in ring) alg_mult :: "'a list \<Rightarrow> 'a \<Rightarrow> nat"
+ where "alg_mult p x =
+ (if p = [] then 0 else
+ (if x \<in> carrier R then Greatest (\<lambda> n. ([ \<one>, \<ominus> x ] [^]\<^bsub>poly_ring R\<^esub> n) pdivides p) else 0))"
+
+definition (in ring) roots :: "'a list \<Rightarrow> 'a multiset"
+ where "roots p = Abs_multiset (alg_mult p)"
+
+definition (in ring) roots_on :: "'a set \<Rightarrow> 'a list \<Rightarrow> 'a multiset"
+ where "roots_on K p = roots p \<inter># mset_set K"
+
+definition (in ring) splitted :: "'a list \<Rightarrow> bool"
+ where "splitted p \<longleftrightarrow> size (roots p) = degree p"
+
+definition (in ring) splitted_on :: "'a set \<Rightarrow> 'a list \<Rightarrow> bool"
+ where "splitted_on K p \<longleftrightarrow> size (roots_on K p) = degree p"
+
lemma (in domain) pdivides_imp_root_sharing:
assumes "p \<in> carrier (poly_ring R)" "p pdivides q" and "a \<in> carrier R"
shows "eval p a = \<zero> \<Longrightarrow> eval q a = \<zero>"
@@ -895,6 +1196,782 @@
show "inv (lead_coeff p) \<otimes> (const_term p) \<in> K"
using p subringE(6)[OF subfieldE(1)[OF assms(1)]] unfolding ct by auto
qed
+lemma (in domain) is_root_imp_pdivides:
+ assumes "p \<in> carrier (poly_ring R)"
+ shows "is_root p x \<Longrightarrow> [ \<one>, \<ominus> x ] pdivides p"
+proof -
+ let ?b = "[ \<one> , \<ominus> x ]"
+
+ interpret UP: domain "poly_ring R"
+ using univ_poly_is_domain[OF carrier_is_subring] .
+
+ assume "is_root p x" hence x: "x \<in> carrier R" and is_root: "eval p x = \<zero>"
+ unfolding is_root_def by auto
+ hence b: "?b \<in> carrier (poly_ring R)"
+ unfolding sym[OF univ_poly_carrier] polynomial_def by auto
+ then obtain q r where q: "q \<in> carrier (poly_ring R)" and r: "r \<in> carrier (poly_ring R)"
+ and long_divides: "p = (?b \<otimes>\<^bsub>poly_ring R\<^esub> q) \<oplus>\<^bsub>poly_ring R\<^esub> r" "r = [] \<or> degree r < degree ?b"
+ using long_division_theorem[OF carrier_is_subring, of p ?b] assms by (auto simp add: univ_poly_carrier)
+
+ show ?thesis
+ proof (cases "r = []")
+ case True then have "r = \<zero>\<^bsub>poly_ring R\<^esub>"
+ unfolding univ_poly_zero[of R "carrier R"] .
+ thus ?thesis
+ using long_divides(1) q r b dividesI[OF q, of p ?b] by (simp add: pdivides_def)
+ next
+ case False then have "length r = Suc 0"
+ using long_divides(2) le_SucE by fastforce
+ then obtain a where "r = [ a ]" and a: "a \<in> carrier R" and "a \<noteq> \<zero>"
+ using r unfolding sym[OF univ_poly_carrier] polynomial_def
+ by (metis False length_0_conv length_Suc_conv list.sel(1) list.set_sel(1) subset_code(1))
+
+ have "eval p x = ((eval ?b x) \<otimes> (eval q x)) \<oplus> (eval r x)"
+ using long_divides(1) ring_hom_memE[OF eval_is_hom[OF carrier_is_subring x]] by (simp add: b q r)
+ also have " ... = eval r x"
+ using ring_hom_memE[OF eval_is_hom[OF carrier_is_subring x]] x b q r by (auto, algebra)
+ finally have "a = \<zero>"
+ using a unfolding \<open>r = [ a ]\<close> is_root by simp
+ with \<open>a \<noteq> \<zero>\<close> have False .. thus ?thesis ..
+ qed
+qed
+
+lemma (in domain) pdivides_imp_is_root:
+ assumes "p \<noteq> []" and "x \<in> carrier R"
+ shows "[ \<one>, \<ominus> x ] pdivides p \<Longrightarrow> is_root p x"
+proof -
+ assume "[ \<one>, \<ominus> x ] pdivides p"
+ then obtain q where q: "q \<in> carrier (poly_ring R)" and pdiv: "p = [ \<one>, \<ominus> x ] \<otimes>\<^bsub>poly_ring R\<^esub> q"
+ unfolding pdivides_def by auto
+ moreover have "[ \<one>, \<ominus> x ] \<in> carrier (poly_ring R)"
+ using assms(2) unfolding sym[OF univ_poly_carrier] polynomial_def by simp
+ ultimately have "eval p x = \<zero>"
+ using ring_hom_memE[OF eval_is_hom[OF carrier_is_subring, of x]] assms(2) by (auto, algebra)
+ with \<open>p \<noteq> []\<close> and \<open>x \<in> carrier R\<close> show "is_root p x"
+ unfolding is_root_def by simp
+qed
+
+lemma (in domain) associated_polynomials_imp_same_is_root:
+ assumes "p \<in> carrier (poly_ring R)" and "q \<in> carrier (poly_ring R)" and "p \<sim>\<^bsub>poly_ring R\<^esub> q"
+ shows "is_root p x \<longleftrightarrow> is_root q x"
+proof (cases "p = []")
+ case True with \<open>p \<sim>\<^bsub>poly_ring R\<^esub> q\<close> have "q = []"
+ unfolding associated_def True factor_def univ_poly_def by auto
+ thus ?thesis
+ using True unfolding is_root_def by simp
+next
+ case False
+ interpret UP: domain "poly_ring R"
+ using univ_poly_is_domain[OF carrier_is_subring] .
+
+ { fix p q
+ assume p: "p \<in> carrier (poly_ring R)" and q: "q \<in> carrier (poly_ring R)" and pq: "p \<sim>\<^bsub>poly_ring R\<^esub> q"
+ have "is_root p x \<Longrightarrow> is_root q x"
+ proof -
+ assume is_root: "is_root p x"
+ then have "[ \<one>, \<ominus> x ] pdivides p" and "p \<noteq> []" and "x \<in> carrier R"
+ using is_root_imp_pdivides[OF p] unfolding is_root_def by auto
+ moreover have "[ \<one>, \<ominus> x ] \<in> carrier (poly_ring R)"
+ using is_root unfolding is_root_def sym[OF univ_poly_carrier] polynomial_def by simp
+ ultimately have "[ \<one>, \<ominus> x ] pdivides q"
+ using UP.divides_cong_r[OF _ pq ] unfolding pdivides_def by simp
+ with \<open>p \<noteq> []\<close> and \<open>x \<in> carrier R\<close> show ?thesis
+ using associated_polynomials_imp_same_length[OF carrier_is_subring p q pq]
+ pdivides_imp_is_root[of q x]
+ by fastforce
+ qed
+ }
+
+ then show ?thesis
+ using assms UP.associated_sym[OF assms(3)] by blast
+qed
+
+lemma (in ring) monic_degree_one_root_condition:
+ assumes "a \<in> carrier R" shows "is_root [ \<one>, \<ominus> a ] b \<longleftrightarrow> a = b"
+ using assms minus_equality r_neg[OF assms] unfolding is_root_def by (auto, fastforce)
+
+lemma (in field) degree_one_root_condition:
+ assumes "p \<in> carrier (poly_ring R)" and "degree p = 1"
+ shows "is_root p x \<longleftrightarrow> x = \<ominus> (inv (lead_coeff p) \<otimes> (const_term p))"
+proof -
+ interpret UP: domain "poly_ring R"
+ using univ_poly_is_domain[OF carrier_is_subring] .
+
+ from \<open>degree p = 1\<close> have "length p = Suc (Suc 0)"
+ by simp
+ then obtain a b where p: "p = [ a, b ]"
+ by (metis length_0_conv length_Cons list.exhaust nat.inject)
+ hence a: "a \<in> carrier R" "a \<noteq> \<zero>" and b: "b \<in> carrier R"
+ using assms(1) unfolding sym[OF univ_poly_carrier] polynomial_def by auto
+ hence inv_a: "inv a \<in> carrier R" "(inv a) \<otimes> a = \<one>"
+ using subfield_m_inv[OF carrier_is_subfield, of a] by auto
+ hence in_carrier: "[ \<one>, (inv a) \<otimes> b ] \<in> carrier (poly_ring R)"
+ using b unfolding sym[OF univ_poly_carrier] polynomial_def by auto
+
+ have "p \<sim>\<^bsub>poly_ring R\<^esub> [ \<one>, (inv a) \<otimes> b ]"
+ proof (rule UP.associatedI2'[OF _ _ in_carrier, of _ "[ a ]"])
+ have "p = [ a ] \<otimes>\<^bsub>poly_ring R\<^esub> [ \<one>, inv a \<otimes> b ]"
+ using a inv_a b m_assoc[of a "inv a" b] unfolding p univ_poly_mult by (auto, algebra)
+ also have " ... = [ \<one>, inv a \<otimes> b ] \<otimes>\<^bsub>poly_ring R\<^esub> [ a ]"
+ using UP.m_comm[OF in_carrier, of "[ a ]"] a
+ by (auto simp add: sym[OF univ_poly_carrier] polynomial_def)
+ finally show "p = [ \<one>, inv a \<otimes> b ] \<otimes>\<^bsub>poly_ring R\<^esub> [ a ]" .
+ next
+ from \<open>a \<in> carrier R\<close> and \<open>a \<noteq> \<zero>\<close> show "[ a ] \<in> Units (poly_ring R)"
+ unfolding univ_poly_units[OF carrier_is_subfield] by simp
+ qed
+
+ moreover have "(inv a) \<otimes> b = \<ominus> (\<ominus> (inv (lead_coeff p) \<otimes> (const_term p)))"
+ and "inv (lead_coeff p) \<otimes> (const_term p) \<in> carrier R"
+ using inv_a a b unfolding p const_term_def by auto
+
+ ultimately show ?thesis
+ using associated_polynomials_imp_same_is_root[OF assms(1) in_carrier]
+ monic_degree_one_root_condition
+ by (metis add.inv_closed)
+qed
+
+lemma (in domain) is_root_poly_mult_imp_is_root:
+ assumes "p \<in> carrier (poly_ring R)" and "q \<in> carrier (poly_ring R)"
+ shows "is_root (p \<otimes>\<^bsub>poly_ring R\<^esub> q) x \<Longrightarrow> (is_root p x) \<or> (is_root q x)"
+proof -
+ interpret UP: domain "poly_ring R"
+ using univ_poly_is_domain[OF carrier_is_subring] .
+
+ assume is_root: "is_root (p \<otimes>\<^bsub>poly_ring R\<^esub> q) x"
+ hence "p \<noteq> []" and "q \<noteq> []"
+ unfolding is_root_def sym[OF univ_poly_zero[of R "carrier R"]]
+ using UP.l_null[OF assms(2)] UP.r_null[OF assms(1)] by blast+
+ moreover have x: "x \<in> carrier R" and "eval (p \<otimes>\<^bsub>poly_ring R\<^esub> q) x = \<zero>"
+ using is_root unfolding is_root_def by simp+
+ hence "eval p x = \<zero> \<or> eval q x = \<zero>"
+ using ring_hom_memE[OF eval_is_hom[OF carrier_is_subring], of x] assms integral by auto
+ ultimately show "(is_root p x) \<or> (is_root q x)"
+ using x unfolding is_root_def by auto
+qed
+
+lemma (in domain) degree_zero_imp_not_is_root:
+ assumes "p \<in> carrier (poly_ring R)" and "degree p = 0" shows "\<not> is_root p x"
+proof (cases "p = []", simp add: is_root_def)
+ case False with \<open>degree p = 0\<close> have "length p = Suc 0"
+ using le_SucE by fastforce
+ then obtain a where "p = [ a ]" and "a \<in> carrier R" and "a \<noteq> \<zero>"
+ using assms unfolding sym[OF univ_poly_carrier] polynomial_def
+ by (metis False length_0_conv length_Suc_conv list.sel(1) list.set_sel(1) subset_code(1))
+ thus ?thesis
+ unfolding is_root_def by auto
+qed
+
+lemma (in domain) finite_number_of_roots:
+ assumes "p \<in> carrier (poly_ring R)" shows "finite { x. is_root p x }"
+ using assms
+proof (induction "degree p" arbitrary: p)
+ case 0 thus ?case
+ by (simp add: degree_zero_imp_not_is_root)
+next
+ case (Suc n) show ?case
+ proof (cases "{ x. is_root p x } = {}")
+ case True thus ?thesis
+ by (simp add: True)
+ next
+ interpret UP: domain "poly_ring R"
+ using univ_poly_is_domain[OF carrier_is_subring] .
+
+ case False
+ then obtain a where is_root: "is_root p a"
+ by blast
+ hence a: "a \<in> carrier R" and eval: "eval p a = \<zero>" and p_not_zero: "p \<noteq> []"
+ unfolding is_root_def by auto
+ hence in_carrier: "[ \<one>, \<ominus> a ] \<in> carrier (poly_ring R)"
+ unfolding sym[OF univ_poly_carrier] polynomial_def by auto
+
+ obtain q where q: "q \<in> carrier (poly_ring R)" and p: "p = [ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> q"
+ using is_root_imp_pdivides[OF Suc(3) is_root] unfolding pdivides_def by auto
+ with \<open>p \<noteq> []\<close> have q_not_zero: "q \<noteq> []"
+ using UP.r_null UP.integral in_carrier unfolding sym[OF univ_poly_zero[of R "carrier R"]]
+ by metis
+ hence "degree q = n"
+ using poly_mult_degree_eq[OF carrier_is_subring, of "[ \<one>, \<ominus> a ]" q]
+ in_carrier q p_not_zero p Suc(2)
+ unfolding univ_poly_carrier
+ by (metis One_nat_def Suc_eq_plus1 diff_Suc_1 list.distinct(1)
+ list.size(3-4) plus_1_eq_Suc univ_poly_mult)
+ hence "finite { x. is_root q x }"
+ using Suc(1)[OF _ q] by simp
+
+ moreover have "{ x. is_root p x } \<subseteq> insert a { x. is_root q x }"
+ using is_root_poly_mult_imp_is_root[OF in_carrier q]
+ monic_degree_one_root_condition[OF a]
+ unfolding p by auto
+
+ ultimately show ?thesis
+ using finite_subset by auto
+ qed
+qed
+
+lemma (in domain) alg_multE:
+ assumes "x \<in> carrier R" and "p \<in> carrier (poly_ring R)" and "p \<noteq> []"
+ shows "([ \<one>, \<ominus> x ] [^]\<^bsub>poly_ring R\<^esub> (alg_mult p x)) pdivides p"
+ and "\<And>n. ([ \<one>, \<ominus> x ] [^]\<^bsub>poly_ring R\<^esub> n) pdivides p \<Longrightarrow> n \<le> alg_mult p x"
+proof -
+ interpret UP: domain "poly_ring R"
+ using univ_poly_is_domain[OF carrier_is_subring] .
+
+ let ?ppow = "\<lambda>n :: nat. ([ \<one>, \<ominus> x ] [^]\<^bsub>poly_ring R\<^esub> n)"
+
+ define S :: "nat set" where "S = { n. ?ppow n pdivides p }"
+ have "?ppow 0 = \<one>\<^bsub>poly_ring R\<^esub>"
+ using UP.nat_pow_0 by simp
+ hence "0 \<in> S"
+ using UP.one_divides[OF assms(2)] unfolding S_def pdivides_def by simp
+ hence "S \<noteq> {}"
+ by auto
+
+ moreover have "n \<le> degree p" if "n \<in> S" for n :: nat
+ proof -
+ have "[ \<one>, \<ominus> x ] \<in> carrier (poly_ring R)"
+ using assms unfolding sym[OF univ_poly_carrier] polynomial_def by auto
+ hence "?ppow n \<in> carrier (poly_ring R)"
+ using assms unfolding univ_poly_zero by auto
+ with \<open>n \<in> S\<close> have "degree (?ppow n) \<le> degree p"
+ using pdivides_imp_degree_le[OF carrier_is_subring _ assms(2-3), of "?ppow n"] by (simp add: S_def)
+ with \<open>[ \<one>, \<ominus> x ] \<in> carrier (poly_ring R)\<close> show ?thesis
+ using polynomial_pow_degree by simp
+ qed
+ hence "finite S"
+ using finite_nat_set_iff_bounded_le by blast
+
+ ultimately have MaxS: "\<And>n. n \<in> S \<Longrightarrow> n \<le> Max S" "Max S \<in> S"
+ using Max_ge[of S] Max_in[of S] by auto
+ with \<open>x \<in> carrier R\<close> have "alg_mult p x = Max S"
+ using Greatest_equality[of "\<lambda>n. ?ppow n pdivides p" "Max S"] assms(3)
+ unfolding S_def alg_mult_def by auto
+ thus "([ \<one>, \<ominus> x ] [^]\<^bsub>poly_ring R\<^esub> (alg_mult p x)) pdivides p"
+ and "\<And>n. ([ \<one>, \<ominus> x ] [^]\<^bsub>poly_ring R\<^esub> n) pdivides p \<Longrightarrow> n \<le> alg_mult p x"
+ using MaxS unfolding S_def by auto
+qed
+
+lemma (in domain) le_alg_mult_imp_pdivides:
+ assumes "x \<in> carrier R" and "p \<in> carrier (poly_ring R)"
+ shows "n \<le> alg_mult p x \<Longrightarrow> ([ \<one>, \<ominus> x ] [^]\<^bsub>poly_ring R\<^esub> n) pdivides p"
+proof -
+ interpret UP: domain "poly_ring R"
+ using univ_poly_is_domain[OF carrier_is_subring] .
+
+ assume le_alg_mult: "n \<le> alg_mult p x"
+ have in_carrier: "[ \<one>, \<ominus> x ] \<in> carrier (poly_ring R)"
+ using assms(1) unfolding sym[OF univ_poly_carrier] polynomial_def by auto
+ hence ppow_pdivides:
+ "([ \<one>, \<ominus> x ] [^]\<^bsub>poly_ring R\<^esub> n) pdivides
+ ([ \<one>, \<ominus> x ] [^]\<^bsub>poly_ring R\<^esub> (alg_mult p x))"
+ using polynomial_pow_division[OF _ le_alg_mult] by simp
+
+ show ?thesis
+ proof (cases "p = []")
+ case True thus ?thesis
+ using in_carrier pdivides_zero[OF carrier_is_subring] by auto
+ next
+ case False thus ?thesis
+ using ppow_pdivides UP.divides_trans UP.nat_pow_closed alg_multE(1)[OF assms] in_carrier
+ unfolding pdivides_def by meson
+ qed
+qed
+
+lemma (in domain) alg_mult_gt_zero_iff_is_root:
+ assumes "p \<in> carrier (poly_ring R)" shows "alg_mult p x > 0 \<longleftrightarrow> is_root p x"
+proof -
+ interpret UP: domain "poly_ring R"
+ using univ_poly_is_domain[OF carrier_is_subring] .
+ show ?thesis
+ proof
+ assume is_root: "is_root p x" hence x: "x \<in> carrier R" and not_zero: "p \<noteq> []"
+ unfolding is_root_def by auto
+ have "[\<one>, \<ominus> x] [^]\<^bsub>poly_ring R\<^esub> (Suc 0) = [\<one>, \<ominus> x]"
+ using x unfolding univ_poly_def by auto
+ thus "alg_mult p x > 0"
+ using is_root_imp_pdivides[OF _ is_root] alg_multE(2)[OF x, of p "Suc 0"] not_zero assms by auto
+ next
+ assume gt_zero: "alg_mult p x > 0"
+ hence x: "x \<in> carrier R" and not_zero: "p \<noteq> []"
+ unfolding alg_mult_def by (cases "p = []", auto, cases "x \<in> carrier R", auto)
+ hence in_carrier: "[ \<one>, \<ominus> x ] \<in> carrier (poly_ring R)"
+ unfolding sym[OF univ_poly_carrier] polynomial_def by auto
+ with \<open>x \<in> carrier R\<close> have "[ \<one>, \<ominus> x ] pdivides p" and "eval [ \<one>, \<ominus> x ] x = \<zero>"
+ using le_alg_mult_imp_pdivides[of x p "1::nat"] gt_zero assms by (auto, algebra)
+ thus "is_root p x"
+ using pdivides_imp_root_sharing[OF in_carrier] not_zero x by (simp add: is_root_def)
+ qed
+qed
+
+lemma (in domain) alg_mult_eq_count_roots:
+ assumes "p \<in> carrier (poly_ring R)" shows "alg_mult p = count (roots p)"
+ using finite_number_of_roots[OF assms]
+ unfolding sym[OF alg_mult_gt_zero_iff_is_root[OF assms]]
+ by (simp add: multiset_def roots_def)
+
+lemma (in domain) roots_mem_iff_is_root:
+ assumes "p \<in> carrier (poly_ring R)" shows "x \<in># roots p \<longleftrightarrow> is_root p x"
+ using alg_mult_eq_count_roots[OF assms] count_greater_zero_iff
+ unfolding roots_def sym[OF alg_mult_gt_zero_iff_is_root[OF assms]] by metis
+
+lemma (in domain) degree_zero_imp_empty_roots:
+ assumes "p \<in> carrier (poly_ring R)" and "degree p = 0" shows "roots p = {#}"
+ using degree_zero_imp_not_is_root[of p] roots_mem_iff_is_root[of p] assms by auto
+
+lemma (in domain) degree_zero_imp_splitted:
+ assumes "p \<in> carrier (poly_ring R)" and "degree p = 0" shows "splitted p"
+ unfolding splitted_def degree_zero_imp_empty_roots[OF assms] assms(2) by simp
+
+lemma (in domain) roots_inclI':
+ assumes "p \<in> carrier (poly_ring R)" and "\<And>a. \<lbrakk> a \<in> carrier R; p \<noteq> [] \<rbrakk> \<Longrightarrow> alg_mult p a \<le> count m a"
+ shows "roots p \<subseteq># m"
+proof (intro mset_subset_eqI)
+ fix a show "count (roots p) a \<le> count m a"
+ using assms unfolding sym[OF alg_mult_eq_count_roots[OF assms(1)]] alg_mult_def
+ by (cases "p = []", simp, cases "a \<in> carrier R", auto)
+qed
+
+lemma (in domain) roots_inclI:
+ assumes "p \<in> carrier (poly_ring R)" and "q \<in> carrier (poly_ring R)" "q \<noteq> []"
+ and "\<And>a. \<lbrakk> a \<in> carrier R; p \<noteq> [] \<rbrakk> \<Longrightarrow> ([ \<one>, \<ominus> a ] [^]\<^bsub>poly_ring R\<^esub> (alg_mult p a)) pdivides q"
+ shows "roots p \<subseteq># roots q"
+ using roots_inclI'[OF assms(1), of "roots q"] assms alg_multE(2)[OF _ assms(2-3)]
+ unfolding sym[OF alg_mult_eq_count_roots[OF assms(2)]] by auto
+
+lemma (in domain) pdivides_imp_roots_incl:
+ assumes "p \<in> carrier (poly_ring R)" and "q \<in> carrier (poly_ring R)" "q \<noteq> []"
+ shows "p pdivides q \<Longrightarrow> roots p \<subseteq># roots q"
+proof (rule roots_inclI[OF assms])
+ interpret UP: domain "poly_ring R"
+ using univ_poly_is_domain[OF carrier_is_subring] .
+
+ fix a assume "p pdivides q" and a: "a \<in> carrier R"
+ hence "[ \<one> , \<ominus> a ] \<in> carrier (poly_ring R)"
+ unfolding sym[OF univ_poly_carrier] polynomial_def by simp
+ with \<open>p pdivides q\<close> show "([\<one>, \<ominus> a] [^]\<^bsub>poly_ring R\<^esub> (alg_mult p a)) pdivides q"
+ using UP.divides_trans[of _p q] le_alg_mult_imp_pdivides[OF a assms(1)]
+ by (auto simp add: pdivides_def)
+qed
+
+lemma (in domain) associated_polynomials_imp_same_roots:
+ assumes "p \<in> carrier (poly_ring R)" and "q \<in> carrier (poly_ring R)" and "p \<sim>\<^bsub>poly_ring R\<^esub> q"
+ shows "roots p = roots q"
+ using assms pdivides_imp_roots_incl zero_pdivides
+ unfolding pdivides_def associated_def
+ by (metis subset_mset.eq_iff)
+
+lemma (in domain) monic_degree_one_roots:
+ assumes "a \<in> carrier R" shows "roots [ \<one> , \<ominus> a ] = {# a #}"
+proof -
+ let ?p = "[ \<one> , \<ominus> a ]"
+
+ interpret UP: domain "poly_ring R"
+ using univ_poly_is_domain[OF carrier_is_subring] .
+
+ from \<open>a \<in> carrier R\<close> have in_carrier: "?p \<in> carrier (poly_ring R)"
+ unfolding sym[OF univ_poly_carrier] polynomial_def by simp
+ show ?thesis
+ proof (rule subset_mset.antisym)
+ show "{# a #} \<subseteq># roots ?p"
+ using roots_mem_iff_is_root[OF in_carrier]
+ monic_degree_one_root_condition[OF assms]
+ by simp
+ next
+ show "roots ?p \<subseteq># {# a #}"
+ proof (rule mset_subset_eqI, auto)
+ fix b assume "a \<noteq> b" thus "count (roots ?p) b = 0"
+ using alg_mult_gt_zero_iff_is_root[OF in_carrier]
+ monic_degree_one_root_condition[OF assms]
+ unfolding sym[OF alg_mult_eq_count_roots[OF in_carrier]]
+ by fastforce
+ next
+ have "(?p [^]\<^bsub>poly_ring R\<^esub> (alg_mult ?p a)) pdivides ?p"
+ using le_alg_mult_imp_pdivides[OF assms in_carrier] by simp
+ hence "degree (?p [^]\<^bsub>poly_ring R\<^esub> (alg_mult ?p a)) \<le> degree ?p"
+ using pdivides_imp_degree_le[OF carrier_is_subring, of _ ?p] in_carrier by auto
+ thus "count (roots ?p) a \<le> Suc 0"
+ using polynomial_pow_degree[OF in_carrier]
+ unfolding sym[OF alg_mult_eq_count_roots[OF in_carrier]]
+ by auto
+ qed
+ qed
+qed
+
+lemma (in domain) degree_one_roots:
+ assumes "a \<in> carrier R" "a' \<in> carrier R" and "b \<in> carrier R" and "a \<otimes> a' = \<one>"
+ shows "roots [ a , b ] = {# \<ominus> (a' \<otimes> b) #}"
+proof -
+ have "[ a, b ] \<in> carrier (poly_ring R)" and "[ \<one>, a' \<otimes> b ] \<in> carrier (poly_ring R)"
+ using assms unfolding sym[OF univ_poly_carrier] polynomial_def by auto
+ thus ?thesis
+ using subring_degree_one_associatedI[OF carrier_is_subring assms] assms
+ monic_degree_one_roots associated_polynomials_imp_same_roots
+ by (metis add.inv_closed local.minus_minus m_closed)
+qed
+
+lemma (in field) degree_one_imp_singleton_roots:
+ assumes "p \<in> carrier (poly_ring R)" and "degree p = 1"
+ shows "roots p = {# \<ominus> (inv (lead_coeff p) \<otimes> (const_term p)) #}"
+proof -
+ from \<open>p \<in> carrier (poly_ring R)\<close> and \<open>degree p = 1\<close>
+ obtain a b where "p = [ a, b ]" and "a \<in> carrier R" "a \<noteq> \<zero>" and "b \<in> carrier R"
+ by auto
+ thus ?thesis
+ using degree_one_roots[of a "inv a" b]
+ by (auto simp add: const_term_def field_Units)
+qed
+
+lemma (in field) degree_one_imp_splitted:
+ assumes "p \<in> carrier (poly_ring R)" and "degree p = 1" shows "splitted p"
+ using degree_one_imp_singleton_roots[OF assms] assms(2) unfolding splitted_def by simp
+
+lemma (in field) no_roots_imp_same_roots:
+ assumes "p \<in> carrier (poly_ring R)" "p \<noteq> []" and "q \<in> carrier (poly_ring R)"
+ shows "roots p = {#} \<Longrightarrow> roots (p \<otimes>\<^bsub>poly_ring R\<^esub> q) = roots q"
+proof -
+ interpret UP: domain "poly_ring R"
+ using univ_poly_is_domain[OF carrier_is_subring] .
+
+ assume no_roots: "roots p = {#}" show "roots (p \<otimes>\<^bsub>poly_ring R\<^esub> q) = roots q"
+ proof (intro subset_mset.antisym)
+ have pdiv: "q pdivides (p \<otimes>\<^bsub>poly_ring R\<^esub> q)"
+ using UP.divides_prod_l assms unfolding pdivides_def by blast
+ show "roots q \<subseteq># roots (p \<otimes>\<^bsub>poly_ring R\<^esub> q)"
+ using pdivides_imp_roots_incl[OF _ _ _ pdiv] assms
+ degree_zero_imp_empty_roots[OF assms(3)]
+ by (cases "q = []", auto, metis UP.l_null UP.m_rcancel UP.zero_closed univ_poly_zero)
+ next
+ show "roots (p \<otimes>\<^bsub>poly_ring R\<^esub> q) \<subseteq># roots q"
+ proof (cases "p \<otimes>\<^bsub>poly_ring R\<^esub> q = []")
+ case True thus ?thesis
+ using degree_zero_imp_empty_roots[OF UP.m_closed[OF assms(1,3)]] by simp
+ next
+ case False with \<open>p \<noteq> []\<close> have q_not_zero: "q \<noteq> []"
+ by (metis UP.r_null assms(1) univ_poly_zero)
+ show ?thesis
+ proof (rule roots_inclI[OF UP.m_closed[OF assms(1,3)] assms(3) q_not_zero])
+ fix a assume a: "a \<in> carrier R"
+ hence "\<not> ([ \<one>, \<ominus> a ] pdivides p)"
+ using assms(1-2) no_roots pdivides_imp_is_root roots_mem_iff_is_root[of p] by auto
+ moreover have in_carrier: "[ \<one>, \<ominus> a ] \<in> carrier (poly_ring R)"
+ using a unfolding sym[OF univ_poly_carrier] polynomial_def by auto
+ hence "pirreducible (carrier R) [ \<one>, \<ominus> a ]"
+ using degree_one_imp_pirreducible[OF carrier_is_subfield] by simp
+ moreover
+ have "([ \<one>, \<ominus> a ] [^]\<^bsub>poly_ring R\<^esub> (alg_mult (p \<otimes>\<^bsub>poly_ring R\<^esub> q) a)) pdivides (p \<otimes>\<^bsub>poly_ring R\<^esub> q)"
+ using le_alg_mult_imp_pdivides[OF a UP.m_closed, of p q] assms by simp
+ ultimately show "([ \<one>, \<ominus> a ] [^]\<^bsub>poly_ring R\<^esub> (alg_mult (p \<otimes>\<^bsub>poly_ring R\<^esub> q) a)) pdivides q"
+ using pirreducible_pow_pdivides_iff[OF carrier_is_subfield in_carrier] assms by auto
+ qed
+ qed
+ qed
+qed
+
+lemma (in field) poly_mult_degree_one_monic_imp_same_roots:
+ assumes "a \<in> carrier R" and "p \<in> carrier (poly_ring R)" "p \<noteq> []"
+ shows "roots ([ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> p) = add_mset a (roots p)"
+proof -
+ interpret UP: domain "poly_ring R"
+ using univ_poly_is_domain[OF carrier_is_subring] .
+
+ from \<open>a \<in> carrier R\<close> have in_carrier: "[ \<one>, \<ominus> a ] \<in> carrier (poly_ring R)"
+ unfolding sym[OF univ_poly_carrier] polynomial_def by simp
+
+ show ?thesis
+ proof (intro subset_mset.antisym[OF roots_inclI' mset_subset_eqI])
+ show "([ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> p) \<in> carrier (poly_ring R)"
+ using in_carrier assms(2) by simp
+ next
+ fix b assume b: "b \<in> carrier R" and "[ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> p \<noteq> []"
+ hence not_zero: "p \<noteq> []"
+ unfolding univ_poly_def by auto
+ from \<open>b \<in> carrier R\<close> have in_carrier': "[ \<one>, \<ominus> b ] \<in> carrier (poly_ring R)"
+ unfolding sym[OF univ_poly_carrier] polynomial_def by simp
+ show "alg_mult ([ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> p) b \<le> count (add_mset a (roots p)) b"
+ proof (cases "a = b")
+ case False
+ hence "\<not> [ \<one>, \<ominus> b ] pdivides [ \<one>, \<ominus> a ]"
+ using assms(1) b monic_degree_one_root_condition pdivides_imp_is_root by blast
+ moreover have "pirreducible (carrier R) [ \<one>, \<ominus> b ]"
+ using degree_one_imp_pirreducible[OF carrier_is_subfield in_carrier'] by simp
+ ultimately
+ have "[ \<one>, \<ominus> b ] [^]\<^bsub>poly_ring R\<^esub> (alg_mult ([ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> p) b) pdivides p"
+ using le_alg_mult_imp_pdivides[OF b UP.m_closed, of _ p] assms(2) in_carrier
+ pirreducible_pow_pdivides_iff[OF carrier_is_subfield in_carrier' in_carrier, of p]
+ by auto
+ with \<open>a \<noteq> b\<close> show ?thesis
+ using alg_mult_eq_count_roots[OF assms(2)] alg_multE(2)[OF b assms(2) not_zero] by auto
+ next
+ case True
+ have "[ \<one>, \<ominus> a ] pdivides ([ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> p)"
+ using dividesI[OF assms(2)] unfolding pdivides_def by auto
+ with \<open>[ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> p \<noteq> []\<close>
+ have "alg_mult ([ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> p) a \<ge> Suc 0"
+ using alg_multE(2)[of a _ "Suc 0"] in_carrier assms by auto
+ then obtain m where m: "alg_mult ([ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> p) a = Suc m"
+ using Suc_le_D by blast
+ hence "([ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> ([ \<one>, \<ominus> a ] [^]\<^bsub>poly_ring R\<^esub> m)) pdivides
+ ([ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> p)"
+ using le_alg_mult_imp_pdivides[OF _ UP.m_closed, of a _ p]
+ in_carrier assms UP.nat_pow_Suc2 by force
+ hence "([ \<one>, \<ominus> a ] [^]\<^bsub>poly_ring R\<^esub> m) pdivides p"
+ using UP.mult_divides in_carrier assms(2)
+ unfolding univ_poly_zero pdivides_def factor_def
+ by (simp add: UP.m_assoc UP.m_lcancel univ_poly_zero)
+ with \<open>a = b\<close> show ?thesis
+ using alg_mult_eq_count_roots assms in_carrier UP.nat_pow_Suc2
+ alg_multE(2)[OF assms(1) _ not_zero] m
+ by auto
+ qed
+ next
+ fix b
+ have not_zero: "[ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> p \<noteq> []"
+ using assms in_carrier univ_poly_zero[of R] UP.integral by auto
+
+ show "count (add_mset a (roots p)) b \<le> count (roots ([\<one>, \<ominus> a] \<otimes>\<^bsub>poly_ring R\<^esub> p)) b"
+ proof (cases "a = b")
+ case True
+ have "([ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> ([ \<one>, \<ominus> a ] [^]\<^bsub>poly_ring R\<^esub> (alg_mult p a))) pdivides
+ ([ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> p)"
+ using UP.divides_mult[OF _ in_carrier] le_alg_mult_imp_pdivides[OF assms(1,2)] in_carrier assms
+ by (auto simp add: pdivides_def)
+ with \<open>a = b\<close> show ?thesis
+ using alg_mult_eq_count_roots assms in_carrier UP.nat_pow_Suc2
+ alg_multE(2)[OF assms(1) _ not_zero]
+ by auto
+ next
+ case False
+ have "p pdivides ([ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> p)"
+ using dividesI[OF in_carrier] UP.m_comm in_carrier assms unfolding pdivides_def by auto
+ thus ?thesis
+ using False pdivides_imp_roots_incl assms in_carrier not_zero
+ by (simp add: subseteq_mset_def)
+ qed
+ qed
+qed
+
+lemma (in domain) not_empty_rootsE[elim]:
+ assumes "p \<in> carrier (poly_ring R)" and "roots p \<noteq> {#}"
+ and "\<And>a. \<lbrakk> a \<in> carrier R; a \<in># roots p;
+ [ \<one>, \<ominus> a ] \<in> carrier (poly_ring R); [ \<one>, \<ominus> a ] pdivides p \<rbrakk> \<Longrightarrow> P"
+ shows P
+proof -
+ from \<open>roots p \<noteq> {#}\<close> obtain a where "a \<in># roots p"
+ by blast
+ with \<open>p \<in> carrier (poly_ring R)\<close> have "[ \<one>, \<ominus> a ] pdivides p"
+ and "[ \<one>, \<ominus> a ] \<in> carrier (poly_ring R)" and "a \<in> carrier R"
+ using is_root_imp_pdivides[of p] roots_mem_iff_is_root[of p] is_root_def[of p a]
+ unfolding sym[OF univ_poly_carrier] polynomial_def by auto
+ with \<open>a \<in># roots p\<close> show ?thesis
+ using assms(3)[of a] by auto
+qed
+
+lemma (in field) associated_polynomials_imp_same_roots:
+ assumes "p \<in> carrier (poly_ring R)" "p \<noteq> []" and "q \<in> carrier (poly_ring R)" "q \<noteq> []"
+ shows "roots (p \<otimes>\<^bsub>poly_ring R\<^esub> q) = roots p + roots q"
+proof -
+ interpret UP: domain "poly_ring R"
+ using univ_poly_is_domain[OF carrier_is_subring] .
+ from assms show ?thesis
+ proof (induction "degree p" arbitrary: p rule: less_induct)
+ case less show ?case
+ proof (cases "roots p = {#}")
+ case True thus ?thesis
+ using no_roots_imp_same_roots[of p q] less by simp
+ next
+ case False with \<open>p \<in> carrier (poly_ring R)\<close>
+ obtain a where a: "a \<in> carrier R" and "a \<in># roots p" and pdiv: "[ \<one>, \<ominus> a ] pdivides p"
+ and in_carrier: "[ \<one>, \<ominus> a ] \<in> carrier (poly_ring R)"
+ by blast
+ show ?thesis
+ proof (cases "degree p = 1")
+ case True with \<open>p \<in> carrier (poly_ring R)\<close>
+ obtain b c where p: "p = [ b, c ]" and b: "b \<in> carrier R" "b \<noteq> \<zero>" and c: "c \<in> carrier R"
+ by auto
+ with \<open>a \<in># roots p\<close> have roots: "roots p = {# a #}" and a: "\<ominus> a = inv b \<otimes> c" "a \<in> carrier R"
+ and lead: "lead_coeff p = b" and const: "const_term p = c"
+ using degree_one_imp_singleton_roots[of p] less(2) field_Units
+ unfolding const_term_def by auto
+ hence "(p \<otimes>\<^bsub>poly_ring R\<^esub> q) \<sim>\<^bsub>poly_ring R\<^esub> ([ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> q)"
+ using UP.mult_cong_l[OF degree_one_associatedI[OF carrier_is_subfield _ True]] less(2,4)
+ by (auto simp add: a lead const)
+ hence "roots (p \<otimes>\<^bsub>poly_ring R\<^esub> q) = roots ([ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> q)"
+ using associated_polynomials_imp_same_roots in_carrier less(2,4) unfolding a by simp
+ thus ?thesis
+ unfolding poly_mult_degree_one_monic_imp_same_roots[OF a(2) less(4,5)] roots by simp
+ next
+ case False
+ from \<open>[ \<one>, \<ominus> a ] pdivides p\<close>
+ obtain r where p: "p = [ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> r" and r: "r \<in> carrier (poly_ring R)"
+ unfolding pdivides_def by auto
+ with \<open>p \<noteq> []\<close> have not_zero: "r \<noteq> []"
+ using in_carrier univ_poly_zero[of R "carrier R"] UP.integral_iff by auto
+ with \<open>p = [ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> r\<close> have deg: "degree p = Suc (degree r)"
+ using poly_mult_degree_eq[OF carrier_is_subring, of _ r] in_carrier r
+ unfolding univ_poly_carrier sym[OF univ_poly_mult[of R "carrier R"]] by auto
+ with \<open>r \<noteq> []\<close> and \<open>q \<noteq> []\<close> have "r \<otimes>\<^bsub>poly_ring R\<^esub> q \<noteq> []"
+ using in_carrier univ_poly_zero[of R "carrier R"] UP.integral less(4) r by auto
+ hence "roots (p \<otimes>\<^bsub>poly_ring R\<^esub> q) = add_mset a (roots (r \<otimes>\<^bsub>poly_ring R\<^esub> q))"
+ using poly_mult_degree_one_monic_imp_same_roots[OF a UP.m_closed[OF r less(4)]]
+ UP.m_assoc[OF in_carrier r less(4)] p by auto
+ also have " ... = add_mset a (roots r + roots q)"
+ using less(1)[OF _ r not_zero less(4-5)] deg by simp
+ also have " ... = (add_mset a (roots r)) + roots q"
+ by simp
+ also have " ... = roots p + roots q"
+ using poly_mult_degree_one_monic_imp_same_roots[OF a r not_zero] p by simp
+ finally show ?thesis .
+ qed
+ qed
+ qed
+qed
+
+lemma (in field) size_roots_le_degree:
+ assumes "p \<in> carrier (poly_ring R)" shows "size (roots p) \<le> degree p"
+ using assms
+proof (induction "degree p" arbitrary: p rule: less_induct)
+ case less show ?case
+ proof (cases "roots p = {#}", simp)
+ interpret UP: domain "poly_ring R"
+ using univ_poly_is_domain[OF carrier_is_subring] .
+
+ case False with \<open>p \<in> carrier (poly_ring R)\<close>
+ obtain a where a: "a \<in> carrier R" and "a \<in># roots p" and "[ \<one>, \<ominus> a ] pdivides p"
+ and in_carrier: "[ \<one>, \<ominus> a ] \<in> carrier (poly_ring R)"
+ by blast
+ then obtain q where p: "p = [ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> q" and q: "q \<in> carrier (poly_ring R)"
+ unfolding pdivides_def by auto
+ with \<open>a \<in># roots p\<close> have "p \<noteq> []"
+ using degree_zero_imp_empty_roots[OF less(2)] by auto
+ hence not_zero: "q \<noteq> []"
+ using in_carrier univ_poly_zero[of R "carrier R"] UP.integral_iff p by auto
+ hence "degree p = Suc (degree q)"
+ using poly_mult_degree_eq[OF carrier_is_subring, of _ q] in_carrier p q
+ unfolding univ_poly_carrier sym[OF univ_poly_mult[of R "carrier R"]] by auto
+ with \<open>q \<noteq> []\<close> show ?thesis
+ using poly_mult_degree_one_monic_imp_same_roots[OF a q] p less(1)[OF _ q]
+ by (metis Suc_le_mono lessI size_add_mset)
+ qed
+qed
+
+lemma (in domain) pirreducible_roots:
+ assumes "p \<in> carrier (poly_ring R)" and "pirreducible (carrier R) p" and "degree p \<noteq> 1"
+ shows "roots p = {#}"
+proof (rule ccontr)
+ assume "roots p \<noteq> {#}" with \<open>p \<in> carrier (poly_ring R)\<close>
+ obtain a where a: "a \<in> carrier R" and "a \<in># roots p" and "[ \<one>, \<ominus> a ] pdivides p"
+ and in_carrier: "[ \<one>, \<ominus> a ] \<in> carrier (poly_ring R)"
+ by blast
+ hence "[ \<one>, \<ominus> a ] \<sim>\<^bsub>poly_ring R\<^esub> p"
+ using divides_pirreducible_condition[OF assms(2) in_carrier]
+ univ_poly_units_incl[OF carrier_is_subring]
+ unfolding pdivides_def by auto
+ hence "degree p = 1"
+ using associated_polynomials_imp_same_length[OF carrier_is_subring in_carrier assms(1)] by auto
+ with \<open>degree p \<noteq> 1\<close> show False ..
+qed
+
+lemma (in field) pirreducible_imp_not_splitted:
+ assumes "p \<in> carrier (poly_ring R)" and "pirreducible (carrier R) p" and "degree p \<noteq> 1"
+ shows "\<not> splitted p"
+ using pirreducible_roots[of p] pirreducible_degree[OF carrier_is_subfield, of p] assms
+ by (simp add: splitted_def)
+
+lemma (in field)
+ assumes "p \<in> carrier (poly_ring R)" and "q \<in> carrier (poly_ring R)"
+ and "pirreducible (carrier R) p" and "degree p \<noteq> 1"
+ shows "roots (p \<otimes>\<^bsub>poly_ring R\<^esub> q) = roots q"
+ using no_roots_imp_same_roots[of p q] pirreducible_roots[of p] assms
+ unfolding ring_irreducible_def univ_poly_zero by auto
+
+lemma (in field) trivial_factors_imp_splitted:
+ assumes "p \<in> carrier (poly_ring R)"
+ and "\<And>q. \<lbrakk> q \<in> carrier (poly_ring R); pirreducible (carrier R) q; q pdivides p \<rbrakk> \<Longrightarrow> degree q \<le> 1"
+ shows "splitted p"
+ using assms
+proof (induction "degree p" arbitrary: p rule: less_induct)
+ interpret UP: principal_domain "poly_ring R"
+ using univ_poly_is_principal[OF carrier_is_subfield] .
+ case less show ?case
+ proof (cases "degree p = 0", simp add: degree_zero_imp_splitted[OF less(2)])
+ case False show ?thesis
+ proof (cases "roots p = {#}")
+ case True
+ from \<open>degree p \<noteq> 0\<close> have "p \<notin> Units (poly_ring R)" and "p \<in> carrier (poly_ring R) - { [] }"
+ using univ_poly_units'[OF carrier_is_subfield, of p] less(2) by auto
+ then obtain q where "q \<in> carrier (poly_ring R)" "pirreducible (carrier R) q" and "q pdivides p"
+ using UP.exists_irreducible_divisor[of p] unfolding univ_poly_zero pdivides_def by auto
+ with \<open>degree p \<noteq> 0\<close> have "roots p \<noteq> {#}"
+ using degree_one_imp_singleton_roots[OF _ , of q] less(3)[of q]
+ pdivides_imp_roots_incl[OF _ less(2), of q]
+ pirreducible_degree[OF carrier_is_subfield, of q]
+ by force
+ from \<open>roots p = {#}\<close> and \<open>roots p \<noteq> {#}\<close> have False
+ by simp
+ thus ?thesis ..
+ next
+ case False with \<open>p \<in> carrier (poly_ring R)\<close>
+ obtain a where a: "a \<in> carrier R" and "a \<in># roots p" and "[ \<one>, \<ominus> a ] pdivides p"
+ and in_carrier: "[ \<one>, \<ominus> a ] \<in> carrier (poly_ring R)"
+ by blast
+ then obtain q where p: "p = [ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> q" and q: "q \<in> carrier (poly_ring R)"
+ unfolding pdivides_def by blast
+ with \<open>degree p \<noteq> 0\<close> have "p \<noteq> []"
+ by auto
+ with \<open>p = [ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> q\<close> have "q \<noteq> []"
+ using in_carrier q unfolding sym[OF univ_poly_zero[of R "carrier R"]] by auto
+ with \<open>p = [ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> q\<close> and \<open>p \<noteq> []\<close> have "degree p = Suc (degree q)"
+ using poly_mult_degree_eq[OF carrier_is_subring] in_carrier q
+ unfolding univ_poly_carrier sym[OF univ_poly_mult[of R "carrier R"]] by auto
+ moreover have "q pdivides p"
+ using p dividesI[OF in_carrier] UP.m_comm[OF in_carrier q] by (auto simp add: pdivides_def)
+ hence "degree r = 1" if "r \<in> carrier (poly_ring R)" and "pirreducible (carrier R) r"
+ and "r pdivides q" for r
+ using less(3)[OF that(1-2)] UP.divides_trans[OF _ _ that(1), of q p] that(3)
+ pirreducible_degree[OF carrier_is_subfield that(1-2)]
+ by (auto simp add: pdivides_def)
+ ultimately have "splitted q"
+ using less(1)[OF _ q] by auto
+ with \<open>degree p = Suc (degree q)\<close> and \<open>q \<noteq> []\<close> show ?thesis
+ using poly_mult_degree_one_monic_imp_same_roots[OF a q]
+ unfolding sym[OF p] splitted_def
+ by simp
+ qed
+ qed
+qed
+
+lemma (in field) pdivides_imp_splitted:
+ assumes "p \<in> carrier (poly_ring R)" and "q \<in> carrier (poly_ring R)" "q \<noteq> []" and "splitted q"
+ shows "p pdivides q \<Longrightarrow> splitted p"
+proof (cases "p = []")
+ case True thus ?thesis
+ using degree_zero_imp_splitted[OF assms(1)] by simp
+next
+ interpret UP: principal_domain "poly_ring R"
+ using univ_poly_is_principal[OF carrier_is_subfield] .
+
+ case False
+ assume "p pdivides q"
+ then obtain b where b: "b \<in> carrier (poly_ring R)" and q: "q = p \<otimes>\<^bsub>poly_ring R\<^esub> b"
+ unfolding pdivides_def by auto
+ with \<open>q \<noteq> []\<close> have "p \<noteq> []" and "b \<noteq> []"
+ using assms UP.integral_iff[of p b] unfolding sym[OF univ_poly_zero[of R "carrier R"]] by auto
+ hence "degree p + degree b = size (roots p) + size (roots b)"
+ using associated_polynomials_imp_same_roots[of p b] assms b q splitted_def
+ poly_mult_degree_eq[OF carrier_is_subring,of p b]
+ unfolding univ_poly_carrier sym[OF univ_poly_mult[of R "carrier R"]]
+ by auto
+ moreover have "size (roots p) \<le> degree p" and "size (roots b) \<le> degree b"
+ using size_roots_le_degree assms(1) b by auto
+ ultimately show ?thesis
+ unfolding splitted_def by linarith
+qed
+
+lemma (in field) splitted_imp_trivial_factors:
+ assumes "p \<in> carrier (poly_ring R)" "p \<noteq> []" and "splitted p"
+ shows "\<And>q. \<lbrakk> q \<in> carrier (poly_ring R); pirreducible (carrier R) q; q pdivides p \<rbrakk> \<Longrightarrow> degree q = 1"
+ using pdivides_imp_splitted[OF _ assms] pirreducible_imp_not_splitted
+ by auto
subsection \<open>Link between @{term \<open>(pmod)\<close>} and @{term rupture_surj}\<close>
@@ -943,32 +2020,6 @@
qed
qed
-(* Move to Ideal.thy ========================================================= *)
-lemma (in ring) quotient_eq_iff_same_a_r_cos:
- assumes "ideal I R" and "a \<in> carrier R" and "b \<in> carrier R"
- shows "a \<ominus> b \<in> I \<longleftrightarrow> I +> a = I +> b"
-proof
- assume "I +> a = I +> b"
- then obtain i where "i \<in> I" and "\<zero> \<oplus> a = i \<oplus> b"
- using additive_subgroup.zero_closed[OF ideal.axioms(1)[OF assms(1)]] assms(2)
- unfolding a_r_coset_def' by blast
- hence "a \<ominus> b = i"
- using assms(2-3) by (metis a_minus_def add.inv_solve_right assms(1) ideal.Icarr l_zero)
- with \<open>i \<in> I\<close> show "a \<ominus> b \<in> I"
- by simp
-next
- assume "a \<ominus> b \<in> I"
- then obtain i where "i \<in> I" and "a = i \<oplus> b"
- using ideal.Icarr[OF assms(1)] assms(2-3)
- by (metis a_minus_def add.inv_solve_right)
- hence "I +> a = (I +> i) +> b"
- using ideal.Icarr[OF assms(1)] assms(3)
- by (simp add: a_coset_add_assoc subsetI)
- with \<open>i \<in> I\<close> show "I +> a = I +> b"
- using a_rcos_zero[OF assms(1)] by simp
-qed
-(* ========================================================================== *)
-
lemma (in domain) rupture_surj_inj_on:
assumes "subfield K R" and "p \<in> carrier (K[X])"
shows "inj_on (rupture_surj K p) ((\<lambda>q. q pmod p) ` (carrier (K[X])))"
--- a/src/HOL/Algebra/Pred_Zorn.thy Tue Apr 30 21:04:08 2019 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,57 +0,0 @@
-theory Pred_Zorn
- imports HOL.Zorn
-
-begin
-
-(* ========== *)
-lemma partial_order_onE:
- assumes "partial_order_on A r" shows "refl_on A r" and "trans r" and "antisym r"
- using assms unfolding partial_order_on_def preorder_on_def by auto
-(* ========== *)
-
-abbreviation rel_of :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> ('a \<times> 'a) set"
- where "rel_of P A \<equiv> { (a, b) \<in> A \<times> A. P a b }"
-
-lemma Field_rel_of:
- assumes "refl_on A (rel_of P A)" shows "Field (rel_of P A) = A"
- using assms unfolding refl_on_def Field_def by auto
-
-(* ========== *)
-lemma Chains_rel_of:
- assumes "C \<in> Chains (rel_of P A)" shows "C \<subseteq> A"
- using assms unfolding Chains_def by auto
-(* ========== *)
-
-lemma partial_order_on_rel_ofI:
- assumes refl: "\<And>a. a \<in> A \<Longrightarrow> P a a"
- and trans: "\<And>a b c. \<lbrakk> a \<in> A; b \<in> A; c \<in> A \<rbrakk> \<Longrightarrow> P a b \<Longrightarrow> P b c \<Longrightarrow> P a c"
- and antisym: "\<And>a b. \<lbrakk> a \<in> A; b \<in> A \<rbrakk> \<Longrightarrow> P a b \<Longrightarrow> P b a \<Longrightarrow> a = b"
- shows "partial_order_on A (rel_of P A)"
-proof -
- from refl have "refl_on A (rel_of P A)"
- unfolding refl_on_def by auto
- moreover have "trans (rel_of P A)" and "antisym (rel_of P A)"
- by (auto intro: transI dest: trans, auto intro: antisymI dest: antisym)
- ultimately show ?thesis
- unfolding partial_order_on_def preorder_on_def by simp
-qed
-
-lemma Partial_order_rel_ofI:
- assumes "partial_order_on A (rel_of P A)" shows "Partial_order (rel_of P A)"
- using assms unfolding Field_rel_of[OF partial_order_onE(1)[OF assms]] .
-
-lemma predicate_Zorn:
- assumes "partial_order_on A (rel_of P A)"
- and "\<forall>C \<in> Chains (rel_of P A). \<exists>u \<in> A. \<forall>a \<in> C. P a u"
- shows "\<exists>m \<in> A. \<forall>a \<in> A. P m a \<longrightarrow> a = m"
-proof -
- have "a \<in> A" if "a \<in> C" and "C \<in> Chains (rel_of P A)" for C a
- using that Chains_rel_of by auto
- moreover have "(a, u) \<in> rel_of P A" if "a \<in> A" and "u \<in> A" and "P a u" for a u
- using that by auto
- ultimately show ?thesis
- using Zorns_po_lemma[OF Partial_order_rel_ofI[OF assms(1)]] assms(2)
- unfolding Field_rel_of[OF partial_order_onE(1)[OF assms(1)]] by auto
-qed
-
-end
\ No newline at end of file
--- a/src/HOL/Algebra/Ring.thy Tue Apr 30 21:04:08 2019 +0100
+++ b/src/HOL/Algebra/Ring.thy Tue Apr 30 21:04:21 2019 +0100
@@ -643,6 +643,9 @@
text \<open>Field would not need to be derived from domain, the properties
for domain follow from the assumptions of field\<close>
+lemma (in field) is_ring: "ring R"
+ using ring_axioms .
+
lemma fieldE :
fixes R (structure)
assumes "field R"
--- a/src/HOL/Nonstandard_Analysis/HDeriv.thy Tue Apr 30 21:04:08 2019 +0100
+++ b/src/HOL/Nonstandard_Analysis/HDeriv.thy Tue Apr 30 21:04:21 2019 +0100
@@ -34,9 +34,6 @@
lemma NS_DERIV_D: "DERIV f x :> D \<Longrightarrow> (\<lambda>h. (f (x + h) - f x) / h) \<midarrow>0\<rightarrow>\<^sub>N\<^sub>S D"
by (simp add: DERIV_def LIM_NSLIM_iff)
-lemma hnorm_of_hypreal: "\<And>r. hnorm (( *f* of_real) r::'a::real_normed_div_algebra star) = \<bar>r\<bar>"
- by transfer (rule norm_of_real)
-
lemma Infinitesimal_of_hypreal:
"x \<in> Infinitesimal \<Longrightarrow> (( *f* of_real) x::'a::real_normed_div_algebra star) \<in> Infinitesimal"
by (metis Infinitesimal_of_hypreal_iff of_hypreal_def)
--- a/src/HOL/Nonstandard_Analysis/HTranscendental.thy Tue Apr 30 21:04:08 2019 +0100
+++ b/src/HOL/Nonstandard_Analysis/HTranscendental.thy Tue Apr 30 21:04:21 2019 +0100
@@ -84,6 +84,13 @@
lemma hypreal_sqrt_ge_zero: "0 \<le> x \<Longrightarrow> 0 \<le> ( *f* sqrt)(x)"
by (auto intro: hypreal_sqrt_gt_zero simp add: order_le_less)
+lemma hypreal_sqrt_lessI:
+ "\<And>x u. \<lbrakk>0 < u; x < u\<^sup>2\<rbrakk> \<Longrightarrow> ( *f* sqrt) x < u"
+proof transfer
+ show "\<And>x u. \<lbrakk>0 < u; x < u\<^sup>2\<rbrakk> \<Longrightarrow> sqrt x < u"
+ by (metis less_le real_sqrt_less_iff real_sqrt_pow2 real_sqrt_power)
+qed
+
lemma hypreal_sqrt_hrabs [simp]: "\<And>x. ( *f* sqrt)(x\<^sup>2) = \<bar>x\<bar>"
by transfer simp
@@ -521,7 +528,7 @@
by (metis Infinitesimal_square_iff STAR_cos_Infinitesimal approx_diff approx_sym diff_zero mem_infmal_iff power2_eq_square)
lemma STAR_cos_Infinitesimal_approx2:
- fixes x :: hypreal \<comment> \<open>perhaps could be generalised, like many other hypreal results\<close>
+ fixes x :: hypreal
assumes "x \<in> Infinitesimal"
shows "( *f* cos) x \<approx> 1 - (x\<^sup>2)/2"
proof -
--- a/src/HOL/Nonstandard_Analysis/HyperNat.thy Tue Apr 30 21:04:08 2019 +0100
+++ b/src/HOL/Nonstandard_Analysis/HyperNat.thy Tue Apr 30 21:04:21 2019 +0100
@@ -154,12 +154,14 @@
lemma hypnat_of_nat_Suc [simp]: "hypnat_of_nat (Suc n) = hypnat_of_nat n + 1"
by transfer simp
-lemma of_nat_eq_add [rule_format]: "\<forall>d::hypnat. of_nat m = of_nat n + d \<longrightarrow> d \<in> range of_nat"
- apply (induct n)
- apply (auto simp add: add.assoc)
- apply (case_tac x)
- apply (auto simp add: add.commute [of 1])
- done
+lemma of_nat_eq_add:
+ fixes d::hypnat
+ shows "of_nat m = of_nat n + d \<Longrightarrow> d \<in> range of_nat"
+proof (induct n arbitrary: d)
+ case (Suc n)
+ then show ?case
+ by (metis Nats_def Nats_eq_Standard Standard_simps(4) hypnat_diff_add_inverse of_nat_in_Nats)
+qed auto
lemma Nats_diff [simp]: "a \<in> Nats \<Longrightarrow> b \<in> Nats \<Longrightarrow> a - b \<in> Nats" for a b :: hypnat
by (simp add: Nats_eq_Standard)
@@ -224,37 +226,22 @@
by (simp add: HNatInfinite_def)
lemma Nats_downward_closed: "x \<in> Nats \<Longrightarrow> y \<le> x \<Longrightarrow> y \<in> Nats" for x y :: hypnat
- apply (simp only: linorder_not_less [symmetric])
- apply (erule contrapos_np)
- apply (drule HNatInfinite_not_Nats_iff [THEN iffD2])
- apply (erule (1) Nats_less_HNatInfinite)
- done
+ using HNatInfinite_not_Nats_iff Nats_le_HNatInfinite by fastforce
lemma HNatInfinite_upward_closed: "x \<in> HNatInfinite \<Longrightarrow> x \<le> y \<Longrightarrow> y \<in> HNatInfinite"
- apply (simp only: HNatInfinite_not_Nats_iff)
- apply (erule contrapos_nn)
- apply (erule (1) Nats_downward_closed)
- done
+ using HNatInfinite_not_Nats_iff Nats_downward_closed by blast
lemma HNatInfinite_add: "x \<in> HNatInfinite \<Longrightarrow> x + y \<in> HNatInfinite"
- apply (erule HNatInfinite_upward_closed)
- apply (rule hypnat_le_add1)
- done
+ using HNatInfinite_upward_closed hypnat_le_add1 by blast
lemma HNatInfinite_add_one: "x \<in> HNatInfinite \<Longrightarrow> x + 1 \<in> HNatInfinite"
by (rule HNatInfinite_add)
-lemma HNatInfinite_diff: "x \<in> HNatInfinite \<Longrightarrow> y \<in> Nats \<Longrightarrow> x - y \<in> HNatInfinite"
- apply (frule (1) Nats_le_HNatInfinite)
- apply (simp only: HNatInfinite_not_Nats_iff)
- apply (erule contrapos_nn)
- apply (drule (1) Nats_add, simp)
- done
+lemma HNatInfinite_diff: "\<lbrakk>x \<in> HNatInfinite; y \<in> Nats\<rbrakk> \<Longrightarrow> x - y \<in> HNatInfinite"
+ by (metis HNatInfinite_not_Nats_iff Nats_add Nats_le_HNatInfinite le_add_diff_inverse)
lemma HNatInfinite_is_Suc: "x \<in> HNatInfinite \<Longrightarrow> \<exists>y. x = y + 1" for x :: hypnat
- apply (rule_tac x = "x - (1::hypnat) " in exI)
- apply (simp add: Nats_le_HNatInfinite)
- done
+ using hypnat_gt_zero_iff2 zero_less_HNatInfinite by blast
subsection \<open>Existence of an infinite hypernatural number\<close>
@@ -308,32 +295,29 @@
text \<open>\<^term>\<open>HNatInfinite = {N. \<forall>n \<in> Nats. n < N}\<close>\<close>
-(*??delete? similar reasoning in hypnat_omega_gt_SHNat above*)
-lemma HNatInfinite_FreeUltrafilterNat_lemma:
- assumes "\<forall>N::nat. eventually (\<lambda>n. f n \<noteq> N) \<U>"
- shows "eventually (\<lambda>n. N < f n) \<U>"
- apply (induct N)
- using assms
- apply (drule_tac x = 0 in spec, simp)
- using assms
- apply (drule_tac x = "Suc N" in spec)
- apply (auto elim: eventually_elim2)
- done
+text\<open>unused, but possibly interesting\<close>
+lemma HNatInfinite_FreeUltrafilterNat_eventually:
+ assumes "\<And>k::nat. eventually (\<lambda>n. f n \<noteq> k) \<U>"
+ shows "eventually (\<lambda>n. m < f n) \<U>"
+proof (induct m)
+ case 0
+ then show ?case
+ using assms eventually_mono by fastforce
+next
+ case (Suc m)
+ then show ?case
+ using assms [of "Suc m"] eventually_elim2 by fastforce
+qed
lemma HNatInfinite_iff: "HNatInfinite = {N. \<forall>n \<in> Nats. n < N}"
- apply (safe intro!: Nats_less_HNatInfinite)
- apply (auto simp add: HNatInfinite_def)
- done
+ using HNatInfinite_def Nats_less_HNatInfinite by auto
subsubsection \<open>Alternative Characterization of \<^term>\<open>HNatInfinite\<close> using Free Ultrafilter\<close>
lemma HNatInfinite_FreeUltrafilterNat:
"star_n X \<in> HNatInfinite \<Longrightarrow> \<forall>u. eventually (\<lambda>n. u < X n) \<U>"
- apply (auto simp add: HNatInfinite_iff SHNat_eq)
- apply (drule_tac x="star_of u" in spec, simp)
- apply (simp add: star_of_def star_less_def starP2_star_n)
- done
+ by (metis (full_types) starP2_star_of starP_star_n star_less_def star_of_less_HNatInfinite)
lemma FreeUltrafilterNat_HNatInfinite:
"\<forall>u. eventually (\<lambda>n. u < X n) \<U> \<Longrightarrow> star_n X \<in> HNatInfinite"
--- a/src/HOL/Nonstandard_Analysis/NSCA.thy Tue Apr 30 21:04:08 2019 +0100
+++ b/src/HOL/Nonstandard_Analysis/NSCA.thy Tue Apr 30 21:04:21 2019 +0100
@@ -22,145 +22,114 @@
subsection\<open>Closure Laws for SComplex, the Standard Complex Numbers\<close>
lemma SComplex_minus_iff [simp]: "(-x \<in> SComplex) = (x \<in> SComplex)"
-by (auto, drule Standard_minus, auto)
+ using Standard_minus by fastforce
lemma SComplex_add_cancel:
- "[| x + y \<in> SComplex; y \<in> SComplex |] ==> x \<in> SComplex"
-by (drule (1) Standard_diff, simp)
+ "\<lbrakk>x + y \<in> SComplex; y \<in> SComplex\<rbrakk> \<Longrightarrow> x \<in> SComplex"
+ using Standard_diff by fastforce
lemma SReal_hcmod_hcomplex_of_complex [simp]:
- "hcmod (hcomplex_of_complex r) \<in> \<real>"
-by (simp add: Reals_eq_Standard)
+ "hcmod (hcomplex_of_complex r) \<in> \<real>"
+ by (simp add: Reals_eq_Standard)
-lemma SReal_hcmod_numeral [simp]: "hcmod (numeral w ::hcomplex) \<in> \<real>"
-by (simp add: Reals_eq_Standard)
+lemma SReal_hcmod_numeral: "hcmod (numeral w ::hcomplex) \<in> \<real>"
+ by simp
-lemma SReal_hcmod_SComplex: "x \<in> SComplex ==> hcmod x \<in> \<real>"
-by (simp add: Reals_eq_Standard)
+lemma SReal_hcmod_SComplex: "x \<in> SComplex \<Longrightarrow> hcmod x \<in> \<real>"
+ by (simp add: Reals_eq_Standard)
lemma SComplex_divide_numeral:
- "r \<in> SComplex ==> r/(numeral w::hcomplex) \<in> SComplex"
-by simp
+ "r \<in> SComplex \<Longrightarrow> r/(numeral w::hcomplex) \<in> SComplex"
+ by simp
lemma SComplex_UNIV_complex:
- "{x. hcomplex_of_complex x \<in> SComplex} = (UNIV::complex set)"
-by simp
+ "{x. hcomplex_of_complex x \<in> SComplex} = (UNIV::complex set)"
+ by simp
lemma SComplex_iff: "(x \<in> SComplex) = (\<exists>y. x = hcomplex_of_complex y)"
-by (simp add: Standard_def image_def)
+ by (simp add: Standard_def image_def)
lemma hcomplex_of_complex_image:
- "hcomplex_of_complex `(UNIV::complex set) = SComplex"
-by (simp add: Standard_def)
+ "range hcomplex_of_complex = SComplex"
+ by (simp add: Standard_def)
lemma inv_hcomplex_of_complex_image: "inv hcomplex_of_complex `SComplex = UNIV"
by (auto simp add: Standard_def image_def) (metis inj_star_of inv_f_f)
lemma SComplex_hcomplex_of_complex_image:
"\<lbrakk>\<exists>x. x \<in> P; P \<le> SComplex\<rbrakk> \<Longrightarrow> \<exists>Q. P = hcomplex_of_complex ` Q"
-apply (simp add: Standard_def, blast)
-done
+ by (metis Standard_def subset_imageE)
lemma SComplex_SReal_dense:
"\<lbrakk>x \<in> SComplex; y \<in> SComplex; hcmod x < hcmod y
\<rbrakk> \<Longrightarrow> \<exists>r \<in> Reals. hcmod x< r \<and> r < hcmod y"
-apply (auto intro: SReal_dense simp add: SReal_hcmod_SComplex)
-done
+ by (simp add: SReal_dense SReal_hcmod_SComplex)
subsection\<open>The Finite Elements form a Subring\<close>
lemma HFinite_hcmod_hcomplex_of_complex [simp]:
- "hcmod (hcomplex_of_complex r) \<in> HFinite"
-by (auto intro!: SReal_subset_HFinite [THEN subsetD])
+ "hcmod (hcomplex_of_complex r) \<in> HFinite"
+ by (auto intro!: SReal_subset_HFinite [THEN subsetD])
-lemma HFinite_hcmod_iff: "(x \<in> HFinite) = (hcmod x \<in> HFinite)"
-by (simp add: HFinite_def)
+lemma HFinite_hcmod_iff [simp]: "hcmod x \<in> HFinite \<longleftrightarrow> x \<in> HFinite"
+ by (simp add: HFinite_def)
lemma HFinite_bounded_hcmod:
"\<lbrakk>x \<in> HFinite; y \<le> hcmod x; 0 \<le> y\<rbrakk> \<Longrightarrow> y \<in> HFinite"
-by (auto intro: HFinite_bounded simp add: HFinite_hcmod_iff)
+ using HFinite_bounded HFinite_hcmod_iff by blast
subsection\<open>The Complex Infinitesimals form a Subring\<close>
-lemma hcomplex_sum_of_halves: "x/(2::hcomplex) + x/(2::hcomplex) = x"
-by auto
-
lemma Infinitesimal_hcmod_iff:
- "(z \<in> Infinitesimal) = (hcmod z \<in> Infinitesimal)"
-by (simp add: Infinitesimal_def)
+ "(z \<in> Infinitesimal) = (hcmod z \<in> Infinitesimal)"
+ by (simp add: Infinitesimal_def)
lemma HInfinite_hcmod_iff: "(z \<in> HInfinite) = (hcmod z \<in> HInfinite)"
-by (simp add: HInfinite_def)
+ by (simp add: HInfinite_def)
lemma HFinite_diff_Infinitesimal_hcmod:
- "x \<in> HFinite - Infinitesimal ==> hcmod x \<in> HFinite - Infinitesimal"
-by (simp add: HFinite_hcmod_iff Infinitesimal_hcmod_iff)
+ "x \<in> HFinite - Infinitesimal \<Longrightarrow> hcmod x \<in> HFinite - Infinitesimal"
+ by (simp add: Infinitesimal_hcmod_iff)
lemma hcmod_less_Infinitesimal:
- "[| e \<in> Infinitesimal; hcmod x < hcmod e |] ==> x \<in> Infinitesimal"
-by (auto elim: hrabs_less_Infinitesimal simp add: Infinitesimal_hcmod_iff)
+ "\<lbrakk>e \<in> Infinitesimal; hcmod x < hcmod e\<rbrakk> \<Longrightarrow> x \<in> Infinitesimal"
+ by (auto elim: hrabs_less_Infinitesimal simp add: Infinitesimal_hcmod_iff)
lemma hcmod_le_Infinitesimal:
- "[| e \<in> Infinitesimal; hcmod x \<le> hcmod e |] ==> x \<in> Infinitesimal"
-by (auto elim: hrabs_le_Infinitesimal simp add: Infinitesimal_hcmod_iff)
-
-lemma Infinitesimal_interval_hcmod:
- "[| e \<in> Infinitesimal;
- e' \<in> Infinitesimal;
- hcmod e' < hcmod x ; hcmod x < hcmod e
- |] ==> x \<in> Infinitesimal"
-by (auto intro: Infinitesimal_interval simp add: Infinitesimal_hcmod_iff)
-
-lemma Infinitesimal_interval2_hcmod:
- "[| e \<in> Infinitesimal;
- e' \<in> Infinitesimal;
- hcmod e' \<le> hcmod x ; hcmod x \<le> hcmod e
- |] ==> x \<in> Infinitesimal"
-by (auto intro: Infinitesimal_interval2 simp add: Infinitesimal_hcmod_iff)
+ "\<lbrakk>e \<in> Infinitesimal; hcmod x \<le> hcmod e\<rbrakk> \<Longrightarrow> x \<in> Infinitesimal"
+ by (auto elim: hrabs_le_Infinitesimal simp add: Infinitesimal_hcmod_iff)
subsection\<open>The ``Infinitely Close'' Relation\<close>
-(*
-Goalw [capprox_def,approx_def] "(z @c= w) = (hcmod z \<approx> hcmod w)"
-by (auto_tac (claset(),simpset() addsimps [Infinitesimal_hcmod_iff]));
-*)
+lemma approx_SComplex_mult_cancel_zero:
+ "\<lbrakk>a \<in> SComplex; a \<noteq> 0; a*x \<approx> 0\<rbrakk> \<Longrightarrow> x \<approx> 0"
+ by (metis Infinitesimal_mult_disj SComplex_iff mem_infmal_iff star_of_Infinitesimal_iff_0 star_zero_def)
-lemma approx_SComplex_mult_cancel_zero:
- "[| a \<in> SComplex; a \<noteq> 0; a*x \<approx> 0 |] ==> x \<approx> 0"
-apply (drule Standard_inverse [THEN Standard_subset_HFinite [THEN subsetD]])
-apply (auto dest: approx_mult2 simp add: mult.assoc [symmetric])
-done
+lemma approx_mult_SComplex1: "\<lbrakk>a \<in> SComplex; x \<approx> 0\<rbrakk> \<Longrightarrow> x*a \<approx> 0"
+ using SComplex_iff approx_mult_subst_star_of by fastforce
-lemma approx_mult_SComplex1: "[| a \<in> SComplex; x \<approx> 0 |] ==> x*a \<approx> 0"
-by (auto dest: Standard_subset_HFinite [THEN subsetD] approx_mult1)
-
-lemma approx_mult_SComplex2: "[| a \<in> SComplex; x \<approx> 0 |] ==> a*x \<approx> 0"
-by (auto dest: Standard_subset_HFinite [THEN subsetD] approx_mult2)
+lemma approx_mult_SComplex2: "\<lbrakk>a \<in> SComplex; x \<approx> 0\<rbrakk> \<Longrightarrow> a*x \<approx> 0"
+ by (metis approx_mult_SComplex1 mult.commute)
lemma approx_mult_SComplex_zero_cancel_iff [simp]:
- "[|a \<in> SComplex; a \<noteq> 0 |] ==> (a*x \<approx> 0) = (x \<approx> 0)"
-by (blast intro: approx_SComplex_mult_cancel_zero approx_mult_SComplex2)
+ "\<lbrakk>a \<in> SComplex; a \<noteq> 0\<rbrakk> \<Longrightarrow> (a*x \<approx> 0) = (x \<approx> 0)"
+ using approx_SComplex_mult_cancel_zero approx_mult_SComplex2 by blast
lemma approx_SComplex_mult_cancel:
- "[| a \<in> SComplex; a \<noteq> 0; a* w \<approx> a*z |] ==> w \<approx> z"
-apply (drule Standard_inverse [THEN Standard_subset_HFinite [THEN subsetD]])
-apply (auto dest: approx_mult2 simp add: mult.assoc [symmetric])
-done
+ "\<lbrakk>a \<in> SComplex; a \<noteq> 0; a*w \<approx> a*z\<rbrakk> \<Longrightarrow> w \<approx> z"
+ by (metis approx_SComplex_mult_cancel_zero approx_minus_iff right_diff_distrib)
lemma approx_SComplex_mult_cancel_iff1 [simp]:
- "[| a \<in> SComplex; a \<noteq> 0|] ==> (a* w \<approx> a*z) = (w \<approx> z)"
-by (auto intro!: approx_mult2 Standard_subset_HFinite [THEN subsetD]
- intro: approx_SComplex_mult_cancel)
+ "\<lbrakk>a \<in> SComplex; a \<noteq> 0\<rbrakk> \<Longrightarrow> (a*w \<approx> a*z) = (w \<approx> z)"
+ by (metis HFinite_star_of SComplex_iff approx_SComplex_mult_cancel approx_mult2)
(* TODO: generalize following theorems: hcmod -> hnorm *)
lemma approx_hcmod_approx_zero: "(x \<approx> y) = (hcmod (y - x) \<approx> 0)"
-apply (subst hnorm_minus_commute)
-apply (simp add: approx_def Infinitesimal_hcmod_iff)
-done
+ by (simp add: Infinitesimal_hcmod_iff approx_def hnorm_minus_commute)
lemma approx_approx_zero_iff: "(x \<approx> 0) = (hcmod x \<approx> 0)"
by (simp add: approx_hcmod_approx_zero)
@@ -169,347 +138,253 @@
by (simp add: approx_def)
lemma Infinitesimal_hcmod_add_diff:
- "u \<approx> 0 ==> hcmod(x + u) - hcmod x \<in> Infinitesimal"
-apply (drule approx_approx_zero_iff [THEN iffD1])
-apply (rule_tac e = "hcmod u" and e' = "- hcmod u" in Infinitesimal_interval2)
-apply (auto simp add: mem_infmal_iff [symmetric])
-apply (rule_tac c1 = "hcmod x" in add_le_cancel_left [THEN iffD1])
-apply auto
-done
+ "u \<approx> 0 \<Longrightarrow> hcmod(x + u) - hcmod x \<in> Infinitesimal"
+ by (metis add.commute add.left_neutral approx_add_right_iff approx_def approx_hnorm)
-lemma approx_hcmod_add_hcmod: "u \<approx> 0 ==> hcmod(x + u) \<approx> hcmod x"
-apply (rule approx_minus_iff [THEN iffD2])
-apply (auto intro: Infinitesimal_hcmod_add_diff simp add: mem_infmal_iff [symmetric])
-done
+lemma approx_hcmod_add_hcmod: "u \<approx> 0 \<Longrightarrow> hcmod(x + u) \<approx> hcmod x"
+ using Infinitesimal_hcmod_add_diff approx_def by blast
subsection\<open>Zero is the Only Infinitesimal Complex Number\<close>
lemma Infinitesimal_less_SComplex:
- "[| x \<in> SComplex; y \<in> Infinitesimal; 0 < hcmod x |] ==> hcmod y < hcmod x"
-by (auto intro: Infinitesimal_less_SReal SReal_hcmod_SComplex simp add: Infinitesimal_hcmod_iff)
+ "\<lbrakk>x \<in> SComplex; y \<in> Infinitesimal; 0 < hcmod x\<rbrakk> \<Longrightarrow> hcmod y < hcmod x"
+ by (auto intro: Infinitesimal_less_SReal SReal_hcmod_SComplex simp add: Infinitesimal_hcmod_iff)
lemma SComplex_Int_Infinitesimal_zero: "SComplex Int Infinitesimal = {0}"
-by (auto simp add: Standard_def Infinitesimal_hcmod_iff)
+ by (auto simp add: Standard_def Infinitesimal_hcmod_iff)
lemma SComplex_Infinitesimal_zero:
- "[| x \<in> SComplex; x \<in> Infinitesimal|] ==> x = 0"
-by (cut_tac SComplex_Int_Infinitesimal_zero, blast)
+ "\<lbrakk>x \<in> SComplex; x \<in> Infinitesimal\<rbrakk> \<Longrightarrow> x = 0"
+ using SComplex_iff by auto
lemma SComplex_HFinite_diff_Infinitesimal:
- "[| x \<in> SComplex; x \<noteq> 0 |] ==> x \<in> HFinite - Infinitesimal"
-by (auto dest: SComplex_Infinitesimal_zero Standard_subset_HFinite [THEN subsetD])
-
-lemma hcomplex_of_complex_HFinite_diff_Infinitesimal:
- "hcomplex_of_complex x \<noteq> 0
- ==> hcomplex_of_complex x \<in> HFinite - Infinitesimal"
-by (rule SComplex_HFinite_diff_Infinitesimal, auto)
+ "\<lbrakk>x \<in> SComplex; x \<noteq> 0\<rbrakk> \<Longrightarrow> x \<in> HFinite - Infinitesimal"
+ using SComplex_iff by auto
lemma numeral_not_Infinitesimal [simp]:
- "numeral w \<noteq> (0::hcomplex) ==> (numeral w::hcomplex) \<notin> Infinitesimal"
-by (fast dest: Standard_numeral [THEN SComplex_Infinitesimal_zero])
+ "numeral w \<noteq> (0::hcomplex) \<Longrightarrow> (numeral w::hcomplex) \<notin> Infinitesimal"
+ by (fast dest: Standard_numeral [THEN SComplex_Infinitesimal_zero])
lemma approx_SComplex_not_zero:
- "[| y \<in> SComplex; x \<approx> y; y\<noteq> 0 |] ==> x \<noteq> 0"
-by (auto dest: SComplex_Infinitesimal_zero approx_sym [THEN mem_infmal_iff [THEN iffD2]])
+ "\<lbrakk>y \<in> SComplex; x \<approx> y; y\<noteq> 0\<rbrakk> \<Longrightarrow> x \<noteq> 0"
+ by (auto dest: SComplex_Infinitesimal_zero approx_sym [THEN mem_infmal_iff [THEN iffD2]])
lemma SComplex_approx_iff:
- "[|x \<in> SComplex; y \<in> SComplex|] ==> (x \<approx> y) = (x = y)"
-by (auto simp add: Standard_def)
-
-lemma numeral_Infinitesimal_iff [simp]:
- "((numeral w :: hcomplex) \<in> Infinitesimal) =
- (numeral w = (0::hcomplex))"
-apply (rule iffI)
-apply (fast dest: Standard_numeral [THEN SComplex_Infinitesimal_zero])
-apply (simp (no_asm_simp))
-done
+ "\<lbrakk>x \<in> SComplex; y \<in> SComplex\<rbrakk> \<Longrightarrow> (x \<approx> y) = (x = y)"
+ by (auto simp add: Standard_def)
lemma approx_unique_complex:
- "[| r \<in> SComplex; s \<in> SComplex; r \<approx> x; s \<approx> x|] ==> r = s"
-by (blast intro: SComplex_approx_iff [THEN iffD1] approx_trans2)
+ "\<lbrakk>r \<in> SComplex; s \<in> SComplex; r \<approx> x; s \<approx> x\<rbrakk> \<Longrightarrow> r = s"
+ by (blast intro: SComplex_approx_iff [THEN iffD1] approx_trans2)
subsection \<open>Properties of \<^term>\<open>hRe\<close>, \<^term>\<open>hIm\<close> and \<^term>\<open>HComplex\<close>\<close>
-
lemma abs_hRe_le_hcmod: "\<And>x. \<bar>hRe x\<bar> \<le> hcmod x"
-by transfer (rule abs_Re_le_cmod)
+ by transfer (rule abs_Re_le_cmod)
lemma abs_hIm_le_hcmod: "\<And>x. \<bar>hIm x\<bar> \<le> hcmod x"
-by transfer (rule abs_Im_le_cmod)
+ by transfer (rule abs_Im_le_cmod)
lemma Infinitesimal_hRe: "x \<in> Infinitesimal \<Longrightarrow> hRe x \<in> Infinitesimal"
-apply (rule InfinitesimalI2, simp)
-apply (rule order_le_less_trans [OF abs_hRe_le_hcmod])
-apply (erule (1) InfinitesimalD2)
-done
+ using Infinitesimal_hcmod_iff abs_hRe_le_hcmod hrabs_le_Infinitesimal by blast
lemma Infinitesimal_hIm: "x \<in> Infinitesimal \<Longrightarrow> hIm x \<in> Infinitesimal"
-apply (rule InfinitesimalI2, simp)
-apply (rule order_le_less_trans [OF abs_hIm_le_hcmod])
-apply (erule (1) InfinitesimalD2)
-done
-
-lemma real_sqrt_lessI: "\<lbrakk>0 < u; x < u\<^sup>2\<rbrakk> \<Longrightarrow> sqrt x < u"
-(* TODO: this belongs somewhere else *)
-by (frule real_sqrt_less_mono) simp
-
-lemma hypreal_sqrt_lessI:
- "\<And>x u. \<lbrakk>0 < u; x < u\<^sup>2\<rbrakk> \<Longrightarrow> ( *f* sqrt) x < u"
-by transfer (rule real_sqrt_lessI)
-
-lemma hypreal_sqrt_ge_zero: "\<And>x. 0 \<le> x \<Longrightarrow> 0 \<le> ( *f* sqrt) x"
-by transfer (rule real_sqrt_ge_zero)
-
-lemma Infinitesimal_sqrt:
- "\<lbrakk>x \<in> Infinitesimal; 0 \<le> x\<rbrakk> \<Longrightarrow> ( *f* sqrt) x \<in> Infinitesimal"
-apply (rule InfinitesimalI2)
-apply (drule_tac r="r\<^sup>2" in InfinitesimalD2, simp)
-apply (simp add: hypreal_sqrt_ge_zero)
-apply (rule hypreal_sqrt_lessI, simp_all)
-done
+ using Infinitesimal_hcmod_iff abs_hIm_le_hcmod hrabs_le_Infinitesimal by blast
lemma Infinitesimal_HComplex:
- "\<lbrakk>x \<in> Infinitesimal; y \<in> Infinitesimal\<rbrakk> \<Longrightarrow> HComplex x y \<in> Infinitesimal"
-apply (rule Infinitesimal_hcmod_iff [THEN iffD2])
-apply (simp add: hcmod_i)
-apply (rule Infinitesimal_add)
-apply (erule Infinitesimal_hrealpow, simp)
-apply (erule Infinitesimal_hrealpow, simp)
-done
+ assumes x: "x \<in> Infinitesimal" and y: "y \<in> Infinitesimal"
+ shows "HComplex x y \<in> Infinitesimal"
+proof -
+ have "hcmod (HComplex 0 y) \<in> Infinitesimal"
+ by (simp add: hcmod_i y)
+ moreover have "hcmod (hcomplex_of_hypreal x) \<in> Infinitesimal"
+ using Infinitesimal_hcmod_iff Infinitesimal_of_hypreal_iff x by blast
+ ultimately have "hcmod (HComplex x y) \<in> Infinitesimal"
+ by (metis Infinitesimal_add Infinitesimal_hcmod_iff add.right_neutral hcomplex_of_hypreal_add_HComplex)
+ then show ?thesis
+ by (simp add: Infinitesimal_hnorm_iff)
+qed
lemma hcomplex_Infinitesimal_iff:
- "(x \<in> Infinitesimal) = (hRe x \<in> Infinitesimal \<and> hIm x \<in> Infinitesimal)"
-apply (safe intro!: Infinitesimal_hRe Infinitesimal_hIm)
-apply (drule (1) Infinitesimal_HComplex, simp)
-done
+ "(x \<in> Infinitesimal) \<longleftrightarrow> (hRe x \<in> Infinitesimal \<and> hIm x \<in> Infinitesimal)"
+ using Infinitesimal_HComplex Infinitesimal_hIm Infinitesimal_hRe by fastforce
lemma hRe_diff [simp]: "\<And>x y. hRe (x - y) = hRe x - hRe y"
-by transfer simp
+ by transfer simp
lemma hIm_diff [simp]: "\<And>x y. hIm (x - y) = hIm x - hIm y"
-by transfer simp
+ by transfer simp
lemma approx_hRe: "x \<approx> y \<Longrightarrow> hRe x \<approx> hRe y"
-unfolding approx_def by (drule Infinitesimal_hRe) simp
+ unfolding approx_def by (drule Infinitesimal_hRe) simp
lemma approx_hIm: "x \<approx> y \<Longrightarrow> hIm x \<approx> hIm y"
-unfolding approx_def by (drule Infinitesimal_hIm) simp
+ unfolding approx_def by (drule Infinitesimal_hIm) simp
lemma approx_HComplex:
"\<lbrakk>a \<approx> b; c \<approx> d\<rbrakk> \<Longrightarrow> HComplex a c \<approx> HComplex b d"
-unfolding approx_def by (simp add: Infinitesimal_HComplex)
+ unfolding approx_def by (simp add: Infinitesimal_HComplex)
lemma hcomplex_approx_iff:
"(x \<approx> y) = (hRe x \<approx> hRe y \<and> hIm x \<approx> hIm y)"
-unfolding approx_def by (simp add: hcomplex_Infinitesimal_iff)
+ unfolding approx_def by (simp add: hcomplex_Infinitesimal_iff)
lemma HFinite_hRe: "x \<in> HFinite \<Longrightarrow> hRe x \<in> HFinite"
-apply (auto simp add: HFinite_def SReal_def)
-apply (rule_tac x="star_of r" in exI, simp)
-apply (erule order_le_less_trans [OF abs_hRe_le_hcmod])
-done
+ using HFinite_bounded_hcmod abs_ge_zero abs_hRe_le_hcmod by blast
lemma HFinite_hIm: "x \<in> HFinite \<Longrightarrow> hIm x \<in> HFinite"
-apply (auto simp add: HFinite_def SReal_def)
-apply (rule_tac x="star_of r" in exI, simp)
-apply (erule order_le_less_trans [OF abs_hIm_le_hcmod])
-done
+ using HFinite_bounded_hcmod abs_ge_zero abs_hIm_le_hcmod by blast
lemma HFinite_HComplex:
- "\<lbrakk>x \<in> HFinite; y \<in> HFinite\<rbrakk> \<Longrightarrow> HComplex x y \<in> HFinite"
-apply (subgoal_tac "HComplex x 0 + HComplex 0 y \<in> HFinite", simp)
-apply (rule HFinite_add)
-apply (simp add: HFinite_hcmod_iff hcmod_i)
-apply (simp add: HFinite_hcmod_iff hcmod_i)
-done
+ assumes "x \<in> HFinite" "y \<in> HFinite"
+ shows "HComplex x y \<in> HFinite"
+proof -
+ have "HComplex x 0 \<in> HFinite" "HComplex 0 y \<in> HFinite"
+ using HFinite_hcmod_iff assms hcmod_i by fastforce+
+ then have "HComplex x 0 + HComplex 0 y \<in> HFinite"
+ using HFinite_add by blast
+ then show ?thesis
+ by simp
+qed
lemma hcomplex_HFinite_iff:
"(x \<in> HFinite) = (hRe x \<in> HFinite \<and> hIm x \<in> HFinite)"
-apply (safe intro!: HFinite_hRe HFinite_hIm)
-apply (drule (1) HFinite_HComplex, simp)
-done
+ using HFinite_HComplex HFinite_hIm HFinite_hRe by fastforce
lemma hcomplex_HInfinite_iff:
"(x \<in> HInfinite) = (hRe x \<in> HInfinite \<or> hIm x \<in> HInfinite)"
-by (simp add: HInfinite_HFinite_iff hcomplex_HFinite_iff)
+ by (simp add: HInfinite_HFinite_iff hcomplex_HFinite_iff)
lemma hcomplex_of_hypreal_approx_iff [simp]:
- "(hcomplex_of_hypreal x \<approx> hcomplex_of_hypreal z) = (x \<approx> z)"
-by (simp add: hcomplex_approx_iff)
-
-lemma Standard_HComplex:
- "\<lbrakk>x \<in> Standard; y \<in> Standard\<rbrakk> \<Longrightarrow> HComplex x y \<in> Standard"
-by (simp add: HComplex_def)
+ "(hcomplex_of_hypreal x \<approx> hcomplex_of_hypreal z) = (x \<approx> z)"
+ by (simp add: hcomplex_approx_iff)
(* Here we go - easy proof now!! *)
-lemma stc_part_Ex: "x \<in> HFinite \<Longrightarrow> \<exists>t \<in> SComplex. x \<approx> t"
-apply (simp add: hcomplex_HFinite_iff hcomplex_approx_iff)
-apply (rule_tac x="HComplex (st (hRe x)) (st (hIm x))" in bexI)
-apply (simp add: st_approx_self [THEN approx_sym])
-apply (simp add: Standard_HComplex st_SReal [unfolded Reals_eq_Standard])
-done
+lemma stc_part_Ex:
+ assumes "x \<in> HFinite"
+ shows "\<exists>t \<in> SComplex. x \<approx> t"
+proof -
+ let ?t = "HComplex (st (hRe x)) (st (hIm x))"
+ have "?t \<in> SComplex"
+ using HFinite_hIm HFinite_hRe Reals_eq_Standard assms st_SReal by auto
+ moreover have "x \<approx> ?t"
+ by (simp add: HFinite_hIm HFinite_hRe assms hcomplex_approx_iff st_HFinite st_eq_approx)
+ ultimately show ?thesis ..
+qed
lemma stc_part_Ex1: "x \<in> HFinite \<Longrightarrow> \<exists>!t. t \<in> SComplex \<and> x \<approx> t"
-apply (drule stc_part_Ex, safe)
-apply (drule_tac [2] approx_sym, drule_tac [2] approx_sym, drule_tac [2] approx_sym)
-apply (auto intro!: approx_unique_complex)
-done
-
-lemmas hcomplex_of_complex_approx_inverse =
- hcomplex_of_complex_HFinite_diff_Infinitesimal [THEN [2] approx_inverse]
+ using approx_sym approx_unique_complex stc_part_Ex by blast
subsection\<open>Theorems About Monads\<close>
lemma monad_zero_hcmod_iff: "(x \<in> monad 0) = (hcmod x \<in> monad 0)"
-by (simp add: Infinitesimal_monad_zero_iff [symmetric] Infinitesimal_hcmod_iff)
+ by (simp add: Infinitesimal_monad_zero_iff [symmetric] Infinitesimal_hcmod_iff)
subsection\<open>Theorems About Standard Part\<close>
-lemma stc_approx_self: "x \<in> HFinite ==> stc x \<approx> x"
-apply (simp add: stc_def)
-apply (frule stc_part_Ex, safe)
-apply (rule someI2)
-apply (auto intro: approx_sym)
-done
+lemma stc_approx_self: "x \<in> HFinite \<Longrightarrow> stc x \<approx> x"
+ unfolding stc_def
+ by (metis (no_types, lifting) approx_reorient someI_ex stc_part_Ex1)
-lemma stc_SComplex: "x \<in> HFinite ==> stc x \<in> SComplex"
-apply (simp add: stc_def)
-apply (frule stc_part_Ex, safe)
-apply (rule someI2)
-apply (auto intro: approx_sym)
-done
+lemma stc_SComplex: "x \<in> HFinite \<Longrightarrow> stc x \<in> SComplex"
+ unfolding stc_def
+ by (metis (no_types, lifting) SComplex_iff approx_sym someI_ex stc_part_Ex)
-lemma stc_HFinite: "x \<in> HFinite ==> stc x \<in> HFinite"
-by (erule stc_SComplex [THEN Standard_subset_HFinite [THEN subsetD]])
+lemma stc_HFinite: "x \<in> HFinite \<Longrightarrow> stc x \<in> HFinite"
+ by (erule stc_SComplex [THEN Standard_subset_HFinite [THEN subsetD]])
lemma stc_unique: "\<lbrakk>y \<in> SComplex; y \<approx> x\<rbrakk> \<Longrightarrow> stc x = y"
-apply (frule Standard_subset_HFinite [THEN subsetD])
-apply (drule (1) approx_HFinite)
-apply (unfold stc_def)
-apply (rule some_equality)
-apply (auto intro: approx_unique_complex)
-done
+ by (metis SComplex_approx_iff SComplex_iff approx_monad_iff approx_star_of_HFinite stc_SComplex stc_approx_self)
-lemma stc_SComplex_eq [simp]: "x \<in> SComplex ==> stc x = x"
-apply (erule stc_unique)
-apply (rule approx_refl)
-done
-
-lemma stc_hcomplex_of_complex:
- "stc (hcomplex_of_complex x) = hcomplex_of_complex x"
-by auto
+lemma stc_SComplex_eq [simp]: "x \<in> SComplex \<Longrightarrow> stc x = x"
+ by (simp add: stc_unique)
lemma stc_eq_approx:
- "[| x \<in> HFinite; y \<in> HFinite; stc x = stc y |] ==> x \<approx> y"
-by (auto dest!: stc_approx_self elim!: approx_trans3)
+ "\<lbrakk>x \<in> HFinite; y \<in> HFinite; stc x = stc y\<rbrakk> \<Longrightarrow> x \<approx> y"
+ by (auto dest!: stc_approx_self elim!: approx_trans3)
lemma approx_stc_eq:
- "[| x \<in> HFinite; y \<in> HFinite; x \<approx> y |] ==> stc x = stc y"
-by (blast intro: approx_trans approx_trans2 SComplex_approx_iff [THEN iffD1]
- dest: stc_approx_self stc_SComplex)
+ "\<lbrakk>x \<in> HFinite; y \<in> HFinite; x \<approx> y\<rbrakk> \<Longrightarrow> stc x = stc y"
+ by (metis approx_sym approx_trans3 stc_part_Ex1 stc_unique)
lemma stc_eq_approx_iff:
- "[| x \<in> HFinite; y \<in> HFinite|] ==> (x \<approx> y) = (stc x = stc y)"
-by (blast intro: approx_stc_eq stc_eq_approx)
+ "\<lbrakk>x \<in> HFinite; y \<in> HFinite\<rbrakk> \<Longrightarrow> (x \<approx> y) = (stc x = stc y)"
+ by (blast intro: approx_stc_eq stc_eq_approx)
lemma stc_Infinitesimal_add_SComplex:
- "[| x \<in> SComplex; e \<in> Infinitesimal |] ==> stc(x + e) = x"
-apply (erule stc_unique)
-apply (erule Infinitesimal_add_approx_self)
-done
+ "\<lbrakk>x \<in> SComplex; e \<in> Infinitesimal\<rbrakk> \<Longrightarrow> stc(x + e) = x"
+ using Infinitesimal_add_approx_self stc_unique by blast
lemma stc_Infinitesimal_add_SComplex2:
- "[| x \<in> SComplex; e \<in> Infinitesimal |] ==> stc(e + x) = x"
-apply (erule stc_unique)
-apply (erule Infinitesimal_add_approx_self2)
-done
+ "\<lbrakk>x \<in> SComplex; e \<in> Infinitesimal\<rbrakk> \<Longrightarrow> stc(e + x) = x"
+ using Infinitesimal_add_approx_self2 stc_unique by blast
lemma HFinite_stc_Infinitesimal_add:
- "x \<in> HFinite ==> \<exists>e \<in> Infinitesimal. x = stc(x) + e"
-by (blast dest!: stc_approx_self [THEN approx_sym] bex_Infinitesimal_iff2 [THEN iffD2])
+ "x \<in> HFinite \<Longrightarrow> \<exists>e \<in> Infinitesimal. x = stc(x) + e"
+ by (blast dest!: stc_approx_self [THEN approx_sym] bex_Infinitesimal_iff2 [THEN iffD2])
lemma stc_add:
- "[| x \<in> HFinite; y \<in> HFinite |] ==> stc (x + y) = stc(x) + stc(y)"
-by (simp add: stc_unique stc_SComplex stc_approx_self approx_add)
+ "\<lbrakk>x \<in> HFinite; y \<in> HFinite\<rbrakk> \<Longrightarrow> stc (x + y) = stc(x) + stc(y)"
+ by (simp add: stc_unique stc_SComplex stc_approx_self approx_add)
-lemma stc_numeral [simp]: "stc (numeral w) = numeral w"
-by (rule Standard_numeral [THEN stc_SComplex_eq])
+lemma stc_zero: "stc 0 = 0"
+ by simp
-lemma stc_zero [simp]: "stc 0 = 0"
-by simp
+lemma stc_one: "stc 1 = 1"
+ by simp
-lemma stc_one [simp]: "stc 1 = 1"
-by simp
-
-lemma stc_minus: "y \<in> HFinite ==> stc(-y) = -stc(y)"
-by (simp add: stc_unique stc_SComplex stc_approx_self approx_minus)
+lemma stc_minus: "y \<in> HFinite \<Longrightarrow> stc(-y) = -stc(y)"
+ by (simp add: stc_unique stc_SComplex stc_approx_self approx_minus)
lemma stc_diff:
- "[| x \<in> HFinite; y \<in> HFinite |] ==> stc (x-y) = stc(x) - stc(y)"
-by (simp add: stc_unique stc_SComplex stc_approx_self approx_diff)
+ "\<lbrakk>x \<in> HFinite; y \<in> HFinite\<rbrakk> \<Longrightarrow> stc (x-y) = stc(x) - stc(y)"
+ by (simp add: stc_unique stc_SComplex stc_approx_self approx_diff)
lemma stc_mult:
- "[| x \<in> HFinite; y \<in> HFinite |]
- ==> stc (x * y) = stc(x) * stc(y)"
-by (simp add: stc_unique stc_SComplex stc_approx_self approx_mult_HFinite)
+ "\<lbrakk>x \<in> HFinite; y \<in> HFinite\<rbrakk>
+ \<Longrightarrow> stc (x * y) = stc(x) * stc(y)"
+ by (simp add: stc_unique stc_SComplex stc_approx_self approx_mult_HFinite)
-lemma stc_Infinitesimal: "x \<in> Infinitesimal ==> stc x = 0"
-by (simp add: stc_unique mem_infmal_iff)
+lemma stc_Infinitesimal: "x \<in> Infinitesimal \<Longrightarrow> stc x = 0"
+ by (simp add: stc_unique mem_infmal_iff)
-lemma stc_not_Infinitesimal: "stc(x) \<noteq> 0 ==> x \<notin> Infinitesimal"
-by (fast intro: stc_Infinitesimal)
+lemma stc_not_Infinitesimal: "stc(x) \<noteq> 0 \<Longrightarrow> x \<notin> Infinitesimal"
+ by (fast intro: stc_Infinitesimal)
lemma stc_inverse:
- "[| x \<in> HFinite; stc x \<noteq> 0 |]
- ==> stc(inverse x) = inverse (stc x)"
-apply (drule stc_not_Infinitesimal)
-apply (simp add: stc_unique stc_SComplex stc_approx_self approx_inverse)
-done
+ "\<lbrakk>x \<in> HFinite; stc x \<noteq> 0\<rbrakk> \<Longrightarrow> stc(inverse x) = inverse (stc x)"
+ by (simp add: stc_unique stc_SComplex stc_approx_self approx_inverse stc_not_Infinitesimal)
lemma stc_divide [simp]:
- "[| x \<in> HFinite; y \<in> HFinite; stc y \<noteq> 0 |]
- ==> stc(x/y) = (stc x) / (stc y)"
-by (simp add: divide_inverse stc_mult stc_not_Infinitesimal HFinite_inverse stc_inverse)
+ "\<lbrakk>x \<in> HFinite; y \<in> HFinite; stc y \<noteq> 0\<rbrakk>
+ \<Longrightarrow> stc(x/y) = (stc x) / (stc y)"
+ by (simp add: divide_inverse stc_mult stc_not_Infinitesimal HFinite_inverse stc_inverse)
-lemma stc_idempotent [simp]: "x \<in> HFinite ==> stc(stc(x)) = stc(x)"
-by (blast intro: stc_HFinite stc_approx_self approx_stc_eq)
+lemma stc_idempotent [simp]: "x \<in> HFinite \<Longrightarrow> stc(stc(x)) = stc(x)"
+ by (blast intro: stc_HFinite stc_approx_self approx_stc_eq)
lemma HFinite_HFinite_hcomplex_of_hypreal:
- "z \<in> HFinite ==> hcomplex_of_hypreal z \<in> HFinite"
-by (simp add: hcomplex_HFinite_iff)
+ "z \<in> HFinite \<Longrightarrow> hcomplex_of_hypreal z \<in> HFinite"
+ by (simp add: hcomplex_HFinite_iff)
lemma SComplex_SReal_hcomplex_of_hypreal:
- "x \<in> \<real> ==> hcomplex_of_hypreal x \<in> SComplex"
-apply (rule Standard_of_hypreal)
-apply (simp add: Reals_eq_Standard)
-done
+ "x \<in> \<real> \<Longrightarrow> hcomplex_of_hypreal x \<in> SComplex"
+ by (simp add: Reals_eq_Standard)
lemma stc_hcomplex_of_hypreal:
- "z \<in> HFinite ==> stc(hcomplex_of_hypreal z) = hcomplex_of_hypreal (st z)"
-apply (rule stc_unique)
-apply (rule SComplex_SReal_hcomplex_of_hypreal)
-apply (erule st_SReal)
-apply (simp add: hcomplex_of_hypreal_approx_iff st_approx_self)
-done
+ "z \<in> HFinite \<Longrightarrow> stc(hcomplex_of_hypreal z) = hcomplex_of_hypreal (st z)"
+ by (simp add: SComplex_SReal_hcomplex_of_hypreal st_SReal st_approx_self stc_unique)
-(*
-Goal "x \<in> HFinite ==> hcmod(stc x) = st(hcmod x)"
-by (dtac stc_approx_self 1)
-by (auto_tac (claset(),simpset() addsimps [bex_Infinitesimal_iff2 RS sym]));
-
-
-approx_hcmod_add_hcmod
-*)
+lemma hmod_stc_eq:
+ assumes "x \<in> HFinite"
+ shows "hcmod(stc x) = st(hcmod x)"
+ by (metis SReal_hcmod_SComplex approx_HFinite approx_hnorm assms st_unique stc_SComplex_eq stc_eq_approx_iff stc_part_Ex)
lemma Infinitesimal_hcnj_iff [simp]:
- "(hcnj z \<in> Infinitesimal) = (z \<in> Infinitesimal)"
-by (simp add: Infinitesimal_hcmod_iff)
-
-lemma Infinitesimal_hcomplex_of_hypreal_epsilon [simp]:
- "hcomplex_of_hypreal \<epsilon> \<in> Infinitesimal"
-by (simp add: Infinitesimal_hcmod_iff)
+ "(hcnj z \<in> Infinitesimal) \<longleftrightarrow> (z \<in> Infinitesimal)"
+ by (simp add: Infinitesimal_hcmod_iff)
end
--- a/src/HOL/Nonstandard_Analysis/NatStar.thy Tue Apr 30 21:04:08 2019 +0100
+++ b/src/HOL/Nonstandard_Analysis/NatStar.thy Tue Apr 30 21:04:21 2019 +0100
@@ -15,33 +15,49 @@
by (simp add: hypnat_omega_def starfun_def star_of_def Ifun_star_n)
lemma starset_n_Un: "*sn* (\<lambda>n. (A n) \<union> (B n)) = *sn* A \<union> *sn* B"
- apply (simp add: starset_n_def star_n_eq_starfun_whn Un_def)
- apply (rule_tac x=whn in spec, transfer, simp)
- done
+proof -
+ have "\<And>N. Iset ((*f* (\<lambda>n. {x. x \<in> A n \<or> x \<in> B n})) N) =
+ {x. x \<in> Iset ((*f* A) N) \<or> x \<in> Iset ((*f* B) N)}"
+ by transfer simp
+ then show ?thesis
+ by (simp add: starset_n_def star_n_eq_starfun_whn Un_def)
+qed
lemma InternalSets_Un: "X \<in> InternalSets \<Longrightarrow> Y \<in> InternalSets \<Longrightarrow> X \<union> Y \<in> InternalSets"
by (auto simp add: InternalSets_def starset_n_Un [symmetric])
lemma starset_n_Int: "*sn* (\<lambda>n. A n \<inter> B n) = *sn* A \<inter> *sn* B"
- apply (simp add: starset_n_def star_n_eq_starfun_whn Int_def)
- apply (rule_tac x=whn in spec, transfer, simp)
- done
+proof -
+ have "\<And>N. Iset ((*f* (\<lambda>n. {x. x \<in> A n \<and> x \<in> B n})) N) =
+ {x. x \<in> Iset ((*f* A) N) \<and> x \<in> Iset ((*f* B) N)}"
+ by transfer simp
+ then show ?thesis
+ by (simp add: starset_n_def star_n_eq_starfun_whn Int_def)
+qed
lemma InternalSets_Int: "X \<in> InternalSets \<Longrightarrow> Y \<in> InternalSets \<Longrightarrow> X \<inter> Y \<in> InternalSets"
by (auto simp add: InternalSets_def starset_n_Int [symmetric])
lemma starset_n_Compl: "*sn* ((\<lambda>n. - A n)) = - ( *sn* A)"
- apply (simp add: starset_n_def star_n_eq_starfun_whn Compl_eq)
- apply (rule_tac x=whn in spec, transfer, simp)
- done
+proof -
+ have "\<And>N. Iset ((*f* (\<lambda>n. {x. x \<notin> A n})) N) =
+ {x. x \<notin> Iset ((*f* A) N)}"
+ by transfer simp
+ then show ?thesis
+ by (simp add: starset_n_def star_n_eq_starfun_whn Compl_eq)
+qed
lemma InternalSets_Compl: "X \<in> InternalSets \<Longrightarrow> - X \<in> InternalSets"
by (auto simp add: InternalSets_def starset_n_Compl [symmetric])
lemma starset_n_diff: "*sn* (\<lambda>n. (A n) - (B n)) = *sn* A - *sn* B"
- apply (simp add: starset_n_def star_n_eq_starfun_whn set_diff_eq)
- apply (rule_tac x=whn in spec, transfer, simp)
- done
+proof -
+ have "\<And>N. Iset ((*f* (\<lambda>n. {x. x \<in> A n \<and> x \<notin> B n})) N) =
+ {x. x \<in> Iset ((*f* A) N) \<and> x \<notin> Iset ((*f* B) N)}"
+ by transfer simp
+ then show ?thesis
+ by (simp add: starset_n_def star_n_eq_starfun_whn set_diff_eq)
+qed
lemma InternalSets_diff: "X \<in> InternalSets \<Longrightarrow> Y \<in> InternalSets \<Longrightarrow> X - Y \<in> InternalSets"
by (auto simp add: InternalSets_def starset_n_diff [symmetric])
@@ -59,9 +75,7 @@
by (auto simp add: InternalSets_def starset_starset_n_eq)
lemma InternalSets_UNIV_diff: "X \<in> InternalSets \<Longrightarrow> UNIV - X \<in> InternalSets"
- apply (subgoal_tac "UNIV - X = - X")
- apply (auto intro: InternalSets_Compl)
- done
+ by (simp add: InternalSets_Compl diff_eq)
subsection \<open>Nonstandard Extensions of Functions\<close>
@@ -104,10 +118,7 @@
lemma starfun_inverse_real_of_nat_eq:
"N \<in> HNatInfinite \<Longrightarrow> ( *f* (\<lambda>x::nat. inverse (real x))) N = inverse (hypreal_of_hypnat N)"
- apply (rule_tac f1 = inverse in starfun_o2 [THEN subst])
- apply (subgoal_tac "hypreal_of_hypnat N \<noteq> 0")
- apply (simp_all add: zero_less_HNatInfinite starfunNat_real_of_nat)
- done
+ by (metis of_hypnat_def starfun_inverse2)
text \<open>Internal functions -- some redundancy with \<open>*f*\<close> now.\<close>
@@ -144,10 +155,7 @@
lemma starfunNat_inverse_real_of_nat_Infinitesimal [simp]:
"N \<in> HNatInfinite \<Longrightarrow> ( *f* (\<lambda>x. inverse (real x))) N \<in> Infinitesimal"
- apply (rule_tac f1 = inverse in starfun_o2 [THEN subst])
- apply (subgoal_tac "hypreal_of_hypnat N \<noteq> 0")
- apply (simp_all add: zero_less_HNatInfinite starfunNat_real_of_nat)
- done
+ using starfun_inverse_real_of_nat_eq by auto
subsection \<open>Nonstandard Characterization of Induction\<close>
@@ -166,23 +174,22 @@
lemma starP2_eq_iff2: "( *p2* (\<lambda>x y. x = y)) X Y \<longleftrightarrow> X = Y"
by (simp add: starP2_eq_iff)
-lemma nonempty_nat_set_Least_mem: "c \<in> S \<Longrightarrow> (LEAST n. n \<in> S) \<in> S"
- for S :: "nat set"
- by (erule LeastI)
+lemma nonempty_set_star_has_least_lemma:
+ "\<exists>n\<in>S. \<forall>m\<in>S. n \<le> m" if "S \<noteq> {}" for S :: "nat set"
+proof
+ show "\<forall>m\<in>S. (LEAST n. n \<in> S) \<le> m"
+ by (simp add: Least_le)
+ show "(LEAST n. n \<in> S) \<in> S"
+ by (meson that LeastI_ex equals0I)
+qed
lemma nonempty_set_star_has_least:
"\<And>S::nat set star. Iset S \<noteq> {} \<Longrightarrow> \<exists>n \<in> Iset S. \<forall>m \<in> Iset S. n \<le> m"
- apply (transfer empty_def)
- apply (rule_tac x="LEAST n. n \<in> S" in bexI)
- apply (simp add: Least_le)
- apply (rule LeastI_ex, auto)
- done
+ using nonempty_set_star_has_least_lemma by (transfer empty_def)
lemma nonempty_InternalNatSet_has_least: "S \<in> InternalSets \<Longrightarrow> S \<noteq> {} \<Longrightarrow> \<exists>n \<in> S. \<forall>m \<in> S. n \<le> m"
for S :: "hypnat set"
- apply (clarsimp simp add: InternalSets_def starset_n_def)
- apply (erule nonempty_set_star_has_least)
- done
+ by (force simp add: InternalSets_def starset_n_def dest!: nonempty_set_star_has_least)
text \<open>Goldblatt, page 129 Thm 11.3.2.\<close>
lemma internal_induct_lemma:
--- a/src/HOL/Nonstandard_Analysis/Star.thy Tue Apr 30 21:04:08 2019 +0100
+++ b/src/HOL/Nonstandard_Analysis/Star.thy Tue Apr 30 21:04:21 2019 +0100
@@ -82,10 +82,8 @@
text \<open>Nonstandard extension of a function (defined using a
constant sequence) as a special case of an internal function.\<close>
-lemma starfun_n_starfun: "\<forall>n. F n = f \<Longrightarrow> *fn* F = *f* f"
- apply (drule fun_eq_iff [THEN iffD2])
- apply (simp add: starfun_n_def starfun_def star_of_def)
- done
+lemma starfun_n_starfun: "F = (\<lambda>n. f) \<Longrightarrow> *fn* F = *f* f"
+ by (simp add: starfun_n_def starfun_def star_of_def)
text \<open>Prove that \<open>abs\<close> for hypreal is a nonstandard extension of abs for real w/o
use of congruence property (proved after this for general
@@ -94,16 +92,13 @@
Proof now Uses the ultrafilter tactic!\<close>
lemma hrabs_is_starext_rabs: "is_starext abs abs"
- apply (simp add: is_starext_def, safe)
- apply (rule_tac x=x in star_cases)
- apply (rule_tac x=y in star_cases)
- apply (unfold star_n_def, auto)
- apply (rule bexI, rule_tac [2] lemma_starrel_refl)
- apply (rule bexI, rule_tac [2] lemma_starrel_refl)
- apply (fold star_n_def)
- apply (unfold star_abs_def starfun_def star_of_def)
- apply (simp add: Ifun_star_n star_n_eq_iff)
- done
+ proof -
+ have "\<exists>f\<in>Rep_star (star_n h). \<exists>g\<in>Rep_star (star_n k). (star_n k = \<bar>star_n h\<bar>) = (\<forall>\<^sub>F n in \<U>. (g n::'a) = \<bar>f n\<bar>)"
+ for x y :: "'a star" and h k
+ by (metis (full_types) Rep_star_star_n star_n_abs star_n_eq_iff)
+ then show ?thesis
+ unfolding is_starext_def by (metis star_cases)
+qed
text \<open>Nonstandard extension of functions.\<close>
@@ -153,34 +148,32 @@
lemma starfun_Id [simp]: "\<And>x. ( *f* (\<lambda>x. x)) x = x"
by transfer (rule refl)
-text \<open>This is trivial, given \<open>starfun_Id\<close>.\<close>
-lemma starfun_Idfun_approx: "x \<approx> star_of a \<Longrightarrow> ( *f* (\<lambda>x. x)) x \<approx> star_of a"
- by (simp only: starfun_Id)
-
text \<open>The Star-function is a (nonstandard) extension of the function.\<close>
lemma is_starext_starfun: "is_starext ( *f* f) f"
- apply (auto simp: is_starext_def)
- apply (rule_tac x = x in star_cases)
- apply (rule_tac x = y in star_cases)
- apply (auto intro!: bexI [OF _ Rep_star_star_n] simp: starfun star_n_eq_iff)
- done
+proof -
+ have "\<exists>X\<in>Rep_star x. \<exists>Y\<in>Rep_star y. (y = (*f* f) x) = (\<forall>\<^sub>F n in \<U>. Y n = f (X n))"
+ for x y
+ by (metis (mono_tags) Rep_star_star_n star_cases star_n_eq_iff starfun_star_n)
+ then show ?thesis
+ by (auto simp: is_starext_def)
+qed
text \<open>Any nonstandard extension is in fact the Star-function.\<close>
-lemma is_starfun_starext: "is_starext F f \<Longrightarrow> F = *f* f"
- apply (simp add: is_starext_def)
- apply (rule ext)
- apply (rule_tac x = x in star_cases)
- apply (drule_tac x = x in spec)
- apply (drule_tac x = "( *f* f) x" in spec)
- apply (auto simp add: starfun_star_n)
- apply (simp add: star_n_eq_iff [symmetric])
- apply (simp add: starfun_star_n [of f, symmetric])
- done
+lemma is_starfun_starext:
+ assumes "is_starext F f"
+ shows "F = *f* f"
+ proof -
+ have "F x = (*f* f) x"
+ if "\<forall>x y. \<exists>X\<in>Rep_star x. \<exists>Y\<in>Rep_star y. (y = F x) = (\<forall>\<^sub>F n in \<U>. Y n = f (X n))" for x
+ by (metis that mem_Rep_star_iff star_n_eq_iff starfun_star_n)
+ with assms show ?thesis
+ by (force simp add: is_starext_def)
+qed
lemma is_starext_starfun_iff: "is_starext F f \<longleftrightarrow> F = *f* f"
by (blast intro: is_starfun_starext is_starext_starfun)
-text \<open>Extented function has same solution as its standard version
+text \<open>Extended function has same solution as its standard version
for real arguments. i.e they are the same for all real arguments.\<close>
lemma starfun_eq: "( *f* f) (star_of a) = star_of (f a)"
by (rule starfun_star_of)
@@ -199,9 +192,7 @@
"( *f* f) x \<approx> l \<Longrightarrow> ( *f* g) x \<approx> m \<Longrightarrow> l \<in> HFinite \<Longrightarrow> m \<in> HFinite \<Longrightarrow>
( *f* (\<lambda>x. f x * g x)) x \<approx> l * m"
for l m :: "'a::real_normed_algebra star"
- apply (drule (3) approx_mult_HFinite)
- apply (auto intro: approx_HFinite [OF _ approx_sym])
- done
+ using approx_mult_HFinite by auto
lemma starfun_add_approx: "( *f* f) x \<approx> l \<Longrightarrow> ( *f* g) x \<approx> m \<Longrightarrow> ( *f* (%x. f x + g x)) x \<approx> l + m"
by (auto intro: approx_add)
@@ -259,35 +250,48 @@
star_of_nat_def starfun_star_n star_n_inverse star_n_less)
lemma HNatInfinite_inverse_Infinitesimal [simp]:
- "n \<in> HNatInfinite \<Longrightarrow> inverse (hypreal_of_hypnat n) \<in> Infinitesimal"
- apply (cases n)
- apply (auto simp: of_hypnat_def starfun_star_n star_n_inverse
- HNatInfinite_FreeUltrafilterNat_iff Infinitesimal_FreeUltrafilterNat_iff2)
- apply (drule_tac x = "Suc m" in spec)
- apply (auto elim!: eventually_mono)
- done
+ assumes "n \<in> HNatInfinite"
+ shows "inverse (hypreal_of_hypnat n) \<in> Infinitesimal"
+proof (cases n)
+ case (star_n X)
+ then have *: "\<And>k. \<forall>\<^sub>F n in \<U>. k < X n"
+ using HNatInfinite_FreeUltrafilterNat assms by blast
+ have "\<forall>\<^sub>F n in \<U>. inverse (real (X n)) < inverse (1 + real m)" for m
+ using * [of "Suc m"] by (auto elim!: eventually_mono)
+ then show ?thesis
+ using star_n by (auto simp: of_hypnat_def starfun_star_n star_n_inverse Infinitesimal_FreeUltrafilterNat_iff2)
+qed
lemma approx_FreeUltrafilterNat_iff:
"star_n X \<approx> star_n Y \<longleftrightarrow> (\<forall>r>0. eventually (\<lambda>n. norm (X n - Y n) < r) \<U>)"
- apply (subst approx_minus_iff)
- apply (rule mem_infmal_iff [THEN subst])
- apply (simp add: star_n_diff)
- apply (simp add: Infinitesimal_FreeUltrafilterNat_iff)
- done
+ (is "?lhs = ?rhs")
+proof -
+ have "?lhs = (star_n X - star_n Y \<approx> 0)"
+ using approx_minus_iff by blast
+ also have "... = ?rhs"
+ by (metis (full_types) Infinitesimal_FreeUltrafilterNat_iff mem_infmal_iff star_n_diff)
+ finally show ?thesis .
+qed
lemma approx_FreeUltrafilterNat_iff2:
"star_n X \<approx> star_n Y \<longleftrightarrow> (\<forall>m. eventually (\<lambda>n. norm (X n - Y n) < inverse (real (Suc m))) \<U>)"
- apply (subst approx_minus_iff)
- apply (rule mem_infmal_iff [THEN subst])
- apply (simp add: star_n_diff)
- apply (simp add: Infinitesimal_FreeUltrafilterNat_iff2)
- done
+ (is "?lhs = ?rhs")
+proof -
+ have "?lhs = (star_n X - star_n Y \<approx> 0)"
+ using approx_minus_iff by blast
+ also have "... = ?rhs"
+ by (metis (full_types) Infinitesimal_FreeUltrafilterNat_iff2 mem_infmal_iff star_n_diff)
+ finally show ?thesis .
+qed
lemma inj_starfun: "inj starfun"
- apply (rule inj_onI)
- apply (rule ext, rule ccontr)
- apply (drule_tac x = "star_n (\<lambda>n. xa)" in fun_cong)
- apply (auto simp add: starfun star_n_eq_iff FreeUltrafilterNat.proper)
- done
+proof (rule inj_onI)
+ show "\<phi> = \<psi>" if eq: "*f* \<phi> = *f* \<psi>" for \<phi> \<psi> :: "'a \<Rightarrow> 'b"
+ proof (rule ext, rule ccontr)
+ show False
+ if "\<phi> x \<noteq> \<psi> x" for x
+ by (metis eq that star_of_inject starfun_eq)
+ qed
+qed
end
--- a/src/HOL/Nonstandard_Analysis/StarDef.thy Tue Apr 30 21:04:08 2019 +0100
+++ b/src/HOL/Nonstandard_Analysis/StarDef.thy Tue Apr 30 21:04:21 2019 +0100
@@ -14,11 +14,8 @@
where "\<U> = (SOME U. freeultrafilter U)"
lemma freeultrafilter_FreeUltrafilterNat: "freeultrafilter \<U>"
- apply (unfold FreeUltrafilterNat_def)
- apply (rule someI_ex)
- apply (rule freeultrafilter_Ex)
- apply (rule infinite_UNIV_nat)
- done
+ unfolding FreeUltrafilterNat_def
+ by (simp add: freeultrafilter_Ex someI_ex)
interpretation FreeUltrafilterNat: freeultrafilter \<U>
by (rule freeultrafilter_FreeUltrafilterNat)
@@ -42,16 +39,10 @@
by (cases x) (auto simp: star_n_def star_def elim: quotientE)
lemma all_star_eq: "(\<forall>x. P x) \<longleftrightarrow> (\<forall>X. P (star_n X))"
- apply auto
- apply (rule_tac x = x in star_cases)
- apply simp
- done
+ by (metis star_cases)
lemma ex_star_eq: "(\<exists>x. P x) \<longleftrightarrow> (\<exists>X. P (star_n X))"
- apply auto
- apply (rule_tac x=x in star_cases)
- apply auto
- done
+ by (metis star_cases)
text \<open>Proving that \<^term>\<open>starrel\<close> is an equivalence relation.\<close>
@@ -599,12 +590,16 @@
subsection \<open>Ordering and lattice classes\<close>
instance star :: (order) order
- apply intro_classes
- apply (transfer, rule less_le_not_le)
- apply (transfer, rule order_refl)
- apply (transfer, erule (1) order_trans)
- apply (transfer, erule (1) order_antisym)
- done
+proof
+ show "\<And>x y::'a star. (x < y) = (x \<le> y \<and> \<not> y \<le> x)"
+ by transfer (rule less_le_not_le)
+ show "\<And>x::'a star. x \<le> x"
+ by transfer (rule order_refl)
+ show "\<And>x y z::'a star. \<lbrakk>x \<le> y; y \<le> z\<rbrakk> \<Longrightarrow> x \<le> z"
+ by transfer (rule order_trans)
+ show "\<And>x y::'a star. \<lbrakk>x \<le> y; y \<le> x\<rbrakk> \<Longrightarrow> x = y"
+ by transfer (rule order_antisym)
+qed
instantiation star :: (semilattice_inf) semilattice_inf
begin
@@ -639,16 +634,12 @@
by (intro_classes, transfer, rule linorder_linear)
lemma star_max_def [transfer_unfold]: "max = *f2* max"
- apply (rule ext, rule ext)
- apply (unfold max_def, transfer, fold max_def)
- apply (rule refl)
- done
+ unfolding max_def
+ by (intro ext, transfer, simp)
lemma star_min_def [transfer_unfold]: "min = *f2* min"
- apply (rule ext, rule ext)
- apply (unfold min_def, transfer, fold min_def)
- apply (rule refl)
- done
+ unfolding min_def
+ by (intro ext, transfer, simp)
lemma Standard_max [simp]: "x \<in> Standard \<Longrightarrow> y \<in> Standard \<Longrightarrow> max x y \<in> Standard"
by (simp add: star_max_def)
@@ -928,10 +919,9 @@
by (erule finite_induct) simp_all
instance star :: (finite) finite
- apply intro_classes
- apply (subst starset_UNIV [symmetric])
- apply (subst starset_finite [OF finite])
- apply (rule finite_imageI [OF finite])
- done
+proof intro_classes
+ show "finite (UNIV::'a star set)"
+ by (metis starset_UNIV finite finite_imageI starset_finite)
+qed
end
--- a/src/HOL/Zorn.thy Tue Apr 30 21:04:08 2019 +0100
+++ b/src/HOL/Zorn.thy Tue Apr 30 21:04:21 2019 +0100
@@ -475,6 +475,10 @@
shows "Chains r = {C. pred_on.chain UNIV (\<lambda>x y. (x, y) \<in> r) C}"
using assms Chains_subset Chains_subset' by blast
+lemma Chains_relation_of:
+ assumes "C \<in> Chains (relation_of P A)" shows "C \<subseteq> A"
+ using assms unfolding Chains_def relation_of_def by auto
+
lemma pairwise_chain_Union:
assumes P: "\<And>S. S \<in> \<C> \<Longrightarrow> pairwise R S" and "chain\<^sub>\<subseteq> \<C>"
shows "pairwise R (\<Union>\<C>)"