Time 
Nick 
Message 
00:22 

aindilis2 joined #isabelle 
10:28 

silver joined #isabelle 
14:18 

silver_ joined #isabelle 
15:10 

inte_ joined #isabelle 
19:23 
ammbauer 
why does this expression (value "(1::real) / 0") spit out ("0"::real)? 
19:30 
ammbauer 
aha, because of thm divide_zero. does anybody have a short explanation for that theorem? 
19:33 
inte 
it's just part of the division_ring definition: class division_ring = ... + assumes inverse_zero [simp]: "inverse 0 = 0" 
19:34 
inte 
My guess is that it's for convenience, since you can't have partial functions in Isabelle, and the value 0 allows for laws like inverse (a*b) = inverse b * inverse a to hold without precondition. 
20:20 
ThreeOfEight 
Yes, exactly that. 
20:20 
ThreeOfEight 
In fact, a lot of theorems hold that way. 
20:20 
ThreeOfEight 
It's just convenient. 
20:21 
ThreeOfEight 
You could define it as "undefined", but that pretty much only has disadvantages 
20:21 
ThreeOfEight 
(for instance, code generation becomes more difficult) 
20:22 
ThreeOfEight 
(you cannot implement "undefined", so you have to throw an exception, and everyone hates exceptions) 
20:23 
ThreeOfEight 
similar tradeoffs were made for "sqrt on negative numbers", "ln x" for real x <= 0, "x powr y" for real x <= 0 etc. 
20:42 
ammbauer 
I see. It also makes finding an n for which "1/n < e" holds really easy :D 
20:50 
ThreeOfEight 
well, normally you require something like "an m such that for all n >= m, 1/n < e" 
20:53 
ammbauer 
or use "1/(Suc n) < e" 
20:54 
ThreeOfEight 
by the way, juggling epsilons is rarely required in Isabelle 
20:54 
ThreeOfEight 
usually it's much more elegant and productive to use filters and topology directly 
20:59 
ammbauer 
yeah, but then I would need to understand filters :) 
23:34 

dmiles joined #isabelle 