isabelle: src/HOL/AxClasses/Group/GroupInsts.thy@a901bafe4578 (annotated)

1247 18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	1	(* Title: GroupInsts.thy
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	2	ID: $Id$
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	3	Author: Markus Wenzel, TU Muenchen
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	4
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	5	Some concrete instantiations: 'structures' and 'functors'.
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	6	*)
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	7
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	8	GroupInsts = GroupDefs +
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	9
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	10
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	11	(* bool *)
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	12
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	13	instance
2907 0e272e4c7cb2 inv -> inverse nipkow parents: 1247 diff changeset	14	bool :: semigroup (bool_assoc)
1247 18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	15	instance
2907 0e272e4c7cb2 inv -> inverse nipkow parents: 1247 diff changeset	16	bool :: monoid (bool_assoc, bool_left_unit, bool_right_unit)
1247 18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	17	instance
2907 0e272e4c7cb2 inv -> inverse nipkow parents: 1247 diff changeset	18	bool :: group (bool_left_unit, bool_left_inverse)
1247 18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	19	instance
2907 0e272e4c7cb2 inv -> inverse nipkow parents: 1247 diff changeset	20	bool :: agroup (bool_commut)
1247 18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	21
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	22
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	23	(* cartesian products *)
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	24
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	25	instance
2907 0e272e4c7cb2 inv -> inverse nipkow parents: 1247 diff changeset	26	"*" :: (semigroup, semigroup) semigroup (prod_assoc)
1247 18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	27	instance
2907 0e272e4c7cb2 inv -> inverse nipkow parents: 1247 diff changeset	28	"*" :: (monoid, monoid) monoid (prod_assoc, prod_left_unit, prod_right_unit)
1247 18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	29	instance
2907 0e272e4c7cb2 inv -> inverse nipkow parents: 1247 diff changeset	30	"*" :: (group, group) group (prod_left_unit, prod_left_inverse)
1247 18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	31	instance
2907 0e272e4c7cb2 inv -> inverse nipkow parents: 1247 diff changeset	32	"*" :: (agroup, agroup) agroup (prod_commut)
1247 18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	33
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	34
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	35	(* function spaces *)
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	36
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	37	instance
2907 0e272e4c7cb2 inv -> inverse nipkow parents: 1247 diff changeset	38	fun :: (term, semigroup) semigroup (fun_assoc)
1247 18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	39	instance
2907 0e272e4c7cb2 inv -> inverse nipkow parents: 1247 diff changeset	40	fun :: (term, monoid) monoid (fun_assoc, fun_left_unit, fun_right_unit)
1247 18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	41	instance
2907 0e272e4c7cb2 inv -> inverse nipkow parents: 1247 diff changeset	42	fun :: (term, group) group (fun_left_unit, fun_left_inverse)
1247 18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	43	instance
2907 0e272e4c7cb2 inv -> inverse nipkow parents: 1247 diff changeset	44	fun :: (term, agroup) agroup (fun_commut)
1247 18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	45
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	46	end

author	wenzelm
	Mon, 29 Nov 1999 15:52:49 +0100
changeset 8039	a901bafe4578
parent 2907	0e272e4c7cb2
permissions	-rw-r--r--