# HG changeset patch # User wenzelm # Date 964476106 -7200 # Node ID ac20534ce4d1bbbe33810a9170c58fc8c8d2a520 # Parent 8b7aad2abcc9ef33b930cec382a76eec46c9d6ab avoid referencing thy value; rename_numerals: use implicit theory context; eliminated some simpset_of Int.thy (why needed anyway?); diff -r 8b7aad2abcc9 -r ac20534ce4d1 src/HOL/Real/RealBin.ML --- a/src/HOL/Real/RealBin.ML Tue Jul 25 00:00:22 2000 +0200 +++ b/src/HOL/Real/RealBin.ML Tue Jul 25 00:01:46 2000 +0200 @@ -1,9 +1,9 @@ -(* Title: HOL/RealBin.ML +(* Title: HOL/Real/RealBin.ML ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1999 University of Cambridge -Binary arithmetic for the reals (integer literals only) +Binary arithmetic for the reals (integer literals only). *) (** real_of_int (coercion from int to real) **) @@ -25,7 +25,7 @@ Goal "(number_of v :: real) + number_of v' = number_of (bin_add v v')"; by (simp_tac - (simpset_of Int.thy addsimps [real_number_of_def, + (HOL_ss addsimps [real_number_of_def, real_of_int_add, number_of_add]) 1); qed "add_real_number_of"; @@ -36,13 +36,13 @@ Goalw [real_number_of_def] "- (number_of w :: real) = number_of (bin_minus w)"; by (simp_tac - (simpset_of Int.thy addsimps [number_of_minus, real_of_int_minus]) 1); + (HOL_ss addsimps [number_of_minus, real_of_int_minus]) 1); qed "minus_real_number_of"; Goalw [real_number_of_def] "(number_of v :: real) - number_of w = number_of (bin_add v (bin_minus w))"; by (simp_tac - (simpset_of Int.thy addsimps [diff_number_of_eq, real_of_int_diff]) 1); + (HOL_ss addsimps [diff_number_of_eq, real_of_int_diff]) 1); qed "diff_real_number_of"; Addsimps [minus_real_number_of, diff_real_number_of]; @@ -52,7 +52,7 @@ Goal "(number_of v :: real) * number_of v' = number_of (bin_mult v v')"; by (simp_tac - (simpset_of Int.thy addsimps [real_number_of_def, + (HOL_ss addsimps [real_number_of_def, real_of_int_mult, number_of_mult]) 1); qed "mult_real_number_of"; @@ -64,7 +64,7 @@ (*For specialist use: NOT as default simprules*) Goal "#2 * z = (z+z::real)"; -by (simp_tac (simpset_of RealDef.thy +by (simp_tac (simpset () addsimps [lemma, real_add_mult_distrib, one_eq_numeral_1 RS sym]) 1); qed "real_mult_2"; @@ -81,7 +81,7 @@ Goal "((number_of v :: real) = number_of v') = \ \ iszero (number_of (bin_add v (bin_minus v')))"; by (simp_tac - (simpset_of Int.thy addsimps [real_number_of_def, + (HOL_ss addsimps [real_number_of_def, real_of_int_eq_iff, eq_number_of_eq]) 1); qed "eq_real_number_of"; @@ -93,7 +93,7 @@ Goal "((number_of v :: real) < number_of v') = \ \ neg (number_of (bin_add v (bin_minus v')))"; by (simp_tac - (simpset_of Int.thy addsimps [real_number_of_def, real_of_int_less_iff, + (HOL_ss addsimps [real_number_of_def, real_of_int_less_iff, less_number_of_eq_neg]) 1); qed "less_real_number_of"; @@ -121,15 +121,15 @@ HOL_ss addsimps [zero_eq_numeral_0, one_eq_numeral_1, minus_numeral_one]; -fun rename_numerals thy th = - asm_full_simplify real_numeral_ss (change_theory thy th); +fun rename_numerals th = + asm_full_simplify real_numeral_ss (Thm.transfer (the_context ()) th); (*Now insert some identities previously stated for 0 and 1r*) (** RealDef & Real **) -Addsimps (map (rename_numerals thy) +Addsimps (map rename_numerals [real_minus_zero, real_minus_zero_iff, real_add_zero_left, real_add_zero_right, real_diff_0, real_diff_0_right, @@ -137,16 +137,16 @@ real_mult_minus_1_right, real_mult_minus_1, real_rinv_1, real_minus_zero_less_iff]); -AddIffs (map (rename_numerals thy) [real_mult_is_0, real_0_is_mult]); +AddIffs (map rename_numerals [real_mult_is_0, real_0_is_mult]); bind_thm ("real_0_less_mult_iff", - rename_numerals thy real_zero_less_mult_iff); + rename_numerals real_zero_less_mult_iff); bind_thm ("real_0_le_mult_iff", - rename_numerals thy real_zero_le_mult_iff); + rename_numerals real_zero_le_mult_iff); bind_thm ("real_mult_less_0_iff", - rename_numerals thy real_mult_less_zero_iff); + rename_numerals real_mult_less_zero_iff); bind_thm ("real_mult_le_0_iff", - rename_numerals thy real_mult_le_zero_iff); + rename_numerals real_mult_le_zero_iff); (*Perhaps add some theorems that aren't in the default simpset, as @@ -186,7 +186,7 @@ \ (if neg (number_of v) then #0 \ \ else (number_of v :: real))"; by (simp_tac - (simpset_of Int.thy addsimps [nat_number_of_def, real_of_nat_real_of_int, + (HOL_ss addsimps [nat_number_of_def, real_of_nat_real_of_int, real_of_nat_neg_int, real_number_of, zero_eq_numeral_0]) 1); qed "real_of_nat_number_of"; @@ -342,9 +342,9 @@ (*Simplify #1*n and n*#1 to n*) -val add_0s = map (rename_numerals thy) +val add_0s = map rename_numerals [real_add_zero_left, real_add_zero_right]; -val mult_1s = map (rename_numerals thy) +val mult_1s = map rename_numerals [real_mult_1, real_mult_1_right, real_mult_minus_1, real_mult_minus_1_right]; @@ -385,7 +385,7 @@ real_mult_0, real_mult_0_right, real_mult_1, real_mult_1_right]; fun prep_simproc (name, pats, proc) = Simplifier.mk_simproc name pats proc; -fun prep_pat s = Thm.read_cterm (Theory.sign_of RealInt.thy) (s, HOLogic.termT); +fun prep_pat s = Thm.read_cterm (Theory.sign_of (the_context ())) (s, HOLogic.termT); val prep_pats = map prep_pat; structure CancelNumeralsCommon = @@ -536,7 +536,7 @@ struct val ss = HOL_ss val eq_reflection = eq_reflection - val thy = RealBin.thy + val sg_ref = Sign.self_ref (Theory.sign_of (the_context ())) val T = HOLogic.realT val plus = Const ("op *", [HOLogic.realT,HOLogic.realT] ---> HOLogic.realT) val add_ac = real_mult_ac @@ -547,105 +547,3 @@ Addsimprocs [Real_Times_Assoc.conv]; -(*---------------------------------------------------------------------------*) -(* Linear arithmetic *) -(*---------------------------------------------------------------------------*) - -(* Instantiation of the generic linear arithmetic package for type real. *) - -(* Author: Tobias Nipkow, TU Muenchen - Copyright 1999 TU Muenchen -*) - -let - -(* reduce contradictory <= to False *) -val simps = [order_less_irrefl, zero_eq_numeral_0, one_eq_numeral_1, - add_real_number_of, minus_real_number_of, diff_real_number_of, - mult_real_number_of, eq_real_number_of, less_real_number_of, - le_real_number_of_eq_not_less, real_diff_def, - real_minus_add_distrib, real_minus_minus]; - -val add_rules = - map (rename_numerals thy) - [real_add_zero_left, real_add_zero_right, - real_add_minus, real_add_minus_left, - real_mult_0, real_mult_0_right, - real_mult_1, real_mult_1_right, - real_mult_minus_1, real_mult_minus_1_right]; - -val simprocs = [Real_Times_Assoc.conv, Real_Numeral_Simprocs.combine_numerals]@ - Real_Numeral_Simprocs.cancel_numerals; - -val mono_ss = simpset() addsimps - [real_add_le_mono,real_add_less_mono, - real_add_less_le_mono,real_add_le_less_mono]; - -val add_mono_thms = - map (fn s => prove_goal thy s - (fn prems => [cut_facts_tac prems 1, asm_simp_tac mono_ss 1])) - ["(i <= j) & (k <= l) ==> i + k <= j + (l::real)", - "(i = j) & (k <= l) ==> i + k <= j + (l::real)", - "(i <= j) & (k = l) ==> i + k <= j + (l::real)", - "(i = j) & (k = l) ==> i + k = j + (l::real)", - "(i < j) & (k = l) ==> i + k < j + (l::real)", - "(i = j) & (k < l) ==> i + k < j + (l::real)", - "(i < j) & (k <= l) ==> i + k < j + (l::real)", - "(i <= j) & (k < l) ==> i + k < j + (l::real)", - "(i < j) & (k < l) ==> i + k < j + (l::real)"]; - -in -LA_Data_Ref.add_mono_thms := !LA_Data_Ref.add_mono_thms @ add_mono_thms; -LA_Data_Ref.ss_ref := !LA_Data_Ref.ss_ref addsimps simps@add_rules - addsimprocs simprocs - addcongs [if_weak_cong]; -LA_Data_Ref.discrete := !LA_Data_Ref.discrete @ [("RealDef.real",false)] -(*We don't change LA_Data_Ref.lessD because the real ordering is dense!*) -end; - -let -val real_arith_simproc_pats = - map (fn s => Thm.read_cterm (Theory.sign_of RealDef.thy) (s, HOLogic.boolT)) - ["(m::real) < n","(m::real) <= n", "(m::real) = n"]; - -val fast_real_arith_simproc = mk_simproc - "fast_real_arith" real_arith_simproc_pats Fast_Arith.lin_arith_prover; -in -Addsimprocs [fast_real_arith_simproc] -end; - -(* Some test data [omitting examples thet assume the ordering to be discrete!] -Goal "!!a::real. [| a <= b; c <= d; x+y a+c <= b+d"; -by (fast_arith_tac 1); -Goal "!!a::real. [| a <= b; b+b <= c |] ==> a+a <= c"; -by (fast_arith_tac 1); -Goal "!!a::real. [| a+b <= i+j; a<=b; i<=j |] ==> a+a <= j+j"; -by (fast_arith_tac 1); -Goal "!!a::real. a+b+c <= i+j+k & a<=b & b<=c & i<=j & j<=k --> a+a+a <= k+k+k"; -by (arith_tac 1); -Goal "!!a::real. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \ -\ ==> a <= l"; -by (fast_arith_tac 1); -Goal "!!a::real. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \ -\ ==> a+a+a+a <= l+l+l+l"; -by (fast_arith_tac 1); -Goal "!!a::real. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \ -\ ==> a+a+a+a+a <= l+l+l+l+i"; -by (fast_arith_tac 1); -Goal "!!a::real. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \ -\ ==> a+a+a+a+a+a <= l+l+l+l+i+l"; -by (fast_arith_tac 1); -Goal "!!a::real. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \ -\ ==> #6*a <= #5*l+i"; -by (fast_arith_tac 1); -*) - -(*---------------------------------------------------------------------------*) -(* End of linear arithmetic *) -(*---------------------------------------------------------------------------*) - -(*useful??*) -Goal "(z = z + w) = (w = (#0::real))"; -by Auto_tac; -qed "real_add_left_cancel0"; -Addsimps [real_add_left_cancel0];