# IRC log for #isabelle, 2016-06-20

All times shown according to UTC.

Time Nick Message
01:47 ilbot3 joined #isabelle
01:47 Topic for #isabelle is now Official channel for the Isabelle/HOL theorem prover: http://www.cl.cam.ac.uk/research/hvg/Isabelle/index.html || Now with logging: http://irclog.perlgeek.de/isabelle/
02:18 fracting joined #isabelle
04:42 fracting joined #isabelle
04:48 fracting joined #isabelle
05:30 fracting joined #isabelle
06:06 fracting joined #isabelle
07:27 fracting joined #isabelle
09:28 silver joined #isabelle
11:06 fracting joined #isabelle
13:39 fracting joined #isabelle
15:22 ammbauer joined #isabelle
17:21 fracting joined #isabelle
17:57 popinman322 joined #isabelle
17:58 popinman322 What is the correct way to check for equality in isabelle? I'm doing something like (if x=e then 1 else 0) and it only really evaluates properly when x=e...
18:09 fracting joined #isabelle
18:17 ThreeOfEight popinman322: I don't understand what you mean
18:17 ThreeOfEight Can you clarify?
18:17 ThreeOfEight Are you using the "value" command?
18:17 popinman322 ThreeOfEight, yes, I'm using value
18:18 ThreeOfEight Okay, short answer: if you just write "(if x = e then 1 else 0)", then x and e are both free variables of unknown value
18:18 ThreeOfEight so of course, Isabelle cannot know whether x and e have the same value
18:18 ThreeOfEight if you write "x = x", then that's obviously true and it can be simplified
18:19 popinman322 But in cases of, say, "1 = 2"
18:19 ThreeOfEight same story
18:19 ThreeOfEight in that case, 1 and 2 are polymorphic numerals
18:19 popinman322 Ah, I see
18:20 ThreeOfEight granted, 1 = 2 probably holds in no reasonable numeric type
18:21 ThreeOfEight but due to the way that Isabelle's type classes are set up, if you write "1" or "2", that can be pretty much any type in which something like a "1" element and additione xist
18:21 ThreeOfEight if you write "(1::nat) = 2", it should work as expected
18:21 ThreeOfEight (Extra information: "value" can use several different methods of evaluation)
18:22 ThreeOfEight (the code generator is the preferred one; then, Isabelle generates executable ML code and runs it and interprets the result; this only works if there are no free variables and if the code generator is set up correctly)
18:22 ThreeOfEight (the other ones are "normalisation by evaluation" and the simplifier, those are much slower, but also work with free variables)
18:23 ThreeOfEight (if you write something like "if 1 = 2 then …", the code generation evaluator fails and Isabelle falls back to nbe, which only simplifies the result but does not necessarily print a definitive result value)
18:24 ThreeOfEight (if you write something like "if (1::nat) = 2 then 1::nat else 0", then code generation works)
18:24 popinman322 ThreeOfEight, can you specify which method to use?
18:24 ThreeOfEight (you can force Isabelle to use a specific evaluator by writing e.g. value [code] "foo")
18:25 ThreeOfEight There's detailed information here if you need it: https://isabelle.in.tum.de/doc/codegen.pdf
18:25 popinman322 Thankee
18:26 ThreeOfEight there's also a small amount of information on the value command in isar-ref, page 280: http://isabelle.in.tum.de/dist/Isabelle2016/doc/isar-ref.pdf
18:26 ThreeOfEight but I think it doesn't say much more than what I've already said here