229 val inducts = #inducts dtinfo; |
229 val inducts = #inducts dtinfo; |
230 val ((raw_perm_def, raw_perm_simps, perms), lthy3) = |
230 val ((raw_perm_def, raw_perm_simps, perms), lthy3) = |
231 Local_Theory.theory_result (define_raw_perms dtinfo (length dts)) lthy2; |
231 Local_Theory.theory_result (define_raw_perms dtinfo (length dts)) lthy2; |
232 val raw_binds_flat = map (map flat) raw_binds; |
232 val raw_binds_flat = map (map flat) raw_binds; |
233 val (((fv_ts_loc, fv_def_loc), alpha), lthy4) = define_fv_alpha dtinfo raw_binds_flat lthy3; |
233 val (((fv_ts_loc, fv_def_loc), alpha), lthy4) = define_fv_alpha dtinfo raw_binds_flat lthy3; |
234 val alpha_ts_loc = #preds alpha |
234 (* val alpha_ts_loc = #preds alpha |
235 val morphism_4_3 = ProofContext.export_morphism lthy4 lthy3; |
235 val morphism_4_3 = ProofContext.export_morphism lthy4 lthy3; |
236 val alpha_ts = map (Morphism.term morphism_4_3) alpha_ts_loc; |
236 val alpha_ts = map (Morphism.term morphism_4_3) alpha_ts_loc; |
237 val alpha_induct_loc = #induct alpha |
237 val alpha_induct_loc = #induct alpha |
238 val dts_names = map (fn (i, (s, _, _)) => (s, i)) (#descr dtinfo); |
238 val dts_names = map (fn (i, (s, _, _)) => (s, i)) (#descr dtinfo); |
239 val bn_tys = map (domain_type o fastype_of) raw_bn_funs; |
239 val bn_tys = map (domain_type o fastype_of) raw_bn_funs; |
252 inject alpha_inj_loc distinct alpha_cases alpha_eqvt_loc lthy6; |
252 inject alpha_inj_loc distinct alpha_cases alpha_eqvt_loc lthy6; |
253 val alpha_equivp = ProofContext.export lthy6 lthy2 alpha_equivp_loc; |
253 val alpha_equivp = ProofContext.export lthy6 lthy2 alpha_equivp_loc; |
254 val qty_names = map (fn (_, b, _, _) => b) dts; |
254 val qty_names = map (fn (_, b, _, _) => b) dts; |
255 val lthy7 = define_quotient_type |
255 val lthy7 = define_quotient_type |
256 (map (fn ((b, t), alpha) => (([], b, NoSyn), (t, alpha))) ((qty_names ~~ all_typs) ~~ alpha_ts)) |
256 (map (fn ((b, t), alpha) => (([], b, NoSyn), (t, alpha))) ((qty_names ~~ all_typs) ~~ alpha_ts)) |
257 (ALLGOALS (resolve_tac alpha_equivp)) lthy6; |
257 (ALLGOALS (resolve_tac alpha_equivp)) lthy6;*) |
258 in |
258 in |
259 ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy7) |
259 ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy4) |
260 end |
260 end |
261 *} |
261 *} |
262 |
262 |
263 ML {* |
263 ML {* |
264 (* parsing the datatypes and declaring *) |
264 (* parsing the datatypes and declaring *) |