author  berghofe 
Wed, 07 May 2008 10:56:35 +0200  
changeset 26793  e36a92ff543e 
parent 26013  8764a1f1253b 
child 29270  0eade173f77e 
permissions  rwrr 
7700  1 
(* Title: HOL/Inductive.thy 
2 
ID: $Id$ 

10402  3 
Author: Markus Wenzel, TU Muenchen 
11688  4 
*) 
10727  5 

24915  6 
header {* KnasterTarski Fixpoint Theorem and inductive definitions *} 
1187  7 

15131  8 
theory Inductive 
24915  9 
imports Lattices Sum_Type 
16417  10 
uses 
10402  11 
("Tools/inductive_package.ML") 
24625
0398a5e802d3
separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
24349
diff
changeset

12 
"Tools/dseq.ML" 
12437
6d4e02b6dd43
Moved code generator setup from Recdef to Inductive.
berghofe
parents:
12023
diff
changeset

13 
("Tools/inductive_codegen.ML") 
10402  14 
("Tools/datatype_aux.ML") 
15 
("Tools/datatype_prop.ML") 

16 
("Tools/datatype_rep_proofs.ML") 

17 
("Tools/datatype_abs_proofs.ML") 

22783  18 
("Tools/datatype_case.ML") 
10402  19 
("Tools/datatype_package.ML") 
25557  20 
("Tools/old_primrec_package.ML") 
15131  21 
("Tools/primrec_package.ML") 
25534
d0b74fdd6067
simplified infrastructure for code generator operational equality
haftmann
parents:
25510
diff
changeset

22 
("Tools/datatype_codegen.ML") 
15131  23 
begin 
10727  24 

24915  25 
subsection {* Least and greatest fixed points *} 
26 

26013
8764a1f1253b
Theorem Inductive.lfp_ordinal_induct generalized to complete lattices
haftmann
parents:
25557
diff
changeset

27 
context complete_lattice 
8764a1f1253b
Theorem Inductive.lfp_ordinal_induct generalized to complete lattices
haftmann
parents:
25557
diff
changeset

28 
begin 
8764a1f1253b
Theorem Inductive.lfp_ordinal_induct generalized to complete lattices
haftmann
parents:
25557
diff
changeset

29 

24915  30 
definition 
26013
8764a1f1253b
Theorem Inductive.lfp_ordinal_induct generalized to complete lattices
haftmann
parents:
25557
diff
changeset

31 
lfp :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a" where 
24915  32 
"lfp f = Inf {u. f u \<le> u}" {*least fixed point*} 
33 

34 
definition 

26013
8764a1f1253b
Theorem Inductive.lfp_ordinal_induct generalized to complete lattices
haftmann
parents:
25557
diff
changeset

35 
gfp :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a" where 
24915  36 
"gfp f = Sup {u. u \<le> f u}" {*greatest fixed point*} 
37 

38 

39 
subsection{* Proof of KnasterTarski Theorem using @{term lfp} *} 

40 

41 
text{*@{term "lfp f"} is the least upper bound of 

42 
the set @{term "{u. f(u) \<le> u}"} *} 

43 

44 
lemma lfp_lowerbound: "f A \<le> A ==> lfp f \<le> A" 

45 
by (auto simp add: lfp_def intro: Inf_lower) 

46 

47 
lemma lfp_greatest: "(!!u. f u \<le> u ==> A \<le> u) ==> A \<le> lfp f" 

48 
by (auto simp add: lfp_def intro: Inf_greatest) 

49 

26013
8764a1f1253b
Theorem Inductive.lfp_ordinal_induct generalized to complete lattices
haftmann
parents:
25557
diff
changeset

50 
end 
8764a1f1253b
Theorem Inductive.lfp_ordinal_induct generalized to complete lattices
haftmann
parents:
25557
diff
changeset

51 

24915  52 
lemma lfp_lemma2: "mono f ==> f (lfp f) \<le> lfp f" 
53 
by (iprover intro: lfp_greatest order_trans monoD lfp_lowerbound) 

54 

55 
lemma lfp_lemma3: "mono f ==> lfp f \<le> f (lfp f)" 

56 
by (iprover intro: lfp_lemma2 monoD lfp_lowerbound) 

57 

58 
lemma lfp_unfold: "mono f ==> lfp f = f (lfp f)" 

59 
by (iprover intro: order_antisym lfp_lemma2 lfp_lemma3) 

60 

