--- 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
--- 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];
--- 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
--- 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 \<le> hypreal_of_real z2) = (z1 \<le> 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 \<le> hypreal_of_real z) = (w \<le> 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";
--- 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 ***)
--- 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";
(*----------------------------------------------------------------------------*)
--- 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";
--- 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<z |] ==> 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 "";
-*)
--- 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 @
--- 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]@
--- 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\
--- 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 \<in> preal"
- and closed: "\<forall>x\<in>A. x + u \<in> A"
- and nonneg: "0 \<le> z"
+ and "\<forall>x\<in>A. x + u \<in> A"
+ and "0 \<le> z"
shows "\<exists>b\<in>A. b + (rat z) * u \<in> 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 \<in> A" "b + rat (int k) * u \<in> A" ..
- hence "b + rat (int k)*u + u \<in> A" by (simp add: closed)
+ hence "b + rat (int k)*u + u \<in> 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
--- 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"
--- 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 \<le> real (n::nat)) = (0 \<le> 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)
--- 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]];
--- 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];