equal
deleted
inserted
replaced
3834 by (induct n) auto |
3834 by (induct n) auto |
3835 |
3835 |
3836 text{* Courtesy of Matthias Daum: *} |
3836 text{* Courtesy of Matthias Daum: *} |
3837 lemma append_replicate_commute: |
3837 lemma append_replicate_commute: |
3838 "replicate n x @ replicate k x = replicate k x @ replicate n x" |
3838 "replicate n x @ replicate k x = replicate k x @ replicate n x" |
3839 apply (simp add: replicate_add [THEN sym]) |
3839 apply (simp add: replicate_add [symmetric]) |
3840 apply (simp add: add.commute) |
3840 apply (simp add: add.commute) |
3841 done |
3841 done |
3842 |
3842 |
3843 text{* Courtesy of Andreas Lochbihler: *} |
3843 text{* Courtesy of Andreas Lochbihler: *} |
3844 lemma filter_replicate: |
3844 lemma filter_replicate: |