moved some generic nonsense to arith_data.ML
authorhaftmann
Fri Mar 13 19:17:57 2009 +0100 (2009-03-13)
changeset 3051807b45c1aa788
parent 30517 51a39ed24c0f
child 30519 c05c0199826f
moved some generic nonsense to arith_data.ML
src/HOL/Tools/arith_data.ML
src/HOL/Tools/int_arith.ML
src/HOL/Tools/int_factor_simprocs.ML
src/HOL/Tools/nat_simprocs.ML
     1.1 --- a/src/HOL/Tools/arith_data.ML	Fri Mar 13 19:17:57 2009 +0100
     1.2 +++ b/src/HOL/Tools/arith_data.ML	Fri Mar 13 19:17:57 2009 +0100
     1.3 @@ -10,6 +10,8 @@
     1.4    val prove_conv: tactic list -> Proof.context -> thm list -> term * term -> thm option
     1.5    val prove_conv2: tactic -> (simpset -> tactic) -> simpset -> term * term -> thm
     1.6    val simp_all_tac: thm list -> simpset -> tactic
     1.7 +  val simplify_meta_eq: thm list -> simpset -> thm -> thm
     1.8 +  val trans_tac: thm option -> tactic
     1.9    val prep_simproc: string * string list * (theory -> simpset -> term -> thm option)
    1.10      -> simproc
    1.11  end;
    1.12 @@ -33,6 +35,13 @@
    1.13    let val ss0 = HOL_ss addsimps rules
    1.14    in fn ss => ALLGOALS (simp_tac (Simplifier.inherit_context ss ss0)) end;
    1.15  
    1.16 +fun simplify_meta_eq rules =
    1.17 +  let val ss0 = HOL_basic_ss addeqcongs [eq_cong2] addsimps rules
    1.18 +  in fn ss => simplify (Simplifier.inherit_context ss ss0) o mk_meta_eq end
    1.19 +
    1.20 +fun trans_tac NONE  = all_tac
    1.21 +  | trans_tac (SOME th) = ALLGOALS (rtac (th RS trans));
    1.22 +
    1.23  fun prep_simproc (name, pats, proc) = (*FIXME avoid the_context*)
    1.24    Simplifier.simproc (the_context ()) name pats proc;
    1.25  
     2.1 --- a/src/HOL/Tools/int_arith.ML	Fri Mar 13 19:17:57 2009 +0100
     2.2 +++ b/src/HOL/Tools/int_arith.ML	Fri Mar 13 19:17:57 2009 +0100
     2.3 @@ -29,41 +29,6 @@
     2.4  (*Maps 0 to Numeral0 and 1 to Numeral1 so that arithmetic isn't complicated by the abstract 0 and 1.*)
     2.5  val numeral_syms = [@{thm numeral_0_eq_0} RS sym, @{thm numeral_1_eq_1} RS sym];
     2.6  
     2.7 -(** New term ordering so that AC-rewriting brings numerals to the front **)
     2.8 -
     2.9 -(*Order integers by absolute value and then by sign. The standard integer
    2.10 -  ordering is not well-founded.*)
    2.11 -fun num_ord (i,j) =
    2.12 -  (case int_ord (abs i, abs j) of
    2.13 -    EQUAL => int_ord (Int.sign i, Int.sign j) 
    2.14 -  | ord => ord);
    2.15 -
    2.16 -(*This resembles TermOrd.term_ord, but it puts binary numerals before other
    2.17 -  non-atomic terms.*)
    2.18 -local open Term 
    2.19 -in 
    2.20 -fun numterm_ord (Abs (_, T, t), Abs(_, U, u)) =
    2.21 -      (case numterm_ord (t, u) of EQUAL => TermOrd.typ_ord (T, U) | ord => ord)
    2.22 -  | numterm_ord
    2.23 -     (Const(@{const_name Int.number_of}, _) $ v, Const(@{const_name Int.number_of}, _) $ w) =
    2.24 -     num_ord (HOLogic.dest_numeral v, HOLogic.dest_numeral w)
    2.25 -  | numterm_ord (Const(@{const_name Int.number_of}, _) $ _, _) = LESS
    2.26 -  | numterm_ord (_, Const(@{const_name Int.number_of}, _) $ _) = GREATER
    2.27 -  | numterm_ord (t, u) =
    2.28 -      (case int_ord (size_of_term t, size_of_term u) of
    2.29 -        EQUAL =>
    2.30 -          let val (f, ts) = strip_comb t and (g, us) = strip_comb u in
    2.31 -            (case TermOrd.hd_ord (f, g) of EQUAL => numterms_ord (ts, us) | ord => ord)
    2.32 -          end
    2.33 -      | ord => ord)
    2.34 -and numterms_ord (ts, us) = list_ord numterm_ord (ts, us)
    2.35 -end;
    2.36 -
    2.37 -fun numtermless tu = (numterm_ord tu = LESS);
    2.38 -
    2.39 -(*Defined in this file, but perhaps needed only for Int_Numeral_Simprocs of type nat.*)
    2.40 -val num_ss = HOL_ss settermless numtermless;
    2.41 -
    2.42  
    2.43  (** Utilities **)
    2.44  
    2.45 @@ -177,6 +142,41 @@
    2.46      in (mk_frac (p, 1), mk_divide (t', one_of T)) end;
    2.47  
    2.48  
    2.49 +(** New term ordering so that AC-rewriting brings numerals to the front **)
    2.50 +
    2.51 +(*Order integers by absolute value and then by sign. The standard integer
    2.52 +  ordering is not well-founded.*)
    2.53 +fun num_ord (i,j) =
    2.54 +  (case int_ord (abs i, abs j) of
    2.55 +    EQUAL => int_ord (Int.sign i, Int.sign j) 
    2.56 +  | ord => ord);
    2.57 +
    2.58 +(*This resembles TermOrd.term_ord, but it puts binary numerals before other
    2.59 +  non-atomic terms.*)
    2.60 +local open Term 
    2.61 +in 
    2.62 +fun numterm_ord (Abs (_, T, t), Abs(_, U, u)) =
    2.63 +      (case numterm_ord (t, u) of EQUAL => TermOrd.typ_ord (T, U) | ord => ord)
    2.64 +  | numterm_ord
    2.65 +     (Const(@{const_name Int.number_of}, _) $ v, Const(@{const_name Int.number_of}, _) $ w) =
    2.66 +     num_ord (HOLogic.dest_numeral v, HOLogic.dest_numeral w)
    2.67 +  | numterm_ord (Const(@{const_name Int.number_of}, _) $ _, _) = LESS
    2.68 +  | numterm_ord (_, Const(@{const_name Int.number_of}, _) $ _) = GREATER
    2.69 +  | numterm_ord (t, u) =
    2.70 +      (case int_ord (size_of_term t, size_of_term u) of
    2.71 +        EQUAL =>
    2.72 +          let val (f, ts) = strip_comb t and (g, us) = strip_comb u in
    2.73 +            (case TermOrd.hd_ord (f, g) of EQUAL => numterms_ord (ts, us) | ord => ord)
    2.74 +          end
    2.75 +      | ord => ord)
    2.76 +and numterms_ord (ts, us) = list_ord numterm_ord (ts, us)
    2.77 +end;
    2.78 +
    2.79 +fun numtermless tu = (numterm_ord tu = LESS);
    2.80 +
    2.81 +val num_ss = HOL_ss settermless numtermless;
    2.82 +
    2.83 +
    2.84  (*Simplify Numeral0+n, n+Numeral0, Numeral1*n, n*Numeral1, 1*x, x*1, x/1 *)
    2.85  val add_0s =  thms "add_0s";
    2.86  val mult_1s = thms "mult_1s" @ [thm"mult_1_left", thm"mult_1_right", thm"divide_1"];
    2.87 @@ -218,14 +218,6 @@
    2.88  val mult_minus_simps =
    2.89      [@{thm mult_assoc}, @{thm minus_mult_left}, minus_mult_eq_1_to_2];
    2.90  
    2.91 -(*Apply the given rewrite (if present) just once*)
    2.92 -fun trans_tac NONE      = all_tac
    2.93 -  | trans_tac (SOME th) = ALLGOALS (rtac (th RS trans));
    2.94 -
    2.95 -fun simplify_meta_eq rules =
    2.96 -  let val ss0 = HOL_basic_ss addeqcongs [eq_cong2] addsimps rules
    2.97 -  in fn ss => simplify (Simplifier.inherit_context ss ss0) o mk_meta_eq end
    2.98 -
    2.99  structure CancelNumeralsCommon =
   2.100    struct
   2.101    val mk_sum            = mk_sum
   2.102 @@ -233,7 +225,7 @@
   2.103    val mk_coeff          = mk_coeff
   2.104    val dest_coeff        = dest_coeff 1
   2.105    val find_first_coeff  = find_first_coeff []
   2.106 -  val trans_tac         = fn _ => trans_tac
   2.107 +  val trans_tac         = K Arith_Data.trans_tac
   2.108  
   2.109    val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @
   2.110      diff_simps @ minus_simps @ @{thms add_ac}
   2.111 @@ -246,7 +238,7 @@
   2.112  
   2.113    val numeral_simp_ss = HOL_ss addsimps add_0s @ simps
   2.114    fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
   2.115 -  val simplify_meta_eq = simplify_meta_eq (add_0s @ mult_1s)
   2.116 +  val simplify_meta_eq = Arith_Data.simplify_meta_eq (add_0s @ mult_1s)
   2.117    end;
   2.118  
   2.119  
   2.120 @@ -316,7 +308,7 @@
   2.121    val dest_coeff        = dest_coeff 1
   2.122    val left_distrib      = @{thm combine_common_factor} RS trans
   2.123    val prove_conv        = Arith_Data.prove_conv_nohyps
   2.124 -  val trans_tac         = fn _ => trans_tac
   2.125 +  val trans_tac         = K Arith_Data.trans_tac
   2.126  
   2.127    val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @
   2.128      diff_simps @ minus_simps @ @{thms add_ac}
   2.129 @@ -329,7 +321,7 @@
   2.130  
   2.131    val numeral_simp_ss = HOL_ss addsimps add_0s @ simps
   2.132    fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
   2.133 -  val simplify_meta_eq = simplify_meta_eq (add_0s @ mult_1s)
   2.134 +  val simplify_meta_eq = Arith_Data.simplify_meta_eq (add_0s @ mult_1s)
   2.135    end;
   2.136  
   2.137  structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData);
   2.138 @@ -346,7 +338,7 @@
   2.139    val dest_coeff        = dest_fcoeff 1
   2.140    val left_distrib      = @{thm combine_common_factor} RS trans
   2.141    val prove_conv        = Arith_Data.prove_conv_nohyps
   2.142 -  val trans_tac         = fn _ => trans_tac
   2.143 +  val trans_tac         = K Arith_Data.trans_tac
   2.144  
   2.145    val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @
   2.146      inverse_1s @ divide_simps @ diff_simps @ minus_simps @ @{thms add_ac}
   2.147 @@ -359,7 +351,7 @@
   2.148  
   2.149    val numeral_simp_ss = HOL_ss addsimps add_0s @ simps @ [@{thm add_frac_eq}]
   2.150    fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
   2.151 -  val simplify_meta_eq = simplify_meta_eq (add_0s @ mult_1s @ divide_1s)
   2.152 +  val simplify_meta_eq = Arith_Data.simplify_meta_eq (add_0s @ mult_1s @ divide_1s)
   2.153    end;
   2.154  
   2.155  structure FieldCombineNumerals = CombineNumeralsFun(FieldCombineNumeralsData);
     3.1 --- a/src/HOL/Tools/int_factor_simprocs.ML	Fri Mar 13 19:17:57 2009 +0100
     3.2 +++ b/src/HOL/Tools/int_factor_simprocs.ML	Fri Mar 13 19:17:57 2009 +0100
     3.3 @@ -29,7 +29,7 @@
     3.4    struct
     3.5    val mk_coeff          = mk_coeff
     3.6    val dest_coeff        = dest_coeff 1
     3.7 -  val trans_tac         = fn _ => trans_tac
     3.8 +  val trans_tac         = K Arith_Data.trans_tac
     3.9  
    3.10    val norm_ss1 = HOL_ss addsimps minus_from_mult_simps @ mult_1s
    3.11    val norm_ss2 = HOL_ss addsimps simps @ mult_minus_simps
    3.12 @@ -41,7 +41,7 @@
    3.13  
    3.14    val numeral_simp_ss = HOL_ss addsimps rel_number_of @ simps
    3.15    fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
    3.16 -  val simplify_meta_eq = Int_Numeral_Simprocs.simplify_meta_eq
    3.17 +  val simplify_meta_eq = Arith_Data.simplify_meta_eq
    3.18      [@{thm add_0}, @{thm add_0_right}, @{thm mult_zero_left},
    3.19        @{thm mult_zero_right}, @{thm mult_Bit1}, @{thm mult_1_right}];
    3.20    end
    3.21 @@ -215,7 +215,7 @@
    3.22          handle TERM _ => find_first_t (t::past) u terms;
    3.23  
    3.24  (** Final simplification for the CancelFactor simprocs **)
    3.25 -val simplify_one = Int_Numeral_Simprocs.simplify_meta_eq  
    3.26 +val simplify_one = Arith_Data.simplify_meta_eq  
    3.27    [@{thm mult_1_left}, @{thm mult_1_right}, @{thm div_by_1}, @{thm numeral_1_eq_1}];
    3.28  
    3.29  fun cancel_simplify_meta_eq cancel_th ss th =
    3.30 @@ -228,7 +228,7 @@
    3.31    val mk_coeff          = mk_coeff
    3.32    val dest_coeff        = dest_coeff
    3.33    val find_first        = find_first_t []
    3.34 -  val trans_tac         = fn _ => trans_tac
    3.35 +  val trans_tac         = K Arith_Data.trans_tac
    3.36    val norm_ss = HOL_ss addsimps mult_1s @ @{thms mult_ac}
    3.37    fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss))
    3.38    end;
     4.1 --- a/src/HOL/Tools/nat_simprocs.ML	Fri Mar 13 19:17:57 2009 +0100
     4.2 +++ b/src/HOL/Tools/nat_simprocs.ML	Fri Mar 13 19:17:57 2009 +0100
     4.3 @@ -41,8 +41,6 @@
     4.4  
     4.5  (** Other simproc items **)
     4.6  
     4.7 -val trans_tac = Int_Numeral_Simprocs.trans_tac;
     4.8 -
     4.9  val bin_simps =
    4.10       [@{thm nat_numeral_0_eq_0} RS sym, @{thm nat_numeral_1_eq_1} RS sym,
    4.11        @{thm add_nat_number_of}, @{thm nat_number_of_add_left}, 
    4.12 @@ -130,15 +128,11 @@
    4.13    @{thm Suc_not_Zero}, @{thm le_0_eq}];
    4.14  
    4.15  val simplify_meta_eq =
    4.16 -    Int_Numeral_Simprocs.simplify_meta_eq
    4.17 +    Arith_Data.simplify_meta_eq
    4.18          ([@{thm nat_numeral_0_eq_0}, @{thm numeral_1_eq_Suc_0}, @{thm add_0}, @{thm add_0_right},
    4.19            @{thm mult_0}, @{thm mult_0_right}, @{thm mult_1}, @{thm mult_1_right}] @ contra_rules);
    4.20  
    4.21  
    4.22 -(*Like HOL_ss but with an ordering that brings numerals to the front
    4.23 -  under AC-rewriting.*)
    4.24 -val num_ss = Int_Numeral_Simprocs.num_ss;
    4.25 -
    4.26  (*** Applying CancelNumeralsFun ***)
    4.27  
    4.28  structure CancelNumeralsCommon =
    4.29 @@ -148,11 +142,11 @@
    4.30    val mk_coeff          = mk_coeff
    4.31    val dest_coeff        = dest_coeff
    4.32    val find_first_coeff  = find_first_coeff []
    4.33 -  val trans_tac         = fn _ => trans_tac
    4.34 +  val trans_tac         = K Arith_Data.trans_tac
    4.35  
    4.36 -  val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @
    4.37 +  val norm_ss1 = Int_Numeral_Simprocs.num_ss addsimps numeral_syms @ add_0s @ mult_1s @
    4.38      [@{thm Suc_eq_add_numeral_1_left}] @ @{thms add_ac}
    4.39 -  val norm_ss2 = num_ss addsimps bin_simps @ @{thms add_ac} @ @{thms mult_ac}
    4.40 +  val norm_ss2 = Int_Numeral_Simprocs.num_ss addsimps bin_simps @ @{thms add_ac} @ @{thms mult_ac}
    4.41    fun norm_tac ss = 
    4.42      ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
    4.43      THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
    4.44 @@ -237,10 +231,10 @@
    4.45    val dest_coeff        = dest_coeff
    4.46    val left_distrib      = @{thm left_add_mult_distrib} RS trans
    4.47    val prove_conv        = Arith_Data.prove_conv_nohyps
    4.48 -  val trans_tac         = fn _ => trans_tac
    4.49 +  val trans_tac         = K Arith_Data.trans_tac
    4.50  
    4.51 -  val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_add_numeral_1}] @ @{thms add_ac}
    4.52 -  val norm_ss2 = num_ss addsimps bin_simps @ @{thms add_ac} @ @{thms mult_ac}
    4.53 +  val norm_ss1 = Int_Numeral_Simprocs.num_ss addsimps numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_add_numeral_1}] @ @{thms add_ac}
    4.54 +  val norm_ss2 = Int_Numeral_Simprocs.num_ss addsimps bin_simps @ @{thms add_ac} @ @{thms mult_ac}
    4.55    fun norm_tac ss =
    4.56      ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
    4.57      THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
    4.58 @@ -262,11 +256,11 @@
    4.59    struct
    4.60    val mk_coeff          = mk_coeff
    4.61    val dest_coeff        = dest_coeff
    4.62 -  val trans_tac         = fn _ => trans_tac
    4.63 +  val trans_tac         = K Arith_Data.trans_tac
    4.64  
    4.65 -  val norm_ss1 = num_ss addsimps
    4.66 +  val norm_ss1 = Int_Numeral_Simprocs.num_ss addsimps
    4.67      numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_add_numeral_1_left}] @ @{thms add_ac}
    4.68 -  val norm_ss2 = num_ss addsimps bin_simps @ @{thms add_ac} @ @{thms mult_ac}
    4.69 +  val norm_ss2 = Int_Numeral_Simprocs.num_ss addsimps bin_simps @ @{thms add_ac} @ @{thms mult_ac}
    4.70    fun norm_tac ss =
    4.71      ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
    4.72      THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
    4.73 @@ -355,7 +349,7 @@
    4.74          handle TERM _ => find_first_t (t::past) u terms;
    4.75  
    4.76  (** Final simplification for the CancelFactor simprocs **)
    4.77 -val simplify_one = Int_Numeral_Simprocs.simplify_meta_eq  
    4.78 +val simplify_one = Arith_Data.simplify_meta_eq  
    4.79    [@{thm mult_1_left}, @{thm mult_1_right}, @{thm div_1}, @{thm numeral_1_eq_Suc_0}];
    4.80  
    4.81  fun cancel_simplify_meta_eq cancel_th ss th =
    4.82 @@ -368,7 +362,7 @@
    4.83    val mk_coeff          = mk_coeff
    4.84    val dest_coeff        = dest_coeff
    4.85    val find_first        = find_first_t []
    4.86 -  val trans_tac         = fn _ => trans_tac
    4.87 +  val trans_tac         = K Arith_Data.trans_tac
    4.88    val norm_ss = HOL_ss addsimps mult_1s @ @{thms mult_ac}
    4.89    fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss))
    4.90    end;