src/HOL/Arith_Tools.thy
author wenzelm
Wed Sep 17 21:27:14 2008 +0200 (2008-09-17)
changeset 28263 69eaa97e7e96
parent 26462 dac4e2bce00d
child 28402 09e4aa3ddc25
permissions -rw-r--r--
moved global ML bindings to global place;
wenzelm@23462
     1
(*  Title:      HOL/Arith_Tools.thy
wenzelm@23462
     2
    ID:         $Id$
wenzelm@23462
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
wenzelm@23462
     4
    Author:     Amine Chaieb, TU Muenchen
wenzelm@23462
     5
*)
wenzelm@23462
     6
wenzelm@23462
     7
header {* Setup of arithmetic tools *}
wenzelm@23462
     8
wenzelm@23462
     9
theory Arith_Tools
chaieb@26154
    10
imports Groebner_Basis
wenzelm@23462
    11
uses
wenzelm@23462
    12
  "~~/src/Provers/Arith/cancel_numeral_factor.ML"
wenzelm@23462
    13
  "~~/src/Provers/Arith/extract_common_term.ML"
wenzelm@23462
    14
  "int_factor_simprocs.ML"
wenzelm@23462
    15
  "nat_simprocs.ML"
wenzelm@23462
    16
begin
wenzelm@23462
    17
wenzelm@23462
    18
subsection {* Simprocs for the Naturals *}
wenzelm@23462
    19
wenzelm@24075
    20
declaration {* K nat_simprocs_setup *}
wenzelm@23462
    21
wenzelm@23462
    22
subsubsection{*For simplifying @{term "Suc m - K"} and  @{term "K - Suc m"}*}
wenzelm@23462
    23
wenzelm@23462
    24
text{*Where K above is a literal*}
wenzelm@23462
    25
wenzelm@23462
    26
lemma Suc_diff_eq_diff_pred: "Numeral0 < n ==> Suc m - n = m - (n - Numeral1)"
wenzelm@23462
    27
by (simp add: numeral_0_eq_0 numeral_1_eq_1 split add: nat_diff_split)
wenzelm@23462
    28
wenzelm@23462
    29
text {*Now just instantiating @{text n} to @{text "number_of v"} does
wenzelm@23462
    30
  the right simplification, but with some redundant inequality
wenzelm@23462
    31
  tests.*}
wenzelm@23462
    32
lemma neg_number_of_pred_iff_0:
haftmann@25919
    33
  "neg (number_of (Int.pred v)::int) = (number_of v = (0::nat))"
haftmann@25919
    34
apply (subgoal_tac "neg (number_of (Int.pred v)) = (number_of v < Suc 0) ")
wenzelm@23462
    35
apply (simp only: less_Suc_eq_le le_0_eq)
wenzelm@23462
    36
apply (subst less_number_of_Suc, simp)
wenzelm@23462
    37
done
wenzelm@23462
    38
wenzelm@23462
    39
text{*No longer required as a simprule because of the @{text inverse_fold}
wenzelm@23462
    40
   simproc*}
wenzelm@23462
    41
lemma Suc_diff_number_of:
wenzelm@23462
    42
     "neg (number_of (uminus v)::int) ==>
haftmann@25919
    43
      Suc m - (number_of v) = m - (number_of (Int.pred v))"
wenzelm@23462
    44
apply (subst Suc_diff_eq_diff_pred)
wenzelm@23462
    45
apply simp
wenzelm@23462
    46
apply (simp del: nat_numeral_1_eq_1)
wenzelm@23462
    47
apply (auto simp only: diff_nat_number_of less_0_number_of [symmetric]
wenzelm@23462
    48
                        neg_number_of_pred_iff_0)
wenzelm@23462
    49
done
wenzelm@23462
    50
wenzelm@23462
    51
lemma diff_Suc_eq_diff_pred: "m - Suc n = (m - 1) - n"
wenzelm@23462
    52
by (simp add: numerals split add: nat_diff_split)
wenzelm@23462
    53
wenzelm@23462
    54
wenzelm@23462
    55
subsubsection{*For @{term nat_case} and @{term nat_rec}*}
wenzelm@23462
    56
wenzelm@23462
    57
lemma nat_case_number_of [simp]:
wenzelm@23462
    58
     "nat_case a f (number_of v) =
haftmann@25919
    59
        (let pv = number_of (Int.pred v) in
wenzelm@23462
    60
         if neg pv then a else f (nat pv))"
wenzelm@23462
    61
by (simp split add: nat.split add: Let_def neg_number_of_pred_iff_0)
wenzelm@23462
    62
wenzelm@23462
    63
lemma nat_case_add_eq_if [simp]:
wenzelm@23462
    64
     "nat_case a f ((number_of v) + n) =
haftmann@25919
    65
       (let pv = number_of (Int.pred v) in
wenzelm@23462
    66
         if neg pv then nat_case a f n else f (nat pv + n))"
wenzelm@23462
    67
apply (subst add_eq_if)
wenzelm@23462
    68
apply (simp split add: nat.split
wenzelm@23462
    69
            del: nat_numeral_1_eq_1
wenzelm@23462
    70
            add: numeral_1_eq_Suc_0 [symmetric] Let_def
wenzelm@23462
    71
                 neg_imp_number_of_eq_0 neg_number_of_pred_iff_0)
wenzelm@23462
    72
done
wenzelm@23462
    73
wenzelm@23462
    74
lemma nat_rec_number_of [simp]:
wenzelm@23462
    75
     "nat_rec a f (number_of v) =
