[isabelle] clashes in _graph names generated by mutual recursion



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




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.