theory NatBin now named Nat_Numeral
authorhaftmann
Wed Apr 15 15:30:39 2009 +0200 (2009-04-15)
changeset 30925c38cbc0ac8d1
parent 30924 c1ed09f3fbfe
child 30926 3a30613aa469
theory NatBin now named Nat_Numeral
src/HOL/Groebner_Basis.thy
src/HOL/Import/HOL/arithmetic.imp
src/HOL/Import/HOL/real.imp
src/HOL/Import/HOLLight/hollight.imp
src/HOL/IsaMakefile
src/HOL/NatBin.thy
src/HOL/Nat_Numeral.thy
     1.1 --- a/src/HOL/Groebner_Basis.thy	Wed Apr 15 15:30:38 2009 +0200
     1.2 +++ b/src/HOL/Groebner_Basis.thy	Wed Apr 15 15:30:39 2009 +0200
     1.3 @@ -5,7 +5,7 @@
     1.4  header {* Semiring normalization and Groebner Bases *}
     1.5  
     1.6  theory Groebner_Basis
     1.7 -imports NatBin
     1.8 +imports Nat_Numeral
     1.9  uses
    1.10    "Tools/Groebner_Basis/misc.ML"
    1.11    "Tools/Groebner_Basis/normalizer_data.ML"
     2.1 --- a/src/HOL/Import/HOL/arithmetic.imp	Wed Apr 15 15:30:38 2009 +0200
     2.2 +++ b/src/HOL/Import/HOL/arithmetic.imp	Wed Apr 15 15:30:39 2009 +0200
     2.3 @@ -43,7 +43,7 @@
     2.4    "TWO" > "HOL4Base.arithmetic.TWO"
     2.5    "TIMES2" > "NatSimprocs.nat_mult_2"
     2.6    "SUC_SUB1" > "HOL4Base.arithmetic.SUC_SUB1"
     2.7 -  "SUC_ONE_ADD" > "NatBin.Suc_eq_add_numeral_1_left"
     2.8 +  "SUC_ONE_ADD" > "Nat_Numeral.Suc_eq_add_numeral_1_left"
     2.9    "SUC_NOT" > "Nat.nat.simps_2"
    2.10    "SUC_ELIM_THM" > "HOL4Base.arithmetic.SUC_ELIM_THM"
    2.11    "SUC_ADD_SYM" > "HOL4Base.arithmetic.SUC_ADD_SYM"
    2.12 @@ -233,7 +233,7 @@
    2.13    "EVEN_AND_ODD" > "HOL4Base.arithmetic.EVEN_AND_ODD"
    2.14    "EVEN_ADD" > "HOL4Base.arithmetic.EVEN_ADD"
    2.15    "EVEN" > "HOL4Base.arithmetic.EVEN"
    2.16 -  "EQ_MULT_LCANCEL" > "NatBin.nat_mult_eq_cancel_disj"
    2.17 +  "EQ_MULT_LCANCEL" > "Nat_Numeral.nat_mult_eq_cancel_disj"
    2.18    "EQ_MONO_ADD_EQ" > "Nat.nat_add_right_cancel"
    2.19    "EQ_LESS_EQ" > "Orderings.order_eq_iff"
    2.20    "EQ_ADD_RCANCEL" > "Nat.nat_add_right_cancel"
     3.1 --- a/src/HOL/Import/HOL/real.imp	Wed Apr 15 15:30:38 2009 +0200
     3.2 +++ b/src/HOL/Import/HOL/real.imp	Wed Apr 15 15:30:39 2009 +0200
     3.3 @@ -99,7 +99,7 @@
     3.4    "REAL_POW_INV" > "Power.power_inverse"
     3.5    "REAL_POW_DIV" > "Power.power_divide"
     3.6    "REAL_POW_ADD" > "Power.power_add"
     3.7 -  "REAL_POW2_ABS" > "NatBin.power2_abs"
     3.8 +  "REAL_POW2_ABS" > "Nat_Numeral.power2_abs"
     3.9    "REAL_POS_NZ" > "HOL4Real.real.REAL_POS_NZ"
    3.10    "REAL_POS" > "RealDef.real_of_nat_ge_zero"
    3.11    "REAL_POASQ" > "HOL4Real.real.REAL_POASQ"
    3.12 @@ -210,7 +210,7 @@
    3.13    "REAL_LE_RDIV_EQ" > "Ring_and_Field.pos_le_divide_eq"
    3.14    "REAL_LE_RDIV" > "Ring_and_Field.mult_imp_le_div_pos"
    3.15    "REAL_LE_RADD" > "OrderedGroup.add_le_cancel_right"
    3.16 -  "REAL_LE_POW2" > "NatBin.zero_compare_simps_12"
    3.17 +  "REAL_LE_POW2" > "Nat_Numeral.zero_compare_simps_12"
    3.18    "REAL_LE_NEGTOTAL" > "HOL4Real.real.REAL_LE_NEGTOTAL"
    3.19    "REAL_LE_NEGR" > "OrderedGroup.le_minus_self_iff"
    3.20    "REAL_LE_NEGL" > "OrderedGroup.minus_le_self_iff"
    3.21 @@ -313,7 +313,7 @@
    3.22    "POW_ONE" > "Power.power_one"
    3.23    "POW_NZ" > "Power.field_power_not_zero"
    3.24    "POW_MUL" > "Power.power_mult_distrib"
    3.25 -  "POW_MINUS1" > "NatBin.power_minus1_even"
    3.26 +  "POW_MINUS1" > "Nat_Numeral.power_minus1_even"
    3.27    "POW_M1" > "HOL4Real.real.POW_M1"
    3.28    "POW_LT" > "HOL4Real.real.POW_LT"
    3.29    "POW_LE" > "Power.power_mono"
    3.30 @@ -323,7 +323,7 @@
    3.31    "POW_ABS" > "Power.power_abs"
    3.32    "POW_2_LT" > "RealPow.two_realpow_gt"
    3.33    "POW_2_LE1" > "RealPow.two_realpow_ge_one"
    3.34 -  "POW_2" > "NatBin.power2_eq_square"
    3.35 +  "POW_2" > "Nat_Numeral.power2_eq_square"
    3.36    "POW_1" > "Power.power_one_right"
    3.37    "POW_0" > "Power.power_0_Suc"
    3.38    "ABS_ZERO" > "OrderedGroup.abs_eq_0"
    3.39 @@ -335,7 +335,7 @@
    3.40    "ABS_SIGN2" > "HOL4Real.real.ABS_SIGN2"
    3.41    "ABS_SIGN" > "HOL4Real.real.ABS_SIGN"
    3.42    "ABS_REFL" > "HOL4Real.real.ABS_REFL"
    3.43 -  "ABS_POW2" > "NatBin.abs_power2"
    3.44 +  "ABS_POW2" > "Nat_Numeral.abs_power2"
    3.45    "ABS_POS" > "OrderedGroup.abs_ge_zero"
    3.46    "ABS_NZ" > "OrderedGroup.zero_less_abs_iff"
    3.47    "ABS_NEG" > "OrderedGroup.abs_minus_cancel"
     4.1 --- a/src/HOL/Import/HOLLight/hollight.imp	Wed Apr 15 15:30:38 2009 +0200
     4.2 +++ b/src/HOL/Import/HOLLight/hollight.imp	Wed Apr 15 15:30:39 2009 +0200
     4.3 @@ -1515,7 +1515,7 @@
     4.4    "EQ_REFL_T" > "HOL.simp_thms_6"
     4.5    "EQ_REFL" > "Presburger.fm_modd_pinf"
     4.6    "EQ_MULT_RCANCEL" > "Nat.mult_cancel2"
     4.7 -  "EQ_MULT_LCANCEL" > "NatBin.nat_mult_eq_cancel_disj"
     4.8 +  "EQ_MULT_LCANCEL" > "Nat_Numeral.nat_mult_eq_cancel_disj"
     4.9    "EQ_IMP_LE" > "HOLLight.hollight.EQ_IMP_LE"
    4.10    "EQ_EXT" > "HOL.meta_eq_to_obj_eq"
    4.11    "EQ_CLAUSES" > "HOLLight.hollight.EQ_CLAUSES"
     5.1 --- a/src/HOL/IsaMakefile	Wed Apr 15 15:30:38 2009 +0200
     5.2 +++ b/src/HOL/IsaMakefile	Wed Apr 15 15:30:39 2009 +0200
     5.3 @@ -216,7 +216,7 @@
     5.4    List.thy \
     5.5    Main.thy \
     5.6    Map.thy \
     5.7 -  NatBin.thy \
     5.8 +  Nat_Numeral.thy \
     5.9    Presburger.thy \
    5.10    Recdef.thy \
    5.11    Relation_Power.thy \
     6.1 --- a/src/HOL/NatBin.thy	Wed Apr 15 15:30:38 2009 +0200
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,975 +0,0 @@
     6.4 -(*  Title:      HOL/NatBin.thy
     6.5 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     6.6 -    Copyright   1999  University of Cambridge
     6.7 -*)
     6.8 -
     6.9 -header {* Binary arithmetic for the natural numbers *}
    6.10 -
    6.11 -theory NatBin
    6.12 -imports IntDiv
    6.13 -uses ("Tools/nat_simprocs.ML")
    6.14 -begin
    6.15 -
    6.16 -text {*
    6.17 -  Arithmetic for naturals is reduced to that for the non-negative integers.
    6.18 -*}
    6.19 -
    6.20 -instantiation nat :: number
    6.21 -begin
    6.22 -
    6.23 -definition
    6.24 -  nat_number_of_def [code inline, code del]: "number_of v = nat (number_of v)"
    6.25 -
    6.26 -instance ..
    6.27 -
    6.28 -end
    6.29 -
    6.30 -lemma [code post]:
    6.31 -  "nat (number_of v) = number_of v"
    6.32 -  unfolding nat_number_of_def ..
    6.33 -
    6.34 -abbreviation (xsymbols)
    6.35 -  power2 :: "'a::power => 'a"  ("(_\<twosuperior>)" [1000] 999) where
    6.36 -  "x\<twosuperior> == x^2"
    6.37 -
    6.38 -notation (latex output)
    6.39 -  power2  ("(_\<twosuperior>)" [1000] 999)
    6.40 -
    6.41 -notation (HTML output)
    6.42 -  power2  ("(_\<twosuperior>)" [1000] 999)
    6.43 -
    6.44 -
    6.45 -subsection {* Predicate for negative binary numbers *}
    6.46 -
    6.47 -definition neg  :: "int \<Rightarrow> bool" where
    6.48 -  "neg Z \<longleftrightarrow> Z < 0"
    6.49 -
    6.50 -lemma not_neg_int [simp]: "~ neg (of_nat n)"
    6.51 -by (simp add: neg_def)
    6.52 -
    6.53 -lemma neg_zminus_int [simp]: "neg (- (of_nat (Suc n)))"
    6.54 -by (simp add: neg_def neg_less_0_iff_less del: of_nat_Suc)
    6.55 -
    6.56 -lemmas neg_eq_less_0 = neg_def
    6.57 -
    6.58 -lemma not_neg_eq_ge_0: "(~neg x) = (0 \<le> x)"
    6.59 -by (simp add: neg_def linorder_not_less)
    6.60 -
    6.61 -text{*To simplify inequalities when Numeral1 can get simplified to 1*}
    6.62 -
    6.63 -lemma not_neg_0: "~ neg 0"
    6.64 -by (simp add: One_int_def neg_def)
    6.65 -
    6.66 -lemma not_neg_1: "~ neg 1"
    6.67 -by (simp add: neg_def linorder_not_less zero_le_one)
    6.68 -
    6.69 -lemma neg_nat: "neg z ==> nat z = 0"
    6.70 -by (simp add: neg_def order_less_imp_le) 
    6.71 -
    6.72 -lemma not_neg_nat: "~ neg z ==> of_nat (nat z) = z"
    6.73 -by (simp add: linorder_not_less neg_def)
    6.74 -
    6.75 -text {*
    6.76 -  If @{term Numeral0} is rewritten to 0 then this rule can't be applied:
    6.77 -  @{term Numeral0} IS @{term "number_of Pls"}
    6.78 -*}
    6.79 -
    6.80 -lemma not_neg_number_of_Pls: "~ neg (number_of Int.Pls)"
    6.81 -  by (simp add: neg_def)
    6.82 -
    6.83 -lemma neg_number_of_Min: "neg (number_of Int.Min)"
    6.84 -  by (simp add: neg_def)
    6.85 -
    6.86 -lemma neg_number_of_Bit0:
    6.87 -  "neg (number_of (Int.Bit0 w)) = neg (number_of w)"
    6.88 -  by (simp add: neg_def)
    6.89 -
    6.90 -lemma neg_number_of_Bit1:
    6.91 -  "neg (number_of (Int.Bit1 w)) = neg (number_of w)"
    6.92 -  by (simp add: neg_def)
    6.93 -
    6.94 -lemmas neg_simps [simp] =
    6.95 -  not_neg_0 not_neg_1
    6.96 -  not_neg_number_of_Pls neg_number_of_Min
    6.97 -  neg_number_of_Bit0 neg_number_of_Bit1
    6.98 -
    6.99 -
   6.100 -subsection{*Function @{term nat}: Coercion from Type @{typ int} to @{typ nat}*}
   6.101 -
   6.102 -declare nat_0 [simp] nat_1 [simp]
   6.103 -
   6.104 -lemma nat_number_of [simp]: "nat (number_of w) = number_of w"
   6.105 -by (simp add: nat_number_of_def)
   6.106 -
   6.107 -lemma nat_numeral_0_eq_0 [simp]: "Numeral0 = (0::nat)"
   6.108 -by (simp add: nat_number_of_def)
   6.109 -
   6.110 -lemma nat_numeral_1_eq_1 [simp]: "Numeral1 = (1::nat)"
   6.111 -by (simp add: nat_1 nat_number_of_def)
   6.112 -
   6.113 -lemma numeral_1_eq_Suc_0: "Numeral1 = Suc 0"
   6.114 -by (simp add: nat_numeral_1_eq_1)
   6.115 -
   6.116 -lemma numeral_2_eq_2: "2 = Suc (Suc 0)"
   6.117 -apply (unfold nat_number_of_def)
   6.118 -apply (rule nat_2)
   6.119 -done
   6.120 -
   6.121 -
   6.122 -subsection{*Function @{term int}: Coercion from Type @{typ nat} to @{typ int}*}
   6.123 -
   6.124 -lemma int_nat_number_of [simp]:
   6.125 -     "int (number_of v) =  
   6.126 -         (if neg (number_of v :: int) then 0  
   6.127 -          else (number_of v :: int))"
   6.128 -  unfolding nat_number_of_def number_of_is_id neg_def
   6.129 -  by simp
   6.130 -
   6.131 -
   6.132 -subsubsection{*Successor *}
   6.133 -
   6.134 -lemma Suc_nat_eq_nat_zadd1: "(0::int) <= z ==> Suc (nat z) = nat (1 + z)"
   6.135 -apply (rule sym)
   6.136 -apply (simp add: nat_eq_iff int_Suc)
   6.137 -done
   6.138 -
   6.139 -lemma Suc_nat_number_of_add:
   6.140 -     "Suc (number_of v + n) =  
   6.141 -        (if neg (number_of v :: int) then 1+n else number_of (Int.succ v) + n)"
   6.142 -  unfolding nat_number_of_def number_of_is_id neg_def numeral_simps
   6.143 -  by (simp add: Suc_nat_eq_nat_zadd1 add_ac)
   6.144 -
   6.145 -lemma Suc_nat_number_of [simp]:
   6.146 -     "Suc (number_of v) =  
   6.147 -        (if neg (number_of v :: int) then 1 else number_of (Int.succ v))"
   6.148 -apply (cut_tac n = 0 in Suc_nat_number_of_add)
   6.149 -apply (simp cong del: if_weak_cong)
   6.150 -done
   6.151 -
   6.152 -
   6.153 -subsubsection{*Addition *}
   6.154 -
   6.155 -lemma add_nat_number_of [simp]:
   6.156 -     "(number_of v :: nat) + number_of v' =  
   6.157 -         (if v < Int.Pls then number_of v'  
   6.158 -          else if v' < Int.Pls then number_of v  
   6.159 -          else number_of (v + v'))"
   6.160 -  unfolding nat_number_of_def number_of_is_id numeral_simps
   6.161 -  by (simp add: nat_add_distrib)
   6.162 -
   6.163 -lemma nat_number_of_add_1 [simp]:
   6.164 -  "number_of v + (1::nat) =
   6.165 -    (if v < Int.Pls then 1 else number_of (Int.succ v))"
   6.166 -  unfolding nat_number_of_def number_of_is_id numeral_simps
   6.167 -  by (simp add: nat_add_distrib)
   6.168 -
   6.169 -lemma nat_1_add_number_of [simp]:
   6.170 -  "(1::nat) + number_of v =
   6.171 -    (if v < Int.Pls then 1 else number_of (Int.succ v))"
   6.172 -  unfolding nat_number_of_def number_of_is_id numeral_simps
   6.173 -  by (simp add: nat_add_distrib)
   6.174 -
   6.175 -lemma nat_1_add_1 [simp]: "1 + 1 = (2::nat)"
   6.176 -  by (rule int_int_eq [THEN iffD1]) simp
   6.177 -
   6.178 -
   6.179 -subsubsection{*Subtraction *}
   6.180 -
   6.181 -lemma diff_nat_eq_if:
   6.182 -     "nat z - nat z' =  
   6.183 -        (if neg z' then nat z   
   6.184 -         else let d = z-z' in     
   6.185 -              if neg d then 0 else nat d)"
   6.186 -by (simp add: Let_def nat_diff_distrib [symmetric] neg_eq_less_0 not_neg_eq_ge_0)
   6.187 -
   6.188 -
   6.189 -lemma diff_nat_number_of [simp]: 
   6.190 -     "(number_of v :: nat) - number_of v' =  
   6.191 -        (if v' < Int.Pls then number_of v  
   6.192 -         else let d = number_of (v + uminus v') in     
   6.193 -              if neg d then 0 else nat d)"
   6.194 -  unfolding nat_number_of_def number_of_is_id numeral_simps neg_def
   6.195 -  by auto
   6.196 -
   6.197 -lemma nat_number_of_diff_1 [simp]:
   6.198 -  "number_of v - (1::nat) =
   6.199 -    (if v \<le> Int.Pls then 0 else number_of (Int.pred v))"
   6.200 -  unfolding nat_number_of_def number_of_is_id numeral_simps
   6.201 -  by auto
   6.202 -
   6.203 -
   6.204 -subsubsection{*Multiplication *}
   6.205 -
   6.206 -lemma mult_nat_number_of [simp]:
   6.207 -     "(number_of v :: nat) * number_of v' =  
   6.208 -       (if v < Int.Pls then 0 else number_of (v * v'))"
   6.209 -  unfolding nat_number_of_def number_of_is_id numeral_simps
   6.210 -  by (simp add: nat_mult_distrib)
   6.211 -
   6.212 -
   6.213 -subsubsection{*Quotient *}
   6.214 -
   6.215 -lemma div_nat_number_of [simp]:
   6.216 -     "(number_of v :: nat)  div  number_of v' =  
   6.217 -          (if neg (number_of v :: int) then 0  
   6.218 -           else nat (number_of v div number_of v'))"
   6.219 -  unfolding nat_number_of_def number_of_is_id neg_def
   6.220 -  by (simp add: nat_div_distrib)
   6.221 -
   6.222 -lemma one_div_nat_number_of [simp]:
   6.223 -     "Suc 0 div number_of v' = nat (1 div number_of v')" 
   6.224 -by (simp del: nat_numeral_1_eq_1 add: numeral_1_eq_Suc_0 [symmetric]) 
   6.225 -
   6.226 -
   6.227 -subsubsection{*Remainder *}
   6.228 -
   6.229 -lemma mod_nat_number_of [simp]:
   6.230 -     "(number_of v :: nat)  mod  number_of v' =  
   6.231 -        (if neg (number_of v :: int) then 0  
   6.232 -         else if neg (number_of v' :: int) then number_of v  
   6.233 -         else nat (number_of v mod number_of v'))"
   6.234 -  unfolding nat_number_of_def number_of_is_id neg_def
   6.235 -  by (simp add: nat_mod_distrib)
   6.236 -
   6.237 -lemma one_mod_nat_number_of [simp]:
   6.238 -     "Suc 0 mod number_of v' =  
   6.239 -        (if neg (number_of v' :: int) then Suc 0
   6.240 -         else nat (1 mod number_of v'))"
   6.241 -by (simp del: nat_numeral_1_eq_1 add: numeral_1_eq_Suc_0 [symmetric]) 
   6.242 -
   6.243 -
   6.244 -subsubsection{* Divisibility *}
   6.245 -
   6.246 -lemmas dvd_eq_mod_eq_0_number_of =
   6.247 -  dvd_eq_mod_eq_0 [of "number_of x" "number_of y", standard]
   6.248 -
   6.249 -declare dvd_eq_mod_eq_0_number_of [simp]
   6.250 -
   6.251 -ML
   6.252 -{*
   6.253 -val nat_number_of_def = thm"nat_number_of_def";
   6.254 -
   6.255 -val nat_number_of = thm"nat_number_of";
   6.256 -val nat_numeral_0_eq_0 = thm"nat_numeral_0_eq_0";
   6.257 -val nat_numeral_1_eq_1 = thm"nat_numeral_1_eq_1";
   6.258 -val numeral_1_eq_Suc_0 = thm"numeral_1_eq_Suc_0";
   6.259 -val numeral_2_eq_2 = thm"numeral_2_eq_2";
   6.260 -val nat_div_distrib = thm"nat_div_distrib";
   6.261 -val nat_mod_distrib = thm"nat_mod_distrib";
   6.262 -val int_nat_number_of = thm"int_nat_number_of";
   6.263 -val Suc_nat_eq_nat_zadd1 = thm"Suc_nat_eq_nat_zadd1";
   6.264 -val Suc_nat_number_of_add = thm"Suc_nat_number_of_add";
   6.265 -val Suc_nat_number_of = thm"Suc_nat_number_of";
   6.266 -val add_nat_number_of = thm"add_nat_number_of";
   6.267 -val diff_nat_eq_if = thm"diff_nat_eq_if";
   6.268 -val diff_nat_number_of = thm"diff_nat_number_of";
   6.269 -val mult_nat_number_of = thm"mult_nat_number_of";
   6.270 -val div_nat_number_of = thm"div_nat_number_of";
   6.271 -val mod_nat_number_of = thm"mod_nat_number_of";
   6.272 -*}
   6.273 -
   6.274 -
   6.275 -subsection{*Comparisons*}
   6.276 -
   6.277 -subsubsection{*Equals (=) *}
   6.278 -
   6.279 -lemma eq_nat_nat_iff:
   6.280 -     "[| (0::int) <= z;  0 <= z' |] ==> (nat z = nat z') = (z=z')"
   6.281 -by (auto elim!: nonneg_eq_int)
   6.282 -
   6.283 -lemma eq_nat_number_of [simp]:
   6.284 -     "((number_of v :: nat) = number_of v') =  
   6.285 -      (if neg (number_of v :: int) then (number_of v' :: int) \<le> 0
   6.286 -       else if neg (number_of v' :: int) then (number_of v :: int) = 0
   6.287 -       else v = v')"
   6.288 -  unfolding nat_number_of_def number_of_is_id neg_def
   6.289 -  by auto
   6.290 -
   6.291 -
   6.292 -subsubsection{*Less-than (<) *}
   6.293 -
   6.294 -lemma less_nat_number_of [simp]:
   6.295 -  "(number_of v :: nat) < number_of v' \<longleftrightarrow>
   6.296 -    (if v < v' then Int.Pls < v' else False)"
   6.297 -  unfolding nat_number_of_def number_of_is_id numeral_simps
   6.298 -  by auto
   6.299 -
   6.300 -
   6.301 -subsubsection{*Less-than-or-equal *}
   6.302 -
   6.303 -lemma le_nat_number_of [simp]:
   6.304 -  "(number_of v :: nat) \<le> number_of v' \<longleftrightarrow>
   6.305 -    (if v \<le> v' then True else v \<le> Int.Pls)"
   6.306 -  unfolding nat_number_of_def number_of_is_id numeral_simps
   6.307 -  by auto
   6.308 -
   6.309 -(*Maps #n to n for n = 0, 1, 2*)
   6.310 -lemmas numerals = nat_numeral_0_eq_0 nat_numeral_1_eq_1 numeral_2_eq_2
   6.311 -
   6.312 -
   6.313 -subsection{*Powers with Numeric Exponents*}
   6.314 -
   6.315 -text{*We cannot refer to the number @{term 2} in @{text Ring_and_Field.thy}.
   6.316 -We cannot prove general results about the numeral @{term "-1"}, so we have to
   6.317 -use @{term "- 1"} instead.*}
   6.318 -
   6.319 -lemma power2_eq_square: "(a::'a::recpower)\<twosuperior> = a * a"
   6.320 -  by (simp add: numeral_2_eq_2 Power.power_Suc)
   6.321 -
   6.322 -lemma zero_power2 [simp]: "(0::'a::{semiring_1,recpower})\<twosuperior> = 0"
   6.323 -  by (simp add: power2_eq_square)
   6.324 -
   6.325 -lemma one_power2 [simp]: "(1::'a::{semiring_1,recpower})\<twosuperior> = 1"
   6.326 -  by (simp add: power2_eq_square)
   6.327 -
   6.328 -lemma power3_eq_cube: "(x::'a::recpower) ^ 3 = x * x * x"
   6.329 -  apply (subgoal_tac "3 = Suc (Suc (Suc 0))")
   6.330 -  apply (erule ssubst)
   6.331 -  apply (simp add: power_Suc mult_ac)
   6.332 -  apply (unfold nat_number_of_def)
   6.333 -  apply (subst nat_eq_iff)
   6.334 -  apply simp
   6.335 -done
   6.336 -
   6.337 -text{*Squares of literal numerals will be evaluated.*}
   6.338 -lemmas power2_eq_square_number_of =
   6.339 -    power2_eq_square [of "number_of w", standard]
   6.340 -declare power2_eq_square_number_of [simp]
   6.341 -
   6.342 -
   6.343 -lemma zero_le_power2[simp]: "0 \<le> (a\<twosuperior>::'a::{ordered_idom,recpower})"
   6.344 -  by (simp add: power2_eq_square)
   6.345 -
   6.346 -lemma zero_less_power2[simp]:
   6.347 -     "(0 < a\<twosuperior>) = (a \<noteq> (0::'a::{ordered_idom,recpower}))"
   6.348 -  by (force simp add: power2_eq_square zero_less_mult_iff linorder_neq_iff)
   6.349 -
   6.350 -lemma power2_less_0[simp]:
   6.351 -  fixes a :: "'a::{ordered_idom,recpower}"
   6.352 -  shows "~ (a\<twosuperior> < 0)"
   6.353 -by (force simp add: power2_eq_square mult_less_0_iff) 
   6.354 -
   6.355 -lemma zero_eq_power2[simp]:
   6.356 -     "(a\<twosuperior> = 0) = (a = (0::'a::{ordered_idom,recpower}))"
   6.357 -  by (force simp add: power2_eq_square mult_eq_0_iff)
   6.358 -
   6.359 -lemma abs_power2[simp]:
   6.360 -     "abs(a\<twosuperior>) = (a\<twosuperior>::'a::{ordered_idom,recpower})"
   6.361 -  by (simp add: power2_eq_square abs_mult abs_mult_self)
   6.362 -
   6.363 -lemma power2_abs[simp]:
   6.364 -     "(abs a)\<twosuperior> = (a\<twosuperior>::'a::{ordered_idom,recpower})"
   6.365 -  by (simp add: power2_eq_square abs_mult_self)
   6.366 -
   6.367 -lemma power2_minus[simp]:
   6.368 -     "(- a)\<twosuperior> = (a\<twosuperior>::'a::{comm_ring_1,recpower})"
   6.369 -  by (simp add: power2_eq_square)
   6.370 -
   6.371 -lemma power2_le_imp_le:
   6.372 -  fixes x y :: "'a::{ordered_semidom,recpower}"
   6.373 -  shows "\<lbrakk>x\<twosuperior> \<le> y\<twosuperior>; 0 \<le> y\<rbrakk> \<Longrightarrow> x \<le> y"
   6.374 -unfolding numeral_2_eq_2 by (rule power_le_imp_le_base)
   6.375 -
   6.376 -lemma power2_less_imp_less:
   6.377 -  fixes x y :: "'a::{ordered_semidom,recpower}"
   6.378 -  shows "\<lbrakk>x\<twosuperior> < y\<twosuperior>; 0 \<le> y\<rbrakk> \<Longrightarrow> x < y"
   6.379 -by (rule power_less_imp_less_base)
   6.380 -
   6.381 -lemma power2_eq_imp_eq:
   6.382 -  fixes x y :: "'a::{ordered_semidom,recpower}"
   6.383 -  shows "\<lbrakk>x\<twosuperior> = y\<twosuperior>; 0 \<le> x; 0 \<le> y\<rbrakk> \<Longrightarrow> x = y"
   6.384 -unfolding numeral_2_eq_2 by (erule (2) power_eq_imp_eq_base, simp)
   6.385 -
   6.386 -lemma power_minus1_even[simp]: "(- 1) ^ (2*n) = (1::'a::{comm_ring_1,recpower})"
   6.387 -proof (induct n)
   6.388 -  case 0 show ?case by simp
   6.389 -next
   6.390 -  case (Suc n) then show ?case by (simp add: power_Suc power_add)
   6.391 -qed
   6.392 -
   6.393 -lemma power_minus1_odd: "(- 1) ^ Suc(2*n) = -(1::'a::{comm_ring_1,recpower})"
   6.394 -  by (simp add: power_Suc) 
   6.395 -
   6.396 -lemma power_even_eq: "(a::'a::recpower) ^ (2*n) = (a^n)^2"
   6.397 -by (subst mult_commute) (simp add: power_mult)
   6.398 -
   6.399 -lemma power_odd_eq: "(a::int) ^ Suc(2*n) = a * (a^n)^2"
   6.400 -by (simp add: power_even_eq) 
   6.401 -
   6.402 -lemma power_minus_even [simp]:
   6.403 -     "(-a) ^ (2*n) = (a::'a::{comm_ring_1,recpower}) ^ (2*n)"
   6.404 -by (simp add: power_minus1_even power_minus [of a]) 
   6.405 -
   6.406 -lemma zero_le_even_power'[simp]:
   6.407 -     "0 \<le> (a::'a::{ordered_idom,recpower}) ^ (2*n)"
   6.408 -proof (induct "n")
   6.409 -  case 0
   6.410 -    show ?case by (simp add: zero_le_one)
   6.411 -next
   6.412 -  case (Suc n)
   6.413 -    have "a ^ (2 * Suc n) = (a*a) * a ^ (2*n)" 
   6.414 -      by (simp add: mult_ac power_add power2_eq_square)
   6.415 -    thus ?case
   6.416 -      by (simp add: prems zero_le_mult_iff)
   6.417 -qed
   6.418 -
   6.419 -lemma odd_power_less_zero:
   6.420 -     "(a::'a::{ordered_idom,recpower}) < 0 ==> a ^ Suc(2*n) < 0"
   6.421 -proof (induct "n")
   6.422 -  case 0
   6.423 -  then show ?case by simp
   6.424 -next
   6.425 -  case (Suc n)
   6.426 -  have "a ^ Suc (2 * Suc n) = (a*a) * a ^ Suc(2*n)"
   6.427 -    by (simp add: mult_ac power_add power2_eq_square)
   6.428 -  thus ?case
   6.429 -    by (simp del: power_Suc add: prems mult_less_0_iff mult_neg_neg)
   6.430 -qed
   6.431 -
   6.432 -lemma odd_0_le_power_imp_0_le:
   6.433 -     "0 \<le> a  ^ Suc(2*n) ==> 0 \<le> (a::'a::{ordered_idom,recpower})"
   6.434 -apply (insert odd_power_less_zero [of a n]) 
   6.435 -apply (force simp add: linorder_not_less [symmetric]) 
   6.436 -done
   6.437 -
   6.438 -text{*Simprules for comparisons where common factors can be cancelled.*}
   6.439 -lemmas zero_compare_simps =
   6.440 -    add_strict_increasing add_strict_increasing2 add_increasing
   6.441 -    zero_le_mult_iff zero_le_divide_iff 
   6.442 -    zero_less_mult_iff zero_less_divide_iff 
   6.443 -    mult_le_0_iff divide_le_0_iff 
   6.444 -    mult_less_0_iff divide_less_0_iff 
   6.445 -    zero_le_power2 power2_less_0
   6.446 -
   6.447 -subsubsection{*Nat *}
   6.448 -
   6.449 -lemma Suc_pred': "0 < n ==> n = Suc(n - 1)"
   6.450 -by (simp add: numerals)
   6.451 -
   6.452 -(*Expresses a natural number constant as the Suc of another one.
   6.453 -  NOT suitable for rewriting because n recurs in the condition.*)
   6.454 -lemmas expand_Suc = Suc_pred' [of "number_of v", standard]
   6.455 -
   6.456 -subsubsection{*Arith *}
   6.457 -
   6.458 -lemma Suc_eq_add_numeral_1: "Suc n = n + 1"
   6.459 -by (simp add: numerals)
   6.460 -
   6.461 -lemma Suc_eq_add_numeral_1_left: "Suc n = 1 + n"
   6.462 -by (simp add: numerals)
   6.463 -
   6.464 -(* These two can be useful when m = number_of... *)
   6.465 -
   6.466 -lemma add_eq_if: "(m::nat) + n = (if m=0 then n else Suc ((m - 1) + n))"
   6.467 -  unfolding One_nat_def by (cases m) simp_all
   6.468 -
   6.469 -lemma mult_eq_if: "(m::nat) * n = (if m=0 then 0 else n + ((m - 1) * n))"
   6.470 -  unfolding One_nat_def by (cases m) simp_all
   6.471 -
   6.472 -lemma power_eq_if: "(p ^ m :: nat) = (if m=0 then 1 else p * (p ^ (m - 1)))"
   6.473 -  unfolding One_nat_def by (cases m) simp_all
   6.474 -
   6.475 -
   6.476 -subsection{*Comparisons involving (0::nat) *}
   6.477 -
   6.478 -text{*Simplification already does @{term "n<0"}, @{term "n\<le>0"} and @{term "0\<le>n"}.*}
   6.479 -
   6.480 -lemma eq_number_of_0 [simp]:
   6.481 -  "number_of v = (0::nat) \<longleftrightarrow> v \<le> Int.Pls"
   6.482 -  unfolding nat_number_of_def number_of_is_id numeral_simps
   6.483 -  by auto
   6.484 -
   6.485 -lemma eq_0_number_of [simp]:
   6.486 -  "(0::nat) = number_of v \<longleftrightarrow> v \<le> Int.Pls"
   6.487 -by (rule trans [OF eq_sym_conv eq_number_of_0])
   6.488 -
   6.489 -lemma less_0_number_of [simp]:
   6.490 -   "(0::nat) < number_of v \<longleftrightarrow> Int.Pls < v"
   6.491 -  unfolding nat_number_of_def number_of_is_id numeral_simps
   6.492 -  by simp
   6.493 -
   6.494 -lemma neg_imp_number_of_eq_0: "neg (number_of v :: int) ==> number_of v = (0::nat)"
   6.495 -by (simp del: nat_numeral_0_eq_0 add: nat_numeral_0_eq_0 [symmetric])
   6.496 -
   6.497 -
   6.498 -
   6.499 -subsection{*Comparisons involving  @{term Suc} *}
   6.500 -
   6.501 -lemma eq_number_of_Suc [simp]:
   6.502 -     "(number_of v = Suc n) =  
   6.503 -        (let pv = number_of (Int.pred v) in  
   6.504 -         if neg pv then False else nat pv = n)"
   6.505 -apply (simp only: simp_thms Let_def neg_eq_less_0 linorder_not_less 
   6.506 -                  number_of_pred nat_number_of_def 
   6.507 -            split add: split_if)
   6.508 -apply (rule_tac x = "number_of v" in spec)
   6.509 -apply (auto simp add: nat_eq_iff)
   6.510 -done
   6.511 -
   6.512 -lemma Suc_eq_number_of [simp]:
   6.513 -     "(Suc n = number_of v) =  
   6.514 -        (let pv = number_of (Int.pred v) in  
   6.515 -         if neg pv then False else nat pv = n)"
   6.516 -by (rule trans [OF eq_sym_conv eq_number_of_Suc])
   6.517 -
   6.518 -lemma less_number_of_Suc [simp]:
   6.519 -     "(number_of v < Suc n) =  
   6.520 -        (let pv = number_of (Int.pred v) in  
   6.521 -         if neg pv then True else nat pv < n)"
   6.522 -apply (simp only: simp_thms Let_def neg_eq_less_0 linorder_not_less 
   6.523 -                  number_of_pred nat_number_of_def  
   6.524 -            split add: split_if)
   6.525 -apply (rule_tac x = "number_of v" in spec)
   6.526 -apply (auto simp add: nat_less_iff)
   6.527 -done
   6.528 -
   6.529 -lemma less_Suc_number_of [simp]:
   6.530 -     "(Suc n < number_of v) =  
   6.531 -        (let pv = number_of (Int.pred v) in  
   6.532 -         if neg pv then False else n < nat pv)"
   6.533 -apply (simp only: simp_thms Let_def neg_eq_less_0 linorder_not_less 
   6.534 -                  number_of_pred nat_number_of_def
   6.535 -            split add: split_if)
   6.536 -apply (rule_tac x = "number_of v" in spec)
   6.537 -apply (auto simp add: zless_nat_eq_int_zless)
   6.538 -done
   6.539 -
   6.540 -lemma le_number_of_Suc [simp]:
   6.541 -     "(number_of v <= Suc n) =  
   6.542 -        (let pv = number_of (Int.pred v) in  
   6.543 -         if neg pv then True else nat pv <= n)"
   6.544 -by (simp add: Let_def less_Suc_number_of linorder_not_less [symmetric])
   6.545 -
   6.546 -lemma le_Suc_number_of [simp]:
   6.547 -     "(Suc n <= number_of v) =  
   6.548 -        (let pv = number_of (Int.pred v) in  
   6.549 -         if neg pv then False else n <= nat pv)"
   6.550 -by (simp add: Let_def less_number_of_Suc linorder_not_less [symmetric])
   6.551 -
   6.552 -
   6.553 -lemma eq_number_of_Pls_Min: "(Numeral0 ::int) ~= number_of Int.Min"
   6.554 -by auto
   6.555 -
   6.556 -
   6.557 -
   6.558 -subsection{*Max and Min Combined with @{term Suc} *}
   6.559 -
   6.560 -lemma max_number_of_Suc [simp]:
   6.561 -     "max (Suc n) (number_of v) =  
   6.562 -        (let pv = number_of (Int.pred v) in  
   6.563 -         if neg pv then Suc n else Suc(max n (nat pv)))"
   6.564 -apply (simp only: Let_def neg_eq_less_0 number_of_pred nat_number_of_def 
   6.565 -            split add: split_if nat.split)
   6.566 -apply (rule_tac x = "number_of v" in spec) 
   6.567 -apply auto
   6.568 -done
   6.569 - 
   6.570 -lemma max_Suc_number_of [simp]:
   6.571 -     "max (number_of v) (Suc n) =  
   6.572 -        (let pv = number_of (Int.pred v) in  
   6.573 -         if neg pv then Suc n else Suc(max (nat pv) n))"
   6.574 -apply (simp only: Let_def neg_eq_less_0 number_of_pred nat_number_of_def 
   6.575 -            split add: split_if nat.split)
   6.576 -apply (rule_tac x = "number_of v" in spec) 
   6.577 -apply auto
   6.578 -done
   6.579 - 
   6.580 -lemma min_number_of_Suc [simp]:
   6.581 -     "min (Suc n) (number_of v) =  
   6.582 -        (let pv = number_of (Int.pred v) in  
   6.583 -         if neg pv then 0 else Suc(min n (nat pv)))"
   6.584 -apply (simp only: Let_def neg_eq_less_0 number_of_pred nat_number_of_def 
   6.585 -            split add: split_if nat.split)
   6.586 -apply (rule_tac x = "number_of v" in spec) 
   6.587 -apply auto
   6.588 -done
   6.589 - 
   6.590 -lemma min_Suc_number_of [simp]:
   6.591 -     "min (number_of v) (Suc n) =  
   6.592 -        (let pv = number_of (Int.pred v) in  
   6.593 -         if neg pv then 0 else Suc(min (nat pv) n))"
   6.594 -apply (simp only: Let_def neg_eq_less_0 number_of_pred nat_number_of_def 
   6.595 -            split add: split_if nat.split)
   6.596 -apply (rule_tac x = "number_of v" in spec) 
   6.597 -apply auto
   6.598 -done
   6.599 - 
   6.600 -subsection{*Literal arithmetic involving powers*}
   6.601 -
   6.602 -lemma nat_power_eq: "(0::int) <= z ==> nat (z^n) = nat z ^ n"
   6.603 -apply (induct "n")
   6.604 -apply (simp_all (no_asm_simp) add: nat_mult_distrib)
   6.605 -done
   6.606 -
   6.607 -lemma power_nat_number_of:
   6.608 -     "(number_of v :: nat) ^ n =  
   6.609 -       (if neg (number_of v :: int) then 0^n else nat ((number_of v :: int) ^ n))"
   6.610 -by (simp only: simp_thms neg_nat not_neg_eq_ge_0 nat_number_of_def nat_power_eq
   6.611 -         split add: split_if cong: imp_cong)
   6.612 -
   6.613 -
   6.614 -lemmas power_nat_number_of_number_of = power_nat_number_of [of _ "number_of w", standard]
   6.615 -declare power_nat_number_of_number_of [simp]
   6.616 -
   6.617 -
   6.618 -
   6.619 -text{*For arbitrary rings*}
   6.620 -
   6.621 -lemma power_number_of_even:
   6.622 -  fixes z :: "'a::{number_ring,recpower}"
   6.623 -  shows "z ^ number_of (Int.Bit0 w) = (let w = z ^ (number_of w) in w * w)"
   6.624 -unfolding Let_def nat_number_of_def number_of_Bit0
   6.625 -apply (rule_tac x = "number_of w" in spec, clarify)
   6.626 -apply (case_tac " (0::int) <= x")
   6.627 -apply (auto simp add: nat_mult_distrib power_even_eq power2_eq_square)
   6.628 -done
   6.629 -
   6.630 -lemma power_number_of_odd:
   6.631 -  fixes z :: "'a::{number_ring,recpower}"
   6.632 -  shows "z ^ number_of (Int.Bit1 w) = (if (0::int) <= number_of w
   6.633 -     then (let w = z ^ (number_of w) in z * w * w) else 1)"
   6.634 -unfolding Let_def nat_number_of_def number_of_Bit1
   6.635 -apply (rule_tac x = "number_of w" in spec, auto)
   6.636 -apply (simp only: nat_add_distrib nat_mult_distrib)
   6.637 -apply simp
   6.638 -apply (auto simp add: nat_add_distrib nat_mult_distrib power_even_eq power2_eq_square neg_nat power_Suc)
   6.639 -done
   6.640 -
   6.641 -lemmas zpower_number_of_even = power_number_of_even [where 'a=int]
   6.642 -lemmas zpower_number_of_odd = power_number_of_odd [where 'a=int]
   6.643 -
   6.644 -lemmas power_number_of_even_number_of [simp] =
   6.645 -    power_number_of_even [of "number_of v", standard]
   6.646 -
   6.647 -lemmas power_number_of_odd_number_of [simp] =
   6.648 -    power_number_of_odd [of "number_of v", standard]
   6.649 -
   6.650 -
   6.651 -
   6.652 -ML
   6.653 -{*
   6.654 -val numeral_ss = @{simpset} addsimps @{thms numerals};
   6.655 -
   6.656 -val nat_bin_arith_setup =
   6.657 - Lin_Arith.map_data
   6.658 -   (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
   6.659 -     {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms,
   6.660 -      inj_thms = inj_thms,
   6.661 -      lessD = lessD, neqE = neqE,
   6.662 -      simpset = simpset addsimps @{thms neg_simps} @
   6.663 -        [@{thm Suc_nat_number_of}, @{thm int_nat_number_of}]})
   6.664 -*}
   6.665 -
   6.666 -declaration {* K nat_bin_arith_setup *}
   6.667 -
   6.668 -(* Enable arith to deal with div/mod k where k is a numeral: *)
   6.669 -declare split_div[of _ _ "number_of k", standard, arith_split]
   6.670 -declare split_mod[of _ _ "number_of k", standard, arith_split]
   6.671 -
   6.672 -lemma nat_number_of_Pls: "Numeral0 = (0::nat)"
   6.673 -  by (simp add: number_of_Pls nat_number_of_def)
   6.674 -
   6.675 -lemma nat_number_of_Min: "number_of Int.Min = (0::nat)"
   6.676 -  apply (simp only: number_of_Min nat_number_of_def nat_zminus_int)
   6.677 -  done
   6.678 -
   6.679 -lemma nat_number_of_Bit0:
   6.680 -    "number_of (Int.Bit0 w) = (let n::nat = number_of w in n + n)"
   6.681 -  unfolding nat_number_of_def number_of_is_id numeral_simps Let_def
   6.682 -  by auto
   6.683 -
   6.684 -lemma nat_number_of_Bit1:
   6.685 -  "number_of (Int.Bit1 w) =
   6.686 -    (if neg (number_of w :: int) then 0
   6.687 -     else let n = number_of w in Suc (n + n))"
   6.688 -  unfolding nat_number_of_def number_of_is_id numeral_simps neg_def Let_def
   6.689 -  by auto
   6.690 -
   6.691 -lemmas nat_number =
   6.692 -  nat_number_of_Pls nat_number_of_Min
   6.693 -  nat_number_of_Bit0 nat_number_of_Bit1
   6.694 -
   6.695 -lemma Let_Suc [simp]: "Let (Suc n) f == f (Suc n)"
   6.696 -  by (simp add: Let_def)
   6.697 -
   6.698 -lemma power_m1_even: "(-1) ^ (2*n) = (1::'a::{number_ring,recpower})"
   6.699 -by (simp add: power_mult power_Suc); 
   6.700 -
   6.701 -lemma power_m1_odd: "(-1) ^ Suc(2*n) = (-1::'a::{number_ring,recpower})"
   6.702 -by (simp add: power_mult power_Suc); 
   6.703 -
   6.704 -
   6.705 -subsection{*Literal arithmetic and @{term of_nat}*}
   6.706 -
   6.707 -lemma of_nat_double:
   6.708 -     "0 \<le> x ==> of_nat (nat (2 * x)) = of_nat (nat x) + of_nat (nat x)"
   6.709 -by (simp only: mult_2 nat_add_distrib of_nat_add) 
   6.710 -
   6.711 -lemma nat_numeral_m1_eq_0: "-1 = (0::nat)"
   6.712 -by (simp only: nat_number_of_def)
   6.713 -
   6.714 -lemma of_nat_number_of_lemma:
   6.715 -     "of_nat (number_of v :: nat) =  
   6.716 -         (if 0 \<le> (number_of v :: int) 
   6.717 -          then (number_of v :: 'a :: number_ring)
   6.718 -          else 0)"
   6.719 -by (simp add: int_number_of_def nat_number_of_def number_of_eq of_nat_nat);
   6.720 -
   6.721 -lemma of_nat_number_of_eq [simp]:
   6.722 -     "of_nat (number_of v :: nat) =  
   6.723 -         (if neg (number_of v :: int) then 0  
   6.724 -          else (number_of v :: 'a :: number_ring))"
   6.725 -by (simp only: of_nat_number_of_lemma neg_def, simp) 
   6.726 -
   6.727 -
   6.728 -subsection {*Lemmas for the Combination and Cancellation Simprocs*}
   6.729 -
   6.730 -lemma nat_number_of_add_left:
   6.731 -     "number_of v + (number_of v' + (k::nat)) =  
   6.732 -         (if neg (number_of v :: int) then number_of v' + k  
   6.733 -          else if neg (number_of v' :: int) then number_of v + k  
   6.734 -          else number_of (v + v') + k)"
   6.735 -  unfolding nat_number_of_def number_of_is_id neg_def
   6.736 -  by auto
   6.737 -
   6.738 -lemma nat_number_of_mult_left:
   6.739 -     "number_of v * (number_of v' * (k::nat)) =  
   6.740 -         (if v < Int.Pls then 0
   6.741 -          else number_of (v * v') * k)"
   6.742 -by simp
   6.743 -
   6.744 -
   6.745 -subsubsection{*For @{text combine_numerals}*}
   6.746 -
   6.747 -lemma left_add_mult_distrib: "i*u + (j*u + k) = (i+j)*u + (k::nat)"
   6.748 -by (simp add: add_mult_distrib)
   6.749 -
   6.750 -
   6.751 -subsubsection{*For @{text cancel_numerals}*}
   6.752 -
   6.753 -lemma nat_diff_add_eq1:
   6.754 -     "j <= (i::nat) ==> ((i*u + m) - (j*u + n)) = (((i-j)*u + m) - n)"
   6.755 -by (simp split add: nat_diff_split add: add_mult_distrib)
   6.756 -
   6.757 -lemma nat_diff_add_eq2:
   6.758 -     "i <= (j::nat) ==> ((i*u + m) - (j*u + n)) = (m - ((j-i)*u + n))"
   6.759 -by (simp split add: nat_diff_split add: add_mult_distrib)
   6.760 -
   6.761 -lemma nat_eq_add_iff1:
   6.762 -     "j <= (i::nat) ==> (i*u + m = j*u + n) = ((i-j)*u + m = n)"
   6.763 -by (auto split add: nat_diff_split simp add: add_mult_distrib)
   6.764 -
   6.765 -lemma nat_eq_add_iff2:
   6.766 -     "i <= (j::nat) ==> (i*u + m = j*u + n) = (m = (j-i)*u + n)"
   6.767 -by (auto split add: nat_diff_split simp add: add_mult_distrib)
   6.768 -
   6.769 -lemma nat_less_add_iff1:
   6.770 -     "j <= (i::nat) ==> (i*u + m < j*u + n) = ((i-j)*u + m < n)"
   6.771 -by (auto split add: nat_diff_split simp add: add_mult_distrib)
   6.772 -
   6.773 -lemma nat_less_add_iff2:
   6.774 -     "i <= (j::nat) ==> (i*u + m < j*u + n) = (m < (j-i)*u + n)"
   6.775 -by (auto split add: nat_diff_split simp add: add_mult_distrib)
   6.776 -
   6.777 -lemma nat_le_add_iff1:
   6.778 -     "j <= (i::nat) ==> (i*u + m <= j*u + n) = ((i-j)*u + m <= n)"
   6.779 -by (auto split add: nat_diff_split simp add: add_mult_distrib)
   6.780 -
   6.781 -lemma nat_le_add_iff2:
   6.782 -     "i <= (j::nat) ==> (i*u + m <= j*u + n) = (m <= (j-i)*u + n)"
   6.783 -by (auto split add: nat_diff_split simp add: add_mult_distrib)
   6.784 -
   6.785 -
   6.786 -subsubsection{*For @{text cancel_numeral_factors} *}
   6.787 -
   6.788 -lemma nat_mult_le_cancel1: "(0::nat) < k ==> (k*m <= k*n) = (m<=n)"
   6.789 -by auto
   6.790 -
   6.791 -lemma nat_mult_less_cancel1: "(0::nat) < k ==> (k*m < k*n) = (m<n)"
   6.792 -by auto
   6.793 -
   6.794 -lemma nat_mult_eq_cancel1: "(0::nat) < k ==> (k*m = k*n) = (m=n)"
   6.795 -by auto
   6.796 -
   6.797 -lemma nat_mult_div_cancel1: "(0::nat) < k ==> (k*m) div (k*n) = (m div n)"
   6.798 -by auto
   6.799 -
   6.800 -lemma nat_mult_dvd_cancel_disj[simp]:
   6.801 -  "(k*m) dvd (k*n) = (k=0 | m dvd (n::nat))"
   6.802 -by(auto simp: dvd_eq_mod_eq_0 mod_mult_distrib2[symmetric])
   6.803 -
   6.804 -lemma nat_mult_dvd_cancel1: "0 < k \<Longrightarrow> (k*m) dvd (k*n::nat) = (m dvd n)"
   6.805 -by(auto)
   6.806 -
   6.807 -
   6.808 -subsubsection{*For @{text cancel_factor} *}
   6.809 -
   6.810 -lemma nat_mult_le_cancel_disj: "(k*m <= k*n) = ((0::nat) < k --> m<=n)"
   6.811 -by auto
   6.812 -
   6.813 -lemma nat_mult_less_cancel_disj: "(k*m < k*n) = ((0::nat) < k & m<n)"
   6.814 -by auto
   6.815 -
   6.816 -lemma nat_mult_eq_cancel_disj: "(k*m = k*n) = (k = (0::nat) | m=n)"
   6.817 -by auto
   6.818 -
   6.819 -lemma nat_mult_div_cancel_disj[simp]:
   6.820 -     "(k*m) div (k*n) = (if k = (0::nat) then 0 else m div n)"
   6.821 -by (simp add: nat_mult_div_cancel1)
   6.822 -
   6.823 -
   6.824 -subsection {* Simprocs for the Naturals *}
   6.825 -
   6.826 -use "Tools/nat_simprocs.ML"
   6.827 -declaration {* K nat_simprocs_setup *}
   6.828 -
   6.829 -subsubsection{*For simplifying @{term "Suc m - K"} and  @{term "K - Suc m"}*}
   6.830 -
   6.831 -text{*Where K above is a literal*}
   6.832 -
   6.833 -lemma Suc_diff_eq_diff_pred: "Numeral0 < n ==> Suc m - n = m - (n - Numeral1)"
   6.834 -by (simp add: numeral_0_eq_0 numeral_1_eq_1 split add: nat_diff_split)
   6.835 -
   6.836 -text {*Now just instantiating @{text n} to @{text "number_of v"} does
   6.837 -  the right simplification, but with some redundant inequality
   6.838 -  tests.*}
   6.839 -lemma neg_number_of_pred_iff_0:
   6.840 -  "neg (number_of (Int.pred v)::int) = (number_of v = (0::nat))"
   6.841 -apply (subgoal_tac "neg (number_of (Int.pred v)) = (number_of v < Suc 0) ")
   6.842 -apply (simp only: less_Suc_eq_le le_0_eq)
   6.843 -apply (subst less_number_of_Suc, simp)
   6.844 -done
   6.845 -
   6.846 -text{*No longer required as a simprule because of the @{text inverse_fold}
   6.847 -   simproc*}
   6.848 -lemma Suc_diff_number_of:
   6.849 -     "Int.Pls < v ==>
   6.850 -      Suc m - (number_of v) = m - (number_of (Int.pred v))"
   6.851 -apply (subst Suc_diff_eq_diff_pred)
   6.852 -apply simp
   6.853 -apply (simp del: nat_numeral_1_eq_1)
   6.854 -apply (auto simp only: diff_nat_number_of less_0_number_of [symmetric]
   6.855 -                        neg_number_of_pred_iff_0)
   6.856 -done
   6.857 -
   6.858 -lemma diff_Suc_eq_diff_pred: "m - Suc n = (m - 1) - n"
   6.859 -by (simp add: numerals split add: nat_diff_split)
   6.860 -
   6.861 -
   6.862 -subsubsection{*For @{term nat_case} and @{term nat_rec}*}
   6.863 -
   6.864 -lemma nat_case_number_of [simp]:
   6.865 -     "nat_case a f (number_of v) =
   6.866 -        (let pv = number_of (Int.pred v) in
   6.867 -         if neg pv then a else f (nat pv))"
   6.868 -by (simp split add: nat.split add: Let_def neg_number_of_pred_iff_0)
   6.869 -
   6.870 -lemma nat_case_add_eq_if [simp]:
   6.871 -     "nat_case a f ((number_of v) + n) =
   6.872 -       (let pv = number_of (Int.pred v) in
   6.873 -         if neg pv then nat_case a f n else f (nat pv + n))"
   6.874 -apply (subst add_eq_if)
   6.875 -apply (simp split add: nat.split
   6.876 -            del: nat_numeral_1_eq_1
   6.877 -            add: nat_numeral_1_eq_1 [symmetric]
   6.878 -                 numeral_1_eq_Suc_0 [symmetric]
   6.879 -                 neg_number_of_pred_iff_0)
   6.880 -done
   6.881 -
   6.882 -lemma nat_rec_number_of [simp]:
   6.883 -     "nat_rec a f (number_of v) =
   6.884 -        (let pv = number_of (Int.pred v) in
   6.885 -         if neg pv then a else f (nat pv) (nat_rec a f (nat pv)))"
   6.886 -apply (case_tac " (number_of v) ::nat")
   6.887 -apply (simp_all (no_asm_simp) add: Let_def neg_number_of_pred_iff_0)
   6.888 -apply (simp split add: split_if_asm)
   6.889 -done
   6.890 -
   6.891 -lemma nat_rec_add_eq_if [simp]:
   6.892 -     "nat_rec a f (number_of v + n) =
   6.893 -        (let pv = number_of (Int.pred v) in
   6.894 -         if neg pv then nat_rec a f n
   6.895 -                   else f (nat pv + n) (nat_rec a f (nat pv + n)))"
   6.896 -apply (subst add_eq_if)
   6.897 -apply (simp split add: nat.split
   6.898 -            del: nat_numeral_1_eq_1
   6.899 -            add: nat_numeral_1_eq_1 [symmetric]
   6.900 -                 numeral_1_eq_Suc_0 [symmetric]
   6.901 -                 neg_number_of_pred_iff_0)
   6.902 -done
   6.903 -
   6.904 -
   6.905 -subsubsection{*Various Other Lemmas*}
   6.906 -
   6.907 -text {*Evens and Odds, for Mutilated Chess Board*}
   6.908 -
   6.909 -text{*Lemmas for specialist use, NOT as default simprules*}
   6.910 -lemma nat_mult_2: "2 * z = (z+z::nat)"
   6.911 -proof -
   6.912 -  have "2*z = (1 + 1)*z" by simp
   6.913 -  also have "... = z+z" by (simp add: left_distrib)
   6.914 -  finally show ?thesis .
   6.915 -qed
   6.916 -
   6.917 -lemma nat_mult_2_right: "z * 2 = (z+z::nat)"
   6.918 -by (subst mult_commute, rule nat_mult_2)
   6.919 -
   6.920 -text{*Case analysis on @{term "n<2"}*}
   6.921 -lemma less_2_cases: "(n::nat) < 2 ==> n = 0 | n = Suc 0"
   6.922 -by arith
   6.923 -
   6.924 -lemma div2_Suc_Suc [simp]: "Suc(Suc m) div 2 = Suc (m div 2)"
   6.925 -by arith
   6.926 -
   6.927 -lemma add_self_div_2 [simp]: "(m + m) div 2 = (m::nat)"
   6.928 -by (simp add: nat_mult_2 [symmetric])
   6.929 -
   6.930 -lemma mod2_Suc_Suc [simp]: "Suc(Suc(m)) mod 2 = m mod 2"
   6.931 -apply (subgoal_tac "m mod 2 < 2")
   6.932 -apply (erule less_2_cases [THEN disjE])
   6.933 -apply (simp_all (no_asm_simp) add: Let_def mod_Suc nat_1)
   6.934 -done
   6.935 -
   6.936 -lemma mod2_gr_0 [simp]: "!!m::nat. (0 < m mod 2) = (m mod 2 = 1)"
   6.937 -apply (subgoal_tac "m mod 2 < 2")
   6.938 -apply (force simp del: mod_less_divisor, simp)
   6.939 -done
   6.940 -
   6.941 -text{*Removal of Small Numerals: 0, 1 and (in additive positions) 2*}
   6.942 -
   6.943 -lemma add_2_eq_Suc [simp]: "2 + n = Suc (Suc n)"
   6.944 -by simp
   6.945 -
   6.946 -lemma add_2_eq_Suc' [simp]: "n + 2 = Suc (Suc n)"
   6.947 -by simp
   6.948 -
   6.949 -text{*Can be used to eliminate long strings of Sucs, but not by default*}
   6.950 -lemma Suc3_eq_add_3: "Suc (Suc (Suc n)) = 3 + n"
   6.951 -by simp
   6.952 -
   6.953 -
   6.954 -text{*These lemmas collapse some needless occurrences of Suc:
   6.955 -    at least three Sucs, since two and fewer are rewritten back to Suc again!
   6.956 -    We already have some rules to simplify operands smaller than 3.*}
   6.957 -
   6.958 -lemma div_Suc_eq_div_add3 [simp]: "m div (Suc (Suc (Suc n))) = m div (3+n)"
   6.959 -by (simp add: Suc3_eq_add_3)
   6.960 -
   6.961 -lemma mod_Suc_eq_mod_add3 [simp]: "m mod (Suc (Suc (Suc n))) = m mod (3+n)"
   6.962 -by (simp add: Suc3_eq_add_3)
   6.963 -
   6.964 -lemma Suc_div_eq_add3_div: "(Suc (Suc (Suc m))) div n = (3+m) div n"
   6.965 -by (simp add: Suc3_eq_add_3)
   6.966 -
   6.967 -lemma Suc_mod_eq_add3_mod: "(Suc (Suc (Suc m))) mod n = (3+m) mod n"
   6.968 -by (simp add: Suc3_eq_add_3)
   6.969 -
   6.970 -lemmas Suc_div_eq_add3_div_number_of =
   6.971 -    Suc_div_eq_add3_div [of _ "number_of v", standard]
   6.972 -declare Suc_div_eq_add3_div_number_of [simp]
   6.973 -
   6.974 -lemmas Suc_mod_eq_add3_mod_number_of =
   6.975 -    Suc_mod_eq_add3_mod [of _ "number_of v", standard]
   6.976 -declare Suc_mod_eq_add3_mod_number_of [simp]
   6.977 -
   6.978 -end
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/HOL/Nat_Numeral.thy	Wed Apr 15 15:30:39 2009 +0200
     7.3 @@ -0,0 +1,975 @@
     7.4 +(*  Title:      HOL/Nat_Numeral.thy
     7.5 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     7.6 +    Copyright   1999  University of Cambridge
     7.7 +*)
     7.8 +
     7.9 +header {* Binary numerals for the natural numbers *}
    7.10 +
    7.11 +theory Nat_Numeral
    7.12 +imports IntDiv
    7.13 +uses ("Tools/nat_simprocs.ML")
    7.14 +begin
    7.15 +
    7.16 +text {*
    7.17 +  Arithmetic for naturals is reduced to that for the non-negative integers.
    7.18 +*}
    7.19 +
    7.20 +instantiation nat :: number
    7.21 +begin
    7.22 +
    7.23 +definition
    7.24 +  nat_number_of_def [code inline, code del]: "number_of v = nat (number_of v)"
    7.25 +
    7.26 +instance ..
    7.27 +
    7.28 +end
    7.29 +
    7.30 +lemma [code post]:
    7.31 +  "nat (number_of v) = number_of v"
    7.32 +  unfolding nat_number_of_def ..
    7.33 +
    7.34 +abbreviation (xsymbols)
    7.35 +  power2 :: "'a::power => 'a"  ("(_\<twosuperior>)" [1000] 999) where
    7.36 +  "x\<twosuperior> == x^2"
    7.37 +
    7.38 +notation (latex output)
    7.39 +  power2  ("(_\<twosuperior>)" [1000] 999)
    7.40 +
    7.41 +notation (HTML output)
    7.42 +  power2  ("(_\<twosuperior>)" [1000] 999)
    7.43 +
    7.44 +
    7.45 +subsection {* Predicate for negative binary numbers *}
    7.46 +
    7.47 +definition neg  :: "int \<Rightarrow> bool" where
    7.48 +  "neg Z \<longleftrightarrow> Z < 0"
    7.49 +
    7.50 +lemma not_neg_int [simp]: "~ neg (of_nat n)"
    7.51 +by (simp add: neg_def)
    7.52 +
    7.53 +lemma neg_zminus_int [simp]: "neg (- (of_nat (Suc n)))"
    7.54 +by (simp add: neg_def neg_less_0_iff_less del: of_nat_Suc)
    7.55 +
    7.56 +lemmas neg_eq_less_0 = neg_def
    7.57 +
    7.58 +lemma not_neg_eq_ge_0: "(~neg x) = (0 \<le> x)"
    7.59 +by (simp add: neg_def linorder_not_less)
    7.60 +
    7.61 +text{*To simplify inequalities when Numeral1 can get simplified to 1*}
    7.62 +
    7.63 +lemma not_neg_0: "~ neg 0"
    7.64 +by (simp add: One_int_def neg_def)
    7.65 +
    7.66 +lemma not_neg_1: "~ neg 1"
    7.67 +by (simp add: neg_def linorder_not_less zero_le_one)
    7.68 +
    7.69 +lemma neg_nat: "neg z ==> nat z = 0"
    7.70 +by (simp add: neg_def order_less_imp_le) 
    7.71 +
    7.72 +lemma not_neg_nat: "~ neg z ==> of_nat (nat z) = z"
    7.73 +by (simp add: linorder_not_less neg_def)
    7.74 +
    7.75 +text {*
    7.76 +  If @{term Numeral0} is rewritten to 0 then this rule can't be applied:
    7.77 +  @{term Numeral0} IS @{term "number_of Pls"}
    7.78 +*}
    7.79 +
    7.80 +lemma not_neg_number_of_Pls: "~ neg (number_of Int.Pls)"
    7.81 +  by (simp add: neg_def)
    7.82 +
    7.83 +lemma neg_number_of_Min: "neg (number_of Int.Min)"
    7.84 +  by (simp add: neg_def)
    7.85 +
    7.86 +lemma neg_number_of_Bit0:
    7.87 +  "neg (number_of (Int.Bit0 w)) = neg (number_of w)"
    7.88 +  by (simp add: neg_def)
    7.89 +
    7.90 +lemma neg_number_of_Bit1:
    7.91 +  "neg (number_of (Int.Bit1 w)) = neg (number_of w)"
    7.92 +  by (simp add: neg_def)
    7.93 +
    7.94 +lemmas neg_simps [simp] =
    7.95 +  not_neg_0 not_neg_1
    7.96 +  not_neg_number_of_Pls neg_number_of_Min
    7.97 +  neg_number_of_Bit0 neg_number_of_Bit1
    7.98 +
    7.99 +
   7.100 +subsection{*Function @{term nat}: Coercion from Type @{typ int} to @{typ nat}*}
   7.101 +
   7.102 +declare nat_0 [simp] nat_1 [simp]
   7.103 +
   7.104 +lemma nat_number_of [simp]: "nat (number_of w) = number_of w"
   7.105 +by (simp add: nat_number_of_def)
   7.106 +
   7.107 +lemma nat_numeral_0_eq_0 [simp]: "Numeral0 = (0::nat)"
   7.108 +by (simp add: nat_number_of_def)
   7.109 +
   7.110 +lemma nat_numeral_1_eq_1 [simp]: "Numeral1 = (1::nat)"
   7.111 +by (simp add: nat_1 nat_number_of_def)
   7.112 +
   7.113 +lemma numeral_1_eq_Suc_0: "Numeral1 = Suc 0"
   7.114 +by (simp add: nat_numeral_1_eq_1)
   7.115 +
   7.116 +lemma numeral_2_eq_2: "2 = Suc (Suc 0)"
   7.117 +apply (unfold nat_number_of_def)
   7.118 +apply (rule nat_2)
   7.119 +done
   7.120 +
   7.121 +
   7.122 +subsection{*Function @{term int}: Coercion from Type @{typ nat} to @{typ int}*}
   7.123 +
   7.124 +lemma int_nat_number_of [simp]:
   7.125 +     "int (number_of v) =  
   7.126 +         (if neg (number_of v :: int) then 0  
   7.127 +          else (number_of v :: int))"
   7.128 +  unfolding nat_number_of_def number_of_is_id neg_def
   7.129 +  by simp
   7.130 +
   7.131 +
   7.132 +subsubsection{*Successor *}
   7.133 +
   7.134 +lemma Suc_nat_eq_nat_zadd1: "(0::int) <= z ==> Suc (nat z) = nat (1 + z)"
   7.135 +apply (rule sym)
   7.136 +apply (simp add: nat_eq_iff int_Suc)
   7.137 +done
   7.138 +
   7.139 +lemma Suc_nat_number_of_add:
   7.140 +     "Suc (number_of v + n) =  
   7.141 +        (if neg (number_of v :: int) then 1+n else number_of (Int.succ v) + n)"
   7.142 +  unfolding nat_number_of_def number_of_is_id neg_def numeral_simps
   7.143 +  by (simp add: Suc_nat_eq_nat_zadd1 add_ac)
   7.144 +
   7.145 +lemma Suc_nat_number_of [simp]:
   7.146 +     "Suc (number_of v) =  
   7.147 +        (if neg (number_of v :: int) then 1 else number_of (Int.succ v))"
   7.148 +apply (cut_tac n = 0 in Suc_nat_number_of_add)
   7.149 +apply (simp cong del: if_weak_cong)
   7.150 +done
   7.151 +
   7.152 +
   7.153 +subsubsection{*Addition *}
   7.154 +
   7.155 +lemma add_nat_number_of [simp]:
   7.156 +     "(number_of v :: nat) + number_of v' =  
   7.157 +         (if v < Int.Pls then number_of v'  
   7.158 +          else if v' < Int.Pls then number_of v  
   7.159 +          else number_of (v + v'))"
   7.160 +  unfolding nat_number_of_def number_of_is_id numeral_simps
   7.161 +  by (simp add: nat_add_distrib)
   7.162 +
   7.163 +lemma nat_number_of_add_1 [simp]:
   7.164 +  "number_of v + (1::nat) =
   7.165 +    (if v < Int.Pls then 1 else number_of (Int.succ v))"
   7.166 +  unfolding nat_number_of_def number_of_is_id numeral_simps
   7.167 +  by (simp add: nat_add_distrib)
   7.168 +
   7.169 +lemma nat_1_add_number_of [simp]:
   7.170 +  "(1::nat) + number_of v =
   7.171 +    (if v < Int.Pls then 1 else number_of (Int.succ v))"
   7.172 +  unfolding nat_number_of_def number_of_is_id numeral_simps
   7.173 +  by (simp add: nat_add_distrib)
   7.174 +
   7.175 +lemma nat_1_add_1 [simp]: "1 + 1 = (2::nat)"
   7.176 +  by (rule int_int_eq [THEN iffD1]) simp
   7.177 +
   7.178 +
   7.179 +subsubsection{*Subtraction *}
   7.180 +
   7.181 +lemma diff_nat_eq_if:
   7.182 +     "nat z - nat z' =  
   7.183 +        (if neg z' then nat z   
   7.184 +         else let d = z-z' in     
   7.185 +              if neg d then 0 else nat d)"
   7.186 +by (simp add: Let_def nat_diff_distrib [symmetric] neg_eq_less_0 not_neg_eq_ge_0)
   7.187 +
   7.188 +
   7.189 +lemma diff_nat_number_of [simp]: 
   7.190 +     "(number_of v :: nat) - number_of v' =  
   7.191 +        (if v' < Int.Pls then number_of v  
   7.192 +         else let d = number_of (v + uminus v') in     
   7.193 +              if neg d then 0 else nat d)"
   7.194 +  unfolding nat_number_of_def number_of_is_id numeral_simps neg_def
   7.195 +  by auto
   7.196 +
   7.197 +lemma nat_number_of_diff_1 [simp]:
   7.198 +  "number_of v - (1::nat) =
   7.199 +    (if v \<le> Int.Pls then 0 else number_of (Int.pred v))"
   7.200 +  unfolding nat_number_of_def number_of_is_id numeral_simps
   7.201 +  by auto
   7.202 +
   7.203 +
   7.204 +subsubsection{*Multiplication *}
   7.205 +
   7.206 +lemma mult_nat_number_of [simp]:
   7.207 +     "(number_of v :: nat) * number_of v' =  
   7.208 +       (if v < Int.Pls then 0 else number_of (v * v'))"
   7.209 +  unfolding nat_number_of_def number_of_is_id numeral_simps
   7.210 +  by (simp add: nat_mult_distrib)
   7.211 +
   7.212 +
   7.213 +subsubsection{*Quotient *}
   7.214 +
   7.215 +lemma div_nat_number_of [simp]:
   7.216 +     "(number_of v :: nat)  div  number_of v' =  
   7.217 +          (if neg (number_of v :: int) then 0  
   7.218 +           else nat (number_of v div number_of v'))"
   7.219 +  unfolding nat_number_of_def number_of_is_id neg_def
   7.220 +  by (simp add: nat_div_distrib)
   7.221 +
   7.222 +lemma one_div_nat_number_of [simp]:
   7.223 +     "Suc 0 div number_of v' = nat (1 div number_of v')" 
   7.224 +by (simp del: nat_numeral_1_eq_1 add: numeral_1_eq_Suc_0 [symmetric]) 
   7.225 +
   7.226 +
   7.227 +subsubsection{*Remainder *}
   7.228 +
   7.229 +lemma mod_nat_number_of [simp]:
   7.230 +     "(number_of v :: nat)  mod  number_of v' =  
   7.231 +        (if neg (number_of v :: int) then 0  
   7.232 +         else if neg (number_of v' :: int) then number_of v  
   7.233 +         else nat (number_of v mod number_of v'))"
   7.234 +  unfolding nat_number_of_def number_of_is_id neg_def
   7.235 +  by (simp add: nat_mod_distrib)
   7.236 +
   7.237 +lemma one_mod_nat_number_of [simp]:
   7.238 +     "Suc 0 mod number_of v' =  
   7.239 +        (if neg (number_of v' :: int) then Suc 0
   7.240 +         else nat (1 mod number_of v'))"
   7.241 +by (simp del: nat_numeral_1_eq_1 add: numeral_1_eq_Suc_0 [symmetric]) 
   7.242 +
   7.243 +
   7.244 +subsubsection{* Divisibility *}
   7.245 +
   7.246 +lemmas dvd_eq_mod_eq_0_number_of =
   7.247 +  dvd_eq_mod_eq_0 [of "number_of x" "number_of y", standard]
   7.248 +
   7.249 +declare dvd_eq_mod_eq_0_number_of [simp]
   7.250 +
   7.251 +ML
   7.252 +{*
   7.253 +val nat_number_of_def = thm"nat_number_of_def";
   7.254 +
   7.255 +val nat_number_of = thm"nat_number_of";
   7.256 +val nat_numeral_0_eq_0 = thm"nat_numeral_0_eq_0";
   7.257 +val nat_numeral_1_eq_1 = thm"nat_numeral_1_eq_1";
   7.258 +val numeral_1_eq_Suc_0 = thm"numeral_1_eq_Suc_0";
   7.259 +val numeral_2_eq_2 = thm"numeral_2_eq_2";
   7.260 +val nat_div_distrib = thm"nat_div_distrib";
   7.261 +val nat_mod_distrib = thm"nat_mod_distrib";
   7.262 +val int_nat_number_of = thm"int_nat_number_of";
   7.263 +val Suc_nat_eq_nat_zadd1 = thm"Suc_nat_eq_nat_zadd1";
   7.264 +val Suc_nat_number_of_add = thm"Suc_nat_number_of_add";
   7.265 +val Suc_nat_number_of = thm"Suc_nat_number_of";
   7.266 +val add_nat_number_of = thm"add_nat_number_of";
   7.267 +val diff_nat_eq_if = thm"diff_nat_eq_if";
   7.268 +val diff_nat_number_of = thm"diff_nat_number_of";
   7.269 +val mult_nat_number_of = thm"mult_nat_number_of";
   7.270 +val div_nat_number_of = thm"div_nat_number_of";
   7.271 +val mod_nat_number_of = thm"mod_nat_number_of";
   7.272 +*}
   7.273 +
   7.274 +
   7.275 +subsection{*Comparisons*}
   7.276 +
   7.277 +subsubsection{*Equals (=) *}
   7.278 +
   7.279 +lemma eq_nat_nat_iff:
   7.280 +     "[| (0::int) <= z;  0 <= z' |] ==> (nat z = nat z') = (z=z')"
   7.281 +by (auto elim!: nonneg_eq_int)
   7.282 +
   7.283 +lemma eq_nat_number_of [simp]:
   7.284 +     "((number_of v :: nat) = number_of v') =  
   7.285 +      (if neg (number_of v :: int) then (number_of v' :: int) \<le> 0
   7.286 +       else if neg (number_of v' :: int) then (number_of v :: int) = 0
   7.287 +       else v = v')"
   7.288 +  unfolding nat_number_of_def number_of_is_id neg_def
   7.289 +  by auto
   7.290 +
   7.291 +
   7.292 +subsubsection{*Less-than (<) *}
   7.293 +
   7.294 +lemma less_nat_number_of [simp]:
   7.295 +  "(number_of v :: nat) < number_of v' \<longleftrightarrow>
   7.296 +    (if v < v' then Int.Pls < v' else False)"
   7.297 +  unfolding nat_number_of_def number_of_is_id numeral_simps
   7.298 +  by auto
   7.299 +
   7.300 +
   7.301 +subsubsection{*Less-than-or-equal *}
   7.302 +
   7.303 +lemma le_nat_number_of [simp]:
   7.304 +  "(number_of v :: nat) \<le> number_of v' \<longleftrightarrow>
   7.305 +    (if v \<le> v' then True else v \<le> Int.Pls)"
   7.306 +  unfolding nat_number_of_def number_of_is_id numeral_simps
   7.307 +  by auto
   7.308 +
   7.309 +(*Maps #n to n for n = 0, 1, 2*)
   7.310 +lemmas numerals = nat_numeral_0_eq_0 nat_numeral_1_eq_1 numeral_2_eq_2
   7.311 +
   7.312 +
   7.313 +subsection{*Powers with Numeric Exponents*}
   7.314 +
   7.315 +text{*We cannot refer to the number @{term 2} in @{text Ring_and_Field.thy}.
   7.316 +We cannot prove general results about the numeral @{term "-1"}, so we have to
   7.317 +use @{term "- 1"} instead.*}
   7.318 +
   7.319 +lemma power2_eq_square: "(a::'a::recpower)\<twosuperior> = a * a"
   7.320 +  by (simp add: numeral_2_eq_2 Power.power_Suc)
   7.321 +
   7.322 +lemma zero_power2 [simp]: "(0::'a::{semiring_1,recpower})\<twosuperior> = 0"
   7.323 +  by (simp add: power2_eq_square)
   7.324 +
   7.325 +lemma one_power2 [simp]: "(1::'a::{semiring_1,recpower})\<twosuperior> = 1"
   7.326 +  by (simp add: power2_eq_square)
   7.327 +
   7.328 +lemma power3_eq_cube: "(x::'a::recpower) ^ 3 = x * x * x"
   7.329 +  apply (subgoal_tac "3 = Suc (Suc (Suc 0))")
   7.330 +  apply (erule ssubst)
   7.331 +  apply (simp add: power_Suc mult_ac)
   7.332 +  apply (unfold nat_number_of_def)
   7.333 +  apply (subst nat_eq_iff)
   7.334 +  apply simp
   7.335 +done
   7.336 +
   7.337 +text{*Squares of literal numerals will be evaluated.*}
   7.338 +lemmas power2_eq_square_number_of =
   7.339 +    power2_eq_square [of "number_of w", standard]
   7.340 +declare power2_eq_square_number_of [simp]
   7.341 +
   7.342 +
   7.343 +lemma zero_le_power2[simp]: "0 \<le> (a\<twosuperior>::'a::{ordered_idom,recpower})"
   7.344 +  by (simp add: power2_eq_square)
   7.345 +
   7.346 +lemma zero_less_power2[simp]:
   7.347 +     "(0 < a\<twosuperior>) = (a \<noteq> (0::'a::{ordered_idom,recpower}))"
   7.348 +  by (force simp add: power2_eq_square zero_less_mult_iff linorder_neq_iff)
   7.349 +
   7.350 +lemma power2_less_0[simp]:
   7.351 +  fixes a :: "'a::{ordered_idom,recpower}"
   7.352 +  shows "~ (a\<twosuperior> < 0)"
   7.353 +by (force simp add: power2_eq_square mult_less_0_iff) 
   7.354 +
   7.355 +lemma zero_eq_power2[simp]:
   7.356 +     "(a\<twosuperior> = 0) = (a = (0::'a::{ordered_idom,recpower}))"
   7.357 +  by (force simp add: power2_eq_square mult_eq_0_iff)
   7.358 +
   7.359 +lemma abs_power2[simp]:
   7.360 +     "abs(a\<twosuperior>) = (a\<twosuperior>::'a::{ordered_idom,recpower})"
   7.361 +  by (simp add: power2_eq_square abs_mult abs_mult_self)
   7.362 +
   7.363 +lemma power2_abs[simp]:
   7.364 +     "(abs a)\<twosuperior> = (a\<twosuperior>::'a::{ordered_idom,recpower})"
   7.365 +  by (simp add: power2_eq_square abs_mult_self)
   7.366 +
   7.367 +lemma power2_minus[simp]:
   7.368 +     "(- a)\<twosuperior> = (a\<twosuperior>::'a::{comm_ring_1,recpower})"
   7.369 +  by (simp add: power2_eq_square)
   7.370 +
   7.371 +lemma power2_le_imp_le:
   7.372 +  fixes x y :: "'a::{ordered_semidom,recpower}"
   7.373 +  shows "\<lbrakk>x\<twosuperior> \<le> y\<twosuperior>; 0 \<le> y\<rbrakk> \<Longrightarrow> x \<le> y"
   7.374 +unfolding numeral_2_eq_2 by (rule power_le_imp_le_base)
   7.375 +
   7.376 +lemma power2_less_imp_less:
   7.377 +  fixes x y :: "'a::{ordered_semidom,recpower}"
   7.378 +  shows "\<lbrakk>x\<twosuperior> < y\<twosuperior>; 0 \<le> y\<rbrakk> \<Longrightarrow> x < y"
   7.379 +by (rule power_less_imp_less_base)
   7.380 +
   7.381 +lemma power2_eq_imp_eq:
   7.382 +  fixes x y :: "'a::{ordered_semidom,recpower}"
   7.383 +  shows "\<lbrakk>x\<twosuperior> = y\<twosuperior>; 0 \<le> x; 0 \<le> y\<rbrakk> \<Longrightarrow> x = y"
   7.384 +unfolding numeral_2_eq_2 by (erule (2) power_eq_imp_eq_base, simp)
   7.385 +
   7.386 +lemma power_minus1_even[simp]: "(- 1) ^ (2*n) = (1::'a::{comm_ring_1,recpower})"
   7.387 +proof (induct n)
   7.388 +  case 0 show ?case by simp
   7.389 +next
   7.390 +  case (Suc n) then show ?case by (simp add: power_Suc power_add)
   7.391 +qed
   7.392 +
   7.393 +lemma power_minus1_odd: "(- 1) ^ Suc(2*n) = -(1::'a::{comm_ring_1,recpower})"
   7.394 +  by (simp add: power_Suc) 
   7.395 +
   7.396 +lemma power_even_eq: "(a::'a::recpower) ^ (2*n) = (a^n)^2"
   7.397 +by (subst mult_commute) (simp add: power_mult)
   7.398 +
   7.399 +lemma power_odd_eq: "(a::int) ^ Suc(2*n) = a * (a^n)^2"
   7.400 +by (simp add: power_even_eq) 
   7.401 +
   7.402 +lemma power_minus_even [simp]:
   7.403 +     "(-a) ^ (2*n) = (a::'a::{comm_ring_1,recpower}) ^ (2*n)"
   7.404 +by (simp add: power_minus1_even power_minus [of a]) 
   7.405 +
   7.406 +lemma zero_le_even_power'[simp]:
   7.407 +     "0 \<le> (a::'a::{ordered_idom,recpower}) ^ (2*n)"
   7.408 +proof (induct "n")
   7.409 +  case 0
   7.410 +    show ?case by (simp add: zero_le_one)
   7.411 +next
   7.412 +  case (Suc n)
   7.413 +    have "a ^ (2 * Suc n) = (a*a) * a ^ (2*n)" 
   7.414 +      by (simp add: mult_ac power_add power2_eq_square)
   7.415 +    thus ?case
   7.416 +      by (simp add: prems zero_le_mult_iff)
   7.417 +qed
   7.418 +
   7.419 +lemma odd_power_less_zero:
   7.420 +     "(a::'a::{ordered_idom,recpower}) < 0 ==> a ^ Suc(2*n) < 0"
   7.421 +proof (induct "n")
   7.422 +  case 0
   7.423 +  then show ?case by simp
   7.424 +next
   7.425 +  case (Suc n)
   7.426 +  have "a ^ Suc (2 * Suc n) = (a*a) * a ^ Suc(2*n)"
   7.427 +    by (simp add: mult_ac power_add power2_eq_square)
   7.428 +  thus ?case
   7.429 +    by (simp del: power_Suc add: prems mult_less_0_iff mult_neg_neg)
   7.430 +qed
   7.431 +
   7.432 +lemma odd_0_le_power_imp_0_le:
   7.433 +     "0 \<le> a  ^ Suc(2*n) ==> 0 \<le> (a::'a::{ordered_idom,recpower})"
   7.434 +apply (insert odd_power_less_zero [of a n]) 
   7.435 +apply (force simp add: linorder_not_less [symmetric]) 
   7.436 +done
   7.437 +
   7.438 +text{*Simprules for comparisons where common factors can be cancelled.*}
   7.439 +lemmas zero_compare_simps =
   7.440 +    add_strict_increasing add_strict_increasing2 add_increasing
   7.441 +    zero_le_mult_iff zero_le_divide_iff 
   7.442 +    zero_less_mult_iff zero_less_divide_iff 
   7.443 +    mult_le_0_iff divide_le_0_iff 
   7.444 +    mult_less_0_iff divide_less_0_iff 
   7.445 +    zero_le_power2 power2_less_0
   7.446 +
   7.447 +subsubsection{*Nat *}
   7.448 +
   7.449 +lemma Suc_pred': "0 < n ==> n = Suc(n - 1)"
   7.450 +by (simp add: numerals)
   7.451 +
   7.452 +(*Expresses a natural number constant as the Suc of another one.
   7.453 +  NOT suitable for rewriting because n recurs in the condition.*)
   7.454 +lemmas expand_Suc = Suc_pred' [of "number_of v", standard]
   7.455 +
   7.456 +subsubsection{*Arith *}
   7.457 +
   7.458 +lemma Suc_eq_add_numeral_1: "Suc n = n + 1"
   7.459 +by (simp add: numerals)
   7.460 +
   7.461 +lemma Suc_eq_add_numeral_1_left: "Suc n = 1 + n"
   7.462 +by (simp add: numerals)
   7.463 +
   7.464 +(* These two can be useful when m = number_of... *)
   7.465 +
   7.466 +lemma add_eq_if: "(m::nat) + n = (if m=0 then n else Suc ((m - 1) + n))"
   7.467 +  unfolding One_nat_def by (cases m) simp_all
   7.468 +
   7.469 +lemma mult_eq_if: "(m::nat) * n = (if m=0 then 0 else n + ((m - 1) * n))"
   7.470 +  unfolding One_nat_def by (cases m) simp_all
   7.471 +
   7.472 +lemma power_eq_if: "(p ^ m :: nat) = (if m=0 then 1 else p * (p ^ (m - 1)))"
   7.473 +  unfolding One_nat_def by (cases m) simp_all
   7.474 +
   7.475 +
   7.476 +subsection{*Comparisons involving (0::nat) *}
   7.477 +
   7.478 +text{*Simplification already does @{term "n<0"}, @{term "n\<le>0"} and @{term "0\<le>n"}.*}
   7.479 +
   7.480 +lemma eq_number_of_0 [simp]:
   7.481 +  "number_of v = (0::nat) \<longleftrightarrow> v \<le> Int.Pls"
   7.482 +  unfolding nat_number_of_def number_of_is_id numeral_simps
   7.483 +  by auto
   7.484 +
   7.485 +lemma eq_0_number_of [simp]:
   7.486 +  "(0::nat) = number_of v \<longleftrightarrow> v \<le> Int.Pls"
   7.487 +by (rule trans [OF eq_sym_conv eq_number_of_0])
   7.488 +
   7.489 +lemma less_0_number_of [simp]:
   7.490 +   "(0::nat) < number_of v \<longleftrightarrow> Int.Pls < v"
   7.491 +  unfolding nat_number_of_def number_of_is_id numeral_simps
   7.492 +  by simp
   7.493 +
   7.494 +lemma neg_imp_number_of_eq_0: "neg (number_of v :: int) ==> number_of v = (0::nat)"
   7.495 +by (simp del: nat_numeral_0_eq_0 add: nat_numeral_0_eq_0 [symmetric])
   7.496 +
   7.497 +
   7.498 +
   7.499 +subsection{*Comparisons involving  @{term Suc} *}
   7.500 +
   7.501 +lemma eq_number_of_Suc [simp]:
   7.502 +     "(number_of v = Suc n) =  
   7.503 +        (let pv = number_of (Int.pred v) in  
   7.504 +         if neg pv then False else nat pv = n)"
   7.505 +apply (simp only: simp_thms Let_def neg_eq_less_0 linorder_not_less 
   7.506 +                  number_of_pred nat_number_of_def 
   7.507 +            split add: split_if)
   7.508 +apply (rule_tac x = "number_of v" in spec)
   7.509 +apply (auto simp add: nat_eq_iff)
   7.510 +done
   7.511 +
   7.512 +lemma Suc_eq_number_of [simp]:
   7.513 +     "(Suc n = number_of v) =  
   7.514 +        (let pv = number_of (Int.pred v) in  
   7.515 +         if neg pv then False else nat pv = n)"
   7.516 +by (rule trans [OF eq_sym_conv eq_number_of_Suc])
   7.517 +
   7.518 +lemma less_number_of_Suc [simp]:
   7.519 +     "(number_of v < Suc n) =  
   7.520 +        (let pv = number_of (Int.pred v) in  
   7.521 +         if neg pv then True else nat pv < n)"
   7.522 +apply (simp only: simp_thms Let_def neg_eq_less_0 linorder_not_less 
   7.523 +                  number_of_pred nat_number_of_def  
   7.524 +            split add: split_if)
   7.525 +apply (rule_tac x = "number_of v" in spec)
   7.526 +apply (auto simp add: nat_less_iff)
   7.527 +done
   7.528 +
   7.529 +lemma less_Suc_number_of [simp]:
   7.530 +     "(Suc n < number_of v) =  
   7.531 +        (let pv = number_of (Int.pred v) in  
   7.532 +         if neg pv then False else n < nat pv)"
   7.533 +apply (simp only: simp_thms Let_def neg_eq_less_0 linorder_not_less 
   7.534 +                  number_of_pred nat_number_of_def
   7.535 +            split add: split_if)
   7.536 +apply (rule_tac x = "number_of v" in spec)
   7.537 +apply (auto simp add: zless_nat_eq_int_zless)
   7.538 +done
   7.539 +
   7.540 +lemma le_number_of_Suc [simp]:
   7.541 +     "(number_of v <= Suc n) =  
   7.542 +        (let pv = number_of (Int.pred v) in  
   7.543 +         if neg pv then True else nat pv <= n)"
   7.544 +by (simp add: Let_def less_Suc_number_of linorder_not_less [symmetric])
   7.545 +
   7.546 +lemma le_Suc_number_of [simp]:
   7.547 +     "(Suc n <= number_of v) =  
   7.548 +        (let pv = number_of (Int.pred v) in  
   7.549 +         if neg pv then False else n <= nat pv)"
   7.550 +by (simp add: Let_def less_number_of_Suc linorder_not_less [symmetric])
   7.551 +
   7.552 +
   7.553 +lemma eq_number_of_Pls_Min: "(Numeral0 ::int) ~= number_of Int.Min"
   7.554 +by auto
   7.555 +
   7.556 +
   7.557 +
   7.558 +subsection{*Max and Min Combined with @{term Suc} *}
   7.559 +
   7.560 +lemma max_number_of_Suc [simp]:
   7.561 +     "max (Suc n) (number_of v) =  
   7.562 +        (let pv = number_of (Int.pred v) in  
   7.563 +         if neg pv then Suc n else Suc(max n (nat pv)))"
   7.564 +apply (simp only: Let_def neg_eq_less_0 number_of_pred nat_number_of_def 
   7.565 +            split add: split_if nat.split)
   7.566 +apply (rule_tac x = "number_of v" in spec) 
   7.567 +apply auto
   7.568 +done
   7.569 + 
   7.570 +lemma max_Suc_number_of [simp]:
   7.571 +     "max (number_of v) (Suc n) =  
   7.572 +        (let pv = number_of (Int.pred v) in  
   7.573 +         if neg pv then Suc n else Suc(max (nat pv) n))"
   7.574 +apply (simp only: Let_def neg_eq_less_0 number_of_pred nat_number_of_def 
   7.575 +            split add: split_if nat.split)
   7.576 +apply (rule_tac x = "number_of v" in spec) 
   7.577 +apply auto
   7.578 +done
   7.579 + 
   7.580 +lemma min_number_of_Suc [simp]:
   7.581 +     "min (Suc n) (number_of v) =  
   7.582 +        (let pv = number_of (Int.pred v) in  
   7.583 +         if neg pv then 0 else Suc(min n (nat pv)))"
   7.584 +apply (simp only: Let_def neg_eq_less_0 number_of_pred nat_number_of_def 
   7.585 +            split add: split_if nat.split)
   7.586 +apply (rule_tac x = "number_of v" in spec) 
   7.587 +apply auto
   7.588 +done
   7.589 + 
   7.590 +lemma min_Suc_number_of [simp]:
   7.591 +     "min (number_of v) (Suc n) =  
   7.592 +        (let pv = number_of (Int.pred v) in  
   7.593 +         if neg pv then 0 else Suc(min (nat pv) n))"
   7.594 +apply (simp only: Let_def neg_eq_less_0 number_of_pred nat_number_of_def 
   7.595 +            split add: split_if nat.split)
   7.596 +apply (rule_tac x = "number_of v" in spec) 
   7.597 +apply auto
   7.598 +done
   7.599 + 
   7.600 +subsection{*Literal arithmetic involving powers*}
   7.601 +
   7.602 +lemma nat_power_eq: "(0::int) <= z ==> nat (z^n) = nat z ^ n"
   7.603 +apply (induct "n")
   7.604 +apply (simp_all (no_asm_simp) add: nat_mult_distrib)
   7.605 +done
   7.606 +
   7.607 +lemma power_nat_number_of:
   7.608 +     "(number_of v :: nat) ^ n =  
   7.609 +       (if neg (number_of v :: int) then 0^n else nat ((number_of v :: int) ^ n))"
   7.610 +by (simp only: simp_thms neg_nat not_neg_eq_ge_0 nat_number_of_def nat_power_eq
   7.611 +         split add: split_if cong: imp_cong)
   7.612 +
   7.613 +
   7.614 +lemmas power_nat_number_of_number_of = power_nat_number_of [of _ "number_of w", standard]
   7.615 +declare power_nat_number_of_number_of [simp]
   7.616 +
   7.617 +
   7.618 +
   7.619 +text{*For arbitrary rings*}
   7.620 +
   7.621 +lemma power_number_of_even:
   7.622 +  fixes z :: "'a::{number_ring,recpower}"
   7.623 +  shows "z ^ number_of (Int.Bit0 w) = (let w = z ^ (number_of w) in w * w)"
   7.624 +unfolding Let_def nat_number_of_def number_of_Bit0
   7.625 +apply (rule_tac x = "number_of w" in spec, clarify)
   7.626 +apply (case_tac " (0::int) <= x")
   7.627 +apply (auto simp add: nat_mult_distrib power_even_eq power2_eq_square)
   7.628 +done
   7.629 +
   7.630 +lemma power_number_of_odd:
   7.631 +  fixes z :: "'a::{number_ring,recpower}"
   7.632 +  shows "z ^ number_of (Int.Bit1 w) = (if (0::int) <= number_of w
   7.633 +     then (let w = z ^ (number_of w) in z * w * w) else 1)"
   7.634 +unfolding Let_def nat_number_of_def number_of_Bit1
   7.635 +apply (rule_tac x = "number_of w" in spec, auto)
   7.636 +apply (simp only: nat_add_distrib nat_mult_distrib)
   7.637 +apply simp
   7.638 +apply (auto simp add: nat_add_distrib nat_mult_distrib power_even_eq power2_eq_square neg_nat power_Suc)
   7.639 +done
   7.640 +
   7.641 +lemmas zpower_number_of_even = power_number_of_even [where 'a=int]
   7.642 +lemmas zpower_number_of_odd = power_number_of_odd [where 'a=int]
   7.643 +
   7.644 +lemmas power_number_of_even_number_of [simp] =
   7.645 +    power_number_of_even [of "number_of v", standard]
   7.646 +
   7.647 +lemmas power_number_of_odd_number_of [simp] =
   7.648 +    power_number_of_odd [of "number_of v", standard]
   7.649 +
   7.650 +
   7.651 +
   7.652 +ML
   7.653 +{*
   7.654 +val numeral_ss = @{simpset} addsimps @{thms numerals};
   7.655 +
   7.656 +val nat_bin_arith_setup =
   7.657 + Lin_Arith.map_data
   7.658 +   (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
   7.659 +     {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms,
   7.660 +      inj_thms = inj_thms,
   7.661 +      lessD = lessD, neqE = neqE,
   7.662 +      simpset = simpset addsimps @{thms neg_simps} @
   7.663 +        [@{thm Suc_nat_number_of}, @{thm int_nat_number_of}]})
   7.664 +*}
   7.665 +
   7.666 +declaration {* K nat_bin_arith_setup *}
   7.667 +
   7.668 +(* Enable arith to deal with div/mod k where k is a numeral: *)
   7.669 +declare split_div[of _ _ "number_of k", standard, arith_split]
   7.670 +declare split_mod[of _ _ "number_of k", standard, arith_split]
   7.671 +
   7.672 +lemma nat_number_of_Pls: "Numeral0 = (0::nat)"
   7.673 +  by (simp add: number_of_Pls nat_number_of_def)
   7.674 +
   7.675 +lemma nat_number_of_Min: "number_of Int.Min = (0::nat)"
   7.676 +  apply (simp only: number_of_Min nat_number_of_def nat_zminus_int)
   7.677 +  done
   7.678 +
   7.679 +lemma nat_number_of_Bit0:
   7.680 +    "number_of (Int.Bit0 w) = (let n::nat = number_of w in n + n)"
   7.681 +  unfolding nat_number_of_def number_of_is_id numeral_simps Let_def
   7.682 +  by auto
   7.683 +
   7.684 +lemma nat_number_of_Bit1:
   7.685 +  "number_of (Int.Bit1 w) =
   7.686 +    (if neg (number_of w :: int) then 0
   7.687 +     else let n = number_of w in Suc (n + n))"
   7.688 +  unfolding nat_number_of_def number_of_is_id numeral_simps neg_def Let_def
   7.689 +  by auto
   7.690 +
   7.691 +lemmas nat_number =
   7.692 +  nat_number_of_Pls nat_number_of_Min
   7.693 +  nat_number_of_Bit0 nat_number_of_Bit1
   7.694 +
   7.695 +lemma Let_Suc [simp]: "Let (Suc n) f == f (Suc n)"
   7.696 +  by (simp add: Let_def)
   7.697 +
   7.698 +lemma power_m1_even: "(-1) ^ (2*n) = (1::'a::{number_ring,recpower})"
   7.699 +by (simp add: power_mult power_Suc); 
   7.700 +
   7.701 +lemma power_m1_odd: "(-1) ^ Suc(2*n) = (-1::'a::{number_ring,recpower})"
   7.702 +by (simp add: power_mult power_Suc); 
   7.703 +
   7.704 +
   7.705 +subsection{*Literal arithmetic and @{term of_nat}*}
   7.706 +
   7.707 +lemma of_nat_double:
   7.708 +     "0 \<le> x ==> of_nat (nat (2 * x)) = of_nat (nat x) + of_nat (nat x)"
   7.709 +by (simp only: mult_2 nat_add_distrib of_nat_add) 
   7.710 +
   7.711 +lemma nat_numeral_m1_eq_0: "-1 = (0::nat)"
   7.712 +by (simp only: nat_number_of_def)
   7.713 +
   7.714 +lemma of_nat_number_of_lemma:
   7.715 +     "of_nat (number_of v :: nat) =  
   7.716 +         (if 0 \<le> (number_of v :: int) 
   7.717 +          then (number_of v :: 'a :: number_ring)
   7.718 +          else 0)"
   7.719 +by (simp add: int_number_of_def nat_number_of_def number_of_eq of_nat_nat);
   7.720 +
   7.721 +lemma of_nat_number_of_eq [simp]:
   7.722 +     "of_nat (number_of v :: nat) =  
   7.723 +         (if neg (number_of v :: int) then 0  
   7.724 +          else (number_of v :: 'a :: number_ring))"
   7.725 +by (simp only: of_nat_number_of_lemma neg_def, simp) 
   7.726 +
   7.727 +
   7.728 +subsection {*Lemmas for the Combination and Cancellation Simprocs*}
   7.729 +
   7.730 +lemma nat_number_of_add_left:
   7.731 +     "number_of v + (number_of v' + (k::nat)) =  
   7.732 +         (if neg (number_of v :: int) then number_of v' + k  
   7.733 +          else if neg (number_of v' :: int) then number_of v + k  
   7.734 +          else number_of (v + v') + k)"
   7.735 +  unfolding nat_number_of_def number_of_is_id neg_def
   7.736 +  by auto
   7.737 +
   7.738 +lemma nat_number_of_mult_left:
   7.739 +     "number_of v * (number_of v' * (k::nat)) =  
   7.740 +         (if v < Int.Pls then 0
   7.741 +          else number_of (v * v') * k)"
   7.742 +by simp
   7.743 +
   7.744 +
   7.745 +subsubsection{*For @{text combine_numerals}*}
   7.746 +
   7.747 +lemma left_add_mult_distrib: "i*u + (j*u + k) = (i+j)*u + (k::nat)"
   7.748 +by (simp add: add_mult_distrib)
   7.749 +
   7.750 +
   7.751 +subsubsection{*For @{text cancel_numerals}*}
   7.752 +
   7.753 +lemma nat_diff_add_eq1:
   7.754 +     "j <= (i::nat) ==> ((i*u + m) - (j*u + n)) = (((i-j)*u + m) - n)"
   7.755 +by (simp split add: nat_diff_split add: add_mult_distrib)
   7.756 +
   7.757 +lemma nat_diff_add_eq2:
   7.758 +     "i <= (j::nat) ==> ((i*u + m) - (j*u + n)) = (m - ((j-i)*u + n))"
   7.759 +by (simp split add: nat_diff_split add: add_mult_distrib)
   7.760 +
   7.761 +lemma nat_eq_add_iff1:
   7.762 +     "j <= (i::nat) ==> (i*u + m = j*u + n) = ((i-j)*u + m = n)"
   7.763 +by (auto split add: nat_diff_split simp add: add_mult_distrib)
   7.764 +
   7.765 +lemma nat_eq_add_iff2:
   7.766 +     "i <= (j::nat) ==> (i*u + m = j*u + n) = (m = (j-i)*u + n)"
   7.767 +by (auto split add: nat_diff_split simp add: add_mult_distrib)
   7.768 +
   7.769 +lemma nat_less_add_iff1:
   7.770 +     "j <= (i::nat) ==> (i*u + m < j*u + n) = ((i-j)*u + m < n)"
   7.771 +by (auto split add: nat_diff_split simp add: add_mult_distrib)
   7.772 +
   7.773 +lemma nat_less_add_iff2:
   7.774 +     "i <= (j::nat) ==> (i*u + m < j*u + n) = (m < (j-i)*u + n)"
   7.775 +by (auto split add: nat_diff_split simp add: add_mult_distrib)
   7.776 +
   7.777 +lemma nat_le_add_iff1:
   7.778 +     "j <= (i::nat) ==> (i*u + m <= j*u + n) = ((i-j)*u + m <= n)"
   7.779 +by (auto split add: nat_diff_split simp add: add_mult_distrib)
   7.780 +
   7.781 +lemma nat_le_add_iff2:
   7.782 +     "i <= (j::nat) ==> (i*u + m <= j*u + n) = (m <= (j-i)*u + n)"
   7.783 +by (auto split add: nat_diff_split simp add: add_mult_distrib)
   7.784 +
   7.785 +
   7.786 +subsubsection{*For @{text cancel_numeral_factors} *}
   7.787 +
   7.788 +lemma nat_mult_le_cancel1: "(0::nat) < k ==> (k*m <= k*n) = (m<=n)"
   7.789 +by auto
   7.790 +
   7.791 +lemma nat_mult_less_cancel1: "(0::nat) < k ==> (k*m < k*n) = (m<n)"
   7.792 +by auto
   7.793 +
   7.794 +lemma nat_mult_eq_cancel1: "(0::nat) < k ==> (k*m = k*n) = (m=n)"
   7.795 +by auto
   7.796 +
   7.797 +lemma nat_mult_div_cancel1: "(0::nat) < k ==> (k*m) div (k*n) = (m div n)"
   7.798 +by auto
   7.799 +
   7.800 +lemma nat_mult_dvd_cancel_disj[simp]:
   7.801 +  "(k*m) dvd (k*n) = (k=0 | m dvd (n::nat))"
   7.802 +by(auto simp: dvd_eq_mod_eq_0 mod_mult_distrib2[symmetric])
   7.803 +
   7.804 +lemma nat_mult_dvd_cancel1: "0 < k \<Longrightarrow> (k*m) dvd (k*n::nat) = (m dvd n)"
   7.805 +by(auto)
   7.806 +
   7.807 +
   7.808 +subsubsection{*For @{text cancel_factor} *}
   7.809 +
   7.810 +lemma nat_mult_le_cancel_disj: "(k*m <= k*n) = ((0::nat) < k --> m<=n)"
   7.811 +by auto
   7.812 +
   7.813 +lemma nat_mult_less_cancel_disj: "(k*m < k*n) = ((0::nat) < k & m<n)"
   7.814 +by auto
   7.815 +
   7.816 +lemma nat_mult_eq_cancel_disj: "(k*m = k*n) = (k = (0::nat) | m=n)"
   7.817 +by auto
   7.818 +
   7.819 +lemma nat_mult_div_cancel_disj[simp]:
   7.820 +     "(k*m) div (k*n) = (if k = (0::nat) then 0 else m div n)"
   7.821 +by (simp add: nat_mult_div_cancel1)
   7.822 +
   7.823 +
   7.824 +subsection {* Simprocs for the Naturals *}
   7.825 +
   7.826 +use "Tools/nat_simprocs.ML"
   7.827 +declaration {* K nat_simprocs_setup *}
   7.828 +
   7.829 +subsubsection{*For simplifying @{term "Suc m - K"} and  @{term "K - Suc m"}*}
   7.830 +
   7.831 +text{*Where K above is a literal*}
   7.832 +
   7.833 +lemma Suc_diff_eq_diff_pred: "Numeral0 < n ==> Suc m - n = m - (n - Numeral1)"
   7.834 +by (simp add: numeral_0_eq_0 numeral_1_eq_1 split add: nat_diff_split)
   7.835 +
   7.836 +text {*Now just instantiating @{text n} to @{text "number_of v"} does
   7.837 +  the right simplification, but with some redundant inequality
   7.838 +  tests.*}
   7.839 +lemma neg_number_of_pred_iff_0:
   7.840 +  "neg (number_of (Int.pred v)::int) = (number_of v = (0::nat))"
   7.841 +apply (subgoal_tac "neg (number_of (Int.pred v)) = (number_of v < Suc 0) ")
   7.842 +apply (simp only: less_Suc_eq_le le_0_eq)
   7.843 +apply (subst less_number_of_Suc, simp)
   7.844 +done
   7.845 +
   7.846 +text{*No longer required as a simprule because of the @{text inverse_fold}
   7.847 +   simproc*}
   7.848 +lemma Suc_diff_number_of:
   7.849 +     "Int.Pls < v ==>
   7.850 +      Suc m - (number_of v) = m - (number_of (Int.pred v))"
   7.851 +apply (subst Suc_diff_eq_diff_pred)
   7.852 +apply simp
   7.853 +apply (simp del: nat_numeral_1_eq_1)
   7.854 +apply (auto simp only: diff_nat_number_of less_0_number_of [symmetric]
   7.855 +                        neg_number_of_pred_iff_0)
   7.856 +done
   7.857 +
   7.858 +lemma diff_Suc_eq_diff_pred: "m - Suc n = (m - 1) - n"
   7.859 +by (simp add: numerals split add: nat_diff_split)
   7.860 +
   7.861 +
   7.862 +subsubsection{*For @{term nat_case} and @{term nat_rec}*}
   7.863 +
   7.864 +lemma nat_case_number_of [simp]:
   7.865 +     "nat_case a f (number_of v) =
   7.866 +        (let pv = number_of (Int.pred v) in
   7.867 +         if neg pv then a else f (nat pv))"
   7.868 +by (simp split add: nat.split add: Let_def neg_number_of_pred_iff_0)
   7.869 +
   7.870 +lemma nat_case_add_eq_if [simp]:
   7.871 +     "nat_case a f ((number_of v) + n) =
   7.872 +       (let pv = number_of (Int.pred v) in
   7.873 +         if neg pv then nat_case a f n else f (nat pv + n))"
   7.874 +apply (subst add_eq_if)
   7.875 +apply (simp split add: nat.split
   7.876 +            del: nat_numeral_1_eq_1
   7.877 +            add: nat_numeral_1_eq_1 [symmetric]
   7.878 +                 numeral_1_eq_Suc_0 [symmetric]
   7.879 +                 neg_number_of_pred_iff_0)
   7.880 +done
   7.881 +
   7.882 +lemma nat_rec_number_of [simp]:
   7.883 +     "nat_rec a f (number_of v) =
   7.884 +        (let pv = number_of (Int.pred v) in
   7.885 +         if neg pv then a else f (nat pv) (nat_rec a f (nat pv)))"
   7.886 +apply (case_tac " (number_of v) ::nat")
   7.887 +apply (simp_all (no_asm_simp) add: Let_def neg_number_of_pred_iff_0)
   7.888 +apply (simp split add: split_if_asm)
   7.889 +done
   7.890 +
   7.891 +lemma nat_rec_add_eq_if [simp]:
   7.892 +     "nat_rec a f (number_of v + n) =
   7.893 +        (let pv = number_of (Int.pred v) in
   7.894 +         if neg pv then nat_rec a f n
   7.895 +                   else f (nat pv + n) (nat_rec a f (nat pv + n)))"
   7.896 +apply (subst add_eq_if)
   7.897 +apply (simp split add: nat.split
   7.898 +            del: nat_numeral_1_eq_1
   7.899 +            add: nat_numeral_1_eq_1 [symmetric]
   7.900 +                 numeral_1_eq_Suc_0 [symmetric]
   7.901 +                 neg_number_of_pred_iff_0)
   7.902 +done
   7.903 +
   7.904 +
   7.905 +subsubsection{*Various Other Lemmas*}
   7.906 +
   7.907 +text {*Evens and Odds, for Mutilated Chess Board*}
   7.908 +
   7.909 +text{*Lemmas for specialist use, NOT as default simprules*}
   7.910 +lemma nat_mult_2: "2 * z = (z+z::nat)"
   7.911 +proof -
   7.912 +  have "2*z = (1 + 1)*z" by simp
   7.913 +  also have "... = z+z" by (simp add: left_distrib)
   7.914 +  finally show ?thesis .
   7.915 +qed
   7.916 +
   7.917 +lemma nat_mult_2_right: "z * 2 = (z+z::nat)"
   7.918 +by (subst mult_commute, rule nat_mult_2)
   7.919 +
   7.920 +text{*Case analysis on @{term "n<2"}*}
   7.921 +lemma less_2_cases: "(n::nat) < 2 ==> n = 0 | n = Suc 0"
   7.922 +by arith
   7.923 +
   7.924 +lemma div2_Suc_Suc [simp]: "Suc(Suc m) div 2 = Suc (m div 2)"
   7.925 +by arith
   7.926 +
   7.927 +lemma add_self_div_2 [simp]: "(m + m) div 2 = (m::nat)"
   7.928 +by (simp add: nat_mult_2 [symmetric])
   7.929 +
   7.930 +lemma mod2_Suc_Suc [simp]: "Suc(Suc(m)) mod 2 = m mod 2"
   7.931 +apply (subgoal_tac "m mod 2 < 2")
   7.932 +apply (erule less_2_cases [THEN disjE])
   7.933 +apply (simp_all (no_asm_simp) add: Let_def mod_Suc nat_1)
   7.934 +done
   7.935 +
   7.936 +lemma mod2_gr_0 [simp]: "!!m::nat. (0 < m mod 2) = (m mod 2 = 1)"
   7.937 +apply (subgoal_tac "m mod 2 < 2")
   7.938 +apply (force simp del: mod_less_divisor, simp)
   7.939 +done
   7.940 +
   7.941 +text{*Removal of Small Numerals: 0, 1 and (in additive positions) 2*}
   7.942 +
   7.943 +lemma add_2_eq_Suc [simp]: "2 + n = Suc (Suc n)"
   7.944 +by simp
   7.945 +
   7.946 +lemma add_2_eq_Suc' [simp]: "n + 2 = Suc (Suc n)"
   7.947 +by simp
   7.948 +
   7.949 +text{*Can be used to eliminate long strings of Sucs, but not by default*}
   7.950 +lemma Suc3_eq_add_3: "Suc (Suc (Suc n)) = 3 + n"
   7.951 +by simp
   7.952 +
   7.953 +
   7.954 +text{*These lemmas collapse some needless occurrences of Suc:
   7.955 +    at least three Sucs, since two and fewer are rewritten back to Suc again!
   7.956 +    We already have some rules to simplify operands smaller than 3.*}
   7.957 +
   7.958 +lemma div_Suc_eq_div_add3 [simp]: "m div (Suc (Suc (Suc n))) = m div (3+n)"
   7.959 +by (simp add: Suc3_eq_add_3)
   7.960 +
   7.961 +lemma mod_Suc_eq_mod_add3 [simp]: "m mod (Suc (Suc (Suc n))) = m mod (3+n)"
   7.962 +by (simp add: Suc3_eq_add_3)
   7.963 +
   7.964 +lemma Suc_div_eq_add3_div: "(Suc (Suc (Suc m))) div n = (3+m) div n"
   7.965 +by (simp add: Suc3_eq_add_3)
   7.966 +
   7.967 +lemma Suc_mod_eq_add3_mod: "(Suc (Suc (Suc m))) mod n = (3+m) mod n"
   7.968 +by (simp add: Suc3_eq_add_3)
   7.969 +
   7.970 +lemmas Suc_div_eq_add3_div_number_of =
   7.971 +    Suc_div_eq_add3_div [of _ "number_of v", standard]
   7.972 +declare Suc_div_eq_add3_div_number_of [simp]
   7.973 +
   7.974 +lemmas Suc_mod_eq_add3_mod_number_of =
   7.975 +    Suc_mod_eq_add3_mod [of _ "number_of v", standard]
   7.976 +declare Suc_mod_eq_add3_mod_number_of [simp]
   7.977 +
   7.978 +end