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