src/HOL/Datatype_Examples/TreeFsetI.thy
author haftmann
Fri Oct 10 19:55:32 2014 +0200 (2014-10-10)
changeset 58646 cd63a4b12a33
parent 58309 a09ec6daaa19
child 58889 5b7a9633cfa8
permissions -rw-r--r--
specialized specification: avoid trivial instances
     1 (*  Title:      HOL/Datatype_Examples/TreeFsetI.thy
     2     Author:     Dmitriy Traytel, TU Muenchen
     3     Author:     Andrei Popescu, TU Muenchen
     4     Copyright   2012
     5 
     6 Finitely branching possibly infinite trees, with sets of children.
     7 *)
     8 
     9 header {* Finitely Branching Possibly Infinite Trees, with Sets of Children *}
    10 
    11 theory TreeFsetI
    12 imports "~~/src/HOL/Library/FSet"
    13 begin
    14 
    15 codatatype 'a treeFsetI = Tree (lab: 'a) (sub: "'a treeFsetI fset")
    16 
    17 (* tree map (contrived example): *)
    18 primcorec tmap where
    19 "lab (tmap f t) = f (lab t)" |
    20 "sub (tmap f t) = fimage (tmap f) (sub t)"
    21 
    22 lemma "tmap (f o g) x = tmap f (tmap g x)"
    23   by (coinduction arbitrary: x) (auto simp: rel_fset_alt)
    24 
    25 end