In my theory, I work with partial functions. To prevent writing
the in some code (readability), I experimented with using
defines to make use of total and partial functions.
This approach worked quite well, but now I encountered a problem when trying to specialize a locale. The following example shows such a case:
abbreviation totalize :: "('a ⇀ 'b) ⇒ 'a ⇒ 'b" where "totalize f a ≡ the (f a)" locale A = fixes a :: "'a set" assumes "finite a" locale B = A: A a + B: A b for a :: "'a set" and b :: "'b set" + fixes f :: "'a ⇀ 'b" and f' :: "'a ⇒ 'b" defines f_def: "f' ≡ totalize f" locale C = B a b "λe. if e ∈ a then Some e else None" id for a b
locale C is rejected with the following error message:
Bad head of lhs: existing constant "id" The error(s) above occurred in definition: "id ≡ λaa. totalize (If (aa ∈ a) (Some aa)) None"
The same "problem"\limitation was reported in 2015 https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2015-August/msg00030.html
Is there any known workaround?
I don’t know understand right now what the precise problem is, let alone whether there’s a workaround for it, but I would argue that generally
id doesn’t fulfill the relevant axiom anyhow.
The representation of the partial function as a total function must use
the None as the result for all arguments that don’t belong to the domain. However,
id uses the arguments as the results. The point is that you’re not free to choose what to return for arguments outside the domain. While you don’t know what value
the None really is, you’re still forced to pick this particular, unknown value.
This restriction is important: If you were free to let the total function have any results for the arguments outside the domain, for example, by replacing the
defines declaration with a
fixes declaration that just insists that the partial and total versions coincide on the domain, then, by choosing different results for the same arguments outside the domain, you could distinguish different interpretations that should morally be the same.
Therefore, my suggestion is: Just use
totalize in the declaration of
C as well.
Thank you Wolfgang for your support :)
The problem still remains:
locale C = B a b "λe. if e ∈ a then Some e else None" "totalize (λe. if e ∈ a then Some e else None)" for a b
will result in the following error:
Bad head of lhs: "λaa. totalize (If (aa ∈ a) (Some aa)) None" The error(s) above occurred in definition: "λaa. totalize (If (aa ∈ a) (Some aa)) None ≡ λaa. totalize (If (aa ∈ a) (Some aa)) None"
Weird. It seems as if
totalize is applied to a partial application of
If instead of the function it is actually applied to, as if the
totalized is pushed under the
Last updated: Dec 07 2023 at 20:16 UTC