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.