src/HOL/Datatype_Examples/TreeFsetI.thy
changeset 58309 a09ec6daaa19
parent 55933 12ee2c407dad
child 58889 5b7a9633cfa8
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Datatype_Examples/TreeFsetI.thy	Thu Sep 11 19:26:59 2014 +0200
     1.3 @@ -0,0 +1,25 @@
     1.4 +(*  Title:      HOL/Datatype_Examples/TreeFsetI.thy
     1.5 +    Author:     Dmitriy Traytel, TU Muenchen
     1.6 +    Author:     Andrei Popescu, TU Muenchen
     1.7 +    Copyright   2012
     1.8 +
     1.9 +Finitely branching possibly infinite trees, with sets of children.
    1.10 +*)
    1.11 +
    1.12 +header {* Finitely Branching Possibly Infinite Trees, with Sets of Children *}
    1.13 +
    1.14 +theory TreeFsetI
    1.15 +imports "~~/src/HOL/Library/FSet"
    1.16 +begin
    1.17 +
    1.18 +codatatype 'a treeFsetI = Tree (lab: 'a) (sub: "'a treeFsetI fset")
    1.19 +
    1.20 +(* tree map (contrived example): *)
    1.21 +primcorec tmap where
    1.22 +"lab (tmap f t) = f (lab t)" |
    1.23 +"sub (tmap f t) = fimage (tmap f) (sub t)"
    1.24 +
    1.25 +lemma "tmap (f o g) x = tmap f (tmap g x)"
    1.26 +  by (coinduction arbitrary: x) (auto simp: rel_fset_alt)
    1.27 +
    1.28 +end