269 (mk_distinct bvars @ |
269 (mk_distinct bvars @ |
270 maps (fn (t, T) => map (fn (u, U) => HOLogic.mk_Trueprop |
270 maps (fn (t, T) => map (fn (u, U) => HOLogic.mk_Trueprop |
271 (NominalDatatype.fresh_const U T $ u $ t)) bvars) |
271 (NominalDatatype.fresh_const U T $ u $ t)) bvars) |
272 (ts ~~ binder_types (fastype_of p)))) prems; |
272 (ts ~~ binder_types (fastype_of p)))) prems; |
273 |
273 |
274 val perm_pi_simp = PureThy.get_thms thy "perm_pi_simp"; |
274 val perm_pi_simp = Global_Theory.get_thms thy "perm_pi_simp"; |
275 val pt2_atoms = map (fn aT => PureThy.get_thm thy |
275 val pt2_atoms = map (fn aT => Global_Theory.get_thm thy |
276 ("pt_" ^ Long_Name.base_name (fst (dest_Type aT)) ^ "2")) atomTs; |
276 ("pt_" ^ Long_Name.base_name (fst (dest_Type aT)) ^ "2")) atomTs; |
277 val eqvt_ss = Simplifier.global_context thy HOL_basic_ss |
277 val eqvt_ss = Simplifier.global_context thy HOL_basic_ss |
278 addsimps (eqvt_thms @ perm_pi_simp @ pt2_atoms) |
278 addsimps (eqvt_thms @ perm_pi_simp @ pt2_atoms) |
279 addsimprocs [mk_perm_bool_simproc ["Fun.id"], |
279 addsimprocs [mk_perm_bool_simproc ["Fun.id"], |
280 NominalPermeq.perm_simproc_app, NominalPermeq.perm_simproc_fun]; |
280 NominalPermeq.perm_simproc_app, NominalPermeq.perm_simproc_fun]; |
281 val fresh_bij = PureThy.get_thms thy "fresh_bij"; |
281 val fresh_bij = Global_Theory.get_thms thy "fresh_bij"; |
282 val perm_bij = PureThy.get_thms thy "perm_bij"; |
282 val perm_bij = Global_Theory.get_thms thy "perm_bij"; |
283 val fs_atoms = map (fn aT => PureThy.get_thm thy |
283 val fs_atoms = map (fn aT => Global_Theory.get_thm thy |
284 ("fs_" ^ Long_Name.base_name (fst (dest_Type aT)) ^ "1")) atomTs; |
284 ("fs_" ^ Long_Name.base_name (fst (dest_Type aT)) ^ "1")) atomTs; |
285 val exists_fresh' = PureThy.get_thms thy "exists_fresh'"; |
285 val exists_fresh' = Global_Theory.get_thms thy "exists_fresh'"; |
286 val fresh_atm = PureThy.get_thms thy "fresh_atm"; |
286 val fresh_atm = Global_Theory.get_thms thy "fresh_atm"; |
287 val swap_simps = PureThy.get_thms thy "swap_simps"; |
287 val swap_simps = Global_Theory.get_thms thy "swap_simps"; |
288 val perm_fresh_fresh = PureThy.get_thms thy "perm_fresh_fresh"; |
288 val perm_fresh_fresh = Global_Theory.get_thms thy "perm_fresh_fresh"; |
289 |
289 |
290 fun obtain_fresh_name ts T (freshs1, freshs2, ctxt) = |
290 fun obtain_fresh_name ts T (freshs1, freshs2, ctxt) = |
291 let |
291 let |
292 (** protect terms to avoid that fresh_prod interferes with **) |
292 (** protect terms to avoid that fresh_prod interferes with **) |
293 (** pairs used in introduction rules of inductive predicate **) |
293 (** pairs used in introduction rules of inductive predicate **) |
608 case subtract (op =) atoms' atoms of |
608 case subtract (op =) atoms' atoms of |
609 [] => () |
609 [] => () |
610 | xs => error ("No such atoms: " ^ commas xs); |
610 | xs => error ("No such atoms: " ^ commas xs); |
611 atoms) |
611 atoms) |
612 end; |
612 end; |
613 val perm_pi_simp = PureThy.get_thms thy "perm_pi_simp"; |
613 val perm_pi_simp = Global_Theory.get_thms thy "perm_pi_simp"; |
614 val eqvt_ss = Simplifier.global_context thy HOL_basic_ss addsimps |
614 val eqvt_ss = Simplifier.global_context thy HOL_basic_ss addsimps |
615 (NominalThmDecls.get_eqvt_thms ctxt @ perm_pi_simp) addsimprocs |
615 (NominalThmDecls.get_eqvt_thms ctxt @ perm_pi_simp) addsimprocs |
616 [mk_perm_bool_simproc names, |
616 [mk_perm_bool_simproc names, |
617 NominalPermeq.perm_simproc_app, NominalPermeq.perm_simproc_fun]; |
617 NominalPermeq.perm_simproc_app, NominalPermeq.perm_simproc_fun]; |
618 val (([t], [pi]), ctxt') = ctxt |> |
618 val (([t], [pi]), ctxt') = ctxt |> |