I have the following language of records:
datatype "term" = Rcd "string ⇀ term"
fun id_term :: "term ⇒ term"
where "id_term (Rcd vals) = Rcd (map_option id_term ∘ vals)"
This doesn't pass the termination checker, because the type's size function is constantly 0. I don't see how to provide a computable measure either without constraining the map to a finite domain.
So: How can I prove termination for the above definition? I suspect I have to prove well-foundedness for some inductive predicate over terms, but I'm not really sure how to do that.
For non-primitively-recursive functions, you can also use the function command, but things get a bit more complicated due to the fact that you don't have a size measure. Essentially, you have to define a subterm relation and show that it is well-founded, and then you can use that to show that your function terminates:
datatype "term" = Rcd "string ⇀ term"
inductive subterm :: "term ⇒ term ⇒ bool" where
"t ∈ ran f ⟹ subterm t (Rcd f)"
lemma accp_subterm: "Wellfounded.accp subterm t"
proof (induction t)
case (Rcd f)
have IH: "Wellfounded.accp subterm t" if "t ∈ ran f" for t
using Rcd[of "Some t" t] and that by (auto simp: eq_commute ran_def)
show ?case by (rule accpI) (auto intro: IH elim!: subterm.cases)
qed
definition subterm_rel where "subterm_rel = {(t, Rcd f) |f t. t ∈ ran f}"
lemma subterm_rel_altdef: "subterm_rel = {(s, t) |s t. subterm s t}"
by (auto simp: subterm_rel_def subterm.simps)
lemma subterm_relI [intro]: "t ∈ ran f ⟹ (t, Rcd f) ∈ subterm_rel"
by (simp add: subterm_rel_def)
lemma subterm_relI' [intro]: "Some t = f x ⟹ (t, Rcd f) ∈ subterm_rel"
by (auto simp: subterm_rel_def ran_def)
lemma wf_subterm_rel [simp, intro]: "wf subterm_rel"
using accp_subterm unfolding subterm_rel_altdef accp_eq_acc wf_acc_iff by simp
function id_term :: "term ⇒ term"
where "id_term (Rcd vals) = Rcd (map_option id_term ∘ vals)"
by pat_completeness simp_all
termination by (relation subterm_rel) auto