1.1 --- a/src/HOL/Library/Code_Integer.thy	Sat Mar 24 16:27:04 2012 +0100
     1.2 +++ b/src/HOL/Library/Code_Integer.thy	Sun Mar 25 20:15:39 2012 +0200
     1.3 @@ -9,6 +9,43 @@
     1.4  begin
     1.5  
     1.6  text {*
     1.7 +  Representation-ignorant code equations for conversions.
     1.8 +*}
     1.9 +
    1.10 +lemma nat_code [code]:
    1.11 +  "nat k = (if k \<le> 0 then 0 else
    1.12 +     let
    1.13 +       (l, j) = divmod_int k 2;
    1.14 +       l' = 2 * nat l
    1.15 +     in if j = 0 then l' else Suc l')"
    1.16 +proof -
    1.17 +  have "2 = nat 2" by simp
    1.18 +  show ?thesis
    1.19 +    apply (auto simp add: Let_def divmod_int_mod_div not_le
    1.20 +     nat_div_distrib nat_mult_distrib mult_div_cancel mod_2_not_eq_zero_eq_one_int)
    1.21 +    apply (unfold `2 = nat 2`)
    1.22 +    apply (subst nat_mod_distrib [symmetric])
    1.23 +    apply simp_all
    1.24 +  done
    1.25 +qed
    1.26 +
    1.27 +lemma (in ring_1) of_int_code:
    1.28 +  "of_int k = (if k = 0 then 0
    1.29 +     else if k < 0 then - of_int (- k)
    1.30 +     else let
    1.31 +       (l, j) = divmod_int k 2;
    1.32 +       l' = 2 * of_int l
    1.33 +     in if j = 0 then l' else l' + 1)"
    1.34 +proof -
    1.35 +  from mod_div_equality have *: "of_int k = of_int (k div 2 * 2 + k mod 2)" by simp
    1.36 +  show ?thesis
    1.37 +    by (simp add: Let_def divmod_int_mod_div mod_2_not_eq_zero_eq_one_int
    1.38 +      of_int_add [symmetric]) (simp add: * mult_commute)
    1.39 +qed
    1.40 +
    1.41 +declare of_int_code [code]
    1.42 +
    1.43 +text {*
    1.44    HOL numeral expressions are mapped to integer literals
    1.45    in target languages, using predefined target language
    1.46    operations for abstract integer operations.
    1.47 @@ -24,43 +61,22 @@
    1.48  code_instance int :: equal
    1.49    (Haskell -)
    1.50  
    1.51 +code_const "0::int"
    1.52 +  (SML "0")
    1.53 +  (OCaml "Big'_int.zero'_big'_int")
    1.54 +  (Haskell "0")
    1.55 +  (Scala "BigInt(0)")
    1.56 +
    1.57  setup {*
    1.58 -  fold (Numeral.add_code @{const_name number_int_inst.number_of_int}
    1.59 +  fold (Numeral.add_code @{const_name Int.Pos}
    1.60 +    false Code_Printer.literal_numeral) ["SML", "OCaml", "Haskell", "Scala"]
    1.61 +*}
    1.62 +
    1.63 +setup {*
    1.64 +  fold (Numeral.add_code @{const_name Int.Neg}
    1.65      true Code_Printer.literal_numeral) ["SML", "OCaml", "Haskell", "Scala"]
    1.66  *}
    1.67  
    1.68 -code_const "Int.Pls" and "Int.Min" and "Int.Bit0" and "Int.Bit1"
    1.69 -  (SML "raise/ Fail/ \"Pls\""
    1.70 -     and "raise/ Fail/ \"Min\""
    1.71 -     and "!((_);/ raise/ Fail/ \"Bit0\")"
    1.72 -     and "!((_);/ raise/ Fail/ \"Bit1\")")
    1.73 -  (OCaml "failwith/ \"Pls\""
    1.74 -     and "failwith/ \"Min\""
    1.75 -     and "!((_);/ failwith/ \"Bit0\")"
    1.76 -     and "!((_);/ failwith/ \"Bit1\")")
    1.77 -  (Haskell "error/ \"Pls\""
    1.78 -     and "error/ \"Min\""
    1.79 -     and "error/ \"Bit0\""
    1.80 -     and "error/ \"Bit1\"")
    1.81 -  (Scala "!error(\"Pls\")"
    1.82 -     and "!error(\"Min\")"
    1.83 -     and "!error(\"Bit0\")"
    1.84 -     and "!error(\"Bit1\")")
    1.85 -
    1.86 -code_const Int.pred
    1.87 -  (SML "IntInf.- ((_), 1)")
    1.88 -  (OCaml "Big'_int.pred'_big'_int")
    1.89 -  (Haskell "!(_/ -/ 1)")
    1.90 -  (Scala "!(_ -/ 1)")
    1.91 -  (Eval "!(_/ -/ 1)")
    1.92 -
    1.93 -code_const Int.succ
    1.94 -  (SML "IntInf.+ ((_), 1)")
    1.95 -  (OCaml "Big'_int.succ'_big'_int")
    1.96 -  (Haskell "!(_/ +/ 1)")
    1.97 -  (Scala "!(_ +/ 1)")
    1.98 -  (Eval "!(_/ +/ 1)")
    1.99 -
   1.100  code_const "op + \<Colon> int \<Rightarrow> int \<Rightarrow> int"
   1.101    (SML "IntInf.+ ((_), (_))")
   1.102    (OCaml "Big'_int.add'_big'_int")
   1.103 @@ -82,6 +98,19 @@
   1.104    (Scala infixl 7 "-")
   1.105    (Eval infixl 8 "-")
   1.106  
   1.107 +code_const Int.dup
   1.108 +  (SML "IntInf.*/ (2,/ (_))")
   1.109 +  (OCaml "Big'_int.mult'_big'_int/ 2")
   1.110 +  (Haskell "!(2 * _)")
   1.111 +  (Scala "!(2 * _)")
   1.112 +  (Eval "!(2 * _)")
   1.113 +
   1.114 +code_const Int.sub
   1.115 +  (SML "!(raise/ Fail/ \"sub\")")
   1.116 +  (OCaml "failwith/ \"sub\"")
   1.117 +  (Haskell "error/ \"sub\"")
   1.118 +  (Scala "!error(\"sub\")")
   1.119 +
   1.120  code_const "op * \<Colon> int \<Rightarrow> int \<Rightarrow> int"
   1.121    (SML "IntInf.* ((_), (_))")
   1.122    (OCaml "Big'_int.mult'_big'_int")
   1.123 @@ -124,9 +153,7 @@
   1.124    (Scala "!_.as'_BigInt")
   1.125    (Eval "_")
   1.126  
   1.127 -text {* Evaluation *}
   1.128 -
   1.129  code_const "Code_Evaluation.term_of \<Colon> int \<Rightarrow> term"
   1.130    (Eval "HOLogic.mk'_number/ HOLogic.intT")
   1.131  
   1.132 -end
   1.133 \ No newline at end of file
   1.134 +end