Re: [isabelle] x is a special variable



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




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.