src/HOL/Library/Code_Target_Int.thy
 author haftmann Fri Mar 22 19:18:08 2019 +0000 (3 months ago) changeset 69946 494934c30f38 parent 68028 1f9f973eed2a permissions -rw-r--r--
improved code equations taken over from AFP
```     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 definition char_of_int :: "int \<Rightarrow> char"
```
```   147   where [code_abbrev]: "char_of_int = char_of"
```
```   148
```
```   149 definition int_of_char :: "char \<Rightarrow> int"
```
```   150   where [code_abbrev]: "int_of_char = of_char"
```
```   151
```
```   152 lemma [code]:
```
```   153   "char_of_int = char_of_integer \<circ> integer_of_int"
```
```   154   including integer.lifting unfolding char_of_integer_def char_of_int_def
```
```   155   by transfer (simp add: fun_eq_iff)
```
```   156
```
```   157 lemma [code]:
```
```   158   "int_of_char = int_of_integer \<circ> integer_of_char"
```
```   159   including integer.lifting unfolding integer_of_char_def int_of_char_def
```
```   160   by transfer (simp add: fun_eq_iff)
```
```   161
```
```   162 code_identifier
```
```   163   code_module Code_Target_Int \<rightharpoonup>
```
```   164     (SML) Arith and (OCaml) Arith and (Haskell) Arith
```
```   165
```
```   166 end
```