# HG changeset patch
# User haftmann
# Date 1158672118 -7200
# Node ID db6bedfba49828a834b21b093de745b0d1997901
# Parent  b80c4a5cd01828ef6a3fa265fa8c3023cb87ec48
improved numeral handling for nbe

diff -r b80c4a5cd018 -r db6bedfba498 src/HOL/Integ/IntArith.thy
--- a/src/HOL/Integ/IntArith.thy	Tue Sep 19 15:21:55 2006 +0200
+++ b/src/HOL/Integ/IntArith.thy	Tue Sep 19 15:21:58 2006 +0200
@@ -368,90 +368,75 @@
   "Numeral.bit" "IntDef.bit"
 
 code_constname
+  "number_of \<Colon> int \<Rightarrow> int" "IntDef.number_of"
+  "Numeral.pred" "IntDef.pred"
+  "Numeral.succ" "IntDef.succ"
   "Numeral.Pls" "IntDef.pls"
   "Numeral.Min" "IntDef.min"
   "Numeral.Bit" "IntDef.bit"
   "Numeral.bit.bit_case" "IntDef.bit_case"
+  "OperationalEquality.eq \<Colon> bit \<Rightarrow> bit \<Rightarrow> bool" "IntDef.eq_bit"
   "Numeral.B0" "IntDef.b0"
   "Numeral.B1" "IntDef.b1"
 
-lemma
-  Numeral_Pls_refl [code func]: "Numeral.Pls = Numeral.Pls" ..
+lemma Numeral_Pls_refl [code func]:
+  "Numeral.Pls = Numeral.Pls" ..
 
-lemma
-  Numeral_Min_refl [code func]: "Numeral.Min = Numeral.Min" ..
+lemma Numeral_Min_refl [code func]:
+  "Numeral.Min = Numeral.Min" ..
 
-lemma
-  Numeral_Bit_refl [code func]: "Numeral.Bit = Numeral.Bit" ..
+lemma Numeral_Bit_refl [code func]:
+  "Numeral.Bit = Numeral.Bit" ..
 
-lemma zero_is_num_zero [code func, code inline]:
-  "(0::int) = Numeral.Pls" 
-  unfolding Pls_def ..
+lemma zero_int_refl [code func]:
+  "(0\<Colon>int) = 0" ..
 
-lemma one_is_num_one [code func, code inline]:
-  "(1::int) = Numeral.Pls BIT bit.B1" 
-  unfolding Pls_def Bit_def by simp 
+lemma one_int_refl [code func]:
+  "(1\<Colon>int) = 1" ..
 
-lemma number_of_is_id [code func, code inline]:
+lemma number_of_int_refl [code func]:
+  "(number_of \<Colon> int \<Rightarrow> int) = number_of" ..
+
+lemma number_of_is_id:
   "number_of (k::int) = k"
   unfolding int_number_of_def by simp
 
