src/HOL/Num.thy
changeset 47108 2a1953f0d20d
child 47126 e980b14c347d
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Num.thy	Sun Mar 25 20:15:39 2012 +0200
     1.3 @@ -0,0 +1,1021 @@
     1.4 +(*  Title:      HOL/Num.thy
     1.5 +    Author:     Florian Haftmann
     1.6 +    Author:     Brian Huffman
     1.7 +*)
     1.8 +
     1.9 +header {* Binary Numerals *}
    1.10 +
    1.11 +theory Num
    1.12 +imports Datatype Power
    1.13 +begin
    1.14 +
    1.15 +subsection {* The @{text num} type *}
    1.16 +
    1.17 +datatype num = One | Bit0 num | Bit1 num
    1.18 +
    1.19 +text {* Increment function for type @{typ num} *}
    1.20 +
    1.21 +primrec inc :: "num \<Rightarrow> num" where
    1.22 +  "inc One = Bit0 One" |
    1.23 +  "inc (Bit0 x) = Bit1 x" |
    1.24 +  "inc (Bit1 x) = Bit0 (inc x)"
    1.25 +
    1.26 +text {* Converting between type @{typ num} and type @{typ nat} *}
    1.27 +
    1.28 +primrec nat_of_num :: "num \<Rightarrow> nat" where
    1.29 +  "nat_of_num One = Suc 0" |
    1.30 +  "nat_of_num (Bit0 x) = nat_of_num x + nat_of_num x" |
    1.31 +  "nat_of_num (Bit1 x) = Suc (nat_of_num x + nat_of_num x)"
    1.32 +
    1.33 +primrec num_of_nat :: "nat \<Rightarrow> num" where
    1.34 +  "num_of_nat 0 = One" |
    1.35 +  "num_of_nat (Suc n) = (if 0 < n then inc (num_of_nat n) else One)"
    1.36 +
    1.37 +lemma nat_of_num_pos: "0 < nat_of_num x"
    1.38 +  by (induct x) simp_all
    1.39 +
    1.40 +lemma nat_of_num_neq_0: " nat_of_num x \<noteq> 0"
    1.41 +  by (induct x) simp_all
    1.42 +
    1.43 +lemma nat_of_num_inc: "nat_of_num (inc x) = Suc (nat_of_num x)"
    1.44 +  by (induct x) simp_all
    1.45 +
    1.46 +lemma num_of_nat_double:
    1.47 +  "0 < n \<Longrightarrow> num_of_nat (n + n) = Bit0 (num_of_nat n)"
    1.48 +  by (induct n) simp_all
    1.49 +
    1.50 +text {*
    1.51 +  Type @{typ num} is isomorphic to the strictly positive
    1.52 +  natural numbers.
    1.53 +*}
    1.54 +
    1.55 +lemma nat_of_num_inverse: "num_of_nat (nat_of_num x) = x"
    1.56 +  by (induct x) (simp_all add: num_of_nat_double nat_of_num_pos)
    1.57 +
    1.58 +lemma num_of_nat_inverse: "0 < n \<Longrightarrow> nat_of_num (num_of_nat n) = n"
    1.59 +  by (induct n) (simp_all add: nat_of_num_inc)
    1.60 +
    1.61 +lemma num_eq_iff: "x = y \<longleftrightarrow> nat_of_num x = nat_of_num y"
    1.62 +  apply safe
    1.63 +  apply (drule arg_cong [where f=num_of_nat])
    1.64 +  apply (simp add: nat_of_num_inverse)
    1.65 +  done
    1.66 +
    1.67 +lemma num_induct [case_names One inc]:
    1.68 +  fixes P :: "num \<Rightarrow> bool"
    1.69 +  assumes One: "P One"
    1.70 +    and inc: "\<And>x. P x \<Longrightarrow> P (inc x)"
    1.71 +  shows "P x"
    1.72 +proof -
    1.73 +  obtain n where n: "Suc n = nat_of_num x"
    1.74 +    by (cases "nat_of_num x", simp_all add: nat_of_num_neq_0)
    1.75 +  have "P (num_of_nat (Suc n))"
    1.76 +  proof (induct n)
    1.77 +    case 0 show ?case using One by simp
    1.78 +  next
    1.79 +    case (Suc n)
    1.80 +    then have "P (inc (num_of_nat (Suc n)))" by (rule inc)
    1.81 +    then show "P (num_of_nat (Suc (Suc n)))" by simp
    1.82 +  qed
    1.83 +  with n show "P x"
    1.84 +    by (simp add: nat_of_num_inverse)
    1.85 +qed
    1.86 +
    1.87 +text {*
    1.88 +  From now on, there are two possible models for @{typ num}:
    1.89 +  as positive naturals (rule @{text "num_induct"})
    1.90 +  and as digit representation (rules @{text "num.induct"}, @{text "num.cases"}).
    1.91 +*}
    1.92 +
    1.93 +
    1.94 +subsection {* Numeral operations *}
    1.95 +
    1.96 +instantiation num :: "{plus,times,linorder}"
    1.97 +begin
    1.98 +
    1.99 +definition [code del]:
   1.100 +  "m + n = num_of_nat (nat_of_num m + nat_of_num n)"
   1.101 +
   1.102 +definition [code del]:
   1.103 +  "m * n = num_of_nat (nat_of_num m * nat_of_num n)"
   1.104 +
   1.105 +definition [code del]:
   1.106 +  "m \<le> n \<longleftrightarrow> nat_of_num m \<le> nat_of_num n"
   1.107 +
   1.108 +definition [code del]:
   1.109 +  "m < n \<longleftrightarrow> nat_of_num m < nat_of_num n"
   1.110 +
   1.111 +instance
   1.112 +  by (default, auto simp add: less_num_def less_eq_num_def num_eq_iff)
   1.113 +
   1.114 +end
   1.115 +
   1.116 +lemma nat_of_num_add: "nat_of_num (x + y) = nat_of_num x + nat_of_num y"
   1.117 +  unfolding plus_num_def
   1.118 +  by (intro num_of_nat_inverse add_pos_pos nat_of_num_pos)
   1.119 +
   1.120 +lemma nat_of_num_mult: "nat_of_num (x * y) = nat_of_num x * nat_of_num y"
   1.121 +  unfolding times_num_def
   1.122 +  by (intro num_of_nat_inverse mult_pos_pos nat_of_num_pos)
   1.123 +
   1.124 +lemma add_num_simps [simp, code]:
   1.125 +  "One + One = Bit0 One"
   1.126 +  "One + Bit0 n = Bit1 n"
   1.127 +  "One + Bit1 n = Bit0 (n + One)"
   1.128 +  "Bit0 m + One = Bit1 m"
   1.129 +  "Bit0 m + Bit0 n = Bit0 (m + n)"
   1.130 +  "Bit0 m + Bit1 n = Bit1 (m + n)"
   1.131 +  "Bit1 m + One = Bit0 (m + One)"
   1.132 +  "Bit1 m + Bit0 n = Bit1 (m + n)"
   1.133 +  "Bit1 m + Bit1 n = Bit0 (m + n + One)"
   1.134 +  by (simp_all add: num_eq_iff nat_of_num_add)
   1.135 +
   1.136 +lemma mult_num_simps [simp, code]:
   1.137 +  "m * One = m"
   1.138 +  "One * n = n"
   1.139 +  "Bit0 m * Bit0 n = Bit0 (Bit0 (m * n))"
   1.140 +  "Bit0 m * Bit1 n = Bit0 (m * Bit1 n)"
   1.141 +  "Bit1 m * Bit0 n = Bit0 (Bit1 m * n)"
   1.142 +  "Bit1 m * Bit1 n = Bit1 (m + n + Bit0 (m * n))"
   1.143 +  by (simp_all add: num_eq_iff nat_of_num_add
   1.144 +    nat_of_num_mult left_distrib right_distrib)
   1.145 +
   1.146 +lemma eq_num_simps:
   1.147 +  "One = One \<longleftrightarrow> True"
   1.148 +  "One = Bit0 n \<longleftrightarrow> False"
   1.149 +  "One = Bit1 n \<longleftrightarrow> False"
   1.150 +  "Bit0 m = One \<longleftrightarrow> False"
   1.151 +  "Bit1 m = One \<longleftrightarrow> False"
   1.152 +  "Bit0 m = Bit0 n \<longleftrightarrow> m = n"
   1.153 +  "Bit0 m = Bit1 n \<longleftrightarrow> False"
   1.154 +  "Bit1 m = Bit0 n \<longleftrightarrow> False"
   1.155 +  "Bit1 m = Bit1 n \<longleftrightarrow> m = n"
   1.156 +  by simp_all
   1.157 +
   1.158 +lemma le_num_simps [simp, code]:
   1.159 +  "One \<le> n \<longleftrightarrow> True"
   1.160 +  "Bit0 m \<le> One \<longleftrightarrow> False"
   1.161 +  "Bit1 m \<le> One \<longleftrightarrow> False"
   1.162 +  "Bit0 m \<le> Bit0 n \<longleftrightarrow> m \<le> n"
   1.163 +  "Bit0 m \<le> Bit1 n \<longleftrightarrow> m \<le> n"
   1.164 +  "Bit1 m \<le> Bit1 n \<longleftrightarrow> m \<le> n"
   1.165 +  "Bit1 m \<le> Bit0 n \<longleftrightarrow> m < n"
   1.166 +  using nat_of_num_pos [of n] nat_of_num_pos [of m]
   1.167 +  by (auto simp add: less_eq_num_def less_num_def)
   1.168 +
   1.169 +lemma less_num_simps [simp, code]:
   1.170 +  "m < One \<longleftrightarrow> False"
   1.171 +  "One < Bit0 n \<longleftrightarrow> True"
   1.172 +  "One < Bit1 n \<longleftrightarrow> True"
   1.173 +  "Bit0 m < Bit0 n \<longleftrightarrow> m < n"
   1.174 +  "Bit0 m < Bit1 n \<longleftrightarrow> m \<le> n"
   1.175 +  "Bit1 m < Bit1 n \<longleftrightarrow> m < n"
   1.176 +  "Bit1 m < Bit0 n \<longleftrightarrow> m < n"
   1.177 +  using nat_of_num_pos [of n] nat_of_num_pos [of m]
   1.178 +  by (auto simp add: less_eq_num_def less_num_def)
   1.179 +
   1.180 +text {* Rules using @{text One} and @{text inc} as constructors *}
   1.181 +
   1.182 +lemma add_One: "x + One = inc x"
   1.183 +  by (simp add: num_eq_iff nat_of_num_add nat_of_num_inc)
   1.184 +
   1.185 +lemma add_One_commute: "One + n = n + One"
   1.186 +  by (induct n) simp_all
   1.187 +
   1.188 +lemma add_inc: "x + inc y = inc (x + y)"
   1.189 +  by (simp add: num_eq_iff nat_of_num_add nat_of_num_inc)
   1.190 +
   1.191 +lemma mult_inc: "x * inc y = x * y + x"
   1.192 +  by (simp add: num_eq_iff nat_of_num_mult nat_of_num_add nat_of_num_inc)
   1.193 +
   1.194 +text {* The @{const num_of_nat} conversion *}
   1.195 +
   1.196 +lemma num_of_nat_One:
   1.197 +  "n \<le> 1 \<Longrightarrow> num_of_nat n = Num.One"
   1.198 +  by (cases n) simp_all
   1.199 +
   1.200 +lemma num_of_nat_plus_distrib:
   1.201 +  "0 < m \<Longrightarrow> 0 < n \<Longrightarrow> num_of_nat (m + n) = num_of_nat m + num_of_nat n"
   1.202 +  by (induct n) (auto simp add: add_One add_One_commute add_inc)
   1.203 +
   1.204 +text {* A double-and-decrement function *}
   1.205 +
   1.206 +primrec BitM :: "num \<Rightarrow> num" where
   1.207 +  "BitM One = One" |
   1.208 +  "BitM (Bit0 n) = Bit1 (BitM n)" |
   1.209 +  "BitM (Bit1 n) = Bit1 (Bit0 n)"
   1.210 +
   1.211 +lemma BitM_plus_one: "BitM n + One = Bit0 n"
   1.212 +  by (induct n) simp_all
   1.213 +
   1.214 +lemma one_plus_BitM: "One + BitM n = Bit0 n"
   1.215 +  unfolding add_One_commute BitM_plus_one ..
   1.216 +
   1.217 +text {* Squaring and exponentiation *}
   1.218 +
   1.219 +primrec sqr :: "num \<Rightarrow> num" where
   1.220 +  "sqr One = One" |
   1.221 +  "sqr (Bit0 n) = Bit0 (Bit0 (sqr n))" |
   1.222 +  "sqr (Bit1 n) = Bit1 (Bit0 (sqr n + n))"
   1.223 +
   1.224 +primrec pow :: "num \<Rightarrow> num \<Rightarrow> num" where
   1.225 +  "pow x One = x" |
   1.226 +  "pow x (Bit0 y) = sqr (pow x y)" |
   1.227 +  "pow x (Bit1 y) = x * sqr (pow x y)"
   1.228 +
   1.229 +lemma nat_of_num_sqr: "nat_of_num (sqr x) = nat_of_num x * nat_of_num x"
   1.230 +  by (induct x, simp_all add: algebra_simps nat_of_num_add)
   1.231 +
   1.232 +lemma sqr_conv_mult: "sqr x = x * x"
   1.233 +  by (simp add: num_eq_iff nat_of_num_sqr nat_of_num_mult)
   1.234 +
   1.235 +
   1.236 +subsection {* Numary numerals *}
   1.237 +
   1.238 +text {*
   1.239 +  We embed numary representations into a generic algebraic
   1.240 +  structure using @{text numeral}.
   1.241 +*}
   1.242 +
   1.243 +class numeral = one + semigroup_add
   1.244 +begin
   1.245 +
   1.246 +primrec numeral :: "num \<Rightarrow> 'a" where
   1.247 +  numeral_One: "numeral One = 1" |
   1.248 +  numeral_Bit0: "numeral (Bit0 n) = numeral n + numeral n" |
   1.249 +  numeral_Bit1: "numeral (Bit1 n) = numeral n + numeral n + 1"
   1.250 +
   1.251 +lemma one_plus_numeral_commute: "1 + numeral x = numeral x + 1"
   1.252 +  apply (induct x)
   1.253 +  apply simp
   1.254 +  apply (simp add: add_assoc [symmetric], simp add: add_assoc)
   1.255 +  apply (simp add: add_assoc [symmetric], simp add: add_assoc)
   1.256 +  done
   1.257 +
   1.258 +lemma numeral_inc: "numeral (inc x) = numeral x + 1"
   1.259 +proof (induct x)
   1.260 +  case (Bit1 x)
   1.261 +  have "numeral x + (1 + numeral x) + 1 = numeral x + (numeral x + 1) + 1"
   1.262 +    by (simp only: one_plus_numeral_commute)
   1.263 +  with Bit1 show ?case
   1.264 +    by (simp add: add_assoc)
   1.265 +qed simp_all
   1.266 +
   1.267 +declare numeral.simps [simp del]
   1.268 +
   1.269 +abbreviation "Numeral1 \<equiv> numeral One"
   1.270 +
   1.271 +declare numeral_One [code_post]
   1.272 +
   1.273 +end
   1.274 +
   1.275 +text {* Negative numerals. *}
   1.276 +
   1.277 +class neg_numeral = numeral + group_add
   1.278 +begin
   1.279 +
   1.280 +definition neg_numeral :: "num \<Rightarrow> 'a" where
   1.281 +  "neg_numeral k = - numeral k"
   1.282 +
   1.283 +end
   1.284 +
   1.285 +text {* Numeral syntax. *}
   1.286 +
   1.287 +syntax
   1.288 +  "_Numeral" :: "num_const \<Rightarrow> 'a"    ("_")
   1.289 +
   1.290 +parse_translation {*
   1.291 +let
   1.292 +  fun num_of_int n = if n > 0 then case IntInf.quotRem (n, 2)
   1.293 +     of (0, 1) => Syntax.const @{const_name One}
   1.294 +      | (n, 0) => Syntax.const @{const_name Bit0} $ num_of_int n
   1.295 +      | (n, 1) => Syntax.const @{const_name Bit1} $ num_of_int n
   1.296 +    else raise Match;
   1.297 +  val pos = Syntax.const @{const_name numeral}
   1.298 +  val neg = Syntax.const @{const_name neg_numeral}
   1.299 +  val one = Syntax.const @{const_name Groups.one}
   1.300 +  val zero = Syntax.const @{const_name Groups.zero}
   1.301 +  fun numeral_tr [(c as Const (@{syntax_const "_constrain"}, _)) $ t $ u] =
   1.302 +        c $ numeral_tr [t] $ u
   1.303 +    | numeral_tr [Const (num, _)] =
   1.304 +        let
   1.305 +          val {value, ...} = Lexicon.read_xnum num;
   1.306 +        in
   1.307 +          if value = 0 then zero else
   1.308 +          if value > 0
   1.309 +          then pos $ num_of_int value
   1.310 +          else neg $ num_of_int (~value)
   1.311 +        end
   1.312 +    | numeral_tr ts = raise TERM ("numeral_tr", ts);
   1.313 +in [("_Numeral", numeral_tr)] end
   1.314 +*}
   1.315 +
   1.316 +typed_print_translation (advanced) {*
   1.317 +let
   1.318 +  fun dest_num (Const (@{const_syntax Bit0}, _) $ n) = 2 * dest_num n
   1.319 +    | dest_num (Const (@{const_syntax Bit1}, _) $ n) = 2 * dest_num n + 1
   1.320 +    | dest_num (Const (@{const_syntax One}, _)) = 1;
   1.321 +  fun num_tr' sign ctxt T [n] =
   1.322 +    let
   1.323 +      val k = dest_num n;
   1.324 +      val t' = Syntax.const @{syntax_const "_Numeral"} $
   1.325 +        Syntax.free (sign ^ string_of_int k);
   1.326 +    in
   1.327 +      case T of
   1.328 +        Type (@{type_name fun}, [_, T']) =>
   1.329 +          if not (Config.get ctxt show_types) andalso can Term.dest_Type T' then t'
   1.330 +          else Syntax.const @{syntax_const "_constrain"} $ t' $ Syntax_Phases.term_of_typ ctxt T'
   1.331 +      | T' => if T' = dummyT then t' else raise Match
   1.332 +    end;
   1.333 +in [(@{const_syntax numeral}, num_tr' ""),
   1.334 +    (@{const_syntax neg_numeral}, num_tr' "-")] end
   1.335 +*}
   1.336 +
   1.337 +subsection {* Class-specific numeral rules *}
   1.338 +
   1.339 +text {*
   1.340 +  @{const numeral} is a morphism.
   1.341 +*}
   1.342 +
   1.343 +subsubsection {* Structures with addition: class @{text numeral} *}
   1.344 +
   1.345 +context numeral
   1.346 +begin
   1.347 +
   1.348 +lemma numeral_add: "numeral (m + n) = numeral m + numeral n"
   1.349 +  by (induct n rule: num_induct)
   1.350 +     (simp_all only: numeral_One add_One add_inc numeral_inc add_assoc)
   1.351 +
   1.352 +lemma numeral_plus_numeral: "numeral m + numeral n = numeral (m + n)"
   1.353 +  by (rule numeral_add [symmetric])
   1.354 +
   1.355 +lemma numeral_plus_one: "numeral n + 1 = numeral (n + One)"
   1.356 +  using numeral_add [of n One] by (simp add: numeral_One)
   1.357 +
   1.358 +lemma one_plus_numeral: "1 + numeral n = numeral (One + n)"
   1.359 +  using numeral_add [of One n] by (simp add: numeral_One)
   1.360 +
   1.361 +lemma one_add_one: "1 + 1 = 2"
   1.362 +  using numeral_add [of One One] by (simp add: numeral_One)
   1.363 +
   1.364 +lemmas add_numeral_special =
   1.365 +  numeral_plus_one one_plus_numeral one_add_one
   1.366 +
   1.367 +end
   1.368 +
   1.369 +subsubsection {*
   1.370 +  Structures with negation: class @{text neg_numeral}
   1.371 +*}
   1.372 +
   1.373 +context neg_numeral
   1.374 +begin
   1.375 +
   1.376 +text {* Numerals form an abelian subgroup. *}
   1.377 +
   1.378 +inductive is_num :: "'a \<Rightarrow> bool" where
   1.379 +  "is_num 1" |
   1.380 +  "is_num x \<Longrightarrow> is_num (- x)" |
   1.381 +  "\<lbrakk>is_num x; is_num y\<rbrakk> \<Longrightarrow> is_num (x + y)"
   1.382 +
   1.383 +lemma is_num_numeral: "is_num (numeral k)"
   1.384 +  by (induct k, simp_all add: numeral.simps is_num.intros)
   1.385 +
   1.386 +lemma is_num_add_commute:
   1.387 +  "\<lbrakk>is_num x; is_num y\<rbrakk> \<Longrightarrow> x + y = y + x"
   1.388 +  apply (induct x rule: is_num.induct)
   1.389 +  apply (induct y rule: is_num.induct)
   1.390 +  apply simp
   1.391 +  apply (rule_tac a=x in add_left_imp_eq)
   1.392 +  apply (rule_tac a=x in add_right_imp_eq)
   1.393 +  apply (simp add: add_assoc minus_add_cancel)
   1.394 +  apply (simp add: add_assoc [symmetric], simp add: add_assoc)
   1.395 +  apply (rule_tac a=x in add_left_imp_eq)
   1.396 +  apply (rule_tac a=x in add_right_imp_eq)
   1.397 +  apply (simp add: add_assoc minus_add_cancel add_minus_cancel)
   1.398 +  apply (simp add: add_assoc, simp add: add_assoc [symmetric])
   1.399 +  done
   1.400 +
   1.401 +lemma is_num_add_left_commute:
   1.402 +  "\<lbrakk>is_num x; is_num y\<rbrakk> \<Longrightarrow> x + (y + z) = y + (x + z)"
   1.403 +  by (simp only: add_assoc [symmetric] is_num_add_commute)
   1.404 +
   1.405 +lemmas is_num_normalize =
   1.406 +  add_assoc is_num_add_commute is_num_add_left_commute
   1.407 +  is_num.intros is_num_numeral
   1.408 +  diff_minus minus_add add_minus_cancel minus_add_cancel
   1.409 +
   1.410 +definition dbl :: "'a \<Rightarrow> 'a" where "dbl x = x + x"
   1.411 +definition dbl_inc :: "'a \<Rightarrow> 'a" where "dbl_inc x = x + x + 1"
   1.412 +definition dbl_dec :: "'a \<Rightarrow> 'a" where "dbl_dec x = x + x - 1"
   1.413 +
   1.414 +definition sub :: "num \<Rightarrow> num \<Rightarrow> 'a" where
   1.415 +  "sub k l = numeral k - numeral l"
   1.416 +
   1.417 +lemma numeral_BitM: "numeral (BitM n) = numeral (Bit0 n) - 1"
   1.418 +  by (simp only: BitM_plus_one [symmetric] numeral_add numeral_One eq_diff_eq)
   1.419 +
   1.420 +lemma dbl_simps [simp]:
   1.421 +  "dbl (neg_numeral k) = neg_numeral (Bit0 k)"
   1.422 +  "dbl 0 = 0"
   1.423 +  "dbl 1 = 2"
   1.424 +  "dbl (numeral k) = numeral (Bit0 k)"
   1.425 +  unfolding dbl_def neg_numeral_def numeral.simps
   1.426 +  by (simp_all add: minus_add)
   1.427 +
   1.428 +lemma dbl_inc_simps [simp]:
   1.429 +  "dbl_inc (neg_numeral k) = neg_numeral (BitM k)"
   1.430 +  "dbl_inc 0 = 1"
   1.431 +  "dbl_inc 1 = 3"
   1.432 +  "dbl_inc (numeral k) = numeral (Bit1 k)"
   1.433 +  unfolding dbl_inc_def neg_numeral_def numeral.simps numeral_BitM
   1.434 +  by (simp_all add: is_num_normalize)
   1.435 +
   1.436 +lemma dbl_dec_simps [simp]:
   1.437 +  "dbl_dec (neg_numeral k) = neg_numeral (Bit1 k)"
   1.438 +  "dbl_dec 0 = -1"
   1.439 +  "dbl_dec 1 = 1"
   1.440 +  "dbl_dec (numeral k) = numeral (BitM k)"
   1.441 +  unfolding dbl_dec_def neg_numeral_def numeral.simps numeral_BitM
   1.442 +  by (simp_all add: is_num_normalize)
   1.443 +
   1.444 +lemma sub_num_simps [simp]:
   1.445 +  "sub One One = 0"
   1.446 +  "sub One (Bit0 l) = neg_numeral (BitM l)"
   1.447 +  "sub One (Bit1 l) = neg_numeral (Bit0 l)"
   1.448 +  "sub (Bit0 k) One = numeral (BitM k)"
   1.449 +  "sub (Bit1 k) One = numeral (Bit0 k)"
   1.450 +  "sub (Bit0 k) (Bit0 l) = dbl (sub k l)"
   1.451 +  "sub (Bit0 k) (Bit1 l) = dbl_dec (sub k l)"
   1.452 +  "sub (Bit1 k) (Bit0 l) = dbl_inc (sub k l)"
   1.453 +  "sub (Bit1 k) (Bit1 l) = dbl (sub k l)"
   1.454 +  unfolding dbl_def dbl_dec_def dbl_inc_def sub_def
   1.455 +  unfolding neg_numeral_def numeral.simps numeral_BitM
   1.456 +  by (simp_all add: is_num_normalize)
   1.457 +
   1.458 +lemma add_neg_numeral_simps:
   1.459 +  "numeral m + neg_numeral n = sub m n"
   1.460 +  "neg_numeral m + numeral n = sub n m"
   1.461 +  "neg_numeral m + neg_numeral n = neg_numeral (m + n)"
   1.462 +  unfolding sub_def diff_minus neg_numeral_def numeral_add numeral.simps
   1.463 +  by (simp_all add: is_num_normalize)
   1.464 +
   1.465 +lemma add_neg_numeral_special:
   1.466 +  "1 + neg_numeral m = sub One m"
   1.467 +  "neg_numeral m + 1 = sub One m"
   1.468 +  unfolding sub_def diff_minus neg_numeral_def numeral_add numeral.simps
   1.469 +  by (simp_all add: is_num_normalize)
   1.470 +
   1.471 +lemma diff_numeral_simps:
   1.472 +  "numeral m - numeral n = sub m n"
   1.473 +  "numeral m - neg_numeral n = numeral (m + n)"
   1.474 +  "neg_numeral m - numeral n = neg_numeral (m + n)"
   1.475 +  "neg_numeral m - neg_numeral n = sub n m"
   1.476 +  unfolding neg_numeral_def sub_def diff_minus numeral_add numeral.simps
   1.477 +  by (simp_all add: is_num_normalize)
   1.478 +
   1.479 +lemma diff_numeral_special:
   1.480 +  "1 - numeral n = sub One n"
   1.481 +  "1 - neg_numeral n = numeral (One + n)"
   1.482 +  "numeral m - 1 = sub m One"
   1.483 +  "neg_numeral m - 1 = neg_numeral (m + One)"
   1.484 +  unfolding neg_numeral_def sub_def diff_minus numeral_add numeral.simps
   1.485 +  by (simp_all add: is_num_normalize)
   1.486 +
   1.487 +lemma minus_one: "- 1 = -1"
   1.488 +  unfolding neg_numeral_def numeral.simps ..
   1.489 +
   1.490 +lemma minus_numeral: "- numeral n = neg_numeral n"
   1.491 +  unfolding neg_numeral_def ..
   1.492 +
   1.493 +lemma minus_neg_numeral: "- neg_numeral n = numeral n"
   1.494 +  unfolding neg_numeral_def by simp
   1.495 +
   1.496 +lemmas minus_numeral_simps [simp] =
   1.497 +  minus_one minus_numeral minus_neg_numeral
   1.498 +
   1.499 +end
   1.500 +
   1.501 +subsubsection {*
   1.502 +  Structures with multiplication: class @{text semiring_numeral}
   1.503 +*}
   1.504 +
   1.505 +class semiring_numeral = semiring + monoid_mult
   1.506 +begin
   1.507 +
   1.508 +subclass numeral ..
   1.509 +
   1.510 +lemma numeral_mult: "numeral (m * n) = numeral m * numeral n"
   1.511 +  apply (induct n rule: num_induct)
   1.512 +  apply (simp add: numeral_One)
   1.513 +  apply (simp add: mult_inc numeral_inc numeral_add numeral_inc right_distrib)
   1.514 +  done
   1.515 +
   1.516 +lemma numeral_times_numeral: "numeral m * numeral n = numeral (m * n)"
   1.517 +  by (rule numeral_mult [symmetric])
   1.518 +
   1.519 +end
   1.520 +
   1.521 +subsubsection {*
   1.522 +  Structures with a zero: class @{text semiring_1}
   1.523 +*}
   1.524 +
   1.525 +context semiring_1
   1.526 +begin
   1.527 +
   1.528 +subclass semiring_numeral ..
   1.529 +
   1.530 +lemma of_nat_numeral [simp]: "of_nat (numeral n) = numeral n"
   1.531 +  by (induct n,
   1.532 +    simp_all only: numeral.simps numeral_class.numeral.simps of_nat_add of_nat_1)
   1.533 +
   1.534 +end
   1.535 +
   1.536 +lemma nat_of_num_numeral: "nat_of_num = numeral"
   1.537 +proof
   1.538 +  fix n
   1.539 +  have "numeral n = nat_of_num n"
   1.540 +    by (induct n) (simp_all add: numeral.simps)
   1.541 +  then show "nat_of_num n = numeral n" by simp
   1.542 +qed
   1.543 +
   1.544 +subsubsection {*
   1.545 +  Equality: class @{text semiring_char_0}
   1.546 +*}
   1.547 +
   1.548 +context semiring_char_0
   1.549 +begin
   1.550 +
   1.551 +lemma numeral_eq_iff: "numeral m = numeral n \<longleftrightarrow> m = n"
   1.552 +  unfolding of_nat_numeral [symmetric] nat_of_num_numeral [symmetric]
   1.553 +    of_nat_eq_iff num_eq_iff ..
   1.554 +
   1.555 +lemma numeral_eq_one_iff: "numeral n = 1 \<longleftrightarrow> n = One"
   1.556 +  by (rule numeral_eq_iff [of n One, unfolded numeral_One])
   1.557 +
   1.558 +lemma one_eq_numeral_iff: "1 = numeral n \<longleftrightarrow> One = n"
   1.559 +  by (rule numeral_eq_iff [of One n, unfolded numeral_One])
   1.560 +
   1.561 +lemma numeral_neq_zero: "numeral n \<noteq> 0"
   1.562 +  unfolding of_nat_numeral [symmetric] nat_of_num_numeral [symmetric]
   1.563 +  by (simp add: nat_of_num_pos)
   1.564 +
   1.565 +lemma zero_neq_numeral: "0 \<noteq> numeral n"
   1.566 +  unfolding eq_commute [of 0] by (rule numeral_neq_zero)
   1.567 +
   1.568 +lemmas eq_numeral_simps [simp] =
   1.569 +  numeral_eq_iff
   1.570 +  numeral_eq_one_iff
   1.571 +  one_eq_numeral_iff
   1.572 +  numeral_neq_zero
   1.573 +  zero_neq_numeral
   1.574 +
   1.575 +end
   1.576 +
   1.577 +subsubsection {*
   1.578 +  Comparisons: class @{text linordered_semidom}
   1.579 +*}
   1.580 +
   1.581 +text {*  Could be perhaps more general than here. *}
   1.582 +
   1.583 +context linordered_semidom
   1.584 +begin
   1.585 +
   1.586 +lemma numeral_le_iff: "numeral m \<le> numeral n \<longleftrightarrow> m \<le> n"
   1.587 +proof -
   1.588 +  have "of_nat (numeral m) \<le> of_nat (numeral n) \<longleftrightarrow> m \<le> n"
   1.589 +    unfolding less_eq_num_def nat_of_num_numeral of_nat_le_iff ..
   1.590 +  then show ?thesis by simp
   1.591 +qed
   1.592 +
   1.593 +lemma one_le_numeral: "1 \<le> numeral n"
   1.594 +using numeral_le_iff [of One n] by (simp add: numeral_One)
   1.595 +
   1.596 +lemma numeral_le_one_iff: "numeral n \<le> 1 \<longleftrightarrow> n \<le> One"
   1.597 +using numeral_le_iff [of n One] by (simp add: numeral_One)
   1.598 +
   1.599 +lemma numeral_less_iff: "numeral m < numeral n \<longleftrightarrow> m < n"
   1.600 +proof -
   1.601 +  have "of_nat (numeral m) < of_nat (numeral n) \<longleftrightarrow> m < n"
   1.602 +    unfolding less_num_def nat_of_num_numeral of_nat_less_iff ..
   1.603 +  then show ?thesis by simp
   1.604 +qed
   1.605 +
   1.606 +lemma not_numeral_less_one: "\<not> numeral n < 1"
   1.607 +  using numeral_less_iff [of n One] by (simp add: numeral_One)
   1.608 +
   1.609 +lemma one_less_numeral_iff: "1 < numeral n \<longleftrightarrow> One < n"
   1.610 +  using numeral_less_iff [of One n] by (simp add: numeral_One)
   1.611 +
   1.612 +lemma zero_le_numeral: "0 \<le> numeral n"
   1.613 +  by (induct n) (simp_all add: numeral.simps)
   1.614 +
   1.615 +lemma zero_less_numeral: "0 < numeral n"
   1.616 +  by (induct n) (simp_all add: numeral.simps add_pos_pos)
   1.617 +
   1.618 +lemma not_numeral_le_zero: "\<not> numeral n \<le> 0"
   1.619 +  by (simp add: not_le zero_less_numeral)
   1.620 +
   1.621 +lemma not_numeral_less_zero: "\<not> numeral n < 0"
   1.622 +  by (simp add: not_less zero_le_numeral)
   1.623 +
   1.624 +lemmas le_numeral_extra =
   1.625 +  zero_le_one not_one_le_zero
   1.626 +  order_refl [of 0] order_refl [of 1]
   1.627 +
   1.628 +lemmas less_numeral_extra =
   1.629 +  zero_less_one not_one_less_zero
   1.630 +  less_irrefl [of 0] less_irrefl [of 1]
   1.631 +
   1.632 +lemmas le_numeral_simps [simp] =
   1.633 +  numeral_le_iff
   1.634 +  one_le_numeral
   1.635 +  numeral_le_one_iff
   1.636 +  zero_le_numeral
   1.637 +  not_numeral_le_zero
   1.638 +
   1.639 +lemmas less_numeral_simps [simp] =
   1.640 +  numeral_less_iff
   1.641 +  one_less_numeral_iff
   1.642 +  not_numeral_less_one
   1.643 +  zero_less_numeral
   1.644 +  not_numeral_less_zero
   1.645 +
   1.646 +end
   1.647 +
   1.648 +subsubsection {*
   1.649 +  Multiplication and negation: class @{text ring_1}
   1.650 +*}
   1.651 +
   1.652 +context ring_1
   1.653 +begin
   1.654 +
   1.655 +subclass neg_numeral ..
   1.656 +
   1.657 +lemma mult_neg_numeral_simps:
   1.658 +  "neg_numeral m * neg_numeral n = numeral (m * n)"
   1.659 +  "neg_numeral m * numeral n = neg_numeral (m * n)"
   1.660 +  "numeral m * neg_numeral n = neg_numeral (m * n)"
   1.661 +  unfolding neg_numeral_def mult_minus_left mult_minus_right
   1.662 +  by (simp_all only: minus_minus numeral_mult)
   1.663 +
   1.664 +lemma mult_minus1 [simp]: "-1 * z = - z"
   1.665 +  unfolding neg_numeral_def numeral.simps mult_minus_left by simp
   1.666 +
   1.667 +lemma mult_minus1_right [simp]: "z * -1 = - z"
   1.668 +  unfolding neg_numeral_def numeral.simps mult_minus_right by simp
   1.669 +
   1.670 +end
   1.671 +
   1.672 +subsubsection {*
   1.673 +  Equality using @{text iszero} for rings with non-zero characteristic
   1.674 +*}
   1.675 +
   1.676 +context ring_1
   1.677 +begin
   1.678 +
   1.679 +definition iszero :: "'a \<Rightarrow> bool"
   1.680 +  where "iszero z \<longleftrightarrow> z = 0"
   1.681 +
   1.682 +lemma iszero_0 [simp]: "iszero 0"
   1.683 +  by (simp add: iszero_def)
   1.684 +
   1.685 +lemma not_iszero_1 [simp]: "\<not> iszero 1"
   1.686 +  by (simp add: iszero_def)
   1.687 +
   1.688 +lemma not_iszero_Numeral1: "\<not> iszero Numeral1"
   1.689 +  by (simp add: numeral_One)
   1.690 +
   1.691 +lemma iszero_neg_numeral [simp]:
   1.692 +  "iszero (neg_numeral w) \<longleftrightarrow> iszero (numeral w)"
   1.693 +  unfolding iszero_def neg_numeral_def
   1.694 +  by (rule neg_equal_0_iff_equal)
   1.695 +
   1.696 +lemma eq_iff_iszero_diff: "x = y \<longleftrightarrow> iszero (x - y)"
   1.697 +  unfolding iszero_def by (rule eq_iff_diff_eq_0)
   1.698 +
   1.699 +text {* The @{text "eq_numeral_iff_iszero"} lemmas are not declared
   1.700 +@{text "[simp]"} by default, because for rings of characteristic zero,
   1.701 +better simp rules are possible. For a type like integers mod @{text
   1.702 +"n"}, type-instantiated versions of these rules should be added to the
   1.703 +simplifier, along with a type-specific rule for deciding propositions
   1.704 +of the form @{text "iszero (numeral w)"}.
   1.705 +
   1.706 +bh: Maybe it would not be so bad to just declare these as simp
   1.707 +rules anyway? I should test whether these rules take precedence over
   1.708 +the @{text "ring_char_0"} rules in the simplifier.
   1.709 +*}
   1.710 +
   1.711 +lemma eq_numeral_iff_iszero:
   1.712 +  "numeral x = numeral y \<longleftrightarrow> iszero (sub x y)"
   1.713 +  "numeral x = neg_numeral y \<longleftrightarrow> iszero (numeral (x + y))"
   1.714 +  "neg_numeral x = numeral y \<longleftrightarrow> iszero (numeral (x + y))"
   1.715 +  "neg_numeral x = neg_numeral y \<longleftrightarrow> iszero (sub y x)"
   1.716 +  "numeral x = 1 \<longleftrightarrow> iszero (sub x One)"
   1.717 +  "1 = numeral y \<longleftrightarrow> iszero (sub One y)"
   1.718 +  "neg_numeral x = 1 \<longleftrightarrow> iszero (numeral (x + One))"
   1.719 +  "1 = neg_numeral y \<longleftrightarrow> iszero (numeral (One + y))"
   1.720 +  "numeral x = 0 \<longleftrightarrow> iszero (numeral x)"
   1.721 +  "0 = numeral y \<longleftrightarrow> iszero (numeral y)"
   1.722 +  "neg_numeral x = 0 \<longleftrightarrow> iszero (numeral x)"
   1.723 +  "0 = neg_numeral y \<longleftrightarrow> iszero (numeral y)"
   1.724 +  unfolding eq_iff_iszero_diff diff_numeral_simps diff_numeral_special
   1.725 +  by simp_all
   1.726 +
   1.727 +end
   1.728 +
   1.729 +subsubsection {*
   1.730 +  Equality and negation: class @{text ring_char_0}
   1.731 +*}
   1.732 +
   1.733 +class ring_char_0 = ring_1 + semiring_char_0
   1.734 +begin
   1.735 +
   1.736 +lemma not_iszero_numeral [simp]: "\<not> iszero (numeral w)"
   1.737 +  by (simp add: iszero_def)
   1.738 +
   1.739 +lemma neg_numeral_eq_iff: "neg_numeral m = neg_numeral n \<longleftrightarrow> m = n"
   1.740 +  by (simp only: neg_numeral_def neg_equal_iff_equal numeral_eq_iff)
   1.741 +
   1.742 +lemma numeral_neq_neg_numeral: "numeral m \<noteq> neg_numeral n"
   1.743 +  unfolding neg_numeral_def eq_neg_iff_add_eq_0
   1.744 +  by (simp add: numeral_plus_numeral)
   1.745 +
   1.746 +lemma neg_numeral_neq_numeral: "neg_numeral m \<noteq> numeral n"
   1.747 +  by (rule numeral_neq_neg_numeral [symmetric])
   1.748 +
   1.749 +lemma zero_neq_neg_numeral: "0 \<noteq> neg_numeral n"
   1.750 +  unfolding neg_numeral_def neg_0_equal_iff_equal by simp
   1.751 +
   1.752 +lemma neg_numeral_neq_zero: "neg_numeral n \<noteq> 0"
   1.753 +  unfolding neg_numeral_def neg_equal_0_iff_equal by simp
   1.754 +
   1.755 +lemma one_neq_neg_numeral: "1 \<noteq> neg_numeral n"
   1.756 +  using numeral_neq_neg_numeral [of One n] by (simp add: numeral_One)
   1.757 +
   1.758 +lemma neg_numeral_neq_one: "neg_numeral n \<noteq> 1"
   1.759 +  using neg_numeral_neq_numeral [of n One] by (simp add: numeral_One)
   1.760 +
   1.761 +lemmas eq_neg_numeral_simps [simp] =
   1.762 +  neg_numeral_eq_iff
   1.763 +  numeral_neq_neg_numeral neg_numeral_neq_numeral
   1.764 +  one_neq_neg_numeral neg_numeral_neq_one
   1.765 +  zero_neq_neg_numeral neg_numeral_neq_zero
   1.766 +
   1.767 +end
   1.768 +
   1.769 +subsubsection {*
   1.770 +  Structures with negation and order: class @{text linordered_idom}
   1.771 +*}
   1.772 +
   1.773 +context linordered_idom
   1.774 +begin
   1.775 +
   1.776 +subclass ring_char_0 ..
   1.777 +
   1.778 +lemma neg_numeral_le_iff: "neg_numeral m \<le> neg_numeral n \<longleftrightarrow> n \<le> m"
   1.779 +  by (simp only: neg_numeral_def neg_le_iff_le numeral_le_iff)
   1.780 +
   1.781 +lemma neg_numeral_less_iff: "neg_numeral m < neg_numeral n \<longleftrightarrow> n < m"
   1.782 +  by (simp only: neg_numeral_def neg_less_iff_less numeral_less_iff)
   1.783 +
   1.784 +lemma neg_numeral_less_zero: "neg_numeral n < 0"
   1.785 +  by (simp only: neg_numeral_def neg_less_0_iff_less zero_less_numeral)
   1.786 +
   1.787 +lemma neg_numeral_le_zero: "neg_numeral n \<le> 0"
   1.788 +  by (simp only: neg_numeral_def neg_le_0_iff_le zero_le_numeral)
   1.789 +
   1.790 +lemma not_zero_less_neg_numeral: "\<not> 0 < neg_numeral n"
   1.791 +  by (simp only: not_less neg_numeral_le_zero)
   1.792 +
   1.793 +lemma not_zero_le_neg_numeral: "\<not> 0 \<le> neg_numeral n"
   1.794 +  by (simp only: not_le neg_numeral_less_zero)
   1.795 +
   1.796 +lemma neg_numeral_less_numeral: "neg_numeral m < numeral n"
   1.797 +  using neg_numeral_less_zero zero_less_numeral by (rule less_trans)
   1.798 +
   1.799 +lemma neg_numeral_le_numeral: "neg_numeral m \<le> numeral n"
   1.800 +  by (simp only: less_imp_le neg_numeral_less_numeral)
   1.801 +
   1.802 +lemma not_numeral_less_neg_numeral: "\<not> numeral m < neg_numeral n"
   1.803 +  by (simp only: not_less neg_numeral_le_numeral)
   1.804 +
   1.805 +lemma not_numeral_le_neg_numeral: "\<not> numeral m \<le> neg_numeral n"
   1.806 +  by (simp only: not_le neg_numeral_less_numeral)
   1.807 +  
   1.808 +lemma neg_numeral_less_one: "neg_numeral m < 1"
   1.809 +  by (rule neg_numeral_less_numeral [of m One, unfolded numeral_One])
   1.810 +
   1.811 +lemma neg_numeral_le_one: "neg_numeral m \<le> 1"
   1.812 +  by (rule neg_numeral_le_numeral [of m One, unfolded numeral_One])
   1.813 +
   1.814 +lemma not_one_less_neg_numeral: "\<not> 1 < neg_numeral m"
   1.815 +  by (simp only: not_less neg_numeral_le_one)
   1.816 +
   1.817 +lemma not_one_le_neg_numeral: "\<not> 1 \<le> neg_numeral m"
   1.818 +  by (simp only: not_le neg_numeral_less_one)
   1.819 +
   1.820 +lemma sub_non_negative:
   1.821 +  "sub n m \<ge> 0 \<longleftrightarrow> n \<ge> m"
   1.822 +  by (simp only: sub_def le_diff_eq) simp
   1.823 +
   1.824 +lemma sub_positive:
   1.825 +  "sub n m > 0 \<longleftrightarrow> n > m"
   1.826 +  by (simp only: sub_def less_diff_eq) simp
   1.827 +
   1.828 +lemma sub_non_positive:
   1.829 +  "sub n m \<le> 0 \<longleftrightarrow> n \<le> m"
   1.830 +  by (simp only: sub_def diff_le_eq) simp
   1.831 +
   1.832 +lemma sub_negative:
   1.833 +  "sub n m < 0 \<longleftrightarrow> n < m"
   1.834 +  by (simp only: sub_def diff_less_eq) simp
   1.835 +
   1.836 +lemmas le_neg_numeral_simps [simp] =
   1.837 +  neg_numeral_le_iff
   1.838 +  neg_numeral_le_numeral not_numeral_le_neg_numeral
   1.839 +  neg_numeral_le_zero not_zero_le_neg_numeral
   1.840 +  neg_numeral_le_one not_one_le_neg_numeral
   1.841 +
   1.842 +lemmas less_neg_numeral_simps [simp] =
   1.843 +  neg_numeral_less_iff
   1.844 +  neg_numeral_less_numeral not_numeral_less_neg_numeral
   1.845 +  neg_numeral_less_zero not_zero_less_neg_numeral
   1.846 +  neg_numeral_less_one not_one_less_neg_numeral
   1.847 +
   1.848 +lemma abs_numeral [simp]: "abs (numeral n) = numeral n"
   1.849 +  by simp
   1.850 +
   1.851 +lemma abs_neg_numeral [simp]: "abs (neg_numeral n) = numeral n"
   1.852 +  by (simp only: neg_numeral_def abs_minus_cancel abs_numeral)
   1.853 +
   1.854 +end
   1.855 +
   1.856 +subsubsection {*
   1.857 +  Natural numbers
   1.858 +*}
   1.859 +
   1.860 +lemma Suc_numeral [simp]: "Suc (numeral n) = numeral (n + One)"
   1.861 +  unfolding numeral_plus_one [symmetric] by simp
   1.862 +
   1.863 +lemma nat_number:
   1.864 +  "1 = Suc 0"
   1.865 +  "numeral One = Suc 0"
   1.866 +  "numeral (Bit0 n) = Suc (numeral (BitM n))"
   1.867 +  "numeral (Bit1 n) = Suc (numeral (Bit0 n))"
   1.868 +  by (simp_all add: numeral.simps BitM_plus_one)
   1.869 +
   1.870 +subsubsection {*
   1.871 +  Structures with exponentiation
   1.872 +*}
   1.873 +
   1.874 +context semiring_numeral
   1.875 +begin
   1.876 +
   1.877 +lemma numeral_sqr: "numeral (sqr n) = numeral n * numeral n"
   1.878 +  by (simp add: sqr_conv_mult numeral_mult)
   1.879 +
   1.880 +lemma numeral_pow: "numeral (pow m n) = numeral m ^ numeral n"
   1.881 +  by (induct n, simp_all add: numeral_class.numeral.simps
   1.882 +    power_add numeral_sqr numeral_mult)
   1.883 +
   1.884 +lemma power_numeral [simp]: "numeral m ^ numeral n = numeral (pow m n)"
   1.885 +  by (rule numeral_pow [symmetric])
   1.886 +
   1.887 +end
   1.888 +
   1.889 +context semiring_1
   1.890 +begin
   1.891 +
   1.892 +lemma power_zero_numeral [simp]: "(0::'a) ^ numeral n = 0"
   1.893 +  by (induct n, simp_all add: numeral_class.numeral.simps power_add)
   1.894 +
   1.895 +end
   1.896 +
   1.897 +context ring_1
   1.898 +begin
   1.899 +
   1.900 +lemma power_minus_Bit0: "(- x) ^ numeral (Bit0 n) = x ^ numeral (Bit0 n)"
   1.901 +  by (induct n, simp_all add: numeral_class.numeral.simps power_add)
   1.902 +
   1.903 +lemma power_minus_Bit1: "(- x) ^ numeral (Bit1 n) = - (x ^ numeral (Bit1 n))"
   1.904 +  by (simp only: nat_number(4) power_Suc power_minus_Bit0 mult_minus_left)
   1.905 +
   1.906 +lemma power_neg_numeral_Bit0 [simp]:
   1.907 +  "neg_numeral m ^ numeral (Bit0 n) = numeral (pow m (Bit0 n))"
   1.908 +  by (simp only: neg_numeral_def power_minus_Bit0 power_numeral)
   1.909 +
   1.910 +lemma power_neg_numeral_Bit1 [simp]:
   1.911 +  "neg_numeral m ^ numeral (Bit1 n) = neg_numeral (pow m (Bit1 n))"
   1.912 +  by (simp only: neg_numeral_def power_minus_Bit1 power_numeral pow.simps)
   1.913 +
   1.914 +end
   1.915 +
   1.916 +subsection {* Numeral equations as default simplification rules *}
   1.917 +
   1.918 +declare (in numeral) numeral_One [simp]
   1.919 +declare (in numeral) numeral_plus_numeral [simp]
   1.920 +declare (in numeral) add_numeral_special [simp]
   1.921 +declare (in neg_numeral) add_neg_numeral_simps [simp]
   1.922 +declare (in neg_numeral) add_neg_numeral_special [simp]
   1.923 +declare (in neg_numeral) diff_numeral_simps [simp]
   1.924 +declare (in neg_numeral) diff_numeral_special [simp]
   1.925 +declare (in semiring_numeral) numeral_times_numeral [simp]
   1.926 +declare (in ring_1) mult_neg_numeral_simps [simp]
   1.927 +
   1.928 +subsection {* Setting up simprocs *}
   1.929 +
   1.930 +lemma numeral_reorient:
   1.931 +  "(numeral w = x) = (x = numeral w)"
   1.932 +  by auto
   1.933 +
   1.934 +lemma mult_numeral_1: "Numeral1 * a = (a::'a::semiring_numeral)"
   1.935 +  by simp
   1.936 +
   1.937 +lemma mult_numeral_1_right: "a * Numeral1 = (a::'a::semiring_numeral)"
   1.938 +  by simp
   1.939 +
   1.940 +lemma divide_numeral_1: "a / Numeral1 = (a::'a::field)"
   1.941 +  by simp
   1.942 +
   1.943 +lemma inverse_numeral_1:
   1.944 +  "inverse Numeral1 = (Numeral1::'a::division_ring)"
   1.945 +  by simp
   1.946 +
   1.947 +text{*Theorem lists for the cancellation simprocs. The use of a numary
   1.948 +numeral for 1 reduces the number of special cases.*}
   1.949 +
   1.950 +lemmas mult_1s =
   1.951 +  mult_numeral_1 mult_numeral_1_right 
   1.952 +  mult_minus1 mult_minus1_right
   1.953 +
   1.954 +
   1.955 +subsubsection {* Simplification of arithmetic operations on integer constants. *}
   1.956 +
   1.957 +lemmas arith_special = (* already declared simp above *)
   1.958 +  add_numeral_special add_neg_numeral_special
   1.959 +  diff_numeral_special minus_one
   1.960 +
   1.961 +(* rules already in simpset *)
   1.962 +lemmas arith_extra_simps =
   1.963 +  numeral_plus_numeral add_neg_numeral_simps add_0_left add_0_right
   1.964 +  minus_numeral minus_neg_numeral minus_zero minus_one
   1.965 +  diff_numeral_simps diff_0 diff_0_right
   1.966 +  numeral_times_numeral mult_neg_numeral_simps
   1.967 +  mult_zero_left mult_zero_right
   1.968 +  abs_numeral abs_neg_numeral
   1.969 +
   1.970 +text {*
   1.971 +  For making a minimal simpset, one must include these default simprules.
   1.972 +  Also include @{text simp_thms}.
   1.973 +*}
   1.974 +
   1.975 +lemmas arith_simps =
   1.976 +  add_num_simps mult_num_simps sub_num_simps
   1.977 +  BitM.simps dbl_simps dbl_inc_simps dbl_dec_simps
   1.978 +  abs_zero abs_one arith_extra_simps
   1.979 +
   1.980 +text {* Simplification of relational operations *}
   1.981 +
   1.982 +lemmas eq_numeral_extra =
   1.983 +  zero_neq_one one_neq_zero
   1.984 +
   1.985 +lemmas rel_simps =
   1.986 +  le_num_simps less_num_simps eq_num_simps
   1.987 +  le_numeral_simps le_neg_numeral_simps le_numeral_extra
   1.988 +  less_numeral_simps less_neg_numeral_simps less_numeral_extra
   1.989 +  eq_numeral_simps eq_neg_numeral_simps eq_numeral_extra
   1.990 +
   1.991 +
   1.992 +subsubsection {* Simplification of arithmetic when nested to the right. *}
   1.993 +
   1.994 +lemma add_numeral_left [simp]:
   1.995 +  "numeral v + (numeral w + z) = (numeral(v + w) + z)"
   1.996 +  by (simp_all add: add_assoc [symmetric])
   1.997 +
   1.998 +lemma add_neg_numeral_left [simp]:
   1.999 +  "numeral v + (neg_numeral w + y) = (sub v w + y)"
  1.1000 +  "neg_numeral v + (numeral w + y) = (sub w v + y)"
  1.1001 +  "neg_numeral v + (neg_numeral w + y) = (neg_numeral(v + w) + y)"
  1.1002 +  by (simp_all add: add_assoc [symmetric])
  1.1003 +
  1.1004 +lemma mult_numeral_left [simp]:
  1.1005 +  "numeral v * (numeral w * z) = (numeral(v * w) * z :: 'a::semiring_numeral)"
  1.1006 +  "neg_numeral v * (numeral w * y) = (neg_numeral(v * w) * y :: 'b::ring_1)"
  1.1007 +  "numeral v * (neg_numeral w * y) = (neg_numeral(v * w) * y :: 'b::ring_1)"
  1.1008 +  "neg_numeral v * (neg_numeral w * y) = (numeral(v * w) * y :: 'b::ring_1)"
  1.1009 +  by (simp_all add: mult_assoc [symmetric])
  1.1010 +
  1.1011 +hide_const (open) One Bit0 Bit1 BitM inc pow sqr sub dbl dbl_inc dbl_dec
  1.1012 +
  1.1013 +subsection {* code module namespace *}
  1.1014 +
  1.1015 +code_modulename SML
  1.1016 +  Numeral Arith
  1.1017 +
  1.1018 +code_modulename OCaml
  1.1019 +  Numeral Arith
  1.1020 +
  1.1021 +code_modulename Haskell
  1.1022 +  Numeral Arith
  1.1023 +
  1.1024 +end