3167
|
1 |
|
|
2 |
- assoc;
|
|
3 |
val it =
|
|
4 |
"(?x::?'a::semigroup) <*> (?y::?'a::semigroup) <*> (?z::?'a::semigroup) =
|
|
5 |
?x <*> (?y <*> ?z)" : thm
|
|
6 |
- left_unit;
|
|
7 |
val it = "1 <*> (?x::?'a::group) = ?x" : thm
|
|
8 |
- left_inv;
|
|
9 |
val it = "inv (?x::?'a::group) <*> ?x = 1" : thm
|
|
10 |
- commut;
|
|
11 |
val it = "(?x::?'a::agroup) <*> (?y::?'a::agroup) = ?y <*> ?x" : thm
|
|
12 |
|
|
13 |
|
|
14 |
- right_unit;
|
|
15 |
val it = "(?x::?'a::group) <*> 1 = ?x" : thm
|
|
16 |
- right_inv;
|
|
17 |
val it = "(?x::?'a::group) <*> inv ?x = 1" : thm
|
|
18 |
- inv_product;
|
|
19 |
val it = "inv ((?x::?'a::group) <*> (?y::?'a::group)) = inv ?y <*> inv ?x"
|
|
20 |
: thm
|
|
21 |
- inv_inv;
|
|
22 |
val it = "inv (inv (?x::?'a::group)) = ?x" : thm
|
|
23 |
- ex1_inv;
|
|
24 |
val it = "ALL x::?'a::group. EX! y::?'a::group. y <*> x = 1" : thm
|
|
25 |
|
|
26 |
|
|
27 |
- groupI;
|
|
28 |
val it =
|
|
29 |
"[| OFCLASS(?'a::term, semigroup_class); !!x::?'a::term. 1 <*> x = x;
|
|
30 |
!!x::?'a::term. inv x <*> x = 1 |] ==> OFCLASS(?'a::term, group_class)"
|
|
31 |
: thm
|
|
32 |
|
|
33 |
|
|
34 |
- open AxClass;
|
|
35 |
- goal_arity Xor.thy ("bool", [], "agroup");
|
|
36 |
Level 0
|
|
37 |
OFCLASS(bool, agroup_class)
|
|
38 |
1. OFCLASS(bool, agroup_class)
|
|
39 |
val it = [] : thm list
|
|
40 |
- by (axclass_tac Xor.thy []);
|
|
41 |
Level 1
|
|
42 |
OFCLASS(bool, agroup_class)
|
|
43 |
1. !!(x::bool) (y::bool) z::bool. x <*> y <*> z = x <*> (y <*> z)
|
|
44 |
2. !!x::bool. 1 <*> x = x
|
|
45 |
3. !!x::bool. inv x <*> x = 1
|
|
46 |
4. !!(x::bool) y::bool. x <*> y = y <*> x
|
|
47 |
val it = () : unit
|
|
48 |
|
|
49 |
- by (rewrite_goals_tac [Xor.prod_bool_def, Xor.inv_bool_def, Xor.unit_bool_def]);
|
|
50 |
Level 2
|
|
51 |
OFCLASS(bool, agroup_class)
|
|
52 |
1. !!(x::bool) (y::bool) z::bool. x ~= y ~= z = (x ~= (y ~= z))
|
|
53 |
2. !!x::bool. False ~= x = x
|
|
54 |
3. !!x::bool. x ~= x = False
|
|
55 |
4. !!(x::bool) y::bool. x ~= y = (y ~= x)
|
|
56 |
val it = () : unit
|
|
57 |
- by (ALLGOALS (fast_tac HOL_cs));
|
|
58 |
Level 3
|
|
59 |
OFCLASS(bool, agroup_class)
|
|
60 |
No subgoals!
|
|
61 |
val it = () : unit
|
|
62 |
- qed "bool_in_agroup";
|
|
63 |
val bool_in_agroup = "OFCLASS(bool, agroup_class)" : thm
|
|
64 |
val it = () : unit
|
|
65 |
|
|
66 |
|
|
67 |
- Product.productI;
|
|
68 |
val it =
|
|
69 |
"OFCLASS(?'a::logic, term_class) ==> OFCLASS(?'a::logic, product_class)"
|
|
70 |
: thm
|