Re: [isabelle] Induction rule for partial_function (tailrec)



Hi Andreas,

On 03/13/2013 08:37 AM, Andreas Lochbihler wrote:
Every now and then, I want to prove that a function that I have defined
with partial_function (tailrec) is undefined when the recursion does not
terminate. Unfortunately, partial_function (tailrec) does not generate
an induction theorem for the functions. So I set out to prove my own
generic induction rule (fixp_induct_tailrec_undefined in the attachment)
similar to fixp_induct_option in Partial_Function.thy. If I manually
instantiate it with the ..._def theorem of the partial function ...,
everything works fine. However, when I register it as the induction
theorem to be used for tailrec (like it is done for fixp_induct_option
and option in Partial_Function.thy), I only get exceptions when using
partial_function.

What's wrong with my induction theorem? How can I change it such that it
works with partial_function?

partial_function currently expects induction rules whose conclusion is of the form "... ==> P x y" where ... intuitively means "f x terminates and evaluates to y". In the option monad, this is simply "f x = Some y ==> P x y", but in the degenerate tailrec monad you would get something like "f x = y ==> y ~= undefined ==> P x y".

I just tried this and got the following rule accepted by partial_function.

lemma fixp_induct_tailrec_undefined:
  fixes F :: "'c ⇒ 'c" and
    U :: "'c ⇒ 'b ⇒ 'a" and
    C :: "('b ⇒ 'a) ⇒ 'c" and
    P :: "'b ⇒ 'a ⇒ bool" and
    x :: "'b"
  assumes mono: "⋀x. mono_tailrec (λf. U (F (C f)) x)"
assumes eq: "f ≡ C (ccpo.fixp (fun_lub (flat_lub undefined)) (fun_ord tailrec_ord) (λf. U (F (C f))))"
  assumes inverse2: "⋀f. U (C f) = f"
assumes step: "⋀f x y. (⋀x y. U f x = y ⟹ y ≠ undefined ⟹ P x y) ⟹ U (F f) x = y ⟹ y ≠ undefined ⟹ P x y"
  assumes result: "U f x = y"
  assumes defined: "y ≠ undefined"
  shows "P x y"
  sorry

I believe this rule should be provable and sufficient for what you want.

I cannot say on the spot whether partial_function could be modified to accept rules like yours. The problem is the curry/uncurry translation, which must do some explicit instantiations and assumes a certain syntactic form.

Let me know when you make progress (or run into more problems).

Alex





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.