333 raw_nominal_decls dts bn_funs bn_eqs bclauses lthy |
333 raw_nominal_decls dts bn_funs bn_eqs bclauses lthy |
334 |
334 |
335 val dtinfo = Datatype.the_info (ProofContext.theory_of lthy1) (hd raw_dt_names); |
335 val dtinfo = Datatype.the_info (ProofContext.theory_of lthy1) (hd raw_dt_names); |
336 val {descr, sorts, ...} = dtinfo; |
336 val {descr, sorts, ...} = dtinfo; |
337 val raw_tys = map (fn (i, _) => nth_dtyp descr sorts i) descr; |
337 val raw_tys = map (fn (i, _) => nth_dtyp descr sorts i) descr; |
338 val all_typs = map (fn i => typ_of_dtyp descr sorts (DtRec i)) (map fst descr) |
338 val all_typs = map (fn i => Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec i)) (map fst descr) |
339 |
339 |
340 val all_full_tnames = map (fn (_, (n, _, _)) => n) descr; |
340 val all_full_tnames = map (fn (_, (n, _, _)) => n) descr; |
341 val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy1)) all_full_tnames; |
341 val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy1)) all_full_tnames; |
342 val inject = flat (map #inject dtinfos); |
342 val inject = flat (map #inject dtinfos); |
343 val distincts = flat (map #distinct dtinfos); |
343 val distincts = flat (map #distinct dtinfos); |
401 val (qtys, lthy7) = define_quotient_types qty_binds all_typs alpha_ts_nobn alpha_equivp lthy6; |
401 val (qtys, lthy7) = define_quotient_types qty_binds all_typs alpha_ts_nobn alpha_equivp lthy6; |
402 val const_names = map Name.of_binding (flat (map (fn (_, _, _, t) => map (fn (b, _, _) => b) t) dts)); |
402 val const_names = map Name.of_binding (flat (map (fn (_, _, _, t) => map (fn (b, _, _) => b) t) dts)); |
403 val raw_consts = |
403 val raw_consts = |
404 flat (map (fn (i, (_, _, l)) => |
404 flat (map (fn (i, (_, _, l)) => |
405 map (fn (cname, dts) => |
405 map (fn (cname, dts) => |
406 Const (cname, map (typ_of_dtyp descr sorts) dts ---> |
406 Const (cname, map (Datatype_Aux.typ_of_dtyp descr sorts) dts ---> |
407 typ_of_dtyp descr sorts (DtRec i))) l) descr); |
407 Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec i))) l) descr); |
408 val (consts, const_defs, lthy8) = quotient_lift_consts_export qtys (const_names ~~ raw_consts) lthy7; |
408 val (consts, const_defs, lthy8) = quotient_lift_consts_export qtys (const_names ~~ raw_consts) lthy7; |
409 val _ = warning "Proving respects"; |
409 val _ = warning "Proving respects"; |
410 val bns_rsp_pre' = build_fvbv_rsps alpha_ts alpha_induct raw_bn_eqs (map fst bns) lthy8; |
410 val bns_rsp_pre' = build_fvbv_rsps alpha_ts alpha_induct raw_bn_eqs (map fst bns) lthy8; |
411 val (bns_rsp_pre, lthy9) = fold_map ( |
411 val (bns_rsp_pre, lthy9) = fold_map ( |
412 fn (bn_t, _) => prove_const_rsp qtys Binding.empty [bn_t] (fn _ => |
412 fn (bn_t, _) => prove_const_rsp qtys Binding.empty [bn_t] (fn _ => |