src/HOL/Datatype_Examples/TreeFsetI.thy

+(*  Title:      HOL/Datatype_Examples/TreeFsetI.thy
+    Author:     Dmitriy Traytel, TU Muenchen
+    Author:     Andrei Popescu, TU Muenchen
+    Copyright   2012
+
+Finitely branching possibly infinite trees, with sets of children.
+*)
+
+header {* Finitely Branching Possibly Infinite Trees, with Sets of Children *}
+
+theory TreeFsetI
+imports "~~/src/HOL/Library/FSet"
+begin
+
+codatatype 'a treeFsetI = Tree (lab: 'a) (sub: "'a treeFsetI fset")
+
+(* tree map (contrived example): *)
+primcorec tmap where
+"lab (tmap f t) = f (lab t)" |
+"sub (tmap f t) = fimage (tmap f) (sub t)"
+
+lemma "tmap (f o g) x = tmap f (tmap g x)"
+  by (coinduction arbitrary: x) (auto simp: rel_fset_alt)
+
+end