1(* Title: CCL/ex/List.thy 2 Author: Martin Coen, Cambridge University Computer Laboratory 3 Copyright 1993 University of Cambridge 4*) 5 6section \<open>Programs defined over lists\<close> 7 8theory List 9imports Nat 10begin 11 12definition map :: "[i\<Rightarrow>i,i]\<Rightarrow>i" 13 where "map(f,l) == lrec(l, [], \<lambda>x xs g. f(x)$g)" 14 15definition comp :: "[i\<Rightarrow>i,i\<Rightarrow>i]\<Rightarrow>i\<Rightarrow>i" (infixr "\<circ>" 55) 16 where "f \<circ> g == (\<lambda>x. f(g(x)))" 17 18definition append :: "[i,i]\<Rightarrow>i" (infixr "@" 55) 19 where "l @ m == lrec(l, m, \<lambda>x xs g. x$g)" 20 21axiomatization member :: "[i,i]\<Rightarrow>i" (infixr "mem" 55) (* FIXME dangling eq *) 22 where member_ax: "a mem l == lrec(l, false, \<lambda>h t g. if eq(a,h) then true else g)" 23 24definition filter :: "[i,i]\<Rightarrow>i" 25 where "filter(f,l) == lrec(l, [], \<lambda>x xs g. if f`x then x$g else g)" 26 27definition flat :: "i\<Rightarrow>i" 28 where "flat(l) == lrec(l, [], \<lambda>h t g. h @ g)" 29 30definition partition :: "[i,i]\<Rightarrow>i" where 31 "partition(f,l) == letrec part l a b be lcase(l, <a,b>, \<lambda>x xs. 32 if f`x then part(xs,x$a,b) else part(xs,a,x$b)) 33 in part(l,[],[])" 34 35definition insert :: "[i,i,i]\<Rightarrow>i" 36 where "insert(f,a,l) == lrec(l, a$[], \<lambda>h t g. if f`a`h then a$h$t else h$g)" 37 38definition isort :: "i\<Rightarrow>i" 39 where "isort(f) == lam l. lrec(l, [], \<lambda>h t g. insert(f,h,g))" 40 41definition qsort :: "i\<Rightarrow>i" where 42 "qsort(f) == lam l. letrec qsortx l be lcase(l, [], \<lambda>h t. 43 let p be partition(f`h,t) 44 in split(p, \<lambda>x y. qsortx(x) @ h$qsortx(y))) 45 in qsortx(l)" 46 47lemmas list_defs = map_def comp_def append_def filter_def flat_def 48 insert_def isort_def partition_def qsort_def 49 50lemma listBs [simp]: 51 "\<And>f g. (f \<circ> g) = (\<lambda>a. f(g(a)))" 52 "\<And>a f g. (f \<circ> g)(a) = f(g(a))" 53 "\<And>f. map(f,[]) = []" 54 "\<And>f x xs. map(f,x$xs) = f(x)$map(f,xs)" 55 "\<And>m. [] @ m = m" 56 "\<And>x xs m. x$xs @ m = x$(xs @ m)" 57 "\<And>f. filter(f,[]) = []" 58 "\<And>f x xs. filter(f,x$xs) = if f`x then x$filter(f,xs) else filter(f,xs)" 59 "flat([]) = []" 60 "\<And>x xs. flat(x$xs) = x @ flat(xs)" 61 "\<And>a f. insert(f,a,[]) = a$[]" 62 "\<And>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 65lemma nmapBnil: "n:Nat \<Longrightarrow> map(f) ^ n ` [] = []" 66 apply (erule Nat_ind) 67 apply simp_all 68 done 69 70lemma nmapBcons: "n:Nat \<Longrightarrow> 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 76lemma mapT: "\<lbrakk>\<And>x. x:A \<Longrightarrow> f(x):B; l : List(A)\<rbrakk> \<Longrightarrow> map(f,l) : List(B)" 77 apply (unfold map_def) 78 apply typechk 79 apply blast 80 done 81 82lemma appendT: "\<lbrakk>l : List(A); m : List(A)\<rbrakk> \<Longrightarrow> l @ m : List(A)" 83 apply (unfold append_def) 84 apply typechk 85 done 86 87lemma appendTS: 88 "\<lbrakk>l : {l:List(A). m : {m:List(A).P(l @ m)}}\<rbrakk> \<Longrightarrow> l @ m : {x:List(A). P(x)}" 89 by (blast intro!: appendT) 90 91lemma filterT: "\<lbrakk>f:A->Bool; l : List(A)\<rbrakk> \<Longrightarrow> filter(f,l) : List(A)" 92 apply (unfold filter_def) 93 apply typechk 94 done 95 96lemma flatT: "l : List(List(A)) \<Longrightarrow> flat(l) : List(A)" 97 apply (unfold flat_def) 98 apply (typechk appendT) 99 done 100 101lemma insertT: "\<lbrakk>f : A->A->Bool; a:A; l : List(A)\<rbrakk> \<Longrightarrow> insert(f,a,l) : List(A)" 102 apply (unfold insert_def) 103 apply typechk 104 done 105 106lemma insertTS: 107 "\<lbrakk>f : {f:A->A->Bool. a : {a:A. l : {l:List(A).P(insert(f,a,l))}}} \<rbrakk> \<Longrightarrow> 108 insert(f,a,l) : {x:List(A). P(x)}" 109 by (blast intro!: insertT) 110 111lemma partitionT: "\<lbrakk>f:A->Bool; l : List(A)\<rbrakk> \<Longrightarrow> partition(f,l) : List(A)*List(A)" 112 apply (unfold partition_def) 113 apply typechk 114 apply clean_ccs 115 apply (rule ListPRI [THEN wfstI, THEN ListPR_wf [THEN wmap_wf, THEN wfI]]) 116 apply assumption+ 117 apply (rule ListPRI [THEN wfstI, THEN ListPR_wf [THEN wmap_wf, THEN wfI]]) 118 apply assumption+ 119 done 120 121end 122