1247
|
1 |
(* bool *)
|
|
2 |
|
|
3 |
(*this is really overkill - should be rather proven 'inline'*)
|
|
4 |
|
5069
|
5 |
Goalw [times_bool_def] "(x * y) * z = x * (y * (z::bool))";
|
1899
|
6 |
by (Fast_tac 1);
|
1247
|
7 |
qed "bool_assoc";
|
|
8 |
|
5069
|
9 |
Goalw [times_bool_def, one_bool_def] "1 * x = (x::bool)";
|
1899
|
10 |
by (Fast_tac 1);
|
1247
|
11 |
qed "bool_left_unit";
|
|
12 |
|
5069
|
13 |
Goalw [times_bool_def, one_bool_def] "x * 1 = (x::bool)";
|
1899
|
14 |
by (Fast_tac 1);
|
1247
|
15 |
qed "bool_right_unit";
|
|
16 |
|
5069
|
17 |
Goalw [times_bool_def, inverse_bool_def, one_bool_def]
|
2907
|
18 |
"inverse(x) * x = (1::bool)";
|
1899
|
19 |
by (Fast_tac 1);
|
2907
|
20 |
qed "bool_left_inverse";
|
1247
|
21 |
|
5069
|
22 |
Goalw [times_bool_def] "x * y = (y * (x::bool))";
|
1899
|
23 |
by (Fast_tac 1);
|
1247
|
24 |
qed "bool_commut";
|
|
25 |
|
|
26 |
|
|
27 |
(* cartesian products *)
|
|
28 |
|
4091
|
29 |
val prod_ss = simpset_of Prod.thy;
|
1266
|
30 |
|
5069
|
31 |
Goalw [times_prod_def]
|
2907
|
32 |
"(x * y) * z = x * (y * (z::'a::semigroup*'b::semigroup))";
|
1247
|
33 |
by (simp_tac (prod_ss addsimps [assoc]) 1);
|
|
34 |
qed "prod_assoc";
|
|
35 |
|
5069
|
36 |
Goalw [times_prod_def, one_prod_def] "1 * x = (x::'a::monoid*'b::monoid)";
|
1247
|
37 |
by (simp_tac (prod_ss addsimps [Monoid.left_unit]) 1);
|
1465
|
38 |
by (rtac (surjective_pairing RS sym) 1);
|
1247
|
39 |
qed "prod_left_unit";
|
|
40 |
|
5069
|
41 |
Goalw [times_prod_def, one_prod_def] "x * 1 = (x::'a::monoid*'b::monoid)";
|
1247
|
42 |
by (simp_tac (prod_ss addsimps [Monoid.right_unit]) 1);
|
1465
|
43 |
by (rtac (surjective_pairing RS sym) 1);
|
1247
|
44 |
qed "prod_right_unit";
|
|
45 |
|
5069
|
46 |
Goalw [times_prod_def, inverse_prod_def, one_prod_def]
|
2907
|
47 |
"inverse x * x = (1::'a::group*'b::group)";
|
|
48 |
by (simp_tac (prod_ss addsimps [left_inverse]) 1);
|
|
49 |
qed "prod_left_inverse";
|
1247
|
50 |
|
5069
|
51 |
Goalw [times_prod_def] "x * y = y * (x::'a::agroup*'b::agroup)";
|
1247
|
52 |
by (simp_tac (prod_ss addsimps [commut]) 1);
|
|
53 |
qed "prod_commut";
|
|
54 |
|
|
55 |
|
|
56 |
(* function spaces *)
|
|
57 |
|
5069
|
58 |
Goalw [times_fun_def] "(x * y) * z = x * (y * (z::'a => 'b::semigroup))";
|
1247
|
59 |
by (stac expand_fun_eq 1);
|
1465
|
60 |
by (rtac allI 1);
|
|
61 |
by (rtac assoc 1);
|
1247
|
62 |
qed "fun_assoc";
|
|
63 |
|
5069
|
64 |
Goalw [times_fun_def, one_fun_def] "1 * x = (x::'a => 'b::monoid)";
|
1247
|
65 |
by (stac expand_fun_eq 1);
|
1465
|
66 |
by (rtac allI 1);
|
|
67 |
by (rtac Monoid.left_unit 1);
|
1247
|
68 |
qed "fun_left_unit";
|
|
69 |
|
5069
|
70 |
Goalw [times_fun_def, one_fun_def] "x * 1 = (x::'a => 'b::monoid)";
|
1247
|
71 |
by (stac expand_fun_eq 1);
|
1465
|
72 |
by (rtac allI 1);
|
|
73 |
by (rtac Monoid.right_unit 1);
|
1247
|
74 |
qed "fun_right_unit";
|
|
75 |
|
5069
|
76 |
Goalw [times_fun_def, inverse_fun_def, one_fun_def]
|
2907
|
77 |
"inverse x * x = (1::'a => 'b::group)";
|
1247
|
78 |
by (stac expand_fun_eq 1);
|
1465
|
79 |
by (rtac allI 1);
|
2907
|
80 |
by (rtac left_inverse 1);
|
|
81 |
qed "fun_left_inverse";
|
1247
|
82 |
|
5069
|
83 |
Goalw [times_fun_def] "x * y = y * (x::'a => 'b::agroup)";
|
1247
|
84 |
by (stac expand_fun_eq 1);
|
1465
|
85 |
by (rtac allI 1);
|
|
86 |
by (rtac commut 1);
|
1247
|
87 |
qed "fun_commut";
|