Re: [isabelle] a question



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






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