Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Evaluation of definitions defined inside a locale


view this post on Zulip Email Gateway (Mar 25 2021 at 09:23):

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.

view this post on Zulip Email Gateway (Mar 28 2021 at 17:41):

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é

view this post on Zulip Email Gateway (Mar 31 2021 at 04:57):

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.

view this post on Zulip Email Gateway (Mar 31 2021 at 05:18):

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

view this post on Zulip Email Gateway (Mar 31 2021 at 05:55):

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: Sep 25 2021 at 08:21 UTC