265 end |
265 end |
266 *} |
266 *} |
267 |
267 |
268 (* These 2 are critical, we don't know how to do it in term5 *) |
268 (* These 2 are critical, we don't know how to do it in term5 *) |
269 ML {* val cheat_fv_rsp = Unsynchronized.ref true *} |
269 ML {* val cheat_fv_rsp = Unsynchronized.ref true *} |
270 ML {* val cheat_const_rsp = Unsynchronized.ref true *} (* For alpha_bn 0 and alpha_bn_rsp *) |
270 ML {* val cheat_alpha_bn_rsp = Unsynchronized.ref true *} |
271 |
271 |
272 ML {* val cheat_equivp = Unsynchronized.ref true *} |
272 ML {* val cheat_equivp = Unsynchronized.ref true *} |
273 |
273 |
274 (* These 2 are not needed any more *) |
274 (* These 2 are not needed any more *) |
275 ML {* val cheat_fv_eqvt = Unsynchronized.ref false *} |
275 ML {* val cheat_fv_eqvt = Unsynchronized.ref false *} |
361 fun fv_rsp_tac _ = if !cheat_fv_rsp then Skip_Proof.cheat_tac thy |
361 fun fv_rsp_tac _ = if !cheat_fv_rsp then Skip_Proof.cheat_tac thy |
362 else fvbv_rsp_tac alpha_induct fv_def 1; |
362 else fvbv_rsp_tac alpha_induct fv_def 1; |
363 val ((_, fv_rsp), lthy10) = prove_const_rsp Binding.empty fv_ts fv_rsp_tac lthy9 |
363 val ((_, fv_rsp), lthy10) = prove_const_rsp Binding.empty fv_ts fv_rsp_tac lthy9 |
364 val (perms_rsp, lthy11) = prove_const_rsp Binding.empty perms |
364 val (perms_rsp, lthy11) = prove_const_rsp Binding.empty perms |
365 (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy10; |
365 (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy10; |
366 fun const_rsp_tac _ = if !cheat_const_rsp then Skip_Proof.cheat_tac thy |
366 val alpha_alphabn = build_alpha_alphabn fv_alpha_all alpha_inducts alpha_eq_iff lthy11; |
367 else constr_rsp_tac alpha_eq_iff (fv_rsp @ bns_rsp) alpha_equivp 1 |
367 fun const_rsp_tac _ = constr_rsp_tac alpha_eq_iff (fv_rsp @ bns_rsp @ reflps @ alpha_alphabn) 1 |
368 val (const_rsps, lthy12) = fold_map (fn cnst => prove_const_rsp Binding.empty [cnst] |
368 fun alpha_bn_rsp_tac x = if !cheat_alpha_bn_rsp then Skip_Proof.cheat_tac thy else const_rsp_tac x |
369 const_rsp_tac) (raw_consts @ alpha_ts_bn) lthy11 |
369 val (const_rsps, lthy11a) = fold_map (fn cnst => prove_const_rsp Binding.empty [cnst] |
|
370 const_rsp_tac) raw_consts lthy11 |
|
371 val (alpha_bn_rsps, lthy12) = fold_map (fn cnst => prove_const_rsp Binding.empty [cnst] |
|
372 alpha_bn_rsp_tac) alpha_ts_bn lthy11a |
370 val qfv_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) ordered_fv_ts |
373 val qfv_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) ordered_fv_ts |
371 val (qfv_ts, qfv_defs, lthy12a) = quotient_lift_consts_export (qfv_names ~~ ordered_fv_ts) lthy12; |
374 val (qfv_ts, qfv_defs, lthy12a) = quotient_lift_consts_export (qfv_names ~~ ordered_fv_ts) lthy12; |
372 val (qfv_ts_nobn, qfv_ts_bn) = chop (length perms) qfv_ts; |
375 val (qfv_ts_nobn, qfv_ts_bn) = chop (length perms) qfv_ts; |
373 val qbn_names = map (fn (b, _ , _) => Name.of_binding b) bn_funs |
376 val qbn_names = map (fn (b, _ , _) => Name.of_binding b) bn_funs |
374 val (qbn_defs, lthy12b) = fold_map Quotient_Def.quotient_lift_const (qbn_names ~~ raw_bn_funs) lthy12a; |
377 val (qbn_defs, lthy12b) = fold_map Quotient_Def.quotient_lift_const (qbn_names ~~ raw_bn_funs) lthy12a; |