-lemma number_of_minus:
-  "number_of (b :: int) = (- number_of (- b) :: int)"
-  unfolding int_number_of_def by simp
+lemma zero_is_num_zero [code inline]:
+  "(0::int) = number_of Numeral.Pls" 
+  by simp
+
+lemma one_is_num_one [code inline]:
+  "(1::int) = number_of  (Numeral.Pls BIT bit.B1)" 
+  by simp 
+
+lemmas int_code_rewrites =
+  arith_simps(5-27)
+  arith_extra_simps(1-4) [where ?'a1 = int]
+  arith_extra_simps(5) [where ?'a = int]
+
+declare int_code_rewrites [code func]
 
 ML {*
 structure Numeral =
 struct
-
-val number_of_minus_thm = eq_reflection OF [thm "number_of_minus"];
-val minus_rewrites = map (fn thm => eq_reflection OF [thm])
-  [minus_1, minus_0, minus_Pls, minus_Min, pred_1, pred_0, pred_Pls, pred_Min];
-
+ 
 fun int_of_numeral thy num = HOLogic.dest_binum num
   handle TERM _
     => error ("not a number: " ^ Sign.string_of_term thy num);
-
-fun elim_negate thy thms =
-  let
-    fun bins_of (Const _) =
-          I
-      | bins_of (Var _) =
-          I
-      | bins_of (Free _) =
-          I
-      | bins_of (Bound _) =
-          I
-      | bins_of (Abs (_, _, t)) =
-          bins_of t
-      | bins_of (t as _ $ _) =
-          case strip_comb t
-           of (Const ("Numeral.Bit", _), _) => cons t
-            | (t', ts) => bins_of t' #> fold bins_of ts;
-    fun is_negative num = case try HOLogic.dest_binum num
-     of SOME i => i < 0
-      | _ => false;
-    fun instantiate_with bin =
-      Drule.instantiate' [] [(SOME o cterm_of thy) bin] number_of_minus_thm;
-    val rewrites  =
-      []
-      |> fold (bins_of o prop_of) thms
-      |> filter is_negative
-      |> map instantiate_with
-  in if null rewrites then thms else
-    map (CodegenTheorems.rewrite_fun (rewrites @ minus_rewrites)) thms
-  end;
-
+ 
 end;
 *}
 
-code_const "Numeral.Pls" and "Numeral.Min"
-  (SML target_atom "(0 : IntInf.int)" and target_atom "(~1 : IntInf.int)")
-  (Haskell target_atom "0" and target_atom "(negate ~1)")
+code_const "number_of \<Colon> int \<Rightarrow> int" and "Numeral.Pls" and "Numeral.Min"
+  (SML "_"
+     and target_atom "(0 : IntInf.int)"
+     and target_atom "(~1 : IntInf.int)")
+  (Haskell "_"
+     and target_atom "0"
+     and target_atom "(negate 1)")
 
 setup {*
-  CodegenTheorems.add_preproc Numeral.elim_negate
-  #> CodegenPackage.add_appconst ("Numeral.Bit", CodegenPackage.appgen_rep_bin Numeral.int_of_numeral)
+  CodegenPackage.add_appconst ("Numeral.Bit", CodegenPackage.appgen_numeral Numeral.int_of_numeral)
 *}
 
 
diff -r b80c4a5cd018 -r db6bedfba498 src/HOL/Integ/IntDef.thy
--- a/src/HOL/Integ/IntDef.thy	Tue Sep 19 15:21:55 2006 +0200
+++ b/src/HOL/Integ/IntDef.thy	Tue Sep 19 15:21:58 2006 +0200
@@ -264,7 +264,7 @@
 by (cases w, cases z, simp add: le)
 
 (* Axiom 'order_less_le' of class 'order': *)
-lemma zless_le: "((w::int) < z) = (w \<le> z & w \<noteq> z)"
+lemma zless_le [code func]: "((w::int) < z) = (w \<le> z & w \<noteq> z)"
 by (simp add: less_int_def)
 
 instance int :: order
@@ -869,11 +869,11 @@
 fun gen_int i = one_of [~1, 1] * random_range 0 i;
 *}
 
-constdefs
+definition
   int_aux :: "int \<Rightarrow> nat \<Rightarrow> int"
-  "int_aux i n == (i + int n)"
+  "int_aux i n = (i + int n)"
   nat_aux :: "nat \<Rightarrow> int \<Rightarrow> nat"
-  "nat_aux n i == (n + nat i)"
+  "nat_aux n i = (n + nat i)"
 
 lemma [code]:
   "int_aux i 0 = i"
@@ -892,6 +892,10 @@
   "neg k = (k < 0)"
   unfolding neg_def ..
 
+lemma [code func]:
+  "\<bar>k\<Colon>int\<bar> = (if k \<le> 0 then - k else k)"
+  unfolding zabs_def by auto
+
 consts_code
   "0" :: "int"                       ("0")
   "1" :: "int"                       ("1")
@@ -902,30 +906,43 @@
   "Orderings.less_eq" :: "int => int => bool" ("(_ <=/ _)")
   "neg"                              ("(_ < 0)")
 
+instance int :: eq ..
+
 code_type int
   (SML target_atom "IntInf.int")
   (Haskell target_atom "Integer")
 
-code_const "op + :: int \<Rightarrow> int \<Rightarrow> int"
+code_instance int :: eq
+  (Haskell -)
+
+code_const "OperationalEquality.eq \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
+  (SML "(op =) (_ : IntInf.int, _)")
+  (Haskell infixl 4 "==")
+
+code_const "op <= \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
+  (SML "IntInf.<= (_, _)")
+  (Haskell infix 4 "<=")
+
+code_const "op < \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
+  (SML "IntInf.< (_, _)")
+  (Haskell infix 4 "<")
+
+code_const "op + \<Colon> int \<Rightarrow> int \<Rightarrow> int"
   (SML "IntInf.+ (_, _)")
   (Haskell infixl 6 "+")
 
-code_const "op * :: int \<Rightarrow> int \<Rightarrow> int"
+code_const "op - \<Colon> int \<Rightarrow> int \<Rightarrow> int"
+  (SML "IntInf.- (_, _)")
+  (Haskell infixl 6 "-")
+
+code_const "op * \<Colon> int \<Rightarrow> int \<Rightarrow> int"
   (SML "IntInf.* (_, _)")
   (Haskell infixl 7 "*")
 
-code_const "uminus :: int \<Rightarrow> int"
+code_const "uminus \<Colon> int \<Rightarrow> int"
   (SML target_atom "IntInf.~")
   (Haskell target_atom "negate")
 
-code_const "op = :: int \<Rightarrow> int \<Rightarrow> bool"
-  (SML "(op =) (_ : IntInf.int, _)")
-  (Haskell infixl 4 "==")
-
-code_const "op <= :: int \<Rightarrow> int \<Rightarrow> bool"
-  (SML "IntInf.<= (_, _)")
-  (Haskell infix 4 "<=")
-
 ML {*
 fun number_of_codegen thy defs gr dep module b (Const ("Numeral.number_of",
       Type ("fun", [_, T as Type ("IntDef.int", [])])) $ bin) =
diff -r b80c4a5cd018 -r db6bedfba498 src/HOL/Integ/NatBin.thy
--- a/src/HOL/Integ/NatBin.thy	Tue Sep 19 15:21:55 2006 +0200
+++ b/src/HOL/Integ/NatBin.thy	Tue Sep 19 15:21:58 2006 +0200
@@ -773,9 +773,56 @@
 
 subsection {* code generator setup *}
 
-lemma number_of_is_nat_rep_bin [code inline]:
-  "(number_of b :: nat) = nat (number_of b)"
-  unfolding nat_number_of_def int_number_of_def by simp
+lemma neg_number_of_Pls:
+  "\<not> neg ((number_of Numeral.Pls) \<Colon> int)"
+  by auto
+
+lemma neg_number_of_Min:
+  "neg ((number_of Numeral.Min) \<Colon> int)"
+  by auto
+
+lemmas nat_number_expand = nat_number Let_def if_def2 if_True if_False
+  neg_number_of_Pls neg_number_of_Min neg_number_of_BIT Nat.plus.simps
+
+ML {*
+structure NumeralNat =
+struct
+
+val nat_number_expand = thms "nat_number_expand";
+
+fun elim_number_of_nat thy thms =
+  let
+    fun bins_of (Const _) =
+          I
+      | bins_of (Var _) =
+          I
+      | bins_of (Free _) =
+          I
+      | bins_of (Bound _) =
+          I
+      | bins_of (Abs (_, _, t)) =
+          bins_of t
+      | bins_of (t as _ $ _) =
+          case strip_comb t
+           of (Const ("Numeral.number_of",
+               Type (_, [_, Type ("nat", [])])), _) => cons t
+            | (t', ts) => bins_of t' #> fold bins_of ts;
+    val simpset =
+      HOL_basic_ss addsimps nat_number_expand;
+    val rewrites  =
+      []
+      |> (fold o Drule.fold_terms) bins_of thms
+      |> map (Simplifier.rewrite simpset o Thm.cterm_of thy);
+  in if null rewrites then thms else
+    map (CodegenData.rewrite_func rewrites) thms
+  end;
+
+end;
+*}
+
+setup {*
+  CodegenData.add_preproc NumeralNat.elim_number_of_nat
+*}
 
 
 subsection {* legacy ML bindings *}
diff -r b80c4a5cd018 -r db6bedfba498 src/HOL/Integ/Presburger.thy
--- a/src/HOL/Integ/Presburger.thy	Tue Sep 19 15:21:55 2006 +0200
+++ b/src/HOL/Integ/Presburger.thy	Tue Sep 19 15:21:58 2006 +0200
@@ -1086,4 +1086,137 @@
 
 setup "Presburger.setup"
 
+text {* Code generator setup *}
+
+text {*
+  Presburger arithmetic is neccesary to prove some
+  of the following code lemmas on integer numerals.
+*}
+
+lemma eq_number_of [code func]:
+  "OperationalEquality.eq ((number_of k)\<Colon>int) (number_of l) \<longleftrightarrow> OperationalEquality.eq k l"
+  unfolding number_of_is_id ..
+
+lemma less_eq_number_of [code func]:
+  "((number_of k)\<Colon>int) <= number_of l \<longleftrightarrow> k <= l"
+  unfolding number_of_is_id ..
+
+lemma eq_Pls_Pls:
+  "OperationalEquality.eq Numeral.Pls Numeral.Pls"
+  unfolding eq_def ..
+
+lemma eq_Pls_Min:
+  "\<not> OperationalEquality.eq Numeral.Pls Numeral.Min"
+  unfolding eq_def Pls_def Min_def by auto
+
+lemma eq_Pls_Bit0:
+  "OperationalEquality.eq Numeral.Pls (Numeral.Bit k bit.B0) \<longleftrightarrow> OperationalEquality.eq Numeral.Pls k"
+  unfolding eq_def Pls_def Bit_def bit.cases by auto
+
+lemma eq_Pls_Bit1:
+  "\<not> OperationalEquality.eq Numeral.Pls (Numeral.Bit k bit.B1)"
+  unfolding eq_def Pls_def Bit_def bit.cases by arith
+
+lemma eq_Min_Pls:
+  "\<not> OperationalEquality.eq Numeral.Min Numeral.Pls"
+  unfolding eq_def Pls_def Min_def by auto
+
+lemma eq_Min_Min:
+  "OperationalEquality.eq Numeral.Min Numeral.Min"
+  unfolding eq_def ..
+
+lemma eq_Min_Bit0:
+  "\<not> OperationalEquality.eq Numeral.Min (Numeral.Bit k bit.B0)"
+  unfolding eq_def Min_def Bit_def bit.cases by arith
+
+lemma eq_Min_Bit1:
+  "OperationalEquality.eq Numeral.Min (Numeral.Bit k bit.B1) \<longleftrightarrow> OperationalEquality.eq Numeral.Min k"
+  unfolding eq_def Min_def Bit_def bit.cases by auto
+
+lemma eq_Bit0_Pls:
+  "OperationalEquality.eq (Numeral.Bit k bit.B0) Numeral.Pls \<longleftrightarrow> OperationalEquality.eq Numeral.Pls k"
+  unfolding eq_def Pls_def Bit_def bit.cases by auto
+
+lemma eq_Bit1_Pls:
+  "\<not> OperationalEquality.eq (Numeral.Bit k bit.B1) Numeral.Pls"
+  unfolding eq_def Pls_def Bit_def bit.cases by arith
+
+lemma eq_Bit0_Min:
+  "\<not> OperationalEquality.eq (Numeral.Bit k bit.B0) Numeral.Min"
+  unfolding eq_def Min_def Bit_def bit.cases by arith
+
+lemma eq_Bit1_Min:
+  "OperationalEquality.eq (Numeral.Bit k bit.B1) Numeral.Min \<longleftrightarrow> OperationalEquality.eq Numeral.Min k"
+  unfolding eq_def Min_def Bit_def bit.cases by auto
+
+lemma eq_Bit_Bit:
+  "OperationalEquality.eq (Numeral.Bit k1 v1) (Numeral.Bit k2 v2) \<longleftrightarrow>
+    OperationalEquality.eq v1 v2 \<and> OperationalEquality.eq k1 k2"
+  unfolding eq_def Bit_def
+  apply (cases v1)
+  apply (cases v2)
+  apply auto
+  apply arith
+  apply (cases v2)
+  apply auto
+  apply arith
+  apply (cases v2)
+  apply auto
+done
+
+lemmas eq_numeral_code [code func] =
+  eq_Pls_Pls eq_Pls_Min eq_Pls_Bit0 eq_Pls_Bit1
+  eq_Min_Pls eq_Min_Min eq_Min_Bit0 eq_Min_Bit1
+  eq_Bit0_Pls eq_Bit1_Pls eq_Bit0_Min eq_Bit1_Min eq_Bit_Bit
+
+lemma less_eq_Pls_Pls:
+  "Numeral.Pls \<le> Numeral.Pls" ..
+
+lemma less_eq_Pls_Min:
+  "\<not> (Numeral.Pls \<le> Numeral.Min)"
+  unfolding Pls_def Min_def by auto
+
+lemma less_eq_Pls_Bit:
+  "Numeral.Pls \<le> Numeral.Bit k v \<longleftrightarrow> Numeral.Pls \<le> k"
+  unfolding Pls_def Bit_def by (cases v) auto
+
+lemma less_eq_Min_Pls:
+  "Numeral.Min \<le> Numeral.Pls"
+  unfolding Pls_def Min_def by auto
+
+lemma less_eq_Min_Min:
+  "Numeral.Min \<le> Numeral.Min" ..
+
+lemma less_eq_Min_Bit0:
+  "Numeral.Min \<le> Numeral.Bit k bit.B0 \<longleftrightarrow> Numeral.Min < k"
+  unfolding Min_def Bit_def by auto
+
+lemma less_eq_Min_Bit1:
+  "Numeral.Min \<le> Numeral.Bit k bit.B1 \<longleftrightarrow> Numeral.Min \<le> k"
+  unfolding Min_def Bit_def by auto
+
+lemma less_eq_Bit0_Pls:
+  "Numeral.Bit k bit.B0 \<le> Numeral.Pls \<longleftrightarrow> k \<le> Numeral.Pls"
+  unfolding Pls_def Bit_def by simp
+
+lemma less_eq_Bit1_Pls:
+  "Numeral.Bit k bit.B1 \<le> Numeral.Pls \<longleftrightarrow> k < Numeral.Pls"
+  unfolding Pls_def Bit_def by auto
+
+lemma less_eq_Bit_Min:
+  "Numeral.Bit k v \<le> Numeral.Min \<longleftrightarrow> k \<le> Numeral.Min"
+  unfolding Min_def Bit_def by (cases v) auto
+
+lemma less_eq_Bit0_Bit:
+  "Numeral.Bit k1 bit.B0 \<le> Numeral.Bit k2 v \<longleftrightarrow> k1 \<le> k2"
+  unfolding Min_def Bit_def bit.cases by (cases v) auto
+
+lemma less_eq_Bit_Bit1:
+  "Numeral.Bit k1 v \<le> Numeral.Bit k2 bit.B1 \<longleftrightarrow> k1 \<le> k2"
+  unfolding Min_def Bit_def bit.cases by (cases v) auto
+
+lemmas less_eq_numeral_code [code func] = less_eq_Pls_Pls less_eq_Pls_Min less_eq_Pls_Bit
+  less_eq_Min_Pls less_eq_Min_Min less_eq_Min_Bit0 less_eq_Min_Bit1
+  less_eq_Bit0_Pls less_eq_Bit1_Pls less_eq_Bit_Min less_eq_Bit0_Bit less_eq_Bit_Bit1
+
 end
diff -r b80c4a5cd018 -r db6bedfba498 src/HOL/Presburger.thy
--- a/src/HOL/Presburger.thy	Tue Sep 19 15:21:55 2006 +0200
+++ b/src/HOL/Presburger.thy	Tue Sep 19 15:21:58 2006 +0200
@@ -1086,4 +1086,137 @@
 
 setup "Presburger.setup"
 
+text {* Code generator setup *}
+
+text {*
+  Presburger arithmetic is neccesary to prove some
+  of the following code lemmas on integer numerals.
+*}
+
+lemma eq_number_of [code func]:
+  "OperationalEquality.eq ((number_of k)\<Colon>int) (number_of l) \<longleftrightarrow> OperationalEquality.eq k l"
+  unfolding number_of_is_id ..
+
+lemma less_eq_number_of [code func]:
+  "((number_of k)\<Colon>int) <= number_of l \<longleftrightarrow> k <= l"
+  unfolding number_of_is_id ..
+
+lemma eq_Pls_Pls:
+  "OperationalEquality.eq Numeral.Pls Numeral.Pls"
+  unfolding eq_def ..
+
+lemma eq_Pls_Min:
+  "\<not> OperationalEquality.eq Numeral.Pls Numeral.Min"
+  unfolding eq_def Pls_def Min_def by auto
+
+lemma eq_Pls_Bit0:
+  "OperationalEquality.eq Numeral.Pls (Numeral.Bit k bit.B0) \<longleftrightarrow> OperationalEquality.eq Numeral.Pls k"
+  unfolding eq_def Pls_def Bit_def bit.cases by auto
+
+lemma eq_Pls_Bit1:
+  "\<not> OperationalEquality.eq Numeral.Pls (Numeral.Bit k bit.B1)"
+  unfolding eq_def Pls_def Bit_def bit.cases by arith
+
+lemma eq_Min_Pls:
+  "\<not> OperationalEquality.eq Numeral.Min Numeral.Pls"
+  unfolding eq_def Pls_def Min_def by auto
+
+lemma eq_Min_Min:
+  "OperationalEquality.eq Numeral.Min Numeral.Min"
+  unfolding eq_def ..
+
+lemma eq_Min_Bit0:
+  "\<not> OperationalEquality.eq Numeral.Min (Numeral.Bit k bit.B0)"
+  unfolding eq_def Min_def Bit_def bit.cases by arith
+
+lemma eq_Min_Bit1:
+  "OperationalEquality.eq Numeral.Min (Numeral.Bit k bit.B1) \<longleftrightarrow> OperationalEquality.eq Numeral.Min k"
+  unfolding eq_def Min_def Bit_def bit.cases by auto
+
+lemma eq_Bit0_Pls:
+  "OperationalEquality.eq (Numeral.Bit k bit.B0) Numeral.Pls \<longleftrightarrow> OperationalEquality.eq Numeral.Pls k"
+  unfolding eq_def Pls_def Bit_def bit.cases by auto
+
+lemma eq_Bit1_Pls:
+  "\<not> OperationalEquality.eq (Numeral.Bit k bit.B1) Numeral.Pls"
+  unfolding eq_def Pls_def Bit_def bit.cases by arith
+
+lemma eq_Bit0_Min:
+  "\<not> OperationalEquality.eq (Numeral.Bit k bit.B0) Numeral.Min"
+  unfolding eq_def Min_def Bit_def bit.cases by arith
+
+lemma eq_Bit1_Min:
+  "OperationalEquality.eq (Numeral.Bit k bit.B1) Numeral.Min \<longleftrightarrow> OperationalEquality.eq Numeral.Min k"
+  unfolding eq_def Min_def Bit_def bit.cases by auto
+
+lemma eq_Bit_Bit:
+  "OperationalEquality.eq (Numeral.Bit k1 v1) (Numeral.Bit k2 v2) \<longleftrightarrow>
+    OperationalEquality.eq v1 v2 \<and> OperationalEquality.eq k1 k2"
+  unfolding eq_def Bit_def
+  apply (cases v1)
+  apply (cases v2)
+  apply auto
+  apply arith
+  apply (cases v2)
+  apply auto
+  apply arith
+  apply (cases v2)
+  apply auto
+done
+
+lemmas eq_numeral_code [code func] =
+  eq_Pls_Pls eq_Pls_Min eq_Pls_Bit0 eq_Pls_Bit1
+  eq_Min_Pls eq_Min_Min eq_Min_Bit0 eq_Min_Bit1
+  eq_Bit0_Pls eq_Bit1_Pls eq_Bit0_Min eq_Bit1_Min eq_Bit_Bit
+
+lemma less_eq_Pls_Pls:
+  "Numeral.Pls \<le> Numeral.Pls" ..
+
+lemma less_eq_Pls_Min:
+  "\<not> (Numeral.Pls \<le> Numeral.Min)"
+  unfolding Pls_def Min_def by auto
+
+lemma less_eq_Pls_Bit:
+  "Numeral.Pls \<le> Numeral.Bit k v \<longleftrightarrow> Numeral.Pls \<le> k"
+  unfolding Pls_def Bit_def by (cases v) auto
+
+lemma less_eq_Min_Pls:
+  "Numeral.Min \<le> Numeral.Pls"
+  unfolding Pls_def Min_def by auto
+
+lemma less_eq_Min_Min:
+  "Numeral.Min \<le> Numeral.Min" ..
+
+lemma less_eq_Min_Bit0:
+  "Numeral.Min \<le> Numeral.Bit k bit.B0 \<longleftrightarrow> Numeral.Min < k"
+  unfolding Min_def Bit_def by auto
+
+lemma less_eq_Min_Bit1:
+  "Numeral.Min \<le> Numeral.Bit k bit.B1 \<longleftrightarrow> Numeral.Min \<le> k"
+  unfolding Min_def Bit_def by auto
+
+lemma less_eq_Bit0_Pls:
+  "Numeral.Bit k bit.B0 \<le> Numeral.Pls \<longleftrightarrow> k \<le> Numeral.Pls"
+  unfolding Pls_def Bit_def by simp
+
+lemma less_eq_Bit1_Pls:
+  "Numeral.Bit k bit.B1 \<le> Numeral.Pls \<longleftrightarrow> k < Numeral.Pls"
+  unfolding Pls_def Bit_def by auto
+
+lemma less_eq_Bit_Min:
+  "Numeral.Bit k v \<le> Numeral.Min \<longleftrightarrow> k \<le> Numeral.Min"
+  unfolding Min_def Bit_def by (cases v) auto
+
+lemma less_eq_Bit0_Bit:
+  "Numeral.Bit k1 bit.B0 \<le> Numeral.Bit k2 v \<longleftrightarrow> k1 \<le> k2"
+  unfolding Min_def Bit_def bit.cases by (cases v) auto
+
+lemma less_eq_Bit_Bit1:
+  "Numeral.Bit k1 v \<le> Numeral.Bit k2 bit.B1 \<longleftrightarrow> k1 \<le> k2"
+  unfolding Min_def Bit_def bit.cases by (cases v) auto
+
+lemmas less_eq_numeral_code [code func] = less_eq_Pls_Pls less_eq_Pls_Min less_eq_Pls_Bit
+  less_eq_Min_Pls less_eq_Min_Min less_eq_Min_Bit0 less_eq_Min_Bit1
+  less_eq_Bit0_Pls less_eq_Bit1_Pls less_eq_Bit_Min less_eq_Bit0_Bit less_eq_Bit_Bit1
+
 end
diff -r b80c4a5cd018 -r db6bedfba498 src/HOL/ex/NormalForm.thy
--- a/src/HOL/ex/NormalForm.thy	Tue Sep 19 15:21:55 2006 +0200
+++ b/src/HOL/ex/NormalForm.thy	Tue Sep 19 15:21:58 2006 +0200
@@ -10,11 +10,10 @@
 
 lemma "p \<longrightarrow> True" by normalization
 declare disj_assoc [code func]
-normal_form  "(P | Q) | R"
-
+lemma "((P | Q) | R) = (P | (Q | R))" by normalization
 lemma "0 + (n::nat) = n" by normalization
-lemma "0 + Suc(n) = Suc n" by normalization
-lemma "Suc(n) + Suc m = n + Suc(Suc m)" by normalization
+lemma "0 + Suc n = Suc n" by normalization
+lemma "Suc n + Suc m = n + Suc (Suc m)" by normalization
 lemma "~((0::nat) < (0::nat))" by normalization
 
 
@@ -93,14 +92,22 @@
 normal_form "%x. case x of None \<Rightarrow> False | Some y \<Rightarrow> True"
 normal_form "map (%x. case x of None \<Rightarrow> False | Some y \<Rightarrow> True) [None, Some ()]"
 
-normal_form "last[a,b,c]"
-normal_form "last([a,b,c]@xs)"
+normal_form "last [a, b, c]"
+normal_form "last ([a, b, c] @ xs)"
 
 normal_form "min 0 x"
 normal_form "min 0 (x::nat)"
 
-text {*
-  Numerals still take their time\<dots>
-*}
+normal_form "(2::int) + 3 - 1 + (- k) * 2"
+normal_form "(4::int) * 2"
+normal_form "(-4::int) * 2"
+normal_form "abs ((-4::int) + 2 * 1)"
+normal_form "(2::int) + 3"
+normal_form "(2::int) + 3 * (- 4) * (- 1)"
+normal_form "(2::int) + 3 * (- 4) * 1 + 0"
+normal_form "(2::int) < 3"
+normal_form "(2::int) <= 3"
+normal_form "abs ((-4::int) + 2 * 1)"
+normal_form "4 - 42 * abs (3 + (-7\<Colon>int))"
 
 end
diff -r b80c4a5cd018 -r db6bedfba498 src/HOL/ex/reflection.ML
--- a/src/HOL/ex/reflection.ML	Tue Sep 19 15:21:55 2006 +0200
+++ b/src/HOL/ex/reflection.ML	Tue Sep 19 15:21:58 2006 +0200
@@ -279,7 +279,7 @@
 fun genreflect ctxt corr_thm raw_eqs t =
     let val th = FWD trans [genreif ctxt raw_eqs t, corr_thm RS sym]
         val ft = (snd o Thm.dest_comb o snd o Thm.dest_comb o snd o Thm.dest_comb o cprop_of) th
-        val rth = normalization_conv ft
+        val rth = NBE.normalization_conv ft
     in simplify (HOL_basic_ss addsimps raw_eqs addsimps [nth_Cons_0, nth_Cons_Suc])
                 (simplify (HOL_basic_ss addsimps [rth]) th)
     end