257 end |
257 end |
258 |
258 |
259 fun NDT ctxt s tac thm = tac thm |
259 fun NDT ctxt s tac thm = tac thm |
260 *} |
260 *} |
261 |
261 |
262 |
|
263 section {* Infrastructure about definitions *} |
|
264 |
|
265 (* Does the same as 'subst' in a given theorem *) |
|
266 ML {* |
|
267 fun eqsubst_thm ctxt thms thm = |
|
268 let |
|
269 val goalstate = Goal.init (Thm.cprop_of thm) |
|
270 val a' = case (SINGLE (EqSubst.eqsubst_tac ctxt [0] thms 1) goalstate) of |
|
271 NONE => error "eqsubst_thm" |
|
272 | SOME th => cprem_of th 1 |
|
273 val tac = (EqSubst.eqsubst_tac ctxt [0] thms 1) THEN simp_tac HOL_ss 1 |
|
274 val goal = Logic.mk_equals (term_of (Thm.cprop_of thm), term_of a'); |
|
275 val cgoal = cterm_of (ProofContext.theory_of ctxt) goal |
|
276 val rt = Goal.prove_internal [] cgoal (fn _ => tac); |
|
277 in |
|
278 @{thm equal_elim_rule1} OF [rt, thm] |
|
279 end |
|
280 *} |
|
281 |
|
282 (* expects atomized definitions *) |
|
283 ML {* |
|
284 fun add_lower_defs_aux lthy thm = |
|
285 let |
|
286 val e1 = @{thm fun_cong} OF [thm]; |
|
287 val f = eqsubst_thm lthy @{thms fun_map.simps} e1; |
|
288 val g = simp_ids f |
|
289 in |
|
290 (simp_ids thm) :: (add_lower_defs_aux lthy g) |
|
291 end |
|
292 handle _ => [simp_ids thm] |
|
293 *} |
|
294 |
|
295 ML {* |
|
296 fun add_lower_defs lthy def = |
|
297 let |
|
298 val def_pre_sym = symmetric def |
|
299 val def_atom = atomize_thm def_pre_sym |
|
300 val defs_all = add_lower_defs_aux lthy def_atom |
|
301 in |
|
302 map Thm.varifyT defs_all |
|
303 end |
|
304 *} |
|
305 |
262 |
306 section {* Infrastructure for collecting theorems for starting the lifting *} |
263 section {* Infrastructure for collecting theorems for starting the lifting *} |
307 |
264 |
308 ML {* |
265 ML {* |
309 fun lookup_quot_data lthy qty = |
266 fun lookup_quot_data lthy qty = |
400 (* FIXME: check that the types correspond to each other? *) |
357 (* FIXME: check that the types correspond to each other? *) |
401 end |
358 end |
402 *} |
359 *} |
403 |
360 |
404 ML {* |
361 ML {* |
405 val mk_babs = Const (@{const_name "Babs"}, dummyT) |
362 val mk_babs = Const (@{const_name Babs}, dummyT) |
406 val mk_ball = Const (@{const_name "Ball"}, dummyT) |
363 val mk_ball = Const (@{const_name Ball}, dummyT) |
407 val mk_bex = Const (@{const_name "Bex"}, dummyT) |
364 val mk_bex = Const (@{const_name Bex}, dummyT) |
408 val mk_resp = Const (@{const_name Respects}, dummyT) |
365 val mk_resp = Const (@{const_name Respects}, dummyT) |
409 *} |
366 *} |
410 |
367 |
411 ML {* |
368 ML {* |
412 (* - applies f to the subterm of an abstraction, *) |
369 (* - applies f to the subterm of an abstraction, *) |