134 in |
134 in |
135 Local_Theory.note ((bind, [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), thms) ctxt |
135 Local_Theory.note ((bind, [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), thms) ctxt |
136 end |
136 end |
137 *} |
137 *} |
138 |
138 |
|
139 lemma exi: "\<exists>(pi :: perm). P pi \<Longrightarrow> (\<And>(p :: perm). P p \<Longrightarrow> Q (pi \<bullet> p)) \<Longrightarrow> \<exists>pi. Q pi" |
|
140 apply (erule exE) |
|
141 apply (rule_tac x="pi \<bullet> pia" in exI) |
|
142 by auto |
139 |
143 |
140 ML {* |
144 ML {* |
141 fun build_alpha_eqvts funs perms simps induct ctxt = |
145 fun build_alpha_eqvts funs perms simps induct ctxt = |
142 let |
146 let |
143 val pi = Free ("p", @{typ perm}); |
147 val pi = Free ("p", @{typ perm}); |
149 fun eqvtc ((alpha, perm), (arg, arg2)) = |
153 fun eqvtc ((alpha, perm), (arg, arg2)) = |
150 HOLogic.mk_imp (alpha $ arg $ arg2, |
154 HOLogic.mk_imp (alpha $ arg $ arg2, |
151 (alpha $ (perm $ pi $ arg) $ (perm $ pi $ arg2))) |
155 (alpha $ (perm $ pi $ arg) $ (perm $ pi $ arg2))) |
152 val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map eqvtc ((funs ~~ perms) ~~ (args ~~ args2)))) |
156 val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map eqvtc ((funs ~~ perms) ~~ (args ~~ args2)))) |
153 fun tac _ = (((rtac impI THEN' etac induct) ORELSE' rtac induct) THEN_ALL_NEW |
157 fun tac _ = (((rtac impI THEN' etac induct) ORELSE' rtac induct) THEN_ALL_NEW |
|
158 ( |
|
159 (asm_full_simp_tac (HOL_ss addsimps |
|
160 (@{thm atom_eqvt} :: (Nominal_ThmDecls.get_eqvts_thms ctxt) @ simps))) |
|
161 THEN_ALL_NEW (etac @{thm exi[of _ _ "p"]} THEN' |
|
162 REPEAT o etac conjE THEN' |
|
163 (TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI))) THEN_ALL_NEW |
|
164 (asm_full_simp_tac HOL_ss) THEN_ALL_NEW |
|
165 (etac @{thm alpha_gen_compose_eqvt[of _ _ _ _ "p"]}) THEN_ALL_NEW |
154 (asm_full_simp_tac (HOL_ss addsimps |
166 (asm_full_simp_tac (HOL_ss addsimps |
155 (@{thm atom_eqvt} :: (Nominal_ThmDecls.get_eqvts_thms ctxt) @ simps))) |
167 (@{thm atom_eqvt} :: (Nominal_ThmDecls.get_eqvts_thms ctxt) @ simps))))) 1 |
156 THEN_ALL_NEW (TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI) THEN_ALL_NEW |
|
157 (etac @{thm alpha_gen_compose_eqvt})) THEN_ALL_NEW |
|
158 (asm_full_simp_tac (HOL_ss addsimps |
|
159 (@{thm atom_eqvt} :: (Nominal_ThmDecls.get_eqvts_thms ctxt) @ simps))) |
|
160 ) 1 |
|
161 val thm = Goal.prove ctxt ("p" :: indnames @ indnames2) [] gl tac |
168 val thm = Goal.prove ctxt ("p" :: indnames @ indnames2) [] gl tac |
162 in |
169 in |
163 map (fn x => mp OF [x]) (HOLogic.conj_elims thm) |
170 map (fn x => mp OF [x]) (HOLogic.conj_elims thm) |
164 end |
171 end |
165 *} |
172 *} |
166 |
173 |
167 |
|
168 end |
174 end |