1.1 --- a/src/HOL/Algebra/Group.thy Wed Jul 30 19:03:33 2008 +0200
1.2 +++ b/src/HOL/Algebra/Group.thy Thu Jul 31 09:49:21 2008 +0200
1.3 @@ -60,7 +60,7 @@
1.4 and l_one: "!!x. x \<in> carrier G ==> \<one> \<otimes> x = x"
1.5 and r_one: "!!x. x \<in> carrier G ==> x \<otimes> \<one> = x"
1.6 shows "monoid G"
1.7 - by (fast intro!: monoid.intro intro: prems)
1.8 + by (fast intro!: monoid.intro intro: assms)
1.9
1.10 lemma (in monoid) Units_closed [dest]:
1.11 "x \<in> Units G ==> x \<in> carrier G"
1.12 @@ -449,8 +449,8 @@
1.13 and inv: "!!a. a \<in> H \<Longrightarrow> inv a \<in> H"
1.14 and mult: "!!a b. \<lbrakk>a \<in> H; b \<in> H\<rbrakk> \<Longrightarrow> a \<otimes> b \<in> H"
1.15 shows "subgroup H G"
1.16 -proof (simp add: subgroup_def prems)
1.17 - show "\<one> \<in> H" by (rule one_in_subset) (auto simp only: prems)
1.18 +proof (simp add: subgroup_def assms)
1.19 + show "\<one> \<in> H" by (rule one_in_subset) (auto simp only: assms)
1.20 qed
1.21
1.22 declare monoid.one_closed [iff] group.inv_closed [simp]
1.23 @@ -489,7 +489,7 @@
1.24 proof -
1.25 interpret G: monoid [G] by fact
1.26 interpret H: monoid [H] by fact
1.27 - from prems
1.28 + from assms
1.29 show ?thesis by (unfold monoid_def DirProd_def, auto)
1.30 qed
1.31
1.32 @@ -527,7 +527,7 @@
1.33 interpret G: group [G] by fact
1.34 interpret H: group [H] by fact
1.35 interpret Prod: group ["G \<times>\<times> H"]
1.36 - by (auto intro: DirProd_group group.intro group.axioms prems)
1.37 + by (auto intro: DirProd_group group.intro group.axioms assms)
1.38 show ?thesis by (simp add: Prod.inv_equality g h)
1.39 qed
1.40
1.41 @@ -657,7 +657,7 @@
1.42 shows "comm_monoid G"
1.43 using l_one
1.44 by (auto intro!: comm_monoid.intro comm_monoid_axioms.intro monoid.intro
1.45 - intro: prems simp: m_closed one_closed m_comm)
1.46 + intro: assms simp: m_closed one_closed m_comm)
1.47
1.48 lemma (in monoid) monoid_comm_monoidI:
1.49 assumes m_comm:
1.50 @@ -700,7 +700,7 @@
1.51 and l_one: "!!x. x \<in> carrier G ==> \<one> \<otimes> x = x"
1.52 and l_inv_ex: "!!x. x \<in> carrier G ==> \<exists>y \<in> carrier G. y \<otimes> x = \<one>"
1.53 shows "comm_group G"
1.54 - by (fast intro: group.group_comm_groupI groupI prems)
1.55 + by (fast intro: group.group_comm_groupI groupI assms)
1.56
1.57 lemma (in comm_group) inv_mult:
1.58 "[| x \<in> carrier G; y \<in> carrier G |] ==> inv (x \<otimes> y) = inv x \<otimes> inv y"
2.1 --- a/src/HOL/Algebra/Ideal.thy Wed Jul 30 19:03:33 2008 +0200
2.2 +++ b/src/HOL/Algebra/Ideal.thy Thu Jul 31 09:49:21 2008 +0200
2.3 @@ -217,9 +217,9 @@
2.4 apply simp
2.5 apply (simp add: a_inv_def[symmetric])
2.6 apply (clarsimp, rule)
2.7 - apply (fast intro: ideal.I_l_closed ideal.intro prems)+
2.8 + apply (fast intro: ideal.I_l_closed ideal.intro assms)+
2.9 apply (clarsimp, rule)
2.10 - apply (fast intro: ideal.I_r_closed ideal.intro prems)+
2.11 + apply (fast intro: ideal.I_r_closed ideal.intro assms)+
2.12 done
2.13 qed
2.14
3.1 --- a/src/HOL/Algebra/Lattice.thy Wed Jul 30 19:03:33 2008 +0200
3.2 +++ b/src/HOL/Algebra/Lattice.thy Thu Jul 31 09:49:21 2008 +0200
3.3 @@ -1,8 +1,10 @@
3.4 (*
3.5 - Title: HOL/Algebra/GLattice.thy
3.6 + Title: HOL/Algebra/Lattice.thy
3.7 Id: $Id$
3.8 Author: Clemens Ballarin, started 7 November 2003
3.9 Copyright: Clemens Ballarin
3.10 +
3.11 +Most congruence rules by Stefan Hohe.
3.12 *)
3.13
3.14 theory Lattice imports Congruence begin
3.15 @@ -41,7 +43,7 @@
3.16 "\<lbrakk> x \<sqsubseteq> y; y .= z; x \<in> carrier L; y \<in> carrier L; z \<in> carrier L \<rbrakk> \<Longrightarrow> x \<sqsubseteq> z"
3.17 by (auto intro: le_cong [THEN iffD1])
3.18
3.19 -lemma gen_refl [intro, simp]: "\<lbrakk> x .= y; x \<in> carrier L; y \<in> carrier L \<rbrakk> \<Longrightarrow> x \<sqsubseteq> y"
3.20 +lemma weak_refl [intro, simp]: "\<lbrakk> x .= y; x \<in> carrier L; y \<in> carrier L \<rbrakk> \<Longrightarrow> x \<sqsubseteq> y"
3.21 by (simp add: le_cong_l)
3.22
3.23 end
3.24 @@ -1150,58 +1152,42 @@
3.25
3.26 subsubsection {* Supremum *}
3.27
3.28 -context partial_order begin
3.29 +declare (in partial_order) weak_sup_of_singleton [simp del]
3.30
3.31 -declare weak_sup_of_singleton [simp del]
3.32 -
3.33 -lemma sup_of_singleton [simp]:
3.34 +lemma (in partial_order) sup_of_singleton [simp]:
3.35 "x \<in> carrier L ==> \<Squnion>{x} = x"
3.36 using weak_sup_of_singleton unfolding eq_is_equal .
3.37
3.38 -end
3.39 -
3.40 -context upper_semilattice begin
3.41 -
3.42 -lemma join_assoc_lemma:
3.43 +lemma (in upper_semilattice) join_assoc_lemma:
3.44 assumes L: "x \<in> carrier L" "y \<in> carrier L" "z \<in> carrier L"
3.45 shows "x \<squnion> (y \<squnion> z) = \<Squnion>{x, y, z}"
3.46 - using weak_join_assoc_lemma unfolding eq_is_equal .
3.47 -
3.48 -end
3.49 + using weak_join_assoc_lemma L unfolding eq_is_equal .
3.50
3.51 lemma (in upper_semilattice) join_assoc:
3.52 assumes L: "x \<in> carrier L" "y \<in> carrier L" "z \<in> carrier L"
3.53 shows "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)"
3.54 - using weak_join_assoc unfolding eq_is_equal .
3.55 + using weak_join_assoc L unfolding eq_is_equal .
3.56
3.57
3.58 subsubsection {* Infimum *}
3.59
3.60 -context partial_order begin
3.61 +declare (in partial_order) weak_inf_of_singleton [simp del]
3.62
3.63 -declare weak_inf_of_singleton [simp del]
3.64 -
3.65 -lemma inf_of_singleton [simp]:
3.66 +lemma (in partial_order) inf_of_singleton [simp]:
3.67 "x \<in> carrier L ==> \<Sqinter>{x} = x"
3.68 using weak_inf_of_singleton unfolding eq_is_equal .
3.69
3.70 -end
3.71 -
3.72 -context lower_semilattice begin
3.73 -
3.74 text {* Condition on @{text A}: infimum exists. *}
3.75
3.76 -lemma meet_assoc_lemma:
3.77 +lemma (in lower_semilattice) meet_assoc_lemma:
3.78 assumes L: "x \<in> carrier L" "y \<in> carrier L" "z \<in> carrier L"
3.79 shows "x \<sqinter> (y \<sqinter> z) = \<Sqinter>{x, y, z}"
3.80 - using weak_meet_assoc_lemma unfolding eq_is_equal .
3.81 -
3.82 -end
3.83 + using weak_meet_assoc_lemma L unfolding eq_is_equal .
3.84
3.85 lemma (in lower_semilattice) meet_assoc:
3.86 assumes L: "x \<in> carrier L" "y \<in> carrier L" "z \<in> carrier L"
3.87 shows "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)"
3.88 - using weak_meet_assoc unfolding eq_is_equal .
3.89 + using weak_meet_assoc L unfolding eq_is_equal .
3.90
3.91
3.92 subsection {* Total Orders *}
4.1 --- a/src/HOL/Algebra/Module.thy Wed Jul 30 19:03:33 2008 +0200
4.2 +++ b/src/HOL/Algebra/Module.thy Thu Jul 31 09:49:21 2008 +0200
4.3 @@ -53,7 +53,7 @@
4.4 "!!x. x \<in> carrier M ==> \<one> \<odot>\<^bsub>M\<^esub> x = x"
4.5 shows "module R M"
4.6 by (auto intro: module.intro cring.axioms abelian_group.axioms
4.7 - module_axioms.intro prems)
4.8 + module_axioms.intro assms)
4.9
4.10 lemma algebraI:
4.11 fixes R (structure) and M (structure)
4.12 @@ -77,14 +77,14 @@
4.13 (a \<odot>\<^bsub>M\<^esub> x) \<otimes>\<^bsub>M\<^esub> y = a \<odot>\<^bsub>M\<^esub> (x \<otimes>\<^bsub>M\<^esub> y)"
4.14 shows "algebra R M"
4.15 apply intro_locales
4.16 -apply (rule cring.axioms ring.axioms abelian_group.axioms comm_monoid.axioms prems)+
4.17 +apply (rule cring.axioms ring.axioms abelian_group.axioms comm_monoid.axioms assms)+
4.18 apply (rule module_axioms.intro)
4.19 apply (simp add: smult_closed)
4.20 apply (simp add: smult_l_distr)
4.21 apply (simp add: smult_r_distr)
4.22 apply (simp add: smult_assoc1)
4.23 apply (simp add: smult_one)
4.24 -apply (rule cring.axioms ring.axioms abelian_group.axioms comm_monoid.axioms prems)+
4.25 +apply (rule cring.axioms ring.axioms abelian_group.axioms comm_monoid.axioms assms)+
4.26 apply (rule algebra_axioms.intro)
4.27 apply (simp add: smult_assoc2)
4.28 done
5.1 --- a/src/HOL/Algebra/Ring.thy Wed Jul 30 19:03:33 2008 +0200
5.2 +++ b/src/HOL/Algebra/Ring.thy Thu Jul 31 09:49:21 2008 +0200
5.3 @@ -53,7 +53,7 @@
5.4 and a_comm:
5.5 "!!x y. [| x \<in> carrier R; y \<in> carrier R |] ==> x \<oplus> y = y \<oplus> x"
5.6 shows "abelian_monoid R"
5.7 - by (auto intro!: abelian_monoid.intro comm_monoidI intro: prems)
5.8 + by (auto intro!: abelian_monoid.intro comm_monoidI intro: assms)
5.9
5.10 lemma abelian_groupI:
5.11 fixes R (structure)
5.12 @@ -70,7 +70,7 @@
5.13 shows "abelian_group R"
5.14 by (auto intro!: abelian_group.intro abelian_monoidI
5.15 abelian_group_axioms.intro comm_monoidI comm_groupI
5.16 - intro: prems)
5.17 + intro: assms)
5.18
5.19 lemma (in abelian_monoid) a_monoid:
5.20 "monoid (| carrier = carrier G, mult = add G, one = zero G |)"
5.21 @@ -374,7 +374,7 @@
5.22 ==> z \<otimes> (x \<oplus> y) = z \<otimes> x \<oplus> z \<otimes> y"
5.23 shows "ring R"
5.24 by (auto intro: ring.intro
5.25 - abelian_group.axioms ring_axioms.intro prems)
5.26 + abelian_group.axioms ring_axioms.intro assms)
5.27
5.28 lemma (in ring) is_abelian_group:
5.29 "abelian_group R"
5.30 @@ -416,7 +416,7 @@
5.31 finally show "z \<otimes> (x \<oplus> y) = z \<otimes> x \<oplus> z \<otimes> y" .
5.32 qed (rule l_distr)
5.33 qed (auto intro: cring.intro
5.34 - abelian_group.axioms comm_monoid.axioms ring_axioms.intro prems)
5.35 + abelian_group.axioms comm_monoid.axioms ring_axioms.intro assms)
5.36
5.37 (*
5.38 lemma (in cring) is_comm_monoid:
5.39 @@ -731,7 +731,7 @@
5.40 h (x \<oplus> y) = h x \<oplus>\<^bsub>S\<^esub> h y"
5.41 and hom_one: "h \<one> = \<one>\<^bsub>S\<^esub>"
5.42 shows "h \<in> ring_hom R S"
5.43 - by (auto simp add: ring_hom_def prems Pi_def)
5.44 + by (auto simp add: ring_hom_def assms Pi_def)
5.45
5.46 lemma ring_hom_closed:
5.47 "[| h \<in> ring_hom R S; x \<in> carrier R |] ==> h x \<in> carrier S"
6.1 --- a/src/HOL/Algebra/UnivPoly.thy Wed Jul 30 19:03:33 2008 +0200
6.2 +++ b/src/HOL/Algebra/UnivPoly.thy Thu Jul 31 09:49:21 2008 +0200
6.3 @@ -435,7 +435,7 @@
6.4
6.5 lemma (in cring) cring:
6.6 "cring R"
6.7 - by (fast intro: cring.intro prems)
6.8 + by unfold_locales
6.9
6.10 lemma (in UP_cring) UP_algebra:
6.11 "algebra R P"
6.12 @@ -898,7 +898,7 @@
6.13 and integral: "!!a b. [| mult R a b = zero R; a \<in> carrier R;
6.14 b \<in> carrier R |] ==> a = zero R | b = zero R"
6.15 shows "domain R"
6.16 - by (auto intro!: domain.intro domain_axioms.intro cring.axioms prems
6.17 + by (auto intro!: domain.intro domain_axioms.intro cring.axioms assms
6.18 del: disjCI)
6.19
6.20 lemma (in UP_domain) UP_one_not_zero:
6.21 @@ -1251,7 +1251,7 @@
6.22 and "h \<in> ring_hom R S"
6.23 shows "ring_hom_cring R S h"
6.24 by (fast intro: ring_hom_cring.intro ring_hom_cring_axioms.intro
6.25 - cring.axioms prems)
6.26 + cring.axioms assms)
6.27
6.28 lemma (in UP_pre_univ_prop) UP_hom_unique:
6.29 assumes "ring_hom_cring P S Phi"