41 qsort_def: "qsort(f) == lam l. letrec qsortx l be lcase(l,[],%h t. |
41 qsort_def: "qsort(f) == lam l. letrec qsortx l be lcase(l,[],%h t. |
42 let p be partition(f`h,t) |
42 let p be partition(f`h,t) |
43 in split(p,%x y. qsortx(x) @ h$qsortx(y))) |
43 in split(p,%x y. qsortx(x) @ h$qsortx(y))) |
44 in qsortx(l)" |
44 in qsortx(l)" |
45 |
45 |
46 ML {* use_legacy_bindings (the_context ()) *} |
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 |
47 |
121 |
48 end |
122 end |