*To*: John Munroe <munddr at googlemail.com>*Subject*: Re: [isabelle] Types for variables*From*: Peter Lammich <peter.lammich at uni-muenster.de>*Date*: Thu, 03 Sep 2009 11:29:07 +0200*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <e4d7be570909020439p3f178de4sb94d331dfbb7794@mail.gmail.com>*References*: <e4d7be570909012125u67b7fc7n5a2c125e00aa6c57@mail.gmail.com> <4A9E34EF.9010801@uni-muenster.de> <e4d7be570909020439p3f178de4sb94d331dfbb7794@mail.gmail.com>*User-agent*: Thunderbird 2.0.0.22 (X11/20090605)

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

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

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

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

- Previous by Date: Re: [isabelle] Types for variables
- Next by Date: Re: [isabelle] Quick question about rule+
- Previous by Thread: Re: [isabelle] Types for variables
- Next by Thread: Re: [isabelle] Why do some abbreviations become "abbreviatees" inside locales?
- 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