101 |
101 |
102 (* The following two equations are not used in any of the decision procedures, |
102 (* The following two equations are not used in any of the decision procedures, |
103 but are still very useful. They also demonstrate mk_group1_tac. |
103 but are still very useful. They also demonstrate mk_group1_tac. |
104 *) |
104 *) |
105 goal Group.thy "x-x = (zero::'a::add_group)"; |
105 goal Group.thy "x-x = (zero::'a::add_group)"; |
106 by(mk_group1_tac 1); |
106 by (mk_group1_tac 1); |
107 by(group1_tac 1); |
107 by (group1_tac 1); |
108 qed "minus_self_zero"; |
108 qed "minus_self_zero"; |
109 |
109 |
110 goal Group.thy "x-zero = (x::'a::add_group)"; |
110 goal Group.thy "x-zero = (x::'a::add_group)"; |
111 by(mk_group1_tac 1); |
111 by (mk_group1_tac 1); |
112 by(group1_tac 1); |
112 by (group1_tac 1); |
113 qed "minus_zero"; |
113 qed "minus_zero"; |
114 |
114 |
115 (*** Abelian Groups ***) |
115 (*** Abelian Groups ***) |
116 |
116 |
117 goal Group.thy "x+(y+z)=y+(x+z::'a::add_agroup)"; |
117 goal Group.thy "x+(y+z)=y+(x+z::'a::add_agroup)"; |
142 "x - (y - z) = (x + z) - (y::'a::add_agroup)" |
142 "x - (y - z) = (x + z) - (y::'a::add_agroup)" |
143 2. and for moving `-' over to the other side: |
143 2. and for moving `-' over to the other side: |
144 (x-y = z) = (x = z+y) and (x = y-z) = (x+z = y) |
144 (x-y = z) = (x = z+y) and (x = y-z) = (x+z = y) |
145 *) |
145 *) |
146 goal Group.thy "x + (y - z) = (x + y) - (z::'a::add_group)"; |
146 goal Group.thy "x + (y - z) = (x + y) - (z::'a::add_group)"; |
147 by(mk_group1_tac 1); |
147 by (mk_group1_tac 1); |
148 by(group1_tac 1); |
148 by (group1_tac 1); |
149 qed "plus_minusR"; |
149 qed "plus_minusR"; |
150 |
150 |
151 goal Group.thy "(x - y) + z = (x + z) - (y::'a::add_agroup)"; |
151 goal Group.thy "(x - y) + z = (x + z) - (y::'a::add_agroup)"; |
152 by(mk_group1_tac 1); |
152 by (mk_group1_tac 1); |
153 by(agroup1_tac 1); |
153 by (agroup1_tac 1); |
154 qed "plus_minusL"; |
154 qed "plus_minusL"; |
155 |
155 |
156 goal Group.thy "(x - y) - z = x - (y + (z::'a::add_agroup))"; |
156 goal Group.thy "(x - y) - z = x - (y + (z::'a::add_agroup))"; |
157 by(mk_group1_tac 1); |
157 by (mk_group1_tac 1); |
158 by(agroup1_tac 1); |
158 by (agroup1_tac 1); |
159 qed "minus_minusL"; |
159 qed "minus_minusL"; |
160 |
160 |
161 goal Group.thy "x - (y - z) = (x + z) - (y::'a::add_agroup)"; |
161 goal Group.thy "x - (y - z) = (x + z) - (y::'a::add_agroup)"; |
162 by(mk_group1_tac 1); |
162 by (mk_group1_tac 1); |
163 by(agroup1_tac 1); |
163 by (agroup1_tac 1); |
164 qed "minus_minusR"; |
164 qed "minus_minusR"; |
165 |
165 |
166 goal Group.thy "!!x::'a::add_group. (x-y = z) = (x = z+y)"; |
166 goal Group.thy "!!x::'a::add_group. (x-y = z) = (x = z+y)"; |
167 by(stac minus_inv 1); |
167 by (stac minus_inv 1); |
168 by(fast_tac (claset() addss (HOL_basic_ss addsimps group1_simps)) 1); |
168 by (fast_tac (claset() addss (HOL_basic_ss addsimps group1_simps)) 1); |
169 qed "minusL_iff"; |
169 qed "minusL_iff"; |
170 |
170 |
171 goal Group.thy "!!x::'a::add_group. (x = y-z) = (x+z = y)"; |
171 goal Group.thy "!!x::'a::add_group. (x = y-z) = (x+z = y)"; |
172 by(stac minus_inv 1); |
172 by (stac minus_inv 1); |
173 by(fast_tac (claset() addss (HOL_basic_ss addsimps group1_simps)) 1); |
173 by (fast_tac (claset() addss (HOL_basic_ss addsimps group1_simps)) 1); |
174 qed "minusR_iff"; |
174 qed "minusR_iff"; |
175 |
175 |
176 val agroup2_simps = |
176 val agroup2_simps = |
177 [zeroL,zeroR,plus_assoc,plus_commute,plus_commuteL, |
177 [zeroL,zeroR,plus_assoc,plus_commute,plus_commuteL, |
178 plus_minusR,plus_minusL,minus_minusL,minus_minusR,minusL_iff,minusR_iff]; |
178 plus_minusR,plus_minusL,minus_minusL,minus_minusR,minusL_iff,minusR_iff]; |