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