src/HOL/Library/Code_Target_Int.thy
changeset 50023 28f3263d4d1b
child 51095 7ae79f2e3cc7
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Library/Code_Target_Int.thy	Thu Nov 08 10:02:38 2012 +0100
     1.3 @@ -0,0 +1,122 @@
     1.4 +(*  Title:      HOL/Library/Code_Target_Int.thy
     1.5 +    Author:     Florian Haftmann, TU Muenchen
     1.6 +*)
     1.7 +
     1.8 +header {* Implementation of integer numbers by target-language integers *}
     1.9 +
    1.10 +theory Code_Target_Int
    1.11 +imports Main "~~/src/HOL/Library/Code_Numeral_Types"
    1.12 +begin
    1.13 +
    1.14 +code_datatype int_of_integer
    1.15 +
    1.16 +lemma [code, code del]:
    1.17 +  "integer_of_int = integer_of_int" ..
    1.18 +
    1.19 +lemma [code]:
    1.20 +  "integer_of_int (int_of_integer k) = k"
    1.21 +  by (simp add: integer_eq_iff)
    1.22 +
    1.23 +lemma [code]:
    1.24 +  "Int.Pos = int_of_integer \<circ> integer_of_num"
    1.25 +  by (simp add: integer_of_num_def fun_eq_iff)
    1.26 +
    1.27 +lemma [code]:
    1.28 +  "Int.Neg = int_of_integer \<circ> uminus \<circ> integer_of_num"
    1.29 +  by (simp add: integer_of_num_def fun_eq_iff)
    1.30 +
    1.31 +lemma [code_abbrev]:
    1.32 +  "int_of_integer (Code_Numeral_Types.Pos k) = Int.Pos k"
    1.33 +  by simp
    1.34 +
    1.35 +lemma [code_abbrev]:
    1.36 +  "int_of_integer (Code_Numeral_Types.Neg k) = Int.Neg k"
    1.37 +  by simp
    1.38 +
    1.39 +lemma [code]:
    1.40 +  "0 = int_of_integer 0"
    1.41 +  by simp
    1.42 +
    1.43 +lemma [code]:
    1.44 +  "1 = int_of_integer 1"
    1.45 +  by simp
    1.46 +
    1.47 +lemma [code]:
    1.48 +  "k + l = int_of_integer (of_int k + of_int l)"
    1.49 +  by simp
    1.50 +
    1.51 +lemma [code]:
    1.52 +  "- k = int_of_integer (- of_int k)"
    1.53 +  by simp
    1.54 +
    1.55 +lemma [code]:
    1.56 +  "k - l = int_of_integer (of_int k - of_int l)"
    1.57 +  by simp
    1.58 +
    1.59 +lemma [code]:
    1.60 +  "Int.dup k = int_of_integer (Code_Numeral_Types.dup (of_int k))"
    1.61 +  by simp
    1.62 +
    1.63 +lemma [code, code del]:
    1.64 +  "Int.sub = Int.sub" ..
    1.65 +
    1.66 +lemma [code]:
    1.67 +  "k * l = int_of_integer (of_int k * of_int l)"
    1.68 +  by simp
    1.69 +
    1.70 +lemma [code]:
    1.71 +  "pdivmod k l = map_pair int_of_integer int_of_integer
    1.72 +    (Code_Numeral_Types.divmod_abs (of_int k) (of_int l))"
    1.73 +  by (simp add: prod_eq_iff pdivmod_def)
    1.74 +
    1.75 +lemma [code]:
    1.76 +  "k div l = int_of_integer (of_int k div of_int l)"
    1.77 +  by simp
    1.78 +
    1.79 +lemma [code]:
    1.80 +  "k mod l = int_of_integer (of_int k mod of_int l)"
    1.81 +  by simp
    1.82 +
    1.83 +lemma [code]:
    1.84 +  "HOL.equal k l = HOL.equal (of_int k :: integer) (of_int l)"
    1.85 +  by (simp add: equal integer_eq_iff)
    1.86 +
    1.87 +lemma [code]:
    1.88 +  "k \<le> l \<longleftrightarrow> (of_int k :: integer) \<le> of_int l"
    1.89 +  by (simp add: less_eq_int_def)
    1.90 +
    1.91 +lemma [code]:
    1.92 +  "k < l \<longleftrightarrow> (of_int k :: integer) < of_int l"
    1.93 +  by (simp add: less_int_def)
    1.94 +
    1.95 +lemma (in ring_1) of_int_code:
    1.96 +  "of_int k = (if k = 0 then 0
    1.97 +     else if k < 0 then - of_int (- k)
    1.98 +     else let
    1.99 +       (l, j) = divmod_int k 2;
   1.100 +       l' = 2 * of_int l
   1.101 +     in if j = 0 then l' else l' + 1)"
   1.102 +proof -
   1.103 +  from mod_div_equality have *: "of_int k = of_int (k div 2 * 2 + k mod 2)" by simp
   1.104 +  show ?thesis
   1.105 +    by (simp add: Let_def divmod_int_mod_div mod_2_not_eq_zero_eq_one_int
   1.106 +      of_int_add [symmetric]) (simp add: * mult_commute)
   1.107 +qed
   1.108 +
   1.109 +declare of_int_code [code]
   1.110 +
   1.111 +lemma [code]:
   1.112 +  "nat = nat_of_integer \<circ> of_int"
   1.113 +  by (simp add: fun_eq_iff nat_of_integer_def)
   1.114 +
   1.115 +code_modulename SML
   1.116 +  Code_Target_Int Arith
   1.117 +
   1.118 +code_modulename OCaml
   1.119 +  Code_Target_Int Arith
   1.120 +
   1.121 +code_modulename Haskell
   1.122 +  Code_Target_Int Arith
   1.123 +
   1.124 +end
   1.125 +