# Theory Num

Up to index of Isabelle/HOL-Proofs

theory Num
imports Datatype
`(*  Title:      HOL/Num.thy    Author:     Florian Haftmann    Author:     Brian Huffman*)header {* Binary Numerals *}theory Numimports Datatypebeginsubsection {* The @{text num} type *}datatype num = One | Bit0 num | Bit1 numtext {* Increment function for type @{typ num} *}primrec inc :: "num => num" where  "inc One = Bit0 One" |  "inc (Bit0 x) = Bit1 x" |  "inc (Bit1 x) = Bit0 (inc x)"text {* Converting between type @{typ num} and type @{typ nat} *}primrec nat_of_num :: "num => nat" where  "nat_of_num One = Suc 0" |  "nat_of_num (Bit0 x) = nat_of_num x + nat_of_num x" |  "nat_of_num (Bit1 x) = Suc (nat_of_num x + nat_of_num x)"primrec num_of_nat :: "nat => num" where  "num_of_nat 0 = One" |  "num_of_nat (Suc n) = (if 0 < n then inc (num_of_nat n) else One)"lemma nat_of_num_pos: "0 < nat_of_num x"  by (induct x) simp_alllemma nat_of_num_neq_0: " nat_of_num x ≠ 0"  by (induct x) simp_alllemma nat_of_num_inc: "nat_of_num (inc x) = Suc (nat_of_num x)"  by (induct x) simp_alllemma num_of_nat_double:  "0 < n ==> num_of_nat (n + n) = Bit0 (num_of_nat n)"  by (induct n) simp_alltext {*  Type @{typ num} is isomorphic to the strictly positive  natural numbers.*}lemma nat_of_num_inverse: "num_of_nat (nat_of_num x) = x"  by (induct x) (simp_all add: num_of_nat_double nat_of_num_pos)lemma num_of_nat_inverse: "0 < n ==> nat_of_num (num_of_nat n) = n"  by (induct n) (simp_all add: nat_of_num_inc)lemma num_eq_iff: "x = y <-> nat_of_num x = nat_of_num y"  apply safe  apply (drule arg_cong [where f=num_of_nat])  apply (simp add: nat_of_num_inverse)  donelemma num_induct [case_names One inc]:  fixes P :: "num => bool"  assumes One: "P One"    and inc: "!!x. P x ==> P (inc x)"  shows "P x"proof -  obtain n where n: "Suc n = nat_of_num x"    by (cases "nat_of_num x", simp_all add: nat_of_num_neq_0)  have "P (num_of_nat (Suc n))"  proof (induct n)    case 0 show ?case using One by simp  next    case (Suc n)    then have "P (inc (num_of_nat (Suc n)))" by (rule inc)    then show "P (num_of_nat (Suc (Suc n)))" by simp  qed  with n show "P x"    by (simp add: nat_of_num_inverse)qedtext {*  From now on, there are two possible models for @{typ num}:  as positive naturals (rule @{text "num_induct"})  and as digit representation (rules @{text "num.induct"}, @{text "num.cases"}).*}subsection {* Numeral operations *}instantiation num :: "{plus,times,linorder}"begindefinition [code del]:  "m + n = num_of_nat (nat_of_num m + nat_of_num n)"definition [code del]:  "m * n = num_of_nat (nat_of_num m * nat_of_num n)"definition [code del]:  "m ≤ n <-> nat_of_num m ≤ nat_of_num n"definition [code del]:  "m < n <-> nat_of_num m < nat_of_num n"instance  by (default, auto simp add: less_num_def less_eq_num_def num_eq_iff)endlemma nat_of_num_add: "nat_of_num (x + y) = nat_of_num x + nat_of_num y"  unfolding plus_num_def  by (intro num_of_nat_inverse add_pos_pos nat_of_num_pos)lemma nat_of_num_mult: "nat_of_num (x * y) = nat_of_num x * nat_of_num y"  unfolding times_num_def  by (intro num_of_nat_inverse mult_pos_pos nat_of_num_pos)lemma add_num_simps [simp, code]:  "One + One = Bit0 One"  "One + Bit0 n = Bit1 n"  "One + Bit1 n = Bit0 (n + One)"  "Bit0 m + One = Bit1 m"  "Bit0 m + Bit0 n = Bit0 (m + n)"  "Bit0 m + Bit1 n = Bit1 (m + n)"  "Bit1 m + One = Bit0 (m + One)"  "Bit1 m + Bit0 n = Bit1 (m + n)"  "Bit1 m + Bit1 n = Bit0 (m + n + One)"  by (simp_all add: num_eq_iff nat_of_num_add)lemma mult_num_simps [simp, code]:  "m * One = m"  "One * n = n"  "Bit0 m * Bit0 n = Bit0 (Bit0 (m * n))"  "Bit0 m * Bit1 n = Bit0 (m * Bit1 n)"  "Bit1 m * Bit0 n = Bit0 (Bit1 m * n)"  "Bit1 m * Bit1 n = Bit1 (m + n + Bit0 (m * n))"  by (simp_all add: num_eq_iff nat_of_num_add    nat_of_num_mult distrib_right distrib_left)lemma eq_num_simps:  "One = One <-> True"  "One = Bit0 n <-> False"  "One = Bit1 n <-> False"  "Bit0 m = One <-> False"  "Bit1 m = One <-> False"  "Bit0 m = Bit0 n <-> m = n"  "Bit0 m = Bit1 n <-> False"  "Bit1 m = Bit0 n <-> False"  "Bit1 m = Bit1 n <-> m = n"  by simp_alllemma le_num_simps [simp, code]:  "One ≤ n <-> True"  "Bit0 m ≤ One <-> False"  "Bit1 m ≤ One <-> False"  "Bit0 m ≤ Bit0 n <-> m ≤ n"  "Bit0 m ≤ Bit1 n <-> m ≤ n"  "Bit1 m ≤ Bit1 n <-> m ≤ n"  "Bit1 m ≤ Bit0 n <-> m < n"  using nat_of_num_pos [of n] nat_of_num_pos [of m]  by (auto simp add: less_eq_num_def less_num_def)lemma less_num_simps [simp, code]:  "m < One <-> False"  "One < Bit0 n <-> True"  "One < Bit1 n <-> True"  "Bit0 m < Bit0 n <-> m < n"  "Bit0 m < Bit1 n <-> m ≤ n"  "Bit1 m < Bit1 n <-> m < n"  "Bit1 m < Bit0 n <-> m < n"  using nat_of_num_pos [of n] nat_of_num_pos [of m]  by (auto simp add: less_eq_num_def less_num_def)text {* Rules using @{text One} and @{text inc} as constructors *}lemma add_One: "x + One = inc x"  by (simp add: num_eq_iff nat_of_num_add nat_of_num_inc)lemma add_One_commute: "One + n = n + One"  by (induct n) simp_alllemma add_inc: "x + inc y = inc (x + y)"  by (simp add: num_eq_iff nat_of_num_add nat_of_num_inc)lemma mult_inc: "x * inc y = x * y + x"  by (simp add: num_eq_iff nat_of_num_mult nat_of_num_add nat_of_num_inc)text {* The @{const num_of_nat} conversion *}lemma num_of_nat_One:  "n ≤ 1 ==> num_of_nat n = One"  by (cases n) simp_alllemma num_of_nat_plus_distrib:  "0 < m ==> 0 < n ==> num_of_nat (m + n) = num_of_nat m + num_of_nat n"  by (induct n) (auto simp add: add_One add_One_commute add_inc)text {* A double-and-decrement function *}primrec BitM :: "num => num" where  "BitM One = One" |  "BitM (Bit0 n) = Bit1 (BitM n)" |  "BitM (Bit1 n) = Bit1 (Bit0 n)"lemma BitM_plus_one: "BitM n + One = Bit0 n"  by (induct n) simp_alllemma one_plus_BitM: "One + BitM n = Bit0 n"  unfolding add_One_commute BitM_plus_one ..text {* Squaring and exponentiation *}primrec sqr :: "num => num" where  "sqr One = One" |  "sqr (Bit0 n) = Bit0 (Bit0 (sqr n))" |  "sqr (Bit1 n) = Bit1 (Bit0 (sqr n + n))"primrec pow :: "num => num => num" where  "pow x One = x" |  "pow x (Bit0 y) = sqr (pow x y)" |  "pow x (Bit1 y) = sqr (pow x y) * x"lemma nat_of_num_sqr: "nat_of_num (sqr x) = nat_of_num x * nat_of_num x"  by (induct x, simp_all add: algebra_simps nat_of_num_add)lemma sqr_conv_mult: "sqr x = x * x"  by (simp add: num_eq_iff nat_of_num_sqr nat_of_num_mult)subsection {* Binary numerals *}text {*  We embed binary representations into a generic algebraic  structure using @{text numeral}.*}class numeral = one + semigroup_addbeginprimrec numeral :: "num => 'a" where  numeral_One: "numeral One = 1" |  numeral_Bit0: "numeral (Bit0 n) = numeral n + numeral n" |  numeral_Bit1: "numeral (Bit1 n) = numeral n + numeral n + 1"lemma numeral_code [code]:  "numeral One = 1"  "numeral (Bit0 n) = (let m = numeral n in m + m)"  "numeral (Bit1 n) = (let m = numeral n in m + m + 1)"  by (simp_all add: Let_def)  lemma one_plus_numeral_commute: "1 + numeral x = numeral x + 1"  apply (induct x)  apply simp  apply (simp add: add_assoc [symmetric], simp add: add_assoc)  apply (simp add: add_assoc [symmetric], simp add: add_assoc)  donelemma numeral_inc: "numeral (inc x) = numeral x + 1"proof (induct x)  case (Bit1 x)  have "numeral x + (1 + numeral x) + 1 = numeral x + (numeral x + 1) + 1"    by (simp only: one_plus_numeral_commute)  with Bit1 show ?case    by (simp add: add_assoc)qed simp_alldeclare numeral.simps [simp del]abbreviation "Numeral1 ≡ numeral One"declare numeral_One [code_post]endtext {* Negative numerals. *}class neg_numeral = numeral + group_addbegindefinition neg_numeral :: "num => 'a" where  "neg_numeral k = - numeral k"endtext {* Numeral syntax. *}syntax  "_Numeral" :: "num_const => 'a"    ("_")parse_translation {*let  fun num_of_int n = if n > 0 then case IntInf.quotRem (n, 2)     of (0, 1) => Syntax.const @{const_name One}      | (n, 0) => Syntax.const @{const_name Bit0} \$ num_of_int n      | (n, 1) => Syntax.const @{const_name Bit1} \$ num_of_int n    else raise Match;  val pos = Syntax.const @{const_name numeral}  val neg = Syntax.const @{const_name neg_numeral}  val one = Syntax.const @{const_name Groups.one}  val zero = Syntax.const @{const_name Groups.zero}  fun numeral_tr [(c as Const (@{syntax_const "_constrain"}, _)) \$ t \$ u] =        c \$ numeral_tr [t] \$ u    | numeral_tr [Const (num, _)] =        let          val {value, ...} = Lexicon.read_xnum num;        in          if value = 0 then zero else          if value > 0          then pos \$ num_of_int value          else neg \$ num_of_int (~value)        end    | numeral_tr ts = raise TERM ("numeral_tr", ts);in [("_Numeral", numeral_tr)] end*}typed_print_translation (advanced) {*let  fun dest_num (Const (@{const_syntax Bit0}, _) \$ n) = 2 * dest_num n    | dest_num (Const (@{const_syntax Bit1}, _) \$ n) = 2 * dest_num n + 1    | dest_num (Const (@{const_syntax One}, _)) = 1;  fun num_tr' sign ctxt T [n] =    let      val k = dest_num n;      val t' = Syntax.const @{syntax_const "_Numeral"} \$        Syntax.free (sign ^ string_of_int k);    in      case T of        Type (@{type_name fun}, [_, T']) =>          if not (Printer.show_type_constraint ctxt) andalso can Term.dest_Type T' then t'          else Syntax.const @{syntax_const "_constrain"} \$ t' \$ Syntax_Phases.term_of_typ ctxt T'      | T' => if T' = dummyT then t' else raise Match    end;in [(@{const_syntax numeral}, num_tr' ""),    (@{const_syntax neg_numeral}, num_tr' "-")] end*}ML_file "Tools/numeral.ML"subsection {* Class-specific numeral rules *}text {*  @{const numeral} is a morphism.*}subsubsection {* Structures with addition: class @{text numeral} *}context numeralbeginlemma numeral_add: "numeral (m + n) = numeral m + numeral n"  by (induct n rule: num_induct)     (simp_all only: numeral_One add_One add_inc numeral_inc add_assoc)lemma numeral_plus_numeral: "numeral m + numeral n = numeral (m + n)"  by (rule numeral_add [symmetric])lemma numeral_plus_one: "numeral n + 1 = numeral (n + One)"  using numeral_add [of n One] by (simp add: numeral_One)lemma one_plus_numeral: "1 + numeral n = numeral (One + n)"  using numeral_add [of One n] by (simp add: numeral_One)lemma one_add_one: "1 + 1 = 2"  using numeral_add [of One One] by (simp add: numeral_One)lemmas add_numeral_special =  numeral_plus_one one_plus_numeral one_add_oneendsubsubsection {*  Structures with negation: class @{text neg_numeral}*}context neg_numeralbegintext {* Numerals form an abelian subgroup. *}inductive is_num :: "'a => bool" where  "is_num 1" |  "is_num x ==> is_num (- x)" |  "[|is_num x; is_num y|] ==> is_num (x + y)"lemma is_num_numeral: "is_num (numeral k)"  by (induct k, simp_all add: numeral.simps is_num.intros)lemma is_num_add_commute:  "[|is_num x; is_num y|] ==> x + y = y + x"  apply (induct x rule: is_num.induct)  apply (induct y rule: is_num.induct)  apply simp  apply (rule_tac a=x in add_left_imp_eq)  apply (rule_tac a=x in add_right_imp_eq)  apply (simp add: add_assoc minus_add_cancel)  apply (simp add: add_assoc [symmetric], simp add: add_assoc)  apply (rule_tac a=x in add_left_imp_eq)  apply (rule_tac a=x in add_right_imp_eq)  apply (simp add: add_assoc minus_add_cancel add_minus_cancel)  apply (simp add: add_assoc, simp add: add_assoc [symmetric])  donelemma is_num_add_left_commute:  "[|is_num x; is_num y|] ==> x + (y + z) = y + (x + z)"  by (simp only: add_assoc [symmetric] is_num_add_commute)lemmas is_num_normalize =  add_assoc is_num_add_commute is_num_add_left_commute  is_num.intros is_num_numeral  diff_minus minus_add add_minus_cancel minus_add_canceldefinition dbl :: "'a => 'a" where "dbl x = x + x"definition dbl_inc :: "'a => 'a" where "dbl_inc x = x + x + 1"definition dbl_dec :: "'a => 'a" where "dbl_dec x = x + x - 1"definition sub :: "num => num => 'a" where  "sub k l = numeral k - numeral l"lemma numeral_BitM: "numeral (BitM n) = numeral (Bit0 n) - 1"  by (simp only: BitM_plus_one [symmetric] numeral_add numeral_One eq_diff_eq)lemma dbl_simps [simp]:  "dbl (neg_numeral k) = neg_numeral (Bit0 k)"  "dbl 0 = 0"  "dbl 1 = 2"  "dbl (numeral k) = numeral (Bit0 k)"  unfolding dbl_def neg_numeral_def numeral.simps  by (simp_all add: minus_add)lemma dbl_inc_simps [simp]:  "dbl_inc (neg_numeral k) = neg_numeral (BitM k)"  "dbl_inc 0 = 1"  "dbl_inc 1 = 3"  "dbl_inc (numeral k) = numeral (Bit1 k)"  unfolding dbl_inc_def neg_numeral_def numeral.simps numeral_BitM  by (simp_all add: is_num_normalize)lemma dbl_dec_simps [simp]:  "dbl_dec (neg_numeral k) = neg_numeral (Bit1 k)"  "dbl_dec 0 = -1"  "dbl_dec 1 = 1"  "dbl_dec (numeral k) = numeral (BitM k)"  unfolding dbl_dec_def neg_numeral_def numeral.simps numeral_BitM  by (simp_all add: is_num_normalize)lemma sub_num_simps [simp]:  "sub One One = 0"  "sub One (Bit0 l) = neg_numeral (BitM l)"  "sub One (Bit1 l) = neg_numeral (Bit0 l)"  "sub (Bit0 k) One = numeral (BitM k)"  "sub (Bit1 k) One = numeral (Bit0 k)"  "sub (Bit0 k) (Bit0 l) = dbl (sub k l)"  "sub (Bit0 k) (Bit1 l) = dbl_dec (sub k l)"  "sub (Bit1 k) (Bit0 l) = dbl_inc (sub k l)"  "sub (Bit1 k) (Bit1 l) = dbl (sub k l)"  unfolding dbl_def dbl_dec_def dbl_inc_def sub_def  unfolding neg_numeral_def numeral.simps numeral_BitM  by (simp_all add: is_num_normalize)lemma add_neg_numeral_simps:  "numeral m + neg_numeral n = sub m n"  "neg_numeral m + numeral n = sub n m"  "neg_numeral m + neg_numeral n = neg_numeral (m + n)"  unfolding sub_def diff_minus neg_numeral_def numeral_add numeral.simps  by (simp_all add: is_num_normalize)lemma add_neg_numeral_special:  "1 + neg_numeral m = sub One m"  "neg_numeral m + 1 = sub One m"  unfolding sub_def diff_minus neg_numeral_def numeral_add numeral.simps  by (simp_all add: is_num_normalize)lemma diff_numeral_simps:  "numeral m - numeral n = sub m n"  "numeral m - neg_numeral n = numeral (m + n)"  "neg_numeral m - numeral n = neg_numeral (m + n)"  "neg_numeral m - neg_numeral n = sub n m"  unfolding neg_numeral_def sub_def diff_minus numeral_add numeral.simps  by (simp_all add: is_num_normalize)lemma diff_numeral_special:  "1 - numeral n = sub One n"  "1 - neg_numeral n = numeral (One + n)"  "numeral m - 1 = sub m One"  "neg_numeral m - 1 = neg_numeral (m + One)"  unfolding neg_numeral_def sub_def diff_minus numeral_add numeral.simps  by (simp_all add: is_num_normalize)lemma minus_one: "- 1 = -1"  unfolding neg_numeral_def numeral.simps ..lemma minus_numeral: "- numeral n = neg_numeral n"  unfolding neg_numeral_def ..lemma minus_neg_numeral: "- neg_numeral n = numeral n"  unfolding neg_numeral_def by simplemmas minus_numeral_simps [simp] =  minus_one minus_numeral minus_neg_numeralendsubsubsection {*  Structures with multiplication: class @{text semiring_numeral}*}class semiring_numeral = semiring + monoid_multbeginsubclass numeral ..lemma numeral_mult: "numeral (m * n) = numeral m * numeral n"  apply (induct n rule: num_induct)  apply (simp add: numeral_One)  apply (simp add: mult_inc numeral_inc numeral_add distrib_left)  donelemma numeral_times_numeral: "numeral m * numeral n = numeral (m * n)"  by (rule numeral_mult [symmetric])endsubsubsection {*  Structures with a zero: class @{text semiring_1}*}context semiring_1beginsubclass semiring_numeral ..lemma of_nat_numeral [simp]: "of_nat (numeral n) = numeral n"  by (induct n,    simp_all only: numeral.simps numeral_class.numeral.simps of_nat_add of_nat_1)lemma mult_2: "2 * z = z + z"  unfolding one_add_one [symmetric] distrib_right by simplemma mult_2_right: "z * 2 = z + z"  unfolding one_add_one [symmetric] distrib_left by simpendlemma nat_of_num_numeral: "nat_of_num = numeral"proof  fix n  have "numeral n = nat_of_num n"    by (induct n) (simp_all add: numeral.simps)  then show "nat_of_num n = numeral n" by simpqedsubsubsection {*  Equality: class @{text semiring_char_0}*}context semiring_char_0beginlemma numeral_eq_iff: "numeral m = numeral n <-> m = n"  unfolding of_nat_numeral [symmetric] nat_of_num_numeral [symmetric]    of_nat_eq_iff num_eq_iff ..lemma numeral_eq_one_iff: "numeral n = 1 <-> n = One"  by (rule numeral_eq_iff [of n One, unfolded numeral_One])lemma one_eq_numeral_iff: "1 = numeral n <-> One = n"  by (rule numeral_eq_iff [of One n, unfolded numeral_One])lemma numeral_neq_zero: "numeral n ≠ 0"  unfolding of_nat_numeral [symmetric] nat_of_num_numeral [symmetric]  by (simp add: nat_of_num_pos)lemma zero_neq_numeral: "0 ≠ numeral n"  unfolding eq_commute [of 0] by (rule numeral_neq_zero)lemmas eq_numeral_simps [simp] =  numeral_eq_iff  numeral_eq_one_iff  one_eq_numeral_iff  numeral_neq_zero  zero_neq_numeralendsubsubsection {*  Comparisons: class @{text linordered_semidom}*}text {*  Could be perhaps more general than here. *}context linordered_semidombeginlemma numeral_le_iff: "numeral m ≤ numeral n <-> m ≤ n"proof -  have "of_nat (numeral m) ≤ of_nat (numeral n) <-> m ≤ n"    unfolding less_eq_num_def nat_of_num_numeral of_nat_le_iff ..  then show ?thesis by simpqedlemma one_le_numeral: "1 ≤ numeral n"using numeral_le_iff [of One n] by (simp add: numeral_One)lemma numeral_le_one_iff: "numeral n ≤ 1 <-> n ≤ One"using numeral_le_iff [of n One] by (simp add: numeral_One)lemma numeral_less_iff: "numeral m < numeral n <-> m < n"proof -  have "of_nat (numeral m) < of_nat (numeral n) <-> m < n"    unfolding less_num_def nat_of_num_numeral of_nat_less_iff ..  then show ?thesis by simpqedlemma not_numeral_less_one: "¬ numeral n < 1"  using numeral_less_iff [of n One] by (simp add: numeral_One)lemma one_less_numeral_iff: "1 < numeral n <-> One < n"  using numeral_less_iff [of One n] by (simp add: numeral_One)lemma zero_le_numeral: "0 ≤ numeral n"  by (induct n) (simp_all add: numeral.simps)lemma zero_less_numeral: "0 < numeral n"  by (induct n) (simp_all add: numeral.simps add_pos_pos)lemma not_numeral_le_zero: "¬ numeral n ≤ 0"  by (simp add: not_le zero_less_numeral)lemma not_numeral_less_zero: "¬ numeral n < 0"  by (simp add: not_less zero_le_numeral)lemmas le_numeral_extra =  zero_le_one not_one_le_zero  order_refl [of 0] order_refl [of 1]lemmas less_numeral_extra =  zero_less_one not_one_less_zero  less_irrefl [of 0] less_irrefl [of 1]lemmas le_numeral_simps [simp] =  numeral_le_iff  one_le_numeral  numeral_le_one_iff  zero_le_numeral  not_numeral_le_zerolemmas less_numeral_simps [simp] =  numeral_less_iff  one_less_numeral_iff  not_numeral_less_one  zero_less_numeral  not_numeral_less_zeroendsubsubsection {*  Multiplication and negation: class @{text ring_1}*}context ring_1beginsubclass neg_numeral ..lemma mult_neg_numeral_simps:  "neg_numeral m * neg_numeral n = numeral (m * n)"  "neg_numeral m * numeral n = neg_numeral (m * n)"  "numeral m * neg_numeral n = neg_numeral (m * n)"  unfolding neg_numeral_def mult_minus_left mult_minus_right  by (simp_all only: minus_minus numeral_mult)lemma mult_minus1 [simp]: "-1 * z = - z"  unfolding neg_numeral_def numeral.simps mult_minus_left by simplemma mult_minus1_right [simp]: "z * -1 = - z"  unfolding neg_numeral_def numeral.simps mult_minus_right by simpendsubsubsection {*  Equality using @{text iszero} for rings with non-zero characteristic*}context ring_1begindefinition iszero :: "'a => bool"  where "iszero z <-> z = 0"lemma iszero_0 [simp]: "iszero 0"  by (simp add: iszero_def)lemma not_iszero_1 [simp]: "¬ iszero 1"  by (simp add: iszero_def)lemma not_iszero_Numeral1: "¬ iszero Numeral1"  by (simp add: numeral_One)lemma iszero_neg_numeral [simp]:  "iszero (neg_numeral w) <-> iszero (numeral w)"  unfolding iszero_def neg_numeral_def  by (rule neg_equal_0_iff_equal)lemma eq_iff_iszero_diff: "x = y <-> iszero (x - y)"  unfolding iszero_def by (rule eq_iff_diff_eq_0)text {* The @{text "eq_numeral_iff_iszero"} lemmas are not declared@{text "[simp]"} by default, because for rings of characteristic zero,better simp rules are possible. For a type like integers mod @{text"n"}, type-instantiated versions of these rules should be added to thesimplifier, along with a type-specific rule for deciding propositionsof the form @{text "iszero (numeral w)"}.bh: Maybe it would not be so bad to just declare these as simprules anyway? I should test whether these rules take precedence overthe @{text "ring_char_0"} rules in the simplifier.*}lemma eq_numeral_iff_iszero:  "numeral x = numeral y <-> iszero (sub x y)"  "numeral x = neg_numeral y <-> iszero (numeral (x + y))"  "neg_numeral x = numeral y <-> iszero (numeral (x + y))"  "neg_numeral x = neg_numeral y <-> iszero (sub y x)"  "numeral x = 1 <-> iszero (sub x One)"  "1 = numeral y <-> iszero (sub One y)"  "neg_numeral x = 1 <-> iszero (numeral (x + One))"  "1 = neg_numeral y <-> iszero (numeral (One + y))"  "numeral x = 0 <-> iszero (numeral x)"  "0 = numeral y <-> iszero (numeral y)"  "neg_numeral x = 0 <-> iszero (numeral x)"  "0 = neg_numeral y <-> iszero (numeral y)"  unfolding eq_iff_iszero_diff diff_numeral_simps diff_numeral_special  by simp_allendsubsubsection {*  Equality and negation: class @{text ring_char_0}*}class ring_char_0 = ring_1 + semiring_char_0beginlemma not_iszero_numeral [simp]: "¬ iszero (numeral w)"  by (simp add: iszero_def)lemma neg_numeral_eq_iff: "neg_numeral m = neg_numeral n <-> m = n"  by (simp only: neg_numeral_def neg_equal_iff_equal numeral_eq_iff)lemma numeral_neq_neg_numeral: "numeral m ≠ neg_numeral n"  unfolding neg_numeral_def eq_neg_iff_add_eq_0  by (simp add: numeral_plus_numeral)lemma neg_numeral_neq_numeral: "neg_numeral m ≠ numeral n"  by (rule numeral_neq_neg_numeral [symmetric])lemma zero_neq_neg_numeral: "0 ≠ neg_numeral n"  unfolding neg_numeral_def neg_0_equal_iff_equal by simplemma neg_numeral_neq_zero: "neg_numeral n ≠ 0"  unfolding neg_numeral_def neg_equal_0_iff_equal by simplemma one_neq_neg_numeral: "1 ≠ neg_numeral n"  using numeral_neq_neg_numeral [of One n] by (simp add: numeral_One)lemma neg_numeral_neq_one: "neg_numeral n ≠ 1"  using neg_numeral_neq_numeral [of n One] by (simp add: numeral_One)lemmas eq_neg_numeral_simps [simp] =  neg_numeral_eq_iff  numeral_neq_neg_numeral neg_numeral_neq_numeral  one_neq_neg_numeral neg_numeral_neq_one  zero_neq_neg_numeral neg_numeral_neq_zeroendsubsubsection {*  Structures with negation and order: class @{text linordered_idom}*}context linordered_idombeginsubclass ring_char_0 ..lemma neg_numeral_le_iff: "neg_numeral m ≤ neg_numeral n <-> n ≤ m"  by (simp only: neg_numeral_def neg_le_iff_le numeral_le_iff)lemma neg_numeral_less_iff: "neg_numeral m < neg_numeral n <-> n < m"  by (simp only: neg_numeral_def neg_less_iff_less numeral_less_iff)lemma neg_numeral_less_zero: "neg_numeral n < 0"  by (simp only: neg_numeral_def neg_less_0_iff_less zero_less_numeral)lemma neg_numeral_le_zero: "neg_numeral n ≤ 0"  by (simp only: neg_numeral_def neg_le_0_iff_le zero_le_numeral)lemma not_zero_less_neg_numeral: "¬ 0 < neg_numeral n"  by (simp only: not_less neg_numeral_le_zero)lemma not_zero_le_neg_numeral: "¬ 0 ≤ neg_numeral n"  by (simp only: not_le neg_numeral_less_zero)lemma neg_numeral_less_numeral: "neg_numeral m < numeral n"  using neg_numeral_less_zero zero_less_numeral by (rule less_trans)lemma neg_numeral_le_numeral: "neg_numeral m ≤ numeral n"  by (simp only: less_imp_le neg_numeral_less_numeral)lemma not_numeral_less_neg_numeral: "¬ numeral m < neg_numeral n"  by (simp only: not_less neg_numeral_le_numeral)lemma not_numeral_le_neg_numeral: "¬ numeral m ≤ neg_numeral n"  by (simp only: not_le neg_numeral_less_numeral)  lemma neg_numeral_less_one: "neg_numeral m < 1"  by (rule neg_numeral_less_numeral [of m One, unfolded numeral_One])lemma neg_numeral_le_one: "neg_numeral m ≤ 1"  by (rule neg_numeral_le_numeral [of m One, unfolded numeral_One])lemma not_one_less_neg_numeral: "¬ 1 < neg_numeral m"  by (simp only: not_less neg_numeral_le_one)lemma not_one_le_neg_numeral: "¬ 1 ≤ neg_numeral m"  by (simp only: not_le neg_numeral_less_one)lemma sub_non_negative:  "sub n m ≥ 0 <-> n ≥ m"  by (simp only: sub_def le_diff_eq) simplemma sub_positive:  "sub n m > 0 <-> n > m"  by (simp only: sub_def less_diff_eq) simplemma sub_non_positive:  "sub n m ≤ 0 <-> n ≤ m"  by (simp only: sub_def diff_le_eq) simplemma sub_negative:  "sub n m < 0 <-> n < m"  by (simp only: sub_def diff_less_eq) simplemmas le_neg_numeral_simps [simp] =  neg_numeral_le_iff  neg_numeral_le_numeral not_numeral_le_neg_numeral  neg_numeral_le_zero not_zero_le_neg_numeral  neg_numeral_le_one not_one_le_neg_numerallemmas less_neg_numeral_simps [simp] =  neg_numeral_less_iff  neg_numeral_less_numeral not_numeral_less_neg_numeral  neg_numeral_less_zero not_zero_less_neg_numeral  neg_numeral_less_one not_one_less_neg_numerallemma abs_numeral [simp]: "abs (numeral n) = numeral n"  by simplemma abs_neg_numeral [simp]: "abs (neg_numeral n) = numeral n"  by (simp only: neg_numeral_def abs_minus_cancel abs_numeral)endsubsubsection {*  Natural numbers*}lemma Suc_1 [simp]: "Suc 1 = 2"  unfolding Suc_eq_plus1 by (rule one_add_one)lemma Suc_numeral [simp]: "Suc (numeral n) = numeral (n + One)"  unfolding Suc_eq_plus1 by (rule numeral_plus_one)definition pred_numeral :: "num => nat"  where [code del]: "pred_numeral k = numeral k - 1"lemma numeral_eq_Suc: "numeral k = Suc (pred_numeral k)"  unfolding pred_numeral_def by simplemma eval_nat_numeral:  "numeral One = Suc 0"  "numeral (Bit0 n) = Suc (numeral (BitM n))"  "numeral (Bit1 n) = Suc (numeral (Bit0 n))"  by (simp_all add: numeral.simps BitM_plus_one)lemma pred_numeral_simps [simp]:  "pred_numeral One = 0"  "pred_numeral (Bit0 k) = numeral (BitM k)"  "pred_numeral (Bit1 k) = numeral (Bit0 k)"  unfolding pred_numeral_def eval_nat_numeral  by (simp_all only: diff_Suc_Suc diff_0)lemma numeral_2_eq_2: "2 = Suc (Suc 0)"  by (simp add: eval_nat_numeral)lemma numeral_3_eq_3: "3 = Suc (Suc (Suc 0))"  by (simp add: eval_nat_numeral)lemma numeral_1_eq_Suc_0: "Numeral1 = Suc 0"  by (simp only: numeral_One One_nat_def)lemma Suc_nat_number_of_add:  "Suc (numeral v + n) = numeral (v + One) + n"  by simp(*Maps #n to n for n = 1, 2*)lemmas numerals = numeral_One [where 'a=nat] numeral_2_eq_2text {* Comparisons involving @{term Suc}. *}lemma eq_numeral_Suc [simp]: "numeral k = Suc n <-> pred_numeral k = n"  by (simp add: numeral_eq_Suc)lemma Suc_eq_numeral [simp]: "Suc n = numeral k <-> n = pred_numeral k"  by (simp add: numeral_eq_Suc)lemma less_numeral_Suc [simp]: "numeral k < Suc n <-> pred_numeral k < n"  by (simp add: numeral_eq_Suc)lemma less_Suc_numeral [simp]: "Suc n < numeral k <-> n < pred_numeral k"  by (simp add: numeral_eq_Suc)lemma le_numeral_Suc [simp]: "numeral k ≤ Suc n <-> pred_numeral k ≤ n"  by (simp add: numeral_eq_Suc)lemma le_Suc_numeral [simp]: "Suc n ≤ numeral k <-> n ≤ pred_numeral k"  by (simp add: numeral_eq_Suc)lemma diff_Suc_numeral [simp]: "Suc n - numeral k = n - pred_numeral k"  by (simp add: numeral_eq_Suc)lemma diff_numeral_Suc [simp]: "numeral k - Suc n = pred_numeral k - n"  by (simp add: numeral_eq_Suc)lemma max_Suc_numeral [simp]:  "max (Suc n) (numeral k) = Suc (max n (pred_numeral k))"  by (simp add: numeral_eq_Suc)lemma max_numeral_Suc [simp]:  "max (numeral k) (Suc n) = Suc (max (pred_numeral k) n)"  by (simp add: numeral_eq_Suc)lemma min_Suc_numeral [simp]:  "min (Suc n) (numeral k) = Suc (min n (pred_numeral k))"  by (simp add: numeral_eq_Suc)lemma min_numeral_Suc [simp]:  "min (numeral k) (Suc n) = Suc (min (pred_numeral k) n)"  by (simp add: numeral_eq_Suc)text {* For @{term nat_case} and @{term nat_rec}. *}lemma nat_case_numeral [simp]:  "nat_case a f (numeral v) = (let pv = pred_numeral v in f pv)"  by (simp add: numeral_eq_Suc)lemma nat_case_add_eq_if [simp]:  "nat_case a f ((numeral v) + n) = (let pv = pred_numeral v in f (pv + n))"  by (simp add: numeral_eq_Suc)lemma nat_rec_numeral [simp]:  "nat_rec a f (numeral v) =    (let pv = pred_numeral v in f pv (nat_rec a f pv))"  by (simp add: numeral_eq_Suc Let_def)lemma nat_rec_add_eq_if [simp]:  "nat_rec a f (numeral v + n) =    (let pv = pred_numeral v in f (pv + n) (nat_rec a f (pv + n)))"  by (simp add: numeral_eq_Suc Let_def)text {* Case analysis on @{term "n < 2"} *}lemma less_2_cases: "n < 2 ==> n = 0 ∨ n = Suc 0"  by (auto simp add: numeral_2_eq_2)text {* Removal of Small Numerals: 0, 1 and (in additive positions) 2 *}text {* bh: Are these rules really a good idea? *}lemma add_2_eq_Suc [simp]: "2 + n = Suc (Suc n)"  by simplemma add_2_eq_Suc' [simp]: "n + 2 = Suc (Suc n)"  by simptext {* Can be used to eliminate long strings of Sucs, but not by default. *}lemma Suc3_eq_add_3: "Suc (Suc (Suc n)) = 3 + n"  by simplemmas nat_1_add_1 = one_add_one [where 'a=nat] (* legacy *)subsection {* Numeral equations as default simplification rules *}declare (in numeral) numeral_One [simp]declare (in numeral) numeral_plus_numeral [simp]declare (in numeral) add_numeral_special [simp]declare (in neg_numeral) add_neg_numeral_simps [simp]declare (in neg_numeral) add_neg_numeral_special [simp]declare (in neg_numeral) diff_numeral_simps [simp]declare (in neg_numeral) diff_numeral_special [simp]declare (in semiring_numeral) numeral_times_numeral [simp]declare (in ring_1) mult_neg_numeral_simps [simp]subsection {* Setting up simprocs *}lemma mult_numeral_1: "Numeral1 * a = (a::'a::semiring_numeral)"  by simplemma mult_numeral_1_right: "a * Numeral1 = (a::'a::semiring_numeral)"  by simplemma divide_numeral_1: "a / Numeral1 = (a::'a::field)"  by simplemma inverse_numeral_1:  "inverse Numeral1 = (Numeral1::'a::division_ring)"  by simptext{*Theorem lists for the cancellation simprocs. The use of a binarynumeral for 1 reduces the number of special cases.*}lemmas mult_1s =  mult_numeral_1 mult_numeral_1_right   mult_minus1 mult_minus1_rightsetup {*  Reorient_Proc.add    (fn Const (@{const_name numeral}, _) \$ _ => true    | Const (@{const_name neg_numeral}, _) \$ _ => true    | _ => false)*}simproc_setup reorient_numeral  ("numeral w = x" | "neg_numeral w = y") = Reorient_Proc.procsubsubsection {* Simplification of arithmetic operations on integer constants. *}lemmas arith_special = (* already declared simp above *)  add_numeral_special add_neg_numeral_special  diff_numeral_special minus_one(* rules already in simpset *)lemmas arith_extra_simps =  numeral_plus_numeral add_neg_numeral_simps add_0_left add_0_right  minus_numeral minus_neg_numeral minus_zero minus_one  diff_numeral_simps diff_0 diff_0_right  numeral_times_numeral mult_neg_numeral_simps  mult_zero_left mult_zero_right  abs_numeral abs_neg_numeraltext {*  For making a minimal simpset, one must include these default simprules.  Also include @{text simp_thms}.*}lemmas arith_simps =  add_num_simps mult_num_simps sub_num_simps  BitM.simps dbl_simps dbl_inc_simps dbl_dec_simps  abs_zero abs_one arith_extra_simpstext {* Simplification of relational operations *}lemmas eq_numeral_extra =  zero_neq_one one_neq_zerolemmas rel_simps =  le_num_simps less_num_simps eq_num_simps  le_numeral_simps le_neg_numeral_simps le_numeral_extra  less_numeral_simps less_neg_numeral_simps less_numeral_extra  eq_numeral_simps eq_neg_numeral_simps eq_numeral_extrasubsubsection {* Simplification of arithmetic when nested to the right. *}lemma add_numeral_left [simp]:  "numeral v + (numeral w + z) = (numeral(v + w) + z)"  by (simp_all add: add_assoc [symmetric])lemma add_neg_numeral_left [simp]:  "numeral v + (neg_numeral w + y) = (sub v w + y)"  "neg_numeral v + (numeral w + y) = (sub w v + y)"  "neg_numeral v + (neg_numeral w + y) = (neg_numeral(v + w) + y)"  by (simp_all add: add_assoc [symmetric])lemma mult_numeral_left [simp]:  "numeral v * (numeral w * z) = (numeral(v * w) * z :: 'a::semiring_numeral)"  "neg_numeral v * (numeral w * y) = (neg_numeral(v * w) * y :: 'b::ring_1)"  "numeral v * (neg_numeral w * y) = (neg_numeral(v * w) * y :: 'b::ring_1)"  "neg_numeral v * (neg_numeral w * y) = (numeral(v * w) * y :: 'b::ring_1)"  by (simp_all add: mult_assoc [symmetric])hide_const (open) One Bit0 Bit1 BitM inc pow sqr sub dbl dbl_inc dbl_decsubsection {* code module namespace *}code_modulename SML  Num Arithcode_modulename OCaml  Num Arithcode_modulename Haskell  Num Arithend`