equal
deleted
inserted
replaced
306 oops |
306 oops |
307 |
307 |
308 lemma lam_tst3a: "(\<lambda>(y :: nat \<times> nat). y) = (\<lambda>(x :: nat \<times> nat). x)" |
308 lemma lam_tst3a: "(\<lambda>(y :: nat \<times> nat). y) = (\<lambda>(x :: nat \<times> nat). x)" |
309 by auto |
309 by auto |
310 |
310 |
|
311 lemma lam_tst3a_clean: "(op \<approx> ===> op \<approx>) |
|
312 ((ABS_my_int ---> REP_my_int) ((REP_my_int ---> ABS_my_int) (Babs (Respects op \<approx>) ( |
|
313 ((ABS_my_int ---> REP_my_int) ((REP_my_int ---> ABS_my_int) (\<lambda>y. REP_my_int (ABS_my_int y)))))))) |
|
314 ((ABS_my_int ---> REP_my_int) ((REP_my_int ---> ABS_my_int) (Babs (Respects op \<approx>) ( |
|
315 ((ABS_my_int ---> REP_my_int) ((REP_my_int ---> ABS_my_int) (\<lambda>y. REP_my_int (ABS_my_int y)))))))) |
|
316 = ((\<lambda>(y::my_int). y) = (\<lambda>x. x))" |
|
317 apply(subst babs_prs[OF Quotient_my_int Quotient_my_int]) |
|
318 apply(subst babs_prs[OF Quotient_my_int Quotient_my_int]) |
|
319 apply(subst lambda_prs[OF Quotient_my_int Quotient_my_int]) |
|
320 apply(subst lambda_prs[OF Quotient_my_int Quotient_my_int]) |
|
321 apply(subst Quotient_rel_rep[OF fun_quotient[OF Quotient_my_int Quotient_my_int]]) |
|
322 apply(rule refl) |
|
323 done |
|
324 |
311 lemma "(\<lambda>(y :: my_int). y) = (\<lambda>(x :: my_int). x)" |
325 lemma "(\<lambda>(y :: my_int). y) = (\<lambda>(x :: my_int). x)" |
312 apply(tactic {* procedure_tac @{context} @{thm lam_tst3a} 1 *}) |
326 apply(tactic {* procedure_tac @{context} @{thm lam_tst3a} 1 *}) |
313 defer |
327 defer |
314 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) |
328 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) |
315 apply(tactic {* clean_tac @{context} 1 *}) |
329 apply(tactic {* clean_tac @{context} 1 *}) |