61 
lemma lfp_const: "lfp (\<lambda>x. t) = t" 

62 
by (rule lfp_unfold) (simp add:mono_def) 

63 

64 

65 
subsection {* General induction rules for least fixed points *} 

66 

67 
theorem lfp_induct: 

68 
assumes mono: "mono f" and ind: "f (inf (lfp f) P) <= P" 

69 
shows "lfp f <= P" 

70 
proof  

71 
have "inf (lfp f) P <= lfp f" by (rule inf_le1) 

72 
with mono have "f (inf (lfp f) P) <= f (lfp f)" .. 

73 
also from mono have "f (lfp f) = lfp f" by (rule lfp_unfold [symmetric]) 

74 
finally have "f (inf (lfp f) P) <= lfp f" . 

75 
from this and ind have "f (inf (lfp f) P) <= inf (lfp f) P" by (rule le_infI) 

76 
hence "lfp f <= inf (lfp f) P" by (rule lfp_lowerbound) 

77 
also have "inf (lfp f) P <= P" by (rule inf_le2) 

78 
finally show ?thesis . 

79 
qed 

80 

81 
lemma lfp_induct_set: 

82 
assumes lfp: "a: lfp(f)" 

83 
and mono: "mono(f)" 

84 
and indhyp: "!!x. [ x: f(lfp(f) Int {x. P(x)}) ] ==> P(x)" 

85 
shows "P(a)" 

86 
by (rule lfp_induct [THEN subsetD, THEN CollectD, OF mono _ lfp]) 

87 
(auto simp: inf_set_eq intro: indhyp) 

88 

26013
8764a1f1253b
Theorem Inductive.lfp_ordinal_induct generalized to complete lattices
haftmann
parents:
25557
diff
changeset

89 
lemma lfp_ordinal_induct: 
8764a1f1253b
Theorem Inductive.lfp_ordinal_induct generalized to complete lattices
haftmann
parents:
25557
diff
changeset

90 
fixes f :: "'a\<Colon>complete_lattice \<Rightarrow> 'a" 
8764a1f1253b
Theorem Inductive.lfp_ordinal_induct generalized to complete lattices
haftmann
parents:
25557
diff
changeset

91 
assumes mono: "mono f" 
8764a1f1253b
Theorem Inductive.lfp_ordinal_induct generalized to complete lattices
haftmann
parents:
25557
diff
changeset

92 
and P_f: "\<And>S. P S \<Longrightarrow> P (f S)" 
8764a1f1253b
Theorem Inductive.lfp_ordinal_induct generalized to complete lattices
haftmann
parents:
25557
diff
changeset

93 
and P_Union: "\<And>M. \<forall>S\<in>M. P S \<Longrightarrow> P (Sup M)" 
8764a1f1253b
Theorem Inductive.lfp_ordinal_induct generalized to complete lattices
haftmann
parents:
25557
diff
changeset

94 
shows "P (lfp f)" 
8764a1f1253b
Theorem Inductive.lfp_ordinal_induct generalized to complete lattices
haftmann
parents:
25557
diff
changeset

95 
proof  
8764a1f1253b
Theorem Inductive.lfp_ordinal_induct generalized to complete lattices
haftmann
parents:
25557
diff
changeset

96 
let ?M = "{S. S \<le> lfp f \<and> P S}" 
8764a1f1253b
Theorem Inductive.lfp_ordinal_induct generalized to complete lattices
haftmann
parents:
25557
diff
changeset

97 
have "P (Sup ?M)" using P_Union by simp 
8764a1f1253b
Theorem Inductive.lfp_ordinal_induct generalized to complete lattices
haftmann
parents:
25557
diff
changeset

98 
also have "Sup ?M = lfp f" 
8764a1f1253b
Theorem Inductive.lfp_ordinal_induct generalized to complete lattices
haftmann
parents:
25557
diff
changeset

99 
proof (rule antisym) 
8764a1f1253b
Theorem Inductive.lfp_ordinal_induct generalized to complete lattices
haftmann
parents:
25557
diff
changeset

100 
show "Sup ?M \<le> lfp f" by (blast intro: Sup_least) 
8764a1f1253b
Theorem Inductive.lfp_ordinal_induct generalized to complete lattices
haftmann
parents:
25557
diff
changeset

101 
hence "f (Sup ?M) \<le> f (lfp f)" by (rule mono [THEN monoD]) 
8764a1f1253b
Theorem Inductive.lfp_ordinal_induct generalized to complete lattices
haftmann
parents:
25557
diff
changeset

