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
