| changeset 1196 | 4efbaba9d754 |
| parent 1193 | a228acf2907e |
| child 1199 | 5770c73f2415 |
| 1193:a228acf2907e | 1196:4efbaba9d754 |
|---|---|
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 {* |
|
219 fun build_alpha_inj_gl thms ctxt = |
|
220 let |
|
221 (* TODO: use the context for export *) |
|
222 val ((_, thms_imp), ctxt') = Variable.import false thms ctxt; |
|
223 fun inj_thm thm_imp = |
|
224 let |
|
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 |
|
234 Logic.mk_conjunction_list (map (HOLogic.mk_Trueprop o inj_thm) thms_imp) |
|
218 end |
235 end |
236 *} |
|
237 |
|
238 end |