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