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