102 
hence "f (Sup ?M) \<le> lfp f" using mono [THEN lfp_unfold] by simp 
8764a1f1253b
Theorem Inductive.lfp_ordinal_induct generalized to complete lattices
haftmann
parents:
25557
diff
changeset

103 
hence "f (Sup ?M) \<in> ?M" using P_f P_Union by simp 
8764a1f1253b
Theorem Inductive.lfp_ordinal_induct generalized to complete lattices
haftmann
parents:
25557
diff
changeset

104 
hence "f (Sup ?M) \<le> Sup ?M" by (rule Sup_upper) 
8764a1f1253b
Theorem Inductive.lfp_ordinal_induct generalized to complete lattices
haftmann
parents:
25557
diff
changeset

105 
thus "lfp f \<le> Sup ?M" by (rule lfp_lowerbound) 
8764a1f1253b
Theorem Inductive.lfp_ordinal_induct generalized to complete lattices
haftmann
parents:
25557
diff
changeset

106 
qed 
8764a1f1253b
Theorem Inductive.lfp_ordinal_induct generalized to complete lattices
haftmann
parents:
25557
diff
changeset

107 
finally show ?thesis . 
8764a1f1253b
Theorem Inductive.lfp_ordinal_induct generalized to complete lattices
haftmann
parents:
25557
diff
changeset

108 
qed 
8764a1f1253b
Theorem Inductive.lfp_ordinal_induct generalized to complete lattices
haftmann
parents:
25557
diff
changeset

109 

8764a1f1253b
Theorem Inductive.lfp_ordinal_induct generalized to complete lattices
haftmann
parents:
25557
diff
changeset

110 
lemma lfp_ordinal_induct_set: 
24915  111 
assumes mono: "mono f" 
112 
and P_f: "!!S. P S ==> P(f S)" 

113 
and P_Union: "!!M. !S:M. P S ==> P(Union M)" 

114 
shows "P(lfp f)" 

26793
e36a92ff543e
Instantiated some rules to avoid problems with HO unification.
berghofe
parents:
26013
diff
changeset

115 
using assms unfolding Sup_set_eq [symmetric] 
e36a92ff543e
Instantiated some rules to avoid problems with HO unification.
berghofe
parents:
26013
diff
changeset

116 
by (rule lfp_ordinal_induct [where P=P]) 
24915  117 

118 

119 
text{*Definition forms of @{text lfp_unfold} and @{text lfp_induct}, 

120 
to control unfolding*} 

121 

122 
lemma def_lfp_unfold: "[ h==lfp(f); mono(f) ] ==> h = f(h)" 

123 
by (auto intro!: lfp_unfold) 

124 

125 
lemma def_lfp_induct: 

126 
"[ A == lfp(f); mono(f); 

127 
f (inf A P) \<le> P 

128 
] ==> A \<le> P" 

129 
by (blast intro: lfp_induct) 

130 

131 
lemma def_lfp_induct_set: 

132 
"[ A == lfp(f); mono(f); a:A; 

133 
!!x. [ x: f(A Int {x. P(x)}) ] ==> P(x) 

134 
] ==> P(a)" 

135 
by (blast intro: lfp_induct_set) 

136 

137 
(*Monotonicity of lfp!*) 

138 
lemma lfp_mono: "(!!Z. f Z \<le> g Z) ==> lfp f \<le> lfp g" 

139 
by (rule lfp_lowerbound [THEN lfp_greatest], blast intro: order_trans) 

140 

141 

142 
subsection {* Proof of KnasterTarski Theorem using @{term gfp} *} 

143 

144 
text{*@{term "gfp f"} is the greatest lower bound of 

145 
the set @{term "{u. u \<le> f(u)}"} *} 

146 

147 
lemma gfp_upperbound: "X \<le> f X ==> X \<le> gfp f" 

148 
by (auto simp add: gfp_def intro: Sup_upper) 

149 

150 
lemma gfp_least: "(!!u. u \<le> f u ==> u \<le> X) ==> gfp f \<le> X" 

151 
by (auto simp add: gfp_def intro: Sup_least) 

152 

153 
lemma gfp_lemma2: "mono f ==> gfp f \<le> f (gfp f)" 

154 
by (iprover intro: gfp_least order_trans monoD gfp_upperbound) 

155 

156 
lemma gfp_lemma3: "mono f ==> f (gfp f) \<le> gfp f" 

