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 
inte 
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 reenter the context to get the symmetric version of a lemma I just proved... any ideas? 
15:13 
inte 
(the paste is a toy example but I have a serious application for this) 
15:25 
larsrh 
inte: I'm kinda surprised that this sublocale command works at all 
15:25 
larsrh 
given that it introduces a cyclic locale relationship 
15:27 
inte 
well, cycles are supported (You can show two locales A and B to be equivalent by establishing A < B and B < A...) 
15:28 
inte 
(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 
inte 
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 
inte 
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 
inte 
(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 
inte 
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 
inte 
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 
inte 
Oh of course... "roundup" means "rounding up" in the sense of "gathering" here. 
17:22 

dmiles joined #isabelle 
23:03 

silver joined #isabelle 