*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: [isabelle] Completeness of patterns for mutually recursive function definitions*From*: Amy Furniss <mjf29 at leicester.ac.uk>*Date*: Tue, 12 Mar 2013 14:11:26 +0000*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:17.0) Gecko/20130221 Thunderbird/17.0.3

Dear all, I have a pair of mutually-recursive functions which are defined using the function command, and I'm struggling to prove the completeness of patterns for the definition. If I remove one of the recursive calls (so that they are no longer mutually recursive) and separate out the functions, the completeness of patterns for both functions is easily solved by atomize_elim, auto, but when they are defined together this no longer works. Can anybody please suggest how I might go about solving this pattern completeness subgoal? Thanks, Amy --- theory Example imports Main begin datatype type1 = CON | ABS type2 type1 and type2 = FCON | FAPP type2 type1 definition regular1 :: "(type1 \<Rightarrow> type1) \<Rightarrow> bool" where "regular1 \<equiv> \<lambda>z. (z = (\<lambda>x. x)) | (z = (\<lambda>x. CON)) | (\<exists>f t. z = (\<lambda>x. ABS (t x) (f x)))" definition regular2:: "(type1 \<Rightarrow> type2) \<Rightarrow> bool" where "regular2 \<equiv> \<lambda>z. (z = (\<lambda>x. FCON)) | (\<exists>f t. z = (\<lambda>x. FAPP (t x) (f x)))" function fun1 :: "(type1 \<Rightarrow> type1) \<Rightarrow> type1" and fun2 :: "(type1 \<Rightarrow> type2) \<Rightarrow> type2" where "fun1 (\<lambda>x. x) = CON" | "fun1 (\<lambda>x. CON) = CON" | "fun1 (\<lambda>x. ABS (t x) (f x)) = ABS (fun2 t) (fun1 f)" | "\<not>regular1 i \<Longrightarrow> fun1 i = CON" | "fun2 (\<lambda>x. FCON) = FCON" | "fun2 (\<lambda>x. FAPP (t x) (f x)) = FAPP (fun2 t) (fun1 f)" | "\<not>regular2 i \<Longrightarrow> fun2 i = FCON" apply(unfold regular1_def regular2_def) apply(atomize_elim) apply(auto) sorry end

**Follow-Ups**:**Re: [isabelle] Completeness of patterns for mutually recursive function definitions***From:*Andreas Lochbihler

- Previous by Date: Re: [isabelle] Set notation for tuples broken
- Next by Date: [isabelle] Lifting a partial definition to a quotient type
- Previous by Thread: [isabelle] CfP PLMMS at CICM, July 2013, Bath, UK
- Next by Thread: Re: [isabelle] Completeness of patterns for mutually recursive function definitions
- Cl-isabelle-users March 2013 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