297 oops |
297 oops |
298 |
298 |
299 lemma lam_tst3a: "(\<lambda>(y :: nat \<times> nat). y) = (\<lambda>(x :: nat \<times> nat). x)" |
299 lemma lam_tst3a: "(\<lambda>(y :: nat \<times> nat). y) = (\<lambda>(x :: nat \<times> nat). x)" |
300 by auto |
300 by auto |
301 |
301 |
302 lemma lam_tst3a_clean: "(op \<approx> ===> op \<approx>) |
|
303 ((ABS_my_int ---> REP_my_int) ((REP_my_int ---> ABS_my_int) (Babs (Respects op \<approx>) ( |
|
304 ((ABS_my_int ---> REP_my_int) ((REP_my_int ---> ABS_my_int) (\<lambda>y. REP_my_int (ABS_my_int y)))))))) |
|
305 ((ABS_my_int ---> REP_my_int) ((REP_my_int ---> ABS_my_int) (Babs (Respects op \<approx>) ( |
|
306 ((ABS_my_int ---> REP_my_int) ((REP_my_int ---> ABS_my_int) (\<lambda>y. REP_my_int (ABS_my_int y)))))))) |
|
307 = ((\<lambda>(y::my_int). y) = (\<lambda>x. x))" |
|
308 apply(subst lambda_prs[OF Quotient_my_int Quotient_my_int]) |
|
309 apply(subst lambda_prs[OF Quotient_my_int Quotient_my_int]) |
|
310 apply(subst Quotient_rel_rep[OF fun_quotient[OF Quotient_my_int Quotient_my_int]]) |
|
311 apply(subst babs_prs[OF Quotient_my_int Quotient_my_int]) |
|
312 apply(subst babs_prs[OF Quotient_my_int Quotient_my_int]) |
|
313 apply(rule refl) |
|
314 done |
|
315 |
|
316 lemma lam_tst3a_inj: "QUOT_TRUE ((\<lambda>(y::my_int). y) = (\<lambda>x. x)) \<Longrightarrow> |
|
317 (op \<approx> ===> op \<approx>) (Babs (Respects op \<approx>) (\<lambda>y. y)) (Babs (Respects op \<approx>) (\<lambda>x. x)) = |
|
318 (op \<approx> ===> op \<approx>) |
|
319 ((ABS_my_int ---> REP_my_int) ((REP_my_int ---> ABS_my_int) (Babs (Respects op \<approx>) ( |
|
320 ((ABS_my_int ---> REP_my_int) ((REP_my_int ---> ABS_my_int) (\<lambda>y. REP_my_int (ABS_my_int y)))))))) |
|
321 ((ABS_my_int ---> REP_my_int) ((REP_my_int ---> ABS_my_int) (Babs (Respects op \<approx>) ( |
|
322 ((ABS_my_int ---> REP_my_int) ((REP_my_int ---> ABS_my_int) (\<lambda>y. REP_my_int (ABS_my_int y))))))))" |
|
323 apply(tactic {* all_inj_repabs_tac @{context} 1*}) |
|
324 done |
|
325 |
|
326 lemma id_rsp: |
302 lemma id_rsp: |
327 shows "(R ===> R) id id" |
303 shows "(R ===> R) id id" |
328 by simp |
304 by simp |
329 |
305 |
330 lemma lam_tst3a_reg: "(op \<approx> ===> op \<approx>) (Babs (Respects op \<approx>) (\<lambda>y. y)) (Babs (Respects op \<approx>) (\<lambda>x. x))" |
306 lemma lam_tst3a_reg: "(op \<approx> ===> op \<approx>) (Babs (Respects op \<approx>) (\<lambda>y. y)) (Babs (Respects op \<approx>) (\<lambda>x. x))" |
331 apply (rule babs_rsp[OF Quotient_my_int]) |
307 apply (rule babs_rsp[OF Quotient_my_int]) |
332 apply (simp add: id_rsp) |
308 apply (simp add: id_rsp) |
333 done |
309 done |
334 |
310 |
335 |
|
336 lemma "(\<lambda>(y :: my_int). y) = (\<lambda>(x :: my_int). x)" |
311 lemma "(\<lambda>(y :: my_int). y) = (\<lambda>(x :: my_int). x)" |
337 apply(tactic {* procedure_tac @{context} @{thm lam_tst3a} 1 *}) |
312 apply(tactic {* procedure_tac @{context} @{thm lam_tst3a} 1 *}) |
338 defer |
313 apply(rule impI) |
|
314 apply(rule lam_tst3a_reg) |
339 apply(tactic {* all_inj_repabs_tac @{context} 1*}) |
315 apply(tactic {* all_inj_repabs_tac @{context} 1*}) |
340 apply(tactic {* clean_tac @{context} 1 *}) |
316 apply(tactic {* clean_tac @{context} 1 *}) |
341 apply(subst babs_rsp) |
317 apply(simp add: babs_prs[OF Quotient_my_int Quotient_my_int]) |
342 apply(tactic {* clean_tac @{context} 1 *}) |
318 done |
343 apply(simp) |
|
344 apply(tactic {* regularize_tac @{context} 1*})? |
|
345 apply(subst babs_reg_eqv) |
|
346 apply(tactic {* equiv_tac @{context} 1*}) |
|
347 apply(subst babs_reg_eqv) |
|
348 apply(tactic {* equiv_tac @{context} 1*}) |
|
349 sorry |
|
350 |
319 |
351 lemma lam_tst3b: "(\<lambda>(y :: nat \<times> nat \<Rightarrow> nat \<times> nat). y) = (\<lambda>(x :: nat \<times> nat \<Rightarrow> nat \<times> nat). x)" |
320 lemma lam_tst3b: "(\<lambda>(y :: nat \<times> nat \<Rightarrow> nat \<times> nat). y) = (\<lambda>(x :: nat \<times> nat \<Rightarrow> nat \<times> nat). x)" |
352 by auto |
321 by auto |
353 |
322 |
354 lemma "(\<lambda>(y :: my_int => my_int). y) = (\<lambda>(x :: my_int => my_int). x)" |
323 lemma "(\<lambda>(y :: my_int => my_int). y) = (\<lambda>(x :: my_int => my_int). x)" |
355 apply(tactic {* procedure_tac @{context} @{thm lam_tst3b} 1 *}) |
324 apply(tactic {* procedure_tac @{context} @{thm lam_tst3b} 1 *}) |
356 defer |
325 apply(rule impI) |
|
326 apply (rule babs_rsp[OF fun_quotient[OF Quotient_my_int Quotient_my_int]]) |
|
327 apply (simp add: id_rsp) |
357 apply(tactic {* all_inj_repabs_tac @{context} 1*}) |
328 apply(tactic {* all_inj_repabs_tac @{context} 1*}) |
358 apply(tactic {* clean_tac @{context} 1 *}) |
329 apply(tactic {* clean_tac @{context} 1 *}) |
359 apply(subst babs_rsp) |
330 apply(subst babs_prs) |
360 apply(tactic {* clean_tac @{context} 1 *}) |
331 apply(tactic {* quotient_tac @{context} 1 *}) |
361 apply(simp) |
332 apply(tactic {* quotient_tac @{context} 1 *}) |
362 apply(tactic {* regularize_tac @{context} 1*})? |
333 apply(subst babs_prs) |
363 sorry |
334 apply(tactic {* quotient_tac @{context} 1 *}) |
|
335 apply(tactic {* quotient_tac @{context} 1 *}) |
|
336 apply(rule refl) |
|
337 done |
364 |
338 |
365 end |
339 end |