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