375 The regularize_trm accepts raw theorems in which equalities |
375 The regularize_trm accepts raw theorems in which equalities |
376 and quantifiers match exactly the ones in the lifted theorem |
376 and quantifiers match exactly the ones in the lifted theorem |
377 but also accepts partially regularized terms. |
377 but also accepts partially regularized terms. |
378 |
378 |
379 This means that the raw theorems can have: |
379 This means that the raw theorems can have: |
380 Ball (Respects R), Bex (Respects R), Bexeq (Respects R), Babs, R |
380 Ball (Respects R), Bex (Respects R), Bex1_rel (Respects R), Babs, R |
381 in the places where: |
381 in the places where: |
382 All, Ex, Ex1, %, (op =) |
382 All, Ex, Ex1, %, (op =) |
383 is required the lifted theorem. |
383 is required the lifted theorem. |
384 |
384 |
385 *) |
385 *) |
386 |
386 |
387 val mk_babs = Const (@{const_name Babs}, dummyT) |
387 val mk_babs = Const (@{const_name Babs}, dummyT) |
388 val mk_ball = Const (@{const_name Ball}, dummyT) |
388 val mk_ball = Const (@{const_name Ball}, dummyT) |
389 val mk_bex = Const (@{const_name Bex}, dummyT) |
389 val mk_bex = Const (@{const_name Bex}, dummyT) |
390 val mk_bex1 = Const (@{const_name Bex1}, dummyT) |
390 val mk_bex1 = Const (@{const_name Bex1}, dummyT) |
391 val mk_bexeq = Const (@{const_name Bexeq}, dummyT) |
391 val mk_bexeq = Const (@{const_name Bex1_rel}, dummyT) |
392 val mk_resp = Const (@{const_name Respects}, dummyT) |
392 val mk_resp = Const (@{const_name Respects}, dummyT) |
393 |
393 |
394 (* - applies f to the subterm of an abstraction, |
394 (* - applies f to the subterm of an abstraction, |
395 otherwise to the given term, |
395 otherwise to the given term, |
396 - used by regularize, therefore abstracted |
396 - used by regularize, therefore abstracted |
501 if resrel <> needrel |
501 if resrel <> needrel |
502 then term_mismatch "regularize (Bex)" ctxt resrel needrel |
502 then term_mismatch "regularize (Bex)" ctxt resrel needrel |
503 else mk_bex $ (mk_resp $ resrel) $ subtrm |
503 else mk_bex $ (mk_resp $ resrel) $ subtrm |
504 end |
504 end |
505 |
505 |
506 | (Const (@{const_name "Bexeq"}, ty) $ resrel $ t, Const (@{const_name "Ex1"}, ty') $ t') => |
506 | (Const (@{const_name "Bex1_rel"}, ty) $ resrel $ t, Const (@{const_name "Ex1"}, ty') $ t') => |
507 let |
507 let |
508 val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
508 val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
509 val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty') |
509 val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty') |
510 in |
510 in |
511 if resrel <> needrel |
511 if resrel <> needrel |