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