Email Gateway (Mar 25 2021 at 09:23): 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.
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é
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.
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
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: Jul 15 2022 at 23:21 UTC