--- a/src/HOL/Tools/lin_arith.ML Mon Nov 04 18:08:47 2013 +0100
+++ b/src/HOL/Tools/lin_arith.ML Mon Nov 04 20:10:06 2013 +0100
@@ -791,37 +791,16 @@
Most of the work is done by the cancel tactics. *)
val init_arith_data =
- Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, number_of, ...} =>
- {add_mono_thms = @{thms add_mono_thms_linordered_semiring} @
- @{thms add_mono_thms_linordered_field} @ add_mono_thms,
- mult_mono_thms = @{thm mult_strict_left_mono} :: @{thm mult_left_mono} ::
- @{lemma "a = b ==> c*a = c*b" by (rule arg_cong)} :: mult_mono_thms,
+ Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, number_of, ...} =>
+ {add_mono_thms = @{thms add_mono_thms_linordered_semiring}
+ @ @{thms add_mono_thms_linordered_field} @ add_mono_thms,
+ mult_mono_thms = @{thm mult_strict_left_mono} :: @{thm mult_left_mono}
+ :: @{lemma "a = b ==> c * a = c * b" by (rule arg_cong)} :: mult_mono_thms,
inj_thms = inj_thms,
- lessD = lessD @ [@{thm "Suc_leI"}],
- neqE = [@{thm linorder_neqE_nat}, @{thm linorder_neqE_linordered_idom}],
- simpset =
- put_simpset HOL_basic_ss @{context}
- addsimps @{thms ring_distribs}
- addsimps [@{thm if_True}, @{thm if_False}]
- addsimps
- [@{thm add_0_left}, @{thm add_0_right},
- @{thm add_Suc}, @{thm add_Suc_right},
- @{thm nat.inject}, @{thm Suc_le_mono}, @{thm Suc_less_eq},
- @{thm "Zero_not_Suc"}, @{thm "Suc_not_Zero"}, @{thm "le_0_eq"}, @{thm "One_nat_def"},
- @{thm "order_less_irrefl"}, @{thm "zero_neq_one"}, @{thm "zero_less_one"},
- @{thm "zero_le_one"}, @{thm "zero_neq_one"} RS not_sym, @{thm "not_one_le_zero"},
- @{thm "not_one_less_zero"}]
- addsimprocs [@{simproc group_cancel_add}, @{simproc group_cancel_diff},
- @{simproc group_cancel_eq}, @{simproc group_cancel_le},
- @{simproc group_cancel_less}]
- (*abel_cancel helps it work in abstract algebraic domains*)
- addsimprocs [@{simproc nateq_cancel_sums},
- @{simproc natless_cancel_sums},
- @{simproc natle_cancel_sums}]
- |> Simplifier.add_cong @{thm if_weak_cong}
- |> simpset_of,
- number_of = number_of}) #>
- add_discrete_type @{type_name nat};
+ lessD = lessD,
+ neqE = @{thm linorder_neqE_nat} :: @{thm linorder_neqE_linordered_idom} :: neqE,
+ simpset = put_simpset HOL_basic_ss @{context} |> Simplifier.add_cong @{thm if_weak_cong} |> simpset_of,
+ number_of = number_of});
(* FIXME !?? *)
fun add_arith_facts ctxt =
@@ -909,9 +888,6 @@
(* context setup *)
-val setup =
- init_arith_data;
-
val global_setup =
map_theory_simpset (fn ctxt => ctxt
addSolver (mk_solver "lin_arith" (add_arith_facts #> Fast_Arith.prems_lin_arith_tac))) #>
@@ -924,4 +900,22 @@
THEN' tac ctxt)))) "linear arithmetic" #>
Arith_Data.add_tactic "linear arithmetic" gen_tac;
+val setup =
+ init_arith_data
+ #> add_discrete_type @{type_name nat}
+ #> add_lessD @{thm Suc_leI}
+ #> add_simps (@{thms simp_thms} @ @{thms ring_distribs} @ [@{thm if_True}, @{thm if_False},
+ @{thm add_0_left}, @{thm add_0_right}, @{thm order_less_irrefl},
+ @{thm zero_neq_one}, @{thm zero_less_one}, @{thm zero_le_one},
+ @{thm zero_neq_one} RS not_sym, @{thm not_one_le_zero}, @{thm not_one_less_zero}])
+ #> add_simps [@{thm add_Suc}, @{thm add_Suc_right}, @{thm nat.inject},
+ @{thm Suc_le_mono}, @{thm Suc_less_eq}, @{thm Zero_not_Suc},
+ @{thm Suc_not_Zero}, @{thm le_0_eq}, @{thm One_nat_def}]
+ #> add_simprocs [@{simproc group_cancel_add}, @{simproc group_cancel_diff},
+ @{simproc group_cancel_eq}, @{simproc group_cancel_le},
+ @{simproc group_cancel_less}]
+ (*abel_cancel helps it work in abstract algebraic domains*)
+ #> add_simprocs [@{simproc nateq_cancel_sums},@{simproc natless_cancel_sums},
+ @{simproc natle_cancel_sums}];
+
end;