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 (* This one is not needed for the proper examples *) |
|
290 ML {* val cheat_equivp = Unsynchronized.ref false *} |
289 ML {* val cheat_equivp = Unsynchronized.ref false *} |
291 |
290 ML {* val cheat_bn_eqvt = Unsynchronized.ref false *} |
292 (* These 4 are not needed any more *) |
|
293 ML {* val cheat_fv_rsp = Unsynchronized.ref false *} |
|
294 ML {* val cheat_fv_eqvt = Unsynchronized.ref false *} |
291 ML {* val cheat_fv_eqvt = Unsynchronized.ref false *} |
295 ML {* val cheat_alpha_eqvt = Unsynchronized.ref false *} |
292 ML {* val cheat_alpha_eqvt = Unsynchronized.ref false *} |
|
293 ML {* val cheat_bn_rsp = Unsynchronized.ref false *} |
|
294 ML {* val cheat_fv_rsp = Unsynchronized.ref false *} |
|
295 ML {* val cheat_const_rsp = Unsynchronized.ref false *} |
296 ML {* val cheat_alpha_bn_rsp = Unsynchronized.ref false *} |
296 ML {* val cheat_alpha_bn_rsp = Unsynchronized.ref false *} |
297 |
297 |
298 ML {* fun map_option _ NONE = NONE |
298 ML {* fun map_option _ NONE = NONE |
299 | map_option f (SOME x) = SOME (f x) *} |
299 | map_option f (SOME x) = SOME (f x) *} |
300 |
300 |
343 (rel_distinct ~~ alpha_ts_nobn)); |
343 (rel_distinct ~~ alpha_ts_nobn)); |
344 val rel_dists_bn = flat (map (distinct_rel lthy4 alpha_cases) |
344 val rel_dists_bn = flat (map (distinct_rel lthy4 alpha_cases) |
345 ((map (fn i => nth rel_distinct i) bn_nos) ~~ alpha_ts_bn)) |
345 ((map (fn i => nth rel_distinct i) bn_nos) ~~ alpha_ts_bn)) |
346 val alpha_eq_iff = build_alpha_inj alpha_intros (inject @ distincts) alpha_cases lthy4 |
346 val alpha_eq_iff = build_alpha_inj alpha_intros (inject @ distincts) alpha_cases lthy4 |
347 val _ = tracing "Proving equivariance"; |
347 val _ = tracing "Proving equivariance"; |
|
348 fun build_bv_eqvt simps inducts (t, n) ctxt = |
|
349 build_eqvts Binding.empty [t] |
|
350 (if !cheat_bn_eqvt then (fn _ => fn _ => Skip_Proof.cheat_tac thy) |
|
351 else build_eqvts_tac (nth inducts n) simps ctxt |
|
352 ) ctxt |
348 val (bv_eqvts, lthy5) = fold_map (build_bv_eqvt (raw_bn_eqs @ raw_perm_def) inducts) bns lthy4; |
353 val (bv_eqvts, lthy5) = fold_map (build_bv_eqvt (raw_bn_eqs @ raw_perm_def) inducts) bns lthy4; |
349 val fv_eqvt_tac = |
354 val fv_eqvt_tac = |
350 if !cheat_fv_eqvt then (fn _ => fn _ => Skip_Proof.cheat_tac thy) |
355 if !cheat_fv_eqvt then (fn _ => fn _ => Skip_Proof.cheat_tac thy) |
351 else build_eqvts_tac induct ((flat (map snd bv_eqvts)) @ fv_def @ raw_perm_def) lthy5 |
356 else build_eqvts_tac induct ((flat (map snd bv_eqvts)) @ fv_def @ raw_perm_def) lthy5 |
352 val (fv_eqvts, lthy6) = build_eqvts Binding.empty fv_ts_nobn fv_eqvt_tac lthy5; |
357 val (fv_eqvts, lthy6) = build_eqvts Binding.empty fv_ts_nobn fv_eqvt_tac lthy5; |
382 val (consts, const_defs, lthy8) = quotient_lift_consts_export (const_names ~~ raw_consts) lthy7; |
387 val (consts, const_defs, lthy8) = quotient_lift_consts_export (const_names ~~ raw_consts) lthy7; |
383 (* Could be done nicer *) |
388 (* Could be done nicer *) |
384 val q_tys = distinct (op =) (map (snd o strip_type o fastype_of) consts); |
389 val q_tys = distinct (op =) (map (snd o strip_type o fastype_of) consts); |
385 val _ = tracing "Proving respects"; |
390 val _ = tracing "Proving respects"; |
386 val (bns_rsp_pre, lthy9) = fold_map ( |
391 val (bns_rsp_pre, lthy9) = fold_map ( |
387 fn (bn_t, i) => prove_const_rsp Binding.empty [bn_t] |
392 fn (bn_t, i) => prove_const_rsp Binding.empty [bn_t] (fn _ => |
388 (fn _ => fvbv_rsp_tac (nth alpha_inducts i) raw_bn_eqs lthy8 1)) bns lthy8; |
393 if !cheat_bn_rsp then (Skip_Proof.cheat_tac thy) else |
|
394 fvbv_rsp_tac (nth alpha_inducts i) raw_bn_eqs lthy8 1)) bns lthy8; |
389 val bns_rsp = flat (map snd bns_rsp_pre); |
395 val bns_rsp = flat (map snd bns_rsp_pre); |
390 fun fv_rsp_tac _ = if !cheat_fv_rsp then Skip_Proof.cheat_tac thy |
396 fun fv_rsp_tac _ = if !cheat_fv_rsp then Skip_Proof.cheat_tac thy |
391 else fvbv_rsp_tac alpha_induct fv_def lthy8 1; |
397 else fvbv_rsp_tac alpha_induct fv_def lthy8 1; |
392 val fv_rsps = prove_fv_rsp fv_alpha_all alpha_ts fv_rsp_tac lthy9; |
398 val fv_rsps = prove_fv_rsp fv_alpha_all alpha_ts fv_rsp_tac lthy9; |
393 val (fv_rsp_pre, lthy10) = fold_map |
399 val (fv_rsp_pre, lthy10) = fold_map |
394 (fn fv => fn ctxt => prove_const_rsp Binding.empty [fv] |
400 (fn fv => fn ctxt => prove_const_rsp Binding.empty [fv] |
395 (fn _ => asm_simp_tac (HOL_ss addsimps fv_rsps) 1) ctxt) fv_ts lthy9; |
401 (fn _ => asm_simp_tac (HOL_ss addsimps fv_rsps) 1) ctxt) fv_ts lthy9; |
396 val fv_rsp = flat (map snd fv_rsp_pre); |
402 val fv_rsp = flat (map snd fv_rsp_pre); |
397 val (perms_rsp, lthy11) = prove_const_rsp Binding.empty perms |
403 val (perms_rsp, lthy11) = prove_const_rsp Binding.empty perms |
398 (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy10; |
404 (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy10; |
399 val alpha_alphabn = build_alpha_alphabn fv_alpha_all alpha_inducts alpha_eq_iff lthy11; |
405 fun const_rsp_tac _ = |
400 fun const_rsp_tac _ = constr_rsp_tac alpha_eq_iff (fv_rsp @ bns_rsp @ reflps @ alpha_alphabn) 1 |
406 if !cheat_const_rsp then Skip_Proof.cheat_tac thy |
|
407 else let val alpha_alphabn = build_alpha_alphabn fv_alpha_all alpha_inducts alpha_eq_iff lthy11 |
|
408 in constr_rsp_tac alpha_eq_iff (fv_rsp @ bns_rsp @ reflps @ alpha_alphabn) 1 end |
401 val (const_rsps, lthy11a) = fold_map (fn cnst => prove_const_rsp Binding.empty [cnst] |
409 val (const_rsps, lthy11a) = fold_map (fn cnst => prove_const_rsp Binding.empty [cnst] |
402 const_rsp_tac) raw_consts lthy11 |
410 const_rsp_tac) raw_consts lthy11 |
403 val alpha_bn_rsp_pre = flat (map (prove_alpha_bn_rsp alpha_ts_nobn alpha_inducts exhausts (alpha_eq_iff @ rel_dists @ rel_dists_bn) (alpha_equivp) lthy11a) (alpha_ts_bn ~~ bn_nos)) |
|
404 val (alpha_bn_rsps, lthy12) = fold_map (fn cnst => prove_const_rsp Binding.empty [cnst] |
411 val (alpha_bn_rsps, lthy12) = fold_map (fn cnst => prove_const_rsp Binding.empty [cnst] |
405 (fn _ => asm_simp_tac (HOL_ss addsimps alpha_bn_rsp_pre) 1)) alpha_ts_bn lthy11a |
412 (fn _ => |
|
413 if !cheat_alpha_bn_rsp then Skip_Proof.cheat_tac thy |
|
414 else |
|
415 let val alpha_bn_rsp_pre = flat (map (prove_alpha_bn_rsp alpha_ts_nobn alpha_inducts exhausts |
|
416 (alpha_eq_iff @ rel_dists @ rel_dists_bn) (alpha_equivp) lthy11a) (alpha_ts_bn ~~ bn_nos)) in |
|
417 asm_simp_tac (HOL_ss addsimps alpha_bn_rsp_pre) 1 end)) alpha_ts_bn lthy11a |
406 val qfv_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) ordered_fv_ts |
418 val qfv_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) ordered_fv_ts |
407 val (qfv_ts, qfv_defs, lthy12a) = quotient_lift_consts_export (qfv_names ~~ ordered_fv_ts) lthy12; |
419 val (qfv_ts, qfv_defs, lthy12a) = quotient_lift_consts_export (qfv_names ~~ ordered_fv_ts) lthy12; |
408 val (qfv_ts_nobn, qfv_ts_bn) = chop (length perms) qfv_ts; |
420 val (qfv_ts_nobn, qfv_ts_bn) = chop (length perms) qfv_ts; |
409 val qbn_names = map (fn (b, _ , _) => Name.of_binding b) bn_funs |
421 val qbn_names = map (fn (b, _ , _) => Name.of_binding b) bn_funs |
410 val (qbn_defs, lthy12b) = fold_map Quotient_Def.quotient_lift_const (qbn_names ~~ raw_bn_funs) lthy12a; |
422 val (qbn_defs, lthy12b) = fold_map Quotient_Def.quotient_lift_const (qbn_names ~~ raw_bn_funs) lthy12a; |