Time 
Nick 
Message 
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/ 
10:04 
ThreeOfEight 
barrucadu: Well, I did find out that you can replace your whole BNF proof for FMap with a simple "lift_bnf (dead 'k, 'v) fmap [wits: "Map.empty :: 'k ⇒ 'v option"] for map: fmap_map rel: fmap_rel by simp_all" in Isabelle2016 
10:04 
ThreeOfEight 
But that doesn't fix the relator thing either. I have no idea how to fix that. 
10:04 
ThreeOfEight 
You should really ask on the isabelle mailing list. 
13:42 
tangentstorm 
ah thanks for the hints on qsort. i think that i want a partial order, inte, because it ought to be able to sort lists with duplicate items. 
13:43 
tangentstorm 
JCaesar: do I just have to know that order_trans and such are there, or is there a way to discover them? 
13:47 
inte 
tangentstorm: with just a partial order, sorting [a,b] might result in [a], because a and b might be incomparable (it's possible that neither b <= a nor a < b hold.) By "duplication" I meant that sorting [a,b] might result in [b,a,b] but on second thought, since x < y is defined as x <= y and not y <= x, even a preorder would be fine there... 
14:19 
JCaesar 
tangentstorm: find_theorems "?a ≤ ?b ==> ?b ≤ ?c ==> ?a ≤ ?c" (find theorems also takes _ instead of ?variable if you're lazy. Also, just stating that as a lemma should trigger auto solvedirect.) 
14:40 
tangentstorm 
oh hey. that's handy. thanks! 