Re: [isabelle] recursive functions



Hi Viorel,

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?

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,

Alex





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