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 subgoalthing is a nogo, 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 