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