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