src/HOL/Int.thy
author haftmann
Wed Feb 18 22:46:48 2015 +0100 (2015-02-18)
changeset 59556 aa2deef7cf47
parent 59536 03bde055a1a0
child 59582 0fbed69ff081
permissions -rw-r--r--
eliminated technical fact alias
     1 (*  Title:      HOL/Int.thy
     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3     Author:     Tobias Nipkow, Florian Haftmann, TU Muenchen
     4 *)
     5 
     6 section {* The Integers as Equivalence Classes over Pairs of Natural Numbers *} 
     7 
     8 theory Int
     9 imports Equiv_Relations Power Quotient Fun_Def
    10 begin
    11 
    12 subsection {* Definition of integers as a quotient type *}
    13 
    14 definition intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" where
    15   "intrel = (\<lambda>(x, y) (u, v). x + v = u + y)"
    16 
    17 lemma intrel_iff [simp]: "intrel (x, y) (u, v) \<longleftrightarrow> x + v = u + y"
    18   by (simp add: intrel_def)
    19 
    20 quotient_type int = "nat \<times> nat" / "intrel"
    21   morphisms Rep_Integ Abs_Integ
    22 proof (rule equivpI)
    23   show "reflp intrel"
    24     unfolding reflp_def by auto
    25   show "symp intrel"
    26     unfolding symp_def by auto
    27   show "transp intrel"
    28     unfolding transp_def by auto
    29 qed
    30 
    31 lemma eq_Abs_Integ [case_names Abs_Integ, cases type: int]:
    32      "(!!x y. z = Abs_Integ (x, y) ==> P) ==> P"
    33 by (induct z) auto
    34 
    35 subsection {* Integers form a commutative ring *}
    36 
    37 instantiation int :: comm_ring_1
    38 begin
    39 
    40 lift_definition zero_int :: "int" is "(0, 0)" .
    41 
    42 lift_definition one_int :: "int" is "(1, 0)" .
    43 
    44 lift_definition plus_int :: "int \<Rightarrow> int \<Rightarrow> int"
    45   is "\<lambda>(x, y) (u, v). (x + u, y + v)"
    46   by clarsimp
    47 
    48 lift_definition uminus_int :: "int \<Rightarrow> int"
    49   is "\<lambda>(x, y). (y, x)"
    50   by clarsimp
    51 
    52 lift_definition minus_int :: "int \<Rightarrow> int \<Rightarrow> int"
    53   is "\<lambda>(x, y) (u, v). (x + v, y + u)"
    54   by clarsimp
    55 
    56 lift_definition times_int :: "int \<Rightarrow> int \<Rightarrow> int"
    57   is "\<lambda>(x, y) (u, v). (x*u + y*v, x*v + y*u)"
    58 proof (clarsimp)
    59   fix s t u v w x y z :: nat
    60   assume "s + v = u + t" and "w + z = y + x"
    61   hence "(s + v) * w + (u + t) * x + u * (w + z) + v * (y + x)
    62        = (u + t) * w + (s + v) * x + u * (y + x) + v * (w + z)"
    63     by simp
    64   thus "(s * w + t * x) + (u * z + v * y) = (u * y + v * z) + (s * x + t * w)"
    65     by (simp add: algebra_simps)
    66 qed
    67 
    68 instance
    69   by default (transfer, clarsimp simp: algebra_simps)+
    70 
    71 end
    72 
    73 abbreviation int :: "nat \<Rightarrow> int" where
    74   "int \<equiv> of_nat"
    75 
    76 lemma int_def: "int n = Abs_Integ (n, 0)"
    77   by (induct n, simp add: zero_int.abs_eq,
    78     simp add: one_int.abs_eq plus_int.abs_eq)
    79 
    80 lemma int_transfer [transfer_rule]:
    81   "(rel_fun (op =) pcr_int) (\<lambda>n. (n, 0)) int"
    82   unfolding rel_fun_def int.pcr_cr_eq cr_int_def int_def by simp
    83 
    84 lemma int_diff_cases:
    85   obtains (diff) m n where "z = int m - int n"
    86   by transfer clarsimp
    87 
    88 subsection {* Integers are totally ordered *}
    89 
    90 instantiation int :: linorder
    91 begin
    92 
    93 lift_definition less_eq_int :: "int \<Rightarrow> int \<Rightarrow> bool"
    94   is "\<lambda>(x, y) (u, v). x + v \<le> u + y"
    95   by auto
    96 
    97 lift_definition less_int :: "int \<Rightarrow> int \<Rightarrow> bool"
    98   is "\<lambda>(x, y) (u, v). x + v < u + y"
    99   by auto
   100 
   101 instance
   102   by default (transfer, force)+
   103 
   104 end
   105 
   106 instantiation int :: distrib_lattice
   107 begin
   108 
   109 definition
   110   "(inf \<Colon> int \<Rightarrow> int \<Rightarrow> int) = min"
   111 
   112 definition
   113   "(sup \<Colon> int \<Rightarrow> int \<Rightarrow> int) = max"
   114 
   115 instance
   116   by intro_classes
   117     (auto simp add: inf_int_def sup_int_def max_min_distrib2)
   118 
   119 end
   120 
   121 subsection {* Ordering properties of arithmetic operations *}
   122 
   123 instance int :: ordered_cancel_ab_semigroup_add
   124 proof
   125   fix i j k :: int
   126   show "i \<le> j \<Longrightarrow> k + i \<le> k + j"
   127     by transfer clarsimp
   128 qed
   129 
   130 text{*Strict Monotonicity of Multiplication*}
   131 
   132 text{*strict, in 1st argument; proof is by induction on k>0*}
   133 lemma zmult_zless_mono2_lemma:
   134      "(i::int)<j ==> 0<k ==> int k * i < int k * j"
   135 apply (induct k)
   136 apply simp
   137 apply (simp add: distrib_right)
   138 apply (case_tac "k=0")
   139 apply (simp_all add: add_strict_mono)
   140 done
   141 
   142 lemma zero_le_imp_eq_int: "(0::int) \<le> k ==> \<exists>n. k = int n"
   143 apply transfer
   144 apply clarsimp
   145 apply (rule_tac x="a - b" in exI, simp)
   146 done
   147 
   148 lemma zero_less_imp_eq_int: "(0::int) < k ==> \<exists>n>0. k = int n"
   149 apply transfer
   150 apply clarsimp
   151 apply (rule_tac x="a - b" in exI, simp)
   152 done
   153 
   154 lemma zmult_zless_mono2: "[| i<j;  (0::int) < k |] ==> k*i < k*j"
   155 apply (drule zero_less_imp_eq_int)
   156 apply (auto simp add: zmult_zless_mono2_lemma)
   157 done
   158 
   159 text{*The integers form an ordered integral domain*}
   160 instantiation int :: linordered_idom
   161 begin
   162 
   163 definition
   164   zabs_def: "\<bar>i\<Colon>int\<bar> = (if i < 0 then - i else i)"
   165 
   166 definition
   167   zsgn_def: "sgn (i\<Colon>int) = (if i=0 then 0 else if 0<i then 1 else - 1)"
   168 
   169 instance proof
   170   fix i j k :: int
   171   show "i < j \<Longrightarrow> 0 < k \<Longrightarrow> k * i < k * j"
   172     by (rule zmult_zless_mono2)
   173   show "\<bar>i\<bar> = (if i < 0 then -i else i)"
   174     by (simp only: zabs_def)
   175   show "sgn (i\<Colon>int) = (if i=0 then 0 else if 0<i then 1 else - 1)"
   176     by (simp only: zsgn_def)
   177 qed
   178 
   179 end
   180 
   181 lemma zless_imp_add1_zle: "w < z \<Longrightarrow> w + (1\<Colon>int) \<le> z"
   182   by transfer clarsimp
   183 
   184 lemma zless_iff_Suc_zadd:
   185   "(w \<Colon> int) < z \<longleftrightarrow> (\<exists>n. z = w + int (Suc n))"
   186 apply transfer
   187 apply auto
   188 apply (rename_tac a b c d)
   189 apply (rule_tac x="c+b - Suc(a+d)" in exI)
   190 apply arith
   191 done
   192 
   193 lemmas int_distrib =
   194   distrib_right [of z1 z2 w]
   195   distrib_left [of w z1 z2]
   196   left_diff_distrib [of z1 z2 w]
   197   right_diff_distrib [of w z1 z2]
   198   for z1 z2 w :: int
   199 
   200 
   201 subsection {* Embedding of the Integers into any @{text ring_1}: @{text of_int}*}
   202 
   203 context ring_1
   204 begin
   205 
   206 lift_definition of_int :: "int \<Rightarrow> 'a" is "\<lambda>(i, j). of_nat i - of_nat j"
   207   by (clarsimp simp add: diff_eq_eq eq_diff_eq diff_add_eq
   208     of_nat_add [symmetric] simp del: of_nat_add)
   209 
   210 lemma of_int_0 [simp]: "of_int 0 = 0"
   211   by transfer simp
   212 
   213 lemma of_int_1 [simp]: "of_int 1 = 1"
   214   by transfer simp
   215 
   216 lemma of_int_add [simp]: "of_int (w+z) = of_int w + of_int z"
   217   by transfer (clarsimp simp add: algebra_simps)
   218 
   219 lemma of_int_minus [simp]: "of_int (-z) = - (of_int z)"
   220   by (transfer fixing: uminus) clarsimp
   221 
   222 lemma of_int_diff [simp]: "of_int (w - z) = of_int w - of_int z"
   223   using of_int_add [of w "- z"] by simp
   224 
   225 lemma of_int_mult [simp]: "of_int (w*z) = of_int w * of_int z"
   226   by (transfer fixing: times) (clarsimp simp add: algebra_simps of_nat_mult)
   227 
   228 text{*Collapse nested embeddings*}
   229 lemma of_int_of_nat_eq [simp]: "of_int (int n) = of_nat n"
   230 by (induct n) auto
   231 
   232 lemma of_int_numeral [simp, code_post]: "of_int (numeral k) = numeral k"
   233   by (simp add: of_nat_numeral [symmetric] of_int_of_nat_eq [symmetric])
   234 
   235 lemma of_int_neg_numeral [code_post]: "of_int (- numeral k) = - numeral k"
   236   by simp
   237 
   238 lemma of_int_power:
   239   "of_int (z ^ n) = of_int z ^ n"
   240   by (induct n) simp_all
   241 
   242 end
   243 
   244 context ring_char_0
   245 begin
   246 
   247 lemma of_int_eq_iff [simp]:
   248    "of_int w = of_int z \<longleftrightarrow> w = z"
   249   by transfer (clarsimp simp add: algebra_simps
   250     of_nat_add [symmetric] simp del: of_nat_add)
   251 
   252 text{*Special cases where either operand is zero*}
   253 lemma of_int_eq_0_iff [simp]:
   254   "of_int z = 0 \<longleftrightarrow> z = 0"
   255   using of_int_eq_iff [of z 0] by simp
   256 
   257 lemma of_int_0_eq_iff [simp]:
   258   "0 = of_int z \<longleftrightarrow> z = 0"
   259   using of_int_eq_iff [of 0 z] by simp
   260 
   261 end
   262 
   263 context linordered_idom
   264 begin
   265 
   266 text{*Every @{text linordered_idom} has characteristic zero.*}
   267 subclass ring_char_0 ..
   268 
   269 lemma of_int_le_iff [simp]:
   270   "of_int w \<le> of_int z \<longleftrightarrow> w \<le> z"
   271   by (transfer fixing: less_eq) (clarsimp simp add: algebra_simps
   272     of_nat_add [symmetric] simp del: of_nat_add)
   273 
   274 lemma of_int_less_iff [simp]:
   275   "of_int w < of_int z \<longleftrightarrow> w < z"
   276   by (simp add: less_le order_less_le)
   277 
   278 lemma of_int_0_le_iff [simp]:
   279   "0 \<le> of_int z \<longleftrightarrow> 0 \<le> z"
   280   using of_int_le_iff [of 0 z] by simp
   281 
   282 lemma of_int_le_0_iff [simp]:
   283   "of_int z \<le> 0 \<longleftrightarrow> z \<le> 0"
   284   using of_int_le_iff [of z 0] by simp
   285 
   286 lemma of_int_0_less_iff [simp]:
   287   "0 < of_int z \<longleftrightarrow> 0 < z"
   288   using of_int_less_iff [of 0 z] by simp
   289 
   290 lemma of_int_less_0_iff [simp]:
   291   "of_int z < 0 \<longleftrightarrow> z < 0"
   292   using of_int_less_iff [of z 0] by simp
   293 
   294 end
   295 
   296 lemma of_nat_less_of_int_iff:
   297   "(of_nat n::'a::linordered_idom) < of_int x \<longleftrightarrow> int n < x"
   298   by (metis of_int_of_nat_eq of_int_less_iff)
   299 
   300 lemma of_int_eq_id [simp]: "of_int = id"
   301 proof
   302   fix z show "of_int z = id z"
   303     by (cases z rule: int_diff_cases, simp)
   304 qed
   305 
   306 
   307 instance int :: no_top
   308   apply default
   309   apply (rule_tac x="x + 1" in exI)
   310   apply simp
   311   done
   312 
   313 instance int :: no_bot
   314   apply default
   315   apply (rule_tac x="x - 1" in exI)
   316   apply simp
   317   done
   318 
   319 subsection {* Magnitude of an Integer, as a Natural Number: @{text nat} *}
   320 
   321 lift_definition nat :: "int \<Rightarrow> nat" is "\<lambda>(x, y). x - y"
   322   by auto
   323 
   324 lemma nat_int [simp]: "nat (int n) = n"
   325   by transfer simp
   326 
   327 lemma int_nat_eq [simp]: "int (nat z) = (if 0 \<le> z then z else 0)"
   328   by transfer clarsimp
   329 
   330 corollary nat_0_le: "0 \<le> z ==> int (nat z) = z"
   331 by simp
   332 
   333 lemma nat_le_0 [simp]: "z \<le> 0 ==> nat z = 0"
   334   by transfer clarsimp
   335 
   336 lemma nat_le_eq_zle: "0 < w | 0 \<le> z ==> (nat w \<le> nat z) = (w\<le>z)"
   337   by transfer (clarsimp, arith)
   338 
   339 text{*An alternative condition is @{term "0 \<le> w"} *}
   340 corollary nat_mono_iff: "0 < z ==> (nat w < nat z) = (w < z)"
   341 by (simp add: nat_le_eq_zle linorder_not_le [symmetric]) 
   342 
   343 corollary nat_less_eq_zless: "0 \<le> w ==> (nat w < nat z) = (w<z)"
   344 by (simp add: nat_le_eq_zle linorder_not_le [symmetric]) 
   345 
   346 lemma zless_nat_conj [simp]: "(nat w < nat z) = (0 < z & w < z)"
   347   by transfer (clarsimp, arith)
   348 
   349 lemma nonneg_eq_int:
   350   fixes z :: int
   351   assumes "0 \<le> z" and "\<And>m. z = int m \<Longrightarrow> P"
   352   shows P
   353   using assms by (blast dest: nat_0_le sym)
   354 
   355 lemma nat_eq_iff:
   356   "nat w = m \<longleftrightarrow> (if 0 \<le> w then w = int m else m = 0)"
   357   by transfer (clarsimp simp add: le_imp_diff_is_add)
   358  
   359 corollary nat_eq_iff2:
   360   "m = nat w \<longleftrightarrow> (if 0 \<le> w then w = int m else m = 0)"
   361   using nat_eq_iff [of w m] by auto
   362 
   363 lemma nat_0 [simp]:
   364   "nat 0 = 0"
   365   by (simp add: nat_eq_iff)
   366 
   367 lemma nat_1 [simp]:
   368   "nat 1 = Suc 0"
   369   by (simp add: nat_eq_iff)
   370 
   371 lemma nat_numeral [simp]:
   372   "nat (numeral k) = numeral k"
   373   by (simp add: nat_eq_iff)
   374 
   375 lemma nat_neg_numeral [simp]:
   376   "nat (- numeral k) = 0"
   377   by simp
   378 
   379 lemma nat_2: "nat 2 = Suc (Suc 0)"
   380   by simp
   381  
   382 lemma nat_less_iff: "0 \<le> w ==> (nat w < m) = (w < of_nat m)"
   383   by transfer (clarsimp, arith)
   384 
   385 lemma nat_le_iff: "nat x \<le> n \<longleftrightarrow> x \<le> int n"
   386   by transfer (clarsimp simp add: le_diff_conv)
   387 
   388 lemma nat_mono: "x \<le> y \<Longrightarrow> nat x \<le> nat y"
   389   by transfer auto
   390 
   391 lemma nat_0_iff[simp]: "nat(i::int) = 0 \<longleftrightarrow> i\<le>0"
   392   by transfer clarsimp
   393 
   394 lemma int_eq_iff: "(of_nat m = z) = (m = nat z & 0 \<le> z)"
   395 by (auto simp add: nat_eq_iff2)
   396 
   397 lemma zero_less_nat_eq [simp]: "(0 < nat z) = (0 < z)"
   398 by (insert zless_nat_conj [of 0], auto)
   399 
   400 lemma nat_add_distrib:
   401   "0 \<le> z \<Longrightarrow> 0 \<le> z' \<Longrightarrow> nat (z + z') = nat z + nat z'"
   402   by transfer clarsimp
   403 
   404 lemma nat_diff_distrib':
   405   "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> nat (x - y) = nat x - nat y"
   406   by transfer clarsimp
   407  
   408 lemma nat_diff_distrib:
   409   "0 \<le> z' \<Longrightarrow> z' \<le> z \<Longrightarrow> nat (z - z') = nat z - nat z'"
   410   by (rule nat_diff_distrib') auto
   411 
   412 lemma nat_zminus_int [simp]: "nat (- int n) = 0"
   413   by transfer simp
   414 
   415 lemma le_nat_iff:
   416   "k \<ge> 0 \<Longrightarrow> n \<le> nat k \<longleftrightarrow> int n \<le> k"
   417   by transfer auto
   418   
   419 lemma zless_nat_eq_int_zless: "(m < nat z) = (int m < z)"
   420   by transfer (clarsimp simp add: less_diff_conv)
   421 
   422 context ring_1
   423 begin
   424 
   425 lemma of_nat_nat: "0 \<le> z \<Longrightarrow> of_nat (nat z) = of_int z"
   426   by transfer (clarsimp simp add: of_nat_diff)
   427 
   428 end
   429 
   430 lemma diff_nat_numeral [simp]: 
   431   "(numeral v :: nat) - numeral v' = nat (numeral v - numeral v')"
   432   by (simp only: nat_diff_distrib' zero_le_numeral nat_numeral)
   433 
   434 
   435 text {* For termination proofs: *}
   436 lemma measure_function_int[measure_function]: "is_measure (nat o abs)" ..
   437 
   438 
   439 subsection{*Lemmas about the Function @{term of_nat} and Orderings*}
   440 
   441 lemma negative_zless_0: "- (int (Suc n)) < (0 \<Colon> int)"
   442 by (simp add: order_less_le del: of_nat_Suc)
   443 
   444 lemma negative_zless [iff]: "- (int (Suc n)) < int m"
   445 by (rule negative_zless_0 [THEN order_less_le_trans], simp)
   446 
   447 lemma negative_zle_0: "- int n \<le> 0"
   448 by (simp add: minus_le_iff)
   449 
   450 lemma negative_zle [iff]: "- int n \<le> int m"
   451 by (rule order_trans [OF negative_zle_0 of_nat_0_le_iff])
   452 
   453 lemma not_zle_0_negative [simp]: "~ (0 \<le> - (int (Suc n)))"
   454 by (subst le_minus_iff, simp del: of_nat_Suc)
   455 
   456 lemma int_zle_neg: "(int n \<le> - int m) = (n = 0 & m = 0)"
   457   by transfer simp
   458 
   459 lemma not_int_zless_negative [simp]: "~ (int n < - int m)"
   460 by (simp add: linorder_not_less)
   461 
   462 lemma negative_eq_positive [simp]: "(- int n = of_nat m) = (n = 0 & m = 0)"
   463 by (force simp add: order_eq_iff [of "- of_nat n"] int_zle_neg)
   464 
   465 lemma zle_iff_zadd: "w \<le> z \<longleftrightarrow> (\<exists>n. z = w + int n)"
   466 proof -
   467   have "(w \<le> z) = (0 \<le> z - w)"
   468     by (simp only: le_diff_eq add_0_left)
   469   also have "\<dots> = (\<exists>n. z - w = of_nat n)"
   470     by (auto elim: zero_le_imp_eq_int)
   471   also have "\<dots> = (\<exists>n. z = w + of_nat n)"
   472     by (simp only: algebra_simps)
   473   finally show ?thesis .
   474 qed
   475 
   476 lemma zadd_int_left: "int m + (int n + z) = int (m + n) + z"
   477 by simp
   478 
   479 lemma int_Suc0_eq_1: "int (Suc 0) = 1"
   480 by simp
   481 
   482 text{*This version is proved for all ordered rings, not just integers!
   483       It is proved here because attribute @{text arith_split} is not available
   484       in theory @{text Rings}.
   485       But is it really better than just rewriting with @{text abs_if}?*}
   486 lemma abs_split [arith_split, no_atp]:
   487      "P(abs(a::'a::linordered_idom)) = ((0 \<le> a --> P a) & (a < 0 --> P(-a)))"
   488 by (force dest: order_less_le_trans simp add: abs_if linorder_not_less)
   489 
   490 lemma negD: "x < 0 \<Longrightarrow> \<exists>n. x = - (int (Suc n))"
   491 apply transfer
   492 apply clarsimp
   493 apply (rule_tac x="b - Suc a" in exI, arith)
   494 done
   495 
   496 subsection {* Cases and induction *}
   497 
   498 text{*Now we replace the case analysis rule by a more conventional one:
   499 whether an integer is negative or not.*}
   500 
   501 theorem int_cases [case_names nonneg neg, cases type: int]:
   502   "[|!! n. z = int n ==> P;  !! n. z =  - (int (Suc n)) ==> P |] ==> P"
   503 apply (cases "z < 0")
   504 apply (blast dest!: negD)
   505 apply (simp add: linorder_not_less del: of_nat_Suc)
   506 apply auto
   507 apply (blast dest: nat_0_le [THEN sym])
   508 done
   509 
   510 theorem int_of_nat_induct [case_names nonneg neg, induct type: int]:
   511      "[|!! n. P (int n);  !!n. P (- (int (Suc n))) |] ==> P z"
   512   by (cases z) auto
   513 
   514 lemma nonneg_int_cases:
   515   assumes "0 \<le> k" obtains n where "k = int n"
   516   using assms by (rule nonneg_eq_int)
   517 
   518 lemma Let_numeral [simp]: "Let (numeral v) f = f (numeral v)"
   519   -- {* Unfold all @{text let}s involving constants *}
   520   by (fact Let_numeral) -- {* FIXME drop *}
   521 
   522 lemma Let_neg_numeral [simp]: "Let (- numeral v) f = f (- numeral v)"
   523   -- {* Unfold all @{text let}s involving constants *}
   524   by (fact Let_neg_numeral) -- {* FIXME drop *}
   525 
   526 text {* Unfold @{text min} and @{text max} on numerals. *}
   527 
   528 lemmas max_number_of [simp] =
   529   max_def [of "numeral u" "numeral v"]
   530   max_def [of "numeral u" "- numeral v"]
   531   max_def [of "- numeral u" "numeral v"]
   532   max_def [of "- numeral u" "- numeral v"] for u v
   533 
   534 lemmas min_number_of [simp] =
   535   min_def [of "numeral u" "numeral v"]
   536   min_def [of "numeral u" "- numeral v"]
   537   min_def [of "- numeral u" "numeral v"]
   538   min_def [of "- numeral u" "- numeral v"] for u v
   539 
   540 
   541 subsubsection {* Binary comparisons *}
   542 
   543 text {* Preliminaries *}
   544 
   545 lemma le_imp_0_less: 
   546   assumes le: "0 \<le> z"
   547   shows "(0::int) < 1 + z"
   548 proof -
   549   have "0 \<le> z" by fact
   550   also have "... < z + 1" by (rule less_add_one)
   551   also have "... = 1 + z" by (simp add: ac_simps)
   552   finally show "0 < 1 + z" .
   553 qed
   554 
   555 lemma odd_less_0_iff:
   556   "(1 + z + z < 0) = (z < (0::int))"
   557 proof (cases z)
   558   case (nonneg n)
   559   thus ?thesis by (simp add: linorder_not_less add.assoc add_increasing
   560                              le_imp_0_less [THEN order_less_imp_le])  
   561 next
   562   case (neg n)
   563   thus ?thesis by (simp del: of_nat_Suc of_nat_add of_nat_1
   564     add: algebra_simps of_nat_1 [where 'a=int, symmetric] of_nat_add [symmetric])
   565 qed
   566 
   567 subsubsection {* Comparisons, for Ordered Rings *}
   568 
   569 lemmas double_eq_0_iff = double_zero
   570 
   571 lemma odd_nonzero:
   572   "1 + z + z \<noteq> (0::int)"
   573 proof (cases z)
   574   case (nonneg n)
   575   have le: "0 \<le> z+z" by (simp add: nonneg add_increasing) 
   576   thus ?thesis using  le_imp_0_less [OF le]
   577     by (auto simp add: add.assoc) 
   578 next
   579   case (neg n)
   580   show ?thesis
   581   proof
   582     assume eq: "1 + z + z = 0"
   583     have "(0::int) < 1 + (int n + int n)"
   584       by (simp add: le_imp_0_less add_increasing) 
   585     also have "... = - (1 + z + z)" 
   586       by (simp add: neg add.assoc [symmetric]) 
   587     also have "... = 0" by (simp add: eq) 
   588     finally have "0<0" ..
   589     thus False by blast
   590   qed
   591 qed
   592 
   593 
   594 subsection {* The Set of Integers *}
   595 
   596 context ring_1
   597 begin
   598 
   599 definition Ints  :: "'a set" where
   600   "Ints = range of_int"
   601 
   602 notation (xsymbols)
   603   Ints  ("\<int>")
   604 
   605 lemma Ints_of_int [simp]: "of_int z \<in> \<int>"
   606   by (simp add: Ints_def)
   607 
   608 lemma Ints_of_nat [simp]: "of_nat n \<in> \<int>"
   609   using Ints_of_int [of "of_nat n"] by simp
   610 
   611 lemma Ints_0 [simp]: "0 \<in> \<int>"
   612   using Ints_of_int [of "0"] by simp
   613 
   614 lemma Ints_1 [simp]: "1 \<in> \<int>"
   615   using Ints_of_int [of "1"] by simp
   616 
   617 lemma Ints_add [simp]: "a \<in> \<int> \<Longrightarrow> b \<in> \<int> \<Longrightarrow> a + b \<in> \<int>"
   618 apply (auto simp add: Ints_def)
   619 apply (rule range_eqI)
   620 apply (rule of_int_add [symmetric])
   621 done
   622 
   623 lemma Ints_minus [simp]: "a \<in> \<int> \<Longrightarrow> -a \<in> \<int>"
   624 apply (auto simp add: Ints_def)
   625 apply (rule range_eqI)
   626 apply (rule of_int_minus [symmetric])
   627 done
   628 
   629 lemma Ints_diff [simp]: "a \<in> \<int> \<Longrightarrow> b \<in> \<int> \<Longrightarrow> a - b \<in> \<int>"
   630 apply (auto simp add: Ints_def)
   631 apply (rule range_eqI)
   632 apply (rule of_int_diff [symmetric])
   633 done
   634 
   635 lemma Ints_mult [simp]: "a \<in> \<int> \<Longrightarrow> b \<in> \<int> \<Longrightarrow> a * b \<in> \<int>"
   636 apply (auto simp add: Ints_def)
   637 apply (rule range_eqI)
   638 apply (rule of_int_mult [symmetric])
   639 done
   640 
   641 lemma Ints_power [simp]: "a \<in> \<int> \<Longrightarrow> a ^ n \<in> \<int>"
   642 by (induct n) simp_all
   643 
   644 lemma Ints_cases [cases set: Ints]:
   645   assumes "q \<in> \<int>"
   646   obtains (of_int) z where "q = of_int z"
   647   unfolding Ints_def
   648 proof -
   649   from `q \<in> \<int>` have "q \<in> range of_int" unfolding Ints_def .
   650   then obtain z where "q = of_int z" ..
   651   then show thesis ..
   652 qed
   653 
   654 lemma Ints_induct [case_names of_int, induct set: Ints]:
   655   "q \<in> \<int> \<Longrightarrow> (\<And>z. P (of_int z)) \<Longrightarrow> P q"
   656   by (rule Ints_cases) auto
   657 
   658 end
   659 
   660 text {* The premise involving @{term Ints} prevents @{term "a = 1/2"}. *}
   661 
   662 lemma Ints_double_eq_0_iff:
   663   assumes in_Ints: "a \<in> Ints"
   664   shows "(a + a = 0) = (a = (0::'a::ring_char_0))"
   665 proof -
   666   from in_Ints have "a \<in> range of_int" unfolding Ints_def [symmetric] .
   667   then obtain z where a: "a = of_int z" ..
   668   show ?thesis
   669   proof
   670     assume "a = 0"
   671     thus "a + a = 0" by simp
   672   next
   673     assume eq: "a + a = 0"
   674     hence "of_int (z + z) = (of_int 0 :: 'a)" by (simp add: a)
   675     hence "z + z = 0" by (simp only: of_int_eq_iff)
   676     hence "z = 0" by (simp only: double_eq_0_iff)
   677     thus "a = 0" by (simp add: a)
   678   qed
   679 qed
   680 
   681 lemma Ints_odd_nonzero:
   682   assumes in_Ints: "a \<in> Ints"
   683   shows "1 + a + a \<noteq> (0::'a::ring_char_0)"
   684 proof -
   685   from in_Ints have "a \<in> range of_int" unfolding Ints_def [symmetric] .
   686   then obtain z where a: "a = of_int z" ..
   687   show ?thesis
   688   proof
   689     assume eq: "1 + a + a = 0"
   690     hence "of_int (1 + z + z) = (of_int 0 :: 'a)" by (simp add: a)
   691     hence "1 + z + z = 0" by (simp only: of_int_eq_iff)
   692     with odd_nonzero show False by blast
   693   qed
   694 qed 
   695 
   696 lemma Nats_numeral [simp]: "numeral w \<in> Nats"
   697   using of_nat_in_Nats [of "numeral w"] by simp
   698 
   699 lemma Ints_odd_less_0: 
   700   assumes in_Ints: "a \<in> Ints"
   701   shows "(1 + a + a < 0) = (a < (0::'a::linordered_idom))"
   702 proof -
   703   from in_Ints have "a \<in> range of_int" unfolding Ints_def [symmetric] .
   704   then obtain z where a: "a = of_int z" ..
   705   hence "((1::'a) + a + a < 0) = (of_int (1 + z + z) < (of_int 0 :: 'a))"
   706     by (simp add: a)
   707   also have "... = (z < 0)" by (simp only: of_int_less_iff odd_less_0_iff)
   708   also have "... = (a < 0)" by (simp add: a)
   709   finally show ?thesis .
   710 qed
   711 
   712 
   713 subsection {* @{term setsum} and @{term setprod} *}
   714 
   715 lemma of_nat_setsum: "of_nat (setsum f A) = (\<Sum>x\<in>A. of_nat(f x))"
   716   apply (cases "finite A")
   717   apply (erule finite_induct, auto)
   718   done
   719 
   720 lemma of_int_setsum: "of_int (setsum f A) = (\<Sum>x\<in>A. of_int(f x))"
   721   apply (cases "finite A")
   722   apply (erule finite_induct, auto)
   723   done
   724 
   725 lemma of_nat_setprod: "of_nat (setprod f A) = (\<Prod>x\<in>A. of_nat(f x))"
   726   apply (cases "finite A")
   727   apply (erule finite_induct, auto simp add: of_nat_mult)
   728   done
   729 
   730 lemma of_int_setprod: "of_int (setprod f A) = (\<Prod>x\<in>A. of_int(f x))"
   731   apply (cases "finite A")
   732   apply (erule finite_induct, auto)
   733   done
   734 
   735 lemmas int_setsum = of_nat_setsum [where 'a=int]
   736 lemmas int_setprod = of_nat_setprod [where 'a=int]
   737 
   738 
   739 text {* Legacy theorems *}
   740 
   741 lemmas zle_int = of_nat_le_iff [where 'a=int]
   742 lemmas int_int_eq = of_nat_eq_iff [where 'a=int]
   743 lemmas numeral_1_eq_1 = numeral_One
   744 
   745 subsection {* Setting up simplification procedures *}
   746 
   747 lemmas of_int_simps =
   748   of_int_0 of_int_1 of_int_add of_int_mult
   749 
   750 ML_file "Tools/int_arith.ML"
   751 declaration {* K Int_Arith.setup *}
   752 
   753 simproc_setup fast_arith ("(m::'a::linordered_idom) < n" |
   754   "(m::'a::linordered_idom) <= n" |
   755   "(m::'a::linordered_idom) = n") =
   756   {* fn _ => fn ss => fn ct => Lin_Arith.simproc ss (term_of ct) *}
   757 
   758 
   759 subsection{*More Inequality Reasoning*}
   760 
   761 lemma zless_add1_eq: "(w < z + (1::int)) = (w<z | w=z)"
   762 by arith
   763 
   764 lemma add1_zle_eq: "(w + (1::int) \<le> z) = (w<z)"
   765 by arith
   766 
   767 lemma zle_diff1_eq [simp]: "(w \<le> z - (1::int)) = (w<z)"
   768 by arith
   769 
   770 lemma zle_add1_eq_le [simp]: "(w < z + (1::int)) = (w\<le>z)"
   771 by arith
   772 
   773 lemma int_one_le_iff_zero_less: "((1::int) \<le> z) = (0 < z)"
   774 by arith
   775 
   776 
   777 subsection{*The functions @{term nat} and @{term int}*}
   778 
   779 text{*Simplify the term @{term "w + - z"}*}
   780 
   781 lemma one_less_nat_eq [simp]: "(Suc 0 < nat z) = (1 < z)"
   782 apply (insert zless_nat_conj [of 1 z])
   783 apply auto
   784 done
   785 
   786 text{*This simplifies expressions of the form @{term "int n = z"} where
   787       z is an integer literal.*}
   788 lemmas int_eq_iff_numeral [simp] = int_eq_iff [of _ "numeral v"] for v
   789 
   790 lemma split_nat [arith_split]:
   791   "P(nat(i::int)) = ((\<forall>n. i = int n \<longrightarrow> P n) & (i < 0 \<longrightarrow> P 0))"
   792   (is "?P = (?L & ?R)")
   793 proof (cases "i < 0")
   794   case True thus ?thesis by auto
   795 next
   796   case False
   797   have "?P = ?L"
   798   proof
   799     assume ?P thus ?L using False by clarsimp
   800   next
   801     assume ?L thus ?P using False by simp
   802   qed
   803   with False show ?thesis by simp
   804 qed
   805 
   806 lemma nat_abs_int_diff: "nat \<bar>int a - int b\<bar> = (if a \<le> b then b - a else a - b)"
   807   by auto
   808 
   809 lemma nat_int_add: "nat (int a + int b) = a + b"
   810   by auto
   811 
   812 context ring_1
   813 begin
   814 
   815 lemma of_int_of_nat [nitpick_simp]:
   816   "of_int k = (if k < 0 then - of_nat (nat (- k)) else of_nat (nat k))"
   817 proof (cases "k < 0")
   818   case True then have "0 \<le> - k" by simp
   819   then have "of_nat (nat (- k)) = of_int (- k)" by (rule of_nat_nat)
   820   with True show ?thesis by simp
   821 next
   822   case False then show ?thesis by (simp add: not_less of_nat_nat)
   823 qed
   824 
   825 end
   826 
   827 lemma nat_mult_distrib:
   828   fixes z z' :: int
   829   assumes "0 \<le> z"
   830   shows "nat (z * z') = nat z * nat z'"
   831 proof (cases "0 \<le> z'")
   832   case False with assms have "z * z' \<le> 0"
   833     by (simp add: not_le mult_le_0_iff)
   834   then have "nat (z * z') = 0" by simp
   835   moreover from False have "nat z' = 0" by simp
   836   ultimately show ?thesis by simp
   837 next
   838   case True with assms have ge_0: "z * z' \<ge> 0" by (simp add: zero_le_mult_iff)
   839   show ?thesis
   840     by (rule injD [of "of_nat :: nat \<Rightarrow> int", OF inj_of_nat])
   841       (simp only: of_nat_mult of_nat_nat [OF True]
   842          of_nat_nat [OF assms] of_nat_nat [OF ge_0], simp)
   843 qed
   844 
   845 lemma nat_mult_distrib_neg: "z \<le> (0::int) ==> nat(z*z') = nat(-z) * nat(-z')"
   846 apply (rule trans)
   847 apply (rule_tac [2] nat_mult_distrib, auto)
   848 done
   849 
   850 lemma nat_abs_mult_distrib: "nat (abs (w * z)) = nat (abs w) * nat (abs z)"
   851 apply (cases "z=0 | w=0")
   852 apply (auto simp add: abs_if nat_mult_distrib [symmetric] 
   853                       nat_mult_distrib_neg [symmetric] mult_less_0_iff)
   854 done
   855 
   856 lemma Suc_nat_eq_nat_zadd1: "(0::int) <= z ==> Suc (nat z) = nat (1 + z)"
   857 apply (rule sym)
   858 apply (simp add: nat_eq_iff)
   859 done
   860 
   861 lemma diff_nat_eq_if:
   862      "nat z - nat z' =  
   863         (if z' < 0 then nat z   
   864          else let d = z-z' in     
   865               if d < 0 then 0 else nat d)"
   866 by (simp add: Let_def nat_diff_distrib [symmetric])
   867 
   868 lemma nat_numeral_diff_1 [simp]:
   869   "numeral v - (1::nat) = nat (numeral v - 1)"
   870   using diff_nat_numeral [of v Num.One] by simp
   871 
   872 
   873 subsection "Induction principles for int"
   874 
   875 text{*Well-founded segments of the integers*}
   876 
   877 definition
   878   int_ge_less_than  ::  "int => (int * int) set"
   879 where
   880   "int_ge_less_than d = {(z',z). d \<le> z' & z' < z}"
   881 
   882 theorem wf_int_ge_less_than: "wf (int_ge_less_than d)"
   883 proof -
   884   have "int_ge_less_than d \<subseteq> measure (%z. nat (z-d))"
   885     by (auto simp add: int_ge_less_than_def)
   886   thus ?thesis 
   887     by (rule wf_subset [OF wf_measure]) 
   888 qed
   889 
   890 text{*This variant looks odd, but is typical of the relations suggested
   891 by RankFinder.*}
   892 
   893 definition
   894   int_ge_less_than2 ::  "int => (int * int) set"
   895 where
   896   "int_ge_less_than2 d = {(z',z). d \<le> z & z' < z}"
   897 
   898 theorem wf_int_ge_less_than2: "wf (int_ge_less_than2 d)"
   899 proof -
   900   have "int_ge_less_than2 d \<subseteq> measure (%z. nat (1+z-d))" 
   901     by (auto simp add: int_ge_less_than2_def)
   902   thus ?thesis 
   903     by (rule wf_subset [OF wf_measure]) 
   904 qed
   905 
   906 (* `set:int': dummy construction *)
   907 theorem int_ge_induct [case_names base step, induct set: int]:
   908   fixes i :: int
   909   assumes ge: "k \<le> i" and
   910     base: "P k" and
   911     step: "\<And>i. k \<le> i \<Longrightarrow> P i \<Longrightarrow> P (i + 1)"
   912   shows "P i"
   913 proof -
   914   { fix n
   915     have "\<And>i::int. n = nat (i - k) \<Longrightarrow> k \<le> i \<Longrightarrow> P i"
   916     proof (induct n)
   917       case 0
   918       hence "i = k" by arith
   919       thus "P i" using base by simp
   920     next
   921       case (Suc n)
   922       then have "n = nat((i - 1) - k)" by arith
   923       moreover
   924       have ki1: "k \<le> i - 1" using Suc.prems by arith
   925       ultimately
   926       have "P (i - 1)" by (rule Suc.hyps)
   927       from step [OF ki1 this] show ?case by simp
   928     qed
   929   }
   930   with ge show ?thesis by fast
   931 qed
   932 
   933 (* `set:int': dummy construction *)
   934 theorem int_gr_induct [case_names base step, induct set: int]:
   935   assumes gr: "k < (i::int)" and
   936         base: "P(k+1)" and
   937         step: "\<And>i. \<lbrakk>k < i; P i\<rbrakk> \<Longrightarrow> P(i+1)"
   938   shows "P i"
   939 apply(rule int_ge_induct[of "k + 1"])
   940   using gr apply arith
   941  apply(rule base)
   942 apply (rule step, simp+)
   943 done
   944 
   945 theorem int_le_induct [consumes 1, case_names base step]:
   946   assumes le: "i \<le> (k::int)" and
   947         base: "P(k)" and
   948         step: "\<And>i. \<lbrakk>i \<le> k; P i\<rbrakk> \<Longrightarrow> P(i - 1)"
   949   shows "P i"
   950 proof -
   951   { fix n
   952     have "\<And>i::int. n = nat(k-i) \<Longrightarrow> i \<le> k \<Longrightarrow> P i"
   953     proof (induct n)
   954       case 0
   955       hence "i = k" by arith
   956       thus "P i" using base by simp
   957     next
   958       case (Suc n)
   959       hence "n = nat (k - (i + 1))" by arith
   960       moreover
   961       have ki1: "i + 1 \<le> k" using Suc.prems by arith
   962       ultimately
   963       have "P (i + 1)" by(rule Suc.hyps)
   964       from step[OF ki1 this] show ?case by simp
   965     qed
   966   }
   967   with le show ?thesis by fast
   968 qed
   969 
   970 theorem int_less_induct [consumes 1, case_names base step]:
   971   assumes less: "(i::int) < k" and
   972         base: "P(k - 1)" and
   973         step: "\<And>i. \<lbrakk>i < k; P i\<rbrakk> \<Longrightarrow> P(i - 1)"
   974   shows "P i"
   975 apply(rule int_le_induct[of _ "k - 1"])
   976   using less apply arith
   977  apply(rule base)
   978 apply (rule step, simp+)
   979 done
   980 
   981 theorem int_induct [case_names base step1 step2]:
   982   fixes k :: int
   983   assumes base: "P k"
   984     and step1: "\<And>i. k \<le> i \<Longrightarrow> P i \<Longrightarrow> P (i + 1)"
   985     and step2: "\<And>i. k \<ge> i \<Longrightarrow> P i \<Longrightarrow> P (i - 1)"
   986   shows "P i"
   987 proof -
   988   have "i \<le> k \<or> i \<ge> k" by arith
   989   then show ?thesis
   990   proof
   991     assume "i \<ge> k"
   992     then show ?thesis using base
   993       by (rule int_ge_induct) (fact step1)
   994   next
   995     assume "i \<le> k"
   996     then show ?thesis using base
   997       by (rule int_le_induct) (fact step2)
   998   qed
   999 qed
  1000 
  1001 subsection{*Intermediate value theorems*}
  1002 
  1003 lemma int_val_lemma:
  1004      "(\<forall>i<n::nat. abs(f(i+1) - f i) \<le> 1) -->  
  1005       f 0 \<le> k --> k \<le> f n --> (\<exists>i \<le> n. f i = (k::int))"
  1006 unfolding One_nat_def
  1007 apply (induct n)
  1008 apply simp
  1009 apply (intro strip)
  1010 apply (erule impE, simp)
  1011 apply (erule_tac x = n in allE, simp)
  1012 apply (case_tac "k = f (Suc n)")
  1013 apply force
  1014 apply (erule impE)
  1015  apply (simp add: abs_if split add: split_if_asm)
  1016 apply (blast intro: le_SucI)
  1017 done
  1018 
  1019 lemmas nat0_intermed_int_val = int_val_lemma [rule_format (no_asm)]
  1020 
  1021 lemma nat_intermed_int_val:
  1022      "[| \<forall>i. m \<le> i & i < n --> abs(f(i + 1::nat) - f i) \<le> 1; m < n;  
  1023          f m \<le> k; k \<le> f n |] ==> ? i. m \<le> i & i \<le> n & f i = (k::int)"
  1024 apply (cut_tac n = "n-m" and f = "%i. f (i+m) " and k = k 
  1025        in int_val_lemma)
  1026 unfolding One_nat_def
  1027 apply simp
  1028 apply (erule exE)
  1029 apply (rule_tac x = "i+m" in exI, arith)
  1030 done
  1031 
  1032 
  1033 subsection{*Products and 1, by T. M. Rasmussen*}
  1034 
  1035 lemma zabs_less_one_iff [simp]: "(\<bar>z\<bar> < 1) = (z = (0::int))"
  1036 by arith
  1037 
  1038 lemma abs_zmult_eq_1:
  1039   assumes mn: "\<bar>m * n\<bar> = 1"
  1040   shows "\<bar>m\<bar> = (1::int)"
  1041 proof -
  1042   have 0: "m \<noteq> 0 & n \<noteq> 0" using mn
  1043     by auto
  1044   have "~ (2 \<le> \<bar>m\<bar>)"
  1045   proof
  1046     assume "2 \<le> \<bar>m\<bar>"
  1047     hence "2*\<bar>n\<bar> \<le> \<bar>m\<bar>*\<bar>n\<bar>"
  1048       by (simp add: mult_mono 0) 
  1049     also have "... = \<bar>m*n\<bar>" 
  1050       by (simp add: abs_mult)
  1051     also have "... = 1"
  1052       by (simp add: mn)
  1053     finally have "2*\<bar>n\<bar> \<le> 1" .
  1054     thus "False" using 0
  1055       by arith
  1056   qed
  1057   thus ?thesis using 0
  1058     by auto
  1059 qed
  1060 
  1061 lemma pos_zmult_eq_1_iff_lemma: "(m * n = 1) ==> m = (1::int) | m = -1"
  1062 by (insert abs_zmult_eq_1 [of m n], arith)
  1063 
  1064 lemma pos_zmult_eq_1_iff:
  1065   assumes "0 < (m::int)" shows "(m * n = 1) = (m = 1 & n = 1)"
  1066 proof -
  1067   from assms have "m * n = 1 ==> m = 1" by (auto dest: pos_zmult_eq_1_iff_lemma)
  1068   thus ?thesis by (auto dest: pos_zmult_eq_1_iff_lemma)
  1069 qed
  1070 
  1071 lemma zmult_eq_1_iff: "(m*n = (1::int)) = ((m = 1 & n = 1) | (m = -1 & n = -1))"
  1072 apply (rule iffI) 
  1073  apply (frule pos_zmult_eq_1_iff_lemma)
  1074  apply (simp add: mult.commute [of m]) 
  1075  apply (frule pos_zmult_eq_1_iff_lemma, auto) 
  1076 done
  1077 
  1078 lemma infinite_UNIV_int: "\<not> finite (UNIV::int set)"
  1079 proof
  1080   assume "finite (UNIV::int set)"
  1081   moreover have "inj (\<lambda>i\<Colon>int. 2 * i)"
  1082     by (rule injI) simp
  1083   ultimately have "surj (\<lambda>i\<Colon>int. 2 * i)"
  1084     by (rule finite_UNIV_inj_surj)
  1085   then obtain i :: int where "1 = 2 * i" by (rule surjE)
  1086   then show False by (simp add: pos_zmult_eq_1_iff)
  1087 qed
  1088 
  1089 
  1090 subsection {* Further theorems on numerals *}
  1091 
  1092 subsubsection{*Special Simplification for Constants*}
  1093 
  1094 text{*These distributive laws move literals inside sums and differences.*}
  1095 
  1096 lemmas distrib_right_numeral [simp] = distrib_right [of _ _ "numeral v"] for v
  1097 lemmas distrib_left_numeral [simp] = distrib_left [of "numeral v"] for v
  1098 lemmas left_diff_distrib_numeral [simp] = left_diff_distrib [of _ _ "numeral v"] for v
  1099 lemmas right_diff_distrib_numeral [simp] = right_diff_distrib [of "numeral v"] for v
  1100 
  1101 text{*These are actually for fields, like real: but where else to put them?*}
  1102 
  1103 lemmas zero_less_divide_iff_numeral [simp, no_atp] = zero_less_divide_iff [of "numeral w"] for w
  1104 lemmas divide_less_0_iff_numeral [simp, no_atp] = divide_less_0_iff [of "numeral w"] for w
  1105 lemmas zero_le_divide_iff_numeral [simp, no_atp] = zero_le_divide_iff [of "numeral w"] for w
  1106 lemmas divide_le_0_iff_numeral [simp, no_atp] = divide_le_0_iff [of "numeral w"] for w
  1107 
  1108 
  1109 text {*Replaces @{text "inverse #nn"} by @{text "1/#nn"}.  It looks
  1110   strange, but then other simprocs simplify the quotient.*}
  1111 
  1112 lemmas inverse_eq_divide_numeral [simp] =
  1113   inverse_eq_divide [of "numeral w"] for w
  1114 
  1115 lemmas inverse_eq_divide_neg_numeral [simp] =
  1116   inverse_eq_divide [of "- numeral w"] for w
  1117 
  1118 text {*These laws simplify inequalities, moving unary minus from a term
  1119 into the literal.*}
  1120 
  1121 lemmas equation_minus_iff_numeral [no_atp] =
  1122   equation_minus_iff [of "numeral v"] for v
  1123 
  1124 lemmas minus_equation_iff_numeral [no_atp] =
  1125   minus_equation_iff [of _ "numeral v"] for v
  1126 
  1127 lemmas le_minus_iff_numeral [no_atp] =
  1128   le_minus_iff [of "numeral v"] for v
  1129 
  1130 lemmas minus_le_iff_numeral [no_atp] =
  1131   minus_le_iff [of _ "numeral v"] for v
  1132 
  1133 lemmas less_minus_iff_numeral [no_atp] =
  1134   less_minus_iff [of "numeral v"] for v
  1135 
  1136 lemmas minus_less_iff_numeral [no_atp] =
  1137   minus_less_iff [of _ "numeral v"] for v
  1138 
  1139 -- {* FIXME maybe simproc *}
  1140 
  1141 
  1142 text {*Cancellation of constant factors in comparisons (@{text "<"} and @{text "\<le>"}) *}
  1143 
  1144 lemmas mult_less_cancel_left_numeral [simp, no_atp] = mult_less_cancel_left [of "numeral v"] for v
  1145 lemmas mult_less_cancel_right_numeral [simp, no_atp] = mult_less_cancel_right [of _ "numeral v"] for v
  1146 lemmas mult_le_cancel_left_numeral [simp, no_atp] = mult_le_cancel_left [of "numeral v"] for v
  1147 lemmas mult_le_cancel_right_numeral [simp, no_atp] = mult_le_cancel_right [of _ "numeral v"] for v
  1148 
  1149 
  1150 text {*Multiplying out constant divisors in comparisons (@{text "<"}, @{text "\<le>"} and @{text "="}) *}
  1151 
  1152 lemmas le_divide_eq_numeral1 [simp] =
  1153   pos_le_divide_eq [of "numeral w", OF zero_less_numeral]
  1154   neg_le_divide_eq [of "- numeral w", OF neg_numeral_less_zero] for w
  1155 
  1156 lemmas divide_le_eq_numeral1 [simp] =
  1157   pos_divide_le_eq [of "numeral w", OF zero_less_numeral]
  1158   neg_divide_le_eq [of "- numeral w", OF neg_numeral_less_zero] for w
  1159 
  1160 lemmas less_divide_eq_numeral1 [simp] =
  1161   pos_less_divide_eq [of "numeral w", OF zero_less_numeral]
  1162   neg_less_divide_eq [of "- numeral w", OF neg_numeral_less_zero] for w
  1163 
  1164 lemmas divide_less_eq_numeral1 [simp] =
  1165   pos_divide_less_eq [of "numeral w", OF zero_less_numeral]
  1166   neg_divide_less_eq [of "- numeral w", OF neg_numeral_less_zero] for w
  1167 
  1168 lemmas eq_divide_eq_numeral1 [simp] =
  1169   eq_divide_eq [of _ _ "numeral w"]
  1170   eq_divide_eq [of _ _ "- numeral w"] for w
  1171 
  1172 lemmas divide_eq_eq_numeral1 [simp] =
  1173   divide_eq_eq [of _ "numeral w"]
  1174   divide_eq_eq [of _ "- numeral w"] for w
  1175 
  1176 
  1177 subsubsection{*Optional Simplification Rules Involving Constants*}
  1178 
  1179 text{*Simplify quotients that are compared with a literal constant.*}
  1180 
  1181 lemmas le_divide_eq_numeral =
  1182   le_divide_eq [of "numeral w"]
  1183   le_divide_eq [of "- numeral w"] for w
  1184 
  1185 lemmas divide_le_eq_numeral =
  1186   divide_le_eq [of _ _ "numeral w"]
  1187   divide_le_eq [of _ _ "- numeral w"] for w
  1188 
  1189 lemmas less_divide_eq_numeral =
  1190   less_divide_eq [of "numeral w"]
  1191   less_divide_eq [of "- numeral w"] for w
  1192 
  1193 lemmas divide_less_eq_numeral =
  1194   divide_less_eq [of _ _ "numeral w"]
  1195   divide_less_eq [of _ _ "- numeral w"] for w
  1196 
  1197 lemmas eq_divide_eq_numeral =
  1198   eq_divide_eq [of "numeral w"]
  1199   eq_divide_eq [of "- numeral w"] for w
  1200 
  1201 lemmas divide_eq_eq_numeral =
  1202   divide_eq_eq [of _ _ "numeral w"]
  1203   divide_eq_eq [of _ _ "- numeral w"] for w
  1204 
  1205 
  1206 text{*Not good as automatic simprules because they cause case splits.*}
  1207 lemmas divide_const_simps =
  1208   le_divide_eq_numeral divide_le_eq_numeral less_divide_eq_numeral
  1209   divide_less_eq_numeral eq_divide_eq_numeral divide_eq_eq_numeral
  1210   le_divide_eq_1 divide_le_eq_1 less_divide_eq_1 divide_less_eq_1
  1211 
  1212 
  1213 subsection {* The divides relation *}
  1214 
  1215 lemma zdvd_antisym_nonneg:
  1216     "0 <= m ==> 0 <= n ==> m dvd n ==> n dvd m ==> m = (n::int)"
  1217   apply (simp add: dvd_def, auto)
  1218   apply (auto simp add: mult.assoc zero_le_mult_iff zmult_eq_1_iff)
  1219   done
  1220 
  1221 lemma zdvd_antisym_abs: assumes "(a::int) dvd b" and "b dvd a" 
  1222   shows "\<bar>a\<bar> = \<bar>b\<bar>"
  1223 proof cases
  1224   assume "a = 0" with assms show ?thesis by simp
  1225 next
  1226   assume "a \<noteq> 0"
  1227   from `a dvd b` obtain k where k:"b = a*k" unfolding dvd_def by blast 
  1228   from `b dvd a` obtain k' where k':"a = b*k'" unfolding dvd_def by blast 
  1229   from k k' have "a = a*k*k'" by simp
  1230   with mult_cancel_left1[where c="a" and b="k*k'"]
  1231   have kk':"k*k' = 1" using `a\<noteq>0` by (simp add: mult.assoc)
  1232   hence "k = 1 \<and> k' = 1 \<or> k = -1 \<and> k' = -1" by (simp add: zmult_eq_1_iff)
  1233   thus ?thesis using k k' by auto
  1234 qed
  1235 
  1236 lemma zdvd_zdiffD: "k dvd m - n ==> k dvd n ==> k dvd (m::int)"
  1237   using dvd_add_right_iff [of k "- n" m] by simp 
  1238 
  1239 lemma zdvd_reduce: "(k dvd n + k * m) = (k dvd (n::int))"
  1240   using dvd_add_times_triv_right_iff [of k n m] by (simp add: ac_simps)
  1241 
  1242 lemma dvd_imp_le_int:
  1243   fixes d i :: int
  1244   assumes "i \<noteq> 0" and "d dvd i"
  1245   shows "\<bar>d\<bar> \<le> \<bar>i\<bar>"
  1246 proof -
  1247   from `d dvd i` obtain k where "i = d * k" ..
  1248   with `i \<noteq> 0` have "k \<noteq> 0" by auto
  1249   then have "1 \<le> \<bar>k\<bar>" and "0 \<le> \<bar>d\<bar>" by auto
  1250   then have "\<bar>d\<bar> * 1 \<le> \<bar>d\<bar> * \<bar>k\<bar>" by (rule mult_left_mono)
  1251   with `i = d * k` show ?thesis by (simp add: abs_mult)
  1252 qed
  1253 
  1254 lemma zdvd_not_zless:
  1255   fixes m n :: int
  1256   assumes "0 < m" and "m < n"
  1257   shows "\<not> n dvd m"
  1258 proof
  1259   from assms have "0 < n" by auto
  1260   assume "n dvd m" then obtain k where k: "m = n * k" ..
  1261   with `0 < m` have "0 < n * k" by auto
  1262   with `0 < n` have "0 < k" by (simp add: zero_less_mult_iff)
  1263   with k `0 < n` `m < n` have "n * k < n * 1" by simp
  1264   with `0 < n` `0 < k` show False unfolding mult_less_cancel_left by auto
  1265 qed
  1266 
  1267 lemma zdvd_mult_cancel: assumes d:"k * m dvd k * n" and kz:"k \<noteq> (0::int)"
  1268   shows "m dvd n"
  1269 proof-
  1270   from d obtain h where h: "k*n = k*m * h" unfolding dvd_def by blast
  1271   {assume "n \<noteq> m*h" hence "k* n \<noteq> k* (m*h)" using kz by simp
  1272     with h have False by (simp add: mult.assoc)}
  1273   hence "n = m * h" by blast
  1274   thus ?thesis by simp
  1275 qed
  1276 
  1277 theorem zdvd_int: "(x dvd y) = (int x dvd int y)"
  1278 proof -
  1279   have "\<And>k. int y = int x * k \<Longrightarrow> x dvd y"
  1280   proof -
  1281     fix k
  1282     assume A: "int y = int x * k"
  1283     then show "x dvd y"
  1284     proof (cases k)
  1285       case (nonneg n)
  1286       with A have "y = x * n" by (simp add: of_nat_mult [symmetric])
  1287       then show ?thesis ..
  1288     next
  1289       case (neg n)
  1290       with A have "int y = int x * (- int (Suc n))" by simp
  1291       also have "\<dots> = - (int x * int (Suc n))" by (simp only: mult_minus_right)
  1292       also have "\<dots> = - int (x * Suc n)" by (simp only: of_nat_mult [symmetric])
  1293       finally have "- int (x * Suc n) = int y" ..
  1294       then show ?thesis by (simp only: negative_eq_positive) auto
  1295     qed
  1296   qed
  1297   then show ?thesis by (auto elim!: dvdE simp only: dvd_triv_left of_nat_mult)
  1298 qed
  1299 
  1300 lemma zdvd1_eq[simp]: "(x::int) dvd 1 = (\<bar>x\<bar> = 1)"
  1301 proof
  1302   assume d: "x dvd 1" hence "int (nat \<bar>x\<bar>) dvd int (nat 1)" by simp
  1303   hence "nat \<bar>x\<bar> dvd 1" by (simp add: zdvd_int)
  1304   hence "nat \<bar>x\<bar> = 1"  by simp
  1305   thus "\<bar>x\<bar> = 1" by (cases "x < 0") auto
  1306 next
  1307   assume "\<bar>x\<bar>=1"
  1308   then have "x = 1 \<or> x = -1" by auto
  1309   then show "x dvd 1" by (auto intro: dvdI)
  1310 qed
  1311 
  1312 lemma zdvd_mult_cancel1: 
  1313   assumes mp:"m \<noteq>(0::int)" shows "(m * n dvd m) = (\<bar>n\<bar> = 1)"
  1314 proof
  1315   assume n1: "\<bar>n\<bar> = 1" thus "m * n dvd m" 
  1316     by (cases "n >0") (auto simp add: minus_equation_iff)
  1317 next
  1318   assume H: "m * n dvd m" hence H2: "m * n dvd m * 1" by simp
  1319   from zdvd_mult_cancel[OF H2 mp] show "\<bar>n\<bar> = 1" by (simp only: zdvd1_eq)
  1320 qed
  1321 
  1322 lemma int_dvd_iff: "(int m dvd z) = (m dvd nat (abs z))"
  1323   unfolding zdvd_int by (cases "z \<ge> 0") simp_all
  1324 
  1325 lemma dvd_int_iff: "(z dvd int m) = (nat (abs z) dvd m)"
  1326   unfolding zdvd_int by (cases "z \<ge> 0") simp_all
  1327 
  1328 lemma dvd_int_unfold_dvd_nat:
  1329   "k dvd l \<longleftrightarrow> nat \<bar>k\<bar> dvd nat \<bar>l\<bar>"
  1330   unfolding dvd_int_iff [symmetric] by simp
  1331 
  1332 lemma nat_dvd_iff: "(nat z dvd m) = (if 0 \<le> z then (z dvd int m) else m = 0)"
  1333   by (auto simp add: dvd_int_iff)
  1334 
  1335 lemma eq_nat_nat_iff:
  1336   "0 \<le> z \<Longrightarrow> 0 \<le> z' \<Longrightarrow> nat z = nat z' \<longleftrightarrow> z = z'"
  1337   by (auto elim!: nonneg_eq_int)
  1338 
  1339 lemma nat_power_eq:
  1340   "0 \<le> z \<Longrightarrow> nat (z ^ n) = nat z ^ n"
  1341   by (induct n) (simp_all add: nat_mult_distrib)
  1342 
  1343 lemma zdvd_imp_le: "[| z dvd n; 0 < n |] ==> z \<le> (n::int)"
  1344   apply (cases n)
  1345   apply (auto simp add: dvd_int_iff)
  1346   apply (cases z)
  1347   apply (auto simp add: dvd_imp_le)
  1348   done
  1349 
  1350 lemma zdvd_period:
  1351   fixes a d :: int
  1352   assumes "a dvd d"
  1353   shows "a dvd (x + t) \<longleftrightarrow> a dvd ((x + c * d) + t)"
  1354 proof -
  1355   from assms obtain k where "d = a * k" by (rule dvdE)
  1356   show ?thesis
  1357   proof
  1358     assume "a dvd (x + t)"
  1359     then obtain l where "x + t = a * l" by (rule dvdE)
  1360     then have "x = a * l - t" by simp
  1361     with `d = a * k` show "a dvd x + c * d + t" by simp
  1362   next
  1363     assume "a dvd x + c * d + t"
  1364     then obtain l where "x + c * d + t = a * l" by (rule dvdE)
  1365     then have "x = a * l - c * d - t" by simp
  1366     with `d = a * k` show "a dvd (x + t)" by simp
  1367   qed
  1368 qed
  1369 
  1370 
  1371 subsection {* Finiteness of intervals *}
  1372 
  1373 lemma finite_interval_int1 [iff]: "finite {i :: int. a <= i & i <= b}"
  1374 proof (cases "a <= b")
  1375   case True
  1376   from this show ?thesis
  1377   proof (induct b rule: int_ge_induct)
  1378     case base
  1379     have "{i. a <= i & i <= a} = {a}" by auto
  1380     from this show ?case by simp
  1381   next
  1382     case (step b)
  1383     from this have "{i. a <= i & i <= b + 1} = {i. a <= i & i <= b} \<union> {b + 1}" by auto
  1384     from this step show ?case by simp
  1385   qed
  1386 next
  1387   case False from this show ?thesis
  1388     by (metis (lifting, no_types) Collect_empty_eq finite.emptyI order_trans)
  1389 qed
  1390 
  1391 lemma finite_interval_int2 [iff]: "finite {i :: int. a <= i & i < b}"
  1392 by (rule rev_finite_subset[OF finite_interval_int1[of "a" "b"]]) auto
  1393 
  1394 lemma finite_interval_int3 [iff]: "finite {i :: int. a < i & i <= b}"
  1395 by (rule rev_finite_subset[OF finite_interval_int1[of "a" "b"]]) auto
  1396 
  1397 lemma finite_interval_int4 [iff]: "finite {i :: int. a < i & i < b}"
  1398 by (rule rev_finite_subset[OF finite_interval_int1[of "a" "b"]]) auto
  1399 
  1400 
  1401 subsection {* Configuration of the code generator *}
  1402 
  1403 text {* Constructors *}
  1404 
  1405 definition Pos :: "num \<Rightarrow> int" where
  1406   [simp, code_abbrev]: "Pos = numeral"
  1407 
  1408 definition Neg :: "num \<Rightarrow> int" where
  1409   [simp, code_abbrev]: "Neg n = - (Pos n)"
  1410 
  1411 code_datatype "0::int" Pos Neg
  1412 
  1413 
  1414 text {* Auxiliary operations *}
  1415 
  1416 definition dup :: "int \<Rightarrow> int" where
  1417   [simp]: "dup k = k + k"
  1418 
  1419 lemma dup_code [code]:
  1420   "dup 0 = 0"
  1421   "dup (Pos n) = Pos (Num.Bit0 n)"
  1422   "dup (Neg n) = Neg (Num.Bit0 n)"
  1423   unfolding Pos_def Neg_def
  1424   by (simp_all add: numeral_Bit0)
  1425 
  1426 definition sub :: "num \<Rightarrow> num \<Rightarrow> int" where
  1427   [simp]: "sub m n = numeral m - numeral n"
  1428 
  1429 lemma sub_code [code]:
  1430   "sub Num.One Num.One = 0"
  1431   "sub (Num.Bit0 m) Num.One = Pos (Num.BitM m)"
  1432   "sub (Num.Bit1 m) Num.One = Pos (Num.Bit0 m)"
  1433   "sub Num.One (Num.Bit0 n) = Neg (Num.BitM n)"
  1434   "sub Num.One (Num.Bit1 n) = Neg (Num.Bit0 n)"
  1435   "sub (Num.Bit0 m) (Num.Bit0 n) = dup (sub m n)"
  1436   "sub (Num.Bit1 m) (Num.Bit1 n) = dup (sub m n)"
  1437   "sub (Num.Bit1 m) (Num.Bit0 n) = dup (sub m n) + 1"
  1438   "sub (Num.Bit0 m) (Num.Bit1 n) = dup (sub m n) - 1"
  1439   apply (simp_all only: sub_def dup_def numeral.simps Pos_def Neg_def numeral_BitM)
  1440   apply (simp_all only: algebra_simps minus_diff_eq)
  1441   apply (simp_all only: add.commute [of _ "- (numeral n + numeral n)"])
  1442   apply (simp_all only: minus_add add.assoc left_minus)
  1443   done
  1444 
  1445 text {* Implementations *}
  1446 
  1447 lemma one_int_code [code, code_unfold]:
  1448   "1 = Pos Num.One"
  1449   by simp
  1450 
  1451 lemma plus_int_code [code]:
  1452   "k + 0 = (k::int)"
  1453   "0 + l = (l::int)"
  1454   "Pos m + Pos n = Pos (m + n)"
  1455   "Pos m + Neg n = sub m n"
  1456   "Neg m + Pos n = sub n m"
  1457   "Neg m + Neg n = Neg (m + n)"
  1458   by simp_all
  1459 
  1460 lemma uminus_int_code [code]:
  1461   "uminus 0 = (0::int)"
  1462   "uminus (Pos m) = Neg m"
  1463   "uminus (Neg m) = Pos m"
  1464   by simp_all
  1465 
  1466 lemma minus_int_code [code]:
  1467   "k - 0 = (k::int)"
  1468   "0 - l = uminus (l::int)"
  1469   "Pos m - Pos n = sub m n"
  1470   "Pos m - Neg n = Pos (m + n)"
  1471   "Neg m - Pos n = Neg (m + n)"
  1472   "Neg m - Neg n = sub n m"
  1473   by simp_all
  1474 
  1475 lemma times_int_code [code]:
  1476   "k * 0 = (0::int)"
  1477   "0 * l = (0::int)"
  1478   "Pos m * Pos n = Pos (m * n)"
  1479   "Pos m * Neg n = Neg (m * n)"
  1480   "Neg m * Pos n = Neg (m * n)"
  1481   "Neg m * Neg n = Pos (m * n)"
  1482   by simp_all
  1483 
  1484 instantiation int :: equal
  1485 begin
  1486 
  1487 definition
  1488   "HOL.equal k l \<longleftrightarrow> k = (l::int)"
  1489 
  1490 instance by default (rule equal_int_def)
  1491 
  1492 end
  1493 
  1494 lemma equal_int_code [code]:
  1495   "HOL.equal 0 (0::int) \<longleftrightarrow> True"
  1496   "HOL.equal 0 (Pos l) \<longleftrightarrow> False"
  1497   "HOL.equal 0 (Neg l) \<longleftrightarrow> False"
  1498   "HOL.equal (Pos k) 0 \<longleftrightarrow> False"
  1499   "HOL.equal (Pos k) (Pos l) \<longleftrightarrow> HOL.equal k l"
  1500   "HOL.equal (Pos k) (Neg l) \<longleftrightarrow> False"
  1501   "HOL.equal (Neg k) 0 \<longleftrightarrow> False"
  1502   "HOL.equal (Neg k) (Pos l) \<longleftrightarrow> False"
  1503   "HOL.equal (Neg k) (Neg l) \<longleftrightarrow> HOL.equal k l"
  1504   by (auto simp add: equal)
  1505 
  1506 lemma equal_int_refl [code nbe]:
  1507   "HOL.equal (k::int) k \<longleftrightarrow> True"
  1508   by (fact equal_refl)
  1509 
  1510 lemma less_eq_int_code [code]:
  1511   "0 \<le> (0::int) \<longleftrightarrow> True"
  1512   "0 \<le> Pos l \<longleftrightarrow> True"
  1513   "0 \<le> Neg l \<longleftrightarrow> False"
  1514   "Pos k \<le> 0 \<longleftrightarrow> False"
  1515   "Pos k \<le> Pos l \<longleftrightarrow> k \<le> l"
  1516   "Pos k \<le> Neg l \<longleftrightarrow> False"
  1517   "Neg k \<le> 0 \<longleftrightarrow> True"
  1518   "Neg k \<le> Pos l \<longleftrightarrow> True"
  1519   "Neg k \<le> Neg l \<longleftrightarrow> l \<le> k"
  1520   by simp_all
  1521 
  1522 lemma less_int_code [code]:
  1523   "0 < (0::int) \<longleftrightarrow> False"
  1524   "0 < Pos l \<longleftrightarrow> True"
  1525   "0 < Neg l \<longleftrightarrow> False"
  1526   "Pos k < 0 \<longleftrightarrow> False"
  1527   "Pos k < Pos l \<longleftrightarrow> k < l"
  1528   "Pos k < Neg l \<longleftrightarrow> False"
  1529   "Neg k < 0 \<longleftrightarrow> True"
  1530   "Neg k < Pos l \<longleftrightarrow> True"
  1531   "Neg k < Neg l \<longleftrightarrow> l < k"
  1532   by simp_all
  1533 
  1534 lemma nat_code [code]:
  1535   "nat (Int.Neg k) = 0"
  1536   "nat 0 = 0"
  1537   "nat (Int.Pos k) = nat_of_num k"
  1538   by (simp_all add: nat_of_num_numeral)
  1539 
  1540 lemma (in ring_1) of_int_code [code]:
  1541   "of_int (Int.Neg k) = - numeral k"
  1542   "of_int 0 = 0"
  1543   "of_int (Int.Pos k) = numeral k"
  1544   by simp_all
  1545 
  1546 
  1547 text {* Serializer setup *}
  1548 
  1549 code_identifier
  1550   code_module Int \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
  1551 
  1552 quickcheck_params [default_type = int]
  1553 
  1554 hide_const (open) Pos Neg sub dup
  1555 
  1556 
  1557 subsection {* Legacy theorems *}
  1558 
  1559 lemmas inj_int = inj_of_nat [where 'a=int]
  1560 lemmas zadd_int = of_nat_add [where 'a=int, symmetric]
  1561 lemmas int_mult = of_nat_mult [where 'a=int]
  1562 lemmas zmult_int = of_nat_mult [where 'a=int, symmetric]
  1563 lemmas int_eq_0_conv = of_nat_eq_0_iff [where 'a=int and m="n"] for n
  1564 lemmas zless_int = of_nat_less_iff [where 'a=int]
  1565 lemmas int_less_0_conv = of_nat_less_0_iff [where 'a=int and m="k"] for k
  1566 lemmas zero_less_int_conv = of_nat_0_less_iff [where 'a=int]
  1567 lemmas zero_zle_int = of_nat_0_le_iff [where 'a=int]
  1568 lemmas int_le_0_conv = of_nat_le_0_iff [where 'a=int and m="n"] for n
  1569 lemmas int_0 = of_nat_0 [where 'a=int]
  1570 lemmas int_1 = of_nat_1 [where 'a=int]
  1571 lemmas int_Suc = of_nat_Suc [where 'a=int]
  1572 lemmas int_numeral = of_nat_numeral [where 'a=int]
  1573 lemmas abs_int_eq = abs_of_nat [where 'a=int and n="m"] for m
  1574 lemmas of_int_int_eq = of_int_of_nat_eq [where 'a=int]
  1575 lemmas zdiff_int = of_nat_diff [where 'a=int, symmetric]
  1576 lemmas zpower_numeral_even = power_numeral_even [where 'a=int]
  1577 lemmas zpower_numeral_odd = power_numeral_odd [where 'a=int]
  1578 
  1579 lemma zpower_zpower:
  1580   "(x ^ y) ^ z = (x ^ (y * z)::int)"
  1581   by (rule power_mult [symmetric])
  1582 
  1583 lemma int_power:
  1584   "int (m ^ n) = int m ^ n"
  1585   by (fact of_nat_power)
  1586 
  1587 lemmas zpower_int = int_power [symmetric]
  1588 
  1589 text {* De-register @{text "int"} as a quotient type: *}
  1590 
  1591 lifting_update int.lifting
  1592 lifting_forget int.lifting
  1593 
  1594 end