49 attach {* |
49 attach {* |
50 fun nat i = if i < 0 then 0 else i; |
50 fun nat i = if i < 0 then 0 else i; |
51 *} |
51 *} |
52 int ("(_)") |
52 int ("(_)") |
53 |
53 |
|
54 definition |
|
55 "nat_plus m n = nat (int m + int n)" |
|
56 "nat_minus m n = nat (int m - int n)" |
|
57 "nat_mult m n = nat (int m * int n)" |
|
58 "nat_div m n = nat (fst (divAlg (int m, int n)))" |
|
59 "nat_mod m n = nat (snd (divAlg (int m, int n)))" |
|
60 "nat_less m n = (int m < int n)" |
|
61 "nat_less_equal m n = (int m <= int n)" |
|
62 "nat_eq m n = (int m = int n)" |
|
63 |
54 code_typapp nat |
64 code_typapp nat |
55 ml (target_atom "IntInf.int") |
65 ml (target_atom "IntInf.int") |
56 haskell (target_atom "Integer") |
66 haskell (target_atom "Integer") |
57 |
67 |
58 definition |
|
59 "nat_of_int (k::int) = (if k < 0 then - k else k)" |
|
60 |
|
61 lemma |
|
62 "nat_of_int = abs" |
|
63 by (simp add: expand_fun_eq nat_of_int_def zabs_def) |
|
64 |
|
65 code_generate (ml, haskell) "abs :: int \<Rightarrow> int" |
|
66 |
|
67 code_constapp |
68 code_constapp |
|
69 "0::nat" (* all constructors of nat must be hidden *) |
|
70 ml (target_atom "(0 :: IntInf.int)") |
|
71 haskell (target_atom "0") |
|
72 Suc (* all constructors of nat must be hidden *) |
|
73 ml ("IntInf.+ (_, 1)") |
|
74 haskell ("(+) 1 _") |
68 nat |
75 nat |
69 ml ("{* abs :: int \<Rightarrow> int *}") |
76 ml (target_atom "(fn n : IntInf.int => if n < 0 then 0 else n)") |
70 haskell ("{* abs :: int \<Rightarrow> int *}") |
77 haskell (target_atom "(\\n :: Int -> if n < 0 then 0 else n)") |
71 int |
78 int |
72 ml ("_") |
79 ml ("_") |
73 haskell ("_") |
80 haskell ("_") |
74 |
81 |
75 text {* |
82 text {* |
76 Eliminate @{const "0::nat"} and @{const "Suc"} |
83 Eliminate @{const "0::nat"} and @{const "1::nat"} |
77 by unfolding in place. |
84 by unfolding in place. |
78 *} |
85 *} |
79 |
86 |
80 lemma [code inline]: |
87 lemma [code inline]: |
81 "0 = nat 0" |
88 "0 = nat 0" |
82 "Suc = (op +) 1" |
89 "1 = nat 1" |
83 by (simp_all add: expand_fun_eq) |
90 by (simp_all add: expand_fun_eq) |
84 |
|
85 declare elim_one_nat [code nofold] |
|
86 |
91 |
87 text {* |
92 text {* |
88 Case analysis on natural numbers is rephrased using a conditional |
93 Case analysis on natural numbers is rephrased using a conditional |
89 expression: |
94 expression: |
90 *} |
95 *} |
110 by (simp add: zdiv_int [symmetric]) |
115 by (simp add: zdiv_int [symmetric]) |
111 lemma [code]: "m mod n = nat (int m mod int n)" |
116 lemma [code]: "m mod n = nat (int m mod int n)" |
112 by (simp add: zmod_int [symmetric]) |
117 by (simp add: zmod_int [symmetric]) |
113 lemma [code]: "(m < n) = (int m < int n)" |
118 lemma [code]: "(m < n) = (int m < int n)" |
114 by simp |
119 by simp |
|
120 |
|
121 lemma [code fun, code inline]: "m + n = nat_plus m n" |
|
122 unfolding nat_plus_def by arith |
|
123 lemma [code fun, code inline]: "m - n = nat_minus m n" |
|
124 unfolding nat_minus_def by arith |
|
125 lemma [code fun, code inline]: "m * n = nat_mult m n" |
|
126 unfolding nat_mult_def by (simp add: zmult_int) |
|
127 lemma [code fun, code inline]: "m div n = nat_div m n" |
|
128 unfolding nat_div_def div_def [symmetric] zdiv_int [symmetric] by simp |
|
129 lemma [code fun, code inline]: "m mod n = nat_mod m n" |
|
130 unfolding nat_mod_def mod_def [symmetric] zmod_int [symmetric] by simp |
|
131 lemma [code fun, code inline]: "(m < n) = nat_less m n" |
|
132 unfolding nat_less_def by simp |
|
133 lemma [code fun, code inline]: "(m <= n) = nat_less_equal m n" |
|
134 unfolding nat_less_equal_def by simp |
|
135 lemma [code fun, code inline]: "(m = n) = nat_eq m n" |
|
136 unfolding nat_eq_def by simp |
115 lemma [code fun]: |
137 lemma [code fun]: |
116 "(m = n) = (int m = int n)" |
138 "int_aux i n = (if nat_eq n 0 then i else int_aux (i + 1) (nat_minus n 1))" |
117 by simp |
139 unfolding nat_eq_def nat_minus_def int_aux_def by simp |
|
140 |
118 |
141 |
119 subsection {* Preprocessors *} |
142 subsection {* Preprocessors *} |
120 |
143 |
121 text {* |
144 text {* |
122 In contrast to @{term "Suc n"}, the term @{term "n + (1::nat)"} is no longer |
145 In contrast to @{term "Suc n"}, the term @{term "n + (1::nat)"} is no longer |