Re: [isabelle] Function Definitions Within Locales



On Tue, 2010-09-14 at 14:42 +0200, Makarius wrote:
> Here is an alternative version: since you have started with "indexed 
> syntax" already (a relatively old feature predating proper definitions 
> within locales) it can be done like this:
> 
> types
>    zone = "nat"
>    myregion = "zone set"
>    myfoo = "nat"
> 
> record 'e foo_rec =
>    zone_map :: "zone \<Rightarrow> 'e set" ("zmap\<index>")
>    foo_map :: "myfoo \<Rightarrow> 'e" ("fmap\<index>")
>    foo_habitat :: "myfoo \<Rightarrow> myregion" ("fhab\<index>")
> 
> fun myregion_map :: "('e, 'a) foo_rec_scheme => myregion \<Rightarrow> 'e 
> set" ("rmap\<index>")
>    where
>    "rmap\<^bsub>d\<^esub> r = (\<Union>z \<in> r. zmap\<^bsub>d\<^esub> z)"
> 
> locale foo =
>    fixes d :: "('e, 'a) foo_rec_scheme" (structure)
>    assumes mapped_foo_in_region: "(fmap f) \<in> rmap (fhab f)"

I see. Thank you very much indeed. This definitely fits my purpose.

Cheers,
---
Matej

Attachment: signature.asc
Description: This is a digitally signed message part



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