263 in |
263 in |
264 Drule.instantiate' [SOME cty] [SOME ct] @{thm equivp_hack} |
264 Drule.instantiate' [SOME cty] [SOME ct] @{thm equivp_hack} |
265 end |
265 end |
266 *} |
266 *} |
267 |
267 |
268 (* These 2 are critical, we don't know how to do it in term5 *) |
|
269 ML {* val cheat_fv_rsp = Unsynchronized.ref true *} |
|
270 ML {* val cheat_alpha_bn_rsp = Unsynchronized.ref true *} |
268 ML {* val cheat_alpha_bn_rsp = Unsynchronized.ref true *} |
271 |
|
272 ML {* val cheat_equivp = Unsynchronized.ref true *} |
269 ML {* val cheat_equivp = Unsynchronized.ref true *} |
273 |
270 |
274 (* These 2 are not needed any more *) |
271 (* These 3 are not needed any more *) |
|
272 ML {* val cheat_fv_rsp = Unsynchronized.ref false *} |
275 ML {* val cheat_fv_eqvt = Unsynchronized.ref false *} |
273 ML {* val cheat_fv_eqvt = Unsynchronized.ref false *} |
276 ML {* val cheat_alpha_eqvt = Unsynchronized.ref false *} |
274 ML {* val cheat_alpha_eqvt = Unsynchronized.ref false *} |
277 |
275 |
278 |
276 |
279 ML {* |
277 ML {* |
330 fun alpha_eqvt_tac' _ = |
328 fun alpha_eqvt_tac' _ = |
331 if !cheat_alpha_eqvt then Skip_Proof.cheat_tac thy |
329 if !cheat_alpha_eqvt then Skip_Proof.cheat_tac thy |
332 else alpha_eqvt_tac alpha_induct (raw_perm_def @ alpha_eq_iff @ raw_fv_bv_eqvt) lthy6a 1 |
330 else alpha_eqvt_tac alpha_induct (raw_perm_def @ alpha_eq_iff @ raw_fv_bv_eqvt) lthy6a 1 |
333 val alpha_eqvt = build_alpha_eqvts alpha_ts alpha_eqvt_tac' lthy6a; |
331 val alpha_eqvt = build_alpha_eqvts alpha_ts alpha_eqvt_tac' lthy6a; |
334 val _ = tracing "Proving equivalence"; |
332 val _ = tracing "Proving equivalence"; |
335 val fv_alpha_all = combine_fv_alpha_bns (fv_ts_nobn, fv_ts_bn) (alpha_ts_nobn, alpha_ts_bn) bn_nos; |
333 val (rfv_ts_nobn, rfv_ts_bn) = chop (length perms) ordered_fv_ts; |
|
334 val fv_alpha_all = combine_fv_alpha_bns (rfv_ts_nobn, rfv_ts_bn) (alpha_ts_nobn, alpha_ts_bn) bn_nos; |
336 val reflps = build_alpha_refl fv_alpha_all induct alpha_eq_iff lthy6a; |
335 val reflps = build_alpha_refl fv_alpha_all induct alpha_eq_iff lthy6a; |
337 val alpha_equivp = |
336 val alpha_equivp = |
338 if !cheat_equivp then map (equivp_hack lthy6a) alpha_ts_nobn |
337 if !cheat_equivp then map (equivp_hack lthy6a) alpha_ts_nobn |
339 else build_equivps alpha_ts reflps alpha_induct |
338 else build_equivps alpha_ts reflps alpha_induct |
340 inject alpha_eq_iff distincts alpha_cases alpha_eqvt lthy6a; |
339 inject alpha_eq_iff distincts alpha_cases alpha_eqvt lthy6a; |
354 (* Could be done nicer *) |
353 (* Could be done nicer *) |
355 val q_tys = distinct (op =) (map (snd o strip_type o fastype_of) consts); |
354 val q_tys = distinct (op =) (map (snd o strip_type o fastype_of) consts); |
356 val _ = tracing "Proving respects"; |
355 val _ = tracing "Proving respects"; |
357 val (bns_rsp_pre, lthy9) = fold_map ( |
356 val (bns_rsp_pre, lthy9) = fold_map ( |
358 fn (bn_t, i) => prove_const_rsp Binding.empty [bn_t] |
357 fn (bn_t, i) => prove_const_rsp Binding.empty [bn_t] |
359 (fn _ => fvbv_rsp_tac (nth alpha_inducts i) raw_bn_eqs 1)) bns lthy8; |
358 (fn _ => fvbv_rsp_tac (nth alpha_inducts i) raw_bn_eqs lthy8 1)) bns lthy8; |
360 val bns_rsp = flat (map snd bns_rsp_pre); |
359 val bns_rsp = flat (map snd bns_rsp_pre); |
361 fun fv_rsp_tac _ = if !cheat_fv_rsp then Skip_Proof.cheat_tac thy |
360 fun fv_rsp_tac _ = if !cheat_fv_rsp then Skip_Proof.cheat_tac thy |
362 else fvbv_rsp_tac alpha_induct fv_def 1; |
361 else fvbv_rsp_tac alpha_induct fv_def lthy8 1; |
363 val ((_, fv_rsp), lthy10) = prove_const_rsp Binding.empty fv_ts fv_rsp_tac lthy9 |
362 val fv_rsps = prove_fv_rsp fv_alpha_all alpha_ts fv_rsp_tac lthy9; |
|
363 val (fv_rsp_pre, lthy10) = fold_map |
|
364 (fn fv => fn ctxt => prove_const_rsp Binding.empty [fv] |
|
365 (fn _ => asm_simp_tac (HOL_ss addsimps fv_rsps) 1) ctxt) fv_ts lthy9; |
|
366 val fv_rsp = flat (map snd fv_rsp_pre); |
364 val (perms_rsp, lthy11) = prove_const_rsp Binding.empty perms |
367 val (perms_rsp, lthy11) = prove_const_rsp Binding.empty perms |
365 (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy10; |
368 (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy10; |
366 val alpha_alphabn = build_alpha_alphabn fv_alpha_all alpha_inducts alpha_eq_iff lthy11; |
369 val alpha_alphabn = build_alpha_alphabn fv_alpha_all alpha_inducts alpha_eq_iff lthy11; |
367 fun const_rsp_tac _ = constr_rsp_tac alpha_eq_iff (fv_rsp @ bns_rsp @ reflps @ alpha_alphabn) 1 |
370 fun const_rsp_tac _ = constr_rsp_tac alpha_eq_iff (fv_rsp @ bns_rsp @ reflps @ alpha_alphabn) 1 |
368 fun alpha_bn_rsp_tac x = if !cheat_alpha_bn_rsp then Skip_Proof.cheat_tac thy else const_rsp_tac x |
371 fun alpha_bn_rsp_tac x = if !cheat_alpha_bn_rsp then Skip_Proof.cheat_tac thy else const_rsp_tac x |