src/HOL/arith_data.ML
changeset 26101 a657683e902a
parent 25484 4c98517601ce
child 28262 aa7ca36d67fd
     1.1 --- a/src/HOL/arith_data.ML	Wed Feb 20 14:52:34 2008 +0100
     1.2 +++ b/src/HOL/arith_data.ML	Wed Feb 20 14:52:38 2008 +0100
     1.3 @@ -5,16 +5,48 @@
     1.4  Basic arithmetic proof tools.
     1.5  *)
     1.6  
     1.7 -(*** cancellation of common terms ***)
     1.8 +signature ARITH_DATA =
     1.9 +sig
    1.10 +  val prove_conv: tactic -> (MetaSimplifier.simpset -> tactic)
    1.11 +    -> MetaSimplifier.simpset -> term * term -> thm
    1.12 +  val simp_all_tac: thm list -> MetaSimplifier.simpset -> tactic
    1.13 +
    1.14 +  val mk_sum: term list -> term
    1.15 +  val mk_norm_sum: term list -> term
    1.16 +  val dest_sum: term -> term list
    1.17 +
    1.18 +  val nat_cancel_sums_add: simproc list
    1.19 +  val nat_cancel_sums: simproc list
    1.20 +  val setup: Context.generic -> Context.generic
    1.21 +end;
    1.22  
    1.23 -structure NatArithUtils =
    1.24 +structure ArithData: ARITH_DATA =
    1.25  struct
    1.26  
    1.27 +(** generic proof tools **)
    1.28 +
    1.29 +(* prove conversions *)
    1.30 +
    1.31 +fun prove_conv expand_tac norm_tac ss tu =  (* FIXME avoid standard *)
    1.32 +  mk_meta_eq (standard (Goal.prove (Simplifier.the_context ss) [] []
    1.33 +      (HOLogic.mk_Trueprop (HOLogic.mk_eq tu))
    1.34 +    (K (EVERY [expand_tac, norm_tac ss]))));
    1.35 +
    1.36 +(* rewriting *)
    1.37 +
    1.38 +fun simp_all_tac rules =
    1.39 +  let val ss0 = HOL_ss addsimps rules
    1.40 +  in fn ss => ALLGOALS (simp_tac (Simplifier.inherit_context ss ss0)) end;
    1.41 +
    1.42 +
    1.43  (** abstract syntax of structure nat: 0, Suc, + **)
    1.44  
    1.45 -(* mk_sum, mk_norm_sum *)
    1.46 +local
    1.47  
    1.48  val mk_plus = HOLogic.mk_binop @{const_name HOL.plus};
    1.49 +val dest_plus = HOLogic.dest_bin @{const_name HOL.plus} HOLogic.natT;
    1.50 +
    1.51 +in
    1.52  
    1.53  fun mk_sum [] = HOLogic.zero
    1.54    | mk_sum [t] = t
    1.55 @@ -27,10 +59,6 @@
    1.56    end;
    1.57  
    1.58  
    1.59 -(* dest_sum *)
    1.60 -
    1.61 -val dest_plus = HOLogic.dest_bin @{const_name HOL.plus} HOLogic.natT;
    1.62 -
    1.63  fun dest_sum tm =
    1.64    if HOLogic.is_zero tm then []
    1.65    else
    1.66 @@ -41,46 +69,9 @@
    1.67            SOME (t, u) => dest_sum t @ dest_sum u
    1.68          | NONE => [tm]));
    1.69  
    1.70 -
    1.71 -
    1.72 -(** generic proof tools **)
    1.73 -
    1.74 -(* prove conversions *)
    1.75 -
    1.76 -fun prove_conv expand_tac norm_tac ss tu =  (* FIXME avoid standard *)
    1.77 -  mk_meta_eq (standard (Goal.prove (Simplifier.the_context ss) [] []
    1.78 -      (HOLogic.mk_Trueprop (HOLogic.mk_eq tu))
    1.79 -    (K (EVERY [expand_tac, norm_tac ss]))));
    1.80 -
    1.81 -
    1.82 -(* rewriting *)
    1.83 -
    1.84 -fun simp_all_tac rules =
    1.85 -  let val ss0 = HOL_ss addsimps rules
    1.86 -  in fn ss => ALLGOALS (simp_tac (Simplifier.inherit_context ss ss0)) end;
    1.87 -
    1.88 -fun prep_simproc (name, pats, proc) =
    1.89 -  Simplifier.simproc (the_context ()) name pats proc;
    1.90 -
    1.91  end;
    1.92  
    1.93  
    1.94 -
    1.95 -(** ArithData **)
    1.96 -
    1.97 -signature ARITH_DATA =
    1.98 -sig
    1.99 -  val nat_cancel_sums_add: simproc list
   1.100 -  val nat_cancel_sums: simproc list
   1.101 -  val arith_data_setup: Context.generic -> Context.generic
   1.102 -end;
   1.103 -
   1.104 -structure ArithData: ARITH_DATA =
   1.105 -struct
   1.106 -
   1.107 -open NatArithUtils;
   1.108 -
   1.109 -
   1.110  (** cancel common summands **)
   1.111  
   1.112  structure Sum =
   1.113 @@ -144,25 +135,23 @@
   1.114  
   1.115  (* prepare nat_cancel simprocs *)
   1.116  
   1.117 -val nat_cancel_sums_add = map prep_simproc
   1.118 -  [("nateq_cancel_sums",
   1.119 -     ["(l::nat) + m = n", "(l::nat) = m + n", "Suc m = n", "m = Suc n"],
   1.120 -     K EqCancelSums.proc),
   1.121 -   ("natless_cancel_sums",
   1.122 -     ["(l::nat) + m < n", "(l::nat) < m + n", "Suc m < n", "m < Suc n"],
   1.123 -     K LessCancelSums.proc),
   1.124 -   ("natle_cancel_sums",
   1.125 -     ["(l::nat) + m <= n", "(l::nat) <= m + n", "Suc m <= n", "m <= Suc n"],
   1.126 -     K LeCancelSums.proc)];
   1.127 +val nat_cancel_sums_add =
   1.128 +  [Simplifier.simproc @{theory} "nateq_cancel_sums"
   1.129 +     ["(l::nat) + m = n", "(l::nat) = m + n", "Suc m = n", "m = Suc n"]
   1.130 +     (K EqCancelSums.proc),
   1.131 +   Simplifier.simproc @{theory} "natless_cancel_sums"
   1.132 +     ["(l::nat) + m < n", "(l::nat) < m + n", "Suc m < n", "m < Suc n"]
   1.133 +     (K LessCancelSums.proc),
   1.134 +   Simplifier.simproc @{theory} "natle_cancel_sums"
   1.135 +     ["(l::nat) + m <= n", "(l::nat) <= m + n", "Suc m <= n", "m <= Suc n"]
   1.136 +     (K LeCancelSums.proc)];
   1.137  
   1.138  val nat_cancel_sums = nat_cancel_sums_add @
   1.139 -  [prep_simproc ("natdiff_cancel_sums",
   1.140 -    ["((l::nat) + m) - n", "(l::nat) - (m + n)", "Suc m - n", "m - Suc n"],
   1.141 -    K DiffCancelSums.proc)];
   1.142 +  [Simplifier.simproc @{theory} "natdiff_cancel_sums"
   1.143 +    ["((l::nat) + m) - n", "(l::nat) - (m + n)", "Suc m - n", "m - Suc n"]
   1.144 +    (K DiffCancelSums.proc)];
   1.145  
   1.146 -val arith_data_setup =
   1.147 +val setup =
   1.148    Simplifier.map_ss (fn ss => ss addsimprocs nat_cancel_sums);
   1.149  
   1.150  end;
   1.151 -
   1.152 -open ArithData;