265 raw_nominal_decls dts bn_funs bn_eqs bclauses lthy |
265 raw_nominal_decls dts bn_funs bn_eqs bclauses lthy |
266 |
266 |
267 val dtinfo = Datatype.the_info (ProofContext.theory_of lthy1) (hd raw_dt_names); |
267 val dtinfo = Datatype.the_info (ProofContext.theory_of lthy1) (hd raw_dt_names); |
268 val {descr, sorts, ...} = dtinfo; |
268 val {descr, sorts, ...} = dtinfo; |
269 |
269 |
|
270 val all_full_tnames = map (fn (_, (n, _, _)) => n) descr; |
|
271 val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy1)) all_full_tnames; |
|
272 val inject = flat (map #inject dtinfos); |
|
273 val distincts = flat (map #distinct dtinfos); |
|
274 val rel_dtinfos = List.take (dtinfos, (length dts)); |
|
275 val rel_distinct = map #distinct rel_dtinfos; |
|
276 val induct = #induct dtinfo; |
|
277 val exhausts = map #exhaust dtinfos; |
|
278 |
270 val ((raw_perm_def, raw_perm_simps, perms), lthy2) = |
279 val ((raw_perm_def, raw_perm_simps, perms), lthy2) = |
271 Local_Theory.theory_result (define_raw_perms dtinfo (length dts)) lthy1; |
280 Local_Theory.theory_result (define_raw_perms dtinfo (length dts)) lthy1; |
272 |
281 |
273 val morphism_2_0 = ProofContext.export_morphism lthy2 lthy |
282 val morphism_2_0 = ProofContext.export_morphism lthy2 lthy |
274 fun export_fun f (t, l) = (f t, map (map (apsnd (Option.map f))) l); |
283 fun export_fun f (t, l) = (f t, map (map (apsnd (Option.map f))) l); |
275 val raw_bns_exp = map (apsnd (map (export_fun (Morphism.term morphism_2_0)))) raw_bns; |
284 val raw_bns_exp = map (apsnd (map (export_fun (Morphism.term morphism_2_0)))) raw_bns; |
276 val bn_funs_decls = flat (map (fn (ith, l) => map (fn (bn, data) => (bn, ith, data)) l) raw_bns_exp); |
285 val bn_funs_decls = flat (map (fn (ith, l) => map (fn (bn, data) => (bn, ith, data)) l) raw_bns_exp); |
277 val thy = Local_Theory.exit_global lthy2; |
286 val thy = Local_Theory.exit_global lthy2; |
278 val lthy3 = Theory_Target.init NONE thy; |
287 val lthy3 = Theory_Target.init NONE thy; |
279 |
288 |
280 val ((fv, fvbn), fvsimps, lthy4) = define_raw_fv dtinfo bn_funs_decls raw_bclauses lthy3; |
289 val ((fv, fvbn), fv_def, lthy3a) = define_raw_fv dtinfo bn_funs_decls raw_bclauses lthy3; |
281 val (((alpha_ts, alpha_intros), (alpha_cases, alpha_induct)), lthy5) = |
290 val (((alpha_ts, alpha_intros), (alpha_cases, alpha_induct)), lthy4) = |
282 define_raw_alpha dtinfo bn_funs_decls raw_bclauses fv lthy4; |
291 define_raw_alpha dtinfo bn_funs_decls raw_bclauses fv lthy3a; |
283 in |
292 val (alpha_ts_nobn, alpha_ts_bn) = chop (length fv) alpha_ts |
284 ((raw_dt_names, raw_bn_funs_loc, raw_bn_eqs_loc, raw_bclauses, raw_bns), lthy5) |
293 |
|
294 in |
|
295 ((raw_dt_names, raw_bn_funs_loc, raw_bn_eqs_loc, raw_bclauses, raw_bns), lthy4) |
285 end |
296 end |
286 *} |
297 *} |
287 |
298 |
288 section {* Preparing and parsing of the specification *} |
299 section {* Preparing and parsing of the specification *} |
289 |
300 |