src/HOL/Library/Code_Binary_Nat.thy
 author wenzelm Mon Dec 28 01:28:28 2015 +0100 (2015-12-28) changeset 61945 1135b8de26c3 parent 61433 a4c0de1df3d8 child 66148 5e60c2d0a1f1 permissions -rw-r--r--
more symbols;
```     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
```