9 |
9 |
10 fun sub r = standard (r RS subst); |
10 fun sub r = standard (r RS subst); |
11 fun ssub r = standard (r RS ssubst); |
11 fun ssub r = standard (r RS ssubst); |
12 |
12 |
13 |
13 |
14 goal thy "x * inv x = (1::'a::group)"; |
14 goal thy "x * inverse x = (1::'a::group)"; |
15 by (rtac (sub left_unit) 1); |
15 by (rtac (sub left_unit) 1); |
16 back(); |
16 back(); |
17 by (rtac (sub assoc) 1); |
17 by (rtac (sub assoc) 1); |
18 by (rtac (sub left_inv) 1); |
18 by (rtac (sub left_inverse) 1); |
19 back(); |
19 back(); |
20 back(); |
20 back(); |
21 by (rtac (ssub assoc) 1); |
21 by (rtac (ssub assoc) 1); |
22 back(); |
22 back(); |
23 by (rtac (ssub left_inv) 1); |
23 by (rtac (ssub left_inverse) 1); |
24 by (rtac (ssub assoc) 1); |
24 by (rtac (ssub assoc) 1); |
25 by (rtac (ssub left_unit) 1); |
25 by (rtac (ssub left_unit) 1); |
26 by (rtac (ssub left_inv) 1); |
26 by (rtac (ssub left_inverse) 1); |
27 by (rtac refl 1); |
27 by (rtac refl 1); |
28 qed "right_inv"; |
28 qed "right_inverse"; |
29 |
29 |
30 |
30 |
31 goal thy "x * 1 = (x::'a::group)"; |
31 goal thy "x * 1 = (x::'a::group)"; |
32 by (rtac (sub left_inv) 1); |
32 by (rtac (sub left_inverse) 1); |
33 by (rtac (sub assoc) 1); |
33 by (rtac (sub assoc) 1); |
34 by (rtac (ssub right_inv) 1); |
34 by (rtac (ssub right_inverse) 1); |
35 by (rtac (ssub left_unit) 1); |
35 by (rtac (ssub left_unit) 1); |
36 by (rtac refl 1); |
36 by (rtac refl 1); |
37 qed "right_unit"; |
37 qed "right_unit"; |
38 |
38 |
39 |
39 |
40 goal thy "e * x = x --> e = (1::'a::group)"; |
40 goal thy "e * x = x --> e = (1::'a::group)"; |
41 by (rtac impI 1); |
41 by (rtac impI 1); |
42 by (rtac (sub right_unit) 1); |
42 by (rtac (sub right_unit) 1); |
43 back(); |
43 back(); |
44 by (res_inst_tac [("x", "x")] (sub right_inv) 1); |
44 by (res_inst_tac [("x", "x")] (sub right_inverse) 1); |
45 by (rtac (sub assoc) 1); |
45 by (rtac (sub assoc) 1); |
46 by (rtac arg_cong 1); |
46 by (rtac arg_cong 1); |
47 back(); |
47 back(); |
48 by (assume_tac 1); |
48 by (assume_tac 1); |
49 qed "strong_one_unit"; |
49 qed "strong_one_unit"; |
72 goal thy "inj (op * (x::'a::group))"; |
72 goal thy "inj (op * (x::'a::group))"; |
73 by (rtac injI 1); |
73 by (rtac injI 1); |
74 by (rtac (sub left_unit) 1); |
74 by (rtac (sub left_unit) 1); |
75 back(); |
75 back(); |
76 by (rtac (sub left_unit) 1); |
76 by (rtac (sub left_unit) 1); |
77 by (res_inst_tac [("x", "x")] (sub left_inv) 1); |
77 by (res_inst_tac [("x", "x")] (sub left_inverse) 1); |
78 by (rtac (ssub assoc) 1); |
78 by (rtac (ssub assoc) 1); |
79 back(); |
79 back(); |
80 by (rtac (ssub assoc) 1); |
80 by (rtac (ssub assoc) 1); |
81 by (rtac arg_cong 1); |
81 by (rtac arg_cong 1); |
82 back(); |
82 back(); |
83 by (assume_tac 1); |
83 by (assume_tac 1); |
84 qed "inj_times"; |
84 qed "inj_times"; |
85 |
85 |
86 |
86 |
87 goal thy "y * x = 1 --> y = inv (x::'a::group)"; |
87 goal thy "y * x = 1 --> y = inverse (x::'a::group)"; |
88 by (rtac impI 1); |
88 by (rtac impI 1); |
89 by (rtac (sub right_unit) 1); |
89 by (rtac (sub right_unit) 1); |
90 back(); |
90 back(); |
91 back(); |
91 back(); |
92 by (rtac (sub right_unit) 1); |
92 by (rtac (sub right_unit) 1); |
93 by (res_inst_tac [("x", "x")] (sub right_inv) 1); |
93 by (res_inst_tac [("x", "x")] (sub right_inverse) 1); |
94 by (rtac (sub assoc) 1); |
94 by (rtac (sub assoc) 1); |
95 by (rtac (sub assoc) 1); |
95 by (rtac (sub assoc) 1); |
96 by (rtac arg_cong 1); |
96 by (rtac arg_cong 1); |
97 back(); |
97 back(); |
98 by (rtac (ssub left_inv) 1); |
98 by (rtac (ssub left_inverse) 1); |
99 by (assume_tac 1); |
99 by (assume_tac 1); |
100 qed "one_inv"; |
100 qed "one_inverse"; |
101 |
101 |
102 |
102 |
103 goal thy "ALL x. EX! y. y * x = (1::'a::group)"; |
103 goal thy "ALL x. EX! y. y * x = (1::'a::group)"; |
104 by (rtac allI 1); |
104 by (rtac allI 1); |
105 by (rtac ex1I 1); |
105 by (rtac ex1I 1); |
106 by (rtac left_inv 1); |
106 by (rtac left_inverse 1); |
107 by (rtac mp 1); |
107 by (rtac mp 1); |
108 by (rtac one_inv 1); |
108 by (rtac one_inverse 1); |
109 by (assume_tac 1); |
109 by (assume_tac 1); |
110 qed "ex1_inv"; |
110 qed "ex1_inverse"; |
111 |
111 |
112 |
112 |
113 goal thy "inv (x * y) = inv y * inv (x::'a::group)"; |
113 goal thy "inverse (x * y) = inverse y * inverse (x::'a::group)"; |
114 by (rtac sym 1); |
114 by (rtac sym 1); |
115 by (rtac mp 1); |
115 by (rtac mp 1); |
116 by (rtac one_inv 1); |
116 by (rtac one_inverse 1); |
117 by (rtac (ssub assoc) 1); |
117 by (rtac (ssub assoc) 1); |
118 by (rtac (sub assoc) 1); |
118 by (rtac (sub assoc) 1); |
119 back(); |
119 back(); |
120 by (rtac (ssub left_inv) 1); |
120 by (rtac (ssub left_inverse) 1); |
121 by (rtac (ssub left_unit) 1); |
121 by (rtac (ssub left_unit) 1); |
122 by (rtac (ssub left_inv) 1); |
122 by (rtac (ssub left_inverse) 1); |
123 by (rtac refl 1); |
123 by (rtac refl 1); |
124 qed "inv_times"; |
124 qed "inverse_times"; |
125 |
125 |
126 |
126 |
127 goal thy "inv (inv x) = (x::'a::group)"; |
127 goal thy "inverse (inverse x) = (x::'a::group)"; |
128 by (rtac sym 1); |
128 by (rtac sym 1); |
129 by (rtac (one_inv RS mp) 1); |
129 by (rtac (one_inverse RS mp) 1); |
130 by (rtac (ssub right_inv) 1); |
130 by (rtac (ssub right_inverse) 1); |
131 by (rtac refl 1); |
131 by (rtac refl 1); |
132 qed "inv_inv"; |
132 qed "inverse_inverse"; |