src/HOL/List.thy

--- a/src/HOL/List.thy	Sun Apr 09 19:29:44 2006 +0200
+++ b/src/HOL/List.thy	Sun Apr 09 19:41:30 2006 +0200
@@ -44,6 +44,7 @@
   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)
@@ -214,6 +215,11 @@
  "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)"
 
@@ -2150,6 +2156,18 @@
 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 *}