Mike Gordon wrote: > HOL nicely simplifies natural number expressions, e.g.: > > - SIMP_CONV arith_ss [] ``?(i:num) (j:num). i <= j``; > > val it = [oracles: DISK_THM] [axioms: ] [] |- (?i j. i <= j) = T : thm > > however, I can't figure out how to get this for integer expressions, e.g.: > > - SIMP_CONV int_ss [] ``?(i:int) (j:int). i <= j``; > ! Uncaught exception: > ! UNCHANGED > > Anyone know if there is a simpset for integers that works on > examples like this?
I know there isn't. There should be though, and I will try to get 'round to it; it's a matter of turning the existing integer decision procedures (Cooper and Omega) into simpset fragments. This has been done for the naturals and the reals, but not yet for the integers. Michael ------------------------------------------------------------------------- This SF.Net email is sponsored by the Moblin Your Move Developer's challenge Build the coolest Linux based applications with Moblin SDK & win great prizes Grand prize is a trip for two to an Open Source event anywhere in the world http://moblin-contest.org/redirect.php?banner_id=100&url=/ _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
