(* Title: CCL/ex/List.thy ID: $Id: List.thy,v 1.6 2005/09/17 15:35:31 wenzelm Exp $ Author: Martin Coen, Cambridge University Computer Laboratory Copyright 1993 University of Cambridge *) header {* Programs defined over lists *} theory List imports Nat begin consts map :: "[i=>i,i]=>i" "o" :: "[i=>i,i=>i]=>i=>i" (infixr 55) "@" :: "[i,i]=>i" (infixr 55) mem :: "[i,i]=>i" (infixr 55) filter :: "[i,i]=>i" flat :: "i=>i" partition :: "[i,i]=>i" insert :: "[i,i,i]=>i" isort :: "i=>i" qsort :: "i=>i" axioms map_def: "map(f,l) == lrec(l,[],%x xs g. f(x)$g)" comp_def: "f o g == (%x. f(g(x)))" append_def: "l @ m == lrec(l,m,%x xs g. x$g)" mem_def: "a mem l == lrec(l,false,%h t g. if eq(a,h) then true else g)" filter_def: "filter(f,l) == lrec(l,[],%x xs g. if f`x then x$g else g)" flat_def: "flat(l) == lrec(l,[],%h t g. h @ g)" insert_def: "insert(f,a,l) == lrec(l,a$[],%h t g. if f`a`h then a$h$t else h$g)" isort_def: "isort(f) == lam l. lrec(l,[],%h t g. insert(f,h,g))" partition_def: "partition(f,l) == letrec part l a b be lcase(l,<a,b>,%x xs. if f`x then part(xs,x$a,b) else part(xs,a,x$b)) in part(l,[],[])" qsort_def: "qsort(f) == lam l. letrec qsortx l be lcase(l,[],%h t. let p be partition(f`h,t) in split(p,%x y. qsortx(x) @ h$qsortx(y))) in qsortx(l)" ML {* use_legacy_bindings (the_context ()) *} end
theorem nmapBnil:
n : Nat ==> map(f) ^ n ` [] = []
theorem nmapBcons:
n : Nat ==> map(f) ^ n ` x $ xs = (f ^ n ` x) $ (map(f) ^ n ` xs)
theorem mapT:
[| !!x. x : A ==> f(x) : B; l : List(A) |] ==> map(f, l) : List(B)
theorem appendT:
[| l : List(A); m : List(A) |] ==> l @ m : List(A)
theorem appendTS:
l : {l: List(A) . m : {m: List(A) . P(l @ m)}} ==> l @ m : Subtype(List(A), P)
theorem filterT:
[| f : A -> Bool; l : List(A) |] ==> filter(f, l) : List(A)
theorem flatT:
l : List(List(A)) ==> flat(l) : List(A)
theorem insertT:
[| f : A -> A -> Bool; a : A; l : List(A) |] ==> insert(f, a, l) : List(A)
theorem insertTS:
f : {f: A -> A -> Bool . a : {a: A . l : {l: List(A) . P(insert(f, a, l))}}} ==> insert(f, a, l) : Subtype(List(A), P)
theorem partitionT:
[| f : A -> Bool; l : List(A) |] ==> partition(f, l) : List(A) * List(A)