author  huffman 
Sun, 06 Nov 2005 01:21:37 +0100  
changeset 18097  d196d84c306f 
parent 18096  574aa0487069 
child 18110  08ec4f1f116d 
permissions  rwrr 
16221  1 
(* Title: HOLCF/Fixrec.thy 
2 
ID: $Id$ 

3 
Author: Amber Telfer and Brian Huffman 

4 
*) 

5 

6 
header "Package for defining recursive functions in HOLCF" 

7 

8 
theory Fixrec 

16551  9 
imports Sprod Ssum Up One Tr Fix 
16417  10 
uses ("fixrec_package.ML") 
16221  11 
begin 
12 

13 
subsection {* Maybe monad type *} 

14 

16776
a3899ac14a1c
generalized types of monadic operators to class cpo; added match function for UU
huffman
parents:
16758
diff
changeset

15 
defaultsort cpo 
a3899ac14a1c
generalized types of monadic operators to class cpo; added match function for UU
huffman
parents:
16758
diff
changeset

16 

16221  17 
types 'a maybe = "one ++ 'a u" 
18 

19 
constdefs 

20 
fail :: "'a maybe" 

21 
"fail \<equiv> sinl\<cdot>ONE" 

22 

23 
return :: "'a \<rightarrow> 'a maybe" 

24 
"return \<equiv> sinr oo up" 

25 

26 
lemma maybeE: 

27 
"\<lbrakk>p = \<bottom> \<Longrightarrow> Q; p = fail \<Longrightarrow> Q; \<And>x. p = return\<cdot>x \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q" 

28 
apply (unfold fail_def return_def) 

29 
apply (rule_tac p=p in ssumE, simp) 

30 
apply (rule_tac p=x in oneE, simp, simp) 

16754  31 
apply (rule_tac p=y in upE, simp, simp) 
16221  32 
done 
33 

18097  34 
subsubsection {* Monadic bind operator *} 
16221  35 

18097  36 
constdefs 
37 
bind :: "'a maybe \<rightarrow> ('a \<rightarrow> 'b maybe) \<rightarrow> 'b maybe" 

38 
"bind \<equiv> \<Lambda> m f. sscase\<cdot>sinl\<cdot>(fup\<cdot>f)\<cdot>m" 

39 

40 
syntax ">>=" :: "['a maybe, 'a \<rightarrow> 'b maybe] \<Rightarrow> 'b maybe" (infixl ">>=" 50) 

41 
translations "m >>= f" == "bind\<cdot>m\<cdot>f" 

16221  42 

43 
nonterminals 

44 
maybebind maybebinds 

45 

46 
syntax 

47 
"_MBIND" :: "pttrn \<Rightarrow> 'a maybe \<Rightarrow> maybebind" ("(2_ </ _)" 10) 

48 
"" :: "maybebind \<Rightarrow> maybebinds" ("_") 

49 

50 
"_MBINDS" :: "[maybebind, maybebinds] \<Rightarrow> maybebinds" ("_;/ _") 

51 
"_MDO" :: "[maybebinds, 'a maybe] \<Rightarrow> 'a maybe" ("(do _;/ (_))" 10) 

52 

53 
translations 

54 
"_MDO (_MBINDS b bs) e" == "_MDO b (_MDO bs e)" 

55 
"do (x,y) < m; e" == "m >>= (LAM <x,y>. e)" 

56 
"do x < m; e" == "m >>= (LAM x. e)" 

57 

58 
text {* monad laws *} 

59 

60 
lemma bind_strict [simp]: "UU >>= f = UU" 

61 
by (simp add: bind_def) 

62 

63 
lemma bind_fail [simp]: "fail >>= f = fail" 

64 
by (simp add: bind_def fail_def) 

65 

66 
lemma left_unit [simp]: "(return\<cdot>a) >>= k = k\<cdot>a" 

67 
by (simp add: bind_def return_def) 

68 

69 
lemma right_unit [simp]: "m >>= return = m" 

70 
by (rule_tac p=m in maybeE, simp_all) 

71 

72 
lemma bind_assoc [simp]: 

16779  73 
"(do b < (do a < m; k\<cdot>a); h\<cdot>b) = (do a < m; b < k\<cdot>a; h\<cdot>b)" 
16221  74 
by (rule_tac p=m in maybeE, simp_all) 
75 

