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 > <jeremy.daw...@anu.edu.au> ha scritto: > > 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 >> hol-info@lists.sourceforge.net >> 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 > hol-info@lists.sourceforge.net > 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 hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
