Email Gateway (Aug 22 2022 at 10:28): Email Gateway (Aug 22 2022 at 10:28):From: Christoph Dittmann <f-isabellelist@yozora.eu>
Hello,
is "context" and "in ..." supposed to be equivalent for function
definitions? When I use "in ..." to define a function with a
termination proof, I get "duplicate fact declaration" errors mentioning
a completely unrelated function (see the example below).
theory test imports Main begin
(* unrelated function, never mentioned below *)
fun foo :: "nat ⇒ nat" where "foo n = 0"
locale TestLocale
context TestLocale begin
(* works fine *)
function f :: "nat ⇒ nat"
where "f i = i" by auto
termination by lexicographic_order
end
(* breaks *)
function (in TestLocale) g :: "nat ⇒ nat"
where "g i = i" by auto
(* The next line produces:
Ignoring duplicate rewrite rule:
foo ?n1 ≡ 0
Duplicate fact declaration "test.foo.simps" vs. "test.foo.simps" *)
termination by lexicographic_order
end
Email Gateway (Aug 22 2022 at 10:29):From: Johannes Hölzl <hoelzl@in.tum.de>
"termination" looks at the last function definition in the current
context. As a solution to your problem you need to add (in TestLocale)
to termination:
function (in TestLocale) g :: "nat ⇒ nat"
where "g i = i" by auto
termination (in TestLocale) by lexicographic_order
works.
Email Gateway (Aug 22 2022 at 10:29):From: Tjark Weber <tjark.weber@it.uu.se>
FWIW, I stumbled over this before, and I still think it is a
misfeature.
Best,
Tjark
Email Gateway (Aug 22 2022 at 10:29):From: Christoph Dittmann <f-isabellelist@yozora.eu>
I see, now the behavior makes perfect sense.
Maybe it would be good to add this sentence to the documentation to help
new users avoid this pitfall? Apologies if it's already in there and I
missed it.
Thanks,
Christoph
Last updated: Apr 24 2024 at 20:16 UTC