src/HOL/Library/EfficientNat.thy
author wenzelm
Thu Jan 19 21:22:08 2006 +0100 (2006-01-19 ago)
changeset 18708 4b3dadb4fe33
parent 18702 7dc7dcd63224
child 18757 f0d901bc0686
permissions -rw-r--r--
setup: theory -> theory;
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
berghofe@15323
    20
subsection {* Basic functions *}
berghofe@15323
    21
berghofe@15323
    22
text {*
berghofe@15323
    23
The implementation of @{term "0::nat"} and @{term "Suc"} using the
berghofe@15323
    24
ML integers is straightforward. Since natural numbers are implemented
berghofe@15323
    25
using integers, the coercion function @{term "int"} of type
berghofe@15323
    26
@{typ "nat \<Rightarrow> int"} is simply implemented by the identity function.
berghofe@15323
    27
For the @{term "nat"} function for converting an integer to a natural
berghofe@15323
    28
number, we give a specific implementation using an ML function that
berghofe@15323
    29
returns its input value, provided that it is non-negative, and otherwise
berghofe@15323
    30
returns @{text "0"}.
berghofe@15323
    31
*}
berghofe@15323
    32
berghofe@16770
    33
types_code
berghofe@16770
    34
  nat ("int")
berghofe@16770
    35
attach (term_of) {*
berghofe@16770
    36
fun term_of_nat 0 = Const ("0", HOLogic.natT)
berghofe@16770
    37
  | term_of_nat 1 = Const ("1", HOLogic.natT)
berghofe@16770
    38
  | term_of_nat i = HOLogic.number_of_const HOLogic.natT $
berghofe@16770
    39
      HOLogic.mk_bin (IntInf.fromInt i);
berghofe@16770
    40
*}
berghofe@16770
    41
attach (test) {*
berghofe@16770
    42
fun gen_nat i = random_range 0 i;
berghofe@16770
    43
*}
berghofe@16770
    44
berghofe@15323
    45
consts_code
berghofe@15323
    46
  0 :: nat ("0")
berghofe@15323
    47
  Suc ("(_ + 1)")
berghofe@16770
    48
  nat ("\<module>nat")
berghofe@16770
    49
attach {*
berghofe@15323
    50
fun nat i = if i < 0 then 0 else i;
berghofe@15323
    51
*}
berghofe@16770
    52
  int ("(_)")
berghofe@15323
    53
haftmann@18702
    54
(* code_syntax_tyco nat
haftmann@18702
    55
  ml (atom "InfInt.int")
haftmann@18702
    56
  haskell (atom "Integer")
haftmann@18702
    57
haftmann@18702
    58
code_syntax_const 0 :: nat
haftmann@18702
    59
  ml ("0 : InfInt.int")
haftmann@18702
    60
  haskell (atom "0")
haftmann@18702
    61
haftmann@18702
    62
code_syntax_const Suc
haftmann@18702
    63
  ml (infixl 8 "_ + 1")
haftmann@18702
    64
  haskell (infixl 6 "_ + 1")
haftmann@18702
    65
haftmann@18702
    66
code_primconst nat
haftmann@18702
    67
ml {*
haftmann@18702
    68
fun nat i = if i < 0 then 0 else i;
haftmann@18702
    69
*}
haftmann@18702
    70
haskell {*
haftmann@18702
    71
nat i = if i < 0 then 0 else i
haftmann@18702
    72
*} *)
haftmann@18702
    73
berghofe@15323
    74
text {*
berghofe@15323
    75
Case analysis on natural numbers is rephrased using a conditional
berghofe@15323
    76
expression:
berghofe@15323
    77
*}
berghofe@15323
    78
berghofe@15323
    79
lemma [code unfold]: "nat_case \<equiv> (\<lambda>f g n. if n = 0 then f else g (n - 1))"
berghofe@15323
    80
  apply (rule eq_reflection ext)+
berghofe@15323
    81
  apply (case_tac n)
berghofe@15323
    82
  apply simp_all
berghofe@15323
    83
  done
berghofe@15323
    84
berghofe@15323
    85
text {*
berghofe@15323
    86
Most standard arithmetic functions on natural numbers are implemented
berghofe@15323
    87
using their counterparts on the integers:
berghofe@15323
    88
*}
berghofe@15323
    89
berghofe@15323
    90
lemma [code]: "m - n = nat (int m - int n)" by arith
berghofe@15323
    91
lemma [code]: "m + n = nat (int m + int n)" by arith
berghofe@15323
    92
lemma [code]: "m * n = nat (int m * int n)"
berghofe@15323
    93
  by (simp add: zmult_int)
berghofe@15323
    94
lemma [code]: "m div n = nat (int m div int n)"
berghofe@15323
    95
  by (simp add: zdiv_int [symmetric])
