Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2016-01-18

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

All times shown according to UTC.

Time Nick Message
05:27 spacekitteh joined #isabelle
12:25 JCaesar Hmm, you know what would be nice for isar proofs? a command free_ih, that just introduces a fact fIH which is just the IH without its prems (and the obvious proof obligation.)
13:11 ThreeOfEight oh dear, there are several problems with this
13:11 ThreeOfEight the first one is: which IH?
13:12 ThreeOfEight there might be several
13:12 ThreeOfEight so, well, you could produce all of them, or allow the user to specify which
13:13 ThreeOfEight the next problem is that you can't really see what this fact is that you are proving just by looking at the Isar code
13:13 ThreeOfEight I think Makarius wants to avoid this kind of thing; the Isar proof should (ideally) be understandable without actually running Isabelle
13:13 ThreeOfEight if I am not mistaken
13:14 ThreeOfEight personally, what I would like the induction method to do is to just throw away the assumptions of the induction hypothesis that match any of the premises or chained facts
13:15 ThreeOfEight now you often get these annoying induction hypotheses with assumptions that are /literally/ in the premises
13:17 larsrh You mean, make induct even more complex?
13:17 larsrh ... as if it isn't doing enough already
19:58 JCaesar Hm. Can I somehow have a code_unfold that is applied only once? I'd like a lemma [code_unfold] "f p = (if P p then efficient_f p else f p)".
21:39 ThreeOfEight I don't think so
21:39 ThreeOfEight make two different constants, perhaps?

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