src/HOL/Library/Code_Target_Int.thy
author haftmann
Mon Jun 05 15:59:41 2017 +0200 (2017-06-05)
changeset 66010 2f7d39285a1a
parent 65552 f533820e7248
child 68028 1f9f973eed2a
permissions -rw-r--r--
executable domain membership checks
     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 context
    40 begin
    41 
    42 qualified definition positive :: "num \<Rightarrow> int"
    43   where [simp]: "positive = numeral"
    44 
    45 qualified definition negative :: "num \<Rightarrow> int"
    46   where [simp]: "negative = uminus \<circ> numeral"
    47 
    48 lemma [code_computation_unfold]:
    49   "numeral = positive"
    50   "Int.Pos = positive"
    51   "Int.Neg = negative"
    52   by (simp_all add: fun_eq_iff)
    53 
    54 end
    55 
    56 lemma [code, symmetric, code_post]:
    57   "0 = int_of_integer 0"
    58   by transfer simp
    59 
    60 lemma [code, symmetric, code_post]:
    61   "1 = int_of_integer 1"
    62   by transfer simp
    63 
    64 lemma [code_post]:
    65   "int_of_integer (- 1) = - 1"
    66   by simp
    67 
    68 lemma [code]:
    69   "k + l = int_of_integer (of_int k + of_int l)"
    70   by transfer simp
    71 
    72 lemma [code]:
    73   "- k = int_of_integer (- of_int k)"
    74   by transfer simp
    75 
    76 lemma [code]:
    77   "k - l = int_of_integer (of_int k - of_int l)"
    78   by transfer simp
    79 
    80 lemma [code]:
    81   "Int.dup k = int_of_integer (Code_Numeral.dup (of_int k))"
    82   by transfer simp
    83 
    84 declare [[code drop: Int.sub]]
    85 
    86 lemma [code]:
    87   "k * l = int_of_integer (of_int k * of_int l)"
    88   by simp
    89 
    90 lemma [code]:
    91   "k div l = int_of_integer (of_int k div of_int l)"
    92   by simp
    93 
    94 lemma [code]:
    95   "k mod l = int_of_integer (of_int k mod of_int l)"
    96   by simp
    97 
    98 lemma [code]:
    99   "divmod m n = map_prod int_of_integer int_of_integer (divmod m n)"
   100   unfolding prod_eq_iff divmod_def map_prod_def case_prod_beta fst_conv snd_conv
   101   by transfer simp
   102 
   103 lemma [code]:
   104   "HOL.equal k l = HOL.equal (of_int k :: integer) (of_int l)"
   105   by transfer (simp add: equal)
   106 
   107 lemma [code]:
   108   "k \<le> l \<longleftrightarrow> (of_int k :: integer) \<le> of_int l"
   109   by transfer rule
   110 
   111 lemma [code]:
   112   "k < l \<longleftrightarrow> (of_int k :: integer) < of_int l"
   113   by transfer rule
   114 
   115 declare [[code drop: "gcd :: int \<Rightarrow> _" "lcm :: int \<Rightarrow> _"]]
   116 
   117 lemma gcd_int_of_integer [code]:
   118   "gcd (int_of_integer x) (int_of_integer y) = int_of_integer (gcd x y)"
   119 by transfer rule
   120 
   121 lemma lcm_int_of_integer [code]:
   122   "lcm (int_of_integer x) (int_of_integer y) = int_of_integer (lcm x y)"
   123 by transfer rule
   124 
   125 end
   126 
   127 lemma (in ring_1) of_int_code_if:
   128   "of_int k = (if k = 0 then 0
   129      else if k < 0 then - of_int (- k)
   130      else let
   131        l = 2 * of_int (k div 2);
   132        j = k mod 2
   133      in if j = 0 then l else l + 1)"
   134 proof -
   135   from div_mult_mod_eq have *: "of_int k = of_int (k div 2 * 2 + k mod 2)" by simp
   136   show ?thesis
   137     by (simp add: Let_def of_int_add [symmetric]) (simp add: * mult.commute)
   138 qed
   139 
   140 declare of_int_code_if [code]
   141 
   142 lemma [code]:
   143   "nat = nat_of_integer \<circ> of_int"
   144   including integer.lifting by transfer (simp add: fun_eq_iff)
   145 
   146 code_identifier
   147   code_module Code_Target_Int \<rightharpoonup>
   148     (SML) Arith and (OCaml) Arith and (Haskell) Arith
   149 
   150 end