# HG changeset patch # User haftmann # Date 1197526143 -3600 # Node ID b337edd55a079b7413a44799fa650f47ecc49fc4 # Parent 0b8baa94b866c02c99bb9866fe5ac2a15881c3d4 target language div and mod diff -r 0b8baa94b866 -r b337edd55a07 src/HOL/Library/Efficient_Nat.thy --- a/src/HOL/Library/Efficient_Nat.thy Thu Dec 13 07:09:02 2007 +0100 +++ b/src/HOL/Library/Efficient_Nat.thy Thu Dec 13 07:09:03 2007 +0100 @@ -74,7 +74,7 @@ *} lemma [code unfold, code inline del]: - "nat_case \ (\f g n. if n = 0 then f else g (n - 1))" + "nat_case = (\f g n. if n = 0 then f else g (n - 1))" proof - have rewrite: "\f g n. nat_case f g n = (if n = 0 then f else g (n - 1))" proof - @@ -82,7 +82,7 @@ show "nat_case f g n = (if n = 0 then f else g (n - 1))" by (cases n) simp_all qed - show "nat_case \ (\f g n. if n = 0 then f else g (n - 1))" + show "nat_case = (\f g n. if n = 0 then f else g (n - 1))" by (rule eq_reflection ext rewrite)+ qed @@ -140,10 +140,10 @@ unfolding mod_def [symmetric] int_of_nat_def zmod_int [symmetric] unfolding int_of_nat_def [symmetric] nat_of_int_int .. -lemma [code, code inline]: "(m < n) \ (int_of_nat m < int_of_nat n)" +lemma [code, code inline]: "m < n \ int_of_nat m < int_of_nat n" unfolding int_of_nat_def by simp -lemma [code func, code inline]: "(m \ n) \ (int_of_nat m \ int_of_nat n)" +lemma [code func, code inline]: "m \ n \ int_of_nat m \ int_of_nat n" unfolding int_of_nat_def by simp lemma [code func, code inline]: "m = n \ int_of_nat m = int_of_nat n" @@ -226,6 +226,18 @@ (OCaml "_") (Haskell "_") +text {* Using target language div and mod *} + +code_const "op div \ nat \ nat \ nat" + (SML "IntInf.div ((_), (_))") + (OCaml "Big'_int.div'_big'_int") + (Haskell "div") + +code_const "op mod \ nat \ nat \ nat" + (SML "IntInf.mod ((_), (_))") + (OCaml "Big'_int.mod'_big'_int") + (Haskell "mod") + subsection {* Preprocessors *}