Time 
Nick 
Message 
00:02 
tangentstorm 
i guess i'll stick with the exercises in concrete semantics for the time being. 
01:21 
inte 
wow, one can make qsort look deceptively simple... http://sprunge.us/KCJa 
01:23 
inte 
(this is a bit shorter than I expected, but it took quite a few detours to get there...) 
01:26 
inte 
Isabelle's own definition of 'sorted' turns out to be more convenient than tangentstorm's; it's fairly easy to show that for linear orders, they are equivalent. 
01:58 
tangentstorm 
cool, inte :) 
02:00 
tangentstorm 
i was trying to make something work by saying if (max(list a)) < (min(list b)) and both a and b are sorted, then a @ b is sorted. 
02:00 
tangentstorm 
i'm stuck just trying to prove that x <= y ==> x = (min x y) though :/ 
02:09 
tangentstorm 
lemma assumes "x ≤ y" shows "(min x y) = x" using assms by (simp only: min_def; auto) 
02:09 
tangentstorm 
surely there's a better way? 
02:48 

ilbot3 joined #isabelle 
02: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/ 
04:10 
tangentstorm 
:( 
04:10 
tangentstorm 
lemma "(x ≤ y) ∧ (y ≤ z) ⟹ (x ≤ z)" sorry 
04:11 
tangentstorm 
why wouldn't ≤ work like that? 
04:18 
tangentstorm 
lemma lt_trans: fixes x y z assumes "(x ≤ y) ∧ (y ≤ z)" shows "(x ≤ z)" sorry 
04:18 
tangentstorm 
still doesn't work but i guess that's better. 
05:27 

spacekitteh joined #isabelle 
05:28 
spacekitteh 
how can i find the documentation for proof method "HOL.step"? 
10:17 
JCaesar 
tangentstorm: I'm guessing your missing a type (class). 
10:21 
JCaesar 
I can show a lemma fixes x y z :: "'a :: preorder" shows "x ≤ y ⇒ y ≤ z ⇒ x ≤ z" by(rule_tac y = y in order_trans, simp_all), but that's kind of more ugly than I would expect. 
10:21 
JCaesar 
Hm, using order_trans also does it with blast and a few others. 
10:22 
JCaesar 
(And It's just reshowing order_trans anyway.) 
11:08 
ThreeOfEight 
larsrh: wait what? 
11:08 
ThreeOfEight 
quicksort is difficult? 
11:10 
ThreeOfEight 
well, as inte has shown, it is not. 
11:10 
larsrh 
ThreeOfEight: it isn't if you use 'sorted' from the library and its setup 
11:10 
larsrh 
I was under the impression tangentstorm wanted to define everything himself 
11:10 
ThreeOfEight 
hm 
11:11 
ThreeOfEight 
yeah it might require a few auxiliary lemmas 
11:11 
ThreeOfEight 
but unlike insertion sort and bubble sort etc., you don't need any auxiliary functions and complicated invariants 
11:12 
ThreeOfEight 
actually, yeah, insertion sort is probably really easy 
11:13 
ThreeOfEight 
tangentstorm: are you using your own definition of min? 
11:13 
ThreeOfEight 
because if you're using the builtin one, there is min_absorb1 
13:32 
inte 
tangentstorm: Oh, I should have brought up type classes... I defined qsort for 'a::linorder instead of 'a::ord (ord just says that the type 'a comes with relations <= and <); one needs a preorder to ensure that the result of qsort is always sorted; a partial order to prevent that elements of the list are duplicated; and a total order (linorder) to prevent that list elements are dropped by qsort. 
14:38 
JCaesar 
ThreeOfEight: It's not entirely simple, is it? Termination is a bit of a problem, no? 
14:43 
larsrh 
JCaesar: for qsort? No, don't think so 
14:43 
larsrh 
For bubblesort, probably yes 
14:50 
JCaesar 
Oops, bubblesort is what I meant, yes… 
16:01 
ThreeOfEight 
yeah I think you have to define the number of inversions in the list and show that that decreases with every step 
17:22 
JCaesar 
I did that for my Semantics christmas homework, but I don't remember how… 
17:22 
JCaesar 
Anyway, does Isabelle have a type like Either? 
17:41 
larsrh 
JCaesar: yes, 'a + 'b 
17:41 
larsrh 
constructors being Inl and Inr 
17:43 
JCaesar 
ty 
17:58 

JCaesar joined #isabelle 
18:08 

JCaesar joined #isabelle 
18:50 

spacekitteh joined #isabelle 
23:25 

spacekittehwork joined #isabelle 