395 val rel_dists_bn = flat (map (distinct_rel lthy4 alpha_cases) |
395 val rel_dists_bn = flat (map (distinct_rel lthy4 alpha_cases) |
396 ((map (fn i => nth rel_distinct i) bn_nos) ~~ alpha_ts_bn)) |
396 ((map (fn i => nth rel_distinct i) bn_nos) ~~ alpha_ts_bn)) |
397 |
397 |
398 (* definition of raw_alpha_eq_iff lemmas *) |
398 (* definition of raw_alpha_eq_iff lemmas *) |
399 val alpha_eq_iff = build_rel_inj alpha_intros (inject @ distincts) alpha_cases lthy4 |
399 val alpha_eq_iff = build_rel_inj alpha_intros (inject @ distincts) alpha_cases lthy4 |
400 |
400 val alpha_eq_iff_simp = map (fn x => @{thm simp_thms(6)} OF [x] handle THM _ => x) alpha_eq_iff; |
|
401 |
401 (* proving equivariance lemmas *) |
402 (* proving equivariance lemmas *) |
402 val _ = warning "Proving equivariance"; |
403 val _ = warning "Proving equivariance"; |
403 val (bv_eqvt, lthy5) = prove_eqvt raw_tys induct (raw_bn_eqs @ raw_perm_def) (map fst bns) lthy4 |
404 val (bv_eqvt, lthy5) = prove_eqvt raw_tys induct (raw_bn_eqs @ raw_perm_def) (map fst bns) lthy4 |
404 val (fv_eqvt, lthy6) = prove_eqvt raw_tys induct (fv_def @ raw_perm_def) (fv @ fvbn) lthy5 |
405 val (fv_eqvt, lthy6) = prove_eqvt raw_tys induct (fv_def @ raw_perm_def) (fv @ fvbn) lthy5 |
405 fun alpha_eqvt_tac' _ = |
406 fun alpha_eqvt_tac' _ = |
406 if !cheat_alpha_eqvt then Skip_Proof.cheat_tac thy |
407 if !cheat_alpha_eqvt then Skip_Proof.cheat_tac thy |
407 else alpha_eqvt_tac alpha_induct (raw_perm_def @ alpha_eq_iff) lthy6 1 |
408 else alpha_eqvt_tac alpha_induct (raw_perm_def @ alpha_eq_iff_simp) lthy6 1 |
408 val alpha_eqvt = build_alpha_eqvts alpha_ts alpha_eqvt_tac' lthy6; |
409 val alpha_eqvt = build_alpha_eqvts alpha_ts alpha_eqvt_tac' lthy6; |
409 |
410 |
410 (* provind alpha equivalence *) |
411 (* provind alpha equivalence *) |
411 val _ = warning "Proving equivalence"; |
412 val _ = warning "Proving equivalence"; |
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 (fv, fvbn) (alpha_ts_nobn, alpha_ts_bn) bn_nos; |
413 val reflps = build_alpha_refl fv_alpha_all alpha_ts induct alpha_eq_iff lthy6; |
414 val reflps = build_alpha_refl fv_alpha_all alpha_ts induct alpha_eq_iff_simp lthy6; |
414 val alpha_equivp = |
415 val alpha_equivp = |
415 if !cheat_equivp then map (equivp_hack lthy6) alpha_ts |
416 if !cheat_equivp then map (equivp_hack lthy6) alpha_ts |
416 else build_equivps alpha_ts reflps alpha_induct |
417 else build_equivps alpha_ts reflps alpha_induct |
417 inject alpha_eq_iff distincts alpha_cases alpha_eqvt lthy6; |
418 inject alpha_eq_iff_simp distincts alpha_cases alpha_eqvt lthy6; |
418 val qty_binds = map (fn (_, b, _, _) => b) dts; |
419 val qty_binds = map (fn (_, b, _, _) => b) dts; |
419 val qty_names = map Name.of_binding qty_binds; |
420 val qty_names = map Name.of_binding qty_binds; |
420 val qty_full_names = map (Long_Name.qualify thy_name) qty_names |
421 val qty_full_names = map (Long_Name.qualify thy_name) qty_names |
421 val (qtys, lthy7) = define_quotient_types qty_binds all_typs alpha_ts_nobn alpha_equivp lthy6; |
422 val (qtys, lthy7) = define_quotient_types qty_binds all_typs alpha_ts_nobn alpha_equivp lthy6; |
422 val const_names = map Name.of_binding (flat (map (fn (_, _, _, t) => map (fn (b, _, _) => b) t) dts)); |
423 val const_names = map Name.of_binding (flat (map (fn (_, _, _, t) => map (fn (b, _, _) => b) t) dts)); |
440 (fn fv => fn ctxt => prove_const_rsp qtys Binding.empty [fv] |
441 (fn fv => fn ctxt => prove_const_rsp qtys Binding.empty [fv] |
441 (fn _ => asm_simp_tac (HOL_ss addsimps fv_rsps) 1) ctxt) (fv @ fvbn) lthy9; |
442 (fn _ => asm_simp_tac (HOL_ss addsimps fv_rsps) 1) ctxt) (fv @ fvbn) lthy9; |
442 val fv_rsp = flat (map snd fv_rsp_pre); |
443 val fv_rsp = flat (map snd fv_rsp_pre); |
443 val (perms_rsp, lthy11) = prove_const_rsp qtys Binding.empty perms |
444 val (perms_rsp, lthy11) = prove_const_rsp qtys Binding.empty perms |
444 (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy10; |
445 (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy10; |
445 (* 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;*) |
446 (* val alpha_bn_rsp_pre = prove_alpha_bn_rsp alpha_ts alpha_induct (alpha_eq_iff_simp @ rel_dists @ rel_dists_bn) alpha_equivp exhausts alpha_ts_bn lthy11;*) |
446 val (alpha_bn_rsps, lthy11a) = fold_map (fn cnst => prove_const_rsp qtys Binding.empty [cnst] |
447 val (alpha_bn_rsps, lthy11a) = fold_map (fn cnst => prove_const_rsp qtys Binding.empty [cnst] |
447 (fn _ => Skip_Proof.cheat_tac thy)) alpha_ts_bn lthy11 |
448 (fn _ => Skip_Proof.cheat_tac thy)) alpha_ts_bn lthy11 |
448 fun const_rsp_tac _ = |
449 fun const_rsp_tac _ = |
449 let val alpha_alphabn = prove_alpha_alphabn alpha_ts alpha_induct alpha_eq_iff alpha_ts_bn lthy11a |
450 let val alpha_alphabn = prove_alpha_alphabn alpha_ts alpha_induct alpha_eq_iff_simp alpha_ts_bn lthy11a |
450 in constr_rsp_tac alpha_eq_iff (fv_rsp @ bns_rsp @ reflps @ alpha_alphabn) 1 end |
451 in constr_rsp_tac alpha_eq_iff_simp (fv_rsp @ bns_rsp @ reflps @ alpha_alphabn) 1 end |
451 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] |
452 const_rsp_tac) raw_consts lthy11a |
453 const_rsp_tac) raw_consts lthy11a |
453 val qfv_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) (fv @ fvbn) |
454 val qfv_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) (fv @ fvbn) |
454 val (qfv_ts, qfv_defs, lthy12a) = quotient_lift_consts_export qtys (qfv_names ~~ (fv @ fvbn)) lthy12; |
455 val (qfv_ts, qfv_defs, lthy12a) = quotient_lift_consts_export qtys (qfv_names ~~ (fv @ fvbn)) lthy12; |
455 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; |
507 fun tac _ = Class.intro_classes_tac [] THEN (ALLGOALS (resolve_tac fin_supp)) |
508 fun tac _ = Class.intro_classes_tac [] THEN (ALLGOALS (resolve_tac fin_supp)) |
508 val lthy22 = Class.prove_instantiation_instance tac lthy21 |
509 val lthy22 = Class.prove_instantiation_instance tac lthy21 |
509 val fv_alpha_all = combine_fv_alpha_bns (qfv_ts_nobn, qfv_ts_bn) (alpha_ts_nobn, qalpha_ts_bn) bn_nos; |
510 val fv_alpha_all = combine_fv_alpha_bns (qfv_ts_nobn, qfv_ts_bn) (alpha_ts_nobn, qalpha_ts_bn) bn_nos; |
510 val (names, supp_eq_t) = supp_eq fv_alpha_all; |
511 val (names, supp_eq_t) = supp_eq fv_alpha_all; |
511 val _ = warning "Support Equations"; |
512 val _ = warning "Support Equations"; |
|
513 val q_eq_iff_simp = map (fn x => @{thm simp_thms(6)} OF [x] handle THM _ => x) q_eq_iff; |
512 (*supp_eq_tac q_induct q_fv q_perm q_eq_iff lthy22 1*) |
514 (*supp_eq_tac q_induct q_fv q_perm q_eq_iff lthy22 1*) |
513 val q_supp = HOLogic.conj_elims (Goal.prove lthy22 names [] supp_eq_t (fn _ => Skip_Proof.cheat_tac thy)) handle _ => []; |
515 val q_supp = HOLogic.conj_elims (Goal.prove lthy22 names [] supp_eq_t (fn _ => Skip_Proof.cheat_tac thy)) handle _ => []; |
514 val lthy23 = note_suffix "supp" q_supp lthy22; |
516 val lthy23 = note_suffix "supp" q_supp lthy22; |
515 in |
517 in |
516 (0, lthy23) |
518 (0, lthy23) |