162 apply(rule refl) |
162 apply(rule refl) |
163 done |
163 done |
164 |
164 |
165 lemma "PLUS a = PLUS a" |
165 lemma "PLUS a = PLUS a" |
166 apply(tactic {* procedure_tac @{context} @{thm test2} 1 *}) |
166 apply(tactic {* procedure_tac @{context} @{thm test2} 1 *}) |
|
167 apply(rule impI) |
167 apply(rule ballI) |
168 apply(rule ballI) |
168 apply(rule apply_rsp[OF Quotient_my_int plus_rsp]) |
169 apply(rule apply_rsp[OF Quotient_my_int plus_rsp]) |
169 apply(simp only: in_respects) |
170 apply(simp only: in_respects) |
170 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) |
171 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) |
171 apply(tactic {* clean_tac @{context} 1 *}) |
172 apply(tactic {* clean_tac @{context} 1 *}) |
269 |
271 |
270 (* What regularising does *) |
272 (* What regularising does *) |
271 (*========================*) |
273 (*========================*) |
272 |
274 |
273 (* 0. preliminary simplification step *) |
275 (* 0. preliminary simplification step *) |
274 thm ball_reg_eqv bex_reg_eqv babs_reg_eqv |
276 thm ball_reg_eqv bex_reg_eqv (* of no use: babs_reg_eqv *) |
275 ball_reg_eqv_range bex_reg_eqv_range |
277 ball_reg_eqv_range bex_reg_eqv_range |
276 (* 1. first two rtacs *) |
278 (* 1. first two rtacs *) |
277 thm ball_reg_right bex_reg_left |
279 thm ball_reg_right bex_reg_left |
278 (* 2. monos *) |
280 (* 2. monos *) |
279 (* 3. commutation rules *) |
281 (* 3. commutation rules *) |
301 apply - |
303 apply - |
302 apply(tactic {* equiv_tac @{context} 1 *}) |
304 apply(tactic {* equiv_tac @{context} 1 *}) |
303 apply(tactic {* equiv_tac @{context} 1 *})? |
305 apply(tactic {* equiv_tac @{context} 1 *})? |
304 oops |
306 oops |
305 |
307 |
306 |
308 lemma lam_tst3a: "(\<lambda>(y :: nat \<times> nat). y) = (\<lambda>(x :: nat \<times> nat). x)" |
307 lemma |
309 by auto |
308 "(\<lambda>y. y) = (\<lambda>x. x) \<longrightarrow> |
310 |
309 (op \<approx> ===> op \<approx>) (Babs (Respects op \<approx>) (\<lambda>y. y)) (Babs (Respects op \<approx>) (\<lambda>x. x))" |
311 lemma "(\<lambda>(y :: my_int). y) = (\<lambda>(x :: my_int). x)" |
310 apply(tactic {* simp_tac simpset 1 *}) |
312 apply(tactic {* procedure_tac @{context} @{thm lam_tst3a} 1 *}) |
|
313 defer |
|
314 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) |
|
315 apply(tactic {* clean_tac @{context} 1 *}) |
|
316 apply(subst babs_rsp) |
|
317 apply(tactic {* clean_tac @{context} 1 *}) |
|
318 apply(simp) |
|
319 apply(tactic {* regularize_tac @{context} 1*})? |
|
320 apply(subst babs_reg_eqv) |
|
321 apply(tactic {* equiv_tac @{context} 1*}) |
|
322 apply(subst babs_reg_eqv) |
|
323 apply(tactic {* equiv_tac @{context} 1*}) |
311 sorry |
324 sorry |
312 |
325 |
313 lemma lam_tst3: "(\<lambda>(y :: nat \<times> nat \<Rightarrow> nat \<times> nat). y) = (\<lambda>(x :: nat \<times> nat \<Rightarrow> nat \<times> nat). x)" |
326 lemma lam_tst3b: "(\<lambda>(y :: nat \<times> nat \<Rightarrow> nat \<times> nat). y) = (\<lambda>(x :: nat \<times> nat \<Rightarrow> nat \<times> nat). x)" |
314 by auto |
327 by auto |
315 |
328 |
316 lemma "(\<lambda>(y :: my_int \<Rightarrow> my_int). y) = (\<lambda>(x :: my_int \<Rightarrow> my_int). x)" |
329 lemma "(\<lambda>(y :: my_int => my_int). y) = (\<lambda>(x :: my_int => my_int). x)" |
317 apply(tactic {* procedure_tac @{context} @{thm lam_tst3} 1 *}) |
330 apply(tactic {* procedure_tac @{context} @{thm lam_tst3b} 1 *}) |
|
331 defer |
|
332 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) |
|
333 apply(tactic {* clean_tac @{context} 1 *}) |
|
334 apply(subst babs_rsp) |
|
335 apply(tactic {* clean_tac @{context} 1 *}) |
|
336 apply(simp) |
318 apply(tactic {* regularize_tac @{context} 1*})? |
337 apply(tactic {* regularize_tac @{context} 1*})? |
319 defer |
|
320 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) |
|
321 apply(tactic {* clean_tac @{context} 1 *}) |
|
322 sorry |
338 sorry |
323 |
339 |
324 end |
340 end |