# IRC log for #isabelle, 2017-06-24

All times shown according to UTC.

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 ?