--- 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"
--- 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 -
--- 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:
--- 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>")
--- 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
--- 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 *}
--- 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`