I think I get it ...
> REWRITE_RULE [FUN_EQ_THM] (ASSUME ``R = R'``);
<>
val it =
[.] |- R = R':
thm
> REWRITE_RULE [FUN_EQ_THM] (ASSUME ``(R:'a -> 'a -> bool) = R'``);
val it =
[.] |- ∀x x'. R x x' ⇔ R' x x':
thm
> Il giorno 24 mar 2017, alle ore 21:50, Thomas Tuerk
Hi Thomas,
Sorry, I found and tried FUN_EQ_THM, but failed to see the path to benefit from
it ...
> Il giorno 24 mar 2017, alle ore 21:50, Thomas Tuerk
> ha scritto:
>
> Hi Chun,
>
> use functional extensionality. There are many ways to do it, one is using
> the
Hi Chun,
use functional extensionality. There are many ways to do it, one is
using the theorem boolTheory.FUN_EQ_THM.
Best
Thomas
On 24.03.2017 21:42, Chun Tian (binghe) wrote:
> Hi again,
>
> If I have a theorem saying two (2-ary) relations are the same:
>
> |- R = R’
>
> Then I can easily
Hi again,
If I have a theorem saying two (2-ary) relations are the same:
|- R = R’
Then I can easily prove the following theorem using REWRITE_TAC:
|- !x y. R x y = R’ x y
But if I had the second one first, how to prove the previous one?
Regards,
Chun Tian
signature.asc
Description: