src/HOL/Num.thy
author haftmann
Sun Oct 08 22:28:22 2017 +0200 (22 months ago)
changeset 66816 212a3334e7da
parent 66283 adf3155c57e2
child 66936 cf8d8fc23891
permissions -rw-r--r--
more fundamental definition of div and mod on int
     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 end
   526 
   527 
   528 subsubsection \<open>Structures with a zero: class \<open>semiring_1\<close>\<close>
   529 
   530 context semiring_1
   531 begin
   532 
   533 subclass semiring_numeral ..
   534 
   535 lemma of_nat_numeral [simp]: "of_nat (numeral n) = numeral n"
   536   by (induct n) (simp_all only: numeral.simps numeral_class.numeral.simps of_nat_add of_nat_1)
   537 
   538 lemma numeral_unfold_funpow:
   539   "numeral k = (op + 1 ^^ numeral k) 0"
   540   unfolding of_nat_def [symmetric] by simp
   541 
   542 end
   543 
   544 lemma transfer_rule_numeral:
   545   fixes R :: "'a::semiring_1 \<Rightarrow> 'b::semiring_1 \<Rightarrow> bool"
   546   assumes [transfer_rule]: "R 0 0" "R 1 1"
   547     "rel_fun R (rel_fun R R) plus plus"
   548   shows "rel_fun HOL.eq R numeral numeral"
   549   apply (subst (2) numeral_unfold_funpow [abs_def])
   550   apply (subst (1) numeral_unfold_funpow [abs_def])
   551   apply transfer_prover
   552   done
   553 
   554 lemma nat_of_num_numeral [code_abbrev]: "nat_of_num = numeral"
   555 proof
   556   fix n
   557   have "numeral n = nat_of_num n"
   558     by (induct n) (simp_all add: numeral.simps)
   559   then show "nat_of_num n = numeral n"
   560     by simp
   561 qed
   562 
   563 lemma nat_of_num_code [code]:
   564   "nat_of_num One = 1"
   565   "nat_of_num (Bit0 n) = (let m = nat_of_num n in m + m)"
   566   "nat_of_num (Bit1 n) = (let m = nat_of_num n in Suc (m + m))"
   567   by (simp_all add: Let_def)
   568 
   569 
   570 subsubsection \<open>Equality: class \<open>semiring_char_0\<close>\<close>
   571 
   572 context semiring_char_0
   573 begin
   574 
   575 lemma numeral_eq_iff: "numeral m = numeral n \<longleftrightarrow> m = n"
   576   by (simp only: of_nat_numeral [symmetric] nat_of_num_numeral [symmetric]
   577     of_nat_eq_iff num_eq_iff)
   578 
   579 lemma numeral_eq_one_iff: "numeral n = 1 \<longleftrightarrow> n = One"
   580   by (rule numeral_eq_iff [of n One, unfolded numeral_One])
   581 
   582 lemma one_eq_numeral_iff: "1 = numeral n \<longleftrightarrow> One = n"
   583   by (rule numeral_eq_iff [of One n, unfolded numeral_One])
   584 
   585 lemma numeral_neq_zero: "numeral n \<noteq> 0"
   586   by (simp add: of_nat_numeral [symmetric] nat_of_num_numeral [symmetric] nat_of_num_pos)
   587 
   588 lemma zero_neq_numeral: "0 \<noteq> numeral n"
   589   unfolding eq_commute [of 0] by (rule numeral_neq_zero)
   590 
   591 lemmas eq_numeral_simps [simp] =
   592   numeral_eq_iff
   593   numeral_eq_one_iff
   594   one_eq_numeral_iff
   595   numeral_neq_zero
   596   zero_neq_numeral
   597 
   598 end
   599 
   600 
   601 subsubsection \<open>Comparisons: class \<open>linordered_semidom\<close>\<close>
   602 
   603 text \<open>Could be perhaps more general than here.\<close>
   604 
   605 context linordered_semidom
   606 begin
   607 
   608 lemma numeral_le_iff: "numeral m \<le> numeral n \<longleftrightarrow> m \<le> n"
   609 proof -
   610   have "of_nat (numeral m) \<le> of_nat (numeral n) \<longleftrightarrow> m \<le> n"
   611     by (simp only: less_eq_num_def nat_of_num_numeral of_nat_le_iff)
   612   then show ?thesis by simp
   613 qed
   614 
   615 lemma one_le_numeral: "1 \<le> numeral n"
   616   using numeral_le_iff [of One n] by (simp add: numeral_One)
   617 
   618 lemma numeral_le_one_iff: "numeral n \<le> 1 \<longleftrightarrow> n \<le> One"
   619   using numeral_le_iff [of n One] by (simp add: numeral_One)
   620 
   621 lemma numeral_less_iff: "numeral m < numeral n \<longleftrightarrow> m < n"
   622 proof -
   623   have "of_nat (numeral m) < of_nat (numeral n) \<longleftrightarrow> m < n"
   624     unfolding less_num_def nat_of_num_numeral of_nat_less_iff ..
   625   then show ?thesis by simp
   626 qed
   627 
   628 lemma not_numeral_less_one: "\<not> numeral n < 1"
   629   using numeral_less_iff [of n One] by (simp add: numeral_One)
   630 
   631 lemma one_less_numeral_iff: "1 < numeral n \<longleftrightarrow> One < n"
   632   using numeral_less_iff [of One n] by (simp add: numeral_One)
   633 
   634 lemma zero_le_numeral: "0 \<le> numeral n"
   635   by (induct n) (simp_all add: numeral.simps)
   636 
   637 lemma zero_less_numeral: "0 < numeral n"
   638   by (induct n) (simp_all add: numeral.simps add_pos_pos)
   639 
   640 lemma not_numeral_le_zero: "\<not> numeral n \<le> 0"
   641   by (simp add: not_le zero_less_numeral)
   642 
   643 lemma not_numeral_less_zero: "\<not> numeral n < 0"
   644   by (simp add: not_less zero_le_numeral)
   645 
   646 lemmas le_numeral_extra =
   647   zero_le_one not_one_le_zero
   648   order_refl [of 0] order_refl [of 1]
   649 
   650 lemmas less_numeral_extra =
   651   zero_less_one not_one_less_zero
   652   less_irrefl [of 0] less_irrefl [of 1]
   653 
   654 lemmas le_numeral_simps [simp] =
   655   numeral_le_iff
   656   one_le_numeral
   657   numeral_le_one_iff
   658   zero_le_numeral
   659   not_numeral_le_zero
   660 
   661 lemmas less_numeral_simps [simp] =
   662   numeral_less_iff
   663   one_less_numeral_iff
   664   not_numeral_less_one
   665   zero_less_numeral
   666   not_numeral_less_zero
   667 
   668 lemma min_0_1 [simp]:
   669   fixes min' :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
   670   defines "min' \<equiv> min"
   671   shows
   672     "min' 0 1 = 0"
   673     "min' 1 0 = 0"
   674     "min' 0 (numeral x) = 0"
   675     "min' (numeral x) 0 = 0"
   676     "min' 1 (numeral x) = 1"
   677     "min' (numeral x) 1 = 1"
   678   by (simp_all add: min'_def min_def le_num_One_iff)
   679 
   680 lemma max_0_1 [simp]:
   681   fixes max' :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
   682   defines "max' \<equiv> max"
   683   shows
   684     "max' 0 1 = 1"
   685     "max' 1 0 = 1"
   686     "max' 0 (numeral x) = numeral x"
   687     "max' (numeral x) 0 = numeral x"
   688     "max' 1 (numeral x) = numeral x"
   689     "max' (numeral x) 1 = numeral x"
   690   by (simp_all add: max'_def max_def le_num_One_iff)
   691 
   692 end
   693 
   694 
   695 subsubsection \<open>Multiplication and negation: class \<open>ring_1\<close>\<close>
   696 
   697 context ring_1
   698 begin
   699 
   700 subclass neg_numeral ..
   701 
   702 lemma mult_neg_numeral_simps:
   703   "- numeral m * - numeral n = numeral (m * n)"
   704   "- numeral m * numeral n = - numeral (m * n)"
   705   "numeral m * - numeral n = - numeral (m * n)"
   706   by (simp_all only: mult_minus_left mult_minus_right minus_minus numeral_mult)
   707 
   708 lemma mult_minus1 [simp]: "- 1 * z = - z"
   709   by (simp add: numeral.simps)
   710 
   711 lemma mult_minus1_right [simp]: "z * - 1 = - z"
   712   by (simp add: numeral.simps)
   713 
   714 end
   715 
   716 
   717 subsubsection \<open>Equality using \<open>iszero\<close> for rings with non-zero characteristic\<close>
   718 
   719 context ring_1
   720 begin
   721 
   722 definition iszero :: "'a \<Rightarrow> bool"
   723   where "iszero z \<longleftrightarrow> z = 0"
   724 
   725 lemma iszero_0 [simp]: "iszero 0"
   726   by (simp add: iszero_def)
   727 
   728 lemma not_iszero_1 [simp]: "\<not> iszero 1"
   729   by (simp add: iszero_def)
   730 
   731 lemma not_iszero_Numeral1: "\<not> iszero Numeral1"
   732   by (simp add: numeral_One)
   733 
   734 lemma not_iszero_neg_1 [simp]: "\<not> iszero (- 1)"
   735   by (simp add: iszero_def)
   736 
   737 lemma not_iszero_neg_Numeral1: "\<not> iszero (- Numeral1)"
   738   by (simp add: numeral_One)
   739 
   740 lemma iszero_neg_numeral [simp]: "iszero (- numeral w) \<longleftrightarrow> iszero (numeral w)"
   741   unfolding iszero_def by (rule neg_equal_0_iff_equal)
   742 
   743 lemma eq_iff_iszero_diff: "x = y \<longleftrightarrow> iszero (x - y)"
   744   unfolding iszero_def by (rule eq_iff_diff_eq_0)
   745 
   746 text \<open>
   747   The \<open>eq_numeral_iff_iszero\<close> lemmas are not declared \<open>[simp]\<close> by default,
   748   because for rings of characteristic zero, better simp rules are possible.
   749   For a type like integers mod \<open>n\<close>, type-instantiated versions of these rules
   750   should be added to the simplifier, along with a type-specific rule for
   751   deciding propositions of the form \<open>iszero (numeral w)\<close>.
   752 
   753   bh: Maybe it would not be so bad to just declare these as simp rules anyway?
   754   I should test whether these rules take precedence over the \<open>ring_char_0\<close>
   755   rules in the simplifier.
   756 \<close>
   757 
   758 lemma eq_numeral_iff_iszero:
   759   "numeral x = numeral y \<longleftrightarrow> iszero (sub x y)"
   760   "numeral x = - numeral y \<longleftrightarrow> iszero (numeral (x + y))"
   761   "- numeral x = numeral y \<longleftrightarrow> iszero (numeral (x + y))"
   762   "- numeral x = - numeral y \<longleftrightarrow> iszero (sub y x)"
   763   "numeral x = 1 \<longleftrightarrow> iszero (sub x One)"
   764   "1 = numeral y \<longleftrightarrow> iszero (sub One y)"
   765   "- numeral x = 1 \<longleftrightarrow> iszero (numeral (x + One))"
   766   "1 = - numeral y \<longleftrightarrow> iszero (numeral (One + y))"
   767   "numeral x = 0 \<longleftrightarrow> iszero (numeral x)"
   768   "0 = numeral y \<longleftrightarrow> iszero (numeral y)"
   769   "- numeral x = 0 \<longleftrightarrow> iszero (numeral x)"
   770   "0 = - numeral y \<longleftrightarrow> iszero (numeral y)"
   771   unfolding eq_iff_iszero_diff diff_numeral_simps diff_numeral_special
   772   by simp_all
   773 
   774 end
   775 
   776 
   777 subsubsection \<open>Equality and negation: class \<open>ring_char_0\<close>\<close>
   778 
   779 context ring_char_0
   780 begin
   781 
   782 lemma not_iszero_numeral [simp]: "\<not> iszero (numeral w)"
   783   by (simp add: iszero_def)
   784 
   785 lemma neg_numeral_eq_iff: "- numeral m = - numeral n \<longleftrightarrow> m = n"
   786   by simp
   787 
   788 lemma numeral_neq_neg_numeral: "numeral m \<noteq> - numeral n"
   789   by (simp add: eq_neg_iff_add_eq_0 numeral_plus_numeral)
   790 
   791 lemma neg_numeral_neq_numeral: "- numeral m \<noteq> numeral n"
   792   by (rule numeral_neq_neg_numeral [symmetric])
   793 
   794 lemma zero_neq_neg_numeral: "0 \<noteq> - numeral n"
   795   by simp
   796 
   797 lemma neg_numeral_neq_zero: "- numeral n \<noteq> 0"
   798   by simp
   799 
   800 lemma one_neq_neg_numeral: "1 \<noteq> - numeral n"
   801   using numeral_neq_neg_numeral [of One n] by (simp add: numeral_One)
   802 
   803 lemma neg_numeral_neq_one: "- numeral n \<noteq> 1"
   804   using neg_numeral_neq_numeral [of n One] by (simp add: numeral_One)
   805 
   806 lemma neg_one_neq_numeral: "- 1 \<noteq> numeral n"
   807   using neg_numeral_neq_numeral [of One n] by (simp add: numeral_One)
   808 
   809 lemma numeral_neq_neg_one: "numeral n \<noteq> - 1"
   810   using numeral_neq_neg_numeral [of n One] by (simp add: numeral_One)
   811 
   812 lemma neg_one_eq_numeral_iff: "- 1 = - numeral n \<longleftrightarrow> n = One"
   813   using neg_numeral_eq_iff [of One n] by (auto simp add: numeral_One)
   814 
   815 lemma numeral_eq_neg_one_iff: "- numeral n = - 1 \<longleftrightarrow> n = One"
   816   using neg_numeral_eq_iff [of n One] by (auto simp add: numeral_One)
   817 
   818 lemma neg_one_neq_zero: "- 1 \<noteq> 0"
   819   by simp
   820 
   821 lemma zero_neq_neg_one: "0 \<noteq> - 1"
   822   by simp
   823 
   824 lemma neg_one_neq_one: "- 1 \<noteq> 1"
   825   using neg_numeral_neq_numeral [of One One] by (simp only: numeral_One not_False_eq_True)
   826 
   827 lemma one_neq_neg_one: "1 \<noteq> - 1"
   828   using numeral_neq_neg_numeral [of One One] by (simp only: numeral_One not_False_eq_True)
   829 
   830 lemmas eq_neg_numeral_simps [simp] =
   831   neg_numeral_eq_iff
   832   numeral_neq_neg_numeral neg_numeral_neq_numeral
   833   one_neq_neg_numeral neg_numeral_neq_one
   834   zero_neq_neg_numeral neg_numeral_neq_zero
   835   neg_one_neq_numeral numeral_neq_neg_one
   836   neg_one_eq_numeral_iff numeral_eq_neg_one_iff
   837   neg_one_neq_zero zero_neq_neg_one
   838   neg_one_neq_one one_neq_neg_one
   839 
   840 end
   841 
   842 
   843 subsubsection \<open>Structures with negation and order: class \<open>linordered_idom\<close>\<close>
   844 
   845 context linordered_idom
   846 begin
   847 
   848 subclass ring_char_0 ..
   849 
   850 lemma neg_numeral_le_iff: "- numeral m \<le> - numeral n \<longleftrightarrow> n \<le> m"
   851   by (simp only: neg_le_iff_le numeral_le_iff)
   852 
   853 lemma neg_numeral_less_iff: "- numeral m < - numeral n \<longleftrightarrow> n < m"
   854   by (simp only: neg_less_iff_less numeral_less_iff)
   855 
   856 lemma neg_numeral_less_zero: "- numeral n < 0"
   857   by (simp only: neg_less_0_iff_less zero_less_numeral)
   858 
   859 lemma neg_numeral_le_zero: "- numeral n \<le> 0"
   860   by (simp only: neg_le_0_iff_le zero_le_numeral)
   861 
   862 lemma not_zero_less_neg_numeral: "\<not> 0 < - numeral n"
   863   by (simp only: not_less neg_numeral_le_zero)
   864 
   865 lemma not_zero_le_neg_numeral: "\<not> 0 \<le> - numeral n"
   866   by (simp only: not_le neg_numeral_less_zero)
   867 
   868 lemma neg_numeral_less_numeral: "- numeral m < numeral n"
   869   using neg_numeral_less_zero zero_less_numeral by (rule less_trans)
   870 
   871 lemma neg_numeral_le_numeral: "- numeral m \<le> numeral n"
   872   by (simp only: less_imp_le neg_numeral_less_numeral)
   873 
   874 lemma not_numeral_less_neg_numeral: "\<not> numeral m < - numeral n"
   875   by (simp only: not_less neg_numeral_le_numeral)
   876 
   877 lemma not_numeral_le_neg_numeral: "\<not> numeral m \<le> - numeral n"
   878   by (simp only: not_le neg_numeral_less_numeral)
   879 
   880 lemma neg_numeral_less_one: "- numeral m < 1"
   881   by (rule neg_numeral_less_numeral [of m One, unfolded numeral_One])
   882 
   883 lemma neg_numeral_le_one: "- numeral m \<le> 1"
   884   by (rule neg_numeral_le_numeral [of m One, unfolded numeral_One])
   885 
   886 lemma not_one_less_neg_numeral: "\<not> 1 < - numeral m"
   887   by (simp only: not_less neg_numeral_le_one)
   888 
   889 lemma not_one_le_neg_numeral: "\<not> 1 \<le> - numeral m"
   890   by (simp only: not_le neg_numeral_less_one)
   891 
   892 lemma not_numeral_less_neg_one: "\<not> numeral m < - 1"
   893   using not_numeral_less_neg_numeral [of m One] by (simp add: numeral_One)
   894 
   895 lemma not_numeral_le_neg_one: "\<not> numeral m \<le> - 1"
   896   using not_numeral_le_neg_numeral [of m One] by (simp add: numeral_One)
   897 
   898 lemma neg_one_less_numeral: "- 1 < numeral m"
   899   using neg_numeral_less_numeral [of One m] by (simp add: numeral_One)
   900 
   901 lemma neg_one_le_numeral: "- 1 \<le> numeral m"
   902   using neg_numeral_le_numeral [of One m] by (simp add: numeral_One)
   903 
   904 lemma neg_numeral_less_neg_one_iff: "- numeral m < - 1 \<longleftrightarrow> m \<noteq> One"
   905   by (cases m) simp_all
   906 
   907 lemma neg_numeral_le_neg_one: "- numeral m \<le> - 1"
   908   by simp
   909 
   910 lemma not_neg_one_less_neg_numeral: "\<not> - 1 < - numeral m"
   911   by simp
   912 
   913 lemma not_neg_one_le_neg_numeral_iff: "\<not> - 1 \<le> - numeral m \<longleftrightarrow> m \<noteq> One"
   914   by (cases m) simp_all
   915 
   916 lemma sub_non_negative: "sub n m \<ge> 0 \<longleftrightarrow> n \<ge> m"
   917   by (simp only: sub_def le_diff_eq) simp
   918 
   919 lemma sub_positive: "sub n m > 0 \<longleftrightarrow> n > m"
   920   by (simp only: sub_def less_diff_eq) simp
   921 
   922 lemma sub_non_positive: "sub n m \<le> 0 \<longleftrightarrow> n \<le> m"
   923   by (simp only: sub_def diff_le_eq) simp
   924 
   925 lemma sub_negative: "sub n m < 0 \<longleftrightarrow> n < m"
   926   by (simp only: sub_def diff_less_eq) simp
   927 
   928 lemmas le_neg_numeral_simps [simp] =
   929   neg_numeral_le_iff
   930   neg_numeral_le_numeral not_numeral_le_neg_numeral
   931   neg_numeral_le_zero not_zero_le_neg_numeral
   932   neg_numeral_le_one not_one_le_neg_numeral
   933   neg_one_le_numeral not_numeral_le_neg_one
   934   neg_numeral_le_neg_one not_neg_one_le_neg_numeral_iff
   935 
   936 lemma le_minus_one_simps [simp]:
   937   "- 1 \<le> 0"
   938   "- 1 \<le> 1"
   939   "\<not> 0 \<le> - 1"
   940   "\<not> 1 \<le> - 1"
   941   by simp_all
   942 
   943 lemmas less_neg_numeral_simps [simp] =
   944   neg_numeral_less_iff
   945   neg_numeral_less_numeral not_numeral_less_neg_numeral
   946   neg_numeral_less_zero not_zero_less_neg_numeral
   947   neg_numeral_less_one not_one_less_neg_numeral
   948   neg_one_less_numeral not_numeral_less_neg_one
   949   neg_numeral_less_neg_one_iff not_neg_one_less_neg_numeral
   950 
   951 lemma less_minus_one_simps [simp]:
   952   "- 1 < 0"
   953   "- 1 < 1"
   954   "\<not> 0 < - 1"
   955   "\<not> 1 < - 1"
   956   by (simp_all add: less_le)
   957 
   958 lemma abs_numeral [simp]: "\<bar>numeral n\<bar> = numeral n"
   959   by simp
   960 
   961 lemma abs_neg_numeral [simp]: "\<bar>- numeral n\<bar> = numeral n"
   962   by (simp only: abs_minus_cancel abs_numeral)
   963 
   964 lemma abs_neg_one [simp]: "\<bar>- 1\<bar> = 1"
   965   by simp
   966 
   967 end
   968 
   969 
   970 subsubsection \<open>Natural numbers\<close>
   971 
   972 lemma Suc_1 [simp]: "Suc 1 = 2"
   973   unfolding Suc_eq_plus1 by (rule one_add_one)
   974 
   975 lemma Suc_numeral [simp]: "Suc (numeral n) = numeral (n + One)"
   976   unfolding Suc_eq_plus1 by (rule numeral_plus_one)
   977 
   978 definition pred_numeral :: "num \<Rightarrow> nat"
   979   where [code del]: "pred_numeral k = numeral k - 1"
   980 
   981 lemma numeral_eq_Suc: "numeral k = Suc (pred_numeral k)"
   982   by (simp add: pred_numeral_def)
   983 
   984 lemma eval_nat_numeral:
   985   "numeral One = Suc 0"
   986   "numeral (Bit0 n) = Suc (numeral (BitM n))"
   987   "numeral (Bit1 n) = Suc (numeral (Bit0 n))"
   988   by (simp_all add: numeral.simps BitM_plus_one)
   989 
   990 lemma pred_numeral_simps [simp]:
   991   "pred_numeral One = 0"
   992   "pred_numeral (Bit0 k) = numeral (BitM k)"
   993   "pred_numeral (Bit1 k) = numeral (Bit0 k)"
   994   by (simp_all only: pred_numeral_def eval_nat_numeral diff_Suc_Suc diff_0)
   995 
   996 lemma numeral_2_eq_2: "2 = Suc (Suc 0)"
   997   by (simp add: eval_nat_numeral)
   998 
   999 lemma numeral_3_eq_3: "3 = Suc (Suc (Suc 0))"
  1000   by (simp add: eval_nat_numeral)
  1001 
  1002 lemma numeral_1_eq_Suc_0: "Numeral1 = Suc 0"
  1003   by (simp only: numeral_One One_nat_def)
  1004 
  1005 lemma Suc_nat_number_of_add: "Suc (numeral v + n) = numeral (v + One) + n"
  1006   by simp
  1007 
  1008 lemma numerals: "Numeral1 = (1::nat)" "2 = Suc (Suc 0)"
  1009   by (rule numeral_One) (rule numeral_2_eq_2)
  1010 
  1011 lemmas numeral_nat = eval_nat_numeral BitM.simps One_nat_def
  1012 
  1013 text \<open>Comparisons involving @{term Suc}.\<close>
  1014 
  1015 lemma eq_numeral_Suc [simp]: "numeral k = Suc n \<longleftrightarrow> pred_numeral k = n"
  1016   by (simp add: numeral_eq_Suc)
  1017 
  1018 lemma Suc_eq_numeral [simp]: "Suc n = numeral k \<longleftrightarrow> n = pred_numeral k"
  1019   by (simp add: numeral_eq_Suc)
  1020 
  1021 lemma less_numeral_Suc [simp]: "numeral k < Suc n \<longleftrightarrow> pred_numeral k < n"
  1022   by (simp add: numeral_eq_Suc)
  1023 
  1024 lemma less_Suc_numeral [simp]: "Suc n < numeral k \<longleftrightarrow> n < pred_numeral k"
  1025   by (simp add: numeral_eq_Suc)
  1026 
  1027 lemma le_numeral_Suc [simp]: "numeral k \<le> Suc n \<longleftrightarrow> pred_numeral k \<le> n"
  1028   by (simp add: numeral_eq_Suc)
  1029 
  1030 lemma le_Suc_numeral [simp]: "Suc n \<le> numeral k \<longleftrightarrow> n \<le> pred_numeral k"
  1031   by (simp add: numeral_eq_Suc)
  1032 
  1033 lemma diff_Suc_numeral [simp]: "Suc n - numeral k = n - pred_numeral k"
  1034   by (simp add: numeral_eq_Suc)
  1035 
  1036 lemma diff_numeral_Suc [simp]: "numeral k - Suc n = pred_numeral k - n"
  1037   by (simp add: numeral_eq_Suc)
  1038 
  1039 lemma max_Suc_numeral [simp]: "max (Suc n) (numeral k) = Suc (max n (pred_numeral k))"
  1040   by (simp add: numeral_eq_Suc)
  1041 
  1042 lemma max_numeral_Suc [simp]: "max (numeral k) (Suc n) = Suc (max (pred_numeral k) n)"
  1043   by (simp add: numeral_eq_Suc)
  1044 
  1045 lemma min_Suc_numeral [simp]: "min (Suc n) (numeral k) = Suc (min n (pred_numeral k))"
  1046   by (simp add: numeral_eq_Suc)
  1047 
  1048 lemma min_numeral_Suc [simp]: "min (numeral k) (Suc n) = Suc (min (pred_numeral k) n)"
  1049   by (simp add: numeral_eq_Suc)
  1050 
  1051 text \<open>For @{term case_nat} and @{term rec_nat}.\<close>
  1052 
  1053 lemma case_nat_numeral [simp]: "case_nat a f (numeral v) = (let pv = pred_numeral v in f pv)"
  1054   by (simp add: numeral_eq_Suc)
  1055 
  1056 lemma case_nat_add_eq_if [simp]:
  1057   "case_nat a f ((numeral v) + n) = (let pv = pred_numeral v in f (pv + n))"
  1058   by (simp add: numeral_eq_Suc)
  1059 
  1060 lemma rec_nat_numeral [simp]:
  1061   "rec_nat a f (numeral v) = (let pv = pred_numeral v in f pv (rec_nat a f pv))"
  1062   by (simp add: numeral_eq_Suc Let_def)
  1063 
  1064 lemma rec_nat_add_eq_if [simp]:
  1065   "rec_nat a f (numeral v + n) = (let pv = pred_numeral v in f (pv + n) (rec_nat a f (pv + n)))"
  1066   by (simp add: numeral_eq_Suc Let_def)
  1067 
  1068 text \<open>Case analysis on @{term "n < 2"}.\<close>
  1069 lemma less_2_cases: "n < 2 \<Longrightarrow> n = 0 \<or> n = Suc 0"
  1070   by (auto simp add: numeral_2_eq_2)
  1071 
  1072 text \<open>Removal of Small Numerals: 0, 1 and (in additive positions) 2.\<close>
  1073 text \<open>bh: Are these rules really a good idea?\<close>
  1074 
  1075 lemma add_2_eq_Suc [simp]: "2 + n = Suc (Suc n)"
  1076   by simp
  1077 
  1078 lemma add_2_eq_Suc' [simp]: "n + 2 = Suc (Suc n)"
  1079   by simp
  1080 
  1081 text \<open>Can be used to eliminate long strings of Sucs, but not by default.\<close>
  1082 lemma Suc3_eq_add_3: "Suc (Suc (Suc n)) = 3 + n"
  1083   by simp
  1084 
  1085 lemmas nat_1_add_1 = one_add_one [where 'a=nat] (* legacy *)
  1086 
  1087 
  1088 subsection \<open>Particular lemmas concerning @{term 2}\<close>
  1089 
  1090 context linordered_field
  1091 begin
  1092 
  1093 subclass field_char_0 ..
  1094 
  1095 lemma half_gt_zero_iff: "0 < a / 2 \<longleftrightarrow> 0 < a"
  1096   by (auto simp add: field_simps)
  1097 
  1098 lemma half_gt_zero [simp]: "0 < a \<Longrightarrow> 0 < a / 2"
  1099   by (simp add: half_gt_zero_iff)
  1100 
  1101 end
  1102 
  1103 
  1104 subsection \<open>Numeral equations as default simplification rules\<close>
  1105 
  1106 declare (in numeral) numeral_One [simp]
  1107 declare (in numeral) numeral_plus_numeral [simp]
  1108 declare (in numeral) add_numeral_special [simp]
  1109 declare (in neg_numeral) add_neg_numeral_simps [simp]
  1110 declare (in neg_numeral) add_neg_numeral_special [simp]
  1111 declare (in neg_numeral) diff_numeral_simps [simp]
  1112 declare (in neg_numeral) diff_numeral_special [simp]
  1113 declare (in semiring_numeral) numeral_times_numeral [simp]
  1114 declare (in ring_1) mult_neg_numeral_simps [simp]
  1115 
  1116 subsection \<open>Setting up simprocs\<close>
  1117 
  1118 lemma mult_numeral_1: "Numeral1 * a = a"
  1119   for a :: "'a::semiring_numeral"
  1120   by simp
  1121 
  1122 lemma mult_numeral_1_right: "a * Numeral1 = a"
  1123   for a :: "'a::semiring_numeral"
  1124   by simp
  1125 
  1126 lemma divide_numeral_1: "a / Numeral1 = a"
  1127   for a :: "'a::field"
  1128   by simp
  1129 
  1130 lemma inverse_numeral_1: "inverse Numeral1 = (Numeral1::'a::division_ring)"
  1131   by simp
  1132 
  1133 text \<open>
  1134   Theorem lists for the cancellation simprocs. The use of a binary
  1135   numeral for 1 reduces the number of special cases.
  1136 \<close>
  1137 
  1138 lemma mult_1s:
  1139   "Numeral1 * a = a"
  1140   "a * Numeral1 = a"
  1141   "- Numeral1 * b = - b"
  1142   "b * - Numeral1 = - b"
  1143   for a :: "'a::semiring_numeral" and b :: "'b::ring_1"
  1144   by simp_all
  1145 
  1146 setup \<open>
  1147   Reorient_Proc.add
  1148     (fn Const (@{const_name numeral}, _) $ _ => true
  1149       | Const (@{const_name uminus}, _) $ (Const (@{const_name numeral}, _) $ _) => true
  1150       | _ => false)
  1151 \<close>
  1152 
  1153 simproc_setup reorient_numeral ("numeral w = x" | "- numeral w = y") =
  1154   Reorient_Proc.proc
  1155 
  1156 
  1157 subsubsection \<open>Simplification of arithmetic operations on integer constants\<close>
  1158 
  1159 lemmas arith_special = (* already declared simp above *)
  1160   add_numeral_special add_neg_numeral_special
  1161   diff_numeral_special
  1162 
  1163 lemmas arith_extra_simps = (* rules already in simpset *)
  1164   numeral_plus_numeral add_neg_numeral_simps add_0_left add_0_right
  1165   minus_zero
  1166   diff_numeral_simps diff_0 diff_0_right
  1167   numeral_times_numeral mult_neg_numeral_simps
  1168   mult_zero_left mult_zero_right
  1169   abs_numeral abs_neg_numeral
  1170 
  1171 text \<open>
  1172   For making a minimal simpset, one must include these default simprules.
  1173   Also include \<open>simp_thms\<close>.
  1174 \<close>
  1175 
  1176 lemmas arith_simps =
  1177   add_num_simps mult_num_simps sub_num_simps
  1178   BitM.simps dbl_simps dbl_inc_simps dbl_dec_simps
  1179   abs_zero abs_one arith_extra_simps
  1180 
  1181 lemmas more_arith_simps =
  1182   neg_le_iff_le
  1183   minus_zero left_minus right_minus
  1184   mult_1_left mult_1_right
  1185   mult_minus_left mult_minus_right
  1186   minus_add_distrib minus_minus mult.assoc
  1187 
  1188 lemmas of_nat_simps =
  1189   of_nat_0 of_nat_1 of_nat_Suc of_nat_add of_nat_mult
  1190 
  1191 text \<open>Simplification of relational operations.\<close>
  1192 
  1193 lemmas eq_numeral_extra =
  1194   zero_neq_one one_neq_zero
  1195 
  1196 lemmas rel_simps =
  1197   le_num_simps less_num_simps eq_num_simps
  1198   le_numeral_simps le_neg_numeral_simps le_minus_one_simps le_numeral_extra
  1199   less_numeral_simps less_neg_numeral_simps less_minus_one_simps less_numeral_extra
  1200   eq_numeral_simps eq_neg_numeral_simps eq_numeral_extra
  1201 
  1202 lemma Let_numeral [simp]: "Let (numeral v) f = f (numeral v)"
  1203   \<comment> \<open>Unfold all \<open>let\<close>s involving constants\<close>
  1204   unfolding Let_def ..
  1205 
  1206 lemma Let_neg_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 declaration \<open>
  1211 let
  1212   fun number_of ctxt T n =
  1213     if not (Sign.of_sort (Proof_Context.theory_of ctxt) (T, @{sort numeral}))
  1214     then raise CTERM ("number_of", [])
  1215     else Numeral.mk_cnumber (Thm.ctyp_of ctxt T) n;
  1216 in
  1217   K (
  1218     Lin_Arith.add_simps
  1219       @{thms arith_simps more_arith_simps rel_simps pred_numeral_simps
  1220         arith_special numeral_One of_nat_simps uminus_numeral_One}
  1221     #> Lin_Arith.add_simps
  1222       @{thms Suc_numeral Let_numeral Let_neg_numeral Let_0 Let_1
  1223         le_Suc_numeral le_numeral_Suc less_Suc_numeral less_numeral_Suc
  1224         Suc_eq_numeral eq_numeral_Suc mult_Suc mult_Suc_right of_nat_numeral}
  1225     #> Lin_Arith.set_number_of number_of)
  1226 end
  1227 \<close>
  1228 
  1229 
  1230 subsubsection \<open>Simplification of arithmetic when nested to the right\<close>
  1231 
  1232 lemma add_numeral_left [simp]: "numeral v + (numeral w + z) = (numeral(v + w) + z)"
  1233   by (simp_all add: add.assoc [symmetric])
  1234 
  1235 lemma add_neg_numeral_left [simp]:
  1236   "numeral v + (- numeral w + y) = (sub v w + y)"
  1237   "- numeral v + (numeral w + y) = (sub w v + y)"
  1238   "- numeral v + (- numeral w + y) = (- numeral(v + w) + y)"
  1239   by (simp_all add: add.assoc [symmetric])
  1240 
  1241 lemma mult_numeral_left [simp]:
  1242   "numeral v * (numeral w * z) = (numeral(v * w) * z :: 'a::semiring_numeral)"
  1243   "- numeral v * (numeral w * y) = (- numeral(v * w) * y :: 'b::ring_1)"
  1244   "numeral v * (- numeral w * y) = (- numeral(v * w) * y :: 'b::ring_1)"
  1245   "- numeral v * (- numeral w * y) = (numeral(v * w) * y :: 'b::ring_1)"
  1246   by (simp_all add: mult.assoc [symmetric])
  1247 
  1248 hide_const (open) One Bit0 Bit1 BitM inc pow sqr sub dbl dbl_inc dbl_dec
  1249 
  1250 
  1251 subsection \<open>Code module namespace\<close>
  1252 
  1253 code_identifier
  1254   code_module Num \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
  1255 
  1256 subsection \<open>Printing of evaluated natural numbers as numerals\<close>
  1257 
  1258 lemma [code_post]:
  1259   "Suc 0 = 1"
  1260   "Suc 1 = 2"
  1261   "Suc (numeral n) = numeral (Num.inc n)"
  1262   by (simp_all add: numeral_inc)
  1263 
  1264 lemmas [code_post] = Num.inc.simps
  1265 
  1266 end