src/HOL/Integ/int_arith1.ML
changeset 14272 5efbb548107d
parent 14271 8ed6989228bb
child 14273 e33ffff0123c
     1.1 --- a/src/HOL/Integ/int_arith1.ML	Wed Dec 03 10:49:34 2003 +0100
     1.2 +++ b/src/HOL/Integ/int_arith1.ML	Thu Dec 04 10:29:17 2003 +0100
     1.3 @@ -5,74 +5,184 @@
     1.4  Simprocs and decision procedure for linear arithmetic.
     1.5  *)
     1.6  
     1.7 -val zadd_ac = thms "Ring_and_Field.add_ac";
     1.8 -val zmult_ac = thms "Ring_and_Field.mult_ac";
     1.9 -
    1.10 -
    1.11 -Addsimps [int_numeral_0_eq_0, int_numeral_1_eq_1];
    1.12 -
    1.13 -(*** Simprocs for numeric literals ***)
    1.14 -
    1.15 -(** Combining of literal coefficients in sums of products **)
    1.16 -
    1.17 -Goal "(x < y) = (x-y < (0::int))";
    1.18 -by (simp_tac (simpset() addsimps compare_rls) 1);
    1.19 -qed "zless_iff_zdiff_zless_0";
    1.20 +val NCons_Pls = thm"NCons_Pls";
    1.21 +val NCons_Min = thm"NCons_Min";
    1.22 +val NCons_BIT = thm"NCons_BIT";
    1.23 +val number_of_Pls = thm"number_of_Pls";
    1.24 +val number_of_Min = thm"number_of_Min";
    1.25 +val number_of_BIT = thm"number_of_BIT";
    1.26 +val bin_succ_Pls = thm"bin_succ_Pls";
    1.27 +val bin_succ_Min = thm"bin_succ_Min";
    1.28 +val bin_succ_BIT = thm"bin_succ_BIT";
    1.29 +val bin_pred_Pls = thm"bin_pred_Pls";
    1.30 +val bin_pred_Min = thm"bin_pred_Min";
    1.31 +val bin_pred_BIT = thm"bin_pred_BIT";
    1.32 +val bin_minus_Pls = thm"bin_minus_Pls";
    1.33 +val bin_minus_Min = thm"bin_minus_Min";
    1.34 +val bin_minus_BIT = thm"bin_minus_BIT";
    1.35 +val bin_add_Pls = thm"bin_add_Pls";
    1.36 +val bin_add_Min = thm"bin_add_Min";
    1.37 +val bin_mult_Pls = thm"bin_mult_Pls";
    1.38 +val bin_mult_Min = thm"bin_mult_Min";
    1.39 +val bin_mult_BIT = thm"bin_mult_BIT";
    1.40  
    1.41 -Goal "(x = y) = (x-y = (0::int))";
    1.42 -by (simp_tac (simpset() addsimps compare_rls) 1);
    1.43 -qed "eq_iff_zdiff_eq_0";
    1.44 +val zadd_ac = thms "Ring_and_Field.add_ac"
    1.45 +val zmult_ac = thms "Ring_and_Field.mult_ac"
    1.46 +val NCons_Pls_0 = thm"NCons_Pls_0";
    1.47 +val NCons_Pls_1 = thm"NCons_Pls_1";
    1.48 +val NCons_Min_0 = thm"NCons_Min_0";
    1.49 +val NCons_Min_1 = thm"NCons_Min_1";
    1.50 +val bin_succ_1 = thm"bin_succ_1";
    1.51 +val bin_succ_0 = thm"bin_succ_0";
    1.52 +val bin_pred_1 = thm"bin_pred_1";
    1.53 +val bin_pred_0 = thm"bin_pred_0";
    1.54 +val bin_minus_1 = thm"bin_minus_1";
    1.55 +val bin_minus_0 = thm"bin_minus_0";
    1.56 +val bin_add_BIT_11 = thm"bin_add_BIT_11";
    1.57 +val bin_add_BIT_10 = thm"bin_add_BIT_10";
    1.58 +val bin_add_BIT_0 = thm"bin_add_BIT_0";
    1.59 +val bin_add_Pls_right = thm"bin_add_Pls_right";
    1.60 +val bin_add_Min_right = thm"bin_add_Min_right";
    1.61 +val bin_add_BIT_BIT = thm"bin_add_BIT_BIT";
    1.62 +val bin_mult_1 = thm"bin_mult_1";
    1.63 +val bin_mult_0 = thm"bin_mult_0";
    1.64 +val number_of_NCons = thm"number_of_NCons";
    1.65 +val number_of_succ = thm"number_of_succ";
    1.66 +val number_of_pred = thm"number_of_pred";
    1.67 +val number_of_minus = thm"number_of_minus";
    1.68 +val number_of_add = thm"number_of_add";
    1.69 +val diff_number_of_eq = thm"diff_number_of_eq";
    1.70 +val number_of_mult = thm"number_of_mult";
    1.71 +val double_number_of_BIT = thm"double_number_of_BIT";
    1.72 +val int_numeral_0_eq_0 = thm"int_numeral_0_eq_0";
    1.73 +val int_numeral_1_eq_1 = thm"int_numeral_1_eq_1";
    1.74 +val zmult_minus1 = thm"zmult_minus1";
    1.75 +val zmult_minus1_right = thm"zmult_minus1_right";
    1.76 +val zminus_number_of_zmult = thm"zminus_number_of_zmult";
    1.77 +val zminus_1_eq_m1 = thm"zminus_1_eq_m1";
    1.78 +val zero_less_nat_eq = thm"zero_less_nat_eq";
    1.79 +val eq_number_of_eq = thm"eq_number_of_eq";
    1.80 +val iszero_number_of_Pls = thm"iszero_number_of_Pls";
    1.81 +val nonzero_number_of_Min = thm"nonzero_number_of_Min";
    1.82 +val iszero_number_of_BIT = thm"iszero_number_of_BIT";
    1.83 +val iszero_number_of_0 = thm"iszero_number_of_0";
    1.84 +val iszero_number_of_1 = thm"iszero_number_of_1";
    1.85 +val less_number_of_eq_neg = thm"less_number_of_eq_neg";
    1.86 +val not_neg_number_of_Pls = thm"not_neg_number_of_Pls";
    1.87 +val neg_number_of_Min = thm"neg_number_of_Min";
    1.88 +val neg_number_of_BIT = thm"neg_number_of_BIT";
    1.89 +val le_number_of_eq_not_less = thm"le_number_of_eq_not_less";
    1.90 +val zabs_number_of = thm"zabs_number_of";
    1.91 +val zabs_0 = thm"zabs_0";
    1.92 +val zabs_1 = thm"zabs_1";
    1.93 +val number_of_reorient = thm"number_of_reorient";
    1.94 +val add_number_of_left = thm"add_number_of_left";
    1.95 +val mult_number_of_left = thm"mult_number_of_left";
    1.96 +val add_number_of_diff1 = thm"add_number_of_diff1";
    1.97 +val add_number_of_diff2 = thm"add_number_of_diff2";
    1.98 +val less_iff_diff_less_0 = thm"less_iff_diff_less_0";
    1.99 +val eq_iff_diff_eq_0 = thm"eq_iff_diff_eq_0";
   1.100 +val le_iff_diff_le_0 = thm"le_iff_diff_le_0";
   1.101  
   1.102 -Goal "(x <= y) = (x-y <= (0::int))";
   1.103 -by (simp_tac (simpset() addsimps compare_rls) 1);
   1.104 -qed "zle_iff_zdiff_zle_0";
   1.105 +val bin_mult_simps = thms"bin_mult_simps";
   1.106 +val NCons_simps = thms"NCons_simps";
   1.107 +val bin_arith_extra_simps = thms"bin_arith_extra_simps";
   1.108 +val bin_arith_simps = thms"bin_arith_simps";
   1.109 +val bin_rel_simps = thms"bin_rel_simps";
   1.110  
   1.111 +val zless_imp_add1_zle = thm "zless_imp_add1_zle";
   1.112  
   1.113 -(** For combine_numerals **)
   1.114 -
   1.115 -Goal "i*u + (j*u + k) = (i+j)*u + (k::int)";
   1.116 -by (asm_simp_tac (simpset() addsimps [zadd_zmult_distrib]) 1);
   1.117 -qed "left_zadd_zmult_distrib";
   1.118 +val combine_common_factor = thm"combine_common_factor";
   1.119 +val eq_add_iff1 = thm"eq_add_iff1";
   1.120 +val eq_add_iff2 = thm"eq_add_iff2";
   1.121 +val less_add_iff1 = thm"less_add_iff1";
   1.122 +val less_add_iff2 = thm"less_add_iff2";
   1.123 +val le_add_iff1 = thm"le_add_iff1";
   1.124 +val le_add_iff2 = thm"le_add_iff2";
   1.125  
   1.126  
   1.127 -(** For cancel_numerals **)
   1.128 +structure Bin_Simprocs =
   1.129 +  struct
   1.130 +  fun prove_conv tacs sg (hyps: thm list) xs (t, u) =
   1.131 +    if t aconv u then None
   1.132 +    else
   1.133 +      let val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u))
   1.134 +      in Some (Tactic.prove sg xs [] eq (K (EVERY tacs))) end
   1.135  
   1.136 -val rel_iff_rel_0_rls = map (inst "y" "?u+?v")
   1.137 -                          [zless_iff_zdiff_zless_0, eq_iff_zdiff_eq_0,
   1.138 -                           zle_iff_zdiff_zle_0] @
   1.139 -                        map (inst "y" "n")
   1.140 -                          [zless_iff_zdiff_zless_0, eq_iff_zdiff_eq_0,
   1.141 -                           zle_iff_zdiff_zle_0];
   1.142 +  fun prove_conv_nohyps tacs sg = prove_conv tacs sg [];
   1.143 +  fun prove_conv_nohyps_novars tacs sg = prove_conv tacs sg [] [];
   1.144 +
   1.145 +  fun prep_simproc (name, pats, proc) =
   1.146 +    Simplifier.simproc (Theory.sign_of (the_context())) name pats proc;
   1.147 +
   1.148 +  fun is_numeral (Const("Numeral.number_of", _) $ w) = true
   1.149 +    | is_numeral _ = false
   1.150  
   1.151 -Goal "!!i::int. (i*u + m = j*u + n) = ((i-j)*u + m = n)";
   1.152 -by (asm_simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]@
   1.153 -                                     zadd_ac@rel_iff_rel_0_rls) 1);
   1.154 -qed "eq_add_iff1";
   1.155 +  fun simplify_meta_eq f_number_of_eq f_eq =
   1.156 +      mk_meta_eq ([f_eq, f_number_of_eq] MRS trans)
   1.157  
   1.158 -Goal "!!i::int. (i*u + m = j*u + n) = (m = (j-i)*u + n)";
   1.159 -by (asm_simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]@
   1.160 -                                     zadd_ac@rel_iff_rel_0_rls) 1);
   1.161 -qed "eq_add_iff2";
   1.162 +  structure IntAbstractNumeralsData =
   1.163 +    struct
   1.164 +    val dest_eq		= HOLogic.dest_eq o HOLogic.dest_Trueprop o concl_of
   1.165 +    val is_numeral	= is_numeral
   1.166 +    val numeral_0_eq_0    = int_numeral_0_eq_0
   1.167 +    val numeral_1_eq_1    = int_numeral_1_eq_1
   1.168 +    val prove_conv	= prove_conv_nohyps_novars
   1.169 +    fun norm_tac simps	= ALLGOALS (simp_tac (HOL_ss addsimps simps))
   1.170 +    val simplify_meta_eq  = simplify_meta_eq 
   1.171 +    end
   1.172 +
   1.173 +  structure IntAbstractNumerals = AbstractNumeralsFun (IntAbstractNumeralsData)
   1.174 +
   1.175  
   1.176 -Goal "!!i::int. (i*u + m < j*u + n) = ((i-j)*u + m < n)";
   1.177 -by (asm_simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]@
   1.178 -                                     zadd_ac@rel_iff_rel_0_rls) 1);
   1.179 -qed "less_add_iff1";
   1.180 -
   1.181 -Goal "!!i::int. (i*u + m < j*u + n) = (m < (j-i)*u + n)";
   1.182 -by (asm_simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]@
   1.183 -                                     zadd_ac@rel_iff_rel_0_rls) 1);
   1.184 -qed "less_add_iff2";
   1.185 +  (*For addition, we already have rules for the operand 0.
   1.186 +    Multiplication is omitted because there are already special rules for 
   1.187 +    both 0 and 1 as operands.  Unary minus is trivial, just have - 1 = -1.
   1.188 +    For the others, having three patterns is a compromise between just having
   1.189 +    one (many spurious calls) and having nine (just too many!) *)
   1.190 +  val eval_numerals = 
   1.191 +    map prep_simproc
   1.192 +     [("int_add_eval_numerals",
   1.193 +       ["(m::int) + 1", "(m::int) + number_of v"], 
   1.194 +       IntAbstractNumerals.proc (number_of_add RS sym)),
   1.195 +      ("int_diff_eval_numerals",
   1.196 +       ["(m::int) - 1", "(m::int) - number_of v"], 
   1.197 +       IntAbstractNumerals.proc diff_number_of_eq),
   1.198 +      ("int_eq_eval_numerals",
   1.199 +       ["(m::int) = 0", "(m::int) = 1", "(m::int) = number_of v"], 
   1.200 +       IntAbstractNumerals.proc eq_number_of_eq),
   1.201 +      ("int_less_eval_numerals",
   1.202 +       ["(m::int) < 0", "(m::int) < 1", "(m::int) < number_of v"], 
   1.203 +       IntAbstractNumerals.proc less_number_of_eq_neg),
   1.204 +      ("int_le_eval_numerals",
   1.205 +       ["(m::int) <= 0", "(m::int) <= 1", "(m::int) <= number_of v"],
   1.206 +       IntAbstractNumerals.proc le_number_of_eq_not_less)]
   1.207  
   1.208 -Goal "!!i::int. (i*u + m <= j*u + n) = ((i-j)*u + m <= n)";
   1.209 -by (asm_simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]@
   1.210 -                                     zadd_ac@rel_iff_rel_0_rls) 1);
   1.211 -qed "le_add_iff1";
   1.212 +  (*reorientation simprules using ==, for the following simproc*)
   1.213 +  val meta_zero_reorient = zero_reorient RS eq_reflection
   1.214 +  val meta_one_reorient = one_reorient RS eq_reflection
   1.215 +  val meta_number_of_reorient = number_of_reorient RS eq_reflection
   1.216  
   1.217 -Goal "!!i::int. (i*u + m <= j*u + n) = (m <= (j-i)*u + n)";
   1.218 -by (asm_simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]
   1.219 -                                     @zadd_ac@rel_iff_rel_0_rls) 1);
   1.220 -qed "le_add_iff2";
   1.221 +  (*reorientation simplification procedure: reorients (polymorphic) 
   1.222 +    0 = x, 1 = x, nnn = x provided x isn't 0, 1 or a numeral.*)
   1.223 +  fun reorient_proc sg _ (_ $ t $ u) =
   1.224 +    case u of
   1.225 +	Const("0", _) => None
   1.226 +      | Const("1", _) => None
   1.227 +      | Const("Numeral.number_of", _) $ _ => None
   1.228 +      | _ => Some (case t of
   1.229 +		  Const("0", _) => meta_zero_reorient
   1.230 +		| Const("1", _) => meta_one_reorient
   1.231 +		| Const("Numeral.number_of", _) $ _ => meta_number_of_reorient)
   1.232 +
   1.233 +  val reorient_simproc = 
   1.234 +      prep_simproc ("reorient_simproc", ["0=x", "1=x", "number_of w = x"], reorient_proc)
   1.235 +
   1.236 +  end;
   1.237 +
   1.238 +
   1.239 +Addsimprocs Bin_Simprocs.eval_numerals;
   1.240 +Addsimprocs [Bin_Simprocs.reorient_simproc];
   1.241  
   1.242  
   1.243  structure Int_Numeral_Simprocs =
   1.244 @@ -285,7 +395,7 @@
   1.245    val dest_sum          = dest_sum
   1.246    val mk_coeff          = mk_coeff
   1.247    val dest_coeff        = dest_coeff 1
   1.248 -  val left_distrib      = left_zadd_zmult_distrib RS trans
   1.249 +  val left_distrib      = combine_common_factor RS trans
   1.250    val prove_conv        = Bin_Simprocs.prove_conv_nohyps
   1.251    val trans_tac          = trans_tac
   1.252    val norm_tac =
   1.253 @@ -436,7 +546,7 @@
   1.254     {add_mono_thms = add_mono_thms @ add_mono_thms_int,
   1.255      mult_mono_thms = mult_mono_thms,
   1.256      inj_thms = [zle_int RS iffD2,int_int_eq RS iffD2] @ inj_thms,
   1.257 -    lessD = lessD @ [add1_zle_eq RS iffD2],
   1.258 +    lessD = lessD @ [zless_imp_add1_zle],
   1.259      simpset = simpset addsimps add_rules
   1.260                        addsimprocs simprocs
   1.261                        addcongs [if_weak_cong]}),