equal
deleted
inserted
replaced
368 The regularize_trm accepts raw theorems in which equalities |
368 The regularize_trm accepts raw theorems in which equalities |
369 and quantifiers match exactly the ones in the lifted theorem |
369 and quantifiers match exactly the ones in the lifted theorem |
370 but also accepts partially regularized terms. |
370 but also accepts partially regularized terms. |
371 |
371 |
372 This means that the raw theorems can have: |
372 This means that the raw theorems can have: |
373 Ball (Respects R), Bex (Respects R), Bexeq (Respects R), R |
373 Ball (Respects R), Bex (Respects R), Bexeq (Respects R), Babs, R |
374 in the places where: |
374 in the places where: |
375 All, Ex, Ex1, (op =) |
375 All, Ex, Ex1, %, (op =) |
376 is required the lifted theorem. |
376 is required the lifted theorem. |
377 |
377 |
378 *) |
378 *) |
379 |
379 |
380 val mk_babs = Const (@{const_name Babs}, dummyT) |
380 val mk_babs = Const (@{const_name Babs}, dummyT) |
437 val subtrm = Abs(x, ty, regularize_trm ctxt (t, t')) |
437 val subtrm = Abs(x, ty, regularize_trm ctxt (t, t')) |
438 in |
438 in |
439 if ty = ty' then subtrm |
439 if ty = ty' then subtrm |
440 else mk_babs $ (mk_resp $ equiv_relation ctxt (ty, ty')) $ subtrm |
440 else mk_babs $ (mk_resp $ equiv_relation ctxt (ty, ty')) $ subtrm |
441 end |
441 end |
|
442 | (Const (@{const_name "Babs"}, T) $ r $ (t as (Abs (_, ty, _))), t' as (Abs (_, ty', _))) => |
|
443 let |
|
444 val subtrm = regularize_trm ctxt (t, t') |
|
445 val needres = mk_resp $ equiv_relation_chk ctxt (ty, ty') |
|
446 in |
|
447 if r <> needres |
|
448 then term_mismatch "regularize (Babs)" ctxt r needres |
|
449 else mk_babs $ r $ subtrm |
|
450 end |
442 |
451 |
443 | (Const (@{const_name "All"}, ty) $ t, Const (@{const_name "All"}, ty') $ t') => |
452 | (Const (@{const_name "All"}, ty) $ t, Const (@{const_name "All"}, ty') $ t') => |
444 let |
453 let |
445 val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
454 val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
446 in |
455 in |