src/HOL/List.thy

 "n_lists 0 xs = [[]]" |
 "n_lists (Suc n) xs = concat (map (\<lambda>ys. map (\<lambda>y. y # ys) xs) (n_lists n xs))"
 
 hide_const (open) n_lists
 
-fun splice :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
+function splice :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
 "splice [] ys = ys" |
-"splice xs [] = xs" |
-"splice (x#xs) (y#ys) = x # y # splice xs ys"
+"splice (x#xs) ys = x # splice ys xs"
+by pat_completeness auto
+
+termination
+by(relation "measure(\<lambda>(xs,ys). size xs + size ys)") auto
 
 function shuffle where
   "shuffle [] ys = {ys}"
 | "shuffle xs [] = {xs}"
 | "shuffle (x # xs) (y # ys) = (#) x ` shuffle xs (y # ys) \<union> (#) y ` shuffle (x # xs) ys"

 qed simp
 
 
 subsubsection \<open>@{const splice}\<close>
 
-lemma splice_Nil2 [simp, code]: "splice xs [] = xs"
+lemma splice_Nil2 [simp]: "splice xs [] = xs"
 by (cases xs) simp_all
-
-declare splice.simps(1,3)[code]
-declare splice.simps(2)[simp del]
 
 lemma length_splice[simp]: "length(splice xs ys) = length xs + length ys"
   by (induct xs ys rule: splice.induct) auto
 
 
 subsubsection \<open>@{const shuffle}\<close>
+
+lemma shuffle_commutes: "shuffle xs ys = shuffle ys xs"
+by (induction xs ys rule: shuffle.induct) (simp_all add: Un_commute)
 
 lemma Nil_in_shuffle[simp]: "[] \<in> shuffle xs ys \<longleftrightarrow> xs = [] \<and> ys = []"
   by (induct xs ys rule: shuffle.induct) auto
 
 lemma shuffleE:

     (xs \<noteq> [] \<and> hd xs = z \<and> zs \<in> shuffle (tl xs) ys \<or>
      ys \<noteq> [] \<and> hd ys = z \<and> zs \<in> shuffle xs (tl ys))"
   by (induct xs ys rule: shuffle.induct) auto
 
 lemma splice_in_shuffle [simp, intro]: "splice xs ys \<in> shuffle xs ys"
-  by (induction xs ys rule: splice.induct) (simp_all add: Cons_in_shuffle_iff)
+by (induction xs ys rule: splice.induct) (simp_all add: Cons_in_shuffle_iff shuffle_commutes)
 
 lemma Nil_in_shuffleI: "xs = [] \<Longrightarrow> ys = [] \<Longrightarrow> [] \<in> shuffle xs ys"
   by simp
 
 lemma Cons_in_shuffle_leftI: "zs \<in> shuffle xs ys \<Longrightarrow> z # zs \<in> shuffle (z # xs) ys"

   proof (cases zs)
     case (Cons z zs')
     with "3.prems" and "3.IH"[of zs'] show ?thesis by (force dest: set_shuffle)
   qed simp_all
 qed simp_all
-
-lemma shuffle_commutes: "shuffle xs ys = shuffle ys xs"
-  by (induction xs ys rule: shuffle.induct) (simp_all add: Un_commute)
 
 lemma Cons_shuffle_subset1: "(#) x ` shuffle xs ys \<subseteq> shuffle (x # xs) ys"
   by (cases ys) auto
 
 lemma Cons_shuffle_subset2: "(#) y ` shuffle xs ys \<subseteq> shuffle xs (y # ys)"