must not cancel common factors on both sides of (in)equations in linear arithmetic decicision procedure
authornipkow
Fri May 30 18:13:40 2014 +0200 (2014-05-30)
changeset 57136653e56c6c963
parent 57135 161cf68af300
child 57137 f174712d0a84
must not cancel common factors on both sides of (in)equations in linear arithmetic decicision procedure
src/HOL/Rat.thy
src/HOL/Tools/numeral_simprocs.ML
     1.1 --- a/src/HOL/Rat.thy	Fri May 30 16:10:57 2014 +0200
     1.2 +++ b/src/HOL/Rat.thy	Fri May 30 18:13:40 2014 +0200
     1.3 @@ -629,7 +629,7 @@
     1.4        @{thm minus_divide_left} RS sym, @{thm minus_divide_right} RS sym,
     1.5        @{thm of_int_minus}, @{thm of_int_diff},
     1.6        @{thm of_int_of_nat_eq}]
     1.7 -  #> Lin_Arith.add_simprocs Numeral_Simprocs.field_cancel_numeral_factors
     1.8 +  #> Lin_Arith.add_simprocs Numeral_Simprocs.field_divide_cancel_numeral_factor
     1.9    #> Lin_Arith.add_inj_const (@{const_name of_nat}, @{typ "nat => rat"})
    1.10    #> Lin_Arith.add_inj_const (@{const_name of_int}, @{typ "int => rat"}))
    1.11  *}
     2.1 --- a/src/HOL/Tools/numeral_simprocs.ML	Fri May 30 16:10:57 2014 +0200
     2.2 +++ b/src/HOL/Tools/numeral_simprocs.ML	Fri May 30 18:13:40 2014 +0200
     2.3 @@ -37,7 +37,7 @@
     2.4    val div_cancel_numeral_factor: Proof.context -> cterm -> thm option
     2.5    val divide_cancel_numeral_factor: Proof.context -> cterm -> thm option
     2.6    val field_combine_numerals: Proof.context -> cterm -> thm option
     2.7 -  val field_cancel_numeral_factors: simproc list
     2.8 +  val field_divide_cancel_numeral_factor: simproc list
     2.9    val num_ss: simpset
    2.10    val field_comp_conv: Proof.context -> conv
    2.11  end;
    2.12 @@ -446,20 +446,24 @@
    2.13  fun div_cancel_numeral_factor ctxt ct = DivCancelNumeralFactor.proc ctxt (term_of ct)
    2.14  fun divide_cancel_numeral_factor ctxt ct = DivideCancelNumeralFactor.proc ctxt (term_of ct)
    2.15  
    2.16 -val field_cancel_numeral_factors =
    2.17 -  map (prep_simproc @{theory})
    2.18 -   [("field_eq_cancel_numeral_factor",
    2.19 -     ["(l::'a::field) * m = n",
    2.20 -      "(l::'a::field) = m * n"],
    2.21 -     EqCancelNumeralFactor.proc),
    2.22 -    ("field_cancel_numeral_factor",
    2.23 +val field_divide_cancel_numeral_factor =
    2.24 +  [prep_simproc @{theory}
    2.25 +    ("field_divide_cancel_numeral_factor",
    2.26       ["((l::'a::field_inverse_zero) * m) / n",
    2.27        "(l::'a::field_inverse_zero) / (m * n)",
    2.28        "((numeral v)::'a::field_inverse_zero) / (numeral w)",
    2.29        "((numeral v)::'a::field_inverse_zero) / (- numeral w)",
    2.30        "((- numeral v)::'a::field_inverse_zero) / (numeral w)",
    2.31        "((- numeral v)::'a::field_inverse_zero) / (- numeral w)"],
    2.32 -     DivideCancelNumeralFactor.proc)]
    2.33 +     DivideCancelNumeralFactor.proc)];
    2.34 +
    2.35 +val field_cancel_numeral_factors =
    2.36 +  prep_simproc @{theory}
    2.37 +    ("field_eq_cancel_numeral_factor",
    2.38 +     ["(l::'a::field) * m = n",
    2.39 +      "(l::'a::field) = m * n"],
    2.40 +     EqCancelNumeralFactor.proc)
    2.41 +   :: field_divide_cancel_numeral_factor;
    2.42  
    2.43  
    2.44  (** Declarations for ExtractCommonTerm **)