[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.