berghofe@15323
    96
lemma [code]: "m mod n = nat (int m mod int n)"
berghofe@15323
    97
  by (simp add: zmod_int [symmetric])
berghofe@16295
    98
lemma [code]: "(m < n) = (int m < int n)"
berghofe@16295
    99
  by simp
berghofe@15323
   100
berghofe@15323
   101
subsection {* Preprocessors *}
berghofe@15323
   102
berghofe@15323
   103
text {*
berghofe@15323
   104
In contrast to @{term "Suc n"}, the term @{term "n + (1::nat)"} is no longer
berghofe@15323
   105
a constructor term. Therefore, all occurrences of this term in a position
berghofe@15323
   106
where a pattern is expected (i.e.\ on the left-hand side of a recursion
berghofe@15323
   107
equation or in the arguments of an inductive relation in an introduction
berghofe@15323
   108
rule) must be eliminated.
berghofe@15323
   109
This can be accomplished by applying the following transformation rules:
berghofe@15323
   110
*}
berghofe@15323
   111
berghofe@16900
   112
theorem Suc_if_eq: "(\<And>n. f (Suc n) = h n) \<Longrightarrow> f 0 = g \<Longrightarrow>
berghofe@15323
   113
  f n = (if n = 0 then g else h (n - 1))"
berghofe@15323
   114
  by (case_tac n) simp_all
berghofe@15323
   115
berghofe@15323
   116
theorem Suc_clause: "(\<And>n. P n (Suc n)) \<Longrightarrow> n \<noteq> 0 \<Longrightarrow> P (n - 1) n"
berghofe@15323
   117
  by (case_tac n) simp_all
berghofe@15323
   118
berghofe@15323
   119
text {*
berghofe@15323
   120
The rules above are built into a preprocessor that is plugged into
berghofe@15323
   121
the code generator. Since the preprocessor for introduction rules
berghofe@15323
   122
does not know anything about modes, some of the modes that worked
berghofe@15323
   123
for the canonical representation of natural numbers may no longer work.
berghofe@15323
   124
*}
berghofe@15323
   125
berghofe@15323
   126
(*<*)
berghofe@15323
   127