haftmann@25919
    76
        (let pv = number_of (Int.pred v) in
wenzelm@23462
    77
         if neg pv then a else f (nat pv) (nat_rec a f (nat pv)))"
wenzelm@23462
    78
apply (case_tac " (number_of v) ::nat")
wenzelm@23462
    79
apply (simp_all (no_asm_simp) add: Let_def neg_number_of_pred_iff_0)
wenzelm@23462
    80
apply (simp split add: split_if_asm)
wenzelm@23462
    81
done
wenzelm@23462
    82
wenzelm@23462
    83
lemma nat_rec_add_eq_if [simp]:
wenzelm@23462
    84
     "nat_rec a f (number_of v + n) =
haftmann@25919
    85
        (let pv = number_of (Int.pred v) in
wenzelm@23462
    86
         if neg pv then nat_rec a f n
wenzelm@23462
    87
                   else f (nat pv + n) (nat_rec a f (nat pv + n)))"
wenzelm@23462
    88
apply (subst add_eq_if)
wenzelm@23462
    89
apply (simp split add: nat.split
wenzelm@23462
    90
            del: nat_numeral_1_eq_1
wenzelm@23462
    91
            add: numeral_1_eq_Suc_0 [symmetric] Let_def neg_imp_number_of_eq_0
wenzelm@23462
    92
                 neg_number_of_pred_iff_0)
wenzelm@23462
    93
done
wenzelm@23462
    94
wenzelm@23462
    95
wenzelm@23462
    96
subsubsection{*Various Other Lemmas*}
wenzelm@23462
    97
wenzelm@23462
    98
text {*Evens and Odds, for Mutilated Chess Board*}
wenzelm@23462
    99
wenzelm@23462
   100
text{*Lemmas for specialist use, NOT as default simprules*}
wenzelm@23462
   101
lemma nat_mult_2: "2 * z = (z+z::nat)"
wenzelm@23462
   102
proof -
wenzelm@23462
   103
  have "2*z = (1 + 1)*z" by simp
wenzelm@23462
   104
  also have "... = z+z" by (simp add: left_distrib)
wenzelm@23462
   105
  finally show ?thesis .
wenzelm@23462
   106
qed
wenzelm@23462
   107
wenzelm@23462
   108
lemma nat_mult_2_right: "z * 2 = (z+z::nat)"
wenzelm@23462
   109
by (subst mult_commute, rule nat_mult_2)
wenzelm@23462
   110
wenzelm@23462
   111
text{*Case analysis on @{term "n<2"}*}
wenzelm@23462
   112
lemma less_2_cases: "(n::nat) < 2 ==> n = 0 | n = Suc 0"
wenzelm@23462
   113
by arith
wenzelm@23462
   114
wenzelm@23462
   115
lemma div2_Suc_Suc [simp]: "Suc(Suc m) div 2 = Suc (m div 2)"
wenzelm@23462
   116
by arith
wenzelm@23462
   117
wenzelm@23462
   118
lemma add_self_div_2 [simp]: "(m + m) div 2 = (m::nat)"
wenzelm@23462
   119
by (simp add: nat_mult_2 [symmetric])
wenzelm@23462
   120
wenzelm@23462
   121
lemma mod2_Suc_Suc [simp]: "Suc(Suc(m)) mod 2 = m mod 2"
wenzelm@23462
   122
apply (subgoal_tac "m mod 2 < 2")
wenzelm@23462
   123
apply (erule less_2_cases [THEN disjE])
wenzelm@23462
   124
apply (simp_all (no_asm_simp) add: Let_def mod_Suc nat_1)
wenzelm@23462
   125
done
wenzelm@23462
   126
wenzelm@23462
   127
lemma mod2_gr_0 [simp]: "!!m::nat. (0 < m mod 2) = (m mod 2 = 1)"
wenzelm@23462
   128
apply (subgoal_tac "m mod 2 < 2")
wenzelm@23462
   129
apply (force simp del: mod_less_divisor, simp)
wenzelm@23462
   130
done
wenzelm@23462
   131
wenzelm@23462
   132
text{*Removal of Small Numerals: 0, 1 and (in additive positions) 2*}
wenzelm@23462
   133
wenzelm@23462
   134
lemma add_2_eq_Suc [simp]: "2 + n = Suc (Suc n)"
wenzelm@23462
   135
by simp
wenzelm@23462
   136
wenzelm@23462
   137
lemma add_2_eq_Suc' [simp]: "n + 2 = Suc (Suc n)"
wenzelm@23462
   138
by simp
wenzelm@23462
   139
wenzelm@23462
   140
text{*Can be used to eliminate long strings of Sucs, but not by default*}
wenzelm@23462
   141
lemma Suc3_eq_add_3: "Suc (Suc (Suc n)) = 3 + n"
wenzelm@23462
   142
by simp
wenzelm@23462
   143
wenzelm@23462
   144
wenzelm@23462
   145
text{*These lemmas collapse some needless occurrences of Suc:
wenzelm@23462
   146
    at least three Sucs, since two and fewer are rewritten back to Suc again!
wenzelm@23462
   147
    We already have some rules to simplify operands smaller than 3.*}
wenzelm@23462
   148
wenzelm@23462
   149
lemma div_Suc_eq_div_add3 [simp]: "m div (Suc (Suc (Suc n))) = m div (3+n)"
wenzelm@23462
   150
by (simp add: Suc3_eq_add_3)
wenzelm@23462
   151
wenzelm@23462
   152
lemma mod_Suc_eq_mod_add3 [simp]: "m mod (Suc (Suc (Suc n))) = m mod (3+n)"
wenzelm@23462
   153
by (simp add: Suc3_eq_add_3)
wenzelm@23462
   154
