Email Gateway (Oct 15 2020 at 21:17): Email Gateway (Oct 15 2020 at 21:17):From: "Fernandez, Matthew" <matthew.fernandez@intel.com>
Hello Isabelle experts,
Consider the following (admittedly silly) definition of two pairs of mutually recursive functions. Either is fine on its own, but they can not be admitted together. The problem is that various generated things derive their names from the mangling <fun1>_<fun2>. E.g. foo_bar_baz.pinduct. I think the core one is foo_bar_baz_graph, which is identified in error messages.
My question is, is the user simply not supposed to write such things? This came up in the context of a generated Isabelle theory. I am thinking about how much I need to teach the generator in order for it to produce output that has a chance of being accepted by Isabelle.
function foo_bar :: "nat ⇒ bool" and baz :: "nat ⇒ bool" where
"foo_bar 0 = True"
| "foo_bar (Suc n) = baz n"
| "baz 0 = False"
| "baz (Suc n) = foo_bar n"
by pat_completeness auto
function foo :: "nat ⇒ bool" and bar_baz :: "nat ⇒ bool" where
"foo 0 = True"
| "foo (Suc n) = bar_baz n"
| "bar_baz 0 = False"
| "bar_baz (Suc n) = foo n"
by pat_completeness auto
Thanks,
Matt
Last updated: Jan 04 2025 at 20:18 UTC