src/HOL/Integ/int_arith1.ML
changeset 11868 56db9f3a6b3e
parent 11713 883d559b0b8c
child 12018 ec054019c910
     1.1 --- a/src/HOL/Integ/int_arith1.ML	Mon Oct 22 11:01:30 2001 +0200
     1.2 +++ b/src/HOL/Integ/int_arith1.ML	Mon Oct 22 11:54:22 2001 +0200
     1.3 @@ -5,19 +5,21 @@
     1.4  Simprocs and decision procedure for linear arithmetic.
     1.5  *)
     1.6  
     1.7 +Addsimps [int_numeral_0_eq_0, int_numeral_1_eq_1];
     1.8 +
     1.9  (*** Simprocs for numeric literals ***)
    1.10  
    1.11  (** Combining of literal coefficients in sums of products **)
    1.12  
    1.13 -Goal "(x < y) = (x-y < (Numeral0::int))";
    1.14 +Goal "(x < y) = (x-y < (0::int))";
    1.15  by (simp_tac (simpset() addsimps zcompare_rls) 1);
    1.16  qed "zless_iff_zdiff_zless_0";
    1.17  
    1.18 -Goal "(x = y) = (x-y = (Numeral0::int))";
    1.19 +Goal "(x = y) = (x-y = (0::int))";
    1.20  by (simp_tac (simpset() addsimps zcompare_rls) 1);
    1.21  qed "eq_iff_zdiff_eq_0";
    1.22  
    1.23 -Goal "(x <= y) = (x-y <= (Numeral0::int))";
    1.24 +Goal "(x <= y) = (x-y <= (0::int))";
    1.25  by (simp_tac (simpset() addsimps zcompare_rls) 1);
    1.26  qed "zle_iff_zdiff_zle_0";
    1.27  
    1.28 @@ -77,12 +79,22 @@
    1.29  structure Int_Numeral_Simprocs =
    1.30  struct
    1.31  
    1.32 +(*Maps 0 to Numeral0 and 1 to Numeral1 so that arithmetic in simprocs
    1.33 +  isn't complicated by the abstract 0 and 1.*)
    1.34 +val numeral_syms = [int_numeral_0_eq_0 RS sym, int_numeral_1_eq_1 RS sym];
    1.35 +val numeral_sym_ss = HOL_ss addsimps numeral_syms;
    1.36 +
    1.37 +fun rename_numerals th = 
    1.38 +    simplify numeral_sym_ss (Thm.transfer (the_context ()) th);
    1.39 +
    1.40  (*Utilities*)
    1.41  
    1.42  fun mk_numeral n = HOLogic.number_of_const HOLogic.intT $ HOLogic.mk_bin n;
    1.43  
    1.44  (*Decodes a binary INTEGER*)
    1.45 -fun dest_numeral (Const("Numeral.number_of", _) $ w) = 
    1.46 +fun dest_numeral (Const("0", _)) = 0
    1.47 +  | dest_numeral (Const("1", _)) = 1
    1.48 +  | dest_numeral (Const("Numeral.number_of", _) $ w) = 
    1.49       (HOLogic.dest_binum w
    1.50        handle TERM _ => raise TERM("Int_Numeral_Simprocs.dest_numeral:1", [w]))
    1.51    | dest_numeral t = raise TERM("Int_Numeral_Simprocs.dest_numeral:2", [t]);
    1.52 @@ -97,7 +109,7 @@
    1.53  
    1.54  val uminus_const = Const ("uminus", HOLogic.intT --> HOLogic.intT);
    1.55  
    1.56 -(*Thus mk_sum[t] yields t+Numeral0; longer sums don't have a trailing zero*)
    1.57 +(*Thus mk_sum[t] yields t+0; longer sums don't have a trailing zero*)
    1.58  fun mk_sum []        = zero
    1.59    | mk_sum [t,u]     = mk_plus (t, u)
    1.60    | mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
    1.61 @@ -157,16 +169,20 @@
    1.62  	handle TERM _ => find_first_coeff (t::past) u terms;
    1.63  
    1.64  
    1.65 -(*Simplify Numeral1*n and n*Numeral1 to n*)
    1.66 -val add_0s = [zadd_0, zadd_0_right];
    1.67 -val mult_1s = [zmult_1, zmult_1_right, zmult_minus1, zmult_minus1_right];
    1.68 +(*Simplify Numeral0+n, n+Numeral0, Numeral1*n, n*Numeral1*)
    1.69 +val add_0s =  map rename_numerals [zadd_0, zadd_0_right];
    1.70 +val mult_1s = map rename_numerals [zmult_1, zmult_1_right] @
    1.71 +              [zmult_minus1, zmult_minus1_right];
    1.72  
    1.73 -(*To perform binary arithmetic*)
    1.74 -val bin_simps = [add_number_of_left] @ bin_arith_simps @ bin_rel_simps;
    1.75 +(*To perform binary arithmetic.  The "left" rewriting handles patterns
    1.76 +  created by the simprocs, such as 3 * (5 * x). *)
    1.77 +val bin_simps = [int_numeral_0_eq_0 RS sym, int_numeral_1_eq_1 RS sym,
    1.78 +                 add_number_of_left, mult_number_of_left] @ 
    1.79 +                bin_arith_simps @ bin_rel_simps;
    1.80  
    1.81  (*To evaluate binary negations of coefficients*)
    1.82  val zminus_simps = NCons_simps @
    1.83 -                   [number_of_minus RS sym, 
    1.84 +                   [zminus_1_eq_m1, number_of_minus RS sym, 
    1.85  		    bin_minus_1, bin_minus_0, bin_minus_Pls, bin_minus_Min,
    1.86  		    bin_pred_1, bin_pred_0, bin_pred_Pls, bin_pred_Min];
    1.87  
    1.88 @@ -189,28 +205,10 @@
    1.89  fun trans_tac None      = all_tac
    1.90    | trans_tac (Some th) = ALLGOALS (rtac (th RS trans));
    1.91  
    1.92 -fun prove_conv name tacs sg (hyps: thm list) (t,u) =
    1.93 -  if t aconv u then None
    1.94 -  else
    1.95 -  let val ct = cterm_of sg (HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u)))
    1.96 -  in Some
    1.97 -     (prove_goalw_cterm [] ct (K tacs)
    1.98 -      handle ERROR => error 
    1.99 -	  ("The error(s) above occurred while trying to prove " ^
   1.100 -	   string_of_cterm ct ^ "\nInternal failure of simproc " ^ name))
   1.101 -  end;
   1.102 -
   1.103 -(*version without the hyps argument*)
   1.104 -fun prove_conv_nohyps name tacs sg = prove_conv name tacs sg [];
   1.105 -
   1.106  fun simplify_meta_eq rules =
   1.107      mk_meta_eq o
   1.108      simplify (HOL_basic_ss addeqcongs[eq_cong2] addsimps rules)
   1.109  
   1.110 -fun prep_simproc (name, pats, proc) = Simplifier.mk_simproc name pats proc;
   1.111 -fun prep_pat s = Thm.read_cterm (Theory.sign_of (the_context())) (s, HOLogic.termT);
   1.112 -val prep_pats = map prep_pat;
   1.113 -
   1.114  structure CancelNumeralsCommon =
   1.115    struct
   1.116    val mk_sum    	= mk_sum
   1.117 @@ -220,8 +218,8 @@
   1.118    val find_first_coeff	= find_first_coeff []
   1.119    val trans_tac         = trans_tac
   1.120    val norm_tac = 
   1.121 -     ALLGOALS (simp_tac (HOL_ss addsimps add_0s@mult_1s@diff_simps@
   1.122 -                                         zminus_simps@zadd_ac))
   1.123 +     ALLGOALS (simp_tac (HOL_ss addsimps numeral_syms@add_0s@mult_1s@
   1.124 +                                         diff_simps@zminus_simps@zadd_ac))
   1.125       THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@int_mult_minus_simps))
   1.126       THEN ALLGOALS (simp_tac (HOL_ss addsimps int_minus_from_mult_simps@
   1.127                                                zadd_ac@zmult_ac))
   1.128 @@ -232,7 +230,7 @@
   1.129  
   1.130  structure EqCancelNumerals = CancelNumeralsFun
   1.131   (open CancelNumeralsCommon
   1.132 -  val prove_conv = prove_conv "inteq_cancel_numerals"
   1.133 +  val prove_conv = Bin_Simprocs.prove_conv "inteq_cancel_numerals"
   1.134    val mk_bal   = HOLogic.mk_eq
   1.135    val dest_bal = HOLogic.dest_bin "op =" HOLogic.intT
   1.136    val bal_add1 = eq_add_iff1 RS trans
   1.137 @@ -241,7 +239,7 @@
   1.138  
   1.139  structure LessCancelNumerals = CancelNumeralsFun
   1.140   (open CancelNumeralsCommon
   1.141 -  val prove_conv = prove_conv "intless_cancel_numerals"
   1.142 +  val prove_conv = Bin_Simprocs.prove_conv "intless_cancel_numerals"
   1.143    val mk_bal   = HOLogic.mk_binrel "op <"
   1.144    val dest_bal = HOLogic.dest_bin "op <" HOLogic.intT
   1.145    val bal_add1 = less_add_iff1 RS trans
   1.146 @@ -250,7 +248,7 @@
   1.147  
   1.148  structure LeCancelNumerals = CancelNumeralsFun
   1.149   (open CancelNumeralsCommon
   1.150 -  val prove_conv = prove_conv "intle_cancel_numerals"
   1.151 +  val prove_conv = Bin_Simprocs.prove_conv "intle_cancel_numerals"
   1.152    val mk_bal   = HOLogic.mk_binrel "op <="
   1.153    val dest_bal = HOLogic.dest_bin "op <=" HOLogic.intT
   1.154    val bal_add1 = le_add_iff1 RS trans
   1.155 @@ -258,19 +256,22 @@
   1.156  );
   1.157  
   1.158  val cancel_numerals = 
   1.159 -  map prep_simproc
   1.160 +  map Bin_Simprocs.prep_simproc
   1.161     [("inteq_cancel_numerals",
   1.162 -     prep_pats ["(l::int) + m = n", "(l::int) = m + n", 
   1.163 +     Bin_Simprocs.prep_pats
   1.164 +               ["(l::int) + m = n", "(l::int) = m + n", 
   1.165  		"(l::int) - m = n", "(l::int) = m - n", 
   1.166  		"(l::int) * m = n", "(l::int) = m * n"], 
   1.167       EqCancelNumerals.proc),
   1.168      ("intless_cancel_numerals", 
   1.169 -     prep_pats ["(l::int) + m < n", "(l::int) < m + n", 
   1.170 +     Bin_Simprocs.prep_pats
   1.171 +               ["(l::int) + m < n", "(l::int) < m + n", 
   1.172  		"(l::int) - m < n", "(l::int) < m - n", 
   1.173  		"(l::int) * m < n", "(l::int) < m * n"], 
   1.174       LessCancelNumerals.proc),
   1.175      ("intle_cancel_numerals", 
   1.176 -     prep_pats ["(l::int) + m <= n", "(l::int) <= m + n", 
   1.177 +     Bin_Simprocs.prep_pats
   1.178 +               ["(l::int) + m <= n", "(l::int) <= m + n", 
   1.179  		"(l::int) - m <= n", "(l::int) <= m - n", 
   1.180  		"(l::int) * m <= n", "(l::int) <= m * n"], 
   1.181       LeCancelNumerals.proc)];
   1.182 @@ -284,11 +285,11 @@
   1.183    val mk_coeff		= mk_coeff
   1.184    val dest_coeff	= dest_coeff 1
   1.185    val left_distrib	= left_zadd_zmult_distrib RS trans
   1.186 -  val prove_conv        = prove_conv_nohyps "int_combine_numerals"
   1.187 +  val prove_conv        = Bin_Simprocs.prove_conv_nohyps "int_combine_numerals"
   1.188    val trans_tac          = trans_tac
   1.189    val norm_tac = 
   1.190 -     ALLGOALS (simp_tac (HOL_ss addsimps add_0s@mult_1s@diff_simps@
   1.191 -                                         zminus_simps@zadd_ac))
   1.192 +     ALLGOALS (simp_tac (HOL_ss addsimps numeral_syms@add_0s@mult_1s@
   1.193 +                                         diff_simps@zminus_simps@zadd_ac))
   1.194       THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@int_mult_minus_simps))
   1.195       THEN ALLGOALS (simp_tac (HOL_ss addsimps int_minus_from_mult_simps@
   1.196                                                zadd_ac@zmult_ac))
   1.197 @@ -299,9 +300,9 @@
   1.198  
   1.199  structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData);
   1.200    
   1.201 -val combine_numerals = 
   1.202 -    prep_simproc ("int_combine_numerals",
   1.203 -		  prep_pats ["(i::int) + j", "(i::int) - j"],
   1.204 +val combine_numerals = Bin_Simprocs.prep_simproc
   1.205 +                 ("int_combine_numerals",
   1.206 +		  Bin_Simprocs.prep_pats ["(i::int) + j", "(i::int) - j"],
   1.207  		  CombineNumerals.proc);
   1.208  
   1.209  end;
   1.210 @@ -316,7 +317,7 @@
   1.211  print_depth 22;
   1.212  set timing;
   1.213  set trace_simp;
   1.214 -fun test s = (Goal s; by (Simp_tac 1)); 
   1.215 +fun test s = (Goal s, by (Simp_tac 1)); 
   1.216  
   1.217  test "l + 2 + 2 + 2 + (l + 2) + (oo + 2) = (uu::int)";
   1.218  
   1.219 @@ -403,17 +404,20 @@
   1.220  local
   1.221  
   1.222  (* reduce contradictory <= to False *)
   1.223 -val add_rules = simp_thms @ bin_arith_simps @ bin_rel_simps @
   1.224 -                [zadd_0, zadd_0_right, zdiff_def,
   1.225 -		 zadd_zminus_inverse, zadd_zminus_inverse2, 
   1.226 -		 zmult_0, zmult_0_right, 
   1.227 -		 zmult_1, zmult_1_right, 
   1.228 -		 zmult_minus1, zmult_minus1_right,
   1.229 -		 zminus_zadd_distrib, zminus_zminus, zmult_assoc,
   1.230 -                 Zero_int_def, One_int_def, int_0, int_1, zadd_int RS sym, int_Suc];
   1.231 +val add_rules = 
   1.232 +    simp_thms @ bin_arith_simps @ bin_rel_simps @ 
   1.233 +    [int_numeral_0_eq_0, int_numeral_1_eq_1,
   1.234 +     zadd_0, zadd_0_right, zdiff_def,
   1.235 +     zadd_zminus_inverse, zadd_zminus_inverse2, 
   1.236 +     zmult_0, zmult_0_right, 
   1.237 +     zmult_1, zmult_1_right, 
   1.238 +     zmult_minus1, zmult_minus1_right,
   1.239 +     zminus_zadd_distrib, zminus_zminus, zmult_assoc,
   1.240 +     int_0, int_1, zadd_int RS sym, int_Suc];
   1.241  
   1.242  val simprocs = [Int_Times_Assoc.conv, Int_Numeral_Simprocs.combine_numerals]@
   1.243 -               Int_Numeral_Simprocs.cancel_numerals;
   1.244 +               Int_Numeral_Simprocs.cancel_numerals @ 
   1.245 +               Bin_Simprocs.eval_numerals;
   1.246  
   1.247  val add_mono_thms_int =
   1.248    map (fn s => prove_goal (the_context ()) s
   1.249 @@ -457,7 +461,7 @@
   1.250  by (fast_arith_tac 1);
   1.251  Goal "!!a::int. [| a < b; c < d |] ==> a-d+ 2 <= b+(-c)";
   1.252  by (fast_arith_tac 1);
   1.253 -Goal "!!a::int. [| a < b; c < d |] ==> a+c+ Numeral1 < b+d";
   1.254 +Goal "!!a::int. [| a < b; c < d |] ==> a+c+ 1 < b+d";
   1.255  by (fast_arith_tac 1);
   1.256  Goal "!!a::int. [| a <= b; b+b <= c |] ==> a+a <= c";
   1.257  by (fast_arith_tac 1);