# Theory List

(*  Title:      CCL/ex/List.thy
Author:     Martin Coen, Cambridge University Computer Laboratory
*)

section Programs defined over lists

theory List
imports Nat
begin

definition map :: "[ii,i]i"
where "map(f,l) == lrec(l, [], λx xs g. f(x)\$g)"

definition comp :: "[ii,ii]ii"  (infixr "" 55)
where "f  g == (λx. f(g(x)))"

definition append :: "[i,i]i"  (infixr "@" 55)
where "l @ m == lrec(l, m, λx xs g. x\$g)"

axiomatization member :: "[i,i]i"  (infixr "mem" 55)  (* FIXME dangling eq *)
where member_ax: "a mem l == lrec(l, false, λh t g. if eq(a,h) then true else g)"

definition filter :: "[i,i]i"
where "filter(f,l) == lrec(l, [], λx xs g. if f`x then x\$g else g)"

definition flat :: "ii"
where "flat(l) == lrec(l, [], λh t g. h @ g)"

definition partition :: "[i,i]i" where
"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,[],[])"

definition insert :: "[i,i,i]i"
where "insert(f,a,l) == lrec(l, a\$[], λh t g. if f`a`h then a\$h\$t else h\$g)"

definition isort :: "ii"
where "isort(f) == lam l. lrec(l, [], λh t g. insert(f,h,g))"

definition qsort :: "ii" where
"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)"

lemmas list_defs = map_def comp_def append_def filter_def flat_def
insert_def isort_def partition_def qsort_def

lemma listBs [simp]:
"f g. (f  g) = (λa. f(g(a)))"
"a f g. (f  g)(a) = f(g(a))"
"f. map(f,[]) = []"
"f x xs. map(f,x\$xs) = f(x)\$map(f,xs)"
"m. [] @ m = m"
"x xs m. x\$xs @ m = x\$(xs @ m)"
"f. filter(f,[]) = []"
"f x xs. filter(f,x\$xs) = if f`x then x\$filter(f,xs) else filter(f,xs)"
"flat([]) = []"
"x xs. flat(x\$xs) = x @ flat(xs)"
"a f. insert(f,a,[]) = a\$[]"
"a f xs. insert(f,a,x\$xs) = if f`a`x then a\$x\$xs else x\$insert(f,a,xs)"

lemma nmapBnil: "n:Nat  map(f) ^ n ` [] = []"
apply (erule Nat_ind)
apply simp_all
done

lemma nmapBcons: "n:Nat  map(f)^n`(x\$xs) = (f^n`x)\$(map(f)^n`xs)"
apply (erule Nat_ind)
apply simp_all
done

lemma mapT: "x. x:A  f(x):B; l : List(A)  map(f,l) : List(B)"
apply (unfold map_def)
apply typechk
apply blast
done

lemma appendT: "l : List(A); m : List(A)  l @ m : List(A)"
apply (unfold append_def)
apply typechk
done

lemma appendTS:
"l : {l:List(A). m : {m:List(A).P(l @ m)}}  l @ m : {x:List(A). P(x)}"
by (blast intro!: appendT)

lemma filterT: "f:A->Bool; l : List(A)  filter(f,l) : List(A)"
apply (unfold filter_def)
apply typechk
done

lemma flatT: "l : List(List(A))  flat(l) : List(A)"
apply (unfold flat_def)
apply (typechk appendT)
done

lemma insertT: "f : A->A->Bool; a:A; l : List(A)  insert(f,a,l) : List(A)"
apply (unfold insert_def)
apply typechk
done

lemma insertTS:
"f : {f:A->A->Bool. a : {a:A. l : {l:List(A).P(insert(f,a,l))}}}
insert(f,a,l)  : {x:List(A). P(x)}"
by (blast intro!: insertT)

lemma partitionT: "f:A->Bool; l : List(A)  partition(f,l) : List(A)*List(A)"
apply (unfold partition_def)
apply typechk
apply clean_ccs
apply (rule ListPRI [THEN wfstI, THEN ListPR_wf [THEN wmap_wf, THEN wfI]])
apply assumption+
apply (rule ListPRI [THEN wfstI, THEN ListPR_wf [THEN wmap_wf, THEN wfI]])
apply assumption+
done

end