Hi Chun,
via a subgoal, you can introduce an assumption for a concrete argument.
This should be what you need. I'm thinking of something like
First show that a CCS q exists with "q <> p"
`?q. q <> p` by ...
Then use this new q as an argument)
`(\t. t) q = (\t. p) q` by PROVE_TAC[]
Now you are done by BETA reduction and contradicting assumptions.
Best
Thomas
On 04.08.2017 20:22, Chun Tian (binghe) 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
------------------------------------------------------------------------------
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
