src/HOL/Integ/int_arith1.ML
changeset 13462 56610e2ba220
parent 12975 d796a2fd6c69
child 13485 acf39e924091
     1.1 --- a/src/HOL/Integ/int_arith1.ML	Tue Aug 06 11:20:47 2002 +0200
     1.2 +++ b/src/HOL/Integ/int_arith1.ML	Tue Aug 06 11:22:05 2002 +0200
     1.3 @@ -34,15 +34,15 @@
     1.4  (** For cancel_numerals **)
     1.5  
     1.6  val rel_iff_rel_0_rls = map (inst "y" "?u+?v")
     1.7 -                          [zless_iff_zdiff_zless_0, eq_iff_zdiff_eq_0, 
     1.8 -			   zle_iff_zdiff_zle_0] @
     1.9 -		        map (inst "y" "n")
    1.10 -                          [zless_iff_zdiff_zless_0, eq_iff_zdiff_eq_0, 
    1.11 -			   zle_iff_zdiff_zle_0];
    1.12 +                          [zless_iff_zdiff_zless_0, eq_iff_zdiff_eq_0,
    1.13 +                           zle_iff_zdiff_zle_0] @
    1.14 +                        map (inst "y" "n")
    1.15 +                          [zless_iff_zdiff_zless_0, eq_iff_zdiff_eq_0,
    1.16 +                           zle_iff_zdiff_zle_0];
    1.17  
    1.18  Goal "!!i::int. (i*u + m = j*u + n) = ((i-j)*u + m = n)";
    1.19  by (asm_simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]@
    1.20 -		                     zadd_ac@rel_iff_rel_0_rls) 1);
    1.21 +                                     zadd_ac@rel_iff_rel_0_rls) 1);
    1.22  qed "eq_add_iff1";
    1.23  
    1.24  Goal "!!i::int. (i*u + m = j*u + n) = (m = (j-i)*u + n)";
    1.25 @@ -79,7 +79,7 @@
    1.26  val numeral_syms = [int_numeral_0_eq_0 RS sym, int_numeral_1_eq_1 RS sym];
    1.27  val numeral_sym_ss = HOL_ss addsimps numeral_syms;
    1.28  
    1.29 -fun rename_numerals th = 
    1.30 +fun rename_numerals th =
    1.31      simplify numeral_sym_ss (Thm.transfer (the_context ()) th);
    1.32  
    1.33  (*Utilities*)
    1.34 @@ -89,14 +89,14 @@
    1.35  (*Decodes a binary INTEGER*)
    1.36  fun dest_numeral (Const("0", _)) = 0
    1.37    | dest_numeral (Const("1", _)) = 1
    1.38 -  | dest_numeral (Const("Numeral.number_of", _) $ w) = 
    1.39 +  | dest_numeral (Const("Numeral.number_of", _) $ w) =
    1.40       (HOLogic.dest_binum w
    1.41        handle TERM _ => raise TERM("Int_Numeral_Simprocs.dest_numeral:1", [w]))
    1.42    | dest_numeral t = raise TERM("Int_Numeral_Simprocs.dest_numeral:2", [t]);
    1.43  
    1.44  fun find_first_numeral past (t::terms) =
    1.45 -	((dest_numeral t, rev past @ terms)
    1.46 -	 handle TERM _ => find_first_numeral (t::past) terms)
    1.47 +        ((dest_numeral t, rev past @ terms)
    1.48 +         handle TERM _ => find_first_numeral (t::past) terms)
    1.49    | find_first_numeral past [] = raise TERM("find_first_numeral", []);
    1.50  
    1.51  val zero = mk_numeral 0;
    1.52 @@ -121,7 +121,7 @@
    1.53    | dest_summing (pos, Const ("op -", _) $ t $ u, ts) =
    1.54          dest_summing (pos, t, dest_summing (not pos, u, ts))
    1.55    | dest_summing (pos, t, ts) =
    1.56 -	if pos then t::ts else uminus_const$t :: ts;
    1.57 +        if pos then t::ts else uminus_const$t :: ts;
    1.58  
    1.59  fun dest_sum t = dest_summing (true, t, []);
    1.60  
    1.61 @@ -139,29 +139,29 @@
    1.62  val dest_times = HOLogic.dest_bin "op *" HOLogic.intT;
    1.63  
    1.64  fun dest_prod t =
    1.65 -      let val (t,u) = dest_times t 
    1.66 +      let val (t,u) = dest_times t
    1.67        in  dest_prod t @ dest_prod u  end
    1.68        handle TERM _ => [t];
    1.69  
    1.70 -(*DON'T do the obvious simplifications; that would create special cases*) 
    1.71 +(*DON'T do the obvious simplifications; that would create special cases*)
    1.72  fun mk_coeff (k, ts) = mk_times (mk_numeral k, ts);
    1.73  
    1.74  (*Express t as a product of (possibly) a numeral with other sorted terms*)
    1.75  fun dest_coeff sign (Const ("uminus", _) $ t) = dest_coeff (~sign) t
    1.76    | dest_coeff sign t =
    1.77      let val ts = sort Term.term_ord (dest_prod t)
    1.78 -	val (n, ts') = find_first_numeral [] ts
    1.79 +        val (n, ts') = find_first_numeral [] ts
    1.80                            handle TERM _ => (1, ts)
    1.81      in (sign*n, mk_prod ts') end;
    1.82  
    1.83  (*Find first coefficient-term THAT MATCHES u*)
    1.84 -fun find_first_coeff past u [] = raise TERM("find_first_coeff", []) 
    1.85 +fun find_first_coeff past u [] = raise TERM("find_first_coeff", [])
    1.86    | find_first_coeff past u (t::terms) =
    1.87 -	let val (n,u') = dest_coeff 1 t
    1.88 -	in  if u aconv u' then (n, rev past @ terms)
    1.89 -			  else find_first_coeff (t::past) u terms
    1.90 -	end
    1.91 -	handle TERM _ => find_first_coeff (t::past) u terms;
    1.92 +        let val (n,u') = dest_coeff 1 t
    1.93 +        in  if u aconv u' then (n, rev past @ terms)
    1.94 +                          else find_first_coeff (t::past) u terms
    1.95 +        end
    1.96 +        handle TERM _ => find_first_coeff (t::past) u terms;
    1.97  
    1.98  
    1.99  (*Simplify Numeral0+n, n+Numeral0, Numeral1*n, n*Numeral1*)
   1.100 @@ -172,24 +172,24 @@
   1.101  (*To perform binary arithmetic.  The "left" rewriting handles patterns
   1.102    created by the simprocs, such as 3 * (5 * x). *)
   1.103  val bin_simps = [int_numeral_0_eq_0 RS sym, int_numeral_1_eq_1 RS sym,
   1.104 -                 add_number_of_left, mult_number_of_left] @ 
   1.105 +                 add_number_of_left, mult_number_of_left] @
   1.106                  bin_arith_simps @ bin_rel_simps;
   1.107  
   1.108  (*To evaluate binary negations of coefficients*)
   1.109  val zminus_simps = NCons_simps @
   1.110 -                   [zminus_1_eq_m1, number_of_minus RS sym, 
   1.111 -		    bin_minus_1, bin_minus_0, bin_minus_Pls, bin_minus_Min,
   1.112 -		    bin_pred_1, bin_pred_0, bin_pred_Pls, bin_pred_Min];
   1.113 +                   [zminus_1_eq_m1, number_of_minus RS sym,
   1.114 +                    bin_minus_1, bin_minus_0, bin_minus_Pls, bin_minus_Min,
   1.115 +                    bin_pred_1, bin_pred_0, bin_pred_Pls, bin_pred_Min];
   1.116  
   1.117  (*To let us treat subtraction as addition*)
   1.118  val diff_simps = [zdiff_def, zminus_zadd_distrib, zminus_zminus];
   1.119  
   1.120  (*push the unary minus down: - x * y = x * - y *)
   1.121 -val int_minus_mult_eq_1_to_2 = 
   1.122 +val int_minus_mult_eq_1_to_2 =
   1.123      [zmult_zminus, zmult_zminus_right RS sym] MRS trans |> standard;
   1.124  
   1.125  (*to extract again any uncancelled minuses*)
   1.126 -val int_minus_from_mult_simps = 
   1.127 +val int_minus_from_mult_simps =
   1.128      [zminus_zminus, zmult_zminus, zmult_zminus_right];
   1.129  
   1.130  (*combine unary minus with numeric literals, however nested within a product*)
   1.131 @@ -206,19 +206,19 @@
   1.132  
   1.133  structure CancelNumeralsCommon =
   1.134    struct
   1.135 -  val mk_sum    	= mk_sum
   1.136 -  val dest_sum		= dest_sum
   1.137 -  val mk_coeff		= mk_coeff
   1.138 -  val dest_coeff	= dest_coeff 1
   1.139 -  val find_first_coeff	= find_first_coeff []
   1.140 +  val mk_sum            = mk_sum
   1.141 +  val dest_sum          = dest_sum
   1.142 +  val mk_coeff          = mk_coeff
   1.143 +  val dest_coeff        = dest_coeff 1
   1.144 +  val find_first_coeff  = find_first_coeff []
   1.145    val trans_tac         = trans_tac
   1.146 -  val norm_tac = 
   1.147 +  val norm_tac =
   1.148       ALLGOALS (simp_tac (HOL_ss addsimps numeral_syms@add_0s@mult_1s@
   1.149                                           diff_simps@zminus_simps@zadd_ac))
   1.150       THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@int_mult_minus_simps))
   1.151       THEN ALLGOALS (simp_tac (HOL_ss addsimps int_minus_from_mult_simps@
   1.152                                                zadd_ac@zmult_ac))
   1.153 -  val numeral_simp_tac	= ALLGOALS (simp_tac (HOL_ss addsimps add_0s@bin_simps))
   1.154 +  val numeral_simp_tac  = ALLGOALS (simp_tac (HOL_ss addsimps add_0s@bin_simps))
   1.155    val simplify_meta_eq  = simplify_meta_eq (add_0s@mult_1s)
   1.156    end;
   1.157  
   1.158 @@ -250,55 +250,51 @@
   1.159    val bal_add2 = le_add_iff2 RS trans
   1.160  );
   1.161  
   1.162 -val cancel_numerals = 
   1.163 +val cancel_numerals =
   1.164    map Bin_Simprocs.prep_simproc
   1.165     [("inteq_cancel_numerals",
   1.166 -     Bin_Simprocs.prep_pats
   1.167 -               ["(l::int) + m = n", "(l::int) = m + n", 
   1.168 -		"(l::int) - m = n", "(l::int) = m - n", 
   1.169 -		"(l::int) * m = n", "(l::int) = m * n"], 
   1.170 +     ["(l::int) + m = n", "(l::int) = m + n",
   1.171 +      "(l::int) - m = n", "(l::int) = m - n",
   1.172 +      "(l::int) * m = n", "(l::int) = m * n"],
   1.173       EqCancelNumerals.proc),
   1.174 -    ("intless_cancel_numerals", 
   1.175 -     Bin_Simprocs.prep_pats
   1.176 -               ["(l::int) + m < n", "(l::int) < m + n", 
   1.177 -		"(l::int) - m < n", "(l::int) < m - n", 
   1.178 -		"(l::int) * m < n", "(l::int) < m * n"], 
   1.179 +    ("intless_cancel_numerals",
   1.180 +     ["(l::int) + m < n", "(l::int) < m + n",
   1.181 +      "(l::int) - m < n", "(l::int) < m - n",
   1.182 +      "(l::int) * m < n", "(l::int) < m * n"],
   1.183       LessCancelNumerals.proc),
   1.184 -    ("intle_cancel_numerals", 
   1.185 -     Bin_Simprocs.prep_pats
   1.186 -               ["(l::int) + m <= n", "(l::int) <= m + n", 
   1.187 -		"(l::int) - m <= n", "(l::int) <= m - n", 
   1.188 -		"(l::int) * m <= n", "(l::int) <= m * n"], 
   1.189 +    ("intle_cancel_numerals",
   1.190 +     ["(l::int) + m <= n", "(l::int) <= m + n",
   1.191 +      "(l::int) - m <= n", "(l::int) <= m - n",
   1.192 +      "(l::int) * m <= n", "(l::int) <= m * n"],
   1.193       LeCancelNumerals.proc)];
   1.194  
   1.195  
   1.196  structure CombineNumeralsData =
   1.197    struct
   1.198 -  val add		= op + : int*int -> int 
   1.199 -  val mk_sum    	= long_mk_sum    (*to work for e.g. 2*x + 3*x *)
   1.200 -  val dest_sum		= dest_sum
   1.201 -  val mk_coeff		= mk_coeff
   1.202 -  val dest_coeff	= dest_coeff 1
   1.203 -  val left_distrib	= left_zadd_zmult_distrib RS trans
   1.204 +  val add               = op + : int*int -> int
   1.205 +  val mk_sum            = long_mk_sum    (*to work for e.g. 2*x + 3*x *)
   1.206 +  val dest_sum          = dest_sum
   1.207 +  val mk_coeff          = mk_coeff
   1.208 +  val dest_coeff        = dest_coeff 1
   1.209 +  val left_distrib      = left_zadd_zmult_distrib RS trans
   1.210    val prove_conv        = Bin_Simprocs.prove_conv_nohyps "int_combine_numerals"
   1.211    val trans_tac          = trans_tac
   1.212 -  val norm_tac = 
   1.213 +  val norm_tac =
   1.214       ALLGOALS (simp_tac (HOL_ss addsimps numeral_syms@add_0s@mult_1s@
   1.215                                           diff_simps@zminus_simps@zadd_ac))
   1.216       THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@int_mult_minus_simps))
   1.217       THEN ALLGOALS (simp_tac (HOL_ss addsimps int_minus_from_mult_simps@
   1.218                                                zadd_ac@zmult_ac))
   1.219 -  val numeral_simp_tac	= ALLGOALS 
   1.220 +  val numeral_simp_tac  = ALLGOALS
   1.221                      (simp_tac (HOL_ss addsimps add_0s@bin_simps))
   1.222    val simplify_meta_eq  = simplify_meta_eq (add_0s@mult_1s)
   1.223    end;
   1.224  
   1.225  structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData);
   1.226 -  
   1.227 -val combine_numerals = Bin_Simprocs.prep_simproc
   1.228 -                 ("int_combine_numerals",
   1.229 -		  Bin_Simprocs.prep_pats ["(i::int) + j", "(i::int) - j"],
   1.230 -		  CombineNumerals.proc);
   1.231 +
   1.232 +val combine_numerals =
   1.233 +  Bin_Simprocs.prep_simproc
   1.234 +    ("int_combine_numerals", ["(i::int) + j", "(i::int) - j"], CombineNumerals.proc);
   1.235  
   1.236  end;
   1.237  
   1.238 @@ -312,7 +308,7 @@
   1.239  print_depth 22;
   1.240  set timing;
   1.241  set trace_simp;
   1.242 -fun test s = (Goal s, by (Simp_tac 1)); 
   1.243 +fun test s = (Goal s, by (Simp_tac 1));
   1.244  
   1.245  test "l + 2 + 2 + 2 + (l + 2) + (oo + 2) = (uu::int)";
   1.246  
   1.247 @@ -355,10 +351,10 @@
   1.248  
   1.249  structure Int_Times_Assoc_Data : ASSOC_FOLD_DATA =
   1.250  struct
   1.251 -  val ss		= HOL_ss
   1.252 -  val eq_reflection	= eq_reflection
   1.253 +  val ss                = HOL_ss
   1.254 +  val eq_reflection     = eq_reflection
   1.255    val sg_ref = Sign.self_ref (Theory.sign_of (the_context ()))
   1.256 -  val T	     = HOLogic.intT
   1.257 +  val T      = HOLogic.intT
   1.258    val plus   = Const ("op *", [HOLogic.intT,HOLogic.intT] ---> HOLogic.intT);
   1.259    val add_ac = zmult_ac
   1.260  end;
   1.261 @@ -372,10 +368,10 @@
   1.262  
   1.263  structure Nat_Times_Assoc_Data : ASSOC_FOLD_DATA =
   1.264  struct
   1.265 -  val ss		= HOL_ss
   1.266 -  val eq_reflection	= eq_reflection
   1.267 +  val ss                = HOL_ss
   1.268 +  val eq_reflection     = eq_reflection
   1.269    val sg_ref = Sign.self_ref (Theory.sign_of (the_context ()))
   1.270 -  val T	     = HOLogic.natT
   1.271 +  val T      = HOLogic.natT
   1.272    val plus   = Const ("op *", [HOLogic.natT,HOLogic.natT] ---> HOLogic.natT);
   1.273    val add_ac = mult_ac
   1.274  end;
   1.275 @@ -399,19 +395,19 @@
   1.276  local
   1.277  
   1.278  (* reduce contradictory <= to False *)
   1.279 -val add_rules = 
   1.280 -    simp_thms @ bin_arith_simps @ bin_rel_simps @ 
   1.281 +val add_rules =
   1.282 +    simp_thms @ bin_arith_simps @ bin_rel_simps @
   1.283      [int_numeral_0_eq_0, int_numeral_1_eq_1,
   1.284       zminus_0, zadd_0, zadd_0_right, zdiff_def,
   1.285 -     zadd_zminus_inverse, zadd_zminus_inverse2, 
   1.286 -     zmult_0, zmult_0_right, 
   1.287 +     zadd_zminus_inverse, zadd_zminus_inverse2,
   1.288 +     zmult_0, zmult_0_right,
   1.289       zmult_1, zmult_1_right,
   1.290       zmult_zminus, zmult_zminus_right,
   1.291       zminus_zadd_distrib, zminus_zminus, zmult_assoc,
   1.292       int_0, int_1, zadd_int RS sym, int_Suc];
   1.293  
   1.294  val simprocs = [Int_Times_Assoc.conv, Int_Numeral_Simprocs.combine_numerals]@
   1.295 -               Int_Numeral_Simprocs.cancel_numerals @ 
   1.296 +               Int_Numeral_Simprocs.cancel_numerals @
   1.297                 Bin_Simprocs.eval_numerals;
   1.298  
   1.299  val add_mono_thms_int =
   1.300 @@ -440,16 +436,12 @@
   1.301  
   1.302  end;
   1.303  
   1.304 -let
   1.305 -val int_arith_simproc_pats =
   1.306 -  map (fn s => Thm.read_cterm (Theory.sign_of (the_context())) (s, HOLogic.boolT))
   1.307 -      ["(m::int) < n","(m::int) <= n", "(m::int) = n"];
   1.308 +val fast_int_arith_simproc =
   1.309 +  Simplifier.simproc (Theory.sign_of (the_context()))
   1.310 +  "fast_int_arith" ["(m::int) < n","(m::int) <= n", "(m::int) = n"] Fast_Arith.lin_arith_prover;
   1.311  
   1.312 -val fast_int_arith_simproc = mk_simproc
   1.313 -  "fast_int_arith" int_arith_simproc_pats Fast_Arith.lin_arith_prover;
   1.314 -in
   1.315  Addsimprocs [fast_int_arith_simproc]
   1.316 -end;
   1.317 +
   1.318  
   1.319  (* Some test data
   1.320  Goal "!!a::int. [| a <= b; c <= d; x+y<z |] ==> a+c <= b+d";