src/HOL/Tools/int_arith.ML
changeset 30518 07b45c1aa788
parent 30496 7cdcc9dd95cb
child 30685 dd5fe091ff04
     1.1 --- a/src/HOL/Tools/int_arith.ML	Fri Mar 13 19:17:57 2009 +0100
     1.2 +++ b/src/HOL/Tools/int_arith.ML	Fri Mar 13 19:17:57 2009 +0100
     1.3 @@ -29,41 +29,6 @@
     1.4  (*Maps 0 to Numeral0 and 1 to Numeral1 so that arithmetic isn't complicated by the abstract 0 and 1.*)
     1.5  val numeral_syms = [@{thm numeral_0_eq_0} RS sym, @{thm numeral_1_eq_1} RS sym];
     1.6  
     1.7 -(** New term ordering so that AC-rewriting brings numerals to the front **)
     1.8 -
     1.9 -(*Order integers by absolute value and then by sign. The standard integer
    1.10 -  ordering is not well-founded.*)
    1.11 -fun num_ord (i,j) =
    1.12 -  (case int_ord (abs i, abs j) of
    1.13 -    EQUAL => int_ord (Int.sign i, Int.sign j) 
    1.14 -  | ord => ord);
    1.15 -
    1.16 -(*This resembles TermOrd.term_ord, but it puts binary numerals before other
    1.17 -  non-atomic terms.*)
    1.18 -local open Term 
    1.19 -in 
    1.20 -fun numterm_ord (Abs (_, T, t), Abs(_, U, u)) =
    1.21 -      (case numterm_ord (t, u) of EQUAL => TermOrd.typ_ord (T, U) | ord => ord)
    1.22 -  | numterm_ord
    1.23 -     (Const(@{const_name Int.number_of}, _) $ v, Const(@{const_name Int.number_of}, _) $ w) =
    1.24 -     num_ord (HOLogic.dest_numeral v, HOLogic.dest_numeral w)
    1.25 -  | numterm_ord (Const(@{const_name Int.number_of}, _) $ _, _) = LESS
    1.26 -  | numterm_ord (_, Const(@{const_name Int.number_of}, _) $ _) = GREATER
    1.27 -  | numterm_ord (t, u) =
    1.28 -      (case int_ord (size_of_term t, size_of_term u) of
    1.29 -        EQUAL =>
    1.30 -          let val (f, ts) = strip_comb t and (g, us) = strip_comb u in
    1.31 -            (case TermOrd.hd_ord (f, g) of EQUAL => numterms_ord (ts, us) | ord => ord)
    1.32 -          end
    1.33 -      | ord => ord)
    1.34 -and numterms_ord (ts, us) = list_ord numterm_ord (ts, us)
    1.35 -end;
    1.36 -
    1.37 -fun numtermless tu = (numterm_ord tu = LESS);
    1.38 -
    1.39 -(*Defined in this file, but perhaps needed only for Int_Numeral_Simprocs of type nat.*)
    1.40 -val num_ss = HOL_ss settermless numtermless;
    1.41 -
    1.42  
    1.43  (** Utilities **)
    1.44  
    1.45 @@ -177,6 +142,41 @@
    1.46      in (mk_frac (p, 1), mk_divide (t', one_of T)) end;
    1.47  
    1.48  
    1.49 +(** New term ordering so that AC-rewriting brings numerals to the front **)
    1.50 +
    1.51 +(*Order integers by absolute value and then by sign. The standard integer
    1.52 +  ordering is not well-founded.*)
    1.53 +fun num_ord (i,j) =
    1.54 +  (case int_ord (abs i, abs j) of
    1.55 +    EQUAL => int_ord (Int.sign i, Int.sign j) 
    1.56 +  | ord => ord);
    1.57 +
    1.58 +(*This resembles TermOrd.term_ord, but it puts binary numerals before other
    1.59 +  non-atomic terms.*)
    1.60 +local open Term 
    1.61 +in 
    1.62 +fun numterm_ord (Abs (_, T, t), Abs(_, U, u)) =
    1.63 +      (case numterm_ord (t, u) of EQUAL => TermOrd.typ_ord (T, U) | ord => ord)
    1.64 +  | numterm_ord
    1.65 +     (Const(@{const_name Int.number_of}, _) $ v, Const(@{const_name Int.number_of}, _) $ w) =
    1.66 +     num_ord (HOLogic.dest_numeral v, HOLogic.dest_numeral w)
    1.67 +  | numterm_ord (Const(@{const_name Int.number_of}, _) $ _, _) = LESS
    1.68 +  | numterm_ord (_, Const(@{const_name Int.number_of}, _) $ _) = GREATER
    1.69 +  | numterm_ord (t, u) =
    1.70 +      (case int_ord (size_of_term t, size_of_term u) of
    1.71 +        EQUAL =>
    1.72 +          let val (f, ts) = strip_comb t and (g, us) = strip_comb u in
    1.73 +            (case TermOrd.hd_ord (f, g) of EQUAL => numterms_ord (ts, us) | ord => ord)
    1.74 +          end
    1.75 +      | ord => ord)
    1.76 +and numterms_ord (ts, us) = list_ord numterm_ord (ts, us)
    1.77 +end;
    1.78 +
    1.79 +fun numtermless tu = (numterm_ord tu = LESS);
    1.80 +
    1.81 +val num_ss = HOL_ss settermless numtermless;
    1.82 +
    1.83 +
    1.84  (*Simplify Numeral0+n, n+Numeral0, Numeral1*n, n*Numeral1, 1*x, x*1, x/1 *)
    1.85  val add_0s =  thms "add_0s";
    1.86  val mult_1s = thms "mult_1s" @ [thm"mult_1_left", thm"mult_1_right", thm"divide_1"];
    1.87 @@ -218,14 +218,6 @@
    1.88  val mult_minus_simps =
    1.89      [@{thm mult_assoc}, @{thm minus_mult_left}, minus_mult_eq_1_to_2];
    1.90  
    1.91 -(*Apply the given rewrite (if present) just once*)
    1.92 -fun trans_tac NONE      = all_tac
    1.93 -  | trans_tac (SOME th) = ALLGOALS (rtac (th RS trans));
    1.94 -
    1.95 -fun simplify_meta_eq rules =
    1.96 -  let val ss0 = HOL_basic_ss addeqcongs [eq_cong2] addsimps rules
    1.97 -  in fn ss => simplify (Simplifier.inherit_context ss ss0) o mk_meta_eq end
    1.98 -
    1.99  structure CancelNumeralsCommon =
   1.100    struct
   1.101    val mk_sum            = mk_sum
   1.102 @@ -233,7 +225,7 @@
   1.103    val mk_coeff          = mk_coeff
   1.104    val dest_coeff        = dest_coeff 1
   1.105    val find_first_coeff  = find_first_coeff []
   1.106 -  val trans_tac         = fn _ => trans_tac
   1.107 +  val trans_tac         = K Arith_Data.trans_tac
   1.108  
   1.109    val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @
   1.110      diff_simps @ minus_simps @ @{thms add_ac}
   1.111 @@ -246,7 +238,7 @@
   1.112  
   1.113    val numeral_simp_ss = HOL_ss addsimps add_0s @ simps
   1.114    fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
   1.115 -  val simplify_meta_eq = simplify_meta_eq (add_0s @ mult_1s)
   1.116 +  val simplify_meta_eq = Arith_Data.simplify_meta_eq (add_0s @ mult_1s)
   1.117    end;
   1.118  
   1.119  
   1.120 @@ -316,7 +308,7 @@
   1.121    val dest_coeff        = dest_coeff 1
   1.122    val left_distrib      = @{thm combine_common_factor} RS trans
   1.123    val prove_conv        = Arith_Data.prove_conv_nohyps
   1.124 -  val trans_tac         = fn _ => trans_tac
   1.125 +  val trans_tac         = K Arith_Data.trans_tac
   1.126  
   1.127    val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @
   1.128      diff_simps @ minus_simps @ @{thms add_ac}
   1.129 @@ -329,7 +321,7 @@
   1.130  
   1.131    val numeral_simp_ss = HOL_ss addsimps add_0s @ simps
   1.132    fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
   1.133 -  val simplify_meta_eq = simplify_meta_eq (add_0s @ mult_1s)
   1.134 +  val simplify_meta_eq = Arith_Data.simplify_meta_eq (add_0s @ mult_1s)
   1.135    end;
   1.136  
   1.137  structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData);
   1.138 @@ -346,7 +338,7 @@
   1.139    val dest_coeff        = dest_fcoeff 1
   1.140    val left_distrib      = @{thm combine_common_factor} RS trans
   1.141    val prove_conv        = Arith_Data.prove_conv_nohyps
   1.142 -  val trans_tac         = fn _ => trans_tac
   1.143 +  val trans_tac         = K Arith_Data.trans_tac
   1.144  
   1.145    val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @
   1.146      inverse_1s @ divide_simps @ diff_simps @ minus_simps @ @{thms add_ac}
   1.147 @@ -359,7 +351,7 @@
   1.148  
   1.149    val numeral_simp_ss = HOL_ss addsimps add_0s @ simps @ [@{thm add_frac_eq}]
   1.150    fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
   1.151 -  val simplify_meta_eq = simplify_meta_eq (add_0s @ mult_1s @ divide_1s)
   1.152 +  val simplify_meta_eq = Arith_Data.simplify_meta_eq (add_0s @ mult_1s @ divide_1s)
   1.153    end;
   1.154  
   1.155  structure FieldCombineNumerals = CombineNumeralsFun(FieldCombineNumeralsData);