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

All times shown according to UTC.

Time Nick Message
00:27 JCaesar AnthonyWeis: Because you can write hence "P x" for x.
00:29 JCaesar Also, I'm not sure what happens to foo[of …] instantiations with foo: "∀x. P x ==> ⋀x. P x"
01:48 ilbot3 joined #isabelle
01:48 Topic for #isabelle is now Official channel for the Isabelle/HOL theorem prover: http://www.cl.cam.ac.uk/research/hvg/Isabelle/index.html || Now with logging: http://irclog.perlgeek.de/isabelle/
02:01 AnthonyWeis ok just to be sure I understand correctly
02:01 AnthonyWeis are all variables implicitely "fixed" variables ?
02:03 AnthonyWeis but I thought the convention is that these varaibles are implicitely all quantified ....
02:05 AnthonyWeis and what exactly is the difference between a fixed and a free variable ?
02:07 JCaesar no, there di
02:08 JCaesar s/di/definitely are free variables/
02:36 AnthonyWeis sorry for asking , but what does "di" and "s/di/" mean ?
08:20 larsrh JCaesar  had a typo :-)
08:21 larsrh what he meant to say was "no, there definitely are free variables"
08:21 larsrh So the full story about variables in Isabelle is a little bit tricky
08:21 larsrh the general theme is: _outside_ of a proof, e.g. in a lemma statement, free variables are implicitly universally quantified
08:22 larsrh that is, if you write lemma "P x", and P is a constant, then x is assumed to be quantified
08:22 larsrh the two statements lemma "P x" and lemma "\And x. P x" are equivalent
08:22 larsrh we prefer to avoid explicit quantification because of that
08:22 larsrh of course, sometimes you need to quantify explicitly in an assumption
08:23 larsrh e.g. if you want to assume that a function f is commutative
08:23 larsrh then you'd write lemma assumes "\And x y. f x y = f y x" shows "something about f"
08:23 larsrh furthermore, you'd try to avoid HOL quantification and favour Pure quantification
08:24 larsrh HOL quantification is the upside-down A, wheras Pure quantification is the big vee
08:24 larsrh in lemma statements and inductive definitions, you can always use Pure quantification
08:24 larsrh in function definitions you sometimes need to use HOL quantification
08:25 larsrh now, inside proofs, any variable that is implicitly quantified outside turns into a fixed variable inside
08:25 larsrh lemma "P x"
08:25 larsrh proof
08:25 larsrh fix x
08:25 larsrh show "P x" ...
08:25 larsrh qed
08:25 larsrh if you forget to fix something inside the system will give the variable a funny highlighting
08:26 larsrh --> long story short: you can express quantification with language elements from Isabelle, hence there is usually little need to quantify manually
08:26 larsrh AnthonyWeis: see above for an attempt at an explanation
08:54 JCaesar oh, there's also the apply style argument for not explicitly quantifying. if you have "P x" and do apply(rule foo[of x]), that works, but if you have "⋀x. P x", it won't.
08:56 JCaesar (there is rule_tac x in foo instead of rule foo[of x] for the explicit variant, but oh, come on. You probably want to avoid this kind of thing in an isar-proof anyway.)
10:38 silver joined #isabelle
11:17 AnthonyWeis ok, first of all, thank you all very much :)
11:17 AnthonyWeis but I am still a bit confused
11:18 AnthonyWeis because I thought that Pure all quantification is the same as "fixing" a variable
11:19 AnthonyWeis for example when I have a look at the rule exE (existential elimination, isabelle tells me it works like this:
11:19 AnthonyWeis ∃x. ?P x ⟹ (⋀x. ?P x ⟹ ?Q) ⟹ ?Q
11:21 AnthonyWeis \exists . ?P x ==> (\And x. ?P x ==> ?Q) ==> ?Q   (in case unicode doesn't work for anyone of you)
11:22 AnthonyWeis but I usually fix the "x"  (the one in the brackets)
11:23 AnthonyWeis so when I use existential elimination I write something along those lines :
11:27 AnthonyWeis assume a:"∃x .P x"
11:27 AnthonyWeis {
11:27 AnthonyWeis fix x
11:27 AnthonyWeis assume "P x"
11:27 AnthonyWeis hence result sorry
11:27 AnthonyWeis }
11:27 AnthonyWeis with a have result by (rule exE)
11:30 larsrh yes, that's correct
11:30 larsrh but that's not the way you'd write it in Isar, usually