src/HOL/Tools/numeral_simprocs.ML
author wenzelm
Tue Sep 26 20:54:40 2017 +0200 (23 months ago)
changeset 66695 91500c024c7f
parent 64240 eabf80376aab
child 67560 0fa87bd86566
permissions -rw-r--r--
tuned;
     1 (* Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     2    Copyright   2000  University of Cambridge
     3 
     4 Simprocs for the (integer) numerals.
     5 *)
     6 
     7 (*To quote from Provers/Arith/cancel_numeral_factor.ML:
     8 
     9 Cancels common coefficients in balanced expressions:
    10 
    11      u*#m ~~ u'*#m'  ==  #n*u ~~ #n'*u'
    12 
    13 where ~~ is an appropriate balancing operation (e.g. =, <=, <, div, /)
    14 and d = gcd(m,m') and n=m/d and n'=m'/d.
    15 *)
    16 
    17 signature NUMERAL_SIMPROCS =
    18 sig
    19   val trans_tac: Proof.context -> thm option -> tactic
    20   val assoc_fold: Proof.context -> cterm -> thm option
    21   val combine_numerals: Proof.context -> cterm -> thm option
    22   val eq_cancel_numerals: Proof.context -> cterm -> thm option
    23   val less_cancel_numerals: Proof.context -> cterm -> thm option
    24   val le_cancel_numerals: Proof.context -> cterm -> thm option
    25   val eq_cancel_factor: Proof.context -> cterm -> thm option
    26   val le_cancel_factor: Proof.context -> cterm -> thm option
    27   val less_cancel_factor: Proof.context -> cterm -> thm option
    28   val div_cancel_factor: Proof.context -> cterm -> thm option
    29   val mod_cancel_factor: Proof.context -> cterm -> thm option
    30   val dvd_cancel_factor: Proof.context -> cterm -> thm option
    31   val divide_cancel_factor: Proof.context -> cterm -> thm option
    32   val eq_cancel_numeral_factor: Proof.context -> cterm -> thm option
    33   val less_cancel_numeral_factor: Proof.context -> cterm -> thm option
    34   val le_cancel_numeral_factor: Proof.context -> cterm -> thm option
    35   val div_cancel_numeral_factor: Proof.context -> cterm -> thm option
    36   val divide_cancel_numeral_factor: Proof.context -> cterm -> thm option
    37   val field_combine_numerals: Proof.context -> cterm -> thm option
    38   val field_divide_cancel_numeral_factor: simproc
    39   val num_ss: simpset
    40   val field_comp_conv: Proof.context -> conv
    41 end;
    42 
    43 structure Numeral_Simprocs : NUMERAL_SIMPROCS =
    44 struct
    45 
    46 fun trans_tac _ NONE  = all_tac
    47   | trans_tac ctxt (SOME th) = ALLGOALS (resolve_tac ctxt [th RS trans]);
    48 
    49 val mk_number = Arith_Data.mk_number;
    50 val mk_sum = Arith_Data.mk_sum;
    51 val long_mk_sum = Arith_Data.long_mk_sum;
    52 val dest_sum = Arith_Data.dest_sum;
    53 
    54 val mk_times = HOLogic.mk_binop @{const_name Groups.times};
    55 
    56 fun one_of T = Const(@{const_name Groups.one}, T);
    57 
    58 (* build product with trailing 1 rather than Numeral 1 in order to avoid the
    59    unnecessary restriction to type class number_ring
    60    which is not required for cancellation of common factors in divisions.
    61    UPDATE: this reasoning no longer applies (number_ring is gone)
    62 *)
    63 fun mk_prod T =
    64   let val one = one_of T
    65   fun mk [] = one
    66     | mk [t] = t
    67     | mk (t :: ts) = if t = one then mk ts else mk_times (t, mk ts)
    68   in mk end;
    69 
    70 (*This version ALWAYS includes a trailing one*)
    71 fun long_mk_prod T []        = one_of T
    72   | long_mk_prod T (t :: ts) = mk_times (t, mk_prod T ts);
    73 
    74 val dest_times = HOLogic.dest_bin @{const_name Groups.times} dummyT;
    75 
    76 fun dest_prod t =
    77       let val (t,u) = dest_times t
    78       in dest_prod t @ dest_prod u end
    79       handle TERM _ => [t];
    80 
    81 fun find_first_numeral past (t::terms) =
    82         ((snd (HOLogic.dest_number t), rev past @ terms)
    83          handle TERM _ => find_first_numeral (t::past) terms)
    84   | find_first_numeral past [] = raise TERM("find_first_numeral", []);
    85 
    86 (*DON'T do the obvious simplifications; that would create special cases*)
    87 fun mk_coeff (k, t) = mk_times (mk_number (Term.fastype_of t) k, t);
    88 
    89 (*Express t as a product of (possibly) a numeral with other sorted terms*)
    90 fun dest_coeff sign (Const (@{const_name Groups.uminus}, _) $ t) = dest_coeff (~sign) t
    91   | dest_coeff sign t =
    92     let val ts = sort Term_Ord.term_ord (dest_prod t)
    93         val (n, ts') = find_first_numeral [] ts
    94                           handle TERM _ => (1, ts)
    95     in (sign*n, mk_prod (Term.fastype_of t) ts') end;
    96 
    97 (*Find first coefficient-term THAT MATCHES u*)
    98 fun find_first_coeff past u [] = raise TERM("find_first_coeff", [])
    99   | find_first_coeff past u (t::terms) =
   100         let val (n,u') = dest_coeff 1 t
   101         in if u aconv u' then (n, rev past @ terms)
   102                          else find_first_coeff (t::past) u terms
   103         end
   104         handle TERM _ => find_first_coeff (t::past) u terms;
   105 
   106 (*Fractions as pairs of ints. Can't use Rat.rat because the representation
   107   needs to preserve negative values in the denominator.*)
   108 fun mk_frac (p, q) = if q = 0 then raise Div else (p, q);
   109 
   110 (*Don't reduce fractions; sums must be proved by rule add_frac_eq.
   111   Fractions are reduced later by the cancel_numeral_factor simproc.*)
   112 fun add_frac ((p1, q1), (p2, q2)) = (p1 * q2 + p2 * q1, q1 * q2);
   113 
   114 val mk_divide = HOLogic.mk_binop @{const_name Rings.divide};
   115 
   116 (*Build term (p / q) * t*)
   117 fun mk_fcoeff ((p, q), t) =
   118   let val T = Term.fastype_of t
   119   in mk_times (mk_divide (mk_number T p, mk_number T q), t) end;
   120 
   121 (*Express t as a product of a fraction with other sorted terms*)
   122 fun dest_fcoeff sign (Const (@{const_name Groups.uminus}, _) $ t) = dest_fcoeff (~sign) t
   123   | dest_fcoeff sign (Const (@{const_name Rings.divide}, _) $ t $ u) =
   124     let val (p, t') = dest_coeff sign t
   125         val (q, u') = dest_coeff 1 u
   126     in (mk_frac (p, q), mk_divide (t', u')) end
   127   | dest_fcoeff sign t =
   128     let val (p, t') = dest_coeff sign t
   129         val T = Term.fastype_of t
   130     in (mk_frac (p, 1), mk_divide (t', one_of T)) end;
   131 
   132 
   133 (** New term ordering so that AC-rewriting brings numerals to the front **)
   134 
   135 (*Order integers by absolute value and then by sign. The standard integer
   136   ordering is not well-founded.*)
   137 fun num_ord (i,j) =
   138   (case int_ord (abs i, abs j) of
   139     EQUAL => int_ord (Int.sign i, Int.sign j)
   140   | ord => ord);
   141 
   142 (*This resembles Term_Ord.term_ord, but it puts binary numerals before other
   143   non-atomic terms.*)
   144 local open Term
   145 in
   146 fun numterm_ord (t, u) =
   147     case (try HOLogic.dest_number t, try HOLogic.dest_number u) of
   148       (SOME (_, i), SOME (_, j)) => num_ord (i, j)
   149     | (SOME _, NONE) => LESS
   150     | (NONE, SOME _) => GREATER
   151     | _ => (
   152       case (t, u) of
   153         (Abs (_, T, t), Abs(_, U, u)) =>
   154         (prod_ord numterm_ord Term_Ord.typ_ord ((t, T), (u, U)))
   155       | _ => (
   156         case int_ord (size_of_term t, size_of_term u) of
   157           EQUAL =>
   158           let val (f, ts) = strip_comb t and (g, us) = strip_comb u in
   159             (prod_ord Term_Ord.hd_ord numterms_ord ((f, ts), (g, us)))
   160           end
   161         | ord => ord))
   162 and numterms_ord (ts, us) = list_ord numterm_ord (ts, us)
   163 end;
   164 
   165 fun numtermless tu = (numterm_ord tu = LESS);
   166 
   167 val num_ss =
   168   simpset_of (put_simpset HOL_basic_ss @{context}
   169     |> Simplifier.set_termless numtermless);
   170 
   171 (*Maps 1 to Numeral1 so that arithmetic isn't complicated by the abstract 1.*)
   172 val numeral_syms = [@{thm numeral_One} RS sym];
   173 
   174 (*Simplify 0+n, n+0, Numeral1*n, n*Numeral1, 1*x, x*1, x/1 *)
   175 val add_0s =  @{thms add_0_left add_0_right};
   176 val mult_1s = @{thms mult_1s divide_numeral_1 mult_1_left mult_1_right mult_minus1 mult_minus1_right div_by_1};
   177 
   178 (* For post-simplification of the rhs of simproc-generated rules *)
   179 val post_simps =
   180     [@{thm numeral_One},
   181      @{thm add_0_left}, @{thm add_0_right},
   182      @{thm mult_zero_left}, @{thm mult_zero_right},
   183      @{thm mult_1_left}, @{thm mult_1_right},
   184      @{thm mult_minus1}, @{thm mult_minus1_right}]
   185 
   186 val field_post_simps =
   187     post_simps @ [@{thm div_0}, @{thm div_by_1}]
   188 
   189 (*Simplify inverse Numeral1*)
   190 val inverse_1s = [@{thm inverse_numeral_1}];
   191 
   192 (*To perform binary arithmetic.  The "left" rewriting handles patterns
   193   created by the Numeral_Simprocs, such as 3 * (5 * x). *)
   194 val simps =
   195     [@{thm numeral_One} RS sym] @
   196     @{thms add_numeral_left} @
   197     @{thms add_neg_numeral_left} @
   198     @{thms mult_numeral_left} @
   199     @{thms arith_simps} @ @{thms rel_simps};
   200 
   201 (*Binary arithmetic BUT NOT ADDITION since it may collapse adjacent terms
   202   during re-arrangement*)
   203 val non_add_simps =
   204   subtract Thm.eq_thm
   205     (@{thms add_numeral_left} @
   206      @{thms add_neg_numeral_left} @
   207      @{thms numeral_plus_numeral} @
   208      @{thms add_neg_numeral_simps}) simps;
   209 
   210 (*To evaluate binary negations of coefficients*)
   211 val minus_simps = [@{thm minus_zero}, @{thm minus_minus}];
   212 
   213 (*To let us treat subtraction as addition*)
   214 val diff_simps = [@{thm diff_conv_add_uminus}, @{thm minus_add_distrib}, @{thm minus_minus}];
   215 
   216 (*To let us treat division as multiplication*)
   217 val divide_simps = [@{thm divide_inverse}, @{thm inverse_mult_distrib}, @{thm inverse_inverse_eq}];
   218 
   219 (*to extract again any uncancelled minuses*)
   220 val minus_from_mult_simps =
   221     [@{thm minus_minus}, @{thm mult_minus_left}, @{thm mult_minus_right}];
   222 
   223 (*combine unary minus with numeric literals, however nested within a product*)
   224 val mult_minus_simps =
   225     [@{thm mult.assoc}, @{thm minus_mult_right}, @{thm minus_mult_commute}, @{thm numeral_times_minus_swap}];
   226 
   227 val norm_ss1 =
   228   simpset_of (put_simpset num_ss @{context}
   229     addsimps numeral_syms @ add_0s @ mult_1s @
   230     diff_simps @ minus_simps @ @{thms ac_simps})
   231 
   232 val norm_ss2 =
   233   simpset_of (put_simpset num_ss @{context}
   234     addsimps non_add_simps @ mult_minus_simps)
   235 
   236 val norm_ss3 =
   237   simpset_of (put_simpset num_ss @{context}
   238     addsimps minus_from_mult_simps @ @{thms ac_simps} @ @{thms ac_simps minus_mult_commute})
   239 
   240 structure CancelNumeralsCommon =
   241 struct
   242   val mk_sum = mk_sum
   243   val dest_sum = dest_sum
   244   val mk_coeff = mk_coeff
   245   val dest_coeff = dest_coeff 1
   246   val find_first_coeff = find_first_coeff []
   247   val trans_tac = trans_tac
   248 
   249   fun norm_tac ctxt =
   250     ALLGOALS (simp_tac (put_simpset norm_ss1 ctxt))
   251     THEN ALLGOALS (simp_tac (put_simpset norm_ss2 ctxt))
   252     THEN ALLGOALS (simp_tac (put_simpset norm_ss3 ctxt))
   253 
   254   val numeral_simp_ss =
   255     simpset_of (put_simpset HOL_basic_ss @{context} addsimps add_0s @ simps)
   256   fun numeral_simp_tac ctxt =
   257     ALLGOALS (simp_tac (put_simpset numeral_simp_ss ctxt))
   258   val simplify_meta_eq = Arith_Data.simplify_meta_eq post_simps
   259   val prove_conv = Arith_Data.prove_conv
   260 end;
   261 
   262 structure EqCancelNumerals = CancelNumeralsFun
   263  (open CancelNumeralsCommon
   264   val mk_bal   = HOLogic.mk_eq
   265   val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} dummyT
   266   val bal_add1 = @{thm eq_add_iff1} RS trans
   267   val bal_add2 = @{thm eq_add_iff2} RS trans
   268 );
   269 
   270 structure LessCancelNumerals = CancelNumeralsFun
   271  (open CancelNumeralsCommon
   272   val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less}
   273   val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} dummyT
   274   val bal_add1 = @{thm less_add_iff1} RS trans
   275   val bal_add2 = @{thm less_add_iff2} RS trans
   276 );
   277 
   278 structure LeCancelNumerals = CancelNumeralsFun
   279  (open CancelNumeralsCommon
   280   val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less_eq}
   281   val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} dummyT
   282   val bal_add1 = @{thm le_add_iff1} RS trans
   283   val bal_add2 = @{thm le_add_iff2} RS trans
   284 );
   285 
   286 val eq_cancel_numerals = EqCancelNumerals.proc
   287 val less_cancel_numerals = LessCancelNumerals.proc
   288 val le_cancel_numerals = LeCancelNumerals.proc
   289 
   290 structure CombineNumeralsData =
   291 struct
   292   type coeff = int
   293   val iszero = (fn x => x = 0)
   294   val add  = op +
   295   val mk_sum = long_mk_sum    (*to work for e.g. 2*x + 3*x *)
   296   val dest_sum = dest_sum
   297   val mk_coeff = mk_coeff
   298   val dest_coeff = dest_coeff 1
   299   val left_distrib = @{thm combine_common_factor} RS trans
   300   val prove_conv = Arith_Data.prove_conv_nohyps
   301   val trans_tac = trans_tac
   302 
   303   fun norm_tac ctxt =
   304     ALLGOALS (simp_tac (put_simpset norm_ss1 ctxt))
   305     THEN ALLGOALS (simp_tac (put_simpset norm_ss2 ctxt))
   306     THEN ALLGOALS (simp_tac (put_simpset norm_ss3 ctxt))
   307 
   308   val numeral_simp_ss =
   309     simpset_of (put_simpset HOL_basic_ss @{context} addsimps add_0s @ simps)
   310   fun numeral_simp_tac ctxt =
   311     ALLGOALS (simp_tac (put_simpset numeral_simp_ss ctxt))
   312   val simplify_meta_eq = Arith_Data.simplify_meta_eq post_simps
   313 end;
   314 
   315 structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData);
   316 
   317 (*Version for fields, where coefficients can be fractions*)
   318 structure FieldCombineNumeralsData =
   319 struct
   320   type coeff = int * int
   321   val iszero = (fn (p, _) => p = 0)
   322   val add = add_frac
   323   val mk_sum = long_mk_sum
   324   val dest_sum = dest_sum
   325   val mk_coeff = mk_fcoeff
   326   val dest_coeff = dest_fcoeff 1
   327   val left_distrib = @{thm combine_common_factor} RS trans
   328   val prove_conv = Arith_Data.prove_conv_nohyps
   329   val trans_tac = trans_tac
   330 
   331   val norm_ss1a =
   332     simpset_of (put_simpset norm_ss1 @{context} addsimps inverse_1s @ divide_simps)
   333   fun norm_tac ctxt =
   334     ALLGOALS (simp_tac (put_simpset norm_ss1a ctxt))
   335     THEN ALLGOALS (simp_tac (put_simpset norm_ss2 ctxt))
   336     THEN ALLGOALS (simp_tac (put_simpset norm_ss3 ctxt))
   337 
   338   val numeral_simp_ss =
   339     simpset_of (put_simpset HOL_basic_ss @{context}
   340       addsimps add_0s @ simps @ [@{thm add_frac_eq}, @{thm not_False_eq_True}])
   341   fun numeral_simp_tac ctxt =
   342     ALLGOALS (simp_tac (put_simpset numeral_simp_ss ctxt))
   343   val simplify_meta_eq = Arith_Data.simplify_meta_eq field_post_simps
   344 end;
   345 
   346 structure FieldCombineNumerals = CombineNumeralsFun(FieldCombineNumeralsData);
   347 
   348 val combine_numerals = CombineNumerals.proc
   349 
   350 val field_combine_numerals = FieldCombineNumerals.proc
   351 
   352 
   353 (** Constant folding for multiplication in semirings **)
   354 
   355 (*We do not need folding for addition: combine_numerals does the same thing*)
   356 
   357 structure Semiring_Times_Assoc_Data : ASSOC_FOLD_DATA =
   358 struct
   359   val assoc_ss = simpset_of (put_simpset HOL_basic_ss @{context} addsimps @{thms ac_simps minus_mult_commute})
   360   val eq_reflection = eq_reflection
   361   val is_numeral = can HOLogic.dest_number
   362 end;
   363 
   364 structure Semiring_Times_Assoc = Assoc_Fold (Semiring_Times_Assoc_Data);
   365 
   366 fun assoc_fold ctxt ct = Semiring_Times_Assoc.proc ctxt (Thm.term_of ct)
   367 
   368 structure CancelNumeralFactorCommon =
   369 struct
   370   val mk_coeff = mk_coeff
   371   val dest_coeff = dest_coeff 1
   372   val trans_tac = trans_tac
   373 
   374   val norm_ss1 =
   375     simpset_of (put_simpset HOL_basic_ss @{context} addsimps minus_from_mult_simps @ mult_1s)
   376   val norm_ss2 =
   377     simpset_of (put_simpset HOL_basic_ss @{context} addsimps simps @ mult_minus_simps)
   378   val norm_ss3 =
   379     simpset_of (put_simpset HOL_basic_ss @{context} addsimps @{thms ac_simps minus_mult_commute numeral_times_minus_swap})
   380   fun norm_tac ctxt =
   381     ALLGOALS (simp_tac (put_simpset norm_ss1 ctxt))
   382     THEN ALLGOALS (simp_tac (put_simpset norm_ss2 ctxt))
   383     THEN ALLGOALS (simp_tac (put_simpset norm_ss3 ctxt))
   384 
   385   (* simp_thms are necessary because some of the cancellation rules below
   386   (e.g. mult_less_cancel_left) introduce various logical connectives *)
   387   val numeral_simp_ss =
   388     simpset_of (put_simpset HOL_basic_ss @{context} addsimps simps @ @{thms simp_thms})
   389   fun numeral_simp_tac ctxt =
   390     ALLGOALS (simp_tac (put_simpset numeral_simp_ss ctxt))
   391   val simplify_meta_eq = Arith_Data.simplify_meta_eq
   392     ([@{thm Nat.add_0}, @{thm Nat.add_0_right}] @ post_simps)
   393   val prove_conv = Arith_Data.prove_conv
   394 end
   395 
   396 (*Version for semiring_div*)
   397 structure DivCancelNumeralFactor = CancelNumeralFactorFun
   398  (open CancelNumeralFactorCommon
   399   val mk_bal   = HOLogic.mk_binop @{const_name Rings.divide}
   400   val dest_bal = HOLogic.dest_bin @{const_name Rings.divide} dummyT
   401   val cancel = @{thm div_mult_mult1} RS trans
   402   val neg_exchanges = false
   403 )
   404 
   405 (*Version for fields*)
   406 structure DivideCancelNumeralFactor = CancelNumeralFactorFun
   407  (open CancelNumeralFactorCommon
   408   val mk_bal   = HOLogic.mk_binop @{const_name Rings.divide}
   409   val dest_bal = HOLogic.dest_bin @{const_name Rings.divide} dummyT
   410   val cancel = @{thm mult_divide_mult_cancel_left} RS trans
   411   val neg_exchanges = false
   412 )
   413 
   414 structure EqCancelNumeralFactor = CancelNumeralFactorFun
   415  (open CancelNumeralFactorCommon
   416   val mk_bal   = HOLogic.mk_eq
   417   val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} dummyT
   418   val cancel = @{thm mult_cancel_left} RS trans
   419   val neg_exchanges = false
   420 )
   421 
   422 structure LessCancelNumeralFactor = CancelNumeralFactorFun
   423  (open CancelNumeralFactorCommon
   424   val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less}
   425   val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} dummyT
   426   val cancel = @{thm mult_less_cancel_left} RS trans
   427   val neg_exchanges = true
   428 )
   429 
   430 structure LeCancelNumeralFactor = CancelNumeralFactorFun
   431 (
   432   open CancelNumeralFactorCommon
   433   val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less_eq}
   434   val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} dummyT
   435   val cancel = @{thm mult_le_cancel_left} RS trans
   436   val neg_exchanges = true
   437 )
   438 
   439 val eq_cancel_numeral_factor = EqCancelNumeralFactor.proc
   440 val less_cancel_numeral_factor = LessCancelNumeralFactor.proc
   441 val le_cancel_numeral_factor = LeCancelNumeralFactor.proc
   442 val div_cancel_numeral_factor = DivCancelNumeralFactor.proc
   443 val divide_cancel_numeral_factor = DivideCancelNumeralFactor.proc
   444 
   445 val field_divide_cancel_numeral_factor =
   446   Simplifier.make_simproc @{context} "field_divide_cancel_numeral_factor"
   447    {lhss =
   448      [@{term "((l::'a::field) * m) / n"},
   449       @{term "(l::'a::field) / (m * n)"},
   450       @{term "((numeral v)::'a::field) / (numeral w)"},
   451       @{term "((numeral v)::'a::field) / (- numeral w)"},
   452       @{term "((- numeral v)::'a::field) / (numeral w)"},
   453       @{term "((- numeral v)::'a::field) / (- numeral w)"}],
   454     proc = K DivideCancelNumeralFactor.proc}
   455 
   456 val field_cancel_numeral_factors =
   457   [Simplifier.make_simproc @{context} "field_eq_cancel_numeral_factor"
   458     {lhss =
   459        [@{term "(l::'a::field) * m = n"},
   460         @{term "(l::'a::field) = m * n"}],
   461       proc = K EqCancelNumeralFactor.proc},
   462    field_divide_cancel_numeral_factor]
   463 
   464 
   465 (** Declarations for ExtractCommonTerm **)
   466 
   467 (*Find first term that matches u*)
   468 fun find_first_t past u []         = raise TERM ("find_first_t", [])
   469   | find_first_t past u (t::terms) =
   470         if u aconv t then (rev past @ terms)
   471         else find_first_t (t::past) u terms
   472         handle TERM _ => find_first_t (t::past) u terms;
   473 
   474 (** Final simplification for the CancelFactor simprocs **)
   475 val simplify_one = Arith_Data.simplify_meta_eq
   476   [@{thm mult_1_left}, @{thm mult_1_right}, @{thm div_by_1}, @{thm numeral_One}];
   477 
   478 fun cancel_simplify_meta_eq ctxt cancel_th th =
   479     simplify_one ctxt (([th, cancel_th]) MRS trans);
   480 
   481 local
   482   val Tp_Eq = Thm.reflexive (Thm.cterm_of @{theory_context HOL} HOLogic.Trueprop)
   483   fun Eq_True_elim Eq =
   484     Thm.equal_elim (Thm.combination Tp_Eq (Thm.symmetric Eq)) @{thm TrueI}
   485 in
   486 fun sign_conv pos_th neg_th ctxt t =
   487   let val T = fastype_of t;
   488       val zero = Const(@{const_name Groups.zero}, T);
   489       val less = Const(@{const_name Orderings.less}, [T,T] ---> HOLogic.boolT);
   490       val pos = less $ zero $ t and neg = less $ t $ zero
   491       fun prove p =
   492         SOME (Eq_True_elim (Simplifier.asm_rewrite ctxt (Thm.cterm_of ctxt p)))
   493         handle THM _ => NONE
   494     in case prove pos of
   495          SOME th => SOME(th RS pos_th)
   496        | NONE => (case prove neg of
   497                     SOME th => SOME(th RS neg_th)
   498                   | NONE => NONE)
   499     end;
   500 end
   501 
   502 structure CancelFactorCommon =
   503 struct
   504   val mk_sum = long_mk_prod
   505   val dest_sum = dest_prod
   506   val mk_coeff = mk_coeff
   507   val dest_coeff = dest_coeff
   508   val find_first = find_first_t []
   509   val trans_tac = trans_tac
   510   val norm_ss =
   511     simpset_of (put_simpset HOL_basic_ss @{context} addsimps mult_1s @ @{thms ac_simps minus_mult_commute})
   512   fun norm_tac ctxt =
   513     ALLGOALS (simp_tac (put_simpset norm_ss ctxt))
   514   val simplify_meta_eq  = cancel_simplify_meta_eq
   515   fun mk_eq (a, b) = HOLogic.mk_Trueprop (HOLogic.mk_eq (a, b))
   516 end;
   517 
   518 (*mult_cancel_left requires a ring with no zero divisors.*)
   519 structure EqCancelFactor = ExtractCommonTermFun
   520  (open CancelFactorCommon
   521   val mk_bal   = HOLogic.mk_eq
   522   val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} dummyT
   523   fun simp_conv _ _ = SOME @{thm mult_cancel_left}
   524 );
   525 
   526 (*for ordered rings*)
   527 structure LeCancelFactor = ExtractCommonTermFun
   528  (open CancelFactorCommon
   529   val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less_eq}
   530   val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} dummyT
   531   val simp_conv = sign_conv
   532     @{thm mult_le_cancel_left_pos} @{thm mult_le_cancel_left_neg}
   533 );
   534 
   535 (*for ordered rings*)
   536 structure LessCancelFactor = ExtractCommonTermFun
   537  (open CancelFactorCommon
   538   val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less}
   539   val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} dummyT
   540   val simp_conv = sign_conv
   541     @{thm mult_less_cancel_left_pos} @{thm mult_less_cancel_left_neg}
   542 );
   543 
   544 (*for semirings with division*)
   545 structure DivCancelFactor = ExtractCommonTermFun
   546  (open CancelFactorCommon
   547   val mk_bal   = HOLogic.mk_binop @{const_name Rings.divide}
   548   val dest_bal = HOLogic.dest_bin @{const_name Rings.divide} dummyT
   549   fun simp_conv _ _ = SOME @{thm div_mult_mult1_if}
   550 );
   551 
   552 structure ModCancelFactor = ExtractCommonTermFun
   553  (open CancelFactorCommon
   554   val mk_bal   = HOLogic.mk_binop @{const_name modulo}
   555   val dest_bal = HOLogic.dest_bin @{const_name modulo} dummyT
   556   fun simp_conv _ _ = SOME @{thm mod_mult_mult1}
   557 );
   558 
   559 (*for idoms*)
   560 structure DvdCancelFactor = ExtractCommonTermFun
   561  (open CancelFactorCommon
   562   val mk_bal   = HOLogic.mk_binrel @{const_name Rings.dvd}
   563   val dest_bal = HOLogic.dest_bin @{const_name Rings.dvd} dummyT
   564   fun simp_conv _ _ = SOME @{thm dvd_mult_cancel_left}
   565 );
   566 
   567 (*Version for all fields, including unordered ones (type complex).*)
   568 structure DivideCancelFactor = ExtractCommonTermFun
   569  (open CancelFactorCommon
   570   val mk_bal   = HOLogic.mk_binop @{const_name Rings.divide}
   571   val dest_bal = HOLogic.dest_bin @{const_name Rings.divide} dummyT
   572   fun simp_conv _ _ = SOME @{thm mult_divide_mult_cancel_left_if}
   573 );
   574 
   575 fun eq_cancel_factor ctxt ct = EqCancelFactor.proc ctxt (Thm.term_of ct)
   576 fun le_cancel_factor ctxt ct = LeCancelFactor.proc ctxt (Thm.term_of ct)
   577 fun less_cancel_factor ctxt ct = LessCancelFactor.proc ctxt (Thm.term_of ct)
   578 fun div_cancel_factor ctxt ct = DivCancelFactor.proc ctxt (Thm.term_of ct)
   579 fun mod_cancel_factor ctxt ct = ModCancelFactor.proc ctxt (Thm.term_of ct)
   580 fun dvd_cancel_factor ctxt ct = DvdCancelFactor.proc ctxt (Thm.term_of ct)
   581 fun divide_cancel_factor ctxt ct = DivideCancelFactor.proc ctxt (Thm.term_of ct)
   582 
   583 local
   584 
   585 val cterm_of = Thm.cterm_of @{context};
   586 fun tvar S = (("'a", 0), S);
   587 
   588 val zero_tvar = tvar @{sort zero};
   589 val zero = cterm_of (Const (@{const_name zero_class.zero}, TVar zero_tvar));
   590 
   591 val type_tvar = tvar @{sort type};
   592 val geq = cterm_of (Const (@{const_name HOL.eq}, TVar type_tvar --> TVar type_tvar --> @{typ bool}));
   593 
   594 val add_frac_eq = mk_meta_eq @{thm "add_frac_eq"}
   595 val add_frac_num = mk_meta_eq @{thm "add_frac_num"}
   596 val add_num_frac = mk_meta_eq @{thm "add_num_frac"}
   597 
   598 fun prove_nz ctxt T t =
   599   let
   600     val z = Thm.instantiate_cterm ([(zero_tvar, T)], []) zero
   601     val eq = Thm.instantiate_cterm ([(type_tvar, T)], []) geq
   602     val th =
   603       Simplifier.rewrite (ctxt addsimps @{thms simp_thms})
   604         (Thm.apply @{cterm "Trueprop"} (Thm.apply @{cterm "Not"}
   605           (Thm.apply (Thm.apply eq t) z)))
   606   in Thm.equal_elim (Thm.symmetric th) TrueI end
   607 
   608 fun proc ctxt ct =
   609   let
   610     val ((x,y),(w,z)) =
   611          (Thm.dest_binop #> (fn (a,b) => (Thm.dest_binop a, Thm.dest_binop b))) ct
   612     val _ = map (HOLogic.dest_number o Thm.term_of) [x,y,z,w]
   613     val T = Thm.ctyp_of_cterm x
   614     val [y_nz, z_nz] = map (prove_nz ctxt T) [y, z]
   615     val th = Thm.instantiate' [SOME T] (map SOME [y,z,x,w]) add_frac_eq
   616   in SOME (Thm.implies_elim (Thm.implies_elim th y_nz) z_nz) end
   617   handle CTERM _ => NONE | TERM _ => NONE | THM _ => NONE
   618 
   619 fun proc2 ctxt ct =
   620   let
   621     val (l,r) = Thm.dest_binop ct
   622     val T = Thm.ctyp_of_cterm l
   623   in (case (Thm.term_of l, Thm.term_of r) of
   624       (Const(@{const_name Rings.divide},_)$_$_, _) =>
   625         let val (x,y) = Thm.dest_binop l val z = r
   626             val _ = map (HOLogic.dest_number o Thm.term_of) [x,y,z]
   627             val ynz = prove_nz ctxt T y
   628         in SOME (Thm.implies_elim (Thm.instantiate' [SOME T] (map SOME [y,x,z]) add_frac_num) ynz)
   629         end
   630      | (_, Const (@{const_name Rings.divide},_)$_$_) =>
   631         let val (x,y) = Thm.dest_binop r val z = l
   632             val _ = map (HOLogic.dest_number o Thm.term_of) [x,y,z]
   633             val ynz = prove_nz ctxt T y
   634         in SOME (Thm.implies_elim (Thm.instantiate' [SOME T] (map SOME [y,z,x]) add_num_frac) ynz)
   635         end
   636      | _ => NONE)
   637   end
   638   handle CTERM _ => NONE | TERM _ => NONE | THM _ => NONE
   639 
   640 fun is_number (Const(@{const_name Rings.divide},_)$a$b) = is_number a andalso is_number b
   641   | is_number t = can HOLogic.dest_number t
   642 
   643 val is_number = is_number o Thm.term_of
   644 
   645 fun proc3 ctxt ct =
   646   (case Thm.term_of ct of
   647     Const(@{const_name Orderings.less},_)$(Const(@{const_name Rings.divide},_)$_$_)$_ =>
   648       let
   649         val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
   650         val _ = map is_number [a,b,c]
   651         val T = Thm.ctyp_of_cterm c
   652         val th = Thm.instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_less_eq"}
   653       in SOME (mk_meta_eq th) end
   654   | Const(@{const_name Orderings.less_eq},_)$(Const(@{const_name Rings.divide},_)$_$_)$_ =>
   655       let
   656         val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
   657         val _ = map is_number [a,b,c]
   658         val T = Thm.ctyp_of_cterm c
   659         val th = Thm.instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_le_eq"}
   660       in SOME (mk_meta_eq th) end
   661   | Const(@{const_name HOL.eq},_)$(Const(@{const_name Rings.divide},_)$_$_)$_ =>
   662       let
   663         val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
   664         val _ = map is_number [a,b,c]
   665         val T = Thm.ctyp_of_cterm c
   666         val th = Thm.instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_eq_eq"}
   667       in SOME (mk_meta_eq th) end
   668   | Const(@{const_name Orderings.less},_)$_$(Const(@{const_name Rings.divide},_)$_$_) =>
   669     let
   670       val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
   671         val _ = map is_number [a,b,c]
   672         val T = Thm.ctyp_of_cterm c
   673         val th = Thm.instantiate' [SOME T] (map SOME [a,b,c]) @{thm "less_divide_eq"}
   674       in SOME (mk_meta_eq th) end
   675   | Const(@{const_name Orderings.less_eq},_)$_$(Const(@{const_name Rings.divide},_)$_$_) =>
   676     let
   677       val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
   678         val _ = map is_number [a,b,c]
   679         val T = Thm.ctyp_of_cterm c
   680         val th = Thm.instantiate' [SOME T] (map SOME [a,b,c]) @{thm "le_divide_eq"}
   681       in SOME (mk_meta_eq th) end
   682   | Const(@{const_name HOL.eq},_)$_$(Const(@{const_name Rings.divide},_)$_$_) =>
   683     let
   684       val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
   685         val _ = map is_number [a,b,c]
   686         val T = Thm.ctyp_of_cterm c
   687         val th = Thm.instantiate' [SOME T] (map SOME [a,b,c]) @{thm "eq_divide_eq"}
   688       in SOME (mk_meta_eq th) end
   689   | _ => NONE) handle TERM _ => NONE | CTERM _ => NONE | THM _ => NONE
   690 
   691 val add_frac_frac_simproc =
   692   Simplifier.make_simproc @{context} "add_frac_frac_simproc"
   693    {lhss = [@{term "(x::'a::field) / y + (w::'a::field) / z"}],
   694     proc = K proc}
   695 
   696 val add_frac_num_simproc =
   697   Simplifier.make_simproc @{context} "add_frac_num_simproc"
   698    {lhss = [@{term "(x::'a::field) / y + z"}, @{term "z + (x::'a::field) / y"}],
   699     proc = K proc2}
   700 
   701 val ord_frac_simproc =
   702   Simplifier.make_simproc @{context} "ord_frac_simproc"
   703    {lhss =
   704      [@{term "(a::'a::{field,ord}) / b < c"},
   705       @{term "(a::'a::{field,ord}) / b \<le> c"},
   706       @{term "c < (a::'a::{field,ord}) / b"},
   707       @{term "c \<le> (a::'a::{field,ord}) / b"},
   708       @{term "c = (a::'a::{field,ord}) / b"},
   709       @{term "(a::'a::{field, ord}) / b = c"}],
   710     proc = K proc3}
   711 
   712 val ths =
   713  [@{thm "mult_numeral_1"}, @{thm "mult_numeral_1_right"},
   714   @{thm "divide_numeral_1"},
   715   @{thm "div_by_0"}, @{thm div_0},
   716   @{thm "divide_divide_eq_left"},
   717   @{thm "times_divide_eq_left"}, @{thm "times_divide_eq_right"},
   718   @{thm "times_divide_times_eq"},
   719   @{thm "divide_divide_eq_right"},
   720   @{thm diff_conv_add_uminus}, @{thm "minus_divide_left"},
   721   @{thm "add_divide_distrib"} RS sym,
   722   @{thm Fields.field_divide_inverse} RS sym, @{thm inverse_divide},
   723   Conv.fconv_rule (Conv.arg_conv (Conv.arg1_conv (Conv.rewr_conv (mk_meta_eq @{thm mult.commute}))))
   724   (@{thm Fields.field_divide_inverse} RS sym)]
   725 
   726 val field_comp_ss =
   727   simpset_of
   728     (put_simpset HOL_basic_ss @{context}
   729       addsimps @{thms "semiring_norm"}
   730       addsimps ths addsimps @{thms simp_thms}
   731       addsimprocs field_cancel_numeral_factors
   732       addsimprocs [add_frac_frac_simproc, add_frac_num_simproc, ord_frac_simproc]
   733       |> Simplifier.add_cong @{thm "if_weak_cong"})
   734 
   735 in
   736 
   737 fun field_comp_conv ctxt =
   738   Simplifier.rewrite (put_simpset field_comp_ss ctxt)
   739   then_conv
   740   Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps [@{thm numeral_One}])
   741 
   742 end
   743 
   744 end;