wenzelm@23462
   155
lemma Suc_div_eq_add3_div: "(Suc (Suc (Suc m))) div n = (3+m) div n"
wenzelm@23462
   156
by (simp add: Suc3_eq_add_3)
wenzelm@23462
   157
wenzelm@23462
   158
lemma Suc_mod_eq_add3_mod: "(Suc (Suc (Suc m))) mod n = (3+m) mod n"
wenzelm@23462
   159
by (simp add: Suc3_eq_add_3)
wenzelm@23462
   160
wenzelm@23462
   161
lemmas Suc_div_eq_add3_div_number_of =
wenzelm@23462
   162
    Suc_div_eq_add3_div [of _ "number_of v", standard]
wenzelm@23462
   163
declare Suc_div_eq_add3_div_number_of [simp]
wenzelm@23462
   164
wenzelm@23462
   165
lemmas Suc_mod_eq_add3_mod_number_of =
wenzelm@23462
   166
    Suc_mod_eq_add3_mod [of _ "number_of v", standard]
wenzelm@23462
   167
declare Suc_mod_eq_add3_mod_number_of [simp]
wenzelm@23462
   168
wenzelm@23462
   169
wenzelm@23462
   170
subsubsection{*Special Simplification for Constants*}
wenzelm@23462
   171
wenzelm@23462
   172
text{*These belong here, late in the development of HOL, to prevent their
wenzelm@23462
   173
interfering with proofs of abstract properties of instances of the function
wenzelm@23462
   174
@{term number_of}*}
wenzelm@23462
   175
wenzelm@23462
   176
text{*These distributive laws move literals inside sums and differences.*}
wenzelm@23462
   177
lemmas left_distrib_number_of = left_distrib [of _ _ "number_of v", standard]
wenzelm@23462
   178
declare left_distrib_number_of [simp]
wenzelm@23462
   179
wenzelm@23462
   180
lemmas right_distrib_number_of = right_distrib [of "number_of v", standard]
wenzelm@23462
   181
declare right_distrib_number_of [simp]
wenzelm@23462
   182
wenzelm@23462
   183
wenzelm@23462
   184
lemmas left_diff_distrib_number_of =
wenzelm@23462
   185
    left_diff_distrib [of _ _ "number_of v", standard]
wenzelm@23462
   186
declare left_diff_distrib_number_of [simp]
wenzelm@23462
   187
wenzelm@23462
   188
lemmas right_diff_distrib_number_of =
wenzelm@23462
   189
    right_diff_distrib [of "number_of v", standard]
wenzelm@23462
   190
declare right_diff_distrib_number_of [simp]
wenzelm@23462
   191
wenzelm@23462
   192
wenzelm@23462
   193
text{*These are actually for fields, like real: but where else to put them?*}
wenzelm@23462
   194
lemmas zero_less_divide_iff_number_of =
wenzelm@23462
   195
    zero_less_divide_iff [of "number_of w", standard]
paulson@24286
   196
declare zero_less_divide_iff_number_of [simp,noatp]
wenzelm@23462
   197
wenzelm@23462
   198
lemmas divide_less_0_iff_number_of =
wenzelm@23462
   199
    divide_less_0_iff [of "number_of w", standard]
paulson@24286
   200
declare divide_less_0_iff_number_of [simp,noatp]
wenzelm@23462
   201
wenzelm@23462
   202
lemmas zero_le_divide_iff_number_of =
wenzelm@23462
   203
    zero_le_divide_iff [of "number_of w", standard]
paulson@24286
   204
declare zero_le_divide_iff_number_of [simp,noatp]
wenzelm@23462
   205
wenzelm@23462
   206
lemmas divide_le_0_iff_number_of =
wenzelm@23462
   207
    divide_le_0_iff [of "number_of w", standard]
paulson@24286
   208
declare divide_le_0_iff_number_of [simp,noatp]
wenzelm@23462
   209
wenzelm@23462
   210
wenzelm@23462
   211
(****
wenzelm@23462
   212
IF times_divide_eq_right and times_divide_eq_left are removed as simprules,
wenzelm@23462
   213
then these special-case declarations may be useful.
wenzelm@23462
   214
wenzelm@23462
   215
text{*These simprules move numerals into numerators and denominators.*}
wenzelm@23462
   216
lemma times_recip_eq_right [simp]: "a * (1/c) = a / (c::'a::field)"
wenzelm@23462
   217
by (simp add: times_divide_eq)
wenzelm@23462
   218
wenzelm@23462
   219
lemma times_recip_eq_left [simp]: "(1/c) * a = a / (c::'a::field)"
wenzelm@23462
   220
by (simp add: times_divide_eq)
wenzelm@23462
   221
wenzelm@23462
   222
lemmas times_divide_eq_right_number_of =
wenzelm@23462
   223
    times_divide_eq_right [of "number_of w", standard]
wenzelm@23462
   224
declare times_divide_eq_right_number_of [simp]
wenzelm@23462
   225
wenzelm@23462
   226
lemmas times_divide_eq_right_number_of =
wenzelm@23462
   227
    times_divide_eq_right [of _ _ "number_of w", standard]
wenzelm@23462
   228
declare times_divide_eq_right_number_of [simp]
wenzelm@23462
   229
wenzelm@23462
   230
lemmas times_divide_eq_left_number_of =
wenzelm@23462
   231
    times_divide_eq_left [of _ "number_of w", standard]
wenzelm@23462
   232
declare times_divide_eq_left_number_of [simp]
wenzelm@23462
   233
wenzelm@23462
   234
lemmas times_divide_eq_left_number_of =
wenzelm@23462
   235
    times_divide_eq_left [of _ _ "number_of w", standard]
wenzelm@23462
   236
declare times_divide_eq_left_number_of [simp]
wenzelm@23462
   237
wenzelm@23462
   238
****)
wenzelm@23462
   239