157 
by (iprover intro: gfp_lemma2 monoD gfp_upperbound) 

158 

159 
lemma gfp_unfold: "mono f ==> gfp f = f (gfp f)" 

160 
by (iprover intro: order_antisym gfp_lemma2 gfp_lemma3) 

161 

162 

163 
subsection {* Coinduction rules for greatest fixed points *} 

164 

165 
text{*weak version*} 

166 
lemma weak_coinduct: "[ a: X; X \<subseteq> f(X) ] ==> a : gfp(f)" 

167 
by (rule gfp_upperbound [THEN subsetD], auto) 

168 

169 
lemma weak_coinduct_image: "!!X. [ a : X; g`X \<subseteq> f (g`X) ] ==> g a : gfp f" 

170 
apply (erule gfp_upperbound [THEN subsetD]) 

171 
apply (erule imageI) 

172 
done 

173 

174 
lemma coinduct_lemma: 

175 
"[ X \<le> f (sup X (gfp f)); mono f ] ==> sup X (gfp f) \<le> f (sup X (gfp f))" 

176 
apply (frule gfp_lemma2) 

177 
apply (drule mono_sup) 

178 
apply (rule le_supI) 

179 
apply assumption 

180 
apply (rule order_trans) 

181 
apply (rule order_trans) 

182 
apply assumption 

183 
apply (rule sup_ge2) 

184 
apply assumption 

185 
done 

186 

187 
text{*strong version, thanks to Coen and Frost*} 

188 
lemma coinduct_set: "[ mono(f); a: X; X \<subseteq> f(X Un gfp(f)) ] ==> a : gfp(f)" 

189 
by (blast intro: weak_coinduct [OF _ coinduct_lemma, simplified sup_set_eq]) 

190 

191 
lemma coinduct: "[ mono(f); X \<le> f (sup X (gfp f)) ] ==> X \<le> gfp(f)" 

192 
apply (rule order_trans) 

193 
apply (rule sup_ge1) 

194 
apply (erule gfp_upperbound [OF coinduct_lemma]) 

195 
apply assumption 

196 
done 

197 

198 
lemma gfp_fun_UnI2: "[ mono(f); a: gfp(f) ] ==> a: f(X Un gfp(f))" 

199 
by (blast dest: gfp_lemma2 mono_Un) 

200 

201 

202 
subsection {* Even Stronger Coinduction Rule, by Martin Coen *} 

203 

204 
text{* Weakens the condition @{term "X \<subseteq> f(X)"} to one expressed using both 

205 
@{term lfp} and @{term gfp}*} 

206 

207 
lemma coinduct3_mono_lemma: "mono(f) ==> mono(%x. f(x) Un X Un B)" 

208 
by (iprover intro: subset_refl monoI Un_mono monoD) 

209 

210 
lemma coinduct3_lemma: 

211 
"[ X \<subseteq> f(lfp(%x. f(x) Un X Un gfp(f))); mono(f) ] 

212 
==> lfp(%x. f(x) Un X Un gfp(f)) \<subseteq> f(lfp(%x. f(x) Un X Un gfp(f)))" 

213 
apply (rule subset_trans) 

214 
apply (erule coinduct3_mono_lemma [THEN lfp_lemma3]) 

215 
apply (rule Un_least [THEN Un_least]) 

216 
apply (rule subset_refl, assumption) 

217 
apply (rule gfp_unfold [THEN equalityD1, THEN subset_trans], assumption) 

26793
e36a92ff543e
Instantiated some rules to avoid problems with HO unification.
berghofe
parents:
26013
diff
changeset

218 
apply (rule monoD [where f=f], assumption) 
24915  219 
apply (subst coinduct3_mono_lemma [THEN lfp_unfold], auto) 
220 
done 

221 

222 
lemma coinduct3: 

223 
"[ mono(f); a:X; X \<subseteq> f(lfp(%x. f(x) Un X Un gfp(f))) ] ==> a : gfp(f)" 

224 
apply (rule coinduct3_lemma [THEN [2] weak_coinduct]) 

225 
apply (rule coinduct3_mono_lemma [THEN lfp_unfold, THEN ssubst], auto) 

226 
done 

227 

228 

229 
text{*Definition forms of @{text gfp_unfold} and @{text coinduct}, 

230 
to control unfolding*} 

231 

232 
lemma def_gfp_unfold: "[ A==gfp(f); mono(f) ] ==> A = f(A)" 

