# HG changeset patch
# User ballarin
# Date 1217490561 -7200
# Node ID 27b4d7c01f8b50cd5edda141b0e8278e5e713f45
# Parent  95b36bfe7fc484d21d6185309341667559d664aa
Tuned (for the sake of a meaningless log entry).

diff -r 95b36bfe7fc4 -r 27b4d7c01f8b src/HOL/Algebra/Group.thy
--- a/src/HOL/Algebra/Group.thy	Wed Jul 30 19:03:33 2008 +0200
+++ b/src/HOL/Algebra/Group.thy	Thu Jul 31 09:49:21 2008 +0200
@@ -60,7 +60,7 @@
     and l_one: "!!x. x \<in> carrier G ==> \<one> \<otimes> x = x"
     and r_one: "!!x. x \<in> carrier G ==> x \<otimes> \<one> = x"
   shows "monoid G"
-  by (fast intro!: monoid.intro intro: prems)
+  by (fast intro!: monoid.intro intro: assms)
 
 lemma (in monoid) Units_closed [dest]:
   "x \<in> Units G ==> x \<in> carrier G"
@@ -449,8 +449,8 @@
     and inv: "!!a. a \<in> H \<Longrightarrow> inv a \<in> H"
     and mult: "!!a b. \<lbrakk>a \<in> H; b \<in> H\<rbrakk> \<Longrightarrow> a \<otimes> b \<in> H"
   shows "subgroup H G"
-proof (simp add: subgroup_def prems)
-  show "\<one> \<in> H" by (rule one_in_subset) (auto simp only: prems)
+proof (simp add: subgroup_def assms)
+  show "\<one> \<in> H" by (rule one_in_subset) (auto simp only: assms)
 qed
 
 declare monoid.one_closed [iff] group.inv_closed [simp]
@@ -489,7 +489,7 @@
 proof -
   interpret G: monoid [G] by fact
   interpret H: monoid [H] by fact
-  from prems
+  from assms
   show ?thesis by (unfold monoid_def DirProd_def, auto) 
 qed
 
@@ -527,7 +527,7 @@
   interpret G: group [G] by fact
   interpret H: group [H] by fact
   interpret Prod: group ["G \<times>\<times> H"]
-    by (auto intro: DirProd_group group.intro group.axioms prems)
+    by (auto intro: DirProd_group group.intro group.axioms assms)
   show ?thesis by (simp add: Prod.inv_equality g h)
 qed
 
@@ -657,7 +657,7 @@
   shows "comm_monoid G"
   using l_one
     by (auto intro!: comm_monoid.intro comm_monoid_axioms.intro monoid.intro 
-             intro: prems simp: m_closed one_closed m_comm)
+             intro: assms simp: m_closed one_closed m_comm)
 
 lemma (in monoid) monoid_comm_monoidI:
   assumes m_comm:
@@ -700,7 +700,7 @@
     and l_one: "!!x. x \<in> carrier G ==> \<one> \<otimes> x = x"
     and l_inv_ex: "!!x. x \<in> carrier G ==> \<exists>y \<in> carrier G. y \<otimes> x = \<one>"
   shows "comm_group G"
-  by (fast intro: group.group_comm_groupI groupI prems)
+  by (fast intro: group.group_comm_groupI groupI assms)
 
 lemma (in comm_group) inv_mult:
   "[| x \<in> carrier G; y \<in> carrier G |] ==> inv (x \<otimes> y) = inv x \<otimes> inv y"
diff -r 95b36bfe7fc4 -r 27b4d7c01f8b src/HOL/Algebra/Ideal.thy
--- a/src/HOL/Algebra/Ideal.thy	Wed Jul 30 19:03:33 2008 +0200
+++ b/src/HOL/Algebra/Ideal.thy	Thu Jul 31 09:49:21 2008 +0200
@@ -217,9 +217,9 @@
    apply simp
   apply (simp add: a_inv_def[symmetric])
  apply (clarsimp, rule)
-  apply (fast intro: ideal.I_l_closed ideal.intro prems)+
+  apply (fast intro: ideal.I_l_closed ideal.intro assms)+
 apply (clarsimp, rule)
- apply (fast intro: ideal.I_r_closed ideal.intro prems)+
+ apply (fast intro: ideal.I_r_closed ideal.intro assms)+
 done
 qed
 
diff -r 95b36bfe7fc4 -r 27b4d7c01f8b src/HOL/Algebra/Lattice.thy
--- a/src/HOL/Algebra/Lattice.thy	Wed Jul 30 19:03:33 2008 +0200
+++ b/src/HOL/Algebra/Lattice.thy	Thu Jul 31 09:49:21 2008 +0200
@@ -1,8 +1,10 @@
 (*
-  Title:     HOL/Algebra/GLattice.thy
+  Title:     HOL/Algebra/Lattice.thy
   Id:        $Id$
   Author:    Clemens Ballarin, started 7 November 2003
   Copyright: Clemens Ballarin
+
+Most congruence rules by Stefan Hohe.
 *)
 
 theory Lattice imports Congruence begin
