equal
deleted
inserted
replaced
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 Group.thy "x <*> inverse x = (1::'a::group)"; |
14 Goal "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_inverse) 1); |
18 by (rtac (sub left_inverse) 1); |
19 back(); |
19 back(); |
26 by (rtac (ssub left_inverse) 1); |
26 by (rtac (ssub left_inverse) 1); |
27 by (rtac refl 1); |
27 by (rtac refl 1); |
28 qed "right_inverse"; |
28 qed "right_inverse"; |
29 |
29 |
30 |
30 |
31 goal Group.thy "x <*> 1 = (x::'a::group)"; |
31 Goal "x <*> 1 = (x::'a::group)"; |
32 by (rtac (sub left_inverse) 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_inverse) 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 Group.thy "e <*> x = x --> e = (1::'a::group)"; |
40 Goal "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_inverse) 1); |
44 by (res_inst_tac [("x", "x")] (sub right_inverse) 1); |
45 by (rtac (sub assoc) 1); |
45 by (rtac (sub assoc) 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"; |
50 |
50 |
51 |
51 |
52 goal Group.thy "EX! e. ALL x. e <*> x = (x::'a::group)"; |
52 Goal "EX! e. ALL x. e <*> x = (x::'a::group)"; |
53 by (rtac ex1I 1); |
53 by (rtac ex1I 1); |
54 by (rtac allI 1); |
54 by (rtac allI 1); |
55 by (rtac left_unit 1); |
55 by (rtac left_unit 1); |
56 by (rtac mp 1); |
56 by (rtac mp 1); |
57 by (rtac strong_one_unit 1); |
57 by (rtac strong_one_unit 1); |
58 by (etac allE 1); |
58 by (etac allE 1); |
59 by (assume_tac 1); |
59 by (assume_tac 1); |
60 qed "ex1_unit"; |
60 qed "ex1_unit"; |
61 |
61 |
62 |
62 |
63 goal Group.thy "ALL x. EX! e. e <*> x = (x::'a::group)"; |
63 Goal "ALL x. EX! e. e <*> x = (x::'a::group)"; |
64 by (rtac allI 1); |
64 by (rtac allI 1); |
65 by (rtac ex1I 1); |
65 by (rtac ex1I 1); |
66 by (rtac left_unit 1); |
66 by (rtac left_unit 1); |
67 by (rtac (strong_one_unit RS mp) 1); |
67 by (rtac (strong_one_unit RS mp) 1); |
68 by (assume_tac 1); |
68 by (assume_tac 1); |
69 qed "ex1_unit'"; |
69 qed "ex1_unit'"; |
70 |
70 |
71 |
71 |
72 goal Group.thy "y <*> x = 1 --> y = inverse (x::'a::group)"; |
72 Goal "y <*> x = 1 --> y = inverse (x::'a::group)"; |
73 by (rtac impI 1); |
73 by (rtac impI 1); |
74 by (rtac (sub right_unit) 1); |
74 by (rtac (sub right_unit) 1); |
75 back(); |
75 back(); |
76 back(); |
76 back(); |
77 by (rtac (sub right_unit) 1); |
77 by (rtac (sub right_unit) 1); |
83 by (rtac (ssub left_inverse) 1); |
83 by (rtac (ssub left_inverse) 1); |
84 by (assume_tac 1); |
84 by (assume_tac 1); |
85 qed "one_inverse"; |
85 qed "one_inverse"; |
86 |
86 |
87 |
87 |
88 goal Group.thy "ALL x. EX! y. y <*> x = (1::'a::group)"; |
88 Goal "ALL x. EX! y. y <*> x = (1::'a::group)"; |
89 by (rtac allI 1); |
89 by (rtac allI 1); |
90 by (rtac ex1I 1); |
90 by (rtac ex1I 1); |
91 by (rtac left_inverse 1); |
91 by (rtac left_inverse 1); |
92 by (rtac mp 1); |
92 by (rtac mp 1); |
93 by (rtac one_inverse 1); |
93 by (rtac one_inverse 1); |
94 by (assume_tac 1); |
94 by (assume_tac 1); |
95 qed "ex1_inverse"; |
95 qed "ex1_inverse"; |
96 |
96 |
97 |
97 |
98 goal Group.thy "inverse (x <*> y) = inverse y <*> inverse (x::'a::group)"; |
98 Goal "inverse (x <*> y) = inverse y <*> inverse (x::'a::group)"; |
99 by (rtac sym 1); |
99 by (rtac sym 1); |
100 by (rtac mp 1); |
100 by (rtac mp 1); |
101 by (rtac one_inverse 1); |
101 by (rtac one_inverse 1); |
102 by (rtac (ssub assoc) 1); |
102 by (rtac (ssub assoc) 1); |
103 by (rtac (sub assoc) 1); |
103 by (rtac (sub assoc) 1); |
107 by (rtac (ssub left_inverse) 1); |
107 by (rtac (ssub left_inverse) 1); |
108 by (rtac refl 1); |
108 by (rtac refl 1); |
109 qed "inverse_product"; |
109 qed "inverse_product"; |
110 |
110 |
111 |
111 |
112 goal Group.thy "inverse (inverse x) = (x::'a::group)"; |
112 Goal "inverse (inverse x) = (x::'a::group)"; |
113 by (rtac sym 1); |
113 by (rtac sym 1); |
114 by (rtac (one_inverse RS mp) 1); |
114 by (rtac (one_inverse RS mp) 1); |
115 by (rtac (ssub right_inverse) 1); |
115 by (rtac (ssub right_inverse) 1); |
116 by (rtac refl 1); |
116 by (rtac refl 1); |
117 qed "inverse_inv"; |
117 qed "inverse_inv"; |