*To*: Alexander Krauss <krauss at in.tum.de>*Subject*: Re: [isabelle] induction for mutually recursive functions*From*: Viorel Preoteasa <viorel.preoteasa at abo.fi>*Date*: Wed, 07 Sep 2011 11:30:41 +0300*Cc*: USR Isabelle Mailinglist <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <4E669CE2.3010509@in.tum.de>*References*: <4E64BBB3.2070104@abo.fi> <4E669CE2.3010509@in.tum.de>*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.6; rv:6.0) Gecko/20110812 Thunderbird/6.0

Hi Alex, That you for your message. Changing the function definition to the curried version helped. After this change I got the proof obligations that I expected. I managed already to prove the theorem by instantiating the induction theorems manually, but it was very cumbersome, and I needed to prove the same facts 3 times. Regarding my initial definition, it still does not seem provable. The conditions na = n; 0 = k; 0 = s cannot be discharged. If you look at the second subgoal, the situation is even worse because one would need to prove k = k+1. Maybe there is an error in applying the induction when the functions have tuples as parameters. Best regards, Viorel On 9/7/11 1:21 AM, Alexander Krauss wrote:

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 autoAsumming that Testa, Testb, Testc, and Test are defined I want toprove 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.The two versions are actually equivalent, so one should be provablewhen the other is. Unfortunately, the equation "na = n" seems to beoriented in an unfortunate way, such that the simplifier does not helpyou here...Note that here you are relying on a feature of the induct method to doinduction over non-variable terms, which introduces equations on thefly (which you already see in the simplified form; if you add(no_simp) after "induct", you see where they come from).You can avoid this situation altogether by using currying instead oftuple arguments in your function definition, which is generallyrecommended: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 terminationapply (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 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)"apply (induct n and n k s and n k s rule:init_fun_loop_fun_final_fun.induct)Hope this helps... Alex

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

**Re: [isabelle] induction for mutually recursive functions***From:*Alexander Krauss

- Previous by Date: Re: [isabelle] induction for mutually recursive functions
- Next by Date: [isabelle] termination of mutually recursive functions
- Previous by Thread: Re: [isabelle] induction for mutually recursive functions
- Next by Thread: [isabelle] strictness flags in Haskell code-generation
- 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