src/HOL/Integ/int_arith1.ML
changeset 15013 34264f5e4691
parent 14738 83f1a514dcb4
child 15184 d2c19aea17bc
     1.1 --- a/src/HOL/Integ/int_arith1.ML	Wed Jun 30 14:04:58 2004 +0200
     1.2 +++ b/src/HOL/Integ/int_arith1.ML	Thu Jul 01 12:29:53 2004 +0200
     1.3 @@ -7,49 +7,37 @@
     1.4  
     1.5  (** Misc ML bindings **)
     1.6  
     1.7 -val NCons_Pls = thm"NCons_Pls";
     1.8 -val NCons_Min = thm"NCons_Min";
     1.9 -val NCons_BIT = thm"NCons_BIT";
    1.10 -val number_of_Pls = thm"number_of_Pls";
    1.11 -val number_of_Min = thm"number_of_Min";
    1.12 -val number_of_BIT = thm"number_of_BIT";
    1.13  val bin_succ_Pls = thm"bin_succ_Pls";
    1.14  val bin_succ_Min = thm"bin_succ_Min";
    1.15 -val bin_succ_BIT = thm"bin_succ_BIT";
    1.16 +val bin_succ_1 = thm"bin_succ_1";
    1.17 +val bin_succ_0 = thm"bin_succ_0";
    1.18 +
    1.19  val bin_pred_Pls = thm"bin_pred_Pls";
    1.20  val bin_pred_Min = thm"bin_pred_Min";
    1.21 -val bin_pred_BIT = thm"bin_pred_BIT";
    1.22 +val bin_pred_1 = thm"bin_pred_1";
    1.23 +val bin_pred_0 = thm"bin_pred_0";
    1.24 +
    1.25  val bin_minus_Pls = thm"bin_minus_Pls";
    1.26  val bin_minus_Min = thm"bin_minus_Min";
    1.27 -val bin_minus_BIT = thm"bin_minus_BIT";
    1.28 +val bin_minus_1 = thm"bin_minus_1";
    1.29 +val bin_minus_0 = thm"bin_minus_0";
    1.30 +
    1.31  val bin_add_Pls = thm"bin_add_Pls";
    1.32  val bin_add_Min = thm"bin_add_Min";
    1.33 -val bin_mult_Pls = thm"bin_mult_Pls";
    1.34 -val bin_mult_Min = thm"bin_mult_Min";
    1.35 -val bin_mult_BIT = thm"bin_mult_BIT";
    1.36 -
    1.37 -val neg_def = thm "neg_def";
    1.38 -val iszero_def = thm "iszero_def";
    1.39 -
    1.40 -val NCons_Pls_0 = thm"NCons_Pls_0";
    1.41 -val NCons_Pls_1 = thm"NCons_Pls_1";
    1.42 -val NCons_Min_0 = thm"NCons_Min_0";
    1.43 -val NCons_Min_1 = thm"NCons_Min_1";
    1.44 -val bin_succ_1 = thm"bin_succ_1";
    1.45 -val bin_succ_0 = thm"bin_succ_0";
    1.46 -val bin_pred_1 = thm"bin_pred_1";
    1.47 -val bin_pred_0 = thm"bin_pred_0";
    1.48 -val bin_minus_1 = thm"bin_minus_1";
    1.49 -val bin_minus_0 = thm"bin_minus_0";
    1.50  val bin_add_BIT_11 = thm"bin_add_BIT_11";
    1.51  val bin_add_BIT_10 = thm"bin_add_BIT_10";
    1.52  val bin_add_BIT_0 = thm"bin_add_BIT_0";
    1.53  val bin_add_Pls_right = thm"bin_add_Pls_right";
    1.54  val bin_add_Min_right = thm"bin_add_Min_right";
    1.55 -val bin_add_BIT_BIT = thm"bin_add_BIT_BIT";
    1.56 +
    1.57 +val bin_mult_Pls = thm"bin_mult_Pls";
    1.58 +val bin_mult_Min = thm"bin_mult_Min";
    1.59  val bin_mult_1 = thm"bin_mult_1";
    1.60  val bin_mult_0 = thm"bin_mult_0";
    1.61 -val number_of_NCons = thm"number_of_NCons";
    1.62 +
    1.63 +val neg_def = thm "neg_def";
    1.64 +val iszero_def = thm "iszero_def";
    1.65 +
    1.66  val number_of_succ = thm"number_of_succ";
    1.67  val number_of_pred = thm"number_of_pred";
    1.68  val number_of_minus = thm"number_of_minus";
    1.69 @@ -86,7 +74,6 @@
    1.70  val eq_iff_diff_eq_0 = thm"eq_iff_diff_eq_0";
    1.71  val le_iff_diff_le_0 = thm"le_iff_diff_le_0";
    1.72  
    1.73 -val NCons_simps = thms"NCons_simps";
    1.74  val bin_arith_extra_simps = thms"bin_arith_extra_simps";
    1.75  val bin_arith_simps = thms"bin_arith_simps";
    1.76  val bin_rel_simps = thms"bin_rel_simps";
    1.77 @@ -298,10 +285,9 @@
    1.78      bin_simps \\ [add_number_of_left, number_of_add RS sym];
    1.79  
    1.80  (*To evaluate binary negations of coefficients*)
    1.81 -val minus_simps = NCons_simps @
    1.82 -                   [numeral_m1_eq_minus_1 RS sym, number_of_minus RS sym,
    1.83 -                    bin_minus_1, bin_minus_0, bin_minus_Pls, bin_minus_Min,
    1.84 -                    bin_pred_1, bin_pred_0, bin_pred_Pls, bin_pred_Min];
    1.85 +val minus_simps = [numeral_m1_eq_minus_1 RS sym, number_of_minus RS sym,
    1.86 +                   bin_minus_1, bin_minus_0, bin_minus_Pls, bin_minus_Min,
    1.87 +                   bin_pred_1, bin_pred_0, bin_pred_Pls, bin_pred_Min];
    1.88  
    1.89  (*To let us treat subtraction as addition*)
    1.90  val diff_simps = [diff_minus, minus_add_distrib, minus_minus];
    1.91 @@ -335,10 +321,10 @@
    1.92    val find_first_coeff  = find_first_coeff []
    1.93    val trans_tac         = trans_tac
    1.94    val norm_tac =
    1.95 -     ALLGOALS (simp_tac (HOL_ss addsimps numeral_syms@add_0s@mult_1s@
    1.96 +     ALLGOALS (simp_tac (num_ss addsimps numeral_syms@add_0s@mult_1s@
    1.97                                           diff_simps@minus_simps@add_ac))
    1.98 -     THEN ALLGOALS (simp_tac (HOL_ss addsimps non_add_bin_simps@mult_minus_simps))
    1.99 -     THEN ALLGOALS (simp_tac (HOL_ss addsimps minus_from_mult_simps@
   1.100 +     THEN ALLGOALS (simp_tac (num_ss addsimps non_add_bin_simps@mult_minus_simps))
   1.101 +     THEN ALLGOALS (simp_tac (num_ss addsimps minus_from_mult_simps@
   1.102                                                add_ac@mult_ac))
   1.103    val numeral_simp_tac  = ALLGOALS (simp_tac (HOL_ss addsimps add_0s@bin_simps))
   1.104    val simplify_meta_eq  = simplify_meta_eq (add_0s@mult_1s)
   1.105 @@ -411,10 +397,10 @@
   1.106    val prove_conv        = Bin_Simprocs.prove_conv_nohyps
   1.107    val trans_tac          = trans_tac
   1.108    val norm_tac =
   1.109 -     ALLGOALS (simp_tac (HOL_ss addsimps numeral_syms@add_0s@mult_1s@
   1.110 +     ALLGOALS (simp_tac (num_ss addsimps numeral_syms@add_0s@mult_1s@
   1.111                                           diff_simps@minus_simps@add_ac))
   1.112 -     THEN ALLGOALS (simp_tac (HOL_ss addsimps non_add_bin_simps@mult_minus_simps))
   1.113 -     THEN ALLGOALS (simp_tac (HOL_ss addsimps minus_from_mult_simps@
   1.114 +     THEN ALLGOALS (simp_tac (num_ss addsimps non_add_bin_simps@mult_minus_simps))
   1.115 +     THEN ALLGOALS (simp_tac (num_ss addsimps minus_from_mult_simps@
   1.116                                                add_ac@mult_ac))
   1.117    val numeral_simp_tac  = ALLGOALS
   1.118                      (simp_tac (HOL_ss addsimps add_0s@bin_simps))