Hi Lu,
If I do the following (MoscowML based HOL),
- app load ["wordsLib","pred_setLib"];
- g `DISJOINT {a | a >= 0x1000w /\ a < 0x2000w}
{a | a >= 0x0w /\ a < 0x1000w}`;
- time e
(RW_TAC (srw_ss()) [pred_setTheory.DISJOINT_DEF,
pred_setTheory.EXTENS
Hi,
I'd like to prove two sets disjoint. Currently, I use
DISJOINT_DEF,INTER_DEF,EXTENSION to rewrite the goal first, then
Cases_on each bound, and finally use WORD_DECIDE_TAC. This approach
works, but it takes a long time.
For example, it takes over 40s to prove the following theorem:
DI