src/HOL/Library/Code_Target_Nat.thy
 author wenzelm Wed Mar 08 10:50:59 2017 +0100 (2017-03-08) changeset 65151 a7394aa4d21c parent 64997 067a6cca39f0 child 66190 a41435469559 permissions -rw-r--r--
tuned proofs;
```     1 (*  Title:      HOL/Library/Code_Target_Nat.thy
```
```     2     Author:     Florian Haftmann, TU Muenchen
```
```     3 *)
```
```     4
```
```     5 section \<open>Implementation of natural numbers by target-language integers\<close>
```
```     6
```
```     7 theory Code_Target_Nat
```
```     8 imports Code_Abstract_Nat
```
```     9 begin
```
```    10
```
```    11 subsection \<open>Implementation for @{typ nat}\<close>
```
```    12
```
```    13 context
```
```    14 includes natural.lifting integer.lifting
```
```    15 begin
```
```    16
```
```    17 lift_definition Nat :: "integer \<Rightarrow> nat"
```
```    18   is nat
```
```    19   .
```
```    20
```
```    21 lemma [code_post]:
```
```    22   "Nat 0 = 0"
```
```    23   "Nat 1 = 1"
```
```    24   "Nat (numeral k) = numeral k"
```
```    25   by (transfer, simp)+
```
```    26
```
```    27 lemma [code_abbrev]:
```
```    28   "integer_of_nat = of_nat"
```
```    29   by transfer rule
```
```    30
```
```    31 lemma [code_unfold]:
```
```    32   "Int.nat (int_of_integer k) = nat_of_integer k"
```
```    33   by transfer rule
```
```    34
```
```    35 lemma [code abstype]:
```
```    36   "Code_Target_Nat.Nat (integer_of_nat n) = n"
```
```    37   by transfer simp
```
```    38
```
```    39 lemma [code abstract]:
```
```    40   "integer_of_nat (nat_of_integer k) = max 0 k"
```
```    41   by transfer auto
```
```    42
```
```    43 lemma [code_abbrev]:
```
```    44   "nat_of_integer (numeral k) = nat_of_num k"
```
```    45   by transfer (simp add: nat_of_num_numeral)
```
```    46
```
```    47 context
```
```    48 begin
```
```    49
```
```    50 qualified definition natural :: "num \<Rightarrow> nat"
```
```    51   where [simp]: "natural = nat_of_num"
```
```    52
```
```    53 lemma [code_computation_unfold]:
```
```    54   "numeral = natural"
```
```    55   "nat_of_num = natural"
```
```    56   by (simp_all add: nat_of_num_numeral)
```
```    57
```
```    58 end
```
```    59
```
```    60 lemma [code abstract]:
```
```    61   "integer_of_nat (nat_of_num n) = integer_of_num n"
```
```    62   by transfer (simp add: nat_of_num_numeral)
```
```    63
```
```    64 lemma [code abstract]:
```
```    65   "integer_of_nat 0 = 0"
```
```    66   by transfer simp
```
```    67
```
```    68 lemma [code abstract]:
```
```    69   "integer_of_nat 1 = 1"
```
```    70   by transfer simp
```
```    71
```
```    72 lemma [code]:
```
```    73   "Suc n = n + 1"
```
```    74   by simp
```
```    75
```
```    76 lemma [code abstract]:
```
```    77   "integer_of_nat (m + n) = of_nat m + of_nat n"
```
```    78   by transfer simp
```
```    79
```
```    80 lemma [code abstract]:
```
```    81   "integer_of_nat (m - n) = max 0 (of_nat m - of_nat n)"
```
```    82   by transfer simp
```
```    83
```
```    84 lemma [code abstract]:
```
```    85   "integer_of_nat (m * n) = of_nat m * of_nat n"
```
```    86   by transfer (simp add: of_nat_mult)
```
```    87
```
```    88 lemma [code abstract]:
```
```    89   "integer_of_nat (m div n) = of_nat m div of_nat n"
```
```    90   by transfer (simp add: zdiv_int)
```
```    91
```
```    92 lemma [code abstract]:
```
```    93   "integer_of_nat (m mod n) = of_nat m mod of_nat n"
```
```    94   by transfer (simp add: zmod_int)
```
```    95
```
```    96 lemma [code]:
```
```    97   "Divides.divmod_nat m n = (m div n, m mod n)"
```
```    98   by (fact divmod_nat_div_mod)
```
```    99
```
```   100 lemma [code]:
```
```   101   "divmod m n = map_prod nat_of_integer nat_of_integer (divmod m n)"
```
```   102   by (simp only: prod_eq_iff divmod_def map_prod_def case_prod_beta fst_conv snd_conv)
```
```   103     (transfer, simp_all only: nat_div_distrib nat_mod_distrib
```
```   104         zero_le_numeral nat_numeral)
```
```   105
```
```   106 lemma [code]:
```
```   107   "HOL.equal m n = HOL.equal (of_nat m :: integer) (of_nat n)"
```
```   108   by transfer (simp add: equal)
```
```   109
```
```   110 lemma [code]:
```
```   111   "m \<le> n \<longleftrightarrow> (of_nat m :: integer) \<le> of_nat n"
```
```   112   by simp
```
```   113
```
```   114 lemma [code]:
```
```   115   "m < n \<longleftrightarrow> (of_nat m :: integer) < of_nat n"
```
```   116   by simp
```
```   117
```
```   118 lemma num_of_nat_code [code]:
```
```   119   "num_of_nat = num_of_integer \<circ> of_nat"
```
```   120   by transfer (simp add: fun_eq_iff)
```
```   121
```
```   122 end
```
```   123
```
```   124 lemma (in semiring_1) of_nat_code_if:
```
```   125   "of_nat n = (if n = 0 then 0
```
```   126      else let
```
```   127        (m, q) = Divides.divmod_nat n 2;
```
```   128        m' = 2 * of_nat m
```
```   129      in if q = 0 then m' else m' + 1)"
```
```   130 proof -
```
```   131   from div_mult_mod_eq have *: "of_nat n = of_nat (n div 2 * 2 + n mod 2)" by simp
```
```   132   show ?thesis
```
```   133     by (simp add: Let_def divmod_nat_div_mod of_nat_add [symmetric])
```
```   134       (simp add: * mult.commute of_nat_mult add.commute)
```
```   135 qed
```
```   136
```
```   137 declare of_nat_code_if [code]
```
```   138
```
```   139 definition int_of_nat :: "nat \<Rightarrow> int" where
```
```   140   [code_abbrev]: "int_of_nat = of_nat"
```
```   141
```
```   142 lemma [code]:
```
```   143   "int_of_nat n = int_of_integer (of_nat n)"
```
```   144   by (simp add: int_of_nat_def)
```
```   145
```
```   146 lemma [code abstract]:
```
```   147   "integer_of_nat (nat k) = max 0 (integer_of_int k)"
```
```   148   including integer.lifting by transfer auto
```
```   149
```
```   150 lemma term_of_nat_code [code]:
```
```   151   \<comment> \<open>Use @{term Code_Numeral.nat_of_integer} in term reconstruction
```
```   152         instead of @{term Code_Target_Nat.Nat} such that reconstructed
```
```   153         terms can be fed back to the code generator\<close>
```
```   154   "term_of_class.term_of n =
```
```   155    Code_Evaluation.App
```
```   156      (Code_Evaluation.Const (STR ''Code_Numeral.nat_of_integer'')
```
```   157         (typerep.Typerep (STR ''fun'')
```
```   158            [typerep.Typerep (STR ''Code_Numeral.integer'') [],
```
```   159          typerep.Typerep (STR ''Nat.nat'') []]))
```
```   160      (term_of_class.term_of (integer_of_nat n))"
```
```   161   by (simp add: term_of_anything)
```
```   162
```
```   163 lemma nat_of_integer_code_post [code_post]:
```
```   164   "nat_of_integer 0 = 0"
```
```   165   "nat_of_integer 1 = 1"
```
```   166   "nat_of_integer (numeral k) = numeral k"
```
```   167   including integer.lifting by (transfer, simp)+
```
```   168
```
```   169 code_identifier
```
```   170   code_module Code_Target_Nat \<rightharpoonup>
```
```   171     (SML) Arith and (OCaml) Arith and (Haskell) Arith
```
```   172
```
```   173 end
```