src/HOL/Library/Code_Binary_Nat.thy
author haftmann
Mon Jun 05 15:59:41 2017 +0200 (2017-06-05)
changeset 66010 2f7d39285a1a
parent 61433 a4c0de1df3d8
child 66148 5e60c2d0a1f1
permissions -rw-r--r--
executable domain membership checks
     1 (*  Title:      HOL/Library/Code_Binary_Nat.thy
     2     Author:     Florian Haftmann, TU Muenchen
     3 *)
     4 
     5 section \<open>Implementation of natural numbers as binary numerals\<close>
     6 
     7 theory Code_Binary_Nat
     8 imports Code_Abstract_Nat
     9 begin
    10 
    11 text \<open>
    12   When generating code for functions on natural numbers, the
    13   canonical representation using @{term "0::nat"} and
    14   @{term Suc} is unsuitable for computations involving large
    15   numbers.  This theory refines the representation of
    16   natural numbers for code generation to use binary
    17   numerals, which do not grow linear in size but logarithmic.
    18 \<close>
    19 
    20 subsection \<open>Representation\<close>
    21 
    22 code_datatype "0::nat" nat_of_num
    23 
    24 lemma [code]:
    25   "num_of_nat 0 = Num.One"
    26   "num_of_nat (nat_of_num k) = k"
    27   by (simp_all add: nat_of_num_inverse)
    28 
    29 lemma [code]:
    30   "(1::nat) = Numeral1"
    31   by simp
    32 
    33 lemma [code_abbrev]: "Numeral1 = (1::nat)"
    34   by simp
    35 
    36 lemma [code]:
    37   "Suc n = n + 1"
    38   by simp
    39 
    40 
    41 subsection \<open>Basic arithmetic\<close>
    42 
    43 context
    44 begin
    45 
    46 lemma [code, code del]:
    47   "(plus :: nat \<Rightarrow> _) = plus" ..
    48 
    49 lemma plus_nat_code [code]:
    50   "nat_of_num k + nat_of_num l = nat_of_num (k + l)"
    51   "m + 0 = (m::nat)"
    52   "0 + n = (n::nat)"
    53   by (simp_all add: nat_of_num_numeral)
    54 
    55 text \<open>Bounded subtraction needs some auxiliary\<close>
    56 
    57 qualified definition dup :: "nat \<Rightarrow> nat" where
    58   "dup n = n + n"
    59 
    60 lemma dup_code [code]:
    61   "dup 0 = 0"
    62   "dup (nat_of_num k) = nat_of_num (Num.Bit0 k)"
    63   by (simp_all add: dup_def numeral_Bit0)
    64 
    65 qualified definition sub :: "num \<Rightarrow> num \<Rightarrow> nat option" where
    66   "sub k l = (if k \<ge> l then Some (numeral k - numeral l) else None)"
    67 
    68 lemma sub_code [code]:
    69   "sub Num.One Num.One = Some 0"
    70   "sub (Num.Bit0 m) Num.One = Some (nat_of_num (Num.BitM m))"
    71   "sub (Num.Bit1 m) Num.One = Some (nat_of_num (Num.Bit0 m))"
    72   "sub Num.One (Num.Bit0 n) = None"
    73   "sub Num.One (Num.Bit1 n) = None"
    74   "sub (Num.Bit0 m) (Num.Bit0 n) = map_option dup (sub m n)"
    75   "sub (Num.Bit1 m) (Num.Bit1 n) = map_option dup (sub m n)"
    76   "sub (Num.Bit1 m) (Num.Bit0 n) = map_option (\<lambda>q. dup q + 1) (sub m n)"
    77   "sub (Num.Bit0 m) (Num.Bit1 n) = (case sub m n of None \<Rightarrow> None
    78      | Some q \<Rightarrow> if q = 0 then None else Some (dup q - 1))"
    79   apply (auto simp add: nat_of_num_numeral
    80     Num.dbl_def Num.dbl_inc_def Num.dbl_dec_def
    81     Let_def le_imp_diff_is_add BitM_plus_one sub_def dup_def)
    82   apply (simp_all add: sub_non_positive)
    83   apply (simp_all add: sub_non_negative [symmetric, where ?'a = int])
    84   done
    85 
    86 lemma [code, code del]:
    87   "(minus :: nat \<Rightarrow> _) = minus" ..
    88 
    89 lemma minus_nat_code [code]:
    90   "nat_of_num k - nat_of_num l = (case sub k l of None \<Rightarrow> 0 | Some j \<Rightarrow> j)"
    91   "m - 0 = (m::nat)"
    92   "0 - n = (0::nat)"
    93   by (simp_all add: nat_of_num_numeral sub_non_positive sub_def)
    94 
    95 lemma [code, code del]:
    96   "(times :: nat \<Rightarrow> _) = times" ..
    97 
    98 lemma times_nat_code [code]:
    99   "nat_of_num k * nat_of_num l = nat_of_num (k * l)"
   100   "m * 0 = (0::nat)"
   101   "0 * n = (0::nat)"
   102   by (simp_all add: nat_of_num_numeral)
   103 
   104 lemma [code, code del]:
   105   "(HOL.equal :: nat \<Rightarrow> _) = HOL.equal" ..
   106 
   107 lemma equal_nat_code [code]:
   108   "HOL.equal 0 (0::nat) \<longleftrightarrow> True"
   109   "HOL.equal 0 (nat_of_num l) \<longleftrightarrow> False"
   110   "HOL.equal (nat_of_num k) 0 \<longleftrightarrow> False"
   111   "HOL.equal (nat_of_num k) (nat_of_num l) \<longleftrightarrow> HOL.equal k l"
   112   by (simp_all add: nat_of_num_numeral equal)
   113 
   114 lemma equal_nat_refl [code nbe]:
   115   "HOL.equal (n::nat) n \<longleftrightarrow> True"
   116   by (rule equal_refl)
   117 
   118 lemma [code, code del]:
   119   "(less_eq :: nat \<Rightarrow> _) = less_eq" ..
   120 
   121 lemma less_eq_nat_code [code]:
   122   "0 \<le> (n::nat) \<longleftrightarrow> True"
   123   "nat_of_num k \<le> 0 \<longleftrightarrow> False"
   124   "nat_of_num k \<le> nat_of_num l \<longleftrightarrow> k \<le> l"
   125   by (simp_all add: nat_of_num_numeral)
   126 
   127 lemma [code, code del]:
   128   "(less :: nat \<Rightarrow> _) = less" ..
   129 
   130 lemma less_nat_code [code]:
   131   "(m::nat) < 0 \<longleftrightarrow> False"
   132   "0 < nat_of_num l \<longleftrightarrow> True"
   133   "nat_of_num k < nat_of_num l \<longleftrightarrow> k < l"
   134   by (simp_all add: nat_of_num_numeral)
   135 
   136 lemma [code, code del]:
   137   "Divides.divmod_nat = Divides.divmod_nat" ..
   138   
   139 lemma divmod_nat_code [code]:
   140   "Divides.divmod_nat (nat_of_num k) (nat_of_num l) = divmod k l"
   141   "Divides.divmod_nat m 0 = (0, m)"
   142   "Divides.divmod_nat 0 n = (0, 0)"
   143   by (simp_all add: prod_eq_iff nat_of_num_numeral)
   144 
   145 end
   146 
   147 
   148 subsection \<open>Conversions\<close>
   149 
   150 lemma [code, code del]:
   151   "of_nat = of_nat" ..
   152 
   153 lemma of_nat_code [code]:
   154   "of_nat 0 = 0"
   155   "of_nat (nat_of_num k) = numeral k"
   156   by (simp_all add: nat_of_num_numeral)
   157 
   158 
   159 code_identifier
   160   code_module Code_Binary_Nat \<rightharpoonup>
   161     (SML) Arith and (OCaml) Arith and (Haskell) Arith
   162 
   163 end