372 typ_of_dtyp descr sorts (DtRec i))) l) descr); |
372 typ_of_dtyp descr sorts (DtRec i))) l) descr); |
373 val (consts, const_defs, lthy8) = quotient_lift_consts_export (const_names ~~ raw_consts) lthy7; |
373 val (consts, const_defs, lthy8) = quotient_lift_consts_export (const_names ~~ raw_consts) lthy7; |
374 (* Could be done nicer *) |
374 (* Could be done nicer *) |
375 val q_tys = distinct (op =) (map (snd o strip_type o fastype_of) consts); |
375 val q_tys = distinct (op =) (map (snd o strip_type o fastype_of) consts); |
376 val _ = tracing "Proving respects"; |
376 val _ = tracing "Proving respects"; |
|
377 val bns_rsp_pre' = build_fvbv_rsps alpha_ts alpha_induct raw_bn_eqs (map fst bns) lthy8; |
377 val (bns_rsp_pre, lthy9) = fold_map ( |
378 val (bns_rsp_pre, lthy9) = fold_map ( |
378 fn (bn_t, i) => prove_const_rsp Binding.empty [bn_t] (fn _ => |
379 fn (bn_t, i) => prove_const_rsp Binding.empty [bn_t] (fn _ => |
379 if !cheat_bn_rsp then (Skip_Proof.cheat_tac thy) else |
380 resolve_tac bns_rsp_pre' 1)) bns lthy8; |
380 fvbv_rsp_tac (nth alpha_inducts i) raw_bn_eqs lthy8 1)) bns lthy8; |
|
381 val bns_rsp = flat (map snd bns_rsp_pre); |
381 val bns_rsp = flat (map snd bns_rsp_pre); |
382 fun fv_rsp_tac _ = if !cheat_fv_rsp then Skip_Proof.cheat_tac thy |
382 fun fv_rsp_tac _ = if !cheat_fv_rsp then Skip_Proof.cheat_tac thy |
383 else fvbv_rsp_tac alpha_induct fv_def lthy8 1; |
383 else fvbv_rsp_tac alpha_induct fv_def lthy8 1; |
384 val fv_rsps = prove_fv_rsp fv_alpha_all alpha_ts fv_rsp_tac lthy9; |
384 val fv_rsps = prove_fv_rsp fv_alpha_all alpha_ts fv_rsp_tac lthy9; |
385 val (fv_rsp_pre, lthy10) = fold_map |
385 val (fv_rsp_pre, lthy10) = fold_map |