388 else build_equivps alpha_ts reflps alpha_induct |
388 else build_equivps alpha_ts reflps alpha_induct |
389 inject alpha_eq_iff distincts alpha_cases alpha_eqvt lthy6; |
389 inject alpha_eq_iff distincts alpha_cases alpha_eqvt lthy6; |
390 val qty_binds = map (fn (_, b, _, _) => b) dts; |
390 val qty_binds = map (fn (_, b, _, _) => b) dts; |
391 val qty_names = map Name.of_binding qty_binds; |
391 val qty_names = map Name.of_binding qty_binds; |
392 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 |
393 val (q_tys, lthy7) = define_quotient_types qty_binds all_typs alpha_ts_nobn alpha_equivp lthy6; |
393 val (qtys, lthy7) = define_quotient_types qty_binds all_typs alpha_ts_nobn alpha_equivp lthy6; |
394 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)); |
395 val raw_consts = |
395 val raw_consts = |
396 flat (map (fn (i, (_, _, l)) => |
396 flat (map (fn (i, (_, _, l)) => |
397 map (fn (cname, dts) => |
397 map (fn (cname, dts) => |
398 Const (cname, map (typ_of_dtyp descr sorts) dts ---> |
398 Const (cname, map (typ_of_dtyp descr sorts) dts ---> |
399 typ_of_dtyp descr sorts (DtRec i))) l) descr); |
399 typ_of_dtyp descr sorts (DtRec i))) l) descr); |
400 val (consts, const_defs, lthy8) = quotient_lift_consts_export (const_names ~~ raw_consts) lthy7; |
400 val (consts, const_defs, lthy8) = quotient_lift_consts_export qtys (const_names ~~ raw_consts) lthy7; |
401 val _ = tracing "Proving respects"; |
401 val _ = tracing "Proving respects"; |
402 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') |
403 val _ = map tracing (map PolyML.makestring bns_rsp_pre') |
404 val (bns_rsp_pre, lthy9) = fold_map ( |
404 val (bns_rsp_pre, lthy9) = fold_map ( |
405 fn (bn_t, i) => prove_const_rsp Binding.empty [bn_t] (fn _ => |
405 fn (bn_t, i) => prove_const_rsp qtys Binding.empty [bn_t] (fn _ => |
406 resolve_tac bns_rsp_pre' 1)) bns lthy8; |
406 resolve_tac bns_rsp_pre' 1)) bns lthy8; |
407 val bns_rsp = flat (map snd bns_rsp_pre); |
407 val bns_rsp = flat (map snd bns_rsp_pre); |
408 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 |
409 else fvbv_rsp_tac alpha_induct fv_def lthy8 1; |
409 else fvbv_rsp_tac alpha_induct fv_def lthy8 1; |
410 val fv_rsps = prove_fv_rsp fv_alpha_all alpha_ts fv_rsp_tac lthy9; |
410 val fv_rsps = prove_fv_rsp fv_alpha_all alpha_ts fv_rsp_tac lthy9; |
411 val (fv_rsp_pre, lthy10) = fold_map |
411 val (fv_rsp_pre, lthy10) = fold_map |
412 (fn fv => fn ctxt => prove_const_rsp Binding.empty [fv] |
412 (fn fv => fn ctxt => prove_const_rsp qtys Binding.empty [fv] |
413 (fn _ => asm_simp_tac (HOL_ss addsimps fv_rsps) 1) ctxt) fv_ts lthy9; |
413 (fn _ => asm_simp_tac (HOL_ss addsimps fv_rsps) 1) ctxt) fv_ts lthy9; |
414 val fv_rsp = flat (map snd fv_rsp_pre); |
414 val fv_rsp = flat (map snd fv_rsp_pre); |
415 val (perms_rsp, lthy11) = prove_const_rsp Binding.empty perms |
415 val (perms_rsp, lthy11) = prove_const_rsp qtys Binding.empty perms |
416 (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy10; |
416 (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy10; |
417 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; |
417 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; |
418 val (alpha_bn_rsps, lthy11a) = fold_map (fn cnst => prove_const_rsp Binding.empty [cnst] |
418 val (alpha_bn_rsps, lthy11a) = fold_map (fn cnst => prove_const_rsp qtys Binding.empty [cnst] |
419 (fn _ => asm_simp_tac (HOL_ss addsimps alpha_bn_rsp_pre) 1)) alpha_ts_bn lthy11 |
419 (fn _ => asm_simp_tac (HOL_ss addsimps alpha_bn_rsp_pre) 1)) alpha_ts_bn lthy11 |
420 (* val _ = map tracing (map PolyML.makestring alpha_bn_rsps);*) |
420 (* val _ = map tracing (map PolyML.makestring alpha_bn_rsps);*) |
421 fun const_rsp_tac _ = |
421 fun const_rsp_tac _ = |
422 if !cheat_const_rsp then Skip_Proof.cheat_tac thy |
422 if !cheat_const_rsp then Skip_Proof.cheat_tac thy |
423 else let val alpha_alphabn = prove_alpha_alphabn alpha_ts alpha_induct alpha_eq_iff alpha_ts_bn lthy11a |
423 else let val alpha_alphabn = prove_alpha_alphabn alpha_ts alpha_induct alpha_eq_iff alpha_ts_bn lthy11a |
424 in constr_rsp_tac alpha_eq_iff (fv_rsp @ bns_rsp @ reflps @ alpha_alphabn) 1 end |
424 in constr_rsp_tac alpha_eq_iff (fv_rsp @ bns_rsp @ reflps @ alpha_alphabn) 1 end |
425 val (const_rsps, lthy12) = fold_map (fn cnst => prove_const_rsp Binding.empty [cnst] |
425 val (const_rsps, lthy12) = fold_map (fn cnst => prove_const_rsp qtys Binding.empty [cnst] |
426 const_rsp_tac) raw_consts lthy11a |
426 const_rsp_tac) raw_consts lthy11a |
427 val qfv_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) ordered_fv_ts |
427 val qfv_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) ordered_fv_ts |
428 val (qfv_ts, qfv_defs, lthy12a) = quotient_lift_consts_export (qfv_names ~~ ordered_fv_ts) lthy12; |
428 val (qfv_ts, qfv_defs, lthy12a) = quotient_lift_consts_export qtys (qfv_names ~~ ordered_fv_ts) lthy12; |
429 val (qfv_ts_nobn, qfv_ts_bn) = chop (length perms) qfv_ts; |
429 val (qfv_ts_nobn, qfv_ts_bn) = chop (length perms) qfv_ts; |
430 val qbn_names = map (fn (b, _ , _) => Name.of_binding b) bn_funs |
430 val qbn_names = map (fn (b, _ , _) => Name.of_binding b) bn_funs |
431 val (qbn_defs, lthy12b) = fold_map Quotient_Def.quotient_lift_const (qbn_names ~~ raw_bn_funs) lthy12a; |
431 val (qbn_ts, qbn_defs, lthy12b) = quotient_lift_consts_export qtys (qbn_names ~~ raw_bn_funs) lthy12a; |
432 val qalpha_bn_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) alpha_ts_bn |
432 val qalpha_bn_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) alpha_ts_bn |
433 val (qalpha_ts_bn, qbn_defs, lthy12c) = quotient_lift_consts_export (qalpha_bn_names ~~ alpha_ts_bn) lthy12b; |
433 val (qalpha_ts_bn, qalphabn_defs, lthy12c) = quotient_lift_consts_export qtys (qalpha_bn_names ~~ alpha_ts_bn) lthy12b; |
434 val _ = tracing "Lifting permutations"; |
434 val _ = tracing "Lifting permutations"; |
435 val thy = Local_Theory.exit_global lthy12c; |
435 val thy = Local_Theory.exit_global lthy12c; |
436 val perm_names = map (fn x => "permute_" ^ x) qty_names |
436 val perm_names = map (fn x => "permute_" ^ x) qty_names |
437 val thy' = define_lifted_perms qty_full_names (perm_names ~~ perms) raw_perm_simps thy; |
437 val thy' = define_lifted_perms qtys qty_full_names (perm_names ~~ perms) raw_perm_simps thy; |
438 val lthy13 = Theory_Target.init NONE thy'; |
438 val lthy13 = Theory_Target.init NONE thy'; |
439 val q_name = space_implode "_" qty_names; |
439 val q_name = space_implode "_" qty_names; |
440 fun suffix_bind s = Binding.qualify true q_name (Binding.name s); |
440 fun suffix_bind s = Binding.qualify true q_name (Binding.name s); |
441 val _ = tracing "Lifting induction"; |
441 val _ = tracing "Lifting induction"; |
442 val constr_names = map (Long_Name.base_name o fst o dest_Const) consts; |
442 val constr_names = map (Long_Name.base_name o fst o dest_Const) consts; |
443 val q_induct = Rule_Cases.name constr_names (lift_thm lthy13 induct); |
443 val q_induct = Rule_Cases.name constr_names (lift_thm qtys lthy13 induct); |
444 fun note_suffix s th ctxt = |
444 fun note_suffix s th ctxt = |
445 snd (Local_Theory.note ((suffix_bind s, []), th) ctxt); |
445 snd (Local_Theory.note ((suffix_bind s, []), th) ctxt); |
446 fun note_simp_suffix s th ctxt = |
446 fun note_simp_suffix s th ctxt = |
447 snd (Local_Theory.note ((suffix_bind s, [Attrib.internal (K Simplifier.simp_add)]), th) ctxt); |
447 snd (Local_Theory.note ((suffix_bind s, [Attrib.internal (K Simplifier.simp_add)]), th) ctxt); |
448 val (_, lthy14) = Local_Theory.note ((suffix_bind "induct", |
448 val (_, lthy14) = Local_Theory.note ((suffix_bind "induct", |
449 [Attrib.internal (K (Rule_Cases.case_names constr_names))]), [Rule_Cases.name constr_names q_induct]) lthy13; |
449 [Attrib.internal (K (Rule_Cases.case_names constr_names))]), [Rule_Cases.name constr_names q_induct]) lthy13; |
450 val q_inducts = Project_Rule.projects lthy13 (1 upto (length alpha_inducts)) q_induct |
450 val q_inducts = Project_Rule.projects lthy13 (1 upto (length alpha_inducts)) q_induct |
451 val (_, lthy14a) = Local_Theory.note ((suffix_bind "inducts", []), q_inducts) lthy14; |
451 val (_, lthy14a) = Local_Theory.note ((suffix_bind "inducts", []), q_inducts) lthy14; |
452 val q_perm = map (lift_thm lthy14) raw_perm_def; |
452 val q_perm = map (lift_thm qtys lthy14) raw_perm_def; |
453 val lthy15 = note_simp_suffix "perm" q_perm lthy14a; |
453 val lthy15 = note_simp_suffix "perm" q_perm lthy14a; |
454 val q_fv = map (lift_thm lthy15) fv_def; |
454 val q_fv = map (lift_thm qtys lthy15) fv_def; |
455 val lthy16 = note_simp_suffix "fv" q_fv lthy15; |
455 val lthy16 = note_simp_suffix "fv" q_fv lthy15; |
456 val q_bn = map (lift_thm lthy16) raw_bn_eqs; |
456 val q_bn = map (lift_thm qtys lthy16) raw_bn_eqs; |
457 val lthy17 = note_simp_suffix "bn" q_bn lthy16; |
457 val lthy17 = note_simp_suffix "bn" q_bn lthy16; |
458 val _ = tracing "Lifting eq-iff"; |
458 val _ = tracing "Lifting eq-iff"; |
459 val eq_iff_unfolded1 = map (Local_Defs.unfold lthy17 @{thms alphas2}) alpha_eq_iff |
459 val eq_iff_unfolded1 = map (Local_Defs.unfold lthy17 @{thms alphas2}) alpha_eq_iff |
460 val eq_iff_unfolded2 = map (Local_Defs.unfold lthy17 @{thms alphas}) eq_iff_unfolded1 |
460 val eq_iff_unfolded2 = map (Local_Defs.unfold lthy17 @{thms alphas}) eq_iff_unfolded1 |
461 val q_eq_iff_pre1 = map (lift_thm lthy17) eq_iff_unfolded2; |
461 val q_eq_iff_pre1 = map (lift_thm qtys lthy17) eq_iff_unfolded2; |
462 val q_eq_iff_pre2 = map (Local_Defs.fold lthy17 @{thms alphas2}) q_eq_iff_pre1 |
462 val q_eq_iff_pre2 = map (Local_Defs.fold lthy17 @{thms alphas2}) q_eq_iff_pre1 |
463 val q_eq_iff = map (Local_Defs.fold lthy17 @{thms alphas}) q_eq_iff_pre2 |
463 val q_eq_iff = map (Local_Defs.fold lthy17 @{thms alphas}) q_eq_iff_pre2 |
464 val (_, lthy18) = Local_Theory.note ((suffix_bind "eq_iff", []), q_eq_iff) lthy17; |
464 val (_, lthy18) = Local_Theory.note ((suffix_bind "eq_iff", []), q_eq_iff) lthy17; |
465 val q_dis = map (lift_thm lthy18) rel_dists; |
465 val q_dis = map (lift_thm qtys lthy18) rel_dists; |
466 val lthy19 = note_simp_suffix "distinct" q_dis lthy18; |
466 val lthy19 = note_simp_suffix "distinct" q_dis lthy18; |
467 val q_eqvt = map (lift_thm lthy19) (bv_eqvt @ fv_eqvt); |
467 val q_eqvt = map (lift_thm qtys lthy19) (bv_eqvt @ fv_eqvt); |
468 val (_, lthy20) = Local_Theory.note ((Binding.empty, |
468 val (_, lthy20) = Local_Theory.note ((Binding.empty, |
469 [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), q_eqvt) lthy19; |
469 [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), q_eqvt) lthy19; |
470 val _ = tracing "Finite Support"; |
470 val _ = tracing "Finite Support"; |
471 val supports = map (prove_supports lthy20 q_perm) consts; |
471 val supports = map (prove_supports lthy20 q_perm) consts; |
472 val fin_supp = HOLogic.conj_elims (prove_fs lthy20 q_induct supports q_tys); |
472 val fin_supp = HOLogic.conj_elims (prove_fs lthy20 q_induct supports qtys); |
473 val thy3 = Local_Theory.exit_global lthy20; |
473 val thy3 = Local_Theory.exit_global lthy20; |
474 val lthy21 = Theory_Target.instantiation (qty_full_names, [], @{sort fs}) thy3; |
474 val lthy21 = Theory_Target.instantiation (qty_full_names, [], @{sort fs}) thy3; |
475 fun tac _ = Class.intro_classes_tac [] THEN (ALLGOALS (resolve_tac fin_supp)) |
475 fun tac _ = Class.intro_classes_tac [] THEN (ALLGOALS (resolve_tac fin_supp)) |
476 val lthy22 = Class.prove_instantiation_instance tac lthy21 |
476 val lthy22 = Class.prove_instantiation_instance tac lthy21 |
477 val fv_alpha_all = combine_fv_alpha_bns (qfv_ts_nobn, qfv_ts_bn) (alpha_ts_nobn, qalpha_ts_bn) bn_nos; |
477 val fv_alpha_all = combine_fv_alpha_bns (qfv_ts_nobn, qfv_ts_bn) (alpha_ts_nobn, qalpha_ts_bn) bn_nos; |