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
```