253 done |
253 done |
254 |
254 |
255 lemma lam_tst2: "(\<lambda>(y :: nat \<times> nat). y) = (\<lambda>(x :: nat \<times> nat). x)" |
255 lemma lam_tst2: "(\<lambda>(y :: nat \<times> nat). y) = (\<lambda>(x :: nat \<times> nat). x)" |
256 by simp |
256 by simp |
257 |
257 |
258 |
258 (* test about lifting identity equations *) |
259 lemma "(\<lambda>(y :: my_int). y) = (\<lambda>(x :: my_int). x)" |
259 |
260 apply(tactic {* procedure_tac @{context} @{thm lam_tst2} 1 *}) |
260 ML {* |
|
261 (* helper code from QuotMain *) |
|
262 val pat_ball = @{term "Ball (Respects (R1 ===> R2)) P"} |
|
263 val pat_bex = @{term "Bex (Respects (R1 ===> R2)) P"} |
|
264 val simproc = Simplifier.simproc_i @{theory} "" [pat_ball, pat_bex] (K (ball_bex_range_simproc)) |
|
265 val simpset = (mk_minimal_ss @{context}) |
|
266 addsimps @{thms ball_reg_eqv bex_reg_eqv babs_reg_eqv} |
|
267 addsimprocs [simproc] addSolver equiv_solver |
|
268 *} |
|
269 |
|
270 (* What regularising does *) |
|
271 (*========================*) |
|
272 |
|
273 (* 0. preliminary simplification step *) |
|
274 thm ball_reg_eqv bex_reg_eqv babs_reg_eqv |
|
275 ball_reg_eqv_range bex_reg_eqv_range |
|
276 (* 1. first two rtacs *) |
|
277 thm ball_reg_right bex_reg_left |
|
278 (* 2. monos *) |
|
279 (* 3. commutation rules *) |
|
280 thm ball_all_comm bex_ex_comm |
|
281 (* 4. then rel-equality *) |
|
282 thm eq_imp_rel |
|
283 (* 5. then simplification like 0 *) |
|
284 (* finally jump to 1 *) |
|
285 |
|
286 |
|
287 (* What cleaning does *) |
|
288 (*====================*) |
|
289 |
|
290 (* 1. conversion *) |
|
291 thm lambda_prs |
|
292 (* 2. simplification with *) |
|
293 thm all_prs ex_prs |
|
294 (* 3. Simplification with *) |
|
295 thm fun_map.simps id_simps Quotient_abs_rep Quotient_rel_rep |
|
296 (* 4. Test for refl *) |
|
297 |
|
298 lemma |
|
299 shows "equivp (op \<approx>)" |
|
300 and "equivp ((op \<approx>) ===> (op \<approx>))" |
|
301 apply - |
|
302 apply(tactic {* equiv_tac @{context} 1 *}) |
|
303 apply(tactic {* equiv_tac @{context} 1 *})? |
|
304 oops |
|
305 |
|
306 |
|
307 lemma |
|
308 "(\<lambda>y. y) = (\<lambda>x. x) \<longrightarrow> |
|
309 (op \<approx> ===> op \<approx>) (Babs (Respects op \<approx>) (\<lambda>y. y)) (Babs (Respects op \<approx>) (\<lambda>x. x))" |
|
310 apply(tactic {* simp_tac simpset 1 *}) |
|
311 sorry |
|
312 |
|
313 lemma lam_tst3: "(\<lambda>(y :: nat \<times> nat \<Rightarrow> nat \<times> nat). y) = (\<lambda>(x :: nat \<times> nat \<Rightarrow> nat \<times> nat). x)" |
|
314 by auto |
|
315 |
|
316 lemma "(\<lambda>(y :: my_int \<Rightarrow> my_int). y) = (\<lambda>(x :: my_int \<Rightarrow> my_int). x)" |
|
317 apply(tactic {* procedure_tac @{context} @{thm lam_tst3} 1 *}) |
|
318 apply(tactic {* regularize_tac @{context} 1*})? |
261 defer |
319 defer |
262 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) |
320 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) |
263 apply(tactic {* clean_tac @{context} 1 *}) |
321 apply(tactic {* clean_tac @{context} 1 *}) |
264 sorry |
322 sorry |
265 |
323 |
266 lemma lam_tst3: "(\<lambda>(y :: nat \<times> nat \<Rightarrow> nat \<times> nat). y) = (\<lambda>(x :: nat \<times> nat \<Rightarrow> nat \<times> nat). x)" |
|
267 by auto |
|
268 |
|
269 lemma "(\<lambda>(y :: my_int \<Rightarrow> my_int). y) = (\<lambda>(x :: my_int \<Rightarrow> my_int). x)" |
|
270 apply(tactic {* procedure_tac @{context} @{thm lam_tst3} 1 *}) |
|
271 defer |
|
272 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) |
|
273 apply(tactic {* clean_tac @{context} 1 *}) |
|
274 sorry |
|
275 |
|
276 end |
324 end |