233 
by (auto intro!: gfp_unfold) 

234 

235 
lemma def_coinduct: 

236 
"[ A==gfp(f); mono(f); X \<le> f(sup X A) ] ==> X \<le> A" 

237 
by (iprover intro!: coinduct) 

238 

239 
lemma def_coinduct_set: 

240 
"[ A==gfp(f); mono(f); a:X; X \<subseteq> f(X Un A) ] ==> a: A" 

241 
by (auto intro!: coinduct_set) 

242 

243 
(*The version used in the induction/coinduction package*) 

244 
lemma def_Collect_coinduct: 

245 
"[ A == gfp(%w. Collect(P(w))); mono(%w. Collect(P(w))); 

246 
a: X; !!z. z: X ==> P (X Un A) z ] ==> 

247 
a : A" 

248 
apply (erule def_coinduct_set, auto) 

249 
done 

250 

251 
lemma def_coinduct3: 

252 
"[ A==gfp(f); mono(f); a:X; X \<subseteq> f(lfp(%x. f(x) Un X Un A)) ] ==> a: A" 

253 
by (auto intro!: coinduct3) 

254 

255 
text{*Monotonicity of @{term gfp}!*} 

256 
lemma gfp_mono: "(!!Z. f Z \<le> g Z) ==> gfp f \<le> gfp g" 

257 
by (rule gfp_upperbound [THEN gfp_least], blast intro: order_trans) 

258 

259 

23734  260 
subsection {* Inductive predicates and sets *} 
11688  261 

262 
text {* Inversion of injective functions. *} 

11436  263 

264 
constdefs 

265 
myinv :: "('a => 'b) => ('b => 'a)" 

266 
"myinv (f :: 'a => 'b) == \<lambda>y. THE x. f x = y" 

267 

268 
lemma myinv_f_f: "inj f ==> myinv f (f x) = x" 

269 
proof  

270 
assume "inj f" 

271 
hence "(THE x'. f x' = f x) = (THE x'. x' = x)" 

272 
by (simp only: inj_eq) 

273 
also have "... = x" by (rule the_eq_trivial) 

11439  274 
finally show ?thesis by (unfold myinv_def) 
11436  275 
qed 
276 

277 
lemma f_myinv_f: "inj f ==> y \<in> range f ==> f (myinv f y) = y" 

278 
proof (unfold myinv_def) 

279 
assume inj: "inj f" 

280 
assume "y \<in> range f" 

281 
then obtain x where "y = f x" .. 

282 
hence x: "f x = y" .. 

283 
thus "f (THE x. f x = y) = y" 

284 
proof (rule theI) 

285 
fix x' assume "f x' = y" 

286 
with x have "f x' = f x" by simp 

287 
with inj show "x' = x" by (rule injD) 

288 
qed 

289 
qed 

290 

291 
hide const myinv 

292 

293 

11688  294 
text {* Package setup. *} 
10402  295 

23734  296 
theorems basic_monos = 
22218  297 
subset_refl imp_refl disj_mono conj_mono ex_mono all_mono if_bool_eq_conj 
11688  298 
Collect_mono in_mono vimage_mono 
299 
imp_conv_disj not_not de_Morgan_disj de_Morgan_conj 

300 
not_all not_ex 

301 
Ball_def Bex_def 

18456  302 
induct_rulify_fallback 
11688  303 

24915  304 
ML {* 
305 
val def_lfp_unfold = @{thm def_lfp_unfold} 

306 
val def_gfp_unfold = @{thm def_gfp_unfold} 

307 
val def_lfp_induct = @{thm def_lfp_induct} 

308 
val def_coinduct = @{thm def_coinduct} 

25510  309 
val inf_bool_eq = @{thm inf_bool_eq} RS @{thm eq_reflection} 
310 
val inf_fun_eq = @{thm inf_fun_eq} RS @{thm eq_reflection} 

311 
val sup_bool_eq = @{thm sup_bool_eq} RS @{thm eq_reflection} 

312 
val sup_fun_eq = @{thm sup_fun_eq} RS @{thm eq_reflection} 

24915  313 
val le_boolI = @{thm le_boolI} 
314 
val le_boolI' = @{thm le_boolI'} 

315 
val le_funI = @{thm le_funI} 

316 
val le_boolE = @{thm le_boolE} 

317 
val le_funE = @{thm le_funE} 

318 
val le_boolD = @{thm le_boolD} 

319 
val le_funD = @{thm le_funD} 

