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