author  haftmann 
Tue, 23 Jun 2009 16:27:12 +0200  
changeset 31784  bd3486c57ba3 
parent 31775  2b04504fcb69 
child 31949  3f933687fae9 
permissions  rwrr 
7700  1 
(* Title: HOL/Inductive.thy 
10402  2 
Author: Markus Wenzel, TU Muenchen 
11688  3 
*) 
10727  4 

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

15131  7 
theory Inductive 
24915  8 
imports Lattices Sum_Type 
16417  9 
uses 
31723
f5cafe803b55
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
31604
diff
changeset

10 
("Tools/inductive.ML") 
24625
0398a5e802d3
separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
24349
diff
changeset

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

12 
("Tools/inductive_codegen.ML") 
31775  13 
("Tools/Datatype/datatype_aux.ML") 
14 
("Tools/Datatype/datatype_prop.ML") 

15 
("Tools/Datatype/datatype_rep_proofs.ML") 

16 
("Tools/Datatype/datatype_abs_proofs.ML") 

17 
("Tools/Datatype/datatype_case.ML") 

18 
("Tools/Datatype/datatype.ML") 

31723
f5cafe803b55
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
31604
diff
changeset

19 
("Tools/old_primrec.ML") 
f5cafe803b55
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
31604
diff
changeset

20 
("Tools/primrec.ML") 
31775  21 
("Tools/Datatype/datatype_codegen.ML") 
15131  22 
begin 
10727  23 

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

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

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

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

28 

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

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

33 
definition 

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

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

37 

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

39 

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

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

42 

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

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

45 

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

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

48 

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

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

50 

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

53 

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

55 
by (iprover intro: lfp_lemma2 monoD lfp_lowerbound) 

56 

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

58 
by (iprover intro: order_antisym lfp_lemma2 lfp_lemma3) 

59 

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

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

62 

63 

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

65 

66 
theorem lfp_induct: 

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

68 
shows "lfp f <= P" 

69 
proof  

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

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

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

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

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

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

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

77 
finally show ?thesis . 

78 
qed 

79 

80 
lemma lfp_induct_set: 

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

82 
and mono: "mono(f)" 

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

84 
shows "P(a)" 

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

86 
(auto simp: inf_set_eq intro: indhyp) 

87 

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

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

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

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

91 
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

92 
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

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

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

95 
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

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

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

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

99 
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

100 
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

101 
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

102 
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

103 
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

104 
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

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

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

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

108 

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

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

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

113 
shows "P(lfp f)" 

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

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

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

117 

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

119 
to control unfolding*} 

120 

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

122 
by (auto intro!: lfp_unfold) 

123 

124 
lemma def_lfp_induct: 

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

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

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

128 
by (blast intro: lfp_induct) 

129 

130 
lemma def_lfp_induct_set: 

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

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

133 
] ==> P(a)" 

134 
by (blast intro: lfp_induct_set) 

135 

136 
(*Monotonicity of lfp!*) 

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

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

139 

140 

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

142 

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

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

145 

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

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

148 

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

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

151 

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

153 
by (iprover intro: gfp_least order_trans monoD gfp_upperbound) 

154 

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

156 
by (iprover intro: gfp_lemma2 monoD gfp_upperbound) 

157 

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

159 
by (iprover intro: order_antisym gfp_lemma2 gfp_lemma3) 

160 

161 

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

163 

164 
text{*weak version*} 

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

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

167 

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

169 
apply (erule gfp_upperbound [THEN subsetD]) 

170 
apply (erule imageI) 

171 
done 

172 

173 
lemma coinduct_lemma: 

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

175 
apply (frule gfp_lemma2) 

176 
apply (drule mono_sup) 

177 
apply (rule le_supI) 

178 
apply assumption 

179 
apply (rule order_trans) 

180 
apply (rule order_trans) 

181 
apply assumption 

182 
apply (rule sup_ge2) 

183 
apply assumption 

184 
done 

185 

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

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

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

189 

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

191 
apply (rule order_trans) 

192 
apply (rule sup_ge1) 

