*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Question concerning HOAS*From*: Thomas Göthel <tgoethel at cs.tu-berlin.de>*Date*: Fri, 20 May 2011 11:27:21 +0200*In-reply-to*: <4DD119EC.1070604@kit.edu>*References*: <4DD10056.9070509@cs.tu-berlin.de> <4DD119EC.1070604@kit.edu>*User-agent*: Mozilla/5.0 (X11; U; Linux x86_64; en-US; rv:1.9.2.17) Gecko/20110424 Lightning/1.0b2 Thunderbird/3.1.10

Thank you very much!

Best regards, Thomas Am 16.05.2011 14:34, schrieb Andreas Lochbihler:

Dear Thomas,support for infinitely branching trees is a bit weak in the datatypepackage. (For finitely branching datatypes, the datatype packageprovides a size function which is typically used to show lemmas likethese. Your infinitely branching tree however does not have such asize function). The easiest way I know of is to define the subtermrelation 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_acyclicwf_tree_subterm)+ultimately show False by(simp add: acyclic_def) qedWell-foundedness of the subterm relation will also help you a lot whenyou try to prove termination for functions defined with the functionpackage. Alex might be able to tell you more about how to set it upsuch 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 havean idea how to prove the following lemmalemma "t n \<noteq> bin_node T (inf_node t)" I would greatly appreciate any hints! Best regards, Thomas

**References**:**[isabelle] Question concerning HOAS***From:*Thomas Göthel

**Re: [isabelle] Question concerning HOAS***From:*Andreas Lochbihler

- Previous by Date: [isabelle] new AFP entry: Knowledge-Based Programs
- Next by Date: [isabelle] unexpected behaviour of user defined command in jedit
- Previous by Thread: Re: [isabelle] Question concerning HOAS
- Next by Thread: [isabelle] CFP: SSV 2011 - Workshop on Systems Software Verification [deadline extended]
- Cl-isabelle-users May 2011 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list