equal
deleted
inserted
replaced
55 |
55 |
56 text {* Specialized @{term "op div \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat"} |
56 text {* Specialized @{term "op div \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat"} |
57 and @{term "op mod \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat"} operations. *} |
57 and @{term "op mod \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat"} operations. *} |
58 |
58 |
59 definition |
59 definition |
60 div_mod_nat_aux :: "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat" |
60 divmod_aux :: "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat" |
61 where |
61 where |
62 [code func del]: "div_mod_nat_aux = Divides.divmod" |
62 [code func del]: "divmod_aux = divmod" |
63 |
63 |
64 lemma [code func]: |
64 lemma [code func]: |
65 "Divides.divmod n m = (if m = 0 then (0, n) else div_mod_nat_aux n m)" |
65 "divmod n m = (if m = 0 then (0, n) else divmod_aux n m)" |
66 unfolding div_mod_nat_aux_def divmod_def by simp |
66 unfolding divmod_aux_def divmod_div_mod by simp |
67 |
67 |
68 lemma div_mod_aux_code [code]: |
68 lemma divmod_aux_code [code]: |
69 "div_mod_nat_aux n m = (nat (of_nat n div of_nat m), nat (of_nat n mod of_nat m))" |
69 "divmod_aux n m = (nat (of_nat n div of_nat m), nat (of_nat n mod of_nat m))" |
70 unfolding div_mod_nat_aux_def divmod_def zdiv_int [symmetric] zmod_int [symmetric] by simp |
70 unfolding divmod_aux_def divmod_div_mod zdiv_int [symmetric] zmod_int [symmetric] by simp |
71 |
71 |
72 lemma eq_nat_code [code]: |
72 lemma eq_nat_code [code]: |
73 "n = m \<longleftrightarrow> (of_nat n \<Colon> int) = of_nat m" |
73 "n = m \<longleftrightarrow> (of_nat n \<Colon> int) = of_nat m" |
74 by simp |
74 by simp |
75 |
75 |
386 code_const "op * \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat" |
386 code_const "op * \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat" |
387 (SML "IntInf.* ((_), (_))") |
387 (SML "IntInf.* ((_), (_))") |
388 (OCaml "Big'_int.mult'_big'_int") |
388 (OCaml "Big'_int.mult'_big'_int") |
389 (Haskell infixl 7 "*") |
389 (Haskell infixl 7 "*") |
390 |
390 |
391 code_const div_mod_nat_aux |
391 code_const divmod_aux |
392 (SML "IntInf.divMod/ ((_),/ (_))") |
392 (SML "IntInf.divMod/ ((_),/ (_))") |
393 (OCaml "Big'_int.quomod'_big'_int") |
393 (OCaml "Big'_int.quomod'_big'_int") |
394 (Haskell "divMod") |
394 (Haskell "divMod") |
395 |
395 |
396 code_const "op = \<Colon> nat \<Rightarrow> nat \<Rightarrow> bool" |
396 code_const "op = \<Colon> nat \<Rightarrow> nat \<Rightarrow> bool" |