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