Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Quantifying over types

view this post on Zulip Email Gateway (Aug 18 2022 at 15:03):

From: Steve W <s.wong.731@googlemail.com>
Hi,

I was wondering why the type of 'func' needs to be be declared in lem1 and
not in lem2.

consts
s :: real
f :: real
F :: "real => real"
Y :: "real => real"
Z :: "real => real"

axioms
ax1 : "F t = Y t + Z t"
ax2 : "Y s = -1"
ax3 : "Z s = 1"
ax4 : "Y f = -1"
ax5 : "Z f = -1"

lemma lem1: "EX func t. func t = 0"
proof -
have "F s = 0"
using ax1 ax2 ax3
by auto
show ?thesis
by auto
qed

That's fine (even without declaring the types of func in the lemma). But
with:

lemma lem2: "EX func t. func t =/ 0"
proof -
have "F f =/ 0"
using ax1 ax4 ax5
by auto
show ?thesis
by auto

Auto cannot solve ?thesis with "F f =/ 0" in lem2 while it can solve the
thesis in lem1 with "F s = 0". It works in lem2 if the lemma was "EX
(func::real=>real) t. func t =/ 0". How come the type of func needs to be
declared in lem2 but not in lem1? Can type be existentially quantified in
some way?

Thanks
Steve

view this post on Zulip Email Gateway (Aug 18 2022 at 15:03):

From: Tobias Nipkow <nipkow@in.tum.de>
Steve W wrote:

Hi,

I was wondering why the type of 'func' needs to be be declared in lem1 and
not in lem2.

consts
s :: real
f :: real
F :: "real => real"
Y :: "real => real"
Z :: "real => real"

axioms
ax1 : "F t = Y t + Z t"
ax2 : "Y s = -1"
ax3 : "Z s = 1"
ax4 : "Y f = -1"
ax5 : "Z f = -1"

lemma lem1: "EX func t. func t = 0"
proof -
have "F s = 0"
using ax1 ax2 ax3
by auto
show ?thesis
by auto
qed

The "F s = 0" refers to type real and contributes nothing to the proof
of ?thesis, which talks about a 0 of some arbitrary type (displayed as
"0::'b"). This thesis is simple enough that auto can solve it (probably
by func = %x. x" and t = 0) but that is more a coincidence.

Auto cannot solve ?thesis with "F f =/ 0" in lem2 while it can solve the
thesis in lem1 with "F s = 0". It works in lem2 if the lemma was "EX
(func::real=>real) t. func t =/ 0". How come the type of func needs to be
declared in lem2 but not in lem1? Can type be existentially quantified in
some way?

No.

Tobias

view this post on Zulip Email Gateway (Aug 18 2022 at 15:04):

From: Tobias Nipkow <nipkow@in.tum.de>

lemma lem1: "EX func t. func t = 0"

This lemma is not true because the the result type of func could be a
one-lement type. The "refute" command finds that counterexample.

Tobias

proof -
have "F s = 0"
using ax1 ax2 ax3
by auto
show ?thesis
by auto
qed

That's fine (even without declaring the types of func in the lemma). But
with:

lemma lem2: "EX func t. func t =/ 0"
proof -
have "F f =/ 0"
using ax1 ax4 ax5
by auto
show ?thesis
by auto

Auto cannot solve ?thesis with "F f =/ 0" in lem2 while it can solve the
thesis in lem1 with "F s = 0". It works in lem2 if the lemma was "EX
(func::real=>real) t. func t =/ 0". How come the type of func needs to be
declared in lem2 but not in lem1? Can type be existentially quantified in
some way?

Thanks
Steve

view this post on Zulip Email Gateway (Aug 18 2022 at 15:04):

From: Tobias Nipkow <nipkow@in.tum.de>
My apologies - I meant to write the "not true" comment under lem2, not lem1.

Tobias

Tobias Nipkow wrote:

Last updated: Apr 19 2024 at 12:27 UTC