1(* 2 * Copyright 2014, NICTA 3 * 4 * This software may be distributed and modified according to the terms of 5 * the BSD 2-Clause license. Note that NO WARRANTY is provided. 6 * See "LICENSE_BSD2.txt" for details. 7 * 8 * @TAG(NICTA_BSD) 9 *) 10 11chapter "List Manipulation Functions" 12 13theory List_Lib 14imports Main 15begin 16 17definition list_replace :: "'a list \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a list" where 18 "list_replace list a b \<equiv> map (\<lambda>x. if x = a then b else x) list" 19 20primrec list_replace_list :: "'a list \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where 21 "list_replace_list [] a list' = []" | 22 "list_replace_list (x # xs) a list' = (if x = a then list' @ xs 23 else x # list_replace_list xs a list')" 24 25definition list_swap :: "'a list \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a list" where 26 "list_swap list a b \<equiv> map (\<lambda>x. if x = a then b else if x = b then a else x) list" 27 28primrec list_insert_after :: "'a list \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a list" where 29 "list_insert_after [] a b = []" | 30 "list_insert_after (x # xs) a b = (if x = a then x # b # xs 31 else x # list_insert_after xs a b)" 32 33primrec list_remove :: "'a list \<Rightarrow> 'a \<Rightarrow> 'a list" where 34 "list_remove [] a = []" | 35 "list_remove (x # xs) a = (if x = a then (list_remove xs a) 36 else x # (list_remove xs a))" 37 38fun after_in_list :: "'a list \<Rightarrow> 'a \<Rightarrow> 'a option" where 39 "after_in_list [] a = None" | 40 "after_in_list [x] a = None" | 41 "after_in_list (x # y # xs) a = (if a = x then Some y else after_in_list (y # xs) a)" 42 43lemma zip_take1: 44 "zip (take n xs) ys = take n (zip xs ys)" 45 apply (induct xs arbitrary: n ys) 46 apply simp_all 47 apply (case_tac n, simp_all) 48 apply (case_tac ys, simp_all) 49 done 50 51lemma zip_take2: 52 "zip xs (take n ys) = take n (zip xs ys)" 53 apply (induct xs arbitrary: n ys) 54 apply simp_all 55 apply (case_tac n, simp_all) 56 apply (case_tac ys, simp_all) 57 done 58 59lemmas zip_take = zip_take1 zip_take2 60 61end 62