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.EXTENSION]
THEN wordsLib.WORD_DECIDE_TAC);
the result comes back in about 3.5 seconds on my ancient laptop:
OK..
runtime: 3.548s, gctime: 0.378s, systime: 0.457s.
> val it =
Initial goal proved.
|- DISJOINT {a | a >= 4096w /\ a < 8192w} {a | a >= 0w /\ a
< 4096w} :
The only difference with what you are trying is the (superfluous)
Cases_on,
and also the use of srw_ss, which knows basic simplifications for the
"current context: which in this case includes sets and set
comprehensions.
Konrad.
On Aug 7, 2009, at 10:11 PM, Lu Zhao wrote:
> 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:
>
> DISJOINT {a | a >= 0x1000w /\ a < 0x2000w}
> {a | a >= 0x0w /\ a < 0x1000w}
>
> I can't image how long it takes if each set has multiple segments. Is
> there any efficient way to prove two sets are disjoint?
>
> Thanks a lot.
> Lu
>
> ----------------------------------------------------------------------
> --------
> Let Crystal Reports handle the reporting - Free Crystal Reports
> 2008 30-Day
> trial. Simplify your report design, integration and deployment -
> and focus on
> what you do best, core application coding. Discover what's new with
> Crystal Reports now. http://p.sf.net/sfu/bobj-july
> _______________________________________________
> hol-info mailing list
> [email protected]
> https://lists.sourceforge.net/lists/listinfo/hol-info
------------------------------------------------------------------------------
Let Crystal Reports handle the reporting - Free Crystal Reports 2008 30-Day
trial. Simplify your report design, integration and deployment - and focus on
what you do best, core application coding. Discover what's new with
Crystal Reports now. http://p.sf.net/sfu/bobj-july
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
