*To*: 张欢欢 <hzhang at ecust.edu.cn>*Subject*: Re: [isabelle] a question*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Mon, 08 Nov 2010 08:23:18 +0100*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <489185911.23463@ecust.edu.cn>*References*: <489185911.23463@ecust.edu.cn>*User-agent*: Thunderbird 2.0.0.24 (Macintosh/20100228)

In your second proof you have a free f that needs to be fixed. In particular, you need to ensure that the type of f and of x and y fit together. You should start with fix f :: "'a" and x y :: "'a tree" (I haven't tried it out...) But writing all of this out by hand is painful. I recommend to use the case (Node x f y) ... show ?case idiom to simplify your life. Tobias 张欢欢 schrieb: > Dear ALL: > > I am trying to figure out the following items this week: > > define a binary tree, function "mirror" is to mirror a tree by swapping subtrees recursively. > Prove lemma "mirror(mirror t)=t" > > The following are my two answers. One is correct, the other is wrong. But they are from the same paper work. Could you tell me why the second one is wrong please? > > theory treeMirror_correct > imports Main > begin > datatype tree = Leaf | Node tree tree > primrec mirror::" tree => tree" where > "mirror Leaf = Leaf"| > "mirror (Node left right) = (Node (mirror right) (mirror left))" > > theorem "mirror(mirror t)=t" > proof (induct t) > show "mirror(mirror Leaf) = Leaf" by simp > next > fix x assume IH:"mirror(mirror(x)) = x" > fix y assume IH1:"mirror(mirror(y)) = y" > have "mirror( mirror(Node x y) ) = mirror( Node (mirror y) (mirror x) )" by auto > also have "...= ( Node (mirror(mirror x)) (mirror(mirror y)) )" by auto > also from IH IH1 have "...= (Node x y)" by simp > ultimately show "mirror( mirror(Node x y) ) = (Node x y)"by simp > qed > end > ***************************************************************** > theory treeMirror_incorrect > imports Main > begin > datatype 'a tree = Tip | Node "'a tree" "'a" "'a tree" > primrec mirror::"'a tree => 'a tree" where > "mirror Tip = Tip"| > "mirror(Node left f right) = Node (mirror right) f (mirror left)" > > theorem "mirror(mirror t)=t" > proof (induct t) > show "mirror(mirror Tip) = Tip" by simp > next > fix x assume IH:"mirror(mirror(x)) = x" > fix y assume IH1:"mirror(mirror(y)) = y" > have " mirror( mirror(Node x f y) ) = mirror( Node (mirror y) f (mirror x) )" by auto > > (**** Type unification failed > *** Type error in application: Incompatible operand type > *** > *** Operator: Node x f :: 'b tree => 'b tree > *** Operand: y :: 'c tree > *** > *** At command "have".*) > > also have "...= (Node mirror(mirror x) f mirror(mirror y))" by auto > also from IH IH1 have "...= (Node x f y)" by simp > ultimately show "mirror( mirror(Node x f y) ) = (Node x f y)"by simp > qed > end > > >

**References**:**[isabelle] a question***From:*张欢欢

- Previous by Date: [isabelle] a question
- Next by Date: [isabelle] CfP: JOURNAL OF APPLIED LOGIC, Special Issue on Automated Specification and Verification of Web Systems
- Previous by Thread: [isabelle] a question
- Next by Thread: [isabelle] CfP: JOURNAL OF APPLIED LOGIC, Special Issue on Automated Specification and Verification of Web Systems
- Cl-isabelle-users November 2010 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