1.1 --- a/src/HOL/Library/Efficient_Nat.thy Fri Jul 23 18:42:46 2010 +0200
1.2 +++ b/src/HOL/Library/Efficient_Nat.thy Sat Jul 24 18:08:41 2010 +0200
1.3 @@ -50,19 +50,9 @@
1.4 "n * m = nat (of_nat n * of_nat m)"
1.5 unfolding of_nat_mult [symmetric] by simp
1.6
1.7 -text {* Specialized @{term "op div \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat"}
1.8 - and @{term "op mod \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat"} operations. *}
1.9 -
1.10 -definition divmod_aux :: "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat" where
1.11 - [code del]: "divmod_aux = divmod_nat"
1.12 -
1.13 -lemma [code]:
1.14 - "divmod_nat n m = (if m = 0 then (0, n) else divmod_aux n m)"
1.15 - unfolding divmod_aux_def divmod_nat_div_mod by simp
1.16 -
1.17 -lemma divmod_aux_code [code]:
1.18 - "divmod_aux n m = (nat (of_nat n div of_nat m), nat (of_nat n mod of_nat m))"
1.19 - unfolding divmod_aux_def divmod_nat_div_mod zdiv_int [symmetric] zmod_int [symmetric] by simp
1.20 +lemma divmod_nat_code [code]:
1.21 + "divmod_nat n m = prod_fun nat nat (pdivmod (of_nat n) (of_nat m))"
1.22 + by (simp add: prod_fun_def split_def pdivmod_def nat_div_distrib nat_mod_distrib divmod_nat_div_mod)
1.23
1.24 lemma eq_nat_code [code]:
1.25 "eq_class.eq n m \<longleftrightarrow> eq_class.eq (of_nat n \<Colon> int) (of_nat m)"
1.26 @@ -233,6 +223,7 @@
1.27 code_type nat
1.28 (SML "IntInf.int")
1.29 (OCaml "Big'_int.big'_int")
1.30 + (Eval "int")
1.31
1.32 types_code
1.33 nat ("int")
1.34 @@ -281,7 +272,9 @@
1.35 instance Integral Nat where {
1.36 toInteger (Nat n) = n;
1.37 divMod n m = quotRem n m;
1.38 - quotRem (Nat n) (Nat m) = (Nat k, Nat l) where (k, l) = quotRem n m;
1.39 + quotRem (Nat n) (Nat m)
1.40 + | (m == 0) = (0, Nat n)
1.41 + | otherwise = (Nat k, Nat l) where (k, l) = quotRem n m;
1.42 };
1.43 *}
1.44
1.45 @@ -353,9 +346,7 @@
1.46
1.47 setup {*
1.48 fold (Numeral.add_code @{const_name number_nat_inst.number_of_nat}
1.49 - false Code_Printer.literal_positive_numeral) ["SML", "OCaml", "Haskell"]
1.50 - #> Numeral.add_code @{const_name number_nat_inst.number_of_nat}
1.51 - false Code_Printer.literal_positive_numeral "Scala"
1.52 + false Code_Printer.literal_positive_numeral) ["SML", "OCaml", "Haskell", "Scala"]
1.53 *}
1.54
1.55 text {*
1.56 @@ -400,6 +391,7 @@
1.57 code_const nat
1.58 (SML "IntInf.max/ (/0,/ _)")
1.59 (OCaml "Big'_int.max'_big'_int/ Big'_int.zero'_big'_int")
1.60 + (Eval "Integer.max/ _/ 0")
1.61
1.62 text {* For Haskell and Scala, things are slightly different again. *}
1.63
1.64 @@ -407,19 +399,21 @@
1.65 (Haskell "toInteger" and "fromInteger")
1.66 (Scala "!_.as'_BigInt" and "Nat")
1.67
1.68 -text {* Conversion from and to indices. *}
1.69 +text {* Conversion from and to code numerals. *}
1.70
1.71 code_const Code_Numeral.of_nat
1.72 (SML "IntInf.toInt")
1.73 (OCaml "_")
1.74 - (Haskell "toInteger")
1.75 - (Scala "!_.as'_Int")
1.76 + (Haskell "!(fromInteger/ ./ toInteger)")
1.77 + (Scala "!Natural(_.as'_BigInt)")
1.78 + (Eval "_")
1.79
1.80 code_const Code_Numeral.nat_of
1.81 (SML "IntInf.fromInt")
1.82 (OCaml "_")
1.83 - (Haskell "fromInteger")
1.84 - (Scala "Nat")
1.85 + (Haskell "!(fromInteger/ ./ toInteger)")
1.86 + (Scala "!Nat(_.as'_BigInt)")
1.87 + (Eval "_")
1.88
1.89 text {* Using target language arithmetic operations whenever appropriate *}
1.90
1.91 @@ -428,6 +422,7 @@
1.92 (OCaml "Big'_int.add'_big'_int")
1.93 (Haskell infixl 6 "+")
1.94 (Scala infixl 7 "+")
1.95 + (Eval infixl 8 "+")
1.96
1.97 code_const "op - \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat"
1.98 (Haskell infixl 6 "-")
1.99 @@ -438,34 +433,35 @@
1.100 (OCaml "Big'_int.mult'_big'_int")
1.101 (Haskell infixl 7 "*")
1.102 (Scala infixl 8 "*")
1.103 + (Eval infixl 9 "*")
1.104
1.105 -code_const divmod_aux
1.106 +code_const divmod_nat
1.107 (SML "IntInf.divMod/ ((_),/ (_))")
1.108 (OCaml "Big'_int.quomod'_big'_int")
1.109 (Haskell "divMod")
1.110 (Scala infixl 8 "/%")
1.111 -
1.112 -code_const divmod_nat
1.113 - (Haskell "divMod")
1.114 - (Scala infixl 8 "/%")
1.115 + (Eval "Integer.div'_mod")
1.116
1.117 code_const "eq_class.eq \<Colon> nat \<Rightarrow> nat \<Rightarrow> bool"
1.118 (SML "!((_ : IntInf.int) = _)")
1.119 (OCaml "Big'_int.eq'_big'_int")
1.120 (Haskell infixl 4 "==")
1.121 (Scala infixl 5 "==")
1.122 + (Eval infixl 6 "=")
1.123
1.124 code_const "op \<le> \<Colon> nat \<Rightarrow> nat \<Rightarrow> bool"
1.125 (SML "IntInf.<= ((_), (_))")
1.126 (OCaml "Big'_int.le'_big'_int")
1.127 (Haskell infix 4 "<=")
1.128 (Scala infixl 4 "<=")
1.129 + (Eval infixl 6 "<=")
1.130
1.131 code_const "op < \<Colon> nat \<Rightarrow> nat \<Rightarrow> bool"
1.132 (SML "IntInf.< ((_), (_))")
1.133 (OCaml "Big'_int.lt'_big'_int")
1.134 (Haskell infix 4 "<")
1.135 (Scala infixl 4 "<")
1.136 + (Eval infixl 6 "<")
1.137
1.138 consts_code
1.139 "0::nat" ("0")