haftmann@23854: (* Title: HOL/Library/Efficient_Nat.thy haftmann@25931: Author: Stefan Berghofer, Florian Haftmann, TU Muenchen haftmann@23854: *) haftmann@23854: haftmann@25931: header {* Implementation of natural numbers by target-language integers *} haftmann@23854: haftmann@23854: theory Efficient_Nat haftmann@31203: imports Code_Integer Main haftmann@23854: begin haftmann@23854: haftmann@23854: text {* haftmann@25931: When generating code for functions on natural numbers, the haftmann@25931: canonical representation using @{term "0::nat"} and haftmann@37388: @{term Suc} is unsuitable for computations involving large haftmann@25931: numbers. The efficiency of the generated code can be improved haftmann@25931: drastically by implementing natural numbers by target-language haftmann@25931: integers. To do this, just include this theory. haftmann@23854: *} haftmann@23854: haftmann@25931: subsection {* Basic arithmetic *} haftmann@23854: haftmann@23854: text {* haftmann@23854: Most standard arithmetic functions on natural numbers are implemented haftmann@23854: using their counterparts on the integers: haftmann@23854: *} haftmann@23854: haftmann@25931: code_datatype number_nat_inst.number_of_nat haftmann@24715: haftmann@32069: lemma zero_nat_code [code, code_unfold_post]: haftmann@25931: "0 = (Numeral0 :: nat)" haftmann@25931: by simp haftmann@24715: haftmann@32069: lemma one_nat_code [code, code_unfold_post]: haftmann@25931: "1 = (Numeral1 :: nat)" haftmann@25931: by simp haftmann@24715: haftmann@25931: lemma Suc_code [code]: haftmann@25931: "Suc n = n + 1" haftmann@25931: by simp haftmann@24715: haftmann@25931: lemma plus_nat_code [code]: haftmann@25931: "n + m = nat (of_nat n + of_nat m)" haftmann@25931: by simp haftmann@24715: haftmann@25931: lemma minus_nat_code [code]: haftmann@25931: "n - m = nat (of_nat n - of_nat m)" haftmann@25931: by simp haftmann@24715: haftmann@25931: lemma times_nat_code [code]: haftmann@25931: "n * m = nat (of_nat n * of_nat m)" haftmann@25931: unfolding of_nat_mult [symmetric] by simp haftmann@24715: haftmann@26009: text {* Specialized @{term "op div \ nat \ nat \ nat"} haftmann@26009: and @{term "op mod \ nat \ nat \ nat"} operations. *} haftmann@26009: haftmann@28694: definition divmod_aux :: "nat \ nat \ nat \ nat" where haftmann@33343: [code del]: "divmod_aux = divmod_nat" haftmann@24715: haftmann@28522: lemma [code]: haftmann@33343: "divmod_nat n m = (if m = 0 then (0, n) else divmod_aux n m)" haftmann@33343: unfolding divmod_aux_def divmod_nat_div_mod by simp haftmann@26009: haftmann@26100: lemma divmod_aux_code [code]: haftmann@26100: "divmod_aux n m = (nat (of_nat n div of_nat m), nat (of_nat n mod of_nat m))" haftmann@33343: unfolding divmod_aux_def divmod_nat_div_mod zdiv_int [symmetric] zmod_int [symmetric] by simp haftmann@24715: haftmann@25931: lemma eq_nat_code [code]: haftmann@28351: "eq_class.eq n m \ eq_class.eq (of_nat n \ int) (of_nat m)" haftmann@28351: by (simp add: eq) haftmann@28351: haftmann@28351: lemma eq_nat_refl [code nbe]: haftmann@28351: "eq_class.eq (n::nat) n \ True" haftmann@28351: by (rule HOL.eq_refl) haftmann@24715: haftmann@25931: lemma less_eq_nat_code [code]: haftmann@25931: "n \ m \ (of_nat n \ int) \ of_nat m" haftmann@25931: by simp haftmann@23854: haftmann@25931: lemma less_nat_code [code]: haftmann@25931: "n < m \ (of_nat n \ int) < of_nat m" haftmann@25931: by simp haftmann@23854: haftmann@25931: subsection {* Case analysis *} haftmann@23854: haftmann@23854: text {* haftmann@25931: Case analysis on natural numbers is rephrased using a conditional haftmann@25931: expression: haftmann@23854: *} haftmann@23854: haftmann@31998: lemma [code, code_unfold]: haftmann@25931: "nat_case = (\f g n. if n = 0 then f else g (n - 1))" haftmann@25931: by (auto simp add: expand_fun_eq dest!: gr0_implies_Suc) haftmann@25615: haftmann@23854: haftmann@23854: subsection {* Preprocessors *} haftmann@23854: haftmann@23854: text {* haftmann@23854: In contrast to @{term "Suc n"}, the term @{term "n + (1::nat)"} is no longer haftmann@23854: a constructor term. Therefore, all occurrences of this term in a position haftmann@23854: where a pattern is expected (i.e.\ on the left-hand side of a recursion haftmann@23854: equation or in the arguments of an inductive relation in an introduction haftmann@23854: rule) must be eliminated. haftmann@23854: This can be accomplished by applying the following transformation rules: haftmann@23854: *} haftmann@23854: haftmann@29937: lemma Suc_if_eq: "(\n. f (Suc n) \ h n) \ f 0 \ g \ haftmann@29937: f n \ if n = 0 then g else h (n - 1)" haftmann@31954: by (rule eq_reflection) (cases n, simp_all) haftmann@29937: haftmann@25931: lemma Suc_clause: "(\n. P n (Suc n)) \ n \ 0 \ P (n - 1) n" haftmann@29932: by (cases n) simp_all haftmann@23854: haftmann@23854: text {* haftmann@23854: The rules above are built into a preprocessor that is plugged into haftmann@23854: the code generator. Since the preprocessor for introduction rules haftmann@23854: does not know anything about modes, some of the modes that worked haftmann@23854: for the canonical representation of natural numbers may no longer work. haftmann@23854: *} haftmann@23854: haftmann@23854: (*<*) haftmann@27609: setup {* haftmann@27609: let haftmann@23854: haftmann@31954: fun remove_suc thy thms = haftmann@23854: let haftmann@23854: val vname = Name.variant (map fst haftmann@29937: (fold (Term.add_var_names o Thm.full_prop_of) thms [])) "n"; haftmann@23854: val cv = cterm_of thy (Var ((vname, 0), HOLogic.natT)); haftmann@23854: fun lhs_of th = snd (Thm.dest_comb haftmann@31954: (fst (Thm.dest_comb (cprop_of th)))); haftmann@31954: fun rhs_of th = snd (Thm.dest_comb (cprop_of th)); haftmann@23854: fun find_vars ct = (case term_of ct of haftmann@29932: (Const (@{const_name Suc}, _) $ Var _) => [(cv, snd (Thm.dest_comb ct))] haftmann@23854: | _ $ _ => haftmann@23854: let val (ct1, ct2) = Thm.dest_comb ct haftmann@23854: in haftmann@23854: map (apfst (fn ct => Thm.capply ct ct2)) (find_vars ct1) @ haftmann@23854: map (apfst (Thm.capply ct1)) (find_vars ct2) haftmann@23854: end haftmann@23854: | _ => []); haftmann@23854: val eqs = maps haftmann@23854: (fn th => map (pair th) (find_vars (lhs_of th))) thms; haftmann@23854: fun mk_thms (th, (ct, cv')) = haftmann@23854: let haftmann@23854: val th' = haftmann@23854: Thm.implies_elim haftmann@23854: (Conv.fconv_rule (Thm.beta_conversion true) haftmann@23854: (Drule.instantiate' haftmann@23854: [SOME (ctyp_of_term ct)] [SOME (Thm.cabs cv ct), haftmann@23854: SOME (Thm.cabs cv' (rhs_of th)), NONE, SOME cv'] haftmann@31954: @{thm Suc_if_eq})) (Thm.forall_intr cv' th) haftmann@23854: in haftmann@23854: case map_filter (fn th'' => haftmann@23854: SOME (th'', singleton wenzelm@36603: (Variable.trade (K (fn [th'''] => [th''' RS th'])) wenzelm@36603: (Variable.global_thm_context th'')) th'') haftmann@23854: handle THM _ => NONE) thms of haftmann@23854: [] => NONE haftmann@23854: | thps => haftmann@23854: let val (ths1, ths2) = split_list thps haftmann@23854: in SOME (subtract Thm.eq_thm (th :: ths1) thms @ ths2) end haftmann@23854: end haftmann@29937: in get_first mk_thms eqs end; haftmann@29937: haftmann@34893: fun eqn_suc_base_preproc thy thms = haftmann@29937: let haftmann@31954: val dest = fst o Logic.dest_equals o prop_of; haftmann@29937: val contains_suc = exists_Const (fn (c, _) => c = @{const_name Suc}); haftmann@29937: in haftmann@29937: if forall (can dest) thms andalso exists (contains_suc o dest) thms haftmann@32348: then thms |> perhaps_loop (remove_suc thy) |> (Option.map o map) Drule.zero_var_indexes haftmann@29937: else NONE haftmann@23854: end; haftmann@23854: haftmann@34893: val eqn_suc_preproc = Code_Preproc.simple_functrans eqn_suc_base_preproc; haftmann@23854: haftmann@23854: fun remove_suc_clause thy thms = haftmann@23854: let haftmann@23854: val vname = Name.variant (map fst wenzelm@29258: (fold (Term.add_var_names o Thm.full_prop_of) thms [])) "x"; haftmann@24222: fun find_var (t as Const (@{const_name Suc}, _) $ (v as Var _)) = SOME (t, v) haftmann@23854: | find_var (t $ u) = (case find_var t of NONE => find_var u | x => x) haftmann@23854: | find_var _ = NONE; haftmann@23854: fun find_thm th = wenzelm@35625: let val th' = Conv.fconv_rule Object_Logic.atomize th haftmann@23854: in Option.map (pair (th, th')) (find_var (prop_of th')) end haftmann@23854: in haftmann@23854: case get_first find_thm thms of haftmann@23854: NONE => thms haftmann@23854: | SOME ((th, th'), (Sucv, v)) => haftmann@23854: let haftmann@23854: val cert = cterm_of (Thm.theory_of_thm th); wenzelm@35625: val th'' = Object_Logic.rulify (Thm.implies_elim haftmann@23854: (Conv.fconv_rule (Thm.beta_conversion true) haftmann@23854: (Drule.instantiate' [] haftmann@23854: [SOME (cert (lambda v (Abs ("x", HOLogic.natT, haftmann@23854: abstract_over (Sucv, haftmann@23854: HOLogic.dest_Trueprop (prop_of th')))))), haftmann@24222: SOME (cert v)] @{thm Suc_clause})) haftmann@23854: (Thm.forall_intr (cert v) th')) haftmann@23854: in haftmann@23854: remove_suc_clause thy (map (fn th''' => haftmann@23854: if (op = o pairself prop_of) (th''', th) then th'' else th''') thms) haftmann@23854: end haftmann@23854: end; haftmann@23854: haftmann@23854: fun clause_suc_preproc thy ths = haftmann@23854: let haftmann@23854: val dest = fst o HOLogic.dest_mem o HOLogic.dest_Trueprop haftmann@23854: in haftmann@23854: if forall (can (dest o concl_of)) ths andalso wenzelm@29287: exists (fn th => exists (exists_Const (fn (c, _) => c = @{const_name Suc})) wenzelm@29287: (map_filter (try dest) (concl_of th :: prems_of th))) ths haftmann@23854: then remove_suc_clause thy ths else ths haftmann@23854: end; haftmann@27609: in haftmann@27609: haftmann@34893: Code_Preproc.add_functrans ("eqn_Suc", eqn_suc_preproc) haftmann@23854: #> Codegen.add_preprocessor clause_suc_preproc haftmann@27609: haftmann@27609: end; haftmann@23854: *} haftmann@23854: (*>*) haftmann@23854: haftmann@27609: haftmann@25931: subsection {* Target language setup *} haftmann@25931: haftmann@25931: text {* haftmann@25967: For ML, we map @{typ nat} to target language integers, where we haftmann@34899: ensure that values are always non-negative. haftmann@25931: *} haftmann@25931: haftmann@25931: code_type nat haftmann@27496: (SML "IntInf.int") haftmann@25931: (OCaml "Big'_int.big'_int") haftmann@25931: haftmann@25931: types_code haftmann@25931: nat ("int") haftmann@25931: attach (term_of) {* haftmann@25931: val term_of_nat = HOLogic.mk_number HOLogic.natT; haftmann@25931: *} haftmann@25931: attach (test) {* haftmann@25931: fun gen_nat i = haftmann@25931: let val n = random_range 0 i haftmann@25931: in (n, fn () => term_of_nat n) end; haftmann@25931: *} haftmann@25931: haftmann@25931: text {* haftmann@34899: For Haskell ans Scala we define our own @{typ nat} type. The reason haftmann@34899: is that we have to distinguish type class instances for @{typ nat} haftmann@34899: and @{typ int}. haftmann@25967: *} haftmann@25967: haftmann@25967: code_include Haskell "Nat" {* haftmann@37050: newtype Nat = Nat Integer deriving (Eq, Show, Read); haftmann@25967: haftmann@25967: instance Num Nat where { haftmann@25967: fromInteger k = Nat (if k >= 0 then k else 0); haftmann@25967: Nat n + Nat m = Nat (n + m); haftmann@25967: Nat n - Nat m = fromInteger (n - m); haftmann@25967: Nat n * Nat m = Nat (n * m); haftmann@25967: abs n = n; haftmann@25967: signum _ = 1; haftmann@25967: negate n = error "negate Nat"; haftmann@25967: }; haftmann@25967: haftmann@25967: instance Ord Nat where { haftmann@25967: Nat n <= Nat m = n <= m; haftmann@25967: Nat n < Nat m = n < m; haftmann@25967: }; haftmann@25967: haftmann@25967: instance Real Nat where { haftmann@25967: toRational (Nat n) = toRational n; haftmann@25967: }; haftmann@25967: haftmann@25967: instance Enum Nat where { haftmann@25967: toEnum k = fromInteger (toEnum k); haftmann@25967: fromEnum (Nat n) = fromEnum n; haftmann@25967: }; haftmann@25967: haftmann@25967: instance Integral Nat where { haftmann@25967: toInteger (Nat n) = n; haftmann@25967: divMod n m = quotRem n m; haftmann@25967: quotRem (Nat n) (Nat m) = (Nat k, Nat l) where (k, l) = quotRem n m; haftmann@25967: }; haftmann@25967: *} haftmann@25967: haftmann@25967: code_reserved Haskell Nat haftmann@25967: haftmann@34899: code_include Scala "Nat" {* haftmann@34944: import scala.Math haftmann@34944: haftmann@34899: object Nat { haftmann@34899: haftmann@34899: def apply(numeral: BigInt): Nat = new Nat(numeral max 0) haftmann@34899: def apply(numeral: Int): Nat = Nat(BigInt(numeral)) haftmann@34899: def apply(numeral: String): Nat = Nat(BigInt(numeral)) haftmann@34899: haftmann@34899: } haftmann@34899: haftmann@34899: class Nat private(private val value: BigInt) { haftmann@34899: haftmann@34899: override def hashCode(): Int = this.value.hashCode() haftmann@34899: haftmann@34899: override def equals(that: Any): Boolean = that match { haftmann@34899: case that: Nat => this equals that haftmann@34899: case _ => false haftmann@34899: } haftmann@34899: haftmann@34899: override def toString(): String = this.value.toString haftmann@34899: haftmann@34899: def equals(that: Nat): Boolean = this.value == that.value haftmann@34899: haftmann@34899: def as_BigInt: BigInt = this.value haftmann@37892: def as_Int: Int = if (this.value >= Int.MinValue && this.value <= Int.MaxValue) haftmann@34944: this.value.intValue haftmann@37846: else this.value.intValue haftmann@34899: haftmann@34899: def +(that: Nat): Nat = new Nat(this.value + that.value) haftmann@37223: def -(that: Nat): Nat = Nat(this.value - that.value) haftmann@34899: def *(that: Nat): Nat = new Nat(this.value * that.value) haftmann@34899: haftmann@34899: def /%(that: Nat): (Nat, Nat) = if (that.value == 0) (new Nat(0), this) haftmann@34899: else { haftmann@34899: val (k, l) = this.value /% that.value haftmann@34899: (new Nat(k), new Nat(l)) haftmann@34899: } haftmann@34899: haftmann@34899: def <=(that: Nat): Boolean = this.value <= that.value haftmann@34899: haftmann@34899: def <(that: Nat): Boolean = this.value < that.value haftmann@34899: haftmann@34899: } haftmann@34899: *} haftmann@34899: haftmann@34899: code_reserved Scala Nat haftmann@34899: haftmann@25967: code_type nat haftmann@29793: (Haskell "Nat.Nat") haftmann@37878: (Scala "Nat") haftmann@25967: haftmann@25967: code_instance nat :: eq haftmann@25967: (Haskell -) haftmann@25967: haftmann@25967: text {* haftmann@25931: Natural numerals. haftmann@25931: *} haftmann@25931: haftmann@32069: lemma [code_unfold_post]: haftmann@25931: "nat (number_of i) = number_nat_inst.number_of_nat i" haftmann@25931: -- {* this interacts as desired with @{thm nat_number_of_def} *} haftmann@25931: by (simp add: number_nat_inst.number_of_nat) haftmann@25931: haftmann@25931: setup {* haftmann@25931: fold (Numeral.add_code @{const_name number_nat_inst.number_of_nat} haftmann@34944: false Code_Printer.literal_positive_numeral) ["SML", "OCaml", "Haskell"] haftmann@34899: #> Numeral.add_code @{const_name number_nat_inst.number_of_nat} haftmann@34944: false Code_Printer.literal_positive_numeral "Scala" haftmann@25931: *} haftmann@25931: haftmann@25931: text {* haftmann@25931: Since natural numbers are implemented haftmann@25967: using integers in ML, the coercion function @{const "of_nat"} of type haftmann@25931: @{typ "nat \ int"} is simply implemented by the identity function. haftmann@37388: For the @{const nat} function for converting an integer to a natural haftmann@25931: number, we give a specific implementation using an ML function that haftmann@25931: returns its input value, provided that it is non-negative, and otherwise haftmann@25931: returns @{text "0"}. haftmann@25931: *} haftmann@25931: haftmann@32073: definition int :: "nat \ int" where haftmann@28562: [code del]: "int = of_nat" haftmann@25931: haftmann@28562: lemma int_code' [code]: haftmann@25931: "int (number_of l) = (if neg (number_of l \ int) then 0 else number_of l)" haftmann@25931: unfolding int_nat_number_of [folded int_def] .. haftmann@25931: haftmann@28562: lemma nat_code' [code]: haftmann@25931: "nat (number_of l) = (if neg (number_of l \ int) then 0 else number_of l)" huffman@28969: unfolding nat_number_of_def number_of_is_id neg_def by simp haftmann@25931: haftmann@32069: lemma of_nat_int [code_unfold_post]: haftmann@25931: "of_nat = int" by (simp add: int_def) haftmann@25931: haftmann@32073: lemma of_nat_aux_int [code_unfold]: haftmann@32073: "of_nat_aux (\i. i + 1) k 0 = int k" haftmann@32073: by (simp add: int_def Nat.of_nat_code) haftmann@32073: haftmann@25931: code_const int haftmann@25931: (SML "_") haftmann@25931: (OCaml "_") haftmann@25931: haftmann@25931: consts_code haftmann@25931: int ("(_)") haftmann@25931: nat ("\nat") haftmann@25931: attach {* haftmann@25931: fun nat i = if i < 0 then 0 else i; haftmann@25931: *} haftmann@25931: haftmann@25967: code_const nat haftmann@25967: (SML "IntInf.max/ (/0,/ _)") haftmann@25967: (OCaml "Big'_int.max'_big'_int/ Big'_int.zero'_big'_int") haftmann@25967: haftmann@35689: text {* For Haskell and Scala, things are slightly different again. *} haftmann@25967: haftmann@25967: code_const int and nat haftmann@25967: (Haskell "toInteger" and "fromInteger") haftmann@37878: (Scala "!_.as'_BigInt" and "Nat") haftmann@25931: haftmann@25931: text {* Conversion from and to indices. *} haftmann@25931: haftmann@31205: code_const Code_Numeral.of_nat haftmann@25967: (SML "IntInf.toInt") haftmann@31377: (OCaml "_") haftmann@27673: (Haskell "fromEnum") haftmann@34902: (Scala "!_.as'_Int") haftmann@25967: haftmann@31205: code_const Code_Numeral.nat_of haftmann@25931: (SML "IntInf.fromInt") haftmann@31377: (OCaml "_") haftmann@27673: (Haskell "toEnum") haftmann@37878: (Scala "Nat") haftmann@25931: haftmann@25931: text {* Using target language arithmetic operations whenever appropriate *} haftmann@25931: haftmann@25931: code_const "op + \ nat \ nat \ nat" haftmann@25931: (SML "IntInf.+ ((_), (_))") haftmann@25931: (OCaml "Big'_int.add'_big'_int") haftmann@25931: (Haskell infixl 6 "+") haftmann@34899: (Scala infixl 7 "+") haftmann@34899: haftmann@34899: code_const "op - \ nat \ nat \ nat" haftmann@34899: (Haskell infixl 6 "-") haftmann@34899: (Scala infixl 7 "-") haftmann@25931: haftmann@25931: code_const "op * \ nat \ nat \ nat" haftmann@25931: (SML "IntInf.* ((_), (_))") haftmann@25931: (OCaml "Big'_int.mult'_big'_int") haftmann@25931: (Haskell infixl 7 "*") haftmann@34899: (Scala infixl 8 "*") haftmann@25931: haftmann@26100: code_const divmod_aux haftmann@26009: (SML "IntInf.divMod/ ((_),/ (_))") haftmann@26009: (OCaml "Big'_int.quomod'_big'_int") haftmann@26009: (Haskell "divMod") haftmann@34899: (Scala infixl 8 "/%") haftmann@34899: haftmann@34899: code_const divmod_nat haftmann@34899: (Haskell "divMod") haftmann@34899: (Scala infixl 8 "/%") haftmann@25931: haftmann@28346: code_const "eq_class.eq \ nat \ nat \ bool" haftmann@25931: (SML "!((_ : IntInf.int) = _)") haftmann@25931: (OCaml "Big'_int.eq'_big'_int") haftmann@25931: (Haskell infixl 4 "==") haftmann@34899: (Scala infixl 5 "==") haftmann@25931: haftmann@25931: code_const "op \ \ nat \ nat \ bool" haftmann@25931: (SML "IntInf.<= ((_), (_))") haftmann@25931: (OCaml "Big'_int.le'_big'_int") haftmann@25931: (Haskell infix 4 "<=") haftmann@34899: (Scala infixl 4 "<=") haftmann@25931: haftmann@25931: code_const "op < \ nat \ nat \ bool" haftmann@25931: (SML "IntInf.< ((_), (_))") haftmann@25931: (OCaml "Big'_int.lt'_big'_int") haftmann@25931: (Haskell infix 4 "<") haftmann@34899: (Scala infixl 4 "<") haftmann@25931: haftmann@25931: consts_code haftmann@28522: "0::nat" ("0") haftmann@28522: "1::nat" ("1") haftmann@25931: Suc ("(_ +/ 1)") haftmann@25931: "op + \ nat \ nat \ nat" ("(_ +/ _)") haftmann@25931: "op * \ nat \ nat \ nat" ("(_ */ _)") haftmann@25931: "op \ \ nat \ nat \ bool" ("(_ <=/ _)") haftmann@25931: "op < \ nat \ nat \ bool" ("(_ nat \ term) = Code_Evaluation.term_of" .. haftmann@28228: haftmann@32657: code_const "Code_Evaluation.term_of \ nat \ term" haftmann@28228: (SML "HOLogic.mk'_number/ HOLogic.natT") haftmann@28228: haftmann@28228: haftmann@25931: text {* Module names *} haftmann@23854: haftmann@23854: code_modulename SML haftmann@33364: Efficient_Nat Arith haftmann@23854: haftmann@23854: code_modulename OCaml haftmann@33364: Efficient_Nat Arith haftmann@23854: haftmann@23854: code_modulename Haskell haftmann@33364: Efficient_Nat Arith haftmann@23854: wenzelm@36176: hide_const int haftmann@23854: haftmann@23854: end