| author | haftmann |
| Mon, 03 Feb 2014 08:23:21 +0100 | |
| changeset 55293 | 42cf5802d36a |
| parent 55129 | 26bd1cba3ab5 |
| child 55933 | 12ee2c407dad |
| permissions | -rw-r--r-- |
| 55075 | 1 |
(* Title: HOL/BNF_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 |
|
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
9 |
header {* 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
|
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)" |
|
54027
e5853a648b59
use new coinduction method and primcorec in examples
traytel
parents:
54014
diff
changeset
|
23 |
by (coinduction arbitrary: x) (auto simp: fset_rel_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 |