Hi prof. Dawson,
thank you very much. With your given new definition (of INVERSE) I believe the
proofs of some related lemmas now become trivial (using theorems of LINV, et
al. in pred_setTheory).
Regards,
Chun
> Il giorno 28 mag 2018, alle ore 04:35, Jeremy Dawson
>
Hi Chun,
See LINV and RINV in pred_set.
I found the definitions of these pointlessly restrictive since they only
applied for an injective/surjective function. So I changed things to
define them both in terms of LINV_OPT which I defined. (Hence the old
theorem names LINV_DEF and RINV_DEF.)
=
Workshop on Formal Verification of Physical Systems (FVPS 2018)
August 17, 2018
RISC, Hagenberg, Austria
Co-located with CICM 2018
Hi,
I saw the following definition in the current pending request (vector theory
#513):
val INVERSE_DEF = Define `INVERSE f = \y. @x. f x = y`;
But isn’t this too common to be already somewhere in HOL’s theory library? If
so, where is it?
Regards,
Chun
signature.asc
Description:
