tuned proofs: avoid implicit prems;
authorwenzelm
Thu Jun 14 10:38:48 2007 +0200 (2007-06-14)
changeset 233835460951833fa
parent 23382 0459ab90389a
child 23384 925b381b4eea
tuned proofs: avoid implicit prems;
src/HOL/Algebra/AbelCoset.thy
src/HOL/Algebra/Ideal.thy
     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)