--- 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)
*}
--- 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) =
--- 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 *}
--- 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
--- 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
--- 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
--- 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