src/HOL/Int.thy
author haftmann
Mon, 10 May 2010 14:55:04 +0200
changeset 36801 3560de0fe851
parent 36749 a8dc19a352e6
child 36811 4ab4aa5bee1c
permissions -rw-r--r--
moved int induction lemma to theory Int as int_bidirectional_induct
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
     1
(*  Title:      Int.thy
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
     3
                Tobias Nipkow, Florian Haftmann, TU Muenchen
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
     4
    Copyright   1994  University of Cambridge
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
     5
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
     6
*)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
     7
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
     8
header {* The Integers as Equivalence Classes over Pairs of Natural Numbers *} 
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
     9
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
    10
theory Int
26748
4d51ddd6aa5c Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents: 26732
diff changeset
    11
imports Equiv_Relations Nat Wellfounded
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
    12
uses
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
    13
  ("Tools/numeral.ML")
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
    14
  ("Tools/numeral_syntax.ML")
31068
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31065
diff changeset
    15
  ("Tools/int_arith.ML")
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
    16
begin
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
    17
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
    18
subsection {* The equivalence relation underlying the integers *}
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
    19
28661
a287d0e8aa9d slightly tuned
haftmann
parents: 28562
diff changeset
    20
definition intrel :: "((nat \<times> nat) \<times> (nat \<times> nat)) set" where
28562
4e74209f113e `code func` now just `code`
haftmann
parents: 28537
diff changeset
    21
  [code del]: "intrel = {((x, y), (u, v)) | x y u v. x + v = u +y }"
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
    22
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
    23
typedef (Integ)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
    24
  int = "UNIV//intrel"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
    25
  by (auto simp add: quotient_def)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
    26
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
    27
instantiation int :: "{zero, one, plus, minus, uminus, times, ord, abs, sgn}"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
    28
begin
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
    29
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
    30
definition
28562
4e74209f113e `code func` now just `code`
haftmann
parents: 28537
diff changeset
    31
  Zero_int_def [code del]: "0 = Abs_Integ (intrel `` {(0, 0)})"
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
    32
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
    33
definition
28562
4e74209f113e `code func` now just `code`
haftmann
parents: 28537
diff changeset
    34
  One_int_def [code del]: "1 = Abs_Integ (intrel `` {(1, 0)})"
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
    35
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
    36
definition
28562
4e74209f113e `code func` now just `code`
haftmann
parents: 28537
diff changeset
    37
  add_int_def [code del]: "z + w = Abs_Integ
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
    38
    (\<Union>(x, y) \<in> Rep_Integ z. \<Union>(u, v) \<in> Rep_Integ w.
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
    39
      intrel `` {(x + u, y + v)})"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
    40
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
    41
definition
28562
4e74209f113e `code func` now just `code`
haftmann
parents: 28537
diff changeset
    42
  minus_int_def [code del]:
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
    43
    "- z = Abs_Integ (\<Union>(x, y) \<in> Rep_Integ z. intrel `` {(y, x)})"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
    44
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
    45
definition
28562
4e74209f113e `code func` now just `code`
haftmann
parents: 28537
diff changeset
    46
  diff_int_def [code del]:  "z - w = z + (-w \<Colon> int)"
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
    47
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
    48
definition
28562
4e74209f113e `code func` now just `code`
haftmann
parents: 28537
diff changeset
    49
  mult_int_def [code del]: "z * w = Abs_Integ
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
    50
    (\<Union>(x, y) \<in> Rep_Integ z. \<Union>(u,v ) \<in> Rep_Integ w.
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
    51
      intrel `` {(x*u + y*v, x*v + y*u)})"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
    52
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
    53
definition
28562
4e74209f113e `code func` now just `code`
haftmann
parents: 28537
diff changeset
    54
  le_int_def [code del]:
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
    55
   "z \<le> w \<longleftrightarrow> (\<exists>x y u v. x+v \<le> u+y \<and> (x, y) \<in> Rep_Integ z \<and> (u, v) \<in> Rep_Integ w)"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
    56
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
    57
definition
28562
4e74209f113e `code func` now just `code`
haftmann
parents: 28537
diff changeset
    58
  less_int_def [code del]: "(z\<Colon>int) < w \<longleftrightarrow> z \<le> w \<and> z \<noteq> w"
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
    59
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
    60
definition
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
    61
  zabs_def: "\<bar>i\<Colon>int\<bar> = (if i < 0 then - i else i)"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
    62
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
    63
definition
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
    64
  zsgn_def: "sgn (i\<Colon>int) = (if i=0 then 0 else if 0<i then 1 else - 1)"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
    65
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
    66
instance ..
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
    67
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
    68
end
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
    69
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
    70
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
    71
subsection{*Construction of the Integers*}
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
    72
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
    73
lemma intrel_iff [simp]: "(((x,y),(u,v)) \<in> intrel) = (x+v = u+y)"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
    74
by (simp add: intrel_def)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
    75
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
    76
lemma equiv_intrel: "equiv UNIV intrel"
30198
922f944f03b2 name changes
nipkow
parents: 30079
diff changeset
    77
by (simp add: intrel_def equiv_def refl_on_def sym_def trans_def)
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
    78
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
    79
text{*Reduces equality of equivalence classes to the @{term intrel} relation:
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
    80
  @{term "(intrel `` {x} = intrel `` {y}) = ((x,y) \<in> intrel)"} *}
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
    81
lemmas equiv_intrel_iff [simp] = eq_equiv_class_iff [OF equiv_intrel UNIV_I UNIV_I]
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
    82
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
    83
text{*All equivalence classes belong to set of representatives*}
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
    84
lemma [simp]: "intrel``{(x,y)} \<in> Integ"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
    85
by (auto simp add: Integ_def intrel_def quotient_def)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
    86
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
    87
text{*Reduces equality on abstractions to equality on representatives:
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
    88
  @{prop "\<lbrakk>x \<in> Integ; y \<in> Integ\<rbrakk> \<Longrightarrow> (Abs_Integ x = Abs_Integ y) = (x=y)"} *}
35828
46cfc4b8112e now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents: 35634
diff changeset
    89
declare Abs_Integ_inject [simp,no_atp]  Abs_Integ_inverse [simp,no_atp]
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
    90
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
    91
text{*Case analysis on the representation of an integer as an equivalence
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
    92
      class of pairs of naturals.*}
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
    93
lemma eq_Abs_Integ [case_names Abs_Integ, cases type: int]:
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
    94
     "(!!x y. z = Abs_Integ(intrel``{(x,y)}) ==> P) ==> P"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
    95
apply (rule Abs_Integ_cases [of z]) 
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
    96
apply (auto simp add: Integ_def quotient_def) 
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
    97
done
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
    98
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
    99
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   100
subsection {* Arithmetic Operations *}
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   101
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   102
lemma minus: "- Abs_Integ(intrel``{(x,y)}) = Abs_Integ(intrel `` {(y,x)})"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   103
proof -
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   104
  have "(\<lambda>(x,y). intrel``{(y,x)}) respects intrel"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   105
    by (simp add: congruent_def) 
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   106
  thus ?thesis
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   107
    by (simp add: minus_int_def UN_equiv_class [OF equiv_intrel])
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   108
qed
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   109
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   110
lemma add:
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   111
     "Abs_Integ (intrel``{(x,y)}) + Abs_Integ (intrel``{(u,v)}) =
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   112
      Abs_Integ (intrel``{(x+u, y+v)})"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   113
proof -
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   114
  have "(\<lambda>z w. (\<lambda>(x,y). (\<lambda>(u,v). intrel `` {(x+u, y+v)}) w) z) 
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   115
        respects2 intrel"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   116
    by (simp add: congruent2_def)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   117
  thus ?thesis
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   118
    by (simp add: add_int_def UN_UN_split_split_eq
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   119
                  UN_equiv_class2 [OF equiv_intrel equiv_intrel])
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   120
qed
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   121
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   122
text{*Congruence property for multiplication*}
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   123
lemma mult_congruent2:
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   124
     "(%p1 p2. (%(x,y). (%(u,v). intrel``{(x*u + y*v, x*v + y*u)}) p2) p1)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   125
      respects2 intrel"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   126
apply (rule equiv_intrel [THEN congruent2_commuteI])
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   127
 apply (force simp add: mult_ac, clarify) 
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   128
apply (simp add: congruent_def mult_ac)  
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   129
apply (rename_tac u v w x y z)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   130
apply (subgoal_tac "u*y + x*y = w*y + v*y  &  u*z + x*z = w*z + v*z")
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   131
apply (simp add: mult_ac)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   132
apply (simp add: add_mult_distrib [symmetric])
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   133
done
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   134
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   135
lemma mult:
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   136
     "Abs_Integ((intrel``{(x,y)})) * Abs_Integ((intrel``{(u,v)})) =
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   137
      Abs_Integ(intrel `` {(x*u + y*v, x*v + y*u)})"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   138
by (simp add: mult_int_def UN_UN_split_split_eq mult_congruent2
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   139
              UN_equiv_class2 [OF equiv_intrel equiv_intrel])
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   140
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   141
text{*The integers form a @{text comm_ring_1}*}
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   142
instance int :: comm_ring_1
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   143
proof
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   144
  fix i j k :: int
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   145
  show "(i + j) + k = i + (j + k)"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   146
    by (cases i, cases j, cases k) (simp add: add add_assoc)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   147
  show "i + j = j + i" 
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   148
    by (cases i, cases j) (simp add: add_ac add)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   149
  show "0 + i = i"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   150
    by (cases i) (simp add: Zero_int_def add)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   151
  show "- i + i = 0"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   152
    by (cases i) (simp add: Zero_int_def minus add)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   153
  show "i - j = i + - j"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   154
    by (simp add: diff_int_def)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   155
  show "(i * j) * k = i * (j * k)"
29667
53103fc8ffa3 Replaced group_ and ring_simps by algebra_simps;
nipkow
parents: 29046
diff changeset
   156
    by (cases i, cases j, cases k) (simp add: mult algebra_simps)
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   157
  show "i * j = j * i"
29667
53103fc8ffa3 Replaced group_ and ring_simps by algebra_simps;
nipkow
parents: 29046
diff changeset
   158
    by (cases i, cases j) (simp add: mult algebra_simps)
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   159
  show "1 * i = i"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   160
    by (cases i) (simp add: One_int_def mult)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   161
  show "(i + j) * k = i * k + j * k"
29667
53103fc8ffa3 Replaced group_ and ring_simps by algebra_simps;
nipkow
parents: 29046
diff changeset
   162
    by (cases i, cases j, cases k) (simp add: add mult algebra_simps)
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   163
  show "0 \<noteq> (1::int)"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   164
    by (simp add: Zero_int_def One_int_def)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   165
qed
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   166
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   167
lemma int_def: "of_nat m = Abs_Integ (intrel `` {(m, 0)})"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   168
by (induct m, simp_all add: Zero_int_def One_int_def add)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   169
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   170
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   171
subsection {* The @{text "\<le>"} Ordering *}
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   172
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   173
lemma le:
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   174
  "(Abs_Integ(intrel``{(x,y)}) \<le> Abs_Integ(intrel``{(u,v)})) = (x+v \<le> u+y)"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   175
by (force simp add: le_int_def)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   176
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   177
lemma less:
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   178
  "(Abs_Integ(intrel``{(x,y)}) < Abs_Integ(intrel``{(u,v)})) = (x+v < u+y)"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   179
by (simp add: less_int_def le order_less_le)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   180
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   181
instance int :: linorder
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   182
proof
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   183
  fix i j k :: int
27682
25aceefd4786 added class preorder
haftmann
parents: 27395
diff changeset
   184
  show antisym: "i \<le> j \<Longrightarrow> j \<le> i \<Longrightarrow> i = j"
