src/HOL/IntDef.thy
author huffman
Wed Jun 13 03:31:11 2007 +0200 (2007-06-13)
changeset 23365 f31794033ae1
parent 23308 95a01ddfb024
child 23372 0035be079bee
permissions -rw-r--r--
removed constant int :: nat => int;
int is now an abbreviation for of_nat :: nat => int
     1 (*  Title:      IntDef.thy
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1996  University of Cambridge
     5 
     6 *)
     7 
     8 header{*The Integers as Equivalence Classes over Pairs of Natural Numbers*} 
     9 
    10 theory IntDef
    11 imports Equiv_Relations Nat
    12 begin
    13 
    14 text {* the equivalence relation underlying the integers *}
    15 
    16 definition
    17   intrel :: "((nat \<times> nat) \<times> (nat \<times> nat)) set"
    18 where
    19   "intrel = {((x, y), (u, v)) | x y u v. x + v = u +y }"
    20 
    21 typedef (Integ)
    22   int = "UNIV//intrel"
    23   by (auto simp add: quotient_def)
    24 
    25 instance int :: zero
    26   Zero_int_def: "0 \<equiv> Abs_Integ (intrel `` {(0, 0)})" ..
    27 
    28 instance int :: one
    29   One_int_def: "1 \<equiv> Abs_Integ (intrel `` {(1, 0)})" ..
    30 
    31 instance int :: plus
    32   add_int_def: "z + w \<equiv> Abs_Integ
    33     (\<Union>(x, y) \<in> Rep_Integ z. \<Union>(u, v) \<in> Rep_Integ w.
    34       intrel `` {(x + u, y + v)})" ..
    35 
    36 instance int :: minus
    37   minus_int_def:
    38     "- z \<equiv> Abs_Integ (\<Union>(x, y) \<in> Rep_Integ z. intrel `` {(y, x)})"
    39   diff_int_def:  "z - w \<equiv> z + (-w)" ..
    40 
    41 instance int :: times
    42   mult_int_def: "z * w \<equiv>  Abs_Integ
    43     (\<Union>(x, y) \<in> Rep_Integ z. \<Union>(u,v ) \<in> Rep_Integ w.
    44       intrel `` {(x*u + y*v, x*v + y*u)})" ..
    45 
    46 instance int :: ord
    47   le_int_def:
    48    "z \<le> w \<equiv> \<exists>x y u v. x+v \<le> u+y \<and> (x, y) \<in> Rep_Integ z \<and> (u, v) \<in> Rep_Integ w"
    49   less_int_def: "z < w \<equiv> z \<le> w \<and> z \<noteq> w" ..
    50 
    51 lemmas [code func del] = Zero_int_def One_int_def add_int_def
    52   minus_int_def mult_int_def le_int_def less_int_def
    53 
    54 
    55 subsection{*Construction of the Integers*}
    56 
    57 subsubsection{*Preliminary Lemmas about the Equivalence Relation*}
    58 
    59 lemma intrel_iff [simp]: "(((x,y),(u,v)) \<in> intrel) = (x+v = u+y)"
    60 by (simp add: intrel_def)
    61 
    62 lemma equiv_intrel: "equiv UNIV intrel"
    63 by (simp add: intrel_def equiv_def refl_def sym_def trans_def)
    64 
    65 text{*Reduces equality of equivalence classes to the @{term intrel} relation:
    66   @{term "(intrel `` {x} = intrel `` {y}) = ((x,y) \<in> intrel)"} *}
    67 lemmas equiv_intrel_iff [simp] = eq_equiv_class_iff [OF equiv_intrel UNIV_I UNIV_I]
    68 
    69 text{*All equivalence classes belong to set of representatives*}
    70 lemma [simp]: "intrel``{(x,y)} \<in> Integ"
    71 by (auto simp add: Integ_def intrel_def quotient_def)
    72 
    73 text{*Reduces equality on abstractions to equality on representatives:
    74   @{prop "\<lbrakk>x \<in> Integ; y \<in> Integ\<rbrakk> \<Longrightarrow> (Abs_Integ x = Abs_Integ y) = (x=y)"} *}
    75 declare Abs_Integ_inject [simp]  Abs_Integ_inverse [simp]
    76 
    77 text{*Case analysis on the representation of an integer as an equivalence
    78       class of pairs of naturals.*}
    79 lemma eq_Abs_Integ [case_names Abs_Integ, cases type: int]:
    80      "(!!x y. z = Abs_Integ(intrel``{(x,y)}) ==> P) ==> P"
    81 apply (rule Abs_Integ_cases [of z]) 
    82 apply (auto simp add: Integ_def quotient_def) 
    83 done
    84 
    85 
    86 subsubsection{*Integer Unary Negation*}
    87 
    88 lemma minus: "- Abs_Integ(intrel``{(x,y)}) = Abs_Integ(intrel `` {(y,x)})"
    89 proof -
    90   have "(\<lambda>(x,y). intrel``{(y,x)}) respects intrel"
    91     by (simp add: congruent_def) 
    92   thus ?thesis
    93     by (simp add: minus_int_def UN_equiv_class [OF equiv_intrel])
    94 qed
    95 
    96 lemma zminus_zminus: "- (- z) = (z::int)"
    97   by (cases z) (simp add: minus)
    98 
    99 lemma zminus_0: "- 0 = (0::int)"
   100   by (simp add: Zero_int_def minus)
   101 
   102 
   103 subsection{*Integer Addition*}
   104 
   105 lemma add:
   106      "Abs_Integ (intrel``{(x,y)}) + Abs_Integ (intrel``{(u,v)}) =
   107       Abs_Integ (intrel``{(x+u, y+v)})"
   108 proof -
   109   have "(\<lambda>z w. (\<lambda>(x,y). (\<lambda>(u,v). intrel `` {(x+u, y+v)}) w) z) 
   110         respects2 intrel"
   111     by (simp add: congruent2_def)
   112   thus ?thesis
   113     by (simp add: add_int_def UN_UN_split_split_eq
   114                   UN_equiv_class2 [OF equiv_intrel equiv_intrel])
   115 qed
   116 
   117 lemma zminus_zadd_distrib: "- (z + w) = (- z) + (- w::int)"
   118   by (cases z, cases w) (simp add: minus add)
   119 
   120 lemma zadd_commute: "(z::int) + w = w + z"
   121   by (cases z, cases w) (simp add: add_ac add)
   122 
   123 lemma zadd_assoc: "((z1::int) + z2) + z3 = z1 + (z2 + z3)"
   124   by (cases z1, cases z2, cases z3) (simp add: add add_assoc)
   125 
   126 (*For AC rewriting*)
   127 lemma zadd_left_commute: "x + (y + z) = y + ((x + z)  ::int)"
   128   apply (rule mk_left_commute [of "op +"])
   129   apply (rule zadd_assoc)
   130   apply (rule zadd_commute)
   131   done
   132 
   133 lemmas zadd_ac = zadd_assoc zadd_commute zadd_left_commute
   134 
   135 lemmas zmult_ac = OrderedGroup.mult_ac
   136 
   137 (*also for the instance declaration int :: comm_monoid_add*)
   138 lemma zadd_0: "(0::int) + z = z"
   139 apply (simp add: Zero_int_def)
   140 apply (cases z, simp add: add)
   141 done
   142 
   143 lemma zadd_0_right: "z + (0::int) = z"
   144 by (rule trans [OF zadd_commute zadd_0])
   145 
   146 lemma zadd_zminus_inverse2: "(- z) + z = (0::int)"
   147 by (cases z, simp add: Zero_int_def minus add)
   148 
   149 
   150 subsection{*Integer Multiplication*}
   151 
   152 text{*Congruence property for multiplication*}
   153 lemma mult_congruent2:
   154      "(%p1 p2. (%(x,y). (%(u,v). intrel``{(x*u + y*v, x*v + y*u)}) p2) p1)
   155       respects2 intrel"
   156 apply (rule equiv_intrel [THEN congruent2_commuteI])
   157  apply (force simp add: mult_ac, clarify) 
   158 apply (simp add: congruent_def mult_ac)  
   159 apply (rename_tac u v w x y z)
   160 apply (subgoal_tac "u*y + x*y = w*y + v*y  &  u*z + x*z = w*z + v*z")
   161 apply (simp add: mult_ac)
   162 apply (simp add: add_mult_distrib [symmetric])
   163 done
   164 
   165 
   166 lemma mult:
   167      "Abs_Integ((intrel``{(x,y)})) * Abs_Integ((intrel``{(u,v)})) =
   168       Abs_Integ(intrel `` {(x*u + y*v, x*v + y*u)})"
   169 by (simp add: mult_int_def UN_UN_split_split_eq mult_congruent2
   170               UN_equiv_class2 [OF equiv_intrel equiv_intrel])
   171 
   172 lemma zmult_zminus: "(- z) * w = - (z * (w::int))"
   173 by (cases z, cases w, simp add: minus mult add_ac)
   174 
   175 lemma zmult_commute: "(z::int) * w = w * z"
   176 by (cases z, cases w, simp add: mult add_ac mult_ac)
   177 
   178 lemma zmult_assoc: "((z1::int) * z2) * z3 = z1 * (z2 * z3)"
   179 by (cases z1, cases z2, cases z3, simp add: mult add_mult_distrib2 mult_ac)
   180 
   181 lemma zadd_zmult_distrib: "((z1::int) + z2) * w = (z1 * w) + (z2 * w)"
   182 by (cases z1, cases z2, cases w, simp add: add mult add_mult_distrib2 mult_ac)
   183 
   184 lemma zadd_zmult_distrib2: "(w::int) * (z1 + z2) = (w * z1) + (w * z2)"
   185 by (simp add: zmult_commute [of w] zadd_zmult_distrib)
   186 
   187 lemma zdiff_zmult_distrib: "((z1::int) - z2) * w = (z1 * w) - (z2 * w)"
   188 by (simp add: diff_int_def zadd_zmult_distrib zmult_zminus)
   189 
   190 lemma zdiff_zmult_distrib2: "(w::int) * (z1 - z2) = (w * z1) - (w * z2)"
   191 by (simp add: zmult_commute [of w] zdiff_zmult_distrib)
   192 
   193 lemmas int_distrib =
   194   zadd_zmult_distrib zadd_zmult_distrib2
   195   zdiff_zmult_distrib zdiff_zmult_distrib2
   196 
   197 
   198 lemma zmult_1: "(1::int) * z = z"
   199 by (cases z, simp add: One_int_def mult)
   200 
   201 lemma zmult_1_right: "z * (1::int) = z"
   202 by (rule trans [OF zmult_commute zmult_1])
   203 
   204 
   205 text{*The integers form a @{text comm_ring_1}*}
   206 instance int :: comm_ring_1
   207 proof
   208   fix i j k :: int
   209   show "(i + j) + k = i + (j + k)" by (simp add: zadd_assoc)
   210   show "i + j = j + i" by (simp add: zadd_commute)
   211   show "0 + i = i" by (rule zadd_0)
   212   show "- i + i = 0" by (rule zadd_zminus_inverse2)
   213   show "i - j = i + (-j)" by (simp add: diff_int_def)
   214   show "(i * j) * k = i * (j * k)" by (rule zmult_assoc)
   215   show "i * j = j * i" by (rule zmult_commute)
   216   show "1 * i = i" by (rule zmult_1) 
   217   show "(i + j) * k = i * k + j * k" by (simp add: int_distrib)
   218   show "0 \<noteq> (1::int)" by (simp add: Zero_int_def One_int_def)
   219 qed
   220 
   221 abbreviation
   222   int :: "nat \<Rightarrow> int"
   223 where
   224   "int \<equiv> of_nat"
   225 
   226 lemma int_def: "int m = Abs_Integ (intrel `` {(m, 0)})"
   227 by (induct m, simp_all add: Zero_int_def One_int_def add)
   228 
   229 
   230 subsection{*The @{text "\<le>"} Ordering*}
   231 
   232 lemma le:
   233   "(Abs_Integ(intrel``{(x,y)}) \<le> Abs_Integ(intrel``{(u,v)})) = (x+v \<le> u+y)"
   234 by (force simp add: le_int_def)
   235 
   236 lemma less:
   237   "(Abs_Integ(intrel``{(x,y)}) < Abs_Integ(intrel``{(u,v)})) = (x+v < u+y)"
   238 by (simp add: less_int_def le order_less_le)
   239 
   240 lemma zle_refl: "w \<le> (w::int)"
   241 by (cases w, simp add: le)
   242 
   243 lemma zle_trans: "[| i \<le> j; j \<le> k |] ==> i \<le> (k::int)"
   244 by (cases i, cases j, cases k, simp add: le)
   245 
   246 lemma zle_anti_sym: "[| z \<le> w; w \<le> z |] ==> z = (w::int)"
   247 by (cases w, cases z, simp add: le)
   248 
   249 instance int :: order
   250   by intro_classes
   251     (assumption |
   252       rule zle_refl zle_trans zle_anti_sym less_int_def [THEN meta_eq_to_obj_eq])+
   253 
   254 lemma zle_linear: "(z::int) \<le> w \<or> w \<le> z"
   255 by (cases z, cases w) (simp add: le linorder_linear)
   256 
   257 instance int :: linorder
   258   by intro_classes (rule zle_linear)
   259 
   260 lemmas zless_linear = linorder_less_linear [where 'a = int]
   261 
   262 
   263 lemma int_0_less_1: "0 < (1::int)"
   264 by (simp add: Zero_int_def One_int_def less)
   265 
   266 lemma int_0_neq_1 [simp]: "0 \<noteq> (1::int)"
   267 by (rule int_0_less_1 [THEN less_imp_neq])
   268 
   269 
   270 subsection{*Monotonicity results*}
   271 
   272 instance int :: pordered_cancel_ab_semigroup_add
   273 proof
   274   fix a b c :: int
   275   show "a \<le> b \<Longrightarrow> c + a \<le> c + b"
   276     by (cases a, cases b, cases c, simp add: le add)
   277 qed
   278 
   279 lemma zadd_left_mono: "i \<le> j ==> k + i \<le> k + (j::int)"
   280 by (rule add_left_mono)
   281 
   282 lemma zadd_strict_right_mono: "i < j ==> i + k < j + (k::int)"
   283 by (rule add_strict_right_mono)
   284 
   285 lemma zadd_zless_mono: "[| w'<w; z'\<le>z |] ==> w' + z' < w + (z::int)"
   286 by (rule add_less_le_mono)
   287 
   288 
   289 subsection{*Strict Monotonicity of Multiplication*}
   290 
   291 text{*strict, in 1st argument; proof is by induction on k>0*}
   292 lemma zmult_zless_mono2_lemma:
   293      "(i::int)<j ==> 0<k ==> of_nat k * i < of_nat k * j"
   294 apply (induct "k", simp)
   295 apply (simp add: left_distrib)
   296 apply (case_tac "k=0")
   297 apply (simp_all add: add_strict_mono)
   298 done
   299 
   300 lemma zero_le_imp_eq_int: "(0::int) \<le> k ==> \<exists>n. k = of_nat n"
   301 apply (cases k)
   302 apply (auto simp add: le add int_def Zero_int_def)
   303 apply (rule_tac x="x-y" in exI, simp)
   304 done
   305 
   306 lemma zero_less_imp_eq_int: "(0::int) < k ==> \<exists>n>0. k = of_nat n"
   307 apply (cases k)
   308 apply (simp add: less int_def Zero_int_def)
   309 apply (rule_tac x="x-y" in exI, simp)
   310 done
   311 
   312 lemma zmult_zless_mono2: "[| i<j;  (0::int) < k |] ==> k*i < k*j"
   313 apply (drule zero_less_imp_eq_int)
   314 apply (auto simp add: zmult_zless_mono2_lemma)
   315 done
   316 
   317 instance int :: minus
   318   zabs_def: "\<bar>i\<Colon>int\<bar> \<equiv> if i < 0 then - i else i" ..
   319 
   320 instance int :: distrib_lattice
   321   "inf \<equiv> min"
   322   "sup \<equiv> max"
   323   by intro_classes
   324     (auto simp add: inf_int_def sup_int_def min_max.sup_inf_distrib1)
   325 
   326 text{*The integers form an ordered integral domain*}
   327 instance int :: ordered_idom
   328 proof
   329   fix i j k :: int
   330   show "i < j ==> 0 < k ==> k * i < k * j" by (rule zmult_zless_mono2)
   331   show "\<bar>i\<bar> = (if i < 0 then -i else i)" by (simp only: zabs_def)
   332 qed
   333 
   334 lemma zless_imp_add1_zle: "w<z ==> w + (1::int) \<le> z"
   335 apply (cases w, cases z) 
   336 apply (simp add: less le add One_int_def)
   337 done
   338 
   339 
   340 subsection{*Magnitude of an Integer, as a Natural Number: @{term nat}*}
   341 
   342 definition
   343   nat :: "int \<Rightarrow> nat"
   344 where
   345   [code func del]: "nat z = contents (\<Union>(x, y) \<in> Rep_Integ z. {x-y})"
   346 
   347 lemma nat: "nat (Abs_Integ (intrel``{(x,y)})) = x-y"
   348 proof -
   349   have "(\<lambda>(x,y). {x-y}) respects intrel"
   350     by (simp add: congruent_def) arith
   351   thus ?thesis
   352     by (simp add: nat_def UN_equiv_class [OF equiv_intrel])
   353 qed
   354 
   355 lemma nat_int [simp]: "nat (int n) = n"
   356 by (simp add: nat int_def)
   357 
   358 lemma nat_zero [simp]: "nat 0 = 0"
   359 by (simp add: Zero_int_def nat)
   360 
   361 lemma int_nat_eq [simp]: "int (nat z) = (if 0 \<le> z then z else 0)"
   362 by (cases z, simp add: nat le int_def Zero_int_def)
   363 
   364 corollary nat_0_le: "0 \<le> z ==> int (nat z) = z"
   365 by simp
   366 
   367 lemma nat_le_0 [simp]: "z \<le> 0 ==> nat z = 0"
   368 by (cases z, simp add: nat le Zero_int_def)
   369 
   370 lemma nat_le_eq_zle: "0 < w | 0 \<le> z ==> (nat w \<le> nat z) = (w\<le>z)"
   371 apply (cases w, cases z) 
   372 apply (simp add: nat le linorder_not_le [symmetric] Zero_int_def, arith)
   373 done
   374 
   375 text{*An alternative condition is @{term "0 \<le> w"} *}
   376 corollary nat_mono_iff: "0 < z ==> (nat w < nat z) = (w < z)"
   377 by (simp add: nat_le_eq_zle linorder_not_le [symmetric]) 
   378 
   379 corollary nat_less_eq_zless: "0 \<le> w ==> (nat w < nat z) = (w<z)"
   380 by (simp add: nat_le_eq_zle linorder_not_le [symmetric]) 
   381 
   382 lemma zless_nat_conj [simp]: "(nat w < nat z) = (0 < z & w < z)"
   383 apply (cases w, cases z) 
   384 apply (simp add: nat le Zero_int_def linorder_not_le [symmetric], arith)
   385 done
   386 
   387 lemma nonneg_eq_int: "[| 0 \<le> z;  !!m. z = int m ==> P |] ==> P"
   388 by (blast dest: nat_0_le sym)
   389 
   390 lemma nat_eq_iff: "(nat w = m) = (if 0 \<le> w then w = int m else m=0)"
   391 by (cases w, simp add: nat le int_def Zero_int_def, arith)
   392 
   393 corollary nat_eq_iff2: "(m = nat w) = (if 0 \<le> w then w = int m else m=0)"
   394 by (simp only: eq_commute [of m] nat_eq_iff)
   395 
   396 lemma nat_less_iff: "0 \<le> w ==> (nat w < m) = (w < int m)"
   397 apply (cases w)
   398 apply (simp add: nat le int_def Zero_int_def linorder_not_le [symmetric], arith)
   399 done
   400 
   401 lemma int_eq_iff: "(int m = z) = (m = nat z & 0 \<le> z)"
   402 by (auto simp add: nat_eq_iff2)
   403 
   404 lemma zero_less_nat_eq [simp]: "(0 < nat z) = (0 < z)"
   405 by (insert zless_nat_conj [of 0], auto)
   406 
   407 lemma nat_add_distrib:
   408      "[| (0::int) \<le> z;  0 \<le> z' |] ==> nat (z+z') = nat z + nat z'"
   409 by (cases z, cases z', simp add: nat add le Zero_int_def)
   410 
   411 lemma nat_diff_distrib:
   412      "[| (0::int) \<le> z';  z' \<le> z |] ==> nat (z-z') = nat z - nat z'"
   413 by (cases z, cases z', 
   414     simp add: nat add minus diff_minus le Zero_int_def)
   415 
   416 lemma nat_zminus_int [simp]: "nat (- (int n)) = 0"
   417 by (simp add: int_def minus nat Zero_int_def) 
   418 
   419 lemma zless_nat_eq_int_zless: "(m < nat z) = (int m < z)"
   420 by (cases z, simp add: nat less int_def, arith)
   421 
   422 
   423 subsection{*Lemmas about the Function @{term int} and Orderings*}
   424 
   425 lemma negative_zless_0: "- (int (Suc n)) < 0"
   426 by (simp add: order_less_le del: of_nat_Suc)
   427 
   428 lemma negative_zless [iff]: "- (int (Suc n)) < int m"
   429 by (rule negative_zless_0 [THEN order_less_le_trans], simp)
   430 
   431 lemma negative_zle_0: "- int n \<le> 0"
   432 by (simp add: minus_le_iff)
   433 
   434 lemma negative_zle [iff]: "- int n \<le> int m"
   435 by (rule order_trans [OF negative_zle_0 of_nat_0_le_iff])
   436 
   437 lemma not_zle_0_negative [simp]: "~ (0 \<le> - (int (Suc n)))"
   438 by (subst le_minus_iff, simp del: of_nat_Suc)
   439 
   440 lemma int_zle_neg: "(int n \<le> - int m) = (n = 0 & m = 0)"
   441 by (simp add: int_def le minus Zero_int_def)
   442 
   443 lemma not_int_zless_negative [simp]: "~ (int n < - int m)"
   444 by (simp add: linorder_not_less)
   445 
   446 lemma negative_eq_positive [simp]: "(- int n = int m) = (n = 0 & m = 0)"
   447 by (force simp add: order_eq_iff [of "- int n"] int_zle_neg)
   448 
   449 lemma zle_iff_zadd: "(w \<le> z) = (\<exists>n. z = w + int n)"
   450 proof (cases w, cases z, simp add: le add int_def)
   451   fix a b c d
   452   assume "w = Abs_Integ (intrel `` {(a,b)})" "z = Abs_Integ (intrel `` {(c,d)})"
   453   show "(a+d \<le> c+b) = (\<exists>n. c+b = a+n+d)"
   454   proof
   455     assume "a + d \<le> c + b" 
   456     thus "\<exists>n. c + b = a + n + d" 
   457       by (auto intro!: exI [where x="c+b - (a+d)"])
   458   next    
   459     assume "\<exists>n. c + b = a + n + d" 
   460     then obtain n where "c + b = a + n + d" ..
   461     thus "a + d \<le> c + b" by arith
   462   qed
   463 qed
   464 
   465 lemma abs_of_nat [simp]: "\<bar>of_nat n::'a::ordered_idom\<bar> = of_nat n"
   466 by (rule  of_nat_0_le_iff [THEN abs_of_nonneg]) (* belongs in Nat.thy *)
   467 
   468 text{*This version is proved for all ordered rings, not just integers!
   469       It is proved here because attribute @{text arith_split} is not available
   470       in theory @{text Ring_and_Field}.
   471       But is it really better than just rewriting with @{text abs_if}?*}
   472 lemma abs_split [arith_split]:
   473      "P(abs(a::'a::ordered_idom)) = ((0 \<le> a --> P a) & (a < 0 --> P(-a)))"
   474 by (force dest: order_less_le_trans simp add: abs_if linorder_not_less)
   475 
   476 
   477 subsection {* Constants @{term neg} and @{term iszero} *}
   478 
   479 definition
   480   neg  :: "'a\<Colon>ordered_idom \<Rightarrow> bool"
   481 where
   482   [code inline]: "neg Z \<longleftrightarrow> Z < 0"
   483 
   484 definition (*for simplifying equalities*)
   485   iszero :: "'a\<Colon>semiring_1 \<Rightarrow> bool"
   486 where
   487   "iszero z \<longleftrightarrow> z = 0"
   488 
   489 lemma not_neg_int [simp]: "~ neg (int n)"
   490 by (simp add: neg_def)
   491 
   492 lemma neg_zminus_int [simp]: "neg (- (int (Suc n)))"
   493 by (simp add: neg_def neg_less_0_iff_less del: of_nat_Suc)
   494 
   495 lemmas neg_eq_less_0 = neg_def
   496 
   497 lemma not_neg_eq_ge_0: "(~neg x) = (0 \<le> x)"
   498 by (simp add: neg_def linorder_not_less)
   499 
   500 
   501 subsection{*To simplify inequalities when Numeral1 can get simplified to 1*}
   502 
   503 lemma not_neg_0: "~ neg 0"
   504 by (simp add: One_int_def neg_def)
   505 
   506 lemma not_neg_1: "~ neg 1"
   507 by (simp add: neg_def linorder_not_less zero_le_one)
   508 
   509 lemma iszero_0: "iszero 0"
   510 by (simp add: iszero_def)
   511 
   512 lemma not_iszero_1: "~ iszero 1"
   513 by (simp add: iszero_def eq_commute)
   514 
   515 lemma neg_nat: "neg z ==> nat z = 0"
   516 by (simp add: neg_def order_less_imp_le) 
   517 
   518 lemma not_neg_nat: "~ neg z ==> int (nat z) = z"
   519 by (simp add: linorder_not_less neg_def)
   520 
   521 
   522 subsection{*The Set of Natural Numbers*}
   523 
   524 constdefs
   525   Nats  :: "'a::semiring_1 set"
   526   "Nats == range of_nat"
   527 
   528 notation (xsymbols)
   529   Nats  ("\<nat>")
   530 
   531 lemma of_nat_in_Nats [simp]: "of_nat n \<in> Nats"
   532 by (simp add: Nats_def)
   533 
   534 lemma Nats_0 [simp]: "0 \<in> Nats"
   535 apply (simp add: Nats_def)
   536 apply (rule range_eqI)
   537 apply (rule of_nat_0 [symmetric])
   538 done
   539 
   540 lemma Nats_1 [simp]: "1 \<in> Nats"
   541 apply (simp add: Nats_def)
   542 apply (rule range_eqI)
   543 apply (rule of_nat_1 [symmetric])
   544 done
   545 
   546 lemma Nats_add [simp]: "[|a \<in> Nats; b \<in> Nats|] ==> a+b \<in> Nats"
   547 apply (auto simp add: Nats_def)
   548 apply (rule range_eqI)
   549 apply (rule of_nat_add [symmetric])
   550 done
   551 
   552 lemma Nats_mult [simp]: "[|a \<in> Nats; b \<in> Nats|] ==> a*b \<in> Nats"
   553 apply (auto simp add: Nats_def)
   554 apply (rule range_eqI)
   555 apply (rule of_nat_mult [symmetric])
   556 done
   557 
   558 lemma of_nat_eq_id [simp]: "of_nat = (id :: nat => nat)"
   559 proof
   560   fix n
   561   show "of_nat n = id n"  by (induct n, simp_all)
   562 qed (* belongs in Nat.thy *)
   563 
   564 
   565 subsection{*Embedding of the Integers into any @{text ring_1}:
   566 @{term of_int}*}
   567 
   568 constdefs
   569    of_int :: "int => 'a::ring_1"
   570    "of_int z == contents (\<Union>(i,j) \<in> Rep_Integ z. { of_nat i - of_nat j })"
   571 
   572 
   573 lemma of_int: "of_int (Abs_Integ (intrel `` {(i,j)})) = of_nat i - of_nat j"
   574 proof -
   575   have "(\<lambda>(i,j). { of_nat i - (of_nat j :: 'a) }) respects intrel"
   576     by (simp add: congruent_def compare_rls of_nat_add [symmetric]
   577             del: of_nat_add) 
   578   thus ?thesis
   579     by (simp add: of_int_def UN_equiv_class [OF equiv_intrel])
   580 qed
   581 
   582 lemma of_int_0 [simp]: "of_int 0 = 0"
   583 by (simp add: of_int Zero_int_def)
   584 
   585 lemma of_int_1 [simp]: "of_int 1 = 1"
   586 by (simp add: of_int One_int_def)
   587 
   588 lemma of_int_add [simp]: "of_int (w+z) = of_int w + of_int z"
   589 by (cases w, cases z, simp add: compare_rls of_int add)
   590 
   591 lemma of_int_minus [simp]: "of_int (-z) = - (of_int z)"
   592 by (cases z, simp add: compare_rls of_int minus)
   593 
   594 lemma of_int_diff [simp]: "of_int (w-z) = of_int w - of_int z"
   595 by (simp add: diff_minus)
   596 
   597 lemma of_int_mult [simp]: "of_int (w*z) = of_int w * of_int z"
   598 apply (cases w, cases z)
   599 apply (simp add: compare_rls of_int left_diff_distrib right_diff_distrib
   600                  mult add_ac)
   601 done
   602 
   603 lemma of_int_le_iff [simp]:
   604      "(of_int w \<le> (of_int z::'a::ordered_idom)) = (w \<le> z)"
   605 apply (cases w)
   606 apply (cases z)
   607 apply (simp add: compare_rls of_int le diff_int_def add minus
   608                  of_nat_add [symmetric]   del: of_nat_add)
   609 done
   610 
   611 text{*Special cases where either operand is zero*}
   612 lemmas of_int_0_le_iff [simp] = of_int_le_iff [of 0, simplified]
   613 lemmas of_int_le_0_iff [simp] = of_int_le_iff [of _ 0, simplified]
   614 
   615 
   616 lemma of_int_less_iff [simp]:
   617      "(of_int w < (of_int z::'a::ordered_idom)) = (w < z)"
   618 by (simp add: linorder_not_le [symmetric])
   619 
   620 text{*Special cases where either operand is zero*}
   621 lemmas of_int_0_less_iff [simp] = of_int_less_iff [of 0, simplified]
   622 lemmas of_int_less_0_iff [simp] = of_int_less_iff [of _ 0, simplified]
   623 
   624 text{*Class for unital rings with characteristic zero.
   625  Includes non-ordered rings like the complex numbers.*}
   626 axclass ring_char_0 < ring_1, semiring_char_0
   627 
   628 lemma of_int_eq_iff [simp]:
   629      "(of_int w = (of_int z::'a::ring_char_0)) = (w = z)"
   630 apply (cases w, cases z, simp add: of_int)
   631 apply (simp only: diff_eq_eq diff_add_eq eq_diff_eq)
   632 apply (simp only: of_nat_add [symmetric] of_nat_eq_iff)
   633 done
   634 
   635 text{*Every @{text ordered_idom} has characteristic zero.*}
   636 instance ordered_idom < ring_char_0 ..
   637 
   638 text{*Special cases where either operand is zero*}
   639 lemmas of_int_0_eq_iff [simp] = of_int_eq_iff [of 0, simplified]
   640 lemmas of_int_eq_0_iff [simp] = of_int_eq_iff [of _ 0, simplified]
   641 
   642 lemma of_int_eq_id [simp]: "of_int = (id :: int => int)"
   643 proof
   644   fix z
   645   show "of_int z = id z"
   646     by (cases z)
   647       (simp add: of_int add minus int_def diff_minus)
   648 qed
   649 
   650 
   651 subsection{*The Set of Integers*}
   652 
   653 constdefs
   654   Ints  :: "'a::ring_1 set"
   655   "Ints == range of_int"
   656 
   657 notation (xsymbols)
   658   Ints  ("\<int>")
   659 
   660 lemma Ints_0 [simp]: "0 \<in> Ints"
   661 apply (simp add: Ints_def)
   662 apply (rule range_eqI)
   663 apply (rule of_int_0 [symmetric])
   664 done
   665 
   666 lemma Ints_1 [simp]: "1 \<in> Ints"
   667 apply (simp add: Ints_def)
   668 apply (rule range_eqI)
   669 apply (rule of_int_1 [symmetric])
   670 done
   671 
   672 lemma Ints_add [simp]: "[|a \<in> Ints; b \<in> Ints|] ==> a+b \<in> Ints"
   673 apply (auto simp add: Ints_def)
   674 apply (rule range_eqI)
   675 apply (rule of_int_add [symmetric])
   676 done
   677 
   678 lemma Ints_minus [simp]: "a \<in> Ints ==> -a \<in> Ints"
   679 apply (auto simp add: Ints_def)
   680 apply (rule range_eqI)
   681 apply (rule of_int_minus [symmetric])
   682 done
   683 
   684 lemma Ints_diff [simp]: "[|a \<in> Ints; b \<in> Ints|] ==> a-b \<in> Ints"
   685 apply (auto simp add: Ints_def)
   686 apply (rule range_eqI)
   687 apply (rule of_int_diff [symmetric])
   688 done
   689 
   690 lemma Ints_mult [simp]: "[|a \<in> Ints; b \<in> Ints|] ==> a*b \<in> Ints"
   691 apply (auto simp add: Ints_def)
   692 apply (rule range_eqI)
   693 apply (rule of_int_mult [symmetric])
   694 done
   695 
   696 text{*Collapse nested embeddings*}
   697 lemma of_int_of_nat_eq [simp]: "of_int (of_nat n) = of_nat n"
   698 by (induct n, auto)
   699 
   700 lemma Ints_cases [cases set: Ints]:
   701   assumes "q \<in> \<int>"
   702   obtains (of_int) z where "q = of_int z"
   703   unfolding Ints_def
   704 proof -
   705   from `q \<in> \<int>` have "q \<in> range of_int" unfolding Ints_def .
   706   then obtain z where "q = of_int z" ..
   707   then show thesis ..
   708 qed
   709 
   710 lemma Ints_induct [case_names of_int, induct set: Ints]:
   711   "q \<in> \<int> ==> (!!z. P (of_int z)) ==> P q"
   712   by (rule Ints_cases) auto
   713 
   714 
   715 (* int (Suc n) = 1 + int n *)
   716 
   717 
   718 
   719 subsection{*More Properties of @{term setsum} and  @{term setprod}*}
   720 
   721 text{*By Jeremy Avigad*}
   722 
   723 
   724 lemma of_nat_setsum: "of_nat (setsum f A) = (\<Sum>x\<in>A. of_nat(f x))"
   725   apply (cases "finite A")
   726   apply (erule finite_induct, auto)
   727   done
   728 
   729 lemma of_int_setsum: "of_int (setsum f A) = (\<Sum>x\<in>A. of_int(f x))"
   730   apply (cases "finite A")
   731   apply (erule finite_induct, auto)
   732   done
   733 
   734 lemma of_nat_setprod: "of_nat (setprod f A) = (\<Prod>x\<in>A. of_nat(f x))"
   735   apply (cases "finite A")
   736   apply (erule finite_induct, auto)
   737   done
   738 
   739 lemma of_int_setprod: "of_int (setprod f A) = (\<Prod>x\<in>A. of_int(f x))"
   740   apply (cases "finite A")
   741   apply (erule finite_induct, auto)
   742   done
   743 
   744 lemma setprod_nonzero_nat:
   745     "finite A ==> (\<forall>x \<in> A. f x \<noteq> (0::nat)) ==> setprod f A \<noteq> 0"
   746   by (rule setprod_nonzero, auto)
   747 
   748 lemma setprod_zero_eq_nat:
   749     "finite A ==> (setprod f A = (0::nat)) = (\<exists>x \<in> A. f x = 0)"
   750   by (rule setprod_zero_eq, auto)
   751 
   752 lemma setprod_nonzero_int:
   753     "finite A ==> (\<forall>x \<in> A. f x \<noteq> (0::int)) ==> setprod f A \<noteq> 0"
   754   by (rule setprod_nonzero, auto)
   755 
   756 lemma setprod_zero_eq_int:
   757     "finite A ==> (setprod f A = (0::int)) = (\<exists>x \<in> A. f x = 0)"
   758   by (rule setprod_zero_eq, auto)
   759 
   760 
   761 subsection {* Further properties *}
   762 
   763 text{*Now we replace the case analysis rule by a more conventional one:
   764 whether an integer is negative or not.*}
   765 
   766 lemma zless_iff_Suc_zadd:
   767     "(w < z) = (\<exists>n. z = w + int (Suc n))"
   768 apply (cases z, cases w)
   769 apply (auto simp add: le add int_def linorder_not_le [symmetric]) 
   770 apply (rename_tac a b c d) 
   771 apply (rule_tac x="a+d - Suc(c+b)" in exI) 
   772 apply arith
   773 done
   774 
   775 lemma negD: "x<0 ==> \<exists>n. x = - (int (Suc n))"
   776 apply (cases x)
   777 apply (auto simp add: le minus Zero_int_def int_def order_less_le)
   778 apply (rule_tac x="y - Suc x" in exI, arith)
   779 done
   780 
   781 theorem int_cases [cases type: int, case_names nonneg neg]:
   782      "[|!! n. z = int n ==> P;  !! n. z =  - (int (Suc n)) ==> P |] ==> P"
   783 apply (cases "z < 0", blast dest!: negD)
   784 apply (simp add: linorder_not_less del: of_nat_Suc)
   785 apply (blast dest: nat_0_le [THEN sym])
   786 done
   787 
   788 theorem int_induct'[induct type: int, case_names nonneg neg]:
   789      "[|!! n. P (int n);  !!n. P (- (int (Suc n))) |] ==> P z"
   790   by (cases z rule: int_cases) auto
   791 
   792 text{*Contributed by Brian Huffman*}
   793 theorem int_diff_cases [case_names diff]:
   794 assumes prem: "!!m n. z = int m - int n ==> P" shows "P"
   795 apply (cases z rule: eq_Abs_Integ)
   796 apply (rule_tac m=x and n=y in prem)
   797 apply (simp add: int_def diff_def minus add)
   798 done
   799 
   800 lemma of_nat_nat: "0 \<le> z ==> of_nat (nat z) = of_int z"
   801 by (cases z rule: eq_Abs_Integ, simp add: nat le of_int Zero_int_def)
   802 
   803 
   804 subsection {* Legacy theorems *}
   805 
   806 lemma zadd_int_left: "(int m) + (int n + z) = int (m + n) + z"
   807 by simp
   808 
   809 lemma int_Suc: "int (Suc m) = 1 + (int m)"
   810 by simp
   811 
   812 lemma int_Suc0_eq_1: "int (Suc 0) = 1"
   813 by simp
   814 
   815 lemmas inj_int = inj_of_nat [where 'a=int]
   816 lemmas int_int_eq = of_nat_eq_iff [where 'a=int]
   817 lemmas zadd_int = of_nat_add [where 'a=int, symmetric]
   818 lemmas int_mult = of_nat_mult [where 'a=int]
   819 lemmas zmult_int = of_nat_mult [where 'a=int, symmetric]
   820 lemmas int_eq_0_conv = of_nat_eq_0_iff [where 'a=int]
   821 lemmas zless_int = of_nat_less_iff [where 'a=int]
   822 lemmas int_less_0_conv = of_nat_less_0_iff [where 'a=int]
   823 lemmas zero_less_int_conv = of_nat_0_less_iff [where 'a=int]
   824 lemmas zle_int = of_nat_le_iff [where 'a=int]
   825 lemmas zero_zle_int = of_nat_0_le_iff [where 'a=int]
   826 lemmas int_le_0_conv = of_nat_le_0_iff [where 'a=int]
   827 lemmas int_0 = of_nat_0 [where ?'a_1.0=int]
   828 lemmas int_1 = of_nat_1 [where 'a=int]
   829 lemmas abs_int_eq = abs_of_nat [where 'a=int]
   830 lemmas of_int_int_eq = of_int_of_nat_eq [where 'a=int]
   831 lemmas int_setsum = of_nat_setsum [where 'a=int]
   832 lemmas int_setprod = of_nat_setprod [where 'a=int]
   833 lemmas zdiff_int = of_nat_diff [where 'a=int, symmetric]
   834 lemmas zless_le = less_int_def [THEN meta_eq_to_obj_eq]
   835 lemmas int_eq_of_nat = TrueI
   836 
   837 abbreviation
   838   int_of_nat :: "nat \<Rightarrow> int"
   839 where
   840   "int_of_nat \<equiv> of_nat"
   841 
   842 end