426 Const (cname, map (typ_of_dtyp descr sorts) dts ---> |
426 Const (cname, map (typ_of_dtyp descr sorts) dts ---> |
427 typ_of_dtyp descr sorts (DtRec i))) l) descr); |
427 typ_of_dtyp descr sorts (DtRec i))) l) descr); |
428 val (consts, const_defs, lthy8) = quotient_lift_consts_export qtys (const_names ~~ raw_consts) lthy7; |
428 val (consts, const_defs, lthy8) = quotient_lift_consts_export qtys (const_names ~~ raw_consts) lthy7; |
429 val _ = tracing "Proving respects"; |
429 val _ = tracing "Proving respects"; |
430 val bns_rsp_pre' = build_fvbv_rsps alpha_ts alpha_induct raw_bn_eqs (map fst bns) lthy8; |
430 val bns_rsp_pre' = build_fvbv_rsps alpha_ts alpha_induct raw_bn_eqs (map fst bns) lthy8; |
431 val _ = map tracing (map PolyML.makestring bns_rsp_pre') |
|
432 val (bns_rsp_pre, lthy9) = fold_map ( |
431 val (bns_rsp_pre, lthy9) = fold_map ( |
433 fn (bn_t, _) => prove_const_rsp qtys Binding.empty [bn_t] (fn _ => |
432 fn (bn_t, _) => prove_const_rsp qtys Binding.empty [bn_t] (fn _ => |
434 resolve_tac bns_rsp_pre' 1)) bns lthy8; |
433 resolve_tac bns_rsp_pre' 1)) bns lthy8; |
435 val bns_rsp = flat (map snd bns_rsp_pre); |
434 val bns_rsp = flat (map snd bns_rsp_pre); |
436 fun fv_rsp_tac _ = if !cheat_fv_rsp then Skip_Proof.cheat_tac thy |
435 fun fv_rsp_tac _ = if !cheat_fv_rsp then Skip_Proof.cheat_tac thy |