Re: [isabelle] Generating fresh type variables



Thanks Sascha and Christian,

I used "Variable.variant_fixes" and it worked great.

I had already used "Variable.variant_frees" for terms, but I hadn't realized 
it can also be used for types. If I understand correctly, type variables and 
term variables are in the same namespace (implicitly separated by the prefix 
"'") ?

By the way, thanks for the Isabelle Cookbook, it's really helpful to start 
with Isabelle/ML.

Mathieu

On 2011-06-29 at 16:27, Christian Urban wrote :
> Hi Mathieu,
> 
> There is also the related function Variable.variant_frees,
> which is explained in the Cookbook on page 16 with a
> small example about generating fresh names for Frees. ;o)
> 
> Hope this helps,
> Christian
> 
> Sascha Boehme writes:
>  > Hi Mathieu,
>  > 
>  > Concerning fresh names relative to a context have a look at the Isar
>  > implementation manual in Chapter 5, Section 1 (Variables), especially
>  > Variable.variant_fixes.  For more details, look into
>  > ~~/src/Pure/variable.ML.
>  > 
>  > Cheers,
>  > Sascha
>  > 
>  > Mathieu Giorgino wrote:
>  > > Hello all,
>  > > 
>  > > I'm basically new to the ML part of Isabelle.
>  > > 
>  > > I'm defining a ML function to automatically generate specifications of
>  > > an Isabelle function (these specifications are given as argument to
>  > > Function_Fun.add_fun). During the generation, I obtain terms
>  > > containing schematic type variables. I need to constrain (with sorts)
>  > > the types appearing in these specifications, and I also transform the
>  > > schematic type variables to type variables (I think I have to).
>  > > 
>  > > However when I use this function in a locale, my generated type
>  > > variables can be the same as the locale's one (and a type capture
>  > > occurs) which certainly means I'm doing something wrong. What is the
>  > > correct way to generate fresh type variables (TFree) ?
>  > > 
>  > > I've searched through the Isabelle Cookbook and the sources
>  > > (Pure/{type.ML,term.ML,Isar/*local*}) without any real clue. Have I to
>  > > collect type variables of current locale fixed terms and use
>  > > Name.variant ?
>  > > 
>  > > Thanks,
>  > > 
>  > > Mathieu




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