25510  320 
val le_bool_def = @{thm le_bool_def} RS @{thm eq_reflection} 
321 
val le_fun_def = @{thm le_fun_def} RS @{thm eq_reflection} 

24915  322 
*} 
323 

21018
e6b8d6784792
Added new package for inductive definitions, moved old package
berghofe
parents:
20604
diff
changeset

324 
use "Tools/inductive_package.ML" 
e6b8d6784792
Added new package for inductive definitions, moved old package
berghofe
parents:
20604
diff
changeset

325 
setup InductivePackage.setup 
e6b8d6784792
Added new package for inductive definitions, moved old package
berghofe
parents:
20604
diff
changeset

326 

23734  327 
theorems [mono] = 
22218  328 
imp_refl disj_mono conj_mono ex_mono all_mono if_bool_eq_conj 
21018
e6b8d6784792
Added new package for inductive definitions, moved old package
berghofe
parents:
20604
diff
changeset

329 
imp_conv_disj not_not de_Morgan_disj de_Morgan_conj 
e6b8d6784792
Added new package for inductive definitions, moved old package
berghofe
parents:
20604
diff
changeset

330 
not_all not_ex 
e6b8d6784792
Added new package for inductive definitions, moved old package
berghofe
parents:
20604
diff
changeset

331 
Ball_def Bex_def 
e6b8d6784792
Added new package for inductive definitions, moved old package
berghofe
parents:
20604
diff
changeset

332 
induct_rulify_fallback 
e6b8d6784792
Added new package for inductive definitions, moved old package
berghofe
parents:
20604
diff
changeset

333 

11688  334 

12023  335 
subsection {* Inductive datatypes and primitive recursion *} 
11688  336 

11825  337 
text {* Package setup. *} 
338 

10402  339 
use "Tools/datatype_aux.ML" 
340 
use "Tools/datatype_prop.ML" 

341 
use "Tools/datatype_rep_proofs.ML" 

342 
use "Tools/datatype_abs_proofs.ML" 

22783  343 
use "Tools/datatype_case.ML" 
10402  344 
use "Tools/datatype_package.ML" 
7700  345 
setup DatatypePackage.setup 
25557  346 
use "Tools/old_primrec_package.ML" 
24699
c6674504103f
datatype interpretators for size and datatype_realizer
haftmann
parents:
24626
diff
changeset

347 
use "Tools/primrec_package.ML" 
12437
6d4e02b6dd43
Moved code generator setup from Recdef to Inductive.
berghofe
parents:
12023
diff
changeset

348 

25534
d0b74fdd6067
simplified infrastructure for code generator operational equality
haftmann
parents:
25510
diff
changeset

349 
use "Tools/datatype_codegen.ML" 
d0b74fdd6067
simplified infrastructure for code generator operational equality
haftmann
parents:
25510
diff
changeset

350 
setup DatatypeCodegen.setup 
d0b74fdd6067
simplified infrastructure for code generator operational equality
haftmann
parents:
25510
diff
changeset

351 

12437
6d4e02b6dd43
Moved code generator setup from Recdef to Inductive.
berghofe
parents:
12023
diff
changeset

352 
use "Tools/inductive_codegen.ML" 
6d4e02b6dd43
Moved code generator setup from Recdef to Inductive.
berghofe
parents:
12023
diff
changeset

353 
setup InductiveCodegen.setup 
6d4e02b6dd43
Moved code generator setup from Recdef to Inductive.
berghofe
parents:
12023
diff
changeset

354 

23526  355 
text{* Lambdaabstractions with pattern matching: *} 
356 

357 
syntax 

23529  358 
"_lam_pats_syntax" :: "cases_syn => 'a => 'b" ("(%_)" 10) 
23526  359 
syntax (xsymbols) 
23529  360 
"_lam_pats_syntax" :: "cases_syn => 'a => 'b" ("(\<lambda>_)" 10) 
23526  361 

23529  362 
parse_translation (advanced) {* 
363 
let 

364 
fun fun_tr ctxt [cs] = 

365 
let 

366 
val x = Free (Name.variant (add_term_free_names (cs, [])) "x", dummyT); 

24349  367 
val ft = DatatypeCase.case_tr true DatatypePackage.datatype_of_constr 
368 
ctxt [x, cs] 

23529  369 
in lambda x ft end 
370 
in [("_lam_pats_syntax", fun_tr)] end 

23526  371 
*} 
372 

373 
end 