equal
deleted
inserted
replaced
245 |
245 |
246 lemma nat_of_code [code]: |
246 lemma nat_of_code [code]: |
247 "nat_of i = nat_of_aux i 0" |
247 "nat_of i = nat_of_aux i 0" |
248 by (simp add: nat_of_aux_def) |
248 by (simp add: nat_of_aux_def) |
249 |
249 |
250 definition div_mod_code_numeral :: "code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral \<times> code_numeral" where |
250 definition div_mod_code_numeral :: "code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral \<times> code_numeral" where |
251 [code del]: "div_mod_code_numeral n m = (n div m, n mod m)" |
251 [code del]: "div_mod_code_numeral n m = (n div m, n mod m)" |
252 |
252 |
253 lemma [code]: |
253 lemma [code]: |
254 "div_mod_code_numeral n m = (if m = 0 then (0, n) else (n div m, n mod m))" |
254 "div_mod_code_numeral n m = (if m = 0 then (0, n) else (n div m, n mod m))" |
255 unfolding div_mod_code_numeral_def by auto |
255 unfolding div_mod_code_numeral_def by auto |