# [isabelle] a question

```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

```

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.