Hi Florian,
On 06/16/2012 03:51 AM, Florian Haftmann wrote:
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"?
Hmmmm... have you got specification pieces which illustrate what you
want to accomplish more exactly?
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).
cheers
chris
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
