284 in |
284 in |
285 Drule.instantiate' [SOME cty] [SOME ct] @{thm equivp_hack} |
285 Drule.instantiate' [SOME cty] [SOME ct] @{thm equivp_hack} |
286 end |
286 end |
287 *} |
287 *} |
288 |
288 |
|
289 ML {* val cheat_alpha_eqvt = Unsynchronized.ref false *} |
289 ML {* val cheat_equivp = Unsynchronized.ref false *} |
290 ML {* val cheat_equivp = Unsynchronized.ref false *} |
290 ML {* val cheat_alpha_eqvt = Unsynchronized.ref false *} |
|
291 ML {* val cheat_bn_rsp = Unsynchronized.ref false *} |
|
292 ML {* val cheat_fv_rsp = Unsynchronized.ref false *} |
291 ML {* val cheat_fv_rsp = Unsynchronized.ref false *} |
293 ML {* val cheat_const_rsp = Unsynchronized.ref false *} |
292 ML {* val cheat_const_rsp = Unsynchronized.ref false *} |
294 ML {* val cheat_alpha_bn_rsp = Unsynchronized.ref false *} |
|
295 |
293 |
296 ML {* fun map_option _ NONE = NONE |
294 ML {* fun map_option _ NONE = NONE |
297 | map_option f (SOME x) = SOME (f x) *} |
295 | map_option f (SOME x) = SOME (f x) *} |
298 |
296 |
299 ML {* |
297 ML {* |
340 val bns = raw_bn_funs ~~ bn_nos; |
338 val bns = raw_bn_funs ~~ bn_nos; |
341 val rel_dists = flat (map (distinct_rel lthy4 alpha_cases) |
339 val rel_dists = flat (map (distinct_rel lthy4 alpha_cases) |
342 (rel_distinct ~~ alpha_ts_nobn)); |
340 (rel_distinct ~~ alpha_ts_nobn)); |
343 val rel_dists_bn = flat (map (distinct_rel lthy4 alpha_cases) |
341 val rel_dists_bn = flat (map (distinct_rel lthy4 alpha_cases) |
344 ((map (fn i => nth rel_distinct i) bn_nos) ~~ alpha_ts_bn)) |
342 ((map (fn i => nth rel_distinct i) bn_nos) ~~ alpha_ts_bn)) |
345 val alpha_eq_iff = build_alpha_inj alpha_intros (inject @ distincts) alpha_cases lthy4 |
343 val alpha_eq_iff = build_rel_inj alpha_intros (inject @ distincts) alpha_cases lthy4 |
346 val _ = tracing "Proving equivariance"; |
344 val _ = tracing "Proving equivariance"; |
347 val (bv_eqvt, lthy5) = prove_eqvt raw_tys induct (raw_bn_eqs @ raw_perm_def) (map fst bns) lthy4 |
345 val (bv_eqvt, lthy5) = prove_eqvt raw_tys induct (raw_bn_eqs @ raw_perm_def) (map fst bns) lthy4 |
348 val (fv_eqvt, lthy6) = prove_eqvt raw_tys induct (fv_def @ raw_perm_def) (fv_ts_nobn @ fv_ts_bn) lthy5 |
346 val (fv_eqvt, lthy6) = prove_eqvt raw_tys induct (fv_def @ raw_perm_def) (fv_ts_nobn @ fv_ts_bn) lthy5 |
349 fun alpha_eqvt_tac' _ = |
347 fun alpha_eqvt_tac' _ = |
350 if !cheat_alpha_eqvt then Skip_Proof.cheat_tac thy |
348 if !cheat_alpha_eqvt then Skip_Proof.cheat_tac thy |
392 if !cheat_const_rsp then Skip_Proof.cheat_tac thy |
390 if !cheat_const_rsp then Skip_Proof.cheat_tac thy |
393 else let val alpha_alphabn = build_alpha_alphabn fv_alpha_all alpha_inducts alpha_eq_iff lthy11 |
391 else let val alpha_alphabn = build_alpha_alphabn fv_alpha_all alpha_inducts alpha_eq_iff lthy11 |
394 in constr_rsp_tac alpha_eq_iff (fv_rsp @ bns_rsp @ reflps @ alpha_alphabn) 1 end |
392 in constr_rsp_tac alpha_eq_iff (fv_rsp @ bns_rsp @ reflps @ alpha_alphabn) 1 end |
395 val (const_rsps, lthy11a) = fold_map (fn cnst => prove_const_rsp Binding.empty [cnst] |
393 val (const_rsps, lthy11a) = fold_map (fn cnst => prove_const_rsp Binding.empty [cnst] |
396 const_rsp_tac) raw_consts lthy11 |
394 const_rsp_tac) raw_consts lthy11 |
|
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; |
397 val (alpha_bn_rsps, lthy12) = fold_map (fn cnst => prove_const_rsp Binding.empty [cnst] |
396 val (alpha_bn_rsps, lthy12) = fold_map (fn cnst => prove_const_rsp Binding.empty [cnst] |
398 (fn _ => |
397 (fn _ => asm_simp_tac (HOL_ss addsimps alpha_bn_rsp_pre) 1)) alpha_ts_bn lthy11a |
399 if !cheat_alpha_bn_rsp then Skip_Proof.cheat_tac thy |
|
400 else |
|
401 let val alpha_bn_rsp_pre = flat (map (prove_alpha_bn_rsp alpha_ts_nobn alpha_inducts exhausts |
|
402 (alpha_eq_iff @ rel_dists @ rel_dists_bn) (alpha_equivp) lthy11a) (alpha_ts_bn ~~ bn_nos)) in |
|
403 asm_simp_tac (HOL_ss addsimps alpha_bn_rsp_pre) 1 end)) alpha_ts_bn lthy11a |
|
404 val qfv_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) ordered_fv_ts |
398 val qfv_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) ordered_fv_ts |
405 val (qfv_ts, qfv_defs, lthy12a) = quotient_lift_consts_export (qfv_names ~~ ordered_fv_ts) lthy12; |
399 val (qfv_ts, qfv_defs, lthy12a) = quotient_lift_consts_export (qfv_names ~~ ordered_fv_ts) lthy12; |
406 val (qfv_ts_nobn, qfv_ts_bn) = chop (length perms) qfv_ts; |
400 val (qfv_ts_nobn, qfv_ts_bn) = chop (length perms) qfv_ts; |
407 val qbn_names = map (fn (b, _ , _) => Name.of_binding b) bn_funs |
401 val qbn_names = map (fn (b, _ , _) => Name.of_binding b) bn_funs |
408 val (qbn_defs, lthy12b) = fold_map Quotient_Def.quotient_lift_const (qbn_names ~~ raw_bn_funs) lthy12a; |
402 val (qbn_defs, lthy12b) = fold_map Quotient_Def.quotient_lift_const (qbn_names ~~ raw_bn_funs) lthy12a; |