*To*: Andreas Lochbihler <andreas.lochbihler at kit.edu>*Subject*: Re: [isabelle] Locale import*From*: Clemens Ballarin <ballarin at in.tum.de>*Date*: Tue, 16 Feb 2010 20:41:36 +0100*Cc*: cl-isabelle-users <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <4B7963AB.6000206@kit.edu>*References*: <4B7963AB.6000206@kit.edu>*User-agent*: Internet Messaging Program (IMP) H3 (4.1.6)

Hi Andreas,

I want to import a locale A into a locale B such that one of A's parameters is replaced by a fixed parameter of B applied to an arbitrary value. Here's a short example what I would like to write: locale A = fixes f :: "'a" assume "f" locale B = A "g b" for g :: "'b => 'a" assumes ...

However, Isabelle complains at B's declaration that b is an illegal free variable. Adding b to the for clause is no solution to my problem, because this fixes b. I am currently doing the following: locale B = fixes g :: "'b => 'a" assumes A: "A (g b)" and ... sublocale B < A "g b" for b by(rule A) Although this works for the moment, I am not happy with this solution: I can only use definitions from A in the other assumptions of B via their full name with all parameters explicitly provided.

What is the best way to import A in B?

Since both declarations of B are "strange" this question is not well-defined.

Best regards, Clemens

**Follow-Ups**:**Re: [isabelle] Locale import***From:*Andreas Lochbihler

**References**:**[isabelle] Locale import***From:*Andreas Lochbihler

- Previous by Date: Re: [isabelle] relation composition
- Next by Date: [isabelle] Aqumacs Emacs fails to cut **.thy!
- Previous by Thread: [isabelle] Locale import
- Next by Thread: Re: [isabelle] Locale import
- Cl-isabelle-users February 2010 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list