*To*: Viorel Preoteasa <viorel.preoteasa at abo.fi>*Subject*: Re: [isabelle] recursive functions*From*: Alexander Krauss <krauss at in.tum.de>*Date*: Sat, 12 Nov 2011 15:30:48 +0100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <4EBB809F.4010108@abo.fi>*References*: <717F714B587F944C88837A99AA4D008149DD634A@TK5EX14MBXC111.redmond.corp.microsoft.com> <4EBB7869.4030900@in.tum.de> <4EBB809F.4010108@abo.fi>*User-agent*: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:1.9.1.16) Gecko/20111004 Icedove/3.0.11

Hi Viorel,

I have the following definitions: datatype Tree = A | B | "tree" "Tree" "Tree" fun changetree:: "Tree => Tree" where "changetree A = B"| "changetree B = A"| "changetree (tree A (tree x y)) = tree (changetree y) (changetree x)" | "changetree (tree (tree u v) (tree x y)) = tree (changetree y) (changetree x)" | "changetree (tree x y) = (tree x y)" consts sometree:: "Tree" lemma X [simp]: "- (sometree = A)" sorry lemma Y [simp]: "- (sometree = B)" sorry lemma Z [simp]: "- (sometree = (tree A (tree x y)))" sorry lemma U [simp]: "- (sometree = (tree (tree u v) (tree x y)))" sorry lemma main: "changetree sometree = sometree" apply (case_tac sometree) apply simp_all I would expect that all simplifications lemmas X ... U will prove the lemma main. How it is possible to do a proof by the cases of the function definition, not the case of tree?

apply (cases sometree rule: changetree.cases)

Hope this helps, Alex

**References**:**[isabelle] No Code Equation for LIMSEQ***From:*Dave Thayer

**Re: [isabelle] No Code Equation for LIMSEQ***From:*Tobias Nipkow

**[isabelle] recursive functions***From:*Viorel Preoteasa

- Previous by Date: [isabelle] Call for paper: iFM 2012
- Next by Date: [isabelle] Hilbert's EPS operator question
- Previous by Thread: [isabelle] recursive functions
- Next by Thread: Re: [isabelle] No Code Equation for LIMSEQ
- Cl-isabelle-users November 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