262 val raw_bclauses = rawify_bclauses dts_env cnstrs_env bn_fun_full_env binds |
262 val raw_bclauses = rawify_bclauses dts_env cnstrs_env bn_fun_full_env binds |
263 |
263 |
264 val (raw_dt_full_names, lthy1) = |
264 val (raw_dt_full_names, lthy1) = |
265 add_datatype_wrapper raw_dt_names raw_dts lthy |
265 add_datatype_wrapper raw_dt_names raw_dts lthy |
266 in |
266 in |
267 (dt_full_names', raw_dt_full_names, raw_dts, raw_bclauses, raw_bn_funs, raw_bn_eqs, lthy1) |
267 (raw_dt_full_names, raw_dts, raw_bclauses, raw_bn_funs, raw_bn_eqs, lthy1) |
268 end |
268 end |
269 *} |
269 *} |
270 |
270 |
271 ML {* |
271 ML {* |
272 fun raw_bn_decls dt_names dts raw_bn_funs raw_bn_eqs constr_thms lthy = |
272 fun raw_bn_decls dt_names dts raw_bn_funs raw_bn_eqs constr_thms lthy = |
311 ML {* |
311 ML {* |
312 fun nominal_datatype2 dts bn_funs bn_eqs bclauses lthy = |
312 fun nominal_datatype2 dts bn_funs bn_eqs bclauses lthy = |
313 let |
313 let |
314 (* definition of the raw datatypes *) |
314 (* definition of the raw datatypes *) |
315 val _ = warning "Definition of raw datatypes"; |
315 val _ = warning "Definition of raw datatypes"; |
316 val (dt_names, raw_dt_names, raw_dts, raw_bclauses, raw_bn_funs, raw_bn_eqs, lthy0) = |
316 val (raw_dt_names, raw_dts, raw_bclauses, raw_bn_funs, raw_bn_eqs, lthy0) = |
317 if get_STEPS lthy > 0 |
317 if get_STEPS lthy > 0 |
318 then raw_nominal_decls dts bn_funs bn_eqs bclauses lthy |
318 then raw_nominal_decls dts bn_funs bn_eqs bclauses lthy |
319 else raise TEST lthy |
319 else raise TEST lthy |
320 |
320 |
321 val dtinfo = Datatype.the_info (ProofContext.theory_of lthy0) (hd raw_dt_names) |
321 val dtinfo = Datatype.the_info (ProofContext.theory_of lthy0) (hd raw_dt_names) |
322 val {descr, sorts, ...} = dtinfo |
322 val {descr, sorts, ...} = dtinfo |
323 val all_tys = map (fn (i, _) => nth_dtyp descr sorts i) descr |
323 val all_raw_tys = map (fn (_, (n, _, _)) => n) descr |
324 val all_full_tnames = map (fn (_, (n, _, _)) => n) descr |
324 val all_raw_constrs = |
325 val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy0)) all_full_tnames |
325 flat (map (map (fn (c, _, _, _) => c)) (all_dtyp_constrs_types descr sorts)) |
326 |
326 |
|
327 val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy0)) all_raw_tys |
327 val inject_thms = flat (map #inject dtinfos); |
328 val inject_thms = flat (map #inject dtinfos); |
328 val distinct_thms = flat (map #distinct dtinfos); |
329 val distinct_thms = flat (map #distinct dtinfos); |
329 val constr_thms = inject_thms @ distinct_thms |
330 val constr_thms = inject_thms @ distinct_thms |
330 val rel_dtinfos = List.take (dtinfos, (length dts)); |
331 val rel_dtinfos = List.take (dtinfos, (length dts)); |
331 val raw_constrs_distinct = (map #distinct rel_dtinfos); |
332 val raw_constrs_distinct = (map #distinct rel_dtinfos); |
350 val _ = warning "Definition of raw fv-functions"; |
351 val _ = warning "Definition of raw fv-functions"; |
351 val lthy3 = Theory_Target.init NONE thy; |
352 val lthy3 = Theory_Target.init NONE thy; |
352 |
353 |
353 val (raw_bn_funs, raw_bn_eqs, raw_bn_info, raw_bn_induct, lthy3a) = |
354 val (raw_bn_funs, raw_bn_eqs, raw_bn_info, raw_bn_induct, lthy3a) = |
354 if get_STEPS lthy3 > 2 |
355 if get_STEPS lthy3 > 2 |
355 then raw_bn_decls dt_names raw_dts raw_bn_funs raw_bn_eqs constr_thms lthy3 |
356 then raw_bn_decls all_raw_tys raw_dts raw_bn_funs raw_bn_eqs constr_thms lthy3 |
356 else raise TEST lthy3 |
357 else raise TEST lthy3 |
357 |
358 |
358 val (raw_fvs, raw_fv_bns, raw_fv_defs, raw_fv_bns_induct, lthy3b) = |
359 val (raw_fvs, raw_fv_bns, raw_fv_defs, raw_fv_bns_induct, lthy3b) = |
359 if get_STEPS lthy3a > 3 |
360 if get_STEPS lthy3a > 3 |
360 then define_raw_fvs descr sorts raw_bn_info raw_bclauses constr_thms lthy3a |
361 then define_raw_fvs descr sorts raw_bn_info raw_bclauses constr_thms lthy3a |
437 else raise TEST lthy6 |
438 else raise TEST lthy6 |
438 |
439 |
439 (* defining the quotient type *) |
440 (* defining the quotient type *) |
440 val _ = warning "Declaring the quotient types" |
441 val _ = warning "Declaring the quotient types" |
441 val qty_descr = map (fn (vs, bind, mx, _) => (vs, bind, mx)) dts |
442 val qty_descr = map (fn (vs, bind, mx, _) => (vs, bind, mx)) dts |
442 val qty_binds = map (fn (_, bind, _, _) => bind) dts |
443 val qty_binds = map (fn (_, bind, _, _) => bind) dts (* not used *) |
443 val qty_names = map Name.of_binding qty_binds; |
444 val qty_names = map Name.of_binding qty_binds; (* not used *) |
444 val qty_full_names = map (Long_Name.qualify thy_name) qty_names |
445 val qty_full_names = map (Long_Name.qualify thy_name) qty_names (* not used *) |
445 |
446 |
446 val qty_args' = map2 (fn ty => fn trm => (ty, trm, false)) alpha_tys alpha_trms |
|
447 val qty_args = (qty_descr ~~ qty_args') ~~ alpha_equivp_thms |
|
448 |
|
449 val (qty_infos, lthy7) = |
447 val (qty_infos, lthy7) = |
450 if get_STEPS lthy > 14 |
448 if get_STEPS lthy > 14 |
451 then fold_map Quotient_Type.add_quotient_type qty_args lthy6 |
449 then qtype_defs qty_descr alpha_tys alpha_trms alpha_equivp_thms lthy6 |
452 else raise TEST lthy6 |
450 else raise TEST lthy6 |
453 |
451 |
454 val qtys = map #qtyp qty_infos |
452 val qtys = map #qtyp qty_infos |
|
453 |
|
454 val _ = tracing ("all_raw_tys: " ^ commas (map @{make_string} all_raw_tys)) |
|
455 val _ = tracing ("constrs: " ^ commas (map @{make_string} all_raw_constrs)) |
|
456 val _ = tracing ("qtys: " ^ commas (map @{make_string} qtys)) |
|
457 |
|
458 |
455 |
459 |
456 val _ = |
460 val _ = |
457 if get_STEPS lthy > 15 |
461 if get_STEPS lthy > 15 |
458 then true else raise TEST lthy7 |
462 then true else raise TEST lthy7 |
459 |
463 |
463 val raw_consts = |
467 val raw_consts = |
464 flat (map (fn (i, (_, _, l)) => |
468 flat (map (fn (i, (_, _, l)) => |
465 map (fn (cname, dts) => |
469 map (fn (cname, dts) => |
466 Const (cname, map (Datatype_Aux.typ_of_dtyp descr sorts) dts ---> |
470 Const (cname, map (Datatype_Aux.typ_of_dtyp descr sorts) dts ---> |
467 Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec i))) l) descr); |
471 Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec i))) l) descr); |
468 val (consts, const_defs, lthy8) = quotient_lift_consts_export qtys (const_names ~~ raw_consts) lthy7; |
472 val dd = map2 (fn x => fn y => (x, y, NoSyn)) const_names raw_consts |
|
473 val (consts, const_defs, lthy8) = quotient_lift_consts_export qtys dd lthy7; |
469 val _ = warning "Proving respects"; |
474 val _ = warning "Proving respects"; |
470 |
475 |
471 val bn_nos = map (fn (_, i, _) => i) raw_bn_info; |
476 val bn_nos = map (fn (_, i, _) => i) raw_bn_info; |
472 val bns = raw_bn_funs ~~ bn_nos; |
477 val bns = raw_bn_funs ~~ bn_nos; |
473 |
478 |
498 let val alpha_alphabn = prove_alpha_alphabn alpha_trms alpha_induct alpha_eq_iff alpha_bn_trms lthy11a |
503 let val alpha_alphabn = prove_alpha_alphabn alpha_trms alpha_induct alpha_eq_iff alpha_bn_trms lthy11a |
499 in constr_rsp_tac alpha_eq_iff (fv_rsp @ bns_rsp @ alpha_refl_thms @ alpha_alphabn) 1 end |
504 in constr_rsp_tac alpha_eq_iff (fv_rsp @ bns_rsp @ alpha_refl_thms @ alpha_alphabn) 1 end |
500 val (const_rsps, lthy12) = fold_map (fn cnst => prove_const_rsp qtys Binding.empty [cnst] |
505 val (const_rsps, lthy12) = fold_map (fn cnst => prove_const_rsp qtys Binding.empty [cnst] |
501 const_rsp_tac) raw_consts lthy11a |
506 const_rsp_tac) raw_consts lthy11a |
502 val qfv_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) (raw_fvs @ raw_fv_bns) |
507 val qfv_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) (raw_fvs @ raw_fv_bns) |
503 val (qfv_ts, qfv_defs, lthy12a) = quotient_lift_consts_export qtys (qfv_names ~~ (raw_fvs @ raw_fv_bns)) lthy12; |
508 val dd = map2 (fn x => fn y => (x, y, NoSyn)) qfv_names (raw_fvs @ raw_fv_bns) |
|
509 val (qfv_ts, qfv_defs, lthy12a) = quotient_lift_consts_export qtys dd lthy12; |
504 val (qfv_ts_nobn, qfv_ts_bn) = chop (length raw_perm_funs) qfv_ts; |
510 val (qfv_ts_nobn, qfv_ts_bn) = chop (length raw_perm_funs) qfv_ts; |
505 val qbn_names = map (fn (b, _ , _) => Name.of_binding b) bn_funs |
511 val qbn_names = map (fn (b, _ , _) => Name.of_binding b) bn_funs |
506 val (qbn_ts, qbn_defs, lthy12b) = quotient_lift_consts_export qtys (qbn_names ~~ raw_bn_funs) lthy12a; |
512 val dd = map2 (fn x => fn y => (x, y, NoSyn)) qbn_names raw_bn_funs |
|
513 val (qbn_ts, qbn_defs, lthy12b) = quotient_lift_consts_export qtys dd lthy12a; |
507 val qalpha_bn_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) alpha_bn_trms |
514 val qalpha_bn_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) alpha_bn_trms |
508 val (qalpha_bn_trms, qalphabn_defs, lthy12c) = |
515 val dd = map2 (fn x => fn y => (x, y, NoSyn)) qalpha_bn_names alpha_bn_trms |
509 quotient_lift_consts_export qtys (qalpha_bn_names ~~ alpha_bn_trms) lthy12b; |
516 val (qalpha_bn_trms, qalphabn_defs, lthy12c) = quotient_lift_consts_export qtys dd lthy12b; |
510 val _ = warning "Lifting permutations"; |
517 val _ = warning "Lifting permutations"; |
511 val thy = Local_Theory.exit_global lthy12c; |
518 val thy = Local_Theory.exit_global lthy12c; |
512 val perm_names = map (fn x => "permute_" ^ x) qty_names |
519 val perm_names = map (fn x => "permute_" ^ x) qty_names |
513 val thy' = define_lifted_perms qtys qty_full_names (perm_names ~~ raw_perm_funs) raw_perm_simps thy; |
520 val dd = map2 (fn x => fn y => (x, y, NoSyn)) perm_names raw_perm_funs |
|
521 val thy' = define_lifted_perms qtys qty_full_names dd raw_perm_simps thy; |
514 val lthy13 = Theory_Target.init NONE thy'; |
522 val lthy13 = Theory_Target.init NONE thy'; |
515 val q_name = space_implode "_" qty_names; |
523 val q_name = space_implode "_" qty_names; |
516 fun suffix_bind s = Binding.qualify true q_name (Binding.name s); |
524 fun suffix_bind s = Binding.qualify true q_name (Binding.name s); |
517 val _ = warning "Lifting induction"; |
525 val _ = warning "Lifting induction"; |
518 val constr_names = map (Long_Name.base_name o fst o dest_Const) consts; |
526 val constr_names = map (Long_Name.base_name o fst o dest_Const) consts; |