src/HOL/Library/Code_Target_Int.thy
 author haftmann Thu Oct 31 11:44:20 2013 +0100 (2013-10-31) changeset 54227 63b441f49645 parent 53069 d165213e3924 child 54489 03ff4d1e6784 permissions -rw-r--r--
moving generic lemmas out of theory parity, disregarding some unused auxiliary lemmas;
tuned presburger
```     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 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 transfer rule
```
```    19
```
```    20 lemma [code]:
```
```    21   "Int.Pos = int_of_integer \<circ> integer_of_num"
```
```    22   by transfer (simp add: fun_eq_iff)
```
```    23
```
```    24 lemma [code]:
```
```    25   "Int.Neg = int_of_integer \<circ> uminus \<circ> integer_of_num"
```
```    26   by transfer (simp add: fun_eq_iff)
```
```    27
```
```    28 lemma [code_abbrev]:
```
```    29   "int_of_integer (numeral k) = Int.Pos k"
```
```    30   by transfer simp
```
```    31
```
```    32 lemma [code_abbrev]:
```
```    33   "int_of_integer (neg_numeral k) = Int.Neg k"
```
```    34   by transfer simp
```
```    35
```
```    36 lemma [code, symmetric, code_post]:
```
```    37   "0 = int_of_integer 0"
```
```    38   by transfer simp
```
```    39
```
```    40 lemma [code, symmetric, code_post]:
```
```    41   "1 = int_of_integer 1"
```
```    42   by transfer simp
```
```    43
```
```    44 lemma [code]:
```
```    45   "k + l = int_of_integer (of_int k + of_int l)"
```
```    46   by transfer simp
```
```    47
```
```    48 lemma [code]:
```
```    49   "- k = int_of_integer (- of_int k)"
```
```    50   by transfer simp
```
```    51
```
```    52 lemma [code]:
```
```    53   "k - l = int_of_integer (of_int k - of_int l)"
```
```    54   by transfer simp
```
```    55
```
```    56 lemma [code]:
```
```    57   "Int.dup k = int_of_integer (Code_Numeral.dup (of_int k))"
```
```    58   by transfer 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   "Divides.divmod_abs k l = map_pair int_of_integer int_of_integer
```
```    69     (Code_Numeral.divmod_abs (of_int k) (of_int l))"
```
```    70   by (simp add: prod_eq_iff)
```
```    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 transfer (simp add: equal)
```
```    83
```
```    84 lemma [code]:
```
```    85   "k \<le> l \<longleftrightarrow> (of_int k :: integer) \<le> of_int l"
```
```    86   by transfer rule
```
```    87
```
```    88 lemma [code]:
```
```    89   "k < l \<longleftrightarrow> (of_int k :: integer) < of_int l"
```
```    90   by transfer rule
```
```    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 not_mod_2_eq_0_eq_1
```
```   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 transfer (simp add: fun_eq_iff)
```
```   111
```
```   112 code_identifier
```
```   113   code_module Code_Target_Int \<rightharpoonup>
```
```   114     (SML) Arith and (OCaml) Arith and (Haskell) Arith
```
```   115
```
```   116 end
```
```   117
```