wenzelm@23462
   240
text {*Replaces @{text "inverse #nn"} by @{text "1/#nn"}.  It looks
wenzelm@23462
   241
  strange, but then other simprocs simplify the quotient.*}
wenzelm@23462
   242
wenzelm@23462
   243
lemmas inverse_eq_divide_number_of =
wenzelm@23462
   244
    inverse_eq_divide [of "number_of w", standard]
wenzelm@23462
   245
declare inverse_eq_divide_number_of [simp]
wenzelm@23462
   246
wenzelm@23462
   247
wenzelm@23462
   248
text {*These laws simplify inequalities, moving unary minus from a term
wenzelm@23462
   249
into the literal.*}
wenzelm@23462
   250
lemmas less_minus_iff_number_of =
wenzelm@23462
   251
    less_minus_iff [of "number_of v", standard]
paulson@24286
   252
declare less_minus_iff_number_of [simp,noatp]
wenzelm@23462
   253
wenzelm@23462
   254
lemmas le_minus_iff_number_of =
wenzelm@23462
   255
    le_minus_iff [of "number_of v", standard]
paulson@24286
   256
declare le_minus_iff_number_of [simp,noatp]
wenzelm@23462
   257
wenzelm@23462
   258
lemmas equation_minus_iff_number_of =
wenzelm@23462
   259
    equation_minus_iff [of "number_of v", standard]
paulson@24286
   260
declare equation_minus_iff_number_of [simp,noatp]
wenzelm@23462
   261
wenzelm@23462
   262
wenzelm@23462
   263
lemmas minus_less_iff_number_of =
wenzelm@23462
   264
    minus_less_iff [of _ "number_of v", standard]
paulson@24286
   265
declare minus_less_iff_number_of [simp,noatp]
wenzelm@23462
   266
wenzelm@23462
   267
lemmas minus_le_iff_number_of =
wenzelm@23462
   268
    minus_le_iff [of _ "number_of v", standard]
paulson@24286
   269
declare minus_le_iff_number_of [simp,noatp]
wenzelm@23462
   270
wenzelm@23462
   271
lemmas minus_equation_iff_number_of =
wenzelm@23462
   272
    minus_equation_iff [of _ "number_of v", standard]
paulson@24286
   273
declare minus_equation_iff_number_of [simp,noatp]
wenzelm@23462
   274
wenzelm@23462
   275
wenzelm@23462
   276
text{*To Simplify Inequalities Where One Side is the Constant 1*}
wenzelm@23462
   277
paulson@24286
   278
lemma less_minus_iff_1 [simp,noatp]:
wenzelm@23462
   279
  fixes b::"'b::{ordered_idom,number_ring}"
wenzelm@23462
   280
  shows "(1 < - b) = (b < -1)"
wenzelm@23462
   281
by auto
wenzelm@23462
   282
paulson@24286
   283
lemma le_minus_iff_1 [simp,noatp]:
wenzelm@23462
   284
  fixes b::"'b::{ordered_idom,number_ring}"
wenzelm@23462
   285
  shows "(1 \<le> - b) = (b \<le> -1)"
wenzelm@23462
   286
by auto
wenzelm@23462
   287
paulson@24286
   288
lemma equation_minus_iff_1 [simp,noatp]:
wenzelm@23462
   289
  fixes b::"'b::number_ring"
wenzelm@23462
   290
  shows "(1 = - b) = (b = -1)"
wenzelm@23462
   291
by (subst equation_minus_iff, auto)
wenzelm@23462
   292
paulson@24286
   293
lemma minus_less_iff_1 [simp,noatp]:
wenzelm@23462
   294
  fixes a::"'b::{ordered_idom,number_ring}"
wenzelm@23462
   295
  shows "(- a < 1) = (-1 < a)"
wenzelm@23462
   296
by auto
wenzelm@23462
   297
paulson@24286
   298
lemma minus_le_iff_1 [simp,noatp]:
wenzelm@23462
   299
  fixes a::"'b::{ordered_idom,number_ring}"
wenzelm@23462
   300
  shows "(- a \<le> 1) = (-1 \<le> a)"
wenzelm@23462
   301
by auto
wenzelm@23462
   302
paulson@24286
   303
lemma minus_equation_iff_1 [simp,noatp]:
wenzelm@23462
   304
  fixes a::"'b::number_ring"
wenzelm@23462
   305
  shows "(- a = 1) = (a = -1)"
wenzelm@23462
   306
by (subst minus_equation_iff, auto)
wenzelm@23462
   307
wenzelm@23462
   308
wenzelm@23462
   309
text {*Cancellation of constant factors in comparisons (@{text "<"} and @{text "\<le>"}) *}
wenzelm@23462
   310
wenzelm@23462
   311
lemmas mult_less_cancel_left_number_of =
wenzelm@23462
   312
    mult_less_cancel_left [of "number_of v", standard]
paulson@24286
   313
declare mult_less_cancel_left_number_of [simp,noatp]
wenzelm@23462
   314
wenzelm@23462
   315
lemmas mult_less_cancel_right_number_of =
wenzelm@23462
   316
    mult_less_cancel_right [of _ "number_of v", standard]
paulson@24286
   317
declare mult_less_cancel_right_number_of [simp,noatp]
wenzelm@23462
   318
wenzelm@23462
   319
