# HG changeset patch
# User nipkow
# Date 1538025514 -7200
# Node ID 6e1b569ccce15595c8620fb31bd9c45ad87bf8ba
# Parent  787f3db8e313af7f9ee54ffa7a8b6de019ce1a27
simpler def

diff -r 787f3db8e313 -r 6e1b569ccce1 src/HOL/List.thy
--- a/src/HOL/List.thy	Wed Sep 26 22:38:16 2018 +0200
+++ b/src/HOL/List.thy	Thu Sep 27 07:18:34 2018 +0200
@@ -258,10 +258,13 @@
 
 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}"
@@ -4522,18 +4525,18 @@
 
 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
 
@@ -4552,7 +4555,7 @@
   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
@@ -4585,9 +4588,6 @@
   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