author  haftmann 
Wed, 16 Sep 2009 13:43:05 +0200  
changeset 32587  caa5ada96a00 
parent 31949  3f933687fae9 
child 32652  3175e23b79f3 
child 32683  7c1fe854ca6a 
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)" 

32587
caa5ada96a00
Inter and Union are mere abbreviations for Inf and Sup
haftmann
parents:
31949
diff
changeset

114 
using assms by (rule lfp_ordinal_induct [where P=P]) 
24915  115 

116 

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

118 
to control unfolding*} 

119 

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

121 
by (auto intro!: lfp_unfold) 

122 

123 
lemma def_lfp_induct: 

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

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

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

127 
by (blast intro: lfp_induct) 

128 

129 
lemma def_lfp_induct_set: 

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

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

132 
] ==> P(a)" 

133 
by (blast intro: lfp_induct_set) 

134 

135 
(*Monotonicity of lfp!*) 

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

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

138 

139 

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

141 

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

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

144 

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

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

147 

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

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

150 

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

152 
by (iprover intro: gfp_least order_trans monoD gfp_upperbound) 

153 

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

155 
by (iprover intro: gfp_lemma2 monoD gfp_upperbound) 

156 

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

158 
by (iprover intro: order_antisym gfp_lemma2 gfp_lemma3) 

159 

160 

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

162 

163 
text{*weak version*} 

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

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

166 

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

168 
apply (erule gfp_upperbound [THEN subsetD]) 

169 
apply (erule imageI) 

170 
done 

171 

172 
lemma coinduct_lemma: 

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

174 
apply (frule gfp_lemma2) 

175 
apply (drule mono_sup) 

176 
apply (rule le_supI) 

177 
apply assumption 

178 
apply (rule order_trans) 

179 
apply (rule order_trans) 

180 
apply assumption 

181 
apply (rule sup_ge2) 

182 
apply assumption 

183 
done 

184 

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

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

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

188 

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

190 
apply (rule order_trans) 

191 
apply (rule sup_ge1) 

192 
apply (erule gfp_upperbound [OF coinduct_lemma]) 

193 
apply assumption 

194 
done 

195 

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

197 
by (blast dest: gfp_lemma2 mono_Un) 

198 

199 

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

201 

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

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

204 

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

206 
by (iprover intro: subset_refl monoI Un_mono monoD) 

207 

208 
lemma coinduct3_lemma: 

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

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

211 
apply (rule subset_trans) 

212 
apply (erule coinduct3_mono_lemma [THEN lfp_lemma3]) 

213 
apply (rule Un_least [THEN Un_least]) 

214 
apply (rule subset_refl, assumption) 

215 
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

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

219 

220 
lemma coinduct3: 

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

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

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

224 
done 

225 

226 

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

228 
to control unfolding*} 

229 

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

231 
by (auto intro!: gfp_unfold) 

232 

233 
lemma def_coinduct: 

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

235 
by (iprover intro!: coinduct) 

236 

237 
lemma def_coinduct_set: 

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

239 
by (auto intro!: coinduct_set) 

240 

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

242 
lemma def_Collect_coinduct: 

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

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

245 
a : A" 

246 
apply (erule def_coinduct_set, auto) 

247 
done 

248 

249 
lemma def_coinduct3: 

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

251 
by (auto intro!: coinduct3) 

252 

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

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

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

256 

257 

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

260 
text {* Package setup. *} 

10402  261 

23734  262 
theorems basic_monos = 
22218  263 
subset_refl imp_refl disj_mono conj_mono ex_mono all_mono if_bool_eq_conj 
11688  264 
Collect_mono in_mono vimage_mono 
265 
imp_conv_disj not_not de_Morgan_disj de_Morgan_conj 

266 
not_all not_ex 

267 
Ball_def Bex_def 

18456  268 
induct_rulify_fallback 
11688  269 

24915  270 
ML {* 
271 
val def_lfp_unfold = @{thm def_lfp_unfold} 

272 
val def_gfp_unfold = @{thm def_gfp_unfold} 

273 
val def_lfp_induct = @{thm def_lfp_induct} 

274 
val def_coinduct = @{thm def_coinduct} 

25510  275 
val inf_bool_eq = @{thm inf_bool_eq} RS @{thm eq_reflection} 
276 
val inf_fun_eq = @{thm inf_fun_eq} RS @{thm eq_reflection} 

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

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

24915  279 
val le_boolI = @{thm le_boolI} 
280 
val le_boolI' = @{thm le_boolI'} 

281 
val le_funI = @{thm le_funI} 

282 
val le_boolE = @{thm le_boolE} 

283 
val le_funE = @{thm le_funE} 

284 
val le_boolD = @{thm le_boolD} 

285 
val le_funD = @{thm le_funD} 

25510  286 
val le_bool_def = @{thm le_bool_def} RS @{thm eq_reflection} 
287 
val le_fun_def = @{thm le_fun_def} RS @{thm eq_reflection} 

24915  288 
*} 
289 

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

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

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

292 

23734  293 
theorems [mono] = 
22218  294 
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

295 
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

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

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

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

299 

11688  300 

12023  301 
subsection {* Inductive datatypes and primitive recursion *} 
11688  302 

11825  303 
text {* Package setup. *} 
304 

31775  305 
use "Tools/Datatype/datatype_aux.ML" 
306 
use "Tools/Datatype/datatype_prop.ML" 

307 
use "Tools/Datatype/datatype_rep_proofs.ML" 

308 
use "Tools/Datatype/datatype_abs_proofs.ML" 

309 
use "Tools/Datatype/datatype_case.ML" 

310 
use "Tools/Datatype/datatype.ML" 

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

311 
setup Datatype.setup 
31604  312 

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

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

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

315 

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

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

318 

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

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

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

321 

23526  322 
text{* Lambdaabstractions with pattern matching: *} 
323 

324 
syntax 

23529  325 
"_lam_pats_syntax" :: "cases_syn => 'a => 'b" ("(%_)" 10) 
23526  326 
syntax (xsymbols) 
23529  327 
"_lam_pats_syntax" :: "cases_syn => 'a => 'b" ("(\<lambda>_)" 10) 
23526  328 

23529  329 
parse_translation (advanced) {* 
330 
let 

331 
fun fun_tr ctxt [cs] = 

332 
let 

29281  333 
val x = Free (Name.variant (Term.add_free_names cs []) "x", dummyT); 
31784  334 
val ft = DatatypeCase.case_tr true Datatype.info_of_constr 
24349  335 
ctxt [x, cs] 
23529  336 
in lambda x ft end 
337 
in [("_lam_pats_syntax", fun_tr)] end 

23526  338 
*} 
339 

340 
end 