Email Gateway (Aug 22 2022 at 11:44): Email Gateway (Aug 22 2022 at 11:44):From: michel levy <michel.levy@imag.fr>
I am an french beginner in Isabelle. I prove (as an exercise) the
following lemma
lemma "∀ y. P y ⟹ P (f a)"
apply (erule_tac x="f a" in allE)
apply (assumption)
done
But why am I obliged to use x in instantiating the quantifier (x = "f a").
If I use y = "f a" to instantiate the quantifier, I have a message "no
such variable in theorem".
Email Gateway (Aug 22 2022 at 11:44):From: Lars Hupel <hupel@in.tum.de>
Dear Michel,
you can have a look at the theorem using the command "thm allE". The
system will print:
∀x. ?P x ⟹ (?P ?x ⟹ ?R) ⟹ ?R
As you can see, the theorem itself uses the variable "x". When
instantiating rules like "x1 = t1", "x2 = t2", ... the variables on the
left-hand side must occur in the theorem you're instantiating.
(I think this also answers your other question.)
Cheers
Lars
PS: Proof methods ending with "_tac" are considered "legacy" and should
only be used if you know what you're doing. If you're a beginner, I
would strongly recommend sticking to modern Isar-style proofs.
Email Gateway (Aug 22 2022 at 11:45):From: Lars Hupel <hupel@in.tum.de>
Hi,
I have started with the document tutorial.pdf which uses mainly
apply(method) in Chapter 5 to build proofs.
the tutorial, while still accurate, is somewhat outdated in some
respects. I recommend the newer book "Programming and Proving in
Isabelle/HOL":
<https://isabelle.in.tum.de/dist/Isabelle2015/doc/prog-prove.pdf>
1) type problem
lemma "⟦ALL y. P y ; Q b ⟧ ⟹ P a"
apply(erule_tac x="b" in allE)
variable 'b not of of sort type
I don't understand this message. Clearly my method is not leading to a
proof (I must choose x = "a").
But I don't understand why the instantiation of the schematic ?x by "b"
is rejected.
In Isabelle, types can have sorts. In almost all cases, at least the
sort "type" is required to do anything useful. Usually, this sort will
be automatically inserted by type inference. There are corner cases
though for which that doesn't work. You ran into one of these. According
to another thread on this list, this happens "if the type of a variable
is fully unconstrained"
(<https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2014-August/msg00166.html>).
2) representation of natural deduction in Isabelle
How the rule allI !!x. ?P x ==> !x. P x implements the proviso x not
free in the hypotheses of A in the rule A / !x. A
Clearly I have the same question for the rule exE.
I'm not quite sure whether this proviso is required for these rules in
Isabelle, since the variable "x" is still quantified in the premise.
There is however a primitive inference rule in the underlying proof
kernel which allows to generalize variables, and there, these checks
happen. But these rules are usually not exposed to the user.
Cheers
Lars
Last updated: Nov 21 2024 at 12:39 UTC