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