src/HOL/Library/Code_Target_Nat.thy
author Andreas Lochbihler
Fri Sep 20 10:09:16 2013 +0200 (2013-09-20)
changeset 53745 788730ab7da4
parent 53027 1774d569b604
child 54796 cdc6d8cbf770
permissions -rw-r--r--
prefer Code.abort over code_abort
     1 (*  Title:      HOL/Library/Code_Target_Nat.thy
     2     Author:     Florian Haftmann, TU Muenchen
     3 *)
     4 
     5 header {* Implementation of natural numbers by target-language integers *}
     6 
     7 theory Code_Target_Nat
     8 imports Code_Abstract_Nat
     9 begin
    10 
    11 subsection {* Implementation for @{typ nat} *}
    12 
    13 lift_definition Nat :: "integer \<Rightarrow> nat"
    14   is nat
    15   .
    16 
    17 lemma [code_post]:
    18   "Nat 0 = 0"
    19   "Nat 1 = 1"
    20   "Nat (numeral k) = numeral k"
    21   by (transfer, simp)+
    22 
    23 lemma [code_abbrev]:
    24   "integer_of_nat = of_nat"
    25   by transfer rule
    26 
    27 lemma [code_unfold]:
    28   "Int.nat (int_of_integer k) = nat_of_integer k"
    29   by transfer rule
    30 
    31 lemma [code abstype]:
    32   "Code_Target_Nat.Nat (integer_of_nat n) = n"
    33   by transfer simp
    34 
    35 lemma [code abstract]:
    36   "integer_of_nat (nat_of_integer k) = max 0 k"
    37   by transfer auto
    38 
    39 lemma [code_abbrev]:
    40   "nat_of_integer (numeral k) = nat_of_num k"
    41   by transfer (simp add: nat_of_num_numeral)
    42 
    43 lemma [code abstract]:
    44   "integer_of_nat (nat_of_num n) = integer_of_num n"
    45   by transfer (simp add: nat_of_num_numeral)
    46 
    47 lemma [code abstract]:
    48   "integer_of_nat 0 = 0"
    49   by transfer simp
    50 
    51 lemma [code abstract]:
    52   "integer_of_nat 1 = 1"
    53   by transfer simp
    54 
    55 lemma [code]:
    56   "Suc n = n + 1"
    57   by simp
    58 
    59 lemma [code abstract]:
    60   "integer_of_nat (m + n) = of_nat m + of_nat n"
    61   by transfer simp
    62 
    63 lemma [code abstract]:
    64   "integer_of_nat (m - n) = max 0 (of_nat m - of_nat n)"
    65   by transfer simp
    66 
    67 lemma [code abstract]:
    68   "integer_of_nat (m * n) = of_nat m * of_nat n"
    69   by transfer (simp add: of_nat_mult)
    70 
    71 lemma [code abstract]:
    72   "integer_of_nat (m div n) = of_nat m div of_nat n"
    73   by transfer (simp add: zdiv_int)
    74 
    75 lemma [code abstract]:
    76   "integer_of_nat (m mod n) = of_nat m mod of_nat n"
    77   by transfer (simp add: zmod_int)
    78 
    79 lemma [code]:
    80   "Divides.divmod_nat m n = (m div n, m mod n)"
    81   by (simp add: prod_eq_iff)
    82 
    83 lemma [code]:
    84   "HOL.equal m n = HOL.equal (of_nat m :: integer) (of_nat n)"
    85   by transfer (simp add: equal)
    86 
    87 lemma [code]:
    88   "m \<le> n \<longleftrightarrow> (of_nat m :: integer) \<le> of_nat n"
    89   by simp
    90 
    91 lemma [code]:
    92   "m < n \<longleftrightarrow> (of_nat m :: integer) < of_nat n"
    93   by simp
    94 
    95 lemma num_of_nat_code [code]:
    96   "num_of_nat = num_of_integer \<circ> of_nat"
    97   by transfer (simp add: fun_eq_iff)
    98 
    99 lemma (in semiring_1) of_nat_code:
   100   "of_nat n = (if n = 0 then 0
   101      else let
   102        (m, q) = divmod_nat n 2;
   103        m' = 2 * of_nat m
   104      in if q = 0 then m' else m' + 1)"
   105 proof -
   106   from mod_div_equality have *: "of_nat n = of_nat (n div 2 * 2 + n mod 2)" by simp
   107   show ?thesis
   108     by (simp add: Let_def divmod_nat_div_mod mod_2_not_eq_zero_eq_one_nat
   109       of_nat_add [symmetric])
   110       (simp add: * mult_commute of_nat_mult add_commute)
   111 qed
   112 
   113 declare of_nat_code [code]
   114 
   115 definition int_of_nat :: "nat \<Rightarrow> int" where
   116   [code_abbrev]: "int_of_nat = of_nat"
   117 
   118 lemma [code]:
   119   "int_of_nat n = int_of_integer (of_nat n)"
   120   by (simp add: int_of_nat_def)
   121 
   122 lemma [code abstract]:
   123   "integer_of_nat (nat k) = max 0 (integer_of_int k)"
   124   by transfer auto
   125 
   126 lemma term_of_nat_code [code]:
   127   -- {* Use @{term Code_Numeral.nat_of_integer} in term reconstruction
   128         instead of @{term Code_Target_Nat.Nat} such that reconstructed
   129         terms can be fed back to the code generator *}
   130   "term_of_class.term_of n =
   131    Code_Evaluation.App
   132      (Code_Evaluation.Const (STR ''Code_Numeral.nat_of_integer'')
   133         (typerep.Typerep (STR ''fun'')
   134            [typerep.Typerep (STR ''Code_Numeral.integer'') [],
   135          typerep.Typerep (STR ''Nat.nat'') []]))
   136      (term_of_class.term_of (integer_of_nat n))"
   137 by(simp add: term_of_anything)
   138 
   139 lemma nat_of_integer_code_post [code_post]:
   140   "nat_of_integer 0 = 0"
   141   "nat_of_integer 1 = 1"
   142   "nat_of_integer (numeral k) = numeral k"
   143 by(transfer, simp)+
   144 
   145 code_identifier
   146   code_module Code_Target_Nat \<rightharpoonup>
   147     (SML) Arith and (OCaml) Arith and (Haskell) Arith
   148 
   149 end