equal
deleted
inserted
replaced
321 ((ABS_my_int ---> REP_my_int) ((REP_my_int ---> ABS_my_int) (Babs (Respects op \<approx>) ( |
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))))))))" |
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*}) |
323 apply(tactic {* all_inj_repabs_tac @{context} 1*}) |
324 done |
324 done |
325 |
325 |
|
326 lemma id_rsp: |
|
327 shows "(R ===> R) id id" |
|
328 by simp |
|
329 |
|
330 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]) |
|
332 apply (simp add: id_rsp) |
|
333 done |
|
334 |
326 |
335 |
327 lemma "(\<lambda>(y :: my_int). y) = (\<lambda>(x :: my_int). x)" |
336 lemma "(\<lambda>(y :: my_int). y) = (\<lambda>(x :: my_int). x)" |
328 apply(tactic {* procedure_tac @{context} @{thm lam_tst3a} 1 *}) |
337 apply(tactic {* procedure_tac @{context} @{thm lam_tst3a} 1 *}) |
329 defer |
338 defer |
330 apply(tactic {* all_inj_repabs_tac @{context} 1*}) |
339 apply(tactic {* all_inj_repabs_tac @{context} 1*}) |