# IRC log for #isabelle, 2017-02-22

All times shown according to UTC.

Time Nick Message
07:59 silver joined #isabelle
09:04 dmiles joined #isabelle
09:06 dmiles joined #isabelle
10:41 notdan I have a goal of the form [/\ x y . (/\ z . f x z = g x z ) ==> P(x,y,f,g)]
10:41 notdan I can do apply (drule ext) to replace the premise with (f x = g x), but I cannot apply (frule ext)
10:42 notdan and i was wondering why is that?
10:45 notdan I am also not being able to say apply (drule ext[of "\lambda z . f x z"]), presumably because x is universally quantified?
11:28 JCaesar I have no clue about the frule/drule thing, that's weird.
11:29 JCaesar but the second is likely because of how your variables are "quantified" (not sure that's the right way to say it.)
11:29 JCaesar try writing subgoal for x y, then you'll declare those two names as usable.
11:30 JCaesar (btw, you can also write drule ext[of "f x"] instead of ext[of "λz. f x z"])
11:32 JCaesar (if that subgoal-thing is a no-go, you can also do it the old way: apply(drule_tac f="f x" in ext), or you can also do it properly and start a new isar proof…)
13:29 pruvisto JCaesar: lemma "A ==> B" is fine
13:29 pruvisto have "A ==> B" used to be really strange in Isar and never did what you expected it to do
13:29 pruvisto Makarius changed that a while ago and now it's better
13:29 pruvisto but I still think that the "if" thing is preferable
13:32 JCaesar Hm, it's better if you do a proof cases or similar after. But if you have a proof(induction …), I don't see how the if holds any advantages…
14:01 pruvisto Yes I guess it makes little difference then
14:02 pruvisto as I said, I'm kind of still under the influence of the way things used to be in Isar
14:02 pruvisto and this used to be a really bad idea
16:13 notdan JCaesar: sorry, what do you mean by writing subgoal for x y?
16:13 JCaesar write litterally that.
16:13 JCaesar subgoal for x y apply(drule ext[of "f x"])
16:14 JCaesar (and observe how the status window changes.)
18:26 JCaesar notdan: got it?
18:36 notdan Sorry I was AFK.Let me try that
18:37 notdan So the quantified variables went from green to orange, that is nice
18:38 notdan and they are quantified no more
18:39 notdan It works, brilliant
18:39 notdan thanks JCaesar
18:39 notdan I am very much an Isabelle noob as you can guess
18:39 notdan frule still doesn't work tho
18:39 notdan :(
18:46 JCaesar I'm entirely puzzled about that…
18:46 notdan bbl changing trains
18:53 notdan well, anyway as I found out today, metis manages to solve my goal without explicitly mentioning funext