*To*: Viorel Preoteasa <viorel.preoteasa at abo.fi>*Subject*: Re: [isabelle] induction for mutually recursive functions*From*: Alexander Krauss <krauss at in.tum.de>*Date*: Wed, 07 Sep 2011 00:21:22 +0200*Cc*: USR Isabelle Mailinglist <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <4E64BBB3.2070104@abo.fi>*References*: <4E64BBB3.2070104@abo.fi>*User-agent*: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:1.9.1.16) Gecko/20101227 Icedove/3.0.11

Hi Viorel,

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.

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

by auto 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)"

Hope this helps... Alex

**Follow-Ups**:**Re: [isabelle] induction for mutually recursive functions***From:*Viorel Preoteasa

**References**:**[isabelle] induction for mutually recursive functions***From:*Viorel Preoteasa

- Previous by Date: Re: [isabelle] Scala Code Generation
- Next by Date: Re: [isabelle] induction for mutually recursive functions
- Previous by Thread: [isabelle] induction for mutually recursive functions
- Next by Thread: Re: [isabelle] induction for mutually recursive functions
- Cl-isabelle-users September 2011 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list