equal
deleted
inserted
replaced
8 |
8 |
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 uses "Tools/datatype_codegen.ML" |
|
14 begin |
13 begin |
15 |
14 |
16 typedef (Node) |
15 typedef (Node) |
17 ('a,'b) node = "{p. EX f x k. p = (f::nat=>'b+nat, x::'a+nat) & f k = Inr 0}" |
16 ('a,'b) node = "{p. EX f x k. p = (f::nat=>'b+nat, x::'a+nat) & f k = Inr 0}" |
18 --{*it is a subtype of @{text "(nat=>'b+nat) * ('a+nat)"}*} |
17 --{*it is a subtype of @{text "(nat=>'b+nat) * ('a+nat)"}*} |
680 by (rule ext) (simp split: sum.split) |
679 by (rule ext) (simp split: sum.split) |
681 |
680 |
682 |
681 |
683 subsubsection {* Code generator setup *} |
682 subsubsection {* Code generator setup *} |
684 |
683 |
685 setup DatatypeCodegen.setup |
|
686 |
|
687 definition |
684 definition |
688 is_none :: "'a option \<Rightarrow> bool" where |
685 is_none :: "'a option \<Rightarrow> bool" where |
689 is_none_none [code post, symmetric, code inline]: "is_none x \<longleftrightarrow> x = None" |
686 is_none_none [code post, symmetric, code inline]: "is_none x \<longleftrightarrow> x = None" |
690 |
687 |
691 lemma is_none_code [code]: |
688 lemma is_none_code [code]: |