src/HOL/Ring_and_Field.thy
changeset 22548 6ce4bddf3bcb
parent 22452 8a86fd2a1bf0
child 22842 6d2fd4e0f984
     1.1 --- a/src/HOL/Ring_and_Field.thy	Thu Mar 29 11:59:54 2007 +0200
     1.2 +++ b/src/HOL/Ring_and_Field.thy	Thu Mar 29 14:21:45 2007 +0200
     1.3 @@ -2067,210 +2067,4 @@
     1.4    then show ?thesis by simp
     1.5  qed
     1.6  
     1.7 -ML {*
     1.8 -val left_distrib = thm "left_distrib";
     1.9 -val right_distrib = thm "right_distrib";
    1.10 -val mult_commute = thm "mult_commute";
    1.11 -val distrib = thm "distrib";
    1.12 -val zero_neq_one = thm "zero_neq_one";
    1.13 -val no_zero_divisors = thm "no_zero_divisors";
    1.14 -val left_inverse = thm "left_inverse";
    1.15 -val divide_inverse = thm "divide_inverse";
    1.16 -val mult_zero_left = thm "mult_zero_left";
    1.17 -val mult_zero_right = thm "mult_zero_right";
    1.18 -val field_mult_eq_0_iff = thm "field_mult_eq_0_iff";
    1.19 -val inverse_zero = thm "inverse_zero";
    1.20 -val ring_distrib = thms "ring_distrib";
    1.21 -val combine_common_factor = thm "combine_common_factor";
    1.22 -val minus_mult_left = thm "minus_mult_left";
    1.23 -val minus_mult_right = thm "minus_mult_right";
    1.24 -val minus_mult_minus = thm "minus_mult_minus";
    1.25 -val minus_mult_commute = thm "minus_mult_commute";
    1.26 -val right_diff_distrib = thm "right_diff_distrib";
    1.27 -val left_diff_distrib = thm "left_diff_distrib";
    1.28 -val mult_left_mono = thm "mult_left_mono";
    1.29 -val mult_right_mono = thm "mult_right_mono";
    1.30 -val mult_strict_left_mono = thm "mult_strict_left_mono";
    1.31 -val mult_strict_right_mono = thm "mult_strict_right_mono";
    1.32 -val mult_mono = thm "mult_mono";
    1.33 -val mult_strict_mono = thm "mult_strict_mono";
    1.34 -val abs_if = thm "abs_if";
    1.35 -val zero_less_one = thm "zero_less_one";
    1.36 -val eq_add_iff1 = thm "eq_add_iff1";
    1.37 -val eq_add_iff2 = thm "eq_add_iff2";
    1.38 -val less_add_iff1 = thm "less_add_iff1";
    1.39 -val less_add_iff2 = thm "less_add_iff2";
    1.40 -val le_add_iff1 = thm "le_add_iff1";
    1.41 -val le_add_iff2 = thm "le_add_iff2";
    1.42 -val mult_left_le_imp_le = thm "mult_left_le_imp_le";
    1.43 -val mult_right_le_imp_le = thm "mult_right_le_imp_le";
    1.44 -val mult_left_less_imp_less = thm "mult_left_less_imp_less";
    1.45 -val mult_right_less_imp_less = thm "mult_right_less_imp_less";
    1.46 -val mult_strict_left_mono_neg = thm "mult_strict_left_mono_neg";
    1.47 -val mult_left_mono_neg = thm "mult_left_mono_neg";
    1.48 -val mult_strict_right_mono_neg = thm "mult_strict_right_mono_neg";
    1.49 -val mult_right_mono_neg = thm "mult_right_mono_neg";
    1.50 -(*
    1.51 -val mult_pos = thm "mult_pos";
    1.52 -val mult_pos_le = thm "mult_pos_le";
    1.53 -val mult_pos_neg = thm "mult_pos_neg";
    1.54 -val mult_pos_neg_le = thm "mult_pos_neg_le";
    1.55 -val mult_pos_neg2 = thm "mult_pos_neg2";
    1.56 -val mult_pos_neg2_le = thm "mult_pos_neg2_le";
    1.57 -val mult_neg = thm "mult_neg";
    1.58 -val mult_neg_le = thm "mult_neg_le";
    1.59 -*)
    1.60 -val zero_less_mult_pos = thm "zero_less_mult_pos";
    1.61 -val zero_less_mult_pos2 = thm "zero_less_mult_pos2";
    1.62 -val zero_less_mult_iff = thm "zero_less_mult_iff";
    1.63 -val mult_eq_0_iff = thm "mult_eq_0_iff";
    1.64 -val zero_le_mult_iff = thm "zero_le_mult_iff";
    1.65 -val mult_less_0_iff = thm "mult_less_0_iff";
    1.66 -val mult_le_0_iff = thm "mult_le_0_iff";
    1.67 -val split_mult_pos_le = thm "split_mult_pos_le";
    1.68 -val split_mult_neg_le = thm "split_mult_neg_le";
    1.69 -val zero_le_square = thm "zero_le_square";
    1.70 -val zero_le_one = thm "zero_le_one";
    1.71 -val not_one_le_zero = thm "not_one_le_zero";
    1.72 -val not_one_less_zero = thm "not_one_less_zero";
    1.73 -val mult_left_mono_neg = thm "mult_left_mono_neg";
    1.74 -val mult_right_mono_neg = thm "mult_right_mono_neg";
    1.75 -val mult_strict_mono = thm "mult_strict_mono";
    1.76 -val mult_strict_mono' = thm "mult_strict_mono'";
    1.77 -val mult_mono = thm "mult_mono";
    1.78 -val less_1_mult = thm "less_1_mult";
    1.79 -val mult_less_cancel_right_disj = thm "mult_less_cancel_right_disj";
    1.80 -val mult_less_cancel_left_disj = thm "mult_less_cancel_left_disj";
    1.81 -val mult_less_cancel_right = thm "mult_less_cancel_right";
    1.82 -val mult_less_cancel_left = thm "mult_less_cancel_left";
    1.83 -val mult_le_cancel_right = thm "mult_le_cancel_right";
    1.84 -val mult_le_cancel_left = thm "mult_le_cancel_left";
    1.85 -val mult_less_imp_less_left = thm "mult_less_imp_less_left";
    1.86 -val mult_less_imp_less_right = thm "mult_less_imp_less_right";
    1.87 -val mult_cancel_right = thm "mult_cancel_right";
    1.88 -val mult_cancel_left = thm "mult_cancel_left";
    1.89 -val ring_eq_simps = thms "ring_eq_simps";
    1.90 -val right_inverse = thm "right_inverse";
    1.91 -val right_inverse_eq = thm "right_inverse_eq";
    1.92 -val nonzero_inverse_eq_divide = thm "nonzero_inverse_eq_divide";
    1.93 -val divide_self = thm "divide_self";
    1.94 -val divide_zero = thm "divide_zero";
    1.95 -val divide_zero_left = thm "divide_zero_left";
    1.96 -val inverse_eq_divide = thm "inverse_eq_divide";
    1.97 -val add_divide_distrib = thm "add_divide_distrib";
    1.98 -val field_mult_eq_0_iff = thm "field_mult_eq_0_iff";
    1.99 -val field_mult_cancel_right_lemma = thm "field_mult_cancel_right_lemma";
   1.100 -val field_mult_cancel_right = thm "field_mult_cancel_right";
   1.101 -val field_mult_cancel_left = thm "field_mult_cancel_left";
   1.102 -val nonzero_imp_inverse_nonzero = thm "nonzero_imp_inverse_nonzero";
   1.103 -val inverse_zero_imp_zero = thm "inverse_zero_imp_zero";
   1.104 -val inverse_nonzero_imp_nonzero = thm "inverse_nonzero_imp_nonzero";
   1.105 -val inverse_nonzero_iff_nonzero = thm "inverse_nonzero_iff_nonzero";
   1.106 -val nonzero_inverse_minus_eq = thm "nonzero_inverse_minus_eq";
   1.107 -val inverse_minus_eq = thm "inverse_minus_eq";
   1.108 -val nonzero_inverse_eq_imp_eq = thm "nonzero_inverse_eq_imp_eq";
   1.109 -val inverse_eq_imp_eq = thm "inverse_eq_imp_eq";
   1.110 -val inverse_eq_iff_eq = thm "inverse_eq_iff_eq";
   1.111 -val nonzero_inverse_inverse_eq = thm "nonzero_inverse_inverse_eq";
   1.112 -val inverse_inverse_eq = thm "inverse_inverse_eq";
   1.113 -val inverse_1 = thm "inverse_1";
   1.114 -val nonzero_inverse_mult_distrib = thm "nonzero_inverse_mult_distrib";
   1.115 -val inverse_mult_distrib = thm "inverse_mult_distrib";
   1.116 -val inverse_add = thm "inverse_add";
   1.117 -val inverse_divide = thm "inverse_divide";
   1.118 -val nonzero_mult_divide_cancel_left = thm "nonzero_mult_divide_cancel_left";
   1.119 -val mult_divide_cancel_left = thm "mult_divide_cancel_left";
   1.120 -val nonzero_mult_divide_cancel_right = thm "nonzero_mult_divide_cancel_right";
   1.121 -val mult_divide_cancel_right = thm "mult_divide_cancel_right";
   1.122 -val mult_divide_cancel_eq_if = thm "mult_divide_cancel_eq_if";
   1.123 -val divide_1 = thm "divide_1";
   1.124 -val times_divide_eq_right = thm "times_divide_eq_right";
   1.125 -val times_divide_eq_left = thm "times_divide_eq_left";
   1.126 -val divide_divide_eq_right = thm "divide_divide_eq_right";
   1.127 -val divide_divide_eq_left = thm "divide_divide_eq_left";
   1.128 -val nonzero_minus_divide_left = thm "nonzero_minus_divide_left";
   1.129 -val nonzero_minus_divide_right = thm "nonzero_minus_divide_right";
   1.130 -val nonzero_minus_divide_divide = thm "nonzero_minus_divide_divide";
   1.131 -val minus_divide_left = thm "minus_divide_left";
   1.132 -val minus_divide_right = thm "minus_divide_right";
   1.133 -val minus_divide_divide = thm "minus_divide_divide";
   1.134 -val diff_divide_distrib = thm "diff_divide_distrib";
   1.135 -val positive_imp_inverse_positive = thm "positive_imp_inverse_positive";
   1.136 -val negative_imp_inverse_negative = thm "negative_imp_inverse_negative";
   1.137 -val inverse_le_imp_le = thm "inverse_le_imp_le";
   1.138 -val inverse_positive_imp_positive = thm "inverse_positive_imp_positive";
   1.139 -val inverse_positive_iff_positive = thm "inverse_positive_iff_positive";
   1.140 -val inverse_negative_imp_negative = thm "inverse_negative_imp_negative";
   1.141 -val inverse_negative_iff_negative = thm "inverse_negative_iff_negative";
   1.142 -val inverse_nonnegative_iff_nonnegative = thm "inverse_nonnegative_iff_nonnegative";
   1.143 -val inverse_nonpositive_iff_nonpositive = thm "inverse_nonpositive_iff_nonpositive";
   1.144 -val less_imp_inverse_less = thm "less_imp_inverse_less";
   1.145 -val inverse_less_imp_less = thm "inverse_less_imp_less";
   1.146 -val inverse_less_iff_less = thm "inverse_less_iff_less";
   1.147 -val le_imp_inverse_le = thm "le_imp_inverse_le";
   1.148 -val inverse_le_iff_le = thm "inverse_le_iff_le";
   1.149 -val inverse_le_imp_le_neg = thm "inverse_le_imp_le_neg";
   1.150 -val less_imp_inverse_less_neg = thm "less_imp_inverse_less_neg";
   1.151 -val inverse_less_imp_less_neg = thm "inverse_less_imp_less_neg";
   1.152 -val inverse_less_iff_less_neg = thm "inverse_less_iff_less_neg";
   1.153 -val le_imp_inverse_le_neg = thm "le_imp_inverse_le_neg";
   1.154 -val inverse_le_iff_le_neg = thm "inverse_le_iff_le_neg";
   1.155 -val one_less_inverse_iff = thm "one_less_inverse_iff";
   1.156 -val inverse_eq_1_iff = thm "inverse_eq_1_iff";
   1.157 -val one_le_inverse_iff = thm "one_le_inverse_iff";
   1.158 -val inverse_less_1_iff = thm "inverse_less_1_iff";
   1.159 -val inverse_le_1_iff = thm "inverse_le_1_iff";
   1.160 -val zero_less_divide_iff = thm "zero_less_divide_iff";
   1.161 -val divide_less_0_iff = thm "divide_less_0_iff";
   1.162 -val zero_le_divide_iff = thm "zero_le_divide_iff";
   1.163 -val divide_le_0_iff = thm "divide_le_0_iff";
   1.164 -val divide_eq_0_iff = thm "divide_eq_0_iff";
   1.165 -val pos_le_divide_eq = thm "pos_le_divide_eq";
   1.166 -val neg_le_divide_eq = thm "neg_le_divide_eq";
   1.167 -val le_divide_eq = thm "le_divide_eq";
   1.168 -val pos_divide_le_eq = thm "pos_divide_le_eq";
   1.169 -val neg_divide_le_eq = thm "neg_divide_le_eq";
   1.170 -val divide_le_eq = thm "divide_le_eq";
   1.171 -val pos_less_divide_eq = thm "pos_less_divide_eq";
   1.172 -val neg_less_divide_eq = thm "neg_less_divide_eq";
   1.173 -val less_divide_eq = thm "less_divide_eq";
   1.174 -val pos_divide_less_eq = thm "pos_divide_less_eq";
   1.175 -val neg_divide_less_eq = thm "neg_divide_less_eq";
   1.176 -val divide_less_eq = thm "divide_less_eq";
   1.177 -val nonzero_eq_divide_eq = thm "nonzero_eq_divide_eq";
   1.178 -val eq_divide_eq = thm "eq_divide_eq";
   1.179 -val nonzero_divide_eq_eq = thm "nonzero_divide_eq_eq";
   1.180 -val divide_eq_eq = thm "divide_eq_eq";
   1.181 -val divide_cancel_right = thm "divide_cancel_right";
   1.182 -val divide_cancel_left = thm "divide_cancel_left";
   1.183 -val divide_eq_1_iff = thm "divide_eq_1_iff";
   1.184 -val one_eq_divide_iff = thm "one_eq_divide_iff";
   1.185 -val zero_eq_1_divide_iff = thm "zero_eq_1_divide_iff";
   1.186 -val one_divide_eq_0_iff = thm "one_divide_eq_0_iff";
   1.187 -val divide_strict_right_mono = thm "divide_strict_right_mono";
   1.188 -val divide_right_mono = thm "divide_right_mono";
   1.189 -val divide_strict_left_mono = thm "divide_strict_left_mono";
   1.190 -val divide_left_mono = thm "divide_left_mono";
   1.191 -val divide_strict_left_mono_neg = thm "divide_strict_left_mono_neg";
   1.192 -val divide_strict_right_mono_neg = thm "divide_strict_right_mono_neg";
   1.193 -val less_add_one = thm "less_add_one";
   1.194 -val zero_less_two = thm "zero_less_two";
   1.195 -val less_half_sum = thm "less_half_sum";
   1.196 -val gt_half_sum = thm "gt_half_sum";
   1.197 -val dense = thm "dense";
   1.198 -val abs_one = thm "abs_one";
   1.199 -val abs_le_mult = thm "abs_le_mult";
   1.200 -val abs_eq_mult = thm "abs_eq_mult";
   1.201 -val abs_mult = thm "abs_mult";
   1.202 -val abs_mult_self = thm "abs_mult_self";
   1.203 -val nonzero_abs_inverse = thm "nonzero_abs_inverse";
   1.204 -val abs_inverse = thm "abs_inverse";
   1.205 -val nonzero_abs_divide = thm "nonzero_abs_divide";
   1.206 -val abs_divide = thm "abs_divide";
   1.207 -val abs_mult_less = thm "abs_mult_less";
   1.208 -val eq_minus_self_iff = thm "eq_minus_self_iff";
   1.209 -val less_minus_self_iff = thm "less_minus_self_iff";
   1.210 -val abs_less_iff = thm "abs_less_iff";
   1.211 -*}
   1.212 -
   1.213  end