src/HOL/Library/Code_Binary_Nat.thy
 author Andreas Lochbihler Wed Feb 27 10:33:30 2013 +0100 (2013-02-27) changeset 51288 be7e9a675ec9 parent 51143 0a2371e7ced3 child 52435 6646bb548c6b permissions -rw-r--r--
add wellorder instance for Numeral_Type (suggested by Jesus Aransay)
```     1 (*  Title:      HOL/Library/Code_Binary_Nat.thy
```
```     2     Author:     Florian Haftmann, TU Muenchen
```
```     3 *)
```
```     4
```
```     5 header {* Implementation of natural numbers as binary numerals *}
```
```     6
```
```     7 theory Code_Binary_Nat
```
```     8 imports Code_Abstract_Nat
```
```     9 begin
```
```    10
```
```    11 text {*
```
```    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 *}
```
```    19
```
```    20 subsection {* Representation *}
```
```    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\<Colon>nat) = Numeral1"
```
```    31   by simp
```
```    32
```
```    33 lemma [code_abbrev]: "Numeral1 = (1\<Colon>nat)"
```
```    34   by simp
```
```    35
```
```    36 lemma [code]:
```
```    37   "Suc n = n + 1"
```
```    38   by simp
```
```    39
```
```    40
```
```    41 subsection {* Basic arithmetic *}
```
```    42
```
```    43 lemma [code, code del]:
```
```    44   "(plus :: nat \<Rightarrow> _) = plus" ..
```
```    45
```
```    46 lemma plus_nat_code [code]:
```
```    47   "nat_of_num k + nat_of_num l = nat_of_num (k + l)"
```
```    48   "m + 0 = (m::nat)"
```
```    49   "0 + n = (n::nat)"
```
```    50   by (simp_all add: nat_of_num_numeral)
```
```    51
```
```    52 text {* Bounded subtraction needs some auxiliary *}
```
```    53
```
```    54 definition dup :: "nat \<Rightarrow> nat" where
```
```    55   "dup n = n + n"
```
```    56
```
```    57 lemma dup_code [code]:
```
```    58   "dup 0 = 0"
```
```    59   "dup (nat_of_num k) = nat_of_num (Num.Bit0 k)"
```
```    60   by (simp_all add: dup_def numeral_Bit0)
```
```    61
```
```    62 definition sub :: "num \<Rightarrow> num \<Rightarrow> nat option" where
```
```    63   "sub k l = (if k \<ge> l then Some (numeral k - numeral l) else None)"
```
```    64
```
```    65 lemma sub_code [code]:
```
```    66   "sub Num.One Num.One = Some 0"
```
```    67   "sub (Num.Bit0 m) Num.One = Some (nat_of_num (Num.BitM m))"
```
```    68   "sub (Num.Bit1 m) Num.One = Some (nat_of_num (Num.Bit0 m))"
```
```    69   "sub Num.One (Num.Bit0 n) = None"
```
```    70   "sub Num.One (Num.Bit1 n) = None"
```
```    71   "sub (Num.Bit0 m) (Num.Bit0 n) = Option.map dup (sub m n)"
```
```    72   "sub (Num.Bit1 m) (Num.Bit1 n) = Option.map dup (sub m n)"
```
```    73   "sub (Num.Bit1 m) (Num.Bit0 n) = Option.map (\<lambda>q. dup q + 1) (sub m n)"
```
```    74   "sub (Num.Bit0 m) (Num.Bit1 n) = (case sub m n of None \<Rightarrow> None
```
```    75      | Some q \<Rightarrow> if q = 0 then None else Some (dup q - 1))"
```
```    76   apply (auto simp add: nat_of_num_numeral
```
```    77     Num.dbl_def Num.dbl_inc_def Num.dbl_dec_def
```
```    78     Let_def le_imp_diff_is_add BitM_plus_one sub_def dup_def)
```
```    79   apply (simp_all add: sub_non_positive)
```
```    80   apply (simp_all add: sub_non_negative [symmetric, where ?'a = int])
```
```    81   done
```
```    82
```
```    83 lemma [code, code del]:
```
```    84   "(minus :: nat \<Rightarrow> _) = minus" ..
```
```    85
```
```    86 lemma minus_nat_code [code]:
```
```    87   "nat_of_num k - nat_of_num l = (case sub k l of None \<Rightarrow> 0 | Some j \<Rightarrow> j)"
```
```    88   "m - 0 = (m::nat)"
```
```    89   "0 - n = (0::nat)"
```
```    90   by (simp_all add: nat_of_num_numeral sub_non_positive sub_def)
```
```    91
```
```    92 lemma [code, code del]:
```
```    93   "(times :: nat \<Rightarrow> _) = times" ..
```
```    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 lemma [code, code del]:
```
```   102   "(HOL.equal :: nat \<Rightarrow> _) = HOL.equal" ..
```
```   103
```
```   104 lemma equal_nat_code [code]:
```
```   105   "HOL.equal 0 (0::nat) \<longleftrightarrow> True"
```
```   106   "HOL.equal 0 (nat_of_num l) \<longleftrightarrow> False"
```
```   107   "HOL.equal (nat_of_num k) 0 \<longleftrightarrow> False"
```
```   108   "HOL.equal (nat_of_num k) (nat_of_num l) \<longleftrightarrow> HOL.equal k l"
```
```   109   by (simp_all add: nat_of_num_numeral equal)
```
```   110
```
```   111 lemma equal_nat_refl [code nbe]:
```
```   112   "HOL.equal (n::nat) n \<longleftrightarrow> True"
```
```   113   by (rule equal_refl)
```
```   114
```
```   115 lemma [code, code del]:
```
```   116   "(less_eq :: nat \<Rightarrow> _) = less_eq" ..
```
```   117
```
```   118 lemma less_eq_nat_code [code]:
```
```   119   "0 \<le> (n::nat) \<longleftrightarrow> True"
```
```   120   "nat_of_num k \<le> 0 \<longleftrightarrow> False"
```
```   121   "nat_of_num k \<le> nat_of_num l \<longleftrightarrow> k \<le> l"
```
```   122   by (simp_all add: nat_of_num_numeral)
```
```   123
```
```   124 lemma [code, code del]:
```
```   125   "(less :: nat \<Rightarrow> _) = less" ..
```
```   126
```
```   127 lemma less_nat_code [code]:
```
```   128   "(m::nat) < 0 \<longleftrightarrow> False"
```
```   129   "0 < nat_of_num l \<longleftrightarrow> True"
```
```   130   "nat_of_num k < nat_of_num l \<longleftrightarrow> k < l"
```
```   131   by (simp_all add: nat_of_num_numeral)
```
```   132
```
```   133
```
```   134 subsection {* Conversions *}
```
```   135
```
```   136 lemma [code, code del]:
```
```   137   "of_nat = of_nat" ..
```
```   138
```
```   139 lemma of_nat_code [code]:
```
```   140   "of_nat 0 = 0"
```
```   141   "of_nat (nat_of_num k) = numeral k"
```
```   142   by (simp_all add: nat_of_num_numeral)
```
```   143
```
```   144
```
```   145 code_modulename SML
```
```   146   Code_Binary_Nat Arith
```
```   147
```
```   148 code_modulename OCaml
```
```   149   Code_Binary_Nat Arith
```
```   150
```
```   151 code_modulename Haskell
```
```   152   Code_Binary_Nat Arith
```
```   153
```
```   154 hide_const (open) dup sub
```
```   155
```
```   156 end
```
```   157
```