213 [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term bv1}, 0)], [], [(SOME @{term bv1}, 0)]]], |
213 [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term bv1}, 0)], [], [(SOME @{term bv1}, 0)]]], |
214 [[], [[]], [[], []]]] *} |
214 [[], [[]], [[], []]]] *} |
215 print_theorems |
215 print_theorems |
216 *) |
216 *) |
217 |
217 |
218 ML {* |
218 |
219 fun build_alpha_inj_gl thms ctxt = |
219 ML {* |
|
220 fun alpha_inj_tac dist_inj intrs elims = |
|
221 SOLVED' (asm_full_simp_tac (HOL_ss addsimps intrs)) ORELSE' |
|
222 rtac @{thm iffI} THEN' RANGE [ |
|
223 (eresolve_tac elims THEN_ALL_NEW |
|
224 asm_full_simp_tac (HOL_ss addsimps dist_inj) |
|
225 ), |
|
226 (asm_full_simp_tac (HOL_ss addsimps intrs))] |
|
227 *} |
|
228 |
|
229 ML {* |
|
230 fun build_alpha_inj_gl thm = |
|
231 let |
|
232 val prop = prop_of thm; |
|
233 val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl prop); |
|
234 val hyps = map HOLogic.dest_Trueprop (Logic.strip_imp_prems prop); |
|
235 fun list_conj l = foldr1 HOLogic.mk_conj l; |
|
236 in |
|
237 if hyps = [] then concl |
|
238 else HOLogic.mk_eq (concl, list_conj hyps) |
|
239 end; |
|
240 *} |
|
241 |
|
242 ML {* |
|
243 fun build_alpha_inj intrs dist_inj elims ctxt = |
220 let |
244 let |
221 (* TODO: use the context for export *) |
245 val ((_, thms_imp), ctxt') = Variable.import false intrs ctxt; |
222 val ((_, thms_imp), ctxt') = Variable.import false thms ctxt; |
246 val gls = map (HOLogic.mk_Trueprop o build_alpha_inj_gl) thms_imp; |
223 fun inj_thm thm_imp = |
247 fun tac _ = alpha_inj_tac dist_inj intrs elims 1; |
224 let |
248 val thms = map (fn gl => Goal.prove ctxt' [] [] gl tac) gls; |
225 val prop = prop_of thm_imp; |
|
226 val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl prop); |
|
227 val hyps = map HOLogic.dest_Trueprop (Logic.strip_imp_prems prop); |
|
228 fun list_conj l = foldr1 HOLogic.mk_conj l; |
|
229 in |
|
230 if hyps = [] then concl |
|
231 else HOLogic.mk_eq (concl, list_conj hyps) |
|
232 end; |
|
233 in |
249 in |
234 Logic.mk_conjunction_list (map (HOLogic.mk_Trueprop o inj_thm) thms_imp) |
250 Variable.export ctxt' ctxt thms |
235 end |
251 end |
236 *} |
252 *} |
237 |
253 |
238 end |
254 end |