Thanks! Actually I was ever taught (by Thomas) to use FUN_EQ_THM to convert relation equations (R = R’) into provable forms (!x y. R x y = R’ x y), but when I was facing lambda functions I didn’t realize they’re essentially the same thing. (Using PAT_X_ASSUM I can precisely target on any single assumptions, thus other assumptions won’t be affected)
And I found that, once I got ``!x. x = prefix (label l) x``, actually the `distinct` theorems generated by Datatype will directly lead it to False, no need to call the “size” theorems and use arithmetic stuff, although the latter idea also works. —Chun > Il giorno 07 ago 2017, alle ore 01:33, michael.norr...@data61.csiro.au ha > scritto: > > I would use > > fs[FUN_EQ_THM] > > to expand the assumptions to > > !x. x = prefix (label l) x > > and > > !x. x = p > > respectively. > > Of course, this is a blunt weapon, so you may not wish to use it if other > assumptions are disrupted too much. > > Michael > > On 5/8/17, 04:25, "Chun Tian (binghe)" <binghe.l...@gmail.com> wrote: > > Hi, > > This is the first time I met the following goal, in which one of the > assumptions should be able to reduce to F (then the goal is resolved): > > R (λt. t) > ------------------------------------ > 4. (λt. t) = (λt. prefix (label l) t) > > The lambda function has the type of ``CCS -> CCS``, which CCS is my > datatype defined by HOL’s Define command. “prefix” is an constructor of CCS > datatype. I *know* the equation doesn’t hold, because the whatever input > arguments, the resulting CCS on both side must have different “size”, simply > because one is the sub-expression of the other. But how can I actually > reduce it to F? > > The other case is a little different: > > R (λt. t) > ------------------------------------ > 4. (λt. t) = (λt. p) > > The assumption "(λt. t) = (λt. p)” hold for only one case: when input of > lambda function is exactly “p”. For all other cases the left side doesn’t > equal to the right side. But from the view of two functions, they’re > obviously not identical. But how can I actually reduce it to F? > > Regards, > > Chun Tian > > > > ------------------------------------------------------------------------------ > 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
signature.asc
Description: Message signed with OpenPGP using GPGMail
------------------------------------------------------------------------------ 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
