src/HOL/BNF_Examples/TreeFsetI.thy
author blanchet
Fri Jan 24 11:51:45 2014 +0100 (2014-01-24)
changeset 55129 26bd1cba3ab5
parent 55091 c43394c2e5ec
child 55933 12ee2c407dad
permissions -rw-r--r--
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet@55075
     1
(*  Title:      HOL/BNF_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)"
traytel@54027
    23
  by (coinduction arbitrary: x) (auto simp: fset_rel_alt)
blanchet@48975
    24
blanchet@48975
    25
end