author | hoelzl |
Thu, 12 Nov 2009 17:21:43 +0100 | |
changeset 33638 | 548a34929e98 |
parent 27221 | 31328dc30196 |
child 35762 | af3ff2ba4c54 |
permissions | -rw-r--r-- |
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) |
|
27221
31328dc30196
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
24825
diff
changeset
|
78 |
apply (tactic "typechk_tac @{context} [] 1") |
20140 | 79 |
apply blast |
80 |
done |
|
81 |
||
82 |
lemma appendT: "[| l : List(A); m : List(A) |] ==> l @ m : List(A)" |
|
83 |
apply (unfold append_def) |
|
27221
31328dc30196
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
24825
diff
changeset
|
84 |
apply (tactic "typechk_tac @{context} [] 1") |
20140 | 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) |
|
27221
31328dc30196
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
24825
diff
changeset
|
93 |
apply (tactic "typechk_tac @{context} [] 1") |
20140 | 94 |
done |
95 |
||
96 |
lemma flatT: "l : List(List(A)) ==> flat(l) : List(A)" |
|
97 |
apply (unfold flat_def) |
|
27221
31328dc30196
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
24825
diff
changeset
|
98 |
apply (tactic {* typechk_tac @{context} @{thms appendT} 1 *}) |
20140 | 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) |
|
27221
31328dc30196
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
24825
diff
changeset
|
103 |
apply (tactic "typechk_tac @{context} [] 1") |
20140 | 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) |
|
27221
31328dc30196
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
24825
diff
changeset
|
114 |
apply (tactic "typechk_tac @{context} [] 1") |
31328dc30196
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
24825
diff
changeset
|
115 |
apply (tactic "clean_ccs_tac @{context}") |
20140 | 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 |