# let eth = prove_general_recursive_function_exists
`?upto. !m n. upto m n =
if n < m then []
else if m = n then [n]
else CONS m (upto (m + 1) n)`;;
val eth : thm =
?(<<). WF (<<) /\ (!m n. (T /\ ~(n < m)) /\ ~(m = n) ==> m + 1,n << m,n)
|- ?upto. !m n.
upto m n =
(if n < m
then []
else if m = n then [n] else CONS m (upto (m + 1) n))
You can prove the condition by supplying an appropriate ordering, e.g.
# let wfth = prove(hd(hyp eth),
EXISTS_TAC `MEASURE (\(m:num,n:num). n - m)` THEN
REWRITE_TAC[WF_MEASURE; MEASURE] THEN ARITH_TAC);;
val wfth : thm =
|- ?(<<). WF (<<) /\ (!m n. (T /\ ~(n < m)) /\ ~(m = n) ==> m + 1,n << m,n)
and so get the pure existence theorem with