Re: [isabelle] About HOL BNF and inner syntax error



Hi Tjark.

I'll read thar doc again. I guess I hadn't understand that prop correctly
and I could understand the meta-logic error now.
Thanks for your explanation!

Glauber

On Wed, Jul 16, 2008 at 6:43 PM, Tjark Weber <tjark.weber at gmx.de> wrote:

> Glauber,
>
> On Mon, 2008-07-14 at 11:31 -0300, Glauber Cabral wrote:
> > Recently I was told that I need to create lemmas over an axiom to put the
> > last in such a way Isabelle can match it against the actual premises.
> > I've searched for a HOL BNF but I could not find it. I need to know what
> > exactly can be written in lemma/theorems, inside double quotes (the lemma
> > itself). I took a look in the logics-HOL.pdf but I didn't find the BNF,
> only
> > rules of the logic. As I'm not sure if I'm looking for HOL inner syntax
> or
> > Isar syntax, I had to ask you some help to find the right doc.
>
> http://isabelle.in.tum.de/dist/Isabelle/doc/logics-HOL.pdf contains a
> grammar in Figure 2.2.
>
> > I thought I should write some lemma as this one:
> > lemma L1:
> > "ALL x.
> >  ALL y.
> >  ALL z.
> > [| [|(x ==' y) = True' ; (y ==' z) = True'|] ==> (x ==' z) = True'; (x
> =='
> > z) = False'|]==> False"
> >
> > but I always get an inner syntax error and I cannot see where the error
> is.
>
> It is important to note the distinction between meta logic and object
> logic (i.e., HOL).  The meta logic uses type "prop" for propositions,
> whereas HOL uses type "bool".  There is a coercion from bool to prop
> (called "Trueprop", but usually implicit).  However, there is no
> coercion from prop to bool.  Therefore connectives of the meta logic
> (e.g., ==, ==>, !!) which yield type prop cannot occur nested below HOL
> connectives (e.g., =, -->, ALL).
>
> Also note that [| P; ...; Q |] ==> R is merely an abbreviation for
> P ==> (... ==> (Q ==> R)).
>
> Best,
> Tjark
>
>




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