# HG changeset patch
# User ballarin
# Date 1229532836 -3600
# Node ID bb81c3709fb689dbb2a37678bbc33d87b53542aa
# Parent  0a64c3418347dc0c10a9219f42826f74441895a9
More porting to new locales.

diff -r 0a64c3418347 -r bb81c3709fb6 src/HOL/Algebra/Group.thy
--- a/src/HOL/Algebra/Group.thy	Wed Dec 17 17:53:41 2008 +0100
+++ b/src/HOL/Algebra/Group.thy	Wed Dec 17 17:53:56 2008 +0100
@@ -541,15 +541,6 @@
     {h. h \<in> carrier G -> carrier H &
       (\<forall>x \<in> carrier G. \<forall>y \<in> carrier G. h (x \<otimes>\<^bsub>G\<^esub> y) = h x \<otimes>\<^bsub>H\<^esub> h y)}"
 
-lemma hom_mult:
-  "[| h \<in> hom G H; x \<in> carrier G; y \<in> carrier G |]
-   ==> h (x \<otimes>\<^bsub>G\<^esub> y) = h x \<otimes>\<^bsub>H\<^esub> h y"
-  by (simp add: hom_def)
-
-lemma hom_closed:
-  "[| h \<in> hom G H; x \<in> carrier G |] ==> h x \<in> carrier H"
-  by (auto simp add: hom_def funcset_mem)
-
 lemma (in group) hom_compose:
      "[|h \<in> hom G H; i \<in> hom H I|] ==> compose (carrier G) i h \<in> hom G I"
 apply (auto simp add: hom_def funcset_compose) 
@@ -589,8 +580,20 @@
 locale group_hom = G: group G + H: group H for G (structure) and H (structure) +
   fixes h
   assumes homh: "h \<in> hom G H"
-  notes hom_mult [simp] = hom_mult [OF homh]
-    and hom_closed [simp] = hom_closed [OF homh]
+
+lemma (in group_hom) hom_mult [simp]:
+  "[| x \<in> carrier G; y \<in> carrier G |] ==> h (x \<otimes>\<^bsub>G\<^esub> y) = h x \<otimes>\<^bsub>H\<^esub> h y"
+proof -
+  assume "x \<in> carrier G" "y \<in> carrier G"
+  with homh [unfolded hom_def] show ?thesis by simp
+qed
+
+lemma (in group_hom) hom_closed [simp]:
+  "x \<in> carrier G ==> h x \<in> carrier H"
+proof -
+  assume "x \<in> carrier G"
+  with homh [unfolded hom_def] show ?thesis by (auto simp add: funcset_mem)
+qed
 
 lemma (in group_hom) one_closed [simp]:
   "h \<one> \<in> carrier H"
diff -r 0a64c3418347 -r bb81c3709fb6 src/HOL/Algebra/Ideal.thy
--- a/src/HOL/Algebra/Ideal.thy	Wed Dec 17 17:53:41 2008 +0100
+++ b/src/HOL/Algebra/Ideal.thy	Wed Dec 17 17:53:56 2008 +0100
@@ -13,7 +13,7 @@
 
 subsubsection {* General definition *}
 
-locale ideal = additive_subgroup I R + ring R +
+locale ideal = additive_subgroup I R + ring R for I and R (structure) +
   assumes I_l_closed: "\<lbrakk>a \<in> I; x \<in> carrier R\<rbrakk> \<Longrightarrow> x \<otimes> a \<in> I"
       and I_r_closed: "\<lbrakk>a \<in> I; x \<in> carrier R\<rbrakk> \<Longrightarrow> a \<otimes> x \<in> I"
 
@@ -127,7 +127,7 @@
       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"
 proof -
-  interpret additive_subgroup [I R] by fact
+  interpret additive_subgroup I R by fact
   interpret cring R by fact
   show ?thesis apply (intro_locales)
     apply (intro ideal_axioms.intro)
