src/HOL/Algebra/Ideal.thy

--- a/src/HOL/Algebra/Ideal.thy	Thu Jun 21 17:28:50 2007 +0200
+++ b/src/HOL/Algebra/Ideal.thy	Thu Jun 21 17:28:53 2007 +0200
@@ -18,9 +18,9 @@
 
 interpretation ideal \<subseteq> abelian_subgroup I R
 apply (intro abelian_subgroupI3 abelian_group.intro)
-  apply (rule ideal.axioms, assumption)
- apply (rule abelian_group.axioms, rule ring.axioms, rule ideal.axioms, assumption)
-apply (rule abelian_group.axioms, rule ring.axioms, rule ideal.axioms, assumption)
+  apply (rule ideal.axioms, rule ideal_axioms)
+ apply (rule abelian_group.axioms, rule ring.axioms, rule ideal.axioms, rule ideal_axioms)
+apply (rule abelian_group.axioms, rule ring.axioms, rule ideal.axioms, rule ideal_axioms)
 done
 
 lemma (in ideal) is_ideal:
@@ -33,7 +33,12 @@
       and I_l_closed: "\<And>a x. \<lbrakk>a \<in> I; x \<in> carrier R\<rbrakk> \<Longrightarrow> x \<otimes> a \<in> I"
       and I_r_closed: "\<And>a x. \<lbrakk>a \<in> I; x \<in> carrier R\<rbrakk> \<Longrightarrow> a \<otimes> x \<in> I"
   shows "ideal I R"
-by (intro ideal.intro ideal_axioms.intro additive_subgroupI, assumption+)
+  apply (intro ideal.intro ideal_axioms.intro additive_subgroupI)
+     apply (rule a_subgroup)
+    apply (rule is_ring)
+   apply (erule (1) I_l_closed)
+  apply (erule (1) I_r_closed)
+  done
 
 
 subsection {* Ideals Generated by a Subset of @{term [locale=ring] "carrier R"} *}
@@ -56,7 +61,7 @@
   includes ideal
   assumes generate: "\<exists>i \<in> carrier R. I = Idl {i}"
   shows "principalideal I R"
-by (intro principalideal.intro principalideal_axioms.intro, assumption+)
+  by (intro principalideal.intro principalideal_axioms.intro) (rule is_ideal, rule generate)
 
 
 subsection {* Maximal Ideals *}
@@ -74,7 +79,8 @@
   assumes I_notcarr: "carrier R \<noteq> I"
      and I_maximal: "\<And>J. \<lbrakk>ideal J R; I \<subseteq> J; J \<subseteq> carrier R\<rbrakk> \<Longrightarrow> J = I \<or> J = carrier R"
   shows "maximalideal I R"
-by (intro maximalideal.intro maximalideal_axioms.intro, assumption+)
+  by (intro maximalideal.intro maximalideal_axioms.intro)
+    (rule is_ideal, rule I_notcarr, rule I_maximal)
 
 
 subsection {* Prime Ideals *}
@@ -93,7 +99,8 @@
   assumes I_notcarr: "carrier R \<noteq> I"
       and I_prime: "\<And>a b. \<lbrakk>a \<in> carrier R; b \<in> carrier R; a \<otimes> b \<in> I\<rbrakk> \<Longrightarrow> a \<in> I \<or> b \<in> I"
   shows "primeideal I R"
-by (intro primeideal.intro primeideal_axioms.intro, assumption+)
+  by (intro primeideal.intro primeideal_axioms.intro)
+    (rule is_ideal, rule is_cring, rule I_notcarr, rule I_prime)
 
 lemma primeidealI2:
   includes additive_subgroup I R
@@ -104,8 +111,12 @@
       and I_prime: "\<And>a b. \<lbrakk>a \<in> carrier R; b \<in> carrier R; a \<otimes> b \<in> I\<rbrakk> \<Longrightarrow> a \<in> I \<or> b \<in> I"
   shows "primeideal I R"
 apply (intro_locales)
- apply (intro ideal_axioms.intro, assumption+)
-apply (intro primeideal_axioms.intro, assumption+)
+ apply (intro ideal_axioms.intro)
+  apply (erule (1) I_l_closed)
+ apply (erule (1) I_r_closed)
+apply (intro primeideal_axioms.intro)
+ apply (rule I_notcarr)
+apply (erule (2) I_prime)
 done
 
 
@@ -135,7 +146,7 @@
  shows "primeideal {\<zero>} R"
 apply (intro primeidealI)
    apply (rule zeroideal)
-  apply (rule domain.axioms,assumption)
+  apply (rule domain.axioms, rule domain_axioms)
  defer 1
  apply (simp add: integral)
 proof (rule ccontr, simp)
@@ -283,7 +294,7 @@
   apply (rule add_additive_subgroups)
    apply (intro ideal.axioms[OF idealI])
   apply (intro ideal.axioms[OF idealJ])
- apply assumption
+ apply (rule is_ring)
 apply (rule ideal_axioms.intro)
  apply (simp add: set_add_defs, clarsimp) defer 1
  apply (simp add: set_add_defs, clarsimp) defer 1
@@ -518,8 +529,8 @@
   apply (rule genideal_ideal, fast intro: icarr)
  apply (rule genideal_self', fast intro: icarr)
 apply (intro genideal_minimal)
- apply (rule cgenideal_ideal, assumption)
-apply (simp, rule cgenideal_self, assumption)
+ apply (rule cgenideal_ideal [OF icarr])
+apply (simp, rule cgenideal_self [OF icarr])
 done
 
 lemma (in cring) cgenideal_eq_rcos: