# HG changeset patch # User ballarin # Date 1154609846 -7200 # Node ID 0e0ea63fe7689e6e05812b258c6cdad190d741c4 # Parent 6e070b33e72bbfcaa0c7d39cd59ead77699fd37f Restructured algebra library, added ideals and quotient rings. diff -r 6e070b33e72b -r 0e0ea63fe768 NEWS --- a/NEWS Thu Aug 03 14:53:57 2006 +0200 +++ b/NEWS Thu Aug 03 14:57:26 2006 +0200 @@ -521,7 +521,13 @@ *** HOL-Algebra *** * Method algebra is now set up via an attribute. For examples see CRing.thy. - INCOMPATIBILITY: the method is now weaker on combinations of algebraic structures. + INCOMPATIBILITY: the method is now weaker on combinations of algebraic + structures. + +* Formalisation of ideals and the quotient construction over rings, contributed + by Stephan Hohe. + +* Renamed `CRing.thy' to `Ring.thy'. INCOMPATIBILITY. *** HOL-Complex *** diff -r 6e070b33e72b -r 0e0ea63fe768 src/HOL/Algebra/AbelCoset.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Algebra/AbelCoset.thy Thu Aug 03 14:57:26 2006 +0200 @@ -0,0 +1,734 @@ +(* + Title: HOL/Algebra/AbelCoset.thy + Id: $Id$ + Author: Stephan Hohe, TU Muenchen +*) + +theory AbelCoset +imports Coset Ring +begin + + +section {* More Lifting from Groups to Abelian Groups *} + +subsection {* Definitions *} + +text {* Hiding @{text "<+>"} from \texttt{Sum\_Type.thy} until I come + up with better syntax here *} + +hide const Plus + +constdefs (structure G) + a_r_coset :: "[_, 'a set, 'a] \ 'a set" (infixl "+>\" 60) + "a_r_coset G \ r_coset \carrier = carrier G, mult = add G, one = zero G\" + + a_l_coset :: "[_, 'a, 'a set] \ 'a set" (infixl "<+\" 60) + "a_l_coset G \ l_coset \carrier = carrier G, mult = add G, one = zero G\" + + A_RCOSETS :: "[_, 'a set] \ ('a set)set" ("a'_rcosets\ _" [81] 80) + "A_RCOSETS G H \ RCOSETS \carrier = carrier G, mult = add G, one = zero G\ H" + + set_add :: "[_, 'a set ,'a set] \ 'a set" (infixl "<+>\" 60) + "set_add G \ set_mult \carrier = carrier G, mult = add G, one = zero G\" + + A_SET_INV :: "[_,'a set] \ 'a set" ("a'_set'_inv\ _" [81] 80) + "A_SET_INV G H \ SET_INV \carrier = carrier G, mult = add G, one = zero G\ H" + +constdefs (structure G) + a_r_congruent :: "[('a,'b)ring_scheme, 'a set] \ ('a*'a)set" + ("racong\ _") + "a_r_congruent G \ r_congruent \carrier = carrier G, mult = add G, one = zero G\" + +constdefs + A_FactGroup :: "[('a,'b) ring_scheme, 'a set] \ ('a set) monoid" + (infixl "A'_Mod" 65) + --{*Actually defined for groups rather than monoids*} + "A_FactGroup G H \ FactGroup \carrier = carrier G, mult = add G, one = zero G\ H" + +constdefs + a_kernel :: "('a, 'm) ring_scheme \ ('b, 'n) ring_scheme \ + ('a \ 'b) \ 'a set" + --{*the kernel of a homomorphism (additive)*} + "a_kernel G H h \ kernel \carrier = carrier G, mult = add G, one = zero G\ + \carrier = carrier H, mult = add H, one = zero H\ h" + +locale abelian_group_hom = abelian_group G + abelian_group H + var h + + assumes a_group_hom: "group_hom (| carrier = carrier G, mult = add G, one = zero G |) + (| carrier = carrier H, mult = add H, one = zero H |) h" + +lemmas a_r_coset_defs = + a_r_coset_def r_coset_def + +lemma a_r_coset_def': + includes struct G + shows "H +> a \ \h\H. {h \ a}" +unfolding a_r_coset_defs +by simp + +lemmas a_l_coset_defs = + a_l_coset_def l_coset_def + +lemma a_l_coset_def': + includes struct G + shows "a <+ H \ \h\H. {a \ h}" +unfolding a_l_coset_defs +by simp + +lemmas A_RCOSETS_defs = + A_RCOSETS_def RCOSETS_def + +lemma A_RCOSETS_def': + includes struct G + shows "a_rcosets H \ \a\carrier G. {H +> a}" +unfolding A_RCOSETS_defs +by (fold a_r_coset_def, simp) + +lemmas set_add_defs = + set_add_def set_mult_def + +lemma set_add_def': + includes struct G + shows "H <+> K \ \h\H. \k\K. {h \ k}" +unfolding set_add_defs +by simp + +lemmas A_SET_INV_defs = + A_SET_INV_def SET_INV_def + +lemma A_SET_INV_def': + includes struct G + shows "a_set_inv H \ \h\H. {\ h}" +unfolding A_SET_INV_defs +by (fold a_inv_def) + + +subsection {* Cosets *} + +lemma (in abelian_group) a_coset_add_assoc: + "[| M \ carrier G; g \ carrier G; h \ carrier G |] + ==> (M +> g) +> h = M +> (g \ h)" +by (rule group.coset_mult_assoc [OF a_group, + folded a_r_coset_def, simplified monoid_record_simps]) + +lemma (in abelian_group) a_coset_add_zero [simp]: + "M \ carrier G ==> M +> \ = M" +by (rule group.coset_mult_one [OF a_group, + folded a_r_coset_def, simplified monoid_record_simps]) + +lemma (in abelian_group) a_coset_add_inv1: + "[| M +> (x \ (\ y)) = M; x \ carrier G ; y \ carrier G; + M \ carrier G |] ==> M +> x = M +> y" +by (rule group.coset_mult_inv1 [OF a_group, + folded a_r_coset_def a_inv_def, simplified monoid_record_simps]) + +lemma (in abelian_group) a_coset_add_inv2: + "[| M +> x = M +> y; x \ carrier G; y \ carrier G; M \ carrier G |] + ==> M +> (x \ (\ y)) = M" +by (rule group.coset_mult_inv2 [OF a_group, + folded a_r_coset_def a_inv_def, simplified monoid_record_simps]) + +lemma (in abelian_group) a_coset_join1: + "[| H +> x = H; x \ carrier G; subgroup H (|carrier = carrier G, mult = add G, one = zero G|) |] ==> x \ H" +by (rule group.coset_join1 [OF a_group, + folded a_r_coset_def, simplified monoid_record_simps]) + +lemma (in abelian_group) a_solve_equation: + "\subgroup H (|carrier = carrier G, mult = add G, one = zero G|); x \ H; y \ H\ \ \h\H. y = h \ x" +by (rule group.solve_equation [OF a_group, + folded a_r_coset_def, simplified monoid_record_simps]) + +lemma (in abelian_group) a_repr_independence: + "\y \ H +> x; x \ carrier G; subgroup H \carrier = carrier G, mult = add G, one = zero G\ \ \ H +> x = H +> y" +by (rule group.repr_independence [OF a_group, + folded a_r_coset_def, simplified monoid_record_simps]) + +lemma (in abelian_group) a_coset_join2: + "\x \ carrier G; subgroup H \carrier = carrier G, mult = add G, one = zero G\; x\H\ \ H +> x = H" +by (rule group.coset_join2 [OF a_group, + folded a_r_coset_def, simplified monoid_record_simps]) + +lemma (in abelian_monoid) a_r_coset_subset_G: + "[| H \ carrier G; x \ carrier G |] ==> H +> x \ carrier G" +by (rule monoid.r_coset_subset_G [OF a_monoid, + folded a_r_coset_def, simplified monoid_record_simps]) + +lemma (in abelian_group) a_rcosI: + "[| h \ H; H \ carrier G; x \ carrier G|] ==> h \ x \ H +> x" +by (rule group.rcosI [OF a_group, + folded a_r_coset_def, simplified monoid_record_simps]) + +lemma (in abelian_group) a_rcosetsI: + "\H \ carrier G; x \ carrier G\ \ H +> x \ a_rcosets H" +by (rule group.rcosetsI [OF a_group, + folded a_r_coset_def A_RCOSETS_def, simplified monoid_record_simps]) + +text{*Really needed?*} +lemma (in abelian_group) a_transpose_inv: + "[| x \ y = z; x \ carrier G; y \ carrier G; z \ carrier G |] + ==> (\ x) \ z = y" +by (rule group.transpose_inv [OF a_group, + folded a_r_coset_def a_inv_def, simplified monoid_record_simps]) + +(* +--"duplicate" +lemma (in abelian_group) a_rcos_self: + "[| x \ carrier G; subgroup H \carrier = carrier G, mult = add G, one = zero G\ |] ==> x \ H +> x" +by (rule group.rcos_self [OF a_group, + folded a_r_coset_def, simplified monoid_record_simps]) +*) + + +subsection {* Subgroups *} + +locale additive_subgroup = var H + struct G + + assumes a_subgroup: "subgroup H \carrier = carrier G, mult = add G, one = zero G\" + +lemma (in additive_subgroup) is_additive_subgroup: + shows "additive_subgroup H G" +by - + +lemma additive_subgroupI: + includes struct G + assumes a_subgroup: "subgroup H \carrier = carrier G, mult = add G, one = zero G\" + shows "additive_subgroup H G" +by (rule additive_subgroup.intro) + +lemma (in additive_subgroup) a_subset: + "H \ carrier G" +by (rule subgroup.subset[OF a_subgroup, + simplified monoid_record_simps]) + +lemma (in additive_subgroup) a_closed [intro, simp]: + "\x \ H; y \ H\ \ x \ y \ H" +by (rule subgroup.m_closed[OF a_subgroup, + simplified monoid_record_simps]) + +lemma (in additive_subgroup) zero_closed [simp]: + "\ \ H" +by (rule subgroup.one_closed[OF a_subgroup, + simplified monoid_record_simps]) + +lemma (in additive_subgroup) a_inv_closed [intro,simp]: + "x \ H \ \ x \ H" +by (rule subgroup.m_inv_closed[OF a_subgroup, + folded a_inv_def, simplified monoid_record_simps]) + + +subsection {* Normal additive subgroups *} + +subsubsection {* Definition of @{text "abelian_subgroup"} *} + +text {* Every subgroup of an @{text "abelian_group"} is normal *} + +locale abelian_subgroup = additive_subgroup H G + abelian_group G + + assumes a_normal: "normal H \carrier = carrier G, mult = add G, one = zero G\" + +lemma (in abelian_subgroup) is_abelian_subgroup: + shows "abelian_subgroup H G" +by - + +lemma abelian_subgroupI: + assumes a_normal: "normal H \carrier = carrier G, mult = add G, one = zero G\" + and a_comm: "!!x y. [| x \ carrier G; y \ carrier G |] ==> x \\<^bsub>G\<^esub> y = y \\<^bsub>G\<^esub> x" + shows "abelian_subgroup H G" +proof - + interpret normal ["H" "\carrier = carrier G, mult = add G, one = zero G\"] + by (rule a_normal) + + show "abelian_subgroup H G" + by (unfold_locales, simp add: a_comm) +qed + +lemma abelian_subgroupI2: + includes struct G + assumes a_comm_group: "comm_group \carrier = carrier G, mult = add G, one = zero G\" + and a_subgroup: "subgroup H \carrier = carrier G, mult = add G, one = zero G\" + shows "abelian_subgroup H G" +proof - + interpret comm_group ["\carrier = carrier G, mult = add G, one = zero G\"] + by (rule a_comm_group) + interpret subgroup ["H" "\carrier = carrier G, mult = add G, one = zero G\"] + by (rule a_subgroup) + + show "abelian_subgroup H G" + apply unfold_locales + proof (simp add: r_coset_def l_coset_def, clarsimp) + fix x + assume xcarr: "x \ carrier G" + from a_subgroup + have Hcarr: "H \ carrier G" by (unfold subgroup_def, simp) + from xcarr Hcarr + show "(\h\H. {h \\<^bsub>G\<^esub> x}) = (\h\H. {x \\<^bsub>G\<^esub> h})" + using m_comm[simplified] + by fast + qed +qed + +lemma abelian_subgroupI3: + includes struct G + assumes asg: "additive_subgroup H G" + and ag: "abelian_group G" + shows "abelian_subgroup H G" +apply (rule abelian_subgroupI2) + apply (rule abelian_group.a_comm_group[OF ag]) +apply (rule additive_subgroup.a_subgroup[OF asg]) +done + +lemma (in abelian_subgroup) a_coset_eq: + "(\x \ carrier G. H +> x = x <+ H)" +by (rule normal.coset_eq[OF a_normal, + folded a_r_coset_def a_l_coset_def, simplified monoid_record_simps]) + +lemma (in abelian_subgroup) a_inv_op_closed1: + shows "\x \ carrier G; h \ H\ \ (\ x) \ h \ x \ H" +by (rule normal.inv_op_closed1 [OF a_normal, + folded a_inv_def, simplified monoid_record_simps]) + +lemma (in abelian_subgroup) a_inv_op_closed2: + shows "\x \ carrier G; h \ H\ \ x \ h \ (\ x) \ H" +by (rule normal.inv_op_closed2 [OF a_normal, + folded a_inv_def, simplified monoid_record_simps]) + +text{*Alternative characterization of normal subgroups*} +lemma (in abelian_group) a_normal_inv_iff: + "(N \ \carrier = carrier G, mult = add G, one = zero G\) = + (subgroup N \carrier = carrier G, mult = add G, one = zero G\ & (\x \ carrier G. \h \ N. x \ h \ (\ x) \ N))" + (is "_ = ?rhs") +by (rule group.normal_inv_iff [OF a_group, + folded a_inv_def, simplified monoid_record_simps]) + +lemma (in abelian_group) a_lcos_m_assoc: + "[| M \ carrier G; g \ carrier G; h \ carrier G |] + ==> g <+ (h <+ M) = (g \ h) <+ M" +by (rule group.lcos_m_assoc [OF a_group, + folded a_l_coset_def, simplified monoid_record_simps]) + +lemma (in abelian_group) a_lcos_mult_one: + "M \ carrier G ==> \ <+ M = M" +by (rule group.lcos_mult_one [OF a_group, + folded a_l_coset_def, simplified monoid_record_simps]) + + +lemma (in abelian_group) a_l_coset_subset_G: + "[| H \ carrier G; x \ carrier G |] ==> x <+ H \ carrier G" +by (rule group.l_coset_subset_G [OF a_group, + folded a_l_coset_def, simplified monoid_record_simps]) + + +lemma (in abelian_group) a_l_coset_swap: + "\y \ x <+ H; x \ carrier G; subgroup H \carrier = carrier G, mult = add G, one = zero G\\ \ x \ y <+ H" +by (rule group.l_coset_swap [OF a_group, + folded a_l_coset_def, simplified monoid_record_simps]) + +lemma (in abelian_group) a_l_coset_carrier: + "[| y \ x <+ H; x \ carrier G; subgroup H \carrier = carrier G, mult = add G, one = zero G\ |] ==> y \ carrier G" +by (rule group.l_coset_carrier [OF a_group, + folded a_l_coset_def, simplified monoid_record_simps]) + +lemma (in abelian_group) a_l_repr_imp_subset: + assumes y: "y \ x <+ H" and x: "x \ carrier G" and sb: "subgroup H \carrier = carrier G, mult = add G, one = zero G\" + shows "y <+ H \ x <+ H" +by (rule group.l_repr_imp_subset [OF a_group, + folded a_l_coset_def, simplified monoid_record_simps]) + +lemma (in abelian_group) a_l_repr_independence: + assumes y: "y \ x <+ H" and x: "x \ carrier G" and sb: "subgroup H \carrier = carrier G, mult = add G, one = zero G\" + shows "x <+ H = y <+ H" +by (rule group.l_repr_independence [OF a_group, + folded a_l_coset_def, simplified monoid_record_simps]) + +lemma (in abelian_group) setadd_subset_G: + "\H \ carrier G; K \ carrier G\ \ H <+> K \ carrier G" +by (rule group.setmult_subset_G [OF a_group, + folded set_add_def, simplified monoid_record_simps]) + +lemma (in abelian_group) subgroup_add_id: "subgroup H \carrier = carrier G, mult = add G, one = zero G\ \ H <+> H = H" +by (rule group.subgroup_mult_id [OF a_group, + folded set_add_def, simplified monoid_record_simps]) + +lemma (in abelian_subgroup) a_rcos_inv: + assumes x: "x \ carrier G" + shows "a_set_inv (H +> x) = H +> (\ x)" +by (rule normal.rcos_inv [OF a_normal, + folded a_r_coset_def a_inv_def A_SET_INV_def, simplified monoid_record_simps]) + +lemma (in abelian_group) a_setmult_rcos_assoc: + "\H \ carrier G; K \ carrier G; x \ carrier G\ + \ H <+> (K +> x) = (H <+> K) +> x" +by (rule group.setmult_rcos_assoc [OF a_group, + folded set_add_def a_r_coset_def, simplified monoid_record_simps]) + +lemma (in abelian_group) a_rcos_assoc_lcos: + "\H \ carrier G; K \ carrier G; x \ carrier G\ + \ (H +> x) <+> K = H <+> (x <+ K)" +by (rule group.rcos_assoc_lcos [OF a_group, + folded set_add_def a_r_coset_def a_l_coset_def, simplified monoid_record_simps]) + +lemma (in abelian_subgroup) a_rcos_sum: + "\x \ carrier G; y \ carrier G\ + \ (H +> x) <+> (H +> y) = H +> (x \ y)" +by (rule normal.rcos_sum [OF a_normal, + folded set_add_def a_r_coset_def, simplified monoid_record_simps]) + +lemma (in abelian_subgroup) rcosets_add_eq: + "M \ a_rcosets H \ H <+> M = M" + -- {* generalizes @{text subgroup_mult_id} *} +by (rule normal.rcosets_mult_eq [OF a_normal, + folded set_add_def A_RCOSETS_def, simplified monoid_record_simps]) + + +subsection {* Congruence Relation *} + +lemma (in abelian_subgroup) a_equiv_rcong: + shows "equiv (carrier G) (racong H)" +by (rule subgroup.equiv_rcong [OF a_subgroup a_group, + folded a_r_congruent_def, simplified monoid_record_simps]) + +lemma (in abelian_subgroup) a_l_coset_eq_rcong: + assumes a: "a \ carrier G" + shows "a <+ H = racong H `` {a}" +by (rule subgroup.l_coset_eq_rcong [OF a_subgroup a_group, + folded a_r_congruent_def a_l_coset_def, simplified monoid_record_simps]) + +lemma (in abelian_subgroup) a_rcos_equation: + shows + "\ha \ a = h \ b; a \ carrier G; b \ carrier G; + h \ H; ha \ H; hb \ H\ + \ hb \ a \ (\h\H. {h \ b})" +by (rule group.rcos_equation [OF a_group a_subgroup, + folded a_r_congruent_def a_l_coset_def, simplified monoid_record_simps]) + +lemma (in abelian_subgroup) a_rcos_disjoint: + shows "\a \ a_rcosets H; b \ a_rcosets H; a\b\ \ a \ b = {}" +by (rule group.rcos_disjoint [OF a_group a_subgroup, + folded A_RCOSETS_def, simplified monoid_record_simps]) + +lemma (in abelian_subgroup) a_rcos_self: + shows "x \ carrier G \ x \ H +> x" +by (rule group.rcos_self [OF a_group a_subgroup, + folded a_r_coset_def, simplified monoid_record_simps]) + +lemma (in abelian_subgroup) a_rcosets_part_G: + shows "\(a_rcosets H) = carrier G" +by (rule group.rcosets_part_G [OF a_group a_subgroup, + folded A_RCOSETS_def, simplified monoid_record_simps]) + +lemma (in abelian_subgroup) a_cosets_finite: + "\c \ a_rcosets H; H \ carrier G; finite (carrier G)\ \ finite c" +by (rule group.cosets_finite [OF a_group, + folded A_RCOSETS_def, simplified monoid_record_simps]) + +lemma (in abelian_group) a_card_cosets_equal: + "\c \ a_rcosets H; H \ carrier G; finite(carrier G)\ + \ card c = card H" +by (rule group.card_cosets_equal [OF a_group, + folded A_RCOSETS_def, simplified monoid_record_simps]) + +lemma (in abelian_group) rcosets_subset_PowG: + "additive_subgroup H G \ a_rcosets H \ Pow(carrier G)" +by (rule group.rcosets_subset_PowG [OF a_group, + folded A_RCOSETS_def, simplified monoid_record_simps], + rule additive_subgroup.a_subgroup) + +theorem (in abelian_group) a_lagrange: + "\finite(carrier G); additive_subgroup H G\ + \ card(a_rcosets H) * card(H) = order(G)" +by (rule group.lagrange [OF a_group, + folded A_RCOSETS_def, simplified monoid_record_simps order_def, folded order_def]) + (fast intro!: additive_subgroup.a_subgroup)+ + + +subsection {* Factorization *} + +lemmas A_FactGroup_defs = A_FactGroup_def FactGroup_def + +lemma A_FactGroup_def': + includes struct G + shows "G A_Mod H \ \carrier = a_rcosets\<^bsub>G\<^esub> H, mult = set_add G, one = H\" +unfolding A_FactGroup_defs +by (fold A_RCOSETS_def set_add_def) + + +lemma (in abelian_subgroup) a_setmult_closed: + "\K1 \ a_rcosets H; K2 \ a_rcosets H\ \ K1 <+> K2 \ a_rcosets H" +by (rule normal.setmult_closed [OF a_normal, + folded A_RCOSETS_def set_add_def, simplified monoid_record_simps]) + +lemma (in abelian_subgroup) a_setinv_closed: + "K \ a_rcosets H \ a_set_inv K \ a_rcosets H" +by (rule normal.setinv_closed [OF a_normal, + folded A_RCOSETS_def A_SET_INV_def, simplified monoid_record_simps]) + +lemma (in abelian_subgroup) a_rcosets_assoc: + "\M1 \ a_rcosets H; M2 \ a_rcosets H; M3 \ a_rcosets H\ + \ M1 <+> M2 <+> M3 = M1 <+> (M2 <+> M3)" +by (rule normal.rcosets_assoc [OF a_normal, + folded A_RCOSETS_def set_add_def, simplified monoid_record_simps]) + +lemma (in abelian_subgroup) a_subgroup_in_rcosets: + "H \ a_rcosets H" +by (rule subgroup.subgroup_in_rcosets [OF a_subgroup a_group, + folded A_RCOSETS_def, simplified monoid_record_simps]) + +lemma (in abelian_subgroup) a_rcosets_inv_mult_group_eq: + "M \ a_rcosets H \ a_set_inv M <+> M = H" +by (rule normal.rcosets_inv_mult_group_eq [OF a_normal, + folded A_RCOSETS_def A_SET_INV_def set_add_def, simplified monoid_record_simps]) + +theorem (in abelian_subgroup) a_factorgroup_is_group: + "group (G A_Mod H)" +by (rule normal.factorgroup_is_group [OF a_normal, + folded A_FactGroup_def, simplified monoid_record_simps]) + +text {* Since the Factorization is based on an \emph{abelian} subgroup, is results in + a commutative group *} +theorem (in abelian_subgroup) a_factorgroup_is_comm_group: + "comm_group (G A_Mod H)" +apply (intro comm_group.intro comm_monoid.intro) prefer 3 + apply (rule a_factorgroup_is_group) + apply (rule group.axioms[OF a_factorgroup_is_group]) +apply (rule comm_monoid_axioms.intro) +apply (unfold A_FactGroup_def FactGroup_def RCOSETS_def, fold set_add_def a_r_coset_def, clarsimp) +apply (simp add: a_rcos_sum a_comm) +done + +lemma add_A_FactGroup [simp]: "X \\<^bsub>(G A_Mod H)\<^esub> X' = X <+>\<^bsub>G\<^esub> X'" +by (simp add: A_FactGroup_def set_add_def) + +lemma (in abelian_subgroup) a_inv_FactGroup: + "X \ carrier (G A_Mod H) \ inv\<^bsub>G A_Mod H\<^esub> X = a_set_inv X" +by (rule normal.inv_FactGroup [OF a_normal, + folded A_FactGroup_def A_SET_INV_def, simplified monoid_record_simps]) + +text{*The coset map is a homomorphism from @{term G} to the quotient group + @{term "G Mod H"}*} +lemma (in abelian_subgroup) a_r_coset_hom_A_Mod: + "(\a. H +> a) \ hom \carrier = carrier G, mult = add G, one = zero G\ (G A_Mod H)" +by (rule normal.r_coset_hom_Mod [OF a_normal, + folded A_FactGroup_def a_r_coset_def, simplified monoid_record_simps]) + +text {* The isomorphism theorems have been omitted from lifting, at + least for now *} + +subsection{*The First Isomorphism Theorem*} + +text{*The quotient by the kernel of a homomorphism is isomorphic to the + range of that homomorphism.*} + +lemmas a_kernel_defs = + a_kernel_def kernel_def + +lemma a_kernel_def': + "a_kernel R S h \ {x \ carrier R. h x = \\<^bsub>S\<^esub>}" +by (rule a_kernel_def[unfolded kernel_def, simplified ring_record_simps]) + + +subsection {* Homomorphisms *} + +lemma abelian_group_homI: + includes abelian_group G + includes abelian_group H + assumes a_group_hom: "group_hom (| carrier = carrier G, mult = add G, one = zero G |) + (| carrier = carrier H, mult = add H, one = zero H |) h" + shows "abelian_group_hom G H h" +by (intro abelian_group_hom.intro abelian_group_hom_axioms.intro) + +lemma (in abelian_group_hom) is_abelian_group_hom: + "abelian_group_hom G H h" +by (unfold_locales) + +lemma (in abelian_group_hom) hom_add [simp]: + "[| x : carrier G; y : carrier G |] + ==> h (x \\<^bsub>G\<^esub> y) = h x \\<^bsub>H\<^esub> h y" +by (rule group_hom.hom_mult[OF a_group_hom, + simplified ring_record_simps]) + +lemma (in abelian_group_hom) hom_closed [simp]: + "x \ carrier G \ h x \ carrier H" +by (rule group_hom.hom_closed[OF a_group_hom, + simplified ring_record_simps]) + +lemma (in abelian_group_hom) zero_closed [simp]: + "h \ \ carrier H" +by (rule group_hom.one_closed[OF a_group_hom, + simplified ring_record_simps]) + +lemma (in abelian_group_hom) hom_zero [simp]: + "h \ = \\<^bsub>H\<^esub>" +by (rule group_hom.hom_one[OF a_group_hom, + simplified ring_record_simps]) + +lemma (in abelian_group_hom) a_inv_closed [simp]: + "x \ carrier G ==> h (\x) \ carrier H" +by (rule group_hom.inv_closed[OF a_group_hom, + folded a_inv_def, simplified ring_record_simps]) + +lemma (in abelian_group_hom) hom_a_inv [simp]: + "x \ carrier G ==> h (\x) = \\<^bsub>H\<^esub> (h x)" +by (rule group_hom.hom_inv[OF a_group_hom, + folded a_inv_def, simplified ring_record_simps]) + +lemma (in abelian_group_hom) additive_subgroup_a_kernel: + "additive_subgroup (a_kernel G H h) G" +apply (rule additive_subgroup.intro) +apply (rule group_hom.subgroup_kernel[OF a_group_hom, + folded a_kernel_def, simplified ring_record_simps]) +done + +text{*The kernel of a homomorphism is an abelian subgroup*} +lemma (in abelian_group_hom) abelian_subgroup_a_kernel: + "abelian_subgroup (a_kernel G H h) G" +apply (rule abelian_subgroupI) +apply (rule group_hom.normal_kernel[OF a_group_hom, + folded a_kernel_def, simplified ring_record_simps]) +apply (simp add: G.a_comm) +done + +lemma (in abelian_group_hom) A_FactGroup_nonempty: + assumes X: "X \ carrier (G A_Mod a_kernel G H h)" + shows "X \ {}" +by (rule group_hom.FactGroup_nonempty[OF a_group_hom, + folded a_kernel_def A_FactGroup_def, simplified ring_record_simps]) + +lemma (in abelian_group_hom) FactGroup_contents_mem: + assumes X: "X \ carrier (G A_Mod (a_kernel G H h))" + shows "contents (h`X) \ carrier H" +by (rule group_hom.FactGroup_contents_mem[OF a_group_hom, + folded a_kernel_def A_FactGroup_def, simplified ring_record_simps]) + +lemma (in abelian_group_hom) A_FactGroup_hom: + "(\X. contents (h`X)) \ hom (G A_Mod (a_kernel G H h)) + \carrier = carrier H, mult = add H, one = zero H\" +by (rule group_hom.FactGroup_hom[OF a_group_hom, + folded a_kernel_def A_FactGroup_def, simplified ring_record_simps]) + +lemma (in abelian_group_hom) A_FactGroup_inj_on: + "inj_on (\X. contents (h ` X)) (carrier (G A_Mod a_kernel G H h))" +by (rule group_hom.FactGroup_inj_on[OF a_group_hom, + folded a_kernel_def A_FactGroup_def, simplified ring_record_simps]) + +text{*If the homomorphism @{term h} is onto @{term H}, then so is the +homomorphism from the quotient group*} +lemma (in abelian_group_hom) A_FactGroup_onto: + assumes h: "h ` carrier G = carrier H" + shows "(\X. contents (h ` X)) ` carrier (G A_Mod a_kernel G H h) = carrier H" +by (rule group_hom.FactGroup_onto[OF a_group_hom, + folded a_kernel_def A_FactGroup_def, simplified ring_record_simps]) + +text{*If @{term h} is a homomorphism from @{term G} onto @{term H}, then the + quotient group @{term "G Mod (kernel G H h)"} is isomorphic to @{term H}.*} +theorem (in abelian_group_hom) A_FactGroup_iso: + "h ` carrier G = carrier H + \ (\X. contents (h`X)) \ (G A_Mod (a_kernel G H h)) \ + (| carrier = carrier H, mult = add H, one = zero H |)" +by (rule group_hom.FactGroup_iso[OF a_group_hom, + folded a_kernel_def A_FactGroup_def, simplified ring_record_simps]) + +section {* Lemmas Lifted from CosetExt.thy *} + +text {* Not eveything from \texttt{CosetExt.thy} is lifted here. *} + +subsection {* General Lemmas from \texttt{AlgebraExt.thy} *} + +lemma (in additive_subgroup) a_Hcarr [simp]: + assumes hH: "h \ H" + shows "h \ carrier G" +by (rule subgroup.mem_carrier [OF a_subgroup, + simplified monoid_record_simps]) + + +subsection {* Lemmas for Right Cosets *} + +lemma (in abelian_subgroup) a_elemrcos_carrier: + assumes acarr: "a \ carrier G" + and a': "a' \ H +> a" + shows "a' \ carrier G" +by (rule subgroup.elemrcos_carrier [OF a_subgroup a_group, + folded a_r_coset_def, simplified monoid_record_simps]) + +lemma (in abelian_subgroup) a_rcos_const: + assumes hH: "h \ H" + shows "H +> h = H" +by (rule subgroup.rcos_const [OF a_subgroup a_group, + folded a_r_coset_def, simplified monoid_record_simps]) + +lemma (in abelian_subgroup) a_rcos_module_imp: + assumes xcarr: "x \ carrier G" + and x'cos: "x' \ H +> x" + shows "(x' \ \x) \ H" +by (rule subgroup.rcos_module_imp [OF a_subgroup a_group, + folded a_r_coset_def a_inv_def, simplified monoid_record_simps]) + +lemma (in abelian_subgroup) a_rcos_module_rev: + assumes carr: "x \ carrier G" "x' \ carrier G" + and xixH: "(x' \ \x) \ H" + shows "x' \ H +> x" +by (rule subgroup.rcos_module_rev [OF a_subgroup a_group, + folded a_r_coset_def a_inv_def, simplified monoid_record_simps]) + +lemma (in abelian_subgroup) a_rcos_module: + assumes carr: "x \ carrier G" "x' \ carrier G" + shows "(x' \ H +> x) = (x' \ \x \ H)" +by (rule subgroup.rcos_module [OF a_subgroup a_group, + folded a_r_coset_def a_inv_def, simplified monoid_record_simps]) + +--"variant" +lemma (in abelian_subgroup) a_rcos_module_minus: + includes ring G + assumes carr: "x \ carrier G" "x' \ carrier G" + shows "(x' \ H +> x) = (x' \ x \ H)" +proof - + from carr + have "(x' \ H +> x) = (x' \ \x \ H)" by (rule a_rcos_module) + from this and carr + show "(x' \ H +> x) = (x' \ x \ H)" + by (simp add: minus_eq) +qed + +lemma (in abelian_subgroup) a_repr_independence': + assumes "y \ H +> x" + and "x \ carrier G" + shows "H +> x = H +> y" +apply (rule a_repr_independence, assumption+) +apply (rule a_subgroup) +done + +lemma (in abelian_subgroup) a_repr_independenceD: + assumes ycarr: "y \ carrier G" + and repr: "H +> x = H +> y" + shows "y \ H +> x" +by (rule group.repr_independenceD [OF a_group a_subgroup, + folded a_r_coset_def, simplified monoid_record_simps]) + + +subsection {* Lemmas for the Set of Right Cosets *} + +lemma (in abelian_subgroup) a_rcosets_carrier: + "X \ a_rcosets H \ X \ carrier G" +by (rule subgroup.rcosets_carrier [OF a_subgroup a_group, + folded A_RCOSETS_def, simplified monoid_record_simps]) + + + +subsection {* Addition of Subgroups *} + +lemma (in abelian_monoid) set_add_closed: + assumes Acarr: "A \ carrier G" + and Bcarr: "B \ carrier G" + shows "A <+> B \ carrier G" +by (rule monoid.set_mult_closed [OF a_monoid, + folded set_add_def, simplified monoid_record_simps]) + +lemma (in abelian_group) add_additive_subgroups: + assumes subH: "additive_subgroup H G" + and subK: "additive_subgroup K G" + shows "additive_subgroup (H <+> K) G" +apply (rule additive_subgroup.intro) +apply (unfold set_add_def) +apply (intro comm_group.mult_subgroups) + apply (rule a_comm_group) + apply (rule additive_subgroup.a_subgroup[OF subH]) +apply (rule additive_subgroup.a_subgroup[OF subK]) +done + +end diff -r 6e070b33e72b -r 0e0ea63fe768 src/HOL/Algebra/Bij.thy --- a/src/HOL/Algebra/Bij.thy Thu Aug 03 14:53:57 2006 +0200 +++ b/src/HOL/Algebra/Bij.thy Thu Aug 03 14:57:26 2006 +0200 @@ -3,9 +3,10 @@ Author: Florian Kammueller, with new proofs by L C Paulson *) -header {* Bijections of a Set, Permutation Groups, Automorphism Groups *} +theory Bij imports Group begin -theory Bij imports Group begin + +section {* Bijections of a Set, Permutation Groups and Automorphism Groups *} constdefs Bij :: "'a set \ ('a \ 'a) set" diff -r 6e070b33e72b -r 0e0ea63fe768 src/HOL/Algebra/CRing.thy --- a/src/HOL/Algebra/CRing.thy Thu Aug 03 14:53:57 2006 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,645 +0,0 @@ -(* - Title: The algebraic hierarchy of rings - Id: $Id$ - Author: Clemens Ballarin, started 9 December 1996 - Copyright: Clemens Ballarin -*) - -header {* Abelian Groups *} - -theory CRing imports FiniteProduct -uses ("ringsimp.ML") begin - -record 'a ring = "'a monoid" + - zero :: 'a ("\\") - add :: "['a, 'a] => 'a" (infixl "\\" 65) - -text {* Derived operations. *} - -constdefs (structure R) - a_inv :: "[('a, 'm) ring_scheme, 'a ] => 'a" ("\\ _" [81] 80) - "a_inv R == m_inv (| carrier = carrier R, mult = add R, one = zero R |)" - - a_minus :: "[('a, 'm) ring_scheme, 'a, 'a] => 'a" (infixl "\\" 65) - "[| x \ carrier R; y \ carrier R |] ==> x \ y == x \ (\ y)" - -locale abelian_monoid = - fixes G (structure) - assumes a_comm_monoid: - "comm_monoid (| carrier = carrier G, mult = add G, one = zero G |)" - - -text {* - The following definition is redundant but simple to use. -*} - -locale abelian_group = abelian_monoid + - assumes a_comm_group: - "comm_group (| carrier = carrier G, mult = add G, one = zero G |)" - - -subsection {* Basic Properties *} - -lemma abelian_monoidI: - fixes R (structure) - assumes a_closed: - "!!x y. [| x \ carrier R; y \ carrier R |] ==> x \ y \ carrier R" - and zero_closed: "\ \ carrier R" - and a_assoc: - "!!x y z. [| x \ carrier R; y \ carrier R; z \ carrier R |] ==> - (x \ y) \ z = x \ (y \ z)" - and l_zero: "!!x. x \ carrier R ==> \ \ x = x" - and a_comm: - "!!x y. [| x \ carrier R; y \ carrier R |] ==> x \ y = y \ x" - shows "abelian_monoid R" - by (auto intro!: abelian_monoid.intro comm_monoidI intro: prems) - -lemma abelian_groupI: - fixes R (structure) - assumes a_closed: - "!!x y. [| x \ carrier R; y \ carrier R |] ==> x \ y \ carrier R" - and zero_closed: "zero R \ carrier R" - and a_assoc: - "!!x y z. [| x \ carrier R; y \ carrier R; z \ carrier R |] ==> - (x \ y) \ z = x \ (y \ z)" - and a_comm: - "!!x y. [| x \ carrier R; y \ carrier R |] ==> x \ y = y \ x" - and l_zero: "!!x. x \ carrier R ==> \ \ x = x" - and l_inv_ex: "!!x. x \ carrier R ==> EX y : carrier R. y \ x = \" - shows "abelian_group R" - by (auto intro!: abelian_group.intro abelian_monoidI - abelian_group_axioms.intro comm_monoidI comm_groupI - intro: prems) - -lemma (in abelian_monoid) a_monoid: - "monoid (| carrier = carrier G, mult = add G, one = zero G |)" -by (rule comm_monoid.axioms, rule a_comm_monoid) - -lemma (in abelian_group) a_group: - "group (| carrier = carrier G, mult = add G, one = zero G |)" - by (simp add: group_def a_monoid) - (simp add: comm_group.axioms group.axioms a_comm_group) - -lemmas monoid_record_simps = partial_object.simps monoid.simps - -lemma (in abelian_monoid) a_closed [intro, simp]: - "\ x \ carrier G; y \ carrier G \ \ x \ y \ carrier G" - by (rule monoid.m_closed [OF a_monoid, simplified monoid_record_simps]) - -lemma (in abelian_monoid) zero_closed [intro, simp]: - "\ \ carrier G" - by (rule monoid.one_closed [OF a_monoid, simplified monoid_record_simps]) - -lemma (in abelian_group) a_inv_closed [intro, simp]: - "x \ carrier G ==> \ x \ carrier G" - by (simp add: a_inv_def - group.inv_closed [OF a_group, simplified monoid_record_simps]) - -lemma (in abelian_group) minus_closed [intro, simp]: - "[| x \ carrier G; y \ carrier G |] ==> x \ y \ carrier G" - by (simp add: a_minus_def) - -lemma (in abelian_group) a_l_cancel [simp]: - "[| x \ carrier G; y \ carrier G; z \ carrier G |] ==> - (x \ y = x \ z) = (y = z)" - by (rule group.l_cancel [OF a_group, simplified monoid_record_simps]) - -lemma (in abelian_group) a_r_cancel [simp]: - "[| x \ carrier G; y \ carrier G; z \ carrier G |] ==> - (y \ x = z \ x) = (y = z)" - by (rule group.r_cancel [OF a_group, simplified monoid_record_simps]) - -lemma (in abelian_monoid) a_assoc: - "\x \ carrier G; y \ carrier G; z \ carrier G\ \ - (x \ y) \ z = x \ (y \ z)" - by (rule monoid.m_assoc [OF a_monoid, simplified monoid_record_simps]) - -lemma (in abelian_monoid) l_zero [simp]: - "x \ carrier G ==> \ \ x = x" - by (rule monoid.l_one [OF a_monoid, simplified monoid_record_simps]) - -lemma (in abelian_group) l_neg: - "x \ carrier G ==> \ x \ x = \" - by (simp add: a_inv_def - group.l_inv [OF a_group, simplified monoid_record_simps]) - -lemma (in abelian_monoid) a_comm: - "\x \ carrier G; y \ carrier G\ \ x \ y = y \ x" - by (rule comm_monoid.m_comm [OF a_comm_monoid, - simplified monoid_record_simps]) - -lemma (in abelian_monoid) a_lcomm: - "\x \ carrier G; y \ carrier G; z \ carrier G\ \ - x \ (y \ z) = y \ (x \ z)" - by (rule comm_monoid.m_lcomm [OF a_comm_monoid, - simplified monoid_record_simps]) - -lemma (in abelian_monoid) r_zero [simp]: - "x \ carrier G ==> x \ \ = x" - using monoid.r_one [OF a_monoid] - by simp - -lemma (in abelian_group) r_neg: - "x \ carrier G ==> x \ (\ x) = \" - using group.r_inv [OF a_group] - by (simp add: a_inv_def) - -lemma (in abelian_group) minus_zero [simp]: - "\ \ = \" - by (simp add: a_inv_def - group.inv_one [OF a_group, simplified monoid_record_simps]) - -lemma (in abelian_group) minus_minus [simp]: - "x \ carrier G ==> \ (\ x) = x" - using group.inv_inv [OF a_group, simplified monoid_record_simps] - by (simp add: a_inv_def) - -lemma (in abelian_group) a_inv_inj: - "inj_on (a_inv G) (carrier G)" - using group.inv_inj [OF a_group, simplified monoid_record_simps] - by (simp add: a_inv_def) - -lemma (in abelian_group) minus_add: - "[| x \ carrier G; y \ carrier G |] ==> \ (x \ y) = \ x \ \ y" - using comm_group.inv_mult [OF a_comm_group] - by (simp add: a_inv_def) - -lemma (in abelian_group) minus_equality: - "[| x \ carrier G; y \ carrier G; y \ x = \ |] ==> \ x = y" - using group.inv_equality [OF a_group] - by (auto simp add: a_inv_def) - -lemma (in abelian_monoid) minus_unique: - "[| x \ carrier G; y \ carrier G; y' \ carrier G; - y \ x = \; x \ y' = \ |] ==> y = y'" - using monoid.inv_unique [OF a_monoid] - by (simp add: a_inv_def) - -lemmas (in abelian_monoid) a_ac = a_assoc a_comm a_lcomm - -subsection {* Sums over Finite Sets *} - -text {* - This definition makes it easy to lift lemmas from @{term finprod}. -*} - -constdefs - finsum :: "[('b, 'm) ring_scheme, 'a => 'b, 'a set] => 'b" - "finsum G f A == finprod (| carrier = carrier G, - mult = add G, one = zero G |) f A" - -syntax - "_finsum" :: "index => idt => 'a set => 'b => 'b" - ("(3\__:_. _)" [1000, 0, 51, 10] 10) -syntax (xsymbols) - "_finsum" :: "index => idt => 'a set => 'b => 'b" - ("(3\__\_. _)" [1000, 0, 51, 10] 10) -syntax (HTML output) - "_finsum" :: "index => idt => 'a set => 'b => 'b" - ("(3\__\_. _)" [1000, 0, 51, 10] 10) -translations - "\\i:A. b" == "finsum \\ (%i. b) A" - -- {* Beware of argument permutation! *} - -(* - lemmas (in abelian_monoid) finsum_empty [simp] = - comm_monoid.finprod_empty [OF a_comm_monoid, simplified] - is dangeous, because attributes (like simplified) are applied upon opening - the locale, simplified refers to the simpset at that time!!! - - lemmas (in abelian_monoid) finsum_empty [simp] = - abelian_monoid.finprod_empty [OF a_abelian_monoid, folded finsum_def, - simplified monoid_record_simps] - makes the locale slow, because proofs are repeated for every - "lemma (in abelian_monoid)" command. - When lemma is used time in UnivPoly.thy from beginning to UP_cring goes down - from 110 secs to 60 secs. -*) - -lemma (in abelian_monoid) finsum_empty [simp]: - "finsum G f {} = \" - by (rule comm_monoid.finprod_empty [OF a_comm_monoid, - folded finsum_def, simplified monoid_record_simps]) - -lemma (in abelian_monoid) finsum_insert [simp]: - "[| finite F; a \ F; f \ F -> carrier G; f a \ carrier G |] - ==> finsum G f (insert a F) = f a \ finsum G f F" - by (rule comm_monoid.finprod_insert [OF a_comm_monoid, - folded finsum_def, simplified monoid_record_simps]) - -lemma (in abelian_monoid) finsum_zero [simp]: - "finite A ==> (\i\A. \) = \" - by (rule comm_monoid.finprod_one [OF a_comm_monoid, folded finsum_def, - simplified monoid_record_simps]) - -lemma (in abelian_monoid) finsum_closed [simp]: - fixes A - assumes fin: "finite A" and f: "f \ A -> carrier G" - shows "finsum G f A \ carrier G" - by (rule comm_monoid.finprod_closed [OF a_comm_monoid, - folded finsum_def, simplified monoid_record_simps]) - -lemma (in abelian_monoid) finsum_Un_Int: - "[| finite A; finite B; g \ A -> carrier G; g \ B -> carrier G |] ==> - finsum G g (A Un B) \ finsum G g (A Int B) = - finsum G g A \ finsum G g B" - by (rule comm_monoid.finprod_Un_Int [OF a_comm_monoid, - folded finsum_def, simplified monoid_record_simps]) - -lemma (in abelian_monoid) finsum_Un_disjoint: - "[| finite A; finite B; A Int B = {}; - g \ A -> carrier G; g \ B -> carrier G |] - ==> finsum G g (A Un B) = finsum G g A \ finsum G g B" - by (rule comm_monoid.finprod_Un_disjoint [OF a_comm_monoid, - folded finsum_def, simplified monoid_record_simps]) - -lemma (in abelian_monoid) finsum_addf: - "[| finite A; f \ A -> carrier G; g \ A -> carrier G |] ==> - finsum G (%x. f x \ g x) A = (finsum G f A \ finsum G g A)" - by (rule comm_monoid.finprod_multf [OF a_comm_monoid, - folded finsum_def, simplified monoid_record_simps]) - -lemma (in abelian_monoid) finsum_cong': - "[| A = B; g : B -> carrier G; - !!i. i : B ==> f i = g i |] ==> finsum G f A = finsum G g B" - by (rule comm_monoid.finprod_cong' [OF a_comm_monoid, - folded finsum_def, simplified monoid_record_simps]) auto - -lemma (in abelian_monoid) finsum_0 [simp]: - "f : {0::nat} -> carrier G ==> finsum G f {..0} = f 0" - by (rule comm_monoid.finprod_0 [OF a_comm_monoid, folded finsum_def, - simplified monoid_record_simps]) - -lemma (in abelian_monoid) finsum_Suc [simp]: - "f : {..Suc n} -> carrier G ==> - finsum G f {..Suc n} = (f (Suc n) \ finsum G f {..n})" - by (rule comm_monoid.finprod_Suc [OF a_comm_monoid, folded finsum_def, - simplified monoid_record_simps]) - -lemma (in abelian_monoid) finsum_Suc2: - "f : {..Suc n} -> carrier G ==> - finsum G f {..Suc n} = (finsum G (%i. f (Suc i)) {..n} \ f 0)" - by (rule comm_monoid.finprod_Suc2 [OF a_comm_monoid, folded finsum_def, - simplified monoid_record_simps]) - -lemma (in abelian_monoid) finsum_add [simp]: - "[| f : {..n} -> carrier G; g : {..n} -> carrier G |] ==> - finsum G (%i. f i \ g i) {..n::nat} = - finsum G f {..n} \ finsum G g {..n}" - by (rule comm_monoid.finprod_mult [OF a_comm_monoid, folded finsum_def, - simplified monoid_record_simps]) - -lemma (in abelian_monoid) finsum_cong: - "[| A = B; f : B -> carrier G; - !!i. i : B =simp=> f i = g i |] ==> finsum G f A = finsum G g B" - by (rule comm_monoid.finprod_cong [OF a_comm_monoid, folded finsum_def, - simplified monoid_record_simps]) (auto simp add: simp_implies_def) - -text {*Usually, if this rule causes a failed congruence proof error, - the reason is that the premise @{text "g \ B -> carrier G"} cannot be shown. - Adding @{thm [source] Pi_def} to the simpset is often useful. *} - -section {* The Algebraic Hierarchy of Rings *} - -subsection {* Basic Definitions *} - -locale ring = abelian_group R + monoid R + - assumes l_distr: "[| x \ carrier R; y \ carrier R; z \ carrier R |] - ==> (x \ y) \ z = x \ z \ y \ z" - and r_distr: "[| x \ carrier R; y \ carrier R; z \ carrier R |] - ==> z \ (x \ y) = z \ x \ z \ y" - -locale cring = ring + comm_monoid R - -locale "domain" = cring + - assumes one_not_zero [simp]: "\ ~= \" - and integral: "[| a \ b = \; a \ carrier R; b \ carrier R |] ==> - a = \ | b = \" - -locale field = "domain" + - assumes field_Units: "Units R = carrier R - {\}" - -subsection {* Basic Facts of Rings *} - -lemma ringI: - fixes R (structure) - assumes abelian_group: "abelian_group R" - and monoid: "monoid R" - and l_distr: "!!x y z. [| x \ carrier R; y \ carrier R; z \ carrier R |] - ==> (x \ y) \ z = x \ z \ y \ z" - and r_distr: "!!x y z. [| x \ carrier R; y \ carrier R; z \ carrier R |] - ==> z \ (x \ y) = z \ x \ z \ y" - shows "ring R" - by (auto intro: ring.intro - abelian_group.axioms ring_axioms.intro prems) - -lemma (in ring) is_abelian_group: - "abelian_group R" - by (auto intro!: abelian_groupI a_assoc a_comm l_neg) - -lemma (in ring) is_monoid: - "monoid R" - by (auto intro!: monoidI m_assoc) - -lemma cringI: - fixes R (structure) - assumes abelian_group: "abelian_group R" - and comm_monoid: "comm_monoid R" - and l_distr: "!!x y z. [| x \ carrier R; y \ carrier R; z \ carrier R |] - ==> (x \ y) \ z = x \ z \ y \ z" - shows "cring R" - proof (intro cring.intro ring.intro) - show "ring_axioms R" - -- {* Right-distributivity follows from left-distributivity and - commutativity. *} - proof (rule ring_axioms.intro) - fix x y z - assume R: "x \ carrier R" "y \ carrier R" "z \ carrier R" - note [simp]= comm_monoid.axioms [OF comm_monoid] - abelian_group.axioms [OF abelian_group] - abelian_monoid.a_closed - - from R have "z \ (x \ y) = (x \ y) \ z" - by (simp add: comm_monoid.m_comm [OF comm_monoid.intro]) - also from R have "... = x \ z \ y \ z" by (simp add: l_distr) - also from R have "... = z \ x \ z \ y" - by (simp add: comm_monoid.m_comm [OF comm_monoid.intro]) - finally show "z \ (x \ y) = z \ x \ z \ y" . - qed - qed (auto intro: cring.intro - abelian_group.axioms comm_monoid.axioms ring_axioms.intro prems) - -lemma (in cring) is_comm_monoid: - "comm_monoid R" - by (auto intro!: comm_monoidI m_assoc m_comm) - -subsection {* Normaliser for Rings *} - -lemma (in abelian_group) r_neg2: - "[| x \ carrier G; y \ carrier G |] ==> x \ (\ x \ y) = y" -proof - - assume G: "x \ carrier G" "y \ carrier G" - then have "(x \ \ x) \ y = y" - by (simp only: r_neg l_zero) - with G show ?thesis - by (simp add: a_ac) -qed - -lemma (in abelian_group) r_neg1: - "[| x \ carrier G; y \ carrier G |] ==> \ x \ (x \ y) = y" -proof - - assume G: "x \ carrier G" "y \ carrier G" - then have "(\ x \ x) \ y = y" - by (simp only: l_neg l_zero) - with G show ?thesis by (simp add: a_ac) -qed - -text {* - The following proofs are from Jacobson, Basic Algebra I, pp.~88--89 -*} - -lemma (in ring) l_null [simp]: - "x \ carrier R ==> \ \ x = \" -proof - - assume R: "x \ carrier R" - then have "\ \ x \ \ \ x = (\ \ \) \ x" - by (simp add: l_distr del: l_zero r_zero) - also from R have "... = \ \ x \ \" by simp - finally have "\ \ x \ \ \ x = \ \ x \ \" . - with R show ?thesis by (simp del: r_zero) -qed - -lemma (in ring) r_null [simp]: - "x \ carrier R ==> x \ \ = \" -proof - - assume R: "x \ carrier R" - then have "x \ \ \ x \ \ = x \ (\ \ \)" - by (simp add: r_distr del: l_zero r_zero) - also from R have "... = x \ \ \ \" by simp - finally have "x \ \ \ x \ \ = x \ \ \ \" . - with R show ?thesis by (simp del: r_zero) -qed - -lemma (in ring) l_minus: - "[| x \ carrier R; y \ carrier R |] ==> \ x \ y = \ (x \ y)" -proof - - assume R: "x \ carrier R" "y \ carrier R" - then have "(\ x) \ y \ x \ y = (\ x \ x) \ y" by (simp add: l_distr) - also from R have "... = \" by (simp add: l_neg l_null) - finally have "(\ x) \ y \ x \ y = \" . - with R have "(\ x) \ y \ x \ y \ \ (x \ y) = \ \ \ (x \ y)" by simp - with R show ?thesis by (simp add: a_assoc r_neg ) -qed - -lemma (in ring) r_minus: - "[| x \ carrier R; y \ carrier R |] ==> x \ \ y = \ (x \ y)" -proof - - assume R: "x \ carrier R" "y \ carrier R" - then have "x \ (\ y) \ x \ y = x \ (\ y \ y)" by (simp add: r_distr) - also from R have "... = \" by (simp add: l_neg r_null) - finally have "x \ (\ y) \ x \ y = \" . - with R have "x \ (\ y) \ x \ y \ \ (x \ y) = \ \ \ (x \ y)" by simp - with R show ?thesis by (simp add: a_assoc r_neg ) -qed - -lemma (in ring) minus_eq: - "[| x \ carrier R; y \ carrier R |] ==> x \ y = x \ \ y" - by (simp only: a_minus_def) - -text {* Setup algebra method: - compute distributive normal form in locale contexts *} - -use "ringsimp.ML" - -setup Algebra.setup - -lemmas (in ring) ring_simprules - [algebra ring "zero R" "add R" "a_inv R" "a_minus R" "one R" "mult R"] = - a_closed zero_closed a_inv_closed minus_closed m_closed one_closed - a_assoc l_zero l_neg a_comm m_assoc l_one l_distr minus_eq - r_zero r_neg r_neg2 r_neg1 minus_add minus_minus minus_zero - a_lcomm r_distr l_null r_null l_minus r_minus - -lemmas (in cring) - [algebra del: ring "zero R" "add R" "a_inv R" "a_minus R" "one R" "mult R"] = - _ - -lemmas (in cring) cring_simprules - [algebra add: cring "zero R" "add R" "a_inv R" "a_minus R" "one R" "mult R"] = - a_closed zero_closed a_inv_closed minus_closed m_closed one_closed - a_assoc l_zero l_neg a_comm m_assoc l_one l_distr m_comm minus_eq - r_zero r_neg r_neg2 r_neg1 minus_add minus_minus minus_zero - a_lcomm m_lcomm r_distr l_null r_null l_minus r_minus - - -lemma (in cring) nat_pow_zero: - "(n::nat) ~= 0 ==> \ (^) n = \" - by (induct n) simp_all - -text {* Two examples for use of method algebra *} - -lemma - includes ring R + cring S - shows "[| a \ carrier R; b \ carrier R; c \ carrier S; d \ carrier S |] ==> - a \ \ (a \ \ b) = b & c \\<^bsub>S\<^esub> d = d \\<^bsub>S\<^esub> c" - by algebra - -lemma - includes cring - shows "[| a \ carrier R; b \ carrier R |] ==> a \ (a \ b) = b" - by algebra - -subsection {* Sums over Finite Sets *} - -lemma (in cring) finsum_ldistr: - "[| finite A; a \ carrier R; f \ A -> carrier R |] ==> - finsum R f A \ a = finsum R (%i. f i \ a) A" -proof (induct set: Finites) - case empty then show ?case by simp -next - case (insert x F) then show ?case by (simp add: Pi_def l_distr) -qed - -lemma (in cring) finsum_rdistr: - "[| finite A; a \ carrier R; f \ A -> carrier R |] ==> - a \ finsum R f A = finsum R (%i. a \ f i) A" -proof (induct set: Finites) - case empty then show ?case by simp -next - case (insert x F) then show ?case by (simp add: Pi_def r_distr) -qed - -subsection {* Facts of Integral Domains *} - -lemma (in "domain") zero_not_one [simp]: - "\ ~= \" - by (rule not_sym) simp - -lemma (in "domain") integral_iff: (* not by default a simp rule! *) - "[| a \ carrier R; b \ carrier R |] ==> (a \ b = \) = (a = \ | b = \)" -proof - assume "a \ carrier R" "b \ carrier R" "a \ b = \" - then show "a = \ | b = \" by (simp add: integral) -next - assume "a \ carrier R" "b \ carrier R" "a = \ | b = \" - then show "a \ b = \" by auto -qed - -lemma (in "domain") m_lcancel: - assumes prem: "a ~= \" - and R: "a \ carrier R" "b \ carrier R" "c \ carrier R" - shows "(a \ b = a \ c) = (b = c)" -proof - assume eq: "a \ b = a \ c" - with R have "a \ (b \ c) = \" by algebra - with R have "a = \ | (b \ c) = \" by (simp add: integral_iff) - with prem and R have "b \ c = \" by auto - with R have "b = b \ (b \ c)" by algebra - also from R have "b \ (b \ c) = c" by algebra - finally show "b = c" . -next - assume "b = c" then show "a \ b = a \ c" by simp -qed - -lemma (in "domain") m_rcancel: - assumes prem: "a ~= \" - and R: "a \ carrier R" "b \ carrier R" "c \ carrier R" - shows conc: "(b \ a = c \ a) = (b = c)" -proof - - from prem and R have "(a \ b = a \ c) = (b = c)" by (rule m_lcancel) - with R show ?thesis by algebra -qed - -subsection {* Morphisms *} - -constdefs (structure R S) - ring_hom :: "[('a, 'm) ring_scheme, ('b, 'n) ring_scheme] => ('a => 'b) set" - "ring_hom R S == {h. h \ carrier R -> carrier S & - (ALL x y. x \ carrier R & y \ carrier R --> - h (x \ y) = h x \\<^bsub>S\<^esub> h y & h (x \ y) = h x \\<^bsub>S\<^esub> h y) & - h \ = \\<^bsub>S\<^esub>}" - -lemma ring_hom_memI: - fixes R (structure) and S (structure) - assumes hom_closed: "!!x. x \ carrier R ==> h x \ carrier S" - and hom_mult: "!!x y. [| x \ carrier R; y \ carrier R |] ==> - h (x \ y) = h x \\<^bsub>S\<^esub> h y" - and hom_add: "!!x y. [| x \ carrier R; y \ carrier R |] ==> - h (x \ y) = h x \\<^bsub>S\<^esub> h y" - and hom_one: "h \ = \\<^bsub>S\<^esub>" - shows "h \ ring_hom R S" - by (auto simp add: ring_hom_def prems Pi_def) - -lemma ring_hom_closed: - "[| h \ ring_hom R S; x \ carrier R |] ==> h x \ carrier S" - by (auto simp add: ring_hom_def funcset_mem) - -lemma ring_hom_mult: - fixes R (structure) and S (structure) - shows - "[| h \ ring_hom R S; x \ carrier R; y \ carrier R |] ==> - h (x \ y) = h x \\<^bsub>S\<^esub> h y" - by (simp add: ring_hom_def) - -lemma ring_hom_add: - fixes R (structure) and S (structure) - shows - "[| h \ ring_hom R S; x \ carrier R; y \ carrier R |] ==> - h (x \ y) = h x \\<^bsub>S\<^esub> h y" - by (simp add: ring_hom_def) - -lemma ring_hom_one: - fixes R (structure) and S (structure) - shows "h \ ring_hom R S ==> h \ = \\<^bsub>S\<^esub>" - by (simp add: ring_hom_def) - -locale ring_hom_cring = cring R + cring S + - fixes h - assumes homh [simp, intro]: "h \ ring_hom R S" - notes hom_closed [simp, intro] = ring_hom_closed [OF homh] - and hom_mult [simp] = ring_hom_mult [OF homh] - and hom_add [simp] = ring_hom_add [OF homh] - and hom_one [simp] = ring_hom_one [OF homh] - -lemma (in ring_hom_cring) hom_zero [simp]: - "h \ = \\<^bsub>S\<^esub>" -proof - - have "h \ \\<^bsub>S\<^esub> h \ = h \ \\<^bsub>S\<^esub> \\<^bsub>S\<^esub>" - by (simp add: hom_add [symmetric] del: hom_add) - then show ?thesis by (simp del: S.r_zero) -qed - -lemma (in ring_hom_cring) hom_a_inv [simp]: - "x \ carrier R ==> h (\ x) = \\<^bsub>S\<^esub> h x" -proof - - assume R: "x \ carrier R" - then have "h x \\<^bsub>S\<^esub> h (\ x) = h x \\<^bsub>S\<^esub> (\\<^bsub>S\<^esub> h x)" - by (simp add: hom_add [symmetric] R.r_neg S.r_neg del: hom_add) - with R show ?thesis by simp -qed - -lemma (in ring_hom_cring) hom_finsum [simp]: - "[| finite A; f \ A -> carrier R |] ==> - h (finsum R f A) = finsum S (h o f) A" -proof (induct set: Finites) - case empty then show ?case by simp -next - case insert then show ?case by (simp add: Pi_def) -qed - -lemma (in ring_hom_cring) hom_finprod: - "[| finite A; f \ A -> carrier R |] ==> - h (finprod R f A) = finprod S (h o f) A" -proof (induct set: Finites) - case empty then show ?case by simp -next - case insert then show ?case by (simp add: Pi_def) -qed - -declare ring_hom_cring.hom_finprod [simp] - -lemma id_ring_hom [simp]: - "id \ ring_hom R R" - by (auto intro!: ring_hom_memI) - -end diff -r 6e070b33e72b -r 0e0ea63fe768 src/HOL/Algebra/Coset.thy --- a/src/HOL/Algebra/Coset.thy Thu Aug 03 14:53:57 2006 +0200 +++ b/src/HOL/Algebra/Coset.thy Thu Aug 03 14:57:26 2006 +0200 @@ -1,11 +1,13 @@ (* Title: HOL/Algebra/Coset.thy ID: $Id$ - Author: Florian Kammueller, with new proofs by L C Paulson + Author: Florian Kammueller, with new proofs by L C Paulson, and + Stephan Hohe *) -header{*Cosets and Quotient Groups*} +theory Coset imports Group Exponent begin -theory Coset imports Group Exponent begin + +section {*Cosets and Quotient Groups*} constdefs (structure G) r_coset :: "[_, 'a set, 'a] \ 'a set" (infixl "#>\" 60) @@ -81,7 +83,7 @@ --{*Alternative proof is to put @{term "x=\"} in @{text repr_independence}.*} by (force simp add: subgroup.m_closed r_coset_def solve_equation) -lemma (in group) r_coset_subset_G: +lemma (in monoid) r_coset_subset_G: "[| H \ carrier G; x \ carrier G |] ==> H #> x \ carrier G" by (auto simp add: r_coset_def) @@ -105,6 +107,254 @@ subgroup.one_closed) done +text {* Opposite of @{thm [locale=group,source] "repr_independence"} *} +lemma (in group) repr_independenceD: + includes subgroup H G + assumes ycarr: "y \ carrier G" + and repr: "H #> x = H #> y" + shows "y \ H #> x" + by (subst repr, intro rcos_self) + +text {* Elements of a right coset are in the carrier *} +lemma (in subgroup) elemrcos_carrier: + includes group + assumes acarr: "a \ carrier G" + and a': "a' \ H #> a" + shows "a' \ carrier G" +proof - + from subset and acarr + have "H #> a \ carrier G" by (rule r_coset_subset_G) + from this and a' + show "a' \ carrier G" + by fast +qed + +lemma (in subgroup) rcos_const: + includes group + assumes hH: "h \ H" + shows "H #> h = H" + apply (unfold r_coset_def) + apply rule apply rule + apply clarsimp + apply (intro subgroup.m_closed) + apply assumption+ + apply rule + apply simp +proof - + fix h' + assume h'H: "h' \ H" + note carr = hH[THEN mem_carrier] h'H[THEN mem_carrier] + from carr + have a: "h' = (h' \ inv h) \ h" by (simp add: m_assoc) + from h'H hH + have "h' \ inv h \ H" by simp + from this and a + show "\x\H. h' = x \ h" by fast +qed + +text {* Step one for lemma @{text "rcos_module"} *} +lemma (in subgroup) rcos_module_imp: + includes group + assumes xcarr: "x \ carrier G" + and x'cos: "x' \ H #> x" + shows "(x' \ inv x) \ H" +proof - + from xcarr x'cos + have x'carr: "x' \ carrier G" + by (rule elemrcos_carrier[OF is_group]) + from xcarr + have ixcarr: "inv x \ carrier G" + by simp + from x'cos + have "\h\H. x' = h \ x" + unfolding r_coset_def + by fast + from this + obtain h + where hH: "h \ H" + and x': "x' = h \ x" + by auto + from hH and subset + have hcarr: "h \ carrier G" by fast + note carr = xcarr x'carr hcarr + from x' and carr + have "x' \ (inv x) = (h \ x) \ (inv x)" by fast + also from carr + have "\ = h \ (x \ inv x)" by (simp add: m_assoc) + also from carr + have "\ = h \ \" by simp + also from carr + have "\ = h" by simp + finally + have "x' \ (inv x) = h" by simp + from hH this + show "x' \ (inv x) \ H" by simp +qed + +text {* Step two for lemma @{text "rcos_module"} *} +lemma (in subgroup) rcos_module_rev: + includes group + assumes carr: "x \ carrier G" "x' \ carrier G" + and xixH: "(x' \ inv x) \ H" + shows "x' \ H #> x" +proof - + from xixH + have "\h\H. x' \ (inv x) = h" by fast + from this + obtain h + where hH: "h \ H" + and hsym: "x' \ (inv x) = h" + by fast + from hH subset have hcarr: "h \ carrier G" by simp + note carr = carr hcarr + from hsym[symmetric] have "h \ x = x' \ (inv x) \ x" by fast + also from carr + have "\ = x' \ ((inv x) \ x)" by (simp add: m_assoc) + also from carr + have "\ = x' \ \" by (simp add: l_inv) + also from carr + have "\ = x'" by simp + finally + have "h \ x = x'" by simp + from this[symmetric] and hH + show "x' \ H #> x" + unfolding r_coset_def + by fast +qed + +text {* Module property of right cosets *} +lemma (in subgroup) rcos_module: + includes group + assumes carr: "x \ carrier G" "x' \ carrier G" + shows "(x' \ H #> x) = (x' \ inv x \ H)" +proof + assume "x' \ H #> x" + from this and carr + show "x' \ inv x \ H" + by (intro rcos_module_imp[OF is_group]) +next + assume "x' \ inv x \ H" + from this and carr + show "x' \ H #> x" + by (intro rcos_module_rev[OF is_group]) +qed + +text {* Right cosets are subsets of the carrier. *} +lemma (in subgroup) rcosets_carrier: + includes group + assumes XH: "X \ rcosets H" + shows "X \ carrier G" +proof - + from XH have "\x\ carrier G. X = H #> x" + unfolding RCOSETS_def + by fast + from this + obtain x + where xcarr: "x\ carrier G" + and X: "X = H #> x" + by fast + from subset and xcarr + show "X \ carrier G" + unfolding X + by (rule r_coset_subset_G) +qed + +text {* Multiplication of general subsets *} +lemma (in monoid) set_mult_closed: + assumes Acarr: "A \ carrier G" + and Bcarr: "B \ carrier G" + shows "A <#> B \ carrier G" +apply rule apply (simp add: set_mult_def, clarsimp) +proof - + fix a b + assume "a \ A" + from this and Acarr + have acarr: "a \ carrier G" by fast + + assume "b \ B" + from this and Bcarr + have bcarr: "b \ carrier G" by fast + + from acarr bcarr + show "a \ b \ carrier G" by (rule m_closed) +qed + +lemma (in comm_group) mult_subgroups: + assumes subH: "subgroup H G" + and subK: "subgroup K G" + shows "subgroup (H <#> K) G" +apply (rule subgroup.intro) + apply (intro set_mult_closed subgroup.subset[OF subH] subgroup.subset[OF subK]) + apply (simp add: set_mult_def) apply clarsimp defer 1 + apply (simp add: set_mult_def) defer 1 + apply (simp add: set_mult_def, clarsimp) defer 1 +proof - + fix ha hb ka kb + assume haH: "ha \ H" and hbH: "hb \ H" and kaK: "ka \ K" and kbK: "kb \ K" + note carr = haH[THEN subgroup.mem_carrier[OF subH]] hbH[THEN subgroup.mem_carrier[OF subH]] + kaK[THEN subgroup.mem_carrier[OF subK]] kbK[THEN subgroup.mem_carrier[OF subK]] + from carr + have "(ha \ ka) \ (hb \ kb) = ha \ (ka \ hb) \ kb" by (simp add: m_assoc) + also from carr + have "\ = ha \ (hb \ ka) \ kb" by (simp add: m_comm) + also from carr + have "\ = (ha \ hb) \ (ka \ kb)" by (simp add: m_assoc) + finally + have eq: "(ha \ ka) \ (hb \ kb) = (ha \ hb) \ (ka \ kb)" . + + from haH hbH have hH: "ha \ hb \ H" by (simp add: subgroup.m_closed[OF subH]) + from kaK kbK have kK: "ka \ kb \ K" by (simp add: subgroup.m_closed[OF subK]) + + from hH and kK and eq + show "\h'\H. \k'\K. (ha \ ka) \ (hb \ kb) = h' \ k'" by fast +next + have "\ = \ \ \" by simp + from subgroup.one_closed[OF subH] subgroup.one_closed[OF subK] this + show "\h\H. \k\K. \ = h \ k" by fast +next + fix h k + assume hH: "h \ H" + and kK: "k \ K" + + from hH[THEN subgroup.mem_carrier[OF subH]] kK[THEN subgroup.mem_carrier[OF subK]] + have "inv (h \ k) = inv h \ inv k" by (simp add: inv_mult_group m_comm) + + from subgroup.m_inv_closed[OF subH hH] and subgroup.m_inv_closed[OF subK kK] and this + show "\ha\H. \ka\K. inv (h \ k) = ha \ ka" by fast +qed + +lemma (in subgroup) lcos_module_rev: + includes group + assumes carr: "x \ carrier G" "x' \ carrier G" + and xixH: "(inv x \ x') \ H" + shows "x' \ x <# H" +proof - + from xixH + have "\h\H. (inv x) \ x' = h" by fast + from this + obtain h + where hH: "h \ H" + and hsym: "(inv x) \ x' = h" + by fast + + from hH subset have hcarr: "h \ carrier G" by simp + note carr = carr hcarr + from hsym[symmetric] have "x \ h = x \ ((inv x) \ x')" by fast + also from carr + have "\ = (x \ (inv x)) \ x'" by (simp add: m_assoc[symmetric]) + also from carr + have "\ = \ \ x'" by simp + also from carr + have "\ = x'" by simp + finally + have "x \ h = x'" by simp + + from this[symmetric] and hH + show "x' \ x <# H" + unfolding l_coset_def + by fast +qed + subsection {* Normal subgroups *} @@ -250,7 +500,7 @@ done -subsubsection {* Set of inverses of an @{text r_coset}. *} +subsubsection {* Set of Inverses of an @{text r_coset}. *} lemma (in normal) rcos_inv: assumes x: "x \ carrier G" @@ -374,7 +624,7 @@ by (force simp add: r_congruent_def l_coset_def m_assoc [symmetric] a ) -subsubsection{*Two distinct right cosets are disjoint*} +subsubsection{*Two Distinct Right Cosets are Disjoint*} lemma (in group) rcos_equation: includes subgroup H G @@ -394,6 +644,79 @@ apply (blast intro: rcos_equation prems sym) done +subsection {* Further lemmas for @{text "r_congruent"} *} + +text {* The relation is a congruence *} + +lemma (in normal) congruent_rcong: + shows "congruent2 (rcong H) (rcong H) (\a b. a \ b <# H)" +proof (intro congruent2I[of "carrier G" _ "carrier G" _] equiv_rcong is_group) + fix a b c + assume abrcong: "(a, b) \ rcong H" + and ccarr: "c \ carrier G" + + from abrcong + have acarr: "a \ carrier G" + and bcarr: "b \ carrier G" + and abH: "inv a \ b \ H" + unfolding r_congruent_def + by fast+ + + note carr = acarr bcarr ccarr + + from ccarr and abH + have "inv c \ (inv a \ b) \ c \ H" by (rule inv_op_closed1) + moreover + from carr and inv_closed + have "inv c \ (inv a \ b) \ c = (inv c \ inv a) \ (b \ c)" + by (force cong: m_assoc) + moreover + from carr and inv_closed + have "\ = (inv (a \ c)) \ (b \ c)" + by (simp add: inv_mult_group) + ultimately + have "(inv (a \ c)) \ (b \ c) \ H" by simp + from carr and this + have "(b \ c) \ (a \ c) <# H" + by (simp add: lcos_module_rev[OF is_group]) + from carr and this and is_subgroup + show "(a \ c) <# H = (b \ c) <# H" by (intro l_repr_independence, simp+) +next + fix a b c + assume abrcong: "(a, b) \ rcong H" + and ccarr: "c \ carrier G" + + from ccarr have "c \ Units G" by (simp add: Units_eq) + hence cinvc_one: "inv c \ c = \" by (rule Units_l_inv) + + from abrcong + have acarr: "a \ carrier G" + and bcarr: "b \ carrier G" + and abH: "inv a \ b \ H" + by (unfold r_congruent_def, fast+) + + note carr = acarr bcarr ccarr + + from carr and inv_closed + have "inv a \ b = inv a \ (\ \ b)" by simp + also from carr and inv_closed + have "\ = inv a \ (inv c \ c) \ b" by simp + also from carr and inv_closed + have "\ = (inv a \ inv c) \ (c \ b)" by (force cong: m_assoc) + also from carr and inv_closed + have "\ = inv (c \ a) \ (c \ b)" by (simp add: inv_mult_group) + finally + have "inv a \ b = inv (c \ a) \ (c \ b)" . + from abH and this + have "inv (c \ a) \ (c \ b) \ H" by simp + + from carr and this + have "(c \ b) \ (c \ a) <# H" + by (simp add: lcos_module_rev[OF is_group]) + from carr and this and is_subgroup + show "(c \ a) <# H = (c \ b) <# H" by (intro l_repr_independence, simp+) +qed + subsection {*Order of a Group and Lagrange's Theorem*} diff -r 6e070b33e72b -r 0e0ea63fe768 src/HOL/Algebra/Exponent.thy --- a/src/HOL/Algebra/Exponent.thy Thu Aug 03 14:53:57 2006 +0200 +++ b/src/HOL/Algebra/Exponent.thy Thu Aug 03 14:57:26 2006 +0200 @@ -5,14 +5,15 @@ exponent p s yields the greatest power of p that divides s. *) -header{*The Combinatorial Argument Underlying the First Sylow Theorem*} - theory Exponent imports Main Primes begin + +section {*The Combinatorial Argument Underlying the First Sylow Theorem*} constdefs exponent :: "[nat, nat] => nat" "exponent p s == if prime p then (GREATEST r. p^r dvd s) else 0" + subsection{*Prime Theorems*} lemma prime_imp_one_less: "prime p ==> Suc 0 < p" @@ -196,7 +197,7 @@ done -subsection{*Lemmas for the Main Combinatorial Argument*} +subsection{*Main Combinatorial Argument*} lemma le_extend_mult: "[| 0 < c; a <= b |] ==> a <= b * (c::nat)" apply (rule_tac P = "%x. x <= b * c" in subst) diff -r 6e070b33e72b -r 0e0ea63fe768 src/HOL/Algebra/FiniteProduct.thy --- a/src/HOL/Algebra/FiniteProduct.thy Thu Aug 03 14:53:57 2006 +0200 +++ b/src/HOL/Algebra/FiniteProduct.thy Thu Aug 03 14:57:26 2006 +0200 @@ -5,9 +5,13 @@ This file is largely based on HOL/Finite_Set.thy. *) -header {* Product Operator for Commutative Monoids *} +theory FiniteProduct imports Group begin + -theory FiniteProduct imports Group begin +section {* Product Operator for Commutative Monoids *} + + +subsection {* Inductive Definition of a Relation for Products over Sets *} text {* Instantiation of locale @{text LC} of theory @{text Finite_Set} is not possible, because here we have explicit typing rules like @@ -58,7 +62,8 @@ then show ?case .. qed -subsection {* Left-commutative operations *} + +subsection {* Left-Commutative Operations *} locale LCD = fixes B :: "'b set" @@ -226,7 +231,8 @@ declare (in LCD) foldSetD_closed [rule del] -subsection {* Commutative monoids *} + +subsection {* Commutative Monoids *} text {* We enter a more restrictive context, with @{text "f :: 'a => 'a => 'a"} @@ -280,6 +286,7 @@ by (simp add: foldD_Un_Int left_commute LCD.foldD_closed [OF LCD.intro [of D]] Un_subset_iff) + subsection {* Products over Finite Sets *} constdefs (structure G) diff -r 6e070b33e72b -r 0e0ea63fe768 src/HOL/Algebra/Group.thy --- a/src/HOL/Algebra/Group.thy Thu Aug 03 14:53:57 2006 +0200 +++ b/src/HOL/Algebra/Group.thy Thu Aug 03 14:57:26 2006 +0200 @@ -6,19 +6,17 @@ Based on work by Florian Kammueller, L C Paulson and Markus Wenzel. *) -header {* Groups *} - theory Group imports FuncSet Lattice begin section {* Monoids and Groups *} +subsection {* Definitions *} + text {* Definitions follow \cite{Jacobson:1985}. *} -subsection {* Definitions *} - record 'a monoid = "'a partial_object" + mult :: "['a, 'a] \ 'a" (infixl "\\" 70) one :: 'a ("\\") @@ -291,6 +289,7 @@ "x \ carrier G ==> inv x \ x = \" using Units_l_inv by simp + subsection {* Cancellation Laws and Basic Properties *} lemma (in group) l_cancel [simp]: @@ -373,15 +372,19 @@ "\ (^) (z::int) = \" by (simp add: int_pow_def2) + subsection {* Subgroups *} locale subgroup = fixes H and G (structure) assumes subset: "H \ carrier G" and m_closed [intro, simp]: "\x \ H; y \ H\ \ x \ y \ H" - and one_closed [simp]: "\ \ H" + and one_closed [simp]: "\ \ H" and m_inv_closed [intro,simp]: "x \ H \ inv x \ H" +lemma (in subgroup) is_subgroup: + "subgroup H G" . + declare (in subgroup) group.intro [intro] lemma (in subgroup) mem_carrier [simp]: @@ -440,6 +443,7 @@ "subgroup (Units G) G" *) + subsection {* Direct Products *} constdefs @@ -524,9 +528,6 @@ apply (simp add: compose_def funcset_mem) done - -subsection {* Isomorphisms *} - constdefs iso :: "_ => _ => ('a => 'b) set" (infixr "\" 60) "G \ H == {h. h \ hom G H & bij_betw h (carrier G) (carrier H)}" @@ -590,6 +591,7 @@ with x show ?thesis by (simp del: H.r_inv) qed + subsection {* Commutative Structures *} text {* @@ -598,8 +600,6 @@ \emph{Abelian}. *} -subsection {* Definition *} - locale comm_monoid = monoid + assumes m_comm: "\x \ carrier G; y \ carrier G\ \ x \ y = y \ x" @@ -679,7 +679,8 @@ "[| x \ carrier G; y \ carrier G |] ==> inv (x \ y) = inv x \ inv y" by (simp add: m_ac inv_mult_group) -subsection {* Lattice of subgroups of a group *} + +subsection {* The Lattice of Subgroups of a Group *} text_raw {* \label{sec:subgroup-lattice} *} diff -r 6e070b33e72b -r 0e0ea63fe768 src/HOL/Algebra/Ideal.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Algebra/Ideal.thy Thu Aug 03 14:57:26 2006 +0200 @@ -0,0 +1,994 @@ +(* + Title: HOL/Algebra/CIdeal.thy + Id: $Id$ + Author: Stephan Hohe, TU Muenchen +*) + +theory Ideal +imports Ring AbelCoset +begin + +section {* Ideals *} + +subsection {* General definition *} + +locale ideal = additive_subgroup I R + ring R + + assumes I_l_closed: "\a \ I; x \ carrier R\ \ x \ a \ I" + and I_r_closed: "\a \ I; x \ carrier R\ \ a \ x \ I" + +interpretation ideal \ abelian_subgroup I R +apply (intro abelian_subgroupI3 abelian_group.intro) + apply (rule ideal.axioms, assumption) + apply (rule abelian_group.axioms, rule ring.axioms, rule ideal.axioms, assumption) +apply (rule abelian_group.axioms, rule ring.axioms, rule ideal.axioms, assumption) +done + +lemma (in ideal) is_ideal: + "ideal I R" +by - + +lemma idealI: + includes ring + assumes a_subgroup: "subgroup I \carrier = carrier R, mult = add R, one = zero R\" + and I_l_closed: "\a x. \a \ I; x \ carrier R\ \ x \ a \ I" + and I_r_closed: "\a x. \a \ I; x \ carrier R\ \ a \ x \ I" + shows "ideal I R" +by (intro ideal.intro ideal_axioms.intro additive_subgroupI, assumption+) + + +subsection {* Ideals Generated by a Subset of @{term [locale=ring] "carrier R"} *} + +constdefs (structure R) + genideal :: "('a, 'b) ring_scheme \ 'a set \ 'a set" ("Idl\ _" [80] 79) + "genideal R S \ Inter {I. ideal I R \ S \ I}" + + +subsection {* Principal Ideals *} + +locale principalideal = ideal + + assumes generate: "\i \ carrier R. I = Idl {i}" + +lemma (in principalideal) is_principalideal: + shows "principalideal I R" +by - + +lemma principalidealI: + includes ideal + assumes generate: "\i \ carrier R. I = Idl {i}" + shows "principalideal I R" +by (intro principalideal.intro principalideal_axioms.intro, assumption+) + + +subsection {* Maximal Ideals *} + +locale maximalideal = ideal + + assumes I_notcarr: "carrier R \ I" + and I_maximal: "\ideal J R; I \ J; J \ carrier R\ \ J = I \ J = carrier R" + +lemma (in maximalideal) is_maximalideal: + shows "maximalideal I R" +by - + +lemma maximalidealI: + includes ideal + assumes I_notcarr: "carrier R \ I" + and I_maximal: "\J. \ideal J R; I \ J; J \ carrier R\ \ J = I \ J = carrier R" + shows "maximalideal I R" +by (intro maximalideal.intro maximalideal_axioms.intro, assumption+) + + +subsection {* Prime Ideals *} + +locale primeideal = ideal + cring + + assumes I_notcarr: "carrier R \ I" + and I_prime: "\a \ carrier R; b \ carrier R; a \ b \ I\ \ a \ I \ b \ I" + +lemma (in primeideal) is_primeideal: + shows "primeideal I R" +by - + +lemma primeidealI: + includes ideal + includes cring + assumes I_notcarr: "carrier R \ I" + and I_prime: "\a b. \a \ carrier R; b \ carrier R; a \ b \ I\ \ a \ I \ b \ I" + shows "primeideal I R" +by (intro primeideal.intro primeideal_axioms.intro, assumption+) + +lemma primeidealI2: + includes additive_subgroup I R + includes cring + assumes I_l_closed: "\a x. \a \ I; x \ carrier R\ \ x \ a \ I" + and I_r_closed: "\a x. \a \ I; x \ carrier R\ \ a \ x \ I" + and I_notcarr: "carrier R \ I" + and I_prime: "\a b. \a \ carrier R; b \ carrier R; a \ b \ I\ \ a \ I \ b \ I" + shows "primeideal I R" +apply (intro_locales) + apply (intro ideal_axioms.intro, assumption+) +apply (intro primeideal_axioms.intro, assumption+) +done + + +section {* Properties of Ideals *} + +subsection {* Special Ideals *} + +lemma (in ring) zeroideal: + shows "ideal {\} R" +apply (intro idealI subgroup.intro) + apply (rule is_ring) + apply simp+ + apply (fold a_inv_def, simp) + apply simp+ +done + +lemma (in ring) oneideal: + shows "ideal (carrier R) R" +apply (intro idealI subgroup.intro) + apply (rule is_ring) + apply simp+ + apply (fold a_inv_def, simp) + apply simp+ +done + +lemma (in "domain") zeroprimeideal: + shows "primeideal {\} R" +apply (intro primeidealI) + apply (rule zeroideal) + apply (rule domain.axioms,assumption) + defer 1 + apply (simp add: integral) +proof (rule ccontr, simp) + assume "carrier R = {\}" + from this have "\ = \" by (rule one_zeroI) + from this and one_not_zero + show "False" by simp +qed + + +subsection {* General Ideal Properies *} + +lemma (in ideal) one_imp_carrier: + assumes I_one_closed: "\ \ I" + shows "I = carrier R" +apply (rule) +apply (rule) +apply (rule a_Hcarr, simp) +proof + fix x + assume xcarr: "x \ carrier R" + from I_one_closed and this + have "x \ \ \ I" by (intro I_l_closed) + from this and xcarr + show "x \ I" by simp +qed + +lemma (in ideal) Icarr: + assumes iI: "i \ I" + shows "i \ carrier R" +by (rule a_Hcarr) + + +subsection {* Intersection of Ideals *} + +text {* \paragraph{Intersection of two ideals} The intersection of any + two ideals is again an ideal in @{term R} *} +lemma (in ring) i_intersect: + includes ideal I R + includes ideal J R + shows "ideal (I \ J) R" +apply (intro idealI subgroup.intro) + apply (rule is_ring) + apply (force simp add: a_subset) + apply (simp add: a_inv_def[symmetric]) + apply simp + apply (simp add: a_inv_def[symmetric]) + apply (clarsimp, rule) + apply (fast intro: ideal.I_l_closed ideal.intro prems)+ +apply (clarsimp, rule) + apply (fast intro: ideal.I_r_closed ideal.intro prems)+ +done + + +subsubsection {* Intersection of a Set of Ideals *} + +text {* The intersection of any Number of Ideals is again + an Ideal in @{term R} *} +lemma (in ring) i_Intersect: + assumes Sideals: "\I. I \ S \ ideal I R" + and notempty: "S \ {}" + shows "ideal (Inter S) R" +apply (unfold_locales) +apply (simp_all add: Inter_def INTER_def) + apply (rule, simp) defer 1 + apply rule defer 1 + apply rule defer 1 + apply (fold a_inv_def, rule) defer 1 + apply rule defer 1 + apply rule defer 1 +proof - + fix x + assume "\I\S. x \ I" + hence xI: "\I. I \ S \ x \ I" by simp + + from notempty have "\I0. I0 \ S" by blast + from this obtain I0 where I0S: "I0 \ S" by auto + + interpret ideal ["I0" "R"] by (rule Sideals[OF I0S]) + + from xI[OF I0S] have "x \ I0" . + from this and a_subset show "x \ carrier R" by fast +next + fix x y + assume "\I\S. x \ I" + hence xI: "\I. I \ S \ x \ I" by simp + assume "\I\S. y \ I" + hence yI: "\I. I \ S \ y \ I" by simp + + fix J + assume JS: "J \ S" + interpret ideal ["J" "R"] by (rule Sideals[OF JS]) + from xI[OF JS] and yI[OF JS] + show "x \ y \ J" by (rule a_closed) +next + fix J + assume JS: "J \ S" + interpret ideal ["J" "R"] by (rule Sideals[OF JS]) + show "\ \ J" by simp +next + fix x + assume "\I\S. x \ I" + hence xI: "\I. I \ S \ x \ I" by simp + + fix J + assume JS: "J \ S" + interpret ideal ["J" "R"] by (rule Sideals[OF JS]) + + from xI[OF JS] + show "\ x \ J" by (rule a_inv_closed) +next + fix x y + assume "\I\S. x \ I" + hence xI: "\I. I \ S \ x \ I" by simp + assume ycarr: "y \ carrier R" + + fix J + assume JS: "J \ S" + interpret ideal ["J" "R"] by (rule Sideals[OF JS]) + + from xI[OF JS] and ycarr + show "y \ x \ J" by (rule I_l_closed) +next + fix x y + assume "\I\S. x \ I" + hence xI: "\I. I \ S \ x \ I" by simp + assume ycarr: "y \ carrier R" + + fix J + assume JS: "J \ S" + interpret ideal ["J" "R"] by (rule Sideals[OF JS]) + + from xI[OF JS] and ycarr + show "x \ y \ J" by (rule I_r_closed) +qed + + +subsection {* Addition of Ideals *} + +lemma (in ring) add_ideals: + assumes idealI: "ideal I R" + and idealJ: "ideal J R" + shows "ideal (I <+> J) R" +apply (rule ideal.intro) + apply (rule add_additive_subgroups) + apply (intro ideal.axioms[OF idealI]) + apply (intro ideal.axioms[OF idealJ]) + apply assumption +apply (rule ideal_axioms.intro) + apply (simp add: set_add_defs, clarsimp) defer 1 + apply (simp add: set_add_defs, clarsimp) defer 1 +proof - + fix x i j + assume xcarr: "x \ carrier R" + and iI: "i \ I" + and jJ: "j \ J" + from xcarr ideal.Icarr[OF idealI iI] ideal.Icarr[OF idealJ jJ] + have c: "(i \ j) \ x = (i \ x) \ (j \ x)" by algebra + from xcarr and iI + have a: "i \ x \ I" by (simp add: ideal.I_r_closed[OF idealI]) + from xcarr and jJ + have b: "j \ x \ J" by (simp add: ideal.I_r_closed[OF idealJ]) + from a b c + show "\ha\I. \ka\J. (i \ j) \ x = ha \ ka" by fast +next + fix x i j + assume xcarr: "x \ carrier R" + and iI: "i \ I" + and jJ: "j \ J" + from xcarr ideal.Icarr[OF idealI iI] ideal.Icarr[OF idealJ jJ] + have c: "x \ (i \ j) = (x \ i) \ (x \ j)" by algebra + from xcarr and iI + have a: "x \ i \ I" by (simp add: ideal.I_l_closed[OF idealI]) + from xcarr and jJ + have b: "x \ j \ J" by (simp add: ideal.I_l_closed[OF idealJ]) + from a b c + show "\ha\I. \ka\J. x \ (i \ j) = ha \ ka" by fast +qed + + +subsection {* Ideals generated by a subset of @{term [locale=ring] + "carrier R"} *} + +subsubsection {* Generation of Ideals in General Rings *} + +text {* @{term genideal} generates an ideal *} +lemma (in ring) genideal_ideal: + assumes Scarr: "S \ carrier R" + shows "ideal (Idl S) R" +unfolding genideal_def +proof (rule i_Intersect, fast, simp) + from oneideal and Scarr + show "\I. ideal I R \ S \ I" by fast +qed + +lemma (in ring) genideal_self: + assumes "S \ carrier R" + shows "S \ Idl S" +unfolding genideal_def +by fast + +lemma (in ring) genideal_self': + assumes carr: "i \ carrier R" + shows "i \ Idl {i}" +proof - + from carr + have "{i} \ Idl {i}" by (fast intro!: genideal_self) + thus "i \ Idl {i}" by fast +qed + +text {* @{term genideal} generates the minimal ideal *} +lemma (in ring) genideal_minimal: + assumes a: "ideal I R" + and b: "S \ I" + shows "Idl S \ I" +unfolding genideal_def +by (rule, elim InterD, simp add: a b) + +text {* Generated ideals and subsets *} +lemma (in ring) Idl_subset_ideal: + assumes Iideal: "ideal I R" + and Hcarr: "H \ carrier R" + shows "(Idl H \ I) = (H \ I)" +proof + assume a: "Idl H \ I" + have "H \ Idl H" by (rule genideal_self) + from this and a + show "H \ I" by simp +next + fix x + assume HI: "H \ I" + + from Iideal and HI + have "I \ {I. ideal I R \ H \ I}" by fast + from this + show "Idl H \ I" + unfolding genideal_def + by fast +qed + +lemma (in ring) subset_Idl_subset: + assumes Icarr: "I \ carrier R" + and HI: "H \ I" + shows "Idl H \ Idl I" +proof - + from HI and genideal_self[OF Icarr] + have HIdlI: "H \ Idl I" by fast + + from Icarr + have Iideal: "ideal (Idl I) R" by (rule genideal_ideal) + from HI and Icarr + have "H \ carrier R" by fast + from Iideal and this + have "(H \ Idl I) = (Idl H \ Idl I)" + by (rule Idl_subset_ideal[symmetric]) + + from HIdlI and this + show "Idl H \ Idl I" by simp +qed + +lemma (in ring) Idl_subset_ideal': + assumes acarr: "a \ carrier R" and bcarr: "b \ carrier R" + shows "(Idl {a} \ Idl {b}) = (a \ Idl {b})" +apply (subst Idl_subset_ideal[OF genideal_ideal[of "{b}"], of "{a}"]) + apply (fast intro: bcarr, fast intro: acarr) +apply fast +done + +lemma (in ring) genideal_zero: + "Idl {\} = {\}" +apply rule + apply (rule genideal_minimal[OF zeroideal], simp) +apply (simp add: genideal_self') +done + +lemma (in ring) genideal_one: + "Idl {\} = carrier R" +proof - + interpret ideal ["Idl {\}" "R"] by (rule genideal_ideal, fast intro: one_closed) + show "Idl {\} = carrier R" + apply (rule, rule a_subset) + apply (simp add: one_imp_carrier genideal_self') + done +qed + + +subsubsection {* Generation of Principal Ideals in Commutative Rings *} + +constdefs (structure R) + cgenideal :: "('a, 'b) monoid_scheme \ 'a \ 'a set" ("PIdl\ _" [80] 79) + "cgenideal R a \ { x \ a | x. x \ carrier R }" + +text {* genhideal (?) really generates an ideal *} +lemma (in cring) cgenideal_ideal: + assumes acarr: "a \ carrier R" + shows "ideal (PIdl a) R" +apply (unfold cgenideal_def) +apply (rule idealI[OF is_ring]) + apply (rule subgroup.intro) + apply (simp_all add: monoid_record_simps) + apply (blast intro: acarr m_closed) + apply clarsimp defer 1 + defer 1 + apply (fold a_inv_def, clarsimp) defer 1 + apply clarsimp defer 1 + apply clarsimp defer 1 +proof - + fix x y + assume xcarr: "x \ carrier R" + and ycarr: "y \ carrier R" + note carr = acarr xcarr ycarr + + from carr + have "x \ a \ y \ a = (x \ y) \ a" by (simp add: l_distr) + from this and carr + show "\z. x \ a \ y \ a = z \ a \ z \ carrier R" by fast +next + from l_null[OF acarr, symmetric] and zero_closed + show "\x. \ = x \ a \ x \ carrier R" by fast +next + fix x + assume xcarr: "x \ carrier R" + note carr = acarr xcarr + + from carr + have "\ (x \ a) = (\ x) \ a" by (simp add: l_minus) + from this and carr + show "\z. \ (x \ a) = z \ a \ z \ carrier R" by fast +next + fix x y + assume xcarr: "x \ carrier R" + and ycarr: "y \ carrier R" + note carr = acarr xcarr ycarr + + from carr + have "y \ a \ x = (y \ x) \ a" by (simp add: m_assoc, simp add: m_comm) + from this and carr + show "\z. y \ a \ x = z \ a \ z \ carrier R" by fast +next + fix x y + assume xcarr: "x \ carrier R" + and ycarr: "y \ carrier R" + note carr = acarr xcarr ycarr + + from carr + have "x \ (y \ a) = (x \ y) \ a" by (simp add: m_assoc) + from this and carr + show "\z. x \ (y \ a) = z \ a \ z \ carrier R" by fast +qed + +lemma (in ring) cgenideal_self: + assumes icarr: "i \ carrier R" + shows "i \ PIdl i" +unfolding cgenideal_def +proof simp + from icarr + have "i = \ \ i" by simp + from this and icarr + show "\x. i = x \ i \ x \ carrier R" by fast +qed + +text {* @{const "cgenideal"} is minimal *} + +lemma (in ring) cgenideal_minimal: + includes ideal J R + assumes aJ: "a \ J" + shows "PIdl a \ J" +unfolding cgenideal_def +by (rule, clarify, rule I_l_closed) + + +lemma (in cring) cgenideal_eq_genideal: + assumes icarr: "i \ carrier R" + shows "PIdl i = Idl {i}" +apply rule + apply (intro cgenideal_minimal) + apply (rule genideal_ideal, fast intro: icarr) + apply (rule genideal_self', fast intro: icarr) +apply (intro genideal_minimal) + apply (rule cgenideal_ideal, assumption) +apply (simp, rule cgenideal_self, assumption) +done + +lemma (in cring) cgenideal_eq_rcos: + "PIdl i = carrier R #> i" +unfolding cgenideal_def r_coset_def +by fast + +lemma (in cring) cgenideal_is_principalideal: + assumes icarr: "i \ carrier R" + shows "principalideal (PIdl i) R" +apply (rule principalidealI) +apply (rule cgenideal_ideal, assumption) +proof - + from icarr + have "PIdl i = Idl {i}" by (rule cgenideal_eq_genideal) + from icarr and this + show "\i'\carrier R. PIdl i = Idl {i'}" by fast +qed + + +subsection {* Union of Ideals *} + +lemma (in ring) union_genideal: + assumes idealI: "ideal I R" + and idealJ: "ideal J R" + shows "Idl (I \ J) = I <+> J" +apply rule + apply (rule ring.genideal_minimal) + apply assumption + apply (rule add_ideals[OF idealI idealJ]) + apply (rule) + apply (simp add: set_add_defs) apply (elim disjE) defer 1 defer 1 + apply (rule) apply (simp add: set_add_defs genideal_def) apply clarsimp defer 1 +proof - + fix x + assume xI: "x \ I" + have ZJ: "\ \ J" + by (intro additive_subgroup.zero_closed, rule ideal.axioms[OF idealJ]) + from ideal.Icarr[OF idealI xI] + have "x = x \ \" by algebra + from xI and ZJ and this + show "\h\I. \k\J. x = h \ k" by fast +next + fix x + assume xJ: "x \ J" + have ZI: "\ \ I" + by (intro additive_subgroup.zero_closed, rule ideal.axioms[OF idealI]) + from ideal.Icarr[OF idealJ xJ] + have "x = \ \ x" by algebra + from ZI and xJ and this + show "\h\I. \k\J. x = h \ k" by fast +next + fix i j K + assume iI: "i \ I" + and jJ: "j \ J" + and idealK: "ideal K R" + and IK: "I \ K" + and JK: "J \ K" + from iI and IK + have iK: "i \ K" by fast + from jJ and JK + have jK: "j \ K" by fast + from iK and jK + show "i \ j \ K" by (intro additive_subgroup.a_closed) (rule ideal.axioms[OF idealK]) +qed + + +subsection {* Properties of Principal Ideals *} + +text {* @{text "\"} generates the zero ideal *} +lemma (in ring) zero_genideal: + shows "Idl {\} = {\}" +apply rule +apply (simp add: genideal_minimal zeroideal) +apply (fast intro!: genideal_self) +done + +text {* @{text "\"} generates the unit ideal *} +lemma (in ring) one_genideal: + shows "Idl {\} = carrier R" +proof - + have "\ \ Idl {\}" by (simp add: genideal_self') + thus "Idl {\} = carrier R" by (intro ideal.one_imp_carrier, fast intro: genideal_ideal) +qed + + +text {* The zero ideal is a principal ideal *} +corollary (in ring) zeropideal: + shows "principalideal {\} R" +apply (rule principalidealI) + apply (rule zeroideal) +apply (blast intro!: zero_closed zero_genideal[symmetric]) +done + +text {* The unit ideal is a principal ideal *} +corollary (in ring) onepideal: + shows "principalideal (carrier R) R" +apply (rule principalidealI) + apply (rule oneideal) +apply (blast intro!: one_closed one_genideal[symmetric]) +done + + +text {* Every principal ideal is a right coset of the carrier *} +lemma (in principalideal) rcos_generate: + includes cring + shows "\x\I. I = carrier R #> x" +proof - + from generate + obtain i + where icarr: "i \ carrier R" + and I1: "I = Idl {i}" + by fast+ + + from icarr and genideal_self[of "{i}"] + have "i \ Idl {i}" by fast + hence iI: "i \ I" by (simp add: I1) + + from I1 icarr + have I2: "I = PIdl i" by (simp add: cgenideal_eq_genideal) + + have "PIdl i = carrier R #> i" + unfolding cgenideal_def r_coset_def + by fast + + from I2 and this + have "I = carrier R #> i" by simp + + from iI and this + show "\x\I. I = carrier R #> x" by fast +qed + + +subsection {* Prime Ideals *} + +lemma (in ideal) primeidealCD: + includes cring + assumes notprime: "\ primeideal I R" + shows "carrier R = I \ (\a b. a \ carrier R \ b \ carrier R \ a \ b \ I \ a \ I \ b \ I)" +proof (rule ccontr, clarsimp) + assume InR: "carrier R \ I" + and "\a. a \ carrier R \ (\b. a \ b \ I \ b \ carrier R \ a \ I \ b \ I)" + hence I_prime: "\ a b. \a \ carrier R; b \ carrier R; a \ b \ I\ \ a \ I \ b \ I" by simp + have "primeideal I R" + apply (rule primeideal.intro, assumption+) + by (rule primeideal_axioms.intro, rule InR, erule I_prime) + from this and notprime + show "False" by simp +qed + +lemma (in ideal) primeidealCE: + includes cring + assumes notprime: "\ primeideal I R" + and elim1: "carrier R = I \ P" + and elim2: "(\a b. a \ carrier R \ b \ carrier R \ a \ b \ I \ a \ I \ b \ I) \ P" + shows "P" +proof - + from notprime + have "carrier R = I \ (\a b. a \ carrier R \ b \ carrier R \ a \ b \ I \ a \ I \ b \ I)" + by (intro primeidealCD) + thus "P" + apply (rule disjE) + by (erule elim1, erule elim2) +qed + +text {* If @{text "{\}"} is a prime ideal of a commutative ring, the ring is a domain *} +lemma (in cring) zeroprimeideal_domainI: + assumes pi: "primeideal {\} R" + shows "domain R" +apply (rule domain.intro, assumption+) +apply (rule domain_axioms.intro) +proof (rule ccontr, simp) + interpret primeideal ["{\}" "R"] by (rule pi) + assume "\ = \" + hence "carrier R = {\}" by (rule one_zeroD) + from this[symmetric] and I_notcarr + show "False" by simp +next + interpret primeideal ["{\}" "R"] by (rule pi) + fix a b + assume ab: "a \ b = \" + and carr: "a \ carrier R" "b \ carrier R" + from ab + have abI: "a \ b \ {\}" by fast + from carr and this + have "a \ {\} \ b \ {\}" by (rule I_prime) + thus "a = \ \ b = \" by simp +qed + +corollary (in cring) domain_eq_zeroprimeideal: + shows "domain R = primeideal {\} R" +apply rule + apply (erule domain.zeroprimeideal) +apply (erule zeroprimeideal_domainI) +done + + +subsection {* Maximal Ideals *} + +lemma (in ideal) helper_I_closed: + assumes carr: "a \ carrier R" "x \ carrier R" "y \ carrier R" + and axI: "a \ x \ I" + shows "a \ (x \ y) \ I" +proof - + from axI and carr + have "(a \ x) \ y \ I" by (simp add: I_r_closed) + also from carr + have "(a \ x) \ y = a \ (x \ y)" by (simp add: m_assoc) + finally + show "a \ (x \ y) \ I" . +qed + +lemma (in ideal) helper_max_prime: + includes cring + assumes acarr: "a \ carrier R" + shows "ideal {x\carrier R. a \ x \ I} R" +apply (rule idealI) + apply (rule cring.axioms[OF is_cring]) + apply (rule subgroup.intro) + apply (simp, fast) + apply clarsimp apply (simp add: r_distr acarr) + apply (simp add: acarr) + apply (simp add: a_inv_def[symmetric], clarify) defer 1 + apply clarsimp defer 1 + apply (fast intro!: helper_I_closed acarr) +proof - + fix x + assume xcarr: "x \ carrier R" + and ax: "a \ x \ I" + from ax and acarr xcarr + have "\(a \ x) \ I" by simp + also from acarr xcarr + have "\(a \ x) = a \ (\x)" by algebra + finally + show "a \ (\x) \ I" . + from acarr + have "a \ \ = \" by simp +next + fix x y + assume xcarr: "x \ carrier R" + and ycarr: "y \ carrier R" + and ayI: "a \ y \ I" + from ayI and acarr xcarr ycarr + have "a \ (y \ x) \ I" by (simp add: helper_I_closed) + moreover from xcarr ycarr + have "y \ x = x \ y" by (simp add: m_comm) + ultimately + show "a \ (x \ y) \ I" by simp +qed + +text {* In a cring every maximal ideal is prime *} +lemma (in cring) maximalideal_is_prime: + includes maximalideal + shows "primeideal I R" +apply (rule ccontr) +apply (rule primeidealCE) + apply assumption+ + apply (simp add: I_notcarr) +proof - + assume "\a b. a \ carrier R \ b \ carrier R \ a \ b \ I \ a \ I \ b \ I" + from this + obtain a b + where acarr: "a \ carrier R" + and bcarr: "b \ carrier R" + and abI: "a \ b \ I" + and anI: "a \ I" + and bnI: "b \ I" + by fast + def J \ "{x\carrier R. a \ x \ I}" + + from acarr + have idealJ: "ideal J R" by (unfold J_def, intro helper_max_prime) + + have IsubJ: "I \ J" + proof + fix x + assume xI: "x \ I" + from this and acarr + have "a \ x \ I" by (intro I_l_closed) + from xI[THEN a_Hcarr] this + show "x \ J" by (unfold J_def, fast) + qed + + from abI and acarr bcarr + have "b \ J" by (unfold J_def, fast) + from bnI and this + have JnI: "J \ I" by fast + from acarr + have "a = a \ \" by algebra + from this and anI + have "a \ \ \ I" by simp + from one_closed and this + have "\ \ J" by (unfold J_def, fast) + hence Jncarr: "J \ carrier R" by fast + + interpret ideal ["J" "R"] by (rule idealJ) + + have "J = I \ J = carrier R" + apply (intro I_maximal) + apply (rule idealJ) + apply (rule IsubJ) + apply (rule a_subset) + done + + from this and JnI and Jncarr + show "False" by simp +qed + + +subsection {* Derived Theorems Involving Ideals *} + +--"A non-zero cring that has only the two trivial ideals is a field" +lemma (in cring) trivialideals_fieldI: + assumes carrnzero: "carrier R \ {\}" + and haveideals: "{I. ideal I R} = {{\}, carrier R}" + shows "field R" +apply (rule cring_fieldI) +apply (rule, rule, rule) + apply (erule Units_closed) +defer 1 + apply rule +defer 1 +proof (rule ccontr, simp) + assume zUnit: "\ \ Units R" + hence a: "\ \ inv \ = \" by (rule Units_r_inv) + from zUnit + have "\ \ inv \ = \" by (intro l_null, rule Units_inv_closed) + from a[symmetric] and this + have "\ = \" by simp + hence "carrier R = {\}" by (rule one_zeroD) + from this and carrnzero + show "False" by simp +next + fix x + assume xcarr': "x \ carrier R - {\}" + hence xcarr: "x \ carrier R" by fast + from xcarr' + have xnZ: "x \ \" by fast + from xcarr + have xIdl: "ideal (PIdl x) R" by (intro cgenideal_ideal, fast) + + from xcarr + have "x \ PIdl x" by (intro cgenideal_self, fast) + from this and xnZ + have "PIdl x \ {\}" by fast + from haveideals and this + have "PIdl x = carrier R" + by (blast intro!: xIdl) + hence "\ \ PIdl x" by simp + hence "\y. \ = y \ x \ y \ carrier R" unfolding cgenideal_def by blast + from this + obtain y + where ycarr: " y \ carrier R" + and ylinv: "\ = y \ x" + by fast+ + from ylinv and xcarr ycarr + have yrinv: "\ = x \ y" by (simp add: m_comm) + from ycarr and ylinv[symmetric] and yrinv[symmetric] + have "\y \ carrier R. y \ x = \ \ x \ y = \" by fast + from this and xcarr + show "x \ Units R" + unfolding Units_def + by fast +qed + +lemma (in field) all_ideals: + shows "{I. ideal I R} = {{\}, carrier R}" +apply (rule, rule) +proof - + fix I + assume a: "I \ {I. ideal I R}" + with this + interpret ideal ["I" "R"] by simp + + show "I \ {{\}, carrier R}" + proof (cases "\a. a \ I - {\}") + assume "\a. a \ I - {\}" + from this + obtain a + where aI: "a \ I" + and anZ: "a \ \" + by fast+ + from aI[THEN a_Hcarr] anZ + have aUnit: "a \ Units R" by (simp add: field_Units) + hence a: "a \ inv a = \" by (rule Units_r_inv) + from aI and aUnit + have "a \ inv a \ I" by (simp add: I_r_closed) + hence oneI: "\ \ I" by (simp add: a[symmetric]) + + have "carrier R \ I" + proof + fix x + assume xcarr: "x \ carrier R" + from oneI and this + have "\ \ x \ I" by (rule I_r_closed) + from this and xcarr + show "x \ I" by simp + qed + from this and a_subset + have "I = carrier R" by fast + thus "I \ {{\}, carrier R}" by fast + next + assume "\ (\a. a \ I - {\})" + hence IZ: "\a. a \ I \ a = \" by simp + + have a: "I \ {\}" + proof + fix x + assume "x \ I" + hence "x = \" by (rule IZ) + thus "x \ {\}" by fast + qed + + have "\ \ I" by simp + hence "{\} \ I" by fast + + from this and a + have "I = {\}" by fast + thus "I \ {{\}, carrier R}" by fast + qed +qed (simp add: zeroideal oneideal) + +--"Jacobson Theorem 2.2" +lemma (in cring) trivialideals_eq_field: + assumes carrnzero: "carrier R \ {\}" + shows "({I. ideal I R} = {{\}, carrier R}) = field R" +by (fast intro!: trivialideals_fieldI[OF carrnzero] field.all_ideals) + + +text {* Like zeroprimeideal for domains *} +lemma (in field) zeromaximalideal: + "maximalideal {\} R" +apply (rule maximalidealI) + apply (rule zeroideal) +proof- + from one_not_zero + have "\ \ {\}" by simp + from this and one_closed + show "carrier R \ {\}" by fast +next + fix J + assume Jideal: "ideal J R" + hence "J \ {I. ideal I R}" + by fast + + from this and all_ideals + show "J = {\} \ J = carrier R" by simp +qed + +lemma (in cring) zeromaximalideal_fieldI: + assumes zeromax: "maximalideal {\} R" + shows "field R" +apply (rule trivialideals_fieldI, rule maximalideal.I_notcarr[OF zeromax]) +apply rule apply clarsimp defer 1 + apply (simp add: zeroideal oneideal) +proof - + fix J + assume Jn0: "J \ {\}" + and idealJ: "ideal J R" + interpret ideal ["J" "R"] by (rule idealJ) + have "{\} \ J" by (rule ccontr, simp) + from zeromax and idealJ and this and a_subset + have "J = {\} \ J = carrier R" by (rule maximalideal.I_maximal) + from this and Jn0 + show "J = carrier R" by simp +qed + +lemma (in cring) zeromaximalideal_eq_field: + "maximalideal {\} R = field R" +apply rule + apply (erule zeromaximalideal_fieldI) +apply (erule field.zeromaximalideal) +done + +end diff -r 6e070b33e72b -r 0e0ea63fe768 src/HOL/Algebra/IntRing.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Algebra/IntRing.thy Thu Aug 03 14:57:26 2006 +0200 @@ -0,0 +1,360 @@ +(* + Title: HOL/Algebra/IntRing.thy + Id: $Id$ + Author: Stephan Hohe, TU Muenchen +*) + +theory IntRing +imports QuotRing IntDef +begin + + +section {* The Ring of Integers *} + +subsection {* Some properties of @{typ int} *} + +lemma dvds_imp_abseq: + "\l dvd k; k dvd l\ \ abs l = abs (k::int)" +apply (subst abs_split, rule conjI) + apply (clarsimp, subst abs_split, rule conjI) + apply (clarsimp) + apply (cases "k=0", simp) + apply (cases "l=0", simp) + apply (simp add: zdvd_anti_sym) + apply clarsimp + apply (cases "k=0", simp) + apply (simp add: zdvd_anti_sym) +apply (clarsimp, subst abs_split, rule conjI) + apply (clarsimp) + apply (cases "l=0", simp) + apply (simp add: zdvd_anti_sym) +apply (clarsimp) +apply (subgoal_tac "-l = -k", simp) +apply (intro zdvd_anti_sym, simp+) +done + +lemma abseq_imp_dvd: + assumes a_lk: "abs l = abs (k::int)" + shows "l dvd k" +proof - + from a_lk + have "nat (abs l) = nat (abs k)" by simp + hence "nat (abs l) dvd nat (abs k)" by simp + hence "int (nat (abs l)) dvd k" by (subst int_dvd_iff) + hence "abs l dvd k" by simp + thus "l dvd k" + apply (unfold dvd_def, cases "l<0") + defer 1 apply clarsimp + proof (clarsimp) + fix k + assume l0: "l < 0" + have "- (l * k) = l * (-k)" by simp + thus "\ka. - (l * k) = l * ka" by fast + qed +qed + +lemma dvds_eq_abseq: + "(l dvd k \ k dvd l) = (abs l = abs (k::int))" +apply rule + apply (simp add: dvds_imp_abseq) +apply (rule conjI) + apply (simp add: abseq_imp_dvd)+ +done + + + +subsection {* The Set of Integers as Algebraic Structure *} + +subsubsection {* Definition of @{text "\"} *} + +constdefs + int_ring :: "int ring" ("\") + "int_ring \ \carrier = UNIV, mult = op *, one = 1, zero = 0, add = op +\" + + int_order :: "int order" + "int_order \ \carrier = UNIV, le = op \\" + +lemma int_Zcarr[simp,intro!]: + "k \ carrier \" +by (simp add: int_ring_def) + +lemma int_is_cring: + "cring \" +unfolding int_ring_def +apply (rule cringI) + apply (rule abelian_groupI, simp_all) + defer 1 + apply (rule comm_monoidI, simp_all) + apply (rule zadd_zmult_distrib) +apply (fast intro: zadd_zminus_inverse2) +done + +lemma int_is_domain: + "domain \" +apply (intro domain.intro domain_axioms.intro) + apply (rule int_is_cring) + apply (unfold int_ring_def, simp+) +done + +interpretation "domain" ["\"] by (rule int_is_domain) + +lemma int_le_total_order: + "total_order int_order" +unfolding int_order_def +apply (rule partial_order.total_orderI) + apply (rule partial_order.intro, simp+) +apply clarsimp +done + +interpretation total_order ["int_order"] by (rule int_le_total_order) + + +subsubsection {* Generated Ideals of @{text "\"} *} + +lemma int_Idl: + "Idl\<^bsub>\\<^esub> {a} = {x * a | x. True}" +apply (subst cgenideal_eq_genideal[symmetric], simp add: int_ring_def) +apply (simp add: cgenideal_def int_ring_def) +done + +lemma multiples_principalideal: + "principalideal {x * a | x. True } \" +apply (subst int_Idl[symmetric], rule principalidealI) + apply (rule genideal_ideal, simp) +apply fast +done + +lemma prime_primeideal: + assumes prime: "prime (nat p)" + shows "primeideal (Idl\<^bsub>\\<^esub> {p}) \" +apply (rule primeidealI) + apply (rule genideal_ideal, simp) + apply (rule int_is_cring) + apply (simp add: cgenideal_eq_genideal[symmetric] cgenideal_def) + apply (simp add: int_ring_def) + apply clarsimp defer 1 + apply (simp add: cgenideal_eq_genideal[symmetric] cgenideal_def) + apply (simp add: int_ring_def) + apply (elim exE) +proof - + fix a b x + + from prime + have ppos: "0 <= p" by (simp add: prime_def) + have unnat: "!!x. nat p dvd nat (abs x) ==> p dvd x" + proof - + fix x + assume "nat p dvd nat (abs x)" + hence "int (nat p) dvd x" by (simp add: int_dvd_iff[symmetric]) + thus "p dvd x" by (simp add: ppos) + qed + + + assume "a * b = x * p" + hence "p dvd a * b" by simp + hence "nat p dvd nat (abs (a * b))" + apply (subst nat_dvd_iff, clarsimp) + apply (rule conjI, clarsimp, simp add: zabs_def) + proof (clarsimp) + assume a: " ~ 0 <= p" + from prime + have "0 < p" by (simp add: prime_def) + from a and this + have "False" by simp + thus "nat (abs (a * b)) = 0" .. + qed + hence "nat p dvd (nat (abs a) * nat (abs b))" by (simp add: nat_abs_mult_distrib) + hence "nat p dvd nat (abs a) | nat p dvd nat (abs b)" by (rule prime_dvd_mult[OF prime]) + hence "p dvd a | p dvd b" by (fast intro: unnat) + thus "(EX x. a = x * p) | (EX x. b = x * p)" + proof + assume "p dvd a" + hence "EX x. a = p * x" by (simp add: dvd_def) + from this obtain x + where "a = p * x" by fast + hence "a = x * p" by simp + hence "EX x. a = x * p" by simp + thus "(EX x. a = x * p) | (EX x. b = x * p)" .. + next + assume "p dvd b" + hence "EX x. b = p * x" by (simp add: dvd_def) + from this obtain x + where "b = p * x" by fast + hence "b = x * p" by simp + hence "EX x. b = x * p" by simp + thus "(EX x. a = x * p) | (EX x. b = x * p)" .. + qed +next + assume "UNIV = {uu. EX x. uu = x * p}" + from this obtain x + where "1 = x * p" by fast + from this [symmetric] + have "p * x = 1" by (subst zmult_commute) + hence "\p * x\ = 1" by simp + hence "\p\ = 1" by (rule abs_zmult_eq_1) + from this and prime + show "False" by (simp add: prime_def) +qed + + +subsubsection {* Ideals and Divisibility *} + +lemma int_Idl_subset_ideal: + "Idl\<^bsub>\\<^esub> {k} \ Idl\<^bsub>\\<^esub> {l} = (k \ Idl\<^bsub>\\<^esub> {l})" +by (rule Idl_subset_ideal', simp+) + +lemma Idl_subset_eq_dvd: + "(Idl\<^bsub>\\<^esub> {k} \ Idl\<^bsub>\\<^esub> {l}) = (l dvd k)" +apply (subst int_Idl_subset_ideal, subst int_Idl, simp) +apply (rule, clarify) +apply (simp add: dvd_def, clarify) +apply (simp add: m_comm) +done + +lemma dvds_eq_Idl: + "(l dvd k \ k dvd l) = (Idl\<^bsub>\\<^esub> {k} = Idl\<^bsub>\\<^esub> {l})" +proof - + have a: "l dvd k = (Idl\<^bsub>\\<^esub> {k} \ Idl\<^bsub>\\<^esub> {l})" by (rule Idl_subset_eq_dvd[symmetric]) + have b: "k dvd l = (Idl\<^bsub>\\<^esub> {l} \ Idl\<^bsub>\\<^esub> {k})" by (rule Idl_subset_eq_dvd[symmetric]) + + have "(l dvd k \ k dvd l) = ((Idl\<^bsub>\\<^esub> {k} \ Idl\<^bsub>\\<^esub> {l}) \ (Idl\<^bsub>\\<^esub> {l} \ Idl\<^bsub>\\<^esub> {k}))" + by (subst a, subst b, simp) + also have "((Idl\<^bsub>\\<^esub> {k} \ Idl\<^bsub>\\<^esub> {l}) \ (Idl\<^bsub>\\<^esub> {l} \ Idl\<^bsub>\\<^esub> {k})) = (Idl\<^bsub>\\<^esub> {k} = Idl\<^bsub>\\<^esub> {l})" by (rule, fast+) + finally + show ?thesis . +qed + +lemma Idl_eq_abs: + "(Idl\<^bsub>\\<^esub> {k} = Idl\<^bsub>\\<^esub> {l}) = (abs l = abs k)" +apply (subst dvds_eq_abseq[symmetric]) +apply (rule dvds_eq_Idl[symmetric]) +done + + +subsubsection {* Ideals and the Modulus *} + +constdefs + ZMod :: "int => int => int set" + "ZMod k r == (Idl\<^bsub>\\<^esub> {k}) +>\<^bsub>\\<^esub> r" + +lemmas ZMod_defs = + ZMod_def genideal_def + +lemma rcos_zfact: + assumes kIl: "k \ ZMod l r" + shows "EX x. k = x * l + r" +proof - + from kIl[unfolded ZMod_def] + have "\xl\Idl\<^bsub>\\<^esub> {l}. k = xl + r" by (simp add: a_r_coset_defs int_ring_def) + from this obtain xl + where xl: "xl \ Idl\<^bsub>\\<^esub> {l}" + and k: "k = xl + r" + by auto + from xl obtain x + where "xl = x * l" + by (simp add: int_Idl, fast) + from k and this + have "k = x * l + r" by simp + thus "\x. k = x * l + r" .. +qed + +lemma ZMod_imp_zmod: + assumes zmods: "ZMod m a = ZMod m b" + shows "a mod m = b mod m" +proof - + interpret ideal ["Idl\<^bsub>\\<^esub> {m}" \] by (rule genideal_ideal, fast) + from zmods + have "b \ ZMod m a" + unfolding ZMod_def + by (simp add: a_repr_independenceD) + from this + have "EX x. b = x * m + a" by (rule rcos_zfact) + from this obtain x + where "b = x * m + a" + by fast + + hence "b mod m = (x * m + a) mod m" by simp + also + have "\ = ((x * m) mod m) + (a mod m)" by (simp add: zmod_zadd1_eq) + also + have "\ = a mod m" by simp + finally + have "b mod m = a mod m" . + thus "a mod m = b mod m" .. +qed + +lemma ZMod_mod: + shows "ZMod m a = ZMod m (a mod m)" +proof - + interpret ideal ["Idl\<^bsub>\\<^esub> {m}" \] by (rule genideal_ideal, fast) + show ?thesis + unfolding ZMod_def + apply (rule a_repr_independence'[symmetric]) + apply (simp add: int_Idl a_r_coset_defs) + apply (simp add: int_ring_def) + proof - + have "a = m * (a div m) + (a mod m)" by (simp add: zmod_zdiv_equality) + hence "a = (a div m) * m + (a mod m)" by simp + thus "\h. (\x. h = x * m) \ a = h + a mod m" by fast + qed simp +qed + +lemma zmod_imp_ZMod: + assumes modeq: "a mod m = b mod m" + shows "ZMod m a = ZMod m b" +proof - + have "ZMod m a = ZMod m (a mod m)" by (rule ZMod_mod) + also have "\ = ZMod m (b mod m)" by (simp add: modeq[symmetric]) + also have "\ = ZMod m b" by (rule ZMod_mod[symmetric]) + finally show ?thesis . +qed + +corollary ZMod_eq_mod: + shows "(ZMod m a = ZMod m b) = (a mod m = b mod m)" +by (rule, erule ZMod_imp_zmod, erule zmod_imp_ZMod) + + +subsubsection {* Factorization *} + +constdefs + ZFact :: "int \ int set ring" + "ZFact k == \ Quot (Idl\<^bsub>\\<^esub> {k})" + +lemmas ZFact_defs = ZFact_def FactRing_def + +lemma ZFact_is_cring: + shows "cring (ZFact k)" +apply (unfold ZFact_def) +apply (rule ideal.quotient_is_cring) + apply (intro ring.genideal_ideal) + apply (simp add: cring.axioms[OF int_is_cring] ring.intro) + apply simp +apply (rule int_is_cring) +done + +lemma ZFact_zero: + "carrier (ZFact 0) = (\a. {{a}})" +apply (insert genideal_zero) +apply (simp add: ZFact_defs A_RCOSETS_defs r_coset_def int_ring_def ring_record_simps) +done + +lemma ZFact_one: + "carrier (ZFact 1) = {UNIV}" +apply (simp only: ZFact_defs A_RCOSETS_defs r_coset_def int_ring_def ring_record_simps) +apply (subst genideal_one[unfolded int_ring_def, simplified ring_record_simps]) +apply (rule, rule, clarsimp) + apply (rule, rule, clarsimp) + apply (rule, clarsimp, arith) +apply (rule, clarsimp) +apply (rule exI[of _ "0"], clarsimp) +done + +lemma ZFact_prime_is_domain: + assumes pprime: "prime (nat p)" + shows "domain (ZFact p)" +apply (unfold ZFact_def) +apply (rule primeideal.quotient_is_domain) +apply (rule prime_primeideal[OF pprime]) +done + +end diff -r 6e070b33e72b -r 0e0ea63fe768 src/HOL/Algebra/Lattice.thy --- a/src/HOL/Algebra/Lattice.thy Thu Aug 03 14:53:57 2006 +0200 +++ b/src/HOL/Algebra/Lattice.thy Thu Aug 03 14:57:26 2006 +0200 @@ -5,15 +5,17 @@ Copyright: Clemens Ballarin *) -header {* Orders and Lattices *} +theory Lattice imports Main begin -theory Lattice imports Main begin + +section {* Orders and Lattices *} text {* Object with a carrier set. *} record 'a partial_object = carrier :: "'a set" + subsection {* Partial Orders *} record 'a order = "'a partial_object" + @@ -822,9 +824,10 @@ (* TODO: prove dual version *) + subsection {* Examples *} -subsubsection {* Powerset of a set is a complete lattice *} +subsubsection {* Powerset of a Set is a Complete Lattice *} theorem powerset_is_complete_lattice: "complete_lattice (| carrier = Pow A, le = op \ |)" diff -r 6e070b33e72b -r 0e0ea63fe768 src/HOL/Algebra/Module.thy --- a/src/HOL/Algebra/Module.thy Thu Aug 03 14:53:57 2006 +0200 +++ b/src/HOL/Algebra/Module.thy Thu Aug 03 14:57:26 2006 +0200 @@ -4,9 +4,12 @@ Copyright: Clemens Ballarin *) -header {* Modules over an Abelian Group *} +theory Module imports Ring begin + -theory Module imports CRing begin +section {* Modules over an Abelian Group *} + +subsection {* Definitions *} record ('a, 'b) module = "'b ring" + smult :: "['a, 'b] => 'b" (infixl "\\" 70) diff -r 6e070b33e72b -r 0e0ea63fe768 src/HOL/Algebra/QuotRing.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Algebra/QuotRing.thy Thu Aug 03 14:57:26 2006 +0200 @@ -0,0 +1,340 @@ +(* + Title: HOL/Algebra/QuotRing.thy + Id: $Id$ + Author: Stephan Hohe +*) + +theory QuotRing +imports RingHom +begin + + +section {* Quotient Rings *} + +subsection {* Multiplication on Cosets *} + +constdefs (structure R) + rcoset_mult :: "[('a, _) ring_scheme, 'a set, 'a set, 'a set] \ 'a set" ("[mod _:] _ \\ _" [81,81,81] 80) + "rcoset_mult R I A B \ \a\A. \b\B. I +> (a \ b)" + + +text {* @{const "rcoset_mult"} fulfils the properties required by + congruences *} +lemma (in ideal) rcoset_mult_add: + "\x \ carrier R; y \ carrier R\ \ [mod I:] (I +> x) \ (I +> y) = I +> (x \ y)" +apply rule +apply (rule, simp add: rcoset_mult_def, clarsimp) +defer 1 +apply (rule, simp add: rcoset_mult_def) +defer 1 +proof - + fix z x' y' + assume carr: "x \ carrier R" "y \ carrier R" + and x'rcos: "x' \ I +> x" + and y'rcos: "y' \ I +> y" + and zrcos: "z \ I +> x' \ y'" + + from x'rcos + have "\h\I. x' = h \ x" by (simp add: a_r_coset_def r_coset_def) + from this obtain hx + where hxI: "hx \ I" + and x': "x' = hx \ x" + by fast+ + + from y'rcos + have "\h\I. y' = h \ y" by (simp add: a_r_coset_def r_coset_def) + from this + obtain hy + where hyI: "hy \ I" + and y': "y' = hy \ y" + by fast+ + + from zrcos + have "\h\I. z = h \ (x' \ y')" by (simp add: a_r_coset_def r_coset_def) + from this + obtain hz + where hzI: "hz \ I" + and z: "z = hz \ (x' \ y')" + by fast+ + + note carr = carr hxI[THEN a_Hcarr] hyI[THEN a_Hcarr] hzI[THEN a_Hcarr] + + from z have "z = hz \ (x' \ y')" . + also from x' y' + have "\ = hz \ ((hx \ x) \ (hy \ y))" by simp + also from carr + have "\ = (hz \ (hx \ (hy \ y)) \ x \ hy) \ x \ y" by algebra + finally + have z2: "z = (hz \ (hx \ (hy \ y)) \ x \ hy) \ x \ y" . + + from hxI hyI hzI carr + have "hz \ (hx \ (hy \ y)) \ x \ hy \ I" by (simp add: I_l_closed I_r_closed) + + from this and z2 + have "\h\I. z = h \ x \ y" by fast + thus "z \ I +> x \ y" by (simp add: a_r_coset_def r_coset_def) +next + fix z + assume xcarr: "x \ carrier R" + and ycarr: "y \ carrier R" + and zrcos: "z \ I +> x \ y" + from xcarr + have xself: "x \ I +> x" by (intro a_rcos_self) + from ycarr + have yself: "y \ I +> y" by (intro a_rcos_self) + + from xself and yself and zrcos + show "\a\I +> x. \b\I +> y. z \ I +> a \ b" by fast +qed + + +subsection {* Quotient Ring Definition *} + +constdefs (structure R) + FactRing :: "[('a,'b) ring_scheme, 'a set] \ ('a set) ring" + (infixl "Quot" 65) + "FactRing R I \ + \carrier = a_rcosets I, mult = rcoset_mult R I, one = (I +> \), zero = I, add = set_add R\" + + +subsection {* Factorization over General Ideals *} + +text {* The quotient is a ring *} +lemma (in ideal) quotient_is_ring: + shows "ring (R Quot I)" +apply (rule ringI) + --{* abelian group *} + apply (rule comm_group_abelian_groupI) + apply (simp add: FactRing_def) + apply (rule a_factorgroup_is_comm_group[unfolded A_FactGroup_def']) + --{* mult monoid *} + apply (rule monoidI) + apply (simp_all add: FactRing_def A_RCOSETS_def RCOSETS_def + a_r_coset_def[symmetric]) + --{* mult closed *} + apply (clarify) + apply (simp add: rcoset_mult_add, fast) + --{* mult one\_closed *} + apply (force intro: one_closed) + --{* mult assoc *} + apply clarify + apply (simp add: rcoset_mult_add m_assoc) + --{* mult one *} + apply clarify + apply (simp add: rcoset_mult_add l_one) + apply clarify + apply (simp add: rcoset_mult_add r_one) + --{* distr *} + apply clarify + apply (simp add: rcoset_mult_add a_rcos_sum l_distr) +apply clarify +apply (simp add: rcoset_mult_add a_rcos_sum r_distr) +done + + +text {* This is a ring homomorphism *} + +lemma (in ideal) rcos_ring_hom: + "(op +> I) \ ring_hom R (R Quot I)" +apply (rule ring_hom_memI) + apply (simp add: FactRing_def a_rcosetsI[OF a_subset]) + apply (simp add: FactRing_def rcoset_mult_add) + apply (simp add: FactRing_def a_rcos_sum) +apply (simp add: FactRing_def) +done + +lemma (in ideal) rcos_ring_hom_ring: + "ring_hom_ring R (R Quot I) (op +> I)" +apply (rule ring_hom_ringI) + apply (rule is_ring, rule quotient_is_ring) + apply (simp add: FactRing_def a_rcosetsI[OF a_subset]) + apply (simp add: FactRing_def rcoset_mult_add) + apply (simp add: FactRing_def a_rcos_sum) +apply (simp add: FactRing_def) +done + +text {* The quotient of a cring is also commutative *} +lemma (in ideal) quotient_is_cring: + includes cring + shows "cring (R Quot I)" +apply (intro cring.intro comm_monoid.intro comm_monoid_axioms.intro) + apply (rule quotient_is_ring) + apply (rule ring.axioms[OF quotient_is_ring]) +apply (simp add: FactRing_def A_RCOSETS_defs a_r_coset_def[symmetric]) +apply clarify +apply (simp add: rcoset_mult_add m_comm) +done + +text {* Cosets as a ring homomorphism on crings *} +lemma (in ideal) rcos_ring_hom_cring: + includes cring + shows "ring_hom_cring R (R Quot I) (op +> I)" +apply (rule ring_hom_cringI) + apply (rule rcos_ring_hom_ring) + apply assumption +apply (rule quotient_is_cring, assumption) +done + + +subsection {* Factorization over Prime Ideals *} + +text {* The quotient ring generated by a prime ideal is a domain *} +lemma (in primeideal) quotient_is_domain: + shows "domain (R Quot I)" +apply (rule domain.intro) + apply (rule quotient_is_cring, rule is_cring) +apply (rule domain_axioms.intro) + apply (simp add: FactRing_def) defer 1 + apply (simp add: FactRing_def A_RCOSETS_defs a_r_coset_def[symmetric], clarify) + apply (simp add: rcoset_mult_add) defer 1 +proof (rule ccontr, clarsimp) + assume "I +> \ = I" + hence "\ \ I" by (simp only: a_coset_join1 one_closed a_subgroup) + hence "carrier R \ I" by (subst one_imp_carrier, simp, fast) + from this and a_subset + have "I = carrier R" by fast + from this and I_notcarr + show "False" by fast +next + fix x y + assume carr: "x \ carrier R" "y \ carrier R" + and a: "I +> x \ y = I" + and b: "I +> y \ I" + + have ynI: "y \ I" + proof (rule ccontr, simp) + assume "y \ I" + hence "I +> y = I" by (rule a_rcos_const) + from this and b + show "False" by simp + qed + + from carr + have "x \ y \ I +> x \ y" by (simp add: a_rcos_self) + from this + have xyI: "x \ y \ I" by (simp add: a) + + from xyI and carr + have xI: "x \ I \ y \ I" by (simp add: I_prime) + from this and ynI + have "x \ I" by fast + thus "I +> x = I" by (rule a_rcos_const) +qed + +text {* Generating right cosets of a prime ideal is a homomorphism + on commutative rings *} +lemma (in primeideal) rcos_ring_hom_cring: + shows "ring_hom_cring R (R Quot I) (op +> I)" +by (rule rcos_ring_hom_cring, rule is_cring) + + +subsection {* Factorization over Maximal Ideals *} + +text {* In a commutative ring, the quotient ring over a maximal ideal + is a field. + The proof follows ``W. Adkins, S. Weintraub: Algebra -- + An Approach via Module Theory'' *} +lemma (in maximalideal) quotient_is_field: + includes cring + shows "field (R Quot I)" +apply (intro cring.cring_fieldI2) + apply (rule quotient_is_cring, rule is_cring) + defer 1 + apply (simp add: FactRing_def A_RCOSETS_defs a_r_coset_def[symmetric], clarsimp) + apply (simp add: rcoset_mult_add) defer 1 +proof (rule ccontr, simp) + --{* Quotient is not empty *} + assume "\\<^bsub>R Quot I\<^esub> = \\<^bsub>R Quot I\<^esub>" + hence II1: "I = I +> \" by (simp add: FactRing_def) + from a_rcos_self[OF one_closed] + have "\ \ I" by (simp add: II1[symmetric]) + hence "I = carrier R" by (rule one_imp_carrier) + from this and I_notcarr + show "False" by simp +next + --{* Existence of Inverse *} + fix a + assume IanI: "I +> a \ I" + and acarr: "a \ carrier R" + + --{* Helper ideal @{text "J"} *} + def J \ "(carrier R #> a) <+> I :: 'a set" + have idealJ: "ideal J R" + apply (unfold J_def, rule add_ideals) + apply (simp only: cgenideal_eq_rcos[symmetric], rule cgenideal_ideal, rule acarr) + apply (rule is_ideal) + done + + --{* Showing @{term "J"} not smaller than @{term "I"} *} + have IinJ: "I \ J" + proof (rule, simp add: J_def r_coset_def set_add_defs) + fix x + assume xI: "x \ I" + have Zcarr: "\ \ carrier R" by fast + from xI[THEN a_Hcarr] acarr + have "x = \ \ a \ x" by algebra + + from Zcarr and xI and this + show "\xa\carrier R. \k\I. x = xa \ a \ k" by fast + qed + + --{* Showing @{term "J \ I"} *} + have anI: "a \ I" + proof (rule ccontr, simp) + assume "a \ I" + hence "I +> a = I" by (rule a_rcos_const) + from this and IanI + show "False" by simp + qed + + have aJ: "a \ J" + proof (simp add: J_def r_coset_def set_add_defs) + from acarr + have "a = \ \ a \ \" by algebra + from one_closed and additive_subgroup.zero_closed[OF is_additive_subgroup] and this + show "\x\carrier R. \k\I. a = x \ a \ k" by fast + qed + + from aJ and anI + have JnI: "J \ I" by fast + + --{* Deducing @{term "J = carrier R"} because @{term "I"} is maximal *} + from idealJ and IinJ + have "J = I \ J = carrier R" + proof (rule I_maximal, unfold J_def) + have "carrier R #> a \ carrier R" + by (rule r_coset_subset_G) fast + from this and a_subset + show "carrier R #> a <+> I \ carrier R" by (rule set_add_closed) + qed + + from this and JnI + have Jcarr: "J = carrier R" by simp + + --{* Calculating an inverse for @{term "a"} *} + from one_closed[folded Jcarr] + have "\r\carrier R. \i\I. \ = r \ a \ i" + by (simp add: J_def r_coset_def set_add_defs) + from this + obtain r i + where rcarr: "r \ carrier R" + and iI: "i \ I" + and one: "\ = r \ a \ i" + by fast + from one and rcarr and acarr and iI[THEN a_Hcarr] + have rai1: "a \ r = \i \ \" by algebra + + --{* Lifting to cosets *} + from iI + have "\i \ \ \ I +> \" + by (intro a_rcosI, simp, intro a_subset, simp) + from this and rai1 + have "a \ r \ I +> \" by simp + from this have "I +> \ = I +> a \ r" + by (rule a_repr_independence, simp) (rule a_subgroup) + + from rcarr and this[symmetric] + show "\r\carrier R. I +> a \ r = I +> \" by fast +qed + +end diff -r 6e070b33e72b -r 0e0ea63fe768 src/HOL/Algebra/ROOT.ML --- a/src/HOL/Algebra/ROOT.ML Thu Aug 03 14:53:57 2006 +0200 +++ b/src/HOL/Algebra/ROOT.ML Thu Aug 03 14:57:26 2006 +0200 @@ -20,6 +20,8 @@ (* Rings *) use_thy "UnivPoly"; (* Rings and polynomials *) +use_thy "IntRing"; (* Ideals and residue classes *) + (*** Old development, based on axiomatic type classes. Will be withdrawn in future. ***) diff -r 6e070b33e72b -r 0e0ea63fe768 src/HOL/Algebra/Ring.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Algebra/Ring.thy Thu Aug 03 14:57:26 2006 +0200 @@ -0,0 +1,769 @@ +(* + Title: The algebraic hierarchy of rings + Id: $Id$ + Author: Clemens Ballarin, started 9 December 1996 + Copyright: Clemens Ballarin +*) + +theory Ring imports FiniteProduct +uses ("ringsimp.ML") begin + + +section {* Abelian Groups *} + +record 'a ring = "'a monoid" + + zero :: 'a ("\\") + add :: "['a, 'a] => 'a" (infixl "\\" 65) + +text {* Derived operations. *} + +constdefs (structure R) + a_inv :: "[('a, 'm) ring_scheme, 'a ] => 'a" ("\\ _" [81] 80) + "a_inv R == m_inv (| carrier = carrier R, mult = add R, one = zero R |)" + + a_minus :: "[('a, 'm) ring_scheme, 'a, 'a] => 'a" (infixl "\\" 65) + "[| x \ carrier R; y \ carrier R |] ==> x \ y == x \ (\ y)" + +locale abelian_monoid = + fixes G (structure) + assumes a_comm_monoid: + "comm_monoid (| carrier = carrier G, mult = add G, one = zero G |)" + + +text {* + The following definition is redundant but simple to use. +*} + +locale abelian_group = abelian_monoid + + assumes a_comm_group: + "comm_group (| carrier = carrier G, mult = add G, one = zero G |)" + + +subsection {* Basic Properties *} + +lemma abelian_monoidI: + fixes R (structure) + assumes a_closed: + "!!x y. [| x \ carrier R; y \ carrier R |] ==> x \ y \ carrier R" + and zero_closed: "\ \ carrier R" + and a_assoc: + "!!x y z. [| x \ carrier R; y \ carrier R; z \ carrier R |] ==> + (x \ y) \ z = x \ (y \ z)" + and l_zero: "!!x. x \ carrier R ==> \ \ x = x" + and a_comm: + "!!x y. [| x \ carrier R; y \ carrier R |] ==> x \ y = y \ x" + shows "abelian_monoid R" + by (auto intro!: abelian_monoid.intro comm_monoidI intro: prems) + +lemma abelian_groupI: + fixes R (structure) + assumes a_closed: + "!!x y. [| x \ carrier R; y \ carrier R |] ==> x \ y \ carrier R" + and zero_closed: "zero R \ carrier R" + and a_assoc: + "!!x y z. [| x \ carrier R; y \ carrier R; z \ carrier R |] ==> + (x \ y) \ z = x \ (y \ z)" + and a_comm: + "!!x y. [| x \ carrier R; y \ carrier R |] ==> x \ y = y \ x" + and l_zero: "!!x. x \ carrier R ==> \ \ x = x" + and l_inv_ex: "!!x. x \ carrier R ==> EX y : carrier R. y \ x = \" + shows "abelian_group R" + by (auto intro!: abelian_group.intro abelian_monoidI + abelian_group_axioms.intro comm_monoidI comm_groupI + intro: prems) + +lemma (in abelian_monoid) a_monoid: + "monoid (| carrier = carrier G, mult = add G, one = zero G |)" +by (rule comm_monoid.axioms, rule a_comm_monoid) + +lemma (in abelian_group) a_group: + "group (| carrier = carrier G, mult = add G, one = zero G |)" + by (simp add: group_def a_monoid) + (simp add: comm_group.axioms group.axioms a_comm_group) + +lemmas monoid_record_simps = partial_object.simps monoid.simps + +lemma (in abelian_monoid) a_closed [intro, simp]: + "\ x \ carrier G; y \ carrier G \ \ x \ y \ carrier G" + by (rule monoid.m_closed [OF a_monoid, simplified monoid_record_simps]) + +lemma (in abelian_monoid) zero_closed [intro, simp]: + "\ \ carrier G" + by (rule monoid.one_closed [OF a_monoid, simplified monoid_record_simps]) + +lemma (in abelian_group) a_inv_closed [intro, simp]: + "x \ carrier G ==> \ x \ carrier G" + by (simp add: a_inv_def + group.inv_closed [OF a_group, simplified monoid_record_simps]) + +lemma (in abelian_group) minus_closed [intro, simp]: + "[| x \ carrier G; y \ carrier G |] ==> x \ y \ carrier G" + by (simp add: a_minus_def) + +lemma (in abelian_group) a_l_cancel [simp]: + "[| x \ carrier G; y \ carrier G; z \ carrier G |] ==> + (x \ y = x \ z) = (y = z)" + by (rule group.l_cancel [OF a_group, simplified monoid_record_simps]) + +lemma (in abelian_group) a_r_cancel [simp]: + "[| x \ carrier G; y \ carrier G; z \ carrier G |] ==> + (y \ x = z \ x) = (y = z)" + by (rule group.r_cancel [OF a_group, simplified monoid_record_simps]) + +lemma (in abelian_monoid) a_assoc: + "\x \ carrier G; y \ carrier G; z \ carrier G\ \ + (x \ y) \ z = x \ (y \ z)" + by (rule monoid.m_assoc [OF a_monoid, simplified monoid_record_simps]) + +lemma (in abelian_monoid) l_zero [simp]: + "x \ carrier G ==> \ \ x = x" + by (rule monoid.l_one [OF a_monoid, simplified monoid_record_simps]) + +lemma (in abelian_group) l_neg: + "x \ carrier G ==> \ x \ x = \" + by (simp add: a_inv_def + group.l_inv [OF a_group, simplified monoid_record_simps]) + +lemma (in abelian_monoid) a_comm: + "\x \ carrier G; y \ carrier G\ \ x \ y = y \ x" + by (rule comm_monoid.m_comm [OF a_comm_monoid, + simplified monoid_record_simps]) + +lemma (in abelian_monoid) a_lcomm: + "\x \ carrier G; y \ carrier G; z \ carrier G\ \ + x \ (y \ z) = y \ (x \ z)" + by (rule comm_monoid.m_lcomm [OF a_comm_monoid, + simplified monoid_record_simps]) + +lemma (in abelian_monoid) r_zero [simp]: + "x \ carrier G ==> x \ \ = x" + using monoid.r_one [OF a_monoid] + by simp + +lemma (in abelian_group) r_neg: + "x \ carrier G ==> x \ (\ x) = \" + using group.r_inv [OF a_group] + by (simp add: a_inv_def) + +lemma (in abelian_group) minus_zero [simp]: + "\ \ = \" + by (simp add: a_inv_def + group.inv_one [OF a_group, simplified monoid_record_simps]) + +lemma (in abelian_group) minus_minus [simp]: + "x \ carrier G ==> \ (\ x) = x" + using group.inv_inv [OF a_group, simplified monoid_record_simps] + by (simp add: a_inv_def) + +lemma (in abelian_group) a_inv_inj: + "inj_on (a_inv G) (carrier G)" + using group.inv_inj [OF a_group, simplified monoid_record_simps] + by (simp add: a_inv_def) + +lemma (in abelian_group) minus_add: + "[| x \ carrier G; y \ carrier G |] ==> \ (x \ y) = \ x \ \ y" + using comm_group.inv_mult [OF a_comm_group] + by (simp add: a_inv_def) + +lemma (in abelian_group) minus_equality: + "[| x \ carrier G; y \ carrier G; y \ x = \ |] ==> \ x = y" + using group.inv_equality [OF a_group] + by (auto simp add: a_inv_def) + +lemma (in abelian_monoid) minus_unique: + "[| x \ carrier G; y \ carrier G; y' \ carrier G; + y \ x = \; x \ y' = \ |] ==> y = y'" + using monoid.inv_unique [OF a_monoid] + by (simp add: a_inv_def) + +lemmas (in abelian_monoid) a_ac = a_assoc a_comm a_lcomm + +text {* Derive an @{text "abelian_group"} from a @{text "comm_group"} *} +lemma comm_group_abelian_groupI: + fixes G (structure) + assumes cg: "comm_group \carrier = carrier G, mult = add G, one = zero G\" + shows "abelian_group G" +proof - + interpret comm_group ["\carrier = carrier G, mult = add G, one = zero G\"] + by (rule cg) + show "abelian_group G" by (unfold_locales) +qed + + +subsection {* Sums over Finite Sets *} + +text {* + This definition makes it easy to lift lemmas from @{term finprod}. +*} + +constdefs + finsum :: "[('b, 'm) ring_scheme, 'a => 'b, 'a set] => 'b" + "finsum G f A == finprod (| carrier = carrier G, + mult = add G, one = zero G |) f A" + +syntax + "_finsum" :: "index => idt => 'a set => 'b => 'b" + ("(3\__:_. _)" [1000, 0, 51, 10] 10) +syntax (xsymbols) + "_finsum" :: "index => idt => 'a set => 'b => 'b" + ("(3\__\_. _)" [1000, 0, 51, 10] 10) +syntax (HTML output) + "_finsum" :: "index => idt => 'a set => 'b => 'b" + ("(3\__\_. _)" [1000, 0, 51, 10] 10) +translations + "\\i:A. b" == "finsum \\ (%i. b) A" + -- {* Beware of argument permutation! *} + +(* + lemmas (in abelian_monoid) finsum_empty [simp] = + comm_monoid.finprod_empty [OF a_comm_monoid, simplified] + is dangeous, because attributes (like simplified) are applied upon opening + the locale, simplified refers to the simpset at that time!!! + + lemmas (in abelian_monoid) finsum_empty [simp] = + abelian_monoid.finprod_empty [OF a_abelian_monoid, folded finsum_def, + simplified monoid_record_simps] + makes the locale slow, because proofs are repeated for every + "lemma (in abelian_monoid)" command. + When lemma is used time in UnivPoly.thy from beginning to UP_cring goes down + from 110 secs to 60 secs. +*) + +lemma (in abelian_monoid) finsum_empty [simp]: + "finsum G f {} = \" + by (rule comm_monoid.finprod_empty [OF a_comm_monoid, + folded finsum_def, simplified monoid_record_simps]) + +lemma (in abelian_monoid) finsum_insert [simp]: + "[| finite F; a \ F; f \ F -> carrier G; f a \ carrier G |] + ==> finsum G f (insert a F) = f a \ finsum G f F" + by (rule comm_monoid.finprod_insert [OF a_comm_monoid, + folded finsum_def, simplified monoid_record_simps]) + +lemma (in abelian_monoid) finsum_zero [simp]: + "finite A ==> (\i\A. \) = \" + by (rule comm_monoid.finprod_one [OF a_comm_monoid, folded finsum_def, + simplified monoid_record_simps]) + +lemma (in abelian_monoid) finsum_closed [simp]: + fixes A + assumes fin: "finite A" and f: "f \ A -> carrier G" + shows "finsum G f A \ carrier G" + by (rule comm_monoid.finprod_closed [OF a_comm_monoid, + folded finsum_def, simplified monoid_record_simps]) + +lemma (in abelian_monoid) finsum_Un_Int: + "[| finite A; finite B; g \ A -> carrier G; g \ B -> carrier G |] ==> + finsum G g (A Un B) \ finsum G g (A Int B) = + finsum G g A \ finsum G g B" + by (rule comm_monoid.finprod_Un_Int [OF a_comm_monoid, + folded finsum_def, simplified monoid_record_simps]) + +lemma (in abelian_monoid) finsum_Un_disjoint: + "[| finite A; finite B; A Int B = {}; + g \ A -> carrier G; g \ B -> carrier G |] + ==> finsum G g (A Un B) = finsum G g A \ finsum G g B" + by (rule comm_monoid.finprod_Un_disjoint [OF a_comm_monoid, + folded finsum_def, simplified monoid_record_simps]) + +lemma (in abelian_monoid) finsum_addf: + "[| finite A; f \ A -> carrier G; g \ A -> carrier G |] ==> + finsum G (%x. f x \ g x) A = (finsum G f A \ finsum G g A)" + by (rule comm_monoid.finprod_multf [OF a_comm_monoid, + folded finsum_def, simplified monoid_record_simps]) + +lemma (in abelian_monoid) finsum_cong': + "[| A = B; g : B -> carrier G; + !!i. i : B ==> f i = g i |] ==> finsum G f A = finsum G g B" + by (rule comm_monoid.finprod_cong' [OF a_comm_monoid, + folded finsum_def, simplified monoid_record_simps]) auto + +lemma (in abelian_monoid) finsum_0 [simp]: + "f : {0::nat} -> carrier G ==> finsum G f {..0} = f 0" + by (rule comm_monoid.finprod_0 [OF a_comm_monoid, folded finsum_def, + simplified monoid_record_simps]) + +lemma (in abelian_monoid) finsum_Suc [simp]: + "f : {..Suc n} -> carrier G ==> + finsum G f {..Suc n} = (f (Suc n) \ finsum G f {..n})" + by (rule comm_monoid.finprod_Suc [OF a_comm_monoid, folded finsum_def, + simplified monoid_record_simps]) + +lemma (in abelian_monoid) finsum_Suc2: + "f : {..Suc n} -> carrier G ==> + finsum G f {..Suc n} = (finsum G (%i. f (Suc i)) {..n} \ f 0)" + by (rule comm_monoid.finprod_Suc2 [OF a_comm_monoid, folded finsum_def, + simplified monoid_record_simps]) + +lemma (in abelian_monoid) finsum_add [simp]: + "[| f : {..n} -> carrier G; g : {..n} -> carrier G |] ==> + finsum G (%i. f i \ g i) {..n::nat} = + finsum G f {..n} \ finsum G g {..n}" + by (rule comm_monoid.finprod_mult [OF a_comm_monoid, folded finsum_def, + simplified monoid_record_simps]) + +lemma (in abelian_monoid) finsum_cong: + "[| A = B; f : B -> carrier G; + !!i. i : B =simp=> f i = g i |] ==> finsum G f A = finsum G g B" + by (rule comm_monoid.finprod_cong [OF a_comm_monoid, folded finsum_def, + simplified monoid_record_simps]) (auto simp add: simp_implies_def) + +text {*Usually, if this rule causes a failed congruence proof error, + the reason is that the premise @{text "g \ B -> carrier G"} cannot be shown. + Adding @{thm [source] Pi_def} to the simpset is often useful. *} + + +section {* The Algebraic Hierarchy of Rings *} + + +subsection {* Basic Definitions *} + +locale ring = abelian_group R + monoid R + + assumes l_distr: "[| x \ carrier R; y \ carrier R; z \ carrier R |] + ==> (x \ y) \ z = x \ z \ y \ z" + and r_distr: "[| x \ carrier R; y \ carrier R; z \ carrier R |] + ==> z \ (x \ y) = z \ x \ z \ y" + +locale cring = ring + comm_monoid R + +locale "domain" = cring + + assumes one_not_zero [simp]: "\ ~= \" + and integral: "[| a \ b = \; a \ carrier R; b \ carrier R |] ==> + a = \ | b = \" + +locale field = "domain" + + assumes field_Units: "Units R = carrier R - {\}" + + +subsection {* Rings *} + +lemma ringI: + fixes R (structure) + assumes abelian_group: "abelian_group R" + and monoid: "monoid R" + and l_distr: "!!x y z. [| x \ carrier R; y \ carrier R; z \ carrier R |] + ==> (x \ y) \ z = x \ z \ y \ z" + and r_distr: "!!x y z. [| x \ carrier R; y \ carrier R; z \ carrier R |] + ==> z \ (x \ y) = z \ x \ z \ y" + shows "ring R" + by (auto intro: ring.intro + abelian_group.axioms ring_axioms.intro prems) + +lemma (in ring) is_abelian_group: + "abelian_group R" + by (auto intro!: abelian_groupI a_assoc a_comm l_neg) + +lemma (in ring) is_monoid: + "monoid R" + by (auto intro!: monoidI m_assoc) + +lemma (in ring) is_ring: + "ring R" + . + +lemmas ring_record_simps = monoid_record_simps ring.simps + +lemma cringI: + fixes R (structure) + assumes abelian_group: "abelian_group R" + and comm_monoid: "comm_monoid R" + and l_distr: "!!x y z. [| x \ carrier R; y \ carrier R; z \ carrier R |] + ==> (x \ y) \ z = x \ z \ y \ z" + shows "cring R" + proof (intro cring.intro ring.intro) + show "ring_axioms R" + -- {* Right-distributivity follows from left-distributivity and + commutativity. *} + proof (rule ring_axioms.intro) + fix x y z + assume R: "x \ carrier R" "y \ carrier R" "z \ carrier R" + note [simp]= comm_monoid.axioms [OF comm_monoid] + abelian_group.axioms [OF abelian_group] + abelian_monoid.a_closed + + from R have "z \ (x \ y) = (x \ y) \ z" + by (simp add: comm_monoid.m_comm [OF comm_monoid.intro]) + also from R have "... = x \ z \ y \ z" by (simp add: l_distr) + also from R have "... = z \ x \ z \ y" + by (simp add: comm_monoid.m_comm [OF comm_monoid.intro]) + finally show "z \ (x \ y) = z \ x \ z \ y" . + qed + qed (auto intro: cring.intro + abelian_group.axioms comm_monoid.axioms ring_axioms.intro prems) + +lemma (in cring) is_comm_monoid: + "comm_monoid R" + by (auto intro!: comm_monoidI m_assoc m_comm) + +lemma (in cring) is_cring: + "cring R" + . + +subsubsection {* Normaliser for Rings *} + +lemma (in abelian_group) r_neg2: + "[| x \ carrier G; y \ carrier G |] ==> x \ (\ x \ y) = y" +proof - + assume G: "x \ carrier G" "y \ carrier G" + then have "(x \ \ x) \ y = y" + by (simp only: r_neg l_zero) + with G show ?thesis + by (simp add: a_ac) +qed + +lemma (in abelian_group) r_neg1: + "[| x \ carrier G; y \ carrier G |] ==> \ x \ (x \ y) = y" +proof - + assume G: "x \ carrier G" "y \ carrier G" + then have "(\ x \ x) \ y = y" + by (simp only: l_neg l_zero) + with G show ?thesis by (simp add: a_ac) +qed + +text {* + The following proofs are from Jacobson, Basic Algebra I, pp.~88--89 +*} + +lemma (in ring) l_null [simp]: + "x \ carrier R ==> \ \ x = \" +proof - + assume R: "x \ carrier R" + then have "\ \ x \ \ \ x = (\ \ \) \ x" + by (simp add: l_distr del: l_zero r_zero) + also from R have "... = \ \ x \ \" by simp + finally have "\ \ x \ \ \ x = \ \ x \ \" . + with R show ?thesis by (simp del: r_zero) +qed + +lemma (in ring) r_null [simp]: + "x \ carrier R ==> x \ \ = \" +proof - + assume R: "x \ carrier R" + then have "x \ \ \ x \ \ = x \ (\ \ \)" + by (simp add: r_distr del: l_zero r_zero) + also from R have "... = x \ \ \ \" by simp + finally have "x \ \ \ x \ \ = x \ \ \ \" . + with R show ?thesis by (simp del: r_zero) +qed + +lemma (in ring) l_minus: + "[| x \ carrier R; y \ carrier R |] ==> \ x \ y = \ (x \ y)" +proof - + assume R: "x \ carrier R" "y \ carrier R" + then have "(\ x) \ y \ x \ y = (\ x \ x) \ y" by (simp add: l_distr) + also from R have "... = \" by (simp add: l_neg l_null) + finally have "(\ x) \ y \ x \ y = \" . + with R have "(\ x) \ y \ x \ y \ \ (x \ y) = \ \ \ (x \ y)" by simp + with R show ?thesis by (simp add: a_assoc r_neg ) +qed + +lemma (in ring) r_minus: + "[| x \ carrier R; y \ carrier R |] ==> x \ \ y = \ (x \ y)" +proof - + assume R: "x \ carrier R" "y \ carrier R" + then have "x \ (\ y) \ x \ y = x \ (\ y \ y)" by (simp add: r_distr) + also from R have "... = \" by (simp add: l_neg r_null) + finally have "x \ (\ y) \ x \ y = \" . + with R have "x \ (\ y) \ x \ y \ \ (x \ y) = \ \ \ (x \ y)" by simp + with R show ?thesis by (simp add: a_assoc r_neg ) +qed + +lemma (in ring) minus_eq: + "[| x \ carrier R; y \ carrier R |] ==> x \ y = x \ \ y" + by (simp only: a_minus_def) + +text {* Setup algebra method: + compute distributive normal form in locale contexts *} + +use "ringsimp.ML" + +setup Algebra.setup + +lemmas (in ring) ring_simprules + [algebra ring "zero R" "add R" "a_inv R" "a_minus R" "one R" "mult R"] = + a_closed zero_closed a_inv_closed minus_closed m_closed one_closed + a_assoc l_zero l_neg a_comm m_assoc l_one l_distr minus_eq + r_zero r_neg r_neg2 r_neg1 minus_add minus_minus minus_zero + a_lcomm r_distr l_null r_null l_minus r_minus + +lemmas (in cring) + [algebra del: ring "zero R" "add R" "a_inv R" "a_minus R" "one R" "mult R"] = + _ + +lemmas (in cring) cring_simprules + [algebra add: cring "zero R" "add R" "a_inv R" "a_minus R" "one R" "mult R"] = + a_closed zero_closed a_inv_closed minus_closed m_closed one_closed + a_assoc l_zero l_neg a_comm m_assoc l_one l_distr m_comm minus_eq + r_zero r_neg r_neg2 r_neg1 minus_add minus_minus minus_zero + a_lcomm m_lcomm r_distr l_null r_null l_minus r_minus + + +lemma (in cring) nat_pow_zero: + "(n::nat) ~= 0 ==> \ (^) n = \" + by (induct n) simp_all + +lemma (in ring) one_zeroD: + assumes onezero: "\ = \" + shows "carrier R = {\}" +proof (rule, rule) + fix x + assume xcarr: "x \ carrier R" + from xcarr + have "x = x \ \" by simp + from this and onezero + have "x = x \ \" by simp + from this and xcarr + have "x = \" by simp + thus "x \ {\}" by fast +qed fast + +lemma (in ring) one_zeroI: + assumes carrzero: "carrier R = {\}" + shows "\ = \" +proof - + from one_closed and carrzero + show "\ = \" by simp +qed + +lemma (in ring) one_zero: + shows "(carrier R = {\}) = (\ = \)" + by (rule, erule one_zeroI, erule one_zeroD) + +lemma (in ring) one_not_zero: + shows "(carrier R \ {\}) = (\ \ \)" + by (simp add: one_zero) + +text {* Two examples for use of method algebra *} + +lemma + includes ring R + cring S + shows "[| a \ carrier R; b \ carrier R; c \ carrier S; d \ carrier S |] ==> + a \ \ (a \ \ b) = b & c \\<^bsub>S\<^esub> d = d \\<^bsub>S\<^esub> c" + by algebra + +lemma + includes cring + shows "[| a \ carrier R; b \ carrier R |] ==> a \ (a \ b) = b" + by algebra + + +subsubsection {* Sums over Finite Sets *} + +lemma (in cring) finsum_ldistr: + "[| finite A; a \ carrier R; f \ A -> carrier R |] ==> + finsum R f A \ a = finsum R (%i. f i \ a) A" +proof (induct set: Finites) + case empty then show ?case by simp +next + case (insert x F) then show ?case by (simp add: Pi_def l_distr) +qed + +lemma (in cring) finsum_rdistr: + "[| finite A; a \ carrier R; f \ A -> carrier R |] ==> + a \ finsum R f A = finsum R (%i. a \ f i) A" +proof (induct set: Finites) + case empty then show ?case by simp +next + case (insert x F) then show ?case by (simp add: Pi_def r_distr) +qed + + +subsection {* Integral Domains *} + +lemma (in "domain") zero_not_one [simp]: + "\ ~= \" + by (rule not_sym) simp + +lemma (in "domain") integral_iff: (* not by default a simp rule! *) + "[| a \ carrier R; b \ carrier R |] ==> (a \ b = \) = (a = \ | b = \)" +proof + assume "a \ carrier R" "b \ carrier R" "a \ b = \" + then show "a = \ | b = \" by (simp add: integral) +next + assume "a \ carrier R" "b \ carrier R" "a = \ | b = \" + then show "a \ b = \" by auto +qed + +lemma (in "domain") m_lcancel: + assumes prem: "a ~= \" + and R: "a \ carrier R" "b \ carrier R" "c \ carrier R" + shows "(a \ b = a \ c) = (b = c)" +proof + assume eq: "a \ b = a \ c" + with R have "a \ (b \ c) = \" by algebra + with R have "a = \ | (b \ c) = \" by (simp add: integral_iff) + with prem and R have "b \ c = \" by auto + with R have "b = b \ (b \ c)" by algebra + also from R have "b \ (b \ c) = c" by algebra + finally show "b = c" . +next + assume "b = c" then show "a \ b = a \ c" by simp +qed + +lemma (in "domain") m_rcancel: + assumes prem: "a ~= \" + and R: "a \ carrier R" "b \ carrier R" "c \ carrier R" + shows conc: "(b \ a = c \ a) = (b = c)" +proof - + from prem and R have "(a \ b = a \ c) = (b = c)" by (rule m_lcancel) + with R show ?thesis by algebra +qed + + +subsection {* Fields *} + +text {* Field would not need to be derived from domain, the properties + for domain follow from the assumptions of field *} +lemma (in cring) cring_fieldI: + assumes field_Units: "Units R = carrier R - {\}" + shows "field R" +proof unfold_locales + from field_Units + have a: "\ \ Units R" by fast + have "\ \ Units R" by fast + from this and a + show "\ \ \" by force +next + fix a b + assume acarr: "a \ carrier R" + and bcarr: "b \ carrier R" + and ab: "a \ b = \" + show "a = \ \ b = \" + proof (cases "a = \", simp) + assume "a \ \" + from this and field_Units and acarr + have aUnit: "a \ Units R" by fast + from bcarr + have "b = \ \ b" by algebra + also from aUnit acarr + have "... = (inv a \ a) \ b" by (simp add: Units_l_inv) + also from acarr bcarr aUnit[THEN Units_inv_closed] + have "... = (inv a) \ (a \ b)" by algebra + also from ab and acarr bcarr aUnit + have "... = (inv a) \ \" by simp + also from aUnit[THEN Units_inv_closed] + have "... = \" by algebra + finally + have "b = \" . + thus "a = \ \ b = \" by simp + qed +qed + +text {* Another variant to show that something is a field *} +lemma (in cring) cring_fieldI2: + assumes notzero: "\ \ \" + and invex: "\a. \a \ carrier R; a \ \\ \ \b\carrier R. a \ b = \" + shows "field R" + apply (rule cring_fieldI, simp add: Units_def) + apply (rule, clarsimp) + apply (simp add: notzero) +proof (clarsimp) + fix x + assume xcarr: "x \ carrier R" + and "x \ \" + from this + have "\y\carrier R. x \ y = \" by (rule invex) + from this + obtain y + where ycarr: "y \ carrier R" + and xy: "x \ y = \" + by fast + from xy xcarr ycarr have "y \ x = \" by (simp add: m_comm) + from ycarr and this and xy + show "\y\carrier R. y \ x = \ \ x \ y = \" by fast +qed + + +subsection {* Morphisms *} + +constdefs (structure R S) + ring_hom :: "[('a, 'm) ring_scheme, ('b, 'n) ring_scheme] => ('a => 'b) set" + "ring_hom R S == {h. h \ carrier R -> carrier S & + (ALL x y. x \ carrier R & y \ carrier R --> + h (x \ y) = h x \\<^bsub>S\<^esub> h y & h (x \ y) = h x \\<^bsub>S\<^esub> h y) & + h \ = \\<^bsub>S\<^esub>}" + +lemma ring_hom_memI: + fixes R (structure) and S (structure) + assumes hom_closed: "!!x. x \ carrier R ==> h x \ carrier S" + and hom_mult: "!!x y. [| x \ carrier R; y \ carrier R |] ==> + h (x \ y) = h x \\<^bsub>S\<^esub> h y" + and hom_add: "!!x y. [| x \ carrier R; y \ carrier R |] ==> + h (x \ y) = h x \\<^bsub>S\<^esub> h y" + and hom_one: "h \ = \\<^bsub>S\<^esub>" + shows "h \ ring_hom R S" + by (auto simp add: ring_hom_def prems Pi_def) + +lemma ring_hom_closed: + "[| h \ ring_hom R S; x \ carrier R |] ==> h x \ carrier S" + by (auto simp add: ring_hom_def funcset_mem) + +lemma ring_hom_mult: + fixes R (structure) and S (structure) + shows + "[| h \ ring_hom R S; x \ carrier R; y \ carrier R |] ==> + h (x \ y) = h x \\<^bsub>S\<^esub> h y" + by (simp add: ring_hom_def) + +lemma ring_hom_add: + fixes R (structure) and S (structure) + shows + "[| h \ ring_hom R S; x \ carrier R; y \ carrier R |] ==> + h (x \ y) = h x \\<^bsub>S\<^esub> h y" + by (simp add: ring_hom_def) + +lemma ring_hom_one: + fixes R (structure) and S (structure) + shows "h \ ring_hom R S ==> h \ = \\<^bsub>S\<^esub>" + by (simp add: ring_hom_def) + +locale ring_hom_cring = cring R + cring S + + fixes h + assumes homh [simp, intro]: "h \ ring_hom R S" + notes hom_closed [simp, intro] = ring_hom_closed [OF homh] + and hom_mult [simp] = ring_hom_mult [OF homh] + and hom_add [simp] = ring_hom_add [OF homh] + and hom_one [simp] = ring_hom_one [OF homh] + +lemma (in ring_hom_cring) hom_zero [simp]: + "h \ = \\<^bsub>S\<^esub>" +proof - + have "h \ \\<^bsub>S\<^esub> h \ = h \ \\<^bsub>S\<^esub> \\<^bsub>S\<^esub>" + by (simp add: hom_add [symmetric] del: hom_add) + then show ?thesis by (simp del: S.r_zero) +qed + +lemma (in ring_hom_cring) hom_a_inv [simp]: + "x \ carrier R ==> h (\ x) = \\<^bsub>S\<^esub> h x" +proof - + assume R: "x \ carrier R" + then have "h x \\<^bsub>S\<^esub> h (\ x) = h x \\<^bsub>S\<^esub> (\\<^bsub>S\<^esub> h x)" + by (simp add: hom_add [symmetric] R.r_neg S.r_neg del: hom_add) + with R show ?thesis by simp +qed + +lemma (in ring_hom_cring) hom_finsum [simp]: + "[| finite A; f \ A -> carrier R |] ==> + h (finsum R f A) = finsum S (h o f) A" +proof (induct set: Finites) + case empty then show ?case by simp +next + case insert then show ?case by (simp add: Pi_def) +qed + +lemma (in ring_hom_cring) hom_finprod: + "[| finite A; f \ A -> carrier R |] ==> + h (finprod R f A) = finprod S (h o f) A" +proof (induct set: Finites) + case empty then show ?case by simp +next + case insert then show ?case by (simp add: Pi_def) +qed + +declare ring_hom_cring.hom_finprod [simp] + +lemma id_ring_hom [simp]: + "id \ ring_hom R R" + by (auto intro!: ring_hom_memI) + +end diff -r 6e070b33e72b -r 0e0ea63fe768 src/HOL/Algebra/RingHom.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Algebra/RingHom.thy Thu Aug 03 14:57:26 2006 +0200 @@ -0,0 +1,178 @@ +(* + Title: HOL/Algebra/RingHom.thy + Id: $Id$ + Author: Stephan Hohe, TU Muenchen +*) + +theory RingHom +imports Ideal +begin + + +section {* Homomorphisms of Non-Commutative Rings *} + +text {* Lifting existing lemmas in a ring\_hom\_ring locale *} +locale ring_hom_ring = ring R + ring S + var h + + assumes homh: "h \ ring_hom R S" + notes hom_mult [simp] = ring_hom_mult [OF homh] + and hom_one [simp] = ring_hom_one [OF homh] + +interpretation ring_hom_cring \ ring_hom_ring + by (unfold_locales, rule homh) + +interpretation ring_hom_ring \ abelian_group_hom R S +apply (rule abelian_group_homI) + apply (rule R.is_abelian_group) + apply (rule S.is_abelian_group) +apply (intro group_hom.intro group_hom_axioms.intro) + apply (rule R.a_group) + apply (rule S.a_group) +apply (insert homh, unfold hom_def ring_hom_def) +apply simp +done + +lemma (in ring_hom_ring) is_ring_hom_ring: + includes struct R + struct S + shows "ring_hom_ring R S h" +by - + +lemma ring_hom_ringI: + includes ring R + ring S + assumes (* morphism: "h \ carrier R \ carrier S" *) + hom_closed: "!!x. x \ carrier R ==> h x \ carrier S" + and compatible_mult: "!!x y. [| x : carrier R; y : carrier R |] ==> h (x \ y) = h x \\<^bsub>S\<^esub> h y" + and compatible_add: "!!x y. [| x : carrier R; y : carrier R |] ==> h (x \ y) = h x \\<^bsub>S\<^esub> h y" + and compatible_one: "h \ = \\<^bsub>S\<^esub>" + shows "ring_hom_ring R S h" +apply unfold_locales +apply (unfold ring_hom_def, safe) + apply (simp add: hom_closed Pi_def, assumption+) +done + +lemma ring_hom_ringI2: + includes ring R + ring S + assumes "h \ ring_hom R S" + shows "ring_hom_ring R S h" +by (intro ring_hom_ring.intro ring_hom_ring_axioms.intro) + +lemma ring_hom_ringI3: + includes abelian_group_hom R S + ring R + ring S + assumes compatible_mult: "!!x y. [| x : carrier R; y : carrier R |] ==> h (x \ y) = h x \\<^bsub>S\<^esub> h y" + and compatible_one: "h \ = \\<^bsub>S\<^esub>" + shows "ring_hom_ring R S h" +apply (intro ring_hom_ring.intro ring_hom_ring_axioms.intro, assumption+) +apply (insert group_hom.homh[OF a_group_hom]) +apply (unfold hom_def ring_hom_def, simp) +apply (safe, assumption+) +done + +lemma ring_hom_cringI: + includes ring_hom_ring R S h + cring R + cring S + shows "ring_hom_cring R S h" +by (intro ring_hom_cring.intro ring_hom_cring_axioms.intro, assumption+, rule homh) + + +subsection {* The kernel of a ring homomorphism *} + +--"the kernel of a ring homomorphism is an ideal" +lemma (in ring_hom_ring) kernel_is_ideal: + shows "ideal (a_kernel R S h) R" +apply (rule idealI) + apply (rule R.is_ring) + apply (rule additive_subgroup.a_subgroup[OF additive_subgroup_a_kernel]) + apply (unfold a_kernel_def', simp+) +done + +text {* Elements of the kernel are mapped to zero *} +lemma (in abelian_group_hom) kernel_zero [simp]: + "i \ a_kernel R S h \ h i = \\<^bsub>S\<^esub>" +by (simp add: a_kernel_defs) + + +subsection {* Cosets *} + +text {* Cosets of the kernel correspond to the elements of the image of the homomorphism *} +lemma (in ring_hom_ring) rcos_imp_homeq: + assumes acarr: "a \ carrier R" + and xrcos: "x \ a_kernel R S h +> a" + shows "h x = h a" +proof - + interpret ideal ["a_kernel R S h" "R"] by (rule kernel_is_ideal) + + from xrcos + have "\i \ a_kernel R S h. x = i \ a" by (simp add: a_r_coset_defs) + from this obtain i + where iker: "i \ a_kernel R S h" + and x: "x = i \ a" + by fast+ + note carr = acarr iker[THEN a_Hcarr] + + from x + have "h x = h (i \ a)" by simp + also from carr + have "\ = h i \\<^bsub>S\<^esub> h a" by simp + also from iker + have "\ = \\<^bsub>S\<^esub> \\<^bsub>S\<^esub> h a" by simp + also from carr + have "\ = h a" by simp + finally + show "h x = h a" . +qed + +lemma (in ring_hom_ring) homeq_imp_rcos: + assumes acarr: "a \ carrier R" + and xcarr: "x \ carrier R" + and hx: "h x = h a" + shows "x \ a_kernel R S h +> a" +proof - + interpret ideal ["a_kernel R S h" "R"] by (rule kernel_is_ideal) + + note carr = acarr xcarr + note hcarr = acarr[THEN hom_closed] xcarr[THEN hom_closed] + + from hx and hcarr + have a: "h x \\<^bsub>S\<^esub> \\<^bsub>S\<^esub>h a = \\<^bsub>S\<^esub>" by algebra + from carr + have "h x \\<^bsub>S\<^esub> \\<^bsub>S\<^esub>h a = h (x \ \a)" by simp + from a and this + have b: "h (x \ \a) = \\<^bsub>S\<^esub>" by simp + + from carr have "x \ \a \ carrier R" by simp + from this and b + have "x \ \a \ a_kernel R S h" + unfolding a_kernel_def' + by fast + + from this and carr + show "x \ a_kernel R S h +> a" by (simp add: a_rcos_module_rev) +qed + +corollary (in ring_hom_ring) rcos_eq_homeq: + assumes acarr: "a \ carrier R" + shows "(a_kernel R S h) +> a = {x \ carrier R. h x = h a}" +apply rule defer 1 +apply clarsimp defer 1 +proof + interpret ideal ["a_kernel R S h" "R"] by (rule kernel_is_ideal) + + fix x + assume xrcos: "x \ a_kernel R S h +> a" + from acarr and this + have xcarr: "x \ carrier R" + by (rule a_elemrcos_carrier) + + from xrcos + have "h x = h a" by (rule rcos_imp_homeq[OF acarr]) + from xcarr and this + show "x \ {x \ carrier R. h x = h a}" by fast +next + interpret ideal ["a_kernel R S h" "R"] by (rule kernel_is_ideal) + + fix x + assume xcarr: "x \ carrier R" + and hx: "h x = h a" + from acarr xcarr hx + show "x \ a_kernel R S h +> a" by (rule homeq_imp_rcos) +qed + +end diff -r 6e070b33e72b -r 0e0ea63fe768 src/HOL/Algebra/Sylow.thy --- a/src/HOL/Algebra/Sylow.thy Thu Aug 03 14:53:57 2006 +0200 +++ b/src/HOL/Algebra/Sylow.thy Thu Aug 03 14:57:26 2006 +0200 @@ -3,9 +3,10 @@ Author: Florian Kammueller, with new proofs by L C Paulson *) -header {* Sylow's theorem *} +theory Sylow imports Coset begin -theory Sylow imports Coset begin + +section {* Sylow's Theorem *} text {* See also \cite{Kammueller-Paulson:1999}. @@ -50,9 +51,9 @@ apply (blast elim!: quotientE) done + subsection{*Main Part of the Proof*} - locale sylow_central = sylow + fixes H and M1 and M assumes M_in_quot: "M \ calM // RelM" @@ -265,7 +266,7 @@ done -subsubsection{*The opposite injection*} +subsubsection{*The Opposite Injection*} lemma (in sylow_central) H_elem_map: "H1 \ rcosets H ==> \g. g \ carrier G & H #> g = H1" @@ -362,6 +363,9 @@ lemma sylow_eq: "sylow G p a m = (group G & sylow_axioms G p a m)" by (simp add: sylow_def group_def) + +subsection {* Sylow's Theorem *} + theorem sylow_thm: "[| prime p; group(G); order(G) = (p^a) * m; finite (carrier G)|] ==> \H. subgroup H G & card(H) = p^a" diff -r 6e070b33e72b -r 0e0ea63fe768 src/HOL/Algebra/UnivPoly.thy --- a/src/HOL/Algebra/UnivPoly.thy Thu Aug 03 14:53:57 2006 +0200 +++ b/src/HOL/Algebra/UnivPoly.thy Thu Aug 03 14:57:26 2006 +0200 @@ -5,9 +5,10 @@ Copyright: Clemens Ballarin *) -header {* Univariate Polynomials *} +theory UnivPoly imports Module begin -theory UnivPoly imports Module begin + +section {* Univariate Polynomials *} text {* Polynomials are formalised as modules with additional operations for @@ -161,7 +162,7 @@ qed -subsection {* Effect of operations on coefficients *} +subsection {* Effect of Operations on Coefficients *} locale UP = fixes R (structure) and P (structure) @@ -219,7 +220,8 @@ from prem and R show "p x = q x" by (simp add: UP_def) qed -subsection {* Polynomials form a commutative ring. *} + +subsection {* Polynomials Form a Commutative Ring. *} text {* Operations are closed over @{term P}. *} @@ -401,7 +403,7 @@ (rule cring.axioms ring.axioms abelian_group.axioms comm_monoid.axioms UP_cring)+ -subsection {* Polynomials form an Algebra *} +subsection {* Polynomials Form an Algebra *} lemma (in UP_cring) UP_smult_l_distr: "[| a \ carrier R; b \ carrier R; p \ carrier P |] ==> @@ -445,7 +447,7 @@ (rule module.axioms algebra.axioms UP_algebra)+ -subsection {* Further lemmas involving monomials *} +subsection {* Further Lemmas Involving Monomials *} lemma (in UP_cring) monom_zero [simp]: "monom P \ n = \\<^bsub>P\<^esub>" @@ -603,7 +605,7 @@ qed -subsection {* The degree function *} +subsection {* The Degree Function *} constdefs (structure R) deg :: "[('a, 'm) ring_scheme, nat => 'a] => nat" @@ -887,7 +889,7 @@ qed -subsection {* Polynomials over an integral domain form an integral domain *} +subsection {* Polynomials over Integral Domains *} lemma domainI: assumes cring: "cring R" @@ -948,7 +950,7 @@ by intro_locales (rule domain.axioms UP_domain)+ -subsection {* Evaluation Homomorphism and Universal Property*} +subsection {* The Evaluation Homomorphism and Universal Property*} (* alternative congruence rule (possibly more efficient) lemma (in abelian_monoid) finsum_cong2: @@ -1290,7 +1292,7 @@ done -subsection {* Sample application of evaluation homomorphism *} +subsection {* Sample Application of Evaluation Homomorphism *} lemma UP_pre_univ_propI: assumes "cring R" diff -r 6e070b33e72b -r 0e0ea63fe768 src/HOL/Algebra/abstract/Factor.thy --- a/src/HOL/Algebra/abstract/Factor.thy Thu Aug 03 14:53:57 2006 +0200 +++ b/src/HOL/Algebra/abstract/Factor.thy Thu Aug 03 14:57:26 2006 +0200 @@ -4,7 +4,7 @@ Author: Clemens Ballarin, started 25 November 1997 *) -theory Factor imports Ring begin +theory Factor imports Ring2 begin constdefs Factorisation :: "['a::ring, 'a list, 'a] => bool" diff -r 6e070b33e72b -r 0e0ea63fe768 src/HOL/Algebra/abstract/Ideal.ML --- a/src/HOL/Algebra/abstract/Ideal.ML Thu Aug 03 14:53:57 2006 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,328 +0,0 @@ -(* - Ideals for commutative rings - $Id$ - Author: Clemens Ballarin, started 24 September 1999 -*) - -(* is_ideal *) - -Goalw [thm "is_ideal_def"] - "!! I. [| !! a b. [| a:I; b:I |] ==> a + b : I; \ -\ !! a. a:I ==> - a : I; 0 : I; \ -\ !! a r. a:I ==> a * r : I |] ==> is_ideal I"; -by Auto_tac; -qed "is_idealI"; - -Goalw [thm "is_ideal_def"] "[| is_ideal I; a:I; b:I |] ==> a + b : I"; -by (Fast_tac 1); -qed "is_ideal_add"; - -Goalw [thm "is_ideal_def"] "[| is_ideal I; a:I |] ==> - a : I"; -by (Fast_tac 1); -qed "is_ideal_uminus"; - -Goalw [thm "is_ideal_def"] "[| is_ideal I |] ==> 0 : I"; -by (Fast_tac 1); -qed "is_ideal_zero"; - -Goalw [thm "is_ideal_def"] "[| is_ideal I; a:I |] ==> a * r : I"; -by (Fast_tac 1); -qed "is_ideal_mult"; - -Goalw [dvd_def, thm "is_ideal_def"] "[| a dvd b; is_ideal I; a:I |] ==> b:I"; -by (Fast_tac 1); -qed "is_ideal_dvd"; - -Goalw [thm "is_ideal_def"] "is_ideal (UNIV::('a::ring) set)"; -by Auto_tac; -qed "UNIV_is_ideal"; - -Goalw [thm "is_ideal_def"] "is_ideal {0::'a::ring}"; -by Auto_tac; -qed "zero_is_ideal"; - -Addsimps [is_ideal_add, is_ideal_uminus, is_ideal_zero, is_ideal_mult, - UNIV_is_ideal, zero_is_ideal]; - -Goal "is_ideal {x::'a::ring. a dvd x}"; -by (rtac is_idealI 1); -by Auto_tac; -qed "is_ideal_1"; - -Goal "is_ideal {x::'a::ring. EX u v. x = a * u + b * v}"; -by (rtac is_idealI 1); -(* by Auto_tac; FIXME: makes Zumkeller's order fail (raises exn Domain) *) -by (Clarify_tac 1); -by (Clarify_tac 2); -by (Clarify_tac 3); -by (Clarify_tac 4); -by (res_inst_tac [("x", "u+ua")] exI 1); -by (res_inst_tac [("x", "v+va")] exI 1); -by (res_inst_tac [("x", "-u")] exI 2); -by (res_inst_tac [("x", "-v")] exI 2); -by (res_inst_tac [("x", "0")] exI 3); -by (res_inst_tac [("x", "0")] exI 3); -by (res_inst_tac [("x", "u * r")] exI 4); -by (res_inst_tac [("x", "v * r")] exI 4); -by (REPEAT (Simp_tac 1)); -qed "is_ideal_2"; - -(* ideal_of *) - -Goalw [thm "is_ideal_def", thm "ideal_of_def"] "is_ideal (ideal_of S)"; -by (Blast_tac 1); (* Here, blast_tac is much superior to fast_tac! *) -qed "ideal_of_is_ideal"; - -Goalw [thm "ideal_of_def"] "a:S ==> a : (ideal_of S)"; -by Auto_tac; -qed "generator_in_ideal"; - -Goalw [thm "ideal_of_def"] "ideal_of {1::'a::ring} = UNIV"; -by (force_tac (claset() addDs [is_ideal_mult], - simpset() addsimps [l_one] delsimprocs [ring_simproc]) 1); - (* FIXME: Zumkeller's order raises Domain exn *) -qed "ideal_of_one_eq"; - -Goalw [thm "ideal_of_def"] "ideal_of {} = {0::'a::ring}"; -by (rtac subset_antisym 1); -by (rtac subsetI 1); -by (dtac InterD 1); -by (assume_tac 2); -by (auto_tac (claset(), simpset() addsimps [is_ideal_zero])); -qed "ideal_of_empty_eq"; - -Goalw [thm "ideal_of_def"] "ideal_of {a} = {x::'a::ring. a dvd x}"; -by (rtac subset_antisym 1); -by (rtac subsetI 1); -by (dtac InterD 1); -by (assume_tac 2); -by (auto_tac (claset() addIs [is_ideal_1], simpset())); -by (asm_simp_tac (simpset() addsimps [is_ideal_dvd]) 1); -qed "pideal_structure"; - -Goalw [thm "ideal_of_def"] - "ideal_of {a, b} = {x::'a::ring. EX u v. x = a * u + b * v}"; -by (rtac subset_antisym 1); -by (rtac subsetI 1); -by (dtac InterD 1); -by (assume_tac 2); -by (auto_tac (claset() addIs [is_ideal_2], - simpset() delsimprocs [ring_simproc])); -(* FIXME: Zumkeller's order *) -by (res_inst_tac [("x", "1")] exI 1); -by (res_inst_tac [("x", "0")] exI 1); -by (res_inst_tac [("x", "0")] exI 2); -by (res_inst_tac [("x", "1")] exI 2); -by (Simp_tac 1); -by (Simp_tac 1); -qed "ideal_of_2_structure"; - -Goalw [thm "ideal_of_def"] "A <= B ==> ideal_of A <= ideal_of B"; -by Auto_tac; -qed "ideal_of_mono"; - -Goal "ideal_of {0::'a::ring} = {0}"; -by (simp_tac (simpset() addsimps [pideal_structure]) 1); -by (rtac subset_antisym 1); -by (auto_tac (claset() addIs [dvd_zero_left], simpset())); -qed "ideal_of_zero_eq"; - -Goal "[| is_ideal I; a : I |] ==> ideal_of {a::'a::ring} <= I"; -by (auto_tac (claset(), - simpset() addsimps [pideal_structure, is_ideal_dvd])); -qed "element_generates_subideal"; - -(* is_pideal *) - -Goalw [thm "is_pideal_def"] "is_pideal (I::('a::ring) set) ==> is_ideal I"; -by (fast_tac (claset() addIs [ideal_of_is_ideal]) 1); -qed "is_pideal_imp_is_ideal"; - -Goalw [thm "is_pideal_def"] "is_pideal (ideal_of {a::'a::ring})"; -by (Fast_tac 1); -qed "pideal_is_pideal"; - -Goalw [thm "is_pideal_def"] "is_pideal I ==> EX a. I = ideal_of {a}"; -by (assume_tac 1); -qed "is_pidealD"; - -(* Ideals and divisibility *) - -Goal "b dvd a ==> ideal_of {a::'a::ring} <= ideal_of {b}"; -by (auto_tac (claset() addIs [dvd_trans_ring], - simpset() addsimps [pideal_structure])); -qed "dvd_imp_subideal"; - -Goal "ideal_of {a::'a::ring} <= ideal_of {b} ==> b dvd a"; -by (auto_tac (claset() addSDs [subsetD], - simpset() addsimps [pideal_structure])); -qed "subideal_imp_dvd"; - -Goal "(ideal_of {a::'a::ring} <= ideal_of {b}) = (b dvd a)"; -by (rtac iffI 1); -by (REPEAT (ares_tac [subideal_imp_dvd, dvd_imp_subideal] 1)); -qed "subideal_is_dvd"; - -Goal "(ideal_of {a::'a::ring} < ideal_of {b}) ==> ~ a dvd b"; -by (full_simp_tac (simpset() addsimps [psubset_eq, pideal_structure]) 1); -by (etac conjE 1); -by (dres_inst_tac [("c", "a")] subsetD 1); -by (auto_tac (claset() addIs [dvd_trans_ring], - simpset())); -qed "psubideal_not_dvd"; - -Goal "[| b dvd a; ~ a dvd b |] ==> ideal_of {a::'a::ring} < ideal_of {b}"; -by (rtac psubsetI 1); -by (etac dvd_imp_subideal 1); -by (blast_tac (claset() addIs [dvd_imp_subideal, subideal_imp_dvd]) 1); -qed "not_dvd_psubideal_singleton"; - -Goal "(ideal_of {a::'a::ring} < ideal_of {b}) = (b dvd a & ~ a dvd b)"; -by (rtac iffI 1); -by (REPEAT (ares_tac - [conjI, psubideal_not_dvd, psubset_imp_subset RS subideal_imp_dvd] 1)); -by (etac conjE 1); -by (REPEAT (ares_tac [not_dvd_psubideal_singleton] 1)); -qed "psubideal_is_dvd"; - -Goal "[| a dvd b; b dvd a |] ==> ideal_of {a::'a::ring} = ideal_of {b}"; -by (rtac subset_antisym 1); -by (REPEAT (ares_tac [dvd_imp_subideal] 1)); -qed "assoc_pideal_eq"; - -AddIffs [subideal_is_dvd, psubideal_is_dvd]; - -Goal "!!a::'a::ring. a dvd b ==> b : (ideal_of {a})"; -by (rtac is_ideal_dvd 1); -by (assume_tac 1); -by (rtac ideal_of_is_ideal 1); -by (rtac generator_in_ideal 1); -by (Simp_tac 1); -qed "dvd_imp_in_pideal"; - -Goal "!!a::'a::ring. b : (ideal_of {a}) ==> a dvd b"; -by (full_simp_tac (simpset() addsimps [pideal_structure]) 1); -qed "in_pideal_imp_dvd"; - -Goal "~ (a dvd b) ==> ideal_of {a::'a::ring} < ideal_of {a, b}"; -by (asm_simp_tac (simpset() addsimps [psubset_eq, ideal_of_mono]) 1); -by (etac contrapos_pp 1); -by (full_simp_tac (simpset() addsimps [ideal_of_2_structure]) 1); -by (rtac in_pideal_imp_dvd 1); -by (Asm_simp_tac 1); -by (res_inst_tac [("x", "0")] exI 1); -by (res_inst_tac [("x", "1")] exI 1); -by (Simp_tac 1); -qed "not_dvd_psubideal"; - -Goalw [thm "irred_def"] - "[| irred (a::'a::ring); is_pideal I; ideal_of {a} < I |] ==> x : I"; -by (dtac is_pidealD 1); -by (etac exE 1); -by (Clarify_tac 1); -by (eres_inst_tac [("x", "aa")] allE 1); -by (Clarify_tac 1); -by (dres_inst_tac [("a", "1")] dvd_imp_subideal 1); -by (auto_tac (claset(), simpset() addsimps [ideal_of_one_eq])); -qed "irred_imp_max_ideal"; - -(* Pid are factorial *) - -(* Divisor chain condition *) -(* proofs not finished *) - -Goal "(ALL i. I i <= I (Suc i)) ==> (n <= m & a : I n --> a : I m)"; -by (induct_tac "m" 1); -by (Blast_tac 1); -(* induction step *) -by (rename_tac "m" 1); -by (case_tac "n <= m" 1); -by Auto_tac; -by (subgoal_tac "n = Suc m" 1); -by (arith_tac 2); -by (Force_tac 1); -qed_spec_mp "subset_chain_lemma"; - -Goal "[| ALL i. is_ideal (I i); ALL i. I i <= I (Suc i) |] \ -\ ==> is_ideal (Union (I`UNIV))"; -by (rtac is_idealI 1); -by Auto_tac; -by (res_inst_tac [("x", "max x xa")] exI 1); -by (rtac is_ideal_add 1); -by (Asm_simp_tac 1); -by (rtac subset_chain_lemma 1); -by (assume_tac 1); -by (rtac conjI 1); -by (assume_tac 2); -by (arith_tac 1); -by (rtac subset_chain_lemma 1); -by (assume_tac 1); -by (rtac conjI 1); -by (assume_tac 2); -by (arith_tac 1); -by (res_inst_tac [("x", "x")] exI 1); -by (Asm_simp_tac 1); -by (res_inst_tac [("x", "x")] exI 1); -by (Asm_simp_tac 1); -qed "chain_is_ideal"; - -(* -Goal "ALL i. ideal_of {a i} < ideal_of {a (Suc i)} ==> \ -\ EX n. Union ((ideal_of o (%a. {a}))`UNIV) = ideal_of {a n}"; - -Goal "wf {(a::'a::pid, b). a dvd b & ~ b dvd a}"; -by (simp_tac (simpset() - addsimps [psubideal_is_dvd RS sym, wf_iff_no_infinite_down_chain] - delsimps [psubideal_is_dvd]) 1); -*) - -(* Primeness condition *) - -Goalw [thm "prime_def"] "irred a ==> prime (a::'a::pid)"; -by (rtac conjI 1); -by (rtac conjI 2); -by (Clarify_tac 3); -by (dres_inst_tac [("I", "ideal_of {a, b}"), ("x", "1")] - irred_imp_max_ideal 3); -by (auto_tac (claset() addIs [ideal_of_is_ideal, thm "pid_ax"], - simpset() addsimps [thm "irred_def", not_dvd_psubideal, thm "pid_ax"])); -by (full_simp_tac (simpset() addsimps [ideal_of_2_structure]) 1); -by (Clarify_tac 1); -by (dres_inst_tac [("f", "op* aa")] arg_cong 1); -by (full_simp_tac (simpset() addsimps [r_distr]) 1); -by (etac subst 1); -by (asm_simp_tac (simpset() addsimps [m_assoc RS sym] - delsimprocs [ring_simproc]) 1); -qed "pid_irred_imp_prime"; - -(* Fields are Pid *) - -Goal "a ~= 0 ==> ideal_of {a::'a::field} = UNIV"; -by (rtac subset_antisym 1); -by (Simp_tac 1); -by (rtac subset_trans 1); -by (rtac dvd_imp_subideal 2); -by (rtac (thm "field_ax") 2); -by (assume_tac 2); -by (simp_tac (simpset() addsimps [ideal_of_one_eq]) 1); -qed "field_pideal_univ"; - -Goal "[| is_ideal I; I ~= {0} |] ==> {0} < I"; -by (asm_simp_tac (simpset() addsimps [psubset_eq, not_sym, is_ideal_zero]) 1); -qed "proper_ideal"; - -Goalw [thm "is_pideal_def"] "is_ideal (I::('a::field) set) ==> is_pideal I"; -by (case_tac "I = {0}" 1); -by (res_inst_tac [("x", "0")] exI 1); -by (asm_simp_tac (simpset() addsimps [ideal_of_zero_eq]) 1); -(* case "I ~= {0}" *) -by (ftac proper_ideal 1); -by (assume_tac 1); -by (dtac psubset_imp_ex_mem 1); -by (etac exE 1); -by (res_inst_tac [("x", "b")] exI 1); -by (cut_inst_tac [("a", "b")] element_generates_subideal 1); - by (assume_tac 1); by (Blast_tac 1); -by (auto_tac (claset(), simpset() addsimps [field_pideal_univ])); -qed "field_pid"; - diff -r 6e070b33e72b -r 0e0ea63fe768 src/HOL/Algebra/abstract/Ideal.thy --- a/src/HOL/Algebra/abstract/Ideal.thy Thu Aug 03 14:53:57 2006 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,26 +0,0 @@ -(* - Ideals for commutative rings - $Id$ - Author: Clemens Ballarin, started 24 September 1999 -*) - -theory Ideal imports Ring begin - -consts - ideal_of :: "('a::ring) set => 'a set" - is_ideal :: "('a::ring) set => bool" - is_pideal :: "('a::ring) set => bool" - -defs - is_ideal_def: "is_ideal I == (ALL a: I. ALL b: I. a + b : I) & - (ALL a: I. - a : I) & 0 : I & - (ALL a: I. ALL r. a * r : I)" - ideal_of_def: "ideal_of S == Inter {I. is_ideal I & S <= I}" - is_pideal_def: "is_pideal I == (EX a. I = ideal_of {a})" - -text {* Principle ideal domains *} - -axclass pid < "domain" - pid_ax: "is_ideal I ==> is_pideal I" - -end diff -r 6e070b33e72b -r 0e0ea63fe768 src/HOL/Algebra/abstract/Ideal2.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Algebra/abstract/Ideal2.ML Thu Aug 03 14:57:26 2006 +0200 @@ -0,0 +1,328 @@ +(* + Ideals for commutative rings + $Id$ + Author: Clemens Ballarin, started 24 September 1999 +*) + +(* is_ideal *) + +Goalw [thm "is_ideal_def"] + "!! I. [| !! a b. [| a:I; b:I |] ==> a + b : I; \ +\ !! a. a:I ==> - a : I; 0 : I; \ +\ !! a r. a:I ==> a * r : I |] ==> is_ideal I"; +by Auto_tac; +qed "is_idealI"; + +Goalw [thm "is_ideal_def"] "[| is_ideal I; a:I; b:I |] ==> a + b : I"; +by (Fast_tac 1); +qed "is_ideal_add"; + +Goalw [thm "is_ideal_def"] "[| is_ideal I; a:I |] ==> - a : I"; +by (Fast_tac 1); +qed "is_ideal_uminus"; + +Goalw [thm "is_ideal_def"] "[| is_ideal I |] ==> 0 : I"; +by (Fast_tac 1); +qed "is_ideal_zero"; + +Goalw [thm "is_ideal_def"] "[| is_ideal I; a:I |] ==> a * r : I"; +by (Fast_tac 1); +qed "is_ideal_mult"; + +Goalw [dvd_def, thm "is_ideal_def"] "[| a dvd b; is_ideal I; a:I |] ==> b:I"; +by (Fast_tac 1); +qed "is_ideal_dvd"; + +Goalw [thm "is_ideal_def"] "is_ideal (UNIV::('a::ring) set)"; +by Auto_tac; +qed "UNIV_is_ideal"; + +Goalw [thm "is_ideal_def"] "is_ideal {0::'a::ring}"; +by Auto_tac; +qed "zero_is_ideal"; + +Addsimps [is_ideal_add, is_ideal_uminus, is_ideal_zero, is_ideal_mult, + UNIV_is_ideal, zero_is_ideal]; + +Goal "is_ideal {x::'a::ring. a dvd x}"; +by (rtac is_idealI 1); +by Auto_tac; +qed "is_ideal_1"; + +Goal "is_ideal {x::'a::ring. EX u v. x = a * u + b * v}"; +by (rtac is_idealI 1); +(* by Auto_tac; FIXME: makes Zumkeller's order fail (raises exn Domain) *) +by (Clarify_tac 1); +by (Clarify_tac 2); +by (Clarify_tac 3); +by (Clarify_tac 4); +by (res_inst_tac [("x", "u+ua")] exI 1); +by (res_inst_tac [("x", "v+va")] exI 1); +by (res_inst_tac [("x", "-u")] exI 2); +by (res_inst_tac [("x", "-v")] exI 2); +by (res_inst_tac [("x", "0")] exI 3); +by (res_inst_tac [("x", "0")] exI 3); +by (res_inst_tac [("x", "u * r")] exI 4); +by (res_inst_tac [("x", "v * r")] exI 4); +by (REPEAT (Simp_tac 1)); +qed "is_ideal_2"; + +(* ideal_of *) + +Goalw [thm "is_ideal_def", thm "ideal_of_def"] "is_ideal (ideal_of S)"; +by (Blast_tac 1); (* Here, blast_tac is much superior to fast_tac! *) +qed "ideal_of_is_ideal"; + +Goalw [thm "ideal_of_def"] "a:S ==> a : (ideal_of S)"; +by Auto_tac; +qed "generator_in_ideal"; + +Goalw [thm "ideal_of_def"] "ideal_of {1::'a::ring} = UNIV"; +by (force_tac (claset() addDs [is_ideal_mult], + simpset() addsimps [l_one] delsimprocs [ring_simproc]) 1); + (* FIXME: Zumkeller's order raises Domain exn *) +qed "ideal_of_one_eq"; + +Goalw [thm "ideal_of_def"] "ideal_of {} = {0::'a::ring}"; +by (rtac subset_antisym 1); +by (rtac subsetI 1); +by (dtac InterD 1); +by (assume_tac 2); +by (auto_tac (claset(), simpset() addsimps [is_ideal_zero])); +qed "ideal_of_empty_eq"; + +Goalw [thm "ideal_of_def"] "ideal_of {a} = {x::'a::ring. a dvd x}"; +by (rtac subset_antisym 1); +by (rtac subsetI 1); +by (dtac InterD 1); +by (assume_tac 2); +by (auto_tac (claset() addIs [is_ideal_1], simpset())); +by (asm_simp_tac (simpset() addsimps [is_ideal_dvd]) 1); +qed "pideal_structure"; + +Goalw [thm "ideal_of_def"] + "ideal_of {a, b} = {x::'a::ring. EX u v. x = a * u + b * v}"; +by (rtac subset_antisym 1); +by (rtac subsetI 1); +by (dtac InterD 1); +by (assume_tac 2); +by (auto_tac (claset() addIs [is_ideal_2], + simpset() delsimprocs [ring_simproc])); +(* FIXME: Zumkeller's order *) +by (res_inst_tac [("x", "1")] exI 1); +by (res_inst_tac [("x", "0")] exI 1); +by (res_inst_tac [("x", "0")] exI 2); +by (res_inst_tac [("x", "1")] exI 2); +by (Simp_tac 1); +by (Simp_tac 1); +qed "ideal_of_2_structure"; + +Goalw [thm "ideal_of_def"] "A <= B ==> ideal_of A <= ideal_of B"; +by Auto_tac; +qed "ideal_of_mono"; + +Goal "ideal_of {0::'a::ring} = {0}"; +by (simp_tac (simpset() addsimps [pideal_structure]) 1); +by (rtac subset_antisym 1); +by (auto_tac (claset() addIs [dvd_zero_left], simpset())); +qed "ideal_of_zero_eq"; + +Goal "[| is_ideal I; a : I |] ==> ideal_of {a::'a::ring} <= I"; +by (auto_tac (claset(), + simpset() addsimps [pideal_structure, is_ideal_dvd])); +qed "element_generates_subideal"; + +(* is_pideal *) + +Goalw [thm "is_pideal_def"] "is_pideal (I::('a::ring) set) ==> is_ideal I"; +by (fast_tac (claset() addIs [ideal_of_is_ideal]) 1); +qed "is_pideal_imp_is_ideal"; + +Goalw [thm "is_pideal_def"] "is_pideal (ideal_of {a::'a::ring})"; +by (Fast_tac 1); +qed "pideal_is_pideal"; + +Goalw [thm "is_pideal_def"] "is_pideal I ==> EX a. I = ideal_of {a}"; +by (assume_tac 1); +qed "is_pidealD"; + +(* Ideals and divisibility *) + +Goal "b dvd a ==> ideal_of {a::'a::ring} <= ideal_of {b}"; +by (auto_tac (claset() addIs [dvd_trans_ring], + simpset() addsimps [pideal_structure])); +qed "dvd_imp_subideal"; + +Goal "ideal_of {a::'a::ring} <= ideal_of {b} ==> b dvd a"; +by (auto_tac (claset() addSDs [subsetD], + simpset() addsimps [pideal_structure])); +qed "subideal_imp_dvd"; + +Goal "(ideal_of {a::'a::ring} <= ideal_of {b}) = (b dvd a)"; +by (rtac iffI 1); +by (REPEAT (ares_tac [subideal_imp_dvd, dvd_imp_subideal] 1)); +qed "subideal_is_dvd"; + +Goal "(ideal_of {a::'a::ring} < ideal_of {b}) ==> ~ a dvd b"; +by (full_simp_tac (simpset() addsimps [psubset_eq, pideal_structure]) 1); +by (etac conjE 1); +by (dres_inst_tac [("c", "a")] subsetD 1); +by (auto_tac (claset() addIs [dvd_trans_ring], + simpset())); +qed "psubideal_not_dvd"; + +Goal "[| b dvd a; ~ a dvd b |] ==> ideal_of {a::'a::ring} < ideal_of {b}"; +by (rtac psubsetI 1); +by (etac dvd_imp_subideal 1); +by (blast_tac (claset() addIs [dvd_imp_subideal, subideal_imp_dvd]) 1); +qed "not_dvd_psubideal_singleton"; + +Goal "(ideal_of {a::'a::ring} < ideal_of {b}) = (b dvd a & ~ a dvd b)"; +by (rtac iffI 1); +by (REPEAT (ares_tac + [conjI, psubideal_not_dvd, psubset_imp_subset RS subideal_imp_dvd] 1)); +by (etac conjE 1); +by (REPEAT (ares_tac [not_dvd_psubideal_singleton] 1)); +qed "psubideal_is_dvd"; + +Goal "[| a dvd b; b dvd a |] ==> ideal_of {a::'a::ring} = ideal_of {b}"; +by (rtac subset_antisym 1); +by (REPEAT (ares_tac [dvd_imp_subideal] 1)); +qed "assoc_pideal_eq"; + +AddIffs [subideal_is_dvd, psubideal_is_dvd]; + +Goal "!!a::'a::ring. a dvd b ==> b : (ideal_of {a})"; +by (rtac is_ideal_dvd 1); +by (assume_tac 1); +by (rtac ideal_of_is_ideal 1); +by (rtac generator_in_ideal 1); +by (Simp_tac 1); +qed "dvd_imp_in_pideal"; + +Goal "!!a::'a::ring. b : (ideal_of {a}) ==> a dvd b"; +by (full_simp_tac (simpset() addsimps [pideal_structure]) 1); +qed "in_pideal_imp_dvd"; + +Goal "~ (a dvd b) ==> ideal_of {a::'a::ring} < ideal_of {a, b}"; +by (asm_simp_tac (simpset() addsimps [psubset_eq, ideal_of_mono]) 1); +by (etac contrapos_pp 1); +by (full_simp_tac (simpset() addsimps [ideal_of_2_structure]) 1); +by (rtac in_pideal_imp_dvd 1); +by (Asm_simp_tac 1); +by (res_inst_tac [("x", "0")] exI 1); +by (res_inst_tac [("x", "1")] exI 1); +by (Simp_tac 1); +qed "not_dvd_psubideal"; + +Goalw [thm "irred_def"] + "[| irred (a::'a::ring); is_pideal I; ideal_of {a} < I |] ==> x : I"; +by (dtac is_pidealD 1); +by (etac exE 1); +by (Clarify_tac 1); +by (eres_inst_tac [("x", "aa")] allE 1); +by (Clarify_tac 1); +by (dres_inst_tac [("a", "1")] dvd_imp_subideal 1); +by (auto_tac (claset(), simpset() addsimps [ideal_of_one_eq])); +qed "irred_imp_max_ideal"; + +(* Pid are factorial *) + +(* Divisor chain condition *) +(* proofs not finished *) + +Goal "(ALL i. I i <= I (Suc i)) ==> (n <= m & a : I n --> a : I m)"; +by (induct_tac "m" 1); +by (Blast_tac 1); +(* induction step *) +by (rename_tac "m" 1); +by (case_tac "n <= m" 1); +by Auto_tac; +by (subgoal_tac "n = Suc m" 1); +by (arith_tac 2); +by (Force_tac 1); +qed_spec_mp "subset_chain_lemma"; + +Goal "[| ALL i. is_ideal (I i); ALL i. I i <= I (Suc i) |] \ +\ ==> is_ideal (Union (I`UNIV))"; +by (rtac is_idealI 1); +by Auto_tac; +by (res_inst_tac [("x", "max x xa")] exI 1); +by (rtac is_ideal_add 1); +by (Asm_simp_tac 1); +by (rtac subset_chain_lemma 1); +by (assume_tac 1); +by (rtac conjI 1); +by (assume_tac 2); +by (arith_tac 1); +by (rtac subset_chain_lemma 1); +by (assume_tac 1); +by (rtac conjI 1); +by (assume_tac 2); +by (arith_tac 1); +by (res_inst_tac [("x", "x")] exI 1); +by (Asm_simp_tac 1); +by (res_inst_tac [("x", "x")] exI 1); +by (Asm_simp_tac 1); +qed "chain_is_ideal"; + +(* +Goal "ALL i. ideal_of {a i} < ideal_of {a (Suc i)} ==> \ +\ EX n. Union ((ideal_of o (%a. {a}))`UNIV) = ideal_of {a n}"; + +Goal "wf {(a::'a::pid, b). a dvd b & ~ b dvd a}"; +by (simp_tac (simpset() + addsimps [psubideal_is_dvd RS sym, wf_iff_no_infinite_down_chain] + delsimps [psubideal_is_dvd]) 1); +*) + +(* Primeness condition *) + +Goalw [thm "prime_def"] "irred a ==> prime (a::'a::pid)"; +by (rtac conjI 1); +by (rtac conjI 2); +by (Clarify_tac 3); +by (dres_inst_tac [("I", "ideal_of {a, b}"), ("x", "1")] + irred_imp_max_ideal 3); +by (auto_tac (claset() addIs [ideal_of_is_ideal, thm "pid_ax"], + simpset() addsimps [thm "irred_def", not_dvd_psubideal, thm "pid_ax"])); +by (full_simp_tac (simpset() addsimps [ideal_of_2_structure]) 1); +by (Clarify_tac 1); +by (dres_inst_tac [("f", "op* aa")] arg_cong 1); +by (full_simp_tac (simpset() addsimps [r_distr]) 1); +by (etac subst 1); +by (asm_simp_tac (simpset() addsimps [m_assoc RS sym] + delsimprocs [ring_simproc]) 1); +qed "pid_irred_imp_prime"; + +(* Fields are Pid *) + +Goal "a ~= 0 ==> ideal_of {a::'a::field} = UNIV"; +by (rtac subset_antisym 1); +by (Simp_tac 1); +by (rtac subset_trans 1); +by (rtac dvd_imp_subideal 2); +by (rtac (thm "field_ax") 2); +by (assume_tac 2); +by (simp_tac (simpset() addsimps [ideal_of_one_eq]) 1); +qed "field_pideal_univ"; + +Goal "[| is_ideal I; I ~= {0} |] ==> {0} < I"; +by (asm_simp_tac (simpset() addsimps [psubset_eq, not_sym, is_ideal_zero]) 1); +qed "proper_ideal"; + +Goalw [thm "is_pideal_def"] "is_ideal (I::('a::field) set) ==> is_pideal I"; +by (case_tac "I = {0}" 1); +by (res_inst_tac [("x", "0")] exI 1); +by (asm_simp_tac (simpset() addsimps [ideal_of_zero_eq]) 1); +(* case "I ~= {0}" *) +by (ftac proper_ideal 1); +by (assume_tac 1); +by (dtac psubset_imp_ex_mem 1); +by (etac exE 1); +by (res_inst_tac [("x", "b")] exI 1); +by (cut_inst_tac [("a", "b")] element_generates_subideal 1); + by (assume_tac 1); by (Blast_tac 1); +by (auto_tac (claset(), simpset() addsimps [field_pideal_univ])); +qed "field_pid"; + diff -r 6e070b33e72b -r 0e0ea63fe768 src/HOL/Algebra/abstract/Ideal2.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Algebra/abstract/Ideal2.thy Thu Aug 03 14:57:26 2006 +0200 @@ -0,0 +1,26 @@ +(* + Ideals for commutative rings + $Id$ + Author: Clemens Ballarin, started 24 September 1999 +*) + +theory Ideal2 imports Ring2 begin + +consts + ideal_of :: "('a::ring) set => 'a set" + is_ideal :: "('a::ring) set => bool" + is_pideal :: "('a::ring) set => bool" + +defs + is_ideal_def: "is_ideal I == (ALL a: I. ALL b: I. a + b : I) & + (ALL a: I. - a : I) & 0 : I & + (ALL a: I. ALL r. a * r : I)" + ideal_of_def: "ideal_of S == Inter {I. is_ideal I & S <= I}" + is_pideal_def: "is_pideal I == (EX a. I = ideal_of {a})" + +text {* Principle ideal domains *} + +axclass pid < "domain" + pid_ax: "is_ideal I ==> is_pideal I" + +end diff -r 6e070b33e72b -r 0e0ea63fe768 src/HOL/Algebra/abstract/PID.thy --- a/src/HOL/Algebra/abstract/PID.thy Thu Aug 03 14:53:57 2006 +0200 +++ b/src/HOL/Algebra/abstract/PID.thy Thu Aug 03 14:57:26 2006 +0200 @@ -4,7 +4,7 @@ Author: Clemens Ballarin, started 5 October 1999 *) -theory PID imports Ideal begin +theory PID imports Ideal2 begin instance pid < factorial apply intro_classes diff -r 6e070b33e72b -r 0e0ea63fe768 src/HOL/Algebra/abstract/Ring.ML --- a/src/HOL/Algebra/abstract/Ring.ML Thu Aug 03 14:53:57 2006 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,404 +0,0 @@ -(* - Abstract class ring (commutative, with 1) - $Id$ - Author: Clemens Ballarin, started 9 December 1996 -*) - -(* -val a_assoc = thm "semigroup_add.add_assoc"; -val l_zero = thm "comm_monoid_add.add_0"; -val a_comm = thm "ab_semigroup_add.add_commute"; - -section "Rings"; - -fun make_left_commute assoc commute s = - [rtac (commute RS trans) 1, rtac (assoc RS trans) 1, - rtac (commute RS arg_cong) 1]; - -(* addition *) - -qed_goal "a_lcomm" Ring.thy "!!a::'a::ring. a+(b+c) = b+(a+c)" - (make_left_commute a_assoc a_comm); - -val a_ac = [a_assoc, a_comm, a_lcomm]; - -Goal "!!a::'a::ring. a + 0 = a"; -by (rtac (a_comm RS trans) 1); -by (rtac l_zero 1); -qed "r_zero"; - -Goal "!!a::'a::ring. a + (-a) = 0"; -by (rtac (a_comm RS trans) 1); -by (rtac l_neg 1); -qed "r_neg"; - -Goal "!! a::'a::ring. a + b = a + c ==> b = c"; -by (rtac box_equals 1); -by (rtac l_zero 2); -by (rtac l_zero 2); -by (res_inst_tac [("a1", "a")] (l_neg RS subst) 1); -by (asm_simp_tac (simpset() addsimps [a_assoc]) 1); -qed "a_lcancel"; - -Goal "!! a::'a::ring. b + a = c + a ==> b = c"; -by (rtac a_lcancel 1); -by (asm_simp_tac (simpset() addsimps a_ac) 1); -qed "a_rcancel"; - -Goal "!! a::'a::ring. (a + b = a + c) = (b = c)"; -by (auto_tac (claset() addSDs [a_lcancel], simpset())); -qed "a_lcancel_eq"; - -Goal "!! a::'a::ring. (b + a = c + a) = (b = c)"; -by (simp_tac (simpset() addsimps [a_lcancel_eq, a_comm]) 1); -qed "a_rcancel_eq"; - -Addsimps [a_lcancel_eq, a_rcancel_eq]; - -Goal "!!a::'a::ring. -(-a) = a"; -by (rtac a_lcancel 1); -by (rtac (r_neg RS trans) 1); -by (rtac (l_neg RS sym) 1); -qed "minus_minus"; - -Goal "- 0 = (0::'a::ring)"; -by (rtac a_lcancel 1); -by (rtac (r_neg RS trans) 1); -by (rtac (l_zero RS sym) 1); -qed "minus0"; - -Goal "!!a::'a::ring. -(a + b) = (-a) + (-b)"; -by (res_inst_tac [("a", "a+b")] a_lcancel 1); -by (simp_tac (simpset() addsimps ([r_neg, l_neg, l_zero]@a_ac)) 1); -qed "minus_add"; - -(* multiplication *) - -qed_goal "m_lcomm" Ring.thy "!!a::'a::ring. a*(b*c) = b*(a*c)" - (make_left_commute m_assoc m_comm); - -val m_ac = [m_assoc, m_comm, m_lcomm]; - -Goal "!!a::'a::ring. a * 1 = a"; -by (rtac (m_comm RS trans) 1); -by (rtac l_one 1); -qed "r_one"; - -(* distributive and derived *) - -Goal "!!a::'a::ring. a * (b + c) = a * b + a * c"; -by (rtac (m_comm RS trans) 1); -by (rtac (l_distr RS trans) 1); -by (simp_tac (simpset() addsimps [m_comm]) 1); -qed "r_distr"; - -val m_distr = m_ac @ [l_distr, r_distr]; - -(* the following two proofs can be found in - Jacobson, Basic Algebra I, pp. 88-89 *) - -Goal "!!a::'a::ring. 0 * a = 0"; -by (rtac a_lcancel 1); -by (rtac (l_distr RS sym RS trans) 1); -by (simp_tac (simpset() addsimps [r_zero]) 1); -qed "l_null"; - -Goal "!!a::'a::ring. a * 0 = 0"; -by (rtac (m_comm RS trans) 1); -by (rtac l_null 1); -qed "r_null"; - -Goal "!!a::'a::ring. (-a) * b = - (a * b)"; -by (rtac a_lcancel 1); -by (rtac (r_neg RS sym RSN (2, trans)) 1); -by (rtac (l_distr RS sym RS trans) 1); -by (simp_tac (simpset() addsimps [l_null, r_neg]) 1); -qed "l_minus"; - -Goal "!!a::'a::ring. a * (-b) = - (a * b)"; -by (rtac a_lcancel 1); -by (rtac (r_neg RS sym RSN (2, trans)) 1); -by (rtac (r_distr RS sym RS trans) 1); -by (simp_tac (simpset() addsimps [r_null, r_neg]) 1); -qed "r_minus"; - -val m_minus = [l_minus, r_minus]; - -Addsimps [l_zero, r_zero, l_neg, r_neg, minus_minus, minus0, - l_one, r_one, l_null, r_null]; - -(* further rules *) - -Goal "!!a::'a::ring. -a = 0 ==> a = 0"; -by (res_inst_tac [("t", "a")] (minus_minus RS subst) 1); -by (Asm_simp_tac 1); -qed "uminus_monom"; - -Goal "!!a::'a::ring. a ~= 0 ==> -a ~= 0"; -by (blast_tac (claset() addIs [uminus_monom]) 1); -qed "uminus_monom_neq"; - -Goal "!!a::'a::ring. a * b ~= 0 ==> a ~= 0"; -by Auto_tac; -qed "l_nullD"; - -Goal "!!a::'a::ring. a * b ~= 0 ==> b ~= 0"; -by Auto_tac; -qed "r_nullD"; - -(* reflection between a = b and a -- b = 0 *) - -Goal "!!a::'a::ring. a = b ==> a + (-b) = 0"; -by (Asm_simp_tac 1); -qed "eq_imp_diff_zero"; - -Goal "!!a::'a::ring. a + (-b) = 0 ==> a = b"; -by (res_inst_tac [("a", "-b")] a_rcancel 1); -by (Asm_simp_tac 1); -qed "diff_zero_imp_eq"; - -(* this could be a rewrite rule, but won't terminate - ==> make it a simproc? -Goal "!!a::'a::ring. (a = b) = (a -- b = 0)"; -*) - -*) - -(* Power *) - -Goal "!!a::'a::ring. a ^ 0 = 1"; -by (simp_tac (simpset() addsimps [power_def]) 1); -qed "power_0"; - -Goal "!!a::'a::ring. a ^ Suc n = a ^ n * a"; -by (simp_tac (simpset() addsimps [power_def]) 1); -qed "power_Suc"; - -Addsimps [power_0, power_Suc]; - -Goal "1 ^ n = (1::'a::ring)"; -by (induct_tac "n" 1); -by Auto_tac; -qed "power_one"; - -Goal "!!n. n ~= 0 ==> 0 ^ n = (0::'a::ring)"; -by (etac rev_mp 1); -by (induct_tac "n" 1); -by Auto_tac; -qed "power_zero"; - -Addsimps [power_zero, power_one]; - -Goal "!! a::'a::ring. a ^ m * a ^ n = a ^ (m + n)"; -by (induct_tac "m" 1); -by (Simp_tac 1); -by (Asm_simp_tac 1); -qed "power_mult"; - -(* Divisibility *) -section "Divisibility"; - -Goalw [dvd_def] "!! a::'a::ring. a dvd 0"; -by (res_inst_tac [("x", "0")] exI 1); -by (Simp_tac 1); -qed "dvd_zero_right"; - -Goalw [dvd_def] "!! a::'a::ring. 0 dvd a ==> a = 0"; -by Auto_tac; -qed "dvd_zero_left"; - -Goalw [dvd_def] "!! a::'a::ring. a dvd a"; -by (res_inst_tac [("x", "1")] exI 1); -by (Simp_tac 1); -qed "dvd_refl_ring"; - -Goalw [dvd_def] "!! a::'a::ring. [| a dvd b; b dvd c |] ==> a dvd c"; -by (Step_tac 1); -by (res_inst_tac [("x", "k * ka")] exI 1); -by (Asm_simp_tac 1); -qed "dvd_trans_ring"; - -Addsimps [dvd_zero_right, dvd_refl_ring]; - -Goalw [dvd_def] - "!!a::'a::ring. [| a dvd 1; b dvd 1 |] ==> a * b dvd 1"; -by (Clarify_tac 1); -by (res_inst_tac [("x", "k * ka")] exI 1); -by (Asm_full_simp_tac 1); -qed "unit_mult"; - -Goal "!!a::'a::ring. a dvd 1 ==> a^n dvd 1"; -by (induct_tac "n" 1); -by (Simp_tac 1); -by (asm_simp_tac (simpset() addsimps [unit_mult]) 1); -qed "unit_power"; - -Goalw [dvd_def] - "!! a::'a::ring. [| a dvd b; a dvd c |] ==> a dvd b + c"; -by (Clarify_tac 1); -by (res_inst_tac [("x", "k + ka")] exI 1); -by (simp_tac (simpset() addsimps [r_distr]) 1); -qed "dvd_add_right"; - -Goalw [dvd_def] - "!! a::'a::ring. a dvd b ==> a dvd -b"; -by (Clarify_tac 1); -by (res_inst_tac [("x", "-k")] exI 1); -by (simp_tac (simpset() addsimps [r_minus]) 1); -qed "dvd_uminus_right"; - -Goalw [dvd_def] - "!! a::'a::ring. a dvd b ==> a dvd c*b"; -by (Clarify_tac 1); -by (res_inst_tac [("x", "c * k")] exI 1); -by (Simp_tac 1); -qed "dvd_l_mult_right"; - -Goalw [dvd_def] - "!! a::'a::ring. a dvd b ==> a dvd b*c"; -by (Clarify_tac 1); -by (res_inst_tac [("x", "k * c")] exI 1); -by (Simp_tac 1); -qed "dvd_r_mult_right"; - -Addsimps [dvd_add_right, dvd_uminus_right, dvd_l_mult_right, dvd_r_mult_right]; - -(* Inverse of multiplication *) - -section "inverse"; - -Goal "!! a::'a::ring. [| a * x = 1; a * y = 1 |] ==> x = y"; -by (res_inst_tac [("a", "(a*y)*x"), ("b", "y*(a*x)")] box_equals 1); -by (Simp_tac 1); -by Auto_tac; -qed "inverse_unique"; - -Goal "!! a::'a::ring. a dvd 1 ==> a * inverse a = 1"; -by (asm_full_simp_tac (simpset () addsimps [inverse_def, dvd_def] - delsimprocs [ring_simproc]) 1); -by (Clarify_tac 1); -by (rtac theI 1); -by (atac 1); -by (rtac inverse_unique 1); -by (atac 1); -by (atac 1); -qed "r_inverse_ring"; - -Goal "!! a::'a::ring. a dvd 1 ==> inverse a * a= 1"; -by (asm_simp_tac (simpset() addsimps [r_inverse_ring]) 1); -qed "l_inverse_ring"; - -(* Integral domain *) - -(* -section "Integral domains"; - -Goal "0 ~= (1::'a::domain)"; -by (rtac not_sym 1); -by (rtac one_not_zero 1); -qed "zero_not_one"; - -Goal "!! a::'a::domain. a dvd 1 ==> a ~= 0"; -by (auto_tac (claset() addDs [dvd_zero_left], - simpset() addsimps [one_not_zero] )); -qed "unit_imp_nonzero"; - -Goal "[| a * b = 0; a ~= 0 |] ==> (b::'a::domain) = 0"; -by (dtac integral 1); -by (Fast_tac 1); -qed "r_integral"; - -Goal "[| a * b = 0; b ~= 0 |] ==> (a::'a::domain) = 0"; -by (dtac integral 1); -by (Fast_tac 1); -qed "l_integral"; - -Goal "!! a::'a::domain. [| a ~= 0; b ~= 0 |] ==> a * b ~= 0"; -by (blast_tac (claset() addIs [l_integral]) 1); -qed "not_integral"; - -Addsimps [not_integral, one_not_zero, zero_not_one]; - -Goal "!! a::'a::domain. [| a * x = x; x ~= 0 |] ==> a = 1"; -by (res_inst_tac [("a", "- 1")] a_lcancel 1); -by (Simp_tac 1); -by (rtac l_integral 1); -by (assume_tac 2); -by (asm_simp_tac (simpset() addsimps [l_distr, l_minus]) 1); -qed "l_one_integral"; - -Goal "!! a::'a::domain. [| x * a = x; x ~= 0 |] ==> a = 1"; -by (res_inst_tac [("a", "- 1")] a_rcancel 1); -by (Simp_tac 1); -by (rtac r_integral 1); -by (assume_tac 2); -by (asm_simp_tac (simpset() addsimps [r_distr, r_minus]) 1); -qed "r_one_integral"; - -(* cancellation laws for multiplication *) - -Goal "!! a::'a::domain. [| a ~= 0; a * b = a * c |] ==> b = c"; -by (rtac diff_zero_imp_eq 1); -by (dtac eq_imp_diff_zero 1); -by (full_simp_tac (simpset() addsimps [r_minus RS sym, r_distr RS sym]) 1); -by (fast_tac (claset() addIs [l_integral]) 1); -qed "m_lcancel"; - -Goal "!! a::'a::domain. [| a ~= 0; b * a = c * a |] ==> b = c"; -by (rtac m_lcancel 1); -by (assume_tac 1); -by (Asm_full_simp_tac 1); -qed "m_rcancel"; - -Goal "!! a::'a::domain. a ~= 0 ==> (a * b = a * c) = (b = c)"; -by (auto_tac (claset() addDs [m_lcancel], simpset())); -qed "m_lcancel_eq"; - -Goal "!! a::'a::domain. a ~= 0 ==> (b * a = c * a) = (b = c)"; -by (asm_simp_tac (simpset() addsimps [m_lcancel_eq, m_comm]) 1); -qed "m_rcancel_eq"; - -Addsimps [m_lcancel_eq, m_rcancel_eq]; -*) - -(* Fields *) - -section "Fields"; - -Goal "!! a::'a::field. (a dvd 1) = (a ~= 0)"; -by (auto_tac (claset() addDs [thm "field_ax", dvd_zero_left], - simpset() addsimps [thm "field_one_not_zero"])); -qed "field_unit"; - -(* required for instantiation of field < domain in file Field.thy *) - -Addsimps [field_unit]; - -val field_one_not_zero = thm "field_one_not_zero"; - -Goal "!! a::'a::field. a ~= 0 ==> a * inverse a = 1"; -by (asm_full_simp_tac (simpset() addsimps [r_inverse_ring]) 1); -qed "r_inverse"; - -Goal "!! a::'a::field. a ~= 0 ==> inverse a * a= 1"; -by (asm_full_simp_tac (simpset() addsimps [l_inverse_ring]) 1); -qed "l_inverse"; - -Addsimps [l_inverse, r_inverse]; - -(* fields are integral domains *) - -Goal "!! a::'a::field. a * b = 0 ==> a = 0 | b = 0"; -by (Step_tac 1); -by (res_inst_tac [("a", "(a*b)*inverse b")] box_equals 1); -by (rtac refl 3); -by (Simp_tac 2); -by Auto_tac; -qed "field_integral"; - -(* fields are factorial domains *) - -Goalw [thm "prime_def", thm "irred_def"] - "!! a::'a::field. irred a ==> prime a"; -by (blast_tac (claset() addIs [thm "field_ax"]) 1); -qed "field_fact_prime"; diff -r 6e070b33e72b -r 0e0ea63fe768 src/HOL/Algebra/abstract/Ring.thy --- a/src/HOL/Algebra/abstract/Ring.thy Thu Aug 03 14:53:57 2006 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,234 +0,0 @@ -(* - Title: The algebraic hierarchy of rings as axiomatic classes - Id: $Id$ - Author: Clemens Ballarin, started 9 December 1996 - Copyright: Clemens Ballarin -*) - -header {* The algebraic hierarchy of rings as axiomatic classes *} - -theory Ring imports Main -uses ("order.ML") begin - -section {* Constants *} - -text {* Most constants are already declared by HOL. *} - -consts - assoc :: "['a::times, 'a] => bool" (infixl 50) - irred :: "'a::{zero, one, times} => bool" - prime :: "'a::{zero, one, times} => bool" - -section {* Axioms *} - -subsection {* Ring axioms *} - -axclass ring < zero, one, plus, minus, times, inverse, power - - a_assoc: "(a + b) + c = a + (b + c)" - l_zero: "0 + a = a" - l_neg: "(-a) + a = 0" - a_comm: "a + b = b + a" - - m_assoc: "(a * b) * c = a * (b * c)" - l_one: "1 * a = a" - - l_distr: "(a + b) * c = a * c + b * c" - - m_comm: "a * b = b * a" - - -- {* Definition of derived operations *} - - minus_def: "a - b = a + (-b)" - inverse_def: "inverse a = (if a dvd 1 then THE x. a*x = 1 else 0)" - divide_def: "a / b = a * inverse b" - power_def: "a ^ n = nat_rec 1 (%u b. b * a) n" - -defs - assoc_def: "a assoc b == a dvd b & b dvd a" - irred_def: "irred a == a ~= 0 & ~ a dvd 1 - & (ALL d. d dvd a --> d dvd 1 | a dvd d)" - prime_def: "prime p == p ~= 0 & ~ p dvd 1 - & (ALL a b. p dvd (a*b) --> p dvd a | p dvd b)" - -subsection {* Integral domains *} - -axclass - "domain" < ring - - one_not_zero: "1 ~= 0" - integral: "a * b = 0 ==> a = 0 | b = 0" - -subsection {* Factorial domains *} - -axclass - factorial < "domain" - -(* - Proper definition using divisor chain condition currently not supported. - factorial_divisor: "wf {(a, b). a dvd b & ~ (b dvd a)}" -*) - factorial_divisor: "True" - factorial_prime: "irred a ==> prime a" - -subsection {* Euclidean domains *} - -(* -axclass - euclidean < "domain" - - euclidean_ax: "b ~= 0 ==> Ex (% (q, r, e_size::('a::ringS)=>nat). - a = b * q + r & e_size r < e_size b)" - - Nothing has been proved about Euclidean domains, yet. - Design question: - Fix quo, rem and e_size as constants that are axiomatised with - euclidean_ax? - - advantage: more pragmatic and easier to use - - disadvantage: for every type, one definition of quo and rem will - be fixed, users may want to use differing ones; - also, it seems not possible to prove that fields are euclidean - domains, because that would require generic (type-independent) - definitions of quo and rem. -*) - -subsection {* Fields *} - -axclass - field < ring - - field_one_not_zero: "1 ~= 0" - (* Avoid a common superclass as the first thing we will - prove about fields is that they are domains. *) - field_ax: "a ~= 0 ==> a dvd 1" - -section {* Basic facts *} - -subsection {* Normaliser for rings *} - -use "order.ML" - -method_setup ring = - {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (full_simp_tac ring_ss)) *} - {* computes distributive normal form in rings *} - - -subsection {* Rings and the summation operator *} - -(* Basic facts --- move to HOL!!! *) - -(* needed because natsum_cong (below) disables atMost_0 *) -lemma natsum_0 [simp]: "setsum f {..(0::nat)} = (f 0::'a::comm_monoid_add)" -by simp -(* -lemma natsum_Suc [simp]: - "setsum f {..Suc n} = (f (Suc n) + setsum f {..n}::'a::comm_monoid_add)" -by (simp add: atMost_Suc) -*) -lemma natsum_Suc2: - "setsum f {..Suc n} = (f 0::'a::comm_monoid_add) + (setsum (%i. f (Suc i)) {..n})" -proof (induct n) - case 0 show ?case by simp -next - case Suc thus ?case by (simp add: semigroup_add_class.add_assoc) -qed - -lemma natsum_cong [cong]: - "!!k. [| j = k; !!i::nat. i <= k ==> f i = (g i::'a::comm_monoid_add) |] ==> - setsum f {..j} = setsum g {..k}" -by (induct j) auto - -lemma natsum_zero [simp]: "setsum (%i. 0) {..n::nat} = (0::'a::comm_monoid_add)" -by (induct n) simp_all - -lemma natsum_add [simp]: - "!!f::nat=>'a::comm_monoid_add. - setsum (%i. f i + g i) {..n::nat} = setsum f {..n} + setsum g {..n}" -by (induct n) (simp_all add: add_ac) - -(* Facts specific to rings *) - -instance ring < comm_monoid_add -proof - fix x y z - show "(x::'a::ring) + y = y + x" by (rule a_comm) - show "((x::'a::ring) + y) + z = x + (y + z)" by (rule a_assoc) - show "0 + (x::'a::ring) = x" by (rule l_zero) -qed - -ML {* - local - val lhss = - ["t + u::'a::ring", - "t - u::'a::ring", - "t * u::'a::ring", - "- t::'a::ring"]; - fun proc ss t = - let val rew = Goal.prove (Simplifier.the_context ss) [] [] - (HOLogic.mk_Trueprop - (HOLogic.mk_eq (t, Var (("x", Term.maxidx_of_term t + 1), fastype_of t)))) - (fn _ => simp_tac (Simplifier.inherit_context ss ring_ss) 1) - |> mk_meta_eq; - val (t', u) = Logic.dest_equals (Thm.prop_of rew); - in if t' aconv u - then NONE - else SOME rew - end; - in - val ring_simproc = Simplifier.simproc (the_context ()) "ring" lhss (K proc); - end; -*} - -ML_setup {* Addsimprocs [ring_simproc] *} - -lemma natsum_ldistr: - "!!a::'a::ring. setsum f {..n::nat} * a = setsum (%i. f i * a) {..n}" -by (induct n) simp_all - -lemma natsum_rdistr: - "!!a::'a::ring. a * setsum f {..n::nat} = setsum (%i. a * f i) {..n}" -by (induct n) simp_all - -subsection {* Integral Domains *} - -declare one_not_zero [simp] - -lemma zero_not_one [simp]: - "0 ~= (1::'a::domain)" -by (rule not_sym) simp - -lemma integral_iff: (* not by default a simp rule! *) - "(a * b = (0::'a::domain)) = (a = 0 | b = 0)" -proof - assume "a * b = 0" then show "a = 0 | b = 0" by (simp add: integral) -next - assume "a = 0 | b = 0" then show "a * b = 0" by auto -qed - -(* -lemma "(a::'a::ring) - (a - b) = b" apply simp - simproc seems to fail on this example (fixed with new term order) -*) -(* -lemma bug: "(b::'a::ring) - (b - a) = a" by simp - simproc for rings cannot prove "(a::'a::ring) - (a - b) = b" -*) -lemma m_lcancel: - assumes prem: "(a::'a::domain) ~= 0" shows conc: "(a * b = a * c) = (b = c)" -proof - assume eq: "a * b = a * c" - then have "a * (b - c) = 0" by simp - then have "a = 0 | (b - c) = 0" by (simp only: integral_iff) - with prem have "b - c = 0" by auto - then have "b = b - (b - c)" by simp - also have "b - (b - c) = c" by simp - finally show "b = c" . -next - assume "b = c" then show "a * b = a * c" by simp -qed - -lemma m_rcancel: - "(a::'a::domain) ~= 0 ==> (b * a = c * a) = (b = c)" -by (simp add: m_lcancel) - -end diff -r 6e070b33e72b -r 0e0ea63fe768 src/HOL/Algebra/abstract/Ring2.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Algebra/abstract/Ring2.ML Thu Aug 03 14:57:26 2006 +0200 @@ -0,0 +1,404 @@ +(* + Abstract class ring (commutative, with 1) + $Id$ + Author: Clemens Ballarin, started 9 December 1996 +*) + +(* +val a_assoc = thm "semigroup_add.add_assoc"; +val l_zero = thm "comm_monoid_add.add_0"; +val a_comm = thm "ab_semigroup_add.add_commute"; + +section "Rings"; + +fun make_left_commute assoc commute s = + [rtac (commute RS trans) 1, rtac (assoc RS trans) 1, + rtac (commute RS arg_cong) 1]; + +(* addition *) + +qed_goal "a_lcomm" Ring2.thy "!!a::'a::ring. a+(b+c) = b+(a+c)" + (make_left_commute a_assoc a_comm); + +val a_ac = [a_assoc, a_comm, a_lcomm]; + +Goal "!!a::'a::ring. a + 0 = a"; +by (rtac (a_comm RS trans) 1); +by (rtac l_zero 1); +qed "r_zero"; + +Goal "!!a::'a::ring. a + (-a) = 0"; +by (rtac (a_comm RS trans) 1); +by (rtac l_neg 1); +qed "r_neg"; + +Goal "!! a::'a::ring. a + b = a + c ==> b = c"; +by (rtac box_equals 1); +by (rtac l_zero 2); +by (rtac l_zero 2); +by (res_inst_tac [("a1", "a")] (l_neg RS subst) 1); +by (asm_simp_tac (simpset() addsimps [a_assoc]) 1); +qed "a_lcancel"; + +Goal "!! a::'a::ring. b + a = c + a ==> b = c"; +by (rtac a_lcancel 1); +by (asm_simp_tac (simpset() addsimps a_ac) 1); +qed "a_rcancel"; + +Goal "!! a::'a::ring. (a + b = a + c) = (b = c)"; +by (auto_tac (claset() addSDs [a_lcancel], simpset())); +qed "a_lcancel_eq"; + +Goal "!! a::'a::ring. (b + a = c + a) = (b = c)"; +by (simp_tac (simpset() addsimps [a_lcancel_eq, a_comm]) 1); +qed "a_rcancel_eq"; + +Addsimps [a_lcancel_eq, a_rcancel_eq]; + +Goal "!!a::'a::ring. -(-a) = a"; +by (rtac a_lcancel 1); +by (rtac (r_neg RS trans) 1); +by (rtac (l_neg RS sym) 1); +qed "minus_minus"; + +Goal "- 0 = (0::'a::ring)"; +by (rtac a_lcancel 1); +by (rtac (r_neg RS trans) 1); +by (rtac (l_zero RS sym) 1); +qed "minus0"; + +Goal "!!a::'a::ring. -(a + b) = (-a) + (-b)"; +by (res_inst_tac [("a", "a+b")] a_lcancel 1); +by (simp_tac (simpset() addsimps ([r_neg, l_neg, l_zero]@a_ac)) 1); +qed "minus_add"; + +(* multiplication *) + +qed_goal "m_lcomm" Ring2.thy "!!a::'a::ring. a*(b*c) = b*(a*c)" + (make_left_commute m_assoc m_comm); + +val m_ac = [m_assoc, m_comm, m_lcomm]; + +Goal "!!a::'a::ring. a * 1 = a"; +by (rtac (m_comm RS trans) 1); +by (rtac l_one 1); +qed "r_one"; + +(* distributive and derived *) + +Goal "!!a::'a::ring. a * (b + c) = a * b + a * c"; +by (rtac (m_comm RS trans) 1); +by (rtac (l_distr RS trans) 1); +by (simp_tac (simpset() addsimps [m_comm]) 1); +qed "r_distr"; + +val m_distr = m_ac @ [l_distr, r_distr]; + +(* the following two proofs can be found in + Jacobson, Basic Algebra I, pp. 88-89 *) + +Goal "!!a::'a::ring. 0 * a = 0"; +by (rtac a_lcancel 1); +by (rtac (l_distr RS sym RS trans) 1); +by (simp_tac (simpset() addsimps [r_zero]) 1); +qed "l_null"; + +Goal "!!a::'a::ring. a * 0 = 0"; +by (rtac (m_comm RS trans) 1); +by (rtac l_null 1); +qed "r_null"; + +Goal "!!a::'a::ring. (-a) * b = - (a * b)"; +by (rtac a_lcancel 1); +by (rtac (r_neg RS sym RSN (2, trans)) 1); +by (rtac (l_distr RS sym RS trans) 1); +by (simp_tac (simpset() addsimps [l_null, r_neg]) 1); +qed "l_minus"; + +Goal "!!a::'a::ring. a * (-b) = - (a * b)"; +by (rtac a_lcancel 1); +by (rtac (r_neg RS sym RSN (2, trans)) 1); +by (rtac (r_distr RS sym RS trans) 1); +by (simp_tac (simpset() addsimps [r_null, r_neg]) 1); +qed "r_minus"; + +val m_minus = [l_minus, r_minus]; + +Addsimps [l_zero, r_zero, l_neg, r_neg, minus_minus, minus0, + l_one, r_one, l_null, r_null]; + +(* further rules *) + +Goal "!!a::'a::ring. -a = 0 ==> a = 0"; +by (res_inst_tac [("t", "a")] (minus_minus RS subst) 1); +by (Asm_simp_tac 1); +qed "uminus_monom"; + +Goal "!!a::'a::ring. a ~= 0 ==> -a ~= 0"; +by (blast_tac (claset() addIs [uminus_monom]) 1); +qed "uminus_monom_neq"; + +Goal "!!a::'a::ring. a * b ~= 0 ==> a ~= 0"; +by Auto_tac; +qed "l_nullD"; + +Goal "!!a::'a::ring. a * b ~= 0 ==> b ~= 0"; +by Auto_tac; +qed "r_nullD"; + +(* reflection between a = b and a -- b = 0 *) + +Goal "!!a::'a::ring. a = b ==> a + (-b) = 0"; +by (Asm_simp_tac 1); +qed "eq_imp_diff_zero"; + +Goal "!!a::'a::ring. a + (-b) = 0 ==> a = b"; +by (res_inst_tac [("a", "-b")] a_rcancel 1); +by (Asm_simp_tac 1); +qed "diff_zero_imp_eq"; + +(* this could be a rewrite rule, but won't terminate + ==> make it a simproc? +Goal "!!a::'a::ring. (a = b) = (a -- b = 0)"; +*) + +*) + +(* Power *) + +Goal "!!a::'a::ring. a ^ 0 = 1"; +by (simp_tac (simpset() addsimps [power_def]) 1); +qed "power_0"; + +Goal "!!a::'a::ring. a ^ Suc n = a ^ n * a"; +by (simp_tac (simpset() addsimps [power_def]) 1); +qed "power_Suc"; + +Addsimps [power_0, power_Suc]; + +Goal "1 ^ n = (1::'a::ring)"; +by (induct_tac "n" 1); +by Auto_tac; +qed "power_one"; + +Goal "!!n. n ~= 0 ==> 0 ^ n = (0::'a::ring)"; +by (etac rev_mp 1); +by (induct_tac "n" 1); +by Auto_tac; +qed "power_zero"; + +Addsimps [power_zero, power_one]; + +Goal "!! a::'a::ring. a ^ m * a ^ n = a ^ (m + n)"; +by (induct_tac "m" 1); +by (Simp_tac 1); +by (Asm_simp_tac 1); +qed "power_mult"; + +(* Divisibility *) +section "Divisibility"; + +Goalw [dvd_def] "!! a::'a::ring. a dvd 0"; +by (res_inst_tac [("x", "0")] exI 1); +by (Simp_tac 1); +qed "dvd_zero_right"; + +Goalw [dvd_def] "!! a::'a::ring. 0 dvd a ==> a = 0"; +by Auto_tac; +qed "dvd_zero_left"; + +Goalw [dvd_def] "!! a::'a::ring. a dvd a"; +by (res_inst_tac [("x", "1")] exI 1); +by (Simp_tac 1); +qed "dvd_refl_ring"; + +Goalw [dvd_def] "!! a::'a::ring. [| a dvd b; b dvd c |] ==> a dvd c"; +by (Step_tac 1); +by (res_inst_tac [("x", "k * ka")] exI 1); +by (Asm_simp_tac 1); +qed "dvd_trans_ring"; + +Addsimps [dvd_zero_right, dvd_refl_ring]; + +Goalw [dvd_def] + "!!a::'a::ring. [| a dvd 1; b dvd 1 |] ==> a * b dvd 1"; +by (Clarify_tac 1); +by (res_inst_tac [("x", "k * ka")] exI 1); +by (Asm_full_simp_tac 1); +qed "unit_mult"; + +Goal "!!a::'a::ring. a dvd 1 ==> a^n dvd 1"; +by (induct_tac "n" 1); +by (Simp_tac 1); +by (asm_simp_tac (simpset() addsimps [unit_mult]) 1); +qed "unit_power"; + +Goalw [dvd_def] + "!! a::'a::ring. [| a dvd b; a dvd c |] ==> a dvd b + c"; +by (Clarify_tac 1); +by (res_inst_tac [("x", "k + ka")] exI 1); +by (simp_tac (simpset() addsimps [r_distr]) 1); +qed "dvd_add_right"; + +Goalw [dvd_def] + "!! a::'a::ring. a dvd b ==> a dvd -b"; +by (Clarify_tac 1); +by (res_inst_tac [("x", "-k")] exI 1); +by (simp_tac (simpset() addsimps [r_minus]) 1); +qed "dvd_uminus_right"; + +Goalw [dvd_def] + "!! a::'a::ring. a dvd b ==> a dvd c*b"; +by (Clarify_tac 1); +by (res_inst_tac [("x", "c * k")] exI 1); +by (Simp_tac 1); +qed "dvd_l_mult_right"; + +Goalw [dvd_def] + "!! a::'a::ring. a dvd b ==> a dvd b*c"; +by (Clarify_tac 1); +by (res_inst_tac [("x", "k * c")] exI 1); +by (Simp_tac 1); +qed "dvd_r_mult_right"; + +Addsimps [dvd_add_right, dvd_uminus_right, dvd_l_mult_right, dvd_r_mult_right]; + +(* Inverse of multiplication *) + +section "inverse"; + +Goal "!! a::'a::ring. [| a * x = 1; a * y = 1 |] ==> x = y"; +by (res_inst_tac [("a", "(a*y)*x"), ("b", "y*(a*x)")] box_equals 1); +by (Simp_tac 1); +by Auto_tac; +qed "inverse_unique"; + +Goal "!! a::'a::ring. a dvd 1 ==> a * inverse a = 1"; +by (asm_full_simp_tac (simpset () addsimps [inverse_def, dvd_def] + delsimprocs [ring_simproc]) 1); +by (Clarify_tac 1); +by (rtac theI 1); +by (atac 1); +by (rtac inverse_unique 1); +by (atac 1); +by (atac 1); +qed "r_inverse_ring"; + +Goal "!! a::'a::ring. a dvd 1 ==> inverse a * a= 1"; +by (asm_simp_tac (simpset() addsimps [r_inverse_ring]) 1); +qed "l_inverse_ring"; + +(* Integral domain *) + +(* +section "Integral domains"; + +Goal "0 ~= (1::'a::domain)"; +by (rtac not_sym 1); +by (rtac one_not_zero 1); +qed "zero_not_one"; + +Goal "!! a::'a::domain. a dvd 1 ==> a ~= 0"; +by (auto_tac (claset() addDs [dvd_zero_left], + simpset() addsimps [one_not_zero] )); +qed "unit_imp_nonzero"; + +Goal "[| a * b = 0; a ~= 0 |] ==> (b::'a::domain) = 0"; +by (dtac integral 1); +by (Fast_tac 1); +qed "r_integral"; + +Goal "[| a * b = 0; b ~= 0 |] ==> (a::'a::domain) = 0"; +by (dtac integral 1); +by (Fast_tac 1); +qed "l_integral"; + +Goal "!! a::'a::domain. [| a ~= 0; b ~= 0 |] ==> a * b ~= 0"; +by (blast_tac (claset() addIs [l_integral]) 1); +qed "not_integral"; + +Addsimps [not_integral, one_not_zero, zero_not_one]; + +Goal "!! a::'a::domain. [| a * x = x; x ~= 0 |] ==> a = 1"; +by (res_inst_tac [("a", "- 1")] a_lcancel 1); +by (Simp_tac 1); +by (rtac l_integral 1); +by (assume_tac 2); +by (asm_simp_tac (simpset() addsimps [l_distr, l_minus]) 1); +qed "l_one_integral"; + +Goal "!! a::'a::domain. [| x * a = x; x ~= 0 |] ==> a = 1"; +by (res_inst_tac [("a", "- 1")] a_rcancel 1); +by (Simp_tac 1); +by (rtac r_integral 1); +by (assume_tac 2); +by (asm_simp_tac (simpset() addsimps [r_distr, r_minus]) 1); +qed "r_one_integral"; + +(* cancellation laws for multiplication *) + +Goal "!! a::'a::domain. [| a ~= 0; a * b = a * c |] ==> b = c"; +by (rtac diff_zero_imp_eq 1); +by (dtac eq_imp_diff_zero 1); +by (full_simp_tac (simpset() addsimps [r_minus RS sym, r_distr RS sym]) 1); +by (fast_tac (claset() addIs [l_integral]) 1); +qed "m_lcancel"; + +Goal "!! a::'a::domain. [| a ~= 0; b * a = c * a |] ==> b = c"; +by (rtac m_lcancel 1); +by (assume_tac 1); +by (Asm_full_simp_tac 1); +qed "m_rcancel"; + +Goal "!! a::'a::domain. a ~= 0 ==> (a * b = a * c) = (b = c)"; +by (auto_tac (claset() addDs [m_lcancel], simpset())); +qed "m_lcancel_eq"; + +Goal "!! a::'a::domain. a ~= 0 ==> (b * a = c * a) = (b = c)"; +by (asm_simp_tac (simpset() addsimps [m_lcancel_eq, m_comm]) 1); +qed "m_rcancel_eq"; + +Addsimps [m_lcancel_eq, m_rcancel_eq]; +*) + +(* Fields *) + +section "Fields"; + +Goal "!! a::'a::field. (a dvd 1) = (a ~= 0)"; +by (auto_tac (claset() addDs [thm "field_ax", dvd_zero_left], + simpset() addsimps [thm "field_one_not_zero"])); +qed "field_unit"; + +(* required for instantiation of field < domain in file Field.thy *) + +Addsimps [field_unit]; + +val field_one_not_zero = thm "field_one_not_zero"; + +Goal "!! a::'a::field. a ~= 0 ==> a * inverse a = 1"; +by (asm_full_simp_tac (simpset() addsimps [r_inverse_ring]) 1); +qed "r_inverse"; + +Goal "!! a::'a::field. a ~= 0 ==> inverse a * a= 1"; +by (asm_full_simp_tac (simpset() addsimps [l_inverse_ring]) 1); +qed "l_inverse"; + +Addsimps [l_inverse, r_inverse]; + +(* fields are integral domains *) + +Goal "!! a::'a::field. a * b = 0 ==> a = 0 | b = 0"; +by (Step_tac 1); +by (res_inst_tac [("a", "(a*b)*inverse b")] box_equals 1); +by (rtac refl 3); +by (Simp_tac 2); +by Auto_tac; +qed "field_integral"; + +(* fields are factorial domains *) + +Goalw [thm "prime_def", thm "irred_def"] + "!! a::'a::field. irred a ==> prime a"; +by (blast_tac (claset() addIs [thm "field_ax"]) 1); +qed "field_fact_prime"; diff -r 6e070b33e72b -r 0e0ea63fe768 src/HOL/Algebra/abstract/Ring2.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Algebra/abstract/Ring2.thy Thu Aug 03 14:57:26 2006 +0200 @@ -0,0 +1,234 @@ +(* + Title: The algebraic hierarchy of rings as axiomatic classes + Id: $Id$ + Author: Clemens Ballarin, started 9 December 1996 + Copyright: Clemens Ballarin +*) + +header {* The algebraic hierarchy of rings as axiomatic classes *} + +theory Ring2 imports Main +uses ("order.ML") begin + +section {* Constants *} + +text {* Most constants are already declared by HOL. *} + +consts + assoc :: "['a::times, 'a] => bool" (infixl 50) + irred :: "'a::{zero, one, times} => bool" + prime :: "'a::{zero, one, times} => bool" + +section {* Axioms *} + +subsection {* Ring axioms *} + +axclass ring < zero, one, plus, minus, times, inverse, power + + a_assoc: "(a + b) + c = a + (b + c)" + l_zero: "0 + a = a" + l_neg: "(-a) + a = 0" + a_comm: "a + b = b + a" + + m_assoc: "(a * b) * c = a * (b * c)" + l_one: "1 * a = a" + + l_distr: "(a + b) * c = a * c + b * c" + + m_comm: "a * b = b * a" + + -- {* Definition of derived operations *} + + minus_def: "a - b = a + (-b)" + inverse_def: "inverse a = (if a dvd 1 then THE x. a*x = 1 else 0)" + divide_def: "a / b = a * inverse b" + power_def: "a ^ n = nat_rec 1 (%u b. b * a) n" + +defs + assoc_def: "a assoc b == a dvd b & b dvd a" + irred_def: "irred a == a ~= 0 & ~ a dvd 1 + & (ALL d. d dvd a --> d dvd 1 | a dvd d)" + prime_def: "prime p == p ~= 0 & ~ p dvd 1 + & (ALL a b. p dvd (a*b) --> p dvd a | p dvd b)" + +subsection {* Integral domains *} + +axclass + "domain" < ring + + one_not_zero: "1 ~= 0" + integral: "a * b = 0 ==> a = 0 | b = 0" + +subsection {* Factorial domains *} + +axclass + factorial < "domain" + +(* + Proper definition using divisor chain condition currently not supported. + factorial_divisor: "wf {(a, b). a dvd b & ~ (b dvd a)}" +*) + factorial_divisor: "True" + factorial_prime: "irred a ==> prime a" + +subsection {* Euclidean domains *} + +(* +axclass + euclidean < "domain" + + euclidean_ax: "b ~= 0 ==> Ex (% (q, r, e_size::('a::ringS)=>nat). + a = b * q + r & e_size r < e_size b)" + + Nothing has been proved about Euclidean domains, yet. + Design question: + Fix quo, rem and e_size as constants that are axiomatised with + euclidean_ax? + - advantage: more pragmatic and easier to use + - disadvantage: for every type, one definition of quo and rem will + be fixed, users may want to use differing ones; + also, it seems not possible to prove that fields are euclidean + domains, because that would require generic (type-independent) + definitions of quo and rem. +*) + +subsection {* Fields *} + +axclass + field < ring + + field_one_not_zero: "1 ~= 0" + (* Avoid a common superclass as the first thing we will + prove about fields is that they are domains. *) + field_ax: "a ~= 0 ==> a dvd 1" + +section {* Basic facts *} + +subsection {* Normaliser for rings *} + +use "order.ML" + +method_setup ring = + {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (full_simp_tac ring_ss)) *} + {* computes distributive normal form in rings *} + + +subsection {* Rings and the summation operator *} + +(* Basic facts --- move to HOL!!! *) + +(* needed because natsum_cong (below) disables atMost_0 *) +lemma natsum_0 [simp]: "setsum f {..(0::nat)} = (f 0::'a::comm_monoid_add)" +by simp +(* +lemma natsum_Suc [simp]: + "setsum f {..Suc n} = (f (Suc n) + setsum f {..n}::'a::comm_monoid_add)" +by (simp add: atMost_Suc) +*) +lemma natsum_Suc2: + "setsum f {..Suc n} = (f 0::'a::comm_monoid_add) + (setsum (%i. f (Suc i)) {..n})" +proof (induct n) + case 0 show ?case by simp +next + case Suc thus ?case by (simp add: semigroup_add_class.add_assoc) +qed + +lemma natsum_cong [cong]: + "!!k. [| j = k; !!i::nat. i <= k ==> f i = (g i::'a::comm_monoid_add) |] ==> + setsum f {..j} = setsum g {..k}" +by (induct j) auto + +lemma natsum_zero [simp]: "setsum (%i. 0) {..n::nat} = (0::'a::comm_monoid_add)" +by (induct n) simp_all + +lemma natsum_add [simp]: + "!!f::nat=>'a::comm_monoid_add. + setsum (%i. f i + g i) {..n::nat} = setsum f {..n} + setsum g {..n}" +by (induct n) (simp_all add: add_ac) + +(* Facts specific to rings *) + +instance ring < comm_monoid_add +proof + fix x y z + show "(x::'a::ring) + y = y + x" by (rule a_comm) + show "((x::'a::ring) + y) + z = x + (y + z)" by (rule a_assoc) + show "0 + (x::'a::ring) = x" by (rule l_zero) +qed + +ML {* + local + val lhss = + ["t + u::'a::ring", + "t - u::'a::ring", + "t * u::'a::ring", + "- t::'a::ring"]; + fun proc ss t = + let val rew = Goal.prove (Simplifier.the_context ss) [] [] + (HOLogic.mk_Trueprop + (HOLogic.mk_eq (t, Var (("x", Term.maxidx_of_term t + 1), fastype_of t)))) + (fn _ => simp_tac (Simplifier.inherit_context ss ring_ss) 1) + |> mk_meta_eq; + val (t', u) = Logic.dest_equals (Thm.prop_of rew); + in if t' aconv u + then NONE + else SOME rew + end; + in + val ring_simproc = Simplifier.simproc (the_context ()) "ring" lhss (K proc); + end; +*} + +ML_setup {* Addsimprocs [ring_simproc] *} + +lemma natsum_ldistr: + "!!a::'a::ring. setsum f {..n::nat} * a = setsum (%i. f i * a) {..n}" +by (induct n) simp_all + +lemma natsum_rdistr: + "!!a::'a::ring. a * setsum f {..n::nat} = setsum (%i. a * f i) {..n}" +by (induct n) simp_all + +subsection {* Integral Domains *} + +declare one_not_zero [simp] + +lemma zero_not_one [simp]: + "0 ~= (1::'a::domain)" +by (rule not_sym) simp + +lemma integral_iff: (* not by default a simp rule! *) + "(a * b = (0::'a::domain)) = (a = 0 | b = 0)" +proof + assume "a * b = 0" then show "a = 0 | b = 0" by (simp add: integral) +next + assume "a = 0 | b = 0" then show "a * b = 0" by auto +qed + +(* +lemma "(a::'a::ring) - (a - b) = b" apply simp + simproc seems to fail on this example (fixed with new term order) +*) +(* +lemma bug: "(b::'a::ring) - (b - a) = a" by simp + simproc for rings cannot prove "(a::'a::ring) - (a - b) = b" +*) +lemma m_lcancel: + assumes prem: "(a::'a::domain) ~= 0" shows conc: "(a * b = a * c) = (b = c)" +proof + assume eq: "a * b = a * c" + then have "a * (b - c) = 0" by simp + then have "a = 0 | (b - c) = 0" by (simp only: integral_iff) + with prem have "b - c = 0" by auto + then have "b = b - (b - c)" by simp + also have "b - (b - c) = c" by simp + finally show "b = c" . +next + assume "b = c" then show "a * b = a * c" by simp +qed + +lemma m_rcancel: + "(a::'a::domain) ~= 0 ==> (b * a = c * a) = (b = c)" +by (simp add: m_lcancel) + +end diff -r 6e070b33e72b -r 0e0ea63fe768 src/HOL/Algebra/abstract/RingHomo.thy --- a/src/HOL/Algebra/abstract/RingHomo.thy Thu Aug 03 14:53:57 2006 +0200 +++ b/src/HOL/Algebra/abstract/RingHomo.thy Thu Aug 03 14:57:26 2006 +0200 @@ -4,7 +4,7 @@ Author: Clemens Ballarin, started 15 April 1997 *) -theory RingHomo imports Ring begin +theory RingHomo imports Ring2 begin constdefs homo :: "('a::ring => 'b::ring) => bool" diff -r 6e070b33e72b -r 0e0ea63fe768 src/HOL/Algebra/document/root.tex --- a/src/HOL/Algebra/document/root.tex Thu Aug 03 14:53:57 2006 +0200 +++ b/src/HOL/Algebra/document/root.tex Thu Aug 03 14:57:26 2006 +0200 @@ -21,8 +21,8 @@ \title{The Isabelle/HOL Algebra Library} \author{ Clemens Ballarin \\ - Florian Kammu\"uller \\ - Lawrence C Paulson \\ + Florian Kammüller \\ + Lawrence C Paulson } \maketitle diff -r 6e070b33e72b -r 0e0ea63fe768 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Thu Aug 03 14:53:57 2006 +0200 +++ b/src/HOL/IsaMakefile Thu Aug 03 14:57:26 2006 +0200 @@ -381,22 +381,27 @@ $(LOG)/HOL-Algebra.gz: $(OUT)/HOL Algebra/ROOT.ML \ Library/Primes.thy Library/FuncSet.thy \ + Algebra/AbelCoset.thy \ Algebra/Bij.thy \ - Algebra/CRing.thy \ Algebra/Coset.thy \ Algebra/Exponent.thy \ Algebra/FiniteProduct.thy \ Algebra/Group.thy \ + Algebra/Ideal.thy \ Algebra/Lattice.thy \ Algebra/Module.thy \ + Algebra/Ring.thy \ Algebra/Sylow.thy \ Algebra/UnivPoly.thy \ + Algebra/IntRing.thy \ + Algebra/QuotRing.thy \ + Algebra/RingHom.thy \ Algebra/abstract/Abstract.thy \ Algebra/abstract/Factor.ML Algebra/abstract/Factor.thy \ Algebra/abstract/Field.thy \ - Algebra/abstract/Ideal.ML Algebra/abstract/Ideal.thy \ + Algebra/abstract/Ideal2.ML Algebra/abstract/Ideal2.thy \ Algebra/abstract/PID.thy \ - Algebra/abstract/Ring.ML Algebra/abstract/Ring.thy \ + Algebra/abstract/Ring2.ML Algebra/abstract/Ring2.thy \ Algebra/abstract/RingHomo.ML Algebra/abstract/RingHomo.thy\ Algebra/abstract/order.ML \ Algebra/document/root.tex \