[isabelle] induction for mutually recursive functions



Hello,

I have the following mutually recursive function definition

function
  init_fun :: "nat => nat * nat * nat"
  and loop_fun :: "nat * nat * nat => nat * nat * nat"
  and final_fun :: "nat * nat * nat => nat * nat * nat"
  where
    "init_fun n = loop_fun (n, 0, 0)" |
    "loop_fun (n, k, s) = (if k < n then loop_fun (n, k + 1, s + k + 1)
                             else if k = n then final_fun (n, k, s)
                             else (n, k, s))"|

    "final_fun (n, k, s) = (n, k, s)"

by pat_completeness auto
termination
apply (relation "measure (% x. case x of Inl n => n + 3 | Inr (Inl (n, k, s)) => n - k + 2 | Inr (Inr (n, k, s)) => n - k + 1)")
  by auto

Asumming that Testa, Testb, Testc, and Test are defined I want to prove by
(mutual) induction:

theorem TestInduction:
  "Testa n ==>  Test (init_fun n)"
  "Testb n k s ==> Test (loop_fun (n, k, s))"
  "Testc n k s ==> Test (final_fun (n, k, s))"

If I try

apply (induct n and "(n, k, s)" and "(n, k, s)" rule: init_fun_loop_fun_final_fun.induct)

I get something that is unprovable:

1. [| [| na = n; 0 = k; 0 = s; Testb n k s|] ==> Test (loop_fun (n, k, s)); Testa na |] ==> Test (init_fun na)
2. ...
3. ...

I would expect something like:

1. [| [| Testb na 0 0|] ==> Test (loop_fun (na, 0, 0)); Testa na |] ==> Test (init_fun na)
2. ...
3. ...

that I can prove using the definition of the Test predicates.

Best regards,

Viorel Preoteasa










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