--- a/src/HOL/Complex/ex/linrtac.ML Fri Feb 15 23:22:02 2008 +0100
+++ b/src/HOL/Complex/ex/linrtac.ML Sat Feb 16 02:01:13 2008 +0100
@@ -4,46 +4,41 @@
val trace = ref false;
fun trace_msg s = if !trace then tracing s else ();
-val ferrack_ss = let val ths = map thm ["real_of_int_inject", "real_of_int_less_iff",
- "real_of_int_le_iff"]
+val ferrack_ss = let val ths = [@{thm real_of_int_inject}, @{thm real_of_int_less_iff},
+ @{thm real_of_int_le_iff}]
in @{simpset} delsimps ths addsimps (map (fn th => th RS sym) ths)
end;
val nT = HOLogic.natT;
-val binarith = map thm
- ["Pls_0_eq", "Min_1_eq",
- "pred_Pls","pred_Min","pred_1","pred_0",
- "succ_Pls", "succ_Min", "succ_1", "succ_0",
- "add_Pls", "add_Min", "add_BIT_0", "add_BIT_10",
- "add_BIT_11", "minus_Pls", "minus_Min", "minus_1",
- "minus_0", "mult_Pls", "mult_Min", "mult_num1", "mult_num0",
- "add_Pls_right", "add_Min_right"];
+val binarith =
+ @{thms normalize_bin_simps} @ @{thms pred_bin_simps} @ @{thms succ_bin_simps} @
+ @{thms add_bin_simps} @ @{thms minus_bin_simps} @ @{thms mult_bin_simps};
val comp_arith = binarith @ simp_thms
-val zdvd_int = thm "zdvd_int";
-val zdiff_int_split = thm "zdiff_int_split";
-val all_nat = thm "all_nat";
-val ex_nat = thm "ex_nat";
-val number_of1 = thm "number_of1";
-val number_of2 = thm "number_of2";
-val split_zdiv = thm "split_zdiv";
-val split_zmod = thm "split_zmod";
-val mod_div_equality' = thm "mod_div_equality'";
-val split_div' = thm "split_div'";
-val Suc_plus1 = thm "Suc_plus1";
-val imp_le_cong = thm "imp_le_cong";
-val conj_le_cong = thm "conj_le_cong";
+val zdvd_int = @{thm zdvd_int};
+val zdiff_int_split = @{thm zdiff_int_split};
+val all_nat = @{thm all_nat};
+val ex_nat = @{thm ex_nat};
+val number_of1 = @{thm number_of1};
+val number_of2 = @{thm number_of2};
+val split_zdiv = @{thm split_zdiv};
+val split_zmod = @{thm split_zmod};
+val mod_div_equality' = @{thm mod_div_equality'};
+val split_div' = @{thm split_div'};
+val Suc_plus1 = @{thm Suc_plus1};
+val imp_le_cong = @{thm imp_le_cong};
+val conj_le_cong = @{thm conj_le_cong};
val nat_mod_add_eq = @{thm mod_add1_eq} RS sym;
val nat_mod_add_left_eq = @{thm mod_add_left_eq} RS sym;
val nat_mod_add_right_eq = @{thm mod_add_right_eq} RS sym;
-val int_mod_add_eq = @{thm "zmod_zadd1_eq"} RS sym;
-val int_mod_add_left_eq = @{thm "zmod_zadd_left_eq"} RS sym;
-val int_mod_add_right_eq = @{thm "zmod_zadd_right_eq"} RS sym;
-val nat_div_add_eq = @{thm "div_add1_eq"} RS sym;
-val int_div_add_eq = @{thm "zdiv_zadd1_eq"} RS sym;
-val ZDIVISION_BY_ZERO_MOD = @{thm "DIVISION_BY_ZERO"} RS conjunct2;
-val ZDIVISION_BY_ZERO_DIV = @{thm "DIVISION_BY_ZERO"} RS conjunct1;
+val int_mod_add_eq = @{thm zmod_zadd1_eq} RS sym;
+val int_mod_add_left_eq = @{thm zmod_zadd_left_eq} RS sym;
+val int_mod_add_right_eq = @{thm zmod_zadd_right_eq} RS sym;
+val nat_div_add_eq = @{thm div_add1_eq} RS sym;
+val int_div_add_eq = @{thm zdiv_zadd1_eq} RS sym;
+val ZDIVISION_BY_ZERO_MOD = @{thm DIVISION_BY_ZERO} RS conjunct2;
+val ZDIVISION_BY_ZERO_DIV = @{thm DIVISION_BY_ZERO} RS conjunct1;
fun prepare_for_linr sg q fm =
let
@@ -74,7 +69,7 @@
fun linr_tac ctxt q i =
(ObjectLogic.atomize_prems_tac i)
- THEN (REPEAT_DETERM (split_tac [@{thm "split_min"}, @{thm "split_max"}, @{thm "abs_split"}] i))
+ THEN (REPEAT_DETERM (split_tac [@{thm split_min}, @{thm split_max}, @{thm abs_split}] i))
THEN (fn st =>
let
val g = List.nth (prems_of st, i - 1)
--- a/src/HOL/Int.thy Fri Feb 15 23:22:02 2008 +0100
+++ b/src/HOL/Int.thy Sat Feb 16 02:01:13 2008 +0100
@@ -652,6 +652,9 @@
"Min BIT B1 = Min"
unfolding numeral_simps by simp
+lemmas normalize_bin_simps =
+ Pls_0_eq Min_1_eq
+
subsection {* The Functions @{term succ}, @{term pred} and @{term uminus} *}
@@ -671,6 +674,9 @@
"succ (k BIT B0) = k BIT B1"
unfolding numeral_simps by simp
+lemmas succ_bin_simps =
+ succ_Pls succ_Min succ_1 succ_0
+
lemma pred_Pls [simp]:
"pred Pls = Min"
unfolding numeral_simps by simp
@@ -687,6 +693,9 @@
"pred (k BIT B0) = pred k BIT B1"
unfolding numeral_simps by simp
+lemmas pred_bin_simps =
+ pred_Pls pred_Min pred_1 pred_0
+
lemma minus_Pls [simp]:
"- Pls = Pls"
unfolding numeral_simps by simp
@@ -703,6 +712,9 @@
"- (k BIT B0) = (- k) BIT B0"
unfolding numeral_simps by simp
+lemmas minus_bin_simps =
+ minus_Pls minus_Min minus_1 minus_0
+
subsection {*
Binary Addition and Multiplication: @{term "op + \<Colon> int \<Rightarrow> int \<Rightarrow> int"}
@@ -737,6 +749,10 @@
"k + Min = pred k"
unfolding numeral_simps by simp
+lemmas add_bin_simps =
+ add_Pls add_Min add_BIT_0 add_BIT_10 add_BIT_11
+ add_Pls_right add_Min_right
+
lemma mult_Pls [simp]:
"Pls * w = Pls"
unfolding numeral_simps by simp
@@ -753,6 +769,9 @@
"(k BIT B0) * l = (k * l) BIT B0"
unfolding numeral_simps int_distrib by simp
+lemmas mult_bin_simps =
+ mult_Pls mult_Min mult_num1 mult_num0
+
subsection {* Converting Numerals to Rings: @{term number_of} *}
@@ -1094,13 +1113,8 @@
lemmas arith_simps =
bit.distinct
- Pls_0_eq Min_1_eq
- pred_Pls pred_Min pred_1 pred_0
- succ_Pls succ_Min succ_1 succ_0
- add_Pls add_Min add_BIT_0 add_BIT_10 add_BIT_11
- minus_Pls minus_Min minus_1 minus_0
- mult_Pls mult_Min mult_num1 mult_num0
- add_Pls_right add_Min_right
+ normalize_bin_simps pred_bin_simps succ_bin_simps
+ add_bin_simps minus_bin_simps mult_bin_simps
abs_zero abs_one arith_extra_simps
text {* Simplification of relational operations *}
--- a/src/HOL/Presburger.thy Fri Feb 15 23:22:02 2008 +0100
+++ b/src/HOL/Presburger.thy Sat Feb 16 02:01:13 2008 +0100
@@ -671,20 +671,19 @@
unfolding number_of_is_id ..
lemmas pred_succ_numeral_code [code func] =
- arith_simps(5-12)
+ pred_bin_simps succ_bin_simps
lemmas plus_numeral_code [code func] =
- arith_simps(13-17)
- arith_simps(26-27)
+ add_bin_simps
arith_extra_simps(1) [where 'a = int]
lemmas minus_numeral_code [code func] =
- arith_simps(18-21)
+ minus_bin_simps
arith_extra_simps(2) [where 'a = int]
arith_extra_simps(5) [where 'a = int]
lemmas times_numeral_code [code func] =
- arith_simps(22-25)
+ mult_bin_simps
arith_extra_simps(4) [where 'a = int]
lemmas eq_numeral_code [code func] =
--- a/src/HOL/Tools/ComputeNumeral.thy Fri Feb 15 23:22:02 2008 +0100
+++ b/src/HOL/Tools/ComputeNumeral.thy Sat Feb 16 02:01:13 2008 +0100
@@ -3,7 +3,7 @@
begin
(* normalization of bit strings *)
-lemmas bitnorm = Pls_0_eq Min_1_eq
+lemmas bitnorm = normalize_bin_simps
(* neg for bit strings *)
lemma neg1: "neg Int.Pls = False" by (simp add: Int.Pls_def)
@@ -88,13 +88,13 @@
bitle9 bitle10 bitle11 bitle12 bitle13 bitle14 bitle15 bitle16
(* succ for bit strings *)
-lemmas bitsucc = succ_Pls succ_Min succ_1 succ_0
+lemmas bitsucc = succ_bin_simps
(* pred for bit strings *)
-lemmas bitpred = pred_Pls pred_Min pred_1 pred_0
+lemmas bitpred = pred_bin_simps
(* unary minus for bit strings *)
-lemmas bituminus = minus_Pls minus_Min minus_1 minus_0
+lemmas bituminus = minus_bin_simps
(* addition for bit strings *)
lemmas bitadd = add_Pls add_Pls_right add_Min add_Min_right add_BIT_11 add_BIT_10 add_BIT_0[where b="Int.B0"] add_BIT_0[where b="Int.B1"]
--- a/src/HOL/ex/coopertac.ML Fri Feb 15 23:22:02 2008 +0100
+++ b/src/HOL/ex/coopertac.ML Sat Feb 16 02:01:13 2008 +0100
@@ -7,8 +7,7 @@
val cooper_ss = @{simpset};
val nT = HOLogic.natT;
-val binarith = map thm
- ["Pls_0_eq", "Min_1_eq"];
+val binarith = @{thms normalize_bin_simps};
val comp_arith = binarith @ simp_thms
val zdvd_int = thm "zdvd_int";
--- a/src/HOL/int_arith1.ML Fri Feb 15 23:22:02 2008 +0100
+++ b/src/HOL/int_arith1.ML Sat Feb 16 02:01:13 2008 +0100
@@ -225,9 +225,8 @@
subtract Thm.eq_thm [@{thm add_number_of_left}, @{thm number_of_add} RS sym] simps;
(*To evaluate binary negations of coefficients*)
-val minus_simps = [@{thm numeral_m1_eq_minus_1} RS sym, @{thm number_of_minus} RS sym,
- @{thm minus_1}, @{thm minus_0}, @{thm minus_Pls}, @{thm minus_Min},
- @{thm pred_1}, @{thm pred_0}, @{thm pred_Pls}, @{thm pred_Min}];
+val minus_simps = [@{thm numeral_m1_eq_minus_1} RS sym, @{thm number_of_minus} RS sym] @
+ @{thms minus_bin_simps} @ @{thms pred_bin_simps};
(*To let us treat subtraction as addition*)
val diff_simps = [@{thm diff_minus}, @{thm minus_add_distrib}, @{thm minus_minus}];