[isabelle-dev] Pattern matching on finite trees [was: "rep_datatype" is illegal in local theory mode]
Christian Sternagel
c-sterna at jaist.ac.jp
Sat Jun 16 05:25:53 CEST 2012
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
More information about the isabelle-dev
mailing list