[isabelle-dev] Numeral simplification: neg and iszero

[Steven Obua]

>
> NatBin.thy is now nearly "neg"-free, but there are still some other  
> places with lemmas that use "neg". For example, Tools/ 
> ComputeNumeral.thy seems to be a complete re-implementation of the  
> simpset defined in NatBin.thy for arithmetic at type nat. If such  
> other lemmas involving "neg" can be made redundant, or merged into  
> NatBin.thy, then we will be able to remove "neg".
>

The rules in Tools/ComputeNumeral.thy are used within ML code for the  
HOL computing oracle. It's true, they are basically a cleaned up  
version of the NatBin.thy rules; simplification with these rules is  
supposed to work together with the oracle, not necessarily with the  
simplifier. Changes here might break my part of the proof of the  
Kepler Conjecture; but chances are it does not run with the current  
version of Isabelle anyway :-)

Steven