1(*  Title:      CCL/ex/List.thy
2    Author:     Martin Coen, Cambridge University Computer Laboratory
3    Copyright   1993  University of Cambridge
4*)
5
6section \<open>Programs defined over lists\<close>
7
8theory List
9imports Nat
10begin
11
12definition map :: "[i\<Rightarrow>i,i]\<Rightarrow>i"
13  where "map(f,l) == lrec(l, [], \<lambda>x xs g. f(x)$g)"
14
15definition comp :: "[i\<Rightarrow>i,i\<Rightarrow>i]\<Rightarrow>i\<Rightarrow>i"  (infixr "\<circ>" 55)
16  where "f \<circ> g == (\<lambda>x. f(g(x)))"
17
18definition append :: "[i,i]\<Rightarrow>i"  (infixr "@" 55)
19  where "l @ m == lrec(l, m, \<lambda>x xs g. x$g)"
20
21axiomatization member :: "[i,i]\<Rightarrow>i"  (infixr "mem" 55)  (* FIXME dangling eq *)
22  where member_ax: "a mem l == lrec(l, false, \<lambda>h t g. if eq(a,h) then true else g)"
23
24definition filter :: "[i,i]\<Rightarrow>i"
25  where "filter(f,l) == lrec(l, [], \<lambda>x xs g. if f`x then x$g else g)"
26
27definition flat :: "i\<Rightarrow>i"
28  where "flat(l) == lrec(l, [], \<lambda>h t g. h @ g)"
29
30definition partition :: "[i,i]\<Rightarrow>i" where
31  "partition(f,l) == letrec part l a b be lcase(l, <a,b>, \<lambda>x xs.
32                            if f`x then part(xs,x$a,b) else part(xs,a,x$b))
33                    in part(l,[],[])"
34
35definition insert :: "[i,i,i]\<Rightarrow>i"
36  where "insert(f,a,l) == lrec(l, a$[], \<lambda>h t g. if f`a`h then a$h$t else h$g)"
37
38definition isort :: "i\<Rightarrow>i"
39  where "isort(f) == lam l. lrec(l, [], \<lambda>h t g. insert(f,h,g))"
40
41definition qsort :: "i\<Rightarrow>i" where
42  "qsort(f) == lam l. letrec qsortx l be lcase(l, [], \<lambda>h t.
43                                   let p be partition(f`h,t)
44                                   in split(p, \<lambda>x y. qsortx(x) @ h$qsortx(y)))
45                          in qsortx(l)"
46
47lemmas list_defs = map_def comp_def append_def filter_def flat_def
48  insert_def isort_def partition_def qsort_def
49
50lemma listBs [simp]:
51  "\<And>f g. (f \<circ> g) = (\<lambda>a. f(g(a)))"
52  "\<And>a f g. (f \<circ> g)(a) = f(g(a))"
53  "\<And>f. map(f,[]) = []"
54  "\<And>f x xs. map(f,x$xs) = f(x)$map(f,xs)"
55  "\<And>m. [] @ m = m"
56  "\<And>x xs m. x$xs @ m = x$(xs @ m)"
57  "\<And>f. filter(f,[]) = []"
58  "\<And>f x xs. filter(f,x$xs) = if f`x then x$filter(f,xs) else filter(f,xs)"
59  "flat([]) = []"
60  "\<And>x xs. flat(x$xs) = x @ flat(xs)"
61  "\<And>a f. insert(f,a,[]) = a$[]"
62  "\<And>a f xs. insert(f,a,x$xs) = if f`a`x then a$x$xs else x$insert(f,a,xs)"
63  by (simp_all add: list_defs)
64
65lemma nmapBnil: "n:Nat \<Longrightarrow> map(f) ^ n ` [] = []"
66  apply (erule Nat_ind)
67   apply simp_all
68  done
69
70lemma nmapBcons: "n:Nat \<Longrightarrow> map(f)^n`(x$xs) = (f^n`x)$(map(f)^n`xs)"
71  apply (erule Nat_ind)
72   apply simp_all
73  done
74
75
76lemma mapT: "\<lbrakk>\<And>x. x:A \<Longrightarrow> f(x):B; l : List(A)\<rbrakk> \<Longrightarrow> map(f,l) : List(B)"
77  apply (unfold map_def)
78  apply typechk
79  apply blast
80  done
81
82lemma appendT: "\<lbrakk>l : List(A); m : List(A)\<rbrakk> \<Longrightarrow> l @ m : List(A)"
83  apply (unfold append_def)
84  apply typechk
85  done
86
87lemma appendTS:
88  "\<lbrakk>l : {l:List(A). m : {m:List(A).P(l @ m)}}\<rbrakk> \<Longrightarrow> l @ m : {x:List(A). P(x)}"
89  by (blast intro!: appendT)
90
91lemma filterT: "\<lbrakk>f:A->Bool; l : List(A)\<rbrakk> \<Longrightarrow> filter(f,l) : List(A)"
92  apply (unfold filter_def)
93  apply typechk
94  done
95
96lemma flatT: "l : List(List(A)) \<Longrightarrow> flat(l) : List(A)"
97  apply (unfold flat_def)
98  apply (typechk appendT)
99  done
100
101lemma insertT: "\<lbrakk>f : A->A->Bool; a:A; l : List(A)\<rbrakk> \<Longrightarrow> insert(f,a,l) : List(A)"
102  apply (unfold insert_def)
103  apply typechk
104  done
105
106lemma insertTS:
107  "\<lbrakk>f : {f:A->A->Bool. a : {a:A. l : {l:List(A).P(insert(f,a,l))}}} \<rbrakk> \<Longrightarrow>
108   insert(f,a,l)  : {x:List(A). P(x)}"
109  by (blast intro!: insertT)
110
111lemma partitionT: "\<lbrakk>f:A->Bool; l : List(A)\<rbrakk> \<Longrightarrow> partition(f,l) : List(A)*List(A)"
112  apply (unfold partition_def)
113  apply typechk
114  apply clean_ccs
115  apply (rule ListPRI [THEN wfstI, THEN ListPR_wf [THEN wmap_wf, THEN wfI]])
116    apply assumption+
117  apply (rule ListPRI [THEN wfstI, THEN ListPR_wf [THEN wmap_wf, THEN wfI]])
118   apply assumption+
119  done
120
121end
122