I would use 


to expand the assumptions to

   !x. x = prefix (label l) x


   !x. x = p


Of course, this is a blunt weapon, so you may not wish to use it if other 
assumptions are disrupted too much. 


On 5/8/17, 04:25, "Chun Tian (binghe)" <binghe.l...@gmail.com> wrote:

    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?
    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

Reply via email to