25aceefd4786 added class preorder
haftmann
parents: 27395
diff changeset
   185
    by (cases i, cases j) (simp add: le)
25aceefd4786 added class preorder
haftmann
parents: 27395
diff changeset
   186
  show "(i < j) = (i \<le> j \<and> \<not> j \<le> i)"
25aceefd4786 added class preorder
haftmann
parents: 27395
diff changeset
   187
    by (auto simp add: less_int_def dest: antisym) 
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   188
  show "i \<le> i"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   189
    by (cases i) (simp add: le)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   190
  show "i \<le> j \<Longrightarrow> j \<le> k \<Longrightarrow> i \<le> k"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   191
    by (cases i, cases j, cases k) (simp add: le)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   192
  show "i \<le> j \<or> j \<le> i"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   193
    by (cases i, cases j) (simp add: le linorder_linear)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   194
qed
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   195
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   196
instantiation int :: distrib_lattice
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   197
begin
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   198
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   199
definition
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   200
  "(inf \<Colon> int \<Rightarrow> int \<Rightarrow> int) = min"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   201
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   202
definition
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   203
  "(sup \<Colon> int \<Rightarrow> int \<Rightarrow> int) = max"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   204
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   205
instance
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   206
  by intro_classes
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   207
    (auto simp add: inf_int_def sup_int_def min_max.sup_inf_distrib1)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   208
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   209
end
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   210
35028
108662d50512 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34055
diff changeset
   211
instance int :: ordered_cancel_ab_semigroup_add
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   212
proof
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   213
  fix i j k :: int
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   214
  show "i \<le> j \<Longrightarrow> k + i \<le> k + j"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   215
    by (cases i, cases j, cases k) (simp add: le add)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   216
qed
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   217
25961
ec39d7e40554 moved definition of power on ints to theory Int
haftmann
parents: 25928
diff changeset
   218
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   219
text{*Strict Monotonicity of Multiplication*}
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   220
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   221
text{*strict, in 1st argument; proof is by induction on k>0*}
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   222
lemma zmult_zless_mono2_lemma:
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   223
     "(i::int)<j ==> 0<k ==> of_nat k * i < of_nat k * j"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   224
apply (induct "k", simp)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   225
apply (simp add: left_distrib)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   226
apply (case_tac "k=0")
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   227
apply (simp_all add: add_strict_mono)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   228
done
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   229
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   230
lemma zero_le_imp_eq_int: "(0::int) \<le> k ==> \<exists>n. k = of_nat n"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   231
apply (cases k)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   232
apply (auto simp add: le add int_def Zero_int_def)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   233
apply (rule_tac x="x-y" in exI, simp)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   234
done
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   235
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   236
lemma zero_less_imp_eq_int: "(0::int) < k ==> \<exists>n>0. k = of_nat n"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   237
apply (cases k)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   238
apply (simp add: less int_def Zero_int_def)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   239
apply (rule_tac x="x-y" in exI, simp)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   240
done
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   241
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   242
lemma zmult_zless_mono2: "[| i<j;  (0::int) < k |] ==> k*i < k*j"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   243
apply (drule zero_less_imp_eq_int)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   244
apply (auto simp add: zmult_zless_mono2_lemma)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   245
done
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   246
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   247
text{*The integers form an ordered integral domain*}
35028
108662d50512 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34055
diff changeset
   248
instance int :: linordered_idom
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   249
proof
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   250
  fix i j k :: int
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   251
  show "i < j \<Longrightarrow> 0 < k \<Longrightarrow> k * i < k * j"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   252
    by (rule zmult_zless_mono2)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   253
  show "\<bar>i\<bar> = (if i < 0 then -i else i)"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   254
    by (simp only: zabs_def)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   255
  show "sgn (i\<Colon>int) = (if i=0 then 0 else if 0<i then 1 else - 1)"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   256
    by (simp only: zsgn_def)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   257
qed
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   258
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   259
lemma zless_imp_add1_zle: "w < z \<Longrightarrow> w + (1\<Colon>int) \<le> z"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   260
apply (cases w, cases z) 
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   261
apply (simp add: less le add One_int_def)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   262
done
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   263
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   264
lemma zless_iff_Suc_zadd:
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   265
  "(w \<Colon> int) < z \<longleftrightarrow> (\<exists>n. z = w + of_nat (Suc n))"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   266
apply (cases z, cases w)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   267
apply (auto simp add: less add int_def)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   268
apply (rename_tac a b c d) 
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   269
apply (rule_tac x="a+d - Suc(c+b)" in exI) 
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   270
apply arith
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   271
done
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   272
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   273
lemmas int_distrib =
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   274
  left_distrib [of "z1::int" "z2" "w", standard]
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   275
  right_distrib [of "w::int" "z1" "z2", standard]
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   276
  left_diff_distrib [of "z1::int" "z2" "w", standard]
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   277
  right_diff_distrib [of "w::int" "z1" "z2", standard]
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   278
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   279
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   280
subsection {* Embedding of the Integers into any @{text ring_1}: @{text of_int}*}
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   281
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   282
context ring_1
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   283
begin
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   284
31015
555f4033cd97 reorganization of power lemmas
haftmann
parents: 31010
diff changeset
   285
definition of_int :: "int \<Rightarrow> 'a" where
28562
4e74209f113e `code func` now just `code`
haftmann
parents: 28537
diff changeset
   286
  [code del]: "of_int z = contents (\<Union>(i, j) \<in> Rep_Integ z. { of_nat i - of_nat j })"
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   287
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   288
lemma of_int: "of_int (Abs_Integ (intrel `` {(i,j)})) = of_nat i - of_nat j"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   289
proof -
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   290
  have "(\<lambda>(i,j). { of_nat i - (of_nat j :: 'a) }) respects intrel"
29667
53103fc8ffa3 Replaced group_ and ring_simps by algebra_simps;
nipkow
parents: 29046
diff changeset
   291
    by (simp add: congruent_def algebra_simps of_nat_add [symmetric]
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   292
            del: of_nat_add) 
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   293
  thus ?thesis
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   294
    by (simp add: of_int_def UN_equiv_class [OF equiv_intrel])
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   295
qed
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   296
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   297
lemma of_int_0 [simp]: "of_int 0 = 0"
29667
53103fc8ffa3 Replaced group_ and ring_simps by algebra_simps;
nipkow
parents: 29046
diff changeset
   298
by (simp add: of_int Zero_int_def)
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   299
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   300
lemma of_int_1 [simp]: "of_int 1 = 1"
29667
53103fc8ffa3 Replaced group_ and ring_simps by algebra_simps;
nipkow
parents: 29046
diff changeset
   301
by (simp add: of_int One_int_def)
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   302
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   303
lemma of_int_add [simp]: "of_int (w+z) = of_int w + of_int z"
29667
53103fc8ffa3 Replaced group_ and ring_simps by algebra_simps;
nipkow
parents: 29046
diff changeset
   304
by (cases w, cases z, simp add: algebra_simps of_int add)
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   305
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   306
lemma of_int_minus [simp]: "of_int (-z) = - (of_int z)"
29667
53103fc8ffa3 Replaced group_ and ring_simps by algebra_simps;
nipkow
parents: 29046
diff changeset
   307
by (cases z, simp add: algebra_simps of_int minus)
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   308
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   309
lemma of_int_diff [simp]: "of_int (w - z) = of_int w - of_int z"
35050
9f841f20dca6 renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents: 35032
diff changeset
   310
by (simp add: diff_minus Groups.diff_minus)
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   311
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   312
lemma of_int_mult [simp]: "of_int (w*z) = of_int w * of_int z"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   313
apply (cases w, cases z)
29667
53103fc8ffa3 Replaced group_ and ring_simps by algebra_simps;
nipkow
parents: 29046
diff changeset
   314
apply (simp add: algebra_simps of_int mult of_nat_mult)
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   315
done
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   316
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   317
text{*Collapse nested embeddings*}
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   318
lemma of_int_of_nat_eq [simp]: "of_int (of_nat n) = of_nat n"
29667
53103fc8ffa3 Replaced group_ and ring_simps by algebra_simps;
nipkow
parents: 29046
diff changeset
   319
by (induct n) auto
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   320
31015
555f4033cd97 reorganization of power lemmas
haftmann
parents: 31010
diff changeset
   321
lemma of_int_power:
555f4033cd97 reorganization of power lemmas
haftmann
parents: 31010
diff changeset
   322
  "of_int (z ^ n) = of_int z ^ n"
555f4033cd97 reorganization of power lemmas
haftmann
parents: 31010
diff changeset
   323
  by (induct n) simp_all
555f4033cd97 reorganization of power lemmas
haftmann
parents: 31010
diff changeset
   324
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   325
end
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   326
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   327
text{*Class for unital rings with characteristic zero.
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   328
 Includes non-ordered rings like the complex numbers.*}
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   329
class ring_char_0 = ring_1 + semiring_char_0
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   330
begin
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   331
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   332
lemma of_int_eq_iff [simp]:
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   333
   "of_int w = of_int z \<longleftrightarrow> w = z"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   334
apply (cases w, cases z, simp add: of_int)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   335
apply (simp only: diff_eq_eq diff_add_eq eq_diff_eq)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   336
apply (simp only: of_nat_add [symmetric] of_nat_eq_iff)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   337
done
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   338
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   339
text{*Special cases where either operand is zero*}
36424
f3f389fc7974 got rid of [simplified]
haftmann
parents: 36409
diff changeset
   340
lemma of_int_eq_0_iff [simp]:
f3f389fc7974 got rid of [simplified]
haftmann
parents: 36409
diff changeset
   341
  "of_int z = 0 \<longleftrightarrow> z = 0"
f3f389fc7974 got rid of [simplified]
haftmann
parents: 36409
diff changeset
   342
  using of_int_eq_iff [of z 0] by simp
f3f389fc7974 got rid of [simplified]
haftmann
parents: 36409
diff changeset
   343
f3f389fc7974 got rid of [simplified]
haftmann
parents: 36409
diff changeset
   344
lemma of_int_0_eq_iff [simp]:
f3f389fc7974 got rid of [simplified]
haftmann
parents: 36409
diff changeset
   345
  "0 = of_int z \<longleftrightarrow> z = 0"
f3f389fc7974 got rid of [simplified]
haftmann
parents: 36409
diff changeset
   346
  using of_int_eq_iff [of 0 z] by simp
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   347
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   348
end
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   349
36424
f3f389fc7974 got rid of [simplified]
haftmann
parents: 36409
diff changeset
   350
context linordered_idom
f3f389fc7974 got rid of [simplified]
haftmann
parents: 36409
diff changeset
   351
begin
f3f389fc7974 got rid of [simplified]
haftmann
parents: 36409
diff changeset
   352
35028
108662d50512 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34055
diff changeset
   353
text{*Every @{text linordered_idom} has characteristic zero.*}
36424
f3f389fc7974 got rid of [simplified]
haftmann
parents: 36409
diff changeset
   354
subclass ring_char_0 ..
f3f389fc7974 got rid of [simplified]
haftmann
parents: 36409
diff changeset
   355
f3f389fc7974 got rid of [simplified]
haftmann
parents: 36409
diff changeset
   356
lemma of_int_le_iff [simp]:
f3f389fc7974 got rid of [simplified]
haftmann
parents: 36409
diff changeset
   357
  "of_int w \<le> of_int z \<longleftrightarrow> w \<le> z"
f3f389fc7974 got rid of [simplified]
haftmann
parents: 36409
diff changeset
   358
  by (cases w, cases z, simp add: of_int le minus algebra_simps of_nat_add [symmetric] del: of_nat_add)
f3f389fc7974 got rid of [simplified]
haftmann
parents: 36409
diff changeset
   359
