174 lemma "PLUS a = PLUS a" |
174 lemma "PLUS a = PLUS a" |
175 apply(tactic {* procedure_tac @{context} @{thm test2} 1 *}) |
175 apply(tactic {* procedure_tac @{context} @{thm test2} 1 *}) |
176 apply(rule ballI) |
176 apply(rule ballI) |
177 apply(rule apply_rsp[OF Quotient_my_int ho_plus_rsp]) |
177 apply(rule apply_rsp[OF Quotient_my_int ho_plus_rsp]) |
178 apply(simp only: in_respects) |
178 apply(simp only: in_respects) |
179 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
179 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) |
180 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
|
181 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
|
182 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
|
183 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
|
184 apply(rule quot_rel_rsp) |
|
185 apply(tactic {* quotient_tac @{context} 1 *}) |
|
186 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
|
187 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
|
188 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
|
189 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
|
190 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
|
191 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
|
192 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
|
193 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
|
194 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
|
195 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
|
196 apply(fold PLUS_def) |
|
197 apply(tactic {* clean_tac @{context} 1 *}) |
180 apply(tactic {* clean_tac @{context} 1 *}) |
198 done |
181 done |
199 |
182 |
200 lemma test3: "my_plus = my_plus" |
183 lemma test3: "my_plus = my_plus" |
201 apply(rule refl) |
184 apply(rule refl) |
202 done |
185 done |
203 |
186 |
204 lemma "PLUS = PLUS" |
187 lemma "PLUS = PLUS" |
205 apply(tactic {* procedure_tac @{context} @{thm test3} 1 *}) |
188 apply(tactic {* procedure_tac @{context} @{thm test3} 1 *}) |
206 apply(rule ho_plus_rsp) |
189 apply(rule ho_plus_rsp) |
207 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
190 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) |
208 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
|
209 apply(rule quot_rel_rsp) |
|
210 apply(tactic {* quotient_tac @{context} 1 *}) |
|
211 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
|
212 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
|
213 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
|
214 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
|
215 apply(tactic {* clean_tac @{context} 1 *}) |
191 apply(tactic {* clean_tac @{context} 1 *}) |
216 done |
192 done |
217 |
193 |
218 |
194 |
219 lemma "PLUS a b = PLUS b a" |
195 lemma "PLUS a b = PLUS b a" |
220 apply(tactic {* procedure_tac @{context} @{thm plus_sym_pre} 1 *}) |
196 apply(tactic {* procedure_tac @{context} @{thm plus_sym_pre} 1 *}) |
221 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
197 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
222 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
198 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) |
223 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
|
224 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
|
225 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
|
226 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
|
227 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
|
228 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
|
229 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
|
230 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
|
231 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
|
232 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
|
233 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
|
234 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
|
235 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
|
236 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
|
237 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
|
238 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
|
239 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
|
240 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
|
241 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
|
242 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
|
243 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
|
244 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
|
245 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
|
246 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
|
247 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
|
248 apply(tactic {* clean_tac @{context} 1 *}) |
199 apply(tactic {* clean_tac @{context} 1 *}) |
249 done |
200 done |
250 |
201 |
251 lemma plus_assoc_pre: |
202 lemma plus_assoc_pre: |
252 shows "my_plus (my_plus i j) k \<approx> my_plus i (my_plus j k)" |
203 shows "my_plus (my_plus i j) k \<approx> my_plus i (my_plus j k)" |