303 ((ABS_my_int ---> REP_my_int) ((REP_my_int ---> ABS_my_int) (Babs (Respects 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)))))))) |
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>) ( |
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)))))))) |
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))" |
307 = ((\<lambda>(y::my_int). y) = (\<lambda>x. x))" |
308 apply(subst babs_prs[OF Quotient_my_int Quotient_my_int]) |
|
309 apply(subst babs_prs[OF Quotient_my_int Quotient_my_int]) |
|
310 apply(subst lambda_prs[OF Quotient_my_int Quotient_my_int]) |
308 apply(subst lambda_prs[OF Quotient_my_int Quotient_my_int]) |
311 apply(subst lambda_prs[OF Quotient_my_int Quotient_my_int]) |
309 apply(subst lambda_prs[OF Quotient_my_int Quotient_my_int]) |
312 apply(subst Quotient_rel_rep[OF fun_quotient[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) |
313 apply(rule refl) |
314 done |
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 |
315 |
326 |
316 lemma "(\<lambda>(y :: my_int). y) = (\<lambda>(x :: my_int). x)" |
327 lemma "(\<lambda>(y :: my_int). y) = (\<lambda>(x :: my_int). x)" |
317 apply(tactic {* procedure_tac @{context} @{thm lam_tst3a} 1 *}) |
328 apply(tactic {* procedure_tac @{context} @{thm lam_tst3a} 1 *}) |
318 defer |
329 defer |
319 apply(tactic {* all_inj_repabs_tac @{context} 1*}) |
330 apply(tactic {* all_inj_repabs_tac @{context} 1*}) |