*To*: Stefan Berghofer <berghofe at in.tum.de>*Subject*: Re: [isabelle] primrec on nested mutually-recursive datatype*From*: Greg Bronevetsky <greg at bronevetsky.com>*Date*: Mon, 23 Jan 2006 18:11:11 -0500*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <43D51E64.50804@in.tum.de>*References*: <43C84BD7.7060301@bronevetsky.com> <43CB7BF4.7010100@in.tum.de> <43CC2203.9000603@bronevetsky.com> <43CFB0AF.2000204@in.tum.de> <43D0A06D.10603@bronevetsky.com> <43D51E64.50804@in.tum.de>*User-agent*: Mozilla Thunderbird 1.0 (Windows/20041206)

My datatype is as follows: datatype AppSrcStmt = skip | ifStmt nat "AppSrcOp list" "AppSrcOp list" | while nat "AppSrcOp list" and AppSrcOp = opTriple "FuncMark * TypeMark * AppSrcStmt" The size function created for this datatype is: size skip = 0 size (ifStmt ?nat ?list1.0 ?list2.0) = AppSrcOp_list_size1 ?list1.0 + AppSrcOp_list_size2 ?list2.0 + Suc 0 size (while ?nat ?list) = AppSrcOp_list_size3 ?list + Suc 0 size (opTriple ?x) = nat_nat_AppSrcStmt_x_x_size ?x + Suc 0 AppSrcOp_list_size1 [] = 0

AppSrcOp_list_size2 [] = 0

AppSrcOp_list_size3 [] = 0

nat_nat_AppSrcStmt_x_x_size (?nat, ?x) = nat_AppSrcStmt_x_size ?x + Suc 0 nat_AppSrcStmt_x_size (?nat, ?AppSrcStmt) = size ?AppSrcStmt + Suc 0 The core of function definition is as follows: consts func :: "(AppSrcOp list) => bool" recdef func "measure size" "func [] = True" "func (asOp # asList) = (case asOp of opTriple triple => (case (snd(snd triple)) of (ifStmt pv aTrue aFalse) => ((func aTrue) & (func aFals)) | (while pv aW) => (func aW) | _ => True) & (func asList) ) " This produces the following error from Isabelle: "*** recursion equations must use the = relation *** At command "recdef"."

When I comment out the ifStmt case and (func asList), Isabelle says: "*** Bad final proof state: *** ALL asList asOp nat pv.

*** 1. ALL asList asOp nat pv.

*** 1 unsolved goals! *** Proof failed! *** At command "recdef". "

datatype AppSrcStmt = skip | ifStmt nat "AppSrcStmt list" "AppSrcStmt list" | while nat "AppSrcStmt list" -- Greg Bronevetsky Stefan Berghofer wrote:

Greg Bronevetsky wrote:I've finally gotten the the point where I need to use the measurefunction to recdef a type. However, Isabelle wants me to prove that(ALL asOp. 0 < AppSrcOpSize asOp). Unfortunately, I don't know how toprove it. The most obvious proof is by structural induction but I'mtoo new to Isabelle to know how to specify that. Doing something assimple as "proof (induct asOp)" does not work since Isabelle says"*** Unable to figure out induct rule". What else can I do?You can only do induction on *free* variables. In your example, induction is actually overkill, since you can prove the above goal by a sequence of case distinctions followed by simplification: lemma "0 < AppSrcOpSize asOp" apply (case_tac asOp) apply (case_tac x) apply (case_tac b) apply (case_tac ba) apply simp_all doneBy the way, why don't you use the standard "size" funtion alreadyprovidedby the datatype package? Greetings, Stefan

**Follow-Ups**:**Re: [isabelle] primrec on nested mutually-recursive datatype***From:*Stefan Berghofer

**References**:**[isabelle] primrec on nested mutually-recursive datatype***From:*Greg Bronevetsky

**Re: [isabelle] primrec on nested mutually-recursive datatype***From:*Stefan Berghofer

**Re: [isabelle] primrec on nested mutually-recursive datatype***From:*Greg Bronevetsky

**Re: [isabelle] primrec on nested mutually-recursive datatype***From:*Stefan Berghofer

**Re: [isabelle] primrec on nested mutually-recursive datatype***From:*Greg Bronevetsky

**Re: [isabelle] primrec on nested mutually-recursive datatype***From:*Stefan Berghofer

- Previous by Date: [isabelle] FLoC'06 - Call for Papers
- Next by Date: [isabelle] ARW'06 Final CFP
- Previous by Thread: Re: [isabelle] primrec on nested mutually-recursive datatype
- Next by Thread: Re: [isabelle] primrec on nested mutually-recursive datatype
- Cl-isabelle-users January 2006 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