Time 
Nick 
Message 
09:48 

seafood joined #isabelle 
10:29 

seafood joined #isabelle 
11:54 

silver joined #isabelle 
16:49 

chindy joined #isabelle 
17:36 
chindy 
can someone help me with this thy? http://pastebin.com/6PpQkiAy \n i am unable to show associativity 
17:39 
larsrh 
chindy: 1) aux_lem1 is oriented the wrong way; 2) aux_lem2 is needless and makes the simplifier loop 
17:41 
chindy 
ahh.. 
17:42 
chindy 
larsrh, the problem with aux_lem2 makes sense but how did you see that aux_lem1 was the wrong way? 
17:46 
chindy 
^nvm 
17:47 
larsrh 
chindy: a healthy dose of experience :) 
17:47 
larsrh 
most of the time the idea is to "bubble up" the constructors 
17:48 
larsrh 
unfortunately I can't provide you with a more coherent explanation 
17:48 
larsrh 
btw, you should prefer induct over induct_tac 
17:48 
larsrh 
where'd you pick up induct_tac anyway? 
17:51 
chindy 
larsrh, the isabelle tutorial from the isabelle website 
17:51 
chindy 
whats the difference between induct and induct_tac ? 
17:53 
larsrh 
that's what I feared ... the "tutorial" is sadly outdated 
17:54 
larsrh 
Please use progprove instead 
17:54 
larsrh 
just a couple of hours ago the 20161 release has been cut; there, the tutorial is not listed as prominently as before 
17:55 
chindy 
ahh i see 
17:55 
larsrh 
"induct_tac" is what we call "old style"; it does a couple of things in the wrong way 
17:55 
larsrh 
e.g. how it deals with assumptions is not as expected 
17:55 
larsrh 
rule of thumb: if it ends with "_tac", don't use it unless you know exactly what you're doing 
17:55 
larsrh 
the "tutorial" itself is not wrong, it's just describing an outdated style of using the system 
17:56 
larsrh 
here's the more modern one: http://isabelle.in.tum.de/dist/Isabelle20161/doc/progprove.pdf 
17:57 
chindy 
thanks a lot 
18:37 
larsrh 
you're welcome :) 
18:55 
chindy 
larsrh, could you just help me out again... this is from the exercise in the tutorial you posted (http://pastebin.com/G69FaUc0) i see that isabelle needs som kind of distributive property of listsum/contents but how can give the correct lemma ? 
19:32 
ThreeOfEight 
chindy: you probably want something like "lemma listsum_append [simp]: "listsum (xs @ ys) = listsum xs + listsum ys"" 
19:32 
ThreeOfEight 
doesn't have anything to do with contents 
19:33 
ThreeOfEight 
you just need the fact that listsum distributes over concatenation of lists 
19:34 
larsrh 
your aux_lem1 is not general enough 
19:34 
larsrh 
(to be proven directly via induction, that is) 
19:34 

ammbauer joined #isabelle 
19:34 
larsrh 
but it follows directly from listsum_append 
19:34 
larsrh 
and with it Ex2_6 goes through as expected 
19:34 

julian__ joined #isabelle 
19:36 
ThreeOfEight 
chindy: out of curiosity, why are you doing Isabelle stuff? Is it for a university course? 
19:39 
julian__ 
ThreeOfEight, not really for a course, but its for University. Basically my prof told me is should learn isabelle for my bachelor thesis. But frankly, i dont really wanna bother him with these "basics" 
19:39 

chindy joined #isabelle 
19:41 
chindy 
@ThreeOfEight, yea thanks that worked 
19:43 
ThreeOfEight 
chindy: that wouldn't be Rene Thiemann, by any chance? 
19:43 
chindy 
no, why ? 
19:44 
ThreeOfEight 
Just wondering who else does Isabelle in Austria. 
19:46 
chindy 
ThreeOfEight, are you from Amsterdam or Uterecht ?= 
19:46 
ThreeOfEight 
chindy: no, Munich. 
19:47 
ThreeOfEight 
Right from the main center of activity. (larsrh, too) 
19:47 
chindy 
ah... i see 
19:47 
ThreeOfEight 
(activity wrt. Isabelle) 
19:47 
ThreeOfEight 
So what are you doing in your thesis? 
19:49 
chindy 
formalizing some (not too difficult) game theory (hopefully) 
19:50 
chindy 
@ThreeOfEight, but why does your ip say you are from amsterdam ??? 
19:52 
ThreeOfEight 
chindy: because that's where my vserver is 
19:52 
ThreeOfEight 
on which my tmux is running 
19:53 
chindy 
ahh ... that makes sense ;) 
19:53 
ThreeOfEight 
Ah, Game Theory. Very interesting. 
19:53 
ThreeOfEight 
I worked on Social Choice Theory in the past. 
19:53 
ThreeOfEight 
I even thought about doing some game theory at some point myself. What results are you interested in in particular? 
20:11 
chindy 
@ThreeOfEight, well i dont know yet, im gonna have to read up on that over the holidays 
22:44 

silver_ joined #isabelle 