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



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.