# Re: [isabelle] Question concerning HOAS

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:

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

--
Karlsruher Institut für Technologie
IPD Snelting
Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Adenauerring 20a, Geb. 50.41, Raum 023
76131 Karlsruhe
Telefon: +49 721 608-48352
Fax: +49 721 608-48457
E-Mail: andreas.lochbihler at kit.edu
http://pp.info.uni-karlsruhe.de

`KIT - Universität des Landes Baden-Württemberg und nationales Forschungszentrum
``in der Helmholtz-Gemeinschaft
`

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