@@ -207,7 +207,7 @@
   shows "ideal (I \<inter> J) R"
 proof -
   interpret ideal I R by fact
-  interpret ideal [J R] by fact
+  interpret ideal J R by fact
   show ?thesis
 apply (intro idealI subgroup.intro)
       apply (rule is_ring)
@@ -532,7 +532,7 @@
   assumes aJ: "a \<in> J"
   shows "PIdl a \<subseteq> J"
 proof -
-  interpret ideal [J R] by fact
+  interpret ideal J R by fact
   show ?thesis unfolding cgenideal_def
     apply rule
     apply clarify
@@ -579,7 +579,7 @@
   shows "Idl (I \<union> J) = I <+> J"
 apply rule
  apply (rule ring.genideal_minimal)
-   apply (rule R.is_ring)
+   apply (rule is_ring)
   apply (rule add_ideals[OF idealI idealJ])
  apply (rule)
  apply (simp add: set_add_defs) apply (elim disjE) defer 1 defer 1
@@ -829,7 +829,7 @@
       by fast
     def J \<equiv> "{x\<in>carrier R. a \<otimes> x \<in> I}"
     
-    from R.is_cring and acarr
+    from is_cring and acarr
     have idealJ: "ideal J R" unfolding J_def by (rule helper_max_prime)
     
     have IsubJ: "I \<subseteq> J"
diff -r 0a64c3418347 -r bb81c3709fb6 src/HOL/Algebra/RingHom.thy
--- a/src/HOL/Algebra/RingHom.thy	Wed Dec 17 17:53:41 2008 +0100
+++ b/src/HOL/Algebra/RingHom.thy	Wed Dec 17 17:53:56 2008 +0100
@@ -10,7 +10,8 @@
 section {* Homomorphisms of Non-Commutative Rings *}
 
 text {* Lifting existing lemmas in a @{text ring_hom_ring} locale *}
-locale ring_hom_ring = R: ring R + S: ring S +
+locale ring_hom_ring = R: ring R + S: ring S
+    for R (structure) and S (structure) +
   fixes h
   assumes homh: "h \<in> ring_hom R S"
   notes hom_mult [simp] = ring_hom_mult [OF homh]
diff -r 0a64c3418347 -r bb81c3709fb6 src/HOL/Algebra/UnivPoly.thy
--- a/src/HOL/Algebra/UnivPoly.thy	Wed Dec 17 17:53:41 2008 +0100
+++ b/src/HOL/Algebra/UnivPoly.thy	Wed Dec 17 17:53:56 2008 +0100
@@ -175,17 +175,17 @@
   fixes R (structure) and P (structure)
   defines P_def: "P == UP R"
 
-locale UP_ring = UP + ring R
+locale UP_ring = UP + R: ring R
 
-locale UP_cring = UP + cring R
+locale UP_cring = UP + R: cring R
 
 sublocale UP_cring < UP_ring
-  by (rule P_def) intro_locales
+  by intro_locales [1] (rule P_def)
 
-locale UP_domain = UP + "domain" R
+locale UP_domain = UP + R: "domain" R
 
 sublocale UP_domain < UP_cring
-  by (rule P_def) intro_locales
+  by intro_locales [1] (rule P_def)
 
 context UP
 begin
@@ -457,8 +457,8 @@
 
 end
 
-sublocale UP_ring < ring P using UP_ring .
-sublocale UP_cring < cring P using UP_cring .
+sublocale UP_ring < P: ring P using UP_ring .
+sublocale UP_cring < P: cring P using UP_cring .
 
 
 subsection {* Polynomials Form an Algebra *}
@@ -1203,7 +1203,9 @@
 
 text {* The universal property of the polynomial ring *}
 
-locale UP_pre_univ_prop = ring_hom_cring R S h + UP_cring R P
+locale UP_pre_univ_prop = ring_hom_cring + UP_cring
+
+(* FIXME print_locale ring_hom_cring fails *)
 
 locale UP_univ_prop = UP_pre_univ_prop +
   fixes s and Eval