Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Notation for Pure.all may not work. Bug or fea...

Email Gateway (Aug 20 2020 at 10:27):

From: Georgy Dunaev <georgedunaev@gmail.com>
Dear all,

I'd like to report that in Isabelle/ZF session I noticed that this
definition is good:

definition PROPFALSE1 :: "prop"
where ‹PROPFALSE1 == Pure.all (%(P::o). Trueprop(P))›

and this is a bad definition:

definition PROPFALSE2 :: "prop"
where ‹PROPFALSE == (⋀P::o. (Trueprop(P)))›

While, I think, they should mean exactly the same.
Error message:

Type unification failed: Clash of types "prop" and "o"
Type error in application: incompatible operand type
Operator: Trueprop :: o ⇒ prop
Operand: P :: prop

I don't have an explanation of such behaviour, do you?

Sincerely Yours,
Georgy Dunaev

Email Gateway (Aug 20 2020 at 12:16):

From: Makarius <makarius@sketis.net>
On 20/08/2020 12:27, Georgy Dunaev wrote:

I'd like to report that in Isabelle/ZF session I noticed that this
definition is good:

definition PROPFALSE1 :: "prop"
where ‹PROPFALSE1 == Pure.all (%(P::o). Trueprop(P))›

and this is a bad definition:

definition PROPFALSE2 :: "prop"
where ‹PROPFALSE == (⋀P::o. (Trueprop(P)))›

While, I think, they should mean exactly the same.
Error message:

This is how to do it properly:

definition PROPFALSE1 :: "prop"
where ‹PROPFALSE1 ≡ Pure.all (λP::o. Trueprop(P))›

definition PROPFALSE2 :: "prop"
where ‹PROPFALSE2 ≡ (⋀P::o. P)›

I don't have an explanation of such behaviour, do you?

Logical syntax inserts the implicit Trueprop already (you can use PROP to
suppress that). The body of a quantification is logical syntax, but plain
application/abstraction of lambda calculus is not.

See also the isar-ref manual chapter 8, especially section 8.4.3 .

(Side-remark: "bug" and "feature" are both mostly equivalent and meaningless.
Complexity and confusion is something else.)

Makarius

Last updated: Apr 19 2024 at 01:05 UTC