# 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 \ carrier G -> carrier H & (\x \ carrier G. \y \ carrier G. h (x \\<^bsub>G\<^esub> y) = h x \\<^bsub>H\<^esub> h y)}" -lemma hom_mult: - "[| h \ hom G H; x \ carrier G; y \ carrier G |] - ==> h (x \\<^bsub>G\<^esub> y) = h x \\<^bsub>H\<^esub> h y" - by (simp add: hom_def) - -lemma hom_closed: - "[| h \ hom G H; x \ carrier G |] ==> h x \ carrier H" - by (auto simp add: hom_def funcset_mem) - lemma (in group) hom_compose: "[|h \ hom G H; i \ hom H I|] ==> compose (carrier G) i h \ 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 \ 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 \ carrier G; y \ carrier G |] ==> h (x \\<^bsub>G\<^esub> y) = h x \\<^bsub>H\<^esub> h y" +proof - + assume "x \ carrier G" "y \ carrier G" + with homh [unfolded hom_def] show ?thesis by simp +qed + +lemma (in group_hom) hom_closed [simp]: + "x \ carrier G ==> h x \ carrier H" +proof - + assume "x \ carrier G" + with homh [unfolded hom_def] show ?thesis by (auto simp add: funcset_mem) +qed lemma (in group_hom) one_closed [simp]: "h \ \ 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: "\a \ I; x \ carrier R\ \ x \ a \ I" and I_r_closed: "\a \ I; x \ carrier R\ \ a \ x \ I" @@ -127,7 +127,7 @@ and I_prime: "\a b. \a \ carrier R; b \ carrier R; a \ b \ I\ \ a \ I \ b \ 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 \ 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 \ J" shows "PIdl a \ 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 \ 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 \ "{x\carrier R. a \ x \ 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 \ 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 \ 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