src/HOL/Library/Code_Target_Int.thy
author haftmann
Sat Aug 08 10:51:33 2015 +0200 (2015-08-08)
changeset 60868 dd18c33c001e
parent 60500 903bb1495239
child 61275 053ec04ea866
permissions -rw-r--r--
direct bootstrap of integer division from natural division
     1 (*  Title:      HOL/Library/Code_Target_Int.thy
     2     Author:     Florian Haftmann, TU Muenchen
     3 *)
     4 
     5 section \<open>Implementation of integer numbers by target-language integers\<close>
     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 context
    16 includes integer.lifting
    17 begin
    18 
    19 lemma [code]:
    20   "integer_of_int (int_of_integer k) = k"
    21   by transfer rule
    22 
    23 lemma [code]:
    24   "Int.Pos = int_of_integer \<circ> integer_of_num"
    25   by transfer (simp add: fun_eq_iff) 
    26 
    27 lemma [code]:
    28   "Int.Neg = int_of_integer \<circ> uminus \<circ> integer_of_num"
    29   by transfer (simp add: fun_eq_iff) 
    30 
    31 lemma [code_abbrev]:
    32   "int_of_integer (numeral k) = Int.Pos k"
    33   by transfer simp
    34 
    35 lemma [code_abbrev]:
    36   "int_of_integer (- numeral k) = Int.Neg k"
    37   by transfer simp
    38   
    39 lemma [code, symmetric, code_post]:
    40   "0 = int_of_integer 0"
    41   by transfer simp
    42 
    43 lemma [code, symmetric, code_post]:
    44   "1 = int_of_integer 1"
    45   by transfer simp
    46 
    47 lemma [code_post]:
    48   "int_of_integer (- 1) = - 1"
    49   by 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   "- k = int_of_integer (- of_int k)"
    57   by transfer simp
    58 
    59 lemma [code]:
    60   "k - l = int_of_integer (of_int k - of_int l)"
    61   by transfer simp
    62 
    63 lemma [code]:
    64   "Int.dup k = int_of_integer (Code_Numeral.dup (of_int k))"
    65   by transfer simp
    66 
    67 declare [[code drop: Int.sub]]
    68 
    69 lemma [code]:
    70   "k * l = int_of_integer (of_int k * of_int l)"
    71   by simp
    72 
    73 lemma [code]:
    74   "k div l = int_of_integer (of_int k div of_int l)"
    75   by simp
    76 
    77 lemma [code]:
    78   "k mod l = int_of_integer (of_int k mod of_int l)"
    79   by simp
    80 
    81 lemma [code]:
    82   "HOL.equal k l = HOL.equal (of_int k :: integer) (of_int l)"
    83   by transfer (simp add: equal)
    84 
    85 lemma [code]:
    86   "k \<le> l \<longleftrightarrow> (of_int k :: integer) \<le> of_int l"
    87   by transfer rule
    88 
    89 lemma [code]:
    90   "k < l \<longleftrightarrow> (of_int k :: integer) < of_int l"
    91   by transfer rule
    92 end
    93 
    94 lemma (in ring_1) of_int_code_if:
    95   "of_int k = (if k = 0 then 0
    96      else if k < 0 then - of_int (- k)
    97      else let
    98        l = 2 * of_int (k div 2);
    99        j = k mod 2
   100      in if j = 0 then l else l + 1)"
   101 proof -
   102   from mod_div_equality have *: "of_int k = of_int (k div 2 * 2 + k mod 2)" by simp
   103   show ?thesis
   104     by (simp add: Let_def of_int_add [symmetric]) (simp add: * mult.commute)
   105 qed
   106 
   107 declare of_int_code_if [code]
   108 
   109 lemma [code]:
   110   "nat = nat_of_integer \<circ> of_int"
   111   including integer.lifting by transfer (simp add: fun_eq_iff)
   112 
   113 code_identifier
   114   code_module Code_Target_Int \<rightharpoonup>
   115     (SML) Arith and (OCaml) Arith and (Haskell) Arith
   116 
   117 end