# IRC log for #isabelle, 2016-01-12

All times shown according to UTC.

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, int-e, 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 int-e 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!