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? 