Re: [isabelle] Question concerning HOAS

Thank you very much!

The idea of using well-founded relations helped me a lot in this and in further cases. :-)

Best regards,

Am 16.05.2011 14:34, schrieb Andreas Lochbihler:
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,

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