src/HOL/Library/Code_Binary_Nat.thy
author Christian Sternagel
Thu Dec 13 13:11:38 2012 +0100 (2012-12-13)
changeset 50516 ed6b40d15d1c
parent 50023 28f3263d4d1b
child 51113 222fb6cb2c3e
permissions -rw-r--r--
renamed "emb" to "list_hembeq";
make "list_hembeq" reflexive independent of the base order;
renamed "sub" to "sublisteq";
dropped "transp_on" (state transitivity explicitly instead);
no need to hide "sub" after renaming;
replaced some ASCII symbols by proper Isabelle symbols;
NEWS
haftmann@50023
     1
(*  Title:      HOL/Library/Code_Binary_Nat.thy
huffman@47108
     2
    Author:     Stefan Berghofer, Florian Haftmann, TU Muenchen
huffman@47108
     3
*)
huffman@47108
     4
huffman@47108
     5
header {* Implementation of natural numbers as binary numerals *}
huffman@47108
     6
haftmann@50023
     7
theory Code_Binary_Nat
huffman@47108
     8
imports Main
huffman@47108
     9
begin
huffman@47108
    10
huffman@47108
    11
text {*
huffman@47108
    12
  When generating code for functions on natural numbers, the
huffman@47108
    13
  canonical representation using @{term "0::nat"} and
huffman@47108
    14
  @{term Suc} is unsuitable for computations involving large
huffman@47108
    15
  numbers.  This theory refines the representation of
huffman@47108
    16
  natural numbers for code generation to use binary
huffman@47108
    17
  numerals, which do not grow linear in size but logarithmic.
huffman@47108
    18
*}
huffman@47108
    19
huffman@47108
    20
subsection {* Representation *}
huffman@47108
    21
haftmann@50023
    22
code_datatype "0::nat" nat_of_num
haftmann@50023
    23
huffman@47108
    24
lemma [code_abbrev]:
huffman@47108
    25
  "nat_of_num = numeral"
huffman@47108
    26
  by (fact nat_of_num_numeral)
huffman@47108
    27
huffman@47108
    28
lemma [code]:
huffman@47108
    29
  "num_of_nat 0 = Num.One"
huffman@47108
    30
  "num_of_nat (nat_of_num k) = k"
huffman@47108
    31
  by (simp_all add: nat_of_num_inverse)
huffman@47108
    32
huffman@47108
    33
lemma [code]:
huffman@47108
    34
  "(1\<Colon>nat) = Numeral1"
huffman@47108
    35
  by simp
huffman@47108
    36
huffman@47108
    37
lemma [code_abbrev]: "Numeral1 = (1\<Colon>nat)"
huffman@47108
    38
  by simp
huffman@47108
    39
huffman@47108
    40
lemma [code]:
huffman@47108
    41
  "Suc n = n + 1"
huffman@47108
    42
  by simp
huffman@47108
    43
huffman@47108
    44
huffman@47108
    45
subsection {* Basic arithmetic *}
huffman@47108
    46
huffman@47108
    47
lemma [code, code del]:
huffman@47108
    48
  "(plus :: nat \<Rightarrow> _) = plus" ..
huffman@47108
    49
huffman@47108
    50
lemma plus_nat_code [code]:
huffman@47108
    51
  "nat_of_num k + nat_of_num l = nat_of_num (k + l)"
huffman@47108
    52
  "m + 0 = (m::nat)"
huffman@47108
    53
  "0 + n = (n::nat)"
huffman@47108
    54
  by (simp_all add: nat_of_num_numeral)
huffman@47108
    55
huffman@47108
    56
text {* Bounded subtraction needs some auxiliary *}
huffman@47108
    57
huffman@47108
    58
definition dup :: "nat \<Rightarrow> nat" where
huffman@47108
    59
  "dup n = n + n"
huffman@47108
    60
huffman@47108
    61
lemma dup_code [code]:
huffman@47108
    62
  "dup 0 = 0"
huffman@47108
    63
  "dup (nat_of_num k) = nat_of_num (Num.Bit0 k)"
haftmann@50023
    64
  by (simp_all add: dup_def numeral_Bit0)
huffman@47108
    65
huffman@47108
    66
