tuned proofs -- avoid implicit prems;
authorwenzelm
Thu Jun 21 17:28:53 2007 +0200 (2007-06-21)
changeset 234639953ff53cc64
parent 23462 11728d83794c
child 23464 bc2563c37b1a
tuned proofs -- avoid implicit prems;
src/HOL/Algebra/AbelCoset.thy
src/HOL/Algebra/Coset.thy
src/HOL/Algebra/Ideal.thy
src/HOL/Algebra/Lattice.thy
src/HOL/Algebra/QuotRing.thy
src/HOL/Algebra/RingHom.thy
src/HOL/Unix/Unix.thy
     1.1 --- a/src/HOL/Algebra/AbelCoset.thy	Thu Jun 21 17:28:50 2007 +0200
     1.2 +++ b/src/HOL/Algebra/AbelCoset.thy	Thu Jun 21 17:28:53 2007 +0200
     1.3 @@ -700,12 +700,14 @@
     1.4  qed
     1.5  
     1.6  lemma (in abelian_subgroup) a_repr_independence':
     1.7 -  assumes "y \<in> H +> x"
     1.8 -      and "x \<in> carrier G"
     1.9 +  assumes y: "y \<in> H +> x"
    1.10 +      and xcarr: "x \<in> carrier G"
    1.11    shows "H +> x = H +> y"
    1.12 -apply (rule a_repr_independence, assumption+)
    1.13 -apply (rule a_subgroup)
    1.14 -done
    1.15 +  apply (rule a_repr_independence)
    1.16 +    apply (rule y)
    1.17 +   apply (rule xcarr)
    1.18 +  apply (rule a_subgroup)
    1.19 +  done
    1.20  
    1.21  lemma (in abelian_subgroup) a_repr_independenceD:
    1.22    assumes ycarr: "y \<in> carrier G"
     2.1 --- a/src/HOL/Algebra/Coset.thy	Thu Jun 21 17:28:50 2007 +0200
     2.2 +++ b/src/HOL/Algebra/Coset.thy	Thu Jun 21 17:28:53 2007 +0200
     2.3 @@ -138,10 +138,13 @@
     2.4    assumes hH: "h \<in> H"
     2.5    shows "H #> h = H"
     2.6    apply (unfold r_coset_def)
     2.7 -  apply rule apply rule
     2.8 -  apply clarsimp
     2.9 -  apply (intro subgroup.m_closed)
    2.10 -  apply assumption+
    2.11 +  apply rule
    2.12 +   apply rule
    2.13 +   apply clarsimp
    2.14 +   apply (intro subgroup.m_closed)
    2.15 +     apply (rule is_subgroup)
    2.16 +    apply assumption
    2.17 +   apply (rule hH)
    2.18    apply rule
    2.19    apply simp
    2.20  proof -
     3.1 --- a/src/HOL/Algebra/Ideal.thy	Thu Jun 21 17:28:50 2007 +0200
     3.2 +++ b/src/HOL/Algebra/Ideal.thy	Thu Jun 21 17:28:53 2007 +0200
     3.3 @@ -18,9 +18,9 @@
     3.4  
     3.5  interpretation ideal \<subseteq> abelian_subgroup I R
     3.6  apply (intro abelian_subgroupI3 abelian_group.intro)
     3.7 -  apply (rule ideal.axioms, assumption)
     3.8 - apply (rule abelian_group.axioms, rule ring.axioms, rule ideal.axioms, assumption)
     3.9 -apply (rule abelian_group.axioms, rule ring.axioms, rule ideal.axioms, assumption)
    3.10 +  apply (rule ideal.axioms, rule ideal_axioms)
    3.11 + apply (rule abelian_group.axioms, rule ring.axioms, rule ideal.axioms, rule ideal_axioms)
    3.12 +apply (rule abelian_group.axioms, rule ring.axioms, rule ideal.axioms, rule ideal_axioms)
    3.13  done
    3.14  
    3.15  lemma (in ideal) is_ideal:
    3.16 @@ -33,7 +33,12 @@
    3.17        and I_l_closed: "\<And>a x. \<lbrakk>a \<in> I; x \<in> carrier R\<rbrakk> \<Longrightarrow> x \<otimes> a \<in> I"
    3.18        and I_r_closed: "\<And>a x. \<lbrakk>a \<in> I; x \<in> carrier R\<rbrakk> \<Longrightarrow> a \<otimes> x \<in> I"
    3.19    shows "ideal I R"
    3.20 -by (intro ideal.intro ideal_axioms.intro additive_subgroupI, assumption+)
    3.21 +  apply (intro ideal.intro ideal_axioms.intro additive_subgroupI)
    3.22 +     apply (rule a_subgroup)
    3.23 +    apply (rule is_ring)
    3.24 +   apply (erule (1) I_l_closed)
    3.25 +  apply (erule (1) I_r_closed)
    3.26 +  done
    3.27  
    3.28  
    3.29  subsection {* Ideals Generated by a Subset of @{term [locale=ring] "carrier R"} *}
    3.30 @@ -56,7 +61,7 @@
    3.31    includes ideal
    3.32    assumes generate: "\<exists>i \<in> carrier R. I = Idl {i}"
    3.33    shows "principalideal I R"
    3.34 -by (intro principalideal.intro principalideal_axioms.intro, assumption+)
    3.35 +  by (intro principalideal.intro principalideal_axioms.intro) (rule is_ideal, rule generate)
    3.36  
    3.37  
    3.38  subsection {* Maximal Ideals *}
    3.39 @@ -74,7 +79,8 @@
    3.40    assumes I_notcarr: "carrier R \<noteq> I"
    3.41       and I_maximal: "\<And>J. \<lbrakk>ideal J R; I \<subseteq> J; J \<subseteq> carrier R\<rbrakk> \<Longrightarrow> J = I \<or> J = carrier R"
    3.42    shows "maximalideal I R"
    3.43 -by (intro maximalideal.intro maximalideal_axioms.intro, assumption+)
    3.44 +  by (intro maximalideal.intro maximalideal_axioms.intro)
    3.45 +    (rule is_ideal, rule I_notcarr, rule I_maximal)
    3.46  
    3.47  
    3.48  subsection {* Prime Ideals *}
    3.49 @@ -93,7 +99,8 @@
    3.50    assumes I_notcarr: "carrier R \<noteq> I"
    3.51        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"
    3.52    shows "primeideal I R"
    3.53 -by (intro primeideal.intro primeideal_axioms.intro, assumption+)
    3.54 +  by (intro primeideal.intro primeideal_axioms.intro)
    3.55 +    (rule is_ideal, rule is_cring, rule I_notcarr, rule I_prime)
    3.56  
    3.57  lemma primeidealI2:
    3.58    includes additive_subgroup I R
    3.59 @@ -104,8 +111,12 @@
    3.60        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"
    3.61    shows "primeideal I R"
    3.62  apply (intro_locales)
    3.63 - apply (intro ideal_axioms.intro, assumption+)
    3.64 -apply (intro primeideal_axioms.intro, assumption+)
    3.65 + apply (intro ideal_axioms.intro)
    3.66 +  apply (erule (1) I_l_closed)
    3.67 + apply (erule (1) I_r_closed)
    3.68 +apply (intro primeideal_axioms.intro)
    3.69 + apply (rule I_notcarr)
    3.70 +apply (erule (2) I_prime)
    3.71  done
    3.72  
    3.73  
    3.74 @@ -135,7 +146,7 @@
    3.75   shows "primeideal {\<zero>} R"
    3.76  apply (intro primeidealI)
    3.77     apply (rule zeroideal)
    3.78 -  apply (rule domain.axioms,assumption)
    3.79 +  apply (rule domain.axioms, rule domain_axioms)
    3.80   defer 1
    3.81   apply (simp add: integral)
    3.82  proof (rule ccontr, simp)
    3.83 @@ -283,7 +294,7 @@
    3.84    apply (rule add_additive_subgroups)
    3.85     apply (intro ideal.axioms[OF idealI])
    3.86    apply (intro ideal.axioms[OF idealJ])
    3.87 - apply assumption
    3.88 + apply (rule is_ring)
    3.89  apply (rule ideal_axioms.intro)
    3.90   apply (simp add: set_add_defs, clarsimp) defer 1
    3.91   apply (simp add: set_add_defs, clarsimp) defer 1
    3.92 @@ -518,8 +529,8 @@
    3.93    apply (rule genideal_ideal, fast intro: icarr)
    3.94   apply (rule genideal_self', fast intro: icarr)
    3.95  apply (intro genideal_minimal)
    3.96 - apply (rule cgenideal_ideal, assumption)
    3.97 -apply (simp, rule cgenideal_self, assumption)
    3.98 + apply (rule cgenideal_ideal [OF icarr])
    3.99 +apply (simp, rule cgenideal_self [OF icarr])
   3.100  done
   3.101  
   3.102  lemma (in cring) cgenideal_eq_rcos:
     4.1 --- a/src/HOL/Algebra/Lattice.thy	Thu Jun 21 17:28:50 2007 +0200
     4.2 +++ b/src/HOL/Algebra/Lattice.thy	Thu Jun 21 17:28:53 2007 +0200
     4.3 @@ -257,7 +257,9 @@
     4.4  	proof
     4.5            have y': "y \<in> Upper L A"
     4.6              apply (rule subsetD [where A = "Upper L (insert x A)"])
     4.7 -            apply (rule Upper_antimono) apply clarify apply assumption
     4.8 +             apply (rule Upper_antimono)
     4.9 +	     apply blast
    4.10 +	    apply (rule y)
    4.11              done
    4.12            assume "z = a"
    4.13            with y' least_a show ?thesis by (fast dest: least_le)
    4.14 @@ -299,7 +301,9 @@
    4.15            proof
    4.16              have y': "y \<in> Upper L A"
    4.17  	      apply (rule subsetD [where A = "Upper L (insert x A)"])
    4.18 -	      apply (rule Upper_antimono) apply clarify apply assumption
    4.19 +	      apply (rule Upper_antimono)
    4.20 +	       apply blast
    4.21 +	      apply (rule y)
    4.22  	      done
    4.23              assume "z = a"
    4.24              with y' least_a show ?thesis by (fast dest: least_le)
    4.25 @@ -483,7 +487,9 @@
    4.26  	proof
    4.27            have y': "y \<in> Lower L A"
    4.28              apply (rule subsetD [where A = "Lower L (insert x A)"])
    4.29 -            apply (rule Lower_antimono) apply clarify apply assumption
    4.30 +            apply (rule Lower_antimono)
    4.31 +	     apply blast
    4.32 +	    apply (rule y)
    4.33              done
    4.34            assume "z = a"
    4.35            with y' greatest_a show ?thesis by (fast dest: greatest_le)
    4.36 @@ -525,7 +531,9 @@
    4.37            proof
    4.38              have y': "y \<in> Lower L A"
    4.39  	      apply (rule subsetD [where A = "Lower L (insert x A)"])
    4.40 -	      apply (rule Lower_antimono) apply clarify apply assumption
    4.41 +	      apply (rule Lower_antimono)
    4.42 +	       apply blast
    4.43 +	      apply (rule y)
    4.44  	      done
    4.45              assume "z = a"
    4.46              with y' greatest_a show ?thesis by (fast dest: greatest_le)
    4.47 @@ -699,7 +707,7 @@
    4.48        ultimately show ?thesis by blast
    4.49      qed
    4.50    qed
    4.51 -qed (assumption | rule total_order_axioms.intro)+
    4.52 +qed (rule total total_order_axioms.intro)+
    4.53  
    4.54  
    4.55  subsection {* Complete lattices *}
    4.56 @@ -721,7 +729,7 @@
    4.57  proof intro_locales
    4.58    show "lattice_axioms L"
    4.59      by (rule lattice_axioms.intro) (blast intro: sup_exists inf_exists)+
    4.60 -qed (assumption | rule complete_lattice_axioms.intro)+
    4.61 +qed (rule complete_lattice_axioms.intro sup_exists inf_exists | assumption)+
    4.62  
    4.63  constdefs (structure L)
    4.64    top :: "_ => 'a" ("\<top>\<index>")
     5.1 --- a/src/HOL/Algebra/QuotRing.thy	Thu Jun 21 17:28:50 2007 +0200
     5.2 +++ b/src/HOL/Algebra/QuotRing.thy	Thu Jun 21 17:28:53 2007 +0200
     5.3 @@ -4,17 +4,17 @@
     5.4    Author:    Stephan Hohe
     5.5  *)
     5.6  
     5.7 +header {* Quotient Rings *}
     5.8 +
     5.9  theory QuotRing
    5.10  imports RingHom
    5.11  begin
    5.12  
    5.13 -
    5.14 -section {* Quotient Rings *}
    5.15 -
    5.16  subsection {* Multiplication on Cosets *}
    5.17  
    5.18  constdefs (structure R)
    5.19 -  rcoset_mult :: "[('a, _) ring_scheme, 'a set, 'a set, 'a set] \<Rightarrow> 'a set"   ("[mod _:] _ \<Otimes>\<index> _" [81,81,81] 80)
    5.20 +  rcoset_mult :: "[('a, _) ring_scheme, 'a set, 'a set, 'a set] \<Rightarrow> 'a set"
    5.21 +    ("[mod _:] _ \<Otimes>\<index> _" [81,81,81] 80)
    5.22    "rcoset_mult R I A B \<equiv> \<Union>a\<in>A. \<Union>b\<in>B. I +> (a \<otimes> b)"
    5.23  
    5.24  
    5.25 @@ -171,8 +171,9 @@
    5.26    shows "ring_hom_cring R (R Quot I) (op +> I)"
    5.27  apply (rule ring_hom_cringI)
    5.28    apply (rule rcos_ring_hom_ring)
    5.29 - apply assumption
    5.30 -apply (rule quotient_is_cring, assumption)
    5.31 + apply (rule R.is_cring)
    5.32 +apply (rule quotient_is_cring)
    5.33 +apply (rule R.is_cring)
    5.34  done
    5.35  
    5.36  
     6.1 --- a/src/HOL/Algebra/RingHom.thy	Thu Jun 21 17:28:50 2007 +0200
     6.2 +++ b/src/HOL/Algebra/RingHom.thy	Thu Jun 21 17:28:53 2007 +0200
     6.3 @@ -46,7 +46,10 @@
     6.4    shows "ring_hom_ring R S h"
     6.5  apply unfold_locales
     6.6  apply (unfold ring_hom_def, safe)
     6.7 -   apply (simp add: hom_closed Pi_def, assumption+)
     6.8 +   apply (simp add: hom_closed Pi_def)
     6.9 +  apply (erule (1) compatible_mult)
    6.10 + apply (erule (1) compatible_add)
    6.11 +apply (rule compatible_one)
    6.12  done
    6.13  
    6.14  lemma ring_hom_ringI2:
    6.15 @@ -67,13 +70,16 @@
    6.16  apply (intro ring_hom_ring.intro ring_hom_ring_axioms.intro, assumption+)
    6.17  apply (insert group_hom.homh[OF a_group_hom])
    6.18  apply (unfold hom_def ring_hom_def, simp)
    6.19 -apply (safe, assumption+)
    6.20 +apply safe
    6.21 +apply (erule (1) compatible_mult)
    6.22 +apply (rule compatible_one)
    6.23  done
    6.24  
    6.25  lemma ring_hom_cringI:
    6.26    includes ring_hom_ring R S h + cring R + cring S
    6.27    shows "ring_hom_cring R S h"
    6.28 -by (intro ring_hom_cring.intro ring_hom_cring_axioms.intro, assumption+, rule homh)
    6.29 +  by (intro ring_hom_cring.intro ring_hom_cring_axioms.intro)
    6.30 +    (rule R.is_cring, rule S.is_cring, rule homh)
    6.31  
    6.32  
    6.33  subsection {* The kernel of a ring homomorphism *}
     7.1 --- a/src/HOL/Unix/Unix.thy	Thu Jun 21 17:28:50 2007 +0200
     7.2 +++ b/src/HOL/Unix/Unix.thy	Thu Jun 21 17:28:53 2007 +0200
     7.3 @@ -570,7 +570,7 @@
     7.4    using trans
     7.5  proof induct
     7.6    case nil
     7.7 -  show ?case by assumption
     7.8 +  show ?case by (rule nil.prems)
     7.9  next
    7.10    case (cons root x root' xs root'')
    7.11    note P = `\<forall>x \<in> set (x # xs). P x`