src/HOL/BNF_Examples/TreeFsetI.thy
author blanchet
Thu, 06 Mar 2014 13:36:49 +0100
changeset 55933 12ee2c407dad
parent 55129 26bd1cba3ab5
permissions -rw-r--r--
renamed 'fset_rel' to 'rel_fset'

(*  Title:      HOL/BNF_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