author  blanchet 
Mon, 15 Sep 2014 10:49:07 +0200  
changeset 58335  a5a3b576fcfb 
parent 45010  8a4db903039f 
child 58889  5b7a9633cfa8 
permissions  rwrr 
17456  1 
(* Title: CCL/ex/List.thy 
1474  2 
Author: Martin Coen, Cambridge University Computer Laboratory 
0  3 
Copyright 1993 University of Cambridge 
4 
*) 

5 

17456  6 
header {* Programs defined over lists *} 
7 

8 
theory List 

9 
imports Nat 

10 
begin 

0  11 

42155
ffe99b07c9c0
modernized specifications  some attempts to avoid wild axiomatizations;
wenzelm
parents:
35762
diff
changeset

12 
definition map :: "[i=>i,i]=>i" 
ffe99b07c9c0
modernized specifications  some attempts to avoid wild axiomatizations;
wenzelm
parents:
35762
diff
changeset

13 
where "map(f,l) == lrec(l,[],%x xs g. f(x)$g)" 
ffe99b07c9c0
modernized specifications  some attempts to avoid wild axiomatizations;
wenzelm
parents:
35762
diff
changeset

14 

ffe99b07c9c0
modernized specifications  some attempts to avoid wild axiomatizations;
wenzelm
parents:
35762
diff
changeset

15 
definition comp :: "[i=>i,i=>i]=>i=>i" (infixr "\<circ>" 55) 
ffe99b07c9c0
modernized specifications  some attempts to avoid wild axiomatizations;
wenzelm
parents:
35762
diff
changeset

16 
where "f \<circ> g == (%x. f(g(x)))" 
ffe99b07c9c0
modernized specifications  some attempts to avoid wild axiomatizations;
wenzelm
parents:
35762
diff
changeset

17 

ffe99b07c9c0
modernized specifications  some attempts to avoid wild axiomatizations;
wenzelm
parents:
35762
diff
changeset

18 
definition append :: "[i,i]=>i" (infixr "@" 55) 
ffe99b07c9c0
modernized specifications  some attempts to avoid wild axiomatizations;
wenzelm
parents:
35762
diff
changeset

19 
where "l @ m == lrec(l,m,%x xs g. x$g)" 
0  20 

42155
ffe99b07c9c0
modernized specifications  some attempts to avoid wild axiomatizations;
wenzelm
parents:
35762
diff
changeset

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

42155
ffe99b07c9c0
modernized specifications  some attempts to avoid wild axiomatizations;
wenzelm
parents:
35762
diff
changeset

24 
definition filter :: "[i,i]=>i" 
ffe99b07c9c0
modernized specifications  some attempts to avoid wild axiomatizations;
wenzelm
parents:
35762
diff
changeset

25 
where "filter(f,l) == lrec(l,[],%x xs g. if f`x then x$g else g)" 
0  26 

42155
ffe99b07c9c0
modernized specifications  some attempts to avoid wild axiomatizations;
wenzelm
parents:
35762
diff
changeset

27 
definition flat :: "i=>i" 
ffe99b07c9c0
modernized specifications  some attempts to avoid wild axiomatizations;
wenzelm
parents:
35762
diff
changeset

28 
where "flat(l) == lrec(l,[],%h t g. h @ g)" 
0  29 

42155
ffe99b07c9c0
modernized specifications  some attempts to avoid wild axiomatizations;
wenzelm
parents:
35762
diff
changeset

