src/HOL/Algebra/Bij.thy
changeset 35848 5443079512ea
parent 35416 d8d7d1b785af
child 35849 b5522b51cb1e
     1.1 --- a/src/HOL/Algebra/Bij.thy	Sun Mar 21 15:57:40 2010 +0100
     1.2 +++ b/src/HOL/Algebra/Bij.thy	Sun Mar 21 16:51:37 2010 +0100
     1.3 @@ -7,12 +7,14 @@
     1.4  
     1.5  section {* Bijections of a Set, Permutation and Automorphism Groups *}
     1.6  
     1.7 -definition Bij :: "'a set \<Rightarrow> ('a \<Rightarrow> 'a) set" where
     1.8 +definition
     1.9 +  Bij :: "'a set \<Rightarrow> ('a \<Rightarrow> 'a) set"
    1.10      --{*Only extensional functions, since otherwise we get too many.*}
    1.11 -  "Bij S \<equiv> extensional S \<inter> {f. bij_betw f S S}"
    1.12 +   where "Bij S = extensional S \<inter> {f. bij_betw f S S}"
    1.13  
    1.14 -definition BijGroup :: "'a set \<Rightarrow> ('a \<Rightarrow> 'a) monoid" where
    1.15 -  "BijGroup S \<equiv>
    1.16 +definition
    1.17 +  BijGroup :: "'a set \<Rightarrow> ('a \<Rightarrow> 'a) monoid"
    1.18 +  where "BijGroup S =
    1.19      \<lparr>carrier = Bij S,
    1.20       mult = \<lambda>g \<in> Bij S. \<lambda>f \<in> Bij S. compose S g f,
    1.21       one = \<lambda>x \<in> S. x\<rparr>"
    1.22 @@ -69,11 +71,13 @@
    1.23  done
    1.24  
    1.25  
    1.26 -definition auto :: "('a, 'b) monoid_scheme \<Rightarrow> ('a \<Rightarrow> 'a) set" where
    1.27 -  "auto G \<equiv> hom G G \<inter> Bij (carrier G)"
    1.28 +definition
    1.29 +  auto :: "('a, 'b) monoid_scheme \<Rightarrow> ('a \<Rightarrow> 'a) set"
    1.30 +  where "auto G = hom G G \<inter> Bij (carrier G)"
    1.31  
    1.32 -definition AutoGroup :: "('a, 'c) monoid_scheme \<Rightarrow> ('a \<Rightarrow> 'a) monoid" where
    1.33 -  "AutoGroup G \<equiv> BijGroup (carrier G) \<lparr>carrier := auto G\<rparr>"
    1.34 +definition
    1.35 +  AutoGroup :: "('a, 'c) monoid_scheme \<Rightarrow> ('a \<Rightarrow> 'a) monoid"
    1.36 +  where "AutoGroup G = BijGroup (carrier G) \<lparr>carrier := auto G\<rparr>"
    1.37  
    1.38  lemma (in group) id_in_auto: "(\<lambda>x \<in> carrier G. x) \<in> auto G"
    1.39    by (simp add: auto_def hom_def restrictI group.axioms id_Bij)