1.1 --- a/src/HOL/Real/RealBin.ML Tue Jul 25 00:00:22 2000 +0200
1.2 +++ b/src/HOL/Real/RealBin.ML Tue Jul 25 00:01:46 2000 +0200
1.3 @@ -1,9 +1,9 @@
1.4 -(* Title: HOL/RealBin.ML
1.5 +(* Title: HOL/Real/RealBin.ML
1.6 ID: $Id$
1.7 Author: Lawrence C Paulson, Cambridge University Computer Laboratory
1.8 Copyright 1999 University of Cambridge
1.9
1.10 -Binary arithmetic for the reals (integer literals only)
1.11 +Binary arithmetic for the reals (integer literals only).
1.12 *)
1.13
1.14 (** real_of_int (coercion from int to real) **)
1.15 @@ -25,7 +25,7 @@
1.16
1.17 Goal "(number_of v :: real) + number_of v' = number_of (bin_add v v')";
1.18 by (simp_tac
1.19 - (simpset_of Int.thy addsimps [real_number_of_def,
1.20 + (HOL_ss addsimps [real_number_of_def,
1.21 real_of_int_add, number_of_add]) 1);
1.22 qed "add_real_number_of";
1.23
1.24 @@ -36,13 +36,13 @@
1.25
1.26 Goalw [real_number_of_def] "- (number_of w :: real) = number_of (bin_minus w)";
1.27 by (simp_tac
1.28 - (simpset_of Int.thy addsimps [number_of_minus, real_of_int_minus]) 1);
1.29 + (HOL_ss addsimps [number_of_minus, real_of_int_minus]) 1);
1.30 qed "minus_real_number_of";
1.31
1.32 Goalw [real_number_of_def]
1.33 "(number_of v :: real) - number_of w = number_of (bin_add v (bin_minus w))";
1.34 by (simp_tac
1.35 - (simpset_of Int.thy addsimps [diff_number_of_eq, real_of_int_diff]) 1);
1.36 + (HOL_ss addsimps [diff_number_of_eq, real_of_int_diff]) 1);
1.37 qed "diff_real_number_of";
1.38
1.39 Addsimps [minus_real_number_of, diff_real_number_of];
1.40 @@ -52,7 +52,7 @@
1.41
1.42 Goal "(number_of v :: real) * number_of v' = number_of (bin_mult v v')";
1.43 by (simp_tac
1.44 - (simpset_of Int.thy addsimps [real_number_of_def,
1.45 + (HOL_ss addsimps [real_number_of_def,
1.46 real_of_int_mult, number_of_mult]) 1);
1.47 qed "mult_real_number_of";
1.48
1.49 @@ -64,7 +64,7 @@
1.50
1.51 (*For specialist use: NOT as default simprules*)
1.52 Goal "#2 * z = (z+z::real)";
1.53 -by (simp_tac (simpset_of RealDef.thy
1.54 +by (simp_tac (simpset ()
1.55 addsimps [lemma, real_add_mult_distrib,
1.56 one_eq_numeral_1 RS sym]) 1);
1.57 qed "real_mult_2";
1.58 @@ -81,7 +81,7 @@
1.59 Goal "((number_of v :: real) = number_of v') = \
1.60 \ iszero (number_of (bin_add v (bin_minus v')))";
1.61 by (simp_tac
1.62 - (simpset_of Int.thy addsimps [real_number_of_def,
1.63 + (HOL_ss addsimps [real_number_of_def,
1.64 real_of_int_eq_iff, eq_number_of_eq]) 1);
1.65 qed "eq_real_number_of";
1.66
1.67 @@ -93,7 +93,7 @@
1.68 Goal "((number_of v :: real) < number_of v') = \
1.69 \ neg (number_of (bin_add v (bin_minus v')))";
1.70 by (simp_tac
1.71 - (simpset_of Int.thy addsimps [real_number_of_def, real_of_int_less_iff,
1.72 + (HOL_ss addsimps [real_number_of_def, real_of_int_less_iff,
1.73 less_number_of_eq_neg]) 1);
1.74 qed "less_real_number_of";
1.75
1.76 @@ -121,15 +121,15 @@
1.77 HOL_ss addsimps [zero_eq_numeral_0, one_eq_numeral_1,
1.78 minus_numeral_one];
1.79
1.80 -fun rename_numerals thy th =
1.81 - asm_full_simplify real_numeral_ss (change_theory thy th);
1.82 +fun rename_numerals th =
1.83 + asm_full_simplify real_numeral_ss (Thm.transfer (the_context ()) th);
1.84
1.85
1.86 (*Now insert some identities previously stated for 0 and 1r*)
1.87
1.88 (** RealDef & Real **)
1.89
1.90 -Addsimps (map (rename_numerals thy)
1.91 +Addsimps (map rename_numerals
1.92 [real_minus_zero, real_minus_zero_iff,
1.93 real_add_zero_left, real_add_zero_right,
1.94 real_diff_0, real_diff_0_right,
1.95 @@ -137,16 +137,16 @@
1.96 real_mult_minus_1_right, real_mult_minus_1, real_rinv_1,
1.97 real_minus_zero_less_iff]);
1.98
1.99 -AddIffs (map (rename_numerals thy) [real_mult_is_0, real_0_is_mult]);
1.100 +AddIffs (map rename_numerals [real_mult_is_0, real_0_is_mult]);
1.101
1.102 bind_thm ("real_0_less_mult_iff",
1.103 - rename_numerals thy real_zero_less_mult_iff);
1.104 + rename_numerals real_zero_less_mult_iff);
1.105 bind_thm ("real_0_le_mult_iff",
1.106 - rename_numerals thy real_zero_le_mult_iff);
1.107 + rename_numerals real_zero_le_mult_iff);
1.108 bind_thm ("real_mult_less_0_iff",
1.109 - rename_numerals thy real_mult_less_zero_iff);
1.110 + rename_numerals real_mult_less_zero_iff);
1.111 bind_thm ("real_mult_le_0_iff",
1.112 - rename_numerals thy real_mult_le_zero_iff);
1.113 + rename_numerals real_mult_le_zero_iff);
1.114
1.115
1.116 (*Perhaps add some theorems that aren't in the default simpset, as
1.117 @@ -186,7 +186,7 @@
1.118 \ (if neg (number_of v) then #0 \
1.119 \ else (number_of v :: real))";
1.120 by (simp_tac
1.121 - (simpset_of Int.thy addsimps [nat_number_of_def, real_of_nat_real_of_int,
1.122 + (HOL_ss addsimps [nat_number_of_def, real_of_nat_real_of_int,
1.123 real_of_nat_neg_int, real_number_of,
1.124 zero_eq_numeral_0]) 1);
1.125 qed "real_of_nat_number_of";
1.126 @@ -342,9 +342,9 @@
1.127
1.128
1.129 (*Simplify #1*n and n*#1 to n*)
1.130 -val add_0s = map (rename_numerals thy)
1.131 +val add_0s = map rename_numerals
1.132 [real_add_zero_left, real_add_zero_right];
1.133 -val mult_1s = map (rename_numerals thy)
1.134 +val mult_1s = map rename_numerals
1.135 [real_mult_1, real_mult_1_right,
1.136 real_mult_minus_1, real_mult_minus_1_right];
1.137
1.138 @@ -385,7 +385,7 @@
1.139 real_mult_0, real_mult_0_right, real_mult_1, real_mult_1_right];
1.140
1.141 fun prep_simproc (name, pats, proc) = Simplifier.mk_simproc name pats proc;
1.142 -fun prep_pat s = Thm.read_cterm (Theory.sign_of RealInt.thy) (s, HOLogic.termT);
1.143 +fun prep_pat s = Thm.read_cterm (Theory.sign_of (the_context ())) (s, HOLogic.termT);
1.144 val prep_pats = map prep_pat;
1.145
1.146 structure CancelNumeralsCommon =
1.147 @@ -536,7 +536,7 @@
1.148 struct
1.149 val ss = HOL_ss
1.150 val eq_reflection = eq_reflection
1.151 - val thy = RealBin.thy
1.152 + val sg_ref = Sign.self_ref (Theory.sign_of (the_context ()))
1.153 val T = HOLogic.realT
1.154 val plus = Const ("op *", [HOLogic.realT,HOLogic.realT] ---> HOLogic.realT)
1.155 val add_ac = real_mult_ac
1.156 @@ -547,105 +547,3 @@
1.157 Addsimprocs [Real_Times_Assoc.conv];
1.158
1.159
1.160 -(*---------------------------------------------------------------------------*)
1.161 -(* Linear arithmetic *)
1.162 -(*---------------------------------------------------------------------------*)
1.163 -
1.164 -(* Instantiation of the generic linear arithmetic package for type real. *)
1.165 -
1.166 -(* Author: Tobias Nipkow, TU Muenchen
1.167 - Copyright 1999 TU Muenchen
1.168 -*)
1.169 -
1.170 -let
1.171 -
1.172 -(* reduce contradictory <= to False *)
1.173 -val simps = [order_less_irrefl, zero_eq_numeral_0, one_eq_numeral_1,
1.174 - add_real_number_of, minus_real_number_of, diff_real_number_of,
1.175 - mult_real_number_of, eq_real_number_of, less_real_number_of,
1.176 - le_real_number_of_eq_not_less, real_diff_def,
1.177 - real_minus_add_distrib, real_minus_minus];
1.178 -
1.179 -val add_rules =
1.180 - map (rename_numerals thy)
1.181 - [real_add_zero_left, real_add_zero_right,
1.182 - real_add_minus, real_add_minus_left,
1.183 - real_mult_0, real_mult_0_right,
1.184 - real_mult_1, real_mult_1_right,
1.185 - real_mult_minus_1, real_mult_minus_1_right];
1.186 -
1.187 -val simprocs = [Real_Times_Assoc.conv, Real_Numeral_Simprocs.combine_numerals]@
1.188 - Real_Numeral_Simprocs.cancel_numerals;
1.189 -
1.190 -val mono_ss = simpset() addsimps
1.191 - [real_add_le_mono,real_add_less_mono,
1.192 - real_add_less_le_mono,real_add_le_less_mono];
1.193 -
1.194 -val add_mono_thms =
1.195 - map (fn s => prove_goal thy s
1.196 - (fn prems => [cut_facts_tac prems 1, asm_simp_tac mono_ss 1]))
1.197 - ["(i <= j) & (k <= l) ==> i + k <= j + (l::real)",
1.198 - "(i = j) & (k <= l) ==> i + k <= j + (l::real)",
1.199 - "(i <= j) & (k = l) ==> i + k <= j + (l::real)",
1.200 - "(i = j) & (k = l) ==> i + k = j + (l::real)",
1.201 - "(i < j) & (k = l) ==> i + k < j + (l::real)",
1.202 - "(i = j) & (k < l) ==> i + k < j + (l::real)",
1.203 - "(i < j) & (k <= l) ==> i + k < j + (l::real)",
1.204 - "(i <= j) & (k < l) ==> i + k < j + (l::real)",
1.205 - "(i < j) & (k < l) ==> i + k < j + (l::real)"];
1.206 -
1.207 -in
1.208 -LA_Data_Ref.add_mono_thms := !LA_Data_Ref.add_mono_thms @ add_mono_thms;
1.209 -LA_Data_Ref.ss_ref := !LA_Data_Ref.ss_ref addsimps simps@add_rules
1.210 - addsimprocs simprocs
1.211 - addcongs [if_weak_cong];
1.212 -LA_Data_Ref.discrete := !LA_Data_Ref.discrete @ [("RealDef.real",false)]
1.213 -(*We don't change LA_Data_Ref.lessD because the real ordering is dense!*)
1.214 -end;
1.215 -
1.216 -let
1.217 -val real_arith_simproc_pats =
1.218 - map (fn s => Thm.read_cterm (Theory.sign_of RealDef.thy) (s, HOLogic.boolT))
1.219 - ["(m::real) < n","(m::real) <= n", "(m::real) = n"];
1.220 -
1.221 -val fast_real_arith_simproc = mk_simproc
1.222 - "fast_real_arith" real_arith_simproc_pats Fast_Arith.lin_arith_prover;
1.223 -in
1.224 -Addsimprocs [fast_real_arith_simproc]
1.225 -end;
1.226 -
1.227 -(* Some test data [omitting examples thet assume the ordering to be discrete!]
1.228 -Goal "!!a::real. [| a <= b; c <= d; x+y<z |] ==> a+c <= b+d";
1.229 -by (fast_arith_tac 1);
1.230 -Goal "!!a::real. [| a <= b; b+b <= c |] ==> a+a <= c";
1.231 -by (fast_arith_tac 1);
1.232 -Goal "!!a::real. [| a+b <= i+j; a<=b; i<=j |] ==> a+a <= j+j";
1.233 -by (fast_arith_tac 1);
1.234 -Goal "!!a::real. a+b+c <= i+j+k & a<=b & b<=c & i<=j & j<=k --> a+a+a <= k+k+k";
1.235 -by (arith_tac 1);
1.236 -Goal "!!a::real. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
1.237 -\ ==> a <= l";
1.238 -by (fast_arith_tac 1);
1.239 -Goal "!!a::real. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
1.240 -\ ==> a+a+a+a <= l+l+l+l";
1.241 -by (fast_arith_tac 1);
1.242 -Goal "!!a::real. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
1.243 -\ ==> a+a+a+a+a <= l+l+l+l+i";
1.244 -by (fast_arith_tac 1);
1.245 -Goal "!!a::real. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
1.246 -\ ==> a+a+a+a+a+a <= l+l+l+l+i+l";
1.247 -by (fast_arith_tac 1);
1.248 -Goal "!!a::real. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
1.249 -\ ==> #6*a <= #5*l+i";
1.250 -by (fast_arith_tac 1);
1.251 -*)
1.252 -
1.253 -(*---------------------------------------------------------------------------*)
1.254 -(* End of linear arithmetic *)
1.255 -(*---------------------------------------------------------------------------*)
1.256 -
1.257 -(*useful??*)
1.258 -Goal "(z = z + w) = (w = (#0::real))";
1.259 -by Auto_tac;
1.260 -qed "real_add_left_cancel0";
1.261 -Addsimps [real_add_left_cancel0];