author berghofe Wed Nov 24 10:29:44 2004 +0100 (2004-11-24) changeset 15323 6c10fe1c0e17 parent 15322 c93e6fd5db59 child 15324 c27165172e30
Code generator plug-in for implementing natural numbers by integers.
```     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 =