src/HOL/GroupTheory/Bij.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/GroupTheory/Bij.thy	Mon Jul 23 17:47:49 2001 +0200
@@ -0,0 +1,42 @@
+(*  Title:      HOL/GroupTheory/Coset
+    ID:         $Id$
+    Author:     Florian Kammueller, with new proofs by L C Paulson
+    Copyright   1998-2001  University of Cambridge
+
+Bijections of a set and the group of bijections
+	Sigma version with locales
+*)
+
+Bij = Group +
+
+constdefs
+  Bij :: "'a set => (('a => 'a)set)" 
+    "Bij S == {f. f \\<in> S \\<rightarrow> S & f`S = S & inj_on f S}"
+
+constdefs 
+BijGroup ::  "'a set => (('a => 'a) grouptype)"
+"BijGroup S == (| carrier = Bij S, 
+                  bin_op  = lam g: Bij S. lam f: Bij S. compose S g f,
+                  inverse = lam f: Bij S. lam x: S. (Inv S f) x, 
+                  unit    = lam x: S. x |)"
+
+locale bij = 
+  fixes 
+    S :: "'a set"
+    B :: "('a => 'a)set"
+    comp :: "[('a => 'a),('a => 'a)]=>('a => 'a)" (infixr "o''" 80)
+    inv'   :: "('a => 'a)=>('a => 'a)"              
+    e'   :: "('a => 'a)"
+  defines
+    B_def    "B == Bij S"
+    o'_def   "g o' f == compose S g f"
+    inv'_def   "inv' f == Inv S f"
+    e'_def   "e'  == (lam x: S. x)"
+
+locale bijgroup = bij +
+  fixes 
+    BG :: "('a => 'a) grouptype"
+  defines
+    BG_def "BG == BijGroup S"
+end
+