improved numeral handling for nbe
authorhaftmann
Tue Sep 19 15:21:58 2006 +0200 (2006-09-19)
changeset 20595db6bedfba498
parent 20594 b80c4a5cd018
child 20596 3950e65f48f8
improved numeral handling for nbe
src/HOL/Integ/IntArith.thy
src/HOL/Integ/IntDef.thy
src/HOL/Integ/NatBin.thy
src/HOL/Integ/Presburger.thy
src/HOL/Presburger.thy
src/HOL/ex/NormalForm.thy
src/HOL/ex/reflection.ML
     1.1 --- a/src/HOL/Integ/IntArith.thy	Tue Sep 19 15:21:55 2006 +0200
     1.2 +++ b/src/HOL/Integ/IntArith.thy	Tue Sep 19 15:21:58 2006 +0200
     1.3 @@ -368,90 +368,75 @@
     1.4    "Numeral.bit" "IntDef.bit"
     1.5  
     1.6  code_constname
     1.7 +  "number_of \<Colon> int \<Rightarrow> int" "IntDef.number_of"
     1.8 +  "Numeral.pred" "IntDef.pred"
     1.9 +  "Numeral.succ" "IntDef.succ"
    1.10    "Numeral.Pls" "IntDef.pls"
    1.11    "Numeral.Min" "IntDef.min"
    1.12    "Numeral.Bit" "IntDef.bit"
    1.13    "Numeral.bit.bit_case" "IntDef.bit_case"
    1.14 +  "OperationalEquality.eq \<Colon> bit \<Rightarrow> bit \<Rightarrow> bool" "IntDef.eq_bit"
    1.15    "Numeral.B0" "IntDef.b0"
    1.16    "Numeral.B1" "IntDef.b1"
    1.17  
    1.18 -lemma
    1.19 -  Numeral_Pls_refl [code func]: "Numeral.Pls = Numeral.Pls" ..
    1.20 +lemma Numeral_Pls_refl [code func]:
    1.21 +  "Numeral.Pls = Numeral.Pls" ..
    1.22  
    1.23 -lemma
    1.24 -  Numeral_Min_refl [code func]: "Numeral.Min = Numeral.Min" ..
    1.25 +lemma Numeral_Min_refl [code func]:
    1.26 +  "Numeral.Min = Numeral.Min" ..
    1.27  
    1.28 -lemma
    1.29 -  Numeral_Bit_refl [code func]: "Numeral.Bit = Numeral.Bit" ..
    1.30 +lemma Numeral_Bit_refl [code func]:
    1.31 +  "Numeral.Bit = Numeral.Bit" ..
    1.32  
    1.33 -lemma zero_is_num_zero [code func, code inline]:
    1.34 -  "(0::int) = Numeral.Pls" 
    1.35 -  unfolding Pls_def ..
    1.36 +lemma zero_int_refl [code func]:
    1.37 +  "(0\<Colon>int) = 0" ..
    1.38  
    1.39 -lemma one_is_num_one [code func, code inline]:
    1.40 -  "(1::int) = Numeral.Pls BIT bit.B1" 
    1.41 -  unfolding Pls_def Bit_def by simp 
    1.42 +lemma one_int_refl [code func]:
    1.43 +  "(1\<Colon>int) = 1" ..
    1.44  
    1.45 -lemma number_of_is_id [code func, code inline]:
    1.46 +lemma number_of_int_refl [code func]:
    1.47 +  "(number_of \<Colon> int \<Rightarrow> int) = number_of" ..
    1.48 +
    1.49 +lemma number_of_is_id:
    1.50    "number_of (k::int) = k"
    1.51    unfolding int_number_of_def by simp
    1.52  
    1.53 -lemma number_of_minus:
    1.54 -  "number_of (b :: int) = (- number_of (- b) :: int)"
    1.55 -  unfolding int_number_of_def by simp
    1.56 +lemma zero_is_num_zero [code inline]:
    1.57 +  "(0::int) = number_of Numeral.Pls" 
    1.58 +  by simp
    1.59 +
    1.60 +lemma one_is_num_one [code inline]:
    1.61 +  "(1::int) = number_of  (Numeral.Pls BIT bit.B1)" 
    1.62 +  by simp 
    1.63 +
    1.64 +lemmas int_code_rewrites =
    1.65 +  arith_simps(5-27)
    1.66 +  arith_extra_simps(1-4) [where ?'a1 = int]
    1.67 +  arith_extra_simps(5) [where ?'a = int]
    1.68 +
    1.69 +declare int_code_rewrites [code func]
    1.70  
    1.71  ML {*
    1.72  structure Numeral =
    1.73  struct
    1.74 -
    1.75 -val number_of_minus_thm = eq_reflection OF [thm "number_of_minus"];
    1.76 -val minus_rewrites = map (fn thm => eq_reflection OF [thm])
    1.77 -  [minus_1, minus_0, minus_Pls, minus_Min, pred_1, pred_0, pred_Pls, pred_Min];
    1.78 -
    1.79 + 
    1.80  fun int_of_numeral thy num = HOLogic.dest_binum num
    1.81    handle TERM _
    1.82      => error ("not a number: " ^ Sign.string_of_term thy num);
    1.83 -
    1.84 -fun elim_negate thy thms =
    1.85 -  let
    1.86 -    fun bins_of (Const _) =
    1.87 -          I
    1.88 -      | bins_of (Var _) =
    1.89 -          I
    1.90 -      | bins_of (Free _) =
    1.91 -          I
    1.92 -      | bins_of (Bound _) =
    1.93 -          I
    1.94 -      | bins_of (Abs (_, _, t)) =
    1.95 -          bins_of t
    1.96 -      | bins_of (t as _ $ _) =
    1.97 -          case strip_comb t
    1.98 -           of (Const ("Numeral.Bit", _), _) => cons t
    1.99 -            | (t', ts) => bins_of t' #> fold bins_of ts;
   1.100 -    fun is_negative num = case try HOLogic.dest_binum num
   1.101 -     of SOME i => i < 0
   1.102 -      | _ => false;
   1.103 -    fun instantiate_with bin =
   1.104 -      Drule.instantiate' [] [(SOME o cterm_of thy) bin] number_of_minus_thm;
   1.105 -    val rewrites  =
   1.106 -      []
   1.107 -      |> fold (bins_of o prop_of) thms
   1.108 -      |> filter is_negative
   1.109 -      |> map instantiate_with
   1.110 -  in if null rewrites then thms else
   1.111 -    map (CodegenTheorems.rewrite_fun (rewrites @ minus_rewrites)) thms
   1.112 -  end;
   1.113 -
   1.114 + 
   1.115  end;
   1.116  *}
   1.117  
   1.118 -code_const "Numeral.Pls" and "Numeral.Min"
   1.119 -  (SML target_atom "(0 : IntInf.int)" and target_atom "(~1 : IntInf.int)")
   1.120 -  (Haskell target_atom "0" and target_atom "(negate ~1)")
   1.121 +code_const "number_of \<Colon> int \<Rightarrow> int" and "Numeral.Pls" and "Numeral.Min"
   1.122 +  (SML "_"
   1.123 +     and target_atom "(0 : IntInf.int)"
   1.124 +     and target_atom "(~1 : IntInf.int)")
   1.125 +  (Haskell "_"
   1.126 +     and target_atom "0"
   1.127 +     and target_atom "(negate 1)")
   1.128  
   1.129  setup {*
   1.130 -  CodegenTheorems.add_preproc Numeral.elim_negate
   1.131 -  #> CodegenPackage.add_appconst ("Numeral.Bit", CodegenPackage.appgen_rep_bin Numeral.int_of_numeral)
   1.132 +  CodegenPackage.add_appconst ("Numeral.Bit", CodegenPackage.appgen_numeral Numeral.int_of_numeral)
   1.133  *}
   1.134  
   1.135  
     2.1 --- a/src/HOL/Integ/IntDef.thy	Tue Sep 19 15:21:55 2006 +0200
     2.2 +++ b/src/HOL/Integ/IntDef.thy	Tue Sep 19 15:21:58 2006 +0200
     2.3 @@ -264,7 +264,7 @@
     2.4  by (cases w, cases z, simp add: le)
     2.5  
     2.6  (* Axiom 'order_less_le' of class 'order': *)
     2.7 -lemma zless_le: "((w::int) < z) = (w \<le> z & w \<noteq> z)"
     2.8 +lemma zless_le [code func]: "((w::int) < z) = (w \<le> z & w \<noteq> z)"
     2.9  by (simp add: less_int_def)
    2.10  
    2.11  instance int :: order
    2.12 @@ -869,11 +869,11 @@
    2.13  fun gen_int i = one_of [~1, 1] * random_range 0 i;
    2.14  *}
    2.15  
    2.16 -constdefs
    2.17 +definition
    2.18    int_aux :: "int \<Rightarrow> nat \<Rightarrow> int"
    2.19 -  "int_aux i n == (i + int n)"
    2.20 +  "int_aux i n = (i + int n)"
    2.21    nat_aux :: "nat \<Rightarrow> int \<Rightarrow> nat"
    2.22 -  "nat_aux n i == (n + nat i)"
    2.23 +  "nat_aux n i = (n + nat i)"
    2.24  
    2.25  lemma [code]:
    2.26    "int_aux i 0 = i"
    2.27 @@ -892,6 +892,10 @@
    2.28    "neg k = (k < 0)"
    2.29    unfolding neg_def ..
    2.30  
    2.31 +lemma [code func]:
    2.32 +  "\<bar>k\<Colon>int\<bar> = (if k \<le> 0 then - k else k)"
    2.33 +  unfolding zabs_def by auto
    2.34 +
    2.35  consts_code
    2.36    "0" :: "int"                       ("0")
    2.37    "1" :: "int"                       ("1")
    2.38 @@ -902,30 +906,43 @@
    2.39    "Orderings.less_eq" :: "int => int => bool" ("(_ <=/ _)")
    2.40    "neg"                              ("(_ < 0)")
    2.41  
    2.42 +instance int :: eq ..
    2.43 +
    2.44  code_type int
    2.45    (SML target_atom "IntInf.int")
    2.46    (Haskell target_atom "Integer")
    2.47  
    2.48 -code_const "op + :: int \<Rightarrow> int \<Rightarrow> int"
    2.49 +code_instance int :: eq
    2.50 +  (Haskell -)
    2.51 +
    2.52 +code_const "OperationalEquality.eq \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
    2.53 +  (SML "(op =) (_ : IntInf.int, _)")
    2.54 +  (Haskell infixl 4 "==")
    2.55 +
    2.56 +code_const "op <= \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
    2.57 +  (SML "IntInf.<= (_, _)")
    2.58 +  (Haskell infix 4 "<=")
    2.59 +
    2.60 +code_const "op < \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
    2.61 +  (SML "IntInf.< (_, _)")
    2.62 +  (Haskell infix 4 "<")
    2.63 +
    2.64 +code_const "op + \<Colon> int \<Rightarrow> int \<Rightarrow> int"
    2.65    (SML "IntInf.+ (_, _)")
    2.66    (Haskell infixl 6 "+")
    2.67  
    2.68 -code_const "op * :: int \<Rightarrow> int \<Rightarrow> int"
    2.69 +code_const "op - \<Colon> int \<Rightarrow> int \<Rightarrow> int"
    2.70 +  (SML "IntInf.- (_, _)")
    2.71 +  (Haskell infixl 6 "-")
    2.72 +
    2.73 +code_const "op * \<Colon> int \<Rightarrow> int \<Rightarrow> int"
    2.74    (SML "IntInf.* (_, _)")
    2.75    (Haskell infixl 7 "*")
    2.76  
    2.77 -code_const "uminus :: int \<Rightarrow> int"
    2.78 +code_const "uminus \<Colon> int \<Rightarrow> int"
    2.79    (SML target_atom "IntInf.~")
    2.80    (Haskell target_atom "negate")
    2.81  
    2.82 -code_const "op = :: int \<Rightarrow> int \<Rightarrow> bool"
    2.83 -  (SML "(op =) (_ : IntInf.int, _)")
    2.84 -  (Haskell infixl 4 "==")
    2.85 -
    2.86 -code_const "op <= :: int \<Rightarrow> int \<Rightarrow> bool"
    2.87 -  (SML "IntInf.<= (_, _)")
    2.88 -  (Haskell infix 4 "<=")
    2.89 -
    2.90  ML {*
    2.91  fun number_of_codegen thy defs gr dep module b (Const ("Numeral.number_of",
    2.92        Type ("fun", [_, T as Type ("IntDef.int", [])])) $ bin) =
     3.1 --- a/src/HOL/Integ/NatBin.thy	Tue Sep 19 15:21:55 2006 +0200
     3.2 +++ b/src/HOL/Integ/NatBin.thy	Tue Sep 19 15:21:58 2006 +0200
     3.3 @@ -773,9 +773,56 @@
     3.4  
     3.5  subsection {* code generator setup *}
     3.6  
     3.7 -lemma number_of_is_nat_rep_bin [code inline]:
     3.8 -  "(number_of b :: nat) = nat (number_of b)"
     3.9 -  unfolding nat_number_of_def int_number_of_def by simp
    3.10 +lemma neg_number_of_Pls:
    3.11 +  "\<not> neg ((number_of Numeral.Pls) \<Colon> int)"
    3.12 +  by auto
    3.13 +
    3.14 +lemma neg_number_of_Min:
    3.15 +  "neg ((number_of Numeral.Min) \<Colon> int)"
    3.16 +  by auto
    3.17 +
    3.18 +lemmas nat_number_expand = nat_number Let_def if_def2 if_True if_False
    3.19 +  neg_number_of_Pls neg_number_of_Min neg_number_of_BIT Nat.plus.simps
    3.20 +
    3.21 +ML {*
    3.22 +structure NumeralNat =
    3.23 +struct
    3.24 +
    3.25 +val nat_number_expand = thms "nat_number_expand";
    3.26 +
    3.27 +fun elim_number_of_nat thy thms =
    3.28 +  let
    3.29 +    fun bins_of (Const _) =
    3.30 +          I
    3.31 +      | bins_of (Var _) =
    3.32 +          I
    3.33 +      | bins_of (Free _) =
    3.34 +          I
    3.35 +      | bins_of (Bound _) =
    3.36 +          I
    3.37 +      | bins_of (Abs (_, _, t)) =
    3.38 +          bins_of t
    3.39 +      | bins_of (t as _ $ _) =
    3.40 +          case strip_comb t
    3.41 +           of (Const ("Numeral.number_of",
    3.42 +               Type (_, [_, Type ("nat", [])])), _) => cons t
    3.43 +            | (t', ts) => bins_of t' #> fold bins_of ts;
    3.44 +    val simpset =
    3.45 +      HOL_basic_ss addsimps nat_number_expand;
    3.46 +    val rewrites  =
    3.47 +      []
    3.48 +      |> (fold o Drule.fold_terms) bins_of thms
    3.49 +      |> map (Simplifier.rewrite simpset o Thm.cterm_of thy);
    3.50 +  in if null rewrites then thms else
    3.51 +    map (CodegenData.rewrite_func rewrites) thms
    3.52 +  end;
    3.53 +
    3.54 +end;
    3.55 +*}
    3.56 +
    3.57 +setup {*
    3.58 +  CodegenData.add_preproc NumeralNat.elim_number_of_nat
    3.59 +*}
    3.60  
    3.61  
    3.62  subsection {* legacy ML bindings *}
     4.1 --- a/src/HOL/Integ/Presburger.thy	Tue Sep 19 15:21:55 2006 +0200
     4.2 +++ b/src/HOL/Integ/Presburger.thy	Tue Sep 19 15:21:58 2006 +0200
     4.3 @@ -1086,4 +1086,137 @@
     4.4  
     4.5  setup "Presburger.setup"
     4.6  
     4.7 +text {* Code generator setup *}
     4.8 +
     4.9 +text {*
    4.10 +  Presburger arithmetic is neccesary to prove some
    4.11 +  of the following code lemmas on integer numerals.
    4.12 +*}
    4.13 +
    4.14 +lemma eq_number_of [code func]:
    4.15 +  "OperationalEquality.eq ((number_of k)\<Colon>int) (number_of l) \<longleftrightarrow> OperationalEquality.eq k l"
    4.16 +  unfolding number_of_is_id ..
    4.17 +
    4.18 +lemma less_eq_number_of [code func]:
    4.19 +  "((number_of k)\<Colon>int) <= number_of l \<longleftrightarrow> k <= l"
    4.20 +  unfolding number_of_is_id ..
    4.21 +
    4.22 +lemma eq_Pls_Pls:
    4.23 +  "OperationalEquality.eq Numeral.Pls Numeral.Pls"
    4.24 +  unfolding eq_def ..
    4.25 +
    4.26 +lemma eq_Pls_Min:
    4.27 +  "\<not> OperationalEquality.eq Numeral.Pls Numeral.Min"
    4.28 +  unfolding eq_def Pls_def Min_def by auto
    4.29 +
    4.30 +lemma eq_Pls_Bit0:
    4.31 +  "OperationalEquality.eq Numeral.Pls (Numeral.Bit k bit.B0) \<longleftrightarrow> OperationalEquality.eq Numeral.Pls k"
    4.32 +  unfolding eq_def Pls_def Bit_def bit.cases by auto
    4.33 +
    4.34 +lemma eq_Pls_Bit1:
    4.35 +  "\<not> OperationalEquality.eq Numeral.Pls (Numeral.Bit k bit.B1)"
    4.36 +  unfolding eq_def Pls_def Bit_def bit.cases by arith
    4.37 +
    4.38 +lemma eq_Min_Pls:
    4.39 +  "\<not> OperationalEquality.eq Numeral.Min Numeral.Pls"
    4.40 +  unfolding eq_def Pls_def Min_def by auto
    4.41 +
    4.42 +lemma eq_Min_Min:
    4.43 +  "OperationalEquality.eq Numeral.Min Numeral.Min"
    4.44 +  unfolding eq_def ..
    4.45 +
    4.46 +lemma eq_Min_Bit0:
    4.47 +  "\<not> OperationalEquality.eq Numeral.Min (Numeral.Bit k bit.B0)"
    4.48 +  unfolding eq_def Min_def Bit_def bit.cases by arith
    4.49 +
    4.50 +lemma eq_Min_Bit1:
    4.51 +  "OperationalEquality.eq Numeral.Min (Numeral.Bit k bit.B1) \<longleftrightarrow> OperationalEquality.eq Numeral.Min k"
    4.52 +  unfolding eq_def Min_def Bit_def bit.cases by auto
    4.53 +
    4.54 +lemma eq_Bit0_Pls:
    4.55 +  "OperationalEquality.eq (Numeral.Bit k bit.B0) Numeral.Pls \<longleftrightarrow> OperationalEquality.eq Numeral.Pls k"
    4.56 +  unfolding eq_def Pls_def Bit_def bit.cases by auto
    4.57 +
    4.58 +lemma eq_Bit1_Pls:
    4.59 +  "\<not> OperationalEquality.eq (Numeral.Bit k bit.B1) Numeral.Pls"
    4.60 +  unfolding eq_def Pls_def Bit_def bit.cases by arith
    4.61 +
    4.62 +lemma eq_Bit0_Min:
    4.63 +  "\<not> OperationalEquality.eq (Numeral.Bit k bit.B0) Numeral.Min"
    4.64 +  unfolding eq_def Min_def Bit_def bit.cases by arith
    4.65 +
    4.66 +lemma eq_Bit1_Min:
    4.67 +  "OperationalEquality.eq (Numeral.Bit k bit.B1) Numeral.Min \<longleftrightarrow> OperationalEquality.eq Numeral.Min k"
    4.68 +  unfolding eq_def Min_def Bit_def bit.cases by auto
    4.69 +
    4.70 +lemma eq_Bit_Bit:
    4.71 +  "OperationalEquality.eq (Numeral.Bit k1 v1) (Numeral.Bit k2 v2) \<longleftrightarrow>
    4.72 +    OperationalEquality.eq v1 v2 \<and> OperationalEquality.eq k1 k2"
    4.73 +  unfolding eq_def Bit_def
    4.74 +  apply (cases v1)
    4.75 +  apply (cases v2)
    4.76 +  apply auto
    4.77 +  apply arith
    4.78 +  apply (cases v2)
    4.79 +  apply auto
    4.80 +  apply arith
    4.81 +  apply (cases v2)
    4.82 +  apply auto
    4.83 +done
    4.84 +
    4.85 +lemmas eq_numeral_code [code func] =
    4.86 +  eq_Pls_Pls eq_Pls_Min eq_Pls_Bit0 eq_Pls_Bit1
    4.87 +  eq_Min_Pls eq_Min_Min eq_Min_Bit0 eq_Min_Bit1
    4.88 +  eq_Bit0_Pls eq_Bit1_Pls eq_Bit0_Min eq_Bit1_Min eq_Bit_Bit
    4.89 +
    4.90 +lemma less_eq_Pls_Pls:
    4.91 +  "Numeral.Pls \<le> Numeral.Pls" ..
    4.92 +
    4.93 +lemma less_eq_Pls_Min:
    4.94 +  "\<not> (Numeral.Pls \<le> Numeral.Min)"
    4.95 +  unfolding Pls_def Min_def by auto
    4.96 +
    4.97 +lemma less_eq_Pls_Bit:
    4.98 +  "Numeral.Pls \<le> Numeral.Bit k v \<longleftrightarrow> Numeral.Pls \<le> k"
    4.99 +  unfolding Pls_def Bit_def by (cases v) auto
   4.100 +
   4.101 +lemma less_eq_Min_Pls:
   4.102 +  "Numeral.Min \<le> Numeral.Pls"
   4.103 +  unfolding Pls_def Min_def by auto
   4.104 +
   4.105 +lemma less_eq_Min_Min:
   4.106 +  "Numeral.Min \<le> Numeral.Min" ..
   4.107 +
   4.108 +lemma less_eq_Min_Bit0:
   4.109 +  "Numeral.Min \<le> Numeral.Bit k bit.B0 \<longleftrightarrow> Numeral.Min < k"
   4.110 +  unfolding Min_def Bit_def by auto
   4.111 +
   4.112 +lemma less_eq_Min_Bit1:
   4.113 +  "Numeral.Min \<le> Numeral.Bit k bit.B1 \<longleftrightarrow> Numeral.Min \<le> k"
   4.114 +  unfolding Min_def Bit_def by auto
   4.115 +
   4.116 +lemma less_eq_Bit0_Pls:
   4.117 +  "Numeral.Bit k bit.B0 \<le> Numeral.Pls \<longleftrightarrow> k \<le> Numeral.Pls"
   4.118 +  unfolding Pls_def Bit_def by simp
   4.119 +
   4.120 +lemma less_eq_Bit1_Pls:
   4.121 +  "Numeral.Bit k bit.B1 \<le> Numeral.Pls \<longleftrightarrow> k < Numeral.Pls"
   4.122 +  unfolding Pls_def Bit_def by auto
   4.123 +
   4.124 +lemma less_eq_Bit_Min:
   4.125 +  "Numeral.Bit k v \<le> Numeral.Min \<longleftrightarrow> k \<le> Numeral.Min"
   4.126 +  unfolding Min_def Bit_def by (cases v) auto
   4.127 +
   4.128 +lemma less_eq_Bit0_Bit:
   4.129 +  "Numeral.Bit k1 bit.B0 \<le> Numeral.Bit k2 v \<longleftrightarrow> k1 \<le> k2"
   4.130 +  unfolding Min_def Bit_def bit.cases by (cases v) auto
   4.131 +
   4.132 +lemma less_eq_Bit_Bit1:
   4.133 +  "Numeral.Bit k1 v \<le> Numeral.Bit k2 bit.B1 \<longleftrightarrow> k1 \<le> k2"
   4.134 +  unfolding Min_def Bit_def bit.cases by (cases v) auto
   4.135 +
   4.136 +lemmas less_eq_numeral_code [code func] = less_eq_Pls_Pls less_eq_Pls_Min less_eq_Pls_Bit
   4.137 +  less_eq_Min_Pls less_eq_Min_Min less_eq_Min_Bit0 less_eq_Min_Bit1
   4.138 +  less_eq_Bit0_Pls less_eq_Bit1_Pls less_eq_Bit_Min less_eq_Bit0_Bit less_eq_Bit_Bit1
   4.139 +
   4.140  end
     5.1 --- a/src/HOL/Presburger.thy	Tue Sep 19 15:21:55 2006 +0200
     5.2 +++ b/src/HOL/Presburger.thy	Tue Sep 19 15:21:58 2006 +0200
     5.3 @@ -1086,4 +1086,137 @@
     5.4  
     5.5  setup "Presburger.setup"
     5.6  
     5.7 +text {* Code generator setup *}
     5.8 +
     5.9 +text {*
    5.10 +  Presburger arithmetic is neccesary to prove some
    5.11 +  of the following code lemmas on integer numerals.
    5.12 +*}
    5.13 +
    5.14 +lemma eq_number_of [code func]:
    5.15 +  "OperationalEquality.eq ((number_of k)\<Colon>int) (number_of l) \<longleftrightarrow> OperationalEquality.eq k l"
    5.16 +  unfolding number_of_is_id ..
    5.17 +
    5.18 +lemma less_eq_number_of [code func]:
    5.19 +  "((number_of k)\<Colon>int) <= number_of l \<longleftrightarrow> k <= l"
    5.20 +  unfolding number_of_is_id ..
    5.21 +
    5.22 +lemma eq_Pls_Pls:
    5.23 +  "OperationalEquality.eq Numeral.Pls Numeral.Pls"
    5.24 +  unfolding eq_def ..
    5.25 +
    5.26 +lemma eq_Pls_Min:
    5.27 +  "\<not> OperationalEquality.eq Numeral.Pls Numeral.Min"
    5.28 +  unfolding eq_def Pls_def Min_def by auto
    5.29 +
    5.30 +lemma eq_Pls_Bit0:
    5.31 +  "OperationalEquality.eq Numeral.Pls (Numeral.Bit k bit.B0) \<longleftrightarrow> OperationalEquality.eq Numeral.Pls k"
    5.32 +  unfolding eq_def Pls_def Bit_def bit.cases by auto
    5.33 +
    5.34 +lemma eq_Pls_Bit1:
    5.35 +  "\<not> OperationalEquality.eq Numeral.Pls (Numeral.Bit k bit.B1)"
    5.36 +  unfolding eq_def Pls_def Bit_def bit.cases by arith
    5.37 +
    5.38 +lemma eq_Min_Pls:
    5.39 +  "\<not> OperationalEquality.eq Numeral.Min Numeral.Pls"
    5.40 +  unfolding eq_def Pls_def Min_def by auto
    5.41 +
    5.42 +lemma eq_Min_Min:
    5.43 +  "OperationalEquality.eq Numeral.Min Numeral.Min"
    5.44 +  unfolding eq_def ..
    5.45 +
    5.46 +lemma eq_Min_Bit0:
    5.47 +  "\<not> OperationalEquality.eq Numeral.Min (Numeral.Bit k bit.B0)"
    5.48 +  unfolding eq_def Min_def Bit_def bit.cases by arith
    5.49 +
    5.50 +lemma eq_Min_Bit1:
    5.51 +  "OperationalEquality.eq Numeral.Min (Numeral.Bit k bit.B1) \<longleftrightarrow> OperationalEquality.eq Numeral.Min k"
    5.52 +  unfolding eq_def Min_def Bit_def bit.cases by auto
    5.53 +
    5.54 +lemma eq_Bit0_Pls:
    5.55 +  "OperationalEquality.eq (Numeral.Bit k bit.B0) Numeral.Pls \<longleftrightarrow> OperationalEquality.eq Numeral.Pls k"
    5.56 +  unfolding eq_def Pls_def Bit_def bit.cases by auto
    5.57 +
    5.58 +lemma eq_Bit1_Pls:
    5.59 +  "\<not> OperationalEquality.eq (Numeral.Bit k bit.B1) Numeral.Pls"
    5.60 +  unfolding eq_def Pls_def Bit_def bit.cases by arith
    5.61 +
    5.62 +lemma eq_Bit0_Min:
    5.63 +  "\<not> OperationalEquality.eq (Numeral.Bit k bit.B0) Numeral.Min"
    5.64 +  unfolding eq_def Min_def Bit_def bit.cases by arith
    5.65 +
    5.66 +lemma eq_Bit1_Min:
    5.67 +  "OperationalEquality.eq (Numeral.Bit k bit.B1) Numeral.Min \<longleftrightarrow> OperationalEquality.eq Numeral.Min k"
    5.68 +  unfolding eq_def Min_def Bit_def bit.cases by auto
    5.69 +
    5.70 +lemma eq_Bit_Bit:
    5.71 +  "OperationalEquality.eq (Numeral.Bit k1 v1) (Numeral.Bit k2 v2) \<longleftrightarrow>
    5.72 +    OperationalEquality.eq v1 v2 \<and> OperationalEquality.eq k1 k2"
    5.73 +  unfolding eq_def Bit_def
    5.74 +  apply (cases v1)
    5.75 +  apply (cases v2)
    5.76 +  apply auto
    5.77 +  apply arith
    5.78 +  apply (cases v2)
    5.79 +  apply auto
    5.80 +  apply arith
    5.81 +  apply (cases v2)
    5.82 +  apply auto
    5.83 +done
    5.84 +
    5.85 +lemmas eq_numeral_code [code func] =
    5.86 +  eq_Pls_Pls eq_Pls_Min eq_Pls_Bit0 eq_Pls_Bit1
    5.87 +  eq_Min_Pls eq_Min_Min eq_Min_Bit0 eq_Min_Bit1
    5.88 +  eq_Bit0_Pls eq_Bit1_Pls eq_Bit0_Min eq_Bit1_Min eq_Bit_Bit
    5.89 +
    5.90 +lemma less_eq_Pls_Pls:
    5.91 +  "Numeral.Pls \<le> Numeral.Pls" ..
    5.92 +
    5.93 +lemma less_eq_Pls_Min:
    5.94 +  "\<not> (Numeral.Pls \<le> Numeral.Min)"
    5.95 +  unfolding Pls_def Min_def by auto
    5.96 +
    5.97 +lemma less_eq_Pls_Bit:
    5.98 +  "Numeral.Pls \<le> Numeral.Bit k v \<longleftrightarrow> Numeral.Pls \<le> k"
    5.99 +  unfolding Pls_def Bit_def by (cases v) auto
   5.100 +
   5.101 +lemma less_eq_Min_Pls:
   5.102 +  "Numeral.Min \<le> Numeral.Pls"
   5.103 +  unfolding Pls_def Min_def by auto
   5.104 +
   5.105 +lemma less_eq_Min_Min:
   5.106 +  "Numeral.Min \<le> Numeral.Min" ..
   5.107 +
   5.108 +lemma less_eq_Min_Bit0:
   5.109 +  "Numeral.Min \<le> Numeral.Bit k bit.B0 \<longleftrightarrow> Numeral.Min < k"
   5.110 +  unfolding Min_def Bit_def by auto
   5.111 +
   5.112 +lemma less_eq_Min_Bit1:
   5.113 +  "Numeral.Min \<le> Numeral.Bit k bit.B1 \<longleftrightarrow> Numeral.Min \<le> k"
   5.114 +  unfolding Min_def Bit_def by auto
   5.115 +
   5.116 +lemma less_eq_Bit0_Pls:
   5.117 +  "Numeral.Bit k bit.B0 \<le> Numeral.Pls \<longleftrightarrow> k \<le> Numeral.Pls"
   5.118 +  unfolding Pls_def Bit_def by simp
   5.119 +
   5.120 +lemma less_eq_Bit1_Pls:
   5.121 +  "Numeral.Bit k bit.B1 \<le> Numeral.Pls \<longleftrightarrow> k < Numeral.Pls"
   5.122 +  unfolding Pls_def Bit_def by auto
   5.123 +
   5.124 +lemma less_eq_Bit_Min:
   5.125 +  "Numeral.Bit k v \<le> Numeral.Min \<longleftrightarrow> k \<le> Numeral.Min"
   5.126 +  unfolding Min_def Bit_def by (cases v) auto
   5.127 +
   5.128 +lemma less_eq_Bit0_Bit:
   5.129 +  "Numeral.Bit k1 bit.B0 \<le> Numeral.Bit k2 v \<longleftrightarrow> k1 \<le> k2"
   5.130 +  unfolding Min_def Bit_def bit.cases by (cases v) auto
   5.131 +
   5.132 +lemma less_eq_Bit_Bit1:
   5.133 +  "Numeral.Bit k1 v \<le> Numeral.Bit k2 bit.B1 \<longleftrightarrow> k1 \<le> k2"
   5.134 +  unfolding Min_def Bit_def bit.cases by (cases v) auto
   5.135 +
   5.136 +lemmas less_eq_numeral_code [code func] = less_eq_Pls_Pls less_eq_Pls_Min less_eq_Pls_Bit
   5.137 +  less_eq_Min_Pls less_eq_Min_Min less_eq_Min_Bit0 less_eq_Min_Bit1
   5.138 +  less_eq_Bit0_Pls less_eq_Bit1_Pls less_eq_Bit_Min less_eq_Bit0_Bit less_eq_Bit_Bit1
   5.139 +
   5.140  end
     6.1 --- a/src/HOL/ex/NormalForm.thy	Tue Sep 19 15:21:55 2006 +0200
     6.2 +++ b/src/HOL/ex/NormalForm.thy	Tue Sep 19 15:21:58 2006 +0200
     6.3 @@ -10,11 +10,10 @@
     6.4  
     6.5  lemma "p \<longrightarrow> True" by normalization
     6.6  declare disj_assoc [code func]
     6.7 -normal_form  "(P | Q) | R"
     6.8 -
     6.9 +lemma "((P | Q) | R) = (P | (Q | R))" by normalization
    6.10  lemma "0 + (n::nat) = n" by normalization
    6.11 -lemma "0 + Suc(n) = Suc n" by normalization
    6.12 -lemma "Suc(n) + Suc m = n + Suc(Suc m)" by normalization
    6.13 +lemma "0 + Suc n = Suc n" by normalization
    6.14 +lemma "Suc n + Suc m = n + Suc (Suc m)" by normalization
    6.15  lemma "~((0::nat) < (0::nat))" by normalization
    6.16  
    6.17  
    6.18 @@ -93,14 +92,22 @@
    6.19  normal_form "%x. case x of None \<Rightarrow> False | Some y \<Rightarrow> True"
    6.20  normal_form "map (%x. case x of None \<Rightarrow> False | Some y \<Rightarrow> True) [None, Some ()]"
    6.21  
    6.22 -normal_form "last[a,b,c]"
    6.23 -normal_form "last([a,b,c]@xs)"
    6.24 +normal_form "last [a, b, c]"
    6.25 +normal_form "last ([a, b, c] @ xs)"
    6.26  
    6.27  normal_form "min 0 x"
    6.28  normal_form "min 0 (x::nat)"
    6.29  
    6.30 -text {*
    6.31 -  Numerals still take their time\<dots>
    6.32 -*}
    6.33 +normal_form "(2::int) + 3 - 1 + (- k) * 2"
    6.34 +normal_form "(4::int) * 2"
    6.35 +normal_form "(-4::int) * 2"
    6.36 +normal_form "abs ((-4::int) + 2 * 1)"
    6.37 +normal_form "(2::int) + 3"
    6.38 +normal_form "(2::int) + 3 * (- 4) * (- 1)"
    6.39 +normal_form "(2::int) + 3 * (- 4) * 1 + 0"
    6.40 +normal_form "(2::int) < 3"
    6.41 +normal_form "(2::int) <= 3"
    6.42 +normal_form "abs ((-4::int) + 2 * 1)"
    6.43 +normal_form "4 - 42 * abs (3 + (-7\<Colon>int))"
    6.44  
    6.45  end
     7.1 --- a/src/HOL/ex/reflection.ML	Tue Sep 19 15:21:55 2006 +0200
     7.2 +++ b/src/HOL/ex/reflection.ML	Tue Sep 19 15:21:58 2006 +0200
     7.3 @@ -279,7 +279,7 @@
     7.4  fun genreflect ctxt corr_thm raw_eqs t =
     7.5      let val th = FWD trans [genreif ctxt raw_eqs t, corr_thm RS sym]
     7.6          val ft = (snd o Thm.dest_comb o snd o Thm.dest_comb o snd o Thm.dest_comb o cprop_of) th
     7.7 -        val rth = normalization_conv ft
     7.8 +        val rth = NBE.normalization_conv ft
     7.9      in simplify (HOL_basic_ss addsimps raw_eqs addsimps [nth_Cons_0, nth_Cons_Suc])
    7.10                  (simplify (HOL_basic_ss addsimps [rth]) th)
    7.11      end