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