--- a/src/HOL/Library/EfficientNat.thy Fri Mar 02 15:43:25 2007 +0100
+++ b/src/HOL/Library/EfficientNat.thy Fri Mar 02 15:43:26 2007 +0100
@@ -31,6 +31,18 @@
nat_of_int :: "int \<Rightarrow> nat" where
"k \<ge> 0 \<Longrightarrow> nat_of_int k = nat k"
+lemma nat_of_int_of_number_of:
+ fixes k
+ assumes "k \<ge> 0"
+ shows "number_of k = nat_of_int k"
+ unfolding nat_of_int_def [OF prems] nat_number_of_def number_of_is_id ..
+
+lemma nat_of_int_of_number_of_aux:
+ fixes k
+ assumes "Numeral.Pls \<le> k \<equiv> True"
+ shows "k \<ge> 0"
+ using prems unfolding Pls_def by simp
+
lemma nat_of_int_int:
"nat_of_int (int n) = n"
using zero_zle_int nat_of_int_def by simp
@@ -121,6 +133,15 @@
then show ?thesis unfolding int_aux_def by simp
qed
+lemma div_nat_code [code func]:
+ "m div k = nat_of_int (fst (divAlg (int m, int k)))"
+ unfolding div_def [symmetric] zdiv_int [symmetric] nat_of_int_int ..
+
+lemma mod_nat_code [code func]:
+ "m mod k = nat_of_int (snd (divAlg (int m, int k)))"
+ unfolding mod_def [symmetric] zmod_int [symmetric] nat_of_int_int ..
+
+
subsection {* Code generator setup for basic functions *}
text {*
@@ -187,12 +208,40 @@
(OCaml "_")
(Haskell "_")
-hide const nat_of_int
-
subsection {* Preprocessors *}
text {*
+ Natural numerals should be expressed using @{const nat_of_int}.
+*}
+
+lemmas [code noinline] = nat_number_of_def
+
+ML {*
+fun nat_of_int_of_number_of thy cts =
+ let
+ val simplify_less = Simplifier.rewrite
+ (HOL_basic_ss addsimps (@{thms less_numeral_code} @ @{thms less_eq_numeral_code}));
+ fun mk_rew (t, ty) =
+ if ty = HOLogic.natT andalso IntInf.<= (0, HOLogic.dest_numeral t) then
+ Thm.capply @{cterm "(op \<le>) Numeral.Pls"} (Thm.cterm_of thy t)
+ |> simplify_less
+ |> (fn thm => @{thm nat_of_int_of_number_of_aux} OF [thm])
+ |> (fn thm => @{thm nat_of_int_of_number_of} OF [thm])
+ |> (fn thm => @{thm eq_reflection} OF [thm])
+ |> SOME
+ else NONE
+ in
+ fold (HOLogic.add_numerals_of o Thm.term_of) cts []
+ |> map_filter mk_rew
+ end;
+*}
+
+setup {*
+ CodegenData.add_inline_proc ("nat_of_int_of_number_of", nat_of_int_of_number_of)
+*}
+
+text {*
In contrast to @{term "Suc n"}, the term @{term "n + (1::nat)"} is no longer
a constructor term. Therefore, all occurrences of this term in a position
where a pattern is expected (i.e.\ on the left-hand side of a recursion
@@ -334,7 +383,6 @@
setup {*
Codegen.add_preprocessor eqn_suc_preproc
#> Codegen.add_preprocessor clause_suc_preproc
- #> CodegenData.del_inline_proc "elim_number_of_nat"
#> CodegenData.add_preproc ("eqn_Suc", lift_obj_eq eqn_suc_preproc)
#> CodegenData.add_preproc ("clause_Suc", lift_obj_eq clause_suc_preproc)
*}
@@ -350,4 +398,6 @@
Nat Integer
EfficientNat Integer
+hide const nat_of_int
+
end