## Stream: Beginner Questions

### Topic: Specialize locales incl. defines

#### Robert Soeldner (Nov 14 2021 at 11:01):

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
``````

Here, `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?

#### Wolfgang Jeltsch (Nov 14 2021 at 16:18):

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.

#### Robert Soeldner (Nov 14 2021 at 17:30):

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"
``````

#### Wolfgang Jeltsch (Nov 14 2021 at 17:43):

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