123 val fv_simps = @{thms rbv2.simps} |
123 val fv_simps = @{thms rbv2.simps} |
124 *} |
124 *} |
125 *) |
125 *) |
126 |
126 |
127 ML {* |
127 ML {* |
128 fun build_eqvts_tac induct simps ctxt inds _ = (Datatype_Aux.indtac induct inds THEN_ALL_NEW |
|
129 (asm_full_simp_tac (HOL_ss addsimps |
|
130 (@{thm atom_eqvt} :: (Nominal_ThmDecls.get_eqvts_thms ctxt) @ (Nominal_ThmDecls.get_eqvts_raw_thms ctxt) @ simps)))) 1 |
|
131 *} |
|
132 |
|
133 ML {* |
|
134 fun perm_arg arg = |
128 fun perm_arg arg = |
135 let |
129 let |
136 val ty = fastype_of arg |
130 val ty = fastype_of arg |
137 in |
131 in |
138 Const (@{const_name permute}, @{typ perm} --> ty --> ty) |
132 Const (@{const_name permute}, @{typ perm} --> ty --> ty) |
139 end |
133 end |
140 *} |
134 |
141 |
135 val perm_at = @{term "permute :: perm \<Rightarrow> atom set \<Rightarrow> atom set"} |
142 |
|
143 ML {* |
|
144 fun build_eqvts bind funs tac ctxt = |
|
145 let |
|
146 val pi = Free ("p", @{typ perm}); |
|
147 val types = map (domain_type o fastype_of) funs; |
|
148 val indnames = Name.variant_list ["p"] (Datatype_Prop.make_tnames types); |
|
149 val args = map Free (indnames ~~ types); |
|
150 val perm_at = @{term "permute :: perm \<Rightarrow> atom set \<Rightarrow> atom set"} |
|
151 fun eqvtc (fnctn, arg) = |
|
152 HOLogic.mk_eq ((perm_at $ pi $ (fnctn $ arg)), (fnctn $ (perm_arg arg $ pi $ arg))) |
|
153 val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map eqvtc (funs ~~ args))) |
|
154 val thm = Goal.prove ctxt ("p" :: indnames) [] gl (tac indnames) |
|
155 val thms = HOLogic.conj_elims thm |
|
156 in |
|
157 Local_Theory.note ((bind, [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), thms) ctxt |
|
158 end |
|
159 *} |
136 *} |
160 |
137 |
161 lemma exi: "\<exists>(pi :: perm). P pi \<Longrightarrow> (\<And>(p :: perm). P p \<Longrightarrow> Q (pi \<bullet> p)) \<Longrightarrow> \<exists>pi. Q pi" |
138 lemma exi: "\<exists>(pi :: perm). P pi \<Longrightarrow> (\<And>(p :: perm). P p \<Longrightarrow> Q (pi \<bullet> p)) \<Longrightarrow> \<exists>pi. Q pi" |
162 apply (erule exE) |
139 apply (erule exE) |
163 apply (rule_tac x="pi \<bullet> pia" in exI) |
140 apply (rule_tac x="pi \<bullet> pia" in exI) |