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