Email Gateway (Aug 18 2022 at 17:42): Email Gateway (Aug 18 2022 at 17:42):From: Thomas Göthel <tgoethel@cs.tu-berlin.de>
Dear Isabelle-Community!
Given the following definition of a tree:
datatype myTree =
leaf
| bin_node "myTree" "myTree"
| inf_node "nat => myTree"
I would like to prove that trees are acyclic. But I do not even have an
idea how to prove the following lemma
lemma "t n \<noteq> bin_node T (inf_node t)"
I would greatly appreciate any hints!
Best regards,
Thomas
Email Gateway (Aug 18 2022 at 17:42):From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
Dear Thomas,
support for infinitely branching trees is a bit weak in the datatype package.
(For finitely branching datatypes, the datatype package provides a size function
which is typically used to show lemmas like these. Your infinitely branching
tree however does not have such a size function). The easiest way I know of is
to define the subterm relation by hand and prove that it is well-founded:
inductive_set tree_subterm :: "(myTree * myTree) set"
where
"(l, bin_node l r) : tree_subterm"
| "(r, bin_node l r) : tree_subterm"
| "(f n, inf_node f) : tree_subterm"
inductive_simps tree_subterm_simps [iff]:
"(t, leaf) : tree_subterm"
"(t, bin_node l r) : tree_subterm"
"(t, inf_node f) : tree_subterm"
lemma wf_tree_subterm: "wf tree_subterm"
unfolding wf_def
apply clarify
apply(induct_tac x)
apply blast+
done
Your inequality is then an easy consequence:
lemma "t n \<noteq> bin_node T (inf_node t)"
proof
assume "t n = bin_node T (inf_node t)"
moreover
have "(t n, bin_node T (inf_node t)) : tree_subterm^+"
by(blast intro: trancl.intros)
moreover have "acyclic tree_subterm" by(rule wf_acyclic wf_tree_subterm)+
ultimately show False by(simp add: acyclic_def)
qed
Well-foundedness of the subterm relation will also help you a lot when you try
to prove termination for functions defined with the function package. Alex might
be able to tell you more about how to set it up such that the function package
can use wf_tree_subterm.
Hope this helps,
Andreas
Thomas Göthel schrieb:
Email Gateway (Aug 18 2022 at 17:42):From: Alexander Krauss <krauss@in.tum.de>
It won't use it automatically, since automated termination proving is
based on measure functions into natural numbers only. However, you can
use such a subterm relation in manual termination proofs, e.g., using
the "relation" method.
Alex
Email Gateway (Aug 18 2022 at 17:43):From: Thomas Göthel <tgoethel@cs.tu-berlin.de>
Thank you very much!
The idea of using well-founded relations helped me a lot in this and in
further cases. :-)
Best regards,
Thomas
Last updated: Apr 19 2024 at 12:27 UTC