added lemma lists {normalize,succ,pred,minus,add,mult}_bin_simps
authorhuffman
Sat Feb 16 02:01:13 2008 +0100 (2008-02-16)
changeset 26075815f3ccc0b45
parent 26074 44c5419cd9f1
child 26076 b9c716a9fb5f
added lemma lists {normalize,succ,pred,minus,add,mult}_bin_simps
src/HOL/Complex/ex/linrtac.ML
src/HOL/Int.thy
src/HOL/Presburger.thy
src/HOL/Tools/ComputeNumeral.thy
src/HOL/ex/coopertac.ML
src/HOL/int_arith1.ML
     1.1 --- a/src/HOL/Complex/ex/linrtac.ML	Fri Feb 15 23:22:02 2008 +0100
     1.2 +++ b/src/HOL/Complex/ex/linrtac.ML	Sat Feb 16 02:01:13 2008 +0100
     1.3 @@ -4,46 +4,41 @@
     1.4  val trace = ref false;
     1.5  fun trace_msg s = if !trace then tracing s else ();
     1.6  
     1.7 -val ferrack_ss = let val ths = map thm ["real_of_int_inject", "real_of_int_less_iff", 
     1.8 -				"real_of_int_le_iff"]
     1.9 +val ferrack_ss = let val ths = [@{thm real_of_int_inject}, @{thm real_of_int_less_iff}, 
    1.10 +				@{thm real_of_int_le_iff}]
    1.11  	     in @{simpset} delsimps ths addsimps (map (fn th => th RS sym) ths)
    1.12  	     end;
    1.13  
    1.14  val nT = HOLogic.natT;
    1.15 -val binarith = map thm
    1.16 -  ["Pls_0_eq", "Min_1_eq",
    1.17 - "pred_Pls","pred_Min","pred_1","pred_0",
    1.18 -  "succ_Pls", "succ_Min", "succ_1", "succ_0",
    1.19 -  "add_Pls", "add_Min", "add_BIT_0", "add_BIT_10",
    1.20 -  "add_BIT_11", "minus_Pls", "minus_Min", "minus_1", 
    1.21 -  "minus_0", "mult_Pls", "mult_Min", "mult_num1", "mult_num0", 
    1.22 -  "add_Pls_right", "add_Min_right"];
    1.23 +val binarith =
    1.24 +  @{thms normalize_bin_simps} @ @{thms pred_bin_simps} @ @{thms succ_bin_simps} @
    1.25 +  @{thms add_bin_simps} @ @{thms minus_bin_simps} @  @{thms mult_bin_simps};
    1.26  val comp_arith = binarith @ simp_thms
    1.27  
    1.28  
    1.29 -val zdvd_int = thm "zdvd_int";
    1.30 -val zdiff_int_split = thm "zdiff_int_split";
    1.31 -val all_nat = thm "all_nat";
    1.32 -val ex_nat = thm "ex_nat";
    1.33 -val number_of1 = thm "number_of1";
    1.34 -val number_of2 = thm "number_of2";
    1.35 -val split_zdiv = thm "split_zdiv";
    1.36 -val split_zmod = thm "split_zmod";
    1.37 -val mod_div_equality' = thm "mod_div_equality'";
    1.38 -val split_div' = thm "split_div'";
    1.39 -val Suc_plus1 = thm "Suc_plus1";
    1.40 -val imp_le_cong = thm "imp_le_cong";
    1.41 -val conj_le_cong = thm "conj_le_cong";
    1.42 +val zdvd_int = @{thm zdvd_int};
    1.43 +val zdiff_int_split = @{thm zdiff_int_split};
    1.44 +val all_nat = @{thm all_nat};
    1.45 +val ex_nat = @{thm ex_nat};
    1.46 +val number_of1 = @{thm number_of1};
    1.47 +val number_of2 = @{thm number_of2};
    1.48 +val split_zdiv = @{thm split_zdiv};
    1.49 +val split_zmod = @{thm split_zmod};
    1.50 +val mod_div_equality' = @{thm mod_div_equality'};
    1.51 +val split_div' = @{thm split_div'};
    1.52 +val Suc_plus1 = @{thm Suc_plus1};
    1.53 +val imp_le_cong = @{thm imp_le_cong};
    1.54 +val conj_le_cong = @{thm conj_le_cong};
    1.55  val nat_mod_add_eq = @{thm mod_add1_eq} RS sym;
    1.56  val nat_mod_add_left_eq = @{thm mod_add_left_eq} RS sym;
    1.57  val nat_mod_add_right_eq = @{thm mod_add_right_eq} RS sym;
    1.58 -val int_mod_add_eq = @{thm "zmod_zadd1_eq"} RS sym;
    1.59 -val int_mod_add_left_eq = @{thm "zmod_zadd_left_eq"} RS sym;
    1.60 -val int_mod_add_right_eq = @{thm "zmod_zadd_right_eq"} RS sym;
    1.61 -val nat_div_add_eq = @{thm "div_add1_eq"} RS sym;
    1.62 -val int_div_add_eq = @{thm "zdiv_zadd1_eq"} RS sym;
    1.63 -val ZDIVISION_BY_ZERO_MOD = @{thm "DIVISION_BY_ZERO"} RS conjunct2;
    1.64 -val ZDIVISION_BY_ZERO_DIV = @{thm "DIVISION_BY_ZERO"} RS conjunct1;
    1.65 +val int_mod_add_eq = @{thm zmod_zadd1_eq} RS sym;
    1.66 +val int_mod_add_left_eq = @{thm zmod_zadd_left_eq} RS sym;
    1.67 +val int_mod_add_right_eq = @{thm zmod_zadd_right_eq} RS sym;
    1.68 +val nat_div_add_eq = @{thm div_add1_eq} RS sym;
    1.69 +val int_div_add_eq = @{thm zdiv_zadd1_eq} RS sym;
    1.70 +val ZDIVISION_BY_ZERO_MOD = @{thm DIVISION_BY_ZERO} RS conjunct2;
    1.71 +val ZDIVISION_BY_ZERO_DIV = @{thm DIVISION_BY_ZERO} RS conjunct1;
    1.72  
    1.73  fun prepare_for_linr sg q fm = 
    1.74    let
    1.75 @@ -74,7 +69,7 @@
    1.76  
    1.77  fun linr_tac ctxt q i = 
    1.78      (ObjectLogic.atomize_prems_tac i) 
    1.79 -	THEN (REPEAT_DETERM (split_tac [@{thm "split_min"}, @{thm "split_max"}, @{thm "abs_split"}] i))
    1.80 +	THEN (REPEAT_DETERM (split_tac [@{thm split_min}, @{thm split_max}, @{thm abs_split}] i))
    1.81  	THEN (fn st =>
    1.82    let
    1.83      val g = List.nth (prems_of st, i - 1)
     2.1 --- a/src/HOL/Int.thy	Fri Feb 15 23:22:02 2008 +0100
     2.2 +++ b/src/HOL/Int.thy	Sat Feb 16 02:01:13 2008 +0100
     2.3 @@ -652,6 +652,9 @@
     2.4    "Min BIT B1 = Min"
     2.5    unfolding numeral_simps by simp
     2.6  
     2.7 +lemmas normalize_bin_simps =
     2.8 +  Pls_0_eq Min_1_eq
     2.9 +
    2.10  
    2.11  subsection {* The Functions @{term succ}, @{term pred} and @{term uminus} *}
    2.12  
    2.13 @@ -671,6 +674,9 @@
    2.14    "succ (k BIT B0) = k BIT B1"
    2.15    unfolding numeral_simps by simp
    2.16  
    2.17 +lemmas succ_bin_simps =
    2.18 +  succ_Pls succ_Min succ_1 succ_0
    2.19 +
    2.20  lemma pred_Pls [simp]:
    2.21    "pred Pls = Min"
    2.22    unfolding numeral_simps by simp
    2.23 @@ -687,6 +693,9 @@
    2.24    "pred (k BIT B0) = pred k BIT B1"
    2.25    unfolding numeral_simps by simp 
    2.26  
    2.27 +lemmas pred_bin_simps =
    2.28 +  pred_Pls pred_Min pred_1 pred_0
    2.29 +
    2.30  lemma minus_Pls [simp]:
    2.31    "- Pls = Pls"
    2.32    unfolding numeral_simps by simp 
    2.33 @@ -703,6 +712,9 @@
    2.34    "- (k BIT B0) = (- k) BIT B0"
    2.35    unfolding numeral_simps by simp 
    2.36  
    2.37 +lemmas minus_bin_simps =
    2.38 +  minus_Pls minus_Min minus_1 minus_0
    2.39 +
    2.40  
    2.41  subsection {*
    2.42    Binary Addition and Multiplication: @{term "op + \<Colon> int \<Rightarrow> int \<Rightarrow> int"}
    2.43 @@ -737,6 +749,10 @@
    2.44    "k + Min = pred k"
    2.45    unfolding numeral_simps by simp 
    2.46  
    2.47 +lemmas add_bin_simps =
    2.48 +  add_Pls add_Min add_BIT_0 add_BIT_10 add_BIT_11
    2.49 +  add_Pls_right add_Min_right
    2.50 +
    2.51  lemma mult_Pls [simp]:
    2.52    "Pls * w = Pls"
    2.53    unfolding numeral_simps by simp 
    2.54 @@ -753,6 +769,9 @@
    2.55    "(k BIT B0) * l = (k * l) BIT B0"
    2.56    unfolding numeral_simps int_distrib by simp 
    2.57  
    2.58 +lemmas mult_bin_simps =
    2.59 +  mult_Pls mult_Min mult_num1 mult_num0 
    2.60 +
    2.61  
    2.62  subsection {* Converting Numerals to Rings: @{term number_of} *}
    2.63  
    2.64 @@ -1094,13 +1113,8 @@
    2.65  
    2.66  lemmas arith_simps = 
    2.67    bit.distinct
    2.68 -  Pls_0_eq Min_1_eq
    2.69 -  pred_Pls pred_Min pred_1 pred_0
    2.70 -  succ_Pls succ_Min succ_1 succ_0
    2.71 -  add_Pls add_Min add_BIT_0 add_BIT_10 add_BIT_11
    2.72 -  minus_Pls minus_Min minus_1 minus_0
    2.73 -  mult_Pls mult_Min mult_num1 mult_num0 
    2.74 -  add_Pls_right add_Min_right
    2.75 +  normalize_bin_simps pred_bin_simps succ_bin_simps
    2.76 +  add_bin_simps minus_bin_simps mult_bin_simps
    2.77    abs_zero abs_one arith_extra_simps
    2.78  
    2.79  text {* Simplification of relational operations *}
     3.1 --- a/src/HOL/Presburger.thy	Fri Feb 15 23:22:02 2008 +0100
     3.2 +++ b/src/HOL/Presburger.thy	Sat Feb 16 02:01:13 2008 +0100
     3.3 @@ -671,20 +671,19 @@
     3.4    unfolding number_of_is_id ..
     3.5  
     3.6  lemmas pred_succ_numeral_code [code func] =
     3.7 -  arith_simps(5-12)
     3.8 +  pred_bin_simps succ_bin_simps
     3.9  
    3.10  lemmas plus_numeral_code [code func] =
    3.11 -  arith_simps(13-17)
    3.12 -  arith_simps(26-27)
    3.13 +  add_bin_simps
    3.14    arith_extra_simps(1) [where 'a = int]
    3.15  
    3.16  lemmas minus_numeral_code [code func] =
    3.17 -  arith_simps(18-21)
    3.18 +  minus_bin_simps
    3.19    arith_extra_simps(2) [where 'a = int]
    3.20    arith_extra_simps(5) [where 'a = int]
    3.21  
    3.22  lemmas times_numeral_code [code func] =
    3.23 -  arith_simps(22-25)
    3.24 +  mult_bin_simps
    3.25    arith_extra_simps(4) [where 'a = int]
    3.26  
    3.27  lemmas eq_numeral_code [code func] =
     4.1 --- a/src/HOL/Tools/ComputeNumeral.thy	Fri Feb 15 23:22:02 2008 +0100
     4.2 +++ b/src/HOL/Tools/ComputeNumeral.thy	Sat Feb 16 02:01:13 2008 +0100
     4.3 @@ -3,7 +3,7 @@
     4.4  begin
     4.5  
     4.6  (* normalization of bit strings *)
     4.7 -lemmas bitnorm = Pls_0_eq Min_1_eq
     4.8 +lemmas bitnorm = normalize_bin_simps
     4.9  
    4.10  (* neg for bit strings *)
    4.11  lemma neg1: "neg Int.Pls = False" by (simp add: Int.Pls_def)
    4.12 @@ -88,13 +88,13 @@
    4.13                   bitle9 bitle10 bitle11 bitle12 bitle13 bitle14 bitle15 bitle16
    4.14  
    4.15  (* succ for bit strings *)
    4.16 -lemmas bitsucc = succ_Pls succ_Min succ_1 succ_0
    4.17 +lemmas bitsucc = succ_bin_simps
    4.18  
    4.19  (* pred for bit strings *)
    4.20 -lemmas bitpred = pred_Pls pred_Min pred_1 pred_0
    4.21 +lemmas bitpred = pred_bin_simps
    4.22  
    4.23  (* unary minus for bit strings *)
    4.24 -lemmas bituminus = minus_Pls minus_Min minus_1 minus_0 
    4.25 +lemmas bituminus = minus_bin_simps
    4.26  
    4.27  (* addition for bit strings *)
    4.28  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"]
     5.1 --- a/src/HOL/ex/coopertac.ML	Fri Feb 15 23:22:02 2008 +0100
     5.2 +++ b/src/HOL/ex/coopertac.ML	Sat Feb 16 02:01:13 2008 +0100
     5.3 @@ -7,8 +7,7 @@
     5.4  val cooper_ss = @{simpset};
     5.5  
     5.6  val nT = HOLogic.natT;
     5.7 -val binarith = map thm
     5.8 -  ["Pls_0_eq", "Min_1_eq"];
     5.9 +val binarith = @{thms normalize_bin_simps};
    5.10  val comp_arith = binarith @ simp_thms
    5.11  
    5.12  val zdvd_int = thm "zdvd_int";
     6.1 --- a/src/HOL/int_arith1.ML	Fri Feb 15 23:22:02 2008 +0100
     6.2 +++ b/src/HOL/int_arith1.ML	Sat Feb 16 02:01:13 2008 +0100
     6.3 @@ -225,9 +225,8 @@
     6.4    subtract Thm.eq_thm [@{thm add_number_of_left}, @{thm number_of_add} RS sym] simps;
     6.5  
     6.6  (*To evaluate binary negations of coefficients*)
     6.7 -val minus_simps = [@{thm numeral_m1_eq_minus_1} RS sym, @{thm number_of_minus} RS sym,
     6.8 -                   @{thm minus_1}, @{thm minus_0}, @{thm minus_Pls}, @{thm minus_Min},
     6.9 -                   @{thm pred_1}, @{thm pred_0}, @{thm pred_Pls}, @{thm pred_Min}];
    6.10 +val minus_simps = [@{thm numeral_m1_eq_minus_1} RS sym, @{thm number_of_minus} RS sym] @
    6.11 +                   @{thms minus_bin_simps} @ @{thms pred_bin_simps};
    6.12  
    6.13  (*To let us treat subtraction as addition*)
    6.14  val diff_simps = [@{thm diff_minus}, @{thm minus_add_distrib}, @{thm minus_minus}];