src/HOL/Library/EfficientNat.thy
author wenzelm
Fri Nov 10 10:42:25 2006 +0100 (2006-11-10)
changeset 21287 a713ae348e8a
parent 21191 c00161fbf990
child 21404 eb85850d3eb7
permissions -rw-r--r--
tuned Variable.trade;
berghofe@15323
     1
(*  Title:      HOL/Library/EfficientNat.thy
berghofe@15323
     2
    ID:         $Id$
berghofe@15323
     3
    Author:     Stefan Berghofer, TU Muenchen
berghofe@15323
     4
*)
berghofe@15323
     5
berghofe@15323
     6
header {* Implementation of natural numbers by integers *}
berghofe@15323
     7
berghofe@15323
     8
theory EfficientNat
berghofe@15323
     9
imports Main
berghofe@15323
    10
begin
berghofe@15323
    11
berghofe@15323
    12
text {*
berghofe@15323
    13
When generating code for functions on natural numbers, the canonical
berghofe@15323
    14
representation using @{term "0::nat"} and @{term "Suc"} is unsuitable for
berghofe@15323
    15
computations involving large numbers. The efficiency of the generated
berghofe@15323
    16
code can be improved drastically by implementing natural numbers by
berghofe@15323
    17
integers. To do this, just include this theory.
berghofe@15323
    18
*}
berghofe@15323
    19
haftmann@20700
    20
subsection {* Logical rewrites *}
berghofe@15323
    21
berghofe@15323
    22
text {*
haftmann@20700
    23
  A int-to-nat conversion with domain
haftmann@20700
    24
  restricted to non-negative ints (in contrast to @{const nat}).
berghofe@16770
    25
*}
berghofe@16770
    26
haftmann@20641
    27
definition
haftmann@20641
    28
  nat_of_int :: "int \<Rightarrow> nat"
haftmann@20641
    29
  "k \<ge> 0 \<Longrightarrow> nat_of_int k = nat k"
haftmann@19889
    30
haftmann@20839
    31
lemma nat_of_int_int:
haftmann@20839
    32
  "nat_of_int (int n) = n"
haftmann@20839
    33
  using zero_zle_int nat_of_int_def by simp
haftmann@20839
    34
haftmann@19889
    35
text {*
haftmann@20700
    36
  Case analysis on natural numbers is rephrased using a conditional
haftmann@20700
    37
  expression:
berghofe@15323
    38
*}
berghofe@15323
    39
haftmann@20839
    40
lemma [code unfold, code noinline]: "nat_case \<equiv> (\<lambda>f g n. if n = 0 then f else g (n - 1))"
haftmann@20700
    41
proof -
haftmann@20700
    42
  have rewrite: "\<And>f g n. nat_case f g n = (if n = 0 then f else g (n - 1))"
haftmann@20700
    43
  proof -
haftmann@20700
    44
    fix f g n
haftmann@20700
    45
    show "nat_case f g n = (if n = 0 then f else g (n - 1))"
haftmann@20700
    46
      by (cases n) simp_all
haftmann@20700
    47
  qed
haftmann@20700
    48
  show "nat_case \<equiv> (\<lambda>f g n. if n = 0 then f else g (n - 1))"
haftmann@20700
    49
    by (rule eq_reflection ext rewrite)+ 
haftmann@20700
    50
qed
berghofe@15323
    51
haftmann@20839
    52
lemma [code inline]:
haftmann@21046
    53
  "nat_case f g n = (if Code_Generator.eq n 0 then f else g (nat_of_int (int n - 1)))"
haftmann@20839
    54
  by (cases n) (simp_all add: eq_def nat_of_int_int)
haftmann@20839
    55
berghofe@15323
    56
text {*
haftmann@20700
    57
  Most standard arithmetic functions on natural numbers are implemented
haftmann@20700
    58
  using their counterparts on the integers:
berghofe@15323
    59
*}
berghofe@15323
    60
haftmann@20641
    61
lemma [code func]: "0 = nat_of_int 0"
haftmann@20641
    62
  by (simp add: nat_of_int_def)
haftmann@20641
    63
lemma [code func, code inline]:  "1 = nat_of_int 1"
haftmann@20641
    64
  by (simp add: nat_of_int_def)
haftmann@20641
    65
lemma [code func]: "Suc n = n + 1"
haftmann@20641
    66
  by simp
haftmann@20641
    67
lemma [code, code inline]: "m + n = nat (int m + int n)"
haftmann@20641
    68
  by arith
