src/HOL/Library/Code_Binary_Nat.thy
author haftmann
Wed Jul 18 20:51:21 2018 +0200 (11 months ago)
changeset 68658 16cc1161ad7f
parent 66148 5e60c2d0a1f1
child 69593 3dda49e08b9d
permissions -rw-r--r--
tuned equation
     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 declare [[code drop: "plus :: nat \<Rightarrow> _"]]  
    47 
    48 lemma plus_nat_code [code]:
    49   "nat_of_num k + nat_of_num l = nat_of_num (k + l)"
    50   "m + 0 = (m::nat)"
    51   "0 + n = (n::nat)"
    52   by (simp_all add: nat_of_num_numeral)
    53 
    54 text \<open>Bounded subtraction needs some auxiliary\<close>
    55 
    56 qualified definition dup :: "nat \<Rightarrow> nat" where
    57   "dup n = n + n"
    58 
    59 lemma dup_code [code]:
    60   "dup 0 = 0"
    61   "dup (nat_of_num k) = nat_of_num (Num.Bit0 k)"
    62   by (simp_all add: dup_def numeral_Bit0)
    63 
    64 qualified definition sub :: "num \<Rightarrow> num \<Rightarrow> nat option" where
    65   "sub k l = (if k \<ge> l then Some (numeral k - numeral l) else None)"
    66 
    67 lemma sub_code [code]:
    68   "sub Num.One Num.One = Some 0"
    69   "sub (Num.Bit0 m) Num.One = Some (nat_of_num (Num.BitM m))"
    70   "sub (Num.Bit1 m) Num.One = Some (nat_of_num (Num.Bit0 m))"
    71   "sub Num.One (Num.Bit0 n) = None"
    72   "sub Num.One (Num.Bit1 n) = None"
    73   "sub (Num.Bit0 m) (Num.Bit0 n) = map_option dup (sub m n)"
    74   "sub (Num.Bit1 m) (Num.Bit1 n) = map_option dup (sub m n)"
    75   "sub (Num.Bit1 m) (Num.Bit0 n) = map_option (\<lambda>q. dup q + 1) (sub m n)"
    76   "sub (Num.Bit0 m) (Num.Bit1 n) = (case sub m n of None \<Rightarrow> None
    77      | Some q \<Rightarrow> if q = 0 then None else Some (dup q - 1))"
    78   apply (auto simp add: nat_of_num_numeral
    79     Num.dbl_def Num.dbl_inc_def Num.dbl_dec_def
    80     Let_def le_imp_diff_is_add BitM_plus_one sub_def dup_def)
    81   apply (simp_all add: sub_non_positive)
    82   apply (simp_all add: sub_non_negative [symmetric, where ?'a = int])
    83   done
    84 
    85 declare [[code drop: "minus :: nat \<Rightarrow> _"]]
    86 
    87 lemma minus_nat_code [code]:
    88   "nat_of_num k - nat_of_num l = (case sub k l of None \<Rightarrow> 0 | Some j \<Rightarrow> j)"
    89   "m - 0 = (m::nat)"
    90   "0 - n = (0::nat)"
    91   by (simp_all add: nat_of_num_numeral sub_non_positive sub_def)
    92 
    93 declare [[code drop: "times :: nat \<Rightarrow> _"]]
    94 
    95 lemma times_nat_code [code]:
    96   "nat_of_num k * nat_of_num l = nat_of_num (k * l)"
    97   "m * 0 = (0::nat)"
    98   "0 * n = (0::nat)"
    99   by (simp_all add: nat_of_num_numeral)
   100 
   101 declare [[code drop: "HOL.equal :: nat \<Rightarrow> _"]]
   102 
   103 lemma equal_nat_code [code]:
   104   "HOL.equal 0 (0::nat) \<longleftrightarrow> True"
   105   "HOL.equal 0 (nat_of_num l) \<longleftrightarrow> False"
   106   "HOL.equal (nat_of_num k) 0 \<longleftrightarrow> False"
   107   "HOL.equal (nat_of_num k) (nat_of_num l) \<longleftrightarrow> HOL.equal k l"
   108   by (simp_all add: nat_of_num_numeral equal)
   109 
   110 lemma equal_nat_refl [code nbe]:
   111   "HOL.equal (n::nat) n \<longleftrightarrow> True"
   112   by (rule equal_refl)
   113 
   114 declare [[code drop: "less_eq :: nat \<Rightarrow> _"]]
   115 
   116 lemma less_eq_nat_code [code]:
   117   "0 \<le> (n::nat) \<longleftrightarrow> True"
   118   "nat_of_num k \<le> 0 \<longleftrightarrow> False"
   119   "nat_of_num k \<le> nat_of_num l \<longleftrightarrow> k \<le> l"
   120   by (simp_all add: nat_of_num_numeral)
   121 
   122 declare [[code drop: "less :: nat \<Rightarrow> _"]]
   123 
   124 lemma less_nat_code [code]:
   125   "(m::nat) < 0 \<longleftrightarrow> False"
   126   "0 < nat_of_num l \<longleftrightarrow> True"
   127   "nat_of_num k < nat_of_num l \<longleftrightarrow> k < l"
   128   by (simp_all add: nat_of_num_numeral)
   129 
   130 declare [[code drop: Divides.divmod_nat]]
   131   
   132 lemma divmod_nat_code [code]:
   133   "Divides.divmod_nat (nat_of_num k) (nat_of_num l) = divmod k l"
   134   "Divides.divmod_nat m 0 = (0, m)"
   135   "Divides.divmod_nat 0 n = (0, 0)"
   136   by (simp_all add: prod_eq_iff nat_of_num_numeral)
   137 
   138 end
   139 
   140 
   141 subsection \<open>Conversions\<close>
   142 
   143 declare [[code drop: of_nat]]
   144 
   145 lemma of_nat_code [code]:
   146   "of_nat 0 = 0"
   147   "of_nat (nat_of_num k) = numeral k"
   148   by (simp_all add: nat_of_num_numeral)
   149 
   150 
   151 code_identifier
   152   code_module Code_Binary_Nat \<rightharpoonup>
   153     (SML) Arith and (OCaml) Arith and (Haskell) Arith
   154 
   155 end