Stream: Archive Mirror: Isabelle Users Mailing List

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

Email Gateway (Aug 18 2022 at 12:11):

From: Glauber Cabral <glauber.sp@gmail.com>
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.

Email Gateway (Aug 18 2022 at 12:12):

From: Tjark Weber <tjark.weber@gmx.de>
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

Email Gateway (Aug 18 2022 at 12:12):

From: Glauber Cabral <glauber.sp@gmail.com>
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

Last updated: Nov 21 2024 at 12:39 UTC