Time 
Nick 
Message 
03:04 

lispy_ joined #isabelle 
10:51 
ThreeOfEight 
the function package is probably the best way, yes. 
10:51 
ThreeOfEight 
someone should really write an ML command to use the function package to just generate an induction scheme without actually declaring a function 
10:52 
ThreeOfEight 
Any volunteers? larsrh, I heard you have a lot of spare time at your hands. 
11:03 
JCaesar 
Don't bash the dead horse… 
12:33 
larsrh 
ThreeOfEight: not sure whether I should laugh or cry about this 
12:33 
larsrh 
Because actually I needed such a thing on more than one occasion already 
12:33 
larsrh 
*would've needed 
12:47 
JCaesar 
So did I. 
12:47 
JCaesar 
larsrh: You gave us the wrong topics for our practikum. :P 
13:11 
ThreeOfEight 
maybe I'll do it at some point 
13:11 
ThreeOfEight 
I've worked on the function package before, after all 
17:31 

mal`` joined #isabelle 
18:27 
JCaesar 
Just me having fun: lemma "0 ≠ 1" … auto Quickcheck found a counterexample: (empty output) 
18:28 
JCaesar 
(I'm just wonderin why it's empty.) 
18:31 
JCaesar 
(Nothing to output I guess.) 
18:31 
inte 
because there are no free variables... it's be helpful to display the chosen types though 
18:32 
inte 
lemma "0 = (1 :: Enum.finite_1)" by simp 
18:32 
inte 
(I tricked it: lemma "0 * x ≠ 1" gives an assignment for x with that type) 
18:33 
inte 
or rather, quickcheck gives the assignment 
18:36 

tangentstorm joined #isabelle 
18:36 
tangentstorm 
fun dub :: "nat ⇒ nat" where "dub 0 = 0"  "dub (Suc m) = add (Suc m) (Suc m)" 
18:36 
tangentstorm 
^ the background turns purple on this for me, but there's no output or tooltip to explain what it means. 
18:36 
tangentstorm 
what does it mean? :) 
18:40 
tangentstorm 
ah, because i had this: theorem add_commut [simp]: "add x y = add x y" 
18:40 
tangentstorm 
.. which was sending it into an infinite loop. removing the [simp] fixed it. 
18:47 
larsrh 
ThreeOfEight: purple means "processing" 
18:47 
larsrh 
sorry 
18:47 
larsrh 
tangentstorm: purple means "processing" 
18:48 
larsrh 
The "fun" package employs the simplifier for some internal tactics, which means it's particularly dependent on a good [simp] setup 
18:48 
tangentstorm 
yeah, thanks. i should have googled a bit more before asking :) 
18:49 
* tangentstorm 
is working through "concrete semantics" 
18:49 
larsrh 
no worries 
18:50 
JCaesar 
(And here I was under the impression that googling doesn't help with Isabelle…) 
18:55 
ThreeOfEight 
it doesn't help much 
19:01 
tangentstorm 
https://lists.cam.ac.uk/pipermail/clisabelleusers/2014January/msg00017.html < it turned up a mailing list discussion that pointed me in the right direction. 
19:02 
tangentstorm 
it doesn't help that all the docs are in PDF though. :/ 
19:02 
ThreeOfEight 
I think they are generated from .thy files 
19:03 
tangentstorm 
that's probably true. i meant for googling though. you get a result and it's just somewhere in a 50page book. :) 
19:04 
tangentstorm 
but there seem to be plenty of great docs, plus stackoverflow ... so it's not like there's a shortage of info. 
19:05 
larsrh 
tangentstorm: Makarius is working on better document preparation 
19:05 
larsrh 
So there's a chance the docs will be available as multipage HTML docs at some point 
19:05 
tangentstorm 
nice :) 
19:28 
tangentstorm 
hrm. i want to prove that `sum range(n)` = `n * (n+1) / 2` for natural numbers, but nat doesn't have / defined. I see Divides.thy, but how would I use it? 
19:28 
tangentstorm 
oh just 'div' i guess 
19:28 
larsrh 
tangentstorm: div 
19:28 
larsrh 
yeah, exactly :) 
19:29 
larsrh 
Don't need to import anything, just plain old 'Main' 
20:10 
tangentstorm 
well i think i made my proof but i can't figure out how to cap it off 
20:10 
tangentstorm 
https://gist.github.com/tangentstorm/4ccb13968414437da36b 
20:13 
tangentstorm 
hrm. hold up. i removed the 'fix n::nat assume n>0' and was able to get isabelle to accept it. any thoughts on how i could make it better? 
20:20 
larsrh 
tangentstorm: unquantified variables in the lemma statement are automatically fixed, so no need to fix them again 
20:21 
larsrh 
You can still 'assume "n > 0"', that way you don't have to repeat your assumption all the time 
20:24 
larsrh 
tangentstorm: I commented on the Gist 
21:15 
tangentstorm 
very nice. thank you, larsrh 
22:04 
ammbauer 
for fucks sake, in einer funktion ∧ statt ∨ benutzt... auf einmal sind die beweise soviel einfacher... kopf > tisch. 
22:08 
larsrh 
ammbauer: I think you picked the wrong channel 
22:13 
ammbauer 
larsrh: ohh, sorry. well, it's isabelle related :D 
22:59 
tangentstorm 
is there any way to make jEdit save as unicode instead of latex? (like for \<LongArrow>) 
23:29 
tangentstorm 
fun qsort :: "'a::ord list ⇒ 'a list" where "qsort [] = []"  "qsort x#xs = qsort (filter (λy. y≤x) xs)" 
23:29 
tangentstorm 
^ why does this give me type problems? "no type arity list::ord" ... op ≤ y :: ??'a ⇒ bool 
23:32 
inte 
qsort x#xs should be qsort (x#xs) 
23:33 
tangentstorm 
aha. thank you 
23:33 
inte 
as written, (qsort x) # xs is a list, and that leads to the odd ord requirement for list. 
23:34 
inte 
err. the x in (qsort x) # xs is a list. 
23:34 
tangentstorm 
gotcha. i keep forgeting how tightly function application binds. 
23:34 
tangentstorm 
thanks 
23:42 
larsrh 
tangentstorm: I don't think there's a way 
23:47 
tangentstorm 
oh, to save as unicode? yeah, i went through like every line in the settings and couldn't find anything. no big deal. 
23:49 
tangentstorm 
i've moved on to trying to prove that my quicksort actually sorts. :) i think i have a decent setup, but i haven't learned enough to know where to go next: https://gist.github.com/tangentstorm/c23f572bf7ed9771b667 
23:53 
larsrh 
tangentstorm: not to curb your enthusiam, but qsort is not trivial, even for advanced users 
23:54 
larsrh 
A simpler sorting function you could try to tackle would be selectionsort 
23:54 
larsrh 
err, I meant insertionsort 
23:55 
larsrh 
If you want to cheat, you can look here: https://github.com/larsrh/sorted/blob/master/Insertion_Sort.thy and check if that looks doable to you 
23:57 
tangentstorm 
hrm. that's a lot more work than i expected. thanks for the warning. 