equal
deleted
inserted
replaced
289 lemma ho_map_rsp: |
289 lemma ho_map_rsp: |
290 "((op = ===> op =) ===> op \<approx> ===> op \<approx>) map map" |
290 "((op = ===> op =) ===> op \<approx> ===> op \<approx>) map map" |
291 by (simp add: fun_rel_id map_rsp) |
291 by (simp add: fun_rel_id map_rsp) |
292 |
292 |
293 lemma map_append : |
293 lemma map_append : |
294 "(map f ((a::'a list) @ b)) \<approx> |
294 "(map f (a @ b)) \<approx> |
295 ((map f a) ::'a list) @ (map f b)" |
295 (map f a) @ (map f b)" |
296 by simp (rule list_eq_refl) |
296 by simp (rule list_eq_refl) |
297 |
297 |
298 |
298 |
299 print_quotients |
299 print_quotients |
300 |
300 |
316 ML {* lift_thm_fset @{context} @{thm m1} *} |
316 ML {* lift_thm_fset @{context} @{thm m1} *} |
317 ML {* lift_thm_fset @{context} @{thm m2} *} |
317 ML {* lift_thm_fset @{context} @{thm m2} *} |
318 ML {* lift_thm_fset @{context} @{thm list_eq.intros(4)} *} |
318 ML {* lift_thm_fset @{context} @{thm list_eq.intros(4)} *} |
319 ML {* lift_thm_fset @{context} @{thm list_eq.intros(5)} *} |
319 ML {* lift_thm_fset @{context} @{thm list_eq.intros(5)} *} |
320 ML {* lift_thm_fset @{context} @{thm card1_suc} *} |
320 ML {* lift_thm_fset @{context} @{thm card1_suc} *} |
321 ML {* lift_thm_fset @{context} @{thm map_append} *} |
321 (*ML {* lift_thm_fset @{context} @{thm map_append} *}*) |
322 ML {* lift_thm_fset @{context} @{thm append_assoc} *} |
322 ML {* lift_thm_fset @{context} @{thm append_assoc} *} |
323 |
323 |
324 thm fold1.simps(2) |
324 thm fold1.simps(2) |
325 thm list.recs(2) |
325 thm list.recs(2) |
326 thm list.cases |
326 thm list.cases |