@@ -41,7 +43,7 @@
   "\<lbrakk> x \<sqsubseteq> y; y .= z; x \<in> carrier L; y \<in> carrier L; z \<in> carrier L \<rbrakk> \<Longrightarrow> x \<sqsubseteq> z"
   by (auto intro: le_cong [THEN iffD1])
 
-lemma gen_refl [intro, simp]: "\<lbrakk> x .= y; x \<in> carrier L; y \<in> carrier L \<rbrakk> \<Longrightarrow> x \<sqsubseteq> y"
+lemma weak_refl [intro, simp]: "\<lbrakk> x .= y; x \<in> carrier L; y \<in> carrier L \<rbrakk> \<Longrightarrow> x \<sqsubseteq> y"
   by (simp add: le_cong_l)
 
 end
@@ -1150,58 +1152,42 @@
 
 subsubsection {* Supremum *}
 
-context partial_order begin
+declare (in partial_order) weak_sup_of_singleton [simp del]
 
-declare weak_sup_of_singleton [simp del]
-
-lemma sup_of_singleton [simp]:
+lemma (in partial_order) sup_of_singleton [simp]:
   "x \<in> carrier L ==> \<Squnion>{x} = x"
   using weak_sup_of_singleton unfolding eq_is_equal .
 
-end
-
-context upper_semilattice begin
-
-lemma join_assoc_lemma:
+lemma (in upper_semilattice) join_assoc_lemma:
   assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
   shows "x \<squnion> (y \<squnion> z) = \<Squnion>{x, y, z}"
-  using weak_join_assoc_lemma unfolding eq_is_equal .
-
-end
+  using weak_join_assoc_lemma L unfolding eq_is_equal .
 
 lemma (in upper_semilattice) join_assoc:
   assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
   shows "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)"
-  using weak_join_assoc unfolding eq_is_equal .
+  using weak_join_assoc L unfolding eq_is_equal .
 
 
 subsubsection {* Infimum *}
 
-context partial_order begin
+declare (in partial_order) weak_inf_of_singleton [simp del]
 
-declare weak_inf_of_singleton [simp del]
-
-lemma inf_of_singleton [simp]:
+lemma (in partial_order) inf_of_singleton [simp]:
   "x \<in> carrier L ==> \<Sqinter>{x} = x"
   using weak_inf_of_singleton unfolding eq_is_equal .
 
-end
-
-context lower_semilattice begin
-
 text {* Condition on @{text A}: infimum exists. *}
 
-lemma meet_assoc_lemma:
+lemma (in lower_semilattice) meet_assoc_lemma:
   assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
   shows "x \<sqinter> (y \<sqinter> z) = \<Sqinter>{x, y, z}"
-  using weak_meet_assoc_lemma unfolding eq_is_equal .
-
-end
+  using weak_meet_assoc_lemma L unfolding eq_is_equal .
 
 lemma (in lower_semilattice) meet_assoc:
   assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
   shows "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)"
-  using weak_meet_assoc unfolding eq_is_equal .
+  using weak_meet_assoc L unfolding eq_is_equal .
 
 
 subsection {* Total Orders *}
diff -r 95b36bfe7fc4 -r 27b4d7c01f8b src/HOL/Algebra/Module.thy
--- a/src/HOL/Algebra/Module.thy	Wed Jul 30 19:03:33 2008 +0200
+++ b/src/HOL/Algebra/Module.thy	Thu Jul 31 09:49:21 2008 +0200
@@ -53,7 +53,7 @@
       "!!x. x \<in> carrier M ==> \<one> \<odot>\<^bsub>M\<^esub> x = x"
   shows "module R M"
   by (auto intro: module.intro cring.axioms abelian_group.axioms
-    module_axioms.intro prems)
+    module_axioms.intro assms)
 
 lemma algebraI:
   fixes R (structure) and M (structure)
@@ -77,14 +77,14 @@
       (a \<odot>\<^bsub>M\<^esub> x) \<otimes>\<^bsub>M\<^esub> y = a \<odot>\<^bsub>M\<^esub> (x \<otimes>\<^bsub>M\<^esub> y)"
   shows "algebra R M"
 apply intro_locales
