# HG changeset patch
# User wenzelm
# Date 1182439733 -7200
# Node ID 9953ff53cc648d052ff488b4fbabd7b52405da72
# Parent  11728d83794cc65dadc33dad4e603b43573b9aea
tuned proofs -- avoid implicit prems;

diff -r 11728d83794c -r 9953ff53cc64 src/HOL/Algebra/AbelCoset.thy
--- a/src/HOL/Algebra/AbelCoset.thy	Thu Jun 21 17:28:50 2007 +0200
+++ b/src/HOL/Algebra/AbelCoset.thy	Thu Jun 21 17:28:53 2007 +0200
@@ -700,12 +700,14 @@
 qed
 
 lemma (in abelian_subgroup) a_repr_independence':
-  assumes "y \<in> H +> x"
-      and "x \<in> carrier G"
+  assumes y: "y \<in> H +> x"
+      and xcarr: "x \<in> carrier G"
   shows "H +> x = H +> y"
-apply (rule a_repr_independence, assumption+)
-apply (rule a_subgroup)
-done
+  apply (rule a_repr_independence)
+    apply (rule y)
+   apply (rule xcarr)
+  apply (rule a_subgroup)
+  done
 
 lemma (in abelian_subgroup) a_repr_independenceD:
   assumes ycarr: "y \<in> carrier G"
diff -r 11728d83794c -r 9953ff53cc64 src/HOL/Algebra/Coset.thy
--- a/src/HOL/Algebra/Coset.thy	Thu Jun 21 17:28:50 2007 +0200
+++ b/src/HOL/Algebra/Coset.thy	Thu Jun 21 17:28:53 2007 +0200
@@ -138,10 +138,13 @@
   assumes hH: "h \<in> H"
   shows "H #> h = H"
   apply (unfold r_coset_def)
-  apply rule apply rule
-  apply clarsimp
-  apply (intro subgroup.m_closed)
-  apply assumption+
+  apply rule
+   apply rule
+   apply clarsimp
+   apply (intro subgroup.m_closed)
+     apply (rule is_subgroup)
+    apply assumption
+   apply (rule hH)
   apply rule
   apply simp
 proof -
diff -r 11728d83794c -r 9953ff53cc64 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:
diff -r 11728d83794c -r 9953ff53cc64 src/HOL/Algebra/Lattice.thy
--- a/src/HOL/Algebra/Lattice.thy	Thu Jun 21 17:28:50 2007 +0200
+++ b/src/HOL/Algebra/Lattice.thy	Thu Jun 21 17:28:53 2007 +0200
@@ -257,7 +257,9 @@
 	proof
           have y': "y \<in> Upper L A"
             apply (rule subsetD [where A = "Upper L (insert x A)"])
-            apply (rule Upper_antimono) apply clarify apply assumption
+             apply (rule Upper_antimono)
+	     apply blast
+	    apply (rule y)
             done
           assume "z = a"
           with y' least_a show ?thesis by (fast dest: least_le)
@@ -299,7 +301,9 @@
           proof
             have y': "y \<in> Upper L A"
 	      apply (rule subsetD [where A = "Upper L (insert x A)"])
-	      apply (rule Upper_antimono) apply clarify apply assumption
+	      apply (rule Upper_antimono)
+	       apply blast
+	      apply (rule y)
 	      done
             assume "z = a"
             with y' least_a show ?thesis by (fast dest: least_le)
@@ -483,7 +487,9 @@
 	proof
           have y': "y \<in> Lower L A"
             apply (rule subsetD [where A = "Lower L (insert x A)"])
-            apply (rule Lower_antimono) apply clarify apply assumption
+            apply (rule Lower_antimono)
+	     apply blast
+	    apply (rule y)
             done
           assume "z = a"
           with y' greatest_a show ?thesis by (fast dest: greatest_le)
@@ -525,7 +531,9 @@
           proof
             have y': "y \<in> Lower L A"
 	      apply (rule subsetD [where A = "Lower L (insert x A)"])
-	      apply (rule Lower_antimono) apply clarify apply assumption
+	      apply (rule Lower_antimono)
+	       apply blast
+	      apply (rule y)
 	      done
             assume "z = a"
             with y' greatest_a show ?thesis by (fast dest: greatest_le)
@@ -699,7 +707,7 @@
       ultimately show ?thesis by blast
     qed
   qed
