*To*: Peter Lammich <peter.lammich at uni-muenster.de>*Subject*: Re: [isabelle] Types for variables*From*: John Munroe <munddr at googlemail.com>*Date*: Wed, 2 Sep 2009 12:39:53 +0100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <4A9E34EF.9010801@uni-muenster.de>*References*: <e4d7be570909012125u67b7fc7n5a2c125e00aa6c57@mail.gmail.com> <4A9E34EF.9010801@uni-muenster.de>

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 > > > >

**Follow-Ups**:**Re: [isabelle] Types for variables***From:*Christian Doczkal

**Re: [isabelle] Types for variables***From:*Peter Lammich

**References**:**[isabelle] Types for variables***From:*John Munroe

**Re: [isabelle] Types for variables***From:*Peter Lammich

- Previous by Date: Re: [isabelle] Why do some abbreviations become "abbreviatees" inside locales?
- Next by Date: [isabelle] New AFP entry: Invertibility in Sequent Calculi by Peter Chapman
- Previous by Thread: Re: [isabelle] Types for variables
- Next by Thread: Re: [isabelle] Types for variables
- Cl-isabelle-users September 2009 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list