18097  76 
subsubsection {* Run operator *} 
16221  77 

78 
constdefs 

16776
a3899ac14a1c
generalized types of monadic operators to class cpo; added match function for UU
huffman
parents:
16758
diff
changeset

79 
run:: "'a::pcpo maybe \<rightarrow> 'a" 
16221  80 
"run \<equiv> sscase\<cdot>\<bottom>\<cdot>(fup\<cdot>ID)" 
81 

82 
text {* rewrite rules for run *} 

83 

84 
lemma run_strict [simp]: "run\<cdot>\<bottom> = \<bottom>" 

85 
by (simp add: run_def) 

86 

87 
lemma run_fail [simp]: "run\<cdot>fail = \<bottom>" 

88 
by (simp add: run_def fail_def) 

89 

90 
lemma run_return [simp]: "run\<cdot>(return\<cdot>x) = x" 

91 
by (simp add: run_def return_def) 

92 

18097  93 
subsubsection {* Monad plus operator *} 
16221  94 

18097  95 
constdefs 
96 
mplus :: "'a maybe \<rightarrow> 'a maybe \<rightarrow> 'a maybe" 

97 
"mplus \<equiv> \<Lambda> m1 m2. sscase\<cdot>(\<Lambda> x. m2)\<cdot>(fup\<cdot>return)\<cdot>m1" 

98 

99 
syntax "+++" :: "['a maybe, 'a maybe] \<Rightarrow> 'a maybe" (infixr "+++" 65) 

100 
translations "m1 +++ m2" == "mplus\<cdot>m1\<cdot>m2" 

16221  101 

102 
text {* rewrite rules for mplus *} 

103 

104 
lemma mplus_strict [simp]: "\<bottom> +++ m = \<bottom>" 

105 
by (simp add: mplus_def) 

106 

107 
lemma mplus_fail [simp]: "fail +++ m = m" 

108 
by (simp add: mplus_def fail_def) 

109 

110 
lemma mplus_return [simp]: "return\<cdot>x +++ m = return\<cdot>x" 

111 
by (simp add: mplus_def return_def) 

112 

16460
72a08d509d62
added match functions for ONE, TT, and FF; added theorem mplus_fail2
huffman
parents:
16417
diff
changeset

113 
lemma mplus_fail2 [simp]: "m +++ fail = m" 
72a08d509d62
added match functions for ONE, TT, and FF; added theorem mplus_fail2
huffman
parents:
16417
diff
changeset

114 
by (rule_tac p=m in maybeE, simp_all) 
72a08d509d62
added match functions for ONE, TT, and FF; added theorem mplus_fail2
huffman
parents:
16417
diff
changeset

115 

16221  116 
lemma mplus_assoc: "(x +++ y) +++ z = x +++ (y +++ z)" 
117 
by (rule_tac p=x in maybeE, simp_all) 

118 

18097  119 
subsubsection {* Fatbar combinator *} 
120 

121 
constdefs 

122 
fatbar :: "('a \<rightarrow> 'b maybe) \<rightarrow> ('a \<rightarrow> 'b maybe) \<rightarrow> ('a \<rightarrow> 'b maybe)" 

123 
"fatbar \<equiv> \<Lambda> a b x. a\<cdot>x +++ b\<cdot>x" 

124 

125 
syntax 

126 
"\<parallel>" :: "['a \<rightarrow> 'b maybe, 'a \<rightarrow> 'b maybe] \<Rightarrow> 'a \<rightarrow> 'b maybe" (infixr "\<parallel>" 60) 

127 
translations 

128 
"m1 \<parallel> m2" == "fatbar\<cdot>m1\<cdot>m2" 

129 

130 
lemma fatbar1: "m\<cdot>x = \<bottom> \<Longrightarrow> (m \<parallel> ms)\<cdot>x = \<bottom>" 

131 
by (simp add: fatbar_def) 

132 

133 
lemma fatbar2: "m\<cdot>x = fail \<Longrightarrow> (m \<parallel> ms)\<cdot>x = ms\<cdot>x" 

134 
by (simp add: fatbar_def) 

135 

136 
lemma fatbar3: "m\<cdot>x = return\<cdot>y \<Longrightarrow> (m \<parallel> ms)\<cdot>x = return\<cdot>y" 