lemmas mult_le_cancel_left_number_of =
wenzelm@23462
   320
    mult_le_cancel_left [of "number_of v", standard]
paulson@24286
   321
declare mult_le_cancel_left_number_of [simp,noatp]
wenzelm@23462
   322
wenzelm@23462
   323
lemmas mult_le_cancel_right_number_of =
wenzelm@23462
   324
    mult_le_cancel_right [of _ "number_of v", standard]
paulson@24286
   325
declare mult_le_cancel_right_number_of [simp,noatp]
wenzelm@23462
   326
wenzelm@23462
   327
wenzelm@23462
   328
text {*Multiplying out constant divisors in comparisons (@{text "<"}, @{text "\<le>"} and @{text "="}) *}
wenzelm@23462
   329
wenzelm@26314
   330
lemmas le_divide_eq_number_of1 [simp] = le_divide_eq [of _ _ "number_of w", standard]
wenzelm@26314
   331
lemmas divide_le_eq_number_of1 [simp] = divide_le_eq [of _ "number_of w", standard]
wenzelm@26314
   332
lemmas less_divide_eq_number_of1 [simp] = less_divide_eq [of _ _ "number_of w", standard]
wenzelm@26314
   333
lemmas divide_less_eq_number_of1 [simp] = divide_less_eq [of _ "number_of w", standard]
wenzelm@26314
   334
lemmas eq_divide_eq_number_of1 [simp] = eq_divide_eq [of _ _ "number_of w", standard]
wenzelm@26314
   335
lemmas divide_eq_eq_number_of1 [simp] = divide_eq_eq [of _ "number_of w", standard]
wenzelm@23462
   336
wenzelm@23462
   337
wenzelm@23462
   338
subsubsection{*Optional Simplification Rules Involving Constants*}
wenzelm@23462
   339
wenzelm@23462
   340
text{*Simplify quotients that are compared with a literal constant.*}
wenzelm@23462
   341
wenzelm@23462
   342
lemmas le_divide_eq_number_of = le_divide_eq [of "number_of w", standard]
wenzelm@23462
   343
lemmas divide_le_eq_number_of = divide_le_eq [of _ _ "number_of w", standard]
wenzelm@23462
   344
lemmas less_divide_eq_number_of = less_divide_eq [of "number_of w", standard]
wenzelm@23462
   345
lemmas divide_less_eq_number_of = divide_less_eq [of _ _ "number_of w", standard]
wenzelm@23462
   346
lemmas eq_divide_eq_number_of = eq_divide_eq [of "number_of w", standard]
wenzelm@23462
   347
lemmas divide_eq_eq_number_of = divide_eq_eq [of _ _ "number_of w", standard]
wenzelm@23462
   348
wenzelm@23462
   349
wenzelm@23462
   350
text{*Not good as automatic simprules because they cause case splits.*}
wenzelm@23462
   351
lemmas divide_const_simps =
wenzelm@23462
   352
  le_divide_eq_number_of divide_le_eq_number_of less_divide_eq_number_of
wenzelm@23462
   353
  divide_less_eq_number_of eq_divide_eq_number_of divide_eq_eq_number_of
wenzelm@23462
   354
  le_divide_eq_1 divide_le_eq_1 less_divide_eq_1 divide_less_eq_1
wenzelm@23462
   355
wenzelm@23462
   356
text{*Division By @{text "-1"}*}
wenzelm@23462
   357
wenzelm@23462
   358
lemma divide_minus1 [simp]:
wenzelm@23462
   359
     "x/-1 = -(x::'a::{field,division_by_zero,number_ring})"
wenzelm@23462
   360
by simp
wenzelm@23462
   361
wenzelm@23462
   362
lemma minus1_divide [simp]:
wenzelm@23462
   363
     "-1 / (x::'a::{field,division_by_zero,number_ring}) = - (1/x)"
wenzelm@23462
   364
by (simp add: divide_inverse inverse_minus_eq)
wenzelm@23462
   365
wenzelm@23462
   366
lemma half_gt_zero_iff:
wenzelm@23462
   367
     "(0 < r/2) = (0 < (r::'a::{ordered_field,division_by_zero,number_ring}))"
wenzelm@23462
   368
by auto
wenzelm@23462
   369
wenzelm@23462
   370
lemmas half_gt_zero = half_gt_zero_iff [THEN iffD2, standard]
wenzelm@23462
   371
declare half_gt_zero [simp]
wenzelm@23462
   372
wenzelm@23462
   373