ML {*
berghofe@15323
   128
val Suc_if_eq = thm "Suc_if_eq";
berghofe@15323
   129
berghofe@15396
   130
fun remove_suc thy thms =
berghofe@15323
   131
  let
berghofe@15396
   132
    val Suc_if_eq' = Thm.transfer thy Suc_if_eq;
berghofe@15323
   133
    val vname = variant (map fst
wenzelm@16861
   134
      (fold (add_term_varnames o Thm.full_prop_of) thms [])) "x";
wenzelm@16861
   135
    val cv = cterm_of Main.thy (Var ((vname, 0), HOLogic.natT));
berghofe@15323
   136
    fun lhs_of th = snd (Thm.dest_comb
berghofe@15323
   137
      (fst (Thm.dest_comb (snd (Thm.dest_comb (cprop_of th))))));
berghofe@15323
   138
    fun rhs_of th = snd (Thm.dest_comb (snd (Thm.dest_comb (cprop_of th))));
berghofe@15323
   139
    fun find_vars ct = (case term_of ct of
berghofe@16900
   140
        (Const ("Suc", _) $ Var _) => [(cv, snd (Thm.dest_comb ct))]
berghofe@15323
   141
      | _ $ _ =>
berghofe@15323
   142
        let val (ct1, ct2) = Thm.dest_comb ct
berghofe@15323
   143
        in 
berghofe@16900
   144
          map (apfst (fn ct => Thm.capply ct ct2)) (find_vars ct1) @
berghofe@16900
   145
          map (apfst (Thm.capply ct1)) (find_vars ct2)
berghofe@15323
   146
        end
berghofe@15323
   147
      | _ => []);
berghofe@16900
   148
    val eqs = List.concat (map
berghofe@15323
   149
      (fn th => map (pair th) (find_vars (lhs_of th))) thms);
berghofe@16900
   150
    fun mk_thms (th, (ct, cv')) =
berghofe@15323
   151
      let
berghofe@16900
   152
        val th' =
berghofe@16900
   153
          Thm.implies_elim
berghofe@15396
   154
           (Drule.fconv_rule (Thm.beta_conversion true)
berghofe@15323
   155
             (Drule.instantiate'
skalberg@15531
   156
               [SOME (ctyp_of_term ct)] [SOME (Thm.cabs cv ct),
berghofe@16900
   157
                 SOME (Thm.cabs cv' (rhs_of th)), NONE, SOME cv']
berghofe@16900
   158
               Suc_if_eq')) (Thm.forall_intr cv' th)
berghofe@15323
   159
      in
berghofe@16900
   160
        case List.mapPartial (fn th'' =>
berghofe@16900
   161
            SOME (th'', standard (Drule.freeze_all th'' RS th'))
berghofe@16900
   162
          handle THM _ => NONE) thms of
berghofe@16900
   163
            [] => NONE
berghofe@16900
   164
          | thps =>
berghofe@16900
   165
              let val (ths1, ths2) = ListPair.unzip thps
berghofe@16900
   166
              in SOME (gen_rems eq_thm (thms, th :: ths1) @ ths2) end
berghofe@15323
   167
      end
berghofe@15323
   168
  in
berghofe@16900
   169
    case Library.get_first mk_thms eqs of
berghofe@16900
   170
      NONE => thms
berghofe@16900
   171
    | SOME x => remove_suc thy x
berghofe@15323
   172
  end;
berghofe@15323
   173
berghofe@15323
   174
fun eqn_suc_preproc thy ths =
berghofe@15323
   175
  let val dest = fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of
berghofe@15323
   176
  in
berghofe@15323
   177
    if forall (can dest) ths andalso
berghofe@15323
   178
      exists (fn th => "Suc" mem term_consts (dest th)) ths
berghofe@15396
   179
    then remove_suc thy ths else ths
berghofe@15323
   180
  end;
berghofe@15323
   181
berghofe@15323
   182
val Suc_clause = thm "Suc_clause";
berghofe@15323
   183
berghofe@15396
   184
fun remove_suc_clause thy thms =
berghofe@15323
   185
  let
berghofe@15396
   186
    val Suc_clause' = Thm.transfer thy Suc_clause;
berghofe@15323
   187
    val vname = variant (map fst
wenzelm@16861
   188
      (fold (add_term_varnames o Thm.full_prop_of) thms [])) "x";
skalberg@15531
   189
    fun find_var (t as Const ("Suc", _) $ (v as Var _)) = SOME (t, v)
skalberg@15531
   190
      | find_var (t $ u) = (case find_var t of NONE => find_var u | x => x)
skalberg@15531
   191
      | find_var _ = NONE;
berghofe@15323
   192
    fun find_thm th =
berghofe@15323
   193
      let val th' = ObjectLogic.atomize_thm th
skalberg@15570
   194
      in Option.map (pair (th, th')) (find_var (prop_of th')) end
berghofe@15323
   195
  in
berghofe@15323
   196
    case get_first find_thm thms of
skalberg@15531
   197
      NONE => thms
skalberg@15531
   198
    | SOME ((th, th'), (Sucv, v)) =>
berghofe@15323
   199
        let
wenzelm@16861
   200
          val cert = cterm_of (Thm.theory_of_thm th);
berghofe@15323
   201
          val th'' = ObjectLogic.rulify (Thm.implies_elim
berghofe@15396
   202
            (Drule.fconv_rule (Thm.beta_conversion true)
berghofe@15323
   203
              (Drule.instantiate' []
skalberg@15531
   204
                [SOME (cert (lambda v (Abs ("x", HOLogic.natT,
berghofe@15323
   205
                   abstract_over (Sucv,
berghofe@15323
   206
                     HOLogic.dest_Trueprop (prop_of th')))))),
skalberg@15531
   207
                 SOME (cert v)] Suc_clause'))
berghofe@15323
   208
            (Thm.forall_intr (cert v) th'))
berghofe@15323
   209
        in
berghofe@15396
   210
          remove_suc_clause thy (map (fn th''' =>
berghofe@15323
   211
            if th''' = th then th'' else th''') thms)
berghofe@15323
   212
        end
berghofe@15323
   213
  end;
berghofe@15323
   214
berghofe@15323
   215
fun clause_suc_preproc thy ths =
berghofe@15323
   216
  let val dest = fst o HOLogic.dest_mem o HOLogic.dest_Trueprop
berghofe@15323
   217
  in
berghofe@15323
   218
    if forall (can (dest o concl_of)) ths andalso
skalberg@15574
   219
      exists (fn th => "Suc" mem foldr add_term_consts
skalberg@15574
   220
        [] (List.mapPartial (try dest) (concl_of th :: prems_of th))) ths
berghofe@15396
   221
    then remove_suc_clause thy ths else ths
berghofe@15323
   222
  end;
berghofe@15323
   223
berghofe@15323
   224
val suc_preproc_setup =
wenzelm@18708
   225
  Codegen.add_preprocessor eqn_suc_preproc #>
wenzelm@18708
   226
  Codegen.add_preprocessor clause_suc_preproc;
berghofe@15323
   227
*}
berghofe@15323
   228
berghofe@15323
   229
setup suc_preproc_setup
berghofe@15323
   230
(*>*)
berghofe@15323
   231
berghofe@15323
   232
end