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"
  "(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+

Your inequality is then an easy consequence:

lemma "t n \<noteq> bin_node T (inf_node t)"
  assume "t n = bin_node T (inf_node t)"
  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)

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,

Thomas Göthel schrieb:
Dear Isabelle-Community!

Given the following definition of a tree:

datatype myTree =
| 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,

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 - 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.