src/HOL/Tools/numeral_simprocs.ML
changeset 44945 2625de88c994
parent 44064 5bce8ff0d9ae
child 44947 8ae418dfe561
     1.1 --- a/src/HOL/Tools/numeral_simprocs.ML	Sat Sep 17 04:41:44 2011 +0200
     1.2 +++ b/src/HOL/Tools/numeral_simprocs.ML	Sat Sep 17 00:37:21 2011 +0200
     1.3 @@ -16,6 +16,9 @@
     1.4  
     1.5  signature NUMERAL_SIMPROCS =
     1.6  sig
     1.7 +  val prep_simproc: theory -> string * string list * (theory -> simpset -> term -> thm option)
     1.8 +    -> simproc
     1.9 +  val trans_tac: thm option -> tactic
    1.10    val assoc_fold_simproc: simproc
    1.11    val combine_numerals: simproc
    1.12    val cancel_numerals: simproc list
    1.13 @@ -30,6 +33,12 @@
    1.14  structure Numeral_Simprocs : NUMERAL_SIMPROCS =
    1.15  struct
    1.16  
    1.17 +fun prep_simproc thy (name, pats, proc) =
    1.18 +  Simplifier.simproc_global thy name pats proc;
    1.19 +
    1.20 +fun trans_tac NONE  = all_tac
    1.21 +  | trans_tac (SOME th) = ALLGOALS (rtac (th RS trans));
    1.22 +
    1.23  val mk_number = Arith_Data.mk_number;
    1.24  val mk_sum = Arith_Data.mk_sum;
    1.25  val long_mk_sum = Arith_Data.long_mk_sum;
    1.26 @@ -199,13 +208,13 @@
    1.27  val norm_ss3 = num_ss addsimps minus_from_mult_simps @ @{thms add_ac} @ @{thms mult_ac}
    1.28  
    1.29  structure CancelNumeralsCommon =
    1.30 -  struct
    1.31 -  val mk_sum            = mk_sum
    1.32 -  val dest_sum          = dest_sum
    1.33 -  val mk_coeff          = mk_coeff
    1.34 -  val dest_coeff        = dest_coeff 1
    1.35 -  val find_first_coeff  = find_first_coeff []
    1.36 -  fun trans_tac _       = Arith_Data.trans_tac
    1.37 +struct
    1.38 +  val mk_sum = mk_sum
    1.39 +  val dest_sum = dest_sum
    1.40 +  val mk_coeff = mk_coeff
    1.41 +  val dest_coeff = dest_coeff 1
    1.42 +  val find_first_coeff = find_first_coeff []
    1.43 +  val trans_tac = K trans_tac
    1.44  
    1.45    fun norm_tac ss =
    1.46      ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
    1.47 @@ -215,12 +224,11 @@
    1.48    val numeral_simp_ss = HOL_ss addsimps add_0s @ simps
    1.49    fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
    1.50    val simplify_meta_eq = Arith_Data.simplify_meta_eq (add_0s @ mult_1s)
    1.51 -  end;
    1.52 -
    1.53 +  val prove_conv = Arith_Data.prove_conv
    1.54 +end;
    1.55  
    1.56  structure EqCancelNumerals = CancelNumeralsFun
    1.57   (open CancelNumeralsCommon
    1.58 -  val prove_conv = Arith_Data.prove_conv
    1.59    val mk_bal   = HOLogic.mk_eq
    1.60    val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} Term.dummyT
    1.61    val bal_add1 = @{thm eq_add_iff1} RS trans
    1.62 @@ -229,7 +237,6 @@
    1.63  
    1.64  structure LessCancelNumerals = CancelNumeralsFun
    1.65   (open CancelNumeralsCommon
    1.66 -  val prove_conv = Arith_Data.prove_conv
    1.67    val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less}
    1.68    val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} Term.dummyT
    1.69    val bal_add1 = @{thm less_add_iff1} RS trans
    1.70 @@ -238,7 +245,6 @@
    1.71  
    1.72  structure LeCancelNumerals = CancelNumeralsFun
    1.73   (open CancelNumeralsCommon
    1.74 -  val prove_conv = Arith_Data.prove_conv
    1.75    val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less_eq}
    1.76    val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} Term.dummyT
    1.77    val bal_add1 = @{thm le_add_iff1} RS trans
    1.78 @@ -246,7 +252,7 @@
    1.79  );
    1.80  
    1.81  val cancel_numerals =
    1.82 -  map (Arith_Data.prep_simproc @{theory})
    1.83 +  map (prep_simproc @{theory})
    1.84     [("inteq_cancel_numerals",
    1.85       ["(l::'a::number_ring) + m = n",
    1.86        "(l::'a::number_ring) = m + n",
    1.87 @@ -273,17 +279,17 @@
    1.88       K LeCancelNumerals.proc)];
    1.89  
    1.90  structure CombineNumeralsData =
    1.91 -  struct
    1.92 -  type coeff            = int
    1.93 -  val iszero            = (fn x => x = 0)
    1.94 -  val add               = op +
    1.95 -  val mk_sum            = long_mk_sum    (*to work for e.g. 2*x + 3*x *)
    1.96 -  val dest_sum          = dest_sum
    1.97 -  val mk_coeff          = mk_coeff
    1.98 -  val dest_coeff        = dest_coeff 1
    1.99 -  val left_distrib      = @{thm combine_common_factor} RS trans
   1.100 -  val prove_conv        = Arith_Data.prove_conv_nohyps
   1.101 -  fun trans_tac _       = Arith_Data.trans_tac
   1.102 +struct
   1.103 +  type coeff = int
   1.104 +  val iszero = (fn x => x = 0)
   1.105 +  val add  = op +
   1.106 +  val mk_sum = long_mk_sum    (*to work for e.g. 2*x + 3*x *)
   1.107 +  val dest_sum = dest_sum
   1.108 +  val mk_coeff = mk_coeff
   1.109 +  val dest_coeff = dest_coeff 1
   1.110 +  val left_distrib = @{thm combine_common_factor} RS trans
   1.111 +  val prove_conv = Arith_Data.prove_conv_nohyps
   1.112 +  val trans_tac = K trans_tac
   1.113  
   1.114    fun norm_tac ss =
   1.115      ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
   1.116 @@ -293,23 +299,23 @@
   1.117    val numeral_simp_ss = HOL_ss addsimps add_0s @ simps
   1.118    fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
   1.119    val simplify_meta_eq = Arith_Data.simplify_meta_eq (add_0s @ mult_1s)
   1.120 -  end;
   1.121 +end;
   1.122  
   1.123  structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData);
   1.124  
   1.125  (*Version for fields, where coefficients can be fractions*)
   1.126  structure FieldCombineNumeralsData =
   1.127 -  struct
   1.128 -  type coeff            = int * int
   1.129 -  val iszero            = (fn (p, q) => p = 0)
   1.130 -  val add               = add_frac
   1.131 -  val mk_sum            = long_mk_sum
   1.132 -  val dest_sum          = dest_sum
   1.133 -  val mk_coeff          = mk_fcoeff
   1.134 -  val dest_coeff        = dest_fcoeff 1
   1.135 -  val left_distrib      = @{thm combine_common_factor} RS trans
   1.136 -  val prove_conv        = Arith_Data.prove_conv_nohyps
   1.137 -  fun trans_tac _       = Arith_Data.trans_tac
   1.138 +struct
   1.139 +  type coeff = int * int
   1.140 +  val iszero = (fn (p, q) => p = 0)
   1.141 +  val add = add_frac
   1.142 +  val mk_sum = long_mk_sum
   1.143 +  val dest_sum = dest_sum
   1.144 +  val mk_coeff = mk_fcoeff
   1.145 +  val dest_coeff = dest_fcoeff 1
   1.146 +  val left_distrib = @{thm combine_common_factor} RS trans
   1.147 +  val prove_conv = Arith_Data.prove_conv_nohyps
   1.148 +  val trans_tac = K trans_tac
   1.149  
   1.150    val norm_ss1a = norm_ss1 addsimps inverse_1s @ divide_simps
   1.151    fun norm_tac ss =
   1.152 @@ -320,18 +326,18 @@
   1.153    val numeral_simp_ss = HOL_ss addsimps add_0s @ simps @ [@{thm add_frac_eq}]
   1.154    fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
   1.155    val simplify_meta_eq = Arith_Data.simplify_meta_eq (add_0s @ mult_1s @ divide_1s)
   1.156 -  end;
   1.157 +end;
   1.158  
   1.159  structure FieldCombineNumerals = CombineNumeralsFun(FieldCombineNumeralsData);
   1.160  
   1.161  val combine_numerals =
   1.162 -  Arith_Data.prep_simproc @{theory}
   1.163 +  prep_simproc @{theory}
   1.164      ("int_combine_numerals", 
   1.165       ["(i::'a::number_ring) + j", "(i::'a::number_ring) - j"], 
   1.166       K CombineNumerals.proc);
   1.167  
   1.168  val field_combine_numerals =
   1.169 -  Arith_Data.prep_simproc @{theory}
   1.170 +  prep_simproc @{theory}
   1.171      ("field_combine_numerals", 
   1.172       ["(i::'a::{field_inverse_zero, number_ring}) + j",
   1.173        "(i::'a::{field_inverse_zero, number_ring}) - j"], 
   1.174 @@ -351,15 +357,15 @@
   1.175  structure Semiring_Times_Assoc = Assoc_Fold (Semiring_Times_Assoc_Data);
   1.176  
   1.177  val assoc_fold_simproc =
   1.178 -  Arith_Data.prep_simproc @{theory}
   1.179 +  prep_simproc @{theory}
   1.180     ("semiring_assoc_fold", ["(a::'a::comm_semiring_1_cancel) * b"],
   1.181      K Semiring_Times_Assoc.proc);
   1.182  
   1.183  structure CancelNumeralFactorCommon =
   1.184 -  struct
   1.185 -  val mk_coeff          = mk_coeff
   1.186 -  val dest_coeff        = dest_coeff 1
   1.187 -  fun trans_tac _       = Arith_Data.trans_tac
   1.188 +struct
   1.189 +  val mk_coeff = mk_coeff
   1.190 +  val dest_coeff = dest_coeff 1
   1.191 +  val trans_tac = K trans_tac
   1.192  
   1.193    val norm_ss1 = HOL_ss addsimps minus_from_mult_simps @ mult_1s
   1.194    val norm_ss2 = HOL_ss addsimps simps @ mult_minus_simps
   1.195 @@ -375,12 +381,12 @@
   1.196    val simplify_meta_eq = Arith_Data.simplify_meta_eq
   1.197      [@{thm Nat.add_0}, @{thm Nat.add_0_right}, @{thm mult_zero_left},
   1.198        @{thm mult_zero_right}, @{thm mult_Bit1}, @{thm mult_1_right}];
   1.199 -  end
   1.200 +  val prove_conv = Arith_Data.prove_conv
   1.201 +end
   1.202  
   1.203  (*Version for semiring_div*)
   1.204  structure DivCancelNumeralFactor = CancelNumeralFactorFun
   1.205   (open CancelNumeralFactorCommon
   1.206 -  val prove_conv = Arith_Data.prove_conv
   1.207    val mk_bal   = HOLogic.mk_binop @{const_name Divides.div}
   1.208    val dest_bal = HOLogic.dest_bin @{const_name Divides.div} Term.dummyT
   1.209    val cancel = @{thm div_mult_mult1} RS trans
   1.210 @@ -390,7 +396,6 @@
   1.211  (*Version for fields*)
   1.212  structure DivideCancelNumeralFactor = CancelNumeralFactorFun
   1.213   (open CancelNumeralFactorCommon
   1.214 -  val prove_conv = Arith_Data.prove_conv
   1.215    val mk_bal   = HOLogic.mk_binop @{const_name Fields.divide}
   1.216    val dest_bal = HOLogic.dest_bin @{const_name Fields.divide} Term.dummyT
   1.217    val cancel = @{thm mult_divide_mult_cancel_left} RS trans
   1.218 @@ -399,7 +404,6 @@
   1.219  
   1.220  structure EqCancelNumeralFactor = CancelNumeralFactorFun
   1.221   (open CancelNumeralFactorCommon
   1.222 -  val prove_conv = Arith_Data.prove_conv
   1.223    val mk_bal   = HOLogic.mk_eq
   1.224    val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} Term.dummyT
   1.225    val cancel = @{thm mult_cancel_left} RS trans
   1.226 @@ -408,7 +412,6 @@
   1.227  
   1.228  structure LessCancelNumeralFactor = CancelNumeralFactorFun
   1.229   (open CancelNumeralFactorCommon
   1.230 -  val prove_conv = Arith_Data.prove_conv
   1.231    val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less}
   1.232    val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} Term.dummyT
   1.233    val cancel = @{thm mult_less_cancel_left} RS trans
   1.234 @@ -417,7 +420,6 @@
   1.235  
   1.236  structure LeCancelNumeralFactor = CancelNumeralFactorFun
   1.237   (open CancelNumeralFactorCommon
   1.238 -  val prove_conv = Arith_Data.prove_conv
   1.239    val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less_eq}
   1.240    val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} Term.dummyT
   1.241    val cancel = @{thm mult_le_cancel_left} RS trans
   1.242 @@ -425,7 +427,7 @@
   1.243  )
   1.244  
   1.245  val cancel_numeral_factors =
   1.246 -  map (Arith_Data.prep_simproc @{theory})
   1.247 +  map (prep_simproc @{theory})
   1.248     [("ring_eq_cancel_numeral_factor",
   1.249       ["(l::'a::{idom,number_ring}) * m = n",
   1.250        "(l::'a::{idom,number_ring}) = m * n"],
   1.251 @@ -449,7 +451,7 @@
   1.252       K DivideCancelNumeralFactor.proc)];
   1.253  
   1.254  val field_cancel_numeral_factors =
   1.255 -  map (Arith_Data.prep_simproc @{theory})
   1.256 +  map (prep_simproc @{theory})
   1.257     [("field_eq_cancel_numeral_factor",
   1.258       ["(l::'a::{field,number_ring}) * m = n",
   1.259        "(l::'a::{field,number_ring}) = m * n"],
   1.260 @@ -499,22 +501,22 @@
   1.261  end
   1.262  
   1.263  structure CancelFactorCommon =
   1.264 -  struct
   1.265 -  val mk_sum            = long_mk_prod
   1.266 -  val dest_sum          = dest_prod
   1.267 -  val mk_coeff          = mk_coeff
   1.268 -  val dest_coeff        = dest_coeff
   1.269 -  val find_first        = find_first_t []
   1.270 -  fun trans_tac _       = Arith_Data.trans_tac
   1.271 +struct
   1.272 +  val mk_sum = long_mk_prod
   1.273 +  val dest_sum = dest_prod
   1.274 +  val mk_coeff = mk_coeff
   1.275 +  val dest_coeff = dest_coeff
   1.276 +  val find_first = find_first_t []
   1.277 +  val trans_tac = K trans_tac
   1.278    val norm_ss = HOL_ss addsimps mult_1s @ @{thms mult_ac}
   1.279    fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss))
   1.280    val simplify_meta_eq  = cancel_simplify_meta_eq 
   1.281 -  end;
   1.282 +  val prove_conv = Arith_Data.prove_conv
   1.283 +end;
   1.284  
   1.285  (*mult_cancel_left requires a ring with no zero divisors.*)
   1.286  structure EqCancelFactor = ExtractCommonTermFun
   1.287   (open CancelFactorCommon
   1.288 -  val prove_conv = Arith_Data.prove_conv
   1.289    val mk_bal   = HOLogic.mk_eq
   1.290    val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} Term.dummyT
   1.291    fun simp_conv _ _ = SOME @{thm mult_cancel_left}
   1.292 @@ -523,7 +525,6 @@
   1.293  (*for ordered rings*)
   1.294  structure LeCancelFactor = ExtractCommonTermFun
   1.295   (open CancelFactorCommon
   1.296 -  val prove_conv = Arith_Data.prove_conv
   1.297    val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less_eq}
   1.298    val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} Term.dummyT
   1.299    val simp_conv = sign_conv
   1.300 @@ -533,7 +534,6 @@
   1.301  (*for ordered rings*)
   1.302  structure LessCancelFactor = ExtractCommonTermFun
   1.303   (open CancelFactorCommon
   1.304 -  val prove_conv = Arith_Data.prove_conv
   1.305    val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less}
   1.306    val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} Term.dummyT
   1.307    val simp_conv = sign_conv
   1.308 @@ -543,7 +543,6 @@
   1.309  (*for semirings with division*)
   1.310  structure DivCancelFactor = ExtractCommonTermFun
   1.311   (open CancelFactorCommon
   1.312 -  val prove_conv = Arith_Data.prove_conv
   1.313    val mk_bal   = HOLogic.mk_binop @{const_name Divides.div}
   1.314    val dest_bal = HOLogic.dest_bin @{const_name Divides.div} Term.dummyT
   1.315    fun simp_conv _ _ = SOME @{thm div_mult_mult1_if}
   1.316 @@ -551,7 +550,6 @@
   1.317  
   1.318  structure ModCancelFactor = ExtractCommonTermFun
   1.319   (open CancelFactorCommon
   1.320 -  val prove_conv = Arith_Data.prove_conv
   1.321    val mk_bal   = HOLogic.mk_binop @{const_name Divides.mod}
   1.322    val dest_bal = HOLogic.dest_bin @{const_name Divides.mod} Term.dummyT
   1.323    fun simp_conv _ _ = SOME @{thm mod_mult_mult1}
   1.324 @@ -560,7 +558,6 @@
   1.325  (*for idoms*)
   1.326  structure DvdCancelFactor = ExtractCommonTermFun
   1.327   (open CancelFactorCommon
   1.328 -  val prove_conv = Arith_Data.prove_conv
   1.329    val mk_bal   = HOLogic.mk_binrel @{const_name Rings.dvd}
   1.330    val dest_bal = HOLogic.dest_bin @{const_name Rings.dvd} Term.dummyT
   1.331    fun simp_conv _ _ = SOME @{thm dvd_mult_cancel_left}
   1.332 @@ -569,14 +566,13 @@
   1.333  (*Version for all fields, including unordered ones (type complex).*)
   1.334  structure DivideCancelFactor = ExtractCommonTermFun
   1.335   (open CancelFactorCommon
   1.336 -  val prove_conv = Arith_Data.prove_conv
   1.337    val mk_bal   = HOLogic.mk_binop @{const_name Fields.divide}
   1.338    val dest_bal = HOLogic.dest_bin @{const_name Fields.divide} Term.dummyT
   1.339    fun simp_conv _ _ = SOME @{thm mult_divide_mult_cancel_left_if}
   1.340  );
   1.341  
   1.342  val cancel_factors =
   1.343 -  map (Arith_Data.prep_simproc @{theory})
   1.344 +  map (prep_simproc @{theory})
   1.345     [("ring_eq_cancel_factor",
   1.346       ["(l::'a::idom) * m = n",
   1.347        "(l::'a::idom) = m * n"],