Thanks for the references and suggestions. As a scaled-down example of part of the time consumption, this takes 400 million CPU cycles:
INT_ARITH `&193650890589077504 * (&2 * (y:int) + &1)
<= &47942158315484610560 * (&2 * (x:int) + &1)
+ &135203236847161865141
/\
&0 <= &2655641718416121605914624 * (&2 * x + &1)
+ &2208414543647439060992 * (&2 * y + &1)
+ &6004289407548407186399935
==>
&0 <= &13137886070707932161376256 * (&2 * x + &1)
+ &17509226798704706453504 * (x + y + &1)
+ &36152178747194683600721967`;;
Hand proof: take 6532449000950803555513091/700376017867732114912 and
26794012414555294513937/5603008142941856919296 times the first and
second inequalities, add, and observe that you now have a stronger
version of the conclusion, offset by 1581608968911709059178093879/256.
Changing INT_ARITH to g still takes around 100 million CPU cycles, which
makes me wonder whether there's some bottleneck in parsing or printing.
The code that I wrote to do a bunch of searching to find and print the
whole sequence of relevant presumed theorems is, with no optimization
effort, thousands of times faster than this. Of course that code doesn't
have to bother with the symbolic aspects of proof manipulation.
---Dan
signature.asc
Description: PGP signature
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
