More porting to new locales.
authorballarin
Wed Dec 17 17:53:56 2008 +0100 (2008-12-17)
changeset 29240bb81c3709fb6
parent 29239 0a64c3418347
child 29241 3adc06d6504f
More porting to new locales.
src/HOL/Algebra/Group.thy
src/HOL/Algebra/Ideal.thy
src/HOL/Algebra/RingHom.thy
src/HOL/Algebra/UnivPoly.thy
     1.1 --- a/src/HOL/Algebra/Group.thy	Wed Dec 17 17:53:41 2008 +0100
     1.2 +++ b/src/HOL/Algebra/Group.thy	Wed Dec 17 17:53:56 2008 +0100
     1.3 @@ -541,15 +541,6 @@
     1.4      {h. h \<in> carrier G -> carrier H &
     1.5        (\<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)}"
     1.6  
     1.7 -lemma hom_mult:
     1.8 -  "[| h \<in> hom G H; x \<in> carrier G; y \<in> carrier G |]
     1.9 -   ==> h (x \<otimes>\<^bsub>G\<^esub> y) = h x \<otimes>\<^bsub>H\<^esub> h y"
    1.10 -  by (simp add: hom_def)
    1.11 -
    1.12 -lemma hom_closed:
    1.13 -  "[| h \<in> hom G H; x \<in> carrier G |] ==> h x \<in> carrier H"
    1.14 -  by (auto simp add: hom_def funcset_mem)
    1.15 -
    1.16  lemma (in group) hom_compose:
    1.17       "[|h \<in> hom G H; i \<in> hom H I|] ==> compose (carrier G) i h \<in> hom G I"
    1.18  apply (auto simp add: hom_def funcset_compose) 
    1.19 @@ -589,8 +580,20 @@
    1.20  locale group_hom = G: group G + H: group H for G (structure) and H (structure) +
    1.21    fixes h
    1.22    assumes homh: "h \<in> hom G H"
    1.23 -  notes hom_mult [simp] = hom_mult [OF homh]
    1.24 -    and hom_closed [simp] = hom_closed [OF homh]
    1.25 +
    1.26 +lemma (in group_hom) hom_mult [simp]:
    1.27 +  "[| x \<in> carrier G; y \<in> carrier G |] ==> h (x \<otimes>\<^bsub>G\<^esub> y) = h x \<otimes>\<^bsub>H\<^esub> h y"
    1.28 +proof -
    1.29 +  assume "x \<in> carrier G" "y \<in> carrier G"
    1.30 +  with homh [unfolded hom_def] show ?thesis by simp
    1.31 +qed
    1.32 +
    1.33 +lemma (in group_hom) hom_closed [simp]:
    1.34 +  "x \<in> carrier G ==> h x \<in> carrier H"
    1.35 +proof -
    1.36 +  assume "x \<in> carrier G"
    1.37 +  with homh [unfolded hom_def] show ?thesis by (auto simp add: funcset_mem)
    1.38 +qed
    1.39  
    1.40  lemma (in group_hom) one_closed [simp]:
    1.41    "h \<one> \<in> carrier H"
     2.1 --- a/src/HOL/Algebra/Ideal.thy	Wed Dec 17 17:53:41 2008 +0100
     2.2 +++ b/src/HOL/Algebra/Ideal.thy	Wed Dec 17 17:53:56 2008 +0100
     2.3 @@ -13,7 +13,7 @@
     2.4  
     2.5  subsubsection {* General definition *}
     2.6  
     2.7 -locale ideal = additive_subgroup I R + ring R +
     2.8 +locale ideal = additive_subgroup I R + ring R for I and R (structure) +
     2.9    assumes I_l_closed: "\<lbrakk>a \<in> I; x \<in> carrier R\<rbrakk> \<Longrightarrow> x \<otimes> a \<in> I"
    2.10        and I_r_closed: "\<lbrakk>a \<in> I; x \<in> carrier R\<rbrakk> \<Longrightarrow> a \<otimes> x \<in> I"
    2.11  
    2.12 @@ -127,7 +127,7 @@
    2.13        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"
    2.14    shows "primeideal I R"
    2.15  proof -
    2.16 -  interpret additive_subgroup [I R] by fact
    2.17 +  interpret additive_subgroup I R by fact
    2.18    interpret cring R by fact
    2.19    show ?thesis apply (intro_locales)
    2.20      apply (intro ideal_axioms.intro)
    2.21 @@ -207,7 +207,7 @@
    2.22    shows "ideal (I \<inter> J) R"
    2.23  proof -
    2.24    interpret ideal I R by fact
    2.25 -  interpret ideal [J R] by fact
    2.26 +  interpret ideal J R by fact
    2.27    show ?thesis
    2.28  apply (intro idealI subgroup.intro)
    2.29        apply (rule is_ring)
    2.30 @@ -532,7 +532,7 @@
    2.31    assumes aJ: "a \<in> J"
    2.32    shows "PIdl a \<subseteq> J"
    2.33  proof -
    2.34 -  interpret ideal [J R] by fact
    2.35 +  interpret ideal J R by fact
    2.36    show ?thesis unfolding cgenideal_def
    2.37      apply rule
    2.38      apply clarify
    2.39 @@ -579,7 +579,7 @@
    2.40    shows "Idl (I \<union> J) = I <+> J"
    2.41  apply rule
    2.42   apply (rule ring.genideal_minimal)
    2.43 -   apply (rule R.is_ring)
    2.44 +   apply (rule is_ring)
    2.45    apply (rule add_ideals[OF idealI idealJ])
    2.46   apply (rule)
    2.47   apply (simp add: set_add_defs) apply (elim disjE) defer 1 defer 1
    2.48 @@ -829,7 +829,7 @@
    2.49        by fast
    2.50      def J \<equiv> "{x\<in>carrier R. a \<otimes> x \<in> I}"
    2.51      
    2.52 -    from R.is_cring and acarr
    2.53 +    from is_cring and acarr
    2.54      have idealJ: "ideal J R" unfolding J_def by (rule helper_max_prime)
    2.55      
    2.56      have IsubJ: "I \<subseteq> J"
     3.1 --- a/src/HOL/Algebra/RingHom.thy	Wed Dec 17 17:53:41 2008 +0100
     3.2 +++ b/src/HOL/Algebra/RingHom.thy	Wed Dec 17 17:53:56 2008 +0100
     3.3 @@ -10,7 +10,8 @@
     3.4  section {* Homomorphisms of Non-Commutative Rings *}
     3.5  
     3.6  text {* Lifting existing lemmas in a @{text ring_hom_ring} locale *}
     3.7 -locale ring_hom_ring = R: ring R + S: ring S +
     3.8 +locale ring_hom_ring = R: ring R + S: ring S
     3.9 +    for R (structure) and S (structure) +
    3.10    fixes h
    3.11    assumes homh: "h \<in> ring_hom R S"
    3.12    notes hom_mult [simp] = ring_hom_mult [OF homh]
     4.1 --- a/src/HOL/Algebra/UnivPoly.thy	Wed Dec 17 17:53:41 2008 +0100
     4.2 +++ b/src/HOL/Algebra/UnivPoly.thy	Wed Dec 17 17:53:56 2008 +0100
     4.3 @@ -175,17 +175,17 @@
     4.4    fixes R (structure) and P (structure)
     4.5    defines P_def: "P == UP R"
     4.6  
     4.7 -locale UP_ring = UP + ring R
     4.8 +locale UP_ring = UP + R: ring R
     4.9  
    4.10 -locale UP_cring = UP + cring R
    4.11 +locale UP_cring = UP + R: cring R
    4.12  
    4.13  sublocale UP_cring < UP_ring
    4.14 -  by (rule P_def) intro_locales
    4.15 +  by intro_locales [1] (rule P_def)
    4.16  
    4.17 -locale UP_domain = UP + "domain" R
    4.18 +locale UP_domain = UP + R: "domain" R
    4.19  
    4.20  sublocale UP_domain < UP_cring
    4.21 -  by (rule P_def) intro_locales
    4.22 +  by intro_locales [1] (rule P_def)
    4.23  
    4.24  context UP
    4.25  begin
    4.26 @@ -457,8 +457,8 @@
    4.27  
    4.28  end
    4.29  
    4.30 -sublocale UP_ring < ring P using UP_ring .
    4.31 -sublocale UP_cring < cring P using UP_cring .
    4.32 +sublocale UP_ring < P: ring P using UP_ring .
    4.33 +sublocale UP_cring < P: cring P using UP_cring .
    4.34  
    4.35  
    4.36  subsection {* Polynomials Form an Algebra *}
    4.37 @@ -1203,7 +1203,9 @@
    4.38  
    4.39  text {* The universal property of the polynomial ring *}
    4.40  
    4.41 -locale UP_pre_univ_prop = ring_hom_cring R S h + UP_cring R P
    4.42 +locale UP_pre_univ_prop = ring_hom_cring + UP_cring
    4.43 +
    4.44 +(* FIXME print_locale ring_hom_cring fails *)
    4.45  
    4.46  locale UP_univ_prop = UP_pre_univ_prop +
    4.47    fixes s and Eval