author  huffman 
Fri, 08 Jul 2005 03:12:58 +0200  
changeset 16758  c32334d98fcd 
parent 16754  1b979f8b7e8e 
child 16776  a3899ac14a1c 
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 

15 
types 'a maybe = "one ++ 'a u" 

16 

17 
constdefs 

18 
fail :: "'a maybe" 

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

20 

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

22 
"return \<equiv> sinr oo up" 

23 

24 
lemma maybeE: 

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

26 
apply (unfold fail_def return_def) 

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

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

16754  29 
apply (rule_tac p=y in upE, simp, simp) 
16221  30 
done 
31 

32 
subsection {* Monadic bind operator *} 

33 

34 
constdefs 

35 
bind :: "'a maybe \<rightarrow> ('a \<rightarrow> 'b maybe) \<rightarrow> 'b maybe" 

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

37 

38 
syntax 

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

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

41 

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

43 

44 
nonterminals 

45 
maybebind maybebinds 

46 

47 
syntax 

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

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

50 

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

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

53 

54 
translations 

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

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

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

58 

59 
text {* monad laws *} 

60 

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

62 
by (simp add: bind_def) 

63 

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

65 
by (simp add: bind_def fail_def) 

66 

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

68 
by (simp add: bind_def return_def) 

69 

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

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

72 

73 
lemma bind_assoc [simp]: 

74 
"(do a < m; b < k\<cdot>a; h\<cdot>b) = (do b < (do a < m; k\<cdot>a); h\<cdot>b)" 

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

76 

77 
subsection {* Run operator *} 

78 

79 
constdefs 

80 
run:: "'a maybe \<rightarrow> 'a" 

81 
"run \<equiv> sscase\<cdot>\<bottom>\<cdot>(fup\<cdot>ID)" 

82 

83 
text {* rewrite rules for run *} 

84 

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

86 
by (simp add: run_def) 

87 

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

89 
by (simp add: run_def fail_def) 

90 

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

92 
by (simp add: run_def return_def) 

93 

94 
subsection {* Monad plus operator *} 

95 

96 
constdefs 

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

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

99 

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

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

102 

103 
text {* rewrite rules for mplus *} 

104 

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

106 
by (simp add: mplus_def) 

107 

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

109 
by (simp add: mplus_def fail_def) 

110 

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

112 
by (simp add: mplus_def return_def) 

113 

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

114 
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

115 
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

116 

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

119 

120 
subsection {* Match functions for builtin types *} 

121 

122 
constdefs 

123 
match_cpair :: "'a \<times> 'b \<rightarrow> ('a \<times> 'b) maybe" 

124 
"match_cpair \<equiv> csplit\<cdot>(\<Lambda> x y. return\<cdot><x,y>)" 

125 

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

128 

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

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

131 

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

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

134 

16221  135 
match_up :: "'a u \<rightarrow> 'a maybe" 
136 
"match_up \<equiv> fup\<cdot>return" 

137 

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

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

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

140 

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

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

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

143 

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

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

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

146 

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

149 
by (simp add: match_cpair_def) 

150 

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

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

154 
by (simp_all add: match_spair_def) 

155 

156 
lemma match_sinl_simps [simp]: 

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

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

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

160 
by (simp_all add: match_sinl_def) 

161 

162 
lemma match_sinr_simps [simp]: 

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

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

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

166 
by (simp_all add: match_sinr_def) 

167 

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

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

171 
by (simp_all add: match_up_def) 

172 

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

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

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

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

176 
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

177 

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

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

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

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

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

182 
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

183 

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

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

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

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

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

188 
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

189 

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

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

191 

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

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

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

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

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

196 

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

197 
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

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

199 

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

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

201 
by simp 
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 
lemma cpair_eqD2: "<x,y> = <x',y'> \<Longrightarrow> y = y'" 
57c35ede00b9
fixrec package now handles mutuallyrecursive definitions
huffman
parents:
16229
diff
changeset

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

205 

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

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

207 

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

208 
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

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

210 

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

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

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

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

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

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

216 
*} 
16221  217 

16758  218 
subsection {* Initializing the fixrec package *} 
16221  219 

16229  220 
use "fixrec_package.ML" 
16221  221 

222 
end 