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"