269 ML {* val cheat_fv_rsp = Unsynchronized.ref true *} |
269 ML {* val cheat_fv_rsp = Unsynchronized.ref true *} |
270 ML {* val cheat_const_rsp = Unsynchronized.ref true *} (* For alpha_bn 0 and alpha_bn_rsp *) |
270 ML {* val cheat_const_rsp = Unsynchronized.ref true *} (* For alpha_bn 0 and alpha_bn_rsp *) |
271 |
271 |
272 ML {* val cheat_equivp = Unsynchronized.ref true *} |
272 ML {* val cheat_equivp = Unsynchronized.ref true *} |
273 |
273 |
274 (* Fixes for these 2 are known *) |
274 (* These 2 are not needed any more *) |
275 ML {* val cheat_fv_eqvt = Unsynchronized.ref true *} (* The tactic works, building the goal needs fixing *) |
275 ML {* val cheat_fv_eqvt = Unsynchronized.ref false *} |
276 ML {* val cheat_alpha_eqvt = Unsynchronized.ref true *} (* The tactic works, building the goal needs fixing *) |
276 ML {* val cheat_alpha_eqvt = Unsynchronized.ref false *} |
277 |
277 |
278 |
278 |
279 ML {* |
279 ML {* |
280 fun nominal_datatype2 dts bn_funs bn_eqs binds lthy = |
280 fun nominal_datatype2 dts bn_funs bn_eqs binds lthy = |
281 let |
281 let |
406 val lthy19 = note_simp_suffix "distinct" q_dis lthy18; |
406 val lthy19 = note_simp_suffix "distinct" q_dis lthy18; |
407 val q_eqvt = map (lift_thm lthy19) raw_fv_bv_eqvt; |
407 val q_eqvt = map (lift_thm lthy19) raw_fv_bv_eqvt; |
408 val (_, lthy20) = Local_Theory.note ((Binding.empty, |
408 val (_, lthy20) = Local_Theory.note ((Binding.empty, |
409 [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), q_eqvt) lthy19; |
409 [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), q_eqvt) lthy19; |
410 val _ = tracing "Finite Support"; |
410 val _ = tracing "Finite Support"; |
411 val supports = map (prove_supports lthy20 q_perm) consts handle _ => [] |
411 val supports = map (prove_supports lthy20 q_perm) consts; |
412 val fin_supp = HOLogic.conj_elims (prove_fs lthy20 q_induct supports q_tys) handle _ => [] |
412 val fin_supp = HOLogic.conj_elims (prove_fs lthy20 q_induct supports q_tys); |
413 val thy3 = Local_Theory.exit_global lthy20; |
413 val thy3 = Local_Theory.exit_global lthy20; |
414 val lthy21 = Theory_Target.instantiation (qty_full_names, [], @{sort fs}) thy3; |
414 val lthy21 = Theory_Target.instantiation (qty_full_names, [], @{sort fs}) thy3; |
415 fun tac _ = Class.intro_classes_tac [] THEN (ALLGOALS (resolve_tac fin_supp)) |
415 fun tac _ = Class.intro_classes_tac [] THEN (ALLGOALS (resolve_tac fin_supp)) |
416 val lthy22 = Class.prove_instantiation_instance tac lthy21 handle _ => lthy20 |
416 val lthy22 = Class.prove_instantiation_instance tac lthy21 handle _ => lthy20 |
417 in |
417 in |