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