351 val rel_dtinfos = List.take (dtinfos, (length dts)); |
351 val rel_dtinfos = List.take (dtinfos, (length dts)); |
352 val inject = flat (map #inject dtinfos); |
352 val inject = flat (map #inject dtinfos); |
353 val distincts = flat (map #distinct dtinfos); |
353 val distincts = flat (map #distinct dtinfos); |
354 val rel_distinct = map #distinct rel_dtinfos; |
354 val rel_distinct = map #distinct rel_dtinfos; |
355 val induct = #induct dtinfo; |
355 val induct = #induct dtinfo; |
356 val inducts = #inducts dtinfo; |
|
357 val exhausts = map #exhaust dtinfos; |
356 val exhausts = map #exhaust dtinfos; |
358 val _ = tracing "Defining permutations, fv and alpha"; |
357 val _ = tracing "Defining permutations, fv and alpha"; |
359 val ((raw_perm_def, raw_perm_simps, perms), lthy3) = |
358 val ((raw_perm_def, raw_perm_simps, perms), lthy3) = |
360 Local_Theory.theory_result (define_raw_perms dtinfo (length dts)) lthy2; |
359 Local_Theory.theory_result (define_raw_perms dtinfo (length dts)) lthy2; |
361 val raw_binds_flat = map (map flat) raw_binds; |
360 val raw_binds_flat = map (map flat) raw_binds; |
389 else build_equivps alpha_ts reflps alpha_induct |
388 else build_equivps alpha_ts reflps alpha_induct |
390 inject alpha_eq_iff distincts alpha_cases alpha_eqvt lthy6; |
389 inject alpha_eq_iff distincts alpha_cases alpha_eqvt lthy6; |
391 val qty_binds = map (fn (_, b, _, _) => b) dts; |
390 val qty_binds = map (fn (_, b, _, _) => b) dts; |
392 val qty_names = map Name.of_binding qty_binds; |
391 val qty_names = map Name.of_binding qty_binds; |
393 val qty_full_names = map (Long_Name.qualify thy_name) qty_names |
392 val qty_full_names = map (Long_Name.qualify thy_name) qty_names |
394 val lthy7 = define_quotient_type |
393 val (q_tys, lthy7) = define_quotient_types qty_binds all_typs alpha_ts_nobn alpha_equivp lthy6; |
395 (map (fn ((b, t), alpha) => (([], b, NoSyn), (t, alpha))) ((qty_binds ~~ all_typs) ~~ alpha_ts_nobn)) |
|
396 (ALLGOALS (resolve_tac alpha_equivp)) lthy6; |
|
397 val const_names = map Name.of_binding (flat (map (fn (_, _, _, t) => map (fn (b, _, _) => b) t) dts)); |
394 val const_names = map Name.of_binding (flat (map (fn (_, _, _, t) => map (fn (b, _, _) => b) t) dts)); |
398 val raw_consts = |
395 val raw_consts = |
399 flat (map (fn (i, (_, _, l)) => |
396 flat (map (fn (i, (_, _, l)) => |
400 map (fn (cname, dts) => |
397 map (fn (cname, dts) => |
401 Const (cname, map (typ_of_dtyp descr sorts) dts ---> |
398 Const (cname, map (typ_of_dtyp descr sorts) dts ---> |
402 typ_of_dtyp descr sorts (DtRec i))) l) descr); |
399 typ_of_dtyp descr sorts (DtRec i))) l) descr); |
403 val (consts, const_defs, lthy8) = quotient_lift_consts_export (const_names ~~ raw_consts) lthy7; |
400 val (consts, const_defs, lthy8) = quotient_lift_consts_export (const_names ~~ raw_consts) lthy7; |
404 (* Could be done nicer *) |
|
405 val q_tys = distinct (op =) (map (snd o strip_type o fastype_of) consts); |
|
406 val _ = tracing "Proving respects"; |
401 val _ = tracing "Proving respects"; |
407 val bns_rsp_pre' = build_fvbv_rsps alpha_ts alpha_induct raw_bn_eqs (map fst bns) lthy8; |
402 val bns_rsp_pre' = build_fvbv_rsps alpha_ts alpha_induct raw_bn_eqs (map fst bns) lthy8; |
|
403 val _ = map tracing (map PolyML.makestring bns_rsp_pre') |
408 val (bns_rsp_pre, lthy9) = fold_map ( |
404 val (bns_rsp_pre, lthy9) = fold_map ( |
409 fn (bn_t, i) => prove_const_rsp Binding.empty [bn_t] (fn _ => |
405 fn (bn_t, i) => prove_const_rsp Binding.empty [bn_t] (fn _ => |
410 resolve_tac bns_rsp_pre' 1)) bns lthy8; |
406 resolve_tac bns_rsp_pre' 1)) bns lthy8; |
411 val bns_rsp = flat (map snd bns_rsp_pre); |
407 val bns_rsp = flat (map snd bns_rsp_pre); |
412 fun fv_rsp_tac _ = if !cheat_fv_rsp then Skip_Proof.cheat_tac thy |
408 fun fv_rsp_tac _ = if !cheat_fv_rsp then Skip_Proof.cheat_tac thy |