Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] clashes in _graph names generated by mutual re...


view this post on Zulip 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: Mar 29 2024 at 12:28 UTC