# [isabelle] recursive functions

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?
Best regards,
Viorel

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