| author | blanchet |
| Tue, 19 Nov 2013 14:33:20 +0100 | |
| changeset 54491 | 27966e17d075 |
| parent 54027 | e5853a648b59 |
| permissions | -rw-r--r-- |
|
49509
163914705f8d
renamed top-level theory from "Codatatype" to "BNF"
blanchet
parents:
49508
diff
changeset
|
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 |
|
49509
163914705f8d
renamed top-level theory from "Codatatype" to "BNF"
blanchet
parents:
49508
diff
changeset
|
12 |
imports "../BNF" |
|
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 |
|
|
53013
3fbcfa911863
remove unnecessary dependencies on Library/Quotient_*
kuncar
parents:
51804
diff
changeset
|
15 |
hide_fact (open) Lifting_Product.prod_rel_def |
|
49092
5eddc9aaebf1
hide newly introduced constant Sublist.sub to allow for name sub in TreeFsetI
Christian Sternagel
parents:
48980
diff
changeset
|
16 |
|
|
51804
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
51410
diff
changeset
|
17 |
codatatype 'a treeFsetI = Tree (lab: 'a) (sub: "'a treeFsetI fset") |
| 49631 | 18 |
|
19 |
(* tree map (contrived example): *) |
|
|
54027
e5853a648b59
use new coinduction method and primcorec in examples
traytel
parents:
54014
diff
changeset
|
20 |
primcorec tmap where |
|
e5853a648b59
use new coinduction method and primcorec in examples
traytel
parents:
54014
diff
changeset
|
21 |
"lab (tmap f t) = f (lab t)" | |
| 54014 | 22 |
"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
|
23 |
|
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
24 |
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
|
25 |
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
|
26 |
|
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
27 |
end |