Re: [isabelle] Types for variables
Thanks for that. I'm trying this at the moment:
A :: "[nat,int] => int"
B :: "[nat,int] => int"
C :: "[nat,int] => int"
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"
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"
I wasn't so lucky. How come it can't unify v with B x y + C x y? What more
do I need?
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
> > 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,
> > 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