haftmann@20641
    69
lemma [code func, code inline]: "m + n = nat_of_int (int m + int n)"
haftmann@20641
    70
  by (simp add: nat_of_int_def)
haftmann@20641
    71
lemma [code, code inline]: "m - n = nat (int m - int n)"
haftmann@20641
    72
  by arith
haftmann@20641
    73
lemma [code, code inline]: "m * n = nat (int m * int n)"
haftmann@20641
    74
  unfolding zmult_int by simp
haftmann@20641
    75
lemma [code func, code inline]: "m * n = nat_of_int (int m * int n)"
haftmann@20641
    76
proof -
haftmann@20641
    77
  have "int (m * n) = int m * int n"
haftmann@20641
    78
    by (induct m) (simp_all add: zadd_zmult_distrib)
haftmann@20641
    79
  then have "m * n = nat (int m * int n)" by auto
haftmann@20641
    80
  also have "\<dots> = nat_of_int (int m * int n)"
haftmann@20641
    81
  proof -
haftmann@20641
    82
    have "int m \<ge> 0" and "int n \<ge> 0" by auto
haftmann@20641
    83
    have "int m * int n \<ge> 0" by (rule split_mult_pos_le) auto
haftmann@20641
    84
    with nat_of_int_def show ?thesis by auto
haftmann@20641
    85
  qed
haftmann@20641
    86
  finally show ?thesis .
haftmann@20641
    87
qed  
haftmann@20641
    88
lemma [code]: "m div n = nat (int m div int n)"
haftmann@20641
    89
  unfolding zdiv_int [symmetric] by simp
haftmann@20641
    90
lemma [code func]: "m div n = fst (Divides.divmod m n)"
haftmann@20641
    91
  unfolding divmod_def by simp
haftmann@20641
    92
lemma [code]: "m mod n = nat (int m mod int n)"
haftmann@20641
    93
  unfolding zmod_int [symmetric] by simp
haftmann@20641
    94
lemma [code func]: "m mod n = snd (Divides.divmod m n)"
haftmann@20641
    95
  unfolding divmod_def by simp
haftmann@20641
    96
lemma [code, code inline]: "(m < n) \<longleftrightarrow> (int m < int n)"
haftmann@20641
    97
  by simp
haftmann@20641
    98
lemma [code func, code inline]: "(m \<le> n) \<longleftrightarrow> (int m \<le> int n)"
haftmann@20641
    99
  by simp
haftmann@21046
   100
lemma [code func, code inline]: "Code_Generator.eq m n \<longleftrightarrow> Code_Generator.eq (int m) (int n)"
haftmann@20641
   101
  unfolding eq_def by simp
haftmann@20641
   102
lemma [code func]: "nat k = (if k < 0 then 0 else nat_of_int k)"
haftmann@20641
   103
proof (cases "k < 0")
haftmann@20641
   104
  case True then show ?thesis by simp
haftmann@20641
   105
next
haftmann@20641
   106
  case False then show ?thesis by (simp add: nat_of_int_def)
haftmann@20641
   107
qed
krauss@20523
   108
lemma [code func]:
haftmann@20641
   109
  "int_aux i n = (if int n = 0 then i else int_aux (i + 1) (nat_of_int (int n - 1)))"
haftmann@20641
   110
proof -
haftmann@20641
   111
  have "0 < n \<Longrightarrow> int n = 1 + int (nat_of_int (int n - 1))"
haftmann@20641
   112
  proof -
haftmann@20641
   113
    assume prem: "n > 0"
haftmann@20641
   114
    then have "int n - 1 \<ge> 0" by auto
haftmann@20641
   115
    then have "nat_of_int (int n - 1) = nat (int n - 1)" by (simp add: nat_of_int_def)
haftmann@20641
   116
    with prem show "int n = 1 + int (nat_of_int (int n - 1))" by simp
haftmann@20641
   117
  qed
haftmann@20641
   118
  then show ?thesis unfolding int_aux_def by simp
haftmann@20641
   119
qed
haftmann@20356
   120
berghofe@15323
   121
haftmann@20700
   122
subsection {* Code generator setup for basic functions *}
haftmann@20700
   123
haftmann@20700
   124
text {*
haftmann@20700
   125
  @{typ nat} is no longer a datatype but embedded into the integers.
haftmann@20700
   126
*}
haftmann@20700
   127
haftmann@20839
   128
code_const "0::nat"
haftmann@21113
   129
  (SML "!(0 : IntInf.int)")
