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.)
see my commits
4e806d114105079ead99b4a27a86c08dd5515d68
f3fcad057ccfff3130edc82912ec54155901f085
So, rather than a multiplicity of similarly defined functions (where the
obvious relations between them would not be provable because of the
indeterminacy of @), I'd suggest defining INVERSE in terms of LINV
(eg, I think it would be INVERSE f y = LINV f UNIV y)
Jeremy
On 05/28/2018 12:01 PM, Chun Tian wrote:
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
------------------------------------------------------------------------------
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
------------------------------------------------------------------------------
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
