src/HOL/Import/HOL_Light/HOLLightInt.thy
 author huffman Sun Mar 25 20:15:39 2012 +0200 (2012-03-25) changeset 47108 2a1953f0d20d parent 46905 6b1c0a80a57a child 47159 978c00c20a59 permissions -rw-r--r--
merged fork with new numeral representation (see NEWS)
```     1 (*  Title:      HOL/Import/HOL_Light/HOLLightInt.thy
```
```     2     Author:     Cezary Kaliszyk
```
```     3 *)
```
```     4
```
```     5 header {* Compatibility theorems for HOL Light integers *}
```
```     6
```
```     7 theory HOLLightInt imports Main Real GCD begin
```
```     8
```
```     9 fun int_coprime where "int_coprime ((a :: int), (b :: int)) = coprime a b"
```
```    10
```
```    11 lemma DEF_int_coprime:
```
```    12   "int_coprime = (\<lambda>u. \<exists>x y. ((fst u) * x) + ((snd u) * y) = int 1)"
```
```    13   apply (auto simp add: fun_eq_iff)
```
```    14   apply (metis bezout_int mult_commute)
```
```    15   by (metis coprime_divisors_nat dvd_triv_left gcd_1_int gcd_add2_int)
```
```    16
```
```    17 lemma INT_FORALL_POS:
```
```    18   "(\<forall>n. P (int n)) = (\<forall>i\<ge>(int 0). P i)"
```
```    19   by (auto, drule_tac x="nat i" in spec) simp
```
```    20
```
```    21 lemma INT_LT_DISCRETE:
```
```    22   "(x < y) = (x + int 1 \<le> y)"
```
```    23   by auto
```
```    24
```
```    25 lemma INT_ABS_MUL_1:
```
```    26   "(abs (x * y) = int 1) = (abs x = int 1 \<and> abs y = int 1)"
```
```    27   by simp (metis dvd_mult_right zdvd1_eq abs_zmult_eq_1 abs_mult mult_1_right)
```
```    28
```
```    29 lemma dest_int_rep:
```
```    30   "\<exists>(n :: nat). real (i :: int) = real n \<or> real i = - real n"
```
```    31   by (metis (full_types) of_int_of_nat real_eq_of_int real_of_nat_def)
```
```    32
```
```    33 lemma DEF_int_add:
```
```    34   "op + = (\<lambda>u ua. floor (real u + real ua))"
```
```    35   by simp
```
```    36
```
```    37 lemma DEF_int_sub:
```
```    38   "op - = (\<lambda>u ua. floor (real u - real ua))"
```
```    39   by simp
```
```    40
```
```    41 lemma DEF_int_mul:
```
```    42   "op * = (\<lambda>u ua. floor (real u * real ua))"
```
```    43   by (metis floor_real_of_int real_of_int_mult)
```
```    44
```
```    45 lemma DEF_int_abs:
```
```    46   "abs = (\<lambda>u. floor (abs (real u)))"
```
```    47   by (metis floor_real_of_int real_of_int_abs)
```
```    48
```
```    49 lemma DEF_int_sgn:
```
```    50   "sgn = (\<lambda>u. floor (sgn (real u)))"
```
```    51   by (simp add: sgn_if fun_eq_iff)
```
```    52
```
```    53 lemma int_sgn_th:
```
```    54   "real (sgn (x :: int)) = sgn (real x)"
```
```    55   by (simp add: sgn_if)
```
```    56
```
```    57 lemma DEF_int_max:
```
```    58   "max = (\<lambda>u ua. floor (max (real u) (real ua)))"
```
```    59   by (metis floor_real_of_int real_of_int_le_iff sup_absorb1 sup_commute sup_max linorder_linear)
```
```    60
```
```    61 lemma int_max_th:
```
```    62   "real (max (x :: int) y) = max (real x) (real y)"
```
```    63   by (metis min_max.le_iff_sup min_max.sup_absorb1 real_of_int_le_iff linorder_linear)
```
```    64
```
```    65 lemma DEF_int_min:
```
```    66   "min = (\<lambda>u ua. floor (min (real u) (real ua)))"
```
```    67   by (metis floor_real_of_int inf_absorb1 inf_absorb2 inf_int_def inf_real_def real_of_int_le_iff linorder_linear)
```
```    68
```
```    69 lemma int_min_th:
```
```    70   "real (min (x :: int) y) = min (real x) (real y)"
```
```    71   by (metis inf_absorb1 inf_absorb2 inf_int_def inf_real_def real_of_int_le_iff linorder_linear)
```
```    72
```
```    73 lemma INT_IMAGE:
```
```    74   "(\<exists>n. x = int n) \<or> (\<exists>n. x = - int n)"
```
```    75   by (metis of_int_eq_id id_def of_int_of_nat)
```
```    76
```
```    77 lemma DEF_int_pow:
```
```    78   "op ^ = (\<lambda>u ua. floor (real u ^ ua))"
```
```    79   by (simp add: floor_power)
```
```    80
```
```    81 lemma DEF_int_divides:
```
```    82   "op dvd = (\<lambda>(u :: int) ua. \<exists>x. ua = u * x)"
```
```    83   by (metis dvdE dvdI)
```
```    84
```
```    85 lemma DEF_int_divides':
```
```    86   "(a :: int) dvd b = (\<exists>x. b = a * x)"
```
```    87   by (metis dvdE dvdI)
```
```    88
```
```    89 definition "int_mod (u :: int) ua ub = (u dvd (ua - ub))"
```
```    90
```
```    91 lemma int_mod_def':
```
```    92   "int_mod = (\<lambda>u ua ub. (u dvd (ua - ub)))"
```
```    93   by (simp add: int_mod_def [abs_def])
```
```    94
```
```    95 lemma int_congruent:
```
```    96   "\<forall>x xa xb. int_mod xb x xa = (\<exists>d. x - xa = xb * d)"
```
```    97   unfolding int_mod_def'
```
```    98   by (auto simp add: DEF_int_divides')
```
```    99
```
```   100 lemma int_congruent':
```
```   101   "\<forall>(x :: int) y n. (n dvd x - y) = (\<exists>d. x - y = n * d)"
```
```   102   using int_congruent[unfolded int_mod_def] .
```
```   103
```
```   104 fun int_gcd where
```
```   105   "int_gcd ((a :: int), (b :: int)) = gcd a b"
```
```   106
```
```   107 definition "hl_mod (k\<Colon>int) (l\<Colon>int) = (if 0 \<le> l then k mod l else k mod - l)"
```
```   108
```
```   109 lemma hl_mod_nonneg:
```
```   110   "b \<noteq> 0 \<Longrightarrow> hl_mod a b \<ge> 0"
```
```   111   by (simp add: hl_mod_def)
```
```   112
```
```   113 lemma hl_mod_lt_abs:
```
```   114   "b \<noteq> 0 \<Longrightarrow> hl_mod a b < abs b"
```
```   115   by (simp add: hl_mod_def)
```
```   116
```
```   117 definition "hl_div k l = (if 0 \<le> l then k div l else -(k div (-l)))"
```
```   118
```
```   119 lemma hl_mod_div:
```
```   120   "n \<noteq> (0\<Colon>int) \<Longrightarrow> m = hl_div m n * n + hl_mod m n"
```
```   121   unfolding hl_div_def hl_mod_def
```
```   122   by auto (metis zmod_zdiv_equality mult_commute mult_minus_left)
```
```   123
```
```   124 lemma sth:
```
```   125   "(\<forall>(x :: int) y z. x + (y + z) = x + y + z) \<and>
```
```   126    (\<forall>(x :: int) y. x + y = y + x) \<and>
```
```   127    (\<forall>(x :: int). int 0 + x = x) \<and>
```
```   128    (\<forall>(x :: int) y z. x * (y * z) = x * y * z) \<and>
```
```   129    (\<forall>(x :: int) y. x * y = y * x) \<and>
```
```   130    (\<forall>(x :: int). int 1 * x = x) \<and>
```
```   131    (\<forall>(x :: int). int 0 * x = int 0) \<and>
```
```   132    (\<forall>(x :: int) y z. x * (y + z) = x * y + x * z) \<and>
```
```   133    (\<forall>(x :: int). x ^ 0 = int 1) \<and> (\<forall>(x :: int) n. x ^ Suc n = x * x ^ n)"
```
```   134   by (simp_all add: right_distrib)
```
```   135
```
```   136 lemma INT_DIVISION:
```
```   137   "n ~= int 0 \<Longrightarrow> m = hl_div m n * n + hl_mod m n \<and> int 0 \<le> hl_mod m n \<and> hl_mod m n < abs n"
```
```   138   by (auto simp add: hl_mod_nonneg hl_mod_lt_abs hl_mod_div)
```
```   139
```
```   140 lemma INT_DIVMOD_EXIST_0:
```
```   141   "\<exists>q r. if n = int 0 then q = int 0 \<and> r = m
```
```   142          else int 0 \<le> r \<and> r < abs n \<and> m = q * n + r"
```
```   143   apply (rule_tac x="hl_div m n" in exI)
```
```   144   apply (rule_tac x="hl_mod m n" in exI)
```
```   145   apply (auto simp add: hl_mod_nonneg hl_mod_lt_abs hl_mod_div)
```
```   146   unfolding hl_div_def hl_mod_def
```
```   147   by auto
```
```   148
```
```   149 lemma DEF_div:
```
```   150   "hl_div = (SOME q. \<exists>r. \<forall>m n. if n = int 0 then q m n = int 0 \<and> r m n = m
```
```   151      else (int 0) \<le> (r m n) \<and> (r m n) < (abs n) \<and> m = ((q m n) * n) + (r m n))"
```
```   152   apply (rule some_equality[symmetric])
```
```   153   apply (rule_tac x="hl_mod" in exI)
```
```   154   apply (auto simp add: fun_eq_iff hl_mod_nonneg hl_mod_lt_abs hl_mod_div)
```
```   155   apply (simp add: hl_div_def)
```
```   156   apply (simp add: hl_mod_def)
```
```   157   apply (drule_tac x="x" in spec)
```
```   158   apply (drule_tac x="xa" in spec)
```
```   159   apply (case_tac "0 = xa")
```
```   160   apply (simp add: hl_mod_def hl_div_def)
```
```   161   apply (case_tac "xa > 0")
```
```   162   apply (simp add: hl_mod_def hl_div_def)
```
```   163   apply (metis comm_semiring_1_class.normalizing_semiring_rules(24) div_mult_self2 not_less_iff_gr_or_eq order_less_le add_0 zdiv_eq_0_iff mult_commute)
```
```   164   apply (simp add: hl_mod_def hl_div_def)
```
```   165   by (metis add.comm_neutral add_pos_nonneg div_mult_self1 less_minus_iff minus_add minus_add_cancel minus_minus mult_zero_right not_square_less_zero zdiv_eq_0_iff zdiv_zminus2)
```
```   166
```
```   167 lemma DEF_rem:
```
```   168   "hl_mod = (SOME r. \<forall>m n. if n = int 0 then
```
```   169      (if 0 \<le> n then m div n else - (m div - n)) = int 0 \<and> r m n = m
```
```   170      else int 0 \<le> r m n \<and> r m n < abs n \<and>
```
```   171             m = (if 0 \<le> n then m div n else - (m div - n)) * n + r m n)"
```
```   172   apply (rule some_equality[symmetric])
```
```   173   apply (fold hl_div_def)
```
```   174   apply (auto simp add: fun_eq_iff hl_mod_nonneg hl_mod_lt_abs hl_mod_div)
```
```   175   apply (simp add: hl_div_def)
```
```   176   apply (simp add: hl_mod_def)
```
```   177   apply (drule_tac x="x" in spec)
```
```   178   apply (drule_tac x="xa" in spec)
```
```   179   apply (case_tac "0 = xa")
```
```   180   apply (simp add: hl_mod_def hl_div_def)
```
```   181   apply (case_tac "xa > 0")
```
```   182   apply (simp add: hl_mod_def hl_div_def)
```
```   183   apply (metis add_left_cancel mod_div_equality)
```
```   184   apply (simp add: hl_mod_def hl_div_def)
```
```   185   by (metis minus_mult_right mod_mult_self2 mod_pos_pos_trivial add_commute zminus_zmod zmod_zminus2 mult_commute)
```
```   186
```
```   187 lemma DEF_int_gcd:
```
```   188   "int_gcd = (SOME d. \<forall>a b. (int 0) \<le> (d (a, b)) \<and> (d (a, b)) dvd a \<and>
```
```   189        (d (a, b)) dvd b \<and> (\<exists>x y. d (a, b) = (a * x) + (b * y)))"
```
```   190   apply (rule some_equality[symmetric])
```
```   191   apply auto
```
```   192   apply (metis bezout_int mult_commute)
```
```   193   apply (auto simp add: fun_eq_iff)
```
```   194   apply (drule_tac x="a" in spec)
```
```   195   apply (drule_tac x="b" in spec)
```
```   196   using gcd_greatest_int zdvd_antisym_nonneg
```
```   197   by auto
```
```   198
```
```   199 definition "eqeq x y (r :: 'a \<Rightarrow> 'b \<Rightarrow> bool) = r x y"
```
```   200
```
```   201 lemma INT_INTEGRAL:
```
```   202   "(\<forall>x. int 0 * x = int 0) \<and>
```
```   203    (\<forall>(x :: int) y z. (x + y = x + z) = (y = z)) \<and>
```
```   204    (\<forall>(w :: int) x y z. (w * y + x * z = w * z + x * y) = (w = x \<or> y = z))"
```
```   205   by (auto simp add: crossproduct_eq)
```
```   206
```
```   207 end
```
```   208
```