src/HOL/List.thy
changeset 69140 f2d233f6356c
parent 69137 d4baf535f845
child 69206 a5c0d61ce5db
--- a/src/HOL/List.thy	Tue Oct 09 13:06:39 2018 +0200
+++ b/src/HOL/List.thy	Thu Oct 11 15:35:18 2018 +0200
@@ -4534,6 +4534,10 @@
 lemma split_Nil_iff[simp]: "splice xs ys = [] \<longleftrightarrow> xs = [] \<and> ys = []"
 by (induct xs ys rule: splice.induct) auto
 
+lemma splice_replicate[simp]: "splice (replicate m x) (replicate n x) = replicate (m+n) x"
+apply(induction "replicate m x" "replicate n x" arbitrary: m n rule: splice.induct)
+apply (auto simp add: Cons_replicate_eq dest: gr0_implies_Suc)
+done
 
 subsubsection \<open>@{const shuffles}\<close>