src/HOL/Algebra/RingHom.thy
changeset 27611 2c01c0bdb385
parent 26204 da9778392d8c
child 27717 21bbd410ba04
     1.1 --- a/src/HOL/Algebra/RingHom.thy	Tue Jul 15 16:02:10 2008 +0200
     1.2 +++ b/src/HOL/Algebra/RingHom.thy	Tue Jul 15 16:50:09 2008 +0200
     1.3 @@ -31,55 +31,73 @@
     1.4  done
     1.5  
     1.6  lemma (in ring_hom_ring) is_ring_hom_ring:
     1.7 -  includes struct R + struct S
     1.8 -  shows "ring_hom_ring R S h"
     1.9 -by (rule ring_hom_ring_axioms)
    1.10 +  "ring_hom_ring R S h"
    1.11 +  by (rule ring_hom_ring_axioms)
    1.12  
    1.13  lemma ring_hom_ringI:
    1.14 -  includes ring R + ring S
    1.15 +  fixes R (structure) and S (structure)
    1.16 +  assumes "ring R" "ring S"
    1.17    assumes (* morphism: "h \<in> carrier R \<rightarrow> carrier S" *)
    1.18            hom_closed: "!!x. x \<in> carrier R ==> h x \<in> carrier S"
    1.19        and compatible_mult: "!!x y. [| x : carrier R; y : carrier R |] ==> h (x \<otimes> y) = h x \<otimes>\<^bsub>S\<^esub> h y"
    1.20        and compatible_add: "!!x y. [| x : carrier R; y : carrier R |] ==> h (x \<oplus> y) = h x \<oplus>\<^bsub>S\<^esub> h y"
    1.21        and compatible_one: "h \<one> = \<one>\<^bsub>S\<^esub>"
    1.22    shows "ring_hom_ring R S h"
    1.23 -apply unfold_locales
    1.24 +proof -
    1.25 +  interpret ring [R] by fact
    1.26 +  interpret ring [S] by fact
    1.27 +  show ?thesis apply unfold_locales
    1.28  apply (unfold ring_hom_def, safe)
    1.29     apply (simp add: hom_closed Pi_def)
    1.30    apply (erule (1) compatible_mult)
    1.31   apply (erule (1) compatible_add)
    1.32  apply (rule compatible_one)
    1.33  done
    1.34 +qed
    1.35  
    1.36  lemma ring_hom_ringI2:
    1.37 -  includes ring R + ring S
    1.38 +  assumes "ring R" "ring S"
    1.39    assumes h: "h \<in> ring_hom R S"
    1.40    shows "ring_hom_ring R S h"
    1.41 -apply (intro ring_hom_ring.intro ring_hom_ring_axioms.intro)
    1.42 -apply (rule R.is_ring)
    1.43 -apply (rule S.is_ring)
    1.44 -apply (rule h)
    1.45 -done
    1.46 +proof -
    1.47 +  interpret R: ring [R] by fact
    1.48 +  interpret S: ring [S] by fact
    1.49 +  show ?thesis apply (intro ring_hom_ring.intro ring_hom_ring_axioms.intro)
    1.50 +    apply (rule R.is_ring)
    1.51 +    apply (rule S.is_ring)
    1.52 +    apply (rule h)
    1.53 +    done
    1.54 +qed
    1.55  
    1.56  lemma ring_hom_ringI3:
    1.57 -  includes abelian_group_hom R S + ring R + ring S 
    1.58 +  fixes R (structure) and S (structure)
    1.59 +  assumes "abelian_group_hom R S h" "ring R" "ring S" 
    1.60    assumes compatible_mult: "!!x y. [| x : carrier R; y : carrier R |] ==> h (x \<otimes> y) = h x \<otimes>\<^bsub>S\<^esub> h y"
    1.61        and compatible_one: "h \<one> = \<one>\<^bsub>S\<^esub>"
    1.62    shows "ring_hom_ring R S h"
    1.63 -apply (intro ring_hom_ring.intro ring_hom_ring_axioms.intro, rule R.is_ring, rule S.is_ring)
    1.64 -apply (insert group_hom.homh[OF a_group_hom])
    1.65 -apply (unfold hom_def ring_hom_def, simp)
    1.66 -apply safe
    1.67 -apply (erule (1) compatible_mult)
    1.68 -apply (rule compatible_one)
    1.69 -done
    1.70 +proof -
    1.71 +  interpret abelian_group_hom [R S h] by fact
    1.72 +  interpret R: ring [R] by fact
    1.73 +  interpret S: ring [S] by fact
    1.74 +  show ?thesis apply (intro ring_hom_ring.intro ring_hom_ring_axioms.intro, rule R.is_ring, rule S.is_ring)
    1.75 +    apply (insert group_hom.homh[OF a_group_hom])
    1.76 +    apply (unfold hom_def ring_hom_def, simp)
    1.77 +    apply safe
    1.78 +    apply (erule (1) compatible_mult)
    1.79 +    apply (rule compatible_one)
    1.80 +    done
    1.81 +qed
    1.82  
    1.83  lemma ring_hom_cringI:
    1.84 -  includes ring_hom_ring R S h + cring R + cring S
    1.85 +  assumes "ring_hom_ring R S h" "cring R" "cring S"
    1.86    shows "ring_hom_cring R S h"
    1.87 -  by (intro ring_hom_cring.intro ring_hom_cring_axioms.intro)
    1.88 +proof -
    1.89 +  interpret ring_hom_ring [R S h] by fact
    1.90 +  interpret R: cring [R] by fact
    1.91 +  interpret S: cring [S] by fact
    1.92 +  show ?thesis by (intro ring_hom_cring.intro ring_hom_cring_axioms.intro)
    1.93      (rule R.is_cring, rule S.is_cring, rule homh)
    1.94 -
    1.95 +qed
    1.96  
    1.97  subsection {* The kernel of a ring homomorphism *}
    1.98