equal
deleted
inserted
replaced
1 (* Title: HOL/AxClasses/Tutorial/BoolGroupInsts.thy |
|
2 ID: $Id$ |
|
3 Author: Markus Wenzel, TU Muenchen |
|
4 |
|
5 Define overloaded constants "<*>", "inverse", "1" on type "bool" |
|
6 appropriately, then prove that this forms a group. |
|
7 *) |
|
8 |
|
9 BoolGroupInsts = Group + |
|
10 |
|
11 (* bool as abelian group *) |
|
12 |
|
13 defs |
|
14 prod_bool_def "x <*> y == x ~= (y::bool)" |
|
15 inverse_bool_def "inverse x == x::bool" |
|
16 unit_bool_def "1 == False" |
|
17 |
|
18 instance |
|
19 bool :: agroup {| ALLGOALS (fast_tac HOL_cs) |} |
|
20 (*"instance" automatically uses above defs, |
|
21 the remaining goals are proven 'inline'*) |
|
22 |
|
23 end |
|