*To*: "Tjark Weber" <tjark.weber at gmx.de>*Subject*: Re: [isabelle] About HOL BNF and inner syntax error*From*: "Glauber Cabral" <glauber.sp at gmail.com>*Date*: Wed, 16 Jul 2008 10:48:35 -0300*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <1216244594.3012.15.camel@weber>*References*: <deb09ce60807140731l1b142c71sde7e0c0bd99fd494@mail.gmail.com> <1216244594.3012.15.camel@weber>

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 > >

**References**:**[isabelle] About HOL BNF and inner syntax error***From:*Glauber Cabral

**Re: [isabelle] About HOL BNF and inner syntax error***From:*Tjark Weber

- Previous by Date: Re: [isabelle] About HOL BNF and inner syntax error
- Next by Date: [isabelle] WLPE'08 -- Call for Papers
- Previous by Thread: Re: [isabelle] About HOL BNF and inner syntax error
- Next by Thread: [isabelle] IJCAR in Australia, 1 month to go
- Cl-isabelle-users July 2008 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