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