src/HOL/Num.thy
author wenzelm
Sat Nov 04 15:24:40 2017 +0100 (19 months ago)
changeset 67003 49850a679c2c
parent 66936 cf8d8fc23891
child 67116 7397a6df81d8
permissions -rw-r--r--
more robust sorted_entries;
     1 (*  Title:      HOL/Num.thy
     2     Author:     Florian Haftmann
     3     Author:     Brian Huffman
     4 *)
     5 
     6 section \<open>Binary Numerals\<close>
     7 
     8 theory Num
     9   imports BNF_Least_Fixpoint Transfer
    10 begin
    11 
    12 subsection \<open>The \<open>num\<close> type\<close>
    13 
    14 datatype num = One | Bit0 num | Bit1 num
    15 
    16 text \<open>Increment function for type @{typ num}\<close>
    17 
    18 primrec inc :: "num \<Rightarrow> num"
    19   where
    20     "inc One = Bit0 One"
    21   | "inc (Bit0 x) = Bit1 x"
    22   | "inc (Bit1 x) = Bit0 (inc x)"
    23 
    24 text \<open>Converting between type @{typ num} and type @{typ nat}\<close>
    25 
    26 primrec nat_of_num :: "num \<Rightarrow> nat"
    27   where
    28     "nat_of_num One = Suc 0"
    29   | "nat_of_num (Bit0 x) = nat_of_num x + nat_of_num x"
    30   | "nat_of_num (Bit1 x) = Suc (nat_of_num x + nat_of_num x)"
    31 
    32 primrec num_of_nat :: "nat \<Rightarrow> num"
    33   where
    34     "num_of_nat 0 = One"
    35   | "num_of_nat (Suc n) = (if 0 < n then inc (num_of_nat n) else One)"
    36 
    37 lemma nat_of_num_pos: "0 < nat_of_num x"
    38   by (induct x) simp_all
    39 
    40 lemma nat_of_num_neq_0: " nat_of_num x \<noteq> 0"
    41   by (induct x) simp_all
    42 
    43 lemma nat_of_num_inc: "nat_of_num (inc x) = Suc (nat_of_num x)"
    44   by (induct x) simp_all
    45 
    46 lemma num_of_nat_double: "0 < n \<Longrightarrow> num_of_nat (n + n) = Bit0 (num_of_nat n)"
    47   by (induct n) simp_all
    48 
    49 text \<open>Type @{typ num} is isomorphic to the strictly positive natural numbers.\<close>
    50 
    51 lemma nat_of_num_inverse: "num_of_nat (nat_of_num x) = x"
    52   by (induct x) (simp_all add: num_of_nat_double nat_of_num_pos)
    53 
    54 lemma num_of_nat_inverse: "0 < n \<Longrightarrow> nat_of_num (num_of_nat n) = n"
    55   by (induct n) (simp_all add: nat_of_num_inc)
    56 
    57 lemma num_eq_iff: "x = y \<longleftrightarrow> nat_of_num x = nat_of_num y"
    58   apply safe
    59   apply (drule arg_cong [where f=num_of_nat])
    60   apply (simp add: nat_of_num_inverse)
    61   done
    62 
    63 lemma num_induct [case_names One inc]:
    64   fixes P :: "num \<Rightarrow> bool"
    65   assumes One: "P One"
    66     and inc: "\<And>x. P x \<Longrightarrow> P (inc x)"
    67   shows "P x"
    68 proof -
    69   obtain n where n: "Suc n = nat_of_num x"
    70     by (cases "nat_of_num x") (simp_all add: nat_of_num_neq_0)
    71   have "P (num_of_nat (Suc n))"
    72   proof (induct n)
    73     case 0
    74     from One show ?case by simp
    75   next
    76     case (Suc n)
    77     then have "P (inc (num_of_nat (Suc n)))" by (rule inc)
    78     then show "P (num_of_nat (Suc (Suc n)))" by simp
    79   qed
    80   with n show "P x"
    81     by (simp add: nat_of_num_inverse)
    82 qed
    83 
    84 text \<open>
    85   From now on, there are two possible models for @{typ num}: as positive
    86   naturals (rule \<open>num_induct\<close>) and as digit representation (rules
    87   \<open>num.induct\<close>, \<open>num.cases\<close>).
    88 \<close>
    89 
    90 
    91 subsection \<open>Numeral operations\<close>
    92 
    93 instantiation num :: "{plus,times,linorder}"
    94 begin
    95 
    96 definition [code del]: "m + n = num_of_nat (nat_of_num m + nat_of_num n)"
    97 
    98 definition [code del]: "m * n = num_of_nat (nat_of_num m * nat_of_num n)"
    99 
   100 definition [code del]: "m \<le> n \<longleftrightarrow> nat_of_num m \<le> nat_of_num n"
   101 
   102 definition [code del]: "m < n \<longleftrightarrow> nat_of_num m < nat_of_num n"
   103 
   104 instance
   105   by standard (auto simp add: less_num_def less_eq_num_def num_eq_iff)
   106 
   107 end
   108 
   109 lemma nat_of_num_add: "nat_of_num (x + y) = nat_of_num x + nat_of_num y"
   110   unfolding plus_num_def
   111   by (intro num_of_nat_inverse add_pos_pos nat_of_num_pos)
   112 
   113 lemma nat_of_num_mult: "nat_of_num (x * y) = nat_of_num x * nat_of_num y"
   114   unfolding times_num_def
   115   by (intro num_of_nat_inverse mult_pos_pos nat_of_num_pos)
   116 
   117 lemma add_num_simps [simp, code]:
   118   "One + One = Bit0 One"
   119   "One + Bit0 n = Bit1 n"
   120   "One + Bit1 n = Bit0 (n + One)"
   121   "Bit0 m + One = Bit1 m"
   122   "Bit0 m + Bit0 n = Bit0 (m + n)"
   123   "Bit0 m + Bit1 n = Bit1 (m + n)"
   124   "Bit1 m + One = Bit0 (m + One)"
   125   "Bit1 m + Bit0 n = Bit1 (m + n)"
   126   "Bit1 m + Bit1 n = Bit0 (m + n + One)"
   127   by (simp_all add: num_eq_iff nat_of_num_add)
   128 
   129 lemma mult_num_simps [simp, code]:
   130   "m * One = m"
   131   "One * n = n"
   132   "Bit0 m * Bit0 n = Bit0 (Bit0 (m * n))"
   133   "Bit0 m * Bit1 n = Bit0 (m * Bit1 n)"
   134   "Bit1 m * Bit0 n = Bit0 (Bit1 m * n)"
   135   "Bit1 m * Bit1 n = Bit1 (m + n + Bit0 (m * n))"
   136   by (simp_all add: num_eq_iff nat_of_num_add nat_of_num_mult distrib_right distrib_left)
   137 
   138 lemma eq_num_simps:
   139   "One = One \<longleftrightarrow> True"
   140   "One = Bit0 n \<longleftrightarrow> False"
   141   "One = Bit1 n \<longleftrightarrow> False"
   142   "Bit0 m = One \<longleftrightarrow> False"
   143   "Bit1 m = One \<longleftrightarrow> False"
   144   "Bit0 m = Bit0 n \<longleftrightarrow> m = n"
   145   "Bit0 m = Bit1 n \<longleftrightarrow> False"
   146   "Bit1 m = Bit0 n \<longleftrightarrow> False"
   147   "Bit1 m = Bit1 n \<longleftrightarrow> m = n"
   148   by simp_all
   149 
   150 lemma le_num_simps [simp, code]:
   151   "One \<le> n \<longleftrightarrow> True"
   152   "Bit0 m \<le> One \<longleftrightarrow> False"
   153   "Bit1 m \<le> One \<longleftrightarrow> False"
   154   "Bit0 m \<le> Bit0 n \<longleftrightarrow> m \<le> n"
   155   "Bit0 m \<le> Bit1 n \<longleftrightarrow> m \<le> n"
   156   "Bit1 m \<le> Bit1 n \<longleftrightarrow> m \<le> n"
   157   "Bit1 m \<le> Bit0 n \<longleftrightarrow> m < n"
   158   using nat_of_num_pos [of n] nat_of_num_pos [of m]
   159   by (auto simp add: less_eq_num_def less_num_def)
   160 
   161 lemma less_num_simps [simp, code]:
   162   "m < One \<longleftrightarrow> False"
   163   "One < Bit0 n \<longleftrightarrow> True"
   164   "One < Bit1 n \<longleftrightarrow> True"
   165   "Bit0 m < Bit0 n \<longleftrightarrow> m < n"
   166   "Bit0 m < Bit1 n \<longleftrightarrow> m \<le> n"
   167   "Bit1 m < Bit1 n \<longleftrightarrow> m < n"
   168   "Bit1 m < Bit0 n \<longleftrightarrow> m < n"
   169   using nat_of_num_pos [of n] nat_of_num_pos [of m]
   170   by (auto simp add: less_eq_num_def less_num_def)
   171 
   172 lemma le_num_One_iff: "x \<le> num.One \<longleftrightarrow> x = num.One"
   173   by (simp add: antisym_conv)
   174 
   175 text \<open>Rules using \<open>One\<close> and \<open>inc\<close> as constructors.\<close>
   176 
   177 lemma add_One: "x + One = inc x"
   178   by (simp add: num_eq_iff nat_of_num_add nat_of_num_inc)
   179 
   180 lemma add_One_commute: "One + n = n + One"
   181   by (induct n) simp_all
   182 
   183 lemma add_inc: "x + inc y = inc (x + y)"
   184   by (simp add: num_eq_iff nat_of_num_add nat_of_num_inc)
   185 
   186 lemma mult_inc: "x * inc y = x * y + x"
   187   by (simp add: num_eq_iff nat_of_num_mult nat_of_num_add nat_of_num_inc)
   188 
   189 text \<open>The @{const num_of_nat} conversion.\<close>
   190 
   191 lemma num_of_nat_One: "n \<le> 1 \<Longrightarrow> num_of_nat n = One"
   192   by (cases n) simp_all
   193 
   194 lemma num_of_nat_plus_distrib:
   195   "0 < m \<Longrightarrow> 0 < n \<Longrightarrow> num_of_nat (m + n) = num_of_nat m + num_of_nat n"
   196   by (induct n) (auto simp add: add_One add_One_commute add_inc)
   197 
   198 text \<open>A double-and-decrement function.\<close>
   199 
   200 primrec BitM :: "num \<Rightarrow> num"
   201   where
   202     "BitM One = One"
   203   | "BitM (Bit0 n) = Bit1 (BitM n)"
   204   | "BitM (Bit1 n) = Bit1 (Bit0 n)"
   205 
   206 lemma BitM_plus_one: "BitM n + One = Bit0 n"
   207   by (induct n) simp_all
   208 
   209 lemma one_plus_BitM: "One + BitM n = Bit0 n"
   210   unfolding add_One_commute BitM_plus_one ..
   211 
   212 text \<open>Squaring and exponentiation.\<close>
   213 
   214 primrec sqr :: "num \<Rightarrow> num"
   215   where
   216     "sqr One = One"
   217   | "sqr (Bit0 n) = Bit0 (Bit0 (sqr n))"
   218   | "sqr (Bit1 n) = Bit1 (Bit0 (sqr n + n))"
   219 
   220 primrec pow :: "num \<Rightarrow> num \<Rightarrow> num"
   221   where
   222     "pow x One = x"
   223   | "pow x (Bit0 y) = sqr (pow x y)"
   224   | "pow x (Bit1 y) = sqr (pow x y) * x"
   225 
   226 lemma nat_of_num_sqr: "nat_of_num (sqr x) = nat_of_num x * nat_of_num x"
   227   by (induct x) (simp_all add: algebra_simps nat_of_num_add)
   228 
   229 lemma sqr_conv_mult: "sqr x = x * x"
   230   by (simp add: num_eq_iff nat_of_num_sqr nat_of_num_mult)
   231 
   232 
   233 subsection \<open>Binary numerals\<close>
   234 
   235 text \<open>
   236   We embed binary representations into a generic algebraic
   237   structure using \<open>numeral\<close>.
   238 \<close>
   239 
   240 class numeral = one + semigroup_add
   241 begin
   242 
   243 primrec numeral :: "num \<Rightarrow> 'a"
   244   where
   245     numeral_One: "numeral One = 1"
   246   | numeral_Bit0: "numeral (Bit0 n) = numeral n + numeral n"
   247   | numeral_Bit1: "numeral (Bit1 n) = numeral n + numeral n + 1"
   248 
   249 lemma numeral_code [code]:
   250   "numeral One = 1"
   251   "numeral (Bit0 n) = (let m = numeral n in m + m)"
   252   "numeral (Bit1 n) = (let m = numeral n in m + m + 1)"
   253   by (simp_all add: Let_def)
   254 
   255 lemma one_plus_numeral_commute: "1 + numeral x = numeral x + 1"
   256 proof (induct x)
   257   case One
   258   then show ?case by simp
   259 next
   260   case Bit0
   261   then show ?case by (simp add: add.assoc [symmetric]) (simp add: add.assoc)
   262 next
   263   case Bit1
   264   then show ?case by (simp add: add.assoc [symmetric]) (simp add: add.assoc)
   265 qed
   266 
   267 lemma numeral_inc: "numeral (inc x) = numeral x + 1"
   268 proof (induct x)
   269   case One
   270   then show ?case by simp
   271 next
   272   case Bit0
   273   then show ?case by simp
   274 next
   275   case (Bit1 x)
   276   have "numeral x + (1 + numeral x) + 1 = numeral x + (numeral x + 1) + 1"
   277     by (simp only: one_plus_numeral_commute)
   278   with Bit1 show ?case
   279     by (simp add: add.assoc)
   280 qed
   281 
   282 declare numeral.simps [simp del]
   283 
   284 abbreviation "Numeral1 \<equiv> numeral One"
   285 
   286 declare numeral_One [code_post]
   287 
   288 end
   289 
   290 text \<open>Numeral syntax.\<close>
   291 
   292 syntax
   293   "_Numeral" :: "num_const \<Rightarrow> 'a"    ("_")
   294 
   295 ML_file "Tools/numeral.ML"
   296 
   297 parse_translation \<open>
   298   let
   299     fun numeral_tr [(c as Const (@{syntax_const "_constrain"}, _)) $ t $ u] =
   300           c $ numeral_tr [t] $ u
   301       | numeral_tr [Const (num, _)] =
   302           (Numeral.mk_number_syntax o #value o Lexicon.read_num) num
   303       | numeral_tr ts = raise TERM ("numeral_tr", ts);
   304   in [(@{syntax_const "_Numeral"}, K numeral_tr)] end
   305 \<close>
   306 
   307 typed_print_translation \<open>
   308   let
   309     fun num_tr' ctxt T [n] =
   310       let
   311         val k = Numeral.dest_num_syntax n;
   312         val t' =
   313           Syntax.const @{syntax_const "_Numeral"} $
   314             Syntax.free (string_of_int k);
   315       in
   316         (case T of
   317           Type (@{type_name fun}, [_, T']) =>
   318             if Printer.type_emphasis ctxt T' then
   319               Syntax.const @{syntax_const "_constrain"} $ t' $
   320                 Syntax_Phases.term_of_typ ctxt T'
   321             else t'
   322         | _ => if T = dummyT then t' else raise Match)
   323       end;
   324   in
   325    [(@{const_syntax numeral}, num_tr')]
   326   end
   327 \<close>
   328 
   329 
   330 subsection \<open>Class-specific numeral rules\<close>
   331 
   332 text \<open>@{const numeral} is a morphism.\<close>
   333 
   334 
   335 subsubsection \<open>Structures with addition: class \<open>numeral\<close>\<close>
   336 
   337 context numeral
   338 begin
   339 
   340 lemma numeral_add: "numeral (m + n) = numeral m + numeral n"
   341   by (induct n rule: num_induct)
   342     (simp_all only: numeral_One add_One add_inc numeral_inc add.assoc)
   343 
   344 lemma numeral_plus_numeral: "numeral m + numeral n = numeral (m + n)"
   345   by (rule numeral_add [symmetric])
   346 
   347 lemma numeral_plus_one: "numeral n + 1 = numeral (n + One)"
   348   using numeral_add [of n One] by (simp add: numeral_One)
   349 
   350 lemma one_plus_numeral: "1 + numeral n = numeral (One + n)"
   351   using numeral_add [of One n] by (simp add: numeral_One)
   352 
   353 lemma one_add_one: "1 + 1 = 2"
   354   using numeral_add [of One One] by (simp add: numeral_One)
   355 
   356 lemmas add_numeral_special =
   357   numeral_plus_one one_plus_numeral one_add_one
   358 
   359 end
   360 
   361 
   362 subsubsection \<open>Structures with negation: class \<open>neg_numeral\<close>\<close>
   363 
   364 class neg_numeral = numeral + group_add
   365 begin
   366 
   367 lemma uminus_numeral_One: "- Numeral1 = - 1"
   368   by (simp add: numeral_One)
   369 
   370 text \<open>Numerals form an abelian subgroup.\<close>
   371 
   372 inductive is_num :: "'a \<Rightarrow> bool"
   373   where
   374     "is_num 1"
   375   | "is_num x \<Longrightarrow> is_num (- x)"
   376   | "is_num x \<Longrightarrow> is_num y \<Longrightarrow> is_num (x + y)"
   377 
   378 lemma is_num_numeral: "is_num (numeral k)"
   379   by (induct k) (simp_all add: numeral.simps is_num.intros)
   380 
   381 lemma is_num_add_commute: "is_num x \<Longrightarrow> is_num y \<Longrightarrow> x + y = y + x"
   382   apply (induct x rule: is_num.induct)
   383     apply (induct y rule: is_num.induct)
   384       apply simp
   385      apply (rule_tac a=x in add_left_imp_eq)
   386      apply (rule_tac a=x in add_right_imp_eq)
   387      apply (simp add: add.assoc)
   388     apply (simp add: add.assoc [symmetric])
   389     apply (simp add: add.assoc)
   390    apply (rule_tac a=x in add_left_imp_eq)
   391    apply (rule_tac a=x in add_right_imp_eq)
   392    apply (simp add: add.assoc)
   393   apply (simp add: add.assoc)
   394   apply (simp add: add.assoc [symmetric])
   395   done
   396 
   397 lemma is_num_add_left_commute: "is_num x \<Longrightarrow> is_num y \<Longrightarrow> x + (y + z) = y + (x + z)"
   398   by (simp only: add.assoc [symmetric] is_num_add_commute)
   399 
   400 lemmas is_num_normalize =
   401   add.assoc is_num_add_commute is_num_add_left_commute
   402   is_num.intros is_num_numeral
   403   minus_add
   404 
   405 definition dbl :: "'a \<Rightarrow> 'a"
   406   where "dbl x = x + x"
   407 
   408 definition dbl_inc :: "'a \<Rightarrow> 'a"
   409   where "dbl_inc x = x + x + 1"
   410 
   411 definition dbl_dec :: "'a \<Rightarrow> 'a"
   412   where "dbl_dec x = x + x - 1"
   413 
   414 definition sub :: "num \<Rightarrow> num \<Rightarrow> 'a"
   415   where "sub k l = numeral k - numeral l"
   416 
   417 lemma numeral_BitM: "numeral (BitM n) = numeral (Bit0 n) - 1"
   418   by (simp only: BitM_plus_one [symmetric] numeral_add numeral_One eq_diff_eq)
   419 
   420 lemma dbl_simps [simp]:
   421   "dbl (- numeral k) = - dbl (numeral k)"
   422   "dbl 0 = 0"
   423   "dbl 1 = 2"
   424   "dbl (- 1) = - 2"
   425   "dbl (numeral k) = numeral (Bit0 k)"
   426   by (simp_all add: dbl_def numeral.simps minus_add)
   427 
   428 lemma dbl_inc_simps [simp]:
   429   "dbl_inc (- numeral k) = - dbl_dec (numeral k)"
   430   "dbl_inc 0 = 1"
   431   "dbl_inc 1 = 3"
   432   "dbl_inc (- 1) = - 1"
   433   "dbl_inc (numeral k) = numeral (Bit1 k)"
   434   by (simp_all add: dbl_inc_def dbl_dec_def numeral.simps numeral_BitM is_num_normalize algebra_simps
   435       del: add_uminus_conv_diff)
   436 
   437 lemma dbl_dec_simps [simp]:
   438   "dbl_dec (- numeral k) = - dbl_inc (numeral k)"
   439   "dbl_dec 0 = - 1"
   440   "dbl_dec 1 = 1"
   441   "dbl_dec (- 1) = - 3"
   442   "dbl_dec (numeral k) = numeral (BitM k)"
   443   by (simp_all add: dbl_dec_def dbl_inc_def numeral.simps numeral_BitM is_num_normalize)
   444 
   445 lemma sub_num_simps [simp]:
   446   "sub One One = 0"
   447   "sub One (Bit0 l) = - numeral (BitM l)"
   448   "sub One (Bit1 l) = - numeral (Bit0 l)"
   449   "sub (Bit0 k) One = numeral (BitM k)"
   450   "sub (Bit1 k) One = numeral (Bit0 k)"
   451   "sub (Bit0 k) (Bit0 l) = dbl (sub k l)"
   452   "sub (Bit0 k) (Bit1 l) = dbl_dec (sub k l)"
   453   "sub (Bit1 k) (Bit0 l) = dbl_inc (sub k l)"
   454   "sub (Bit1 k) (Bit1 l) = dbl (sub k l)"
   455   by (simp_all add: dbl_def dbl_dec_def dbl_inc_def sub_def numeral.simps
   456     numeral_BitM is_num_normalize del: add_uminus_conv_diff add: diff_conv_add_uminus)
   457 
   458 lemma add_neg_numeral_simps:
   459   "numeral m + - numeral n = sub m n"
   460   "- numeral m + numeral n = sub n m"
   461   "- numeral m + - numeral n = - (numeral m + numeral n)"
   462   by (simp_all add: sub_def numeral_add numeral.simps is_num_normalize
   463       del: add_uminus_conv_diff add: diff_conv_add_uminus)
   464 
   465 lemma add_neg_numeral_special:
   466   "1 + - numeral m = sub One m"
   467   "- numeral m + 1 = sub One m"
   468   "numeral m + - 1 = sub m One"
   469   "- 1 + numeral n = sub n One"
   470   "- 1 + - numeral n = - numeral (inc n)"
   471   "- numeral m + - 1 = - numeral (inc m)"
   472   "1 + - 1 = 0"
   473   "- 1 + 1 = 0"
   474   "- 1 + - 1 = - 2"
   475   by (simp_all add: sub_def numeral_add numeral.simps is_num_normalize right_minus numeral_inc
   476       del: add_uminus_conv_diff add: diff_conv_add_uminus)
   477 
   478 lemma diff_numeral_simps:
   479   "numeral m - numeral n = sub m n"
   480   "numeral m - - numeral n = numeral (m + n)"
   481   "- numeral m - numeral n = - numeral (m + n)"
   482   "- numeral m - - numeral n = sub n m"
   483   by (simp_all add: sub_def numeral_add numeral.simps is_num_normalize
   484       del: add_uminus_conv_diff add: diff_conv_add_uminus)
   485 
   486 lemma diff_numeral_special:
   487   "1 - numeral n = sub One n"
   488   "numeral m - 1 = sub m One"
   489   "1 - - numeral n = numeral (One + n)"
   490   "- numeral m - 1 = - numeral (m + One)"
   491   "- 1 - numeral n = - numeral (inc n)"
   492   "numeral m - - 1 = numeral (inc m)"
   493   "- 1 - - numeral n = sub n One"
   494   "- numeral m - - 1 = sub One m"
   495   "1 - 1 = 0"
   496   "- 1 - 1 = - 2"
   497   "1 - - 1 = 2"
   498   "- 1 - - 1 = 0"
   499   by (simp_all add: sub_def numeral_add numeral.simps is_num_normalize numeral_inc
   500       del: add_uminus_conv_diff add: diff_conv_add_uminus)
   501 
   502 end
   503 
   504 
   505 subsubsection \<open>Structures with multiplication: class \<open>semiring_numeral\<close>\<close>
   506 
   507 class semiring_numeral = semiring + monoid_mult
   508 begin
   509 
   510 subclass numeral ..
   511 
   512 lemma numeral_mult: "numeral (m * n) = numeral m * numeral n"
   513   by (induct n rule: num_induct)
   514     (simp_all add: numeral_One mult_inc numeral_inc numeral_add distrib_left)
   515 
   516 lemma numeral_times_numeral: "numeral m * numeral n = numeral (m * n)"
   517   by (rule numeral_mult [symmetric])
   518 
   519 lemma mult_2: "2 * z = z + z"
   520   by (simp add: one_add_one [symmetric] distrib_right)
   521 
   522 lemma mult_2_right: "z * 2 = z + z"
   523   by (simp add: one_add_one [symmetric] distrib_left)
   524 
   525 lemma left_add_twice:
   526   "a + (a + b) = 2 * a + b"
   527   by (simp add: mult_2 ac_simps)
   528 
   529 end
   530 
   531 
   532 subsubsection \<open>Structures with a zero: class \<open>semiring_1\<close>\<close>
   533 
   534 context semiring_1
   535 begin
   536 
   537 subclass semiring_numeral ..
   538 
   539 lemma of_nat_numeral [simp]: "of_nat (numeral n) = numeral n"
   540   by (induct n) (simp_all only: numeral.simps numeral_class.numeral.simps of_nat_add of_nat_1)
   541 
   542 lemma numeral_unfold_funpow:
   543   "numeral k = (op + 1 ^^ numeral k) 0"
   544   unfolding of_nat_def [symmetric] by simp
   545 
   546 end
   547 
   548 lemma transfer_rule_numeral:
   549   fixes R :: "'a::semiring_1 \<Rightarrow> 'b::semiring_1 \<Rightarrow> bool"
   550   assumes [transfer_rule]: "R 0 0" "R 1 1"
   551     "rel_fun R (rel_fun R R) plus plus"
   552   shows "rel_fun HOL.eq R numeral numeral"
   553   apply (subst (2) numeral_unfold_funpow [abs_def])
   554   apply (subst (1) numeral_unfold_funpow [abs_def])
   555   apply transfer_prover
   556   done
   557 
   558 lemma nat_of_num_numeral [code_abbrev]: "nat_of_num = numeral"
   559 proof
   560   fix n
   561   have "numeral n = nat_of_num n"
   562     by (induct n) (simp_all add: numeral.simps)
   563   then show "nat_of_num n = numeral n"
   564     by simp
   565 qed
   566 
   567 lemma nat_of_num_code [code]:
   568   "nat_of_num One = 1"
   569   "nat_of_num (Bit0 n) = (let m = nat_of_num n in m + m)"
   570   "nat_of_num (Bit1 n) = (let m = nat_of_num n in Suc (m + m))"
   571   by (simp_all add: Let_def)
   572 
   573 
   574 subsubsection \<open>Equality: class \<open>semiring_char_0\<close>\<close>
   575 
   576 context semiring_char_0
   577 begin
   578 
   579 lemma numeral_eq_iff: "numeral m = numeral n \<longleftrightarrow> m = n"
   580   by (simp only: of_nat_numeral [symmetric] nat_of_num_numeral [symmetric]
   581     of_nat_eq_iff num_eq_iff)
   582 
   583 lemma numeral_eq_one_iff: "numeral n = 1 \<longleftrightarrow> n = One"
   584   by (rule numeral_eq_iff [of n One, unfolded numeral_One])
   585 
   586 lemma one_eq_numeral_iff: "1 = numeral n \<longleftrightarrow> One = n"
   587   by (rule numeral_eq_iff [of One n, unfolded numeral_One])
   588 
   589 lemma numeral_neq_zero: "numeral n \<noteq> 0"
   590   by (simp add: of_nat_numeral [symmetric] nat_of_num_numeral [symmetric] nat_of_num_pos)
   591 
   592 lemma zero_neq_numeral: "0 \<noteq> numeral n"
   593   unfolding eq_commute [of 0] by (rule numeral_neq_zero)
   594 
   595 lemmas eq_numeral_simps [simp] =
   596   numeral_eq_iff
   597   numeral_eq_one_iff
   598   one_eq_numeral_iff
   599   numeral_neq_zero
   600   zero_neq_numeral
   601 
   602 end
   603 
   604 
   605 subsubsection \<open>Comparisons: class \<open>linordered_semidom\<close>\<close>
   606 
   607 text \<open>Could be perhaps more general than here.\<close>
   608 
   609 context linordered_semidom
   610 begin
   611 
   612 lemma numeral_le_iff: "numeral m \<le> numeral n \<longleftrightarrow> m \<le> n"
   613 proof -
   614   have "of_nat (numeral m) \<le> of_nat (numeral n) \<longleftrightarrow> m \<le> n"
   615     by (simp only: less_eq_num_def nat_of_num_numeral of_nat_le_iff)
   616   then show ?thesis by simp
   617 qed
   618 
   619 lemma one_le_numeral: "1 \<le> numeral n"
   620   using numeral_le_iff [of One n] by (simp add: numeral_One)
   621 
   622 lemma numeral_le_one_iff: "numeral n \<le> 1 \<longleftrightarrow> n \<le> One"
   623   using numeral_le_iff [of n One] by (simp add: numeral_One)
   624 
   625 lemma numeral_less_iff: "numeral m < numeral n \<longleftrightarrow> m < n"
   626 proof -
   627   have "of_nat (numeral m) < of_nat (numeral n) \<longleftrightarrow> m < n"
   628     unfolding less_num_def nat_of_num_numeral of_nat_less_iff ..
   629   then show ?thesis by simp
   630 qed
   631 
   632 lemma not_numeral_less_one: "\<not> numeral n < 1"
   633   using numeral_less_iff [of n One] by (simp add: numeral_One)
   634 
   635 lemma one_less_numeral_iff: "1 < numeral n \<longleftrightarrow> One < n"
   636   using numeral_less_iff [of One n] by (simp add: numeral_One)
   637 
   638 lemma zero_le_numeral: "0 \<le> numeral n"
   639   by (induct n) (simp_all add: numeral.simps)
   640 
   641 lemma zero_less_numeral: "0 < numeral n"
   642   by (induct n) (simp_all add: numeral.simps add_pos_pos)
   643 
   644 lemma not_numeral_le_zero: "\<not> numeral n \<le> 0"
   645   by (simp add: not_le zero_less_numeral)
   646 
   647 lemma not_numeral_less_zero: "\<not> numeral n < 0"
   648   by (simp add: not_less zero_le_numeral)
   649 
   650 lemmas le_numeral_extra =
   651   zero_le_one not_one_le_zero
   652   order_refl [of 0] order_refl [of 1]
   653 
   654 lemmas less_numeral_extra =
   655   zero_less_one not_one_less_zero
   656   less_irrefl [of 0] less_irrefl [of 1]
   657 
   658 lemmas le_numeral_simps [simp] =
   659   numeral_le_iff
   660   one_le_numeral
   661   numeral_le_one_iff
   662   zero_le_numeral
   663   not_numeral_le_zero
   664 
   665 lemmas less_numeral_simps [simp] =
   666   numeral_less_iff
   667   one_less_numeral_iff
   668   not_numeral_less_one
   669   zero_less_numeral
   670   not_numeral_less_zero
   671 
   672 lemma min_0_1 [simp]:
   673   fixes min' :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
   674   defines "min' \<equiv> min"
   675   shows
   676     "min' 0 1 = 0"
   677     "min' 1 0 = 0"
   678     "min' 0 (numeral x) = 0"
   679     "min' (numeral x) 0 = 0"
   680     "min' 1 (numeral x) = 1"
   681     "min' (numeral x) 1 = 1"
   682   by (simp_all add: min'_def min_def le_num_One_iff)
   683 
   684 lemma max_0_1 [simp]:
   685   fixes max' :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
   686   defines "max' \<equiv> max"
   687   shows
   688     "max' 0 1 = 1"
   689     "max' 1 0 = 1"
   690     "max' 0 (numeral x) = numeral x"
   691     "max' (numeral x) 0 = numeral x"
   692     "max' 1 (numeral x) = numeral x"
   693     "max' (numeral x) 1 = numeral x"
   694   by (simp_all add: max'_def max_def le_num_One_iff)
   695 
   696 end
   697 
   698 
   699 subsubsection \<open>Multiplication and negation: class \<open>ring_1\<close>\<close>
   700 
   701 context ring_1
   702 begin
   703 
   704 subclass neg_numeral ..
   705 
   706 lemma mult_neg_numeral_simps:
   707   "- numeral m * - numeral n = numeral (m * n)"
   708   "- numeral m * numeral n = - numeral (m * n)"
   709   "numeral m * - numeral n = - numeral (m * n)"
   710   by (simp_all only: mult_minus_left mult_minus_right minus_minus numeral_mult)
   711 
   712 lemma mult_minus1 [simp]: "- 1 * z = - z"
   713   by (simp add: numeral.simps)
   714 
   715 lemma mult_minus1_right [simp]: "z * - 1 = - z"
   716   by (simp add: numeral.simps)
   717 
   718 end
   719 
   720 
   721 subsubsection \<open>Equality using \<open>iszero\<close> for rings with non-zero characteristic\<close>
   722 
   723 context ring_1
   724 begin
   725 
   726 definition iszero :: "'a \<Rightarrow> bool"
   727   where "iszero z \<longleftrightarrow> z = 0"
   728 
   729 lemma iszero_0 [simp]: "iszero 0"
   730   by (simp add: iszero_def)
   731 
   732 lemma not_iszero_1 [simp]: "\<not> iszero 1"
   733   by (simp add: iszero_def)
   734 
   735 lemma not_iszero_Numeral1: "\<not> iszero Numeral1"
   736   by (simp add: numeral_One)
   737 
   738 lemma not_iszero_neg_1 [simp]: "\<not> iszero (- 1)"
   739   by (simp add: iszero_def)
   740 
   741 lemma not_iszero_neg_Numeral1: "\<not> iszero (- Numeral1)"
   742   by (simp add: numeral_One)
   743 
   744 lemma iszero_neg_numeral [simp]: "iszero (- numeral w) \<longleftrightarrow> iszero (numeral w)"
   745   unfolding iszero_def by (rule neg_equal_0_iff_equal)
   746 
   747 lemma eq_iff_iszero_diff: "x = y \<longleftrightarrow> iszero (x - y)"
   748   unfolding iszero_def by (rule eq_iff_diff_eq_0)
   749 
   750 text \<open>
   751   The \<open>eq_numeral_iff_iszero\<close> lemmas are not declared \<open>[simp]\<close> by default,
   752   because for rings of characteristic zero, better simp rules are possible.
   753   For a type like integers mod \<open>n\<close>, type-instantiated versions of these rules
   754   should be added to the simplifier, along with a type-specific rule for
   755   deciding propositions of the form \<open>iszero (numeral w)\<close>.
   756 
   757   bh: Maybe it would not be so bad to just declare these as simp rules anyway?
   758   I should test whether these rules take precedence over the \<open>ring_char_0\<close>
   759   rules in the simplifier.
   760 \<close>
   761 
   762 lemma eq_numeral_iff_iszero:
   763   "numeral x = numeral y \<longleftrightarrow> iszero (sub x y)"
   764   "numeral x = - numeral y \<longleftrightarrow> iszero (numeral (x + y))"
   765   "- numeral x = numeral y \<longleftrightarrow> iszero (numeral (x + y))"
   766   "- numeral x = - numeral y \<longleftrightarrow> iszero (sub y x)"
   767   "numeral x = 1 \<longleftrightarrow> iszero (sub x One)"
   768   "1 = numeral y \<longleftrightarrow> iszero (sub One y)"
   769   "- numeral x = 1 \<longleftrightarrow> iszero (numeral (x + One))"
   770   "1 = - numeral y \<longleftrightarrow> iszero (numeral (One + y))"
   771   "numeral x = 0 \<longleftrightarrow> iszero (numeral x)"
   772   "0 = numeral y \<longleftrightarrow> iszero (numeral y)"
   773   "- numeral x = 0 \<longleftrightarrow> iszero (numeral x)"
   774   "0 = - numeral y \<longleftrightarrow> iszero (numeral y)"
   775   unfolding eq_iff_iszero_diff diff_numeral_simps diff_numeral_special
   776   by simp_all
   777 
   778 end
   779 
   780 
   781 subsubsection \<open>Equality and negation: class \<open>ring_char_0\<close>\<close>
   782 
   783 context ring_char_0
   784 begin
   785 
   786 lemma not_iszero_numeral [simp]: "\<not> iszero (numeral w)"
   787   by (simp add: iszero_def)
   788 
   789 lemma neg_numeral_eq_iff: "- numeral m = - numeral n \<longleftrightarrow> m = n"
   790   by simp
   791 
   792 lemma numeral_neq_neg_numeral: "numeral m \<noteq> - numeral n"
   793   by (simp add: eq_neg_iff_add_eq_0 numeral_plus_numeral)
   794 
   795 lemma neg_numeral_neq_numeral: "- numeral m \<noteq> numeral n"
   796   by (rule numeral_neq_neg_numeral [symmetric])
   797 
   798 lemma zero_neq_neg_numeral: "0 \<noteq> - numeral n"
   799   by simp
   800 
   801 lemma neg_numeral_neq_zero: "- numeral n \<noteq> 0"
   802   by simp
   803 
   804 lemma one_neq_neg_numeral: "1 \<noteq> - numeral n"
   805   using numeral_neq_neg_numeral [of One n] by (simp add: numeral_One)
   806 
   807 lemma neg_numeral_neq_one: "- numeral n \<noteq> 1"
   808   using neg_numeral_neq_numeral [of n One] by (simp add: numeral_One)
   809 
   810 lemma neg_one_neq_numeral: "- 1 \<noteq> numeral n"
   811   using neg_numeral_neq_numeral [of One n] by (simp add: numeral_One)
   812 
   813 lemma numeral_neq_neg_one: "numeral n \<noteq> - 1"
   814   using numeral_neq_neg_numeral [of n One] by (simp add: numeral_One)
   815 
   816 lemma neg_one_eq_numeral_iff: "- 1 = - numeral n \<longleftrightarrow> n = One"
   817   using neg_numeral_eq_iff [of One n] by (auto simp add: numeral_One)
   818 
   819 lemma numeral_eq_neg_one_iff: "- numeral n = - 1 \<longleftrightarrow> n = One"
   820   using neg_numeral_eq_iff [of n One] by (auto simp add: numeral_One)
   821 
   822 lemma neg_one_neq_zero: "- 1 \<noteq> 0"
   823   by simp
   824 
   825 lemma zero_neq_neg_one: "0 \<noteq> - 1"
   826   by simp
   827 
   828 lemma neg_one_neq_one: "- 1 \<noteq> 1"
   829   using neg_numeral_neq_numeral [of One One] by (simp only: numeral_One not_False_eq_True)
   830 
   831 lemma one_neq_neg_one: "1 \<noteq> - 1"
   832   using numeral_neq_neg_numeral [of One One] by (simp only: numeral_One not_False_eq_True)
   833 
   834 lemmas eq_neg_numeral_simps [simp] =
   835   neg_numeral_eq_iff
   836   numeral_neq_neg_numeral neg_numeral_neq_numeral
   837   one_neq_neg_numeral neg_numeral_neq_one
   838   zero_neq_neg_numeral neg_numeral_neq_zero
   839   neg_one_neq_numeral numeral_neq_neg_one
   840   neg_one_eq_numeral_iff numeral_eq_neg_one_iff
   841   neg_one_neq_zero zero_neq_neg_one
   842   neg_one_neq_one one_neq_neg_one
   843 
   844 end
   845 
   846 
   847 subsubsection \<open>Structures with negation and order: class \<open>linordered_idom\<close>\<close>
   848 
   849 context linordered_idom
   850 begin
   851 
   852 subclass ring_char_0 ..
   853 
   854 lemma neg_numeral_le_iff: "- numeral m \<le> - numeral n \<longleftrightarrow> n \<le> m"
   855   by (simp only: neg_le_iff_le numeral_le_iff)
   856 
   857 lemma neg_numeral_less_iff: "- numeral m < - numeral n \<longleftrightarrow> n < m"
   858   by (simp only: neg_less_iff_less numeral_less_iff)
   859 
   860 lemma neg_numeral_less_zero: "- numeral n < 0"
   861   by (simp only: neg_less_0_iff_less zero_less_numeral)
   862 
   863 lemma neg_numeral_le_zero: "- numeral n \<le> 0"
   864   by (simp only: neg_le_0_iff_le zero_le_numeral)
   865 
   866 lemma not_zero_less_neg_numeral: "\<not> 0 < - numeral n"
   867   by (simp only: not_less neg_numeral_le_zero)
   868 
   869 lemma not_zero_le_neg_numeral: "\<not> 0 \<le> - numeral n"
   870   by (simp only: not_le neg_numeral_less_zero)
   871 
   872 lemma neg_numeral_less_numeral: "- numeral m < numeral n"
   873   using neg_numeral_less_zero zero_less_numeral by (rule less_trans)
   874 
   875 lemma neg_numeral_le_numeral: "- numeral m \<le> numeral n"
   876   by (simp only: less_imp_le neg_numeral_less_numeral)
   877 
   878 lemma not_numeral_less_neg_numeral: "\<not> numeral m < - numeral n"
   879   by (simp only: not_less neg_numeral_le_numeral)
   880 
   881 lemma not_numeral_le_neg_numeral: "\<not> numeral m \<le> - numeral n"
   882   by (simp only: not_le neg_numeral_less_numeral)
   883 
   884 lemma neg_numeral_less_one: "- numeral m < 1"
   885   by (rule neg_numeral_less_numeral [of m One, unfolded numeral_One])
   886 
   887 lemma neg_numeral_le_one: "- numeral m \<le> 1"
   888   by (rule neg_numeral_le_numeral [of m One, unfolded numeral_One])
   889 
   890 lemma not_one_less_neg_numeral: "\<not> 1 < - numeral m"
   891   by (simp only: not_less neg_numeral_le_one)
   892 
   893 lemma not_one_le_neg_numeral: "\<not> 1 \<le> - numeral m"
   894   by (simp only: not_le neg_numeral_less_one)
   895 
   896 lemma not_numeral_less_neg_one: "\<not> numeral m < - 1"
   897   using not_numeral_less_neg_numeral [of m One] by (simp add: numeral_One)
   898 
   899 lemma not_numeral_le_neg_one: "\<not> numeral m \<le> - 1"
   900   using not_numeral_le_neg_numeral [of m One] by (simp add: numeral_One)
   901 
   902 lemma neg_one_less_numeral: "- 1 < numeral m"
   903   using neg_numeral_less_numeral [of One m] by (simp add: numeral_One)
   904 
   905 lemma neg_one_le_numeral: "- 1 \<le> numeral m"
   906   using neg_numeral_le_numeral [of One m] by (simp add: numeral_One)
   907 
   908 lemma neg_numeral_less_neg_one_iff: "- numeral m < - 1 \<longleftrightarrow> m \<noteq> One"
   909   by (cases m) simp_all
   910 
   911 lemma neg_numeral_le_neg_one: "- numeral m \<le> - 1"
   912   by simp
   913 
   914 lemma not_neg_one_less_neg_numeral: "\<not> - 1 < - numeral m"
   915   by simp
   916 
   917 lemma not_neg_one_le_neg_numeral_iff: "\<not> - 1 \<le> - numeral m \<longleftrightarrow> m \<noteq> One"
   918   by (cases m) simp_all
   919 
   920 lemma sub_non_negative: "sub n m \<ge> 0 \<longleftrightarrow> n \<ge> m"
   921   by (simp only: sub_def le_diff_eq) simp
   922 
   923 lemma sub_positive: "sub n m > 0 \<longleftrightarrow> n > m"
   924   by (simp only: sub_def less_diff_eq) simp
   925 
   926 lemma sub_non_positive: "sub n m \<le> 0 \<longleftrightarrow> n \<le> m"
   927   by (simp only: sub_def diff_le_eq) simp
   928 
   929 lemma sub_negative: "sub n m < 0 \<longleftrightarrow> n < m"
   930   by (simp only: sub_def diff_less_eq) simp
   931 
   932 lemmas le_neg_numeral_simps [simp] =
   933   neg_numeral_le_iff
   934   neg_numeral_le_numeral not_numeral_le_neg_numeral
   935   neg_numeral_le_zero not_zero_le_neg_numeral
   936   neg_numeral_le_one not_one_le_neg_numeral
   937   neg_one_le_numeral not_numeral_le_neg_one
   938   neg_numeral_le_neg_one not_neg_one_le_neg_numeral_iff
   939 
   940 lemma le_minus_one_simps [simp]:
   941   "- 1 \<le> 0"
   942   "- 1 \<le> 1"
   943   "\<not> 0 \<le> - 1"
   944   "\<not> 1 \<le> - 1"
   945   by simp_all
   946 
   947 lemmas less_neg_numeral_simps [simp] =
   948   neg_numeral_less_iff
   949   neg_numeral_less_numeral not_numeral_less_neg_numeral
   950   neg_numeral_less_zero not_zero_less_neg_numeral
   951   neg_numeral_less_one not_one_less_neg_numeral
   952   neg_one_less_numeral not_numeral_less_neg_one
   953   neg_numeral_less_neg_one_iff not_neg_one_less_neg_numeral
   954 
   955 lemma less_minus_one_simps [simp]:
   956   "- 1 < 0"
   957   "- 1 < 1"
   958   "\<not> 0 < - 1"
   959   "\<not> 1 < - 1"
   960   by (simp_all add: less_le)
   961 
   962 lemma abs_numeral [simp]: "\<bar>numeral n\<bar> = numeral n"
   963   by simp
   964 
   965 lemma abs_neg_numeral [simp]: "\<bar>- numeral n\<bar> = numeral n"
   966   by (simp only: abs_minus_cancel abs_numeral)
   967 
   968 lemma abs_neg_one [simp]: "\<bar>- 1\<bar> = 1"
   969   by simp
   970 
   971 end
   972 
   973 
   974 subsubsection \<open>Natural numbers\<close>
   975 
   976 lemma Suc_1 [simp]: "Suc 1 = 2"
   977   unfolding Suc_eq_plus1 by (rule one_add_one)
   978 
   979 lemma Suc_numeral [simp]: "Suc (numeral n) = numeral (n + One)"
   980   unfolding Suc_eq_plus1 by (rule numeral_plus_one)
   981 
   982 definition pred_numeral :: "num \<Rightarrow> nat"
   983   where [code del]: "pred_numeral k = numeral k - 1"
   984 
   985 lemma numeral_eq_Suc: "numeral k = Suc (pred_numeral k)"
   986   by (simp add: pred_numeral_def)
   987 
   988 lemma eval_nat_numeral:
   989   "numeral One = Suc 0"
   990   "numeral (Bit0 n) = Suc (numeral (BitM n))"
   991   "numeral (Bit1 n) = Suc (numeral (Bit0 n))"
   992   by (simp_all add: numeral.simps BitM_plus_one)
   993 
   994 lemma pred_numeral_simps [simp]:
   995   "pred_numeral One = 0"
   996   "pred_numeral (Bit0 k) = numeral (BitM k)"
   997   "pred_numeral (Bit1 k) = numeral (Bit0 k)"
   998   by (simp_all only: pred_numeral_def eval_nat_numeral diff_Suc_Suc diff_0)
   999 
  1000 lemma numeral_2_eq_2: "2 = Suc (Suc 0)"
  1001   by (simp add: eval_nat_numeral)
  1002 
  1003 lemma numeral_3_eq_3: "3 = Suc (Suc (Suc 0))"
  1004   by (simp add: eval_nat_numeral)
  1005 
  1006 lemma numeral_1_eq_Suc_0: "Numeral1 = Suc 0"
  1007   by (simp only: numeral_One One_nat_def)
  1008 
  1009 lemma Suc_nat_number_of_add: "Suc (numeral v + n) = numeral (v + One) + n"
  1010   by simp
  1011 
  1012 lemma numerals: "Numeral1 = (1::nat)" "2 = Suc (Suc 0)"
  1013   by (rule numeral_One) (rule numeral_2_eq_2)
  1014 
  1015 lemmas numeral_nat = eval_nat_numeral BitM.simps One_nat_def
  1016 
  1017 text \<open>Comparisons involving @{term Suc}.\<close>
  1018 
  1019 lemma eq_numeral_Suc [simp]: "numeral k = Suc n \<longleftrightarrow> pred_numeral k = n"
  1020   by (simp add: numeral_eq_Suc)
  1021 
  1022 lemma Suc_eq_numeral [simp]: "Suc n = numeral k \<longleftrightarrow> n = pred_numeral k"
  1023   by (simp add: numeral_eq_Suc)
  1024 
  1025 lemma less_numeral_Suc [simp]: "numeral k < Suc n \<longleftrightarrow> pred_numeral k < n"
  1026   by (simp add: numeral_eq_Suc)
  1027 
  1028 lemma less_Suc_numeral [simp]: "Suc n < numeral k \<longleftrightarrow> n < pred_numeral k"
  1029   by (simp add: numeral_eq_Suc)
  1030 
  1031 lemma le_numeral_Suc [simp]: "numeral k \<le> Suc n \<longleftrightarrow> pred_numeral k \<le> n"
  1032   by (simp add: numeral_eq_Suc)
  1033 
  1034 lemma le_Suc_numeral [simp]: "Suc n \<le> numeral k \<longleftrightarrow> n \<le> pred_numeral k"
  1035   by (simp add: numeral_eq_Suc)
  1036 
  1037 lemma diff_Suc_numeral [simp]: "Suc n - numeral k = n - pred_numeral k"
  1038   by (simp add: numeral_eq_Suc)
  1039 
  1040 lemma diff_numeral_Suc [simp]: "numeral k - Suc n = pred_numeral k - n"
  1041   by (simp add: numeral_eq_Suc)
  1042 
  1043 lemma max_Suc_numeral [simp]: "max (Suc n) (numeral k) = Suc (max n (pred_numeral k))"
  1044   by (simp add: numeral_eq_Suc)
  1045 
  1046 lemma max_numeral_Suc [simp]: "max (numeral k) (Suc n) = Suc (max (pred_numeral k) n)"
  1047   by (simp add: numeral_eq_Suc)
  1048 
  1049 lemma min_Suc_numeral [simp]: "min (Suc n) (numeral k) = Suc (min n (pred_numeral k))"
  1050   by (simp add: numeral_eq_Suc)
  1051 
  1052 lemma min_numeral_Suc [simp]: "min (numeral k) (Suc n) = Suc (min (pred_numeral k) n)"
  1053   by (simp add: numeral_eq_Suc)
  1054 
  1055 text \<open>For @{term case_nat} and @{term rec_nat}.\<close>
  1056 
  1057 lemma case_nat_numeral [simp]: "case_nat a f (numeral v) = (let pv = pred_numeral v in f pv)"
  1058   by (simp add: numeral_eq_Suc)
  1059 
  1060 lemma case_nat_add_eq_if [simp]:
  1061   "case_nat a f ((numeral v) + n) = (let pv = pred_numeral v in f (pv + n))"
  1062   by (simp add: numeral_eq_Suc)
  1063 
  1064 lemma rec_nat_numeral [simp]:
  1065   "rec_nat a f (numeral v) = (let pv = pred_numeral v in f pv (rec_nat a f pv))"
  1066   by (simp add: numeral_eq_Suc Let_def)
  1067 
  1068 lemma rec_nat_add_eq_if [simp]:
  1069   "rec_nat a f (numeral v + n) = (let pv = pred_numeral v in f (pv + n) (rec_nat a f (pv + n)))"
  1070   by (simp add: numeral_eq_Suc Let_def)
  1071 
  1072 text \<open>Case analysis on @{term "n < 2"}.\<close>
  1073 lemma less_2_cases: "n < 2 \<Longrightarrow> n = 0 \<or> n = Suc 0"
  1074   by (auto simp add: numeral_2_eq_2)
  1075 
  1076 text \<open>Removal of Small Numerals: 0, 1 and (in additive positions) 2.\<close>
  1077 text \<open>bh: Are these rules really a good idea?\<close>
  1078 
  1079 lemma add_2_eq_Suc [simp]: "2 + n = Suc (Suc n)"
  1080   by simp
  1081 
  1082 lemma add_2_eq_Suc' [simp]: "n + 2 = Suc (Suc n)"
  1083   by simp
  1084 
  1085 text \<open>Can be used to eliminate long strings of Sucs, but not by default.\<close>
  1086 lemma Suc3_eq_add_3: "Suc (Suc (Suc n)) = 3 + n"
  1087   by simp
  1088 
  1089 lemmas nat_1_add_1 = one_add_one [where 'a=nat] (* legacy *)
  1090 
  1091 
  1092 subsection \<open>Particular lemmas concerning @{term 2}\<close>
  1093 
  1094 context linordered_field
  1095 begin
  1096 
  1097 subclass field_char_0 ..
  1098 
  1099 lemma half_gt_zero_iff: "0 < a / 2 \<longleftrightarrow> 0 < a"
  1100   by (auto simp add: field_simps)
  1101 
  1102 lemma half_gt_zero [simp]: "0 < a \<Longrightarrow> 0 < a / 2"
  1103   by (simp add: half_gt_zero_iff)
  1104 
  1105 end
  1106 
  1107 
  1108 subsection \<open>Numeral equations as default simplification rules\<close>
  1109 
  1110 declare (in numeral) numeral_One [simp]
  1111 declare (in numeral) numeral_plus_numeral [simp]
  1112 declare (in numeral) add_numeral_special [simp]
  1113 declare (in neg_numeral) add_neg_numeral_simps [simp]
  1114 declare (in neg_numeral) add_neg_numeral_special [simp]
  1115 declare (in neg_numeral) diff_numeral_simps [simp]
  1116 declare (in neg_numeral) diff_numeral_special [simp]
  1117 declare (in semiring_numeral) numeral_times_numeral [simp]
  1118 declare (in ring_1) mult_neg_numeral_simps [simp]
  1119 
  1120 subsection \<open>Setting up simprocs\<close>
  1121 
  1122 lemma mult_numeral_1: "Numeral1 * a = a"
  1123   for a :: "'a::semiring_numeral"
  1124   by simp
  1125 
  1126 lemma mult_numeral_1_right: "a * Numeral1 = a"
  1127   for a :: "'a::semiring_numeral"
  1128   by simp
  1129 
  1130 lemma divide_numeral_1: "a / Numeral1 = a"
  1131   for a :: "'a::field"
  1132   by simp
  1133 
  1134 lemma inverse_numeral_1: "inverse Numeral1 = (Numeral1::'a::division_ring)"
  1135   by simp
  1136 
  1137 text \<open>
  1138   Theorem lists for the cancellation simprocs. The use of a binary
  1139   numeral for 1 reduces the number of special cases.
  1140 \<close>
  1141 
  1142 lemma mult_1s:
  1143   "Numeral1 * a = a"
  1144   "a * Numeral1 = a"
  1145   "- Numeral1 * b = - b"
  1146   "b * - Numeral1 = - b"
  1147   for a :: "'a::semiring_numeral" and b :: "'b::ring_1"
  1148   by simp_all
  1149 
  1150 setup \<open>
  1151   Reorient_Proc.add
  1152     (fn Const (@{const_name numeral}, _) $ _ => true
  1153       | Const (@{const_name uminus}, _) $ (Const (@{const_name numeral}, _) $ _) => true
  1154       | _ => false)
  1155 \<close>
  1156 
  1157 simproc_setup reorient_numeral ("numeral w = x" | "- numeral w = y") =
  1158   Reorient_Proc.proc
  1159 
  1160 
  1161 subsubsection \<open>Simplification of arithmetic operations on integer constants\<close>
  1162 
  1163 lemmas arith_special = (* already declared simp above *)
  1164   add_numeral_special add_neg_numeral_special
  1165   diff_numeral_special
  1166 
  1167 lemmas arith_extra_simps = (* rules already in simpset *)
  1168   numeral_plus_numeral add_neg_numeral_simps add_0_left add_0_right
  1169   minus_zero
  1170   diff_numeral_simps diff_0 diff_0_right
  1171   numeral_times_numeral mult_neg_numeral_simps
  1172   mult_zero_left mult_zero_right
  1173   abs_numeral abs_neg_numeral
  1174 
  1175 text \<open>
  1176   For making a minimal simpset, one must include these default simprules.
  1177   Also include \<open>simp_thms\<close>.
  1178 \<close>
  1179 
  1180 lemmas arith_simps =
  1181   add_num_simps mult_num_simps sub_num_simps
  1182   BitM.simps dbl_simps dbl_inc_simps dbl_dec_simps
  1183   abs_zero abs_one arith_extra_simps
  1184 
  1185 lemmas more_arith_simps =
  1186   neg_le_iff_le
  1187   minus_zero left_minus right_minus
  1188   mult_1_left mult_1_right
  1189   mult_minus_left mult_minus_right
  1190   minus_add_distrib minus_minus mult.assoc
  1191 
  1192 lemmas of_nat_simps =
  1193   of_nat_0 of_nat_1 of_nat_Suc of_nat_add of_nat_mult
  1194 
  1195 text \<open>Simplification of relational operations.\<close>
  1196 
  1197 lemmas eq_numeral_extra =
  1198   zero_neq_one one_neq_zero
  1199 
  1200 lemmas rel_simps =
  1201   le_num_simps less_num_simps eq_num_simps
  1202   le_numeral_simps le_neg_numeral_simps le_minus_one_simps le_numeral_extra
  1203   less_numeral_simps less_neg_numeral_simps less_minus_one_simps less_numeral_extra
  1204   eq_numeral_simps eq_neg_numeral_simps eq_numeral_extra
  1205 
  1206 lemma Let_numeral [simp]: "Let (numeral v) f = f (numeral v)"
  1207   \<comment> \<open>Unfold all \<open>let\<close>s involving constants\<close>
  1208   unfolding Let_def ..
  1209 
  1210 lemma Let_neg_numeral [simp]: "Let (- numeral v) f = f (- numeral v)"
  1211   \<comment> \<open>Unfold all \<open>let\<close>s involving constants\<close>
  1212   unfolding Let_def ..
  1213 
  1214 declaration \<open>
  1215 let
  1216   fun number_of ctxt T n =
  1217     if not (Sign.of_sort (Proof_Context.theory_of ctxt) (T, @{sort numeral}))
  1218     then raise CTERM ("number_of", [])
  1219     else Numeral.mk_cnumber (Thm.ctyp_of ctxt T) n;
  1220 in
  1221   K (
  1222     Lin_Arith.add_simps
  1223       @{thms arith_simps more_arith_simps rel_simps pred_numeral_simps
  1224         arith_special numeral_One of_nat_simps uminus_numeral_One}
  1225     #> Lin_Arith.add_simps
  1226       @{thms Suc_numeral Let_numeral Let_neg_numeral Let_0 Let_1
  1227         le_Suc_numeral le_numeral_Suc less_Suc_numeral less_numeral_Suc
  1228         Suc_eq_numeral eq_numeral_Suc mult_Suc mult_Suc_right of_nat_numeral}
  1229     #> Lin_Arith.set_number_of number_of)
  1230 end
  1231 \<close>
  1232 
  1233 
  1234 subsubsection \<open>Simplification of arithmetic when nested to the right\<close>
  1235 
  1236 lemma add_numeral_left [simp]: "numeral v + (numeral w + z) = (numeral(v + w) + z)"
  1237   by (simp_all add: add.assoc [symmetric])
  1238 
  1239 lemma add_neg_numeral_left [simp]:
  1240   "numeral v + (- numeral w + y) = (sub v w + y)"
  1241   "- numeral v + (numeral w + y) = (sub w v + y)"
  1242   "- numeral v + (- numeral w + y) = (- numeral(v + w) + y)"
  1243   by (simp_all add: add.assoc [symmetric])
  1244 
  1245 lemma mult_numeral_left [simp]:
  1246   "numeral v * (numeral w * z) = (numeral(v * w) * z :: 'a::semiring_numeral)"
  1247   "- numeral v * (numeral w * y) = (- numeral(v * w) * y :: 'b::ring_1)"
  1248   "numeral v * (- numeral w * y) = (- numeral(v * w) * y :: 'b::ring_1)"
  1249   "- numeral v * (- numeral w * y) = (numeral(v * w) * y :: 'b::ring_1)"
  1250   by (simp_all add: mult.assoc [symmetric])
  1251 
  1252 hide_const (open) One Bit0 Bit1 BitM inc pow sqr sub dbl dbl_inc dbl_dec
  1253 
  1254 
  1255 subsection \<open>Code module namespace\<close>
  1256 
  1257 code_identifier
  1258   code_module Num \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
  1259 
  1260 subsection \<open>Printing of evaluated natural numbers as numerals\<close>
  1261 
  1262 lemma [code_post]:
  1263   "Suc 0 = 1"
  1264   "Suc 1 = 2"
  1265   "Suc (numeral n) = numeral (Num.inc n)"
  1266   by (simp_all add: numeral_inc)
  1267 
  1268 lemmas [code_post] = Num.inc.simps
  1269 
  1270 end