author  huffman 
Mon, 07 Nov 2005 23:33:01 +0100  
changeset 18112  dc1d6f588204 
parent 18110  08ec4f1f116d 
child 18293  4eaa654c92f2 
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 

18112
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

141 
lemma run_fatbar1: "m\<cdot>x = \<bottom> \<Longrightarrow> run\<cdot>((m \<parallel> ms)\<cdot>x) = \<bottom>" 
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

142 
by (simp add: fatbar_def) 
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

143 

dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

144 
lemma run_fatbar2: "m\<cdot>x = fail \<Longrightarrow> run\<cdot>((m \<parallel> ms)\<cdot>x) = run\<cdot>(ms\<cdot>x)" 
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

145 
by (simp add: fatbar_def) 
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

146 

dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

147 
lemma run_fatbar3: "m\<cdot>x = return\<cdot>y \<Longrightarrow> run\<cdot>((m \<parallel> ms)\<cdot>x) = y" 
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

148 
by (simp add: fatbar_def) 
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

149 

dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

150 
lemmas run_fatbar_simps [simp] = run_fatbar1 run_fatbar2 run_fatbar3 
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

151 

18097  152 
subsection {* Pattern combinators *} 
153 

18112
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

154 
types ('a,'b,'c) pat = "'b \<rightarrow> 'a \<rightarrow> 'c maybe" 
18097  155 

156 
constdefs 

18112
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

157 
wild_pat :: "('a, 'b, 'b) pat" 
18097  158 
"wild_pat \<equiv> \<Lambda> r a. return\<cdot>r" 
159 

18112
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

160 
var_pat :: "('a, 'a \<rightarrow> 'b, 'b) pat" 
18097  161 
"var_pat \<equiv> \<Lambda> r a. return\<cdot>(r\<cdot>a)" 
162 

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

164 
by (simp add: wild_pat_def) 

165 

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

167 
by (simp add: var_pat_def) 

168 

169 
subsection {* Case syntax *} 

170 

171 
nonterminals 

172 
Case_syn Cases_syn 

173 

174 
syntax 

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

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

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

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

179 

180 
syntax (xsymbols) 

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

182 

18112
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

183 
text {* Intermediate tags for parsing/printing *} 
18097  184 
syntax 
18112
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

185 
"_pat" :: "'a" 
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

186 
"_var" :: "'a" 
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

187 
"_match" :: "'a" 
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

188 

dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

189 
text {* Parsing Case expressions *} 
18097  190 

191 
translations 

18112
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

192 
"_Case_syntax x cs" => "run\<cdot>(cs\<cdot>x)" 
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

193 
"_Case2 c cs" => "fatbar\<cdot>c\<cdot>cs" 
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

194 
"_Case1 p r" => "_match (_var p) r" 
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

195 
"_var _" => "wild_pat" 
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

196 

dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

197 
parse_translation {* 
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

198 
let 
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

199 
fun capp (t,u) = Syntax.const "Rep_CFun" $ t $ u; 
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

200 
fun cabs (x,t) = (snd (mk_binder_tr ("_cabs", "Abs_CFun"))) [x,t]; 
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

201 

dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

202 
fun get_vars (Const ("_var",_) $ x) = [x] 
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

203 
 get_vars (t $ u) = get_vars t @ get_vars u 
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

204 
 get_vars t = []; 
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

205 

dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

206 
fun rem_vars (Const ("_var",_) $ x) = Syntax.const "var_pat" 
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

207 
 rem_vars (t $ u) = rem_vars t $ rem_vars u 
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

208 
 rem_vars t = t; 
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

209 

dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

210 
fun match_tr [pat, rhs] = 
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

211 
capp (rem_vars pat, foldr cabs rhs (get_vars pat)) 
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

212 
 match_tr ts = raise TERM ("match_tr", ts); 
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

213 

dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

214 
in [("_match", match_tr)] end; 
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

215 
*} 
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

216 

dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

217 
text {* Printing Case expressions *} 
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

218 

dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

219 
translations 
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

220 
"_" <= "_pat wild_pat" 
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

221 
"x" <= "_pat (_var x)" 
18097  222 

18112
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

223 
print_translation {* 
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

224 
let 
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

225 
fun dest_cabs (Const ("Abs_CFun",_) $ t) = 
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

226 
let val abs = case t of Abs abs => abs 
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

227 
 _ => ("x", dummyT, incr_boundvars 1 t $ Bound 0); 
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

228 
in atomic_abs_tr' abs end 
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

229 
 dest_cabs _ = raise Match; (* too few vars: abort translation *) 
18097  230 

18112
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

231 
fun put_vars (Const ("var_pat",_), rhs) = 
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

232 
let val (x, rhs') = dest_cabs rhs; 
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

233 
in (Syntax.const "_var" $ x, rhs') end 
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

234 
 put_vars (t $ u, rhs) = 
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

235 
let 
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

236 
val (t', rhs') = put_vars (t,rhs); 
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

237 
val (u', rhs'') = put_vars (u,rhs'); 
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

238 
in (t' $ u', rhs'') end 
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

239 
 put_vars (t, rhs) = (t, rhs); 
18097  240 

18112
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

241 
fun Case1_tr' (_ $ pat $ rhs) = let 
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

242 
val (pat', rhs') = put_vars (pat, rhs); 
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

243 
in Syntax.const "_Case1" $ (Syntax.const "_pat" $ pat') $ rhs' end; 
18097  244 

18112
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

245 
fun Case2_tr' (_ $ (_ $ Const ("fatbar",_) $ m) $ ms) = 
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

246 
Syntax.const "_Case2" $ Case1_tr' m $ Case2_tr' ms 
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

247 
 Case2_tr' t = Case1_tr' t; 
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

248 

dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

249 
fun Case_syntax_tr' [Const ("run",_), _ $ ms $ x] = 
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

250 
Syntax.const "_Case_syntax" $ x $ Case2_tr' ms; 
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

251 

dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

252 
in [("Rep_CFun", Case_syntax_tr')] end; 
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

253 
*} 
18097  254 

255 
subsection {* Pattern combinators for builtin types *} 

256 

257 
constdefs 

18112
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

258 
cpair_pat :: "('a, _, _) pat \<Rightarrow> ('b, _, _) pat \<Rightarrow> ('a \<times> 'b, _, _) pat" 
18097  259 
"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)" 
260 

18112
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

261 
spair_pat :: "(_, _, _) pat \<Rightarrow> (_, _, _) pat \<Rightarrow> (_, _, _) pat" 
18097  262 
"spair_pat p1 p2 \<equiv> \<Lambda> r (:x,y:). cpair_pat p1 p2\<cdot>r\<cdot>\<langle>x,y\<rangle>" 
263 

18112
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

264 
sinl_pat :: "(_, _, _) pat \<Rightarrow> (_, _, _) pat" 
18097  265 
"sinl_pat p \<equiv> \<Lambda> r a. case a of sinl\<cdot>x \<Rightarrow> p\<cdot>r\<cdot>x  sinr\<cdot>y \<Rightarrow> fail" 
266 

18112
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

267 
sinr_pat :: "(_, _, _) pat \<Rightarrow> (_, _, _) pat" 
18097  268 
"sinr_pat p \<equiv> \<Lambda> r a. case a of sinl\<cdot>x \<Rightarrow> fail  sinr\<cdot>y \<Rightarrow> p\<cdot>r\<cdot>y" 
269 

18112
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

270 
up_pat :: "('a, _, _) pat \<Rightarrow> ('a u, _, _) pat" 
18097  271 
"up_pat p \<equiv> \<Lambda> r a. case a of up\<cdot>x \<Rightarrow> p\<cdot>r\<cdot>x" 
272 

18112
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

273 
Def_pat :: "'a::type \<Rightarrow> ('a lift, _, _) pat" 
18097  274 
"Def_pat x \<equiv> \<Lambda> r. FLIFT y. if x = y then return\<cdot>r else fail" 
275 

18112
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

276 
ONE_pat :: "(one, _, _) pat" 
18097  277 
"ONE_pat \<equiv> \<Lambda> r ONE. return\<cdot>r" 
278 

18112
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

279 
TT_pat :: "(tr, _, _) pat" 
18097  280 
"TT_pat \<equiv> \<Lambda> r b. If b then return\<cdot>r else fail fi" 
281 

18112
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

282 
FF_pat :: "(tr, _, _) pat" 
18097  283 
"FF_pat \<equiv> \<Lambda> r b. If b then fail else return\<cdot>r fi" 
284 

18112
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

285 
text {* Parse translations *} 
18097  286 
translations 
18112
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

287 
"_var (cpair\<cdot>p1\<cdot>p2)" => "cpair_pat (_var p1) (_var p2)" 
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

288 
"_var (spair\<cdot>p1\<cdot>p2)" => "spair_pat (_var p1) (_var p2)" 
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

289 
"_var (sinl\<cdot>p1)" => "sinl_pat (_var p1)" 
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

290 
"_var (sinr\<cdot>p1)" => "sinr_pat (_var p1)" 
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

291 
"_var (up\<cdot>p1)" => "up_pat (_var p1)" 
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

292 
"_var (Def x)" => "Def_pat x" 
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

293 
"_var ONE" => "ONE_pat" 
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

294 
"_var TT" => "TT_pat" 
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

295 
"_var FF" => "FF_pat" 
18097  296 

18112
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

297 
text {* Print translations *} 
18097  298 
translations 
18112
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

299 
"cpair\<cdot>(_pat p1)\<cdot>(_pat p2)" <= "_pat (cpair_pat p1 p2)" 
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

300 
"spair\<cdot>(_pat p1)\<cdot>(_pat p2)" <= "_pat (spair_pat p1 p2)" 
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

301 
"sinl\<cdot>(_pat p1)" <= "_pat (sinl_pat p1)" 
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

302 
"sinr\<cdot>(_pat p1)" <= "_pat (sinr_pat p1)" 
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

303 
"up\<cdot>(_pat p1)" <= "_pat (up_pat p1)" 
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

304 
"Def x" <= "_pat (Def_pat x)" 
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

305 
"TT" <= "_pat (TT_pat)" 
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

306 
"FF" <= "_pat (FF_pat)" 
18097  307 

308 
lemma cpair_pat_simps [simp]: 

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

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

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

312 
by (simp_all add: cpair_pat_def) 

313 

314 
lemma spair_pat_simps [simp]: 

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

316 
"\<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>" 

317 
by (simp_all add: spair_pat_def) 

318 

319 
lemma sinl_pat_simps [simp]: 

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

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

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

323 
by (simp_all add: sinl_pat_def) 

324 

325 
lemma sinr_pat_simps [simp]: 

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

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

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

329 
by (simp_all add: sinr_pat_def) 

330 

331 
lemma up_pat_simps [simp]: 

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

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

334 
by (simp_all add: up_pat_def) 

335 

336 
lemma Def_pat_simps [simp]: 

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

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

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

340 
by (simp_all add: Def_pat_def) 

341 

342 
lemma ONE_pat_simps [simp]: 

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

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

345 
by (simp_all add: ONE_pat_def) 

346 

347 
lemma TT_pat_simps [simp]: 

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

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

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

351 
by (simp_all add: TT_pat_def) 

352 

353 
lemma FF_pat_simps [simp]: 

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

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

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

357 
by (simp_all add: FF_pat_def) 

358 

18112
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

359 
subsection {* Aspatterns *} 
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

360 

dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

361 
syntax 
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

362 
"_as_pattern" :: "['a, 'a] \<Rightarrow> 'a" (* infixr "as" 10 *) 
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

363 
(* TODO: choose a nonambiguous syntax for aspatterns *) 
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

364 

dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

365 
constdefs 
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

366 
as_pat :: "('a,'b,'c) pat \<Rightarrow> ('a,'c,'d) pat \<Rightarrow> ('a,'b,'d) pat" 
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

367 
"as_pat p1 p2 \<equiv> \<Lambda> r a. cpair_pat p1 p2\<cdot>r\<cdot>\<langle>a, a\<rangle>" 
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

368 

dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

369 
translations 
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

370 
"_var (_as_pattern p1 p2)" => "as_pat (_var p1) (_var p2)" 
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

371 
"_as_pattern (_pat p1) (_pat p2)" <= "_pat (as_pat p1 p2)" 
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

372 

dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

373 
lemma as_pat [simp]: "as_pat p1 p2\<cdot>r\<cdot>a = cpair_pat p1 p2\<cdot>r\<cdot>\<langle>a, a\<rangle>" 
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

374 
by (simp add: as_pat_def) 
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

375 

16221  376 
subsection {* Match functions for builtin types *} 
377 

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

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

379 

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

381 
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

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

383 

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

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

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

389 

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

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

392 

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

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

395 

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

396 
match_up :: "'a::cpo u \<rightarrow> 'a maybe" 
16221  397 
"match_up \<equiv> fup\<cdot>return" 
398 

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

399 
match_ONE :: "one \<rightarrow> unit maybe" 
18094  400 
"match_ONE \<equiv> \<Lambda> ONE. return\<cdot>()" 
401 

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

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

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

405 
match_FF :: "tr \<rightarrow> unit maybe" 
18094  406 
"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

407 

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

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

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

410 
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

411 

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

414 
by (simp add: match_cpair_def) 

415 

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

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

419 
by (simp_all add: match_spair_def) 

420 

421 
lemma match_sinl_simps [simp]: 

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

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

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

425 
by (simp_all add: match_sinl_def) 

426 

427 
lemma match_sinr_simps [simp]: 

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

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

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

431 
by (simp_all add: match_sinr_def) 

432 

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

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

436 
by (simp_all add: match_up_def) 

437 

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

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

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

440 
"match_ONE\<cdot>\<bottom> = \<bottom>" 
18094  441 
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

442 

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

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

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

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

446 
"match_TT\<cdot>\<bottom> = \<bottom>" 
18094  447 
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

448 

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

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

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

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

452 
"match_FF\<cdot>\<bottom> = \<bottom>" 
18094  453 
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

454 

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

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

456 

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

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

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

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

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

461 

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

462 
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

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

464 

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

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

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

467 

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

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

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

470 

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

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

472 

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

473 
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

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

475 

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

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

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

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

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

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

481 
*} 
16221  482 

16758  483 
subsection {* Initializing the fixrec package *} 
16221  484 

16229  485 
use "fixrec_package.ML" 
16221  486 

487 
end 