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