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 upsidedown 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 isarproof 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 
11:30 
larsrh 
instead: 
11:30 
larsrh 
assume a: "∃x .P x" 
11:30 
larsrh 
then obtain x where "P x" by (rule exE) 
11:30 
larsrh 
hence result sorry 
11:33 
AnthonyWeis 
ok. 
11:36 
AnthonyWeis 
but is my assumption that Pure all quantification and "fixing" is the same write or wrong ? because for me, it behaves like it is the same (at when I've proven stuff so far) 
11:36 
larsrh 
yes, your assumption is correct 
11:37 
AnthonyWeis 
ok thank you very much :) 
18:23 

silver joined #isabelle 
22:38 

dmiles joined #isabelle 