cleaned up code generator setup for int
authorhaftmann
Thu Apr 26 13:33:05 2007 +0200 (2007-04-26)
changeset 22801caffcb450ef4
parent 22800 eaf5e7ef35d9
child 22802 92026479179e
cleaned up code generator setup for int
src/HOL/Integ/IntArith.thy
src/HOL/Integ/IntDef.thy
src/HOL/Integ/Numeral.thy
src/HOL/Integ/Presburger.thy
src/HOL/Presburger.thy
     1.1 --- a/src/HOL/Integ/IntArith.thy	Thu Apr 26 13:33:04 2007 +0200
     1.2 +++ b/src/HOL/Integ/IntArith.thy	Thu Apr 26 13:33:05 2007 +0200
     1.3 @@ -14,13 +14,6 @@
     1.4  declare numeral_0_eq_0 [simp]
     1.5  
     1.6  
     1.7 -subsection{*Instantiating Binary Arithmetic for the Integers*}
     1.8 -
     1.9 -instance int :: number_ring
    1.10 -  int_number_of_def: "number_of w \<equiv> of_int w"
    1.11 -  by intro_classes (simp only: int_number_of_def)
    1.12 -
    1.13 -
    1.14  subsection{*Inequality Reasoning for the Arithmetic Simproc*}
    1.15  
    1.16  lemma add_numeral_0: "Numeral0 + a = (a::'a::number_ring)"
    1.17 @@ -191,8 +184,7 @@
    1.18  
    1.19  text{*This simplifies expressions of the form @{term "int n = z"} where
    1.20        z is an integer literal.*}
    1.21 -lemmas int_eq_iff_number_of = int_eq_iff [of _ "number_of v", standard]
    1.22 -declare int_eq_iff_number_of [simp]
    1.23 +lemmas int_eq_iff_number_of [simp] = int_eq_iff [of _ "number_of v", standard]
    1.24  
    1.25  
    1.26  lemma split_nat [arith_split]:
    1.27 @@ -217,7 +209,7 @@
    1.28  by (induct m n rule: diff_induct, simp_all)
    1.29  
    1.30  lemma nat_mult_distrib: "(0::int) \<le> z ==> nat (z*z') = nat z * nat z'"
    1.31 -apply (case_tac "0 \<le> z'")
    1.32 +apply (cases "0 \<le> z'")
    1.33  apply (rule inj_int [THEN injD])
    1.34  apply (simp add: int_mult zero_le_mult_iff)
    1.35  apply (simp add: mult_le_0_iff)
    1.36 @@ -229,7 +221,7 @@
    1.37  done
    1.38  
    1.39  lemma nat_abs_mult_distrib: "nat (abs (w * z)) = nat (abs w) * nat (abs z)"
    1.40 -apply (case_tac "z=0 | w=0")
    1.41 +apply (cases "z=0 | w=0")
    1.42  apply (auto simp add: abs_if nat_mult_distrib [symmetric] 
    1.43                        nat_mult_distrib_neg [symmetric] mult_less_0_iff)
    1.44  done
    1.45 @@ -375,7 +367,7 @@
    1.46  by arith
    1.47  
    1.48  lemma abs_zmult_eq_1: "(\<bar>m * n\<bar> = 1) ==> \<bar>m\<bar> = (1::int)"
    1.49 -apply (case_tac "\<bar>n\<bar>=1") 
    1.50 +apply (cases "\<bar>n\<bar>=1") 
    1.51  apply (simp add: abs_mult) 
    1.52  apply (rule ccontr) 
    1.53  apply (auto simp add: linorder_neq_iff abs_mult) 
    1.54 @@ -402,110 +394,12 @@
    1.55  done
    1.56  
    1.57  
    1.58 -subsection {* code generator setup *}
    1.59 -
    1.60 -code_modulename SML
    1.61 -  Numeral Integer
    1.62 -
    1.63 -code_modulename OCaml
    1.64 -  Numeral Integer
    1.65 -
    1.66 -lemma Numeral_Pls_refl [code func]:
    1.67 -  "Numeral.Pls = Numeral.Pls" ..
    1.68 -
    1.69 -lemma Numeral_Min_refl [code func]:
    1.70 -  "Numeral.Min = Numeral.Min" ..
    1.71 -
    1.72 -lemma zero_int_refl [code func]:
    1.73 -  "(0\<Colon>int) = 0" ..
    1.74 -
    1.75 -lemma one_int_refl [code func]:
    1.76 -  "(1\<Colon>int) = 1" ..
    1.77 -
    1.78 -lemma number_of_int_refl [code func]:
    1.79 -  "(number_of \<Colon> int \<Rightarrow> int) = number_of" ..
    1.80 -
    1.81 -lemma number_of_is_id:
    1.82 -  "number_of (k::int) = k"
    1.83 -  unfolding int_number_of_def by simp
    1.84 -
    1.85 -lemma zero_is_num_zero [code inline, symmetric, normal post]:
    1.86 -  "(0::int) = number_of Numeral.Pls" 
    1.87 -  by simp
    1.88 -
    1.89 -lemma one_is_num_one [code inline, symmetric, normal post]:
    1.90 -  "(1::int) = number_of  (Numeral.Pls BIT bit.B1)" 
    1.91 -  by simp 
    1.92 -
    1.93 -lemmas int_code_rewrites =
    1.94 -  arith_simps(5-27)
    1.95 -  arith_extra_simps(1-5) [where 'a = int]
    1.96 -
    1.97 -declare int_code_rewrites [code func]
    1.98 -
    1.99 -code_type bit
   1.100 -  (SML "bool")
   1.101 -  (OCaml "bool")
   1.102 -  (Haskell "Bool")
   1.103 -code_const "Numeral.bit.B0" and "Numeral.bit.B1"
   1.104 -  (SML "false" and "true")
   1.105 -  (OCaml "false" and "true")
   1.106 -  (Haskell "False" and "True")
   1.107 +subsection {* Legavy ML bindings *}
   1.108  
   1.109 -code_const "number_of \<Colon> int \<Rightarrow> int"
   1.110 -  and "Numeral.Pls" and "Numeral.Min" and "Numeral.Bit"
   1.111 -  and "Numeral.succ" and "Numeral.pred"
   1.112 -  (SML "_"
   1.113 -     and "0/ :/ IntInf.int"
   1.114 -     and "~1/ :/ IntInf.int"
   1.115 -     and "!(_; _; raise Fail \"BIT\")"
   1.116 -     and "IntInf.+/ (_,/ 1)"
   1.117 -     and "IntInf.-/ (_,/ 1))")
   1.118 -  (OCaml "_"
   1.119 -     and "Big'_int.big'_int'_of'_int/ 0"
   1.120 -     and "Big'_int.big'_int'_of'_int/ (-1)"
   1.121 -     and "!(_; _; failwith \"BIT\")"
   1.122 -     and "Big'_int.succ'_big'_int"
   1.123 -     and "Big'_int.pred'_big'_int")
   1.124 -  (Haskell "_"
   1.125 -     and "0"
   1.126 -     and "!(-1)"
   1.127 -     and "error/ \"BIT\""
   1.128 -     and "(+)/ 1"
   1.129 -     and "(-)/ _/ 1")
   1.130 -
   1.131 -setup {*
   1.132 -  CodegenPackage.add_appconst ("Numeral.Bit", CodegenPackage.appgen_numeral (try HOLogic.dest_numeral))
   1.133 -*}
   1.134 -
   1.135 -
   1.136 -subsection {* legacy ML bindings *}
   1.137 -
   1.138 -ML
   1.139 -{*
   1.140 -val zle_diff1_eq = thm "zle_diff1_eq";
   1.141 -val zle_add1_eq_le = thm "zle_add1_eq_le";
   1.142 -val nonneg_eq_int = thm "nonneg_eq_int";
   1.143 -val abs_minus_one = thm "abs_minus_one";
   1.144 -val of_int_number_of_eq = thm"of_int_number_of_eq";
   1.145 -val nat_eq_iff = thm "nat_eq_iff";
   1.146 -val nat_eq_iff2 = thm "nat_eq_iff2";
   1.147 -val nat_less_iff = thm "nat_less_iff";
   1.148 -val int_eq_iff = thm "int_eq_iff";
   1.149 -val nat_0 = thm "nat_0";
   1.150 -val nat_1 = thm "nat_1";
   1.151 -val nat_2 = thm "nat_2";
   1.152 -val nat_less_eq_zless = thm "nat_less_eq_zless";
   1.153 -val nat_le_eq_zle = thm "nat_le_eq_zle";
   1.154 -
   1.155 -val nat_intermed_int_val = thm "nat_intermed_int_val";
   1.156 -val pos_zmult_eq_1_iff = thm "pos_zmult_eq_1_iff";
   1.157 -val zmult_eq_1_iff = thm "zmult_eq_1_iff";
   1.158 -val nat_add_distrib = thm "nat_add_distrib";
   1.159 -val nat_diff_distrib = thm "nat_diff_distrib";
   1.160 -val nat_mult_distrib = thm "nat_mult_distrib";
   1.161 -val nat_mult_distrib_neg = thm "nat_mult_distrib_neg";
   1.162 -val nat_abs_mult_distrib = thm "nat_abs_mult_distrib";
   1.163 +ML {*
   1.164 +val of_int_number_of_eq = @{thm of_int_number_of_eq};
   1.165 +val nat_0 = @{thm nat_0};
   1.166 +val nat_1 = @{thm nat_1};
   1.167  *}
   1.168  
   1.169  end
     2.1 --- a/src/HOL/Integ/IntDef.thy	Thu Apr 26 13:33:04 2007 +0200
     2.2 +++ b/src/HOL/Integ/IntDef.thy	Thu Apr 26 13:33:05 2007 +0200
     2.3 @@ -11,47 +11,50 @@
     2.4  imports Equiv_Relations Nat
     2.5  begin
     2.6  
     2.7 -constdefs
     2.8 -  intrel :: "((nat * nat) * (nat * nat)) set"
     2.9 -    --{*the equivalence relation underlying the integers*}
    2.10 -    "intrel == {((x,y),(u,v)) | x y u v. x+v = u+y}"
    2.11 +text {* the equivalence relation underlying the integers *}
    2.12 +
    2.13 +definition
    2.14 +  intrel :: "((nat \<times> nat) \<times> (nat \<times> nat)) set"
    2.15 +where
    2.16 +  "intrel = {((x, y), (u, v)) | x y u v. x + v = u +y }"
    2.17  
    2.18  typedef (Integ)
    2.19    int = "UNIV//intrel"
    2.20 -    by (auto simp add: quotient_def)
    2.21 -
    2.22 -instance int :: "{ord, zero, one, plus, times, minus}" ..
    2.23 +  by (auto simp add: quotient_def)
    2.24  
    2.25 -constdefs
    2.26 -  int :: "nat => int"
    2.27 -  "int m == Abs_Integ(intrel `` {(m,0)})"
    2.28 +definition
    2.29 +  int :: "nat \<Rightarrow> int"
    2.30 +where
    2.31 +  [code nofunc]: "int m = Abs_Integ (intrel `` {(m, 0)})"
    2.32  
    2.33 -
    2.34 -defs (overloaded)
    2.35 +instance int :: zero
    2.36 +  Zero_int_def: "0 \<equiv> int 0" ..
    2.37  
    2.38 -  Zero_int_def:  "0 == int 0"
    2.39 -  One_int_def:   "1 == int 1"
    2.40 +instance int :: one
    2.41 +  One_int_def: "1 \<equiv> int 1" ..
    2.42  
    2.43 -  minus_int_def:
    2.44 -    "- z == Abs_Integ (\<Union>(x,y) \<in> Rep_Integ z. intrel``{(y,x)})"
    2.45 +instance int :: plus
    2.46 +  add_int_def: "z + w \<equiv> Abs_Integ
    2.47 +    (\<Union>(x, y) \<in> Rep_Integ z. \<Union>(u, v) \<in> Rep_Integ w.
    2.48 +      intrel `` {(x + u, y + v)})" ..
    2.49  
    2.50 -  add_int_def:
    2.51 -   "z + w ==
    2.52 -       Abs_Integ (\<Union>(x,y) \<in> Rep_Integ z. \<Union>(u,v) \<in> Rep_Integ w.
    2.53 -		 intrel``{(x+u, y+v)})"
    2.54 -
    2.55 -  diff_int_def:  "z - (w::int) == z + (-w)"
    2.56 +instance int :: minus
    2.57 +  minus_int_def:
    2.58 +    "- z \<equiv> Abs_Integ (\<Union>(x, y) \<in> Rep_Integ z. intrel `` {(y, x)})"
    2.59 +  diff_int_def:  "z - w \<equiv> z + (-w)" ..
    2.60  
    2.61 -  mult_int_def:
    2.62 -   "z * w ==
    2.63 -       Abs_Integ (\<Union>(x,y) \<in> Rep_Integ z. \<Union>(u,v) \<in> Rep_Integ w.
    2.64 -		  intrel``{(x*u + y*v, x*v + y*u)})"
    2.65 +instance int :: times
    2.66 +  mult_int_def: "z * w \<equiv>  Abs_Integ
    2.67 +    (\<Union>(x, y) \<in> Rep_Integ z. \<Union>(u,v ) \<in> Rep_Integ w.
    2.68 +      intrel `` {(x*u + y*v, x*v + y*u)})" ..
    2.69  
    2.70 +instance int :: ord
    2.71    le_int_def:
    2.72 -   "z \<le> (w::int) == 
    2.73 -    \<exists>x y u v. x+v \<le> u+y & (x,y) \<in> Rep_Integ z & (u,v) \<in> Rep_Integ w"
    2.74 +   "z \<le> w \<equiv> \<exists>x y u v. x+v \<le> u+y \<and> (x, y) \<in> Rep_Integ z \<and> (u, v) \<in> Rep_Integ w"
    2.75 +  less_int_def: "z < w \<equiv> z \<le> w \<and> z \<noteq> w" ..
    2.76  
    2.77 -  less_int_def: "(z < (w::int)) == (z \<le> w & z \<noteq> w)"
    2.78 +lemmas [code nofunc] = Zero_int_def One_int_def add_int_def
    2.79 +  minus_int_def mult_int_def le_int_def less_int_def
    2.80  
    2.81  
    2.82  subsection{*Construction of the Integers*}
    2.83 @@ -66,10 +69,7 @@
    2.84  
    2.85  text{*Reduces equality of equivalence classes to the @{term intrel} relation:
    2.86    @{term "(intrel `` {x} = intrel `` {y}) = ((x,y) \<in> intrel)"} *}
    2.87 -lemmas equiv_intrel_iff = eq_equiv_class_iff [OF equiv_intrel UNIV_I UNIV_I]
    2.88 -
    2.89 -declare equiv_intrel_iff [simp]
    2.90 -
    2.91 +lemmas equiv_intrel_iff [simp] = eq_equiv_class_iff [OF equiv_intrel UNIV_I UNIV_I]
    2.92  
    2.93  text{*All equivalence classes belong to set of representatives*}
    2.94  lemma [simp]: "intrel``{(x,y)} \<in> Integ"
    2.95 @@ -154,9 +154,6 @@
    2.96  lemma zadd_int_left: "(int m) + (int n + z) = int (m + n) + z"
    2.97    by (simp add: zadd_int zadd_assoc [symmetric])
    2.98  
    2.99 -lemma int_Suc: "int (Suc m) = 1 + (int m)"
   2.100 -  by (simp add: One_int_def zadd_int)
   2.101 -
   2.102  (*also for the instance declaration int :: comm_monoid_add*)
   2.103  lemma zadd_0: "(0::int) + z = z"
   2.104  apply (simp add: Zero_int_def int_def)
   2.105 @@ -268,14 +265,12 @@
   2.106      (assumption |
   2.107        rule zle_refl zle_trans zle_anti_sym less_int_def [THEN meta_eq_to_obj_eq])+
   2.108  
   2.109 -(* Axiom 'linorder_linear' of class 'linorder': *)
   2.110 -lemma zle_linear: "(z::int) \<le> w | w \<le> z"
   2.111 +lemma zle_linear: "(z::int) \<le> w \<or> w \<le> z"
   2.112  by (cases z, cases w) (simp add: le linorder_linear)
   2.113  
   2.114  instance int :: linorder
   2.115    by intro_classes (rule zle_linear)
   2.116  
   2.117 -
   2.118  lemmas zless_linear = linorder_less_linear [where 'a = int]
   2.119  
   2.120  
   2.121 @@ -315,6 +310,9 @@
   2.122  lemma int_Suc0_eq_1: "int (Suc 0) = 1"
   2.123  by (simp add: One_int_def One_nat_def)
   2.124  
   2.125 +lemma int_Suc: "int (Suc m) = 1 + (int m)"
   2.126 +by (simp add: One_int_def zadd_int)
   2.127 +
   2.128  
   2.129  subsection{*Monotonicity results*}
   2.130  
   2.131 @@ -355,7 +353,7 @@
   2.132  done
   2.133  
   2.134  instance int :: minus
   2.135 -  zabs_def:  "abs(i::int) == if i < 0 then -i else i" ..
   2.136 +  zabs_def: "\<bar>i\<Colon>int\<bar> \<equiv> if i < 0 then - i else i" ..
   2.137  
   2.138  instance int :: distrib_lattice
   2.139    "inf \<equiv> min"
   2.140 @@ -379,9 +377,10 @@
   2.141  
   2.142  subsection{*Magnitide of an Integer, as a Natural Number: @{term nat}*}
   2.143  
   2.144 -constdefs
   2.145 -   nat  :: "int => nat"
   2.146 -    "nat z == contents (\<Union>(x,y) \<in> Rep_Integ z. { x-y })"
   2.147 +definition
   2.148 +  nat :: "int \<Rightarrow> nat"
   2.149 +where
   2.150 +  [code nofunc]: "nat z = contents (\<Union>(x, y) \<in> Rep_Integ z. {x-y})"
   2.151  
   2.152  lemma nat: "nat (Abs_Integ (intrel``{(x,y)})) = x-y"
   2.153  proof -
   2.154 @@ -514,16 +513,14 @@
   2.155  by (force dest: order_less_le_trans simp add: abs_if linorder_not_less)
   2.156  
   2.157  
   2.158 -
   2.159 -subsection{*The Constants @{term neg} and @{term iszero}*}
   2.160 +subsection {* Constants @{term neg} and @{term iszero} *}
   2.161  
   2.162  definition
   2.163    neg  :: "'a\<Colon>ordered_idom \<Rightarrow> bool"
   2.164  where
   2.165 -  "neg Z \<longleftrightarrow> Z < 0"
   2.166 +  [code inline]: "neg Z \<longleftrightarrow> Z < 0"
   2.167  
   2.168 -definition
   2.169 -  (*For simplifying equalities*)
   2.170 +definition (*for simplifying equalities*)
   2.171    iszero :: "'a\<Colon>comm_semiring_1_cancel \<Rightarrow> bool"
   2.172  where
   2.173    "iszero z \<longleftrightarrow> z = 0"
   2.174 @@ -658,20 +655,18 @@
   2.175  done
   2.176  
   2.177  text{*Special cases where either operand is zero*}
   2.178 -lemmas of_int_0_le_iff = of_int_le_iff [of 0, simplified]
   2.179 -lemmas of_int_le_0_iff = of_int_le_iff [of _ 0, simplified]
   2.180 -declare of_int_0_le_iff [simp]
   2.181 -declare of_int_le_0_iff [simp]
   2.182 +lemmas of_int_0_le_iff [simp] = of_int_le_iff [of 0, simplified]
   2.183 +lemmas of_int_le_0_iff [simp] = of_int_le_iff [of _ 0, simplified]
   2.184 +
   2.185  
   2.186  lemma of_int_less_iff [simp]:
   2.187       "(of_int w < (of_int z::'a::ordered_idom)) = (w < z)"
   2.188  by (simp add: linorder_not_le [symmetric])
   2.189  
   2.190  text{*Special cases where either operand is zero*}
   2.191 -lemmas of_int_0_less_iff = of_int_less_iff [of 0, simplified]
   2.192 -lemmas of_int_less_0_iff = of_int_less_iff [of _ 0, simplified]
   2.193 -declare of_int_0_less_iff [simp]
   2.194 -declare of_int_less_0_iff [simp]
   2.195 +lemmas of_int_0_less_iff [simp] = of_int_less_iff [of 0, simplified]
   2.196 +lemmas of_int_less_0_iff [simp] = of_int_less_iff [of _ 0, simplified]
   2.197 +
   2.198  
   2.199  text{*The ordering on the @{text ring_1} is necessary.
   2.200   See @{text of_nat_eq_iff} above.*}
   2.201 @@ -680,10 +675,8 @@
   2.202  by (simp add: order_eq_iff)
   2.203  
   2.204  text{*Special cases where either operand is zero*}
   2.205 -lemmas of_int_0_eq_iff = of_int_eq_iff [of 0, simplified]
   2.206 -lemmas of_int_eq_0_iff = of_int_eq_iff [of _ 0, simplified]
   2.207 -declare of_int_0_eq_iff [simp]
   2.208 -declare of_int_eq_0_iff [simp]
   2.209 +lemmas of_int_0_eq_iff [simp] = of_int_eq_iff [of 0, simplified]
   2.210 +lemmas of_int_eq_0_iff [simp] = of_int_eq_iff [of _ 0, simplified]
   2.211  
   2.212  lemma of_int_eq_id [simp]: "of_int = (id :: int => int)"
   2.213  proof
   2.214 @@ -762,7 +755,7 @@
   2.215  
   2.216  
   2.217  (* int (Suc n) = 1 + int n *)
   2.218 -declare int_Suc [simp]
   2.219 +
   2.220  
   2.221  
   2.222  subsection{*More Properties of @{term setsum} and  @{term setprod}*}
   2.223 @@ -813,6 +806,8 @@
   2.224    by (rule setprod_zero_eq, auto)
   2.225  
   2.226  
   2.227 +subsection {* Further properties *}
   2.228 +
   2.229  text{*Now we replace the case analysis rule by a more conventional one:
   2.230  whether an integer is negative or not.*}
   2.231  
   2.232 @@ -833,7 +828,7 @@
   2.233  
   2.234  theorem int_cases [cases type: int, case_names nonneg neg]:
   2.235       "[|!! n. z = int n ==> P;  !! n. z =  - (int (Suc n)) ==> P |] ==> P"
   2.236 -apply (case_tac "z < 0", blast dest!: negD)
   2.237 +apply (cases "z < 0", blast dest!: negD)
   2.238  apply (simp add: linorder_not_less)
   2.239  apply (blast dest: nat_0_le [THEN sym])
   2.240  done
   2.241 @@ -857,248 +852,33 @@
   2.242  
   2.243  lemmas zless_le = less_int_def [THEN meta_eq_to_obj_eq]
   2.244  
   2.245 -subsection {* Configuration of the code generator *}
   2.246 -
   2.247 -(*FIXME: the IntInf.fromInt below hides a dependence on fixed-precision ints!*)
   2.248 -
   2.249 -types_code
   2.250 -  "int" ("int")
   2.251 -attach (term_of) {*
   2.252 -val term_of_int = HOLogic.mk_number HOLogic.intT o IntInf.fromInt;
   2.253 -*}
   2.254 -attach (test) {*
   2.255 -fun gen_int i = one_of [~1, 1] * random_range 0 i;
   2.256 -*}
   2.257 -
   2.258 -definition
   2.259 -  int_aux :: "int \<Rightarrow> nat \<Rightarrow> int" where
   2.260 -  "int_aux i n = (i + int n)"
   2.261 -
   2.262 -definition
   2.263 -  nat_aux :: "nat \<Rightarrow> int \<Rightarrow> nat" where
   2.264 -  "nat_aux n i = (n + nat i)"
   2.265 -
   2.266 -lemma [code]:
   2.267 -  "int_aux i 0 = i"
   2.268 -  "int_aux i (Suc n) = int_aux (i + 1) n" -- {* tail recursive *}
   2.269 -  "int n = int_aux 0 n"
   2.270 -  by (simp add: int_aux_def)+
   2.271 -
   2.272 -lemma [code]: "nat_aux n i = (if i <= 0 then n else nat_aux (Suc n) (i - 1))"
   2.273 -  -- {* tail recursive *}
   2.274 -  by (auto simp add: nat_aux_def nat_eq_iff linorder_not_le order_less_imp_le
   2.275 -    dest: zless_imp_add1_zle)
   2.276 -lemma [code]: "nat i = nat_aux 0 i"
   2.277 -  by (simp add: nat_aux_def)
   2.278 -
   2.279 -lemma [code inline]:
   2.280 -  "neg k \<longleftrightarrow> k < 0"
   2.281 -  unfolding neg_def ..
   2.282 -
   2.283 -lemma [code func]:
   2.284 -  "\<bar>k\<Colon>int\<bar> = (if k < 0 then - k else k)"
   2.285 -  unfolding zabs_def ..
   2.286 -
   2.287 -consts_code
   2.288 -  "HOL.zero" :: "int"                ("0")
   2.289 -  "HOL.one" :: "int"                 ("1")
   2.290 -  "HOL.uminus" :: "int => int"       ("~")
   2.291 -  "HOL.plus" :: "int => int => int"  ("(_ +/ _)")
   2.292 -  "HOL.times" :: "int => int => int" ("(_ */ _)")
   2.293 -  "Orderings.less" :: "int => int => bool" ("(_ </ _)")
   2.294 -  "Orderings.less_eq" :: "int => int => bool" ("(_ <=/ _)")
   2.295 -  "neg"                              ("(_ < 0)")
   2.296 +lemmas [simp] = int_Suc
   2.297  
   2.298 -instance int :: eq ..
   2.299  
   2.300 -code_type int
   2.301 -  (SML "IntInf.int")
   2.302 -  (OCaml "Big'_int.big'_int")
   2.303 -  (Haskell "Integer")
   2.304 -
   2.305 -code_instance int :: eq
   2.306 -  (Haskell -)
   2.307 -
   2.308 -code_const "op = \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
   2.309 -  (SML "!((_ : IntInf.int) = _)")
   2.310 -  (OCaml "Big'_int.eq'_big'_int")
   2.311 -  (Haskell infixl 4 "==")
   2.312 -
   2.313 -code_const "op \<le> \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
   2.314 -  (SML "IntInf.<= (_, _)")
   2.315 -  (OCaml "Big'_int.le'_big'_int")
   2.316 -  (Haskell infix 4 "<=")
   2.317 -
   2.318 -code_const "op < \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
   2.319 -  (SML "IntInf.< (_, _)")
   2.320 -  (OCaml "Big'_int.lt'_big'_int")
   2.321 -  (Haskell infix 4 "<")
   2.322 -
   2.323 -code_const "op + \<Colon> int \<Rightarrow> int \<Rightarrow> int"
   2.324 -  (SML "IntInf.+ (_, _)")
   2.325 -  (OCaml "Big'_int.add'_big'_int")
   2.326 -  (Haskell infixl 6 "+")
   2.327 -
   2.328 -code_const "op - \<Colon> int \<Rightarrow> int \<Rightarrow> int"
   2.329 -  (SML "IntInf.- (_, _)")
   2.330 -  (OCaml "Big'_int.sub'_big'_int")
   2.331 -  (Haskell infixl 6 "-")
   2.332 -
   2.333 -code_const "op * \<Colon> int \<Rightarrow> int \<Rightarrow> int"
   2.334 -  (SML "IntInf.* (_, _)")
   2.335 -  (OCaml "Big'_int.mult'_big'_int")
   2.336 -  (Haskell infixl 7 "*")
   2.337 -
   2.338 -code_const "uminus \<Colon> int \<Rightarrow> int"
   2.339 -  (SML "IntInf.~")
   2.340 -  (OCaml "Big'_int.minus'_big'_int")
   2.341 -  (Haskell "negate")
   2.342 -
   2.343 -code_reserved SML IntInf
   2.344 -code_reserved OCaml Big_int
   2.345 -
   2.346 -code_modulename SML
   2.347 -  IntDef Integer
   2.348 -
   2.349 -code_modulename Haskell
   2.350 -  IntDef Integer
   2.351 +subsection {* Legacy ML bindings *}
   2.352  
   2.353  ML {*
   2.354 -fun number_of_codegen thy defs gr dep module b (Const ("Numeral.number_of", Type ("fun", [_, T])) $ t) =
   2.355 -      if T = HOLogic.intT then
   2.356 -        (SOME (fst (Codegen.invoke_tycodegen thy defs dep module false (gr, T)),
   2.357 -          (Pretty.str o IntInf.toString o HOLogic.dest_numeral) t) handle TERM _ => NONE)
   2.358 -      else if T = HOLogic.natT then
   2.359 -        SOME (Codegen.invoke_codegen thy defs dep module b (gr,
   2.360 -          Const ("IntDef.nat", HOLogic.intT --> HOLogic.natT) $
   2.361 -            (Const ("Numeral.number_of", HOLogic.intT --> HOLogic.intT) $ t)))
   2.362 -      else NONE
   2.363 -  | number_of_codegen _ _ _ _ _ _ _ = NONE;
   2.364 -*}
   2.365 -
   2.366 -setup {*
   2.367 -  Codegen.add_codegen "number_of_codegen" number_of_codegen
   2.368 +val of_nat_0 = @{thm of_nat_0};
   2.369 +val of_nat_1 = @{thm of_nat_1};
   2.370 +val of_nat_Suc = @{thm of_nat_Suc};
   2.371 +val of_nat_add = @{thm of_nat_add};
   2.372 +val of_nat_mult = @{thm of_nat_mult};
   2.373 +val of_int_0 = @{thm of_int_0};
   2.374 +val of_int_1 = @{thm of_int_1};
   2.375 +val of_int_add = @{thm of_int_add};
   2.376 +val of_int_mult = @{thm of_int_mult};
   2.377 +val int_eq_of_nat = @{thm int_eq_of_nat};
   2.378 +val zle_int = @{thm zle_int};
   2.379 +val int_int_eq = @{thm int_int_eq};
   2.380 +val diff_int_def = @{thm diff_int_def};
   2.381 +val zadd_ac = @{thms zadd_ac};
   2.382 +val zless_int = @{thm zless_int};
   2.383 +val zadd_int = @{thm zadd_int};
   2.384 +val zmult_int = @{thm zmult_int};
   2.385 +val nat_0_le = @{thm nat_0_le};
   2.386 +val int_0 = @{thm int_0};
   2.387 +val int_1 = @{thm int_1};
   2.388 +val abs_split = @{thm abs_split};
   2.389  *}
   2.390  
   2.391 -quickcheck_params [default_type = int]
   2.392 -
   2.393 -
   2.394 -(*Legacy ML bindings, but no longer the structure Int.*)
   2.395 -ML
   2.396 -{*
   2.397 -val zabs_def = thm "zabs_def"
   2.398 -
   2.399 -val int_0 = thm "int_0";
   2.400 -val int_1 = thm "int_1";
   2.401 -val int_Suc0_eq_1 = thm "int_Suc0_eq_1";
   2.402 -val neg_eq_less_0 = thm "neg_eq_less_0";
   2.403 -val not_neg_eq_ge_0 = thm "not_neg_eq_ge_0";
   2.404 -val not_neg_0 = thm "not_neg_0";
   2.405 -val not_neg_1 = thm "not_neg_1";
   2.406 -val iszero_0 = thm "iszero_0";
   2.407 -val not_iszero_1 = thm "not_iszero_1";
   2.408 -val int_0_less_1 = thm "int_0_less_1";
   2.409 -val int_0_neq_1 = thm "int_0_neq_1";
   2.410 -val negative_zless = thm "negative_zless";
   2.411 -val negative_zle = thm "negative_zle";
   2.412 -val not_zle_0_negative = thm "not_zle_0_negative";
   2.413 -val not_int_zless_negative = thm "not_int_zless_negative";
   2.414 -val negative_eq_positive = thm "negative_eq_positive";
   2.415 -val zle_iff_zadd = thm "zle_iff_zadd";
   2.416 -val abs_int_eq = thm "abs_int_eq";
   2.417 -val abs_split = thm"abs_split";
   2.418 -val nat_int = thm "nat_int";
   2.419 -val nat_zminus_int = thm "nat_zminus_int";
   2.420 -val nat_zero = thm "nat_zero";
   2.421 -val not_neg_nat = thm "not_neg_nat";
   2.422 -val neg_nat = thm "neg_nat";
   2.423 -val zless_nat_eq_int_zless = thm "zless_nat_eq_int_zless";
   2.424 -val nat_0_le = thm "nat_0_le";
   2.425 -val nat_le_0 = thm "nat_le_0";
   2.426 -val zless_nat_conj = thm "zless_nat_conj";
   2.427 -val int_cases = thm "int_cases";
   2.428 -
   2.429 -val int_def = thm "int_def";
   2.430 -val Zero_int_def = thm "Zero_int_def";
   2.431 -val One_int_def = thm "One_int_def";
   2.432 -val diff_int_def = thm "diff_int_def";
   2.433 -
   2.434 -val inj_int = thm "inj_int";
   2.435 -val zminus_zminus = thm "zminus_zminus";
   2.436 -val zminus_0 = thm "zminus_0";
   2.437 -val zminus_zadd_distrib = thm "zminus_zadd_distrib";
   2.438 -val zadd_commute = thm "zadd_commute";
   2.439 -val zadd_assoc = thm "zadd_assoc";
   2.440 -val zadd_left_commute = thm "zadd_left_commute";
   2.441 -val zadd_ac = thms "zadd_ac";
   2.442 -val zmult_ac = thms "zmult_ac";
   2.443 -val zadd_int = thm "zadd_int";
   2.444 -val zadd_int_left = thm "zadd_int_left";
   2.445 -val int_Suc = thm "int_Suc";
   2.446 -val zadd_0 = thm "zadd_0";
   2.447 -val zadd_0_right = thm "zadd_0_right";
   2.448 -val zmult_zminus = thm "zmult_zminus";
   2.449 -val zmult_commute = thm "zmult_commute";
   2.450 -val zmult_assoc = thm "zmult_assoc";
   2.451 -val zadd_zmult_distrib = thm "zadd_zmult_distrib";
   2.452 -val zadd_zmult_distrib2 = thm "zadd_zmult_distrib2";
   2.453 -val zdiff_zmult_distrib = thm "zdiff_zmult_distrib";
   2.454 -val zdiff_zmult_distrib2 = thm "zdiff_zmult_distrib2";
   2.455 -val int_distrib = thms "int_distrib";
   2.456 -val zmult_int = thm "zmult_int";
   2.457 -val zmult_1 = thm "zmult_1";
   2.458 -val zmult_1_right = thm "zmult_1_right";
   2.459 -val int_int_eq = thm "int_int_eq";
   2.460 -val int_eq_0_conv = thm "int_eq_0_conv";
   2.461 -val zless_int = thm "zless_int";
   2.462 -val int_less_0_conv = thm "int_less_0_conv";
   2.463 -val zero_less_int_conv = thm "zero_less_int_conv";
   2.464 -val zle_int = thm "zle_int";
   2.465 -val zero_zle_int = thm "zero_zle_int";
   2.466 -val int_le_0_conv = thm "int_le_0_conv";
   2.467 -val zle_refl = thm "zle_refl";
   2.468 -val zle_linear = thm "zle_linear";
   2.469 -val zle_trans = thm "zle_trans";
   2.470 -val zle_anti_sym = thm "zle_anti_sym";
   2.471 -
   2.472 -val Ints_def = thm "Ints_def";
   2.473 -val Nats_def = thm "Nats_def";
   2.474 -
   2.475 -val of_nat_0 = thm "of_nat_0";
   2.476 -val of_nat_Suc = thm "of_nat_Suc";
   2.477 -val of_nat_1 = thm "of_nat_1";
   2.478 -val of_nat_add = thm "of_nat_add";
   2.479 -val of_nat_mult = thm "of_nat_mult";
   2.480 -val zero_le_imp_of_nat = thm "zero_le_imp_of_nat";
   2.481 -val less_imp_of_nat_less = thm "less_imp_of_nat_less";
   2.482 -val of_nat_less_imp_less = thm "of_nat_less_imp_less";
   2.483 -val of_nat_less_iff = thm "of_nat_less_iff";
   2.484 -val of_nat_le_iff = thm "of_nat_le_iff";
   2.485 -val of_nat_eq_iff = thm "of_nat_eq_iff";
   2.486 -val Nats_0 = thm "Nats_0";
   2.487 -val Nats_1 = thm "Nats_1";
   2.488 -val Nats_add = thm "Nats_add";
   2.489 -val Nats_mult = thm "Nats_mult";
   2.490 -val int_eq_of_nat = thm"int_eq_of_nat";
   2.491 -val of_int = thm "of_int";
   2.492 -val of_int_0 = thm "of_int_0";
   2.493 -val of_int_1 = thm "of_int_1";
   2.494 -val of_int_add = thm "of_int_add";
   2.495 -val of_int_minus = thm "of_int_minus";
   2.496 -val of_int_diff = thm "of_int_diff";
   2.497 -val of_int_mult = thm "of_int_mult";
   2.498 -val of_int_le_iff = thm "of_int_le_iff";
   2.499 -val of_int_less_iff = thm "of_int_less_iff";
   2.500 -val of_int_eq_iff = thm "of_int_eq_iff";
   2.501 -val Ints_0 = thm "Ints_0";
   2.502 -val Ints_1 = thm "Ints_1";
   2.503 -val Ints_add = thm "Ints_add";
   2.504 -val Ints_minus = thm "Ints_minus";
   2.505 -val Ints_diff = thm "Ints_diff";
   2.506 -val Ints_mult = thm "Ints_mult";
   2.507 -val of_int_of_nat_eq = thm"of_int_of_nat_eq";
   2.508 -val Ints_cases = thm "Ints_cases";
   2.509 -val Ints_induct = thm "Ints_induct";
   2.510 -*}
   2.511 -
   2.512 -end
   2.513 +end
   2.514 \ No newline at end of file
     3.1 --- a/src/HOL/Integ/Numeral.thy	Thu Apr 26 13:33:04 2007 +0200
     3.2 +++ b/src/HOL/Integ/Numeral.thy	Thu Apr 26 13:33:05 2007 +0200
     3.3 @@ -7,10 +7,12 @@
     3.4  header {* Arithmetic on Binary Integers *}
     3.5  
     3.6  theory Numeral
     3.7 -imports IntDef Datatype
     3.8 +imports IntDef
     3.9  uses "../Tools/numeral_syntax.ML"
    3.10  begin
    3.11  
    3.12 +subsection {* Binary representation *}
    3.13 +
    3.14  text {*
    3.15    This formalization defines binary arithmetic in terms of the integers
    3.16    rather than using a datatype. This avoids multiple representations (leading
    3.17 @@ -23,13 +25,13 @@
    3.18    @{text "-5 = (-3)*2 + 1"}.
    3.19  *}
    3.20  
    3.21 +datatype bit = B0 | B1
    3.22 +
    3.23  text{*
    3.24 -  This type avoids the use of type @{typ bool}, which would make
    3.25 +  Type @{typ bit} avoids the use of type @{typ bool}, which would make
    3.26    all of the rewrite rules higher-order.
    3.27  *}
    3.28  
    3.29 -datatype bit = B0 | B1
    3.30 -
    3.31  definition
    3.32    Pls :: int where
    3.33    [code nofunc]:"Pls = 0"
    3.34 @@ -74,9 +76,12 @@
    3.35    pred :: "int \<Rightarrow> int" where
    3.36    [code nofunc]: "pred k = k - 1"
    3.37  
    3.38 -declare
    3.39 - max_def[of "number_of u" "number_of v", standard, simp]
    3.40 - min_def[of "number_of u" "number_of v", standard, simp]
    3.41 +lemmas
    3.42 +  max_number_of [simp] = max_def
    3.43 +    [of "number_of u" "number_of v", standard, simp]
    3.44 +and
    3.45 +  min_number_of [simp] = min_def 
    3.46 +    [of "number_of u" "number_of v", standard, simp]
    3.47    -- {* unfolding @{text minx} and @{text max} on numerals *}
    3.48  
    3.49  lemmas numeral_simps = 
    3.50 @@ -84,11 +89,11 @@
    3.51  
    3.52  text {* Removal of leading zeroes *}
    3.53  
    3.54 -lemma Pls_0_eq [simp, code func]:
    3.55 +lemma Pls_0_eq [simp, normal post]:
    3.56    "Pls BIT B0 = Pls"
    3.57    unfolding numeral_simps by simp
    3.58  
    3.59 -lemma Min_1_eq [simp, code func]:
    3.60 +lemma Min_1_eq [simp, normal post]:
    3.61    "Min BIT B1 = Min"
    3.62    unfolding numeral_simps by simp
    3.63  
    3.64 @@ -200,6 +205,18 @@
    3.65  axclass number_ring \<subseteq> number, comm_ring_1
    3.66    number_of_eq: "number_of k = of_int k"
    3.67  
    3.68 +text {* self-embedding of the intergers *}
    3.69 +
    3.70 +instance int :: number_ring
    3.71 +  int_number_of_def: "number_of w \<equiv> of_int w"
    3.72 +  by intro_classes (simp only: int_number_of_def)
    3.73 +
    3.74 +lemmas [code nofunc] = int_number_of_def
    3.75 +
    3.76 +lemma number_of_is_id:
    3.77 +  "number_of (k::int) = k"
    3.78 +  unfolding int_number_of_def by simp
    3.79 +
    3.80  lemma number_of_succ:
    3.81    "number_of (succ k) = (1 + number_of k ::'a::number_ring)"
    3.82    unfolding number_of_eq numeral_simps by simp
    3.83 @@ -483,7 +500,7 @@
    3.84  
    3.85  subsection {* Simplification of arithmetic operations on integer constants. *}
    3.86  
    3.87 -lemmas arith_extra_simps [standard] =
    3.88 +lemmas arith_extra_simps [standard, simp] =
    3.89    number_of_add [symmetric]
    3.90    number_of_minus [symmetric] numeral_m1_eq_minus_1 [symmetric]
    3.91    number_of_mult [symmetric]
    3.92 @@ -507,7 +524,7 @@
    3.93  
    3.94  text {* Simplification of relational operations *}
    3.95  
    3.96 -lemmas rel_simps = 
    3.97 +lemmas rel_simps [simp] = 
    3.98    eq_number_of_eq iszero_number_of_Pls nonzero_number_of_Min
    3.99    iszero_number_of_0 iszero_number_of_1
   3.100    less_number_of_eq_neg
   3.101 @@ -515,9 +532,6 @@
   3.102    neg_number_of_Min neg_number_of_BIT
   3.103    le_number_of_eq
   3.104  
   3.105 -declare arith_extra_simps [simp]
   3.106 -declare rel_simps [simp]
   3.107 -
   3.108  
   3.109  subsection {* Simplification of arithmetic when nested to the right. *}
   3.110  
   3.111 @@ -544,6 +558,109 @@
   3.112  done
   3.113  
   3.114  
   3.115 +subsection {* Configuration of the code generator *}
   3.116 +
   3.117 +instance int :: eq ..
   3.118 +
   3.119 +code_datatype Pls Min Bit "number_of \<Colon> int \<Rightarrow> int"
   3.120 +
   3.121 +definition
   3.122 +  int_aux :: "int \<Rightarrow> nat \<Rightarrow> int" where
   3.123 +  "int_aux i n = (i + int n)"
   3.124 +
   3.125 +lemma [code]:
   3.126 +  "int_aux i 0 = i"
   3.127 +  "int_aux i (Suc n) = int_aux (i + 1) n" -- {* tail recursive *}
   3.128 +  by (simp add: int_aux_def)+
   3.129 +
   3.130 +lemma [code]:
   3.131 +  "int n = int_aux 0 n"
   3.132 +  by (simp add: int_aux_def)
   3.133 +
   3.134 +definition
   3.135 +  nat_aux :: "nat \<Rightarrow> int \<Rightarrow> nat" where
   3.136 +  "nat_aux n i = (n + nat i)"
   3.137 +
   3.138 +lemma [code]: "nat_aux n i = (if i <= 0 then n else nat_aux (Suc n) (i - 1))"
   3.139 +  -- {* tail recursive *}
   3.140 +  by (auto simp add: nat_aux_def nat_eq_iff linorder_not_le order_less_imp_le
   3.141 +    dest: zless_imp_add1_zle)
   3.142 +
   3.143 +lemma [code]: "nat i = nat_aux 0 i"
   3.144 +  by (simp add: nat_aux_def)
   3.145 +
   3.146 +lemma zero_is_num_zero [code func, code inline, symmetric, normal post]:
   3.147 +  "(0\<Colon>int) = number_of Numeral.Pls" 
   3.148 +  by simp
   3.149 +
   3.150 +lemma one_is_num_one [code func, code inline, symmetric, normal post]:
   3.151 +  "(1\<Colon>int) = number_of (Numeral.Pls BIT bit.B1)" 
   3.152 +  by simp 
   3.153 +
   3.154 +code_modulename SML
   3.155 +  IntDef Integer
   3.156 +
   3.157 +code_modulename OCaml
   3.158 +  IntDef Integer
   3.159 +
   3.160 +code_modulename Haskell
   3.161 +  IntDef Integer
   3.162 +
   3.163 +code_modulename SML
   3.164 +  Numeral Integer
   3.165 +
   3.166 +code_modulename OCaml
   3.167 +  Numeral Integer
   3.168 +
   3.169 +code_modulename Haskell
   3.170 +  Numeral Integer
   3.171 +
   3.172 +(*FIXME: the IntInf.fromInt below hides a dependence on fixed-precision ints!*)
   3.173 +
   3.174 +types_code
   3.175 +  "int" ("int")
   3.176 +attach (term_of) {*
   3.177 +val term_of_int = HOLogic.mk_number HOLogic.intT o IntInf.fromInt;
   3.178 +*}
   3.179 +attach (test) {*
   3.180 +fun gen_int i = one_of [~1, 1] * random_range 0 i;
   3.181 +*}
   3.182 +
   3.183 +setup {*
   3.184 +let
   3.185 +
   3.186 +fun number_of_codegen thy defs gr dep module b (Const ("Numeral.number_of", Type ("fun", [_, T])) $ t) =
   3.187 +      if T = HOLogic.intT then
   3.188 +        (SOME (fst (Codegen.invoke_tycodegen thy defs dep module false (gr, T)),
   3.189 +          (Pretty.str o IntInf.toString o HOLogic.dest_numeral) t) handle TERM _ => NONE)
   3.190 +      else if T = HOLogic.natT then
   3.191 +        SOME (Codegen.invoke_codegen thy defs dep module b (gr,
   3.192 +          Const ("IntDef.nat", HOLogic.intT --> HOLogic.natT) $
   3.193 +            (Const ("Numeral.number_of", HOLogic.intT --> HOLogic.intT) $ t)))
   3.194 +      else NONE
   3.195 +  | number_of_codegen _ _ _ _ _ _ _ = NONE;
   3.196 +
   3.197 +in
   3.198 +
   3.199 +Codegen.add_codegen "number_of_codegen" number_of_codegen
   3.200 +
   3.201 +end
   3.202 +*}
   3.203 +
   3.204 +consts_code
   3.205 +  "HOL.zero" :: "int"                ("0")
   3.206 +  "HOL.one" :: "int"                 ("1")
   3.207 +  "HOL.uminus" :: "int => int"       ("~")
   3.208 +  "HOL.plus" :: "int => int => int"  ("(_ +/ _)")
   3.209 +  "HOL.times" :: "int => int => int" ("(_ */ _)")
   3.210 +  "Orderings.less" :: "int => int => bool" ("(_ </ _)")
   3.211 +  "Orderings.less_eq" :: "int => int => bool" ("(_ <=/ _)")
   3.212 +  "neg"                              ("(_ < 0)")
   3.213 +
   3.214 +quickcheck_params [default_type = int]
   3.215 +
   3.216 +(* setup continues in theory Presburger *)
   3.217 +
   3.218  hide (open) const Pls Min B0 B1 succ pred
   3.219  
   3.220  end
     4.1 --- a/src/HOL/Integ/Presburger.thy	Thu Apr 26 13:33:04 2007 +0200
     4.2 +++ b/src/HOL/Integ/Presburger.thy	Thu Apr 26 13:33:05 2007 +0200
     4.3 @@ -9,7 +9,7 @@
     4.4  header {* Presburger Arithmetic: Cooper's Algorithm *}
     4.5  
     4.6  theory Presburger
     4.7 -imports NatSimprocs
     4.8 +imports NatSimprocs "../SetInterval"
     4.9  uses
    4.10    ("cooper_dec.ML") ("cooper_proof.ML") ("qelim.ML") 
    4.11    ("reflected_presburger.ML") ("reflected_cooper.ML") ("presburger.ML")
    4.12 @@ -1059,17 +1059,14 @@
    4.13  
    4.14  setup "Presburger.setup"
    4.15  
    4.16 -text {* Code generator setup *}
    4.17 +
    4.18 +subsection {* Code generator setup *}
    4.19  
    4.20  text {*
    4.21 -  Presburger arithmetic is necessary (at least convenient) to prove some
    4.22 -  of the following code lemmas on integer numerals.
    4.23 +  Presburger arithmetic is convenient to prove some
    4.24 +  of the following code lemmas on integer numerals:
    4.25  *}
    4.26  
    4.27 -lemma eq_number_of [code func]:
    4.28 -  "((number_of k)\<Colon>int) = number_of l \<longleftrightarrow> k = l"
    4.29 -  unfolding number_of_is_id ..
    4.30 -
    4.31  lemma eq_Pls_Pls:
    4.32    "Numeral.Pls = Numeral.Pls \<longleftrightarrow> True" by rule+
    4.33  
    4.34 @@ -1131,14 +1128,10 @@
    4.35    apply auto
    4.36  done
    4.37  
    4.38 -lemmas eq_numeral_code [code func] =
    4.39 -  eq_Pls_Pls eq_Pls_Min eq_Pls_Bit0 eq_Pls_Bit1
    4.40 -  eq_Min_Pls eq_Min_Min eq_Min_Bit0 eq_Min_Bit1
    4.41 -  eq_Bit0_Pls eq_Bit1_Pls eq_Bit0_Min eq_Bit1_Min eq_Bit_Bit
    4.42 +lemma eq_number_of:
    4.43 +  "(number_of k \<Colon> int) = number_of l \<longleftrightarrow> k = l"
    4.44 +  unfolding number_of_is_id ..
    4.45  
    4.46 -lemma less_eq_number_of [code func]:
    4.47 -  "(number_of k \<Colon> int) \<le> number_of l \<longleftrightarrow> k \<le> l"
    4.48 -  unfolding number_of_is_id ..
    4.49  
    4.50  lemma less_eq_Pls_Pls:
    4.51    "Numeral.Pls \<le> Numeral.Pls \<longleftrightarrow> True" by rule+
    4.52 @@ -1190,13 +1183,10 @@
    4.53    "Numeral.Bit k1 bit.B1 \<le> Numeral.Bit k2 bit.B0 \<longleftrightarrow> k1 < k2"
    4.54    unfolding Bit_def by (auto split: bit.split)
    4.55  
    4.56 -lemmas less_eq_numeral_code [code func] = less_eq_Pls_Pls less_eq_Pls_Min less_eq_Pls_Bit
    4.57 -  less_eq_Min_Pls less_eq_Min_Min less_eq_Min_Bit0 less_eq_Min_Bit1
    4.58 -  less_eq_Bit0_Pls less_eq_Bit1_Pls less_eq_Bit_Min less_eq_Bit0_Bit less_eq_Bit_Bit1 less_eq_Bit1_Bit0
    4.59 +lemma less_eq_number_of:
    4.60 +  "(number_of k \<Colon> int) \<le> number_of l \<longleftrightarrow> k \<le> l"
    4.61 +  unfolding number_of_is_id ..
    4.62  
    4.63 -lemma less_eq_number_of [code func]:
    4.64 -  "(number_of k \<Colon> int) < number_of l \<longleftrightarrow> k < l"
    4.65 -  unfolding number_of_is_id ..
    4.66  
    4.67  lemma less_Pls_Pls:
    4.68    "Numeral.Pls < Numeral.Pls \<longleftrightarrow> False" by auto
    4.69 @@ -1248,8 +1238,42 @@
    4.70    "Numeral.Bit k1 bit.B0 < Numeral.Bit k2 bit.B1 \<longleftrightarrow> k1 \<le> k2"
    4.71    unfolding Bit_def bit.cases by auto
    4.72  
    4.73 +lemma less_number_of:
    4.74 +  "(number_of k \<Colon> int) < number_of l \<longleftrightarrow> k < l"
    4.75 +  unfolding number_of_is_id ..
    4.76 +
    4.77 +
    4.78 +lemmas pred_succ_numeral_code [code func] =
    4.79 +  arith_simps(5-12)
    4.80 +
    4.81 +lemmas plus_numeral_code [code func] =
    4.82 +  arith_simps(13-17)
    4.83 +  arith_simps(26-27)
    4.84 +  arith_extra_simps(1) [where 'a = int]
    4.85 +
    4.86 +lemmas minus_numeral_code [code func] =
    4.87 +  arith_simps(18-21)
    4.88 +  arith_extra_simps(2) [where 'a = int]
    4.89 +  arith_extra_simps(5) [where 'a = int]
    4.90 +
    4.91 +lemmas times_numeral_code [code func] =
    4.92 +  arith_simps(22-25)
    4.93 +  arith_extra_simps(4) [where 'a = int]
    4.94 +
    4.95 +lemmas eq_numeral_code [code func] =
    4.96 +  eq_Pls_Pls eq_Pls_Min eq_Pls_Bit0 eq_Pls_Bit1
    4.97 +  eq_Min_Pls eq_Min_Min eq_Min_Bit0 eq_Min_Bit1
    4.98 +  eq_Bit0_Pls eq_Bit1_Pls eq_Bit0_Min eq_Bit1_Min eq_Bit_Bit
    4.99 +  eq_number_of
   4.100 +
   4.101 +lemmas less_eq_numeral_code [code func] = less_eq_Pls_Pls less_eq_Pls_Min less_eq_Pls_Bit
   4.102 +  less_eq_Min_Pls less_eq_Min_Min less_eq_Min_Bit0 less_eq_Min_Bit1
   4.103 +  less_eq_Bit0_Pls less_eq_Bit1_Pls less_eq_Bit_Min less_eq_Bit0_Bit less_eq_Bit_Bit1 less_eq_Bit1_Bit0
   4.104 +  less_eq_number_of
   4.105 +
   4.106  lemmas less_numeral_code [code func] = less_Pls_Pls less_Pls_Min less_Pls_Bit0
   4.107    less_Pls_Bit1 less_Min_Pls less_Min_Min less_Min_Bit less_Bit_Pls
   4.108    less_Bit0_Min less_Bit1_Min less_Bit_Bit0 less_Bit1_Bit less_Bit0_Bit1
   4.109 +  less_number_of
   4.110  
   4.111  end
     5.1 --- a/src/HOL/Presburger.thy	Thu Apr 26 13:33:04 2007 +0200
     5.2 +++ b/src/HOL/Presburger.thy	Thu Apr 26 13:33:05 2007 +0200
     5.3 @@ -9,7 +9,7 @@
     5.4  header {* Presburger Arithmetic: Cooper's Algorithm *}
     5.5  
     5.6  theory Presburger
     5.7 -imports NatSimprocs
     5.8 +imports NatSimprocs "../SetInterval"
     5.9  uses
    5.10    ("cooper_dec.ML") ("cooper_proof.ML") ("qelim.ML") 
    5.11    ("reflected_presburger.ML") ("reflected_cooper.ML") ("presburger.ML")
    5.12 @@ -1059,17 +1059,14 @@
    5.13  
    5.14  setup "Presburger.setup"
    5.15  
    5.16 -text {* Code generator setup *}
    5.17 +
    5.18 +subsection {* Code generator setup *}
    5.19  
    5.20  text {*
    5.21 -  Presburger arithmetic is necessary (at least convenient) to prove some
    5.22 -  of the following code lemmas on integer numerals.
    5.23 +  Presburger arithmetic is convenient to prove some
    5.24 +  of the following code lemmas on integer numerals:
    5.25  *}
    5.26  
    5.27 -lemma eq_number_of [code func]:
    5.28 -  "((number_of k)\<Colon>int) = number_of l \<longleftrightarrow> k = l"
    5.29 -  unfolding number_of_is_id ..
    5.30 -
    5.31  lemma eq_Pls_Pls:
    5.32    "Numeral.Pls = Numeral.Pls \<longleftrightarrow> True" by rule+
    5.33  
    5.34 @@ -1131,14 +1128,10 @@
    5.35    apply auto
    5.36  done
    5.37  
    5.38 -lemmas eq_numeral_code [code func] =
    5.39 -  eq_Pls_Pls eq_Pls_Min eq_Pls_Bit0 eq_Pls_Bit1
    5.40 -  eq_Min_Pls eq_Min_Min eq_Min_Bit0 eq_Min_Bit1
    5.41 -  eq_Bit0_Pls eq_Bit1_Pls eq_Bit0_Min eq_Bit1_Min eq_Bit_Bit
    5.42 +lemma eq_number_of:
    5.43 +  "(number_of k \<Colon> int) = number_of l \<longleftrightarrow> k = l"
    5.44 +  unfolding number_of_is_id ..
    5.45  
    5.46 -lemma less_eq_number_of [code func]:
    5.47 -  "(number_of k \<Colon> int) \<le> number_of l \<longleftrightarrow> k \<le> l"
    5.48 -  unfolding number_of_is_id ..
    5.49  
    5.50  lemma less_eq_Pls_Pls:
    5.51    "Numeral.Pls \<le> Numeral.Pls \<longleftrightarrow> True" by rule+
    5.52 @@ -1190,13 +1183,10 @@
    5.53    "Numeral.Bit k1 bit.B1 \<le> Numeral.Bit k2 bit.B0 \<longleftrightarrow> k1 < k2"
    5.54    unfolding Bit_def by (auto split: bit.split)
    5.55  
    5.56 -lemmas less_eq_numeral_code [code func] = less_eq_Pls_Pls less_eq_Pls_Min less_eq_Pls_Bit
    5.57 -  less_eq_Min_Pls less_eq_Min_Min less_eq_Min_Bit0 less_eq_Min_Bit1
    5.58 -  less_eq_Bit0_Pls less_eq_Bit1_Pls less_eq_Bit_Min less_eq_Bit0_Bit less_eq_Bit_Bit1 less_eq_Bit1_Bit0
    5.59 +lemma less_eq_number_of:
    5.60 +  "(number_of k \<Colon> int) \<le> number_of l \<longleftrightarrow> k \<le> l"
    5.61 +  unfolding number_of_is_id ..
    5.62  
    5.63 -lemma less_eq_number_of [code func]:
    5.64 -  "(number_of k \<Colon> int) < number_of l \<longleftrightarrow> k < l"
    5.65 -  unfolding number_of_is_id ..
    5.66  
    5.67  lemma less_Pls_Pls:
    5.68    "Numeral.Pls < Numeral.Pls \<longleftrightarrow> False" by auto
    5.69 @@ -1248,8 +1238,42 @@
    5.70    "Numeral.Bit k1 bit.B0 < Numeral.Bit k2 bit.B1 \<longleftrightarrow> k1 \<le> k2"
    5.71    unfolding Bit_def bit.cases by auto
    5.72  
    5.73 +lemma less_number_of:
    5.74 +  "(number_of k \<Colon> int) < number_of l \<longleftrightarrow> k < l"
    5.75 +  unfolding number_of_is_id ..
    5.76 +
    5.77 +
    5.78 +lemmas pred_succ_numeral_code [code func] =
    5.79 +  arith_simps(5-12)
    5.80 +
    5.81 +lemmas plus_numeral_code [code func] =
    5.82 +  arith_simps(13-17)
    5.83 +  arith_simps(26-27)
    5.84 +  arith_extra_simps(1) [where 'a = int]
    5.85 +
    5.86 +lemmas minus_numeral_code [code func] =
    5.87 +  arith_simps(18-21)
    5.88 +  arith_extra_simps(2) [where 'a = int]
    5.89 +  arith_extra_simps(5) [where 'a = int]
    5.90 +
    5.91 +lemmas times_numeral_code [code func] =
    5.92 +  arith_simps(22-25)
    5.93 +  arith_extra_simps(4) [where 'a = int]
    5.94 +
    5.95 +lemmas eq_numeral_code [code func] =
    5.96 +  eq_Pls_Pls eq_Pls_Min eq_Pls_Bit0 eq_Pls_Bit1
    5.97 +  eq_Min_Pls eq_Min_Min eq_Min_Bit0 eq_Min_Bit1
    5.98 +  eq_Bit0_Pls eq_Bit1_Pls eq_Bit0_Min eq_Bit1_Min eq_Bit_Bit
    5.99 +  eq_number_of
   5.100 +
   5.101 +lemmas less_eq_numeral_code [code func] = less_eq_Pls_Pls less_eq_Pls_Min less_eq_Pls_Bit
   5.102 +  less_eq_Min_Pls less_eq_Min_Min less_eq_Min_Bit0 less_eq_Min_Bit1
   5.103 +  less_eq_Bit0_Pls less_eq_Bit1_Pls less_eq_Bit_Min less_eq_Bit0_Bit less_eq_Bit_Bit1 less_eq_Bit1_Bit0
   5.104 +  less_eq_number_of
   5.105 +
   5.106  lemmas less_numeral_code [code func] = less_Pls_Pls less_Pls_Min less_Pls_Bit0
   5.107    less_Pls_Bit1 less_Min_Pls less_Min_Min less_Min_Bit less_Bit_Pls
   5.108    less_Bit0_Min less_Bit1_Min less_Bit_Bit0 less_Bit1_Bit less_Bit0_Bit1
   5.109 +  less_number_of
   5.110  
   5.111  end