src/HOL/Int.thy
 changeset 48045 fbf77fdf9ae4 parent 48044 fea6f3060b65 child 48066 c6783c9b87bf
equal 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`
`   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)`
`   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`