Code generator plug-in for implementing natural numbers by integers.
authorberghofe
Wed Nov 24 10:29:44 2004 +0100 (2004-11-24)
changeset 153236c10fe1c0e17
parent 15322 c93e6fd5db59
child 15324 c27165172e30
Code generator plug-in for implementing natural numbers by integers.
src/HOL/Library/EfficientNat.thy
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Library/EfficientNat.thy	Wed Nov 24 10:29:44 2004 +0100
     1.3 @@ -0,0 +1,205 @@
     1.4 +(*  Title:      HOL/Library/EfficientNat.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     Stefan Berghofer, TU Muenchen
     1.7 +*)
     1.8 +
     1.9 +header {* Implementation of natural numbers by integers *}
    1.10 +
    1.11 +theory EfficientNat
    1.12 +imports Main
    1.13 +begin
    1.14 +
    1.15 +text {*
    1.16 +When generating code for functions on natural numbers, the canonical
    1.17 +representation using @{term "0::nat"} and @{term "Suc"} is unsuitable for
    1.18 +computations involving large numbers. The efficiency of the generated
    1.19 +code can be improved drastically by implementing natural numbers by
    1.20 +integers. To do this, just include this theory.
    1.21 +*}
    1.22 +
    1.23 +subsection {* Basic functions *}
    1.24 +
    1.25 +text {*
    1.26 +The implementation of @{term "0::nat"} and @{term "Suc"} using the
    1.27 +ML integers is straightforward. Since natural numbers are implemented
    1.28 +using integers, the coercion function @{term "int"} of type
    1.29 +@{typ "nat \<Rightarrow> int"} is simply implemented by the identity function.
    1.30 +For the @{term "nat"} function for converting an integer to a natural
    1.31 +number, we give a specific implementation using an ML function that
    1.32 +returns its input value, provided that it is non-negative, and otherwise
    1.33 +returns @{text "0"}.
    1.34 +*}
    1.35 +
    1.36 +types_code nat ("int")
    1.37 +consts_code
    1.38 +  0 :: nat ("0")
    1.39 +  Suc ("(_ + 1)")
    1.40 +  nat ("nat")
    1.41 +  int ("(_)")
    1.42 +
    1.43 +ML {*
    1.44 +fun nat i = if i < 0 then 0 else i;
    1.45 +*}
    1.46 +
    1.47 +text {*
    1.48 +Case analysis on natural numbers is rephrased using a conditional
    1.49 +expression:
    1.50 +*}
    1.51 +
    1.52 +lemma [code unfold]: "nat_case \<equiv> (\<lambda>f g n. if n = 0 then f else g (n - 1))"
    1.53 +  apply (rule eq_reflection ext)+
    1.54 +  apply (case_tac n)
    1.55 +  apply simp_all
    1.56 +  done
    1.57 +
    1.58 +text {*
    1.59 +Most standard arithmetic functions on natural numbers are implemented
    1.60 +using their counterparts on the integers:
    1.61 +*}
    1.62 +
    1.63 +lemma [code]: "m - n = nat (int m - int n)" by arith
    1.64 +lemma [code]: "m + n = nat (int m + int n)" by arith
    1.65 +lemma [code]: "m * n = nat (int m * int n)"
    1.66 +  by (simp add: zmult_int)
    1.67 +lemma [code]: "m div n = nat (int m div int n)"
    1.68 +  by (simp add: zdiv_int [symmetric])
    1.69 +lemma [code]: "m mod n = nat (int m mod int n)"
    1.70 +  by (simp add: zmod_int [symmetric])
    1.71 +
    1.72 +subsection {* Preprocessors *}
    1.73 +
    1.74 +text {*
    1.75 +In contrast to @{term "Suc n"}, the term @{term "n + (1::nat)"} is no longer
    1.76 +a constructor term. Therefore, all occurrences of this term in a position
    1.77 +where a pattern is expected (i.e.\ on the left-hand side of a recursion
    1.78 +equation or in the arguments of an inductive relation in an introduction
    1.79 +rule) must be eliminated.
    1.80 +This can be accomplished by applying the following transformation rules:
    1.81 +*}
    1.82 +
    1.83 +theorem Suc_if_eq: "f 0 = g \<Longrightarrow> (\<And>n. f (Suc n) = h n) \<Longrightarrow>
    1.84 +  f n = (if n = 0 then g else h (n - 1))"
    1.85 +  by (case_tac n) simp_all
    1.86 +
    1.87 +theorem Suc_clause: "(\<And>n. P n (Suc n)) \<Longrightarrow> n \<noteq> 0 \<Longrightarrow> P (n - 1) n"
    1.88 +  by (case_tac n) simp_all
    1.89 +
    1.90 +text {*
    1.91 +The rules above are built into a preprocessor that is plugged into
    1.92 +the code generator. Since the preprocessor for introduction rules
    1.93 +does not know anything about modes, some of the modes that worked
    1.94 +for the canonical representation of natural numbers may no longer work.
    1.95 +*}
    1.96 +
    1.97 +(*<*)
    1.98 +ML {*
    1.99 +val Suc_if_eq = thm "Suc_if_eq";
   1.100 +
   1.101 +fun remove_suc thms =
   1.102 +  let
   1.103 +    val ctzero = cterm_of (sign_of Main.thy) HOLogic.zero;
   1.104 +    val vname = variant (map fst
   1.105 +      (foldl add_term_varnames ([], map prop_of thms))) "x";
   1.106 +    val cv = cterm_of (sign_of Main.thy) (Var ((vname, 0), HOLogic.natT));
   1.107 +    fun lhs_of th = snd (Thm.dest_comb
   1.108 +      (fst (Thm.dest_comb (snd (Thm.dest_comb (cprop_of th))))));
   1.109 +    fun rhs_of th = snd (Thm.dest_comb (snd (Thm.dest_comb (cprop_of th))));
   1.110 +    fun find_vars ct = (case term_of ct of
   1.111 +        (Const ("Suc", _) $ Var _) => [((cv, ctzero), snd (Thm.dest_comb ct))]
   1.112 +      | _ $ _ =>
   1.113 +        let val (ct1, ct2) = Thm.dest_comb ct
   1.114 +        in 
   1.115 +          map (apfst (pairself (fn ct => Thm.capply ct ct2))) (find_vars ct1) @
   1.116 +          map (apfst (pairself (Thm.capply ct1))) (find_vars ct2)
   1.117 +        end
   1.118 +      | _ => []);
   1.119 +    val eqs1 = flat (map
   1.120 +      (fn th => map (pair th) (find_vars (lhs_of th))) thms);
   1.121 +    val eqs2 = map (fn x as (_, ((_, ctzero), _)) => (x, mapfilter (fn th =>
   1.122 +      Some (th, Thm.cterm_match (lhs_of th, ctzero))
   1.123 +        handle Pattern.MATCH => None) thms)) eqs1;
   1.124 +    fun distinct_vars vs = forall is_Var vs andalso null (duplicates vs);
   1.125 +    val eqs2' = map (apsnd (filter (fn (_, (_, s)) =>
   1.126 +      distinct_vars (map (term_of o snd) s)))) eqs2;
   1.127 +    fun mk_thms b ((th, ((ct, _), cv')), (th', s) :: _) =
   1.128 +      let
   1.129 +        val th'' = Thm.instantiate s th';
   1.130 +        val th''' =
   1.131 +          Thm.implies_elim (Thm.implies_elim
   1.132 +           (Drule.fconv_rule Drule.beta_eta_conversion
   1.133 +             (Drule.instantiate'
   1.134 +               [Some (ctyp_of_term ct)] [Some (Thm.cabs cv ct),
   1.135 +                 Some (rhs_of th''), Some (Thm.cabs cv' (rhs_of th)), Some cv']
   1.136 +               Suc_if_eq)) th'') (Thm.forall_intr cv' th)
   1.137 +      in
   1.138 +        mapfilter (fn thm =>
   1.139 +          if thm = th then Some th'''
   1.140 +          else if b andalso thm = th' then None
   1.141 +          else Some thm) thms
   1.142 +      end
   1.143 +  in
   1.144 +    case Library.find_first (not o null o snd) eqs2' of
   1.145 +      None => (case Library.find_first (not o null o snd) eqs2 of
   1.146 +        None => thms
   1.147 +      | Some x => remove_suc (mk_thms false x))
   1.148 +    | Some x => remove_suc (mk_thms true x)
   1.149 +  end;
   1.150 +
   1.151 +fun eqn_suc_preproc thy ths =
   1.152 +  let val dest = fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of
   1.153 +  in
   1.154 +    if forall (can dest) ths andalso
   1.155 +      exists (fn th => "Suc" mem term_consts (dest th)) ths
   1.156 +    then remove_suc ths else ths
   1.157 +  end;
   1.158 +
   1.159 +val Suc_clause = thm "Suc_clause";
   1.160 +
   1.161 +fun remove_suc_clause thms =
   1.162 +  let
   1.163 +    val vname = variant (map fst
   1.164 +      (foldl add_term_varnames ([], map prop_of thms))) "x";
   1.165 +    fun find_var (t as Const ("Suc", _) $ (v as Var _)) = Some (t, v)
   1.166 +      | find_var (t $ u) = (case find_var t of None => find_var u | x => x)
   1.167 +      | find_var _ = None;
   1.168 +    fun find_thm th =
   1.169 +      let val th' = ObjectLogic.atomize_thm th
   1.170 +      in apsome (pair (th, th')) (find_var (prop_of th')) end
   1.171 +  in
   1.172 +    case get_first find_thm thms of
   1.173 +      None => thms
   1.174 +    | Some ((th, th'), (Sucv, v)) =>
   1.175 +        let
   1.176 +          val cert = cterm_of (sign_of_thm th);
   1.177 +          val th'' = ObjectLogic.rulify (Thm.implies_elim
   1.178 +            (Drule.fconv_rule Drule.beta_eta_conversion
   1.179 +              (Drule.instantiate' []
   1.180 +                [Some (cert (lambda v (Abs ("x", HOLogic.natT,
   1.181 +                   abstract_over (Sucv,
   1.182 +                     HOLogic.dest_Trueprop (prop_of th')))))),
   1.183 +                 Some (cert v)] Suc_clause))
   1.184 +            (Thm.forall_intr (cert v) th'))
   1.185 +        in
   1.186 +          remove_suc_clause (map (fn th''' =>
   1.187 +            if th''' = th then th'' else th''') thms)
   1.188 +        end
   1.189 +  end;
   1.190 +
   1.191 +fun clause_suc_preproc thy ths =
   1.192 +  let val dest = fst o HOLogic.dest_mem o HOLogic.dest_Trueprop
   1.193 +  in
   1.194 +    if forall (can (dest o concl_of)) ths andalso
   1.195 +      exists (fn th => "Suc" mem foldr add_term_consts
   1.196 +        (mapfilter (try dest) (concl_of th :: prems_of th), [])) ths
   1.197 +    then remove_suc_clause ths else ths
   1.198 +  end;
   1.199 +
   1.200 +val suc_preproc_setup =
   1.201 +  [Codegen.add_preprocessor eqn_suc_preproc,
   1.202 +   Codegen.add_preprocessor clause_suc_preproc];
   1.203 +*}
   1.204 +
   1.205 +setup suc_preproc_setup
   1.206 +(*>*)
   1.207 +
   1.208 +end