Time 
Nick 
Message 
12:32 

silver joined #isabelle 
15:12 

silver_ joined #isabelle 
16:06 

AnthonyWeis joined #isabelle 
16:43 
AnthonyWeis 
hi, sorry in advance for the newbie question 
16:43 
AnthonyWeis 
when I have something like this 
16:44 
AnthonyWeis 
assume "something" 
16:44 
AnthonyWeis 
hence "\And x . something" by simp 
16:45 
AnthonyWeis 
and I look at the simp trace 
16:46 
AnthonyWeis 
then the simp trace starts with "\And something ==> something2" and not as I would expect it with "something ==> (\And x. someting2)" 
16:47 
AnthonyWeis 
is this (always) a legit rule to put the "\And x." in front ? 
16:48 
AnthonyWeis 
what if there is already a free variable named "x" in "something" ? (I guess it just gets renamed automatically) 
16:49 
AnthonyWeis 
* hence "\And x . something2" not just "something" .... 
17:20 
pruvisto 
well, if you can show "P x" for a free variable x, then logically, that means that P holds for all x 
17:22 
pruvisto 
apart from that, it's a bit difficult to see what situation you are talkin gabout exactly 
17:47 
AnthonyWeis 
ok, it is something like this (\forall x . P x) ==> (\And x. P x) ... and in this case I guess it is no problem (because the x that belongs to the \forall shadows the fixed x) 
17:47 
AnthonyWeis 
I was just wondering if I missed something about the simplifier ... (like that I used it the wrong way 
17:48 
AnthonyWeis 
well actually I had it like this : 
17:48 
AnthonyWeis 
assume "(\forall x . P x)" 
17:48 
AnthonyWeis 
hence "(\And x. P x)" by simp 
17:49 
AnthonyWeis 
I know it is a dumb question ... sorry ^^ 
18:03 
pruvisto 
well, one normally doesn't write "\And x. P x" in Isar anyway 
18:04 
pruvisto 
the simplifier probably just descends under the "\And" and does its stuff there 
21:57 
AnthonyWeis 
"well, one normally doesn't write "\And x. P x" in Isar anyway"  why is that so ? 