1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 *) 6 7chapter "List Manipulation Functions" 8 9theory List_Lib 10imports Main 11begin 12 13definition list_replace :: "'a list \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a list" where 14 "list_replace list a b \<equiv> map (\<lambda>x. if x = a then b else x) list" 15 16primrec list_replace_list :: "'a list \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where 17 "list_replace_list [] a list' = []" | 18 "list_replace_list (x # xs) a list' = (if x = a then list' @ xs 19 else x # list_replace_list xs a list')" 20 21definition list_swap :: "'a list \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a list" where 22 "list_swap list a b \<equiv> map (\<lambda>x. if x = a then b else if x = b then a else x) list" 23 24primrec list_insert_after :: "'a list \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a list" where 25 "list_insert_after [] a b = []" | 26 "list_insert_after (x # xs) a b = (if x = a then x # b # xs 27 else x # list_insert_after xs a b)" 28 29primrec list_remove :: "'a list \<Rightarrow> 'a \<Rightarrow> 'a list" where 30 "list_remove [] a = []" | 31 "list_remove (x # xs) a = (if x = a then (list_remove xs a) 32 else x # (list_remove xs a))" 33 34fun after_in_list :: "'a list \<Rightarrow> 'a \<Rightarrow> 'a option" where 35 "after_in_list [] a = None" | 36 "after_in_list [x] a = None" | 37 "after_in_list (x # y # xs) a = (if a = x then Some y else after_in_list (y # xs) a)" 38 39lemma zip_take1: 40 "zip (take n xs) ys = take n (zip xs ys)" 41 apply (induct xs arbitrary: n ys) 42 apply simp_all 43 apply (case_tac n, simp_all) 44 apply (case_tac ys, simp_all) 45 done 46 47lemma zip_take2: 48 "zip xs (take n ys) = take n (zip xs ys)" 49 apply (induct xs arbitrary: n ys) 50 apply simp_all 51 apply (case_tac n, simp_all) 52 apply (case_tac ys, simp_all) 53 done 54 55lemmas zip_take = zip_take1 zip_take2 56 57lemma replicate_append: "replicate n x @ (x # xs) = replicate (n + 1) x @ xs" 58 by (induct n, simp+) 59 60end 61