tuned tactic
authorchaieb
Mon Jun 11 11:06:15 2007 +0200 (2007-06-11)
changeset 233186d68b07ab5cf
parent 23317 90be000da2a7
child 23319 173f4d2dedc2
tuned tactic
src/HOL/Complex/ex/linrtac.ML
src/HOL/Complex/ex/mirtac.ML
src/HOL/Real/ferrante_rackoff.ML
src/HOL/ex/coopertac.ML
     1.1 --- a/src/HOL/Complex/ex/linrtac.ML	Mon Jun 11 11:06:13 2007 +0200
     1.2 +++ b/src/HOL/Complex/ex/linrtac.ML	Mon Jun 11 11:06:15 2007 +0200
     1.3 @@ -18,28 +18,7 @@
     1.4    "add_BIT_11", "minus_Pls", "minus_Min", "minus_1", 
     1.5    "minus_0", "mult_Pls", "mult_Min", "mult_num1", "mult_num0", 
     1.6    "add_Pls_right", "add_Min_right"];
     1.7 - val intarithrel = 
     1.8 -     (map thm ["int_eq_number_of_eq","int_neg_number_of_BIT", 
     1.9 -		"int_le_number_of_eq","int_iszero_number_of_0",
    1.10 -		"int_less_number_of_eq_neg"]) @
    1.11 -     (map (fn s => thm s RS thm "lift_bool") 
    1.12 -	  ["int_iszero_number_of_Pls","int_iszero_number_of_1",
    1.13 -	   "int_neg_number_of_Min"])@
    1.14 -     (map (fn s => thm s RS thm "nlift_bool") 
    1.15 -	  ["int_nonzero_number_of_Min","int_not_neg_number_of_Pls"]);
    1.16 -     
    1.17 -val intarith = map thm ["int_number_of_add_sym", "int_number_of_minus_sym",
    1.18 -			"int_number_of_diff_sym", "int_number_of_mult_sym"];
    1.19 -val natarith = map thm ["add_nat_number_of", "diff_nat_number_of",
    1.20 -			"mult_nat_number_of", "eq_nat_number_of",
    1.21 -			"less_nat_number_of"]
    1.22 -val powerarith = 
    1.23 -    (map thm ["nat_number_of", "zpower_number_of_even", 
    1.24 -	      "zpower_Pls", "zpower_Min"]) @ 
    1.25 -    [thm "zpower_number_of_odd"]
    1.26 -
    1.27 -val comp_arith = binarith @ intarith @ intarithrel @ natarith 
    1.28 -	    @ powerarith @[thm"not_false_eq_true", thm "not_true_eq_false"];
    1.29 +val comp_arith = binarith @ simp_thms
    1.30  
    1.31  
    1.32  val zdvd_int = thm "zdvd_int";
     2.1 --- a/src/HOL/Complex/ex/mirtac.ML	Mon Jun 11 11:06:13 2007 +0200
     2.2 +++ b/src/HOL/Complex/ex/mirtac.ML	Mon Jun 11 11:06:15 2007 +0200
     2.3 @@ -28,13 +28,6 @@
     2.4               @{thm "diff_def"}, @{thm "minus_divide_left"}]
     2.5  val comp_ths = ths @ comp_arith @ simp_thms 
     2.6  
     2.7 -val powerarith = 
     2.8 -    (map thm ["nat_number_of", "zpower_number_of_even", 
     2.9 -	      "zpower_Pls", "zpower_Min"]) @ 
    2.10 -    [thm "zpower_number_of_odd"]
    2.11 -
    2.12 -val comp_arith = comp_ths @ powerarith @[thm"not_false_eq_true", thm "not_true_eq_false"];
    2.13 -
    2.14  
    2.15  val zdvd_int = @{thm "zdvd_int"};
    2.16  val zdiff_int_split = @{thm "zdiff_int_split"};
    2.17 @@ -108,7 +101,7 @@
    2.18  			addsimprocs [cancel_div_mod_proc]
    2.19      val simpset0 = HOL_basic_ss
    2.20        addsimps [mod_div_equality', Suc_plus1]
    2.21 -      addsimps comp_arith
    2.22 +      addsimps comp_ths
    2.23        addsplits [@{thm "split_zdiv"}, @{thm "split_zmod"}, @{thm "split_div'"}, @{thm "split_min"}, @{thm "split_max"}]
    2.24      (* Simp rules for changing (n::int) to int n *)
    2.25      val simpset1 = HOL_basic_ss
     3.1 --- a/src/HOL/Real/ferrante_rackoff.ML	Mon Jun 11 11:06:13 2007 +0200
     3.2 +++ b/src/HOL/Real/ferrante_rackoff.ML	Mon Jun 11 11:06:15 2007 +0200
     3.3 @@ -25,28 +25,7 @@
     3.4    "mult_Pls", "mult_Min", "mult_1", "mult_0", 
     3.5    "add_Pls_right", "add_Min_right"];
     3.6  
     3.7 -val intarithrel = 
     3.8 -  map thm ["int_eq_number_of_eq", "int_neg_number_of_BIT", "int_le_number_of_eq",
     3.9 -    "int_iszero_number_of_0", "int_less_number_of_eq_neg"]
    3.10 -  @ map (fn s => thm s RS thm "lift_bool") ["int_iszero_number_of_Pls",
    3.11 -    "int_iszero_number_of_1", "int_neg_number_of_Min"]
    3.12 -  @ map (fn s => thm s RS thm "nlift_bool") ["int_nonzero_number_of_Min",
    3.13 -    "int_not_neg_number_of_Pls"];
    3.14 - 
    3.15 -val intarith = map thm ["int_number_of_add_sym", "int_number_of_minus_sym",
    3.16 -  "int_number_of_diff_sym", "int_number_of_mult_sym"];
    3.17 -
    3.18 -val natarith = map thm ["add_nat_number_of", "diff_nat_number_of",
    3.19 -  "mult_nat_number_of", "eq_nat_number_of", "less_nat_number_of"];
    3.20 -
    3.21 -val powerarith =
    3.22 -  map thm ["nat_number_of", "zpower_number_of_even",
    3.23 -  "zpower_Pls", "zpower_Min"]
    3.24 -  @ [MetaSimplifier.simplify true [thm "zero_eq_Numeral0_nring", thm "one_eq_Numeral1_nring"]
    3.25 -    (thm "zpower_number_of_odd")]
    3.26 -
    3.27 -val comp_arith = binarith @ intarith @ intarithrel @ natarith 
    3.28 -  @ powerarith @ [thm "not_false_eq_true", thm "not_true_eq_false"];
    3.29 +val comp_arith = binarith @ arith_simps @ simp_thms
    3.30  
    3.31  fun prepare_for_linr q fm = 
    3.32    let
     4.1 --- a/src/HOL/ex/coopertac.ML	Mon Jun 11 11:06:13 2007 +0200
     4.2 +++ b/src/HOL/ex/coopertac.ML	Mon Jun 11 11:06:15 2007 +0200
     4.3 @@ -9,31 +9,7 @@
     4.4  val nT = HOLogic.natT;
     4.5  val binarith = map thm
     4.6    ["Pls_0_eq", "Min_1_eq"];
     4.7 - val intarithrel = 
     4.8 -     (map thm ["int_eq_number_of_eq","int_neg_number_of_BIT", 
     4.9 -		"int_le_number_of_eq","int_iszero_number_of_0",
    4.10 -		"int_less_number_of_eq_neg"]) @
    4.11 -     (map (fn s => thm s RS thm "lift_bool") 
    4.12 -	  ["int_iszero_number_of_Pls","int_iszero_number_of_1",
    4.13 -	   "int_neg_number_of_Min"])@
    4.14 -     (map (fn s => thm s RS thm "nlift_bool") 
    4.15 -	  ["int_nonzero_number_of_Min","int_not_neg_number_of_Pls"]);
    4.16 -     
    4.17 -val intarith = map thm ["int_number_of_add_sym", "int_number_of_minus_sym",
    4.18 -			"int_number_of_diff_sym", "int_number_of_mult_sym"];
    4.19 -val natarith = map thm ["add_nat_number_of", "diff_nat_number_of",
    4.20 -			"mult_nat_number_of", "eq_nat_number_of",
    4.21 -			"less_nat_number_of"]
    4.22 -val powerarith = 
    4.23 -    (map thm ["nat_number_of", "zpower_number_of_even", 
    4.24 -	      "zpower_Pls", "zpower_Min"]) @ 
    4.25 -    [simplify (HOL_basic_ss addsimps [thm "zero_eq_Numeral0_nring", 
    4.26 -			   thm "one_eq_Numeral1_nring"])
    4.27 -  (thm "zpower_number_of_odd")]
    4.28 -
    4.29 -val comp_arith = binarith @ intarith @ intarithrel @ natarith 
    4.30 -	    @ powerarith @[thm"not_false_eq_true", thm "not_true_eq_false"];
    4.31 -
    4.32 +val comp_arith = binarith @ simp_thms
    4.33  
    4.34  val zdvd_int = thm "zdvd_int";
    4.35  val zdiff_int_split = thm "zdiff_int_split";