Time 
Nick 
Message 
01:48 

ilbot3 joined #isabelle 
01:48 

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:33 

stoopkid joined #isabelle 
05:51 
pruvisto 
okay monoid_mult /isn't/ enough because you can't do "2 * …" 
05:51 
pruvisto 
you'd have to rewrite your function without the 2* and then it would work 
05:51 
pruvisto 
JCaesar: so, I trust you found and proved the solution? 
05:53 
pruvisto 
inte: my guess is that it has something to do with it being defined in a type class 
07:01 
JCaesar 
pruvisto: Did. k*2^(2^n). 
07:02 
pruvisto 
yup 
07:02 
pruvisto 
primrec works fine, too 
07:02 
pruvisto 
by (induction n arbitrary: k) (simp_all add: semiring_normalization_rules(36)) 
07:09 
JCaesar 
interestingly, my sledgehammer used number 26 instead of 36… 
07:15 
pruvisto 
That's Numberwang! 
07:21 
larsrh 
ouch, there seems to be even more fallout from the LDAP problem 
07:54 

dave24 joined #isabelle 
09:11 
dave24 
is there a logarithm function? 
09:18 
dave24 
nvm found it 
09:18 
JCaesar 
what's it called? 
09:23 
dave24 
its in http://isabelle.in.tum.de/library/HOL/HOL/Transcendental.html 
09:23 
dave24 
called just log 
09:24 
dave24 
and theres one for natural numbers as well: http://isabelle.in.tum.de/library/HOL/HOLLibrary/Log_Nat.html 
09:27 
JCaesar 
ah. :) 
10:18 
pruvisto 
there's also ln 
10:19 
pruvisto 
and then there's Discrete.log, which I think is essentially "natlog 2" 
10:19 
pruvisto 
not sure if bitlen still exists, that was also more or less "natlog 2", iirc 
10:35 

silver joined #isabelle 
10:40 
JCaesar 
I saw something called bitlog in Log_Nat. 
14:01 

stoopkid joined #isabelle 
15:00 
larsrh 
I just created a datatype plugin that generates the following theorem: 
15:00 
larsrh 
Typerep.typerep.Typerep_def: Typerep.Typerep.typerep.Typerep ≡ typerep.Typerep 
15:05 
pruvisto 
Lovely. 
16:06 
JCaesar 
wtf? meson is capable of not solving goals? 
16:06 
JCaesar 
I do an apply meson, I have one subgoal before and one after. 
16:06 
JCaesar 
and sledgehammer claims that by meson would solve the goal. 
16:07 
JCaesar 
metis does solve it. O_O 
17:43 
JCaesar 
Hm, does anybody know what kind of goat I have to sacrifice to get proper list comprehensions in latex output? 
20:05 
pruvisto 
JCaesar: what do you mean by "proper"? 
20:05 
JCaesar 
actually… existent would be enough… 
20:06 
pruvisto 
hm 
20:06 
JCaesar 
(i've already sprayed a version of the id function that gets printed to nothing to avoid etacontractions all over the place, so that should not be a problem.) 
20:07 
pruvisto 
"filter" usually prettyprints as a list comprehension for me 
20:07 
pruvisto 
don't know about the rest 
20:07 
pruvisto 
I don't use the LaTeX output 
20:34 
JCaesar 
I proved some lemma on [foo a b. a < A, b < B]. it gets printed as concat (map (λ a. map (λ b. foo a b))). 
20:35 
JCaesar 
I wonder if I can just define some constant and then give that an appropriate printing… 
22:59 

stoopkid joined #isabelle 
23:09 
chindy 
what is \longrightarrow? and how is continuous F f defined using a said arrow ? 
23:41 
chindy 
should f22 follow quite simply ? http://downthetypehole.de/paste/BImdLQzm 