author | wenzelm |
Sun, 02 Nov 2014 18:21:45 +0100 | |
changeset 58889 | 5b7a9633cfa8 |
parent 45010 | 8a4db903039f |
child 58971 | 8c9a319821b3 |
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 |
||
58889 | 6 |
section {* Programs defined over lists *} |
17456 | 7 |
|
8 |
theory List |
|
9 |
imports Nat |
|
10 |
begin |
|
0 | 11 |
|
42155
ffe99b07c9c0
modernized specifications -- some attempts to avoid wild axiomatizations;
wenzelm
parents:
35762
diff
changeset
|
12 |
definition map :: "[i=>i,i]=>i" |
ffe99b07c9c0
modernized specifications -- some attempts to avoid wild axiomatizations;
wenzelm
parents:
35762
diff
changeset
|
13 |
where "map(f,l) == lrec(l,[],%x xs g. f(x)$g)" |
ffe99b07c9c0
modernized specifications -- some attempts to avoid wild axiomatizations;
wenzelm
parents:
35762
diff
changeset
|
14 |
|
ffe99b07c9c0
modernized specifications -- some attempts to avoid wild axiomatizations;
wenzelm
parents:
35762
diff
changeset
|
15 |
definition comp :: "[i=>i,i=>i]=>i=>i" (infixr "\<circ>" 55) |
ffe99b07c9c0
modernized specifications -- some attempts to avoid wild axiomatizations;
wenzelm
parents:
35762
diff
changeset
|
16 |
where "f \<circ> g == (%x. f(g(x)))" |
ffe99b07c9c0
modernized specifications -- some attempts to avoid wild axiomatizations;
wenzelm
parents:
35762
diff
changeset
|
17 |
|
ffe99b07c9c0
modernized specifications -- some attempts to avoid wild axiomatizations;
wenzelm
parents:
35762
diff
changeset
|
18 |
definition append :: "[i,i]=>i" (infixr "@" 55) |
ffe99b07c9c0
modernized specifications -- some attempts to avoid wild axiomatizations;
wenzelm
parents:
35762
diff
changeset
|
19 |
where "l @ m == lrec(l,m,%x xs g. x$g)" |
0 | 20 |
|
42155
ffe99b07c9c0
modernized specifications -- some attempts to avoid wild axiomatizations;
wenzelm
parents:
35762
diff
changeset
|
21 |
axiomatization member :: "[i,i]=>i" (infixr "mem" 55) (* FIXME dangling eq *) |
45010 | 22 |
where member_ax: "a mem l == lrec(l,false,%h t g. if eq(a,h) then true else g)" |
0 | 23 |
|
42155
ffe99b07c9c0
modernized specifications -- some attempts to avoid wild axiomatizations;
wenzelm
parents:
35762
diff
changeset
|
24 |
definition filter :: "[i,i]=>i" |
ffe99b07c9c0
modernized specifications -- some attempts to avoid wild axiomatizations;
wenzelm
parents:
35762
diff
changeset
|
25 |
where "filter(f,l) == lrec(l,[],%x xs g. if f`x then x$g else g)" |
0 | 26 |
|
42155
ffe99b07c9c0
modernized specifications -- some attempts to avoid wild axiomatizations;
wenzelm
parents:
35762
diff
changeset
|
27 |
definition flat :: "i=>i" |
ffe99b07c9c0
modernized specifications -- some attempts to avoid wild axiomatizations;
wenzelm
parents:
35762
diff
changeset
|
28 |
where "flat(l) == lrec(l,[],%h t g. h @ g)" |
0 | 29 |
|
42155
ffe99b07c9c0
modernized specifications -- some attempts to avoid wild axiomatizations;
wenzelm
parents:
35762
diff
changeset
|
30 |
definition partition :: "[i,i]=>i" where |
1149 | 31 |
"partition(f,l) == letrec part l a b be lcase(l,<a,b>,%x xs. |
17456 | 32 |
if f`x then part(xs,x$a,b) else part(xs,a,x$b)) |
1149 | 33 |
in part(l,[],[])" |
42155
ffe99b07c9c0
modernized specifications -- some attempts to avoid wild axiomatizations;
wenzelm
parents:
35762
diff
changeset
|
34 |
|
ffe99b07c9c0
modernized specifications -- some attempts to avoid wild axiomatizations;
wenzelm
parents:
35762
diff
changeset
|
35 |
definition insert :: "[i,i,i]=>i" |
ffe99b07c9c0
modernized specifications -- some attempts to avoid wild axiomatizations;
wenzelm
parents:
35762
diff
changeset
|
36 |
where "insert(f,a,l) == lrec(l,a$[],%h t g. if f`a`h then a$h$t else h$g)" |
ffe99b07c9c0
modernized specifications -- some attempts to avoid wild axiomatizations;
wenzelm
parents:
35762
diff
changeset
|
37 |
|
ffe99b07c9c0
modernized specifications -- some attempts to avoid wild axiomatizations;
wenzelm
parents:
35762
diff
changeset
|
38 |
definition isort :: "i=>i" |
ffe99b07c9c0
modernized specifications -- some attempts to avoid wild axiomatizations;
wenzelm
parents:
35762
diff
changeset
|
39 |
where "isort(f) == lam l. lrec(l,[],%h t g. insert(f,h,g))" |
ffe99b07c9c0
modernized specifications -- some attempts to avoid wild axiomatizations;
wenzelm
parents:
35762
diff
changeset
|
40 |
|
ffe99b07c9c0
modernized specifications -- some attempts to avoid wild axiomatizations;
wenzelm
parents:
35762
diff
changeset
|
41 |
definition qsort :: "i=>i" where |
ffe99b07c9c0
modernized specifications -- some attempts to avoid wild axiomatizations;
wenzelm
parents:
35762
diff
changeset
|
42 |
"qsort(f) == lam l. letrec qsortx l be lcase(l,[],%h t. |
17456 | 43 |
let p be partition(f`h,t) |
44 |
in split(p,%x y. qsortx(x) @ h$qsortx(y))) |
|
1149 | 45 |
in qsortx(l)" |
0 | 46 |
|
20140 | 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]: |
|
42155
ffe99b07c9c0
modernized specifications -- some attempts to avoid wild axiomatizations;
wenzelm
parents:
35762
diff
changeset
|
51 |
"!!f g. (f \<circ> g) = (%a. f(g(a)))" |
ffe99b07c9c0
modernized specifications -- some attempts to avoid wild axiomatizations;
wenzelm
parents:
35762
diff
changeset
|
52 |
"!!a f g. (f \<circ> g)(a) = f(g(a))" |
20140 | 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)}" |
|
42155
ffe99b07c9c0
modernized specifications -- some attempts to avoid wild axiomatizations;
wenzelm
parents:
35762
diff
changeset
|
89 |
by (blast intro!: appendT) |
20140 | 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)}" |
|
42155
ffe99b07c9c0
modernized specifications -- some attempts to avoid wild axiomatizations;
wenzelm
parents:
35762
diff
changeset
|
109 |
by (blast intro!: insertT) |
20140 | 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 |