On 06/18/2012 01:18 AM, Florian Haftmann wrote:
Hi Christian,
PS: I am just playing around with a locale for finite trees and wanted
to introduce some recursive functions (and later also inductive
predicates) but pattern matching is only possible on constructors. Is
anybody aware of an earlier attempt for doing such a thing or a better
way to prove something "for all kinds of (non empty) finite trees"?
Yes I have. In the wqo AFP entry (theory Kruskal) I have a proof of the
tree theorem for a concrete datatype of (non-empty) finite trees
datatype 'a tree = Node 'a "'a tree list"
However, the result only relies on definitions (and properties about
them) that are (or at least I guess so) available for _any_ conceivable
type of finite trees, namely getting the root of a tree
root (Node x ts) = x
getting the direct successors of a node
args (Node x ts) = ts
the subtree relation
inductive
subtree :: "'a tree ⇒ 'a tree ⇒ bool"
where
base: "s ∈ set ss ⟹ subtree s (Node x ss)" |
step: "subtree s t ⟹ t ∈ set ts ⟹ subtree s (Node x ts)"
homomorphic embedding on trees
inductive
subtree :: "'a tree ⇒ 'a tree ⇒ bool"
where
base: "s ∈ set ss ⟹ subtree s (Node x ss)" |
step: "subtree s t ⟹ t ∈ set ts ⟹ subtree s (Node x ts)"
and maybe one or two more.
So I wanted to define all these operations inside a locale (and proof
the required properties) that encapsulates the essentials of being a
finite tree, where my first attempt was
locale finite_tree =
fixes mk :: "'b ⇒ 'a list ⇒ 'a"
and root :: "'a ⇒ 'b"
and succs :: "'a ⇒ 'a list"
assumes inject: "mk x ts = mk x' ts' ⟷ x = x' ∧ ts = ts'"
and induct: "(⋀x ts. P2 ts ⟹ P1 (mk x ts)) ⟹
P2 [] ⟹ (⋀t ts. P1 t ⟹ P2 ts ⟹ P2 (t#ts)) ⟹ P1 t ∧ P2 ts"
and root_node [simp]: "root (mk x ts) = x"
and succs_node [simp]: "succs (mk x ts) = ts"
begin
So if "mk" is injective, allows induction (hence only finite trees), and
has proper selector functions, then it is a constructor of finite trees.
Next I wanted to define a function
function nodes where
"nodes t = {root t} ∪ ⋃set (map nodes (succs t))"
which would be trivial, if "mk" was a datatype constructor. But as is, I
would essentially have to repeat all the constructions that happen
inside the datatype package to get this function (I guess).
I see. From a practical point of view, I doubt a localized rep_datatype
would be helpful here since the »datatype« in your example syntactically
is a type variable 'a (or maybe even to mutual dependent »datatypes« 'a
and 'b, if I guess correctly), and this would mean that the bookkeeping
of the datatype package needed to be generalized from type constructors
to the union of type constructors and type variables.
However, there is a big chance that you can help yourself by
a) either defining a generic recursion combinator »once and for all« to
traverse trees;
Thanks for the advice this worked (after looking through Stefan's master
thesis on the datatype package, which is great for following the
internal constructions, like defining generic recursion combinators).
cheers
chris
b) providing a set of lemmas to help you prove your function
specifications consistent with little specific effort.
I don't really understand this point though ;)
Maybe similar patterns can be found in the Collection Library in the AFP.
Cheers,
Florian
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
