--- a/Nominal/Rsp.thy Tue Mar 02 08:58:28 2010 +0100
+++ b/Nominal/Rsp.thy Tue Mar 02 11:04:49 2010 +0100
@@ -136,6 +136,10 @@
end
*}
+lemma exi: "\<exists>(pi :: perm). P pi \<Longrightarrow> (\<And>(p :: perm). P p \<Longrightarrow> Q (pi \<bullet> p)) \<Longrightarrow> \<exists>pi. Q pi"
+apply (erule exE)
+apply (rule_tac x="pi \<bullet> pia" in exI)
+by auto
ML {*
fun build_alpha_eqvts funs perms simps induct ctxt =
@@ -151,18 +155,20 @@
(alpha $ (perm $ pi $ arg) $ (perm $ pi $ arg2)))
val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map eqvtc ((funs ~~ perms) ~~ (args ~~ args2))))
fun tac _ = (((rtac impI THEN' etac induct) ORELSE' rtac induct) THEN_ALL_NEW
- (asm_full_simp_tac (HOL_ss addsimps
+ (
+ (asm_full_simp_tac (HOL_ss addsimps
(@{thm atom_eqvt} :: (Nominal_ThmDecls.get_eqvts_thms ctxt) @ simps)))
- THEN_ALL_NEW (TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI) THEN_ALL_NEW
- (etac @{thm alpha_gen_compose_eqvt})) THEN_ALL_NEW
+ THEN_ALL_NEW (etac @{thm exi[of _ _ "p"]} THEN'
+ REPEAT o etac conjE THEN'
+ (TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI))) THEN_ALL_NEW
+ (asm_full_simp_tac HOL_ss) THEN_ALL_NEW
+ (etac @{thm alpha_gen_compose_eqvt[of _ _ _ _ "p"]}) THEN_ALL_NEW
(asm_full_simp_tac (HOL_ss addsimps
- (@{thm atom_eqvt} :: (Nominal_ThmDecls.get_eqvts_thms ctxt) @ simps)))
-) 1
+ (@{thm atom_eqvt} :: (Nominal_ThmDecls.get_eqvts_thms ctxt) @ simps))))) 1
val thm = Goal.prove ctxt ("p" :: indnames @ indnames2) [] gl tac
in
map (fn x => mp OF [x]) (HOLogic.conj_elims thm)
end
*}
-
end