Mercurial Mercurial > repos > isabelle / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Datatype_Examples/TreeFsetI.thy
author wenzelm
Sat, 26 Jun 2021 20:55:43 +0200
changeset 73884 0a12ca4f3e8d
parent 66453 cc19f7ca2ed6
permissions -rw-r--r--
proper Font_Subst.cache for paintScreenLineRange;

(*  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.
*)

section \<open>Finitely Branching Possibly Infinite Trees, with Sets of Children\<close>

theory TreeFsetI
imports "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
isabelle