# IRC log for #isabelle, 2016-10-14

All times shown according to UTC.

Time Nick Message
00:38 ski joined #isabelle
01:47 ilbot3 joined #isabelle
01:47 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/
13:23 silver joined #isabelle
15:12 int-e I'm playing around with a locale that has a symmetric assumption... I've come up with this pattern: http://sprunge.us/APAH?ocaml  but I'm wondering why I have to re-enter the context to get the symmetric version of a lemma I just proved... any ideas?
15:13 int-e (the paste is a toy example but I have a serious application for this)
15:25 larsrh int-e: I'm kinda surprised that this sublocale command works at all
15:25 larsrh given that it introduces a cyclic locale relationship
15:27 int-e well, cycles are supported (You can show two locales A and B to be equivalent by establishing A < B and B < A...)
15:28 int-e (which one reason why I actually use the subset symbol instead because < looks too strict)
15:29 larsrh eh ... then I must be reading the documentation wrong
15:30 int-e but *maybe* supporting such cycles is a reason for not making the demo.sym.useful_lemma available.
15:30 larsrh Hmmm ... maybe the sublocale command is actually very smart
15:30 larsrh The documentation says: "a cyclic interpretation that leads to an infinite chain ... is rejected"
15:31 larsrh But your interpretation doesn't actually lead to an infinite chain
15:31 larsrh I'm simultaneously scared and amazed by this.
15:33 int-e fun. sublocale sym: demo "Suc x" "Suc y" using o by (subst demo_def) simp  leads to an error: "Roundup bound exceeded (sublocale relation probably not terminating)."
15:34 int-e (oh there was no reason not to use unfold_locales there)
15:40 larsrh But to get back to your original question, I have no idea
15:40 larsrh My intuition would be that local theory updates would only get propagated when you leave a target
15:46 int-e yeah, apprently. I can also trigger this by a  lemma (in demo) ..., which is perhaps a bit nicer than explicitly leaving the context only to immediately enter it again
15:50 int-e okay, so basically the code seems to unfold the dependencies up to depth 120 (wow) and then gives up if the graph still isn't complete at that point.
15:52 int-e Oh of course... "roundup" means "rounding up" in the sense of "gathering" here.
17:22 dmiles joined #isabelle
23:03 silver joined #isabelle