f3f389fc7974 got rid of [simplified]
haftmann
parents: 36409
diff changeset
   360
lemma of_int_less_iff [simp]:
f3f389fc7974 got rid of [simplified]
haftmann
parents: 36409
diff changeset
   361
  "of_int w < of_int z \<longleftrightarrow> w < z"
f3f389fc7974 got rid of [simplified]
haftmann
parents: 36409
diff changeset
   362
  by (simp add: less_le order_less_le)
f3f389fc7974 got rid of [simplified]
haftmann
parents: 36409
diff changeset
   363
f3f389fc7974 got rid of [simplified]
haftmann
parents: 36409
diff changeset
   364
lemma of_int_0_le_iff [simp]:
f3f389fc7974 got rid of [simplified]
haftmann
parents: 36409
diff changeset
   365
  "0 \<le> of_int z \<longleftrightarrow> 0 \<le> z"
f3f389fc7974 got rid of [simplified]
haftmann
parents: 36409
diff changeset
   366
  using of_int_le_iff [of 0 z] by simp
f3f389fc7974 got rid of [simplified]
haftmann
parents: 36409
diff changeset
   367
f3f389fc7974 got rid of [simplified]
haftmann
parents: 36409
diff changeset
   368
lemma of_int_le_0_iff [simp]:
f3f389fc7974 got rid of [simplified]
haftmann
parents: 36409
diff changeset
   369
  "of_int z \<le> 0 \<longleftrightarrow> z \<le> 0"
f3f389fc7974 got rid of [simplified]
haftmann
parents: 36409
diff changeset
   370
  using of_int_le_iff [of z 0] by simp
f3f389fc7974 got rid of [simplified]
haftmann
parents: 36409
diff changeset
   371
f3f389fc7974 got rid of [simplified]
haftmann
parents: 36409
diff changeset
   372
lemma of_int_0_less_iff [simp]:
f3f389fc7974 got rid of [simplified]
haftmann
parents: 36409
diff changeset
   373
  "0 < of_int z \<longleftrightarrow> 0 < z"
f3f389fc7974 got rid of [simplified]
haftmann
parents: 36409
diff changeset
   374
  using of_int_less_iff [of 0 z] by simp
f3f389fc7974 got rid of [simplified]
haftmann
parents: 36409
diff changeset
   375
f3f389fc7974 got rid of [simplified]
haftmann
parents: 36409
diff changeset
   376
lemma of_int_less_0_iff [simp]:
f3f389fc7974 got rid of [simplified]
haftmann
parents: 36409
diff changeset
   377
  "of_int z < 0 \<longleftrightarrow> z < 0"
f3f389fc7974 got rid of [simplified]
haftmann
parents: 36409
diff changeset
   378
  using of_int_less_iff [of z 0] by simp
f3f389fc7974 got rid of [simplified]
haftmann
parents: 36409
diff changeset
   379
f3f389fc7974 got rid of [simplified]
haftmann
parents: 36409
diff changeset
   380
end
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   381
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   382
lemma of_int_eq_id [simp]: "of_int = id"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   383
proof
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   384
  fix z show "of_int z = id z"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   385
    by (cases z) (simp add: of_int add minus int_def diff_minus)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   386
qed
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   387
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   388
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   389
subsection {* Magnitude of an Integer, as a Natural Number: @{text nat} *}
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   390
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   391
definition
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   392
  nat :: "int \<Rightarrow> nat"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   393
where
28562
4e74209f113e `code func` now just `code`
haftmann
parents: 28537
diff changeset
   394
  [code del]: "nat z = contents (\<Union>(x, y) \<in> Rep_Integ z. {x-y})"
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   395
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   396
lemma nat: "nat (Abs_Integ (intrel``{(x,y)})) = x-y"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   397
proof -
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   398
  have "(\<lambda>(x,y). {x-y}) respects intrel"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   399
    by (simp add: congruent_def) arith
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   400
  thus ?thesis
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   401
    by (simp add: nat_def UN_equiv_class [OF equiv_intrel])
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   402
qed
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   403
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   404
lemma nat_int [simp]: "nat (of_nat n) = n"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   405
by (simp add: nat int_def)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   406
35216
7641e8d831d2 get rid of many duplicate simp rule warnings
huffman
parents: 35123
diff changeset
   407
(* FIXME: duplicates nat_0 *)
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   408
lemma nat_zero [simp]: "nat 0 = 0"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   409
by (simp add: Zero_int_def nat)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   410
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   411
lemma int_nat_eq [simp]: "of_nat (nat z) = (if 0 \<le> z then z else 0)"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   412
by (cases z, simp add: nat le int_def Zero_int_def)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   413
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   414
corollary nat_0_le: "0 \<le> z ==> of_nat (nat z) = z"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   415
by simp
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   416
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   417
lemma nat_le_0 [simp]: "z \<le> 0 ==> nat z = 0"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   418
by (cases z, simp add: nat le Zero_int_def)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   419
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   420
lemma nat_le_eq_zle: "0 < w | 0 \<le> z ==> (nat w \<le> nat z) = (w\<le>z)"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   421
apply (cases w, cases z) 
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   422
apply (simp add: nat le linorder_not_le [symmetric] Zero_int_def, arith)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   423
done
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   424
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   425
text{*An alternative condition is @{term "0 \<le> w"} *}
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   426
corollary nat_mono_iff: "0 < z ==> (nat w < nat z) = (w < z)"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   427
by (simp add: nat_le_eq_zle linorder_not_le [symmetric]) 
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   428
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   429
corollary nat_less_eq_zless: "0 \<le> w ==> (nat w < nat z) = (w<z)"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   430
by (simp add: nat_le_eq_zle linorder_not_le [symmetric]) 
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   431
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   432
lemma zless_nat_conj [simp]: "(nat w < nat z) = (0 < z & w < z)"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   433
apply (cases w, cases z) 
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   434
apply (simp add: nat le Zero_int_def linorder_not_le [symmetric], arith)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   435
done
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   436
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   437
lemma nonneg_eq_int:
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   438
  fixes z :: int
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   439
  assumes "0 \<le> z" and "\<And>m. z = of_nat m \<Longrightarrow> P"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   440
  shows P
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   441
  using assms by (blast dest: nat_0_le sym)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   442
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   443
lemma nat_eq_iff: "(nat w = m) = (if 0 \<le> w then w = of_nat m else m=0)"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   444
by (cases w, simp add: nat le int_def Zero_int_def, arith)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   445
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   446
corollary nat_eq_iff2: "(m = nat w) = (if 0 \<le> w then w = of_nat m else m=0)"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   447
by (simp only: eq_commute [of m] nat_eq_iff)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   448
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   449
lemma nat_less_iff: "0 \<le> w ==> (nat w < m) = (w < of_nat m)"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   450
apply (cases w)
29700
22faf21db3df added some simp rules
nipkow
parents: 29668
diff changeset
   451
apply (simp add: nat le int_def Zero_int_def linorder_not_le[symmetric], arith)
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   452
done
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   453
29700
22faf21db3df added some simp rules
nipkow
parents: 29668
diff changeset
   454
lemma nat_0_iff[simp]: "nat(i::int) = 0 \<longleftrightarrow> i\<le>0"
22faf21db3df added some simp rules
nipkow
parents: 29668
diff changeset
   455
by(simp add: nat_eq_iff) arith
22faf21db3df added some simp rules
nipkow
parents: 29668
diff changeset
   456
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   457
lemma int_eq_iff: "(of_nat m = z) = (m = nat z & 0 \<le> z)"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   458
by (auto simp add: nat_eq_iff2)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   459
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   460
lemma zero_less_nat_eq [simp]: "(0 < nat z) = (0 < z)"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   461
by (insert zless_nat_conj [of 0], auto)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   462
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   463
lemma nat_add_distrib:
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   464
     "[| (0::int) \<le> z;  0 \<le> z' |] ==> nat (z+z') = nat z + nat z'"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   465
