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)
```