src/HOL/Library/Code_Target_Int.thy
author haftmann
Sun Aug 18 15:29:50 2013 +0200 (2013-08-18)
changeset 53069 d165213e3924
parent 52435 6646bb548c6b
child 54227 63b441f49645
permissions -rw-r--r--
execution of int division by class semiring_numeral_div, replacing pdivmod by divmod_abs
     1 (*  Title:      HOL/Library/Code_Target_Int.thy
     2     Author:     Florian Haftmann, TU Muenchen
     3 *)
     4 
     5 header {* Implementation of integer numbers by target-language integers *}
     6 
     7 theory Code_Target_Int
     8 imports Main
     9 begin
    10 
    11 code_datatype int_of_integer
    12 
    13 lemma [code, code del]:
    14   "integer_of_int = integer_of_int" ..
    15 
    16 lemma [code]:
    17   "integer_of_int (int_of_integer k) = k"
    18   by transfer rule
    19 
    20 lemma [code]:
    21   "Int.Pos = int_of_integer \<circ> integer_of_num"
    22   by transfer (simp add: fun_eq_iff) 
    23 
    24 lemma [code]:
    25   "Int.Neg = int_of_integer \<circ> uminus \<circ> integer_of_num"
    26   by transfer (simp add: fun_eq_iff) 
    27 
    28 lemma [code_abbrev]:
    29   "int_of_integer (numeral k) = Int.Pos k"
    30   by transfer simp
    31 
    32 lemma [code_abbrev]:
    33   "int_of_integer (neg_numeral k) = Int.Neg k"
    34   by transfer simp
    35   
    36 lemma [code, symmetric, code_post]:
    37   "0 = int_of_integer 0"
    38   by transfer simp
    39 
    40 lemma [code, symmetric, code_post]:
    41   "1 = int_of_integer 1"
    42   by transfer simp
    43 
    44 lemma [code]:
    45   "k + l = int_of_integer (of_int k + of_int l)"
    46   by transfer simp
    47 
    48 lemma [code]:
    49   "- k = int_of_integer (- of_int k)"
    50   by transfer simp
    51 
    52 lemma [code]:
    53   "k - l = int_of_integer (of_int k - of_int l)"
    54   by transfer simp
    55 
    56 lemma [code]:
    57   "Int.dup k = int_of_integer (Code_Numeral.dup (of_int k))"
    58   by transfer simp
    59 
    60 lemma [code, code del]:
    61   "Int.sub = Int.sub" ..
    62 
    63 lemma [code]:
    64   "k * l = int_of_integer (of_int k * of_int l)"
    65   by simp
    66 
    67 lemma [code]:
    68   "Divides.divmod_abs k l = map_pair int_of_integer int_of_integer
    69     (Code_Numeral.divmod_abs (of_int k) (of_int l))"
    70   by (simp add: prod_eq_iff)
    71 
    72 lemma [code]:
    73   "k div l = int_of_integer (of_int k div of_int l)"
    74   by simp
    75 
    76 lemma [code]:
    77   "k mod l = int_of_integer (of_int k mod of_int l)"
    78   by simp
    79 
    80 lemma [code]:
    81   "HOL.equal k l = HOL.equal (of_int k :: integer) (of_int l)"
    82   by transfer (simp add: equal)
    83 
    84 lemma [code]:
    85   "k \<le> l \<longleftrightarrow> (of_int k :: integer) \<le> of_int l"
    86   by transfer rule
    87 
    88 lemma [code]:
    89   "k < l \<longleftrightarrow> (of_int k :: integer) < of_int l"
    90   by transfer rule
    91 
    92 lemma (in ring_1) of_int_code:
    93   "of_int k = (if k = 0 then 0
    94      else if k < 0 then - of_int (- k)
    95      else let
    96        (l, j) = divmod_int k 2;
    97        l' = 2 * of_int l
    98      in if j = 0 then l' else l' + 1)"
    99 proof -
   100   from mod_div_equality have *: "of_int k = of_int (k div 2 * 2 + k mod 2)" by simp
   101   show ?thesis
   102     by (simp add: Let_def divmod_int_mod_div mod_2_not_eq_zero_eq_one_int
   103       of_int_add [symmetric]) (simp add: * mult_commute)
   104 qed
   105 
   106 declare of_int_code [code]
   107 
   108 lemma [code]:
   109   "nat = nat_of_integer \<circ> of_int"
   110   by transfer (simp add: fun_eq_iff)
   111 
   112 code_identifier
   113   code_module Code_Target_Int \<rightharpoonup>
   114     (SML) Arith and (OCaml) Arith and (Haskell) Arith
   115 
   116 end
   117