-qed (assumption | rule total_order_axioms.intro)+
+qed (rule total total_order_axioms.intro)+
 
 
 subsection {* Complete lattices *}
@@ -721,7 +729,7 @@
 proof intro_locales
   show "lattice_axioms L"
     by (rule lattice_axioms.intro) (blast intro: sup_exists inf_exists)+
-qed (assumption | rule complete_lattice_axioms.intro)+
+qed (rule complete_lattice_axioms.intro sup_exists inf_exists | assumption)+
 
 constdefs (structure L)
   top :: "_ => 'a" ("\<top>\<index>")
diff -r 11728d83794c -r 9953ff53cc64 src/HOL/Algebra/QuotRing.thy
--- a/src/HOL/Algebra/QuotRing.thy	Thu Jun 21 17:28:50 2007 +0200
+++ b/src/HOL/Algebra/QuotRing.thy	Thu Jun 21 17:28:53 2007 +0200
@@ -4,17 +4,17 @@
   Author:    Stephan Hohe
 *)
 
+header {* Quotient Rings *}
+
 theory QuotRing
 imports RingHom
 begin
 
-
-section {* Quotient Rings *}
-
 subsection {* Multiplication on Cosets *}
 
 constdefs (structure R)
-  rcoset_mult :: "[('a, _) ring_scheme, 'a set, 'a set, 'a set] \<Rightarrow> 'a set"   ("[mod _:] _ \<Otimes>\<index> _" [81,81,81] 80)
+  rcoset_mult :: "[('a, _) ring_scheme, 'a set, 'a set, 'a set] \<Rightarrow> 'a set"
+    ("[mod _:] _ \<Otimes>\<index> _" [81,81,81] 80)
   "rcoset_mult R I A B \<equiv> \<Union>a\<in>A. \<Union>b\<in>B. I +> (a \<otimes> b)"
 
 
@@ -171,8 +171,9 @@
   shows "ring_hom_cring R (R Quot I) (op +> I)"
 apply (rule ring_hom_cringI)
   apply (rule rcos_ring_hom_ring)
- apply assumption
-apply (rule quotient_is_cring, assumption)
+ apply (rule R.is_cring)
+apply (rule quotient_is_cring)
+apply (rule R.is_cring)
 done
 
 
diff -r 11728d83794c -r 9953ff53cc64 src/HOL/Algebra/RingHom.thy
--- a/src/HOL/Algebra/RingHom.thy	Thu Jun 21 17:28:50 2007 +0200
+++ b/src/HOL/Algebra/RingHom.thy	Thu Jun 21 17:28:53 2007 +0200
@@ -46,7 +46,10 @@
   shows "ring_hom_ring R S h"
 apply unfold_locales
 apply (unfold ring_hom_def, safe)
-   apply (simp add: hom_closed Pi_def, assumption+)
+   apply (simp add: hom_closed Pi_def)
+  apply (erule (1) compatible_mult)
+ apply (erule (1) compatible_add)
+apply (rule compatible_one)
 done
 
 lemma ring_hom_ringI2:
@@ -67,13 +70,16 @@
 apply (intro ring_hom_ring.intro ring_hom_ring_axioms.intro, assumption+)
 apply (insert group_hom.homh[OF a_group_hom])
 apply (unfold hom_def ring_hom_def, simp)
-apply (safe, assumption+)
+apply safe
+apply (erule (1) compatible_mult)
+apply (rule compatible_one)
 done
 
 lemma ring_hom_cringI:
   includes ring_hom_ring R S h + cring R + cring S
   shows "ring_hom_cring R S h"
-by (intro ring_hom_cring.intro ring_hom_cring_axioms.intro, assumption+, rule homh)
+  by (intro ring_hom_cring.intro ring_hom_cring_axioms.intro)
+    (rule R.is_cring, rule S.is_cring, rule homh)
 
 
 subsection {* The kernel of a ring homomorphism *}
diff -r 11728d83794c -r 9953ff53cc64 src/HOL/Unix/Unix.thy
--- a/src/HOL/Unix/Unix.thy	Thu Jun 21 17:28:50 2007 +0200
+++ b/src/HOL/Unix/Unix.thy	Thu Jun 21 17:28:53 2007 +0200
@@ -570,7 +570,7 @@
   using trans
 proof induct
   case nil
-  show ?case by assumption
+  show ?case by (rule nil.prems)
 next
   case (cons root x root' xs root'')
   note P = `\<forall>x \<in> set (x # xs). P x`