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

[Christian Sternagel]

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