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 |
281 |
|
282 ML {* val cheat_equivp = ref true *} |
|
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 |
286 |
288 |
315 val (((fv_ts_loc, fv_def_loc), alpha), lthy4) = define_fv_alpha dtinfo raw_binds_flat bn_funs_decls lthy3; |
317 val (((fv_ts_loc, fv_def_loc), alpha), lthy4) = define_fv_alpha dtinfo raw_binds_flat bn_funs_decls lthy3; |
316 val alpha_ts_loc = #preds alpha |
318 val alpha_ts_loc = #preds alpha |
317 val alpha_ts_loc_nobn = List.take (alpha_ts_loc, length perms) |
319 val alpha_ts_loc_nobn = List.take (alpha_ts_loc, length perms) |
318 val morphism_4_3 = ProofContext.export_morphism lthy4 lthy3; |
320 val morphism_4_3 = ProofContext.export_morphism lthy4 lthy3; |
319 val fv_ts = map (Morphism.term morphism_4_3) fv_ts_loc; |
321 val fv_ts = map (Morphism.term morphism_4_3) fv_ts_loc; |
320 val fv_ts_loc_nobn = List.take (fv_ts_loc, length perms) |
322 val (fv_ts_loc_nobn, fv_ts_loc_bn) = chop (length perms) fv_ts_loc; |
321 val fv_ts_nobn = List.take (fv_ts, length perms) |
323 val (fv_ts_nobn, fv_ts_bn) = chop (length perms) fv_ts; |
322 val alpha_ts = map (Morphism.term morphism_4_3) alpha_ts_loc; |
324 val alpha_ts = map (Morphism.term morphism_4_3) alpha_ts_loc; |
323 val (alpha_ts_nobn, alpha_ts_bn) = chop (length perms) alpha_ts |
325 val (alpha_ts_nobn, alpha_ts_bn) = chop (length perms) alpha_ts |
324 val alpha_induct_loc = #induct alpha |
326 val alpha_induct_loc = #induct alpha |
325 val [alpha_induct] = ProofContext.export lthy4 lthy3 [alpha_induct_loc]; |
327 val [alpha_induct] = ProofContext.export lthy4 lthy3 [alpha_induct_loc]; |
326 val alpha_inducts = Project_Rule.projects lthy4 (1 upto (length dts)) alpha_induct |
328 val alpha_inducts = Project_Rule.projects lthy4 (1 upto (length dts)) alpha_induct |
335 val alpha_inj_loc = build_alpha_inj alpha_intros (inject @ distincts) alpha_cases_loc lthy4 |
337 val alpha_inj_loc = build_alpha_inj alpha_intros (inject @ distincts) alpha_cases_loc lthy4 |
336 val alpha_inj = ProofContext.export lthy4 lthy3 alpha_inj_loc |
338 val alpha_inj = ProofContext.export lthy4 lthy3 alpha_inj_loc |
337 fun alpha_eqvt_tac' _ = |
339 fun alpha_eqvt_tac' _ = |
338 if !cheat_alpha_eqvt then Skip_Proof.cheat_tac thy |
340 if !cheat_alpha_eqvt then Skip_Proof.cheat_tac thy |
339 else alpha_eqvt_tac alpha_induct_loc (raw_perm_def @ alpha_inj_loc) lthy4 1 |
341 else alpha_eqvt_tac alpha_induct_loc (raw_perm_def @ alpha_inj_loc) lthy4 1 |
340 val alpha_eqvt_loc = build_alpha_eqvts alpha_ts_loc_nobn perms alpha_eqvt_tac' lthy4; |
342 val alpha_eqvt_loc = build_alpha_eqvts alpha_ts_loc alpha_eqvt_tac' lthy4; |
341 val alpha_eqvt = ProofContext.export lthy4 lthy2 alpha_eqvt_loc; |
343 val alpha_eqvt = ProofContext.export lthy4 lthy2 alpha_eqvt_loc; |
|
344 val _ = map tracing (map PolyML.makestring alpha_eqvt) |
342 val (bv_eqvts, lthy5) = fold_map (build_bv_eqvt (raw_bn_eqs @ raw_perm_def) inducts) bns lthy4; |
345 val (bv_eqvts, lthy5) = fold_map (build_bv_eqvt (raw_bn_eqs @ raw_perm_def) inducts) bns lthy4; |
343 val fv_eqvt_tac = |
346 val fv_eqvt_tac = |
344 if !cheat_fv_eqvt then (fn _ => fn _ => Skip_Proof.cheat_tac thy) |
347 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 |
348 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; |
349 val (fv_eqvts, lthy6) = build_eqvts Binding.empty fv_ts_loc_nobn fv_eqvt_tac lthy5; |
|
350 val (fv_bn_eqvts, lthy6a) = fold_map (build_bv_eqvt ((flat (map snd bv_eqvts)) @ fv_def_loc @ raw_perm_def) inducts) (fv_ts_loc_bn ~~ (map snd bns)) lthy6; |
|
351 val lthy6 = lthy6a; |
347 val raw_fv_bv_eqvt_loc = flat (map snd bv_eqvts) @ (snd fv_eqvts) |
352 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; |
353 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 |
354 val alpha_equivp_loc = |
350 (* val alpha_equivp_loc = build_equivps alpha_ts_loc induct alpha_induct_loc |
355 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;*) |
356 else build_equivps alpha_ts_loc induct alpha_induct_loc |
|
357 inject alpha_inj_loc distincts alpha_cases_loc alpha_eqvt_loc lthy6; |
352 val alpha_equivp = ProofContext.export lthy6 lthy2 alpha_equivp_loc; |
358 val alpha_equivp = ProofContext.export lthy6 lthy2 alpha_equivp_loc; |
353 val qty_binds = map (fn (_, b, _, _) => b) dts; |
359 val qty_binds = map (fn (_, b, _, _) => b) dts; |
354 val qty_names = map Name.of_binding qty_binds; |
360 val qty_names = map Name.of_binding qty_binds; |
355 val qty_full_names = map (Long_Name.qualify thy_name) qty_names |
361 val qty_full_names = map (Long_Name.qualify thy_name) qty_names |
356 val lthy7 = define_quotient_type |
362 val lthy7 = define_quotient_type |
392 val thy' = define_lifted_perms qty_full_names (perm_names ~~ perms) raw_perm_simps thy; |
398 val thy' = define_lifted_perms qty_full_names (perm_names ~~ perms) raw_perm_simps thy; |
393 val lthy13 = Theory_Target.init NONE thy'; |
399 val lthy13 = Theory_Target.init NONE thy'; |
394 val q_name = space_implode "_" qty_names; |
400 val q_name = space_implode "_" qty_names; |
395 val q_induct = lift_thm lthy13 induct; |
401 val q_induct = lift_thm lthy13 induct; |
396 val (_, lthy14) = Local_Theory.note ((Binding.name (q_name ^ "_induct"), []), [q_induct]) lthy13; |
402 val (_, lthy14) = Local_Theory.note ((Binding.name (q_name ^ "_induct"), []), [q_induct]) lthy13; |
|
403 val q_inducts = Project_Rule.projects lthy13 (1 upto (length alpha_inducts)) q_induct |
|
404 val (_, lthy14a) = Local_Theory.note ((Binding.name (q_name ^ "_inducts"), []), q_inducts) lthy14; |
397 val q_perm = map (lift_thm lthy14) raw_perm_def; |
405 val q_perm = map (lift_thm lthy14) raw_perm_def; |
398 val (_, lthy15) = Local_Theory.note ((Binding.name (q_name ^ "_perm"), []), q_perm) lthy14; |
406 val (_, lthy15) = Local_Theory.note ((Binding.name (q_name ^ "_perm"), []), q_perm) lthy14a; |
399 val q_fv = map (lift_thm lthy15) fv_def; |
407 val q_fv = map (lift_thm lthy15) fv_def; |
400 val (_, lthy16) = Local_Theory.note ((Binding.name (q_name ^ "_fv"), []), q_fv) lthy15; |
408 val (_, lthy16) = Local_Theory.note ((Binding.name (q_name ^ "_fv"), []), q_fv) lthy15; |
401 val q_bn = map (lift_thm lthy16) raw_bn_eqs; |
409 val q_bn = map (lift_thm lthy16) raw_bn_eqs; |
402 val (_, lthy17) = Local_Theory.note ((Binding.name (q_name ^ "_bn"), []), q_bn) lthy16; |
410 val (_, lthy17) = Local_Theory.note ((Binding.name (q_name ^ "_bn"), []), q_bn) lthy16; |
403 val inj_unfolded = map (Local_Defs.unfold lthy17 @{thms alpha_gen}) alpha_inj |
411 val inj_unfolded = map (Local_Defs.unfold lthy17 @{thms alpha_gen}) alpha_inj |