*To*: michel levy <michel.levy at imag.fr>*Subject*: Re: [isabelle] x is a special variable*From*: Lars Hupel <hupel at in.tum.de>*Date*: Wed, 14 Oct 2015 11:39:27 +0200*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <561D0181.8020805@imag.fr>*References*: <561BE0A0.9020005@imag.fr> <561CB496.6090304@in.tum.de> <561D0181.8020805@imag.fr>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:38.0) Gecko/20100101 Thunderbird/38.3.0

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

**References**:**[isabelle] x is a special variable***From:*michel levy

**Re: [isabelle] x is a special variable***From:*Lars Hupel

- Previous by Date: Re: [isabelle] sublocale problem
- Next by Date: Re: [isabelle] Code generation for reverse sorting
- Previous by Thread: Re: [isabelle] x is a special variable
- Next by Thread: [isabelle] sublocale problem
- Cl-isabelle-users October 2015 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list