src/HOL/Int.thy
changeset 48045 fbf77fdf9ae4
parent 48044 fea6f3060b65
child 48066 c6783c9b87bf
equal deleted inserted replaced
48044:fea6f3060b65 48045:fbf77fdf9ae4
     4 *)
     4 *)
     5 
     5 
     6 header {* The Integers as Equivalence Classes over Pairs of Natural Numbers *} 
     6 header {* The Integers as Equivalence Classes over Pairs of Natural Numbers *} 
     7 
     7 
     8 theory Int
     8 theory Int
     9 imports Equiv_Relations Wellfounded
     9 imports Equiv_Relations Wellfounded Quotient
    10 uses
    10 uses
    11   ("Tools/int_arith.ML")
    11   ("Tools/int_arith.ML")
    12 begin
    12 begin
    13 
    13 
    14 subsection {* The equivalence relation underlying the integers *}
    14 subsection {* Definition of integers as a quotient type *}
    15 
    15 
    16 definition intrel :: "((nat \<times> nat) \<times> (nat \<times> nat)) set" where
    16 definition intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" where
    17   "intrel = {((x, y), (u, v)) | x y u v. x + v = u +y }"
    17   "intrel = (\<lambda>(x, y) (u, v). x + v = u + y)"
    18 
    18 
    19 definition "Integ = UNIV//intrel"
    19 lemma intrel_iff [simp]: "intrel (x, y) (u, v) \<longleftrightarrow> x + v = u + y"
    20 
    20   by (simp add: intrel_def)
    21 typedef (open) int = Integ
    21 
       
    22 quotient_type int = "nat \<times> nat" / "intrel"
    22   morphisms Rep_Integ Abs_Integ
    23   morphisms Rep_Integ Abs_Integ
    23   unfolding Integ_def by (auto simp add: quotient_def)
    24 proof (rule equivpI)
    24 
    25   show "reflp intrel"
    25 instantiation int :: "{zero, one, plus, minus, uminus, times, ord, abs, sgn}"
    26     unfolding reflp_def by auto
       
    27   show "symp intrel"
       
    28     unfolding symp_def by auto
       
    29   show "transp intrel"
       
    30     unfolding transp_def by auto
       
    31 qed
       
    32 
       
    33 lemma eq_Abs_Integ [case_names Abs_Integ, cases type: int]:
       
    34      "(!!x y. z = Abs_Integ (x, y) ==> P) ==> P"
       
    35 by (induct z) auto
       
    36 
       
    37 subsection {* Integers form a commutative ring *}
       
    38 
       
    39 instantiation int :: comm_ring_1
    26 begin
    40 begin
    27 
    41 
    28 definition
    42 lift_definition zero_int :: "int" is "(0, 0)"
    29   Zero_int_def: "0 = Abs_Integ (intrel `` {(0, 0)})"
    43   by simp
    30 
    44 
    31 definition
    45 lift_definition one_int :: "int" is "(1, 0)"
    32   One_int_def: "1 = Abs_Integ (intrel `` {(1, 0)})"
    46   by simp
    33 
    47 
    34 definition
    48 lift_definition plus_int :: "int \<Rightarrow> int \<Rightarrow> int"
    35   add_int_def: "z + w = Abs_Integ
    49   is "\<lambda>(x, y) (u, v). (x + u, y + v)"
    36     (\<Union>(x, y) \<in> Rep_Integ z. \<Union>(u, v) \<in> Rep_Integ w.
    50   by clarsimp
    37       intrel `` {(x + u, y + v)})"
    51 
    38 
    52 lift_definition uminus_int :: "int \<Rightarrow> int"
    39 definition
    53   is "\<lambda>(x, y). (y, x)"
    40   minus_int_def:
    54   by clarsimp
    41     "- z = Abs_Integ (\<Union>(x, y) \<in> Rep_Integ z. intrel `` {(y, x)})"
    55 
    42 
    56 lift_definition minus_int :: "int \<Rightarrow> int \<Rightarrow> int"
    43 definition
    57   is "\<lambda>(x, y) (u, v). (x + v, y + u)"
    44   diff_int_def:  "z - w = z + (-w \<Colon> int)"
    58   by clarsimp
    45 
    59 
    46 definition
    60 lift_definition times_int :: "int \<Rightarrow> int \<Rightarrow> int"
    47   mult_int_def: "z * w = Abs_Integ
    61   is "\<lambda>(x, y) (u, v). (x*u + y*v, x*v + y*u)"
    48     (\<Union>(x, y) \<in> Rep_Integ z. \<Union>(u,v ) \<in> Rep_Integ w.
    62 proof (clarsimp)
    49       intrel `` {(x*u + y*v, x*v + y*u)})"
    63   fix s t u v w x y z :: nat
    50 
    64   assume "s + v = u + t" and "w + z = y + x"
    51 definition
    65   hence "(s + v) * w + (u + t) * x + u * (w + z) + v * (y + x)
    52   le_int_def:
    66        = (u + t) * w + (s + v) * x + u * (y + x) + v * (w + z)"
    53    "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)"
    67     by simp
    54 
    68   thus "(s * w + t * x) + (u * z + v * y) = (u * y + v * z) + (s * x + t * w)"
    55 definition
    69     by (simp add: algebra_simps)
    56   less_int_def: "(z\<Colon>int) < w \<longleftrightarrow> z \<le> w \<and> z \<noteq> w"
    70 qed
    57 
    71 
    58 definition
    72 instance
    59   zabs_def: "\<bar>i\<Colon>int\<bar> = (if i < 0 then - i else i)"
    73   by default (transfer, clarsimp simp: algebra_simps)+
    60 
       
    61 definition
       
    62   zsgn_def: "sgn (i\<Colon>int) = (if i=0 then 0 else if 0<i then 1 else - 1)"
       
    63 
       
    64 instance ..
       
    65 
    74 
    66 end
    75 end
    67 
       
    68 
       
    69 subsection{*Construction of the Integers*}
       
    70 
       
    71 lemma intrel_iff [simp]: "(((x,y),(u,v)) \<in> intrel) = (x+v = u+y)"
       
    72 by (simp add: intrel_def)
       
    73 
       
    74 lemma equiv_intrel: "equiv UNIV intrel"
       
    75 by (simp add: intrel_def equiv_def refl_on_def sym_def trans_def)
       
    76 
       
    77 text{*Reduces equality of equivalence classes to the @{term intrel} relation:
       
    78   @{term "(intrel `` {x} = intrel `` {y}) = ((x,y) \<in> intrel)"} *}
       
    79 lemmas equiv_intrel_iff [simp] = eq_equiv_class_iff [OF equiv_intrel UNIV_I UNIV_I]
       
    80 
       
    81 text{*All equivalence classes belong to set of representatives*}
       
    82 lemma [simp]: "intrel``{(x,y)} \<in> Integ"
       
    83 by (auto simp add: Integ_def intrel_def quotient_def)
       
    84 
       
    85 text{*Reduces equality on abstractions to equality on representatives:
       
    86   @{prop "\<lbrakk>x \<in> Integ; y \<in> Integ\<rbrakk> \<Longrightarrow> (Abs_Integ x = Abs_Integ y) = (x=y)"} *}
       
    87 declare Abs_Integ_inject [simp,no_atp]  Abs_Integ_inverse [simp,no_atp]
       
    88 
       
    89 text{*Case analysis on the representation of an integer as an equivalence
       
    90       class of pairs of naturals.*}
       
    91 lemma eq_Abs_Integ [case_names Abs_Integ, cases type: int]:
       
    92      "(!!x y. z = Abs_Integ(intrel``{(x,y)}) ==> P) ==> P"
       
    93 apply (rule Abs_Integ_cases [of z]) 
       
    94 apply (auto simp add: Integ_def quotient_def) 
       
    95 done
       
    96 
       
    97 
       
    98 subsection {* Arithmetic Operations *}
       
    99 
       
   100 lemma minus: "- Abs_Integ(intrel``{(x,y)}) = Abs_Integ(intrel `` {(y,x)})"
       
   101 proof -
       
   102   have "(\<lambda>(x,y). intrel``{(y,x)}) respects intrel"
       
   103     by (auto simp add: congruent_def)
       
   104   thus ?thesis
       
   105     by (simp add: minus_int_def UN_equiv_class [OF equiv_intrel])
       
   106 qed
       
   107 
       
   108 lemma add:
       
   109      "Abs_Integ (intrel``{(x,y)}) + Abs_Integ (intrel``{(u,v)}) =
       
   110       Abs_Integ (intrel``{(x+u, y+v)})"
       
   111 proof -
       
   112   have "(\<lambda>z w. (\<lambda>(x,y). (\<lambda>(u,v). intrel `` {(x+u, y+v)}) w) z) 
       
   113         respects2 intrel"
       
   114     by (auto simp add: congruent2_def)
       
   115   thus ?thesis
       
   116     by (simp add: add_int_def UN_UN_split_split_eq
       
   117                   UN_equiv_class2 [OF equiv_intrel equiv_intrel])
       
   118 qed
       
   119 
       
   120 text{*Congruence property for multiplication*}
       
   121 lemma mult_congruent2:
       
   122      "(%p1 p2. (%(x,y). (%(u,v). intrel``{(x*u + y*v, x*v + y*u)}) p2) p1)
       
   123       respects2 intrel"
       
   124 apply (rule equiv_intrel [THEN congruent2_commuteI])
       
   125  apply (force simp add: mult_ac, clarify) 
       
   126 apply (simp add: congruent_def mult_ac)  
       
   127 apply (rename_tac u v w x y z)
       
   128 apply (subgoal_tac "u*y + x*y = w*y + v*y  &  u*z + x*z = w*z + v*z")
       
   129 apply (simp add: mult_ac)
       
   130 apply (simp add: add_mult_distrib [symmetric])
       
   131 done
       
   132 
       
   133 lemma mult:
       
   134      "Abs_Integ((intrel``{(x,y)})) * Abs_Integ((intrel``{(u,v)})) =
       
   135       Abs_Integ(intrel `` {(x*u + y*v, x*v + y*u)})"
       
   136 by (simp add: mult_int_def UN_UN_split_split_eq mult_congruent2
       
   137               UN_equiv_class2 [OF equiv_intrel equiv_intrel])
       
   138 
       
   139 text{*The integers form a @{text comm_ring_1}*}
       
   140 instance int :: comm_ring_1
       
   141 proof
       
   142   fix i j k :: int
       
   143   show "(i + j) + k = i + (j + k)"
       
   144     by (cases i, cases j, cases k) (simp add: add add_assoc)
       
   145   show "i + j = j + i" 
       
   146     by (cases i, cases j) (simp add: add_ac add)
       
   147   show "0 + i = i"
       
   148     by (cases i) (simp add: Zero_int_def add)
       
   149   show "- i + i = 0"
       
   150     by (cases i) (simp add: Zero_int_def minus add)
       
   151   show "i - j = i + - j"
       
   152     by (simp add: diff_int_def)
       
   153   show "(i * j) * k = i * (j * k)"
       
   154     by (cases i, cases j, cases k) (simp add: mult algebra_simps)
       
   155   show "i * j = j * i"
       
   156     by (cases i, cases j) (simp add: mult algebra_simps)
       
   157   show "1 * i = i"
       
   158     by (cases i) (simp add: One_int_def mult)
       
   159   show "(i + j) * k = i * k + j * k"
       
   160     by (cases i, cases j, cases k) (simp add: add mult algebra_simps)
       
   161   show "0 \<noteq> (1::int)"
       
   162     by (simp add: Zero_int_def One_int_def)
       
   163 qed
       
   164 
    76 
   165 abbreviation int :: "nat \<Rightarrow> int" where
    77 abbreviation int :: "nat \<Rightarrow> int" where
   166   "int \<equiv> of_nat"
    78   "int \<equiv> of_nat"
   167 
    79 
   168 lemma int_def: "int m = Abs_Integ (intrel `` {(m, 0)})"
    80 lemma int_def: "int n = Abs_Integ (n, 0)"
   169 by (induct m) (simp_all add: Zero_int_def One_int_def add)
    81   by (induct n, simp add: zero_int.abs_eq,
   170 
    82     simp add: one_int.abs_eq plus_int.abs_eq)
   171 
    83 
   172 subsection {* The @{text "\<le>"} Ordering *}
    84 lemma int_transfer [transfer_rule]:
   173 
    85   "(fun_rel (op =) cr_int) (\<lambda>n. (n, 0)) int"
   174 lemma le:
    86   unfolding fun_rel_def cr_int_def int_def by simp
   175   "(Abs_Integ(intrel``{(x,y)}) \<le> Abs_Integ(intrel``{(u,v)})) = (x+v \<le> u+y)"
    87 
   176 by (force simp add: le_int_def)
    88 lemma int_diff_cases:
   177 
    89   obtains (diff) m n where "z = int m - int n"
   178 lemma less:
    90   by transfer clarsimp
   179   "(Abs_Integ(intrel``{(x,y)}) < Abs_Integ(intrel``{(u,v)})) = (x+v < u+y)"
    91 
   180 by (simp add: less_int_def le order_less_le)
    92 subsection {* Integers are totally ordered *}
   181 
    93 
   182 instance int :: linorder
    94 instantiation int :: linorder
   183 proof
    95 begin
   184   fix i j k :: int
    96 
   185   show antisym: "i \<le> j \<Longrightarrow> j \<le> i \<Longrightarrow> i = j"
    97 lift_definition less_eq_int :: "int \<Rightarrow> int \<Rightarrow> bool"
   186     by (cases i, cases j) (simp add: le)
    98   is "\<lambda>(x, y) (u, v). x + v \<le> u + y"
   187   show "(i < j) = (i \<le> j \<and> \<not> j \<le> i)"
    99   by auto
   188     by (auto simp add: less_int_def dest: antisym) 
   100 
   189   show "i \<le> i"
   101 lift_definition less_int :: "int \<Rightarrow> int \<Rightarrow> bool"
   190     by (cases i) (simp add: le)
   102   is "\<lambda>(x, y) (u, v). x + v < u + y"
   191   show "i \<le> j \<Longrightarrow> j \<le> k \<Longrightarrow> i \<le> k"
   103   by auto
   192     by (cases i, cases j, cases k) (simp add: le)
   104 
   193   show "i \<le> j \<or> j \<le> i"
   105 instance
   194     by (cases i, cases j) (simp add: le linorder_linear)
   106   by default (transfer, force)+
   195 qed
   107 
       
   108 end
   196 
   109 
   197 instantiation int :: distrib_lattice
   110 instantiation int :: distrib_lattice
   198 begin
   111 begin
   199 
   112 
   200 definition
   113 definition
   206 instance
   119 instance
   207   by intro_classes
   120   by intro_classes
   208     (auto simp add: inf_int_def sup_int_def min_max.sup_inf_distrib1)
   121     (auto simp add: inf_int_def sup_int_def min_max.sup_inf_distrib1)
   209 
   122 
   210 end
   123 end
       
   124 
       
   125 subsection {* Ordering properties of arithmetic operations *}
   211 
   126 
   212 instance int :: ordered_cancel_ab_semigroup_add
   127 instance int :: ordered_cancel_ab_semigroup_add
   213 proof
   128 proof
   214   fix i j k :: int
   129   fix i j k :: int
   215   show "i \<le> j \<Longrightarrow> k + i \<le> k + j"
   130   show "i \<le> j \<Longrightarrow> k + i \<le> k + j"
   216     by (cases i, cases j, cases k) (simp add: le add)
   131     by transfer clarsimp
   217 qed
   132 qed
   218 
       
   219 
   133 
   220 text{*Strict Monotonicity of Multiplication*}
   134 text{*Strict Monotonicity of Multiplication*}
   221 
   135 
   222 text{*strict, in 1st argument; proof is by induction on k>0*}
   136 text{*strict, in 1st argument; proof is by induction on k>0*}
   223 lemma zmult_zless_mono2_lemma:
   137 lemma zmult_zless_mono2_lemma:
   228 apply (case_tac "k=0")
   142 apply (case_tac "k=0")
   229 apply (simp_all add: add_strict_mono)
   143 apply (simp_all add: add_strict_mono)
   230 done
   144 done
   231 
   145 
   232 lemma zero_le_imp_eq_int: "(0::int) \<le> k ==> \<exists>n. k = int n"
   146 lemma zero_le_imp_eq_int: "(0::int) \<le> k ==> \<exists>n. k = int n"
   233 apply (cases k)
   147 apply transfer
   234 apply (auto simp add: le add int_def Zero_int_def)
   148 apply clarsimp
   235 apply (rule_tac x="x-y" in exI, simp)
   149 apply (rule_tac x="a - b" in exI, simp)
   236 done
   150 done
   237 
   151 
   238 lemma zero_less_imp_eq_int: "(0::int) < k ==> \<exists>n>0. k = int n"
   152 lemma zero_less_imp_eq_int: "(0::int) < k ==> \<exists>n>0. k = int n"
   239 apply (cases k)
   153 apply transfer
   240 apply (simp add: less int_def Zero_int_def)
   154 apply clarsimp
   241 apply (rule_tac x="x-y" in exI, simp)
   155 apply (rule_tac x="a - b" in exI, simp)
   242 done
   156 done
   243 
   157 
   244 lemma zmult_zless_mono2: "[| i<j;  (0::int) < k |] ==> k*i < k*j"
   158 lemma zmult_zless_mono2: "[| i<j;  (0::int) < k |] ==> k*i < k*j"
   245 apply (drule zero_less_imp_eq_int)
   159 apply (drule zero_less_imp_eq_int)
   246 apply (auto simp add: zmult_zless_mono2_lemma)
   160 apply (auto simp add: zmult_zless_mono2_lemma)
   247 done
   161 done
   248 
   162 
   249 text{*The integers form an ordered integral domain*}
   163 text{*The integers form an ordered integral domain*}
   250 instance int :: linordered_idom
   164 instantiation int :: linordered_idom
   251 proof
   165 begin
       
   166 
       
   167 definition
       
   168   zabs_def: "\<bar>i\<Colon>int\<bar> = (if i < 0 then - i else i)"
       
   169 
       
   170 definition
       
   171   zsgn_def: "sgn (i\<Colon>int) = (if i=0 then 0 else if 0<i then 1 else - 1)"
       
   172 
       
   173 instance proof
   252   fix i j k :: int
   174   fix i j k :: int
   253   show "i < j \<Longrightarrow> 0 < k \<Longrightarrow> k * i < k * j"
   175   show "i < j \<Longrightarrow> 0 < k \<Longrightarrow> k * i < k * j"
   254     by (rule zmult_zless_mono2)
   176     by (rule zmult_zless_mono2)
   255   show "\<bar>i\<bar> = (if i < 0 then -i else i)"
   177   show "\<bar>i\<bar> = (if i < 0 then -i else i)"
   256     by (simp only: zabs_def)
   178     by (simp only: zabs_def)
   257   show "sgn (i\<Colon>int) = (if i=0 then 0 else if 0<i then 1 else - 1)"
   179   show "sgn (i\<Colon>int) = (if i=0 then 0 else if 0<i then 1 else - 1)"
   258     by (simp only: zsgn_def)
   180     by (simp only: zsgn_def)
   259 qed
   181 qed
   260 
   182 
       
   183 end
       
   184 
   261 lemma zless_imp_add1_zle: "w < z \<Longrightarrow> w + (1\<Colon>int) \<le> z"
   185 lemma zless_imp_add1_zle: "w < z \<Longrightarrow> w + (1\<Colon>int) \<le> z"
   262 apply (cases w, cases z) 
   186   by transfer clarsimp
   263 apply (simp add: less le add One_int_def)
       
   264 done
       
   265 
   187 
   266 lemma zless_iff_Suc_zadd:
   188 lemma zless_iff_Suc_zadd:
   267   "(w \<Colon> int) < z \<longleftrightarrow> (\<exists>n. z = w + int (Suc n))"
   189   "(w \<Colon> int) < z \<longleftrightarrow> (\<exists>n. z = w + int (Suc n))"
   268 apply (cases z, cases w)
   190 apply transfer
   269 apply (auto simp add: less add int_def)
   191 apply auto
   270 apply (rename_tac a b c d) 
   192 apply (rename_tac a b c d)
   271 apply (rule_tac x="a+d - Suc(c+b)" in exI) 
   193 apply (rule_tac x="c+b - Suc(a+d)" in exI)
   272 apply arith
   194 apply arith
   273 done
   195 done
   274 
   196 
   275 lemmas int_distrib =
   197 lemmas int_distrib =
   276   left_distrib [of z1 z2 w]
   198   left_distrib [of z1 z2 w]
   283 subsection {* Embedding of the Integers into any @{text ring_1}: @{text of_int}*}
   205 subsection {* Embedding of the Integers into any @{text ring_1}: @{text of_int}*}
   284 
   206 
   285 context ring_1
   207 context ring_1
   286 begin
   208 begin
   287 
   209 
   288 definition of_int :: "int \<Rightarrow> 'a" where
   210 lift_definition of_int :: "int \<Rightarrow> 'a" is "\<lambda>(i, j). of_nat i - of_nat j"
   289   "of_int z = the_elem (\<Union>(i, j) \<in> Rep_Integ z. { of_nat i - of_nat j })"
   211   by (clarsimp simp add: diff_eq_eq eq_diff_eq diff_add_eq
   290 
   212     of_nat_add [symmetric] simp del: of_nat_add)
   291 lemma of_int: "of_int (Abs_Integ (intrel `` {(i,j)})) = of_nat i - of_nat j"
       
   292 proof -
       
   293   have "(\<lambda>(i,j). { of_nat i - (of_nat j :: 'a) }) respects intrel"
       
   294     by (auto simp add: congruent_def) (simp add: algebra_simps of_nat_add [symmetric]
       
   295             del: of_nat_add) 
       
   296   thus ?thesis
       
   297     by (simp add: of_int_def UN_equiv_class [OF equiv_intrel])
       
   298 qed
       
   299 
   213 
   300 lemma of_int_0 [simp]: "of_int 0 = 0"
   214 lemma of_int_0 [simp]: "of_int 0 = 0"
   301 by (simp add: of_int Zero_int_def)
   215 by (simp add: of_int.abs_eq zero_int.abs_eq) (* FIXME: transfer *)
   302 
   216 
   303 lemma of_int_1 [simp]: "of_int 1 = 1"
   217 lemma of_int_1 [simp]: "of_int 1 = 1"
   304 by (simp add: of_int One_int_def)
   218 by (simp add: of_int.abs_eq one_int.abs_eq) (* FIXME: transfer *)
   305 
   219 
   306 lemma of_int_add [simp]: "of_int (w+z) = of_int w + of_int z"
   220 lemma of_int_add [simp]: "of_int (w+z) = of_int w + of_int z"
   307 by (cases w, cases z) (simp add: algebra_simps of_int add)
   221 (* FIXME: transfer *)
       
   222 by (cases w, cases z) (simp add: algebra_simps of_int.abs_eq plus_int.abs_eq)
   308 
   223 
   309 lemma of_int_minus [simp]: "of_int (-z) = - (of_int z)"
   224 lemma of_int_minus [simp]: "of_int (-z) = - (of_int z)"
   310 by (cases z) (simp add: algebra_simps of_int minus)
   225 (* FIXME: transfer *)
       
   226 by (cases z) (simp add: algebra_simps of_int.abs_eq uminus_int.abs_eq)
   311 
   227 
   312 lemma of_int_diff [simp]: "of_int (w - z) = of_int w - of_int z"
   228 lemma of_int_diff [simp]: "of_int (w - z) = of_int w - of_int z"
   313 by (simp add: diff_minus Groups.diff_minus)
   229 by (simp add: diff_minus Groups.diff_minus)
   314 
   230 
   315 lemma of_int_mult [simp]: "of_int (w*z) = of_int w * of_int z"
   231 lemma of_int_mult [simp]: "of_int (w*z) = of_int w * of_int z"
   316 apply (cases w, cases z)
   232 by (cases w, cases z, (* FIXME: transfer *)
   317 apply (simp add: algebra_simps of_int mult of_nat_mult)
   233   simp add: algebra_simps of_int.abs_eq times_int.abs_eq of_nat_mult)
   318 done
       
   319 
   234 
   320 text{*Collapse nested embeddings*}
   235 text{*Collapse nested embeddings*}
   321 lemma of_int_of_nat_eq [simp]: "of_int (int n) = of_nat n"
   236 lemma of_int_of_nat_eq [simp]: "of_int (int n) = of_nat n"
   322 by (induct n) auto
   237 by (induct n) auto
   323 
   238 
   337 context ring_char_0
   252 context ring_char_0
   338 begin
   253 begin
   339 
   254 
   340 lemma of_int_eq_iff [simp]:
   255 lemma of_int_eq_iff [simp]:
   341    "of_int w = of_int z \<longleftrightarrow> w = z"
   256    "of_int w = of_int z \<longleftrightarrow> w = z"
       
   257 (* FIXME: transfer *)
   342 apply (cases w, cases z)
   258 apply (cases w, cases z)
   343 apply (simp add: of_int)
   259 apply (simp add: of_int.abs_eq int.abs_eq_iff)
   344 apply (simp only: diff_eq_eq diff_add_eq eq_diff_eq)
   260 apply (simp only: diff_eq_eq diff_add_eq eq_diff_eq)
   345 apply (simp only: of_nat_add [symmetric] of_nat_eq_iff)
   261 apply (simp only: of_nat_add [symmetric] of_nat_eq_iff)
   346 done
   262 done
   347 
   263 
   348 text{*Special cases where either operand is zero*}
   264 text{*Special cases where either operand is zero*}
   362 text{*Every @{text linordered_idom} has characteristic zero.*}
   278 text{*Every @{text linordered_idom} has characteristic zero.*}
   363 subclass ring_char_0 ..
   279 subclass ring_char_0 ..
   364 
   280 
   365 lemma of_int_le_iff [simp]:
   281 lemma of_int_le_iff [simp]:
   366   "of_int w \<le> of_int z \<longleftrightarrow> w \<le> z"
   282   "of_int w \<le> of_int z \<longleftrightarrow> w \<le> z"
   367   by (cases w, cases z)
   283   by (cases w, cases z) (* FIXME: transfer *)
   368     (simp add: of_int le minus algebra_simps of_nat_add [symmetric] del: of_nat_add)
   284     (simp add: of_int.abs_eq less_eq_int.abs_eq
       
   285       algebra_simps of_nat_add [symmetric] del: of_nat_add)
   369 
   286 
   370 lemma of_int_less_iff [simp]:
   287 lemma of_int_less_iff [simp]:
   371   "of_int w < of_int z \<longleftrightarrow> w < z"
   288   "of_int w < of_int z \<longleftrightarrow> w < z"
   372   by (simp add: less_le order_less_le)
   289   by (simp add: less_le order_less_le)
   373 
   290 
   390 end
   307 end
   391 
   308 
   392 lemma of_int_eq_id [simp]: "of_int = id"
   309 lemma of_int_eq_id [simp]: "of_int = id"
   393 proof
   310 proof
   394   fix z show "of_int z = id z"
   311   fix z show "of_int z = id z"
   395     by (cases z) (simp add: of_int add minus int_def diff_minus)
   312     by (cases z rule: int_diff_cases, simp)
   396 qed
   313 qed
   397 
   314 
   398 
   315 
   399 subsection {* Magnitude of an Integer, as a Natural Number: @{text nat} *}
   316 subsection {* Magnitude of an Integer, as a Natural Number: @{text nat} *}
   400 
   317 
   401 definition nat :: "int \<Rightarrow> nat" where
   318 lift_definition nat :: "int \<Rightarrow> nat" is "\<lambda>(x, y). x - y"
   402   "nat z = the_elem (\<Union>(x, y) \<in> Rep_Integ z. {x-y})"
   319   by auto
   403 
       
   404 lemma nat: "nat (Abs_Integ (intrel``{(x,y)})) = x-y"
       
   405 proof -
       
   406   have "(\<lambda>(x,y). {x-y}) respects intrel"
       
   407     by (auto simp add: congruent_def)
       
   408   thus ?thesis
       
   409     by (simp add: nat_def UN_equiv_class [OF equiv_intrel])
       
   410 qed
       
   411 
   320 
   412 lemma nat_int [simp]: "nat (int n) = n"
   321 lemma nat_int [simp]: "nat (int n) = n"
   413 by (simp add: nat int_def)
   322   by transfer simp
   414 
   323 
   415 lemma int_nat_eq [simp]: "int (nat z) = (if 0 \<le> z then z else 0)"
   324 lemma int_nat_eq [simp]: "int (nat z) = (if 0 \<le> z then z else 0)"
   416 by (cases z) (simp add: nat le int_def Zero_int_def)
   325   by transfer clarsimp
   417 
   326 
   418 corollary nat_0_le: "0 \<le> z ==> int (nat z) = z"
   327 corollary nat_0_le: "0 \<le> z ==> int (nat z) = z"
   419 by simp
   328 by simp
   420 
   329 
   421 lemma nat_le_0 [simp]: "z \<le> 0 ==> nat z = 0"
   330 lemma nat_le_0 [simp]: "z \<le> 0 ==> nat z = 0"
   422 by (cases z) (simp add: nat le Zero_int_def)
   331   by transfer clarsimp
   423 
   332 
   424 lemma nat_le_eq_zle: "0 < w | 0 \<le> z ==> (nat w \<le> nat z) = (w\<le>z)"
   333 lemma nat_le_eq_zle: "0 < w | 0 \<le> z ==> (nat w \<le> nat z) = (w\<le>z)"
   425 apply (cases w, cases z) 
   334   by transfer (clarsimp, arith)
   426 apply (simp add: nat le linorder_not_le [symmetric] Zero_int_def, arith)
       
   427 done
       
   428 
   335 
   429 text{*An alternative condition is @{term "0 \<le> w"} *}
   336 text{*An alternative condition is @{term "0 \<le> w"} *}
   430 corollary nat_mono_iff: "0 < z ==> (nat w < nat z) = (w < z)"
   337 corollary nat_mono_iff: "0 < z ==> (nat w < nat z) = (w < z)"
   431 by (simp add: nat_le_eq_zle linorder_not_le [symmetric]) 
   338 by (simp add: nat_le_eq_zle linorder_not_le [symmetric]) 
   432 
   339 
   433 corollary nat_less_eq_zless: "0 \<le> w ==> (nat w < nat z) = (w<z)"
   340 corollary nat_less_eq_zless: "0 \<le> w ==> (nat w < nat z) = (w<z)"
   434 by (simp add: nat_le_eq_zle linorder_not_le [symmetric]) 
   341 by (simp add: nat_le_eq_zle linorder_not_le [symmetric]) 
   435 
   342 
   436 lemma zless_nat_conj [simp]: "(nat w < nat z) = (0 < z & w < z)"
   343 lemma zless_nat_conj [simp]: "(nat w < nat z) = (0 < z & w < z)"
   437 apply (cases w, cases z) 
   344   by transfer (clarsimp, arith)
   438 apply (simp add: nat le Zero_int_def linorder_not_le [symmetric], arith)
       
   439 done
       
   440 
   345 
   441 lemma nonneg_eq_int:
   346 lemma nonneg_eq_int:
   442   fixes z :: int
   347   fixes z :: int
   443   assumes "0 \<le> z" and "\<And>m. z = int m \<Longrightarrow> P"
   348   assumes "0 \<le> z" and "\<And>m. z = int m \<Longrightarrow> P"
   444   shows P
   349   shows P
   445   using assms by (blast dest: nat_0_le sym)
   350   using assms by (blast dest: nat_0_le sym)
   446 
   351 
   447 lemma nat_eq_iff: "(nat w = m) = (if 0 \<le> w then w = int m else m=0)"
   352 lemma nat_eq_iff: "(nat w = m) = (if 0 \<le> w then w = int m else m=0)"
   448 by (cases w) (simp add: nat le int_def Zero_int_def, arith)
   353   by transfer (clarsimp simp add: le_imp_diff_is_add)
   449 
   354 
   450 corollary nat_eq_iff2: "(m = nat w) = (if 0 \<le> w then w = int m else m=0)"
   355 corollary nat_eq_iff2: "(m = nat w) = (if 0 \<le> w then w = int m else m=0)"
   451 by (simp only: eq_commute [of m] nat_eq_iff)
   356 by (simp only: eq_commute [of m] nat_eq_iff)
   452 
   357 
   453 lemma nat_less_iff: "0 \<le> w ==> (nat w < m) = (w < of_nat m)"
   358 lemma nat_less_iff: "0 \<le> w ==> (nat w < m) = (w < of_nat m)"
   454 apply (cases w)
   359   by transfer (clarsimp, arith)
   455 apply (simp add: nat le int_def Zero_int_def linorder_not_le[symmetric], arith)
       
   456 done
       
   457 
   360 
   458 lemma nat_le_iff: "nat x \<le> n \<longleftrightarrow> x \<le> int n"
   361 lemma nat_le_iff: "nat x \<le> n \<longleftrightarrow> x \<le> int n"
   459   by (cases x, simp add: nat le int_def le_diff_conv)
   362   by transfer (clarsimp simp add: le_diff_conv)
   460 
   363 
   461 lemma nat_mono: "x \<le> y \<Longrightarrow> nat x \<le> nat y"
   364 lemma nat_mono: "x \<le> y \<Longrightarrow> nat x \<le> nat y"
   462   by (cases x, cases y, simp add: nat le)
   365   by transfer auto
   463 
   366 
   464 lemma nat_0_iff[simp]: "nat(i::int) = 0 \<longleftrightarrow> i\<le>0"
   367 lemma nat_0_iff[simp]: "nat(i::int) = 0 \<longleftrightarrow> i\<le>0"
   465 by(simp add: nat_eq_iff) arith
   368   by transfer clarsimp
   466 
   369 
   467 lemma int_eq_iff: "(of_nat m = z) = (m = nat z & 0 \<le> z)"
   370 lemma int_eq_iff: "(of_nat m = z) = (m = nat z & 0 \<le> z)"
   468 by (auto simp add: nat_eq_iff2)
   371 by (auto simp add: nat_eq_iff2)
   469 
   372 
   470 lemma zero_less_nat_eq [simp]: "(0 < nat z) = (0 < z)"
   373 lemma zero_less_nat_eq [simp]: "(0 < nat z) = (0 < z)"
   471 by (insert zless_nat_conj [of 0], auto)
   374 by (insert zless_nat_conj [of 0], auto)
   472 
   375 
   473 lemma nat_add_distrib:
   376 lemma nat_add_distrib:
   474      "[| (0::int) \<le> z;  0 \<le> z' |] ==> nat (z+z') = nat z + nat z'"
   377      "[| (0::int) \<le> z;  0 \<le> z' |] ==> nat (z+z') = nat z + nat z'"
   475 by (cases z, cases z') (simp add: nat add le Zero_int_def)
   378   by transfer clarsimp
   476 
   379 
   477 lemma nat_diff_distrib:
   380 lemma nat_diff_distrib:
   478      "[| (0::int) \<le> z';  z' \<le> z |] ==> nat (z-z') = nat z - nat z'"
   381      "[| (0::int) \<le> z';  z' \<le> z |] ==> nat (z-z') = nat z - nat z'"
   479 by (cases z, cases z')
   382   by transfer clarsimp
   480   (simp add: nat add minus diff_minus le Zero_int_def)
       
   481 
   383 
   482 lemma nat_zminus_int [simp]: "nat (- int n) = 0"
   384 lemma nat_zminus_int [simp]: "nat (- int n) = 0"
   483 by (simp add: int_def minus nat Zero_int_def) 
   385   by transfer simp
   484 
   386 
   485 lemma zless_nat_eq_int_zless: "(m < nat z) = (int m < z)"
   387 lemma zless_nat_eq_int_zless: "(m < nat z) = (int m < z)"
   486 by (cases z) (simp add: nat less int_def, arith)
   388   by transfer (clarsimp simp add: less_diff_conv)
   487 
   389 
   488 context ring_1
   390 context ring_1
   489 begin
   391 begin
   490 
   392 
   491 lemma of_nat_nat: "0 \<le> z \<Longrightarrow> of_nat (nat z) = of_int z"
   393 lemma of_nat_nat: "0 \<le> z \<Longrightarrow> of_nat (nat z) = of_int z"
   492   by (cases z rule: eq_Abs_Integ)
   394   by (cases z rule: eq_Abs_Integ) (* FIXME: transfer *)
   493    (simp add: nat le of_int Zero_int_def of_nat_diff)
   395    (simp add: nat.abs_eq less_eq_int.abs_eq of_int.abs_eq zero_int.abs_eq of_nat_diff)
   494 
   396 
   495 end
   397 end
   496 
   398 
   497 text {* For termination proofs: *}
   399 text {* For termination proofs: *}
   498 lemma measure_function_int[measure_function]: "is_measure (nat o abs)" ..
   400 lemma measure_function_int[measure_function]: "is_measure (nat o abs)" ..
   514 
   416 
   515 lemma not_zle_0_negative [simp]: "~ (0 \<le> - (int (Suc n)))"
   417 lemma not_zle_0_negative [simp]: "~ (0 \<le> - (int (Suc n)))"
   516 by (subst le_minus_iff, simp del: of_nat_Suc)
   418 by (subst le_minus_iff, simp del: of_nat_Suc)
   517 
   419 
   518 lemma int_zle_neg: "(int n \<le> - int m) = (n = 0 & m = 0)"
   420 lemma int_zle_neg: "(int n \<le> - int m) = (n = 0 & m = 0)"
   519 by (simp add: int_def le minus Zero_int_def)
   421   by transfer simp
   520 
   422 
   521 lemma not_int_zless_negative [simp]: "~ (int n < - int m)"
   423 lemma not_int_zless_negative [simp]: "~ (int n < - int m)"
   522 by (simp add: linorder_not_less)
   424 by (simp add: linorder_not_less)
   523 
   425 
   524 lemma negative_eq_positive [simp]: "(- int n = of_nat m) = (n = 0 & m = 0)"
   426 lemma negative_eq_positive [simp]: "(- int n = of_nat m) = (n = 0 & m = 0)"
   548 lemma abs_split [arith_split,no_atp]:
   450 lemma abs_split [arith_split,no_atp]:
   549      "P(abs(a::'a::linordered_idom)) = ((0 \<le> a --> P a) & (a < 0 --> P(-a)))"
   451      "P(abs(a::'a::linordered_idom)) = ((0 \<le> a --> P a) & (a < 0 --> P(-a)))"
   550 by (force dest: order_less_le_trans simp add: abs_if linorder_not_less)
   452 by (force dest: order_less_le_trans simp add: abs_if linorder_not_less)
   551 
   453 
   552 lemma negD: "x < 0 \<Longrightarrow> \<exists>n. x = - (int (Suc n))"
   454 lemma negD: "x < 0 \<Longrightarrow> \<exists>n. x = - (int (Suc n))"
   553 apply (cases x)
   455 apply transfer
   554 apply (auto simp add: le minus Zero_int_def int_def order_less_le)
   456 apply clarsimp
   555 apply (rule_tac x="y - Suc x" in exI, arith)
   457 apply (rule_tac x="b - Suc a" in exI, arith)
   556 done
   458 done
   557 
   459 
   558 
   460 
   559 subsection {* Cases and induction *}
   461 subsection {* Cases and induction *}
   560 
   462 
   575   by (cases z) auto
   477   by (cases z) auto
   576 
   478 
   577 lemma nonneg_int_cases:
   479 lemma nonneg_int_cases:
   578   assumes "0 \<le> k" obtains n where "k = int n"
   480   assumes "0 \<le> k" obtains n where "k = int n"
   579   using assms by (cases k, simp, simp del: of_nat_Suc)
   481   using assms by (cases k, simp, simp del: of_nat_Suc)
   580 
       
   581 text{*Contributed by Brian Huffman*}
       
   582 theorem int_diff_cases:
       
   583   obtains (diff) m n where "z = int m - int n"
       
   584 apply (cases z rule: eq_Abs_Integ)
       
   585 apply (rule_tac m=x and n=y in diff)
       
   586 apply (simp add: int_def minus add diff_minus)
       
   587 done
       
   588 
   482 
   589 lemma Let_numeral [simp]: "Let (numeral v) f = f (numeral v)"
   483 lemma Let_numeral [simp]: "Let (numeral v) f = f (numeral v)"
   590   -- {* Unfold all @{text let}s involving constants *}
   484   -- {* Unfold all @{text let}s involving constants *}
   591   unfolding Let_def ..
   485   unfolding Let_def ..
   592 
   486 
   869 
   763 
   870 
   764 
   871 subsection{*The functions @{term nat} and @{term int}*}
   765 subsection{*The functions @{term nat} and @{term int}*}
   872 
   766 
   873 text{*Simplify the term @{term "w + - z"}*}
   767 text{*Simplify the term @{term "w + - z"}*}
   874 lemmas diff_int_def_symmetric = diff_int_def [symmetric, simp]
   768 lemmas diff_int_def_symmetric = diff_def [where 'a=int, symmetric, simp]
   875 
   769 
   876 lemma nat_0 [simp]: "nat 0 = 0"
   770 lemma nat_0 [simp]: "nat 0 = 0"
   877 by (simp add: nat_eq_iff)
   771 by (simp add: nat_eq_iff)
   878 
   772 
   879 lemma nat_1 [simp]: "nat 1 = Suc 0"
   773 lemma nat_1 [simp]: "nat 1 = Suc 0"
  1765   "int (m ^ n) = int m ^ n"
  1659   "int (m ^ n) = int m ^ n"
  1766   by (rule of_nat_power)
  1660   by (rule of_nat_power)
  1767 
  1661 
  1768 lemmas zpower_int = int_power [symmetric]
  1662 lemmas zpower_int = int_power [symmetric]
  1769 
  1663 
       
  1664 text {* De-register @{text "int"} as a quotient type: *}
       
  1665 
       
  1666 lemmas [transfer_rule del] =
       
  1667   int.id_abs_transfer int.rel_eq_transfer zero_int.transfer one_int.transfer
       
  1668   plus_int.transfer uminus_int.transfer minus_int.transfer times_int.transfer
       
  1669   int_transfer less_eq_int.transfer less_int.transfer of_int.transfer
       
  1670   nat.transfer
       
  1671 
       
  1672 declare Quotient_int [quot_del]
       
  1673 
  1770 end
  1674 end