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
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)"
Hi Thomas,
Thanks! Now I got your points:
1. ``(λt. t) = (λt. p)`` cannot reduce to F unless the underlying type
has at least two distinct values (for datatypes with at least two constructors,
it’s easily provable by cases analysis, I think).
2. To prove two lambda-functions,
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