30 
definition partition :: "[i,i]=>i" where 
1149  31 
"partition(f,l) == letrec part l a b be lcase(l,<a,b>,%x xs. 
17456  32 
if f`x then part(xs,x$a,b) else part(xs,a,x$b)) 
1149  33 
in part(l,[],[])" 
42155
ffe99b07c9c0
modernized specifications  some attempts to avoid wild axiomatizations;
wenzelm
parents:
35762
diff
changeset

34 

ffe99b07c9c0
modernized specifications  some attempts to avoid wild axiomatizations;
wenzelm
parents:
35762
diff
changeset

35 
definition insert :: "[i,i,i]=>i" 
ffe99b07c9c0
modernized specifications  some attempts to avoid wild axiomatizations;
wenzelm
parents:
35762
diff
changeset

36 
where "insert(f,a,l) == lrec(l,a$[],%h t g. if f`a`h then a$h$t else h$g)" 
ffe99b07c9c0
modernized specifications  some attempts to avoid wild axiomatizations;
wenzelm
parents:
35762
diff
changeset

37 

ffe99b07c9c0
modernized specifications  some attempts to avoid wild axiomatizations;
wenzelm
parents:
35762
diff
changeset

38 
definition isort :: "i=>i" 
ffe99b07c9c0
modernized specifications  some attempts to avoid wild axiomatizations;
wenzelm
parents:
35762
diff
changeset

39 
where "isort(f) == lam l. lrec(l,[],%h t g. insert(f,h,g))" 
ffe99b07c9c0
modernized specifications  some attempts to avoid wild axiomatizations;
wenzelm
parents:
35762
diff
changeset

40 

ffe99b07c9c0
modernized specifications  some attempts to avoid wild axiomatizations;
wenzelm
parents:
35762
diff
changeset

41 
definition qsort :: "i=>i" where 
ffe99b07c9c0
modernized specifications  some attempts to avoid wild axiomatizations;
wenzelm
parents:
35762
diff
changeset

42 
"qsort(f) == lam l. letrec qsortx l be lcase(l,[],%h t. 
17456  43 
let p be partition(f`h,t) 
44 
in split(p,%x y. qsortx(x) @ h$qsortx(y))) 

1149  45 
in qsortx(l)" 
0  46 

20140  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]: 

42155
ffe99b07c9c0
modernized specifications  some attempts to avoid wild axiomatizations;
wenzelm
parents:
35762
diff
changeset

51 
"!!f g. (f \<circ> g) = (%a. f(g(a)))" 
ffe99b07c9c0
modernized specifications  some attempts to avoid wild axiomatizations;
wenzelm
parents:
35762
diff
changeset

52 
"!!a f g. (f \<circ> g)(a) = f(g(a))" 
20140  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) 

27221
31328dc30196
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
24825
diff
changeset

78 
apply (tactic "typechk_tac @{context} [] 1") 
20140  79 
apply blast 
80 
done 

81 

82 
lemma appendT: "[ l : List(A); m : List(A) ] ==> l @ m : List(A)" 

83 
apply (unfold append_def) 

27221
31328dc30196
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
24825
diff
changeset

84 
apply (tactic "typechk_tac @{context} [] 1") 
20140  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)}" 

42155
ffe99b07c9c0
modernized specifications  some attempts to avoid wild axiomatizations;
wenzelm
parents:
35762
diff
changeset

89 
by (blast intro!: appendT) 
20140  90 

91 
lemma filterT: "[ f:A>Bool; l : List(A) ] ==> filter(f,l) : List(A)" 

92 
apply (unfold filter_def) 

27221
31328dc30196
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
24825
diff
changeset

93 
apply (tactic "typechk_tac @{context} [] 1") 
20140  94 
done 
95 

96 
lemma flatT: "l : List(List(A)) ==> flat(l) : List(A)" 

97 
apply (unfold flat_def) 

27221
31328dc30196
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
24825
diff
changeset

98 
apply (tactic {* typechk_tac @{context} @{thms appendT} 1 *}) 
20140  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) 

27221
31328dc30196
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
24825
diff
changeset

103 
apply (tactic "typechk_tac @{context} [] 1") 
20140  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)}" 

42155
ffe99b07c9c0
modernized specifications  some attempts to avoid wild axiomatizations;
wenzelm
parents:
35762
diff
changeset

109 
by (blast intro!: insertT) 
20140  110 

111 
lemma partitionT: 

112 
"[ f:A>Bool; l : List(A) ] ==> partition(f,l) : List(A)*List(A)" 

113 
apply (unfold partition_def) 

27221
31328dc30196
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
24825
diff
changeset

114 
apply (tactic "typechk_tac @{context} [] 1") 
31328dc30196
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
24825
diff
changeset

115 
apply (tactic "clean_ccs_tac @{context}") 
20140  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 

17456  121 

0  122 
end 