prove_recursive_functions_exist : thm -> term -> thm
fn v1 ... (C1 vs1) ... vm = body1 /\ fn v1 ... (C2 vs2) ... vm = body2 /\ . . fn v1 ... (Cn vsn) ... vm = bodyn
`fn t1 ... v ... tm`
prove_recursive_functions_exist th ``;;
|- ?fn.
fn v1 ... (Ci vsi) ... vn
prove_recursive_functions_exist num_RECURSION `(prod f 0 = 1) /\ (!n. prod f (SUC n) = f(SUC n) * prod f n)`;; val it : thm = |- ?prod. prod f 0 = 1 /\ (!n. prod f (SUC n) = f (SUC n) * prod f n)