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