equal
deleted
inserted
replaced
9 header {* Analogues of the Cartesian Product and Disjoint Sum for Datatypes *} |
9 header {* Analogues of the Cartesian Product and Disjoint Sum for Datatypes *} |
10 |
10 |
11 theory Datatype |
11 theory Datatype |
12 imports Finite_Set |
12 imports Finite_Set |
13 begin |
13 begin |
|
14 |
|
15 lemma size_bool [code func]: |
|
16 "size (b\<Colon>bool) = 0" by (cases b) auto |
|
17 |
|
18 declare "prod.size" [noatp] |
14 |
19 |
15 typedef (Node) |
20 typedef (Node) |
16 ('a,'b) node = "{p. EX f x k. p = (f::nat=>'b+nat, x::'a+nat) & f k = Inr 0}" |
21 ('a,'b) node = "{p. EX f x k. p = (f::nat=>'b+nat, x::'a+nat) & f k = Inr 0}" |
17 --{*it is a subtype of @{text "(nat=>'b+nat) * ('a+nat)"}*} |
22 --{*it is a subtype of @{text "(nat=>'b+nat) * ('a+nat)"}*} |
18 by auto |
23 by auto |