# IRC log for #isabelle, 2016-08-23

All times shown according to UTC.

Time Nick Message
00:22 aindilis2 joined #isabelle
10:28 silver joined #isabelle
14:18 silver_ joined #isabelle
15:10 int-e_ 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 int-e it's just part of the division_ring definition: class division_ring = ... + assumes inverse_zero [simp]: "inverse 0 = 0"
19:34 int-e 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