src/HOL/BNF_Examples/TreeFsetI.thy
changeset 55933 12ee2c407dad
parent 55129 26bd1cba3ab5
equal deleted inserted replaced
55932:68c5104d2204 55933:12ee2c407dad
    18 primcorec tmap where
    18 primcorec tmap where
    19 "lab (tmap f t) = f (lab t)" |
    19 "lab (tmap f t) = f (lab t)" |
    20 "sub (tmap f t) = fimage (tmap f) (sub t)"
    20 "sub (tmap f t) = fimage (tmap f) (sub t)"
    21 
    21 
    22 lemma "tmap (f o g) x = tmap f (tmap g x)"
    22 lemma "tmap (f o g) x = tmap f (tmap g x)"
    23   by (coinduction arbitrary: x) (auto simp: fset_rel_alt)
    23   by (coinduction arbitrary: x) (auto simp: rel_fset_alt)
    24 
    24 
    25 end
    25 end