137 
by (simp add: fatbar_def) 

138 

139 
lemmas fatbar_simps = fatbar1 fatbar2 fatbar3 

140 

141 
subsection {* Pattern combinators *} 

142 

143 
types ('a,'b,'c) pattern = "'b \<rightarrow> 'a \<rightarrow> 'c maybe" 

144 

145 
constdefs 

146 
wild_pat :: "('a, 'b, 'b) pattern" 

147 
"wild_pat \<equiv> \<Lambda> r a. return\<cdot>r" 

148 

149 
var_pat :: "('a, 'a \<rightarrow> 'b, 'b) pattern" 

150 
"var_pat \<equiv> \<Lambda> r a. return\<cdot>(r\<cdot>a)" 

151 

152 
as_pat :: "('a, 'b, 'c) pattern \<Rightarrow> ('a, 'a \<rightarrow> 'b, 'c) pattern" 

153 
"as_pat p \<equiv> \<Lambda> r a. p\<cdot>(r\<cdot>a)\<cdot>a" 

154 

155 
lemma wild_pat [simp]: "wild_pat\<cdot>r\<cdot>a = return\<cdot>r" 

156 
by (simp add: wild_pat_def) 

157 

158 
lemma var_pat [simp]: "var_pat\<cdot>r\<cdot>a = return\<cdot>(r\<cdot>a)" 

159 
by (simp add: var_pat_def) 

160 

161 
lemma as_pat [simp]: "as_pat p\<cdot>r\<cdot>a = p\<cdot>(r\<cdot>a)\<cdot>a" 

162 
by (simp add: as_pat_def) 

163 

164 
subsection {* Case syntax *} 

165 

166 
nonterminals 

167 
Case_syn Cases_syn 

168 

169 
syntax 

170 
"_Case_syntax":: "['a, Cases_syn] => 'b" ("(Case _ of/ _)" 10) 

171 
"_Case1" :: "['a, 'b] => Case_syn" ("(2_ =>/ _)" 10) 

172 
"" :: "Case_syn => Cases_syn" ("_") 

173 
"_Case2" :: "[Case_syn, Cases_syn] => Cases_syn" ("_/  _") 

174 
"_as_pattern" :: "[idt, 'a] \<Rightarrow> 'a" (infixr "as" 10) 

175 

176 
syntax (xsymbols) 

177 
"_Case1" :: "['a, 'b] => Case_syn" ("(2_ \<Rightarrow>/ _)" 10) 

178 

179 
syntax 

180 
"_match" :: "'a \<Rightarrow> Case_syn" (* or Cases_syn *) 

181 
"_as" :: "[pttrn, Case_syn] \<Rightarrow> Case_syn" 

182 
"_matches" :: "['a, Case_syn, 'a list] \<Rightarrow> Case_syn" 

183 
"_cons" :: "['a, 'a list] \<Rightarrow> 'a list" 

184 
"_nil" :: "'a list" 

185 

186 
translations 

187 
"_Case_syntax x (_match m)" == "run\<cdot>(m\<cdot>x)" 

188 
"_Case2 (_match c) (_match cs)" == "_match (c \<parallel> cs)" 

189 
"_Case1 dummy_pattern r" == "_match (wild_pat\<cdot>r)" 

190 
"_as x (_match (p\<cdot>t))" == "_match ((as_pat p)\<cdot>(\<Lambda> x. t))" 

191 
"_Case1 (_as_pattern x e) r" == "_as x (_Case1 e r)" 

192 
"_Case1 x t" == "_match (var_pat\<cdot>(\<Lambda> x. t))" 

193 
"_Case1 (f\<cdot>e) r" == "_matches f (_Case1 e r) _nil" 

194 
"_matches (f\<cdot>e) (_match (p\<cdot>r)) ps" == "_matches f (_Case1 e r) (_cons p ps)" 

195 

196 
lemma run_fatbar1: "m\<cdot>x = \<bottom> \<Longrightarrow> run\<cdot>((m \<parallel> ms)\<cdot>x) = \<bottom>" 

197 
by (simp add: fatbar_def) 

198 

199 
lemma run_fatbar2: "m\<cdot>x = fail \<Longrightarrow> run\<cdot>((m \<parallel> ms)\<cdot>x) = run\<cdot>(ms\<cdot>x)" 

200 
by (simp add: fatbar_def) 

201 

202 
lemma run_fatbar3: "m\<cdot>x = return\<cdot>y \<Longrightarrow> run\<cdot>((m \<parallel> ms)\<cdot>x) = y" 

203 
by (simp add: fatbar_def) 

204 

205 
lemmas run_fatbar_simps [simp] = run_fatbar1 run_fatbar2 run_fatbar3 

206 

207 
subsection {* Pattern combinators for builtin types *} 

208 

209 
constdefs 

210 
cpair_pat :: "_" 

211 
"cpair_pat p1 p2 \<equiv> \<Lambda> r1 \<langle>x1,x2\<rangle>. bind\<cdot>(p1\<cdot>r1\<cdot>x1)\<cdot>(\<Lambda> r2. p2\<cdot>r2\<cdot>x2)" 

212 

213 
spair_pat :: "_" 

214 
"spair_pat p1 p2 \<equiv> \<Lambda> r (:x,y:). cpair_pat p1 p2\<cdot>r\<cdot>\<langle>x,y\<rangle>" 

215 

216 
sinl_pat :: "_" 

217 
"sinl_pat p \<equiv> \<Lambda> r a. case a of sinl\<cdot>x \<Rightarrow> p\<cdot>r\<cdot>x  sinr\<cdot>y \<Rightarrow> fail" 

218 

219 
sinr_pat :: "_" 

220 
"sinr_pat p \<equiv> \<Lambda> r a. case a of sinl\<cdot>x \<Rightarrow> fail  sinr\<cdot>y \<Rightarrow> p\<cdot>r\<cdot>y" 

221 

222 
up_pat :: "_" 

223 
"up_pat p \<equiv> \<Lambda> r a. case a of up\<cdot>x \<Rightarrow> p\<cdot>r\<cdot>x" 

224 

225 
Def_pat :: "'a::type \<Rightarrow> ('a lift, 'b, 'b) pattern" 

226 
"Def_pat x \<equiv> \<Lambda> r. FLIFT y. if x = y then return\<cdot>r else fail" 

227 

228 
ONE_pat :: "_" 

229 
"ONE_pat \<equiv> \<Lambda> r ONE. return\<cdot>r" 

230 

231 
TT_pat :: "(tr, _, _) pattern" 

232 
"TT_pat \<equiv> \<Lambda> r b. If b then return\<cdot>r else fail fi" 

233 

234 
FF_pat :: "(tr, _, _) pattern" 

235 
"FF_pat \<equiv> \<Lambda> r b. If b then fail else return\<cdot>r fi" 

236 

237 
translations 

238 
"_matches cpair (_match (p1\<cdot>r)) (_cons p2 _nil)" 

239 
== "_match ((cpair_pat p1 p2)\<cdot>r)" 

240 

241 
"_matches spair (_match (p1\<cdot>r)) (_cons p2 _nil)" 

242 
== "_match ((spair_pat p1 p2)\<cdot>r)" 

243 

244 
translations 

245 
"_matches sinl (_match (p1\<cdot>r)) _nil" == "_match ((sinl_pat p1)\<cdot>r)" 

246 
"_matches sinr (_match (p1\<cdot>r)) _nil" == "_match ((sinr_pat p1)\<cdot>r)" 

247 
"_matches up (_match (p1\<cdot>r)) _nil" == "_match ((up_pat p1)\<cdot>r)" 

248 

249 
translations 

250 
"_Case1 (Def x) r" == "_match (Def_pat x\<cdot>r)" 

251 
"_Case1 ONE r" == "_match (ONE_pat\<cdot>r)" 

252 
"_Case1 TT r" == "_match (TT_pat\<cdot>r)" 

253 
"_Case1 FF r" == "_match (FF_pat\<cdot>r)" 

254 

255 
lemma cpair_pat_simps [simp]: 

256 
"p1\<cdot>r\<cdot>x = \<bottom> \<Longrightarrow> cpair_pat p1 p2\<cdot>r\<cdot><x,y> = \<bottom>" 

257 
"p1\<cdot>r\<cdot>x = fail \<Longrightarrow> cpair_pat p1 p2\<cdot>r\<cdot><x,y> = fail" 

258 
"p1\<cdot>r\<cdot>x = return\<cdot>r' \<Longrightarrow> cpair_pat p1 p2\<cdot>r\<cdot><x,y> = p2\<cdot>r'\<cdot>y" 

259 
by (simp_all add: cpair_pat_def) 

260 

261 
lemma spair_pat_simps [simp]: 

262 
"spair_pat p1 p2\<cdot>r\<cdot>\<bottom> = \<bottom>" 

263 
"\<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> spair_pat p1 p2\<cdot>r\<cdot>(:x, y:) = cpair_pat p1 p2\<cdot>r\<cdot>\<langle>x, y\<rangle>" 

264 
by (simp_all add: spair_pat_def) 

265 

266 
lemma sinl_pat_simps [simp]: 

267 
"sinl_pat p\<cdot>r\<cdot>\<bottom> = \<bottom>" 

268 
"x \<noteq> \<bottom> \<Longrightarrow> sinl_pat p\<cdot>r\<cdot>(sinl\<cdot>x) = p\<cdot>r\<cdot>x" 

269 
"x \<noteq> \<bottom> \<Longrightarrow> sinl_pat p\<cdot>r\<cdot>(sinr\<cdot>x) = fail" 

270 
by (simp_all add: sinl_pat_def) 

271 

272 
lemma sinr_pat_simps [simp]: 

273 
"sinr_pat p\<cdot>r\<cdot>\<bottom> = \<bottom>" 

274 
"x \<noteq> \<bottom> \<Longrightarrow> sinr_pat p\<cdot>r\<cdot>(sinl\<cdot>x) = fail" 

275 
"x \<noteq> \<bottom> \<Longrightarrow> sinr_pat p\<cdot>r\<cdot>(sinr\<cdot>x) = p\<cdot>r\<cdot>x" 

276 
by (simp_all add: sinr_pat_def) 

277 

278 
lemma up_pat_simps [simp]: 

279 
"up_pat p\<cdot>r\<cdot>\<bottom> = \<bottom>" 

280 
"up_pat p\<cdot>r\<cdot>(up\<cdot>x) = p\<cdot>r\<cdot>x" 

281 
by (simp_all add: up_pat_def) 

282 

283 
lemma Def_pat_simps [simp]: 

284 
"Def_pat x\<cdot>r\<cdot>\<bottom> = \<bottom>" 

285 
"Def_pat x\<cdot>r\<cdot>(Def x) = return\<cdot>r" 

286 
"x \<noteq> y \<Longrightarrow> Def_pat x\<cdot>r\<cdot>(Def y) = fail" 

287 
by (simp_all add: Def_pat_def) 

288 

289 
lemma ONE_pat_simps [simp]: 

290 
"ONE_pat\<cdot>r\<cdot>\<bottom> = \<bottom>" 

291 
"ONE_pat\<cdot>r\<cdot>ONE = return\<cdot>r" 

292 
by (simp_all add: ONE_pat_def) 

293 

294 
lemma TT_pat_simps [simp]: 

295 
"TT_pat\<cdot>r\<cdot>\<bottom> = \<bottom>" 

296 
"TT_pat\<cdot>r\<cdot>TT = return\<cdot>r" 

297 
"TT_pat\<cdot>r\<cdot>FF = fail" 

298 
by (simp_all add: TT_pat_def) 

299 

300 
lemma FF_pat_simps [simp]: 

301 
"FF_pat\<cdot>r\<cdot>\<bottom> = \<bottom>" 

302 
"FF_pat\<cdot>r\<cdot>TT = fail" 

303 
"FF_pat\<cdot>r\<cdot>FF = return\<cdot>r" 

304 
by (simp_all add: FF_pat_def) 

305 

16221  306 
subsection {* Match functions for builtin types *} 
307 

16776
a3899ac14a1c
generalized types of monadic operators to class cpo; added match function for UU
huffman
parents:
16758
diff
changeset

308 
defaultsort pcpo 
a3899ac14a1c
generalized types of monadic operators to class cpo; added match function for UU
huffman
parents:
16758
diff
changeset

309 

16221  310 
constdefs 
16776
a3899ac14a1c
generalized types of monadic operators to class cpo; added match function for UU
huffman
parents:
16758
diff
changeset

311 
match_UU :: "'a \<rightarrow> unit maybe" 
a3899ac14a1c
generalized types of monadic operators to class cpo; added match function for UU
huffman
parents:
16758
diff
changeset

312 
"match_UU \<equiv> \<Lambda> x. fail" 
a3899ac14a1c
generalized types of monadic operators to class cpo; added match function for UU
huffman
parents:
16758
diff
changeset

313 

a3899ac14a1c
generalized types of monadic operators to class cpo; added match function for UU
huffman
parents:
16758
diff
changeset

314 
match_cpair :: "'a::cpo \<times> 'b::cpo \<rightarrow> ('a \<times> 'b) maybe" 
16221  315 
"match_cpair \<equiv> csplit\<cdot>(\<Lambda> x y. return\<cdot><x,y>)" 
316 

16551  317 
match_spair :: "'a \<otimes> 'b \<rightarrow> ('a \<times> 'b) maybe" 
318 
"match_spair \<equiv> ssplit\<cdot>(\<Lambda> x y. return\<cdot><x,y>)" 

319 

320 
match_sinl :: "'a \<oplus> 'b \<rightarrow> 'a maybe" 

321 
"match_sinl \<equiv> sscase\<cdot>return\<cdot>(\<Lambda> y. fail)" 

322 

323 
match_sinr :: "'a \<oplus> 'b \<rightarrow> 'b maybe" 

324 
"match_sinr \<equiv> sscase\<cdot>(\<Lambda> x. fail)\<cdot>return" 

325 

16776
a3899ac14a1c
generalized types of monadic operators to class cpo; added match function for UU
huffman
parents:
16758
diff
changeset

326 
match_up :: "'a::cpo u \<rightarrow> 'a maybe" 
16221  327 
"match_up \<equiv> fup\<cdot>return" 
328 

16460
72a08d509d62
added match functions for ONE, TT, and FF; added theorem mplus_fail2
huffman
parents:
16417
diff
changeset

329 
match_ONE :: "one \<rightarrow> unit maybe" 
18094  330 
"match_ONE \<equiv> \<Lambda> ONE. return\<cdot>()" 
331 

16460
72a08d509d62
added match functions for ONE, TT, and FF; added theorem mplus_fail2
huffman
parents:
16417
diff
changeset

332 
match_TT :: "tr \<rightarrow> unit maybe" 
18094  333 
"match_TT \<equiv> \<Lambda> b. If b then return\<cdot>() else fail fi" 
334 

16460
72a08d509d62
added match functions for ONE, TT, and FF; added theorem mplus_fail2
huffman
parents:
16417
diff
changeset

335 
match_FF :: "tr \<rightarrow> unit maybe" 
18094  336 
"match_FF \<equiv> \<Lambda> b. If b then fail else return\<cdot>() fi" 
16460
72a08d509d62
added match functions for ONE, TT, and FF; added theorem mplus_fail2
huffman
parents:
16417
diff
changeset

337 

16776
a3899ac14a1c
generalized types of monadic operators to class cpo; added match function for UU
huffman
parents:
16758
diff
changeset

338 
lemma match_UU_simps [simp]: 
a3899ac14a1c
generalized types of monadic operators to class cpo; added match function for UU
huffman
parents:
16758
diff
changeset

339 
"match_UU\<cdot>x = fail" 
a3899ac14a1c
generalized types of monadic operators to class cpo; added match function for UU
huffman
parents:
16758
diff
changeset

340 
by (simp add: match_UU_def) 
a3899ac14a1c
generalized types of monadic operators to class cpo; added match function for UU
huffman
parents:
16758
diff
changeset

341 

16221  342 
lemma match_cpair_simps [simp]: 
343 
"match_cpair\<cdot><x,y> = return\<cdot><x,y>" 

344 
by (simp add: match_cpair_def) 

345 

16551  346 
lemma match_spair_simps [simp]: 
347 
"\<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> match_spair\<cdot>(:x,y:) = return\<cdot><x,y>" 

348 
"match_spair\<cdot>\<bottom> = \<bottom>" 

349 
by (simp_all add: match_spair_def) 

350 

351 
lemma match_sinl_simps [simp]: 

352 
"x \<noteq> \<bottom> \<Longrightarrow> match_sinl\<cdot>(sinl\<cdot>x) = return\<cdot>x" 

353 
"x \<noteq> \<bottom> \<Longrightarrow> match_sinl\<cdot>(sinr\<cdot>x) = fail" 

354 
"match_sinl\<cdot>\<bottom> = \<bottom>" 

355 
by (simp_all add: match_sinl_def) 

356 

357 
lemma match_sinr_simps [simp]: 

358 
"x \<noteq> \<bottom> \<Longrightarrow> match_sinr\<cdot>(sinr\<cdot>x) = return\<cdot>x" 

359 
"x \<noteq> \<bottom> \<Longrightarrow> match_sinr\<cdot>(sinl\<cdot>x) = fail" 

360 
"match_sinr\<cdot>\<bottom> = \<bottom>" 

361 
by (simp_all add: match_sinr_def) 

362 

16221  363 
lemma match_up_simps [simp]: 
364 
"match_up\<cdot>(up\<cdot>x) = return\<cdot>x" 

365 
"match_up\<cdot>\<bottom> = \<bottom>" 

366 
by (simp_all add: match_up_def) 

367 

16460
72a08d509d62
added match functions for ONE, TT, and FF; added theorem mplus_fail2
huffman
parents:
16417
diff
changeset

368 
lemma match_ONE_simps [simp]: 
72a08d509d62
added match functions for ONE, TT, and FF; added theorem mplus_fail2
huffman
parents:
16417
diff
changeset

369 
"match_ONE\<cdot>ONE = return\<cdot>()" 
72a08d509d62
added match functions for ONE, TT, and FF; added theorem mplus_fail2
huffman
parents:
16417
diff
changeset

370 
"match_ONE\<cdot>\<bottom> = \<bottom>" 
18094  371 
by (simp_all add: match_ONE_def) 
16460
72a08d509d62
added match functions for ONE, TT, and FF; added theorem mplus_fail2
huffman
parents:
16417
diff
changeset

372 

72a08d509d62
added match functions for ONE, TT, and FF; added theorem mplus_fail2
huffman
parents:
16417
diff
changeset

373 
lemma match_TT_simps [simp]: 
72a08d509d62
added match functions for ONE, TT, and FF; added theorem mplus_fail2
huffman
parents:
16417
diff
changeset

374 
"match_TT\<cdot>TT = return\<cdot>()" 
72a08d509d62
added match functions for ONE, TT, and FF; added theorem mplus_fail2
huffman
parents:
16417
diff
changeset

375 
"match_TT\<cdot>FF = fail" 
72a08d509d62
added match functions for ONE, TT, and FF; added theorem mplus_fail2
huffman
parents:
16417
diff
changeset

376 
"match_TT\<cdot>\<bottom> = \<bottom>" 
18094  377 
by (simp_all add: match_TT_def) 
16460
72a08d509d62
added match functions for ONE, TT, and FF; added theorem mplus_fail2
huffman
parents:
16417
diff
changeset

378 

72a08d509d62
added match functions for ONE, TT, and FF; added theorem mplus_fail2
huffman
parents:
16417
diff
changeset

379 
lemma match_FF_simps [simp]: 
72a08d509d62
added match functions for ONE, TT, and FF; added theorem mplus_fail2
huffman
parents:
16417
diff
changeset

380 
"match_FF\<cdot>FF = return\<cdot>()" 
72a08d509d62
added match functions for ONE, TT, and FF; added theorem mplus_fail2
huffman
parents:
16417
diff
changeset

381 
"match_FF\<cdot>TT = fail" 
72a08d509d62
added match functions for ONE, TT, and FF; added theorem mplus_fail2
huffman
parents:
16417
diff
changeset

382 
"match_FF\<cdot>\<bottom> = \<bottom>" 
18094  383 
by (simp_all add: match_FF_def) 
16460
72a08d509d62
added match functions for ONE, TT, and FF; added theorem mplus_fail2
huffman
parents:
16417
diff
changeset

384 

16401
57c35ede00b9
fixrec package now handles mutuallyrecursive definitions
huffman
parents:
16229
diff
changeset

385 
subsection {* Mutual recursion *} 
57c35ede00b9
fixrec package now handles mutuallyrecursive definitions
huffman
parents:
16229
diff
changeset

386 

57c35ede00b9
fixrec package now handles mutuallyrecursive definitions
huffman
parents:
16229
diff
changeset

387 
text {* 
57c35ede00b9
fixrec package now handles mutuallyrecursive definitions
huffman
parents:
16229
diff
changeset

388 
The following rules are used to prove unfolding theorems from 
57c35ede00b9
fixrec package now handles mutuallyrecursive definitions
huffman
parents:
16229
diff
changeset

389 
fixedpoint definitions of mutually recursive functions. 
57c35ede00b9
fixrec package now handles mutuallyrecursive definitions
huffman
parents:
16229
diff
changeset

390 
*} 
57c35ede00b9
fixrec package now handles mutuallyrecursive definitions
huffman
parents:
16229
diff
changeset

391 

57c35ede00b9
fixrec package now handles mutuallyrecursive definitions
huffman
parents:
16229
diff
changeset

392 
lemma cpair_equalI: "\<lbrakk>x \<equiv> cfst\<cdot>p; y \<equiv> csnd\<cdot>p\<rbrakk> \<Longrightarrow> <x,y> \<equiv> p" 
57c35ede00b9
fixrec package now handles mutuallyrecursive definitions
huffman
parents:
16229
diff
changeset

393 
by (simp add: surjective_pairing_Cprod2) 
57c35ede00b9
fixrec package now handles mutuallyrecursive definitions
huffman
parents:
16229
diff
changeset

394 

57c35ede00b9
fixrec package now handles mutuallyrecursive definitions
huffman
parents:
16229
diff
changeset

395 
lemma cpair_eqD1: "<x,y> = <x',y'> \<Longrightarrow> x = x'" 
57c35ede00b9
fixrec package now handles mutuallyrecursive definitions
huffman
parents:
16229
diff
changeset

396 
by simp 
57c35ede00b9
fixrec package now handles mutuallyrecursive definitions
huffman
parents:
16229
diff
changeset

397 

57c35ede00b9
fixrec package now handles mutuallyrecursive definitions
huffman
parents:
16229
diff
changeset

398 
lemma cpair_eqD2: "<x,y> = <x',y'> \<Longrightarrow> y = y'" 
57c35ede00b9
fixrec package now handles mutuallyrecursive definitions
huffman
parents:
16229
diff
changeset

399 
by simp 
57c35ede00b9
fixrec package now handles mutuallyrecursive definitions
huffman
parents:
16229
diff
changeset

400 

16463
342d74ca8815
fixrec shows unsolved subgoals when proofs of rewrites fail
huffman
parents:
16460
diff
changeset

401 
text {* lemma for proving rewrite rules *} 
342d74ca8815
fixrec shows unsolved subgoals when proofs of rewrites fail
huffman
parents:
16460
diff
changeset

402 

342d74ca8815
fixrec shows unsolved subgoals when proofs of rewrites fail
huffman
parents:
16460
diff
changeset

403 
lemma ssubst_lhs: "\<lbrakk>t = s; P s = Q\<rbrakk> \<Longrightarrow> P t = Q" 
342d74ca8815
fixrec shows unsolved subgoals when proofs of rewrites fail
huffman
parents:
16460
diff
changeset

404 
by simp 
342d74ca8815
fixrec shows unsolved subgoals when proofs of rewrites fail
huffman
parents:
16460
diff
changeset

405 

16401
57c35ede00b9
fixrec package now handles mutuallyrecursive definitions
huffman
parents:
16229
diff
changeset

406 
ML {* 
57c35ede00b9
fixrec package now handles mutuallyrecursive definitions
huffman
parents:
16229
diff
changeset

407 
val cpair_equalI = thm "cpair_equalI"; 
57c35ede00b9
fixrec package now handles mutuallyrecursive definitions
huffman
parents:
16229
diff
changeset

408 
val cpair_eqD1 = thm "cpair_eqD1"; 
57c35ede00b9
fixrec package now handles mutuallyrecursive definitions
huffman
parents:
16229
diff
changeset

409 
val cpair_eqD2 = thm "cpair_eqD2"; 
16463
342d74ca8815
fixrec shows unsolved subgoals when proofs of rewrites fail
huffman
parents:
16460
diff
changeset

410 
val ssubst_lhs = thm "ssubst_lhs"; 
16401
57c35ede00b9
fixrec package now handles mutuallyrecursive definitions
huffman
parents:
16229
diff
changeset

411 
*} 
16221  412 

16758  413 
subsection {* Initializing the fixrec package *} 
16221  414 

16229  415 
use "fixrec_package.ML" 
16221  416 

417 
end 