Email Gateway (Aug 18 2022 at 18:42): Email Gateway (Aug 18 2022 at 18:42):From: Viorel Preoteasa <viorel.preoteasa@abo.fi>
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
Email Gateway (Aug 18 2022 at 18:43):From: Alexander Krauss <krauss@in.tum.de>
Hi Viorel,
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
Last updated: Apr 24 2024 at 04:17 UTC