src/HOL/Datatype_Examples/TreeFsetI.thy
author wenzelm
Sun, 02 Nov 2014 18:21:45 +0100
changeset 58889 5b7a9633cfa8
parent 58309 a09ec6daaa19
child 63167 0909deb8059b
permissions -rw-r--r--
modernized header uniformly as section;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
58309
a09ec6daaa19 renamed 'BNF_Examples' to 'Datatype_Examples' (cf. 'datatypes.pdf')
blanchet
parents: 55933
diff changeset
     1
(*  Title:      HOL/Datatype_Examples/TreeFsetI.thy
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
     2
    Author:     Dmitriy Traytel, TU Muenchen
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
     3
    Author:     Andrei Popescu, TU Muenchen
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
     4
    Copyright   2012
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
     5
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
     6
Finitely branching possibly infinite trees, with sets of children.
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
     7
*)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
     8
58889
5b7a9633cfa8 modernized header uniformly as section;
wenzelm
parents: 58309
diff changeset
     9
section {* Finitely Branching Possibly Infinite Trees, with Sets of Children *}
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    10
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    11
theory TreeFsetI
55129
26bd1cba3ab5 killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents: 55091
diff changeset
    12
imports "~~/src/HOL/Library/FSet"
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    13
begin
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    14
51804
be6e703908f4 renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents: 51410
diff changeset
    15
codatatype 'a treeFsetI = Tree (lab: 'a) (sub: "'a treeFsetI fset")
49631
9ce0c2cbadb8 modernized example
blanchet
parents: 49594
diff changeset
    16
9ce0c2cbadb8 modernized example
blanchet
parents: 49594
diff changeset
    17
(* tree map (contrived example): *)
54027
e5853a648b59 use new coinduction method and primcorec in examples
traytel
parents: 54014
diff changeset
    18
primcorec tmap where
e5853a648b59 use new coinduction method and primcorec in examples
traytel
parents: 54014
diff changeset
    19
"lab (tmap f t) = f (lab t)" |
54014
21dac9a60f0c base the fset bnf on the new FSet theory
traytel
parents: 53013
diff changeset
    20
"sub (tmap f t) = fimage (tmap f) (sub t)"
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    21
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    22
lemma "tmap (f o g) x = tmap f (tmap g x)"
55933
12ee2c407dad renamed 'fset_rel' to 'rel_fset'
blanchet
parents: 55129
diff changeset
    23
  by (coinduction arbitrary: x) (auto simp: rel_fset_alt)
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    24
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    25
end