Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2016-05-17

| Channels | #isabelle index | Today | | Search | Google Search | Plain-Text | summary

All times shown according to UTC.

Time Nick Message
00:42 wagle joined #isabelle
01:00 tangentstorm andromeda-galaxy: there's a search feature built in, yes. i'm afraid i don't remember how to invoke it.
01:01 andromeda-galaxy tangentstorm: thanks; I saw documentation for how to do it in proof general in the tutorial, but can't figure out how to do it in JEdit
01:01 tangentstorm lemme see
01:06 tangentstorm find_theorems name: "*"
01:06 tangentstorm ^ lists all theorems
01:06 tangentstorm well it lists about 40 theorems out of all theorems
01:07 tangentstorm see find_theorems in the isar ref for more things you can search on
01:08 andromeda-galaxy tangentstorm: great, thanks! I don't know how I missed that
01:09 andromeda-galaxy by the way: when using the Haskell codegen, what do I need to do to get Show instances for the generated types?
01:19 tangentstorm try:   export_code in Haskell(string_classes)
01:21 andromeda-galaxy tangentstorm: thanks!  how should I go about finding that sort of thing in the future?  I've tried searching through codegen but couldn't find it anywhere
01:22 andromeda-galaxy (hmm, that reuslts in command expected but module_name found)
01:23 tangentstorm i have never used codegen either, but i searched for it on google and found a reference to string_classes.. then searched for that in the isar_ref and tried to decipher how to use it from the syntax diagram. :/
01:24 tangentstorm there is a mailing list discussion that suggests it might not work very well. i think it's only intended for simple record types.
01:25 andromeda-galaxy tangentstorm: okay, I'll try to do that more in the future.  Since I haven't been using isabelle much for long, I wonder if part of it is that my google filter buble is more focused on haskell/etc, questions and misses isabelle resources occasionally
01:26 tangentstorm i just searched for "isabelle haskell Show" on google
01:27 andromeda-galaxy tangentstorm: that's so weird!  I don't get anything including string_classes!
01:27 andromeda-galaxy not even for more targeted queries like "isabelle codegen deriving (Show)"
01:28 tangentstorm there's also this http://www.isa-afp.org/entries/Show.shtml
01:28 tangentstorm sorry i searched for "isabelle haskell deriving show"
01:28 tangentstorm it was in one of the list discussions
01:30 andromeda-galaxy still nothing, all I get is stuff like the afp link above (about reimplimenting something similar in Isabelle).  I'll see if my Google searches start returning better targeted results soon
01:31 tangentstorm you could try adding site: lists.cam.ac.uk
03:23 andromeda-galaxy tangentstorm: sorry I missed you, thanks for the hint
05:56 ThreeOfEight Isabelle/jEdit also has a search panel
05:57 ThreeOfEight unlike Hoogle, that only works when you've loaded and imported the theories in question.
05:57 ThreeOfEight Isabelle's module system is really, really bad. But at least it now has private/qualified modifiers.
06:08 ammbauer ThreeOfEight: What? How? Where?
06:10 ThreeOfEight ammbauer: referring to what?
06:33 ammbauer ThreeOfEight: private/qualified imports
06:35 ThreeOfEight that's been around since Isabelle 2015
06:35 ThreeOfEight context
06:35 ThreeOfEight begin
06:36 ThreeOfEight private lemma "P"
06:36 ThreeOfEight end
06:36 ThreeOfEight and then it's gone
06:36 ThreeOfEight You need an anonymous context surrounding it though
06:36 ThreeOfEight Which is a bit strange.
06:36 ThreeOfEight In the good ol' days, you would just do "hide_fact foo" afterwards and that also did the trick.
06:37 ThreeOfEight Isabelle really is in dire need of a proper module system though, but that's going to take a while.
06:37 ammbauer ahh, i thought you could do "import Main as Maine"
06:45 ThreeOfEight …no
06:45 ThreeOfEight Oh God no that would break so many things.
08:13 fracting joined #isabelle
10:11 larsrh ThreeOfEight: could you try this please? find_theorems name: induct length
10:21 mal`` joined #isabelle
10:56 mal`` joined #isabelle
13:59 fracting joined #isabelle
17:15 relrod_ joined #isabelle
17:15 relrod_ joined #isabelle
17:37 fracting joined #isabelle
18:07 ilbot3 joined #isabelle
18:07 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/
20:24 andromeda-galaxy Is using sledgehammer to try to get more intuition about how "close" two statements need to be to be provable in one step in Isar a bad idea?
20:35 larsrh No, that sounds reasonable
20:39 andromeda-galaxy larsrh: great!  I'm having some trouble figuring out what the overwhelming attitude towards sledgehammer is, so I wasn't sure
20:39 andromeda-galaxy (by the way: what's the best way to use induction to prove things about a function implemented with fold(l)?  List.fold(l)
20:39 andromeda-galaxy _append seems like the only thing that (might) let you use an induction hypothesis
20:41 int-e just use normal induction on the second argument (list.induct)?
20:42 andromeda-galaxy int-e: when doing that, I'm having trouble getting the foldl ... expression rewritten in such a way that I can use the induction hypothesis
20:42 int-e err, third argument.
20:42 andromeda-galaxy because, e.g., foldl_cons results in a new foldl with a different initial "base" value
20:49 int-e sounds like you need to use 'arbitrary'. for example: lemma "foldl (λa b. a + b) c xs = (c + listsum xs :: 'a :: comm_monoid_add)" by (induct xs arbitrary: c) (simp_all add: ac_simps)
20:50 int-e oh that doesn't need to be a commutative monoid; any monoid will work.
20:50 int-e but that wasn't the point.
20:51 int-e note the abritrary: c... that will allow using the induction hypothesis with c + x instead of c, where x is the first element of the list.
20:52 andromeda-galaxy int-e: I tried using arbitrary before, but now I realise that that's just because of the particular lemma that I was proving (where knowing what the "base" is happens to be really important to the proof of the empty case)
20:52 andromeda-galaxy thanks anyway!
20:52 andromeda-galaxy I'll try that again ,as well as foldl
20:52 andromeda-galaxy _append
21:41 andromeda-galaxy on further reflection, it makes sense that list induction isn't working here, I'm just not sure what would.  As an exercise, I'm currently trying to prove that given a delay automaton does in fact delay; the foldl is folding a transition function across a list of inputs, and the base value is "current state x outputs so far".  Since the current state is in there, and the state affects what happens next, I
21:41 andromeda-galaxy can't make it arbitrary...
21:42 andromeda-galaxy maybe inducting on (rev xs) would work?

| Channels | #isabelle index | Today | | Search | Google Search | Plain-Text | summary