Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Types for variables

Email Gateway (Aug 18 2022 at 13:59):

From: John Munroe <munddr@googlemail.com>
Thanks for that. I'm trying this at the moment:

consts
A :: "[nat,int] => int"
B :: "[nat,int] => int"
C :: "[nat,int] => int"

axioms
ax: "A p t = B p t + C p t"

lemma lem1: "EX func x y.func x y = B x y + C x y"
using ax
by blast

It can infer the types of all func, x and y and blast resolves it. However,
if I change the LHS to a free variable:

lemma lem1: "EX func x y.func x y = v"
using ax
by blast

I wasn't so lucky. How come it can't unify v with B x y + C x y? What more
do I need?

Thanks again
John

Email Gateway (Aug 18 2022 at 14:00):

From: Peter Lammich <peter.lammich@uni-muenster.de>
John Munroe wrote:

Thanks for that. I'm trying this at the moment:

consts
A :: "[nat,int] => int"
B :: "[nat,int] => int"
C :: "[nat,int] => int"

axioms
ax: "A p t = B p t + C p t"

lemma lem1: "EX func x y.func x y = B x y + C x y"
using ax
by blast

It can infer the types of all func, x and y and blast resolves it. However,
if I change the LHS to a free variable:

lemma lem1: "EX func x y.func x y = v"
using ax
by blast

Have a look at the typing of your lemma (Switch on
Settings->Show-Types), it is: func::'a => 'b => 'c, x::'a, y::'b, v::'c.
As there are no type constraints specified, Isabelle infers the most
generic type. However,
your axiom ax only works for nat and int.

To solve your problem, you have to explicitely constrain the type of,
say, func:
EX (func::nat=>int=>int) x y. ...

However, your lemma means not what you seem to intend. The free variable
(v) will be implicitely universally quantified,
i.e. your lemma means that, for each v, there is a function func and
arguments x and y such that func x y = v.
To prove your lemma (even with the generic types), try e.g.

lemma lem2: "EX func x y. func x y = v"
apply (rule_tac x="%x y. v" in exI)
apply blast
done

This always works, because types in Isabelle are not empty, such there
is always some x and y that the function (%x y. v) can be applied to.

Regards,
Peter

I wasn't so lucky. How come it can't unify v with B x y + C x y? What more
do I need?

Thanks again
John

On Wed, Sep 2, 2009 at 10:03 AM, Peter Lammich <
peter.lammich@uni-muenster.de> wrote:

John Munroe wrote:

Hi,

I got a question about types for variables: can they have types? For
example, if I want to prove if a binary function that takes in a Natural

and

an Integer can be instantiated:

consts
F :: "[nat,int] => int"
axioms
ax: "F p t = G p t"

lemma lem1: "EX f.f x y = G p t"
using ax

Isabelle infers the type automatically to the most generic type in an
ML-like fashion.
You can constrain the type of any expression and variable by:
exp :: type, i.e.
EX f :: nat => int => int. f x y = G p t

the types of x and y are then inferred automatically to nat and int.
Usually you will have to put parenthesis around the type constraint, i.e.
EX f. f (x::nat) (y::int) = G p t

If you are unsure about the actual types, activate the option "Show
types" (In the Isabelle->Settings menu of PG)

Hope this helps,
Peter

where f should be typed (perhaps x and y as well).

Thanks very much
John

Email Gateway (Aug 18 2022 at 14:00):

From: Christian Doczkal <c.doczkal@stud.uni-saarland.de>
Hello

The free variable is to become a free/schematic variable of the theorem.
Hence its logically some arbitrary but fixed value which need not be
related to B and C.

On the other hand the claim is trivially true since there is the
constant v function (% is a lambda)

lemma lem2: "EX func x y. func x y = v"
apply (rule exI[where x="% x y . v"])
by simp
smime.p7s

Email Gateway (Aug 18 2022 at 14:06):

From: John Munroe <munddr@googlemail.com>
Hi,

I got a question about types for variables: can they have types? For
example, if I want to prove if a binary function that takes in a Natural and
an Integer can be instantiated:

consts
F :: "[nat,int] => int"
axioms
ax: "F p t = G p t"

lemma lem1: "EX f.f x y = G p t"
using ax

where f should be typed (perhaps x and y as well).

Thanks very much
John

Email Gateway (Aug 18 2022 at 14:07):

From: Peter Lammich <peter.lammich@uni-muenster.de>
John Munroe wrote:

Hi,

I got a question about types for variables: can they have types? For
example, if I want to prove if a binary function that takes in a Natural and
an Integer can be instantiated:

consts
F :: "[nat,int] => int"
axioms
ax: "F p t = G p t"

lemma lem1: "EX f.f x y = G p t"
using ax

Isabelle infers the type automatically to the most generic type in an
ML-like fashion.
You can constrain the type of any expression and variable by:
exp :: type, i.e.
EX f :: nat => int => int. f x y = G p t

the types of x and y are then inferred automatically to nat and int.
Usually you will have to put parenthesis around the type constraint, i.e.
EX f. f (x::nat) (y::int) = G p t

If you are unsure about the actual types, activate the option "Show
types" (In the Isabelle->Settings menu of PG)

Hope this helps,
Peter

where f should be typed (perhaps x and y as well).

Thanks very much
John

Last updated: Apr 23 2024 at 16:19 UTC