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