Re: [isabelle] Types for variables



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






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