Stream: Beginner Questions

Topic: termination adding assumption

Bernhard Stöckl (Sep 27 2021 at 14:21):

I have a function like this where I can prove termination:

function to_dtree_aux :: "'a ⇒ ('a,'b) dtree" where
  "to_dtree_aux r = Node r (Abs_fset {(x,e).
    (if e ∈ out_arcs T r then x = to_dtree_aux (head T e) else False)})"

I would expect this to be equivalent to ("if P then Q else False" replaced by "P and Q"):

function to_dtree_aux :: "'a ⇒ ('a,'b) dtree" where
  "to_dtree_aux r = Node r (Abs_fset {(x,e).
    (e ∈ out_arcs T r ∧ x = to_dtree_aux (head T e))})"

But for the second function, I can't prove termination because the assumption e ∈ out_arcs T r is missing in the goal. Is there a better way to introduce this assumption than using a "if P then Q else False" construct?
The goals generated by apply(relation "measure (λr. Finite_Set.card {x. r →⇧*⇘T⇙ x})") look like this:

⋀r x xa. xa ∈ out_arcs T r ⟹ (head T xa, r) ∈ measure (λr. card {x. r →⇧*⇘T⇙ x})
⋀r x xa. (head T xa, r) ∈ measure (λr. card {x. r →⇧*⇘T⇙ x})

Last updated: Apr 25 2024 at 04:18 UTC