huffman@16221
|
1 |
(* Title: HOLCF/Fixrec.thy
|
huffman@16221
|
2 |
ID: $Id$
|
huffman@16221
|
3 |
Author: Amber Telfer and Brian Huffman
|
huffman@16221
|
4 |
*)
|
huffman@16221
|
5 |
|
huffman@16221
|
6 |
header "Package for defining recursive functions in HOLCF"
|
huffman@16221
|
7 |
|
huffman@16221
|
8 |
theory Fixrec
|
huffman@16551
|
9 |
imports Sprod Ssum Up One Tr Fix
|
haftmann@16417
|
10 |
uses ("fixrec_package.ML")
|
huffman@16221
|
11 |
begin
|
huffman@16221
|
12 |
|
huffman@16221
|
13 |
subsection {* Maybe monad type *}
|
huffman@16221
|
14 |
|
huffman@16776
|
15 |
defaultsort cpo
|
huffman@16776
|
16 |
|
huffman@16221
|
17 |
types 'a maybe = "one ++ 'a u"
|
huffman@16221
|
18 |
|
huffman@16221
|
19 |
constdefs
|
huffman@16221
|
20 |
fail :: "'a maybe"
|
huffman@16221
|
21 |
"fail \<equiv> sinl\<cdot>ONE"
|
huffman@16221
|
22 |
|
huffman@16221
|
23 |
return :: "'a \<rightarrow> 'a maybe"
|
huffman@16221
|
24 |
"return \<equiv> sinr oo up"
|
huffman@16221
|
25 |
|
huffman@16221
|
26 |
lemma maybeE:
|
huffman@16221
|
27 |
"\<lbrakk>p = \<bottom> \<Longrightarrow> Q; p = fail \<Longrightarrow> Q; \<And>x. p = return\<cdot>x \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
|
huffman@16221
|
28 |
apply (unfold fail_def return_def)
|
huffman@16221
|
29 |
apply (rule_tac p=p in ssumE, simp)
|
huffman@16221
|
30 |
apply (rule_tac p=x in oneE, simp, simp)
|
huffman@16754
|
31 |
apply (rule_tac p=y in upE, simp, simp)
|
huffman@16221
|
32 |
done
|
huffman@16221
|
33 |
|
huffman@16221
|
34 |
subsection {* Monadic bind operator *}
|
huffman@16221
|
35 |
|
huffman@16221
|
36 |
constdefs
|
huffman@16221
|
37 |
bind :: "'a maybe \<rightarrow> ('a \<rightarrow> 'b maybe) \<rightarrow> 'b maybe"
|
huffman@16221
|
38 |
"bind \<equiv> \<Lambda> m f. sscase\<cdot>sinl\<cdot>(fup\<cdot>f)\<cdot>m"
|
huffman@16221
|
39 |
|
huffman@16221
|
40 |
syntax
|
huffman@16221
|
41 |
"_bind" :: "'a maybe \<Rightarrow> ('a \<rightarrow> 'b maybe) \<Rightarrow> 'b maybe"
|
huffman@16221
|
42 |
("(_ >>= _)" [50, 51] 50)
|
huffman@16221
|
43 |
|
huffman@16221
|
44 |
translations "m >>= k" == "bind\<cdot>m\<cdot>k"
|
huffman@16221
|
45 |
|
huffman@16221
|
46 |
nonterminals
|
huffman@16221
|
47 |
maybebind maybebinds
|
huffman@16221
|
48 |
|
huffman@16221
|
49 |
syntax
|
huffman@16221
|
50 |
"_MBIND" :: "pttrn \<Rightarrow> 'a maybe \<Rightarrow> maybebind" ("(2_ <-/ _)" 10)
|
huffman@16221
|
51 |
"" :: "maybebind \<Rightarrow> maybebinds" ("_")
|
huffman@16221
|
52 |
|
huffman@16221
|
53 |
"_MBINDS" :: "[maybebind, maybebinds] \<Rightarrow> maybebinds" ("_;/ _")
|
huffman@16221
|
54 |
"_MDO" :: "[maybebinds, 'a maybe] \<Rightarrow> 'a maybe" ("(do _;/ (_))" 10)
|
huffman@16221
|
55 |
|
huffman@16221
|
56 |
translations
|
huffman@16221
|
57 |
"_MDO (_MBINDS b bs) e" == "_MDO b (_MDO bs e)"
|
huffman@16221
|
58 |
"do (x,y) <- m; e" == "m >>= (LAM <x,y>. e)"
|
huffman@16221
|
59 |
"do x <- m; e" == "m >>= (LAM x. e)"
|
huffman@16221
|
60 |
|
huffman@16221
|
61 |
text {* monad laws *}
|
huffman@16221
|
62 |
|
huffman@16221
|
63 |
lemma bind_strict [simp]: "UU >>= f = UU"
|
huffman@16221
|
64 |
by (simp add: bind_def)
|
huffman@16221
|
65 |
|
huffman@16221
|
66 |
lemma bind_fail [simp]: "fail >>= f = fail"
|
huffman@16221
|
67 |
by (simp add: bind_def fail_def)
|
huffman@16221
|
68 |
|
huffman@16221
|
69 |
lemma left_unit [simp]: "(return\<cdot>a) >>= k = k\<cdot>a"
|
huffman@16221
|
70 |
by (simp add: bind_def return_def)
|
huffman@16221
|
71 |
|
huffman@16221
|
72 |
lemma right_unit [simp]: "m >>= return = m"
|
huffman@16221
|
73 |
by (rule_tac p=m in maybeE, simp_all)
|
huffman@16221
|
74 |
|
huffman@16221
|
75 |
lemma bind_assoc [simp]:
|
huffman@16779
|
76 |
"(do b <- (do a <- m; k\<cdot>a); h\<cdot>b) = (do a <- m; b <- k\<cdot>a; h\<cdot>b)"
|
huffman@16221
|
77 |
by (rule_tac p=m in maybeE, simp_all)
|
huffman@16221
|
78 |
|
huffman@16221
|
79 |
subsection {* Run operator *}
|
huffman@16221
|
80 |
|
huffman@16221
|
81 |
constdefs
|
huffman@16776
|
82 |
run:: "'a::pcpo maybe \<rightarrow> 'a"
|
huffman@16221
|
83 |
"run \<equiv> sscase\<cdot>\<bottom>\<cdot>(fup\<cdot>ID)"
|
huffman@16221
|
84 |
|
huffman@16221
|
85 |
text {* rewrite rules for run *}
|
huffman@16221
|
86 |
|
huffman@16221
|
87 |
lemma run_strict [simp]: "run\<cdot>\<bottom> = \<bottom>"
|
huffman@16221
|
88 |
by (simp add: run_def)
|
huffman@16221
|
89 |
|
huffman@16221
|
90 |
lemma run_fail [simp]: "run\<cdot>fail = \<bottom>"
|
huffman@16221
|
91 |
by (simp add: run_def fail_def)
|
huffman@16221
|
92 |
|
huffman@16221
|
93 |
lemma run_return [simp]: "run\<cdot>(return\<cdot>x) = x"
|
huffman@16221
|
94 |
by (simp add: run_def return_def)
|
huffman@16221
|
95 |
|
huffman@16221
|
96 |
subsection {* Monad plus operator *}
|
huffman@16221
|
97 |
|
huffman@16221
|
98 |
constdefs
|
huffman@16221
|
99 |
mplus :: "'a maybe \<rightarrow> 'a maybe \<rightarrow> 'a maybe"
|
huffman@16221
|
100 |
"mplus \<equiv> \<Lambda> m1 m2. sscase\<cdot>(\<Lambda> x. m2)\<cdot>(fup\<cdot>return)\<cdot>m1"
|
huffman@16221
|
101 |
|
huffman@16221
|
102 |
syntax "+++" :: "'a maybe \<Rightarrow> 'a maybe \<Rightarrow> 'a maybe" (infixr 65)
|
huffman@16221
|
103 |
translations "x +++ y" == "mplus\<cdot>x\<cdot>y"
|
huffman@16221
|
104 |
|
huffman@16221
|
105 |
text {* rewrite rules for mplus *}
|
huffman@16221
|
106 |
|
huffman@16221
|
107 |
lemma mplus_strict [simp]: "\<bottom> +++ m = \<bottom>"
|
huffman@16221
|
108 |
by (simp add: mplus_def)
|
huffman@16221
|
109 |
|
huffman@16221
|
110 |
lemma mplus_fail [simp]: "fail +++ m = m"
|
huffman@16221
|
111 |
by (simp add: mplus_def fail_def)
|
huffman@16221
|
112 |
|
huffman@16221
|
113 |
lemma mplus_return [simp]: "return\<cdot>x +++ m = return\<cdot>x"
|
huffman@16221
|
114 |
by (simp add: mplus_def return_def)
|
huffman@16221
|
115 |
|
huffman@16460
|
116 |
lemma mplus_fail2 [simp]: "m +++ fail = m"
|
huffman@16460
|
117 |
by (rule_tac p=m in maybeE, simp_all)
|
huffman@16460
|
118 |
|
huffman@16221
|
119 |
lemma mplus_assoc: "(x +++ y) +++ z = x +++ (y +++ z)"
|
huffman@16221
|
120 |
by (rule_tac p=x in maybeE, simp_all)
|
huffman@16221
|
121 |
|
huffman@16221
|
122 |
subsection {* Match functions for built-in types *}
|
huffman@16221
|
123 |
|
huffman@16776
|
124 |
defaultsort pcpo
|
huffman@16776
|
125 |
|
huffman@16221
|
126 |
constdefs
|
huffman@16776
|
127 |
match_UU :: "'a \<rightarrow> unit maybe"
|
huffman@16776
|
128 |
"match_UU \<equiv> \<Lambda> x. fail"
|
huffman@16776
|
129 |
|
huffman@16776
|
130 |
match_cpair :: "'a::cpo \<times> 'b::cpo \<rightarrow> ('a \<times> 'b) maybe"
|
huffman@16221
|
131 |
"match_cpair \<equiv> csplit\<cdot>(\<Lambda> x y. return\<cdot><x,y>)"
|
huffman@16221
|
132 |
|
huffman@16551
|
133 |
match_spair :: "'a \<otimes> 'b \<rightarrow> ('a \<times> 'b) maybe"
|
huffman@16551
|
134 |
"match_spair \<equiv> ssplit\<cdot>(\<Lambda> x y. return\<cdot><x,y>)"
|
huffman@16551
|
135 |
|
huffman@16551
|
136 |
match_sinl :: "'a \<oplus> 'b \<rightarrow> 'a maybe"
|
huffman@16551
|
137 |
"match_sinl \<equiv> sscase\<cdot>return\<cdot>(\<Lambda> y. fail)"
|
huffman@16551
|
138 |
|
huffman@16551
|
139 |
match_sinr :: "'a \<oplus> 'b \<rightarrow> 'b maybe"
|
huffman@16551
|
140 |
"match_sinr \<equiv> sscase\<cdot>(\<Lambda> x. fail)\<cdot>return"
|
huffman@16551
|
141 |
|
huffman@16776
|
142 |
match_up :: "'a::cpo u \<rightarrow> 'a maybe"
|
huffman@16221
|
143 |
"match_up \<equiv> fup\<cdot>return"
|
huffman@16221
|
144 |
|
huffman@16460
|
145 |
match_ONE :: "one \<rightarrow> unit maybe"
|
huffman@18094
|
146 |
"match_ONE \<equiv> \<Lambda> ONE. return\<cdot>()"
|
huffman@18094
|
147 |
|
huffman@16460
|
148 |
match_TT :: "tr \<rightarrow> unit maybe"
|
huffman@18094
|
149 |
"match_TT \<equiv> \<Lambda> b. If b then return\<cdot>() else fail fi"
|
huffman@18094
|
150 |
|
huffman@16460
|
151 |
match_FF :: "tr \<rightarrow> unit maybe"
|
huffman@18094
|
152 |
"match_FF \<equiv> \<Lambda> b. If b then fail else return\<cdot>() fi"
|
huffman@16460
|
153 |
|
huffman@16776
|
154 |
lemma match_UU_simps [simp]:
|
huffman@16776
|
155 |
"match_UU\<cdot>x = fail"
|
huffman@16776
|
156 |
by (simp add: match_UU_def)
|
huffman@16776
|
157 |
|
huffman@16221
|
158 |
lemma match_cpair_simps [simp]:
|
huffman@16221
|
159 |
"match_cpair\<cdot><x,y> = return\<cdot><x,y>"
|
huffman@16221
|
160 |
by (simp add: match_cpair_def)
|
huffman@16221
|
161 |
|
huffman@16551
|
162 |
lemma match_spair_simps [simp]:
|
huffman@16551
|
163 |
"\<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> match_spair\<cdot>(:x,y:) = return\<cdot><x,y>"
|
huffman@16551
|
164 |
"match_spair\<cdot>\<bottom> = \<bottom>"
|
huffman@16551
|
165 |
by (simp_all add: match_spair_def)
|
huffman@16551
|
166 |
|
huffman@16551
|
167 |
lemma match_sinl_simps [simp]:
|
huffman@16551
|
168 |
"x \<noteq> \<bottom> \<Longrightarrow> match_sinl\<cdot>(sinl\<cdot>x) = return\<cdot>x"
|
huffman@16551
|
169 |
"x \<noteq> \<bottom> \<Longrightarrow> match_sinl\<cdot>(sinr\<cdot>x) = fail"
|
huffman@16551
|
170 |
"match_sinl\<cdot>\<bottom> = \<bottom>"
|
huffman@16551
|
171 |
by (simp_all add: match_sinl_def)
|
huffman@16551
|
172 |
|
huffman@16551
|
173 |
lemma match_sinr_simps [simp]:
|
huffman@16551
|
174 |
"x \<noteq> \<bottom> \<Longrightarrow> match_sinr\<cdot>(sinr\<cdot>x) = return\<cdot>x"
|
huffman@16551
|
175 |
"x \<noteq> \<bottom> \<Longrightarrow> match_sinr\<cdot>(sinl\<cdot>x) = fail"
|
huffman@16551
|
176 |
"match_sinr\<cdot>\<bottom> = \<bottom>"
|
huffman@16551
|
177 |
by (simp_all add: match_sinr_def)
|
huffman@16551
|
178 |
|
huffman@16221
|
179 |
lemma match_up_simps [simp]:
|
huffman@16221
|
180 |
"match_up\<cdot>(up\<cdot>x) = return\<cdot>x"
|
huffman@16221
|
181 |
"match_up\<cdot>\<bottom> = \<bottom>"
|
huffman@16221
|
182 |
by (simp_all add: match_up_def)
|
huffman@16221
|
183 |
|
huffman@16460
|
184 |
lemma match_ONE_simps [simp]:
|
huffman@16460
|
185 |
"match_ONE\<cdot>ONE = return\<cdot>()"
|
huffman@16460
|
186 |
"match_ONE\<cdot>\<bottom> = \<bottom>"
|
huffman@18094
|
187 |
by (simp_all add: match_ONE_def)
|
huffman@16460
|
188 |
|
huffman@16460
|
189 |
lemma match_TT_simps [simp]:
|
huffman@16460
|
190 |
"match_TT\<cdot>TT = return\<cdot>()"
|
huffman@16460
|
191 |
"match_TT\<cdot>FF = fail"
|
huffman@16460
|
192 |
"match_TT\<cdot>\<bottom> = \<bottom>"
|
huffman@18094
|
193 |
by (simp_all add: match_TT_def)
|
huffman@16460
|
194 |
|
huffman@16460
|
195 |
lemma match_FF_simps [simp]:
|
huffman@16460
|
196 |
"match_FF\<cdot>FF = return\<cdot>()"
|
huffman@16460
|
197 |
"match_FF\<cdot>TT = fail"
|
huffman@16460
|
198 |
"match_FF\<cdot>\<bottom> = \<bottom>"
|
huffman@18094
|
199 |
by (simp_all add: match_FF_def)
|
huffman@16460
|
200 |
|
huffman@16401
|
201 |
subsection {* Mutual recursion *}
|
huffman@16401
|
202 |
|
huffman@16401
|
203 |
text {*
|
huffman@16401
|
204 |
The following rules are used to prove unfolding theorems from
|
huffman@16401
|
205 |
fixed-point definitions of mutually recursive functions.
|
huffman@16401
|
206 |
*}
|
huffman@16401
|
207 |
|
huffman@16401
|
208 |
lemma cpair_equalI: "\<lbrakk>x \<equiv> cfst\<cdot>p; y \<equiv> csnd\<cdot>p\<rbrakk> \<Longrightarrow> <x,y> \<equiv> p"
|
huffman@16401
|
209 |
by (simp add: surjective_pairing_Cprod2)
|
huffman@16401
|
210 |
|
huffman@16401
|
211 |
lemma cpair_eqD1: "<x,y> = <x',y'> \<Longrightarrow> x = x'"
|
huffman@16401
|
212 |
by simp
|
huffman@16401
|
213 |
|
huffman@16401
|
214 |
lemma cpair_eqD2: "<x,y> = <x',y'> \<Longrightarrow> y = y'"
|
huffman@16401
|
215 |
by simp
|
huffman@16401
|
216 |
|
huffman@16463
|
217 |
text {* lemma for proving rewrite rules *}
|
huffman@16463
|
218 |
|
huffman@16463
|
219 |
lemma ssubst_lhs: "\<lbrakk>t = s; P s = Q\<rbrakk> \<Longrightarrow> P t = Q"
|
huffman@16463
|
220 |
by simp
|
huffman@16463
|
221 |
|
huffman@16401
|
222 |
ML {*
|
huffman@16401
|
223 |
val cpair_equalI = thm "cpair_equalI";
|
huffman@16401
|
224 |
val cpair_eqD1 = thm "cpair_eqD1";
|
huffman@16401
|
225 |
val cpair_eqD2 = thm "cpair_eqD2";
|
huffman@16463
|
226 |
val ssubst_lhs = thm "ssubst_lhs";
|
huffman@16401
|
227 |
*}
|
huffman@16221
|
228 |
|
huffman@16758
|
229 |
subsection {* Initializing the fixrec package *}
|
huffman@16221
|
230 |
|
huffman@16229
|
231 |
use "fixrec_package.ML"
|
huffman@16221
|
232 |
|
huffman@16221
|
233 |
end
|