equal
deleted
inserted
replaced
19 by (simp_all add: fun_eq_iff) |
19 by (simp_all add: fun_eq_iff) |
20 |
20 |
21 |
21 |
22 subsection {* The datatype universe *} |
22 subsection {* The datatype universe *} |
23 |
23 |
24 typedef (Node) |
24 definition "Node = {p. EX f x k. p = (f :: nat => 'b + nat, x ::'a + nat) & f k = Inr 0}" |
25 ('a,'b) node = "{p. EX f x k. p = (f::nat=>'b+nat, x::'a+nat) & f k = Inr 0}" |
25 |
26 --{*it is a subtype of @{text "(nat=>'b+nat) * ('a+nat)"}*} |
26 typedef (open) ('a, 'b) node = "Node :: ((nat => 'b + nat) * ('a + nat)) set" |
27 by auto |
27 morphisms Rep_Node Abs_Node |
|
28 unfolding Node_def by auto |
28 |
29 |
29 text{*Datatypes will be represented by sets of type @{text node}*} |
30 text{*Datatypes will be represented by sets of type @{text node}*} |
30 |
31 |
31 type_synonym 'a item = "('a, unit) node set" |
32 type_synonym 'a item = "('a, unit) node set" |
32 type_synonym ('a, 'b) dtree = "('a, 'b) node set" |
33 type_synonym ('a, 'b) dtree = "('a, 'b) node set" |