[isabelle] About HOL BNF and inner syntax error



Hi everybody.

I'm really new to Isabelle. This is my second message to the list.
I've been using Isabelle to prove some HasCASL specifications and until now
I only had to use the Isar apply method.
I've already read the Isabelle Tutorial when I started working with the
tool.

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.

The motivation to get the BNF is this:
I have this axiom:
EqualTransT [rule_format] :
"ALL x.
 ALL y.
 ALL z. x ==' y = True' & y ==' z = True' --> x ==' z = True'"

And I need to prove this goal:
1. (!!(x (y z)).
        ([| ((x ==' y) = True'); ((y ==' z) = True');
            ((x <' z) = False');
            ((x ==' z) = False') |]
         ==> False))

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.

Even this lemma cannot pass:
lemma L1:
"ALL x.
 ALL z.
[| (x ==' z) = True'; (x ==' z) = False'|] ==> False"

So I guess I need some doc to learn the correct HOL inner syntax (I guess)
and I could not found it.

I'd be very thankful if you can give me some advices.

Thanks in advance,
Glauber.




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