From: "Sanan Baena David Miguel (Dr)" <sanan@ntu.edu.sg>

Hi Isabelle users,

I am trying to evaluate definitions declared inside a locale, but I am getting errors saying that I am using terms that are not constructors. However, if I use abbreviations instead it works slightly better (details below).

In this very simple example

theory test

imports Main

begin

locale mytest =

fixes s1::"nat set"

fixes l1::"nat list"

begin

definition add::"nat ⇒ nat set"

where "add v ≡ insert v s1"

definition addl::"nat ⇒ nat list"

where "addl v ≡ v#l1"

abbreviation abbs::"nat ⇒ nat set"

where "abbs v ≡ insert v s1"

abbreviation abbl::"nat => nat list"

where "abbl ≡ insert v l1"

end

If I do an interpretation of mytest using numbers (1,2,3..) instead of 0 and Suc.

interpretation v: mytest "{0,1}" "[0,1]".

and I evaluate function add

value "v.addl 2"

I get

""Nat.one_nat_inst.one_nat" is not a constructor, on left hand side of equation, in theorem:

mytest.addl [zero_nat_inst.zero_nat, one_nat_inst.one_nat] ?v ≡

[?v, zero_nat_inst.zero_nat, one_nat_inst.one_nat]"

if I change the interpretation

interpretation v: mytest "{0,1}" "[0,Suc 0]".

then the evaluation of addl is correct.

However, it always fails when trying to evaluate "add" no matter whether the set is instantiated with numbers or with the natural number constructs.

interpretation v: mytest "{0,Suc 0}" "[0,Suc 0]".

gives the following error

"Set.insert" is not a constructor, on left hand side of equation, in theorem:

mytest.add

(insert zero_nat_inst.zero_nat

(insert (Suc zero_nat_inst.zero_nat) bot_set_inst.bot_set))

?v ≡

insert ?v

(insert zero_nat_inst.zero_nat

(insert (Suc zero_nat_inst.zero_nat) bot_set_inst.bot_set))

I am guessing that the problem here is that a set is an axiomatization and it doesn't have proper constructs.

If instead of using "definition" I use "abbreviation" for the declaration, it works then when using sets and instantiating the set by using 0 and Suc. If I use numbers, it doesn't evaluate the definition, it just gives the type. But at least it doesn't throw any error.

Is there any workaround for this?

Thank you very much!

Best regards,

David.

CONFIDENTIALITY: This email is intended solely for the person(s) named and may be confidential and/or privileged. If you are not the intended recipient, please delete it, notify us and do not copy, use, or disclose its contents.

Towards a sustainable earth: Print only when necessary. Thank you.

From: "Thiemann, René" <Rene.Thiemann@uibk.ac.at>

Hi David,

if you want executable of definitions inside a locale, you have to explicitly add code-equations outside the locale.

e.g., in your case

locale mytest = …

begin

…

definition addl = …

fun some_fun …

...

end

declare mytest.addl_def[code]

declare mytest.some_fun.simps[code]

interpretation v: mytest "{0,1}" "[0,1]" .

Then your execution will succeed.

value "v.addl 2”

Best,

René

From: "Sanan Baena David Miguel (Dr)" <sanan@ntu.edu.sg>

Thank you very much for your answer, René.

It works well by adding the code-equation outside of the locale.

But when adding assumptions to the locale like in

locale mytest =

fixes s1::"nat set"

fixes l1::"nat list"

assumes not_empty:"s1≠{}"

begin

definition add::"nat ⇒ nat set"

where "add v ≡ insert v s1"

definition addl::"nat ⇒ nat list"

where "addl v ≡ v#l1"

end

declare mytest.add_def[code]

the code-equation first warms:

Not an equation, in theorem:mytest ?s1.0 ⟹ mytest.add ?s1.0 ?v ≡ insert ?v ?s1.0

Which makes sense to me.

But then after doing the interpretation and trying to evaluate the definition I get again the same problem.

interpretation v:mytest "{1}" "[]"

apply unfold_locales by auto

value "v.add {1} 2"

Is there anything else that I am missing?

Thanks again!

David.

From: "YAMADA, Akihisa" <ayamada@trs.cm.is.nagoya-u.ac.jp>

Hi David,

locales with assumptions inserts the assumptions to all facts including

defining equations (when they are seen from outside the locale). One

trick is to declare a locale without assumptions, and then extend it

with assumptions.

locale pre_mytest =

fixes s1::"nat set"

fixes l1::"nat list"

begin

definition add::"nat ⇒ nat set"

where "add v ≡ insert v s1"

definition addl::"nat ⇒ nat list"

where "addl v ≡ v#l1"

end

declare pre_mytest.add_def[code]

locale mytest = pre_mytest +

assumes not_empty:"s1≠{}"

HTH,

Akihisa

From: "Sanan Baena David Miguel (Dr)" <sanan@ntu.edu.sg>

Thanks a lot Akihisa,

This does the trick, of course! (How I didn't think about that...)

David.

Last updated: Jul 15 2022 at 23:21 UTC