| author | wenzelm |
| Mon, 24 Oct 2016 11:42:39 +0200 | |
| changeset 64367 | a424f2737646 |
| parent 63167 | 0909deb8059b |
| child 66453 | cc19f7ca2ed6 |
| permissions | -rw-r--r-- |
|
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 |
|
| 63167 | 9 |
section \<open>Finitely Branching Possibly Infinite Trees, with Sets of Children\<close> |
|
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 | 16 |
|
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 | 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 | 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 |