193 
apply (erule gfp_upperbound [OF coinduct_lemma]) 

194 
apply assumption 

195 
done 

196 

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

198 
by (blast dest: gfp_lemma2 mono_Un) 

199 

200 

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

202 

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

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

205 

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

207 
by (iprover intro: subset_refl monoI Un_mono monoD) 

208 

209 
lemma coinduct3_lemma: 

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

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

212 
apply (rule subset_trans) 

213 
apply (erule coinduct3_mono_lemma [THEN lfp_lemma3]) 

214 
apply (rule Un_least [THEN Un_least]) 

215 
apply (rule subset_refl, assumption) 

216 
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

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

220 

221 
lemma coinduct3: 

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

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

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

225 
done 

226 

227 

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

229 
to control unfolding*} 

230 

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

232 
by (auto intro!: gfp_unfold) 

233 

234 
lemma def_coinduct: 

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

236 
by (iprover intro!: coinduct) 

237 

238 
lemma def_coinduct_set: 

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

240 
by (auto intro!: coinduct_set) 

241 

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

243 
lemma def_Collect_coinduct: 

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

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

246 
a : A" 

247 
apply (erule def_coinduct_set, auto) 

248 
done 

249 

250 
lemma def_coinduct3: 

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

252 
by (auto intro!: coinduct3) 

253 

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

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

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

257 

258 

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

261 
text {* Inversion of injective functions. *} 

11436  262 

263 
constdefs 

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

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

266 

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

268 
proof  

269 
assume "inj f" 

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

271 
by (simp only: inj_eq) 

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

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

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

277 
proof (unfold myinv_def) 

278 
assume inj: "inj f" 

279 
assume "y \<in> range f" 

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

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

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

283 
proof (rule theI) 

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

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

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

287 
qed 

288 
qed 

289 

290 
hide const myinv 

291 

292 

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

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

299 
not_all not_ex 

300 
Ball_def Bex_def 

18456  301 
induct_rulify_fallback 
11688  302 

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

305 
val def_gfp_unfold = @{thm def_gfp_unfold} 

306 
val def_lfp_induct = @{thm def_lfp_induct} 

307 
val def_coinduct = @{thm def_coinduct} 

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

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

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

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

314 
val le_funI = @{thm le_funI} 

315 
val le_boolE = @{thm le_boolE} 

316 
val le_funE = @{thm le_funE} 

317 
val le_boolD = @{thm le_boolD} 

318 
val le_funD = @{thm le_funD} 

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

24915  321 
*} 
322 

31723
f5cafe803b55
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
31604
diff
changeset

323 
use "Tools/inductive.ML" 
f5cafe803b55
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
31604
diff
changeset

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

325 

23734  326 
theorems [mono] = 
22218  327 
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

328 
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

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

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

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

332 

11688  333 

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

11825  336 
text {* Package setup. *} 
337 

31775  338 
use "Tools/Datatype/datatype_aux.ML" 
339 
use "Tools/Datatype/datatype_prop.ML" 

340 
use "Tools/Datatype/datatype_rep_proofs.ML" 

341 
use "Tools/Datatype/datatype_abs_proofs.ML" 

342 
use "Tools/Datatype/datatype_case.ML" 

343 
use "Tools/Datatype/datatype.ML" 

31723
f5cafe803b55
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
31604
diff
changeset

344 
setup Datatype.setup 
31604  345 

31723
f5cafe803b55
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
31604
diff
changeset

346 
use "Tools/old_primrec.ML" 
f5cafe803b55
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
31604
diff
changeset

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

348 

31775  349 
use "Tools/Datatype/datatype_codegen.ML" 
25534
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 

29281  366 
val x = Free (Name.variant (Term.add_free_names cs []) "x", dummyT); 
31784  367 
val ft = DatatypeCase.case_tr true Datatype.info_of_constr 
24349  368 
ctxt [x, cs] 
23529  369 
in lambda x ft end 
370 
in [("_lam_pats_syntax", fun_tr)] end 

23526  371 
*} 
372 

373 
end 