385 val exhausts = map #exhaust dtinfos; |
385 val exhausts = map #exhaust dtinfos; |
386 val _ = tracing "Defining permutations, fv and alpha"; |
386 val _ = tracing "Defining permutations, fv and alpha"; |
387 val ((raw_perm_def, raw_perm_simps, perms), lthy3) = |
387 val ((raw_perm_def, raw_perm_simps, perms), lthy3) = |
388 Local_Theory.theory_result (define_raw_perms dtinfo (length dts)) lthy2; |
388 Local_Theory.theory_result (define_raw_perms dtinfo (length dts)) lthy2; |
389 val raw_binds_flat = map (map flat) raw_binds; |
389 val raw_binds_flat = map (map flat) raw_binds; |
390 val ((((fv_ts, ordered_fv_ts), fv_def), ((alpha_ts, alpha_intros), (alpha_cases, alpha_induct))), lthy4) = |
390 val ((((_, fv_ts), fv_def), ((alpha_ts, alpha_intros), (alpha_cases, alpha_induct))), lthy4) = |
391 define_fv_alpha_export dtinfo raw_binds_flat bn_funs_decls lthy3; |
391 define_fv_alpha_export dtinfo raw_binds_flat bn_funs_decls lthy3; |
392 val (fv_ts_nobn, fv_ts_bn) = chop (length perms) fv_ts; |
392 val (fv, fvbn) = chop (length perms) fv_ts; |
393 val (alpha_ts_nobn, alpha_ts_bn) = chop (length perms) alpha_ts |
393 |
394 val alpha_inducts = Project_Rule.projects lthy4 (1 upto (length dts)) alpha_induct; |
394 val (alpha_ts_nobn, alpha_ts_bn) = chop (length fv) alpha_ts |
395 val dts_names = map (fn (i, (s, _, _)) => (s, i)) (#descr dtinfo); |
395 val dts_names = map (fn (i, (s, _, _)) => (s, i)) (#descr dtinfo); |
396 val bn_tys = map (domain_type o fastype_of) raw_bn_funs; |
396 val bn_tys = map (domain_type o fastype_of) raw_bn_funs; |
397 val bn_nos = map (dtyp_no_of_typ dts_names) bn_tys; |
397 val bn_nos = map (dtyp_no_of_typ dts_names) bn_tys; |
398 val bns = raw_bn_funs ~~ bn_nos; |
398 val bns = raw_bn_funs ~~ bn_nos; |
399 val rel_dists = flat (map (distinct_rel lthy4 alpha_cases) |
399 val rel_dists = flat (map (distinct_rel lthy4 alpha_cases) |
401 val rel_dists_bn = flat (map (distinct_rel lthy4 alpha_cases) |
401 val rel_dists_bn = flat (map (distinct_rel lthy4 alpha_cases) |
402 ((map (fn i => nth rel_distinct i) bn_nos) ~~ alpha_ts_bn)) |
402 ((map (fn i => nth rel_distinct i) bn_nos) ~~ alpha_ts_bn)) |
403 val alpha_eq_iff = build_rel_inj alpha_intros (inject @ distincts) alpha_cases lthy4 |
403 val alpha_eq_iff = build_rel_inj alpha_intros (inject @ distincts) alpha_cases lthy4 |
404 val _ = tracing "Proving equivariance"; |
404 val _ = tracing "Proving equivariance"; |
405 val (bv_eqvt, lthy5) = prove_eqvt raw_tys induct (raw_bn_eqs @ raw_perm_def) (map fst bns) lthy4 |
405 val (bv_eqvt, lthy5) = prove_eqvt raw_tys induct (raw_bn_eqs @ raw_perm_def) (map fst bns) lthy4 |
406 val (fv_eqvt, lthy6) = prove_eqvt raw_tys induct (fv_def @ raw_perm_def) (fv_ts_nobn @ fv_ts_bn) lthy5 |
406 val (fv_eqvt, lthy6) = prove_eqvt raw_tys induct (fv_def @ raw_perm_def) (fv @ fvbn) lthy5 |
407 fun alpha_eqvt_tac' _ = |
407 fun alpha_eqvt_tac' _ = |
408 if !cheat_alpha_eqvt then Skip_Proof.cheat_tac thy |
408 if !cheat_alpha_eqvt then Skip_Proof.cheat_tac thy |
409 else alpha_eqvt_tac alpha_induct (raw_perm_def @ alpha_eq_iff) lthy6 1 |
409 else alpha_eqvt_tac alpha_induct (raw_perm_def @ alpha_eq_iff) lthy6 1 |
410 val alpha_eqvt = build_alpha_eqvts alpha_ts alpha_eqvt_tac' lthy6; |
410 val alpha_eqvt = build_alpha_eqvts alpha_ts alpha_eqvt_tac' lthy6; |
411 val _ = tracing "Proving equivalence"; |
411 val _ = tracing "Proving equivalence"; |
412 val (rfv_ts_nobn, rfv_ts_bn) = chop (length perms) ordered_fv_ts; |
412 val fv_alpha_all = combine_fv_alpha_bns (fv, fvbn) (alpha_ts_nobn, alpha_ts_bn) bn_nos; |
413 val fv_alpha_all = combine_fv_alpha_bns (rfv_ts_nobn, rfv_ts_bn) (alpha_ts_nobn, alpha_ts_bn) bn_nos; |
|
414 val reflps = build_alpha_refl fv_alpha_all alpha_ts induct alpha_eq_iff lthy6; |
413 val reflps = build_alpha_refl fv_alpha_all alpha_ts induct alpha_eq_iff lthy6; |
415 val alpha_equivp = |
414 val alpha_equivp = |
416 if !cheat_equivp then map (equivp_hack lthy6) alpha_ts_nobn |
415 if !cheat_equivp then map (equivp_hack lthy6) alpha_ts_nobn |
417 else build_equivps alpha_ts reflps alpha_induct |
416 else build_equivps alpha_ts reflps alpha_induct |
418 inject alpha_eq_iff distincts alpha_cases alpha_eqvt lthy6; |
417 inject alpha_eq_iff distincts alpha_cases alpha_eqvt lthy6; |
427 Const (cname, map (typ_of_dtyp descr sorts) dts ---> |
426 Const (cname, map (typ_of_dtyp descr sorts) dts ---> |
428 typ_of_dtyp descr sorts (DtRec i))) l) descr); |
427 typ_of_dtyp descr sorts (DtRec i))) l) descr); |
429 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; |
430 val _ = tracing "Proving respects"; |
429 val _ = tracing "Proving respects"; |
431 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; |
432 val _ = map tracing (map PolyML.makestring bns_rsp_pre') |
|
433 val (bns_rsp_pre, lthy9) = fold_map ( |
431 val (bns_rsp_pre, lthy9) = fold_map ( |
434 fn (bn_t, i) => prove_const_rsp qtys Binding.empty [bn_t] (fn _ => |
432 fn (bn_t, _) => prove_const_rsp qtys Binding.empty [bn_t] (fn _ => |
435 resolve_tac bns_rsp_pre' 1)) bns lthy8; |
433 resolve_tac bns_rsp_pre' 1)) bns lthy8; |
436 val bns_rsp = flat (map snd bns_rsp_pre); |
434 val bns_rsp = flat (map snd bns_rsp_pre); |
437 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 |
438 else fvbv_rsp_tac alpha_induct fv_def lthy8 1; |
436 else fvbv_rsp_tac alpha_induct fv_def lthy8 1; |
439 val fv_rsps = prove_fv_rsp fv_alpha_all alpha_ts fv_rsp_tac lthy9; |
437 val fv_rsps = prove_fv_rsp fv_alpha_all alpha_ts fv_rsp_tac lthy9; |
440 val (fv_rsp_pre, lthy10) = fold_map |
438 val (fv_rsp_pre, lthy10) = fold_map |
441 (fn fv => fn ctxt => prove_const_rsp qtys Binding.empty [fv] |
439 (fn fv => fn ctxt => prove_const_rsp qtys Binding.empty [fv] |
442 (fn _ => asm_simp_tac (HOL_ss addsimps fv_rsps) 1) ctxt) fv_ts lthy9; |
440 (fn _ => asm_simp_tac (HOL_ss addsimps fv_rsps) 1) ctxt) (fv @ fvbn) lthy9; |
443 val fv_rsp = flat (map snd fv_rsp_pre); |
441 val fv_rsp = flat (map snd fv_rsp_pre); |
444 val (perms_rsp, lthy11) = prove_const_rsp qtys Binding.empty perms |
442 val (perms_rsp, lthy11) = prove_const_rsp qtys Binding.empty perms |
445 (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy10; |
443 (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy10; |
446 val alpha_bn_rsp_pre = prove_alpha_bn_rsp alpha_ts alpha_induct (alpha_eq_iff @ rel_dists @ rel_dists_bn) alpha_equivp exhausts alpha_ts_bn lthy11; |
444 val alpha_bn_rsp_pre = prove_alpha_bn_rsp alpha_ts alpha_induct (alpha_eq_iff @ rel_dists @ rel_dists_bn) alpha_equivp exhausts alpha_ts_bn lthy11; |
447 val (alpha_bn_rsps, lthy11a) = fold_map (fn cnst => prove_const_rsp qtys Binding.empty [cnst] |
445 val (alpha_bn_rsps, lthy11a) = fold_map (fn cnst => prove_const_rsp qtys Binding.empty [cnst] |
451 if !cheat_const_rsp then Skip_Proof.cheat_tac thy |
449 if !cheat_const_rsp then Skip_Proof.cheat_tac thy |
452 else let val alpha_alphabn = prove_alpha_alphabn alpha_ts alpha_induct alpha_eq_iff alpha_ts_bn lthy11a |
450 else let val alpha_alphabn = prove_alpha_alphabn alpha_ts alpha_induct alpha_eq_iff alpha_ts_bn lthy11a |
453 in constr_rsp_tac alpha_eq_iff (fv_rsp @ bns_rsp @ reflps @ alpha_alphabn) 1 end |
451 in constr_rsp_tac alpha_eq_iff (fv_rsp @ bns_rsp @ reflps @ alpha_alphabn) 1 end |
454 val (const_rsps, lthy12) = fold_map (fn cnst => prove_const_rsp qtys Binding.empty [cnst] |
452 val (const_rsps, lthy12) = fold_map (fn cnst => prove_const_rsp qtys Binding.empty [cnst] |
455 const_rsp_tac) raw_consts lthy11a |
453 const_rsp_tac) raw_consts lthy11a |
456 val qfv_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) ordered_fv_ts |
454 val qfv_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) (fv @ fvbn) |
457 val (qfv_ts, qfv_defs, lthy12a) = quotient_lift_consts_export qtys (qfv_names ~~ ordered_fv_ts) lthy12; |
455 val (qfv_ts, qfv_defs, lthy12a) = quotient_lift_consts_export qtys (qfv_names ~~ (fv @ fvbn)) lthy12; |
458 val (qfv_ts_nobn, qfv_ts_bn) = chop (length perms) qfv_ts; |
456 val (qfv_ts_nobn, qfv_ts_bn) = chop (length perms) qfv_ts; |
459 val qbn_names = map (fn (b, _ , _) => Name.of_binding b) bn_funs |
457 val qbn_names = map (fn (b, _ , _) => Name.of_binding b) bn_funs |
460 val (qbn_ts, qbn_defs, lthy12b) = quotient_lift_consts_export qtys (qbn_names ~~ raw_bn_funs) lthy12a; |
458 val (qbn_ts, qbn_defs, lthy12b) = quotient_lift_consts_export qtys (qbn_names ~~ raw_bn_funs) lthy12a; |
461 val qalpha_bn_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) alpha_ts_bn |
459 val qalpha_bn_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) alpha_ts_bn |
462 val (qalpha_ts_bn, qalphabn_defs, lthy12c) = quotient_lift_consts_export qtys (qalpha_bn_names ~~ alpha_ts_bn) lthy12b; |
460 val (qalpha_ts_bn, qalphabn_defs, lthy12c) = quotient_lift_consts_export qtys (qalpha_bn_names ~~ alpha_ts_bn) lthy12b; |
474 snd (Local_Theory.note ((suffix_bind s, []), th) ctxt); |
472 snd (Local_Theory.note ((suffix_bind s, []), th) ctxt); |
475 fun note_simp_suffix s th ctxt = |
473 fun note_simp_suffix s th ctxt = |
476 snd (Local_Theory.note ((suffix_bind s, [Attrib.internal (K Simplifier.simp_add)]), th) ctxt); |
474 snd (Local_Theory.note ((suffix_bind s, [Attrib.internal (K Simplifier.simp_add)]), th) ctxt); |
477 val (_, lthy14) = Local_Theory.note ((suffix_bind "induct", |
475 val (_, lthy14) = Local_Theory.note ((suffix_bind "induct", |
478 [Attrib.internal (K (Rule_Cases.case_names constr_names))]), [Rule_Cases.name constr_names q_induct]) lthy13; |
476 [Attrib.internal (K (Rule_Cases.case_names constr_names))]), [Rule_Cases.name constr_names q_induct]) lthy13; |
479 val q_inducts = Project_Rule.projects lthy13 (1 upto (length alpha_inducts)) q_induct |
477 val q_inducts = Project_Rule.projects lthy13 (1 upto (length fv)) q_induct |
480 val (_, lthy14a) = Local_Theory.note ((suffix_bind "inducts", []), q_inducts) lthy14; |
478 val (_, lthy14a) = Local_Theory.note ((suffix_bind "inducts", []), q_inducts) lthy14; |
481 val q_perm = map (lift_thm qtys lthy14) raw_perm_def; |
479 val q_perm = map (lift_thm qtys lthy14) raw_perm_def; |
482 val lthy15 = note_simp_suffix "perm" q_perm lthy14a; |
480 val lthy15 = note_simp_suffix "perm" q_perm lthy14a; |
483 val q_fv = map (lift_thm qtys lthy15) fv_def; |
481 val q_fv = map (lift_thm qtys lthy15) fv_def; |
484 val lthy16 = note_simp_suffix "fv" q_fv lthy15; |
482 val lthy16 = note_simp_suffix "fv" q_fv lthy15; |