src/HOL/Library/Code_Target_Nat.thy
author haftmann
Tue Apr 24 14:17:58 2018 +0000 (15 months ago)
changeset 68028 1f9f973eed2a
parent 66808 1907167b6038
child 69593 3dda49e08b9d
permissions -rw-r--r--
proper datatype for 8-bit characters
     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 (simp add: nat_of_num_numeral integer_of_nat_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_def)
    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_def 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 definition char_of_nat :: "nat \<Rightarrow> char"
   151   where [code_abbrev]: "char_of_nat = char_of"
   152 
   153 definition nat_of_char :: "char \<Rightarrow> nat"
   154   where [code_abbrev]: "nat_of_char = of_char"
   155 
   156 lemma [code]:
   157   "char_of_nat = char_of_integer \<circ> integer_of_nat"
   158   including integer.lifting unfolding char_of_integer_def char_of_nat_def
   159   by transfer (simp add: fun_eq_iff)
   160 
   161 lemma [code abstract]:
   162   "integer_of_nat (nat_of_char c) = integer_of_char c"
   163   by (cases c) (simp add: nat_of_char_def integer_of_char_def integer_of_nat_eq_of_nat)
   164 
   165 lemma term_of_nat_code [code]:
   166   \<comment> \<open>Use @{term Code_Numeral.nat_of_integer} in term reconstruction
   167         instead of @{term Code_Target_Nat.Nat} such that reconstructed
   168         terms can be fed back to the code generator\<close>
   169   "term_of_class.term_of n =
   170    Code_Evaluation.App
   171      (Code_Evaluation.Const (STR ''Code_Numeral.nat_of_integer'')
   172         (typerep.Typerep (STR ''fun'')
   173            [typerep.Typerep (STR ''Code_Numeral.integer'') [],
   174          typerep.Typerep (STR ''Nat.nat'') []]))
   175      (term_of_class.term_of (integer_of_nat n))"
   176   by (simp add: term_of_anything)
   177 
   178 lemma nat_of_integer_code_post [code_post]:
   179   "nat_of_integer 0 = 0"
   180   "nat_of_integer 1 = 1"
   181   "nat_of_integer (numeral k) = numeral k"
   182   including integer.lifting by (transfer, simp)+
   183 
   184 code_identifier
   185   code_module Code_Target_Nat \<rightharpoonup>
   186     (SML) Arith and (OCaml) Arith and (Haskell) Arith
   187 
   188 end