*To*: Amy Furniss <mjf29 at leicester.ac.uk>*Subject*: Re: [isabelle] Completeness of patterns for mutually recursive function definitions*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Wed, 13 Mar 2013 13:31:31 +0100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <513F378E.7020105@le.ac.uk>*References*: <513F378E.7020105@le.ac.uk>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:17.0) Gecko/20130221 Thunderbird/17.0.3

Hi Amy,

apply(unfold regular1_def regular2_def) apply(atomize_elim) apply(case_tac x) (* new *) apply(auto)

the following solves all of them: apply(auto simp add: fun_eq_iff intro: arg_cong) Hope this helps, Andreas On 12/03/13 15:11, Amy Furniss wrote:

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**:

**References**:

- Previous by Date: [isabelle] Induction rule for partial_function (tailrec)
- Next by Date: Re: [isabelle] Completeness of patterns for mutually recursive function definitions
- Previous by Thread: [isabelle] Completeness of patterns for mutually recursive function definitions
- 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