equal
deleted
inserted
replaced
564 lemma Lmap_compose: "M \<in> llist(A) ==> Lmap (f o g) M = Lmap f (Lmap g M)" |
564 lemma Lmap_compose: "M \<in> llist(A) ==> Lmap (f o g) M = Lmap f (Lmap g M)" |
565 apply (simp add: o_def) |
565 apply (simp add: o_def) |
566 apply (drule imageI) |
566 apply (drule imageI) |
567 apply (erule LList_equalityI, safe) |
567 apply (erule LList_equalityI, safe) |
568 apply (erule llist.cases, simp_all) |
568 apply (erule llist.cases, simp_all) |
569 apply (rule LListD_Fun_NIL_I imageI UnI1 rangeI [THEN LListD_Fun_CONS_I])+ |
569 apply (rule LListD_Fun_NIL_I imageI UnI1 rangeI [THEN LListD_Fun_CONS_I, of _ _ _ f])+ |
570 apply assumption |
570 apply assumption |
571 done |
571 done |
572 |
572 |
573 lemma Lmap_ident: "M \<in> llist(A) ==> Lmap (%x. x) M = M" |
573 lemma Lmap_ident: "M \<in> llist(A) ==> Lmap (%x. x) M = M" |
574 apply (drule imageI) |
574 apply (drule imageI) |
575 apply (erule LList_equalityI, safe) |
575 apply (erule LList_equalityI, safe) |
576 apply (erule llist.cases, simp_all) |
576 apply (erule llist.cases, simp_all) |
577 apply (rule LListD_Fun_NIL_I imageI UnI1 rangeI [THEN LListD_Fun_CONS_I])+ |
577 apply (rule LListD_Fun_NIL_I imageI UnI1 rangeI [THEN LListD_Fun_CONS_I, of _ _ _ "%x. x"])+ |
578 apply assumption |
578 apply assumption |
579 done |
579 done |
580 |
580 |
581 |
581 |
582 subsection{* @{text Lappend} -- its two arguments cause some complications! *} |
582 subsection{* @{text Lappend} -- its two arguments cause some complications! *} |