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 |
54 ML {* set Toplevel.debug *} |
55 "nat_plus m n = nat (int m + int n)" |
55 setup {* |
56 "nat_minus m n = nat (int m - int n)" |
56 CodegenData.del_datatype "nat" |
57 "nat_mult m n = nat (int m * int n)" |
57 *} |
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 |
58 |
64 code_type nat |
59 code_type nat |
65 (SML target_atom "IntInf.int") |
60 (SML target_atom "IntInf.int") |
66 (Haskell target_atom "Integer") |
61 (Haskell target_atom "Integer") |
67 |
62 |
68 code_const "0::nat" and Suc (*all constructors of nat must be hidden*) |
63 code_const int |
69 (SML target_atom "(0 :: IntInf.int)" and "IntInf.+ (_, 1)") |
64 (SML "_") |
70 (Haskell target_atom "0" and "(+) 1 _") |
65 (Haskell "_") |
71 |
66 |
72 code_const nat and int |
67 definition |
73 (SML target_atom "(fn n : IntInf.int => if n < 0 then 0 else n)" and "_") |
68 nat_of_int :: "int \<Rightarrow> nat" |
74 (Haskell target_atom "(\\n :: Int -> if n < 0 then 0 else n)" and "_") |
69 "k \<ge> 0 \<Longrightarrow> nat_of_int k = nat k" |
75 |
|
76 text {* |
|
77 Eliminate @{const "0::nat"} and @{const "1::nat"} |
|
78 by unfolding in place. |
|
79 *} |
|
80 |
|
81 lemma [code inline]: |
|
82 "0 = nat 0" |
|
83 "1 = nat 1" |
|
84 by (simp_all add: expand_fun_eq) |
|
85 |
70 |
86 text {* |
71 text {* |
87 Case analysis on natural numbers is rephrased using a conditional |
72 Case analysis on natural numbers is rephrased using a conditional |
88 expression: |
73 expression: |
89 *} |
74 *} |
97 text {* |
82 text {* |
98 Most standard arithmetic functions on natural numbers are implemented |
83 Most standard arithmetic functions on natural numbers are implemented |
99 using their counterparts on the integers: |
84 using their counterparts on the integers: |
100 *} |
85 *} |
101 |
86 |
102 lemma [code]: "m + n = nat (int m + int n)" |
87 code_constname |
|
88 nat_of_int "IntDef.nat_of_int" |
|
89 |
|
90 code_const nat_of_int |
|
91 (SML "_") |
|
92 (Haskell "_") |
|
93 |
|
94 lemma [code func]: "0 = nat_of_int 0" |
|
95 by (simp add: nat_of_int_def) |
|
96 lemma [code func, code inline]: "1 = nat_of_int 1" |
|
97 by (simp add: nat_of_int_def) |
|
98 lemma [code func]: "Suc n = n + 1" |
|
99 by simp |
|
100 lemma [code, code inline]: "m + n = nat (int m + int n)" |
103 by arith |
101 by arith |
104 lemma [code]: "m - n = nat (int m - int n)" |
102 lemma [code func, code inline]: "m + n = nat_of_int (int m + int n)" |
|
103 by (simp add: nat_of_int_def) |
|
104 lemma [code, code inline]: "m - n = nat (int m - int n)" |
105 by arith |
105 by arith |
106 lemma [code]: "m * n = nat (int m * int n)" |
106 lemma [code, code inline]: "m * n = nat (int m * int n)" |
107 by (simp add: zmult_int) |
107 unfolding zmult_int by simp |
|
108 lemma [code func, code inline]: "m * n = nat_of_int (int m * int n)" |
|
109 proof - |
|
110 have "int (m * n) = int m * int n" |
|
111 by (induct m) (simp_all add: zadd_zmult_distrib) |
|
112 then have "m * n = nat (int m * int n)" by auto |
|
113 also have "\<dots> = nat_of_int (int m * int n)" |
|
114 proof - |
|
115 have "int m \<ge> 0" and "int n \<ge> 0" by auto |
|
116 have "int m * int n \<ge> 0" by (rule split_mult_pos_le) auto |
|
117 with nat_of_int_def show ?thesis by auto |
|
118 qed |
|
119 finally show ?thesis . |
|
120 qed |
108 lemma [code]: "m div n = nat (int m div int n)" |
121 lemma [code]: "m div n = nat (int m div int n)" |
109 by (simp add: zdiv_int [symmetric]) |
122 unfolding zdiv_int [symmetric] by simp |
|
123 lemma [code func]: "m div n = fst (Divides.divmod m n)" |
|
124 unfolding divmod_def by simp |
110 lemma [code]: "m mod n = nat (int m mod int n)" |
125 lemma [code]: "m mod n = nat (int m mod int n)" |
111 by (simp add: zmod_int [symmetric]) |
126 unfolding zmod_int [symmetric] by simp |
112 lemma [code]: "(m < n) = (int m < int n)" |
127 lemma [code func]: "m mod n = snd (Divides.divmod m n)" |
|
128 unfolding divmod_def by simp |
|
129 lemma [code, code inline]: "(m < n) \<longleftrightarrow> (int m < int n)" |
113 by simp |
130 by simp |
114 |
131 lemma [code func, code inline]: "(m \<le> n) \<longleftrightarrow> (int m \<le> int n)" |
115 lemma [code func, code inline]: "m + n = nat_plus m n" |
132 by simp |
116 unfolding nat_plus_def by arith |
133 lemma [code func, code inline]: "OperationalEquality.eq m n \<longleftrightarrow> OperationalEquality.eq (int m) (int n)" |
117 lemma [code func, code inline]: "m - n = nat_minus m n" |
134 unfolding eq_def by simp |
118 unfolding nat_minus_def by arith |
135 lemma [code func]: "nat k = (if k < 0 then 0 else nat_of_int k)" |
119 lemma [code func, code inline]: "m * n = nat_mult m n" |
136 proof (cases "k < 0") |
120 unfolding nat_mult_def by (simp add: zmult_int) |
137 case True then show ?thesis by simp |
121 lemma [code func, code inline]: "m div n = nat_div m n" |
138 next |
122 unfolding nat_div_def div_def [symmetric] zdiv_int [symmetric] by simp |
139 case False then show ?thesis by (simp add: nat_of_int_def) |
123 lemma [code func, code inline]: "m mod n = nat_mod m n" |
140 qed |
124 unfolding nat_mod_def mod_def [symmetric] zmod_int [symmetric] by simp |
|
125 lemma [code func, code inline]: "(m < n) = nat_less m n" |
|
126 unfolding nat_less_def by simp |
|
127 lemma [code func, code inline]: "(m <= n) = nat_less_equal m n" |
|
128 unfolding nat_less_equal_def by simp |
|
129 lemma [code func, code inline]: "OperationalEquality.eq m n = nat_eq m n" |
|
130 unfolding nat_eq_def eq_def by simp |
|
131 lemma [code func]: |
141 lemma [code func]: |
132 "int_aux i n = (if nat_eq n 0 then i else int_aux (i + 1) (nat_minus n 1))" |
142 "int_aux i n = (if int n = 0 then i else int_aux (i + 1) (nat_of_int (int n - 1)))" |
133 unfolding nat_eq_def nat_minus_def int_aux_def by simp |
143 proof - |
|
144 have "0 < n \<Longrightarrow> int n = 1 + int (nat_of_int (int n - 1))" |
|
145 proof - |
|
146 assume prem: "n > 0" |
|
147 then have "int n - 1 \<ge> 0" by auto |
|
148 then have "nat_of_int (int n - 1) = nat (int n - 1)" by (simp add: nat_of_int_def) |
|
149 with prem show "int n = 1 + int (nat_of_int (int n - 1))" by simp |
|
150 qed |
|
151 then show ?thesis unfolding int_aux_def by simp |
|
152 qed |
134 |
153 |
135 |
154 |
136 subsection {* Preprocessors *} |
155 subsection {* Preprocessors *} |
137 |
156 |
138 text {* |
157 text {* |