# Theory List

theory List
imports Nat
`(*  Title:      CCL/ex/List.thy    Author:     Martin Coen, Cambridge University Computer Laboratory    Copyright   1993  University of Cambridge*)header {* Programs defined over lists *}theory Listimports Natbegindefinition map :: "[i=>i,i]=>i"  where "map(f,l) == lrec(l,[],%x xs g. f(x)\$g)"definition comp :: "[i=>i,i=>i]=>i=>i"  (infixr "o" 55)  where "f o 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 :: "i=>i"  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 :: "i=>i"  where "isort(f) == lam l. lrec(l,[],%h t g. insert(f,h,g))"definition qsort :: "i=>i" 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_deflemma listBs [simp]:  "!!f g. (f o g) = (%a. f(g(a)))"  "!!a f g. (f o 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)"  by (simp_all add: list_defs)lemma nmapBnil: "n:Nat ==> map(f) ^ n ` [] = []"  apply (erule Nat_ind)   apply simp_all  donelemma nmapBcons: "n:Nat ==> map(f)^n`(x\$xs) = (f^n`x)\$(map(f)^n`xs)"  apply (erule Nat_ind)   apply simp_all  donelemma mapT: "[| !!x. x:A==>f(x):B;  l : List(A) |] ==> map(f,l) : List(B)"  apply (unfold map_def)  apply (tactic "typechk_tac @{context} [] 1")  apply blast  donelemma appendT: "[| l : List(A);  m : List(A) |] ==> l @ m : List(A)"  apply (unfold append_def)  apply (tactic "typechk_tac @{context} [] 1")  donelemma 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 (tactic "typechk_tac @{context} [] 1")  donelemma flatT: "l : List(List(A)) ==> flat(l) : List(A)"  apply (unfold flat_def)  apply (tactic {* typechk_tac @{context} @{thms appendT} 1 *})  donelemma insertT: "[|  f : A->A->Bool; a:A; l : List(A) |] ==> insert(f,a,l) : List(A)"  apply (unfold insert_def)  apply (tactic "typechk_tac @{context} [] 1")  donelemma 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 (tactic "typechk_tac @{context} [] 1")  apply (tactic "clean_ccs_tac @{context}")  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+  doneend`