src/HOL/Library/Efficient_Nat.thy
changeset 37958 9728342bcd56
parent 37947 844977c7abeb
child 37969 3bf1fffcdd48
     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")