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