76 |
76 |
77 |
77 |
78 ML {* |
78 ML {* |
79 fun fvbv_rsp_tac induct fvbv_simps = |
79 fun fvbv_rsp_tac induct fvbv_simps = |
80 ((((rtac impI THEN' etac induct) ORELSE' rtac induct) THEN_ALL_NEW |
80 ((((rtac impI THEN' etac induct) ORELSE' rtac induct) THEN_ALL_NEW |
81 (TRY o rtac @{thm TrueI})) THEN_ALL_NEW asm_full_simp_tac |
81 (TRY o rtac @{thm TrueI})) THEN_ALL_NEW |
82 (HOL_ss addsimps (@{thm alpha_gen} :: fvbv_simps))) |
82 asm_full_simp_tac |
|
83 (HOL_ss addsimps (@{thm alpha_gen} :: fvbv_simps)) |
|
84 THEN_ALL_NEW (REPEAT o eresolve_tac [conjE, exE] THEN' |
|
85 asm_full_simp_tac |
|
86 (HOL_ss addsimps (@{thm alpha_gen} :: fvbv_simps)))) |
83 *} |
87 *} |
84 |
88 |
85 ML {* |
89 ML {* |
86 fun constr_rsp_tac inj rsp equivps = |
90 fun constr_rsp_tac inj rsp equivps = |
87 let |
91 let |
134 in |
138 in |
135 Local_Theory.note ((bind, [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), thms) ctxt |
139 Local_Theory.note ((bind, [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), thms) ctxt |
136 end |
140 end |
137 *} |
141 *} |
138 |
142 |
|
143 lemma exi: "\<exists>(pi :: perm). P pi \<Longrightarrow> (\<And>(p :: perm). P p \<Longrightarrow> Q (pi \<bullet> p)) \<Longrightarrow> \<exists>pi. Q pi" |
|
144 apply (erule exE) |
|
145 apply (rule_tac x="pi \<bullet> pia" in exI) |
|
146 by auto |
139 |
147 |
140 ML {* |
148 ML {* |
141 fun build_alpha_eqvts funs perms simps induct ctxt = |
149 fun build_alpha_eqvts funs perms simps induct ctxt = |
142 let |
150 let |
143 val pi = Free ("p", @{typ perm}); |
151 val pi = Free ("p", @{typ perm}); |
149 fun eqvtc ((alpha, perm), (arg, arg2)) = |
157 fun eqvtc ((alpha, perm), (arg, arg2)) = |
150 HOLogic.mk_imp (alpha $ arg $ arg2, |
158 HOLogic.mk_imp (alpha $ arg $ arg2, |
151 (alpha $ (perm $ pi $ arg) $ (perm $ pi $ arg2))) |
159 (alpha $ (perm $ pi $ arg) $ (perm $ pi $ arg2))) |
152 val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map eqvtc ((funs ~~ perms) ~~ (args ~~ args2)))) |
160 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 |
161 fun tac _ = (((rtac impI THEN' etac induct) ORELSE' rtac induct) THEN_ALL_NEW |
|
162 ( |
|
163 (asm_full_simp_tac (HOL_ss addsimps |
|
164 (@{thm atom_eqvt} :: (Nominal_ThmDecls.get_eqvts_thms ctxt) @ simps))) |
|
165 THEN_ALL_NEW (REPEAT o etac conjE THEN' etac @{thm exi[of _ _ "p"]} THEN' |
|
166 REPEAT o etac conjE THEN' |
|
167 (TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI))) THEN_ALL_NEW |
|
168 (asm_full_simp_tac HOL_ss) THEN_ALL_NEW |
|
169 (etac @{thm alpha_gen_compose_eqvt[of _ _ _ _ "p"]}) THEN_ALL_NEW |
154 (asm_full_simp_tac (HOL_ss addsimps |
170 (asm_full_simp_tac (HOL_ss addsimps |
155 (@{thm atom_eqvt} :: (Nominal_ThmDecls.get_eqvts_thms ctxt) @ simps))) |
171 (@{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 |
172 val thm = Goal.prove ctxt ("p" :: indnames @ indnames2) [] gl tac |
162 in |
173 in |
163 map (fn x => mp OF [x]) (HOLogic.conj_elims thm) |
174 map (fn x => mp OF [x]) (HOLogic.conj_elims thm) |
164 end |
175 end |
165 *} |
176 *} |
166 |
177 |
167 |
|
168 end |
178 end |