src/HOL/Library/EfficientNat.thy
author chaieb
Mon Jun 11 11:06:04 2007 +0200 (2007-06-11)
changeset 23315 df3a7e9ebadb
parent 23269 851b8ea067ac
child 23365 f31794033ae1
permissions -rw-r--r--
tuned Proof
     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 Pretty_Int
    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 {* Logical rewrites *}
    21 
    22 text {*
    23   An int-to-nat conversion
    24   restricted to non-negative ints (in contrast to @{const nat}).
    25   Note that this restriction has no logical relevance and
    26   is just a kind of proof hint -- nothing prevents you from 
    27   writing nonsense like @{term "nat_of_int (-4)"}
    28 *}
    29 
    30 definition
    31   nat_of_int :: "int \<Rightarrow> nat" where
    32   "k \<ge> 0 \<Longrightarrow> nat_of_int k = nat k"
    33 
    34 lemma nat_of_int_of_number_of:
    35   fixes k
    36   assumes "k \<ge> 0"
    37   shows "number_of k = nat_of_int (number_of k)"
    38   unfolding nat_of_int_def [OF prems] nat_number_of_def number_of_is_id ..
    39 
    40 lemma nat_of_int_of_number_of_aux:
    41   fixes k
    42   assumes "Numeral.Pls \<le> k \<equiv> True"
    43   shows "k \<ge> 0"
    44   using prems unfolding Pls_def by simp
    45 
    46 lemma nat_of_int_int:
    47   "nat_of_int (int n) = n"
    48   using zero_zle_int nat_of_int_def by simp
    49 
    50 text {*
    51   Case analysis on natural numbers is rephrased using a conditional
    52   expression:
    53 *}
    54 
    55 lemma [code unfold, code inline del]:
    56   "nat_case \<equiv> (\<lambda>f g n. if n = 0 then f else g (n - 1))"
    57 proof -
    58   have rewrite: "\<And>f g n. nat_case f g n = (if n = 0 then f else g (n - 1))"
    59   proof -
    60     fix f g n
    61     show "nat_case f g n = (if n = 0 then f else g (n - 1))"
    62       by (cases n) simp_all
    63   qed
    64   show "nat_case \<equiv> (\<lambda>f g n. if n = 0 then f else g (n - 1))"
    65     by (rule eq_reflection ext rewrite)+ 
    66 qed
    67 
    68 lemma [code inline]:
    69   "nat_case = (\<lambda>f g n. if n = 0 then f else g (nat_of_int (int n - 1)))"
    70 proof (rule ext)+
    71   fix f g n
    72   show "nat_case f g n = (if n = 0 then f else g (nat_of_int (int n - 1)))"
    73   by (cases n) (simp_all add: nat_of_int_int)
    74 qed
    75 
    76 text {*
    77   Most standard arithmetic functions on natural numbers are implemented
    78   using their counterparts on the integers:
    79 *}
    80 
    81 lemma [code func]: "0 = nat_of_int 0"
    82   by (simp add: nat_of_int_def)
    83 lemma [code func, code inline]:  "1 = nat_of_int 1"
    84   by (simp add: nat_of_int_def)
    85 lemma [code func]: "Suc n = nat_of_int (int n + 1)"
    86   by (simp add: nat_of_int_def)
    87 lemma [code]: "m + n = nat (int m + int n)"
    88   by arith
    89 lemma [code func, code inline]: "m + n = nat_of_int (int m + int n)"
    90   by (simp add: nat_of_int_def)
    91 lemma [code, code inline]: "m - n = nat (int m - int n)"
    92   by arith
    93 lemma [code]: "m * n = nat (int m * int n)"
    94   unfolding zmult_int by simp
    95 lemma [code func, code inline]: "m * n = nat_of_int (int m * int n)"
    96 proof -
    97   have "int (m * n) = int m * int n"
    98     by (induct m) (simp_all add: zadd_zmult_distrib)
    99   then have "m * n = nat (int m * int n)" by auto
   100   also have "\<dots> = nat_of_int (int m * int n)"
   101   proof -
   102     have "int m \<ge> 0" and "int n \<ge> 0" by auto
   103     have "int m * int n \<ge> 0" by (rule split_mult_pos_le) auto
   104     with nat_of_int_def show ?thesis by auto
   105   qed
   106   finally show ?thesis .
   107 qed  
   108 lemma [code]: "m div n = nat (int m div int n)"
   109   unfolding zdiv_int [symmetric] by simp
   110 lemma [code func]: "m div n = fst (Divides.divmod m n)"
   111   unfolding divmod_def by simp
   112 lemma [code]: "m mod n = nat (int m mod int n)"
   113   unfolding zmod_int [symmetric] by simp
   114 lemma [code func]: "m mod n = snd (Divides.divmod m n)"
   115   unfolding divmod_def by simp
   116 lemma [code, code inline]: "(m < n) \<longleftrightarrow> (int m < int n)"
   117   by simp
   118 lemma [code func, code inline]: "(m \<le> n) \<longleftrightarrow> (int m \<le> int n)"
   119   by simp
   120 lemma [code func, code inline]: "m = n \<longleftrightarrow> int m = int n"
   121   by simp
   122 lemma [code func]: "nat k = (if k < 0 then 0 else nat_of_int k)"
   123 proof (cases "k < 0")
   124   case True then show ?thesis by simp
   125 next
   126   case False then show ?thesis by (simp add: nat_of_int_def)
   127 qed
   128 lemma [code func]:
   129   "int_aux i n = (if int n = 0 then i else int_aux (i + 1) (nat_of_int (int n - 1)))"
   130 proof -
   131   have "0 < n \<Longrightarrow> int n = 1 + int (nat_of_int (int n - 1))"
   132   proof -
   133     assume prem: "n > 0"
   134     then have "int n - 1 \<ge> 0" by auto
   135     then have "nat_of_int (int n - 1) = nat (int n - 1)" by (simp add: nat_of_int_def)
   136     with prem show "int n = 1 + int (nat_of_int (int n - 1))" by simp
   137   qed
   138   then show ?thesis unfolding int_aux_def by simp
   139 qed
   140 
   141 lemma div_nat_code [code func]:
   142   "m div k = nat_of_int (fst (divAlg (int m, int k)))"
   143   unfolding div_def [symmetric] zdiv_int [symmetric] nat_of_int_int ..
   144 
   145 lemma mod_nat_code [code func]:
   146   "m mod k = nat_of_int (snd (divAlg (int m, int k)))"
   147   unfolding mod_def [symmetric] zmod_int [symmetric] nat_of_int_int ..
   148 
   149 
   150 subsection {* Code generator setup for basic functions *}
   151 
   152 text {*
   153   @{typ nat} is no longer a datatype but embedded into the integers.
   154 *}
   155 
   156 code_datatype nat_of_int
   157 
   158 code_type nat
   159   (SML "IntInf.int")
   160   (OCaml "Big'_int.big'_int")
   161   (Haskell "Integer")
   162 
   163 types_code
   164   nat ("int")
   165 attach (term_of) {*
   166 val term_of_nat = HOLogic.mk_number HOLogic.natT o IntInf.fromInt;
   167 *}
   168 attach (test) {*
   169 fun gen_nat i = random_range 0 i;
   170 *}
   171 
   172 consts_code
   173   "0 \<Colon> nat" ("0")
   174   Suc ("(_ + 1)")
   175 
   176 text {*
   177   Since natural numbers are implemented
   178   using integers, the coercion function @{const "int"} of type
   179   @{typ "nat \<Rightarrow> int"} is simply implemented by the identity function,
   180   likewise @{const nat_of_int} of type @{typ "int \<Rightarrow> nat"}.
   181   For the @{const "nat"} function for converting an integer to a natural
   182   number, we give a specific implementation using an ML function that
   183   returns its input value, provided that it is non-negative, and otherwise
   184   returns @{text "0"}.
   185 *}
   186 
   187 consts_code
   188   int ("(_)")
   189   nat ("\<module>nat")
   190 attach {*
   191 fun nat i = if i < 0 then 0 else i;
   192 *}
   193 
   194 code_const int
   195   (SML "_")
   196   (OCaml "_")
   197   (Haskell "_")
   198 
   199 code_const nat_of_int
   200   (SML "_")
   201   (OCaml "_")
   202   (Haskell "_")
   203 
   204 
   205 subsection {* Preprocessors *}
   206 
   207 text {*
   208   Natural numerals should be expressed using @{const nat_of_int}.
   209 *}
   210 
   211 lemmas [code inline del] = nat_number_of_def
   212 
   213 ML {*
   214 fun nat_of_int_of_number_of thy cts =
   215   let
   216     val simplify_less = Simplifier.rewrite 
   217       (HOL_basic_ss addsimps (@{thms less_numeral_code} @ @{thms less_eq_numeral_code}));
   218     fun mk_rew (t, ty) =
   219       if ty = HOLogic.natT andalso IntInf.<= (0, HOLogic.dest_numeral t) then
   220         Thm.capply @{cterm "(op \<le>) Numeral.Pls"} (Thm.cterm_of thy t)
   221         |> simplify_less
   222         |> (fn thm => @{thm nat_of_int_of_number_of_aux} OF [thm])
   223         |> (fn thm => @{thm nat_of_int_of_number_of} OF [thm])
   224         |> (fn thm => @{thm eq_reflection} OF [thm])
   225         |> SOME
   226       else NONE
   227   in
   228     fold (HOLogic.add_numerals o Thm.term_of) cts []
   229     |> map_filter mk_rew
   230   end;
   231 *}
   232 
   233 setup {*
   234   CodegenData.add_inline_proc ("nat_of_int_of_number_of", nat_of_int_of_number_of)
   235 *}
   236 
   237 text {*
   238   In contrast to @{term "Suc n"}, the term @{term "n + (1::nat)"} is no longer
   239   a constructor term. Therefore, all occurrences of this term in a position
   240   where a pattern is expected (i.e.\ on the left-hand side of a recursion
   241   equation or in the arguments of an inductive relation in an introduction
   242   rule) must be eliminated.
   243   This can be accomplished by applying the following transformation rules:
   244 *}
   245 
   246 theorem Suc_if_eq: "(\<And>n. f (Suc n) = h n) \<Longrightarrow> f 0 = g \<Longrightarrow>
   247   f n = (if n = 0 then g else h (n - 1))"
   248   by (case_tac n) simp_all
   249 
   250 theorem Suc_clause: "(\<And>n. P n (Suc n)) \<Longrightarrow> n \<noteq> 0 \<Longrightarrow> P (n - 1) n"
   251   by (case_tac n) simp_all
   252 
   253 text {*
   254   The rules above are built into a preprocessor that is plugged into
   255   the code generator. Since the preprocessor for introduction rules
   256   does not know anything about modes, some of the modes that worked
   257   for the canonical representation of natural numbers may no longer work.
   258 *}
   259 
   260 (*<*)
   261 
   262 ML {*
   263 local
   264   val Suc_if_eq = thm "Suc_if_eq";
   265   val Suc_clause = thm "Suc_clause";
   266   fun contains_suc t = member (op =) (term_consts t) "Suc";
   267 in
   268 
   269 fun remove_suc thy thms =
   270   let
   271     val Suc_if_eq' = Thm.transfer thy Suc_if_eq;
   272     val vname = Name.variant (map fst
   273       (fold (Term.add_varnames o Thm.full_prop_of) thms [])) "x";
   274     val cv = cterm_of thy (Var ((vname, 0), HOLogic.natT));
   275     fun lhs_of th = snd (Thm.dest_comb
   276       (fst (Thm.dest_comb (snd (Thm.dest_comb (cprop_of th))))));
   277     fun rhs_of th = snd (Thm.dest_comb (snd (Thm.dest_comb (cprop_of th))));
   278     fun find_vars ct = (case term_of ct of
   279         (Const ("Suc", _) $ Var _) => [(cv, snd (Thm.dest_comb ct))]
   280       | _ $ _ =>
   281         let val (ct1, ct2) = Thm.dest_comb ct
   282         in 
   283           map (apfst (fn ct => Thm.capply ct ct2)) (find_vars ct1) @
   284           map (apfst (Thm.capply ct1)) (find_vars ct2)
   285         end
   286       | _ => []);
   287     val eqs = List.concat (map
   288       (fn th => map (pair th) (find_vars (lhs_of th))) thms);
   289     fun mk_thms (th, (ct, cv')) =
   290       let
   291         val th' =
   292           Thm.implies_elim
   293            (Conv.fconv_rule (Thm.beta_conversion true)
   294              (Drule.instantiate'
   295                [SOME (ctyp_of_term ct)] [SOME (Thm.cabs cv ct),
   296                  SOME (Thm.cabs cv' (rhs_of th)), NONE, SOME cv']
   297                Suc_if_eq')) (Thm.forall_intr cv' th)
   298       in
   299         case map_filter (fn th'' =>
   300             SOME (th'', singleton
   301               (Variable.trade (K (fn [th'''] => [th''' RS th'])) (Variable.thm_context th'')) th'')
   302           handle THM _ => NONE) thms of
   303             [] => NONE
   304           | thps =>
   305               let val (ths1, ths2) = split_list thps
   306               in SOME (subtract Thm.eq_thm (th :: ths1) thms @ ths2) end
   307       end
   308   in
   309     case get_first mk_thms eqs of
   310       NONE => thms
   311     | SOME x => remove_suc thy x
   312   end;
   313 
   314 fun eqn_suc_preproc thy ths =
   315   let
   316     val dest = fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of
   317   in
   318     if forall (can dest) ths andalso
   319       exists (contains_suc o dest) ths
   320     then remove_suc thy ths else ths
   321   end;
   322 
   323 fun remove_suc_clause thy thms =
   324   let
   325     val Suc_clause' = Thm.transfer thy Suc_clause;
   326     val vname = Name.variant (map fst
   327       (fold (Term.add_varnames o Thm.full_prop_of) thms [])) "x";
   328     fun find_var (t as Const ("Suc", _) $ (v as Var _)) = SOME (t, v)
   329       | find_var (t $ u) = (case find_var t of NONE => find_var u | x => x)
   330       | find_var _ = NONE;
   331     fun find_thm th =
   332       let val th' = ObjectLogic.atomize_thm th
   333       in Option.map (pair (th, th')) (find_var (prop_of th')) end
   334   in
   335     case get_first find_thm thms of
   336       NONE => thms
   337     | SOME ((th, th'), (Sucv, v)) =>
   338         let
   339           val cert = cterm_of (Thm.theory_of_thm th);
   340           val th'' = ObjectLogic.rulify (Thm.implies_elim
   341             (Conv.fconv_rule (Thm.beta_conversion true)
   342               (Drule.instantiate' []
   343                 [SOME (cert (lambda v (Abs ("x", HOLogic.natT,
   344                    abstract_over (Sucv,
   345                      HOLogic.dest_Trueprop (prop_of th')))))),
   346                  SOME (cert v)] Suc_clause'))
   347             (Thm.forall_intr (cert v) th'))
   348         in
   349           remove_suc_clause thy (map (fn th''' =>
   350             if (op = o pairself prop_of) (th''', th) then th'' else th''') thms)
   351         end
   352   end;
   353 
   354 fun clause_suc_preproc thy ths =
   355   let
   356     val dest = fst o HOLogic.dest_mem o HOLogic.dest_Trueprop
   357   in
   358     if forall (can (dest o concl_of)) ths andalso
   359       exists (fn th => member (op =) (foldr add_term_consts
   360         [] (map_filter (try dest) (concl_of th :: prems_of th))) "Suc") ths
   361     then remove_suc_clause thy ths else ths
   362   end;
   363 
   364 end; (*local*)
   365 
   366 fun lift_obj_eq f thy =
   367   map (fn thm => thm RS @{thm meta_eq_to_obj_eq})
   368   #> f thy
   369   #> map (fn thm => thm RS @{thm eq_reflection})
   370   #> map (Conv.fconv_rule Drule.beta_eta_conversion)
   371 *}
   372 
   373 setup {*
   374   Codegen.add_preprocessor eqn_suc_preproc
   375   #> Codegen.add_preprocessor clause_suc_preproc
   376   #> CodegenData.add_preproc ("eqn_Suc", lift_obj_eq eqn_suc_preproc)
   377   #> CodegenData.add_preproc ("clause_Suc", lift_obj_eq clause_suc_preproc)
   378 *}
   379 (*>*)
   380 
   381 subsection {* Module names *}
   382 
   383 code_modulename SML
   384   Nat Integer
   385   EfficientNat Integer
   386 
   387 code_modulename OCaml
   388   Nat Integer
   389   EfficientNat Integer
   390 
   391 code_modulename Haskell
   392   Nat Integer
   393   EfficientNat Integer
   394 
   395 hide const nat_of_int
   396 
   397 end