src/HOL/List.thy

   null:: "'a list => bool"
   "distinct":: "'a list => bool"
   replicate :: "nat => 'a => 'a list"
   rotate1 :: "'a list \<Rightarrow> 'a list"
   rotate :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list"
+  splice :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
   sublist :: "'a list => nat set => 'a list"
 (* For efficiency *)
   mem :: "'a => 'a list => bool"    (infixl 55)
   list_inter :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
   list_ex :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool"

  "list_all2 P xs ys ==
   length xs = length ys \<and> (\<forall>(x, y) \<in> set (zip xs ys). P x y)"
 
 sublist_def:
  "sublist xs A == map fst (filter (%p. snd p : A) (zip xs [0..<size xs]))"
+
+primrec
+"splice [] ys = ys"
+"splice (x#xs) ys = (if ys=[] then x#xs else x # hd ys # splice xs (tl ys))"
+  -- {*Warning: simpset does not contain the second eqn but a derived one. *}
 
 primrec
   "x mem [] = False"
   "x mem (y#ys) = (if y=x then True else x mem ys)"
 

   moreover hence "!x. x: set xs \<longrightarrow> x \<noteq> a" by auto
   ultimately show ?case by(simp add: sublist_Cons cong:filter_cong)
 qed
 
 
+subsubsection {* @{const splice} *}
+
+lemma splice_Nil2[simp]:
+ "splice xs [] = xs"
+by (cases xs) simp_all
+
+lemma splice_Cons_Cons[simp]:
+ "splice (x#xs) (y#ys) = x # y # splice xs ys"
+by simp
+
+declare splice.simps(2)[simp del]
+
 subsubsection{*Sets of Lists*}
 
 subsubsection {* @{text lists}: the list-forming operator over sets *}
 
 consts lists :: "'a set => 'a list set"