author  huffman 
Tue, 12 Jul 2005 18:44:32 +0200  
changeset 16779  ac1dc3d4746a 
parent 16776  a3899ac14a1c 
child 18094  404f298220af 
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 

34 
subsection {* Monadic bind operator *} 

35 

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 

41 
"_bind" :: "'a maybe \<Rightarrow> ('a \<rightarrow> 'b maybe) \<Rightarrow> 'b maybe" 

42 
("(_ >>= _)" [50, 51] 50) 

43 

44 
translations "m >>= k" == "bind\<cdot>m\<cdot>k" 

45 

46 
nonterminals 

47 
maybebind maybebinds 

48 

49 
syntax 

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

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

52 

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

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

55 

56 
translations 

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

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

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

60 

61 
text {* monad laws *} 

62 

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

64 
by (simp add: bind_def) 

65 

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

67 
by (simp add: bind_def fail_def) 

68 

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

70 
by (simp add: bind_def return_def) 

71 

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

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

74 

75 
lemma bind_assoc [simp]: 

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

79 
subsection {* Run operator *} 

80 

81 
constdefs 

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

82 
run:: "'a::pcpo maybe \<rightarrow> 'a" 
16221  83 
"run \<equiv> sscase\<cdot>\<bottom>\<cdot>(fup\<cdot>ID)" 
84 

85 
text {* rewrite rules for run *} 

86 

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

88 
by (simp add: run_def) 

89 

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

91 
by (simp add: run_def fail_def) 

92 

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

94 
by (simp add: run_def return_def) 

95 

96 
subsection {* Monad plus operator *} 

97 

98 
constdefs 

99 
mplus :: "'a maybe \<rightarrow> 'a maybe \<rightarrow> 'a maybe" 

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

101 

102 
syntax "+++" :: "'a maybe \<Rightarrow> 'a maybe \<Rightarrow> 'a maybe" (infixr 65) 

103 
translations "x +++ y" == "mplus\<cdot>x\<cdot>y" 

104 

105 
text {* rewrite rules for mplus *} 

106 

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

108 
by (simp add: mplus_def) 

109 

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

111 
by (simp add: mplus_def fail_def) 

112 

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

114 
by (simp add: mplus_def return_def) 

115 

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

116 
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

117 
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

118 

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

121 

122 
subsection {* Match functions for builtin types *} 

123 

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

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

125 

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

127 
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

128 
"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

129 

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

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

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

135 

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

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

138 

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

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

141 

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

142 
match_up :: "'a::cpo u \<rightarrow> 'a maybe" 
16221  143 
"match_up \<equiv> fup\<cdot>return" 
144 

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

145 
match_ONE :: "one \<rightarrow> unit maybe" 
72a08d509d62
added match functions for ONE, TT, and FF; added theorem mplus_fail2
huffman
parents:
16417
diff
changeset

146 
"match_ONE \<equiv> flift1 (\<lambda>u. return\<cdot>())" 
72a08d509d62
added match functions for ONE, TT, and FF; added theorem mplus_fail2
huffman
parents:
16417
diff
changeset

147 

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

148 
match_TT :: "tr \<rightarrow> unit maybe" 
72a08d509d62
added match functions for ONE, TT, and FF; added theorem mplus_fail2
huffman
parents:
16417
diff
changeset

149 
"match_TT \<equiv> flift1 (\<lambda>b. if b then return\<cdot>() else fail)" 
72a08d509d62
added match functions for ONE, TT, and FF; added theorem mplus_fail2
huffman
parents:
16417
diff
changeset

150 

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

151 
match_FF :: "tr \<rightarrow> unit maybe" 
72a08d509d62
added match functions for ONE, TT, and FF; added theorem mplus_fail2
huffman
parents:
16417
diff
changeset

152 
"match_FF \<equiv> flift1 (\<lambda>b. if b then fail else return\<cdot>())" 
72a08d509d62
added match functions for ONE, TT, and FF; added theorem mplus_fail2
huffman
parents:
16417
diff
changeset

153 

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

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

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

156 
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

157 

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

160 
by (simp add: match_cpair_def) 

161 

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

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

165 
by (simp_all add: match_spair_def) 

166 

167 
lemma match_sinl_simps [simp]: 

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

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

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

171 
by (simp_all add: match_sinl_def) 

172 

173 
lemma match_sinr_simps [simp]: 

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

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

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

177 
by (simp_all add: match_sinr_def) 

178 

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

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

182 
by (simp_all add: match_up_def) 

183 

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

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

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

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

187 
by (simp_all add: ONE_def match_ONE_def) 
72a08d509d62
added match functions for ONE, TT, and FF; added theorem mplus_fail2
huffman
parents:
16417
diff
changeset

188 

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

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

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

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

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

193 
by (simp_all add: TT_def FF_def match_TT_def) 
72a08d509d62
added match functions for ONE, TT, and FF; added theorem mplus_fail2
huffman
parents:
16417
diff
changeset

194 

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

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

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

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

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

199 
by (simp_all add: TT_def FF_def match_FF_def) 
72a08d509d62
added match functions for ONE, TT, and FF; added theorem mplus_fail2
huffman
parents:
16417
diff
changeset

200 

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

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

202 

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

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

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

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

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

207 

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

208 
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

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

210 

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

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

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

213 

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

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

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

216 

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

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

218 

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

219 
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

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

221 

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

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

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

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

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

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

227 
*} 
16221  228 

16758  229 
subsection {* Initializing the fixrec package *} 
16221  230 

16229  231 
use "fixrec_package.ML" 
16221  232 

233 
end 