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 ```