by (cases z, cases z', simp add: nat add le Zero_int_def)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   466
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   467
lemma nat_diff_distrib:
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   468
     "[| (0::int) \<le> z';  z' \<le> z |] ==> nat (z-z') = nat z - nat z'"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   469
by (cases z, cases z', 
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   470
    simp add: nat add minus diff_minus le Zero_int_def)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   471
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   472
lemma nat_zminus_int [simp]: "nat (- (of_nat n)) = 0"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   473
by (simp add: int_def minus nat Zero_int_def) 
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   474
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   475
lemma zless_nat_eq_int_zless: "(m < nat z) = (of_nat m < z)"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   476
by (cases z, simp add: nat less int_def, arith)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   477
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   478
context ring_1
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   479
begin
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   480
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   481
lemma of_nat_nat: "0 \<le> z \<Longrightarrow> of_nat (nat z) = of_int z"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   482
  by (cases z rule: eq_Abs_Integ)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   483
   (simp add: nat le of_int Zero_int_def of_nat_diff)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   484
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   485
end
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   486
29779
2786b348c376 declare "nat o abs" as default measure for int
krauss
parents: 29700
diff changeset
   487
text {* For termination proofs: *}
2786b348c376 declare "nat o abs" as default measure for int
krauss
parents: 29700
diff changeset
   488
lemma measure_function_int[measure_function]: "is_measure (nat o abs)" ..
2786b348c376 declare "nat o abs" as default measure for int
krauss
parents: 29700
diff changeset
   489
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   490
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   491
subsection{*Lemmas about the Function @{term of_nat} and Orderings*}
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   492
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   493
lemma negative_zless_0: "- (of_nat (Suc n)) < (0 \<Colon> int)"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   494
by (simp add: order_less_le del: of_nat_Suc)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   495
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   496
lemma negative_zless [iff]: "- (of_nat (Suc n)) < (of_nat m \<Colon> int)"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   497
by (rule negative_zless_0 [THEN order_less_le_trans], simp)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   498
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   499
lemma negative_zle_0: "- of_nat n \<le> (0 \<Colon> int)"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   500
by (simp add: minus_le_iff)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   501
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   502
lemma negative_zle [iff]: "- of_nat n \<le> (of_nat m \<Colon> int)"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   503
by (rule order_trans [OF negative_zle_0 of_nat_0_le_iff])
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   504
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   505
lemma not_zle_0_negative [simp]: "~ (0 \<le> - (of_nat (Suc n) \<Colon> int))"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   506
by (subst le_minus_iff, simp del: of_nat_Suc)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   507
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   508
lemma int_zle_neg: "((of_nat n \<Colon> int) \<le> - of_nat m) = (n = 0 & m = 0)"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   509
by (simp add: int_def le minus Zero_int_def)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   510
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   511
lemma not_int_zless_negative [simp]: "~ ((of_nat n \<Colon> int) < - of_nat m)"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   512
by (simp add: linorder_not_less)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   513
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   514
lemma negative_eq_positive [simp]: "((- of_nat n \<Colon> int) = of_nat m) = (n = 0 & m = 0)"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   515
by (force simp add: order_eq_iff [of "- of_nat n"] int_zle_neg)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   516
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   517
lemma zle_iff_zadd: "(w\<Colon>int) \<le> z \<longleftrightarrow> (\<exists>n. z = w + of_nat n)"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   518
proof -
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   519
  have "(w \<le> z) = (0 \<le> z - w)"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   520
    by (simp only: le_diff_eq add_0_left)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   521
  also have "\<dots> = (\<exists>n. z - w = of_nat n)"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   522
    by (auto elim: zero_le_imp_eq_int)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   523
  also have "\<dots> = (\<exists>n. z = w + of_nat n)"
29667
53103fc8ffa3 Replaced group_ and ring_simps by algebra_simps;
nipkow
parents: 29046
diff changeset
   524
    by (simp only: algebra_simps)
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   525
  finally show ?thesis .
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   526
qed
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   527
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   528
lemma zadd_int_left: "of_nat m + (of_nat n + z) = of_nat (m + n) + (z\<Colon>int)"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   529
by simp
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   530
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   531
lemma int_Suc0_eq_1: "of_nat (Suc 0) = (1\<Colon>int)"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   532
by simp
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   533
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   534
text{*This version is proved for all ordered rings, not just integers!
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   535
      It is proved here because attribute @{text arith_split} is not available
35050
9f841f20dca6 renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents: 35032
diff changeset
   536
      in theory @{text Rings}.
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   537
      But is it really better than just rewriting with @{text abs_if}?*}
35828
46cfc4b8112e now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents: 35634
diff changeset
   538
lemma abs_split [arith_split,no_atp]:
35028
108662d50512 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34055
diff changeset
   539
     "P(abs(a::'a::linordered_idom)) = ((0 \<le> a --> P a) & (a < 0 --> P(-a)))"
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   540
by (force dest: order_less_le_trans simp add: abs_if linorder_not_less)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   541
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   542
lemma negD: "(x \<Colon> int) < 0 \<Longrightarrow> \<exists>n. x = - (of_nat (Suc n))"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   543
apply (cases x)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   544
apply (auto simp add: le minus Zero_int_def int_def order_less_le)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   545
apply (rule_tac x="y - Suc x" in exI, arith)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   546
done
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   547
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   548
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   549
subsection {* Cases and induction *}
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   550
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   551
text{*Now we replace the case analysis rule by a more conventional one:
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   552
whether an integer is negative or not.*}
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   553
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   554
theorem int_cases [cases type: int, case_names nonneg neg]:
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   555
  "[|!! n. (z \<Colon> int) = of_nat n ==> P;  !! n. z =  - (of_nat (Suc n)) ==> P |] ==> P"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   556
apply (cases "z < 0", blast dest!: negD)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   557
apply (simp add: linorder_not_less del: of_nat_Suc)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   558
apply auto
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   559
apply (blast dest: nat_0_le [THEN sym])
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   560
done
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   561
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   562
theorem int_induct [induct type: int, case_names nonneg neg]:
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   563
     "[|!! n. P (of_nat n \<Colon> int);  !!n. P (- (of_nat (Suc n))) |] ==> P z"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   564
  by (cases z rule: int_cases) auto
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   565
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   566
text{*Contributed by Brian Huffman*}
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   567
theorem int_diff_cases:
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   568
  obtains (diff) m n where "(z\<Colon>int) = of_nat m - of_nat n"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   569
apply (cases z rule: eq_Abs_Integ)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   570
apply (rule_tac m=x and n=y in diff)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   571
apply (simp add: int_def diff_def minus add)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   572
done
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   573
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   574
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   575
subsection {* Binary representation *}
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   576
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   577
text {*
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   578
  This formalization defines binary arithmetic in terms of the integers
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   579
  rather than using a datatype. This avoids multiple representations (leading
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   580
  zeroes, etc.)  See @{text "ZF/Tools/twos-compl.ML"}, function @{text
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   581
  int_of_binary}, for the numerical interpretation.
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   582
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   583
  The representation expects that @{text "(m mod 2)"} is 0 or 1,
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   584
  even if m is negative;
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   585
  For instance, @{text "-5 div 2 = -3"} and @{text "-5 mod 2 = 1"}; thus
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   586
  @{text "-5 = (-3)*2 + 1"}.
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   587
  
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   588
  This two's complement binary representation derives from the paper 
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   589
  "An Efficient Representation of Arithmetic for Term Rewriting" by
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   590
  Dave Cohen and Phil Watson, Rewriting Techniques and Applications,
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   591
  Springer LNCS 488 (240-251), 1991.
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   592
*}
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   593
28958
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   594
subsubsection {* The constructors @{term Bit0}, @{term Bit1}, @{term Pls} and @{term Min} *}
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   595
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   596
definition
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   597
  Pls :: int where
28562
4e74209f113e `code func` now just `code`
haftmann
parents: 28537
diff changeset
   598
  [code del]: "Pls = 0"
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   599
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   600
definition
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   601
  Min :: int where
28562
4e74209f113e `code func` now just `code`
haftmann
parents: 28537
diff changeset
   602
  [code del]: "Min = - 1"
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   603
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   604
definition
26086
3c243098b64a New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents: 26075
diff changeset
   605
  Bit0 :: "int \<Rightarrow> int" where
28562
4e74209f113e `code func` now just `code`
haftmann
parents: 28537
diff changeset
   606
  [code del]: "Bit0 k = k + k"
26086
3c243098b64a New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents: 26075
diff changeset
   607
3c243098b64a New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents: 26075
diff changeset
   608
definition
3c243098b64a New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents: 26075
diff changeset
   609
  Bit1 :: "int \<Rightarrow> int" where
28562
4e74209f113e `code func` now just `code`
haftmann
parents: 28537
diff changeset
   610
  [code del]: "Bit1 k = 1 + k + k"
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   611
29608
564ea783ace8 no base sort in class import
haftmann
parents: 29046
diff changeset
   612
class number = -- {* for numeric types: nat, int, real, \dots *}
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   613
  fixes number_of :: "int \<Rightarrow> 'a"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   614
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   615
use "Tools/numeral.ML"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   616
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   617
syntax
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   618
  "_Numeral" :: "num_const \<Rightarrow> 'a"    ("_")
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   619
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   620
use "Tools/numeral_syntax.ML"
35123
e286d5df187a modernized structures;
wenzelm
parents: 35050
diff changeset
   621
setup Numeral_Syntax.setup
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   622
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   623
abbreviation
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   624
  "Numeral0 \<equiv> number_of Pls"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   625
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   626
abbreviation
26086
3c243098b64a New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents: 26075
diff changeset
   627
  "Numeral1 \<equiv> number_of (Bit1 Pls)"
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   628
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   629
lemma Let_number_of [simp]: "Let (number_of v) f = f (number_of v)"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   630
  -- {* Unfold all @{text let}s involving constants *}
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   631
  unfolding Let_def ..
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   632
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   633
definition
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   634
  succ :: "int \<Rightarrow> int" where
28562
4e74209f113e `code func` now just `code`
haftmann
parents: 28537
diff changeset
   635
  [code del]: "succ k = k + 1"
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   636
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   637
definition
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   638
  pred :: "int \<Rightarrow> int" where
28562
4e74209f113e `code func` now just `code`
haftmann
parents: 28537
diff changeset
   639
  [code del]: "pred k = k - 1"
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   640
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   641
lemmas
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   642
  max_number_of [simp] = max_def
35216
7641e8d831d2 get rid of many duplicate simp rule warnings
huffman
parents: 35123
diff changeset
   643
    [of "number_of u" "number_of v", standard]
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   644
and
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   645
  min_number_of [simp] = min_def 
35216
7641e8d831d2 get rid of many duplicate simp rule warnings
huffman
parents: 35123
diff changeset
   646
    [of "number_of u" "number_of v", standard]
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   647
  -- {* unfolding @{text minx} and @{text max} on numerals *}
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   648
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   649
lemmas numeral_simps = 
26086
3c243098b64a New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents: 26075
diff changeset
   650
  succ_def pred_def Pls_def Min_def Bit0_def Bit1_def
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   651
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   652
text {* Removal of leading zeroes *}
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   653
31998
2c7a24f74db9 code attributes use common underscore convention
haftmann
parents: 31100
diff changeset
   654
lemma Bit0_Pls [simp, code_post]:
26086
3c243098b64a New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents: 26075
diff changeset
   655
  "Bit0 Pls = Pls"
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   656
  unfolding numeral_simps by simp
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   657
31998
2c7a24f74db9 code attributes use common underscore convention
haftmann
parents: 31100
diff changeset
   658
lemma Bit1_Min [simp, code_post]:
26086
3c243098b64a New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents: 26075
diff changeset
   659
  "Bit1 Min = Min"
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   660
  unfolding numeral_simps by simp
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   661
26075
815f3ccc0b45 added lemma lists {normalize,succ,pred,minus,add,mult}_bin_simps
huffman
parents: 26072
diff changeset
   662
lemmas normalize_bin_simps =
26086
3c243098b64a New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents: 26075
diff changeset
   663
  Bit0_Pls Bit1_Min
26075
815f3ccc0b45 added lemma lists {normalize,succ,pred,minus,add,mult}_bin_simps
huffman
parents: 26072
diff changeset
   664
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   665
28958
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   666
subsubsection {* Successor and predecessor functions *}
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   667
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   668
text {* Successor *}
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   669
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   670
lemma succ_Pls:
26086
3c243098b64a New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents: 26075
diff changeset
   671
  "succ Pls = Bit1 Pls"
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   672
  unfolding numeral_simps by simp
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   673
28958
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   674
lemma succ_Min:
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   675
  "succ Min = Pls"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   676
  unfolding numeral_simps by simp
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   677
28958
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   678
lemma succ_Bit0:
26086
3c243098b64a New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents: 26075
diff changeset
   679
  "succ (Bit0 k) = Bit1 k"
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   680
  unfolding numeral_simps by simp
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   681
28958
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   682
lemma succ_Bit1:
26086
3c243098b64a New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents: 26075
diff changeset
   683
  "succ (Bit1 k) = Bit0 (succ k)"
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   684
  unfolding numeral_simps by simp
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   685
28958
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   686
lemmas succ_bin_simps [simp] =
26086
3c243098b64a New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents: 26075
diff changeset
   687
  succ_Pls succ_Min succ_Bit0 succ_Bit1
26075
815f3ccc0b45 added lemma lists {normalize,succ,pred,minus,add,mult}_bin_simps
huffman
parents: 26072
diff changeset
   688
28958
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   689
text {* Predecessor *}
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   690
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   691
lemma pred_Pls:
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   692
  "pred Pls = Min"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   693
  unfolding numeral_simps by simp
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   694
28958
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   695
lemma pred_Min:
26086
3c243098b64a New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents: 26075
diff changeset
   696
  "pred Min = Bit0 Min"
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   697
  unfolding numeral_simps by simp
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   698
28958
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   699
lemma pred_Bit0:
26086
3c243098b64a New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents: 26075
diff changeset
   700
  "pred (Bit0 k) = Bit1 (pred k)"
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   701
  unfolding numeral_simps by simp 
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   702
28958
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   703
lemma pred_Bit1:
26086
3c243098b64a New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents: 26075
diff changeset
   704
  "pred (Bit1 k) = Bit0 k"
3c243098b64a New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents: 26075
diff changeset
   705
  unfolding numeral_simps by simp
3c243098b64a New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents: 26075
diff changeset
   706
28958
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   707
lemmas pred_bin_simps [simp] =
26086
3c243098b64a New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents: 26075
diff changeset
   708
  pred_Pls pred_Min pred_Bit0 pred_Bit1
26075
815f3ccc0b45 added lemma lists {normalize,succ,pred,minus,add,mult}_bin_simps
huffman
parents: 26072
diff changeset
   709
28958
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   710
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   711
subsubsection {* Binary arithmetic *}
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   712
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   713
text {* Addition *}
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   714
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   715
lemma add_Pls:
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   716
  "Pls + k = k"
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   717
  unfolding numeral_simps by simp
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   718
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   719
lemma add_Min:
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   720
  "Min + k = pred k"
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   721
  unfolding numeral_simps by simp
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   722
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   723
lemma add_Bit0_Bit0:
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   724
  "(Bit0 k) + (Bit0 l) = Bit0 (k + l)"
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   725
  unfolding numeral_simps by simp
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   726
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   727
lemma add_Bit0_Bit1:
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   728
  "(Bit0 k) + (Bit1 l) = Bit1 (k + l)"
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   729
  unfolding numeral_simps by simp
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   730
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   731
lemma add_Bit1_Bit0:
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   732
  "(Bit1 k) + (Bit0 l) = Bit1 (k + l)"
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   733
  unfolding numeral_simps by simp
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   734
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   735
lemma add_Bit1_Bit1:
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   736
  "(Bit1 k) + (Bit1 l) = Bit0 (k + succ l)"
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   737
  unfolding numeral_simps by simp
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   738
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   739
lemma add_Pls_right:
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   740
  "k + Pls = k"
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   741
  unfolding numeral_simps by simp
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   742
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   743
lemma add_Min_right:
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   744
  "k + Min = pred k"
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   745
  unfolding numeral_simps by simp
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   746
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   747
lemmas add_bin_simps [simp] =
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   748
  add_Pls add_Min add_Pls_right add_Min_right
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   749
  add_Bit0_Bit0 add_Bit0_Bit1 add_Bit1_Bit0 add_Bit1_Bit1
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   750
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   751
text {* Negation *}
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   752
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   753
lemma minus_Pls:
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   754
  "- Pls = Pls"
28958
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   755
  unfolding numeral_simps by simp
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   756
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   757
lemma minus_Min:
26086
3c243098b64a New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents: 26075
diff changeset
   758
  "- Min = Bit1 Pls"
28958
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   759
  unfolding numeral_simps by simp
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   760
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   761
lemma minus_Bit0:
26086
3c243098b64a New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents: 26075
diff changeset
   762
  "- (Bit0 k) = Bit0 (- k)"
28958
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   763
  unfolding numeral_simps by simp
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   764
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   765
lemma minus_Bit1:
26086
3c243098b64a New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents: 26075
diff changeset
   766
  "- (Bit1 k) = Bit1 (pred (- k))"
3c243098b64a New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents: 26075
diff changeset
   767
  unfolding numeral_simps by simp
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   768
28958
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   769
lemmas minus_bin_simps [simp] =
26086
3c243098b64a New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents: 26075
diff changeset
   770
  minus_Pls minus_Min minus_Bit0 minus_Bit1
26075
815f3ccc0b45 added lemma lists {normalize,succ,pred,minus,add,mult}_bin_simps
huffman
parents: 26072
diff changeset
   771
28958
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   772
text {* Subtraction *}
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   773
29046
773098b76201 clean up diff_bin_simps
huffman
parents: 29040
diff changeset
   774
lemma diff_bin_simps [simp]:
773098b76201 clean up diff_bin_simps
huffman
parents: 29040
diff changeset
   775
  "k - Pls = k"
773098b76201 clean up diff_bin_simps
huffman
parents: 29040
diff changeset
   776
  "k - Min = succ k"
773098b76201 clean up diff_bin_simps
huffman
parents: 29040
diff changeset
   777
  "Pls - (Bit0 l) = Bit0 (Pls - l)"
773098b76201 clean up diff_bin_simps
huffman
parents: 29040
diff changeset
   778
  "Pls - (Bit1 l) = Bit1 (Min - l)"
773098b76201 clean up diff_bin_simps
huffman
parents: 29040
diff changeset
   779
  "Min - (Bit0 l) = Bit1 (Min - l)"
773098b76201 clean up diff_bin_simps
huffman
parents: 29040
diff changeset
   780
  "Min - (Bit1 l) = Bit0 (Min - l)"
28958
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   781
  "(Bit0 k) - (Bit0 l) = Bit0 (k - l)"
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   782
  "(Bit0 k) - (Bit1 l) = Bit1 (pred k - l)"
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   783
  "(Bit1 k) - (Bit0 l) = Bit1 (k - l)"
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   784
  "(Bit1 k) - (Bit1 l) = Bit0 (k - l)"
29046
773098b76201 clean up diff_bin_simps
huffman
parents: 29040
diff changeset
   785
  unfolding numeral_simps by simp_all
28958
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   786
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   787
text {* Multiplication *}
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   788
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   789
lemma mult_Pls:
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   790
  "Pls * w = Pls"
26086
3c243098b64a New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents: 26075
diff changeset
   791
  unfolding numeral_simps by simp
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   792
28958
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   793
lemma mult_Min:
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   794
  "Min * k = - k"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   795
  unfolding numeral_simps by simp
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   796
28958
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   797
lemma mult_Bit0:
26086
3c243098b64a New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents: 26075
diff changeset
   798
  "(Bit0 k) * l = Bit0 (k * l)"
3c243098b64a New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents: 26075
diff changeset
   799
  unfolding numeral_simps int_distrib by simp
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   800
28958
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   801
lemma mult_Bit1:
26086
3c243098b64a New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents: 26075
diff changeset
   802
  "(Bit1 k) * l = (Bit0 (k * l)) + l"
28958
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   803
  unfolding numeral_simps int_distrib by simp
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   804
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   805
lemmas mult_bin_simps [simp] =
26086
3c243098b64a New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents: 26075
diff changeset
   806
  mult_Pls mult_Min mult_Bit0 mult_Bit1
26075
815f3ccc0b45 added lemma lists {normalize,succ,pred,minus,add,mult}_bin_simps
huffman
parents: 26072
diff changeset
   807
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   808
28958
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   809
subsubsection {* Binary comparisons *}
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   810
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   811
text {* Preliminaries *}
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   812
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   813
lemma even_less_0_iff:
35028
108662d50512 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34055
diff changeset
   814
  "a + a < 0 \<longleftrightarrow> a < (0::'a::linordered_idom)"
28958
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   815
proof -
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   816
  have "a + a < 0 \<longleftrightarrow> (1+1)*a < 0" by (simp add: left_distrib)
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   817
  also have "(1+1)*a < 0 \<longleftrightarrow> a < 0"
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   818
    by (simp add: mult_less_0_iff zero_less_two 
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   819
                  order_less_not_sym [OF zero_less_two])
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   820
  finally show ?thesis .
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   821
qed
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   822
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   823
lemma le_imp_0_less: 
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   824
  assumes le: "0 \<le> z"
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   825
  shows "(0::int) < 1 + z"
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   826
proof -
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   827
  have "0 \<le> z" by fact
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   828
  also have "... < z + 1" by (rule less_add_one) 
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   829
  also have "... = 1 + z" by (simp add: add_ac)
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   830
  finally show "0 < 1 + z" .
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   831
qed
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   832
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   833
lemma odd_less_0_iff:
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   834
  "(1 + z + z < 0) = (z < (0::int))"
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   835
proof (cases z rule: int_cases)
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   836
  case (nonneg n)
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   837
  thus ?thesis by (simp add: linorder_not_less add_assoc add_increasing
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   838
                             le_imp_0_less [THEN order_less_imp_le])  
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   839
next
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   840
  case (neg n)
30079
293b896b9c25 make proofs work whether or not One_nat_def is a simp rule; replace 1 with Suc 0 in the rhs of some simp rules
huffman
parents: 30000
diff changeset
   841
  thus ?thesis by (simp del: of_nat_Suc of_nat_add of_nat_1
293b896b9c25 make proofs work whether or not One_nat_def is a simp rule; replace 1 with Suc 0 in the rhs of some simp rules
huffman
parents: 30000
diff changeset
   842
    add: algebra_simps of_nat_1 [where 'a=int, symmetric] of_nat_add [symmetric])
28958
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   843
qed
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   844
28985
af325cd29b15 add named lemma lists: neg_simps and iszero_simps
huffman
parents: 28984
diff changeset
   845
lemma bin_less_0_simps:
28958
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   846
  "Pls < 0 \<longleftrightarrow> False"
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   847
  "Min < 0 \<longleftrightarrow> True"
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   848
  "Bit0 w < 0 \<longleftrightarrow> w < 0"
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   849
  "Bit1 w < 0 \<longleftrightarrow> w < 0"
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   850
  unfolding numeral_simps
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   851
  by (simp_all add: even_less_0_iff odd_less_0_iff)
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   852
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   853
lemma less_bin_lemma: "k < l \<longleftrightarrow> k - l < (0::int)"
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   854
  by simp
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   855
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   856
lemma le_iff_pred_less: "k \<le> l \<longleftrightarrow> pred k < l"
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   857
  unfolding numeral_simps
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   858
  proof
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   859
    have "k - 1 < k" by simp
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   860
    also assume "k \<le> l"
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   861
    finally show "k - 1 < l" .
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   862
  next
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   863
    assume "k - 1 < l"
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   864
    hence "(k - 1) + 1 \<le> l" by (rule zless_imp_add1_zle)
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   865
    thus "k \<le> l" by simp
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   866
  qed
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   867
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   868
lemma succ_pred: "succ (pred x) = x"
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   869
  unfolding numeral_simps by simp
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   870
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   871
text {* Less-than *}
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   872
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   873
lemma less_bin_simps [simp]:
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   874
  "Pls < Pls \<longleftrightarrow> False"
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   875
  "Pls < Min \<longleftrightarrow> False"
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   876
  "Pls < Bit0 k \<longleftrightarrow> Pls < k"
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   877
  "Pls < Bit1 k \<longleftrightarrow> Pls \<le> k"
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   878
  "Min < Pls \<longleftrightarrow> True"
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   879
  "Min < Min \<longleftrightarrow> False"
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   880
  "Min < Bit0 k \<longleftrightarrow> Min < k"
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   881
  "Min < Bit1 k \<longleftrightarrow> Min < k"
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   882
  "Bit0 k < Pls \<longleftrightarrow> k < Pls"
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   883
  "Bit0 k < Min \<longleftrightarrow> k \<le> Min"
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   884
  "Bit1 k < Pls \<longleftrightarrow> k < Pls"
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   885
  "Bit1 k < Min \<longleftrightarrow> k < Min"
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   886
  "Bit0 k < Bit0 l \<longleftrightarrow> k < l"
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   887
  "Bit0 k < Bit1 l \<longleftrightarrow> k \<le> l"
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   888
  "Bit1 k < Bit0 l \<longleftrightarrow> k < l"
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   889
  "Bit1 k < Bit1 l \<longleftrightarrow> k < l"
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   890
  unfolding le_iff_pred_less
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   891
    less_bin_lemma [of Pls]
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   892
    less_bin_lemma [of Min]
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   893
    less_bin_lemma [of "k"]
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   894
    less_bin_lemma [of "Bit0 k"]
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   895
    less_bin_lemma [of "Bit1 k"]
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   896
    less_bin_lemma [of "pred Pls"]
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   897
    less_bin_lemma [of "pred k"]
28985
af325cd29b15 add named lemma lists: neg_simps and iszero_simps
huffman
parents: 28984
diff changeset
   898
  by (simp_all add: bin_less_0_simps succ_pred)
28958
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   899
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   900
text {* Less-than-or-equal *}
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   901
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   902
lemma le_bin_simps [simp]:
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   903
  "Pls \<le> Pls \<longleftrightarrow> True"
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   904
  "Pls \<le> Min \<longleftrightarrow> False"
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   905
  "Pls \<le> Bit0 k \<longleftrightarrow> Pls \<le> k"
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   906
  "Pls \<le> Bit1 k \<longleftrightarrow> Pls \<le> k"
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   907
  "Min \<le> Pls \<longleftrightarrow> True"
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   908
  "Min \<le> Min \<longleftrightarrow> True"
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   909
  "Min \<le> Bit0 k \<longleftrightarrow> Min < k"
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   910
  "Min \<le> Bit1 k \<longleftrightarrow> Min \<le> k"
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   911
  "Bit0 k \<le> Pls \<longleftrightarrow> k \<le> Pls"
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   912
  "Bit0 k \<le> Min \<longleftrightarrow> k \<le> Min"
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   913
  "Bit1 k \<le> Pls \<longleftrightarrow> k < Pls"
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   914
  "Bit1 k \<le> Min \<longleftrightarrow> k \<le> Min"
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   915
  "Bit0 k \<le> Bit0 l \<longleftrightarrow> k \<le> l"
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   916
  "Bit0 k \<le> Bit1 l \<longleftrightarrow> k \<le> l"
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   917
  "Bit1 k \<le> Bit0 l \<longleftrightarrow> k < l"
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   918
  "Bit1 k \<le> Bit1 l \<longleftrightarrow> k \<le> l"
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   919
  unfolding not_less [symmetric]
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   920
  by (simp_all add: not_le)
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   921
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   922
text {* Equality *}
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   923
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   924
lemma eq_bin_simps [simp]:
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   925
  "Pls = Pls \<longleftrightarrow> True"
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   926
  "Pls = Min \<longleftrightarrow> False"
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   927
  "Pls = Bit0 l \<longleftrightarrow> Pls = l"
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   928
  "Pls = Bit1 l \<longleftrightarrow> False"
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   929
  "Min = Pls \<longleftrightarrow> False"
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   930
  "Min = Min \<longleftrightarrow> True"
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   931
  "Min = Bit0 l \<longleftrightarrow> False"
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   932
  "Min = Bit1 l \<longleftrightarrow> Min = l"
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   933
  "Bit0 k = Pls \<longleftrightarrow> k = Pls"
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   934
  "Bit0 k = Min \<longleftrightarrow> False"
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   935
  "Bit1 k = Pls \<longleftrightarrow> False"
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   936
  "Bit1 k = Min \<longleftrightarrow> k = Min"
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   937
  "Bit0 k = Bit0 l \<longleftrightarrow> k = l"
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   938
  "Bit0 k = Bit1 l \<longleftrightarrow> False"
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   939
  "Bit1 k = Bit0 l \<longleftrightarrow> False"
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   940
  "Bit1 k = Bit1 l \<longleftrightarrow> k = l"
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   941
  unfolding order_eq_iff [where 'a=int]
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   942
  by (simp_all add: not_less)
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   943
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   944
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   945
subsection {* Converting Numerals to Rings: @{term number_of} *}
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   946
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   947
class number_ring = number + comm_ring_1 +
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   948
  assumes number_of_eq: "number_of k = of_int k"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   949
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   950
text {* self-embedding of the integers *}
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   951
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   952
instantiation int :: number_ring
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   953
begin
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   954
28724
haftmann
parents: 28661
diff changeset
   955
definition int_number_of_def [code del]:
haftmann
parents: 28661
diff changeset
   956
  "number_of w = (of_int w \<Colon> int)"
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   957
28724
haftmann
parents: 28661
diff changeset
   958
instance proof
haftmann
parents: 28661
diff changeset
   959
qed (simp only: int_number_of_def)
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   960
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   961
end
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   962
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   963
lemma number_of_is_id:
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   964
  "number_of (k::int) = k"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   965
  unfolding int_number_of_def by simp
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   966
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   967
lemma number_of_succ:
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   968
  "number_of (succ k) = (1 + number_of k ::'a::number_ring)"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   969
  unfolding number_of_eq numeral_simps by simp
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   970
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   971
lemma number_of_pred:
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   972
  "number_of (pred w) = (- 1 + number_of w ::'a::number_ring)"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   973
  unfolding number_of_eq numeral_simps by simp
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   974
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   975
lemma number_of_minus:
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   976
  "number_of (uminus w) = (- (number_of w)::'a::number_ring)"
28958
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   977
  unfolding number_of_eq by (rule of_int_minus)
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   978
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   979
lemma number_of_add:
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   980
  "number_of (v + w) = (number_of v + number_of w::'a::number_ring)"
28958
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   981
  unfolding number_of_eq by (rule of_int_add)
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   982
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   983
lemma number_of_diff:
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   984
  "number_of (v - w) = (number_of v - number_of w::'a::number_ring)"
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   985
  unfolding number_of_eq by (rule of_int_diff)
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   986
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   987
lemma number_of_mult:
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   988
  "number_of (v * w) = (number_of v * number_of w::'a::number_ring)"
28958
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   989
  unfolding number_of_eq by (rule of_int_mult)
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   990
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   991
text {*
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   992
  The correctness of shifting.
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   993
  But it doesn't seem to give a measurable speed-up.
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   994
*}
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   995
26086
3c243098b64a New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents: 26075
diff changeset
   996
lemma double_number_of_Bit0:
3c243098b64a New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents: 26075
diff changeset
   997
  "(1 + 1) * number_of w = (number_of (Bit0 w) ::'a::number_ring)"
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   998
  unfolding number_of_eq numeral_simps left_distrib by simp
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   999
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1000
text {*
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1001
  Converting numerals 0 and 1 to their abstract versions.
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1002
*}
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1003
32272
cc1bf9077167 added numeral code postprocessor rules on type int
haftmann
parents: 32069
diff changeset
  1004
lemma numeral_0_eq_0 [simp, code_post]:
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1005
  "Numeral0 = (0::'a::number_ring)"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1006
  unfolding number_of_eq numeral_simps by simp
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1007
32272
cc1bf9077167 added numeral code postprocessor rules on type int
haftmann
parents: 32069
diff changeset
  1008
lemma numeral_1_eq_1 [simp, code_post]:
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1009
  "Numeral1 = (1::'a::number_ring)"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1010
  unfolding number_of_eq numeral_simps by simp
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1011
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1012
text {*
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1013
  Special-case simplification for small constants.
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1014
*}
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1015
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1016
text{*
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1017
  Unary minus for the abstract constant 1. Cannot be inserted
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1018
  as a simprule until later: it is @{text number_of_Min} re-oriented!
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1019
*}
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1020
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1021
lemma numeral_m1_eq_minus_1:
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1022
  "(-1::'a::number_ring) = - 1"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1023
  unfolding number_of_eq numeral_simps by simp
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1024
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1025
lemma mult_minus1 [simp]:
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1026
  "-1 * z = -(z::'a::number_ring)"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1027
  unfolding number_of_eq numeral_simps by simp
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1028
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1029
lemma mult_minus1_right [simp]:
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1030
  "z * -1 = -(z::'a::number_ring)"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1031
  unfolding number_of_eq numeral_simps by simp
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1032
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1033
(*Negation of a coefficient*)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1034
lemma minus_number_of_mult [simp]:
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1035
   "- (number_of w) * z = number_of (uminus w) * (z::'a::number_ring)"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1036
   unfolding number_of_eq by simp
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1037
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1038
text {* Subtraction *}
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1039
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1040
lemma diff_number_of_eq:
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1041
  "number_of v - number_of w =
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1042
    (number_of (v + uminus w)::'a::number_ring)"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1043
  unfolding number_of_eq by simp
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1044
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1045
lemma number_of_Pls:
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1046
  "number_of Pls = (0::'a::number_ring)"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1047
  unfolding number_of_eq numeral_simps by simp
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1048
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1049
lemma number_of_Min:
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1050
  "number_of Min = (- 1::'a::number_ring)"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1051
  unfolding number_of_eq numeral_simps by simp
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1052
26086
3c243098b64a New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents: 26075
diff changeset
  1053
lemma number_of_Bit0:
3c243098b64a New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents: 26075
diff changeset
  1054
  "number_of (Bit0 w) = (0::'a::number_ring) + (number_of w) + (number_of w)"
3c243098b64a New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents: 26075
diff changeset
  1055
  unfolding number_of_eq numeral_simps by simp
3c243098b64a New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents: 26075
diff changeset
  1056
3c243098b64a New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents: 26075
diff changeset
  1057
lemma number_of_Bit1:
3c243098b64a New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents: 26075
diff changeset
  1058
  "number_of (Bit1 w) = (1::'a::number_ring) + (number_of w) + (number_of w)"
3c243098b64a New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents: 26075
diff changeset
  1059
  unfolding number_of_eq numeral_simps by simp
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1060
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1061
28958
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
  1062
subsubsection {* Equality of Binary Numbers *}
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1063
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1064
text {* First version by Norbert Voelker *}
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1065
36716
b09f3ad3208f moved generic lemmas to appropriate places
haftmann
parents: 36424
diff changeset
  1066
definition (*for simplifying equalities*) iszero :: "'a\<Colon>semiring_1 \<Rightarrow> bool" where
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1067
  "iszero z \<longleftrightarrow> z = 0"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1068
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1069
lemma iszero_0: "iszero 0"
36716
b09f3ad3208f moved generic lemmas to appropriate places
haftmann
parents: 36424
diff changeset
  1070
  by (simp add: iszero_def)
b09f3ad3208f moved generic lemmas to appropriate places
haftmann
parents: 36424
diff changeset
  1071
b09f3ad3208f moved generic lemmas to appropriate places
haftmann
parents: 36424
diff changeset
  1072
lemma iszero_Numeral0: "iszero (Numeral0 :: 'a::number_ring)"
b09f3ad3208f moved generic lemmas to appropriate places
haftmann
parents: 36424
diff changeset
  1073
  by (simp add: iszero_0)
b09f3ad3208f moved generic lemmas to appropriate places
haftmann
parents: 36424
diff changeset
  1074
b09f3ad3208f moved generic lemmas to appropriate places
haftmann
parents: 36424
diff changeset
  1075
lemma not_iszero_1: "\<not> iszero 1"
b09f3ad3208f moved generic lemmas to appropriate places
haftmann
parents: 36424
diff changeset
  1076
  by (simp add: iszero_def)
b09f3ad3208f moved generic lemmas to appropriate places
haftmann
parents: 36424
diff changeset
  1077
b09f3ad3208f moved generic lemmas to appropriate places
haftmann
parents: 36424
diff changeset
  1078
lemma not_iszero_Numeral1: "\<not> iszero (Numeral1 :: 'a::number_ring)"
b09f3ad3208f moved generic lemmas to appropriate places
haftmann
parents: 36424
diff changeset
  1079
  by (simp add: not_iszero_1)
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1080
35216
7641e8d831d2 get rid of many duplicate simp rule warnings
huffman
parents: 35123
diff changeset
  1081
lemma eq_number_of_eq [simp]:
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1082
  "((number_of x::'a::number_ring) = number_of y) =
36716
b09f3ad3208f moved generic lemmas to appropriate places
haftmann
parents: 36424
diff changeset
  1083
     iszero (number_of (x + uminus y) :: 'a)"
29667
53103fc8ffa3 Replaced group_ and ring_simps by algebra_simps;
nipkow
parents: 29046
diff changeset
  1084
unfolding iszero_def number_of_add number_of_minus
53103fc8ffa3 Replaced group_ and ring_simps by algebra_simps;
nipkow
parents: 29046
diff changeset
  1085
by (simp add: algebra_simps)
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1086
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1087
lemma iszero_number_of_Pls:
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1088
  "iszero ((number_of Pls)::'a::number_ring)"
29667
53103fc8ffa3 Replaced group_ and ring_simps by algebra_simps;
nipkow
parents: 29046
diff changeset
  1089
unfolding iszero_def numeral_0_eq_0 ..
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1090
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1091
lemma nonzero_number_of_Min:
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1092
  "~ iszero ((number_of Min)::'a::number_ring)"
29667
53103fc8ffa3 Replaced group_ and ring_simps by algebra_simps;
nipkow
parents: 29046
diff changeset
  1093
unfolding iszero_def numeral_m1_eq_minus_1 by simp
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1094
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1095
28958
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
  1096
subsubsection {* Comparisons, for Ordered Rings *}
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1097
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1098
lemmas double_eq_0_iff = double_zero
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1099
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1100
lemma odd_nonzero:
33296
a3924d1069e5 moved theory Divides after theory Nat_Numeral; tuned some proof texts
haftmann
parents: 33056
diff changeset
  1101
  "1 + z + z \<noteq> (0::int)"
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1102
proof (cases z rule: int_cases)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1103
  case (nonneg n)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1104
  have le: "0 \<le> z+z" by (simp add: nonneg add_increasing) 
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1105
  thus ?thesis using  le_imp_0_less [OF le]
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1106
    by (auto simp add: add_assoc) 
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1107
next
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1108
  case (neg n)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1109
  show ?thesis
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1110
  proof
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1111
    assume eq: "1 + z + z = 0"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1112
    have "(0::int) < 1 + (of_nat n + of_nat n)"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1113
      by (simp add: le_imp_0_less add_increasing) 
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1114
    also have "... = - (1 + z + z)" 
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1115
      by (simp add: neg add_assoc [symmetric]) 
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1116
    also have "... = 0" by (simp add: eq) 
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1117
    finally have "0<0" ..
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1118
    thus False by blast
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1119
  qed
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1120
qed
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1121
26086
3c243098b64a New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents: 26075
diff changeset
  1122
lemma iszero_number_of_Bit0:
3c243098b64a New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents: 26075
diff changeset
  1123
  "iszero (number_of (Bit0 w)::'a) = 
3c243098b64a New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents: 26075
diff changeset
  1124
   iszero (number_of w::'a::{ring_char_0,number_ring})"
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1125
proof -
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1126
  have "(of_int w + of_int w = (0::'a)) \<Longrightarrow> (w = 0)"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1127
  proof -
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1128
    assume eq: "of_int w + of_int w = (0::'a)"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1129
    then have "of_int (w + w) = (of_int 0 :: 'a)" by simp
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1130
    then have "w + w = 0" by (simp only: of_int_eq_iff)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1131
    then show "w = 0" by (simp only: double_eq_0_iff)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1132
  qed
26086
3c243098b64a New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents: 26075
diff changeset
  1133
  thus ?thesis
3c243098b64a New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents: 26075
diff changeset
  1134
    by (auto simp add: iszero_def number_of_eq numeral_simps)
3c243098b64a New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents: 26075
diff changeset
  1135
qed
3c243098b64a New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents: 26075
diff changeset
  1136
3c243098b64a New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents: 26075
diff changeset
  1137
lemma iszero_number_of_Bit1:
3c243098b64a New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents: 26075
diff changeset
  1138
  "~ iszero (number_of (Bit1 w)::'a::{ring_char_0,number_ring})"
3c243098b64a New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents: 26075
diff changeset
  1139
proof -
3c243098b64a New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents: 26075
diff changeset
  1140
  have "1 + of_int w + of_int w \<noteq> (0::'a)"
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1141
  proof
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1142
    assume eq: "1 + of_int w + of_int w = (0::'a)"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1143
    hence "of_int (1 + w + w) = (of_int 0 :: 'a)" by simp 
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1144
    hence "1 + w + w = 0" by (simp only: of_int_eq_iff)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1145
    with odd_nonzero show False by blast
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1146
  qed
26086
3c243098b64a New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents: 26075
diff changeset
  1147
  thus ?thesis
3c243098b64a New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents: 26075
diff changeset
  1148
    by (auto simp add: iszero_def number_of_eq numeral_simps)
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1149
qed
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1150
35216
7641e8d831d2 get rid of many duplicate simp rule warnings
huffman
parents: 35123
diff changeset
  1151
lemmas iszero_simps [simp] =
28985
af325cd29b15 add named lemma lists: neg_simps and iszero_simps
huffman
parents: 28984
diff changeset
  1152
  iszero_0 not_iszero_1
af325cd29b15 add named lemma lists: neg_simps and iszero_simps
huffman
parents: 28984
diff changeset
  1153
  iszero_number_of_Pls nonzero_number_of_Min
af325cd29b15 add named lemma lists: neg_simps and iszero_simps
huffman
parents: 28984
diff changeset
  1154
  iszero_number_of_Bit0 iszero_number_of_Bit1
af325cd29b15 add named lemma lists: neg_simps and iszero_simps
huffman
parents: 28984
diff changeset
  1155
(* iszero_number_of_Pls would never normally be used
af325cd29b15 add named lemma lists: neg_simps and iszero_simps
huffman
parents: 28984
diff changeset
  1156
   because its lhs simplifies to "iszero 0" *)
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1157
28958
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
  1158
subsubsection {* The Less-Than Relation *}
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1159
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1160
lemma double_less_0_iff:
35028
108662d50512 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34055
diff changeset
  1161
  "(a + a < 0) = (a < (0::'a::linordered_idom))"
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1162
proof -
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1163
  have "(a + a < 0) = ((1+1)*a < 0)" by (simp add: left_distrib)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1164
  also have "... = (a < 0)"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1165
    by (simp add: mult_less_0_iff zero_less_two 
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1166
                  order_less_not_sym [OF zero_less_two]) 
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1167
  finally show ?thesis .
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1168
qed
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1169
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1170
lemma odd_less_0:
33296
a3924d1069e5 moved theory Divides after theory Nat_Numeral; tuned some proof texts
haftmann
parents: 33056
diff changeset
  1171
  "(1 + z + z < 0) = (z < (0::int))"
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1172
proof (cases z rule: int_cases)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1173
  case (nonneg n)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1174
  thus ?thesis by (simp add: linorder_not_less add_assoc add_increasing
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1175
                             le_imp_0_less [THEN order_less_imp_le])  
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1176
next
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1177
  case (neg n)
30079
293b896b9c25 make proofs work whether or not One_nat_def is a simp rule; replace 1 with Suc 0 in the rhs of some simp rules
huffman
parents: 30000
diff changeset
  1178
  thus ?thesis by (simp del: of_nat_Suc of_nat_add of_nat_1
293b896b9c25 make proofs work whether or not One_nat_def is a simp rule; replace 1 with Suc 0 in the rhs of some simp rules
huffman
parents: 30000
diff changeset
  1179
    add: algebra_simps of_nat_1 [where 'a=int, symmetric] of_nat_add [symmetric])
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1180
qed
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1181
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1182
text {* Less-Than or Equals *}
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1183
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1184
text {* Reduces @{term "a\<le>b"} to @{term "~ (b<a)"} for ALL numerals. *}
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1185
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1186
lemmas le_number_of_eq_not_less =
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1187
  linorder_not_less [of "number_of w" "number_of v", symmetric, 
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1188
  standard]
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1189
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1190
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1191
text {* Absolute value (@{term abs}) *}
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1192
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1193
lemma abs_number_of:
35028
108662d50512 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34055
diff changeset
  1194
  "abs(number_of x::'a::{linordered_idom,number_ring}) =
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1195
   (if number_of x < (0::'a) then -number_of x else number_of x)"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1196
  by (simp add: abs_if)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1197
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1198
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1199
text {* Re-orientation of the equation nnn=x *}
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1200
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1201
lemma number_of_reorient:
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1202
  "(number_of w = x) = (x = number_of w)"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1203
  by auto
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1204
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1205
28958
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
  1206
subsubsection {* Simplification of arithmetic operations on integer constants. *}
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1207
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1208
lemmas arith_extra_simps [standard, simp] =
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1209
  number_of_add [symmetric]
28958
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
  1210
  number_of_minus [symmetric]
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
  1211
  numeral_m1_eq_minus_1 [symmetric]
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1212
  number_of_mult [symmetric]
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1213
  diff_number_of_eq abs_number_of 
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1214
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1215
text {*
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1216
  For making a minimal simpset, one must include these default simprules.
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1217
  Also include @{text simp_thms}.
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1218
*}
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1219
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1220
lemmas arith_simps = 
26075
815f3ccc0b45 added lemma lists {normalize,succ,pred,minus,add,mult}_bin_simps
huffman
parents: 26072
diff changeset
  1221
  normalize_bin_simps pred_bin_simps succ_bin_simps
815f3ccc0b45 added lemma lists {normalize,succ,pred,minus,add,mult}_bin_simps
huffman
parents: 26072
diff changeset
  1222
  add_bin_simps minus_bin_simps mult_bin_simps
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1223
  abs_zero abs_one arith_extra_simps
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1224
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1225
text {* Simplification of relational operations *}
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1226
28962
f603183f7a5c enable le_bin_simps and less_bin_simps for simplifying inequalities on numerals
huffman
parents: 28958
diff changeset
  1227
lemma less_number_of [simp]:
35028
108662d50512 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34055
diff changeset
  1228
  "(number_of x::'a::{linordered_idom,number_ring}) < number_of y \<longleftrightarrow> x < y"
28962
f603183f7a5c enable le_bin_simps and less_bin_simps for simplifying inequalities on numerals
huffman
parents: 28958
diff changeset
  1229
  unfolding number_of_eq by (rule of_int_less_iff)
f603183f7a5c enable le_bin_simps and less_bin_simps for simplifying inequalities on numerals
huffman
parents: 28958
diff changeset
  1230
f603183f7a5c enable le_bin_simps and less_bin_simps for simplifying inequalities on numerals
huffman
parents: 28958
diff changeset
  1231
lemma le_number_of [simp]:
35028
108662d50512 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34055
diff changeset
  1232
  "(number_of x::'a::{linordered_idom,number_ring}) \<le> number_of y \<longleftrightarrow> x \<le> y"
28962
f603183f7a5c enable le_bin_simps and less_bin_simps for simplifying inequalities on numerals
huffman
parents: 28958
diff changeset
  1233
  unfolding number_of_eq by (rule of_int_le_iff)
f603183f7a5c enable le_bin_simps and less_bin_simps for simplifying inequalities on numerals
huffman
parents: 28958
diff changeset
  1234
28967
3bdb1eae352c enable eq_bin_simps for simplifying equalities on numerals
huffman
parents: 28962
diff changeset
  1235
lemma eq_number_of [simp]:
3bdb1eae352c enable eq_bin_simps for simplifying equalities on numerals
huffman
parents: 28962
diff changeset
  1236
  "(number_of x::'a::{ring_char_0,number_ring}) = number_of y \<longleftrightarrow> x = y"
3bdb1eae352c enable eq_bin_simps for simplifying equalities on numerals
huffman
parents: 28962
diff changeset
  1237
  unfolding number_of_eq by (rule of_int_eq_iff)
3bdb1eae352c enable eq_bin_simps for simplifying equalities on numerals
huffman
parents: 28962
diff changeset
  1238
35216
7641e8d831d2 get rid of many duplicate simp rule warnings
huffman
parents: 35123
diff changeset
  1239
lemmas rel_simps =
28962
f603183f7a5c enable le_bin_simps and less_bin_simps for simplifying inequalities on numerals
huffman
parents: 28958
diff changeset
  1240
  less_number_of less_bin_simps
f603183f7a5c enable le_bin_simps and less_bin_simps for simplifying inequalities on numerals
huffman
parents: 28958
diff changeset
  1241
  le_number_of le_bin_simps
28988
13d6f120992b revert to using eq_number_of_eq for simplification (Groebner_Examples.thy was broken)
huffman
parents: 28985
diff changeset
  1242
  eq_number_of_eq eq_bin_simps
29039
8b9207f82a78 separate neg_simps from rel_simps
huffman
parents: 28988
diff changeset
  1243
  iszero_simps
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1244
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1245
28958
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
  1246
subsubsection {* Simplification of arithmetic when nested to the right. *}
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1247
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1248
lemma add_number_of_left [simp]:
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1249
  "number_of v + (number_of w + z) =
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1250
   (number_of(v + w) + z::'a::number_ring)"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1251
  by (simp add: add_assoc [symmetric])
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1252
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1253
lemma mult_number_of_left [simp]:
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1254
  "number_of v * (number_of w * z) =
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1255
   (number_of(v * w) * z::'a::number_ring)"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1256
  by (simp add: mult_assoc [symmetric])
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1257
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1258
lemma add_number_of_diff1:
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1259
  "number_of v + (number_of w - c) = 
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1260
  number_of(v + w) - (c::'a::number_ring)"
35216
7641e8d831d2 get rid of many duplicate simp rule warnings
huffman
parents: 35123
diff changeset
  1261
  by (simp add: diff_minus)
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1262
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1263
lemma add_number_of_diff2 [simp]:
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1264
  "number_of v + (c - number_of w) =
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1265
   number_of (v + uminus w) + (c::'a::number_ring)"
29667
53103fc8ffa3 Replaced group_ and ring_simps by algebra_simps;
nipkow
parents: 29046
diff changeset
  1266
by (simp add: algebra_simps diff_number_of_eq [symmetric])
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1267
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1268
30652
752329615264 distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents: 30496
diff changeset
  1269
752329615264 distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents: 30496
diff changeset
  1270
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1271
subsection {* The Set of Integers *}
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1272
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1273
context ring_1
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1274
begin
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1275
30652
752329615264 distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents: 30496
diff changeset
  1276
definition Ints  :: "'a set" where
28562
4e74209f113e `code func` now just `code`
haftmann
parents: 28537
diff changeset
  1277
  [code del]: "Ints = range of_int"
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1278
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1279
notation (xsymbols)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1280
  Ints  ("\<int>")
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1281
35634
6fdfe37b84d6 add more simp rules for Ints
huffman
parents: 35216
diff changeset
  1282
lemma Ints_of_int [simp]: "of_int z \<in> \<int>"
6fdfe37b84d6 add more simp rules for Ints
huffman
parents: 35216
diff changeset
  1283
  by (simp add: Ints_def)
6fdfe37b84d6 add more simp rules for Ints
huffman
parents: 35216
diff changeset
  1284
6fdfe37b84d6 add more simp rules for Ints
huffman
parents: 35216
diff changeset
  1285
lemma Ints_of_nat [simp]: "of_nat n \<in> \<int>"
6fdfe37b84d6 add more simp rules for Ints
huffman
parents: 35216
diff changeset
  1286
apply (simp add: Ints_def)
6fdfe37b84d6 add more simp rules for Ints
huffman
parents: 35216
diff changeset
  1287
apply (rule range_eqI)
6fdfe37b84d6 add more simp rules for Ints
huffman
parents: 35216
diff changeset
  1288
apply (rule of_int_of_nat_eq [symmetric])
6fdfe37b84d6 add more simp rules for Ints
huffman
parents: 35216
diff changeset
  1289
done
6fdfe37b84d6 add more simp rules for Ints
huffman
parents: 35216
diff changeset
  1290
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1291
lemma Ints_0 [simp]: "0 \<in> \<int>"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1292
apply (simp add: Ints_def)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1293
apply (rule range_eqI)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1294
apply (rule of_int_0 [symmetric])
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1295
done
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1296
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1297
lemma Ints_1 [simp]: "1 \<in> \<int>"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1298
apply (simp add: Ints_def)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1299
apply (rule range_eqI)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1300
apply (rule of_int_1 [symmetric])
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1301
done
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1302
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1303
lemma Ints_add [simp]: "a \<in> \<int> \<Longrightarrow> b \<in> \<int> \<Longrightarrow> a + b \<in> \<int>"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1304
apply (auto simp add: Ints_def)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1305
apply (rule range_eqI)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1306
apply (rule of_int_add [symmetric])
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1307
done
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1308
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1309
lemma Ints_minus [simp]: "a \<in> \<int> \<Longrightarrow> -a \<in> \<int>"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1310
apply (auto simp add: Ints_def)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1311
apply (rule range_eqI)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1312
apply (rule of_int_minus [symmetric])
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1313
done
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1314
35634
6fdfe37b84d6 add more simp rules for Ints
huffman
parents: 35216
diff changeset
  1315
lemma Ints_diff [simp]: "a \<in> \<int> \<Longrightarrow> b \<in> \<int> \<Longrightarrow> a - b \<in> \<int>"
6fdfe37b84d6 add more simp rules for Ints
huffman
parents: 35216
diff changeset
  1316
apply (auto simp add: Ints_def)
6fdfe37b84d6 add more simp rules for Ints
huffman
parents: 35216
diff changeset
  1317
apply (rule range_eqI)
6fdfe37b84d6 add more simp rules for Ints
huffman
parents: 35216
diff changeset
  1318
apply (rule of_int_diff [symmetric])
6fdfe37b84d6 add more simp rules for Ints
huffman
parents: 35216
diff changeset
  1319
done
6fdfe37b84d6 add more simp rules for Ints
huffman
parents: 35216
diff changeset
  1320
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1321
lemma Ints_mult [simp]: "a \<in> \<int> \<Longrightarrow> b \<in> \<int> \<Longrightarrow> a * b \<in> \<int>"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1322
apply (auto simp add: Ints_def)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1323
apply (rule range_eqI)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1324
apply (rule of_int_mult [symmetric])
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1325
done
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1326
35634
6fdfe37b84d6 add more simp rules for Ints
huffman
parents: 35216
diff changeset
  1327
lemma Ints_power [simp]: "a \<in> \<int> \<Longrightarrow> a ^ n \<in> \<int>"
6fdfe37b84d6 add more simp rules for Ints
huffman
parents: 35216
diff changeset
  1328
by (induct n) simp_all
6fdfe37b84d6 add more simp rules for Ints
huffman
parents: 35216
diff changeset
  1329
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1330
lemma Ints_cases [cases set: Ints]:
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1331
  assumes "q \<in> \<int>"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1332
  obtains (of_int) z where "q = of_int z"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1333
  unfolding Ints_def
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1334
proof -
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1335
  from `q \<in> \<int>` have "q \<in> range of_int" unfolding Ints_def .
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1336
  then obtain z where "q = of_int z" ..
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1337
  then show thesis ..
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1338
qed
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1339
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1340
lemma Ints_induct [case_names of_int, induct set: Ints]:
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1341
  "q \<in> \<int> \<Longrightarrow> (\<And>z. P (of_int z)) \<Longrightarrow> P q"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1342
  by (rule Ints_cases) auto
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1343
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1344
end
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1345
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1346
text {* The premise involving @{term Ints} prevents @{term "a = 1/2"}. *}
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1347
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1348
lemma Ints_double_eq_0_iff:
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1349
  assumes in_Ints: "a \<in> Ints"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1350
  shows "(a + a = 0) = (a = (0::'a::ring_char_0))"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1351
proof -
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1352
  from in_Ints have "a \<in> range of_int" unfolding Ints_def [symmetric] .
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1353
  then obtain z where a: "a = of_int z" ..
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1354
  show ?thesis
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1355
  proof
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1356
    assume "a = 0"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1357
    thus "a + a = 0" by simp
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1358
  next
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1359
    assume eq: "a + a = 0"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1360
    hence "of_int (z + z) = (of_int 0 :: 'a)" by (simp add: a)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1361
    hence "z + z = 0" by (simp only: of_int_eq_iff)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1362
    hence "z = 0" by (simp only: double_eq_0_iff)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1363
    thus "a = 0" by (simp add: a)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1364
  qed
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1365
qed
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1366
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1367
lemma Ints_odd_nonzero:
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1368
  assumes in_Ints: "a \<in> Ints"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1369
  shows "1 + a + a \<noteq> (0::'a::ring_char_0)"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1370
proof -
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1371
  from in_Ints have "a \<in> range of_int" unfolding Ints_def [symmetric] .
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1372
  then obtain z where a: "a = of_int z" ..
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1373
  show ?thesis
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1374
  proof
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1375
    assume eq: "1 + a + a = 0"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1376
    hence "of_int (1 + z + z) = (of_int 0 :: 'a)" by (simp add: a)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1377
    hence "1 + z + z = 0" by (simp only: of_int_eq_iff)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1378
    with odd_nonzero show False by blast
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1379
  qed
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1380
qed 
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1381
35634
6fdfe37b84d6 add more simp rules for Ints
huffman
parents: 35216
diff changeset
  1382
lemma Ints_number_of [simp]:
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1383
  "(number_of w :: 'a::number_ring) \<in> Ints"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1384
  unfolding number_of_eq Ints_def by simp
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1385
35634
6fdfe37b84d6 add more simp rules for Ints
huffman
parents: 35216
diff changeset
  1386
lemma Nats_number_of [simp]:
6fdfe37b84d6 add more simp rules for Ints
huffman
parents: 35216
diff changeset
  1387
  "Int.Pls \<le> w \<Longrightarrow> (number_of w :: 'a::number_ring) \<in> Nats"
6fdfe37b84d6 add more simp rules for Ints
huffman
parents: 35216
diff changeset
  1388
unfolding Int.Pls_def number_of_eq
6fdfe37b84d6 add more simp rules for Ints
huffman
parents: 35216
diff changeset
  1389
by (simp only: of_nat_nat [symmetric] of_nat_in_Nats)
6fdfe37b84d6 add more simp rules for Ints
huffman
parents: 35216
diff changeset
  1390
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1391
lemma Ints_odd_less_0: 
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1392
  assumes in_Ints: "a \<in> Ints"
35028
108662d50512 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34055
diff changeset
  1393
  shows "(1 + a + a < 0) = (a < (0::'a::linordered_idom))"
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1394
proof -
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1395
  from in_Ints have "a \<in> range of_int" unfolding Ints_def [symmetric] .
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1396
  then obtain z where a: "a = of_int z" ..
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1397
  hence "((1::'a) + a + a < 0) = (of_int (1 + z + z) < (of_int 0 :: 'a))"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1398
    by (simp add: a)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1399
  also have "... = (z < 0)" by (simp only: of_int_less_iff odd_less_0)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1400
  also have "... = (a < 0)" by (simp add: a)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1401
  finally show ?thesis .
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1402
qed
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1403
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1404
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1405
subsection {* @{term setsum} and @{term setprod} *}
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1406
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1407
lemma of_nat_setsum: "of_nat (setsum f A) = (\<Sum>x\<in>A. of_nat(f x))"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1408
  apply (cases "finite A")
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1409
  apply (erule finite_induct, auto)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1410
  done
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1411
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1412
lemma of_int_setsum: "of_int (setsum f A) = (\<Sum>x\<in>A. of_int(f x))"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1413
  apply (cases "finite A")
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1414
  apply (erule finite_induct, auto)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1415
  done
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1416
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1417
lemma of_nat_setprod: "of_nat (setprod f A) = (\<Prod>x\<in>A. of_nat(f x))"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1418
  apply (cases "finite A")
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1419
  apply (erule finite_induct, auto simp add: of_nat_mult)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1420
  done
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1421
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1422
lemma of_int_setprod: "of_int (setprod f A) = (\<Prod>x\<in>A. of_int(f x))"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1423
  apply (cases "finite A")
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1424
  apply (erule finite_induct, auto)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1425
  done
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1426
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1427
lemmas int_setsum = of_nat_setsum [where 'a=int]
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1428
lemmas int_setprod = of_nat_setprod [where 'a=int]
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1429
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1430
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1431
subsection{*Inequality Reasoning for the Arithmetic Simproc*}
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1432
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1433
lemma add_numeral_0: "Numeral0 + a = (a::'a::number_ring)"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1434
by simp 
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1435
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1436
lemma add_numeral_0_right: "a + Numeral0 = (a::'a::number_ring)"