[isabelle-dev] Pattern matching on finite trees [was: "rep_datatype" is illegal in local theory mode]

[Florian Haftmann]

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;

b) providing a set of lemmas to help you prove your function
specifications consistent with little specific effort.

Maybe similar patterns can be found in the Collection Library in the AFP.

Cheers,
	Florian


-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 262 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20120617/a53e7f42/attachment.sig>