(* The following lemma should appear in Divides.thy, but there the proof
wenzelm@23462
   374
   doesn't work. *)
wenzelm@23462
   375
wenzelm@23462
   376
lemma nat_dvd_not_less:
wenzelm@23462
   377
  "[| 0 < m; m < n |] ==> \<not> n dvd (m::nat)"
wenzelm@23462
   378
  by (unfold dvd_def) auto
wenzelm@23462
   379
wenzelm@23462
   380
ML {*
wenzelm@23462
   381
val divide_minus1 = @{thm divide_minus1};
wenzelm@23462
   382
val minus1_divide = @{thm minus1_divide};
wenzelm@23462
   383
*}
wenzelm@23462
   384
wenzelm@23462
   385
wenzelm@23462
   386
subsection{* Groebner Bases for fields *}
wenzelm@23462
   387
wenzelm@23462
   388
interpretation class_fieldgb:
wenzelm@23462
   389
  fieldgb["op +" "op *" "op ^" "0::'a::{field,recpower,number_ring}" "1" "op -" "uminus" "op /" "inverse"] apply (unfold_locales) by (simp_all add: divide_inverse)
wenzelm@23462
   390
wenzelm@23462
   391
lemma divide_Numeral1: "(x::'a::{field,number_ring}) / Numeral1 = x" by simp
wenzelm@23462
   392
lemma divide_Numeral0: "(x::'a::{field,number_ring, division_by_zero}) / Numeral0 = 0"
wenzelm@23462
   393
  by simp
wenzelm@23462
   394
lemma mult_frac_frac: "((x::'a::{field,division_by_zero}) / y) * (z / w) = (x*z) / (y*w)"
wenzelm@23462
   395
  by simp
wenzelm@23462
   396
lemma mult_frac_num: "((x::'a::{field, division_by_zero}) / y) * z  = (x*z) / y"
wenzelm@23462
   397
  by simp
wenzelm@23462
   398
lemma mult_num_frac: "((x::'a::{field, division_by_zero}) / y) * z  = (x*z) / y"
wenzelm@23462
   399
  by simp
wenzelm@23462
   400
wenzelm@23462
   401
lemma Numeral1_eq1_nat: "(1::nat) = Numeral1" by simp
wenzelm@23462
   402
wenzelm@23462
   403
lemma add_frac_num: "y\<noteq> 0 \<Longrightarrow> (x::'a::{field, division_by_zero}) / y + z = (x + z*y) / y"
wenzelm@23462
   404
  by (simp add: add_divide_distrib)
wenzelm@23462
   405
lemma add_num_frac: "y\<noteq> 0 \<Longrightarrow> z + (x::'a::{field, division_by_zero}) / y = (x + z*y) / y"
wenzelm@23462
   406
  by (simp add: add_divide_distrib)
wenzelm@23462
   407
chaieb@25249
   408
chaieb@25249
   409
ML{* 
chaieb@25249
   410
local
wenzelm@23462
   411
 val zr = @{cpat "0"}
wenzelm@23462
   412
 val zT = ctyp_of_term zr
wenzelm@23462
   413
 val geq = @{cpat "op ="}
wenzelm@23462
   414
 val eqT = Thm.dest_ctyp (ctyp_of_term geq) |> hd
wenzelm@23462
   415
 val add_frac_eq = mk_meta_eq @{thm "add_frac_eq"}
wenzelm@23462
   416
 val add_frac_num = mk_meta_eq @{thm "add_frac_num"}
wenzelm@23462
   417
 val add_num_frac = mk_meta_eq @{thm "add_num_frac"}
wenzelm@23462
   418
chaieb@25249
   419
 fun prove_nz ss T t =
wenzelm@23462
   420
    let
wenzelm@23462
   421
      val z = instantiate_cterm ([(zT,T)],[]) zr
wenzelm@23462
   422
      val eq = instantiate_cterm ([(eqT,T)],[]) geq
wenzelm@23462
   423
      val th = Simplifier.rewrite (ss addsimps simp_thms)
wenzelm@23462
   424
           (Thm.capply @{cterm "Trueprop"} (Thm.capply @{cterm "Not"}
wenzelm@23462
   425
                  (Thm.capply (Thm.capply eq t) z)))
wenzelm@23462
   426
    in equal_elim (symmetric th) TrueI
wenzelm@23462
   427
    end
wenzelm@23462
   428
chaieb@25249
   429
 fun proc phi ss ct =
wenzelm@23462
   430
  let
wenzelm@23462
   431
    val ((x,y),(w,z)) =
wenzelm@23462
   432
         (Thm.dest_binop #> (fn (a,b) => (Thm.dest_binop a, Thm.dest_binop b))) ct
wenzelm@23462
   433
    val _ = map (HOLogic.dest_number o term_of) [x,y,z,w]
wenzelm@23462
   434
    val T = ctyp_of_term x
chaieb@25249
   435
    val [y_nz, z_nz] = map (prove_nz ss T) [y, z]
wenzelm@23462
   436
    val th = instantiate' [SOME T] (map SOME [y,z,x,w]) add_frac_eq
wenzelm@23462
   437
  in SOME (implies_elim (implies_elim th y_nz) z_nz)
wenzelm@23462
   438
  end
wenzelm@23462
   439
  handle CTERM _ => NONE | TERM _ => NONE | THM _ => NONE
wenzelm@23462
   440
chaieb@25249
   441
 fun proc2 phi ss ct =
wenzelm@23462
   442
  let
wenzelm@23462
   443
    val (l,r) = Thm.dest_binop ct
wenzelm@23462
   444
    val T = ctyp_of_term l
wenzelm@23462
   445
  in (case (term_of l, term_of r) of
wenzelm@23462
   446
      (Const(@{const_name "HOL.divide"},_)$_$_, _) =>
wenzelm@23462
   447
        let val (x,y) = Thm.dest_binop l val z = r
wenzelm@23462
   448
            val _ = map (HOLogic.dest_number o term_of) [x,y,z]
chaieb@25249
   449
            val ynz = prove_nz ss T y
wenzelm@23462
   450
        in SOME (implies_elim (instantiate' [SOME T] (map SOME [y,x,z]) add_frac_num) ynz)
wenzelm@23462
   451
        end
wenzelm@23462
   452
     | (_, Const (@{const_name "HOL.divide"},_)$_$_) =>
wenzelm@23462
   453
        let val (x,y) = Thm.dest_binop r val z = l
wenzelm@23462
   454
            val _ = map (HOLogic.dest_number o term_of) [x,y,z]
chaieb@25249
   455
            val ynz = prove_nz ss T y
wenzelm@23462
   456
        in SOME (implies_elim (instantiate' [SOME T] (map SOME [y,z,x]) add_num_frac) ynz)
wenzelm@23462
   457
        end
wenzelm@23462
   458
     | _ => NONE)
wenzelm@23462
   459
  end
wenzelm@23462
   460
  handle CTERM _ => NONE | TERM _ => NONE | THM _ => NONE
wenzelm@23462
   461
wenzelm@23462
   462
 fun is_number (Const(@{const_name "HOL.divide"},_)$a$b) = is_number a andalso is_number b
wenzelm@23462
   463
   | is_number t = can HOLogic.dest_number t
wenzelm@23462
   464
wenzelm@23462
   465
 val is_number = is_number o term_of
wenzelm@23462
   466
wenzelm@23462
   467
 fun proc3 phi ss ct =
wenzelm@23462
   468
  (case term_of ct of
haftmann@23881
   469
    Const(@{const_name HOL.less},_)$(Const(@{const_name "HOL.divide"},_)$_$_)$_ =>
wenzelm@23462
   470
      let
wenzelm@23462
   471
        val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
wenzelm@23462
   472
        val _ = map is_number [a,b,c]
wenzelm@23462
   473
        val T = ctyp_of_term c
wenzelm@23462
   474
        val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_less_eq"}
wenzelm@23462
   475
      in SOME (mk_meta_eq th) end
haftmann@23881
   476
  | Const(@{const_name HOL.less_eq},_)$(Const(@{const_name "HOL.divide"},_)$_$_)$_ =>
wenzelm@23462
   477
      let
wenzelm@23462
   478
        val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
wenzelm@23462
   479
        val _ = map is_number [a,b,c]
wenzelm@23462
   480
        val T = ctyp_of_term c
wenzelm@23462
   481
        val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_le_eq"}
wenzelm@23462
   482
      in SOME (mk_meta_eq th) end
wenzelm@23462
   483
  | Const("op =",_)$(Const(@{const_name "HOL.divide"},_)$_$_)$_ =>
wenzelm@23462
   484
      let
wenzelm@23462
   485
        val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
wenzelm@23462
   486
        val _ = map is_number [a,b,c]
wenzelm@23462
   487
        val T = ctyp_of_term c
wenzelm@23462
   488
        val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_eq_eq"}
wenzelm@23462
   489
      in SOME (mk_meta_eq th) end
haftmann@23881
   490
  | Const(@{const_name HOL.less},_)$_$(Const(@{const_name "HOL.divide"},_)$_$_) =>
wenzelm@23462
   491
    let
wenzelm@23462
   492
      val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
wenzelm@23462
   493
        val _ = map is_number [a,b,c]
wenzelm@23462
   494
        val T = ctyp_of_term c
wenzelm@23462
   495
        val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "less_divide_eq"}
wenzelm@23462
   496
      in SOME (mk_meta_eq th) end
haftmann@23881
   497
  | Const(@{const_name HOL.less_eq},_)$_$(Const(@{const_name "HOL.divide"},_)$_$_) =>
wenzelm@23462
   498
    let
wenzelm@23462
   499
      val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
wenzelm@23462
   500
        val _ = map is_number [a,b,c]
wenzelm@23462
   501
        val T = ctyp_of_term c
wenzelm@23462
   502
        val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "le_divide_eq"}
wenzelm@23462
   503
      in SOME (mk_meta_eq th) end
wenzelm@23462
   504
  | Const("op =",_)$_$(Const(@{const_name "HOL.divide"},_)$_$_) =>
wenzelm@23462
   505
    let
wenzelm@23462
   506
      val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
wenzelm@23462
   507
        val _ = map is_number [a,b,c]
wenzelm@23462
   508
        val T = ctyp_of_term c
wenzelm@23462
   509
        val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "eq_divide_eq"}
wenzelm@23462
   510
      in SOME (mk_meta_eq th) end
wenzelm@23462
   511
  | _ => NONE)
wenzelm@23462
   512
  handle TERM _ => NONE | CTERM _ => NONE | THM _ => NONE
wenzelm@23462
   513
chaieb@25249
   514
val add_frac_frac_simproc =
wenzelm@23462
   515
       make_simproc {lhss = [@{cpat "(?x::?'a::field)/?y + (?w::?'a::field)/?z"}],
wenzelm@23462
   516
                     name = "add_frac_frac_simproc",
chaieb@25249
   517
                     proc = proc, identifier = []}
wenzelm@23462
   518
chaieb@25249
   519
val add_frac_num_simproc =
wenzelm@23462
   520
       make_simproc {lhss = [@{cpat "(?x::?'a::field)/?y + ?z"}, @{cpat "?z + (?x::?'a::field)/?y"}],
wenzelm@23462
   521
                     name = "add_frac_num_simproc",
chaieb@25249
   522
                     proc = proc2, identifier = []}
wenzelm@23462
   523
wenzelm@23462
   524
val ord_frac_simproc =
wenzelm@23462
   525
  make_simproc
wenzelm@23462
   526
    {lhss = [@{cpat "(?a::(?'a::{field, ord}))/?b < ?c"},
wenzelm@23462
   527
             @{cpat "(?a::(?'a::{field, ord}))/?b \<le> ?c"},
wenzelm@23462
   528
             @{cpat "?c < (?a::(?'a::{field, ord}))/?b"},
wenzelm@23462
   529
             @{cpat "?c \<le> (?a::(?'a::{field, ord}))/?b"},
wenzelm@23462
   530
             @{cpat "?c = ((?a::(?'a::{field, ord}))/?b)"},
wenzelm@23462
   531
             @{cpat "((?a::(?'a::{field, ord}))/ ?b) = ?c"}],
wenzelm@23462
   532
             name = "ord_frac_simproc", proc = proc3, identifier = []}
wenzelm@23462
   533
wenzelm@23462
   534
val nat_arith = map thm ["add_nat_number_of", "diff_nat_number_of",
wenzelm@23462
   535
               "mult_nat_number_of", "eq_nat_number_of", "less_nat_number_of"]
wenzelm@23462
   536
wenzelm@23462
   537
val comp_arith = (map thm ["Let_def", "if_False", "if_True", "add_0",
wenzelm@23462
   538
                 "add_Suc", "add_number_of_left", "mult_number_of_left",
wenzelm@23462
   539
                 "Suc_eq_add_numeral_1"])@
wenzelm@23462
   540
                 (map (fn s => thm s RS sym) ["numeral_1_eq_1", "numeral_0_eq_0"])
haftmann@25481
   541
                 @ @{thms arith_simps} @ nat_arith @ @{thms rel_simps}
wenzelm@23462
   542
val ths = [@{thm "mult_numeral_1"}, @{thm "mult_numeral_1_right"},
wenzelm@23462
   543
           @{thm "divide_Numeral1"},
wenzelm@23462
   544
           @{thm "Ring_and_Field.divide_zero"}, @{thm "divide_Numeral0"},
wenzelm@23462
   545
           @{thm "divide_divide_eq_left"}, @{thm "mult_frac_frac"},
wenzelm@23462
   546
           @{thm "mult_num_frac"}, @{thm "mult_frac_num"},
wenzelm@23462
   547
           @{thm "mult_frac_frac"}, @{thm "times_divide_eq_right"},
wenzelm@23462
   548
           @{thm "times_divide_eq_left"}, @{thm "divide_divide_eq_right"},
wenzelm@23462
   549
           @{thm "diff_def"}, @{thm "minus_divide_left"},
wenzelm@23462
   550
           @{thm "Numeral1_eq1_nat"}, @{thm "add_divide_distrib"} RS sym]
wenzelm@23462
   551
wenzelm@23462
   552
local
wenzelm@23462
   553
open Conv
wenzelm@23462
   554
in
chaieb@25249
   555
val comp_conv = (Simplifier.rewrite
wenzelm@23462
   556
(HOL_basic_ss addsimps @{thms "Groebner_Basis.comp_arith"}
wenzelm@23462
   557
              addsimps ths addsimps comp_arith addsimps simp_thms
wenzelm@23462
   558
              addsimprocs field_cancel_numeral_factors
chaieb@25249
   559
               addsimprocs [add_frac_frac_simproc, add_frac_num_simproc,
wenzelm@23462
   560
                            ord_frac_simproc]
wenzelm@23462
   561
                addcongs [@{thm "if_weak_cong"}]))
wenzelm@23462
   562
then_conv (Simplifier.rewrite (HOL_basic_ss addsimps
wenzelm@23462
   563
  [@{thm numeral_1_eq_1},@{thm numeral_0_eq_0}] @ @{thms numerals(1-2)}))
wenzelm@23462
   564
end
wenzelm@23462
   565
wenzelm@23462
   566
fun numeral_is_const ct =
wenzelm@23462
   567
  case term_of ct of
wenzelm@23462
   568
   Const (@{const_name "HOL.divide"},_) $ a $ b =>
wenzelm@23462
   569
     numeral_is_const (Thm.dest_arg1 ct) andalso numeral_is_const (Thm.dest_arg ct)
wenzelm@23462
   570
 | Const (@{const_name "HOL.uminus"},_)$t => numeral_is_const (Thm.dest_arg ct)
wenzelm@23462
   571
 | t => can HOLogic.dest_number t
wenzelm@23462
   572
chaieb@25128
   573
fun dest_const ct = ((case term_of ct of
wenzelm@23462
   574
   Const (@{const_name "HOL.divide"},_) $ a $ b=>
wenzelm@23462
   575
    Rat.rat_of_quotient (snd (HOLogic.dest_number a), snd (HOLogic.dest_number b))
chaieb@25128
   576
 | t => Rat.rat_of_int (snd (HOLogic.dest_number t))) 
chaieb@25128
   577
   handle TERM _ => error "ring_dest_const")
wenzelm@23462
   578
wenzelm@23462
   579
fun mk_const phi cT x =
wenzelm@23462
   580
 let val (a, b) = Rat.quotient_of_rat x
wenzelm@23572
   581
 in if b = 1 then Numeral.mk_cnumber cT a
wenzelm@23462
   582
    else Thm.capply
wenzelm@23462
   583
         (Thm.capply (Drule.cterm_rule (instantiate' [SOME cT] []) @{cpat "op /"})
wenzelm@23572
   584
                     (Numeral.mk_cnumber cT a))
wenzelm@23572
   585
         (Numeral.mk_cnumber cT b)
wenzelm@23462
   586
  end
wenzelm@23462
   587
wenzelm@23462
   588
in
chaieb@25249
   589
 val field_comp_conv = comp_conv;
chaieb@25249
   590
 val fieldgb_declaration = 
wenzelm@26462
   591
  NormalizerData.funs @{thm class_fieldgb.fieldgb_axioms'}
wenzelm@23462
   592
   {is_const = K numeral_is_const,
wenzelm@23462
   593
    dest_const = K dest_const,
wenzelm@23462
   594
    mk_const = mk_const,
chaieb@25249
   595
    conv = K (K comp_conv)}
chaieb@25249
   596
end;
chaieb@25249
   597
*}
wenzelm@23462
   598
chaieb@25249
   599
declaration{* fieldgb_declaration *}
wenzelm@23462
   600
end