[isabelle] Function Definitions Within Locales



Hello all,

I hope you don't mind a question about locales:

Is it possible to provide function definitions within locales (before
the 'assumes' block)?

Some of my locale's assumptions refer to functions which need not be
locale parameters. I want to provide full definitions for such functions
within the locale (after the parameters and before the assumptions). See
example below:

========== A silly example ==========

types
  zone = "nat"
  myregion = "zone set"
  myfoo = "nat"

record 'e foo_rec =
  zone_map :: "zone ⇒ 'e set" ("zmapı _" [80] 70)
  foo_map :: "myfoo ⇒ 'e" ("fmapı _" [80] 70)
  foo_habitat :: "myfoo ⇒ myregion" ("fhabı _" [80] 70)

locale foo =
  fixes d :: "('e, 'a) foo_rec_scheme" (structure)

  (* Problem here: I want to say that a mapped 'foo' is an element
  of its habitat, but the 'rmap' function is not defined yet. *)
  assumes mapped_foo_in_region: "(fmap f) ∈ rmap (fhab f)"

begin

(* I would like this function to be just above 'assumes' -- to make
  it accessible within 'mapped_foo_in_region.' *)
fun myregion_map :: "myregion ⇒ 'e set" ("rmap _" [80] 70)
  where
  "myregion_map r = (⋃z ∈ r. zmap z)"

end

=====================================

Apologies if this has been answered before.

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.