-apply (rule cring.axioms ring.axioms abelian_group.axioms comm_monoid.axioms prems)+
+apply (rule cring.axioms ring.axioms abelian_group.axioms comm_monoid.axioms assms)+
 apply (rule module_axioms.intro)
  apply (simp add: smult_closed)
  apply (simp add: smult_l_distr)
  apply (simp add: smult_r_distr)
  apply (simp add: smult_assoc1)
  apply (simp add: smult_one)
-apply (rule cring.axioms ring.axioms abelian_group.axioms comm_monoid.axioms prems)+
+apply (rule cring.axioms ring.axioms abelian_group.axioms comm_monoid.axioms assms)+
 apply (rule algebra_axioms.intro)
  apply (simp add: smult_assoc2)
 done
diff -r 95b36bfe7fc4 -r 27b4d7c01f8b src/HOL/Algebra/Ring.thy
--- a/src/HOL/Algebra/Ring.thy	Wed Jul 30 19:03:33 2008 +0200
+++ b/src/HOL/Algebra/Ring.thy	Thu Jul 31 09:49:21 2008 +0200
@@ -53,7 +53,7 @@
     and a_comm:
       "!!x y. [| x \<in> carrier R; y \<in> carrier R |] ==> x \<oplus> y = y \<oplus> x"
   shows "abelian_monoid R"
-  by (auto intro!: abelian_monoid.intro comm_monoidI intro: prems)
+  by (auto intro!: abelian_monoid.intro comm_monoidI intro: assms)
 
 lemma abelian_groupI:
   fixes R (structure)
@@ -70,7 +70,7 @@
   shows "abelian_group R"
   by (auto intro!: abelian_group.intro abelian_monoidI
       abelian_group_axioms.intro comm_monoidI comm_groupI
-    intro: prems)
+    intro: assms)
 
 lemma (in abelian_monoid) a_monoid:
   "monoid (| carrier = carrier G, mult = add G, one = zero G |)"
@@ -374,7 +374,7 @@
       ==> z \<otimes> (x \<oplus> y) = z \<otimes> x \<oplus> z \<otimes> y"
   shows "ring R"
   by (auto intro: ring.intro
-    abelian_group.axioms ring_axioms.intro prems)
+    abelian_group.axioms ring_axioms.intro assms)
 
 lemma (in ring) is_abelian_group:
   "abelian_group R"
@@ -416,7 +416,7 @@
     finally show "z \<otimes> (x \<oplus> y) = z \<otimes> x \<oplus> z \<otimes> y" .
   qed (rule l_distr)
 qed (auto intro: cring.intro
-  abelian_group.axioms comm_monoid.axioms ring_axioms.intro prems)
+  abelian_group.axioms comm_monoid.axioms ring_axioms.intro assms)
 
 (*
 lemma (in cring) is_comm_monoid:
@@ -731,7 +731,7 @@
       h (x \<oplus> y) = h x \<oplus>\<^bsub>S\<^esub> h y"
     and hom_one: "h \<one> = \<one>\<^bsub>S\<^esub>"
   shows "h \<in> ring_hom R S"
-  by (auto simp add: ring_hom_def prems Pi_def)
+  by (auto simp add: ring_hom_def assms Pi_def)
 
 lemma ring_hom_closed:
   "[| h \<in> ring_hom R S; x \<in> carrier R |] ==> h x \<in> carrier S"
diff -r 95b36bfe7fc4 -r 27b4d7c01f8b src/HOL/Algebra/UnivPoly.thy
--- a/src/HOL/Algebra/UnivPoly.thy	Wed Jul 30 19:03:33 2008 +0200
+++ b/src/HOL/Algebra/UnivPoly.thy	Thu Jul 31 09:49:21 2008 +0200
@@ -435,7 +435,7 @@
 
 lemma (in cring) cring:
   "cring R"
-  by (fast intro: cring.intro prems)
+  by unfold_locales
 
 lemma (in UP_cring) UP_algebra:
   "algebra R P"
@@ -898,7 +898,7 @@
     and integral: "!!a b. [| mult R a b = zero R; a \<in> carrier R;
       b \<in> carrier R |] ==> a = zero R | b = zero R"
   shows "domain R"
-  by (auto intro!: domain.intro domain_axioms.intro cring.axioms prems
+  by (auto intro!: domain.intro domain_axioms.intro cring.axioms assms
     del: disjCI)
 
 lemma (in UP_domain) UP_one_not_zero:
@@ -1251,7 +1251,7 @@
     and "h \<in> ring_hom R S"
   shows "ring_hom_cring R S h"
   by (fast intro: ring_hom_cring.intro ring_hom_cring_axioms.intro
-    cring.axioms prems)
+    cring.axioms assms)
 
 lemma (in UP_pre_univ_prop) UP_hom_unique:
   assumes "ring_hom_cring P S Phi"