Re: [isabelle] Specification depends on extra type variables


On 26/03/2010, at 11:49 PM, Viorel Preoteasa wrote:

> definition
> f :: "'a => ('b itself) => bool" where
> "f a x = (?g . !u . g (u::'b) = a)";
> However like this I have to use x as parameter for f everywhere.
> Moreover, I am defining Hoare triples for some kind of programs,
> and I want to use the syntax "|- _ {| _ |} _", but with this approach
> I need a place for the extra dummy parameter also.
> The fact is that the type 'b must be a type variable. I cannot instantiate it
> at this point.

Can I suggest you look into locales?

locale L =
  fixes unused_x :: "'b"

  "f a = (?g. !u. g (u::'b) = a)"


(untested, but I can expand on this if you think it might be a profitable approach.)

You can later instantiate 'b with a sublocale or interpretation command.



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