src/HOL/Datatype_Examples/TreeFsetI.thy
author blanchet
Thu Sep 11 19:26:59 2014 +0200 (2014-09-11)
changeset 58309 a09ec6daaa19
parent 55933 src/HOL/BNF_Examples/TreeFsetI.thy@12ee2c407dad
child 58889 5b7a9633cfa8
permissions -rw-r--r--
renamed 'BNF_Examples' to 'Datatype_Examples' (cf. 'datatypes.pdf')
blanchet@58309
     1
(*  Title:      HOL/Datatype_Examples/TreeFsetI.thy
blanchet@48975
     2
    Author:     Dmitriy Traytel, TU Muenchen
blanchet@48975
     3
    Author:     Andrei Popescu, TU Muenchen
blanchet@48975
     4
    Copyright   2012
blanchet@48975
     5
blanchet@48975
     6
Finitely branching possibly infinite trees, with sets of children.
blanchet@48975
     7
*)
blanchet@48975
     8
blanchet@48975
     9
header {* Finitely Branching Possibly Infinite Trees, with Sets of Children *}
blanchet@48975
    10
blanchet@48975
    11
theory TreeFsetI
blanchet@55129
    12
imports "~~/src/HOL/Library/FSet"
blanchet@48975
    13
begin
blanchet@48975
    14
blanchet@51804
    15
codatatype 'a treeFsetI = Tree (lab: 'a) (sub: "'a treeFsetI fset")
blanchet@49631
    16
blanchet@49631
    17
(* tree map (contrived example): *)
traytel@54027
    18
primcorec tmap where
traytel@54027
    19
"lab (tmap f t) = f (lab t)" |
traytel@54014
    20
"sub (tmap f t) = fimage (tmap f) (sub t)"
blanchet@48975
    21
blanchet@48975
    22
lemma "tmap (f o g) x = tmap f (tmap g x)"
blanchet@55933
    23
  by (coinduction arbitrary: x) (auto simp: rel_fset_alt)
blanchet@48975
    24
blanchet@48975
    25
end