equal
deleted
inserted
replaced
12 |
12 |
13 subsection {* The datatype universe *} |
13 subsection {* The datatype universe *} |
14 |
14 |
15 definition "Node = {p. EX f x k. p = (f :: nat => 'b + nat, x ::'a + nat) & f k = Inr 0}" |
15 definition "Node = {p. EX f x k. p = (f :: nat => 'b + nat, x ::'a + nat) & f k = Inr 0}" |
16 |
16 |
17 typedef (open) ('a, 'b) node = "Node :: ((nat => 'b + nat) * ('a + nat)) set" |
17 typedef ('a, 'b) node = "Node :: ((nat => 'b + nat) * ('a + nat)) set" |
18 morphisms Rep_Node Abs_Node |
18 morphisms Rep_Node Abs_Node |
19 unfolding Node_def by auto |
19 unfolding Node_def by auto |
20 |
20 |
21 text{*Datatypes will be represented by sets of type @{text node}*} |
21 text{*Datatypes will be represented by sets of type @{text node}*} |
22 |
22 |