Re: [isabelle] Inequality assumption



As virtually everything in Isabelle/HOL is defined rather than postulated, there is no danger of inconsistency. Moreover, extending the domain of a partial function does not affect any statements that are confined to the original domain. We can use any values we please, but in the case of division, the choice of zero is best in that it allows a number of well-known laws to hold unconditionally. An example is (x + y) / z = x/z + y/z.

Larry Paulson


> On 7 Jul 2016, at 11:57, Andreas RÃhler <andreas.roehler at easy-emacs.de> wrote:
> 
> 
> 
> On 05.07.2016 17:27, Lawrence Paulson wrote:
>> We have taken the liberty of extending division with x/0 = 0 precisely so that a great many theorems, including the one you mention, can be proved more generally.
>> 
>> Larry Paulson
>> 
>> 
>> 
> 
> Hmm, than it would still more useful to replace False by Truth, which makes Truth and Truth a much more refreshing experience and a happier world ;)
> 
> Well, the nasty thing here IMHO is: dividing by zero might be permitted, but can't be zero, it's negativ or positiv infinity, resp. |infinity| - quite different from 0.
> 
> Andreas,
> not that much surprised.
> 





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.