# HG changeset patch # User paulson # Date 1075305661 -3600 # Node ID c50188fe6366f6db017bd2f885d1f7197f980967 # Parent 2763da611ad9e04819d3d7b1686b456fd60971bf tidying up arithmetic for the hyperreals diff -r 2763da611ad9 -r c50188fe6366 src/HOL/Hyperreal/HyperArith.thy --- a/src/HOL/Hyperreal/HyperArith.thy Wed Jan 28 10:41:49 2004 +0100 +++ b/src/HOL/Hyperreal/HyperArith.thy Wed Jan 28 17:01:01 2004 +0100 @@ -1,17 +1,148 @@ -theory HyperArith = HyperBin -files "hypreal_arith.ML": +(* Title: HOL/HyperBin.thy + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1999 University of Cambridge +*) + +header{*Binary arithmetic and Simplification for the Hyperreals*} + +theory HyperArith = HyperOrd +files ("hypreal_arith.ML"): + +subsection{*Binary Arithmetic for the Hyperreals*} + +instance hypreal :: number .. + +defs (overloaded) + hypreal_number_of_def: + "number_of v == hypreal_of_real (number_of v)" + (*::bin=>hypreal ::bin=>real*) + --{*This case is reduced to that for the reals.*} + + + +subsubsection{*Embedding the Reals into the Hyperreals*} + +lemma hypreal_number_of [simp]: "hypreal_of_real (number_of w) = number_of w" +by (simp add: hypreal_number_of_def) + +lemma hypreal_numeral_0_eq_0: "Numeral0 = (0::hypreal)" +by (simp add: hypreal_number_of_def) + +lemma hypreal_numeral_1_eq_1: "Numeral1 = (1::hypreal)" +by (simp add: hypreal_number_of_def) + +subsubsection{*Addition*} + +lemma add_hypreal_number_of [simp]: + "(number_of v :: hypreal) + number_of v' = number_of (bin_add v v')" +by (simp only: hypreal_number_of_def hypreal_of_real_add [symmetric] + add_real_number_of) + + +subsubsection{*Subtraction*} + +lemma minus_hypreal_number_of [simp]: + "- (number_of w :: hypreal) = number_of (bin_minus w)" +by (simp only: hypreal_number_of_def minus_real_number_of + hypreal_of_real_minus [symmetric]) + +lemma diff_hypreal_number_of [simp]: + "(number_of v :: hypreal) - number_of w = + number_of (bin_add v (bin_minus w))" +by (unfold hypreal_number_of_def hypreal_diff_def, simp) + + +subsubsection{*Multiplication*} + +lemma mult_hypreal_number_of [simp]: + "(number_of v :: hypreal) * number_of v' = number_of (bin_mult v v')" +by (simp only: hypreal_number_of_def hypreal_of_real_mult [symmetric] mult_real_number_of) + +text{*Lemmas for specialist use, NOT as default simprules*} +lemma hypreal_mult_2: "2 * z = (z+z::hypreal)" +proof - + have eq: "(2::hypreal) = 1 + 1" + by (simp add: hypreal_numeral_1_eq_1 [symmetric]) + thus ?thesis by (simp add: eq left_distrib) +qed + +lemma hypreal_mult_2_right: "z * 2 = (z+z::hypreal)" +by (subst hypreal_mult_commute, rule hypreal_mult_2) + + +subsubsection{*Comparisons*} + +(** Equals (=) **) + +lemma eq_hypreal_number_of [simp]: + "((number_of v :: hypreal) = number_of v') = + iszero (number_of (bin_add v (bin_minus v')))" +apply (simp only: hypreal_number_of_def hypreal_of_real_eq_iff eq_real_number_of) +done + + +(** Less-than (<) **) + +(*"neg" is used in rewrite rules for binary comparisons*) +lemma less_hypreal_number_of [simp]: + "((number_of v :: hypreal) < number_of v') = + neg (number_of (bin_add v (bin_minus v')))" +by (simp only: hypreal_number_of_def hypreal_of_real_less_iff less_real_number_of) + + + +text{*New versions of existing theorems involving 0, 1*} + +lemma hypreal_minus_1_eq_m1 [simp]: "- 1 = (-1::hypreal)" +by (simp add: hypreal_numeral_1_eq_1 [symmetric]) + +lemma hypreal_mult_minus1 [simp]: "-1 * z = -(z::hypreal)" +proof - + have "-1 * z = (- 1) * z" by (simp add: hypreal_minus_1_eq_m1) + also have "... = - (1 * z)" by (simp only: minus_mult_left) + also have "... = -z" by simp + finally show ?thesis . +qed + +lemma hypreal_mult_minus1_right [simp]: "(z::hypreal) * -1 = -z" +by (subst hypreal_mult_commute, rule hypreal_mult_minus1) + + +subsection{*Simplification of Arithmetic when Nested to the Right*} + +lemma hypreal_add_number_of_left [simp]: + "number_of v + (number_of w + z) = (number_of(bin_add v w) + z::hypreal)" +by (simp add: add_assoc [symmetric]) + +lemma hypreal_mult_number_of_left [simp]: + "number_of v *(number_of w * z) = (number_of(bin_mult v w) * z::hypreal)" +by (simp add: hypreal_mult_assoc [symmetric]) + +lemma hypreal_add_number_of_diff1: + "number_of v + (number_of w - c) = number_of(bin_add v w) - (c::hypreal)" +by (simp add: hypreal_diff_def hypreal_add_number_of_left) + +lemma hypreal_add_number_of_diff2 [simp]: + "number_of v + (c - number_of w) = + number_of (bin_add v (bin_minus w)) + (c::hypreal)" +apply (subst diff_hypreal_number_of [symmetric]) +apply (simp only: hypreal_diff_def add_ac) +done + + +declare hypreal_numeral_0_eq_0 [simp] hypreal_numeral_1_eq_1 [simp] + + + +use "hypreal_arith.ML" setup hypreal_arith_setup text{*Used once in NSA*} lemma hypreal_add_minus_eq_minus: "x + y = (0::hypreal) ==> x = -y" -apply arith -done +by arith -ML -{* -val hypreal_add_minus_eq_minus = thm "hypreal_add_minus_eq_minus"; -*} subsubsection{*Division By @{term 1} and @{term "-1"}*} @@ -22,10 +153,50 @@ by (simp add: hypreal_divide_def hypreal_minus_inverse) + + +(** number_of related to hypreal_of_real. +Could similar theorems be useful for other injections? **) + +lemma number_of_less_hypreal_of_real_iff [simp]: + "(number_of w < hypreal_of_real z) = (number_of w < z)" +apply (subst hypreal_of_real_less_iff [symmetric]) +apply (simp (no_asm)) +done + +lemma number_of_le_hypreal_of_real_iff [simp]: + "(number_of w <= hypreal_of_real z) = (number_of w <= z)" +apply (subst hypreal_of_real_le_iff [symmetric]) +apply (simp (no_asm)) +done + +lemma hypreal_of_real_eq_number_of_iff [simp]: + "(hypreal_of_real z = number_of w) = (z = number_of w)" +apply (subst hypreal_of_real_eq_iff [symmetric]) +apply (simp (no_asm)) +done + +lemma hypreal_of_real_less_number_of_iff [simp]: + "(hypreal_of_real z < number_of w) = (z < number_of w)" +apply (subst hypreal_of_real_less_iff [symmetric]) +apply (simp (no_asm)) +done + +lemma hypreal_of_real_le_number_of_iff [simp]: + "(hypreal_of_real z <= number_of w) = (z <= number_of w)" +apply (subst hypreal_of_real_le_iff [symmetric]) +apply (simp (no_asm)) +done + (* FIXME: we should have this, as for type int, but many proofs would break. It replaces x+-y by x-y. Addsimps [symmetric hypreal_diff_def] *) +ML +{* +val hypreal_add_minus_eq_minus = thm "hypreal_add_minus_eq_minus"; +*} + end diff -r 2763da611ad9 -r c50188fe6366 src/HOL/Hyperreal/HyperBin.ML --- a/src/HOL/Hyperreal/HyperBin.ML Wed Jan 28 10:41:49 2004 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,618 +0,0 @@ -(* Title: HOL/Hyperreal/HyperBin.ML - ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 2000 University of Cambridge - -Binary arithmetic for the hypreals (integer literals only). -*) - -(** hypreal_of_real (coercion from int to real) **) - -Goal "hypreal_of_real (number_of w) = number_of w"; -by (simp_tac (simpset() addsimps [hypreal_number_of_def]) 1); -qed "hypreal_number_of"; -Addsimps [hypreal_number_of]; - -Goalw [hypreal_number_of_def] "Numeral0 = (0::hypreal)"; -by (Simp_tac 1); -qed "hypreal_numeral_0_eq_0"; - -Goalw [hypreal_number_of_def] "Numeral1 = (1::hypreal)"; -by (Simp_tac 1); -qed "hypreal_numeral_1_eq_1"; - -(** Addition **) - -Goal "(number_of v :: hypreal) + number_of v' = number_of (bin_add v v')"; -by (simp_tac - (HOL_ss addsimps [hypreal_number_of_def, - hypreal_of_real_add RS sym, add_real_number_of]) 1); -qed "add_hypreal_number_of"; -Addsimps [add_hypreal_number_of]; - - -(** Subtraction **) - -Goalw [hypreal_number_of_def] - "- (number_of w :: hypreal) = number_of (bin_minus w)"; -by (simp_tac - (HOL_ss addsimps [minus_real_number_of, hypreal_of_real_minus RS sym]) 1); -qed "minus_hypreal_number_of"; -Addsimps [minus_hypreal_number_of]; - -Goalw [hypreal_number_of_def, hypreal_diff_def] - "(number_of v :: hypreal) - number_of w = \ -\ number_of (bin_add v (bin_minus w))"; -by (Simp_tac 1); -qed "diff_hypreal_number_of"; -Addsimps [diff_hypreal_number_of]; - - -(** Multiplication **) - -Goal "(number_of v :: hypreal) * number_of v' = number_of (bin_mult v v')"; -by (simp_tac - (HOL_ss addsimps [hypreal_number_of_def, - hypreal_of_real_mult RS sym, mult_real_number_of]) 1); -qed "mult_hypreal_number_of"; -Addsimps [mult_hypreal_number_of]; - -Goal "(2::hypreal) = 1 + 1"; -by (simp_tac (simpset() addsimps [hypreal_numeral_1_eq_1 RS sym]) 1); -val lemma = result(); - -(*For specialist use: NOT as default simprules*) -Goal "2 * z = (z+z::hypreal)"; -by (simp_tac (simpset () - addsimps [lemma, left_distrib, - hypreal_numeral_1_eq_1]) 1); -qed "hypreal_mult_2"; - -Goal "z * 2 = (z+z::hypreal)"; -by (stac hypreal_mult_commute 1 THEN rtac hypreal_mult_2 1); -qed "hypreal_mult_2_right"; - - -(*** Comparisons ***) - -(** Equals (=) **) - -Goal "((number_of v :: hypreal) = number_of v') = \ -\ iszero (number_of (bin_add v (bin_minus v')))"; -by (simp_tac - (HOL_ss addsimps [hypreal_number_of_def, - hypreal_of_real_eq_iff, eq_real_number_of]) 1); -qed "eq_hypreal_number_of"; -Addsimps [eq_hypreal_number_of]; - -(** Less-than (<) **) - -(*"neg" is used in rewrite rules for binary comparisons*) -Goal "((number_of v :: hypreal) < number_of v') = \ -\ neg (number_of (bin_add v (bin_minus v')))"; -by (simp_tac - (HOL_ss addsimps [hypreal_number_of_def, hypreal_of_real_less_iff, - less_real_number_of]) 1); -qed "less_hypreal_number_of"; -Addsimps [less_hypreal_number_of]; - - -(** Less-than-or-equals (<=) **) - -Goal "(number_of x <= (number_of y::hypreal)) = \ -\ (~ number_of y < (number_of x::hypreal))"; -by (rtac (linorder_not_less RS sym) 1); -qed "le_hypreal_number_of_eq_not_less"; -Addsimps [le_hypreal_number_of_eq_not_less]; - -(*** New versions of existing theorems involving 0, 1 ***) - -Goal "- 1 = (-1::hypreal)"; -by (simp_tac (simpset() addsimps [hypreal_numeral_1_eq_1 RS sym]) 1); -qed "hypreal_minus_1_eq_m1"; - -(*Maps 0 to Numeral0 and 1 to Numeral1 and -(Numeral1) to -1*) -val hypreal_numeral_ss = - real_numeral_ss addsimps [hypreal_numeral_0_eq_0 RS sym, - hypreal_numeral_1_eq_1 RS sym, - hypreal_minus_1_eq_m1]; - -fun rename_numerals th = - asm_full_simplify hypreal_numeral_ss (Thm.transfer (the_context ()) th); - - -(** Simplification of arithmetic when nested to the right **) - -Goal "number_of v + (number_of w + z) = (number_of(bin_add v w) + z::hypreal)"; -by (asm_full_simp_tac (simpset() addsimps [add_assoc RS sym]) 1); -qed "hypreal_add_number_of_left"; - -Goal "number_of v *(number_of w * z) = (number_of(bin_mult v w) * z::hypreal)"; -by (simp_tac (simpset() addsimps [hypreal_mult_assoc RS sym]) 1); -qed "hypreal_mult_number_of_left"; - -Goalw [hypreal_diff_def] - "number_of v + (number_of w - c) = number_of(bin_add v w) - (c::hypreal)"; -by (rtac hypreal_add_number_of_left 1); -qed "hypreal_add_number_of_diff1"; - -Goal "number_of v + (c - number_of w) = \ -\ number_of (bin_add v (bin_minus w)) + (c::hypreal)"; -by (stac (diff_hypreal_number_of RS sym) 1); -by (asm_full_simp_tac (HOL_ss addsimps [hypreal_diff_def]@add_ac) 1); -qed "hypreal_add_number_of_diff2"; - -Addsimps [hypreal_add_number_of_left, hypreal_mult_number_of_left, - hypreal_add_number_of_diff1, hypreal_add_number_of_diff2]; - - -(**** Simprocs for numeric literals ****) - -(** For combine_numerals **) - -Goal "i*u + (j*u + k) = (i+j)*u + (k::hypreal)"; -by (asm_simp_tac (simpset() addsimps [left_distrib] @ add_ac) 1); -qed "left_hypreal_add_mult_distrib"; - - -(** For cancel_numerals **) - -val rel_iff_rel_0_rls = - map (inst "b" "?u+?v") - [less_iff_diff_less_0, eq_iff_diff_eq_0, - le_iff_diff_le_0] @ - map (inst "b" "n") - [less_iff_diff_less_0, eq_iff_diff_eq_0, - le_iff_diff_le_0]; - -Goal "!!i::hypreal. (i*u + m = j*u + n) = ((i-j)*u + m = n)"; -by (asm_simp_tac - (simpset() addsimps [hypreal_diff_def, left_distrib]@ - add_ac@rel_iff_rel_0_rls) 1); -qed "hypreal_eq_add_iff1"; - -Goal "!!i::hypreal. (i*u + m = j*u + n) = (m = (j-i)*u + n)"; -by (asm_simp_tac - (simpset() addsimps [hypreal_diff_def, left_distrib]@ - add_ac@rel_iff_rel_0_rls) 1); -qed "hypreal_eq_add_iff2"; - -Goal "!!i::hypreal. (i*u + m < j*u + n) = ((i-j)*u + m < n)"; -by (asm_simp_tac - (simpset() addsimps [hypreal_diff_def, left_distrib]@ - add_ac@rel_iff_rel_0_rls) 1); -qed "hypreal_less_add_iff1"; - -Goal "!!i::hypreal. (i*u + m < j*u + n) = (m < (j-i)*u + n)"; -by (asm_simp_tac - (simpset() addsimps [hypreal_diff_def, left_distrib]@ - add_ac@rel_iff_rel_0_rls) 1); -qed "hypreal_less_add_iff2"; - -Goal "!!i::hypreal. (i*u + m <= j*u + n) = ((i-j)*u + m <= n)"; -by (asm_simp_tac - (simpset() addsimps [hypreal_diff_def, left_distrib]@ - add_ac@rel_iff_rel_0_rls) 1); -qed "hypreal_le_add_iff1"; - -Goal "!!i::hypreal. (i*u + m <= j*u + n) = (m <= (j-i)*u + n)"; -by (asm_simp_tac - (simpset() addsimps [hypreal_diff_def, left_distrib]@ - add_ac@rel_iff_rel_0_rls) 1); -qed "hypreal_le_add_iff2"; - -Goal "-1 * (z::hypreal) = -z"; -by (simp_tac (simpset() addsimps [hypreal_minus_1_eq_m1 RS sym, - hypreal_mult_minus_1]) 1); -qed "hypreal_mult_minus1"; -Addsimps [hypreal_mult_minus1]; - -Goal "(z::hypreal) * -1 = -z"; -by (stac hypreal_mult_commute 1 THEN rtac hypreal_mult_minus1 1); -qed "hypreal_mult_minus1_right"; -Addsimps [hypreal_mult_minus1_right]; - - -Addsimps [hypreal_numeral_0_eq_0, hypreal_numeral_1_eq_1]; - - -structure Hyperreal_Numeral_Simprocs = -struct - -(*Maps 0 to Numeral0 and 1 to Numeral1 so that arithmetic in simprocs - isn't complicated by the abstract 0 and 1.*) -val numeral_syms = [hypreal_numeral_0_eq_0 RS sym, - hypreal_numeral_1_eq_1 RS sym]; - -(*Utilities*) - -val hyprealT = Type("HyperDef.hypreal",[]); - -fun mk_numeral n = HOLogic.number_of_const hyprealT $ HOLogic.mk_bin n; - -val dest_numeral = Real_Numeral_Simprocs.dest_numeral; - -val find_first_numeral = Real_Numeral_Simprocs.find_first_numeral; - -val zero = mk_numeral 0; -val mk_plus = Real_Numeral_Simprocs.mk_plus; - -val uminus_const = Const ("uminus", hyprealT --> hyprealT); - -(*Thus mk_sum[t] yields t+0; longer sums don't have a trailing zero*) -fun mk_sum [] = zero - | mk_sum [t,u] = mk_plus (t, u) - | mk_sum (t :: ts) = mk_plus (t, mk_sum ts); - -(*this version ALWAYS includes a trailing zero*) -fun long_mk_sum [] = zero - | long_mk_sum (t :: ts) = mk_plus (t, mk_sum ts); - -val dest_plus = HOLogic.dest_bin "op +" hyprealT; - -(*decompose additions AND subtractions as a sum*) -fun dest_summing (pos, Const ("op +", _) $ t $ u, ts) = - dest_summing (pos, t, dest_summing (pos, u, ts)) - | dest_summing (pos, Const ("op -", _) $ t $ u, ts) = - dest_summing (pos, t, dest_summing (not pos, u, ts)) - | dest_summing (pos, t, ts) = - if pos then t::ts else uminus_const$t :: ts; - -fun dest_sum t = dest_summing (true, t, []); - -val mk_diff = HOLogic.mk_binop "op -"; -val dest_diff = HOLogic.dest_bin "op -" hyprealT; - -val one = mk_numeral 1; -val mk_times = HOLogic.mk_binop "op *"; - -fun mk_prod [] = one - | mk_prod [t] = t - | mk_prod (t :: ts) = if t = one then mk_prod ts - else mk_times (t, mk_prod ts); - -val dest_times = HOLogic.dest_bin "op *" hyprealT; - -fun dest_prod t = - let val (t,u) = dest_times t - in dest_prod t @ dest_prod u end - handle TERM _ => [t]; - -(*DON'T do the obvious simplifications; that would create special cases*) -fun mk_coeff (k, ts) = mk_times (mk_numeral k, ts); - -(*Express t as a product of (possibly) a numeral with other sorted terms*) -fun dest_coeff sign (Const ("uminus", _) $ t) = dest_coeff (~sign) t - | dest_coeff sign t = - let val ts = sort Term.term_ord (dest_prod t) - val (n, ts') = find_first_numeral [] ts - handle TERM _ => (1, ts) - in (sign*n, mk_prod ts') end; - -(*Find first coefficient-term THAT MATCHES u*) -fun find_first_coeff past u [] = raise TERM("find_first_coeff", []) - | find_first_coeff past u (t::terms) = - let val (n,u') = dest_coeff 1 t - in if u aconv u' then (n, rev past @ terms) - else find_first_coeff (t::past) u terms - end - handle TERM _ => find_first_coeff (t::past) u terms; - - -(*Simplify Numeral0+n, n+Numeral0, Numeral1*n, n*Numeral1*) -val add_0s = map rename_numerals - [hypreal_add_zero_left, hypreal_add_zero_right]; -val mult_1s = map rename_numerals [hypreal_mult_1, hypreal_mult_1_right] @ - [hypreal_mult_minus1, hypreal_mult_minus1_right]; - -(*To perform binary arithmetic*) -val bin_simps = - [hypreal_numeral_0_eq_0 RS sym, hypreal_numeral_1_eq_1 RS sym, - add_hypreal_number_of, hypreal_add_number_of_left, - minus_hypreal_number_of, - diff_hypreal_number_of, mult_hypreal_number_of, - hypreal_mult_number_of_left] @ bin_arith_simps @ bin_rel_simps; - -(*Binary arithmetic BUT NOT ADDITION since it may collapse adjacent terms - during re-arrangement*) -val non_add_bin_simps = - bin_simps \\ [hypreal_add_number_of_left, add_hypreal_number_of]; - -(*To evaluate binary negations of coefficients*) -val hypreal_minus_simps = NCons_simps @ - [hypreal_minus_1_eq_m1, minus_hypreal_number_of, - bin_minus_1, bin_minus_0, bin_minus_Pls, bin_minus_Min, - bin_pred_1, bin_pred_0, bin_pred_Pls, bin_pred_Min]; - -(*To let us treat subtraction as addition*) -val diff_simps = [hypreal_diff_def, minus_add_distrib, minus_minus]; - -(*push the unary minus down: - x * y = x * - y *) -val hypreal_minus_mult_eq_1_to_2 = - [minus_mult_left RS sym, minus_mult_right] MRS trans - |> standard; - -(*to extract again any uncancelled minuses*) -val hypreal_minus_from_mult_simps = - [minus_minus, minus_mult_left RS sym, minus_mult_right RS sym]; - -(*combine unary minus with numeric literals, however nested within a product*) -val hypreal_mult_minus_simps = - [hypreal_mult_assoc, minus_mult_left, hypreal_minus_mult_eq_1_to_2]; - -(*Final simplification: cancel + and * *) -val simplify_meta_eq = - Int_Numeral_Simprocs.simplify_meta_eq - [hypreal_add_zero_left, hypreal_add_zero_right, - mult_zero_left, mult_zero_right, mult_1, mult_1_right]; - -val prep_simproc = Real_Numeral_Simprocs.prep_simproc; - -structure CancelNumeralsCommon = - struct - val mk_sum = mk_sum - val dest_sum = dest_sum - val mk_coeff = mk_coeff - val dest_coeff = dest_coeff 1 - val find_first_coeff = find_first_coeff [] - val trans_tac = Real_Numeral_Simprocs.trans_tac - val norm_tac = - ALLGOALS (simp_tac (HOL_ss addsimps add_0s@mult_1s@diff_simps@ - hypreal_minus_simps@add_ac)) - THEN ALLGOALS (simp_tac (HOL_ss addsimps non_add_bin_simps@hypreal_mult_minus_simps)) - THEN ALLGOALS - (simp_tac (HOL_ss addsimps hypreal_minus_from_mult_simps@ - add_ac@mult_ac)) - val numeral_simp_tac = ALLGOALS (simp_tac (HOL_ss addsimps add_0s@bin_simps)) - val simplify_meta_eq = simplify_meta_eq - end; - - -structure EqCancelNumerals = CancelNumeralsFun - (open CancelNumeralsCommon - val prove_conv = Bin_Simprocs.prove_conv - val mk_bal = HOLogic.mk_eq - val dest_bal = HOLogic.dest_bin "op =" hyprealT - val bal_add1 = hypreal_eq_add_iff1 RS trans - val bal_add2 = hypreal_eq_add_iff2 RS trans -); - -structure LessCancelNumerals = CancelNumeralsFun - (open CancelNumeralsCommon - val prove_conv = Bin_Simprocs.prove_conv - val mk_bal = HOLogic.mk_binrel "op <" - val dest_bal = HOLogic.dest_bin "op <" hyprealT - val bal_add1 = hypreal_less_add_iff1 RS trans - val bal_add2 = hypreal_less_add_iff2 RS trans -); - -structure LeCancelNumerals = CancelNumeralsFun - (open CancelNumeralsCommon - val prove_conv = Bin_Simprocs.prove_conv - val mk_bal = HOLogic.mk_binrel "op <=" - val dest_bal = HOLogic.dest_bin "op <=" hyprealT - val bal_add1 = hypreal_le_add_iff1 RS trans - val bal_add2 = hypreal_le_add_iff2 RS trans -); - -val cancel_numerals = - map prep_simproc - [("hyprealeq_cancel_numerals", - ["(l::hypreal) + m = n", "(l::hypreal) = m + n", - "(l::hypreal) - m = n", "(l::hypreal) = m - n", - "(l::hypreal) * m = n", "(l::hypreal) = m * n"], - EqCancelNumerals.proc), - ("hyprealless_cancel_numerals", - ["(l::hypreal) + m < n", "(l::hypreal) < m + n", - "(l::hypreal) - m < n", "(l::hypreal) < m - n", - "(l::hypreal) * m < n", "(l::hypreal) < m * n"], - LessCancelNumerals.proc), - ("hyprealle_cancel_numerals", - ["(l::hypreal) + m <= n", "(l::hypreal) <= m + n", - "(l::hypreal) - m <= n", "(l::hypreal) <= m - n", - "(l::hypreal) * m <= n", "(l::hypreal) <= m * n"], - LeCancelNumerals.proc)]; - - -structure CombineNumeralsData = - struct - val add = op + : int*int -> int - val mk_sum = long_mk_sum (*to work for e.g. 2*x + 3*x *) - val dest_sum = dest_sum - val mk_coeff = mk_coeff - val dest_coeff = dest_coeff 1 - val left_distrib = left_hypreal_add_mult_distrib RS trans - val prove_conv = Bin_Simprocs.prove_conv_nohyps - val trans_tac = Real_Numeral_Simprocs.trans_tac - val norm_tac = - ALLGOALS (simp_tac (HOL_ss addsimps add_0s@mult_1s@diff_simps@ - hypreal_minus_simps@add_ac)) - THEN ALLGOALS (simp_tac (HOL_ss addsimps non_add_bin_simps@hypreal_mult_minus_simps)) - THEN ALLGOALS (simp_tac (HOL_ss addsimps hypreal_minus_from_mult_simps@ - add_ac@mult_ac)) - val numeral_simp_tac = ALLGOALS - (simp_tac (HOL_ss addsimps add_0s@bin_simps)) - val simplify_meta_eq = simplify_meta_eq - end; - -structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData); - -val combine_numerals = - prep_simproc - ("hypreal_combine_numerals", ["(i::hypreal) + j", "(i::hypreal) - j"], CombineNumerals.proc); - - -(** Declarations for ExtractCommonTerm **) - -(*this version ALWAYS includes a trailing one*) -fun long_mk_prod [] = one - | long_mk_prod (t :: ts) = mk_times (t, mk_prod ts); - -(*Find first term that matches u*) -fun find_first past u [] = raise TERM("find_first", []) - | find_first past u (t::terms) = - if u aconv t then (rev past @ terms) - else find_first (t::past) u terms - handle TERM _ => find_first (t::past) u terms; - -(*Final simplification: cancel + and * *) -fun cancel_simplify_meta_eq cancel_th th = - Int_Numeral_Simprocs.simplify_meta_eq - [mult_1, mult_1_right] - (([th, cancel_th]) MRS trans); - -(*** Making constant folding work for 0 and 1 too ***) - -structure HyperrealAbstractNumeralsData = - struct - val dest_eq = HOLogic.dest_eq o HOLogic.dest_Trueprop o concl_of - val is_numeral = Bin_Simprocs.is_numeral - val numeral_0_eq_0 = hypreal_numeral_0_eq_0 - val numeral_1_eq_1 = hypreal_numeral_1_eq_1 - val prove_conv = Bin_Simprocs.prove_conv_nohyps_novars - fun norm_tac simps = ALLGOALS (simp_tac (HOL_ss addsimps simps)) - val simplify_meta_eq = Bin_Simprocs.simplify_meta_eq - end - -structure HyperrealAbstractNumerals = - AbstractNumeralsFun (HyperrealAbstractNumeralsData) - -(*For addition, we already have rules for the operand 0. - Multiplication is omitted because there are already special rules for - both 0 and 1 as operands. Unary minus is trivial, just have - 1 = -1. - For the others, having three patterns is a compromise between just having - one (many spurious calls) and having nine (just too many!) *) -val eval_numerals = - map prep_simproc - [("hypreal_add_eval_numerals", - ["(m::hypreal) + 1", "(m::hypreal) + number_of v"], - HyperrealAbstractNumerals.proc add_hypreal_number_of), - ("hypreal_diff_eval_numerals", - ["(m::hypreal) - 1", "(m::hypreal) - number_of v"], - HyperrealAbstractNumerals.proc diff_hypreal_number_of), - ("hypreal_eq_eval_numerals", - ["(m::hypreal) = 0", "(m::hypreal) = 1", "(m::hypreal) = number_of v"], - HyperrealAbstractNumerals.proc eq_hypreal_number_of), - ("hypreal_less_eval_numerals", - ["(m::hypreal) < 0", "(m::hypreal) < 1", "(m::hypreal) < number_of v"], - HyperrealAbstractNumerals.proc less_hypreal_number_of), - ("hypreal_le_eval_numerals", - ["(m::hypreal) <= 0", "(m::hypreal) <= 1", "(m::hypreal) <= number_of v"], - HyperrealAbstractNumerals.proc le_hypreal_number_of_eq_not_less)] - -end; - -Addsimprocs Hyperreal_Numeral_Simprocs.eval_numerals; -Addsimprocs Hyperreal_Numeral_Simprocs.cancel_numerals; -Addsimprocs [Hyperreal_Numeral_Simprocs.combine_numerals]; - -(*examples: -print_depth 22; -set timing; -set trace_simp; -fun test s = (Goal s, by (Simp_tac 1)); - -test "l + 2 + 2 + 2 + (l + 2) + (oo + 2) = (uu::hypreal)"; -test "2*u = (u::hypreal)"; -test "(i + j + 12 + (k::hypreal)) - 15 = y"; -test "(i + j + 12 + (k::hypreal)) - 5 = y"; - -test "y - b < (b::hypreal)"; -test "y - (3*b + c) < (b::hypreal) - 2*c"; - -test "(2*x - (u*v) + y) - v*3*u = (w::hypreal)"; -test "(2*x*u*v + (u*v)*4 + y) - v*u*4 = (w::hypreal)"; -test "(2*x*u*v + (u*v)*4 + y) - v*u = (w::hypreal)"; -test "u*v - (x*u*v + (u*v)*4 + y) = (w::hypreal)"; - -test "(i + j + 12 + (k::hypreal)) = u + 15 + y"; -test "(i + j*2 + 12 + (k::hypreal)) = j + 5 + y"; - -test "2*y + 3*z + 6*w + 2*y + 3*z + 2*u = 2*y' + 3*z' + 6*w' + 2*y' + 3*z' + u + (vv::hypreal)"; - -test "a + -(b+c) + b = (d::hypreal)"; -test "a + -(b+c) - b = (d::hypreal)"; - -(*negative numerals*) -test "(i + j + -2 + (k::hypreal)) - (u + 5 + y) = zz"; -test "(i + j + -3 + (k::hypreal)) < u + 5 + y"; -test "(i + j + 3 + (k::hypreal)) < u + -6 + y"; -test "(i + j + -12 + (k::hypreal)) - 15 = y"; -test "(i + j + 12 + (k::hypreal)) - -15 = y"; -test "(i + j + -12 + (k::hypreal)) - -15 = y"; -*) - - -(** Constant folding for hypreal plus and times **) - -(*We do not need - structure Hyperreal_Plus_Assoc = Assoc_Fold (Hyperreal_Plus_Assoc_Data); - because combine_numerals does the same thing*) - -structure Hyperreal_Times_Assoc_Data : ASSOC_FOLD_DATA = -struct - val ss = HOL_ss - val eq_reflection = eq_reflection - val sg_ref = Sign.self_ref (Theory.sign_of (the_context ())) - val T = Hyperreal_Numeral_Simprocs.hyprealT - val plus = Const ("op *", [T,T] ---> T) - val add_ac = mult_ac -end; - -structure Hyperreal_Times_Assoc = Assoc_Fold (Hyperreal_Times_Assoc_Data); - -Addsimprocs [Hyperreal_Times_Assoc.conv]; - -(*Simplification of x-y < 0, etc.*) -AddIffs [less_iff_diff_less_0 RS sym]; -AddIffs [eq_iff_diff_eq_0 RS sym]; -AddIffs [le_iff_diff_le_0 RS sym]; - - -(** number_of related to hypreal_of_real **) - -Goal "(number_of w < hypreal_of_real z) = (number_of w < z)"; -by (stac (hypreal_of_real_less_iff RS sym) 1); -by (Simp_tac 1); -qed "number_of_less_hypreal_of_real_iff"; -Addsimps [number_of_less_hypreal_of_real_iff]; - -Goal "(number_of w <= hypreal_of_real z) = (number_of w <= z)"; -by (stac (hypreal_of_real_le_iff RS sym) 1); -by (Simp_tac 1); -qed "number_of_le_hypreal_of_real_iff"; -Addsimps [number_of_le_hypreal_of_real_iff]; - -Goal "(hypreal_of_real z = number_of w) = (z = number_of w)"; -by (stac (hypreal_of_real_eq_iff RS sym) 1); -by (Simp_tac 1); -qed "hypreal_of_real_eq_number_of_iff"; -Addsimps [hypreal_of_real_eq_number_of_iff]; - -Goal "(hypreal_of_real z < number_of w) = (z < number_of w)"; -by (stac (hypreal_of_real_less_iff RS sym) 1); -by (Simp_tac 1); -qed "hypreal_of_real_less_number_of_iff"; -Addsimps [hypreal_of_real_less_number_of_iff]; - -Goal "(hypreal_of_real z <= number_of w) = (z <= number_of w)"; -by (stac (hypreal_of_real_le_iff RS sym) 1); -by (Simp_tac 1); -qed "hypreal_of_real_le_number_of_iff"; -Addsimps [hypreal_of_real_le_number_of_iff]; - -(*As above, for the special case of zero*) -Addsimps - (map (simplify (simpset()) o inst "w" "bin.Pls") - [hypreal_of_real_eq_number_of_iff, - hypreal_of_real_le_number_of_iff, hypreal_of_real_less_number_of_iff, - number_of_le_hypreal_of_real_iff, number_of_less_hypreal_of_real_iff]); - -(*As above, for the special case of one*) -Addsimps - (map (simplify (simpset()) o inst "w" "bin.Pls BIT True") - [hypreal_of_real_eq_number_of_iff, - hypreal_of_real_le_number_of_iff, hypreal_of_real_less_number_of_iff, - number_of_le_hypreal_of_real_iff, number_of_less_hypreal_of_real_iff]); - -Addsimps [hypreal_minus_1_eq_m1]; diff -r 2763da611ad9 -r c50188fe6366 src/HOL/Hyperreal/HyperBin.thy --- a/src/HOL/Hyperreal/HyperBin.thy Wed Jan 28 10:41:49 2004 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,21 +0,0 @@ -(* Title: HOL/HyperBin.thy - ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1999 University of Cambridge - -Binary arithmetic for the hyperreals - -This case is reduced to that for the reals. -*) - -HyperBin = HyperOrd + - -instance - hypreal :: number - -defs - hypreal_number_of_def - "number_of v == hypreal_of_real (number_of v)" - (*::bin=>hypreal ::bin=>real*) - -end diff -r 2763da611ad9 -r c50188fe6366 src/HOL/Hyperreal/HyperDef.thy --- a/src/HOL/Hyperreal/HyperDef.thy Wed Jan 28 10:41:49 2004 +0100 +++ b/src/HOL/Hyperreal/HyperDef.thy Wed Jan 28 17:01:01 2004 +0100 @@ -766,58 +766,75 @@ subsection{*@{term hypreal_of_real} Preserves Field and Order Properties*} lemma hypreal_of_real_add [simp]: - "hypreal_of_real (z1 + z2) = hypreal_of_real z1 + hypreal_of_real z2" + "hypreal_of_real (w + z) = hypreal_of_real w + hypreal_of_real z" apply (unfold hypreal_of_real_def) apply (simp add: hypreal_add left_distrib) done lemma hypreal_of_real_mult [simp]: - "hypreal_of_real (z1 * z2) = hypreal_of_real z1 * hypreal_of_real z2" + "hypreal_of_real (w * z) = hypreal_of_real w * hypreal_of_real z" apply (unfold hypreal_of_real_def) apply (simp add: hypreal_mult right_distrib) done -lemma hypreal_of_real_less_iff [simp]: - "(hypreal_of_real z1 < hypreal_of_real z2) = (z1 < z2)" -apply (unfold hypreal_less_def hypreal_of_real_def, auto) -apply (rule_tac [2] x = "%n. z1" in exI, safe) -apply (rule_tac [3] x = "%n. z2" in exI, auto) -apply (rule FreeUltrafilterNat_P, ultra) -done - -lemma hypreal_of_real_le_iff [simp]: - "(hypreal_of_real z1 \ hypreal_of_real z2) = (z1 \ z2)" -by (force simp add: hypreal_less hypreal_le_def linorder_not_less[symmetric]) - -lemma hypreal_of_real_eq_iff [simp]: - "(hypreal_of_real z1 = hypreal_of_real z2) = (z1 = z2)" -by (force intro: order_antisym hypreal_of_real_le_iff [THEN iffD1]) - -lemma hypreal_of_real_minus [simp]: - "hypreal_of_real (-r) = - hypreal_of_real r" -apply (unfold hypreal_of_real_def) -apply (auto simp add: hypreal_minus) -done - lemma hypreal_of_real_one [simp]: "hypreal_of_real 1 = (1::hypreal)" by (unfold hypreal_of_real_def hypreal_one_def, simp) lemma hypreal_of_real_zero [simp]: "hypreal_of_real 0 = 0" by (unfold hypreal_of_real_def hypreal_zero_def, simp) -lemma hypreal_of_real_zero_iff: "(hypreal_of_real r = 0) = (r = 0)" -by (auto intro: FreeUltrafilterNat_P simp add: hypreal_of_real_def hypreal_zero_def FreeUltrafilterNat_Nat_set) +lemma hypreal_of_real_less_iff [simp]: + "(hypreal_of_real w < hypreal_of_real z) = (w < z)" +apply (unfold hypreal_less_def hypreal_of_real_def, auto) +apply (rule_tac [2] x = "%n. w" in exI, safe) +apply (rule_tac [3] x = "%n. z" in exI, auto) +apply (rule FreeUltrafilterNat_P, ultra) +done + +lemma hypreal_of_real_le_iff [simp]: + "(hypreal_of_real w \ hypreal_of_real z) = (w \ z)" +by (force simp add: hypreal_less hypreal_le_def linorder_not_less[symmetric]) + +lemma hypreal_of_real_eq_iff [simp]: + "(hypreal_of_real w = hypreal_of_real z) = (w = z)" +by (force intro: order_antisym hypreal_of_real_le_iff [THEN iffD1]) + +text{*As above, for 0*} + +declare hypreal_of_real_less_iff [of 0, simplified, simp] +declare hypreal_of_real_le_iff [of 0, simplified, simp] +declare hypreal_of_real_eq_iff [of 0, simplified, simp] + +declare hypreal_of_real_less_iff [of _ 0, simplified, simp] +declare hypreal_of_real_le_iff [of _ 0, simplified, simp] +declare hypreal_of_real_eq_iff [of _ 0, simplified, simp] + +text{*As above, for 1*} + +declare hypreal_of_real_less_iff [of 1, simplified, simp] +declare hypreal_of_real_le_iff [of 1, simplified, simp] +declare hypreal_of_real_eq_iff [of 1, simplified, simp] + +declare hypreal_of_real_less_iff [of _ 1, simplified, simp] +declare hypreal_of_real_le_iff [of _ 1, simplified, simp] +declare hypreal_of_real_eq_iff [of _ 1, simplified, simp] + +lemma hypreal_of_real_minus [simp]: + "hypreal_of_real (-r) = - hypreal_of_real r" +apply (unfold hypreal_of_real_def) +apply (auto simp add: hypreal_minus) +done lemma hypreal_of_real_inverse [simp]: "hypreal_of_real (inverse r) = inverse (hypreal_of_real r)" apply (case_tac "r=0") apply (simp add: DIVISION_BY_ZERO INVERSE_ZERO HYPREAL_INVERSE_ZERO) apply (rule_tac c1 = "hypreal_of_real r" in hypreal_mult_left_cancel [THEN iffD1]) -apply (auto simp add: hypreal_of_real_zero_iff hypreal_of_real_mult [symmetric]) +apply (auto simp add: hypreal_of_real_mult [symmetric]) done lemma hypreal_of_real_divide [simp]: - "hypreal_of_real (z1 / z2) = hypreal_of_real z1 / hypreal_of_real z2" + "hypreal_of_real (w / z) = hypreal_of_real w / hypreal_of_real z" by (simp add: hypreal_divide_def real_divide_def) @@ -959,7 +976,6 @@ val hypreal_of_real_minus = thm "hypreal_of_real_minus"; val hypreal_of_real_one = thm "hypreal_of_real_one"; val hypreal_of_real_zero = thm "hypreal_of_real_zero"; -val hypreal_of_real_zero_iff = thm "hypreal_of_real_zero_iff"; val hypreal_of_real_inverse = thm "hypreal_of_real_inverse"; val hypreal_of_real_divide = thm "hypreal_of_real_divide"; val hypreal_divide_one = thm "hypreal_divide_one"; diff -r 2763da611ad9 -r c50188fe6366 src/HOL/Hyperreal/HyperOrd.thy --- a/src/HOL/Hyperreal/HyperOrd.thy Wed Jan 28 10:41:49 2004 +0100 +++ b/src/HOL/Hyperreal/HyperOrd.thy Wed Jan 28 17:01:01 2004 +0100 @@ -7,10 +7,6 @@ theory HyperOrd = HyperDef: -ML -{* -val left_distrib = thm"left_distrib"; -*} (*** Monotonicity results ***) diff -r 2763da611ad9 -r c50188fe6366 src/HOL/Hyperreal/Lim.ML --- a/src/HOL/Hyperreal/Lim.ML Wed Jan 28 10:41:49 2004 +0100 +++ b/src/HOL/Hyperreal/Lim.ML Wed Jan 28 17:01:01 2004 +0100 @@ -1734,11 +1734,9 @@ by Auto_tac; by (res_inst_tac [("x","s")] exI 1 THEN Clarify_tac 1); by (res_inst_tac [("x","abs(f x) + 1")] exI 1 THEN Clarify_tac 1); -by (dres_inst_tac [("x","xa - x")] spec 1 THEN Safe_tac); -by (arith_tac 1); -by (arith_tac 1); -by (asm_full_simp_tac (simpset() addsimps [abs_ge_self]) 1); -by (arith_tac 1); +by (dres_inst_tac [("x","xa - x")] spec 1); +by (auto_tac (claset(), simpset() addsimps [abs_ge_self])); +by (REPEAT (arith_tac 1)); qed "isCont_bounded"; (*----------------------------------------------------------------------------*) diff -r 2763da611ad9 -r c50188fe6366 src/HOL/Hyperreal/Poly.ML --- a/src/HOL/Hyperreal/Poly.ML Wed Jan 28 10:41:49 2004 +0100 +++ b/src/HOL/Hyperreal/Poly.ML Wed Jan 28 17:01:01 2004 +0100 @@ -232,7 +232,7 @@ Goal "[| a < b; 0 < poly p a; poly p b < 0 |] \ \ ==> EX x. a < x & x < b & (poly p x = 0)"; by (blast_tac (claset() addIs [full_simplify (simpset() - addsimps [poly_minus, rename_numerals neg_less_0_iff_less]) + addsimps [poly_minus, neg_less_0_iff_less]) (read_instantiate [("p","-- p")] poly_IVT_pos)]) 1); qed "poly_IVT_neg"; diff -r 2763da611ad9 -r c50188fe6366 src/HOL/Hyperreal/hypreal_arith.ML --- a/src/HOL/Hyperreal/hypreal_arith.ML Wed Jan 28 10:41:49 2004 +0100 +++ b/src/HOL/Hyperreal/hypreal_arith.ML Wed Jan 28 17:01:01 2004 +0100 @@ -8,6 +8,358 @@ Instantiation of the generic linear arithmetic package for type hypreal. *) +(*FIXME DELETE*) +val hypreal_mult_left_mono = + read_instantiate_sg(sign_of (the_context())) [("a","?a::hypreal")] mult_left_mono; + + +val hypreal_number_of = thm "hypreal_number_of"; +val hypreal_numeral_0_eq_0 = thm "hypreal_numeral_0_eq_0"; +val hypreal_numeral_1_eq_1 = thm "hypreal_numeral_1_eq_1"; +val hypreal_number_of_def = thm "hypreal_number_of_def"; +val add_hypreal_number_of = thm "add_hypreal_number_of"; +val minus_hypreal_number_of = thm "minus_hypreal_number_of"; +val diff_hypreal_number_of = thm "diff_hypreal_number_of"; +val mult_hypreal_number_of = thm "mult_hypreal_number_of"; +val hypreal_mult_2 = thm "hypreal_mult_2"; +val hypreal_mult_2_right = thm "hypreal_mult_2_right"; +val eq_hypreal_number_of = thm "eq_hypreal_number_of"; +val less_hypreal_number_of = thm "less_hypreal_number_of"; +val hypreal_minus_1_eq_m1 = thm "hypreal_minus_1_eq_m1"; +val hypreal_mult_minus1 = thm "hypreal_mult_minus1"; +val hypreal_mult_minus1_right = thm "hypreal_mult_minus1_right"; +val hypreal_add_number_of_left = thm "hypreal_add_number_of_left"; +val hypreal_mult_number_of_left = thm "hypreal_mult_number_of_left"; +val hypreal_add_number_of_diff1 = thm "hypreal_add_number_of_diff1"; +val hypreal_add_number_of_diff2 = thm "hypreal_add_number_of_diff2"; + +(*Maps 0 to Numeral0 and 1 to Numeral1 and -(Numeral1) to -1*) +val hypreal_numeral_ss = + real_numeral_ss addsimps [hypreal_numeral_0_eq_0 RS sym, + hypreal_numeral_1_eq_1 RS sym, + hypreal_minus_1_eq_m1] + +fun rename_numerals th = + asm_full_simplify hypreal_numeral_ss (Thm.transfer (the_context ()) th) + + +structure Hyperreal_Numeral_Simprocs = +struct + +(*Maps 0 to Numeral0 and 1 to Numeral1 so that arithmetic in simprocs + isn't complicated by the abstract 0 and 1.*) +val numeral_syms = [hypreal_numeral_0_eq_0 RS sym, + hypreal_numeral_1_eq_1 RS sym] + +(*Utilities*) + +val hyprealT = Type("HyperDef.hypreal",[]) + +fun mk_numeral n = HOLogic.number_of_const hyprealT $ HOLogic.mk_bin n + +val dest_numeral = Real_Numeral_Simprocs.dest_numeral + +val find_first_numeral = Real_Numeral_Simprocs.find_first_numeral + +val zero = mk_numeral 0 +val mk_plus = Real_Numeral_Simprocs.mk_plus + +val uminus_const = Const ("uminus", hyprealT --> hyprealT) + +(*Thus mk_sum[t] yields t+0; longer sums don't have a trailing zero*) +fun mk_sum [] = zero + | mk_sum [t,u] = mk_plus (t, u) + | mk_sum (t :: ts) = mk_plus (t, mk_sum ts) + +(*this version ALWAYS includes a trailing zero*) +fun long_mk_sum [] = zero + | long_mk_sum (t :: ts) = mk_plus (t, mk_sum ts) + +val dest_plus = HOLogic.dest_bin "op +" hyprealT + +(*decompose additions AND subtractions as a sum*) +fun dest_summing (pos, Const ("op +", _) $ t $ u, ts) = + dest_summing (pos, t, dest_summing (pos, u, ts)) + | dest_summing (pos, Const ("op -", _) $ t $ u, ts) = + dest_summing (pos, t, dest_summing (not pos, u, ts)) + | dest_summing (pos, t, ts) = + if pos then t::ts else uminus_const$t :: ts + +fun dest_sum t = dest_summing (true, t, []) + +val mk_diff = HOLogic.mk_binop "op -" +val dest_diff = HOLogic.dest_bin "op -" hyprealT + +val one = mk_numeral 1 +val mk_times = HOLogic.mk_binop "op *" + +fun mk_prod [] = one + | mk_prod [t] = t + | mk_prod (t :: ts) = if t = one then mk_prod ts + else mk_times (t, mk_prod ts) + +val dest_times = HOLogic.dest_bin "op *" hyprealT + +fun dest_prod t = + let val (t,u) = dest_times t + in dest_prod t @ dest_prod u end + handle TERM _ => [t] + +(*DON'T do the obvious simplifications; that would create special cases*) +fun mk_coeff (k, ts) = mk_times (mk_numeral k, ts) + +(*Express t as a product of (possibly) a numeral with other sorted terms*) +fun dest_coeff sign (Const ("uminus", _) $ t) = dest_coeff (~sign) t + | dest_coeff sign t = + let val ts = sort Term.term_ord (dest_prod t) + val (n, ts') = find_first_numeral [] ts + handle TERM _ => (1, ts) + in (sign*n, mk_prod ts') end + +(*Find first coefficient-term THAT MATCHES u*) +fun find_first_coeff past u [] = raise TERM("find_first_coeff", []) + | find_first_coeff past u (t::terms) = + let val (n,u') = dest_coeff 1 t + in if u aconv u' then (n, rev past @ terms) + else find_first_coeff (t::past) u terms + end + handle TERM _ => find_first_coeff (t::past) u terms + + +(*Simplify Numeral0+n, n+Numeral0, Numeral1*n, n*Numeral1*) +val add_0s = map rename_numerals + [hypreal_add_zero_left, hypreal_add_zero_right] +val mult_1s = map rename_numerals [hypreal_mult_1, hypreal_mult_1_right] @ + [hypreal_mult_minus1, hypreal_mult_minus1_right] + +(*To perform binary arithmetic*) +val bin_simps = + [hypreal_numeral_0_eq_0 RS sym, hypreal_numeral_1_eq_1 RS sym, + add_hypreal_number_of, hypreal_add_number_of_left, + minus_hypreal_number_of, + diff_hypreal_number_of, mult_hypreal_number_of, + hypreal_mult_number_of_left] @ bin_arith_simps @ bin_rel_simps + +(*Binary arithmetic BUT NOT ADDITION since it may collapse adjacent terms + during re-arrangement*) +val non_add_bin_simps = + bin_simps \\ [hypreal_add_number_of_left, add_hypreal_number_of] + +(*To evaluate binary negations of coefficients*) +val hypreal_minus_simps = NCons_simps @ + [hypreal_minus_1_eq_m1, minus_hypreal_number_of, + bin_minus_1, bin_minus_0, bin_minus_Pls, bin_minus_Min, + bin_pred_1, bin_pred_0, bin_pred_Pls, bin_pred_Min] + +(*To let us treat subtraction as addition*) +val diff_simps = [hypreal_diff_def, minus_add_distrib, minus_minus] + +(*push the unary minus down: - x * y = x * - y *) +val hypreal_minus_mult_eq_1_to_2 = + [minus_mult_left RS sym, minus_mult_right] MRS trans + |> standard + +(*to extract again any uncancelled minuses*) +val hypreal_minus_from_mult_simps = + [minus_minus, minus_mult_left RS sym, minus_mult_right RS sym] + +(*combine unary minus with numeric literals, however nested within a product*) +val hypreal_mult_minus_simps = + [hypreal_mult_assoc, minus_mult_left, hypreal_minus_mult_eq_1_to_2] + +(*Final simplification: cancel + and * *) +val simplify_meta_eq = + Int_Numeral_Simprocs.simplify_meta_eq + [hypreal_add_zero_left, hypreal_add_zero_right, + mult_zero_left, mult_zero_right, mult_1, mult_1_right] + +val prep_simproc = Real_Numeral_Simprocs.prep_simproc + +structure CancelNumeralsCommon = + struct + val mk_sum = mk_sum + val dest_sum = dest_sum + val mk_coeff = mk_coeff + val dest_coeff = dest_coeff 1 + val find_first_coeff = find_first_coeff [] + val trans_tac = Real_Numeral_Simprocs.trans_tac + val norm_tac = + ALLGOALS (simp_tac (HOL_ss addsimps add_0s@mult_1s@diff_simps@ + hypreal_minus_simps@add_ac)) + THEN ALLGOALS (simp_tac (HOL_ss addsimps non_add_bin_simps@hypreal_mult_minus_simps)) + THEN ALLGOALS + (simp_tac (HOL_ss addsimps hypreal_minus_from_mult_simps@ + add_ac@mult_ac)) + val numeral_simp_tac = ALLGOALS (simp_tac (HOL_ss addsimps add_0s@bin_simps)) + val simplify_meta_eq = simplify_meta_eq + end + + +structure EqCancelNumerals = CancelNumeralsFun + (open CancelNumeralsCommon + val prove_conv = Bin_Simprocs.prove_conv + val mk_bal = HOLogic.mk_eq + val dest_bal = HOLogic.dest_bin "op =" hyprealT + val bal_add1 = eq_add_iff1 RS trans + val bal_add2 = eq_add_iff2 RS trans +) + +structure LessCancelNumerals = CancelNumeralsFun + (open CancelNumeralsCommon + val prove_conv = Bin_Simprocs.prove_conv + val mk_bal = HOLogic.mk_binrel "op <" + val dest_bal = HOLogic.dest_bin "op <" hyprealT + val bal_add1 = less_add_iff1 RS trans + val bal_add2 = less_add_iff2 RS trans +) + +structure LeCancelNumerals = CancelNumeralsFun + (open CancelNumeralsCommon + val prove_conv = Bin_Simprocs.prove_conv + val mk_bal = HOLogic.mk_binrel "op <=" + val dest_bal = HOLogic.dest_bin "op <=" hyprealT + val bal_add1 = le_add_iff1 RS trans + val bal_add2 = le_add_iff2 RS trans +) + +val cancel_numerals = + map prep_simproc + [("hyprealeq_cancel_numerals", + ["(l::hypreal) + m = n", "(l::hypreal) = m + n", + "(l::hypreal) - m = n", "(l::hypreal) = m - n", + "(l::hypreal) * m = n", "(l::hypreal) = m * n"], + EqCancelNumerals.proc), + ("hyprealless_cancel_numerals", + ["(l::hypreal) + m < n", "(l::hypreal) < m + n", + "(l::hypreal) - m < n", "(l::hypreal) < m - n", + "(l::hypreal) * m < n", "(l::hypreal) < m * n"], + LessCancelNumerals.proc), + ("hyprealle_cancel_numerals", + ["(l::hypreal) + m <= n", "(l::hypreal) <= m + n", + "(l::hypreal) - m <= n", "(l::hypreal) <= m - n", + "(l::hypreal) * m <= n", "(l::hypreal) <= m * n"], + LeCancelNumerals.proc)] + + +structure CombineNumeralsData = + struct + val add = op + : int*int -> int + val mk_sum = long_mk_sum (*to work for e.g. 2*x + 3*x *) + val dest_sum = dest_sum + val mk_coeff = mk_coeff + val dest_coeff = dest_coeff 1 + val left_distrib = combine_common_factor RS trans + val prove_conv = Bin_Simprocs.prove_conv_nohyps + val trans_tac = Real_Numeral_Simprocs.trans_tac + val norm_tac = + ALLGOALS (simp_tac (HOL_ss addsimps numeral_syms@add_0s@mult_1s@ + diff_simps@hypreal_minus_simps@add_ac)) + THEN ALLGOALS (simp_tac (HOL_ss addsimps non_add_bin_simps@hypreal_mult_minus_simps)) + THEN ALLGOALS (simp_tac (HOL_ss addsimps hypreal_minus_from_mult_simps@ + add_ac@mult_ac)) + val numeral_simp_tac = ALLGOALS + (simp_tac (HOL_ss addsimps add_0s@bin_simps)) + val simplify_meta_eq = simplify_meta_eq + end + +structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData) + +val combine_numerals = + prep_simproc + ("hypreal_combine_numerals", ["(i::hypreal) + j", "(i::hypreal) - j"], CombineNumerals.proc) + + +(** Declarations for ExtractCommonTerm **) + +(*this version ALWAYS includes a trailing one*) +fun long_mk_prod [] = one + | long_mk_prod (t :: ts) = mk_times (t, mk_prod ts) + +(*Find first term that matches u*) +fun find_first past u [] = raise TERM("find_first", []) + | find_first past u (t::terms) = + if u aconv t then (rev past @ terms) + else find_first (t::past) u terms + handle TERM _ => find_first (t::past) u terms + +(*Final simplification: cancel + and * *) +fun cancel_simplify_meta_eq cancel_th th = + Int_Numeral_Simprocs.simplify_meta_eq + [mult_1, mult_1_right] + (([th, cancel_th]) MRS trans) + +(*** Making constant folding work for 0 and 1 too ***) + +structure HyperrealAbstractNumeralsData = + struct + val dest_eq = HOLogic.dest_eq o HOLogic.dest_Trueprop o concl_of + val is_numeral = Bin_Simprocs.is_numeral + val numeral_0_eq_0 = hypreal_numeral_0_eq_0 + val numeral_1_eq_1 = hypreal_numeral_1_eq_1 + val prove_conv = Bin_Simprocs.prove_conv_nohyps_novars + fun norm_tac simps = ALLGOALS (simp_tac (HOL_ss addsimps simps)) + val simplify_meta_eq = Bin_Simprocs.simplify_meta_eq + end + +structure HyperrealAbstractNumerals = + AbstractNumeralsFun (HyperrealAbstractNumeralsData) + +(*For addition, we already have rules for the operand 0. + Multiplication is omitted because there are already special rules for + both 0 and 1 as operands. Unary minus is trivial, just have - 1 = -1. + For the others, having three patterns is a compromise between just having + one (many spurious calls) and having nine (just too many!) *) +val eval_numerals = + map prep_simproc + [("hypreal_add_eval_numerals", + ["(m::hypreal) + 1", "(m::hypreal) + number_of v"], + HyperrealAbstractNumerals.proc add_hypreal_number_of), + ("hypreal_diff_eval_numerals", + ["(m::hypreal) - 1", "(m::hypreal) - number_of v"], + HyperrealAbstractNumerals.proc diff_hypreal_number_of), + ("hypreal_eq_eval_numerals", + ["(m::hypreal) = 0", "(m::hypreal) = 1", "(m::hypreal) = number_of v"], + HyperrealAbstractNumerals.proc eq_hypreal_number_of), + ("hypreal_less_eval_numerals", + ["(m::hypreal) < 0", "(m::hypreal) < 1", "(m::hypreal) < number_of v"], + HyperrealAbstractNumerals.proc less_hypreal_number_of), + ("hypreal_le_eval_numerals", + ["(m::hypreal) <= 0", "(m::hypreal) <= 1", "(m::hypreal) <= number_of v"], + HyperrealAbstractNumerals.proc le_number_of_eq_not_less)] + +end; + +Addsimprocs Hyperreal_Numeral_Simprocs.eval_numerals; +Addsimprocs Hyperreal_Numeral_Simprocs.cancel_numerals; +Addsimprocs [Hyperreal_Numeral_Simprocs.combine_numerals]; + + + + +(**** Constant folding for hypreal plus and times ****) + +(*We do not need + structure Hyperreal_Plus_Assoc = Assoc_Fold (Hyperreal_Plus_Assoc_Data) + because combine_numerals does the same thing*) + +structure Hyperreal_Times_Assoc_Data : ASSOC_FOLD_DATA = +struct + val ss = HOL_ss + val eq_reflection = eq_reflection + val sg_ref = Sign.self_ref (Theory.sign_of (the_context ())) + val T = Hyperreal_Numeral_Simprocs.hyprealT + val plus = Const ("op *", [T,T] ---> T) + val add_ac = mult_ac +end; + +structure Hyperreal_Times_Assoc = Assoc_Fold (Hyperreal_Times_Assoc_Data); + +Addsimprocs [Hyperreal_Times_Assoc.conv]; + + + +(**** Simprocs for numeric literals ****) + (****Common factor cancellation****) @@ -16,7 +368,7 @@ in val rel_hypreal_number_of = [eq_hypreal_number_of, less_hypreal_number_of, - le_hypreal_number_of_eq_not_less]; + le_number_of_eq_not_less]; structure CancelNumeralFactorCommon = struct @@ -95,42 +447,6 @@ Addsimprocs hypreal_cancel_numeral_factors; -(*examples: -print_depth 22; -set timing; -set trace_simp; -fun test s = (Goal s; by (Simp_tac 1)); - -test "0 <= (y::hypreal) * -2"; -test "9*x = 12 * (y::hypreal)"; -test "(9*x) / (12 * (y::hypreal)) = z"; -test "9*x < 12 * (y::hypreal)"; -test "9*x <= 12 * (y::hypreal)"; - -test "-99*x = 123 * (y::hypreal)"; -test "(-99*x) / (123 * (y::hypreal)) = z"; -test "-99*x < 123 * (y::hypreal)"; -test "-99*x <= 123 * (y::hypreal)"; - -test "999*x = -396 * (y::hypreal)"; -test "(999*x) / (-396 * (y::hypreal)) = z"; -test "999*x < -396 * (y::hypreal)"; -test "999*x <= -396 * (y::hypreal)"; - -test "-99*x = -81 * (y::hypreal)"; -test "(-99*x) / (-81 * (y::hypreal)) = z"; -test "-99*x <= -81 * (y::hypreal)"; -test "-99*x < -81 * (y::hypreal)"; - -test "-2 * x = -1 * (y::hypreal)"; -test "-2 * x = -(y::hypreal)"; -test "(-2 * x) / (-1 * (y::hypreal)) = z"; -test "-2 * x < -(y::hypreal)"; -test "-2 * x <= -1 * (y::hypreal)"; -test "-x < -23 * (y::hypreal)"; -test "-x <= -23 * (y::hypreal)"; -*) - (** Declarations for ExtractCommonTerm **) @@ -178,66 +494,18 @@ Addsimprocs hypreal_cancel_factor; -(*examples: -print_depth 22; -set timing; -set trace_simp; -fun test s = (Goal s; by (Asm_simp_tac 1)); - -test "x*k = k*(y::hypreal)"; -test "k = k*(y::hypreal)"; -test "a*(b*c) = (b::hypreal)"; -test "a*(b*c) = d*(b::hypreal)*(x*a)"; - - -test "(x*k) / (k*(y::hypreal)) = (uu::hypreal)"; -test "(k) / (k*(y::hypreal)) = (uu::hypreal)"; -test "(a*(b*c)) / ((b::hypreal)) = (uu::hypreal)"; -test "(a*(b*c)) / (d*(b::hypreal)*(x*a)) = (uu::hypreal)"; - -(*FIXME: what do we do about this?*) -test "a*(b*c)/(y*z) = d*(b::hypreal)*(x*a)/z"; -*) (****Instantiation of the generic linear arithmetic package****) -val hypreal_mult_left_mono = - read_instantiate_sg(sign_of HyperBin.thy) [("a","?a::hypreal")] - mult_left_mono; - local (* reduce contradictory <= to False *) val add_rules = - [order_less_irrefl, hypreal_numeral_0_eq_0, hypreal_numeral_1_eq_1, + [hypreal_numeral_0_eq_0, hypreal_numeral_1_eq_1, add_hypreal_number_of, minus_hypreal_number_of, diff_hypreal_number_of, - mult_hypreal_number_of, eq_hypreal_number_of, less_hypreal_number_of, - le_hypreal_number_of_eq_not_less, hypreal_diff_def, - minus_add_distrib, minus_minus, mult_assoc, minus_zero, - hypreal_add_zero_left, hypreal_add_zero_right, - hypreal_add_minus, hypreal_add_minus_left, - mult_zero_left, mult_zero_right, - mult_1, mult_1_right, - hypreal_mult_minus_1, hypreal_mult_minus_1_right]; - -val mono_ss = simpset() addsimps - [add_mono, add_strict_mono, - hypreal_add_less_le_mono,hypreal_add_le_less_mono]; - -val add_mono_thms_hypreal = - map (fn s => prove_goal (the_context ()) s - (fn prems => [cut_facts_tac prems 1, asm_simp_tac mono_ss 1])) - ["(i <= j) & (k <= l) ==> i + k <= j + (l::hypreal)", - "(i = j) & (k <= l) ==> i + k <= j + (l::hypreal)", - "(i <= j) & (k = l) ==> i + k <= j + (l::hypreal)", - "(i = j) & (k = l) ==> i + k = j + (l::hypreal)", - "(i < j) & (k = l) ==> i + k < j + (l::hypreal)", - "(i = j) & (k < l) ==> i + k < j + (l::hypreal)", - "(i < j) & (k <= l) ==> i + k < j + (l::hypreal)", - "(i <= j) & (k < l) ==> i + k < j + (l::hypreal)", - "(i < j) & (k < l) ==> i + k < j + (l::hypreal)"]; + mult_hypreal_number_of, eq_hypreal_number_of, less_hypreal_number_of]; val simprocs = [Hyperreal_Times_Assoc.conv, Hyperreal_Numeral_Simprocs.combine_numerals, @@ -245,11 +513,6 @@ Hyperreal_Numeral_Simprocs.cancel_numerals @ Hyperreal_Numeral_Simprocs.eval_numerals; -(* reduce contradictory <= to False *) -val simps = [True_implies_equals, - inst "a" "(number_of ?v)::hypreal" right_distrib, - divide_1,times_divide_eq_right,times_divide_eq_left]; - fun cvar(th,_ $ (_ $ _ $ var)) = cterm_of (#sign(rep_thm th)) var; val hypreal_mult_mono_thms = @@ -258,6 +521,10 @@ (hypreal_mult_left_mono, cvar(hypreal_mult_left_mono, hd(tl(prems_of hypreal_mult_left_mono))))] +val real_inj_thms = [hypreal_of_real_le_iff RS iffD2, + hypreal_of_real_less_iff RS iffD2, + hypreal_of_real_eq_iff RS iffD2]; + in val fast_hypreal_arith_simproc = @@ -268,58 +535,18 @@ val hypreal_arith_setup = [Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset} => - {add_mono_thms = add_mono_thms @ add_mono_thms_hypreal, + {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms @ hypreal_mult_mono_thms, - inj_thms = inj_thms, (*FIXME: add hypreal*) + inj_thms = inj_thms @ real_inj_thms, lessD = lessD, (*Can't change LA_Data_Ref.lessD: the hypreals are dense!*) simpset = simpset addsimps add_rules - addsimps simps addsimprocs simprocs}), + arith_inj_const ("HyperDef.hypreal_of_real", + HOLogic.realT --> Hyperreal_Numeral_Simprocs.hyprealT), arith_discrete ("HyperDef.hypreal",false), Simplifier.change_simpset_of (op addsimprocs) [fast_hypreal_arith_simproc]]; end; -(* Some test data [omitting examples that assume the ordering to be discrete!] -Goal "!!a::hypreal. [| a <= b; c <= d; x+y a+c <= b+d"; -by (fast_arith_tac 1); -qed ""; -Goal "!!a::hypreal. [| a <= b; b+b <= c |] ==> a+a <= c"; -by (fast_arith_tac 1); -qed ""; - -Goal "!!a::hypreal. [| a+b <= i+j; a<=b; i<=j |] ==> a+a <= j+j"; -by (fast_arith_tac 1); -qed ""; - -Goal "!!a::hypreal. a+b+c <= i+j+k & a<=b & b<=c & i<=j & j<=k --> a+a+a <= k+k+k"; -by (arith_tac 1); -qed ""; - -Goal "!!a::hypreal. [| 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); -qed ""; - -Goal "!!a::hypreal. [| 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); -qed ""; - -Goal "!!a::hypreal. [| 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); -qed ""; - -Goal "!!a::hypreal. [| 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); -qed ""; - -Goal "!!a::hypreal. [| 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); -qed ""; -*) diff -r 2763da611ad9 -r c50188fe6366 src/HOL/Integ/int_arith1.ML --- a/src/HOL/Integ/int_arith1.ML Wed Jan 28 10:41:49 2004 +0100 +++ b/src/HOL/Integ/int_arith1.ML Wed Jan 28 17:01:01 2004 +0100 @@ -516,13 +516,12 @@ val add_rules = simp_thms @ bin_arith_simps @ bin_rel_simps @ [int_numeral_0_eq_0, int_numeral_1_eq_1, - zminus_0, zdiff_def, - zadd_zminus_inverse, zadd_zminus_inverse2, - zmult_0, zmult_0_right, - zmult_1, zmult_1_right, - zmult_zminus, zmult_zminus_right, - zminus_zadd_distrib, zminus_zminus, zmult_assoc, - int_0, int_1, int_Suc, zadd_int RS sym, zmult_int RS sym]; + minus_zero, diff_minus, left_minus, right_minus, + mult_zero_left, mult_zero_right, mult_1, mult_1_right, + minus_mult_left RS sym, minus_mult_right RS sym, + minus_add_distrib, minus_minus, mult_assoc, + int_0, int_1, int_Suc, zadd_int RS sym, zmult_int RS sym, + le_number_of_eq_not_less]; val simprocs = [Int_Times_Assoc.conv, Int_Numeral_Simprocs.combine_numerals]@ Int_Numeral_Simprocs.cancel_numerals @ diff -r 2763da611ad9 -r c50188fe6366 src/HOL/Integ/nat_simprocs.ML --- a/src/HOL/Integ/nat_simprocs.ML Wed Jan 28 10:41:49 2004 +0100 +++ b/src/HOL/Integ/nat_simprocs.ML Wed Jan 28 17:01:01 2004 +0100 @@ -510,9 +510,9 @@ le_Suc_number_of,le_number_of_Suc, less_Suc_number_of,less_number_of_Suc, Suc_eq_number_of,eq_number_of_Suc, - mult_0, mult_0_right, mult_Suc, mult_Suc_right, + mult_Suc, mult_Suc_right, eq_number_of_0, eq_0_number_of, less_0_number_of, - nat_number_of, thm "Let_number_of", if_True, if_False]; + nat_number_of, if_True, if_False]; val simprocs = [Nat_Times_Assoc.conv, Nat_Numeral_Simprocs.combine_numerals]@ diff -r 2763da611ad9 -r c50188fe6366 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Wed Jan 28 10:41:49 2004 +0100 +++ b/src/HOL/IsaMakefile Wed Jan 28 17:01:01 2004 +0100 @@ -147,7 +147,7 @@ Hyperreal/Fact.ML Hyperreal/Fact.thy\ Hyperreal/Filter.ML Hyperreal/Filter.thy\ Hyperreal/HRealAbs.thy Hyperreal/HSeries.ML Hyperreal/HSeries.thy\ - Hyperreal/HyperArith.thy Hyperreal/HyperBin.ML Hyperreal/HyperBin.thy \ + Hyperreal/HyperArith.thy \ Hyperreal/HyperDef.thy Hyperreal/HyperNat.ML Hyperreal/HyperNat.thy\ Hyperreal/HyperOrd.thy Hyperreal/HyperPow.thy Hyperreal/Hyperreal.thy\ Hyperreal/IntFloor.thy Hyperreal/IntFloor.ML\ diff -r 2763da611ad9 -r c50188fe6366 src/HOL/Real/PReal.thy --- a/src/HOL/Real/PReal.thy Wed Jan 28 10:41:49 2004 +0100 +++ b/src/HOL/Real/PReal.thy Wed Jan 28 17:01:01 2004 +0100 @@ -694,14 +694,13 @@ subsection{*Gleason's Lemma 9-3.4, page 122*} -(*????Why can't I get case_names like nonneg to work?*) lemma Gleason9_34_exists: assumes A: "A \ preal" - and closed: "\x\A. x + u \ A" - and nonneg: "0 \ z" + and "\x\A. x + u \ A" + and "0 \ z" shows "\b\A. b + (rat z) * u \ A" -proof (cases z) - case (1 n) +proof (cases z rule: int_cases) + case (nonneg n) show ?thesis proof (simp add: prems, induct n) case 0 @@ -709,12 +708,12 @@ show ?case by force case (Suc k) from this obtain b where "b \ A" "b + rat (int k) * u \ A" .. - hence "b + rat (int k)*u + u \ A" by (simp add: closed) + hence "b + rat (int k)*u + u \ A" by (simp add: prems) thus ?case by (force simp add: left_distrib add_ac prems) qed next - case (2 n) - with nonneg show ?thesis by simp + case (neg n) + with prems show ?thesis by simp qed diff -r 2763da611ad9 -r c50188fe6366 src/HOL/Real/RealArith.thy --- a/src/HOL/Real/RealArith.thy Wed Jan 28 10:41:49 2004 +0100 +++ b/src/HOL/Real/RealArith.thy Wed Jan 28 17:01:01 2004 +0100 @@ -2,11 +2,9 @@ ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1999 University of Cambridge - -Binary arithmetic and simplification for the reals +*) -This case is reduced to that for the integers -*) +header{*Binary arithmetic and Simplification for the Reals*} theory RealArith = RealDef files ("real_arith.ML"): @@ -148,11 +146,6 @@ declare real_numeral_0_eq_0 [simp] real_numeral_1_eq_1 [simp] -(*Simplification of x-y < 0, etc.*) -declare less_iff_diff_less_0 [symmetric, iff] -declare eq_iff_diff_eq_0 [symmetric, iff] -declare le_iff_diff_le_0 [symmetric, iff] - use "real_arith.ML" diff -r 2763da611ad9 -r c50188fe6366 src/HOL/Real/RealDef.thy --- a/src/HOL/Real/RealDef.thy Wed Jan 28 10:41:49 2004 +0100 +++ b/src/HOL/Real/RealDef.thy Wed Jan 28 17:01:01 2004 +0100 @@ -1017,7 +1017,6 @@ lemma real_of_nat_ge_zero_cancel_iff [simp]: "(0 \ real (n::nat)) = (0 \ n)" by (simp add: linorder_not_less) -text{*Now obsolete, but used in Hyperreal/IntFloor???*} lemma real_of_int_real_of_nat: "real (int n) = real n" by (simp add: real_of_nat_def) diff -r 2763da611ad9 -r c50188fe6366 src/HOL/Real/rat_arith.ML --- a/src/HOL/Real/rat_arith.ML Wed Jan 28 10:41:49 2004 +0100 +++ b/src/HOL/Real/rat_arith.ML Wed Jan 28 17:01:01 2004 +0100 @@ -585,12 +585,7 @@ [order_less_irrefl, rat_numeral_0_eq_0, rat_numeral_1_eq_1, rat_minus_1_eq_m1, add_rat_number_of, minus_rat_number_of, diff_rat_number_of, - mult_rat_number_of, eq_rat_number_of, less_rat_number_of, - le_number_of_eq_not_less, diff_minus, - minus_add_distrib, minus_minus, mult_assoc, minus_zero, - left_minus, right_minus, - mult_zero_left, mult_zero_right, mult_1, mult_1_right, - minus_mult_left RS sym, minus_mult_right RS sym]; + mult_rat_number_of, eq_rat_number_of, less_rat_number_of]; val simprocs = [Rat_Times_Assoc.conv, Rat_Numeral_Simprocs.combine_numerals, rat_cancel_numeral_factors_divide]@ @@ -617,17 +612,16 @@ (rat_mult_left_mono, cvar(rat_mult_left_mono, hd(tl(prems_of rat_mult_left_mono))))] -(* reduce contradictory <= to False *) val simps = [True_implies_equals, - inst "a" "(number_of ?v)::rat" right_distrib, - divide_1,times_divide_eq_right,times_divide_eq_left, - rat_of_int_zero, rat_of_int_one, rat_of_int_add_distrib, - rat_of_int_minus_distrib, rat_of_int_diff_distrib, - rat_of_int_mult_distrib, number_of_rat RS sym]; + inst "a" "(number_of ?v)" right_distrib, + divide_1, times_divide_eq_right, times_divide_eq_left, + rat_of_int_zero, rat_of_int_one, rat_of_int_add_distrib, + rat_of_int_minus_distrib, rat_of_int_diff_distrib, + rat_of_int_mult_distrib, number_of_rat RS sym]; in -val fast_rat_arith_simproc = Simplifier.simproc (Theory.sign_of (the_context ())) +val fast_rat_arith_simproc = Simplifier.simproc (Theory.sign_of(the_context())) "fast_rat_arith" ["(m::rat) < n","(m::rat) <= n", "(m::rat) = n"] Fast_Arith.lin_arith_prover; @@ -638,14 +632,12 @@ [Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset} => {add_mono_thms = add_mono_thms @ add_mono_thms_ordered_field, mult_mono_thms = mult_mono_thms @ rat_mult_mono_thms, - inj_thms = (***int_inj_thms @*???**) inj_thms, + inj_thms = int_inj_thms @ inj_thms, lessD = lessD, (*Can't change LA_Data_Ref.lessD: the rats are dense!*) simpset = simpset addsimps add_rules addsimps simps addsimprocs simprocs}), -(*??? arith_inj_const ("Rational.rat", HOLogic.intT --> Rat_Numeral_Simprocs.ratT), -???*) arith_discrete ("Rational.rat",false), Simplifier.change_simpset_of (op addsimprocs) [fast_rat_arith_simproc]]; diff -r 2763da611ad9 -r c50188fe6366 src/HOL/Real/real_arith.ML --- a/src/HOL/Real/real_arith.ML Wed Jan 28 10:41:49 2004 +0100 +++ b/src/HOL/Real/real_arith.ML Wed Jan 28 17:01:01 2004 +0100 @@ -595,15 +595,9 @@ (* reduce contradictory <= to False *) val add_rules = - [order_less_irrefl, real_numeral_0_eq_0, real_numeral_1_eq_1, - real_minus_1_eq_m1, + [real_numeral_0_eq_0, real_numeral_1_eq_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_number_of_eq_not_less, diff_minus, - minus_add_distrib, minus_minus, mult_assoc, minus_zero, - left_minus, right_minus, - mult_zero_left, mult_zero_right, mult_1, mult_1_right, - minus_mult_left RS sym, minus_mult_right RS sym]; + mult_real_number_of, eq_real_number_of, less_real_number_of]; val simprocs = [Real_Times_Assoc.conv, Real_Numeral_Simprocs.combine_numerals, real_cancel_numeral_factors_divide]@ @@ -618,14 +612,10 @@ (real_mult_left_mono, cvar(real_mult_left_mono, hd(tl(prems_of real_mult_left_mono))))] -(* reduce contradictory <= to False *) -val simps = [True_implies_equals, - inst "a" "(number_of ?v)::real" right_distrib, - divide_1,times_divide_eq_right,times_divide_eq_left, - real_of_nat_zero, real_of_nat_Suc, real_of_nat_add, real_of_nat_mult, - real_of_int_zero, real_of_one, real_of_int_add RS sym, - real_of_int_minus RS sym, real_of_int_diff RS sym, - real_of_int_mult RS sym, symmetric real_number_of_def]; +val simps = [real_of_nat_zero, real_of_nat_Suc, real_of_nat_add, + real_of_nat_mult, real_of_int_zero, real_of_one, real_of_int_add RS sym, + real_of_int_minus RS sym, real_of_int_diff RS sym, + real_of_int_mult RS sym, symmetric real_number_of_def]; val int_inj_thms = [real_of_int_le_iff RS iffD2, real_of_int_less_iff RS iffD2, real_of_int_inject RS iffD2];