src/HOL/BNF_Examples/TreeFsetI.thy
author blanchet
Tue, 21 Jan 2014 01:14:49 +0100
changeset 55091 c43394c2e5ec
parent 55076 1e73e090a514
child 55129 26bd1cba3ab5
permissions -rw-r--r--
compile
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
55075
b3d0a02a756d dissolved BNF session
blanchet
parents: 55071
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
55076
1e73e090a514 compile
blanchet
parents: 55075
diff changeset
    12
imports "~~/src/HOL/Library/More_BNFs"
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)"
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