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