 # Membership function

For a strictly increasing total natural number function, we can always determine whether some number is in its image. Here's the function that allows you to do that, written in a very general way:

Let $$f$$ be a strictly increasing total natural number function. Let $$P$$ and $$Q$$ be total predicates, such that

\begin{align} & P(x, y) = \begin{cases} P(x + 1, y) & \text{if }f(x) < y \\ f(x) = y & \text{otherwise} \end{cases} \\[1em] & Q(y) = P(0, y) \end{align}

Then $$Q$$ also satisfies

$$Q(y) \longleftrightarrow \exists x : f(x) = y$$

As an example, suppose $$f(x) = 2x.$$ Then $$Q(y),$$ would be true whenever $$y$$ is even.

theory Scratch imports Main begin

(* Locale *)

locale loc =
fixes f :: "nat ⇒ nat"
assumes assm: "f x < f (Suc x)"
begin

function P :: "nat ⇒ nat ⇒ bool" where
"P x y = (if f x < y then P (Suc x) y else f x = y)"
apply auto
done

termination P
apply (relation "measure (λ(x, y). y - f x)")
apply simp
apply auto
apply (rule diff_less_mono2)
apply (rule assm)
apply assumption
done

fun Q :: "nat ⇒ bool" where
"Q y = P 0 y"

end

(* Locale instantiation *)

fun f :: "nat ⇒ nat" where
"f x = x + 1"

global_interpretation interp: loc "f"
defines global_P = interp.P
and global_Q = interp.Q
apply unfold_locales
apply auto
done

value "map global_Q [0, 1, 2, 3, 4]"

end