384 (fn fv => fn ctxt => prove_const_rsp Binding.empty [fv] |
384 (fn fv => fn ctxt => prove_const_rsp Binding.empty [fv] |
385 (fn _ => asm_simp_tac (HOL_ss addsimps fv_rsps) 1) ctxt) fv_ts lthy9; |
385 (fn _ => asm_simp_tac (HOL_ss addsimps fv_rsps) 1) ctxt) fv_ts lthy9; |
386 val fv_rsp = flat (map snd fv_rsp_pre); |
386 val fv_rsp = flat (map snd fv_rsp_pre); |
387 val (perms_rsp, lthy11) = prove_const_rsp Binding.empty perms |
387 val (perms_rsp, lthy11) = prove_const_rsp Binding.empty perms |
388 (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy10; |
388 (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy10; |
|
389 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; |
|
390 val (alpha_bn_rsps, lthy11a) = fold_map (fn cnst => prove_const_rsp Binding.empty [cnst] |
|
391 (fn _ => asm_simp_tac (HOL_ss addsimps alpha_bn_rsp_pre) 1)) alpha_ts_bn lthy11 |
|
392 (* val _ = map tracing (map PolyML.makestring alpha_bn_rsps);*) |
389 fun const_rsp_tac _ = |
393 fun const_rsp_tac _ = |
390 if !cheat_const_rsp then Skip_Proof.cheat_tac thy |
394 if !cheat_const_rsp then Skip_Proof.cheat_tac thy |
391 else let val alpha_alphabn = build_alpha_alphabn fv_alpha_all alpha_inducts alpha_eq_iff lthy11 |
395 else let val alpha_alphabn = prove_alpha_alphabn alpha_ts alpha_induct alpha_eq_iff alpha_ts_bn lthy11a |
392 in constr_rsp_tac alpha_eq_iff (fv_rsp @ bns_rsp @ reflps @ alpha_alphabn) 1 end |
396 in constr_rsp_tac alpha_eq_iff (fv_rsp @ bns_rsp @ reflps @ alpha_alphabn) 1 end |
393 val (const_rsps, lthy11a) = fold_map (fn cnst => prove_const_rsp Binding.empty [cnst] |
397 val (const_rsps, lthy12) = fold_map (fn cnst => prove_const_rsp Binding.empty [cnst] |
394 const_rsp_tac) raw_consts lthy11 |
398 const_rsp_tac) raw_consts lthy11a |
395 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 lthy11a; |
|
396 val (alpha_bn_rsps, lthy12) = fold_map (fn cnst => prove_const_rsp Binding.empty [cnst] |
|
397 (fn _ => asm_simp_tac (HOL_ss addsimps alpha_bn_rsp_pre) 1)) alpha_ts_bn lthy11a |
|
398 val qfv_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) ordered_fv_ts |
399 val qfv_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) ordered_fv_ts |
399 val (qfv_ts, qfv_defs, lthy12a) = quotient_lift_consts_export (qfv_names ~~ ordered_fv_ts) lthy12; |
400 val (qfv_ts, qfv_defs, lthy12a) = quotient_lift_consts_export (qfv_names ~~ ordered_fv_ts) lthy12; |
400 val (qfv_ts_nobn, qfv_ts_bn) = chop (length perms) qfv_ts; |
401 val (qfv_ts_nobn, qfv_ts_bn) = chop (length perms) qfv_ts; |
401 val qbn_names = map (fn (b, _ , _) => Name.of_binding b) bn_funs |
402 val qbn_names = map (fn (b, _ , _) => Name.of_binding b) bn_funs |
402 val (qbn_defs, lthy12b) = fold_map Quotient_Def.quotient_lift_const (qbn_names ~~ raw_bn_funs) lthy12a; |
403 val (qbn_defs, lthy12b) = fold_map Quotient_Def.quotient_lift_const (qbn_names ~~ raw_bn_funs) lthy12a; |