Re: [isabelle] Types for variables



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

On Wed, Sep 2, 2009 at 10:03 AM, Peter Lammich <
peter.lammich at 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
> >
>
>




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