Function induction rules

[Kha]

For recursive functions, especially ones that are not trivially structurally recursive, we want to automatically generate induction rules that reflect the function's recursion structure so that proofs over the function do not have to reconstruct this structure manually. For reference, see Sections 2.2 & 5.1 of https://isabelle.in.tum.de/doc/functions.pdf for how this works in Isabelle.