src/HOL/Word/BinOperations.thy

 subsection {* Splitting and concatenation *}
 
 definition bin_rcat :: "nat \<Rightarrow> int list \<Rightarrow> int" where
   "bin_rcat n = foldl (%u v. bin_cat u n v) Int.Pls"
 
-function bin_rsplit_aux :: "nat \<Rightarrow> nat \<Rightarrow> int \<Rightarrow> int list \<Rightarrow> int list" where
+fun bin_rsplit_aux :: "nat \<Rightarrow> nat \<Rightarrow> int \<Rightarrow> int list \<Rightarrow> int list" where
   "bin_rsplit_aux n m c bs =
     (if m = 0 | n = 0 then bs else
       let (a, b) = bin_split n c 
       in bin_rsplit_aux n (m - n) a (b # bs))"
-by pat_completeness auto
-termination by (relation "measure (fst o snd)") simp_all
 
 definition bin_rsplit :: "nat \<Rightarrow> nat \<times> int \<Rightarrow> int list" where
   "bin_rsplit n w = bin_rsplit_aux n (fst w) (snd w) []"
 
-function bin_rsplitl_aux :: "nat \<Rightarrow> nat \<Rightarrow> int \<Rightarrow> int list \<Rightarrow> int list" where
+fun bin_rsplitl_aux :: "nat \<Rightarrow> nat \<Rightarrow> int \<Rightarrow> int list \<Rightarrow> int list" where
   "bin_rsplitl_aux n m c bs =
     (if m = 0 | n = 0 then bs else
       let (a, b) = bin_split (min m n) c 
       in bin_rsplitl_aux n (m - n) a (b # bs))"
-by pat_completeness auto
-termination by (relation "measure (fst o snd)") simp_all
 
 definition bin_rsplitl :: "nat \<Rightarrow> nat \<times> int \<Rightarrow> int list" where
   "bin_rsplitl n w = bin_rsplitl_aux n (fst w) (snd w) []"
 
 declare bin_rsplit_aux.simps [simp del]