276 *} |
276 *} |
277 |
277 |
278 (* These 2 are critical, we don't know how to do it in term5 *) |
278 (* These 2 are critical, we don't know how to do it in term5 *) |
279 ML {* val cheat_fv_rsp = ref true *} |
279 ML {* val cheat_fv_rsp = ref true *} |
280 ML {* val cheat_const_rsp = ref true *} (* For alpha_bn 0 and alpha_bn_rsp *) |
280 ML {* val cheat_const_rsp = ref true *} (* For alpha_bn 0 and alpha_bn_rsp *) |
|
281 |
|
282 ML {* val cheat_equivp = ref true *} |
281 |
283 |
282 (* Fixes for these 2 are known *) |
284 (* Fixes for these 2 are known *) |
283 ML {* val cheat_fv_eqvt = ref true *} (* The tactic works, building the goal needs fixing *) |
285 ML {* val cheat_fv_eqvt = ref true *} (* The tactic works, building the goal needs fixing *) |
284 ML {* val cheat_alpha_eqvt = ref true *} (* The tactic works, building the goal needs fixing *) |
286 ML {* val cheat_alpha_eqvt = ref true *} (* The tactic works, building the goal needs fixing *) |
285 |
287 |
344 if !cheat_fv_eqvt then (fn _ => fn _ => Skip_Proof.cheat_tac thy) |
346 if !cheat_fv_eqvt then (fn _ => fn _ => Skip_Proof.cheat_tac thy) |
345 else build_eqvts_tac induct ((flat (map snd bv_eqvts)) @ fv_def_loc @ raw_perm_def) lthy5 |
347 else build_eqvts_tac induct ((flat (map snd bv_eqvts)) @ fv_def_loc @ raw_perm_def) lthy5 |
346 val (fv_eqvts, lthy6) = build_eqvts Binding.empty fv_ts_loc fv_eqvt_tac lthy5; |
348 val (fv_eqvts, lthy6) = build_eqvts Binding.empty fv_ts_loc fv_eqvt_tac lthy5; |
347 val raw_fv_bv_eqvt_loc = flat (map snd bv_eqvts) @ (snd fv_eqvts) |
349 val raw_fv_bv_eqvt_loc = flat (map snd bv_eqvts) @ (snd fv_eqvts) |
348 val raw_fv_bv_eqvt = ProofContext.export lthy6 lthy3 raw_fv_bv_eqvt_loc; |
350 val raw_fv_bv_eqvt = ProofContext.export lthy6 lthy3 raw_fv_bv_eqvt_loc; |
349 val alpha_equivp_loc = map (equivp_hack lthy6) alpha_ts_loc_nobn |
351 val alpha_equivp_loc = |
350 (* val alpha_equivp_loc = build_equivps alpha_ts_loc induct alpha_induct_loc |
352 if !cheat_equivp then map (equivp_hack lthy6) alpha_ts_loc_nobn |
351 inject alpha_inj_loc distinct alpha_cases_loc alpha_eqvt_loc lthy6;*) |
353 else build_equivps alpha_ts_loc induct alpha_induct_loc |
|
354 inject alpha_inj_loc distincts alpha_cases_loc alpha_eqvt_loc lthy6; |
352 val alpha_equivp = ProofContext.export lthy6 lthy2 alpha_equivp_loc; |
355 val alpha_equivp = ProofContext.export lthy6 lthy2 alpha_equivp_loc; |
353 val qty_binds = map (fn (_, b, _, _) => b) dts; |
356 val qty_binds = map (fn (_, b, _, _) => b) dts; |
354 val qty_names = map Name.of_binding qty_binds; |
357 val qty_names = map Name.of_binding qty_binds; |
355 val qty_full_names = map (Long_Name.qualify thy_name) qty_names |
358 val qty_full_names = map (Long_Name.qualify thy_name) qty_names |
356 val lthy7 = define_quotient_type |
359 val lthy7 = define_quotient_type |