118 val fv_simps = @{thms rbv2.simps} |
118 val fv_simps = @{thms rbv2.simps} |
119 *} |
119 *} |
120 *) |
120 *) |
121 |
121 |
122 ML {* |
122 ML {* |
123 fun build_eqvts bind funs perms simps induct ctxt = |
123 fun build_eqvts bind funs simps induct ctxt = |
124 let |
124 let |
125 val pi = Free ("p", @{typ perm}); |
125 val pi = Free ("p", @{typ perm}); |
126 val types = map (domain_type o fastype_of) funs; |
126 val types = map (domain_type o fastype_of) funs; |
127 val indnames = Name.variant_list ["p"] (Datatype_Prop.make_tnames (map body_type types)); |
127 val indnames = Name.variant_list ["p"] (Datatype_Prop.make_tnames (map body_type types)); |
128 val args = map Free (indnames ~~ types); |
128 val args = map Free (indnames ~~ types); |
129 val perm_at = @{term "permute :: perm \<Rightarrow> atom set \<Rightarrow> atom set"} |
129 val perm_at = @{term "permute :: perm \<Rightarrow> atom set \<Rightarrow> atom set"} |
130 fun eqvtc (fnctn, (arg, perm)) = |
130 fun perm_arg arg = Const (@{const_name permute}, @{typ perm} --> fastype_of arg --> fastype_of arg) |
131 HOLogic.mk_eq ((perm_at $ pi $ (fnctn $ arg)), (fnctn $ (perm $ pi $ arg))) |
131 fun eqvtc (fnctn, arg) = |
132 val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map eqvtc (funs ~~ (args ~~ perms)))) |
132 HOLogic.mk_eq ((perm_at $ pi $ (fnctn $ arg)), (fnctn $ (perm_arg arg $ pi $ arg))) |
|
133 val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map eqvtc (funs ~~ args))) |
133 fun tac _ = (Datatype_Aux.indtac induct indnames THEN_ALL_NEW |
134 fun tac _ = (Datatype_Aux.indtac induct indnames THEN_ALL_NEW |
134 (asm_full_simp_tac (HOL_ss addsimps |
135 (asm_full_simp_tac (HOL_ss addsimps |
135 (@{thm atom_eqvt} :: (Nominal_ThmDecls.get_eqvts_thms ctxt) @ (Nominal_ThmDecls.get_eqvts_raw_thms ctxt) @ simps)))) 1 |
136 (@{thm atom_eqvt} :: (Nominal_ThmDecls.get_eqvts_thms ctxt) @ (Nominal_ThmDecls.get_eqvts_raw_thms ctxt) @ simps)))) 1 |
136 val thm = Goal.prove ctxt ("p" :: indnames) [] gl tac |
137 val thm = Goal.prove ctxt ("p" :: indnames) [] gl tac |
137 val thms = HOLogic.conj_elims thm |
138 val thms = HOLogic.conj_elims thm |