src/HOL/Tools/int_arith.ML
changeset 30496 7cdcc9dd95cb
parent 29269 5c25a2012975
child 30518 07b45c1aa788
     1.1 --- a/src/HOL/Tools/int_arith.ML	Thu Mar 12 18:01:25 2009 +0100
     1.2 +++ b/src/HOL/Tools/int_arith.ML	Thu Mar 12 18:01:26 2009 +0100
     1.3 @@ -1,59 +1,32 @@
     1.4 -(*  Title:      HOL/Tools/int_arith1.ML
     1.5 -    Authors:    Larry Paulson and Tobias Nipkow
     1.6 -
     1.7 -Simprocs and decision procedure for linear arithmetic.
     1.8 -*)
     1.9 -
    1.10 -structure Int_Numeral_Base_Simprocs =
    1.11 -  struct
    1.12 -  fun prove_conv tacs ctxt (_: thm list) (t, u) =
    1.13 -    if t aconv u then NONE
    1.14 -    else
    1.15 -      let val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u))
    1.16 -      in SOME (Goal.prove ctxt [] [] eq (K (EVERY tacs))) end
    1.17 -
    1.18 -  fun prove_conv_nohyps tacs sg = prove_conv tacs sg [];
    1.19 -
    1.20 -  fun prep_simproc (name, pats, proc) =
    1.21 -    Simplifier.simproc (the_context()) name pats proc;
    1.22 -
    1.23 -  fun is_numeral (Const(@{const_name Int.number_of}, _) $ w) = true
    1.24 -    | is_numeral _ = false
    1.25 -
    1.26 -  fun simplify_meta_eq f_number_of_eq f_eq =
    1.27 -      mk_meta_eq ([f_eq, f_number_of_eq] MRS trans)
    1.28 +(* Authors: Larry Paulson and Tobias Nipkow
    1.29  
    1.30 -  (*reorientation simprules using ==, for the following simproc*)
    1.31 -  val meta_zero_reorient = @{thm zero_reorient} RS eq_reflection
    1.32 -  val meta_one_reorient = @{thm one_reorient} RS eq_reflection
    1.33 -  val meta_number_of_reorient = @{thm number_of_reorient} RS eq_reflection
    1.34 -
    1.35 -  (*reorientation simplification procedure: reorients (polymorphic) 
    1.36 -    0 = x, 1 = x, nnn = x provided x isn't 0, 1 or a Int.*)
    1.37 -  fun reorient_proc sg _ (_ $ t $ u) =
    1.38 -    case u of
    1.39 -        Const(@{const_name HOL.zero}, _) => NONE
    1.40 -      | Const(@{const_name HOL.one}, _) => NONE
    1.41 -      | Const(@{const_name Int.number_of}, _) $ _ => NONE
    1.42 -      | _ => SOME (case t of
    1.43 -          Const(@{const_name HOL.zero}, _) => meta_zero_reorient
    1.44 -        | Const(@{const_name HOL.one}, _) => meta_one_reorient
    1.45 -        | Const(@{const_name Int.number_of}, _) $ _ => meta_number_of_reorient)
    1.46 -
    1.47 -  val reorient_simproc = 
    1.48 -      prep_simproc ("reorient_simproc", ["0=x", "1=x", "number_of w = x"], reorient_proc)
    1.49 -
    1.50 -  end;
    1.51 -
    1.52 -
    1.53 -Addsimprocs [Int_Numeral_Base_Simprocs.reorient_simproc];
    1.54 -
    1.55 +Simprocs and decision procedure for numerals and linear arithmetic.
    1.56 +*)
    1.57  
    1.58  structure Int_Numeral_Simprocs =
    1.59  struct
    1.60  
    1.61 -(*Maps 0 to Numeral0 and 1 to Numeral1 so that arithmetic in Int_Numeral_Base_Simprocs
    1.62 -  isn't complicated by the abstract 0 and 1.*)
    1.63 +(*reorientation simprules using ==, for the following simproc*)
    1.64 +val meta_zero_reorient = @{thm zero_reorient} RS eq_reflection
    1.65 +val meta_one_reorient = @{thm one_reorient} RS eq_reflection
    1.66 +val meta_number_of_reorient = @{thm number_of_reorient} RS eq_reflection
    1.67 +
    1.68 +(*reorientation simplification procedure: reorients (polymorphic) 
    1.69 +  0 = x, 1 = x, nnn = x provided x isn't 0, 1 or a Int.*)
    1.70 +fun reorient_proc sg _ (_ $ t $ u) =
    1.71 +  case u of
    1.72 +      Const(@{const_name HOL.zero}, _) => NONE
    1.73 +    | Const(@{const_name HOL.one}, _) => NONE
    1.74 +    | Const(@{const_name Int.number_of}, _) $ _ => NONE
    1.75 +    | _ => SOME (case t of
    1.76 +        Const(@{const_name HOL.zero}, _) => meta_zero_reorient
    1.77 +      | Const(@{const_name HOL.one}, _) => meta_one_reorient
    1.78 +      | Const(@{const_name Int.number_of}, _) $ _ => meta_number_of_reorient)
    1.79 +
    1.80 +val reorient_simproc = 
    1.81 +  Arith_Data.prep_simproc ("reorient_simproc", ["0=x", "1=x", "number_of w = x"], reorient_proc);
    1.82 +
    1.83 +(*Maps 0 to Numeral0 and 1 to Numeral1 so that arithmetic isn't complicated by the abstract 0 and 1.*)
    1.84  val numeral_syms = [@{thm numeral_0_eq_0} RS sym, @{thm numeral_1_eq_1} RS sym];
    1.85  
    1.86  (** New term ordering so that AC-rewriting brings numerals to the front **)
    1.87 @@ -88,7 +61,7 @@
    1.88  
    1.89  fun numtermless tu = (numterm_ord tu = LESS);
    1.90  
    1.91 -(*Defined in this file, but perhaps needed only for Int_Numeral_Base_Simprocs of type nat.*)
    1.92 +(*Defined in this file, but perhaps needed only for Int_Numeral_Simprocs of type nat.*)
    1.93  val num_ss = HOL_ss settermless numtermless;
    1.94  
    1.95  
    1.96 @@ -213,7 +186,7 @@
    1.97  val divide_1s = [@{thm divide_numeral_1}];
    1.98  
    1.99  (*To perform binary arithmetic.  The "left" rewriting handles patterns
   1.100 -  created by the Int_Numeral_Base_Simprocs, such as 3 * (5 * x). *)
   1.101 +  created by the Int_Numeral_Simprocs, such as 3 * (5 * x). *)
   1.102  val simps = [@{thm numeral_0_eq_0} RS sym, @{thm numeral_1_eq_1} RS sym,
   1.103                   @{thm add_number_of_left}, @{thm mult_number_of_left}] @
   1.104                  @{thms arith_simps} @ @{thms rel_simps};
   1.105 @@ -279,7 +252,7 @@
   1.106  
   1.107  structure EqCancelNumerals = CancelNumeralsFun
   1.108   (open CancelNumeralsCommon
   1.109 -  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
   1.110 +  val prove_conv = Arith_Data.prove_conv
   1.111    val mk_bal   = HOLogic.mk_eq
   1.112    val dest_bal = HOLogic.dest_bin "op =" Term.dummyT
   1.113    val bal_add1 = @{thm eq_add_iff1} RS trans
   1.114 @@ -288,7 +261,7 @@
   1.115  
   1.116  structure LessCancelNumerals = CancelNumeralsFun
   1.117   (open CancelNumeralsCommon
   1.118 -  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
   1.119 +  val prove_conv = Arith_Data.prove_conv
   1.120    val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less}
   1.121    val dest_bal = HOLogic.dest_bin @{const_name HOL.less} Term.dummyT
   1.122    val bal_add1 = @{thm less_add_iff1} RS trans
   1.123 @@ -297,7 +270,7 @@
   1.124  
   1.125  structure LeCancelNumerals = CancelNumeralsFun
   1.126   (open CancelNumeralsCommon
   1.127 -  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
   1.128 +  val prove_conv = Arith_Data.prove_conv
   1.129    val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less_eq}
   1.130    val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} Term.dummyT
   1.131    val bal_add1 = @{thm le_add_iff1} RS trans
   1.132 @@ -305,7 +278,7 @@
   1.133  );
   1.134  
   1.135  val cancel_numerals =
   1.136 -  map Int_Numeral_Base_Simprocs.prep_simproc
   1.137 +  map Arith_Data.prep_simproc
   1.138     [("inteq_cancel_numerals",
   1.139       ["(l::'a::number_ring) + m = n",
   1.140        "(l::'a::number_ring) = m + n",
   1.141 @@ -342,7 +315,7 @@
   1.142    val mk_coeff          = mk_coeff
   1.143    val dest_coeff        = dest_coeff 1
   1.144    val left_distrib      = @{thm combine_common_factor} RS trans
   1.145 -  val prove_conv        = Int_Numeral_Base_Simprocs.prove_conv_nohyps
   1.146 +  val prove_conv        = Arith_Data.prove_conv_nohyps
   1.147    val trans_tac         = fn _ => trans_tac
   1.148  
   1.149    val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @
   1.150 @@ -372,7 +345,7 @@
   1.151    val mk_coeff          = mk_fcoeff
   1.152    val dest_coeff        = dest_fcoeff 1
   1.153    val left_distrib      = @{thm combine_common_factor} RS trans
   1.154 -  val prove_conv        = Int_Numeral_Base_Simprocs.prove_conv_nohyps
   1.155 +  val prove_conv        = Arith_Data.prove_conv_nohyps
   1.156    val trans_tac         = fn _ => trans_tac
   1.157  
   1.158    val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @
   1.159 @@ -392,23 +365,42 @@
   1.160  structure FieldCombineNumerals = CombineNumeralsFun(FieldCombineNumeralsData);
   1.161  
   1.162  val combine_numerals =
   1.163 -  Int_Numeral_Base_Simprocs.prep_simproc
   1.164 +  Arith_Data.prep_simproc
   1.165      ("int_combine_numerals", 
   1.166       ["(i::'a::number_ring) + j", "(i::'a::number_ring) - j"], 
   1.167       K CombineNumerals.proc);
   1.168  
   1.169  val field_combine_numerals =
   1.170 -  Int_Numeral_Base_Simprocs.prep_simproc
   1.171 +  Arith_Data.prep_simproc
   1.172      ("field_combine_numerals", 
   1.173       ["(i::'a::{number_ring,field,division_by_zero}) + j",
   1.174        "(i::'a::{number_ring,field,division_by_zero}) - j"], 
   1.175       K FieldCombineNumerals.proc);
   1.176  
   1.177 +(** Constant folding for multiplication in semirings **)
   1.178 +
   1.179 +(*We do not need folding for addition: combine_numerals does the same thing*)
   1.180 +
   1.181 +structure Semiring_Times_Assoc_Data : ASSOC_FOLD_DATA =
   1.182 +struct
   1.183 +  val assoc_ss = HOL_ss addsimps @{thms mult_ac}
   1.184 +  val eq_reflection = eq_reflection
   1.185  end;
   1.186  
   1.187 +structure Semiring_Times_Assoc = Assoc_Fold (Semiring_Times_Assoc_Data);
   1.188 +
   1.189 +val assoc_fold_simproc =
   1.190 +  Arith_Data.prep_simproc
   1.191 +   ("semiring_assoc_fold", ["(a::'a::comm_semiring_1_cancel) * b"],
   1.192 +    K Semiring_Times_Assoc.proc);
   1.193 +
   1.194 +end;
   1.195 +
   1.196 +Addsimprocs [Int_Numeral_Simprocs.reorient_simproc];
   1.197  Addsimprocs Int_Numeral_Simprocs.cancel_numerals;
   1.198  Addsimprocs [Int_Numeral_Simprocs.combine_numerals];
   1.199  Addsimprocs [Int_Numeral_Simprocs.field_combine_numerals];
   1.200 +Addsimprocs [Int_Numeral_Simprocs.assoc_fold_simproc];
   1.201  
   1.202  (*examples:
   1.203  print_depth 22;
   1.204 @@ -447,29 +439,6 @@
   1.205  test "(i + j + -12 + (k::int)) - -15 = y";
   1.206  *)
   1.207  
   1.208 -
   1.209 -(** Constant folding for multiplication in semirings **)
   1.210 -
   1.211 -(*We do not need folding for addition: combine_numerals does the same thing*)
   1.212 -
   1.213 -structure Semiring_Times_Assoc_Data : ASSOC_FOLD_DATA =
   1.214 -struct
   1.215 -  val assoc_ss = HOL_ss addsimps @{thms mult_ac}
   1.216 -  val eq_reflection = eq_reflection
   1.217 -end;
   1.218 -
   1.219 -structure Semiring_Times_Assoc = Assoc_Fold (Semiring_Times_Assoc_Data);
   1.220 -
   1.221 -val assoc_fold_simproc =
   1.222 -  Int_Numeral_Base_Simprocs.prep_simproc
   1.223 -   ("semiring_assoc_fold", ["(a::'a::comm_semiring_1_cancel) * b"],
   1.224 -    K Semiring_Times_Assoc.proc);
   1.225 -
   1.226 -Addsimprocs [assoc_fold_simproc];
   1.227 -
   1.228 -
   1.229 -
   1.230 -
   1.231  (*** decision procedure for linear arithmetic ***)
   1.232  
   1.233  (*---------------------------------------------------------------------------*)
   1.234 @@ -480,8 +449,10 @@
   1.235  Instantiation of the generic linear arithmetic package for int.
   1.236  *)
   1.237  
   1.238 +structure Int_Arith =
   1.239 +struct
   1.240 +
   1.241  (* Update parameters of arithmetic prover *)
   1.242 -local
   1.243  
   1.244  (* reduce contradictory =/</<= to False *)
   1.245  
   1.246 @@ -489,25 +460,31 @@
   1.247     and m and n are ground terms over rings (roughly speaking).
   1.248     That is, m and n consist only of 1s combined with "+", "-" and "*".
   1.249  *)
   1.250 -local
   1.251 +
   1.252  val zeroth = (symmetric o mk_meta_eq) @{thm of_int_0};
   1.253 +
   1.254  val lhss0 = [@{cpat "0::?'a::ring"}];
   1.255 +
   1.256  fun proc0 phi ss ct =
   1.257    let val T = ctyp_of_term ct
   1.258    in if typ_of T = @{typ int} then NONE else
   1.259       SOME (instantiate' [SOME T] [] zeroth)
   1.260    end;
   1.261 +
   1.262  val zero_to_of_int_zero_simproc =
   1.263    make_simproc {lhss = lhss0, name = "zero_to_of_int_zero_simproc",
   1.264    proc = proc0, identifier = []};
   1.265  
   1.266  val oneth = (symmetric o mk_meta_eq) @{thm of_int_1};
   1.267 +
   1.268  val lhss1 = [@{cpat "1::?'a::ring_1"}];
   1.269 +
   1.270  fun proc1 phi ss ct =
   1.271    let val T = ctyp_of_term ct
   1.272    in if typ_of T = @{typ int} then NONE else
   1.273       SOME (instantiate' [SOME T] [] oneth)
   1.274    end;
   1.275 +
   1.276  val one_to_of_int_one_simproc =
   1.277    make_simproc {lhss = lhss1, name = "one_to_of_int_one_simproc",
   1.278    proc = proc1, identifier = []};
   1.279 @@ -533,15 +510,15 @@
   1.280       addsimprocs [zero_to_of_int_zero_simproc,one_to_of_int_one_simproc]);
   1.281  
   1.282  fun sproc phi ss ct = if check (term_of ct) then SOME (conv ct) else NONE
   1.283 +
   1.284  val lhss' =
   1.285    [@{cpat "(?x::?'a::ring_char_0) = (?y::?'a)"},
   1.286     @{cpat "(?x::?'a::ordered_idom) < (?y::?'a)"},
   1.287     @{cpat "(?x::?'a::ordered_idom) <= (?y::?'a)"}]
   1.288 -in
   1.289 +
   1.290  val zero_one_idom_simproc =
   1.291    make_simproc {lhss = lhss' , name = "zero_one_idom_simproc",
   1.292    proc = sproc, identifier = []}
   1.293 -end;
   1.294  
   1.295  val add_rules =
   1.296      simp_thms @ @{thms arith_simps} @ @{thms rel_simps} @ @{thms arith_special} @
   1.297 @@ -556,13 +533,11 @@
   1.298  
   1.299  val nat_inj_thms = [@{thm zle_int} RS iffD2, @{thm int_int_eq} RS iffD2]
   1.300  
   1.301 -val Int_Numeral_Base_Simprocs = assoc_fold_simproc :: zero_one_idom_simproc
   1.302 +val int_numeral_base_simprocs = Int_Numeral_Simprocs.assoc_fold_simproc :: zero_one_idom_simproc
   1.303    :: Int_Numeral_Simprocs.combine_numerals
   1.304    :: Int_Numeral_Simprocs.cancel_numerals;
   1.305  
   1.306 -in
   1.307 -
   1.308 -val int_arith_setup =
   1.309 +val setup =
   1.310    LinArith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
   1.311     {add_mono_thms = add_mono_thms,
   1.312      mult_mono_thms = @{thm mult_strict_left_mono} :: @{thm mult_left_mono} :: mult_mono_thms,
   1.313 @@ -570,13 +545,11 @@
   1.314      lessD = lessD @ [@{thm zless_imp_add1_zle}],
   1.315      neqE = neqE,
   1.316      simpset = simpset addsimps add_rules
   1.317 -                      addsimprocs Int_Numeral_Base_Simprocs
   1.318 +                      addsimprocs int_numeral_base_simprocs
   1.319                        addcongs [if_weak_cong]}) #>
   1.320    arith_inj_const (@{const_name of_nat}, HOLogic.natT --> HOLogic.intT) #>
   1.321    arith_discrete @{type_name Int.int}
   1.322  
   1.323 -end;
   1.324 -
   1.325  val fast_int_arith_simproc =
   1.326    Simplifier.simproc (the_context ())
   1.327    "fast_int_arith" 
   1.328 @@ -584,4 +557,6 @@
   1.329        "(m::'a::{ordered_idom,number_ring}) <= n",
   1.330        "(m::'a::{ordered_idom,number_ring}) = n"] (K LinArith.lin_arith_simproc);
   1.331  
   1.332 -Addsimprocs [fast_int_arith_simproc];
   1.333 +end;
   1.334 +
   1.335 +Addsimprocs [Int_Arith.fast_int_arith_simproc];