tuned structures in arith_data.ML
authorhaftmann
Wed Feb 20 14:52:38 2008 +0100 (2008-02-20)
changeset 26101a657683e902a
parent 26100 fbc60cd02ae2
child 26102 2ae572207783
tuned structures in arith_data.ML
src/HOL/IntDiv.thy
src/HOL/Nat.thy
src/HOL/Tools/lin_arith.ML
src/HOL/arith_data.ML
     1.1 --- a/src/HOL/IntDiv.thy	Wed Feb 20 14:52:34 2008 +0100
     1.2 +++ b/src/HOL/IntDiv.thy	Wed Feb 20 14:52:38 2008 +0100
     1.3 @@ -274,13 +274,13 @@
     1.4    val prove_eq_sums =
     1.5      let
     1.6        val simps = @{thm diff_int_def} :: Int_Numeral_Simprocs.add_0s @ @{thms zadd_ac}
     1.7 -    in NatArithUtils.prove_conv all_tac (NatArithUtils.simp_all_tac simps) end;
     1.8 +    in ArithData.prove_conv all_tac (ArithData.simp_all_tac simps) end;
     1.9  end)
    1.10  
    1.11  in
    1.12  
    1.13 -val cancel_zdiv_zmod_proc = NatArithUtils.prep_simproc
    1.14 -  ("cancel_zdiv_zmod", ["(m::int) + n"], K CancelDivMod.proc)
    1.15 +val cancel_zdiv_zmod_proc = Simplifier.simproc @{theory}
    1.16 +  "cancel_zdiv_zmod" ["(m::int) + n"] (K CancelDivMod.proc)
    1.17  
    1.18  end;
    1.19  
     2.1 --- a/src/HOL/Nat.thy	Wed Feb 20 14:52:34 2008 +0100
     2.2 +++ b/src/HOL/Nat.thy	Wed Feb 20 14:52:38 2008 +0100
     2.3 @@ -1199,7 +1199,7 @@
     2.4    using 2 1 by (rule trans)
     2.5  
     2.6  use "arith_data.ML"
     2.7 -declaration {* K arith_data_setup *}
     2.8 +declaration {* K ArithData.setup *}
     2.9  
    2.10  use "Tools/lin_arith.ML"
    2.11  declaration {* K LinArith.setup *}
     3.1 --- a/src/HOL/Tools/lin_arith.ML	Wed Feb 20 14:52:34 2008 +0100
     3.2 +++ b/src/HOL/Tools/lin_arith.ML	Wed Feb 20 14:52:38 2008 +0100
     3.3 @@ -810,7 +810,7 @@
     3.4          @{thm "not_one_less_zero"}]
     3.5        addsimprocs [ab_group_add_cancel.sum_conv, ab_group_add_cancel.rel_conv]
     3.6         (*abel_cancel helps it work in abstract algebraic domains*)
     3.7 -      addsimprocs nat_cancel_sums_add}) #>
     3.8 +      addsimprocs ArithData.nat_cancel_sums_add}) #>
     3.9    arith_discrete "nat";
    3.10  
    3.11  val lin_arith_simproc = Fast_Arith.lin_arith_simproc;
     4.1 --- a/src/HOL/arith_data.ML	Wed Feb 20 14:52:34 2008 +0100
     4.2 +++ b/src/HOL/arith_data.ML	Wed Feb 20 14:52:38 2008 +0100
     4.3 @@ -5,16 +5,48 @@
     4.4  Basic arithmetic proof tools.
     4.5  *)
     4.6  
     4.7 -(*** cancellation of common terms ***)
     4.8 +signature ARITH_DATA =
     4.9 +sig
    4.10 +  val prove_conv: tactic -> (MetaSimplifier.simpset -> tactic)
    4.11 +    -> MetaSimplifier.simpset -> term * term -> thm
    4.12 +  val simp_all_tac: thm list -> MetaSimplifier.simpset -> tactic
    4.13 +
    4.14 +  val mk_sum: term list -> term
    4.15 +  val mk_norm_sum: term list -> term
    4.16 +  val dest_sum: term -> term list
    4.17 +
    4.18 +  val nat_cancel_sums_add: simproc list
    4.19 +  val nat_cancel_sums: simproc list
    4.20 +  val setup: Context.generic -> Context.generic
    4.21 +end;
    4.22  
    4.23 -structure NatArithUtils =
    4.24 +structure ArithData: ARITH_DATA =
    4.25  struct
    4.26  
    4.27 +(** generic proof tools **)
    4.28 +
    4.29 +(* prove conversions *)
    4.30 +
    4.31 +fun prove_conv expand_tac norm_tac ss tu =  (* FIXME avoid standard *)
    4.32 +  mk_meta_eq (standard (Goal.prove (Simplifier.the_context ss) [] []
    4.33 +      (HOLogic.mk_Trueprop (HOLogic.mk_eq tu))
    4.34 +    (K (EVERY [expand_tac, norm_tac ss]))));
    4.35 +
    4.36 +(* rewriting *)
    4.37 +
    4.38 +fun simp_all_tac rules =
    4.39 +  let val ss0 = HOL_ss addsimps rules
    4.40 +  in fn ss => ALLGOALS (simp_tac (Simplifier.inherit_context ss ss0)) end;
    4.41 +
    4.42 +
    4.43  (** abstract syntax of structure nat: 0, Suc, + **)
    4.44  
    4.45 -(* mk_sum, mk_norm_sum *)
    4.46 +local
    4.47  
    4.48  val mk_plus = HOLogic.mk_binop @{const_name HOL.plus};
    4.49 +val dest_plus = HOLogic.dest_bin @{const_name HOL.plus} HOLogic.natT;
    4.50 +
    4.51 +in
    4.52  
    4.53  fun mk_sum [] = HOLogic.zero
    4.54    | mk_sum [t] = t
    4.55 @@ -27,10 +59,6 @@
    4.56    end;
    4.57  
    4.58  
    4.59 -(* dest_sum *)
    4.60 -
    4.61 -val dest_plus = HOLogic.dest_bin @{const_name HOL.plus} HOLogic.natT;
    4.62 -
    4.63  fun dest_sum tm =
    4.64    if HOLogic.is_zero tm then []
    4.65    else
    4.66 @@ -41,46 +69,9 @@
    4.67            SOME (t, u) => dest_sum t @ dest_sum u
    4.68          | NONE => [tm]));
    4.69  
    4.70 -
    4.71 -
    4.72 -(** generic proof tools **)
    4.73 -
    4.74 -(* prove conversions *)
    4.75 -
    4.76 -fun prove_conv expand_tac norm_tac ss tu =  (* FIXME avoid standard *)
    4.77 -  mk_meta_eq (standard (Goal.prove (Simplifier.the_context ss) [] []
    4.78 -      (HOLogic.mk_Trueprop (HOLogic.mk_eq tu))
    4.79 -    (K (EVERY [expand_tac, norm_tac ss]))));
    4.80 -
    4.81 -
    4.82 -(* rewriting *)
    4.83 -
    4.84 -fun simp_all_tac rules =
    4.85 -  let val ss0 = HOL_ss addsimps rules
    4.86 -  in fn ss => ALLGOALS (simp_tac (Simplifier.inherit_context ss ss0)) end;
    4.87 -
    4.88 -fun prep_simproc (name, pats, proc) =
    4.89 -  Simplifier.simproc (the_context ()) name pats proc;
    4.90 -
    4.91  end;
    4.92  
    4.93  
    4.94 -
    4.95 -(** ArithData **)
    4.96 -
    4.97 -signature ARITH_DATA =
    4.98 -sig
    4.99 -  val nat_cancel_sums_add: simproc list
   4.100 -  val nat_cancel_sums: simproc list
   4.101 -  val arith_data_setup: Context.generic -> Context.generic
   4.102 -end;
   4.103 -
   4.104 -structure ArithData: ARITH_DATA =
   4.105 -struct
   4.106 -
   4.107 -open NatArithUtils;
   4.108 -
   4.109 -
   4.110  (** cancel common summands **)
   4.111  
   4.112  structure Sum =
   4.113 @@ -144,25 +135,23 @@
   4.114  
   4.115  (* prepare nat_cancel simprocs *)
   4.116  
   4.117 -val nat_cancel_sums_add = map prep_simproc
   4.118 -  [("nateq_cancel_sums",
   4.119 -     ["(l::nat) + m = n", "(l::nat) = m + n", "Suc m = n", "m = Suc n"],
   4.120 -     K EqCancelSums.proc),
   4.121 -   ("natless_cancel_sums",
   4.122 -     ["(l::nat) + m < n", "(l::nat) < m + n", "Suc m < n", "m < Suc n"],
   4.123 -     K LessCancelSums.proc),
   4.124 -   ("natle_cancel_sums",
   4.125 -     ["(l::nat) + m <= n", "(l::nat) <= m + n", "Suc m <= n", "m <= Suc n"],
   4.126 -     K LeCancelSums.proc)];
   4.127 +val nat_cancel_sums_add =
   4.128 +  [Simplifier.simproc @{theory} "nateq_cancel_sums"
   4.129 +     ["(l::nat) + m = n", "(l::nat) = m + n", "Suc m = n", "m = Suc n"]
   4.130 +     (K EqCancelSums.proc),
   4.131 +   Simplifier.simproc @{theory} "natless_cancel_sums"
   4.132 +     ["(l::nat) + m < n", "(l::nat) < m + n", "Suc m < n", "m < Suc n"]
   4.133 +     (K LessCancelSums.proc),
   4.134 +   Simplifier.simproc @{theory} "natle_cancel_sums"
   4.135 +     ["(l::nat) + m <= n", "(l::nat) <= m + n", "Suc m <= n", "m <= Suc n"]
   4.136 +     (K LeCancelSums.proc)];
   4.137  
   4.138  val nat_cancel_sums = nat_cancel_sums_add @
   4.139 -  [prep_simproc ("natdiff_cancel_sums",
   4.140 -    ["((l::nat) + m) - n", "(l::nat) - (m + n)", "Suc m - n", "m - Suc n"],
   4.141 -    K DiffCancelSums.proc)];
   4.142 +  [Simplifier.simproc @{theory} "natdiff_cancel_sums"
   4.143 +    ["((l::nat) + m) - n", "(l::nat) - (m + n)", "Suc m - n", "m - Suc n"]
   4.144 +    (K DiffCancelSums.proc)];
   4.145  
   4.146 -val arith_data_setup =
   4.147 +val setup =
   4.148    Simplifier.map_ss (fn ss => ss addsimprocs nat_cancel_sums);
   4.149  
   4.150  end;
   4.151 -
   4.152 -open ArithData;