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
```