src/HOL/Library/Code_Target_Int.thy
author Christian Sternagel
Thu Dec 13 13:11:38 2012 +0100 (2012-12-13)
changeset 50516 ed6b40d15d1c
parent 50023 28f3263d4d1b
child 51095 7ae79f2e3cc7
permissions -rw-r--r--
renamed "emb" to "list_hembeq";
make "list_hembeq" reflexive independent of the base order;
renamed "sub" to "sublisteq";
dropped "transp_on" (state transitivity explicitly instead);
no need to hide "sub" after renaming;
replaced some ASCII symbols by proper Isabelle symbols;
NEWS
     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 "~~/src/HOL/Library/Code_Numeral_Types"
     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 (simp add: integer_eq_iff)
    19 
    20 lemma [code]:
    21   "Int.Pos = int_of_integer \<circ> integer_of_num"
    22   by (simp add: integer_of_num_def fun_eq_iff)
    23 
    24 lemma [code]:
    25   "Int.Neg = int_of_integer \<circ> uminus \<circ> integer_of_num"
    26   by (simp add: integer_of_num_def fun_eq_iff)
    27 
    28 lemma [code_abbrev]:
    29   "int_of_integer (Code_Numeral_Types.Pos k) = Int.Pos k"
    30   by simp
    31 
    32 lemma [code_abbrev]:
    33   "int_of_integer (Code_Numeral_Types.Neg k) = Int.Neg k"
    34   by simp
    35 
    36 lemma [code]:
    37   "0 = int_of_integer 0"
    38   by simp
    39 
    40 lemma [code]:
    41   "1 = int_of_integer 1"
    42   by simp
    43 
    44 lemma [code]:
    45   "k + l = int_of_integer (of_int k + of_int l)"
    46   by simp
    47 
    48 lemma [code]:
    49   "- k = int_of_integer (- of_int k)"
    50   by simp
    51 
    52 lemma [code]:
    53   "k - l = int_of_integer (of_int k - of_int l)"
    54   by simp
    55 
    56 lemma [code]:
    57   "Int.dup k = int_of_integer (Code_Numeral_Types.dup (of_int k))"
    58   by 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   "pdivmod k l = map_pair int_of_integer int_of_integer
    69     (Code_Numeral_Types.divmod_abs (of_int k) (of_int l))"
    70   by (simp add: prod_eq_iff pdivmod_def)
    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 (simp add: equal integer_eq_iff)
    83 
    84 lemma [code]:
    85   "k \<le> l \<longleftrightarrow> (of_int k :: integer) \<le> of_int l"
    86   by (simp add: less_eq_int_def)
    87 
    88 lemma [code]:
    89   "k < l \<longleftrightarrow> (of_int k :: integer) < of_int l"
    90   by (simp add: less_int_def)
    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 (simp add: fun_eq_iff nat_of_integer_def)
   111 
   112 code_modulename SML
   113   Code_Target_Int Arith
   114 
   115 code_modulename OCaml
   116   Code_Target_Int Arith
   117 
   118 code_modulename Haskell
   119   Code_Target_Int Arith
   120 
   121 end
   122