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 |
|