author | wenzelm |

Thu Jun 14 10:38:48 2007 +0200 (2007-06-14) | |

changeset 23383 | 5460951833fa |

parent 23382 | 0459ab90389a |

child 23384 | 925b381b4eea |

tuned proofs: avoid implicit prems;

src/HOL/Algebra/AbelCoset.thy | file | annotate | diff | revisions | |

src/HOL/Algebra/Ideal.thy | file | annotate | diff | revisions |

1.1 --- a/src/HOL/Algebra/AbelCoset.thy Thu Jun 14 09:54:14 2007 +0200 1.2 +++ b/src/HOL/Algebra/AbelCoset.thy Thu Jun 14 10:38:48 2007 +0200 1.3 @@ -712,7 +712,7 @@ 1.4 and repr: "H +> x = H +> y" 1.5 shows "y \<in> H +> x" 1.6 by (rule group.repr_independenceD [OF a_group a_subgroup, 1.7 - folded a_r_coset_def, simplified monoid_record_simps]) 1.8 + folded a_r_coset_def, simplified monoid_record_simps]) (rule ycarr, rule repr) 1.9 1.10 1.11 subsection {* Lemmas for the Set of Right Cosets *} 1.12 @@ -731,7 +731,7 @@ 1.13 and Bcarr: "B \<subseteq> carrier G" 1.14 shows "A <+> B \<subseteq> carrier G" 1.15 by (rule monoid.set_mult_closed [OF a_monoid, 1.16 - folded set_add_def, simplified monoid_record_simps]) 1.17 + folded set_add_def, simplified monoid_record_simps]) (rule Acarr, rule Bcarr) 1.18 1.19 lemma (in abelian_group) add_additive_subgroups: 1.20 assumes subH: "additive_subgroup H G"

2.1 --- a/src/HOL/Algebra/Ideal.thy Thu Jun 14 09:54:14 2007 +0200 2.2 +++ b/src/HOL/Algebra/Ideal.thy Thu Jun 14 10:38:48 2007 +0200 2.3 @@ -67,7 +67,7 @@ 2.4 2.5 lemma (in maximalideal) is_maximalideal: 2.6 shows "maximalideal I R" 2.7 -by - 2.8 +by fact 2.9 2.10 lemma maximalidealI: 2.11 includes ideal 2.12 @@ -673,17 +673,9 @@ 2.13 lemma (in ideal) primeidealCE: 2.14 includes cring 2.15 assumes notprime: "\<not> primeideal I R" 2.16 - and elim1: "carrier R = I \<Longrightarrow> P" 2.17 - and elim2: "(\<exists>a b. a \<in> carrier R \<and> b \<in> carrier R \<and> a \<otimes> b \<in> I \<and> a \<notin> I \<and> b \<notin> I) \<Longrightarrow> P" 2.18 - shows "P" 2.19 -proof - 2.20 - from notprime 2.21 - have "carrier R = I \<or> (\<exists>a b. a \<in> carrier R \<and> b \<in> carrier R \<and> a \<otimes> b \<in> I \<and> a \<notin> I \<and> b \<notin> I)" 2.22 - by (intro primeidealCD) 2.23 - thus "P" 2.24 - apply (rule disjE) 2.25 - by (erule elim1, erule elim2) 2.26 -qed 2.27 + obtains "carrier R = I" 2.28 + | "\<exists>a b. a \<in> carrier R \<and> b \<in> carrier R \<and> a \<otimes> b \<in> I \<and> a \<notin> I \<and> b \<notin> I" 2.29 + using primeidealCD [OF R.is_cring notprime] by blast 2.30 2.31 text {* If @{text "{\<zero>}"} is a prime ideal of a commutative ring, the ring is a domain *} 2.32 lemma (in cring) zeroprimeideal_domainI: 2.33 @@ -790,21 +782,21 @@ 2.34 by fast 2.35 def J \<equiv> "{x\<in>carrier R. a \<otimes> x \<in> I}" 2.36 2.37 - from acarr 2.38 - have idealJ: "ideal J R" by (unfold J_def, intro helper_max_prime) 2.39 + from R.is_cring and acarr 2.40 + have idealJ: "ideal J R" unfolding J_def by (rule helper_max_prime) 2.41 2.42 have IsubJ: "I \<subseteq> J" 2.43 proof 2.44 fix x 2.45 assume xI: "x \<in> I" 2.46 from this and acarr 2.47 - have "a \<otimes> x \<in> I" by (intro I_l_closed) 2.48 + have "a \<otimes> x \<in> I" by (intro I_l_closed) 2.49 from xI[THEN a_Hcarr] this 2.50 - show "x \<in> J" by (unfold J_def, fast) 2.51 + show "x \<in> J" unfolding J_def by fast 2.52 qed 2.53 2.54 from abI and acarr bcarr 2.55 - have "b \<in> J" by (unfold J_def, fast) 2.56 + have "b \<in> J" unfolding J_def by fast 2.57 from bnI and this 2.58 have JnI: "J \<noteq> I" by fast 2.59 from acarr 2.60 @@ -812,7 +804,7 @@ 2.61 from this and anI 2.62 have "a \<otimes> \<one> \<notin> I" by simp 2.63 from one_closed and this 2.64 - have "\<one> \<notin> J" by (unfold J_def, fast) 2.65 + have "\<one> \<notin> J" unfolding J_def by fast 2.66 hence Jncarr: "J \<noteq> carrier R" by fast 2.67 2.68 interpret ideal ["J" "R"] by (rule idealJ)