src/HOL/Algebra/AbelCoset.thy
 changeset 35848 5443079512ea parent 35847 19f1f7066917 child 35849 b5522b51cb1e
```     1.1 --- a/src/HOL/Algebra/AbelCoset.thy	Sun Mar 21 15:57:40 2010 +0100
1.2 +++ b/src/HOL/Algebra/AbelCoset.thy	Sun Mar 21 16:51:37 2010 +0100
1.3 @@ -19,37 +19,39 @@
1.4
1.5  definition
1.6    a_r_coset    :: "[_, 'a set, 'a] \<Rightarrow> 'a set"    (infixl "+>\<index>" 60)
1.7 -  where "a_r_coset G \<equiv> r_coset \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
1.8 +  where "a_r_coset G = r_coset \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
1.9
1.10  definition
1.11    a_l_coset    :: "[_, 'a, 'a set] \<Rightarrow> 'a set"    (infixl "<+\<index>" 60)
1.12 -  where "a_l_coset G \<equiv> l_coset \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
1.13 +  where "a_l_coset G = l_coset \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
1.14
1.15  definition
1.16    A_RCOSETS  :: "[_, 'a set] \<Rightarrow> ('a set)set"   ("a'_rcosets\<index> _" [81] 80)
1.17 -  where "A_RCOSETS G H \<equiv> RCOSETS \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> H"
1.18 +  where "A_RCOSETS G H = RCOSETS \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> H"
1.19
1.20  definition
1.21    set_add  :: "[_, 'a set ,'a set] \<Rightarrow> 'a set" (infixl "<+>\<index>" 60)
1.22 -  where "set_add G \<equiv> set_mult \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
1.23 +  where "set_add G = set_mult \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
1.24
1.25  definition
1.26    A_SET_INV :: "[_,'a set] \<Rightarrow> 'a set"  ("a'_set'_inv\<index> _" [81] 80)
1.27 -  where "A_SET_INV G H \<equiv> SET_INV \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> H"
1.28 +  where "A_SET_INV G H = SET_INV \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> H"
1.29
1.30  definition
1.31    a_r_congruent :: "[('a,'b)ring_scheme, 'a set] \<Rightarrow> ('a*'a)set"  ("racong\<index> _")
1.32 -  where "a_r_congruent G \<equiv> r_congruent \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
1.33 +  where "a_r_congruent G = r_congruent \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
1.34
1.35 -definition A_FactGroup :: "[('a,'b) ring_scheme, 'a set] \<Rightarrow> ('a set) monoid" (infixl "A'_Mod" 65) where
1.36 +definition
1.37 +  A_FactGroup :: "[('a,'b) ring_scheme, 'a set] \<Rightarrow> ('a set) monoid" (infixl "A'_Mod" 65)
1.38      --{*Actually defined for groups rather than monoids*}
1.39 -  "A_FactGroup G H \<equiv> FactGroup \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> H"
1.40 +  where "A_FactGroup G H = FactGroup \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> H"
1.41
1.42 -definition a_kernel :: "('a, 'm) ring_scheme \<Rightarrow> ('b, 'n) ring_scheme \<Rightarrow>
1.43 -             ('a \<Rightarrow> 'b) \<Rightarrow> 'a set" where
1.44 +definition
1.45 +  a_kernel :: "('a, 'm) ring_scheme \<Rightarrow> ('b, 'n) ring_scheme \<Rightarrow>  ('a \<Rightarrow> 'b) \<Rightarrow> 'a set"
1.46      --{*the kernel of a homomorphism (additive)*}
1.47 -  "a_kernel G H h \<equiv> kernel \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>
1.48 -                              \<lparr>carrier = carrier H, mult = add H, one = zero H\<rparr> h"
1.49 +  where "a_kernel G H h =
1.50 +    kernel \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>
1.51 +      \<lparr>carrier = carrier H, mult = add H, one = zero H\<rparr> h"
1.52
1.53  locale abelian_group_hom = G: abelian_group G + H: abelian_group H
1.54      for G (structure) and H (structure) +
1.55 @@ -527,7 +529,7 @@
1.56    a_kernel_def kernel_def
1.57
1.58  lemma a_kernel_def':
1.59 -  "a_kernel R S h \<equiv> {x \<in> carrier R. h x = \<zero>\<^bsub>S\<^esub>}"
1.60 +  "a_kernel R S h = {x \<in> carrier R. h x = \<zero>\<^bsub>S\<^esub>}"
1.61  by (rule a_kernel_def[unfolded kernel_def, simplified ring_record_simps])
1.62
1.63
```