Re: [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)"
lemma X [simp]: "- (sometree = A)"
lemma Y [simp]: "- (sometree = B)"
lemma Z [simp]: "- (sometree = (tree A (tree x y)))"
lemma U [simp]: "- (sometree = (tree (tree u v) (tree x y)))"
lemma main: "changetree sometree = sometree"
apply (case_tac sometree)
I would expect that all simplifications lemmas X ... U will prove the
How it is possible to do a proof by the cases of the function
definition, not the case
The function package derives a case analysis rule "changetree.cases" for
you (which is basically a degenerate form of induction). Use it with
apply (cases sometree rule: changetree.cases)
Note that the cases you actually get are more than you wrote down in the
definition, due to pattern disambiguation.
Another remark (even if this is just a toy example): Don't use unary
minus when you mean negation, in particular in [simp] rules. Negation is
written ~ or \<not>, negated equality is written ~= or \<noteq>. Your
simp rules would never apply, because terms of this forms generally do
not occur. More generally: Write your simp rules in such a way that the
left hand side is a normal form wrt. to the existing simp rules.
Hope this helps,
This archive was generated by a fusion of
Pipermail (Mailman edition) and