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

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

**Follow-Ups**:**Re: [isabelle] About HOL BNF and inner syntax error***From:*Glauber Cabral

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

- Previous by Date: [isabelle] LaSh08: Last Call for Papers
- Next by Date: Re: [isabelle] About HOL BNF and inner syntax error
- Previous by Thread: [isabelle] About HOL BNF and inner syntax error
- Next by Thread: Re: [isabelle] About HOL BNF and inner syntax error
- 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