Tuned (for the sake of a meaningless log entry).
authorballarin
Thu Jul 31 09:49:21 2008 +0200 (2008-07-31)
changeset 2771427b4d7c01f8b
parent 27713 95b36bfe7fc4
child 27715 087db5aacac3
Tuned (for the sake of a meaningless log entry).
src/HOL/Algebra/Group.thy
src/HOL/Algebra/Ideal.thy
src/HOL/Algebra/Lattice.thy
src/HOL/Algebra/Module.thy
src/HOL/Algebra/Ring.thy
src/HOL/Algebra/UnivPoly.thy
     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"