definition sub :: "num \<Rightarrow> num \<Rightarrow> nat option" where
huffman@47108
    67
  "sub k l = (if k \<ge> l then Some (numeral k - numeral l) else None)"
huffman@47108
    68
huffman@47108
    69
lemma sub_code [code]:
huffman@47108
    70
  "sub Num.One Num.One = Some 0"
huffman@47108
    71
  "sub (Num.Bit0 m) Num.One = Some (nat_of_num (Num.BitM m))"
huffman@47108
    72
  "sub (Num.Bit1 m) Num.One = Some (nat_of_num (Num.Bit0 m))"
huffman@47108
    73
  "sub Num.One (Num.Bit0 n) = None"
huffman@47108
    74
  "sub Num.One (Num.Bit1 n) = None"
huffman@47108
    75
  "sub (Num.Bit0 m) (Num.Bit0 n) = Option.map dup (sub m n)"
huffman@47108
    76
  "sub (Num.Bit1 m) (Num.Bit1 n) = Option.map dup (sub m n)"
huffman@47108
    77
  "sub (Num.Bit1 m) (Num.Bit0 n) = Option.map (\<lambda>q. dup q + 1) (sub m n)"
huffman@47108
    78
  "sub (Num.Bit0 m) (Num.Bit1 n) = (case sub m n of None \<Rightarrow> None
huffman@47108
    79
     | Some q \<Rightarrow> if q = 0 then None else Some (dup q - 1))"
huffman@47108
    80
  apply (auto simp add: nat_of_num_numeral
huffman@47108
    81
    Num.dbl_def Num.dbl_inc_def Num.dbl_dec_def
huffman@47108
    82
    Let_def le_imp_diff_is_add BitM_plus_one sub_def dup_def)
huffman@47108
    83
  apply (simp_all add: sub_non_positive)