haftmann@21113
   130
  (Haskell "0")
haftmann@20839
   131
haftmann@20839
   132
code_const "Suc"
haftmann@21125
   133
  (SML "IntInf.+ ((_), 1)")
haftmann@21125
   134
  (Haskell "!((_) + 1)")
haftmann@20839
   135
haftmann@20700
   136
setup {*
haftmann@20700
   137
  CodegenData.del_datatype "nat"
haftmann@20700
   138
*}
haftmann@20700
   139
haftmann@20700
   140
types_code
haftmann@20700
   141
  nat ("int")
haftmann@20700
   142
attach (term_of) {*
haftmann@20713
   143
fun term_of_nat 0 = Const ("HOL.zero", HOLogic.natT)
haftmann@20713
   144
  | term_of_nat 1 = Const ("HOL.one", HOLogic.natT)
haftmann@20700
   145
  | term_of_nat i = HOLogic.number_of_const HOLogic.natT $
haftmann@20700
   146
      HOLogic.mk_binum (IntInf.fromInt i);
haftmann@20700
   147
*}
haftmann@20700
   148
attach (test) {*
haftmann@20700
   149
fun gen_nat i = random_range 0 i;
haftmann@20700
   150
*}
haftmann@20700
   151
haftmann@20700
   152
code_type nat
haftmann@21113
   153
  (SML "IntInf.int")
haftmann@21113
   154
  (Haskell "Integer")
haftmann@20700
   155
haftmann@20700
   156
consts_code
haftmann@20713
   157
  "HOL.zero" :: nat ("0")
haftmann@20700
   158
  Suc ("(_ + 1)")
haftmann@20700
   159
haftmann@20700
   160
text {*
haftmann@20700
   161
  Since natural numbers are implemented
haftmann@20700
   162
  using integers, the coercion function @{const "int"} of type
haftmann@20700
   163
  @{typ "nat \<Rightarrow> int"} is simply implemented by the identity function,
haftmann@20700
   164
  likewise @{const nat_of_int} of type @{typ "int \<Rightarrow> nat"}.
haftmann@20700
   165
  For the @{const "nat"} function for converting an integer to a natural
haftmann@20700
   166
  number, we give a specific implementation using an ML function that
haftmann@20700
   167
  returns its input value, provided that it is non-negative, and otherwise
haftmann@20700
   168
  returns @{text "0"}.
haftmann@20700
   169
*}
haftmann@20700
   170
haftmann@20700
   171
consts_code
haftmann@20700
   172
  int ("(_)")
haftmann@20700
   173
  nat ("\<module>nat")
haftmann@20700
   174
attach {*
haftmann@20700
   175
fun nat i = if i < 0 then 0 else i;
haftmann@20700
   176
*}
haftmann@20700
   177
haftmann@20700
   178
code_const int
haftmann@20700
   179
  (SML "_")
haftmann@20700
   180
  (Haskell "_")
haftmann@20700
   181
haftmann@20700
   182
code_const nat_of_int
haftmann@20700
   183
  (SML "_")
haftmann@20700
   184
  (Haskell "_")
haftmann@20700
   185
haftmann@20700
   186
berghofe@15323
   187
subsection {* Preprocessors *}
berghofe@15323
   188
berghofe@15323
   189
text {*
haftmann@20700
   190
  In contrast to @{term "Suc n"}, the term @{term "n + (1::nat)"} is no longer
haftmann@20700
   191
  a constructor term. Therefore, all occurrences of this term in a position
haftmann@20700
   192
  where a pattern is expected (i.e.\ on the left-hand side of a recursion
haftmann@20700
   193
  equation or in the arguments of an inductive relation in an introduction
haftmann@20700
   194
  rule) must be eliminated.
haftmann@20700
   195
  This can be accomplished by applying the following transformation rules:
berghofe@15323
   196
*}
berghofe@15323
   197
berghofe@16900
   198
theorem Suc_if_eq: "(\<And>n. f (Suc n) = h n) \<Longrightarrow> f 0 = g \<Longrightarrow>
berghofe@15323
   199
  f n = (if n = 0 then g else h (n - 1))"
berghofe@15323
   200
  by (case_tac n) simp_all
berghofe@15323
   201
berghofe@15323
   202
theorem Suc_clause: "(\<And>n. P n (Suc n)) \<Longrightarrow> n \<noteq> 0 \<Longrightarrow> P (n - 1) n"
berghofe@15323
   203
  by (case_tac n) simp_all
berghofe@15323
   204
