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

[Christian Sternagel]

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
>
>