src/HOL/BNF/Examples/TreeFsetI.thy
author blanchet
Mon, 29 Apr 2013 09:10:49 +0200
changeset 51804 be6e703908f4
parent 51410 f0865a641e76
child 53013 3fbcfa911863
permissions -rw-r--r--
renamed BNF "(co)data" commands to names that are closer to their final names
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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
49508
1e205327f059 adapted examples to renamings
blanchet
parents: 49463
diff changeset
    15
hide_fact (open) Quotient_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
9ce0c2cbadb8 modernized example
blanchet
parents: 49594
diff changeset
    18
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    19
definition pair_fun (infixr "\<odot>" 50) where
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    20
  "f \<odot> g \<equiv> \<lambda>x. (f x, g x)"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    21
49631
9ce0c2cbadb8 modernized example
blanchet
parents: 49594
diff changeset
    22
(* tree map (contrived example): *)
9ce0c2cbadb8 modernized example
blanchet
parents: 49594
diff changeset
    23
definition tmap where
9ce0c2cbadb8 modernized example
blanchet
parents: 49594
diff changeset
    24
"tmap f = treeFsetI_unfold (f o lab) sub"
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    25
49631
9ce0c2cbadb8 modernized example
blanchet
parents: 49594
diff changeset
    26
lemma tmap_simps[simp]:
9ce0c2cbadb8 modernized example
blanchet
parents: 49594
diff changeset
    27
"lab (tmap f t) = f (lab t)"
51410
f0865a641e76 BNF uses fset defined via Lifting/Transfer rather than Quotient
traytel
parents: 50516
diff changeset
    28
"sub (tmap f t) = fmap (tmap f) (sub t)"
49631
9ce0c2cbadb8 modernized example
blanchet
parents: 49594
diff changeset
    29
unfolding tmap_def treeFsetI.sel_unfold by simp+
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    30
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    31
lemma "tmap (f o g) x = tmap f (tmap g x)"
49631
9ce0c2cbadb8 modernized example
blanchet
parents: 49594
diff changeset
    32
apply (rule treeFsetI.coinduct[of "%x1 x2. \<exists>x. x1 = tmap (f o g) x \<and> x2 = tmap f (tmap g x)"])
9ce0c2cbadb8 modernized example
blanchet
parents: 49594
diff changeset
    33
apply auto
9ce0c2cbadb8 modernized example
blanchet
parents: 49594
diff changeset
    34
apply (unfold fset_rel_def)
9ce0c2cbadb8 modernized example
blanchet
parents: 49594
diff changeset
    35
by auto
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    36
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    37
end