src/HOL/Library/EfficientNat.thy
author paulson
Tue Jun 28 15:27:45 2005 +0200 (2005-06-28)
changeset 16587 b34c8aa657a5
parent 16295 cd7a83dae4f9
child 16770 1f1b1fae30e4
permissions -rw-r--r--
Constant "If" is now local
     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 nat ("int")
    34 consts_code
    35   0 :: nat ("0")
    36   Suc ("(_ + 1)")
    37   nat ("nat")
    38   int ("(_)")
    39 
    40 ML {*
    41 fun nat i = if i < 0 then 0 else i;
    42 *}
    43 
    44 text {*
    45 Case analysis on natural numbers is rephrased using a conditional
    46 expression:
    47 *}
    48 
    49 lemma [code unfold]: "nat_case \<equiv> (\<lambda>f g n. if n = 0 then f else g (n - 1))"
    50   apply (rule eq_reflection ext)+
    51   apply (case_tac n)
    52   apply simp_all
    53   done
    54 
    55 text {*
    56 Most standard arithmetic functions on natural numbers are implemented
    57 using their counterparts on the integers:
    58 *}
    59 
    60 lemma [code]: "m - n = nat (int m - int n)" by arith
    61 lemma [code]: "m + n = nat (int m + int n)" by arith
    62 lemma [code]: "m * n = nat (int m * int n)"
    63   by (simp add: zmult_int)
    64 lemma [code]: "m div n = nat (int m div int n)"
    65   by (simp add: zdiv_int [symmetric])
    66 lemma [code]: "m mod n = nat (int m mod int n)"
    67   by (simp add: zmod_int [symmetric])
    68 lemma [code]: "(m < n) = (int m < int n)"
    69   by simp
    70 
    71 subsection {* Preprocessors *}
    72 
    73 text {*
    74 In contrast to @{term "Suc n"}, the term @{term "n + (1::nat)"} is no longer
    75 a constructor term. Therefore, all occurrences of this term in a position
    76 where a pattern is expected (i.e.\ on the left-hand side of a recursion
    77 equation or in the arguments of an inductive relation in an introduction
    78 rule) must be eliminated.
    79 This can be accomplished by applying the following transformation rules:
    80 *}
    81 
    82 theorem Suc_if_eq: "f 0 = g \<Longrightarrow> (\<And>n. f (Suc n) = h n) \<Longrightarrow>
    83   f n = (if n = 0 then g else h (n - 1))"
    84   by (case_tac n) simp_all
    85 
    86 theorem Suc_clause: "(\<And>n. P n (Suc n)) \<Longrightarrow> n \<noteq> 0 \<Longrightarrow> P (n - 1) n"
    87   by (case_tac n) simp_all
    88 
    89 text {*
    90 The rules above are built into a preprocessor that is plugged into
    91 the code generator. Since the preprocessor for introduction rules
    92 does not know anything about modes, some of the modes that worked
    93 for the canonical representation of natural numbers may no longer work.
    94 *}
    95 
    96 (*<*)
    97 ML {*
    98 val Suc_if_eq = thm "Suc_if_eq";
    99 
   100 fun remove_suc thy thms =
   101   let
   102     val Suc_if_eq' = Thm.transfer thy Suc_if_eq;
   103     val ctzero = cterm_of (sign_of Main.thy) HOLogic.zero;
   104     val vname = variant (map fst
   105       (Library.foldl add_term_varnames ([], map prop_of thms))) "x";
   106     val cv = cterm_of (sign_of Main.thy) (Var ((vname, 0), HOLogic.natT));
   107     fun lhs_of th = snd (Thm.dest_comb
   108       (fst (Thm.dest_comb (snd (Thm.dest_comb (cprop_of th))))));
   109     fun rhs_of th = snd (Thm.dest_comb (snd (Thm.dest_comb (cprop_of th))));
   110     fun find_vars ct = (case term_of ct of
   111         (Const ("Suc", _) $ Var _) => [((cv, ctzero), snd (Thm.dest_comb ct))]
   112       | _ $ _ =>
   113         let val (ct1, ct2) = Thm.dest_comb ct
   114         in 
   115           map (apfst (pairself (fn ct => Thm.capply ct ct2))) (find_vars ct1) @
   116           map (apfst (pairself (Thm.capply ct1))) (find_vars ct2)
   117         end
   118       | _ => []);
   119     val eqs1 = List.concat (map
   120       (fn th => map (pair th) (find_vars (lhs_of th))) thms);
   121     val eqs2 = map (fn x as (_, ((_, ctzero), _)) => (x, List.mapPartial (fn th =>
   122       SOME (th, Thm.cterm_match (lhs_of th, ctzero))
   123         handle Pattern.MATCH => NONE) thms)) eqs1;
   124     fun distinct_vars vs = forall is_Var vs andalso null (duplicates vs);
   125     val eqs2' = map (apsnd (List.filter (fn (_, (_, s)) =>
   126       distinct_vars (map (term_of o snd) s)))) eqs2;
   127     fun mk_thms b ((th, ((ct, _), cv')), (th', s) :: _) =
   128       let
   129         val th'' = Thm.instantiate s th';
   130         val th''' =
   131           Thm.implies_elim (Thm.implies_elim
   132            (Drule.fconv_rule (Thm.beta_conversion true)
   133              (Drule.instantiate'
   134                [SOME (ctyp_of_term ct)] [SOME (Thm.cabs cv ct),
   135                  SOME (rhs_of th''), SOME (Thm.cabs cv' (rhs_of th)), SOME cv']
   136                Suc_if_eq')) th'') (Thm.forall_intr cv' th)
   137       in
   138         List.mapPartial (fn thm =>
   139           if thm = th then SOME th'''
   140           else if b andalso thm = th' then NONE
   141           else SOME thm) thms
   142       end
   143   in
   144     case Library.find_first (not o null o snd) eqs2' of
   145       NONE => (case Library.find_first (not o null o snd) eqs2 of
   146         NONE => thms
   147       | SOME x => remove_suc thy (mk_thms false x))
   148     | SOME x => remove_suc thy (mk_thms true x)
   149   end;
   150 
   151 fun eqn_suc_preproc thy ths =
   152   let val dest = fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of
   153   in
   154     if forall (can dest) ths andalso
   155       exists (fn th => "Suc" mem term_consts (dest th)) ths
   156     then remove_suc thy ths else ths
   157   end;
   158 
   159 val Suc_clause = thm "Suc_clause";
   160 
   161 fun remove_suc_clause thy thms =
   162   let
   163     val Suc_clause' = Thm.transfer thy Suc_clause;
   164     val vname = variant (map fst
   165       (Library.foldl add_term_varnames ([], map prop_of thms))) "x";
   166     fun find_var (t as Const ("Suc", _) $ (v as Var _)) = SOME (t, v)
   167       | find_var (t $ u) = (case find_var t of NONE => find_var u | x => x)
   168       | find_var _ = NONE;
   169     fun find_thm th =
   170       let val th' = ObjectLogic.atomize_thm th
   171       in Option.map (pair (th, th')) (find_var (prop_of th')) end
   172   in
   173     case get_first find_thm thms of
   174       NONE => thms
   175     | SOME ((th, th'), (Sucv, v)) =>
   176         let
   177           val cert = cterm_of (sign_of_thm th);
   178           val th'' = ObjectLogic.rulify (Thm.implies_elim
   179             (Drule.fconv_rule (Thm.beta_conversion true)
   180               (Drule.instantiate' []
   181                 [SOME (cert (lambda v (Abs ("x", HOLogic.natT,
   182                    abstract_over (Sucv,
   183                      HOLogic.dest_Trueprop (prop_of th')))))),
   184                  SOME (cert v)] Suc_clause'))
   185             (Thm.forall_intr (cert v) th'))
   186         in
   187           remove_suc_clause thy (map (fn th''' =>
   188             if th''' = th then th'' else th''') thms)
   189         end
   190   end;
   191 
   192 fun clause_suc_preproc thy ths =
   193   let val dest = fst o HOLogic.dest_mem o HOLogic.dest_Trueprop
   194   in
   195     if forall (can (dest o concl_of)) ths andalso
   196       exists (fn th => "Suc" mem foldr add_term_consts
   197         [] (List.mapPartial (try dest) (concl_of th :: prems_of th))) ths
   198     then remove_suc_clause thy ths else ths
   199   end;
   200 
   201 val suc_preproc_setup =
   202   [Codegen.add_preprocessor eqn_suc_preproc,
   203    Codegen.add_preprocessor clause_suc_preproc];
   204 *}
   205 
   206 setup suc_preproc_setup
   207 (*>*)
   208 
   209 end