434 if get_STEPS lthy > 11 |
434 if get_STEPS lthy > 11 |
435 then raw_prove_trans (alpha_trms @ alpha_bn_trms) (distinct_thms @ inject_thms) |
435 then raw_prove_trans (alpha_trms @ alpha_bn_trms) (distinct_thms @ inject_thms) |
436 alpha_intros alpha_induct alpha_cases lthy_tmp'' |
436 alpha_intros alpha_induct alpha_cases lthy_tmp'' |
437 else raise TEST lthy4 |
437 else raise TEST lthy4 |
438 |
438 |
|
439 val alpha_equivp_thms = |
|
440 if get_STEPS lthy > 12 |
|
441 then raw_prove_equivp alpha_trms alpha_refl_thms alpha_sym_thms alpha_trans_thms lthy_tmp'' |
|
442 else raise TEST lthy4 |
|
443 |
439 (* proving alpha implies alpha_bn *) |
444 (* proving alpha implies alpha_bn *) |
440 val _ = warning "Proving alpha implies bn" |
445 val _ = warning "Proving alpha implies bn" |
441 |
446 |
442 val alpha_bn_imp_thms = |
447 val alpha_bn_imp_thms = |
443 if get_STEPS lthy > 12 |
448 if get_STEPS lthy > 13 |
444 then raw_prove_bn_imp alpha_trms alpha_bn_trms alpha_intros alpha_induct lthy_tmp'' |
449 then raw_prove_bn_imp alpha_trms alpha_bn_trms alpha_intros alpha_induct lthy_tmp'' |
445 else raise TEST lthy4 |
450 else raise TEST lthy4 |
446 |
451 |
447 |
|
448 val _ = tracing ("alphas " ^ commas (map (Syntax.string_of_term lthy4) alpha_trms)) |
452 val _ = tracing ("alphas " ^ commas (map (Syntax.string_of_term lthy4) alpha_trms)) |
449 val _ = tracing ("alpha_bns " ^ commas (map (Syntax.string_of_term lthy4) alpha_bn_trms)) |
453 val _ = tracing ("alpha_bns " ^ commas (map (Syntax.string_of_term lthy4) alpha_bn_trms)) |
450 val _ = tracing ("alpha_refl\n" ^ |
454 val _ = tracing ("alpha_refl\n" ^ |
451 cat_lines (map (Syntax.string_of_term lthy4 o prop_of) alpha_refl_thms)) |
455 cat_lines (map (Syntax.string_of_term lthy4 o prop_of) alpha_refl_thms)) |
452 val _ = tracing ("alpha_bn_imp\n" ^ |
456 val _ = tracing ("alpha_bn_imp\n" ^ |
453 cat_lines (map (Syntax.string_of_term lthy4 o prop_of) alpha_bn_imp_thms)) |
457 cat_lines (map (Syntax.string_of_term lthy4 o prop_of) alpha_bn_imp_thms)) |
|
458 val _ = tracing ("alpha_equivp\n" ^ |
|
459 cat_lines (map (Syntax.string_of_term lthy4 o prop_of) alpha_equivp_thms)) |
454 |
460 |
455 (* old stuff *) |
461 (* old stuff *) |
456 val _ = |
462 val _ = |
457 if get_STEPS lthy > 13 |
463 if get_STEPS lthy > 14 |
458 then true else raise TEST lthy4 |
|
459 |
|
460 val bn_nos = map (fn (_, i, _) => i) raw_bn_info; |
|
461 val bns = raw_bn_funs ~~ bn_nos; |
|
462 |
|
463 val fv_alpha_all = combine_fv_alpha_bns (raw_fvs, raw_fv_bns) (alpha_trms, alpha_bn_trms) bn_nos |
|
464 |
|
465 val reflps = build_alpha_refl fv_alpha_all alpha_trms induct_thm alpha_eq_iff lthy4; |
|
466 |
|
467 val _ = tracing ("reflps\n" ^ |
|
468 cat_lines (map (Syntax.string_of_term lthy4 o prop_of) reflps)) |
|
469 |
|
470 val _ = |
|
471 if get_STEPS lthy > 13 |
|
472 then true else raise TEST lthy4 |
464 then true else raise TEST lthy4 |
473 |
465 |
474 val alpha_equivp = |
466 val alpha_equivp = |
475 if !cheat_equivp then map (equivp_hack lthy4) alpha_trms |
467 if !cheat_equivp then map (equivp_hack lthy4) alpha_trms |
476 else build_equivps alpha_trms reflps alpha_induct |
468 else build_equivps alpha_trms alpha_refl_thms alpha_induct |
477 inject_thms alpha_eq_iff distinct_thms alpha_cases alpha_eqvt lthy4; |
469 inject_thms alpha_eq_iff distinct_thms alpha_cases alpha_eqvt lthy4; |
478 |
470 |
479 val qty_binds = map (fn (_, b, _, _) => b) dts; |
471 val qty_binds = map (fn (_, b, _, _) => b) dts; |
480 val qty_names = map Name.of_binding qty_binds; |
472 val qty_names = map Name.of_binding qty_binds; |
481 val qty_full_names = map (Long_Name.qualify thy_name) qty_names |
473 val qty_full_names = map (Long_Name.qualify thy_name) qty_names |
486 map (fn (cname, dts) => |
478 map (fn (cname, dts) => |
487 Const (cname, map (Datatype_Aux.typ_of_dtyp descr sorts) dts ---> |
479 Const (cname, map (Datatype_Aux.typ_of_dtyp descr sorts) dts ---> |
488 Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec i))) l) descr); |
480 Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec i))) l) descr); |
489 val (consts, const_defs, lthy8) = quotient_lift_consts_export qtys (const_names ~~ raw_consts) lthy7; |
481 val (consts, const_defs, lthy8) = quotient_lift_consts_export qtys (const_names ~~ raw_consts) lthy7; |
490 val _ = warning "Proving respects"; |
482 val _ = warning "Proving respects"; |
|
483 |
|
484 val bn_nos = map (fn (_, i, _) => i) raw_bn_info; |
|
485 val bns = raw_bn_funs ~~ bn_nos; |
|
486 |
491 val bns_rsp_pre' = build_fvbv_rsps alpha_trms alpha_induct raw_bn_eqs (map fst bns) lthy8; |
487 val bns_rsp_pre' = build_fvbv_rsps alpha_trms alpha_induct raw_bn_eqs (map fst bns) lthy8; |
492 val (bns_rsp_pre, lthy9) = fold_map ( |
488 val (bns_rsp_pre, lthy9) = fold_map ( |
493 fn (bn_t, _) => prove_const_rsp qtys Binding.empty [bn_t] (fn _ => |
489 fn (bn_t, _) => prove_const_rsp qtys Binding.empty [bn_t] (fn _ => |
494 resolve_tac bns_rsp_pre' 1)) bns lthy8; |
490 resolve_tac bns_rsp_pre' 1)) bns lthy8; |
495 val bns_rsp = flat (map snd bns_rsp_pre); |
491 val bns_rsp = flat (map snd bns_rsp_pre); |
496 |
492 |
497 fun fv_rsp_tac _ = if !cheat_fv_rsp then Skip_Proof.cheat_tac thy |
493 fun fv_rsp_tac _ = if !cheat_fv_rsp then Skip_Proof.cheat_tac thy |
498 else fvbv_rsp_tac alpha_induct raw_fv_defs lthy8 1; |
494 else fvbv_rsp_tac alpha_induct raw_fv_defs lthy8 1; |
|
495 |
|
496 val fv_alpha_all = combine_fv_alpha_bns (raw_fvs, raw_fv_bns) (alpha_trms, alpha_bn_trms) bn_nos |
|
497 |
499 val fv_rsps = prove_fv_rsp fv_alpha_all alpha_trms fv_rsp_tac lthy9; |
498 val fv_rsps = prove_fv_rsp fv_alpha_all alpha_trms fv_rsp_tac lthy9; |
500 val (fv_rsp_pre, lthy10) = fold_map |
499 val (fv_rsp_pre, lthy10) = fold_map |
501 (fn fv => fn ctxt => prove_const_rsp qtys Binding.empty [fv] |
500 (fn fv => fn ctxt => prove_const_rsp qtys Binding.empty [fv] |
502 (fn _ => asm_simp_tac (HOL_ss addsimps fv_rsps) 1) ctxt) (raw_fvs @ raw_fv_bns) lthy9; |
501 (fn _ => asm_simp_tac (HOL_ss addsimps fv_rsps) 1) ctxt) (raw_fvs @ raw_fv_bns) lthy9; |
503 val fv_rsp = flat (map snd fv_rsp_pre); |
502 val fv_rsp = flat (map snd fv_rsp_pre); |
508 let val alpha_bn_rsp_pre = prove_alpha_bn_rsp alpha_trms alpha_induct (alpha_eq_iff @ alpha_distincts @ alpha_bn_distincts) alpha_equivp exhaust_thms alpha_bn_trms lthy11 in asm_simp_tac (HOL_ss addsimps alpha_bn_rsp_pre) 1 end; |
507 let val alpha_bn_rsp_pre = prove_alpha_bn_rsp alpha_trms alpha_induct (alpha_eq_iff @ alpha_distincts @ alpha_bn_distincts) alpha_equivp exhaust_thms alpha_bn_trms lthy11 in asm_simp_tac (HOL_ss addsimps alpha_bn_rsp_pre) 1 end; |
509 val (alpha_bn_rsps, lthy11a) = fold_map (fn cnst => prove_const_rsp qtys Binding.empty [cnst] |
508 val (alpha_bn_rsps, lthy11a) = fold_map (fn cnst => prove_const_rsp qtys Binding.empty [cnst] |
510 alpha_bn_rsp_tac) alpha_bn_trms lthy11 |
509 alpha_bn_rsp_tac) alpha_bn_trms lthy11 |
511 fun const_rsp_tac _ = |
510 fun const_rsp_tac _ = |
512 let val alpha_alphabn = prove_alpha_alphabn alpha_trms alpha_induct alpha_eq_iff alpha_bn_trms lthy11a |
511 let val alpha_alphabn = prove_alpha_alphabn alpha_trms alpha_induct alpha_eq_iff alpha_bn_trms lthy11a |
513 in constr_rsp_tac alpha_eq_iff (fv_rsp @ bns_rsp @ reflps @ alpha_alphabn) 1 end |
512 in constr_rsp_tac alpha_eq_iff (fv_rsp @ bns_rsp @ alpha_refl_thms @ alpha_alphabn) 1 end |
514 val (const_rsps, lthy12) = fold_map (fn cnst => prove_const_rsp qtys Binding.empty [cnst] |
513 val (const_rsps, lthy12) = fold_map (fn cnst => prove_const_rsp qtys Binding.empty [cnst] |
515 const_rsp_tac) raw_consts lthy11a |
514 const_rsp_tac) raw_consts lthy11a |
516 val qfv_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) (raw_fvs @ raw_fv_bns) |
515 val qfv_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) (raw_fvs @ raw_fv_bns) |
517 val (qfv_ts, qfv_defs, lthy12a) = quotient_lift_consts_export qtys (qfv_names ~~ (raw_fvs @ raw_fv_bns)) lthy12; |
516 val (qfv_ts, qfv_defs, lthy12a) = quotient_lift_consts_export qtys (qfv_names ~~ (raw_fvs @ raw_fv_bns)) lthy12; |
518 val (qfv_ts_nobn, qfv_ts_bn) = chop (length raw_perm_funs) qfv_ts; |
517 val (qfv_ts_nobn, qfv_ts_bn) = chop (length raw_perm_funs) qfv_ts; |