src/HOL/Library/Code_Target_Int.thy
author haftmann
Wed Jan 01 11:35:21 2014 +0100 (2014-01-01)
changeset 54891 2f4491f15fe6
parent 54796 cdc6d8cbf770
child 55736 f1ed1e9cd080
permissions -rw-r--r--
examples how to avoid the "code, code del" antipattern
     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 declare [[code drop: integer_of_int]]
    14 
    15 lemma [code]:
    16   "integer_of_int (int_of_integer k) = k"
    17   by transfer rule
    18 
    19 lemma [code]:
    20   "Int.Pos = int_of_integer \<circ> integer_of_num"
    21   by transfer (simp add: fun_eq_iff) 
    22 
    23 lemma [code]:
    24   "Int.Neg = int_of_integer \<circ> uminus \<circ> integer_of_num"
    25   by transfer (simp add: fun_eq_iff) 
    26 
    27 lemma [code_abbrev]:
    28   "int_of_integer (numeral k) = Int.Pos k"
    29   by transfer simp
    30 
    31 lemma [code_abbrev]:
    32   "int_of_integer (- numeral k) = Int.Neg k"
    33   by transfer simp
    34   
    35 lemma [code, symmetric, code_post]:
    36   "0 = int_of_integer 0"
    37   by transfer simp
    38 
    39 lemma [code, symmetric, code_post]:
    40   "1 = int_of_integer 1"
    41   by transfer simp
    42 
    43 lemma [code]:
    44   "k + l = int_of_integer (of_int k + of_int l)"
    45   by transfer simp
    46 
    47 lemma [code]:
    48   "- k = int_of_integer (- of_int k)"
    49   by transfer simp
    50 
    51 lemma [code]:
    52   "k - l = int_of_integer (of_int k - of_int l)"
    53   by transfer simp
    54 
    55 lemma [code]:
    56   "Int.dup k = int_of_integer (Code_Numeral.dup (of_int k))"
    57   by transfer simp
    58 
    59 declare [[code drop: Int.sub]]
    60 
    61 lemma [code]:
    62   "k * l = int_of_integer (of_int k * of_int l)"
    63   by simp
    64 
    65 lemma [code]:
    66   "Divides.divmod_abs k l = map_pair int_of_integer int_of_integer
    67     (Code_Numeral.divmod_abs (of_int k) (of_int l))"
    68   by (simp add: prod_eq_iff)
    69 
    70 lemma [code]:
    71   "k div l = int_of_integer (of_int k div of_int l)"
    72   by simp
    73 
    74 lemma [code]:
    75   "k mod l = int_of_integer (of_int k mod of_int l)"
    76   by simp
    77 
    78 lemma [code]:
    79   "HOL.equal k l = HOL.equal (of_int k :: integer) (of_int l)"
    80   by transfer (simp add: equal)
    81 
    82 lemma [code]:
    83   "k \<le> l \<longleftrightarrow> (of_int k :: integer) \<le> of_int l"
    84   by transfer rule
    85 
    86 lemma [code]:
    87   "k < l \<longleftrightarrow> (of_int k :: integer) < of_int l"
    88   by transfer rule
    89 
    90 lemma (in ring_1) of_int_code_if:
    91   "of_int k = (if k = 0 then 0
    92      else if k < 0 then - of_int (- k)
    93      else let
    94        (l, j) = divmod_int k 2;
    95        l' = 2 * of_int l
    96      in if j = 0 then l' else l' + 1)"
    97 proof -
    98   from mod_div_equality have *: "of_int k = of_int (k div 2 * 2 + k mod 2)" by simp
    99   show ?thesis
   100     by (simp add: Let_def divmod_int_mod_div of_int_add [symmetric])
   101       (simp add: * mult_commute)
   102 qed
   103 
   104 declare of_int_code_if [code]
   105 
   106 lemma [code]:
   107   "nat = nat_of_integer \<circ> of_int"
   108   by transfer (simp add: fun_eq_iff)
   109 
   110 code_identifier
   111   code_module Code_Target_Int \<rightharpoonup>
   112     (SML) Arith and (OCaml) Arith and (Haskell) Arith
   113 
   114 end
   115