huffman@47108
    84
  apply (simp_all add: sub_non_negative [symmetric, where ?'a = int])
huffman@47108
    85
  done
huffman@47108
    86
huffman@47108
    87
lemma [code, code del]:
huffman@47108
    88
  "(minus :: nat \<Rightarrow> _) = minus" ..
huffman@47108
    89
huffman@47108
    90
lemma minus_nat_code [code]:
huffman@47108
    91
  "nat_of_num k - nat_of_num l = (case sub k l of None \<Rightarrow> 0 | Some j \<Rightarrow> j)"
huffman@47108
    92
  "m - 0 = (m::nat)"
huffman@47108
    93
  "0 - n = (0::nat)"
huffman@47108
    94
  by (simp_all add: nat_of_num_numeral sub_non_positive sub_def)
huffman@47108
    95
huffman@47108
    96
lemma [code, code del]:
huffman@47108
    97
  "(times :: nat \<Rightarrow> _) = times" ..
huffman@47108
    98
huffman@47108
    99
lemma times_nat_code [code]:
huffman@47108
   100
  "nat_of_num k * nat_of_num l = nat_of_num (k * l)"
huffman@47108
   101
  "m * 0 = (0::nat)"
huffman@47108
   102
  "0 * n = (0::nat)"
huffman@47108
   103
  by (simp_all add: nat_of_num_numeral)
huffman@47108
   104
huffman@47108
   105
lemma [code, code del]:
huffman@47108
   106
  "(HOL.equal :: nat \<Rightarrow> _) = HOL.equal" ..
huffman@47108
   107
huffman@47108
   108
lemma equal_nat_code [code]:
huffman@47108
   109
  "HOL.equal 0 (0::nat) \<longleftrightarrow> True"
huffman@47108
   110
  "HOL.equal 0 (nat_of_num l) \<longleftrightarrow> False"
huffman@47108
   111
  "HOL.equal (nat_of_num k) 0 \<longleftrightarrow> False"
huffman@47108
   112
  "HOL.equal (nat_of_num k) (nat_of_num l) \<longleftrightarrow> HOL.equal k l"
huffman@47108
   113
  by (simp_all add: nat_of_num_numeral equal)
huffman@47108
   114
huffman@47108
   115
lemma equal_nat_refl [code nbe]:
huffman@47108
   116
  "HOL.equal (n::nat) n \<longleftrightarrow> True"
huffman@47108
   117
  by (rule equal_refl)
huffman@47108
   118
huffman@47108
   119
lemma [code, code del]:
huffman@47108
   120
  "(less_eq :: nat \<Rightarrow> _) = less_eq" ..
huffman@47108
   121
huffman@47108
   122
lemma less_eq_nat_code [code]:
huffman@47108
   123
  "0 \<le> (n::nat) \<longleftrightarrow> True"
huffman@47108
   124
  "nat_of_num k \<le> 0 \<longleftrightarrow> False"
huffman@47108
   125
  "nat_of_num k \<le> nat_of_num l \<longleftrightarrow> k \<le> l"
huffman@47108
   126
  by (simp_all add: nat_of_num_numeral)
huffman@47108
   127
huffman@47108
   128
lemma [code, code del]:
huffman@47108
   129
  "(less :: nat \<Rightarrow> _) = less" ..
huffman@47108
   130
huffman@47108
   131
lemma less_nat_code [code]:
huffman@47108
   132
  "(m::nat) < 0 \<longleftrightarrow> False"
huffman@47108
   133
  "0 < nat_of_num l \<longleftrightarrow> True"
huffman@47108
   134
  "nat_of_num k < nat_of_num l \<longleftrightarrow> k < l"
huffman@47108
   135
  by (simp_all add: nat_of_num_numeral)
huffman@47108
   136
huffman@47108
   137
huffman@47108
   138
subsection {* Conversions *}
huffman@47108
   139
huffman@47108
   140
lemma [code, code del]:
huffman@47108
   141
  "of_nat = of_nat" ..
huffman@47108
   142
huffman@47108
   143
lemma of_nat_code [code]:
huffman@47108
   144
  "of_nat 0 = 0"
huffman@47108
   145
  "of_nat (nat_of_num k) = numeral k"
huffman@47108
   146
  by (simp_all add: nat_of_num_numeral)
huffman@47108
   147
huffman@47108
   148
huffman@47108
   149
subsection {* Case analysis *}
huffman@47108
   150
huffman@47108
   151
text {*
huffman@47108
   152
  Case analysis on natural numbers is rephrased using a conditional
huffman@47108
   153
  expression:
huffman@47108
   154
*}
huffman@47108
   155
huffman@47108
   156
lemma [code, code_unfold]:
huffman@47108
   157
  "nat_case = (\<lambda>f g n. if n = 0 then f else g (n - 1))"
huffman@47108
   158
  by (auto simp add: fun_eq_iff dest!: gr0_implies_Suc)
huffman@47108
   159
huffman@47108
   160
huffman@47108
   161
subsection {* Preprocessors *}
huffman@47108
   162
huffman@47108
   163
text {*
huffman@47108
   164
  The term @{term "Suc n"} is no longer a valid pattern.
huffman@47108
   165
  Therefore, all occurrences of this term in a position
huffman@47108
   166
  where a pattern is expected (i.e.~on the left-hand side of a recursion
huffman@47108
   167
  equation) must be eliminated.
huffman@47108
   168
  This can be accomplished by applying the following transformation rules:
huffman@47108
   169
*}
huffman@47108
   170
huffman@47108
   171
lemma Suc_if_eq: "(\<And>n. f (Suc n) \<equiv> h n) \<Longrightarrow> f 0 \<equiv> g \<Longrightarrow>
huffman@47108
   172
  f n \<equiv> if n = 0 then g else h (n - 1)"
huffman@47108
   173
  by (rule eq_reflection) (cases n, simp_all)
huffman@47108
   174
huffman@47108
   175
text {*
huffman@47108
   176
  The rules above are built into a preprocessor that is plugged into
huffman@47108
   177
  the code generator. Since the preprocessor for introduction rules
huffman@47108
   178
  does not know anything about modes, some of the modes that worked
huffman@47108
   179
  for the canonical representation of natural numbers may no longer work.
huffman@47108
   180
*}
huffman@47108
   181
huffman@47108
   182
(*<*)
huffman@47108
   183
setup {*
huffman@47108
   184
let
huffman@47108
   185
huffman@47108
   186
fun remove_suc thy thms =
huffman@47108
   187
  let
huffman@47108
   188
    val vname = singleton (Name.variant_list (map fst
huffman@47108
   189
      (fold (Term.add_var_names o Thm.full_prop_of) thms []))) "n";
huffman@47108
   190
    val cv = cterm_of thy (Var ((vname, 0), HOLogic.natT));
huffman@47108
   191
    fun lhs_of th = snd (Thm.dest_comb
huffman@47108
   192
      (fst (Thm.dest_comb (cprop_of th))));
huffman@47108
   193
    fun rhs_of th = snd (Thm.dest_comb (cprop_of th));
huffman@47108
   194
    fun find_vars ct = (case term_of ct of
huffman@47108
   195
        (Const (@{const_name Suc}, _) $ Var _) => [(cv, snd (Thm.dest_comb ct))]
huffman@47108
   196
      | _ $ _ =>
huffman@47108
   197
        let val (ct1, ct2) = Thm.dest_comb ct
huffman@47108
   198
        in 
huffman@47108
   199
          map (apfst (fn ct => Thm.apply ct ct2)) (find_vars ct1) @
huffman@47108
   200
          map (apfst (Thm.apply ct1)) (find_vars ct2)
huffman@47108
   201
        end
huffman@47108
   202
      | _ => []);
huffman@47108
   203
    val eqs = maps
huffman@47108
   204
      (fn th => map (pair th) (find_vars (lhs_of th))) thms;
huffman@47108
   205
    fun mk_thms (th, (ct, cv')) =
huffman@47108
   206
      let
huffman@47108
   207
        val th' =
huffman@47108
   208
          Thm.implies_elim
huffman@47108
   209
           (Conv.fconv_rule (Thm.beta_conversion true)
huffman@47108
   210
             (Drule.instantiate'
huffman@47108
   211
               [SOME (ctyp_of_term ct)] [SOME (Thm.lambda cv ct),
huffman@47108
   212
                 SOME (Thm.lambda cv' (rhs_of th)), NONE, SOME cv']
huffman@47108
   213
               @{thm Suc_if_eq})) (Thm.forall_intr cv' th)
huffman@47108
   214
      in
huffman@47108
   215
        case map_filter (fn th'' =>
huffman@47108
   216
            SOME (th'', singleton
huffman@47108
   217
              (Variable.trade (K (fn [th'''] => [th''' RS th']))
huffman@47108
   218
                (Variable.global_thm_context th'')) th'')
huffman@47108
   219
          handle THM _ => NONE) thms of
huffman@47108
   220
            [] => NONE
huffman@47108
   221
          | thps =>
huffman@47108
   222
              let val (ths1, ths2) = split_list thps
huffman@47108
   223
              in SOME (subtract Thm.eq_thm (th :: ths1) thms @ ths2) end
huffman@47108
   224
      end
huffman@47108
   225
  in get_first mk_thms eqs end;
huffman@47108
   226
huffman@47108
   227
fun eqn_suc_base_preproc thy thms =
huffman@47108
   228
  let
huffman@47108
   229
    val dest = fst o Logic.dest_equals o prop_of;
huffman@47108
   230
    val contains_suc = exists_Const (fn (c, _) => c = @{const_name Suc});
huffman@47108
   231
  in
huffman@47108
   232
    if forall (can dest) thms andalso exists (contains_suc o dest) thms
huffman@47108
   233
      then thms |> perhaps_loop (remove_suc thy) |> (Option.map o map) Drule.zero_var_indexes
huffman@47108
   234
       else NONE
huffman@47108
   235
  end;
huffman@47108
   236
huffman@47108
   237
val eqn_suc_preproc = Code_Preproc.simple_functrans eqn_suc_base_preproc;
huffman@47108
   238
huffman@47108
   239
in
huffman@47108
   240
huffman@47108
   241
  Code_Preproc.add_functrans ("eqn_Suc", eqn_suc_preproc)
huffman@47108
   242
huffman@47108
   243
end;
huffman@47108
   244
*}
huffman@47108
   245
(*>*)
huffman@47108
   246
huffman@47108
   247
code_modulename SML
haftmann@50023
   248
  Code_Binary_Nat Arith
huffman@47108
   249
huffman@47108
   250
code_modulename OCaml
haftmann@50023
   251
  Code_Binary_Nat Arith
huffman@47108
   252
huffman@47108
   253
code_modulename Haskell
haftmann@50023
   254
  Code_Binary_Nat Arith
huffman@47108
   255
huffman@47108
   256
hide_const (open) dup sub
huffman@47108
   257
huffman@47108
   258
end
haftmann@50023
   259