src/HOL/Algebra/Bij.thy
 changeset 35416 d8d7d1b785af parent 33057 764547b68538 child 35848 5443079512ea
```     1.1 --- a/src/HOL/Algebra/Bij.thy	Wed Feb 24 11:55:52 2010 +0100
1.2 +++ b/src/HOL/Algebra/Bij.thy	Mon Mar 01 13:40:23 2010 +0100
1.3 @@ -1,5 +1,4 @@
1.4  (*  Title:      HOL/Algebra/Bij.thy
1.5 -    ID:         \$Id\$
1.6      Author:     Florian Kammueller, with new proofs by L C Paulson
1.7  *)
1.8
1.9 @@ -8,12 +7,11 @@
1.10
1.11  section {* Bijections of a Set, Permutation and Automorphism Groups *}
1.12
1.13 -constdefs
1.14 -  Bij :: "'a set \<Rightarrow> ('a \<Rightarrow> 'a) set"
1.15 +definition Bij :: "'a set \<Rightarrow> ('a \<Rightarrow> 'a) set" where
1.16      --{*Only extensional functions, since otherwise we get too many.*}
1.17    "Bij S \<equiv> extensional S \<inter> {f. bij_betw f S S}"
1.18
1.19 -  BijGroup :: "'a set \<Rightarrow> ('a \<Rightarrow> 'a) monoid"
1.20 +definition BijGroup :: "'a set \<Rightarrow> ('a \<Rightarrow> 'a) monoid" where
1.21    "BijGroup S \<equiv>
1.22      \<lparr>carrier = Bij S,
1.23       mult = \<lambda>g \<in> Bij S. \<lambda>f \<in> Bij S. compose S g f,
1.24 @@ -71,11 +69,10 @@
1.25  done
1.26
1.27
1.28 -constdefs
1.29 -  auto :: "('a, 'b) monoid_scheme \<Rightarrow> ('a \<Rightarrow> 'a) set"
1.30 +definition auto :: "('a, 'b) monoid_scheme \<Rightarrow> ('a \<Rightarrow> 'a) set" where
1.31    "auto G \<equiv> hom G G \<inter> Bij (carrier G)"
1.32
1.33 -  AutoGroup :: "('a, 'c) monoid_scheme \<Rightarrow> ('a \<Rightarrow> 'a) monoid"
1.34 +definition AutoGroup :: "('a, 'c) monoid_scheme \<Rightarrow> ('a \<Rightarrow> 'a) monoid" where
1.35    "AutoGroup G \<equiv> BijGroup (carrier G) \<lparr>carrier := auto G\<rparr>"
1.36
1.37  lemma (in group) id_in_auto: "(\<lambda>x \<in> carrier G. x) \<in> auto G"
```