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