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