berghofe@15323
   205
text {*
haftmann@20700
   206
  The rules above are built into a preprocessor that is plugged into
haftmann@20700
   207
  the code generator. Since the preprocessor for introduction rules
haftmann@20700
   208
  does not know anything about modes, some of the modes that worked
haftmann@20700
   209
  for the canonical representation of natural numbers may no longer work.
berghofe@15323
   210
*}
berghofe@15323
   211
berghofe@15323
   212
(*<*)
haftmann@19791
   213
berghofe@15323
   214
ML {*
haftmann@19791
   215
local
haftmann@19791
   216
  val Suc_if_eq = thm "Suc_if_eq";
haftmann@19791
   217
  val Suc_clause = thm "Suc_clause";
haftmann@19791
   218
  fun contains_suc t = member (op =) (term_consts t) "Suc";
haftmann@19791
   219
in
berghofe@15323
   220
berghofe@15396
   221
fun remove_suc thy thms =
berghofe@15323
   222
  let
berghofe@15396
   223
    val Suc_if_eq' = Thm.transfer thy Suc_if_eq;
wenzelm@20071
   224
    val vname = Name.variant (map fst
wenzelm@20196
   225
      (fold (Term.add_varnames o Thm.full_prop_of) thms [])) "x";
wenzelm@16861
   226
    val cv = cterm_of Main.thy (Var ((vname, 0), HOLogic.natT));
berghofe@15323
   227
    fun lhs_of th = snd (Thm.dest_comb
berghofe@15323
   228
      (fst (Thm.dest_comb (snd (Thm.dest_comb (cprop_of th))))));
berghofe@15323
   229
    fun rhs_of th = snd (Thm.dest_comb (snd (Thm.dest_comb (cprop_of th))));
berghofe@15323
   230
    fun find_vars ct = (case term_of ct of
berghofe@16900
   231
        (Const ("Suc", _) $ Var _) => [(cv, snd (Thm.dest_comb ct))]
berghofe@15323
   232
      | _ $ _ =>
berghofe@15323
   233
        let val (ct1, ct2) = Thm.dest_comb ct
berghofe@15323
   234
        in 
berghofe@16900
   235
          map (apfst (fn ct => Thm.capply ct ct2)) (find_vars ct1) @
berghofe@16900
   236
          map (apfst (Thm.capply ct1)) (find_vars ct2)
berghofe@15323
   237
        end
berghofe@15323
   238
      | _ => []);
berghofe@16900
   239
    val eqs = List.concat (map
berghofe@15323
   240
      (fn th => map (pair th) (find_vars (lhs_of th))) thms);
berghofe@16900
   241
    fun mk_thms (th, (ct, cv')) =
berghofe@15323
   242
      let
berghofe@16900
   243
        val th' =
berghofe@16900
   244
          Thm.implies_elim
berghofe@15396
   245
           (Drule.fconv_rule (Thm.beta_conversion true)
berghofe@15323
   246
             (Drule.instantiate'
skalberg@15531
   247
               [SOME (ctyp_of_term ct)] [SOME (Thm.cabs cv ct),
berghofe@16900
   248
                 SOME (Thm.cabs cv' (rhs_of th)), NONE, SOME cv']
berghofe@16900
   249
               Suc_if_eq')) (Thm.forall_intr cv' th)
berghofe@15323
   250
      in
wenzelm@21287
   251
        case map_filter (fn th'' =>
wenzelm@20287
   252
            SOME (th'', singleton
wenzelm@21287
   253
              (Variable.trade (K (fn [th'''] => [th''' RS th'])) (Variable.thm_context th'')) th'')
berghofe@16900
   254
          handle THM _ => NONE) thms of
berghofe@16900
   255
            [] => NONE
berghofe@16900
   256
          | thps =>
haftmann@19791
   257
              let val (ths1, ths2) = split_list thps
haftmann@20951
   258
              in SOME (subtract eq_thm (th :: ths1) thms @ ths2) end
berghofe@15323
   259
      end
berghofe@15323
   260
  in
haftmann@19791
   261
    case get_first mk_thms eqs of
berghofe@16900
   262
      NONE => thms
berghofe@16900
   263
    | SOME x => remove_suc thy x
berghofe@15323
   264
  end;
berghofe@15323
   265
berghofe@15323
   266
fun eqn_suc_preproc thy ths =
haftmann@19791
   267
  let
haftmann@19791
   268
    val dest = fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of
berghofe@15323
   269
  in
berghofe@15323
   270
    if forall (can dest) ths andalso
haftmann@19791
   271
      exists (contains_suc o dest) ths
berghofe@15396
   272
    then remove_suc thy ths else ths
berghofe@15323
   273
  end;
berghofe@15323
   274
berghofe@15396
   275
fun remove_suc_clause thy thms =
berghofe@15323
   276
  let
berghofe@15396
   277
    val Suc_clause' = Thm.transfer thy Suc_clause;
wenzelm@20071
   278
    val vname = Name.variant (map fst
wenzelm@20196
   279
      (fold (Term.add_varnames o Thm.full_prop_of) thms [])) "x";
skalberg@15531
   280
    fun find_var (t as Const ("Suc", _) $ (v as Var _)) = SOME (t, v)
skalberg@15531
   281
      | find_var (t $ u) = (case find_var t of NONE => find_var u | x => x)
skalberg@15531
   282
      | find_var _ = NONE;
berghofe@15323
   283
    fun find_thm th =
berghofe@15323
   284
      let val th' = ObjectLogic.atomize_thm th
skalberg@15570
   285
      in Option.map (pair (th, th')) (find_var (prop_of th')) end
berghofe@15323
   286
  in
berghofe@15323
   287
    case get_first find_thm thms of
skalberg@15531
   288
      NONE => thms
skalberg@15531
   289
    | SOME ((th, th'), (Sucv, v)) =>
berghofe@15323
   290
        let
wenzelm@16861
   291
          val cert = cterm_of (Thm.theory_of_thm th);
berghofe@15323
   292
          val th'' = ObjectLogic.rulify (Thm.implies_elim
berghofe@15396
   293
            (Drule.fconv_rule (Thm.beta_conversion true)
berghofe@15323
   294
              (Drule.instantiate' []
skalberg@15531
   295
                [SOME (cert (lambda v (Abs ("x", HOLogic.natT,
berghofe@15323
   296
                   abstract_over (Sucv,
berghofe@19828
   297
                     HOLogic.dest_Trueprop (prop_of th')))))),
skalberg@15531
   298
                 SOME (cert v)] Suc_clause'))
berghofe@15323
   299
            (Thm.forall_intr (cert v) th'))
berghofe@15323
   300
        in
berghofe@15396
   301
          remove_suc_clause thy (map (fn th''' =>
wenzelm@19617
   302
            if (op = o pairself prop_of) (th''', th) then th'' else th''') thms)
berghofe@15323
   303
        end
berghofe@15323
   304
  end;
berghofe@15323
   305
berghofe@15323
   306
fun clause_suc_preproc thy ths =
haftmann@19791
   307
  let
berghofe@19828
   308
    val dest = fst o HOLogic.dest_mem o HOLogic.dest_Trueprop
berghofe@15323
   309
  in
berghofe@15323
   310
    if forall (can (dest o concl_of)) ths andalso
haftmann@19791
   311
      exists (fn th => member (op =) (foldr add_term_consts
wenzelm@21287
   312
        [] (map_filter (try dest) (concl_of th :: prems_of th))) "Suc") ths
berghofe@15396
   313
    then remove_suc_clause thy ths else ths
berghofe@15323
   314
  end;
berghofe@15323
   315
haftmann@19791
   316
end; (*local*)
haftmann@19791
   317
haftmann@19791
   318
fun lift_obj_eq f thy =
haftmann@19791
   319
  map (fn thm => thm RS meta_eq_to_obj_eq)
haftmann@19791
   320
  #> f thy
haftmann@19791
   321
  #> map (fn thm => thm RS HOL.eq_reflection)
haftmann@19791
   322
*}
haftmann@19791
   323
haftmann@19791
   324
setup {*
haftmann@19603
   325
  Codegen.add_preprocessor eqn_suc_preproc
haftmann@19603
   326
  #> Codegen.add_preprocessor clause_suc_preproc
haftmann@20597
   327
  #> CodegenData.add_preproc (lift_obj_eq eqn_suc_preproc)
haftmann@20597
   328
  #> CodegenData.add_preproc (lift_obj_eq clause_suc_preproc)
berghofe@15323
   329
*}
berghofe@15323
   330
(*>*)
berghofe@15323
   331
haftmann@21191
   332
subsection {* Module names *}
haftmann@21191
   333
haftmann@21191
   334
code_modulename SML
haftmann@21191
   335
  Nat Integer
haftmann@21191
   336
  EfficientNat Integer
haftmann@21191
   337
berghofe@15323
   338
end