# HG changeset patch # User huffman # Date 1203123673 -3600 # Node ID 815f3ccc0b454ea6985b4cace9ca15da4eecd805 # Parent 44c5419cd9f1a437c19303f0fd0984e30b88a53e added lemma lists {normalize,succ,pred,minus,add,mult}_bin_simps diff -r 44c5419cd9f1 -r 815f3ccc0b45 src/HOL/Complex/ex/linrtac.ML --- 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) diff -r 44c5419cd9f1 -r 815f3ccc0b45 src/HOL/Int.thy --- 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 + \ int \ int \ 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 *} diff -r 44c5419cd9f1 -r 815f3ccc0b45 src/HOL/Presburger.thy --- 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] = diff -r 44c5419cd9f1 -r 815f3ccc0b45 src/HOL/Tools/ComputeNumeral.thy --- 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"] diff -r 44c5419cd9f1 -r 815f3ccc0b45 src/HOL/ex/coopertac.ML --- 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"; diff -r 44c5419cd9f1 -r 815f3ccc0b45 src/HOL/int_arith1.ML --- 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}];