--- a/src/HOL/Complex/CStar.ML Thu Feb 05 10:45:28 2004 +0100
+++ b/src/HOL/Complex/CStar.ML Tue Feb 10 12:02:11 2004 +0100
@@ -404,10 +404,9 @@
Goal "( *fcNat* (%n. z ^ n)) N = (hcomplex_of_complex z) hcpow N";
*)
-Goalw [hypnat_of_nat_def]
- "( *fc* (%z. z ^ n)) Z = Z hcpow hypnat_of_nat n";
+Goal "( *fc* (%z. z ^ n)) Z = Z hcpow hypnat_of_nat n";
by (res_inst_tac [("z","Z")] eq_Abs_hcomplex 1);
-by (auto_tac (claset(), simpset() addsimps [hcpow,starfunC]));
+by (auto_tac (claset(), simpset() addsimps [hcpow,starfunC,hypnat_of_nat_eq]));
qed "starfunC_hcpow";
Goal "( *fc* (%h. f (x + h))) xa = ( *fc* f) (hcomplex_of_complex x + xa)";
--- a/src/HOL/Complex/ComplexBin.ML Thu Feb 05 10:45:28 2004 +0100
+++ b/src/HOL/Complex/ComplexBin.ML Tue Feb 10 12:02:11 2004 +0100
@@ -70,7 +70,7 @@
(** Equals (=) **)
Goal "((number_of v :: complex) = number_of v') = \
-\ iszero (number_of (bin_add v (bin_minus v')))";
+\ iszero (number_of (bin_add v (bin_minus v')) :: int)";
by (simp_tac
(HOL_ss addsimps [complex_number_of_def,
complex_of_real_eq_iff, eq_real_number_of]) 1);
--- a/src/HOL/Complex/NSComplexBin.ML Thu Feb 05 10:45:28 2004 +0100
+++ b/src/HOL/Complex/NSComplexBin.ML Tue Feb 10 12:02:11 2004 +0100
@@ -100,7 +100,7 @@
(** Equals (=) **)
Goal "((number_of v :: hcomplex) = number_of v') = \
-\ iszero (number_of (bin_add v (bin_minus v')))";
+\ iszero (number_of (bin_add v (bin_minus v')) :: int)";
by (simp_tac
(HOL_ss addsimps [hcomplex_number_of_def,
hcomplex_of_complex_eq_iff, eq_complex_number_of]) 1);
--- a/src/HOL/Complex/NSInduct.ML Thu Feb 05 10:45:28 2004 +0100
+++ b/src/HOL/Complex/NSInduct.ML Tue Feb 10 12:02:11 2004 +0100
@@ -11,8 +11,8 @@
by (Ultra_tac 1);
qed "starPNat";
-Goalw [hypnat_of_nat_def] "( *pNat* P) (hypnat_of_nat n) = P n";
-by (auto_tac (claset(),simpset() addsimps [starPNat]));
+Goal "( *pNat* P) (hypnat_of_nat n) = P n";
+by (auto_tac (claset(),simpset() addsimps [starPNat, hypnat_of_nat_eq]));
qed "starPNat_hypnat_of_nat";
Addsimps [starPNat_hypnat_of_nat];
@@ -27,7 +27,7 @@
by (dres_inst_tac [("x","hypnat_of_nat n")] spec 1);
by (rtac ccontr 1);
by (auto_tac (claset(),simpset() addsimps [starPNat,
- hypnat_of_nat_def,hypnat_add]));
+ hypnat_of_nat_eq,hypnat_add]));
qed "hypnat_induct_obj";
Goal
--- a/src/HOL/Complex/ex/NSPrimes.ML Thu Feb 05 10:45:28 2004 +0100
+++ b/src/HOL/Complex/ex/NSPrimes.ML Tue Feb 10 12:02:11 2004 +0100
@@ -175,7 +175,7 @@
(* behaves as expected! *)
Goal "( *sNat* insert x A) = insert (hypnat_of_nat x) ( *sNat* A)";
by (auto_tac (claset(),simpset() addsimps [starsetNat_def,
- hypnat_of_nat_def]));
+ hypnat_of_nat_eq]));
by (ALLGOALS(res_inst_tac [("z","xa")] eq_Abs_hypnat));
by Auto_tac;
by (TRYALL(dtac bspec));
@@ -251,9 +251,8 @@
by Auto_tac;
qed "lemma_infinite_set_singleton";
-Goalw [SHNat_def,hypnat_of_nat_def]
- "inj f ==> Abs_hypnat(hypnatrel `` {f}) ~: Nats";
-by Auto_tac;
+Goal "inj f ==> Abs_hypnat(hypnatrel `` {f}) ~: Nats";
+by (auto_tac (claset(), simpset() addsimps [SHNat_eq,hypnat_of_nat_eq]));
by (subgoal_tac "ALL m n. m ~= n --> f n ~= f m" 1);
by Auto_tac;
by (dtac injD 2);
@@ -357,7 +356,7 @@
by Auto_tac;
by (dtac inj_fun_not_hypnat_in_SHNat 1);
by (dtac range_subset_mem_starsetNat 1);
-by (auto_tac (claset(),simpset() addsimps [SHNat_def]));
+by (auto_tac (claset(),simpset() addsimps [SHNat_eq]));
qed "hypnat_infinite_has_nonstandard";
Goal "*sNat* A = hypnat_of_nat ` A ==> finite A";
@@ -385,7 +384,7 @@
Goal "~ (ALL n:- {0}. hypnat_of_nat n hdvd 1)";
by Auto_tac;
by (res_inst_tac [("x","2")] bexI 1);
-by (auto_tac (claset(),simpset() addsimps [hypnat_of_nat_def,
+by (auto_tac (claset(),simpset() addsimps [hypnat_of_nat_eq,
hypnat_one_def,hdvd,dvd_def]));
val lemma_not_dvd_hypnat_one = result();
Addsimps [lemma_not_dvd_hypnat_one];
@@ -417,9 +416,9 @@
qed "zero_not_prime";
Addsimps [zero_not_prime];
-Goalw [starprime_def,starsetNat_def,hypnat_of_nat_def]
- "hypnat_of_nat 0 ~: starprime";
-by (auto_tac (claset() addSIs [bexI],simpset()));
+Goal "hypnat_of_nat 0 ~: starprime";
+by (auto_tac (claset() addSIs [bexI],
+ simpset() addsimps [starprime_def,starsetNat_def,hypnat_of_nat_eq]));
qed "hypnat_of_nat_zero_not_prime";
Addsimps [hypnat_of_nat_zero_not_prime];
@@ -443,9 +442,9 @@
qed "one_not_prime2";
Addsimps [one_not_prime2];
-Goalw [starprime_def,starsetNat_def,hypnat_of_nat_def]
- "hypnat_of_nat 1 ~: starprime";
-by (auto_tac (claset() addSIs [bexI],simpset()));
+Goal "hypnat_of_nat 1 ~: starprime";
+by (auto_tac (claset() addSIs [bexI],
+ simpset() addsimps [starprime_def,starsetNat_def,hypnat_of_nat_eq]));
qed "hypnat_of_nat_one_not_prime";
Addsimps [hypnat_of_nat_one_not_prime];
--- a/src/HOL/Hyperreal/HSeries.ML Thu Feb 05 10:45:28 2004 +0100
+++ b/src/HOL/Hyperreal/HSeries.ML Tue Feb 10 12:02:11 2004 +0100
@@ -5,6 +5,8 @@
for hyperreals
*)
+val hypreal_of_nat_eq = thm"hypreal_of_nat_eq";
+
Goalw [sumhr_def]
"sumhr(M,N,f) = \
\ Abs_hypreal(UN X:Rep_hypnat(M). UN Y: Rep_hypnat(N). \
@@ -125,12 +127,11 @@
qed "sumhr_hrabs";
(* other general version also needed *)
-Goalw [hypnat_of_nat_def]
- "(ALL r. m <= r & r < n --> f r = g r) --> \
+Goal "(ALL r. m <= r & r < n --> f r = g r) --> \
\ sumhr(hypnat_of_nat m, hypnat_of_nat n, f) = \
\ sumhr(hypnat_of_nat m, hypnat_of_nat n, g)";
by (Step_tac 1 THEN dtac sumr_fun_eq 1);
-by (auto_tac (claset(), simpset() addsimps [sumhr]));
+by (auto_tac (claset(), simpset() addsimps [sumhr, hypnat_of_nat_eq]));
qed "sumhr_fun_hypnat_eq";
Goalw [hypnat_zero_def,hypreal_of_real_def]
@@ -163,12 +164,11 @@
by (auto_tac (claset(), simpset() addsimps [sumhr, hypreal_minus,sumr_minus]));
qed "sumhr_minus";
-Goalw [hypnat_of_nat_def]
- "sumhr(m+hypnat_of_nat k,n+hypnat_of_nat k,f) = sumhr(m,n,%i. f(i + k))";
+Goal "sumhr(m+hypnat_of_nat k,n+hypnat_of_nat k,f) = sumhr(m,n,%i. f(i + k))";
by (res_inst_tac [("z","m")] eq_Abs_hypnat 1);
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
by (auto_tac (claset(),
- simpset() addsimps [sumhr, hypnat_add,sumr_shift_bounds]));
+ simpset() addsimps [sumhr, hypnat_add,sumr_shift_bounds, hypnat_of_nat_eq]));
qed "sumhr_shift_bounds";
(*------------------------------------------------------------------
@@ -196,12 +196,11 @@
qed "sumhr_minus_one_realpow_zero";
Addsimps [sumhr_minus_one_realpow_zero];
-Goalw [hypnat_of_nat_def,hypreal_of_real_def]
- "(ALL n. m <= Suc n --> f n = r) & m <= na \
+Goal "(ALL n. m <= Suc n --> f n = r) & m <= na \
\ ==> sumhr(hypnat_of_nat m,hypnat_of_nat na,f) = \
\ (hypreal_of_nat (na - m) * hypreal_of_real r)";
by (auto_tac (claset() addSDs [sumr_interval_const],
- simpset() addsimps [sumhr,hypreal_of_nat_def,
+ simpset() addsimps [hypreal_of_real_def, sumhr,hypreal_of_nat_eq, hypnat_of_nat_eq,
hypreal_of_real_def, hypreal_mult]));
qed "sumhr_interval_const";
--- a/src/HOL/Hyperreal/HTranscendental.ML Thu Feb 05 10:45:28 2004 +0100
+++ b/src/HOL/Hyperreal/HTranscendental.ML Tue Feb 10 12:02:11 2004 +0100
@@ -122,7 +122,7 @@
Goal "( *f* sqrt)(x pow (hypnat_of_nat 2)) = abs(x)";
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
by (auto_tac (claset(),simpset() addsimps [starfun,
- hypreal_hrabs,hypnat_of_nat_def,hyperpow]));
+ hypreal_hrabs,hypnat_of_nat_eq,hyperpow]));
qed "hypreal_sqrt_hyperpow_hrabs";
Addsimps [hypreal_sqrt_hyperpow_hrabs];
--- a/src/HOL/Hyperreal/HyperArith.thy Thu Feb 05 10:45:28 2004 +0100
+++ b/src/HOL/Hyperreal/HyperArith.thy Tue Feb 10 12:02:11 2004 +0100
@@ -77,7 +77,7 @@
lemma eq_hypreal_number_of [simp]:
"((number_of v :: hypreal) = number_of v') =
- iszero (number_of (bin_add v (bin_minus v')))"
+ iszero (number_of (bin_add v (bin_minus v')) :: int)"
apply (simp only: hypreal_number_of_def hypreal_of_real_eq_iff eq_real_number_of)
done
@@ -87,7 +87,7 @@
(*"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')))"
+ neg (number_of (bin_add v (bin_minus v')) :: int)"
by (simp only: hypreal_number_of_def hypreal_of_real_less_iff less_real_number_of)
@@ -139,10 +139,6 @@
setup hypreal_arith_setup
-text{*Used once in NSA*}
-lemma hypreal_add_minus_eq_minus: "x + y = (0::hypreal) ==> x = -y"
-by arith
-
lemma hypreal_le_add_order: "[| 0 \<le> x; 0 \<le> y |] ==> (0::hypreal) \<le> x + y"
by arith
@@ -192,7 +188,7 @@
lemma hrabs_number_of [simp]:
"abs (number_of v :: hypreal) =
- (if neg (number_of v) then number_of (bin_minus v)
+ (if neg (number_of v :: int) then number_of (bin_minus v)
else number_of v)"
by (simp add: hrabs_def)
@@ -229,8 +225,11 @@
constdefs
- hypreal_of_nat :: "nat => hypreal"
- "hypreal_of_nat (n::nat) == hypreal_of_real (real n)"
+ hypreal_of_nat :: "nat => hypreal"
+ "hypreal_of_nat m == of_nat m"
+
+lemma SNat_eq: "Nats = {n. \<exists>N. n = hypreal_of_nat N}"
+by (force simp add: hypreal_of_nat_def Nats_def)
lemma hypreal_of_nat_add [simp]:
@@ -252,46 +251,42 @@
(* is a hyperreal c.f. NS extension *)
(*------------------------------------------------------------*)
-lemma hypreal_of_nat_iff:
- "hypreal_of_nat m = Abs_hypreal(hyprel``{%n. real m})"
-by (simp add: hypreal_of_nat_def hypreal_of_real_def real_of_nat_def)
+lemma hypreal_of_nat_eq:
+ "hypreal_of_nat (n::nat) = hypreal_of_real (real n)"
+apply (induct n)
+apply (simp_all add: hypreal_of_nat_def real_of_nat_def)
+done
-lemma inj_hypreal_of_nat: "inj hypreal_of_nat"
-by (simp add: inj_on_def hypreal_of_nat_def)
+lemma hypreal_of_nat:
+ "hypreal_of_nat m = Abs_hypreal(hyprel``{%n. real m})"
+apply (induct m)
+apply (simp_all add: hypreal_of_nat_def real_of_nat_def hypreal_zero_def
+ hypreal_one_def hypreal_add)
+done
lemma hypreal_of_nat_Suc:
"hypreal_of_nat (Suc n) = hypreal_of_nat n + (1::hypreal)"
-by (simp add: hypreal_of_nat_def real_of_nat_Suc)
+by (simp add: hypreal_of_nat_def)
(*"neg" is used in rewrite rules for binary comparisons*)
lemma hypreal_of_nat_number_of [simp]:
"hypreal_of_nat (number_of v :: nat) =
- (if neg (number_of v) then 0
+ (if neg (number_of v :: int) then 0
else (number_of v :: hypreal))"
-by (simp add: hypreal_of_nat_def)
+by (simp add: hypreal_of_nat_eq)
lemma hypreal_of_nat_zero [simp]: "hypreal_of_nat 0 = 0"
-by (simp del: numeral_0_eq_0 add: numeral_0_eq_0 [symmetric])
+by (simp add: hypreal_of_nat_def)
lemma hypreal_of_nat_one [simp]: "hypreal_of_nat 1 = 1"
-by (simp add: hypreal_of_nat_Suc)
-
-lemma hypreal_of_nat: "hypreal_of_nat m = Abs_hypreal(hyprel `` {%n. real m})"
-apply (induct_tac "m")
-apply (auto simp add: hypreal_zero_def hypreal_of_nat_Suc hypreal_zero_num hypreal_one_num hypreal_add real_of_nat_Suc)
-done
+by (simp add: hypreal_of_nat_def)
-lemma hypreal_of_nat_le_iff:
- "(hypreal_of_nat n \<le> hypreal_of_nat m) = (n \<le> m)"
-apply (auto simp add: linorder_not_less [symmetric])
-done
-declare hypreal_of_nat_le_iff [simp]
+lemma hypreal_of_nat_le_iff [simp]:
+ "(hypreal_of_nat n \<le> hypreal_of_nat m) = (n \<le> m)"
+by (simp add: hypreal_of_nat_def)
-lemma hypreal_of_nat_ge_zero: "0 \<le> hypreal_of_nat n"
-apply (simp (no_asm) add: hypreal_of_nat_zero [symmetric]
- del: hypreal_of_nat_zero)
-done
-declare hypreal_of_nat_ge_zero [simp]
+lemma hypreal_of_nat_ge_zero [simp]: "0 \<le> hypreal_of_nat n"
+by (simp add: hypreal_of_nat_def)
(*
@@ -302,7 +297,6 @@
ML
{*
-val hypreal_add_minus_eq_minus = thm "hypreal_add_minus_eq_minus";
val hypreal_le_add_order = thm"hypreal_le_add_order";
val hypreal_of_nat_def = thm"hypreal_of_nat_def";
@@ -316,8 +310,6 @@
val hypreal_of_nat_add = thm "hypreal_of_nat_add";
val hypreal_of_nat_mult = thm "hypreal_of_nat_mult";
val hypreal_of_nat_less_iff = thm "hypreal_of_nat_less_iff";
-val hypreal_of_nat_iff = thm "hypreal_of_nat_iff";
-val inj_hypreal_of_nat = thm "inj_hypreal_of_nat";
val hypreal_of_nat_Suc = thm "hypreal_of_nat_Suc";
val hypreal_of_nat_number_of = thm "hypreal_of_nat_number_of";
val hypreal_of_nat_zero = thm "hypreal_of_nat_zero";
--- a/src/HOL/Hyperreal/HyperDef.thy Thu Feb 05 10:45:28 2004 +0100
+++ b/src/HOL/Hyperreal/HyperDef.thy Tue Feb 10 12:02:11 2004 +0100
@@ -176,6 +176,11 @@
"(X: FreeUltrafilterNat) = (-X \<notin> FreeUltrafilterNat)"
by (auto simp add: FreeUltrafilterNat_Compl_iff1 [symmetric])
+lemma cofinite_mem_FreeUltrafilterNat: "finite (-X) ==> X \<in> FreeUltrafilterNat"
+apply (drule FreeUltrafilterNat_finite)
+apply (simp add: FreeUltrafilterNat_Compl_iff2 [symmetric])
+done
+
lemma FreeUltrafilterNat_UNIV [simp]: "(UNIV::nat set) \<in> FreeUltrafilterNat"
by (rule FreeUltrafilterNat_mem [THEN FreeUltrafilter_Ultrafilter, THEN Ultrafilter_Filter, THEN mem_FiltersetD4])
@@ -768,7 +773,7 @@
lemma lemma_omega_empty_singleton_disj: "{n::nat. x = real n} = {} |
(\<exists>y. {n::nat. x = real n} = {y})"
-by (force dest: inj_real_of_nat [THEN injD])
+by (force)
lemma lemma_finite_omega_set: "finite {n::nat. x = real n}"
by (cut_tac x = x in lemma_omega_empty_singleton_disj, auto)
@@ -789,7 +794,7 @@
lemma lemma_epsilon_empty_singleton_disj:
"{n::nat. x = inverse(real(Suc n))} = {} |
(\<exists>y. {n::nat. x = inverse(real(Suc n))} = {y})"
-by (auto simp add: inj_real_of_nat [THEN inj_eq])
+by (auto)
lemma lemma_finite_epsilon_set: "finite {n. x = inverse(real(Suc n))}"
by (cut_tac x = x in lemma_epsilon_empty_singleton_disj, auto)
--- a/src/HOL/Hyperreal/HyperNat.thy Thu Feb 05 10:45:28 2004 +0100
+++ b/src/HOL/Hyperreal/HyperNat.thy Tue Feb 10 12:02:11 2004 +0100
@@ -24,36 +24,9 @@
consts whn :: hypnat
-constdefs
-
- (* embedding the naturals in the hypernaturals *)
- hypnat_of_nat :: "nat => hypnat"
- "hypnat_of_nat m == Abs_hypnat(hypnatrel``{%n::nat. m})"
-
- (* hypernaturals as members of the hyperreals; the set is defined as *)
- (* the nonstandard extension of set of naturals embedded in the reals *)
- HNat :: "hypreal set"
- "HNat == *s* {n. \<exists>no::nat. n = real no}"
-
- (* the set of infinite hypernatural numbers *)
- HNatInfinite :: "hypnat set"
- "HNatInfinite == {n. n \<notin> Nats}"
-
- (* explicit embedding of the hypernaturals in the hyperreals *)
- hypreal_of_hypnat :: "hypnat => hypreal"
- "hypreal_of_hypnat N == Abs_hypreal(\<Union>X \<in> Rep_hypnat(N).
- hyprel``{%n::nat. real (X n)})"
defs (overloaded)
- (** the overloaded constant "Nats" **)
-
- (* set of naturals embedded in the hyperreals*)
- SNat_def: "Nats == {n. \<exists>N. n = hypreal_of_nat N}"
-
- (* set of naturals embedded in the hypernaturals*)
- SHNat_def: "Nats == {n. \<exists>N. n = hypnat_of_nat N}"
-
(** hypernatural arithmetic **)
hypnat_zero_def: "0 == Abs_hypnat(hypnatrel``{%n::nat. 0})"
@@ -151,18 +124,6 @@
declare Rep_hypnat_nonempty [simp]
-subsection{*@{term hypnat_of_nat}:
- the Injection from @{typ nat} to @{typ hypnat}*}
-
-lemma inj_hypnat_of_nat: "inj(hypnat_of_nat)"
-apply (rule inj_onI)
-apply (unfold hypnat_of_nat_def)
-apply (drule inj_on_Abs_hypnat [THEN inj_onD])
-apply (rule hypnatrel_in_hypnat)+
-apply (drule eq_equiv_class)
-apply (rule equiv_hypnatrel)
-apply (simp_all split: split_if_asm)
-done
lemma eq_Abs_hypnat:
"(!!x. z = Abs_hypnat(hypnatrel``{x}) ==> P) ==> P"
@@ -439,6 +400,13 @@
apply (auto simp add: hypnat_zero_def hypnat_mult, ultra+)
done
+lemma hypnat_diff_is_0_eq [simp]: "((m::hypnat) - n = 0) = (m \<le> n)"
+apply (rule eq_Abs_hypnat [of m])
+apply (rule eq_Abs_hypnat [of n])
+apply (simp add: hypnat_le hypnat_minus hypnat_zero_def)
+done
+
+
subsection{*Theorems for Ordering*}
@@ -496,42 +464,73 @@
apply (insert add_le_less_mono [OF _ zero_less_one, of 0], auto)
done
+lemma hypnat_add_self_not_less: "~ (x + y < (x::hypnat))"
+by (simp add: linorder_not_le [symmetric] add_commute [of x])
+
+lemma hypnat_diff_split:
+ "P(a - b::hypnat) = ((a<b --> P 0) & (ALL d. a = b + d --> P d))"
+ -- {* elimination of @{text -} on @{text hypnat} *}
+proof (cases "a<b" rule: case_split)
+ case True
+ thus ?thesis
+ by (auto simp add: hypnat_add_self_not_less order_less_imp_le
+ hypnat_diff_is_0_eq [THEN iffD2])
+next
+ case False
+ thus ?thesis
+ by (auto simp add: linorder_not_less dest: order_le_less_trans);
+qed
+
+
subsection{*The Embedding @{term hypnat_of_nat} Preserves Ring and
Order Properties*}
+constdefs
+
+ hypnat_of_nat :: "nat => hypnat"
+ "hypnat_of_nat m == of_nat m"
+
+ (* the set of infinite hypernatural numbers *)
+ HNatInfinite :: "hypnat set"
+ "HNatInfinite == {n. n \<notin> Nats}"
+
+
lemma hypnat_of_nat_add:
"hypnat_of_nat ((z::nat) + w) = hypnat_of_nat z + hypnat_of_nat w"
-by (simp add: hypnat_of_nat_def hypnat_add)
-
-lemma hypnat_of_nat_minus:
- "hypnat_of_nat ((z::nat) - w) = hypnat_of_nat z - hypnat_of_nat w"
-by (simp add: hypnat_of_nat_def hypnat_minus)
+by (simp add: hypnat_of_nat_def)
lemma hypnat_of_nat_mult:
"hypnat_of_nat (z * w) = hypnat_of_nat z * hypnat_of_nat w"
-by (simp add: hypnat_of_nat_def hypnat_mult)
+by (simp add: hypnat_of_nat_def)
lemma hypnat_of_nat_less_iff [simp]:
"(hypnat_of_nat z < hypnat_of_nat w) = (z < w)"
-by (simp add: hypnat_less hypnat_of_nat_def)
+by (simp add: hypnat_of_nat_def)
lemma hypnat_of_nat_le_iff [simp]:
"(hypnat_of_nat z \<le> hypnat_of_nat w) = (z \<le> w)"
-by (simp add: linorder_not_less [symmetric])
+by (simp add: hypnat_of_nat_def)
-lemma hypnat_of_nat_one: "hypnat_of_nat (Suc 0) = (1::hypnat)"
-by (simp add: hypnat_of_nat_def hypnat_one_def)
+lemma hypnat_of_nat_eq_iff [simp]:
+ "(hypnat_of_nat z = hypnat_of_nat w) = (z = w)"
+by (simp add: hypnat_of_nat_def)
-lemma hypnat_of_nat_zero: "hypnat_of_nat 0 = 0"
-by (simp add: hypnat_of_nat_def hypnat_zero_def)
+lemma hypnat_of_nat_one [simp]: "hypnat_of_nat (Suc 0) = (1::hypnat)"
+by (simp add: hypnat_of_nat_def)
-lemma hypnat_of_nat_zero_iff: "(hypnat_of_nat n = 0) = (n = 0)"
-by (auto intro: FreeUltrafilterNat_P
- simp add: hypnat_of_nat_def hypnat_zero_def)
+lemma hypnat_of_nat_zero [simp]: "hypnat_of_nat 0 = 0"
+by (simp add: hypnat_of_nat_def)
+
+lemma hypnat_of_nat_zero_iff [simp]: "(hypnat_of_nat n = 0) = (n = 0)"
+by (simp add: hypnat_of_nat_def)
-lemma hypnat_of_nat_Suc:
+lemma hypnat_of_nat_Suc [simp]:
"hypnat_of_nat (Suc n) = hypnat_of_nat n + (1::hypnat)"
-by (auto simp add: hypnat_add hypnat_of_nat_def hypnat_one_def)
+by (simp add: hypnat_of_nat_def)
+
+lemma hypnat_of_nat_minus:
+ "hypnat_of_nat ((j::nat) - k) = hypnat_of_nat j - hypnat_of_nat k"
+by (simp add: hypnat_of_nat_def split: nat_diff_split hypnat_diff_split)
subsection{*Existence of an Infinite Hypernatural Number*}
@@ -546,111 +545,64 @@
follows because member @{term FreeUltrafilterNat} is not finite.
See @{text HyperDef.thy} for similar argument.*}
-lemma not_ex_hypnat_of_nat_eq_omega:
- "~ (\<exists>x. hypnat_of_nat x = whn)"
-apply (simp add: hypnat_omega_def hypnat_of_nat_def)
-apply (auto dest: FreeUltrafilterNat_not_finite)
-done
-
-lemma hypnat_of_nat_not_eq_omega: "hypnat_of_nat x \<noteq> whn"
-by (cut_tac not_ex_hypnat_of_nat_eq_omega, auto)
-declare hypnat_of_nat_not_eq_omega [THEN not_sym, simp]
-
subsection{*Properties of the set @{term Nats} of Embedded Natural Numbers*}
-(* Infinite hypernatural not in embedded Nats *)
-lemma SHNAT_omega_not_mem [simp]: "whn \<notin> Nats"
-by (simp add: SHNat_def)
-
-(*-----------------------------------------------------------------------
- Closure laws for members of (embedded) set standard naturals Nats
- -----------------------------------------------------------------------*)
-lemma SHNat_add:
- "!!x::hypnat. [| x \<in> Nats; y \<in> Nats |] ==> x + y \<in> Nats"
-apply (simp add: SHNat_def, safe)
-apply (rule_tac x = "N + Na" in exI)
-apply (simp add: hypnat_of_nat_add)
-done
-
-lemma SHNat_minus:
- "!!x::hypnat. [| x \<in> Nats; y \<in> Nats |] ==> x - y \<in> Nats"
-apply (simp add: SHNat_def, safe)
-apply (rule_tac x = "N - Na" in exI)
-apply (simp add: hypnat_of_nat_minus)
-done
-
-lemma SHNat_mult:
- "!!x::hypnat. [| x \<in> Nats; y \<in> Nats |] ==> x * y \<in> Nats"
-apply (simp add: SHNat_def, safe)
-apply (rule_tac x = "N * Na" in exI)
-apply (simp (no_asm) add: hypnat_of_nat_mult)
+lemma of_nat_eq_add [rule_format]:
+ "\<forall>d::hypnat. of_nat m = of_nat n + d --> d \<in> range of_nat"
+apply (induct n)
+apply (auto simp add: add_assoc)
+apply (case_tac x)
+apply (auto simp add: add_commute [of 1])
done
-lemma SHNat_add_cancel: "!!x::hypnat. [| x + y \<in> Nats; y \<in> Nats |] ==> x \<in> Nats"
-by (drule_tac x = "x+y" in SHNat_minus, auto)
-
-lemma SHNat_hypnat_of_nat [simp]: "hypnat_of_nat x \<in> Nats"
-by (simp add: SHNat_def, blast)
-
-lemma SHNat_hypnat_of_nat_one [simp]: "hypnat_of_nat (Suc 0) \<in> Nats"
-by simp
-
-lemma SHNat_hypnat_of_nat_zero [simp]: "hypnat_of_nat 0 \<in> Nats"
-by simp
-
-lemma SHNat_one [simp]: "(1::hypnat) \<in> Nats"
-by (simp add: hypnat_of_nat_one [symmetric])
-
-lemma SHNat_zero [simp]: "(0::hypnat) \<in> Nats"
-by (simp add: hypnat_of_nat_zero [symmetric])
-
-lemma SHNat_iff: "(x \<in> Nats) = (\<exists>y. x = hypnat_of_nat y)"
-by (simp add: SHNat_def)
-
-lemma SHNat_hypnat_of_nat_iff:
- "Nats = hypnat_of_nat ` (UNIV::nat set)"
-by (auto simp add: SHNat_def)
-
-lemma leSuc_Un_eq: "{n. n \<le> Suc m} = {n. n \<le> m} Un {n. n = Suc m}"
-by (auto simp add: le_Suc_eq)
-
-lemma finite_nat_le_segment: "finite {n::nat. n \<le> m}"
-apply (induct_tac "m")
-apply (auto simp add: leSuc_Un_eq)
+lemma Nats_diff [simp]: "[|a \<in> Nats; b \<in> Nats|] ==> (a-b :: hypnat) \<in> Nats"
+apply (auto simp add: of_nat_eq_add Nats_def split: hypnat_diff_split)
done
lemma lemma_unbounded_set [simp]: "{n::nat. m < n} \<in> FreeUltrafilterNat"
-by (insert finite_nat_le_segment
- [THEN FreeUltrafilterNat_finite,
- THEN FreeUltrafilterNat_Compl_mem, of m], ultra)
-
-(*????hyperdef*)
-lemma cofinite_mem_FreeUltrafilterNat: "finite (-X) ==> X \<in> FreeUltrafilterNat"
-apply (drule FreeUltrafilterNat_finite)
-apply (simp add: FreeUltrafilterNat_Compl_iff2 [symmetric])
+apply (insert finite_atMost [of m])
+apply (simp add: atMost_def)
+apply (drule FreeUltrafilterNat_finite)
+apply (drule FreeUltrafilterNat_Compl_mem)
+apply ultra
done
lemma Compl_Collect_le: "- {n::nat. N \<le> n} = {n. n < N}"
by (simp add: Collect_neg_eq [symmetric] linorder_not_le)
+
+lemma hypnat_of_nat_eq:
+ "hypnat_of_nat m = Abs_hypnat(hypnatrel``{%n::nat. m})"
+apply (induct m)
+apply (simp_all add: hypnat_zero_def hypnat_one_def hypnat_add);
+done
+
+lemma SHNat_eq: "Nats = {n. \<exists>N. n = hypnat_of_nat N}"
+by (force simp add: hypnat_of_nat_def Nats_def)
+
lemma hypnat_omega_gt_SHNat:
"n \<in> Nats ==> n < whn"
-apply (auto simp add: SHNat_def hypnat_of_nat_def hypnat_less_def
- hypnat_le_def hypnat_omega_def)
+apply (auto simp add: hypnat_of_nat_eq hypnat_less_def hypnat_le_def
+ hypnat_omega_def SHNat_eq)
prefer 2 apply (force dest: FreeUltrafilterNat_not_finite)
apply (auto intro!: exI)
apply (rule cofinite_mem_FreeUltrafilterNat)
apply (simp add: Compl_Collect_le finite_nat_segment)
done
-lemma hypnat_of_nat_less_whn: "hypnat_of_nat n < whn"
-by (insert hypnat_omega_gt_SHNat [of "hypnat_of_nat n"], auto)
-declare hypnat_of_nat_less_whn [simp]
+(* Infinite hypernatural not in embedded Nats *)
+lemma SHNAT_omega_not_mem [simp]: "whn \<notin> Nats"
+apply (blast dest: hypnat_omega_gt_SHNat)
+done
-lemma hypnat_of_nat_le_whn: "hypnat_of_nat n \<le> whn"
+lemma hypnat_of_nat_less_whn [simp]: "hypnat_of_nat n < whn"
+apply (insert hypnat_omega_gt_SHNat [of "hypnat_of_nat n"])
+apply (simp add: hypnat_of_nat_def)
+done
+
+lemma hypnat_of_nat_le_whn [simp]: "hypnat_of_nat n \<le> whn"
by (rule hypnat_of_nat_less_whn [THEN order_less_imp_le])
-declare hypnat_of_nat_le_whn [simp]
lemma hypnat_zero_less_hypnat_omega [simp]: "0 < whn"
by (simp add: hypnat_omega_gt_SHNat)
@@ -661,37 +613,22 @@
subsection{*Infinite Hypernatural Numbers -- @{term HNatInfinite}*}
-lemma HNatInfinite_whn: "whn \<in> HNatInfinite"
-by (simp add: HNatInfinite_def SHNat_def)
-declare HNatInfinite_whn [simp]
-
-lemma SHNat_not_HNatInfinite: "x \<in> Nats ==> x \<notin> HNatInfinite"
-by (simp add: HNatInfinite_def)
-
-lemma not_HNatInfinite_SHNat: "x \<notin> HNatInfinite ==> x \<in> Nats"
+lemma HNatInfinite_whn [simp]: "whn \<in> HNatInfinite"
by (simp add: HNatInfinite_def)
-lemma not_SHNat_HNatInfinite: "x \<notin> Nats ==> x \<in> HNatInfinite"
-by (simp add: HNatInfinite_def)
-
-lemma HNatInfinite_not_SHNat: "x \<in> HNatInfinite ==> x \<notin> Nats"
+lemma Nats_not_HNatInfinite_iff: "(x \<in> Nats) = (x \<notin> HNatInfinite)"
by (simp add: HNatInfinite_def)
-lemma SHNat_not_HNatInfinite_iff: "(x \<in> Nats) = (x \<notin> HNatInfinite)"
-by (blast intro!: SHNat_not_HNatInfinite not_HNatInfinite_SHNat)
-
-lemma not_SHNat_HNatInfinite_iff: "(x \<notin> Nats) = (x \<in> HNatInfinite)"
-by (blast intro!: not_SHNat_HNatInfinite HNatInfinite_not_SHNat)
-
-lemma SHNat_HNatInfinite_disj: "x \<in> Nats | x \<in> HNatInfinite"
-by (simp add: SHNat_not_HNatInfinite_iff)
+lemma HNatInfinite_not_Nats_iff: "(x \<in> HNatInfinite) = (x \<notin> Nats)"
+by (simp add: HNatInfinite_def)
subsection{*Alternative Characterization of the Set of Infinite Hypernaturals:
@{term "HNatInfinite = {N. \<forall>n \<in> Nats. n < N}"}*}
(*??delete? similar reasoning in hypnat_omega_gt_SHNat above*)
-lemma HNatInfinite_FreeUltrafilterNat_lemma: "\<forall>N::nat. {n. f n \<noteq> N} \<in> FreeUltrafilterNat
+lemma HNatInfinite_FreeUltrafilterNat_lemma:
+ "\<forall>N::nat. {n. f n \<noteq> N} \<in> FreeUltrafilterNat
==> {n. N < f n} \<in> FreeUltrafilterNat"
apply (induct_tac "N")
apply (drule_tac x = 0 in spec)
@@ -700,15 +637,14 @@
done
lemma HNatInfinite_iff: "HNatInfinite = {N. \<forall>n \<in> Nats. n < N}"
-apply (unfold HNatInfinite_def SHNat_def hypnat_of_nat_def, safe)
-apply (drule_tac [2] x = "Abs_hypnat (hypnatrel `` {%n. N}) " in bspec)
+apply (auto simp add: HNatInfinite_def SHNat_eq hypnat_of_nat_eq)
apply (rule_tac z = x in eq_Abs_hypnat)
-apply (rule_tac z = n in eq_Abs_hypnat)
-apply (auto simp add: hypnat_less)
-apply (auto elim: HNatInfinite_FreeUltrafilterNat_lemma
- simp add: FreeUltrafilterNat_Compl_iff1 Collect_neg_eq [symmetric])
+apply (auto elim: HNatInfinite_FreeUltrafilterNat_lemma
+ simp add: hypnat_less FreeUltrafilterNat_Compl_iff1
+ Collect_neg_eq [symmetric])
done
+
subsection{*Alternative Characterization of @{term HNatInfinite} using
Free Ultrafilter*}
@@ -716,9 +652,8 @@
"x \<in> HNatInfinite
==> \<exists>X \<in> Rep_hypnat x. \<forall>u. {n. u < X n}: FreeUltrafilterNat"
apply (rule eq_Abs_hypnat [of x])
-apply (auto simp add: HNatInfinite_iff SHNat_iff hypnat_of_nat_def)
+apply (auto simp add: HNatInfinite_iff SHNat_eq hypnat_of_nat_eq)
apply (rule bexI [OF _ lemma_hypnatrel_refl], clarify)
-apply (drule_tac x = "hypnat_of_nat u" in bspec, simp)
apply (auto simp add: hypnat_of_nat_def hypnat_less)
done
@@ -726,26 +661,24 @@
"\<exists>X \<in> Rep_hypnat x. \<forall>u. {n. u < X n}: FreeUltrafilterNat
==> x \<in> HNatInfinite"
apply (rule eq_Abs_hypnat [of x])
-apply (auto simp add: hypnat_less HNatInfinite_iff SHNat_iff hypnat_of_nat_def)
+apply (auto simp add: hypnat_less HNatInfinite_iff SHNat_eq hypnat_of_nat_eq)
apply (drule spec, ultra, auto)
done
lemma HNatInfinite_FreeUltrafilterNat_iff:
"(x \<in> HNatInfinite) =
(\<exists>X \<in> Rep_hypnat x. \<forall>u. {n. u < X n}: FreeUltrafilterNat)"
-apply (blast intro: HNatInfinite_FreeUltrafilterNat FreeUltrafilterNat_HNatInfinite)
-done
+by (blast intro: HNatInfinite_FreeUltrafilterNat
+ FreeUltrafilterNat_HNatInfinite)
-lemma HNatInfinite_gt_one: "x \<in> HNatInfinite ==> (1::hypnat) < x"
+lemma HNatInfinite_gt_one [simp]: "x \<in> HNatInfinite ==> (1::hypnat) < x"
by (auto simp add: HNatInfinite_iff)
-declare HNatInfinite_gt_one [simp]
-lemma zero_not_mem_HNatInfinite: "0 \<notin> HNatInfinite"
+lemma zero_not_mem_HNatInfinite [simp]: "0 \<notin> HNatInfinite"
apply (auto simp add: HNatInfinite_iff)
apply (drule_tac a = " (1::hypnat) " in equals0D)
apply simp
done
-declare zero_not_mem_HNatInfinite [simp]
lemma HNatInfinite_not_eq_zero: "x \<in> HNatInfinite ==> 0 < x"
apply (drule HNatInfinite_gt_one)
@@ -758,78 +691,60 @@
subsection{*Closure Rules*}
-lemma HNatInfinite_add: "[| x \<in> HNatInfinite; y \<in> HNatInfinite |]
- ==> x + y \<in> HNatInfinite"
+lemma HNatInfinite_add:
+ "[| x \<in> HNatInfinite; y \<in> HNatInfinite |] ==> x + y \<in> HNatInfinite"
apply (auto simp add: HNatInfinite_iff)
apply (drule bspec, assumption)
-apply (drule bspec [OF _ SHNat_zero])
+apply (drule bspec [OF _ Nats_0])
apply (drule add_strict_mono, assumption, simp)
done
-lemma HNatInfinite_SHNat_add: "[| x \<in> HNatInfinite; y \<in> Nats |] ==> x + y \<in> HNatInfinite"
-apply (rule ccontr, drule not_HNatInfinite_SHNat)
-apply (drule_tac x = "x + y" in SHNat_minus)
-apply (auto simp add: SHNat_not_HNatInfinite_iff)
+lemma HNatInfinite_SHNat_add:
+ "[| x \<in> HNatInfinite; y \<in> Nats |] ==> x + y \<in> HNatInfinite"
+apply (auto simp add: HNatInfinite_not_Nats_iff)
+apply (drule_tac a = "x + y" in Nats_diff)
+apply (auto );
done
-lemma HNatInfinite_SHNat_diff: "[| x \<in> HNatInfinite; y \<in> Nats |] ==> x - y \<in> HNatInfinite"
-apply (rule ccontr, drule not_HNatInfinite_SHNat)
-apply (drule_tac x = "x - y" in SHNat_add)
-apply (subgoal_tac [2] "y \<le> x")
-apply (auto dest!: hypnat_le_add_diff_inverse2 simp add: not_SHNat_HNatInfinite_iff [symmetric])
-apply (auto intro!: order_less_imp_le simp add: not_SHNat_HNatInfinite_iff HNatInfinite_iff)
-done
+lemma HNatInfinite_Nats_imp_less: "[| x \<in> HNatInfinite; y \<in> Nats |] ==> y < x"
+by (simp add: HNatInfinite_iff)
+
+lemma HNatInfinite_SHNat_diff:
+ assumes x: "x \<in> HNatInfinite" and y: "y \<in> Nats"
+ shows "x - y \<in> HNatInfinite"
+proof -
+ have "y < x" by (simp add: HNatInfinite_Nats_imp_less prems)
+ hence "x - y + y = x" by (simp add: order_less_imp_le)
+ with x show ?thesis
+ by (force simp add: HNatInfinite_not_Nats_iff
+ dest: Nats_add [of "x-y", OF _ y])
+qed
lemma HNatInfinite_add_one: "x \<in> HNatInfinite ==> x + (1::hypnat) \<in> HNatInfinite"
by (auto intro: HNatInfinite_SHNat_add)
-lemma HNatInfinite_minus_one: "x \<in> HNatInfinite ==> x - (1::hypnat) \<in> HNatInfinite"
-apply (rule ccontr, drule not_HNatInfinite_SHNat)
-apply (drule_tac x = "x - (1::hypnat) " and y = " (1::hypnat) " in SHNat_add)
-apply (auto simp add: not_SHNat_HNatInfinite_iff [symmetric])
-done
-
lemma HNatInfinite_is_Suc: "x \<in> HNatInfinite ==> \<exists>y. x = y + (1::hypnat)"
apply (rule_tac x = "x - (1::hypnat) " in exI)
apply auto
done
-subsection{*@{term HNat}: the Hypernaturals Embedded in the Hyperreals*}
-
+subsection{*Embedding of the Hypernaturals into the Hyperreals*}
text{*Obtained using the nonstandard extension of the naturals*}
-lemma HNat_hypreal_of_nat: "hypreal_of_nat N \<in> HNat"
-apply (simp add: HNat_def starset_def hypreal_of_nat_def hypreal_of_real_def, auto, ultra)
-apply (rule_tac x = N in exI, auto)
-done
-declare HNat_hypreal_of_nat [simp]
-
-lemma HNat_add: "[| x \<in> HNat; y \<in> HNat |] ==> x + y \<in> HNat"
-apply (simp add: HNat_def starset_def)
-apply (rule_tac z = x in eq_Abs_hypreal)
-apply (rule_tac z = y in eq_Abs_hypreal)
-apply (auto dest!: bspec intro: lemma_hyprel_refl simp add: hypreal_add, ultra)
-apply (rule_tac x = "no+noa" in exI, auto)
-done
-
-lemma HNat_mult:
- "[| x \<in> HNat; y \<in> HNat |] ==> x * y \<in> HNat"
-apply (simp add: HNat_def starset_def)
-apply (rule_tac z = x in eq_Abs_hypreal)
-apply (rule_tac z = y in eq_Abs_hypreal)
-apply (auto dest!: bspec intro: lemma_hyprel_refl simp add: hypreal_mult, ultra)
-apply (rule_tac x = "no*noa" in exI, auto)
-done
+constdefs
+ hypreal_of_hypnat :: "hypnat => hypreal"
+ "hypreal_of_hypnat N ==
+ Abs_hypreal(\<Union>X \<in> Rep_hypnat(N). hyprel``{%n::nat. real (X n)})"
-subsection{*Embedding of the Hypernaturals into the Hyperreals*}
+lemma HNat_hypreal_of_nat [simp]: "hypreal_of_nat N \<in> Nats"
+by (simp add: hypreal_of_nat_def)
(*WARNING: FRAGILE!*)
-lemma lemma_hyprel_FUFN: "(Ya \<in> hyprel ``{%n. f(n)}) =
- ({n. f n = Ya n} \<in> FreeUltrafilterNat)"
-apply auto
-done
+lemma lemma_hyprel_FUFN:
+ "(Ya \<in> hyprel ``{%n. f(n)}) = ({n. f n = Ya n} \<in> FreeUltrafilterNat)"
+by force
lemma hypreal_of_hypnat:
"hypreal_of_hypnat (Abs_hypnat(hypnatrel``{%n. X n})) =
@@ -840,16 +755,13 @@
simp add: lemma_hyprel_FUFN)
done
-lemma inj_hypreal_of_hypnat: "inj(hypreal_of_hypnat)"
-apply (rule inj_onI)
-apply (rule_tac z = x in eq_Abs_hypnat)
-apply (rule_tac z = y in eq_Abs_hypnat)
+lemma hypreal_of_hypnat_inject [simp]:
+ "(hypreal_of_hypnat m = hypreal_of_hypnat n) = (m=n)"
+apply (rule eq_Abs_hypnat [of m])
+apply (rule eq_Abs_hypnat [of n])
apply (auto simp add: hypreal_of_hypnat)
done
-declare inj_hypreal_of_hypnat [THEN inj_eq, simp]
-declare inj_hypnat_of_nat [THEN inj_eq, simp]
-
lemma hypreal_of_hypnat_zero: "hypreal_of_hypnat 0 = 0"
by (simp add: hypnat_zero_def hypreal_zero_def hypreal_of_hypnat)
@@ -886,43 +798,21 @@
apply (simp add: hypreal_of_hypnat hypreal_zero_num hypreal_le)
done
-(*????DELETE??*)
-lemma hypnat_eq_zero: "\<forall>n. N \<le> n ==> N = (0::hypnat)"
-apply (drule_tac x = 0 in spec)
-apply (rule_tac z = N in eq_Abs_hypnat)
-apply (auto simp add: hypnat_le hypnat_zero_def)
-done
-
-(*????DELETE??*)
-lemma hypnat_not_all_eq_zero: "~ (\<forall>n. n = (0::hypnat))"
-by auto
-
-(*????DELETE??*)
-lemma hypnat_le_one_eq_one: "n \<noteq> 0 ==> (n \<le> (1::hypnat)) = (n = (1::hypnat))"
-by (auto simp add: order_le_less)
-
-(*WHERE DO THESE BELONG???*)
-lemma HNatInfinite_inverse_Infinitesimal: "n \<in> HNatInfinite ==> inverse (hypreal_of_hypnat n) \<in> Infinitesimal"
+lemma HNatInfinite_inverse_Infinitesimal [simp]:
+ "n \<in> HNatInfinite ==> inverse (hypreal_of_hypnat n) \<in> Infinitesimal"
apply (rule eq_Abs_hypnat [of n])
-apply (auto simp add: hypreal_of_hypnat hypreal_inverse HNatInfinite_FreeUltrafilterNat_iff Infinitesimal_FreeUltrafilterNat_iff2)
+apply (auto simp add: hypreal_of_hypnat hypreal_inverse
+ HNatInfinite_FreeUltrafilterNat_iff Infinitesimal_FreeUltrafilterNat_iff2)
apply (rule bexI, rule_tac [2] lemma_hyprel_refl, auto)
apply (drule_tac x = "m + 1" in spec, ultra)
done
-declare HNatInfinite_inverse_Infinitesimal [simp]
-
-lemma HNatInfinite_inverse_not_zero: "n \<in> HNatInfinite ==> hypreal_of_hypnat n \<noteq> 0"
-by (simp add: HNatInfinite_not_eq_zero)
-
ML
{*
val hypnat_of_nat_def = thm"hypnat_of_nat_def";
-val HNat_def = thm"HNat_def";
val HNatInfinite_def = thm"HNatInfinite_def";
val hypreal_of_hypnat_def = thm"hypreal_of_hypnat_def";
-val SNat_def = thm"SNat_def";
-val SHNat_def = thm"SHNat_def";
val hypnat_zero_def = thm"hypnat_zero_def";
val hypnat_one_def = thm"hypnat_one_def";
val hypnat_omega_def = thm"hypnat_omega_def";
@@ -939,7 +829,6 @@
val lemma_hypnatrel_refl = thm "lemma_hypnatrel_refl";
val hypnat_empty_not_mem = thm "hypnat_empty_not_mem";
val Rep_hypnat_nonempty = thm "Rep_hypnat_nonempty";
-val inj_hypnat_of_nat = thm "inj_hypnat_of_nat";
val eq_Abs_hypnat = thm "eq_Abs_hypnat";
val hypnat_add_congruent2 = thm "hypnat_add_congruent2";
val hypnat_add = thm "hypnat_add";
@@ -1000,39 +889,14 @@
val hypnat_of_nat_Suc = thm "hypnat_of_nat_Suc";
val hypnat_omega = thm "hypnat_omega";
val Rep_hypnat_omega = thm "Rep_hypnat_omega";
-val not_ex_hypnat_of_nat_eq_omega = thm "not_ex_hypnat_of_nat_eq_omega";
-val hypnat_of_nat_not_eq_omega = thm "hypnat_of_nat_not_eq_omega";
val SHNAT_omega_not_mem = thm "SHNAT_omega_not_mem";
-val SHNat_add = thm "SHNat_add";
-val SHNat_minus = thm "SHNat_minus";
-val SHNat_mult = thm "SHNat_mult";
-val SHNat_add_cancel = thm "SHNat_add_cancel";
-val SHNat_hypnat_of_nat = thm "SHNat_hypnat_of_nat";
-val SHNat_hypnat_of_nat_one = thm "SHNat_hypnat_of_nat_one";
-val SHNat_hypnat_of_nat_zero = thm "SHNat_hypnat_of_nat_zero";
-val SHNat_one = thm "SHNat_one";
-val SHNat_zero = thm "SHNat_zero";
-val SHNat_iff = thm "SHNat_iff";
-val SHNat_hypnat_of_nat_iff = thm "SHNat_hypnat_of_nat_iff";
-val leSuc_Un_eq = thm "leSuc_Un_eq";
-val finite_nat_le_segment = thm "finite_nat_le_segment";
-val lemma_unbounded_set = thm "lemma_unbounded_set";
val cofinite_mem_FreeUltrafilterNat = thm "cofinite_mem_FreeUltrafilterNat";
-val Compl_Collect_le = thm "Compl_Collect_le";
val hypnat_omega_gt_SHNat = thm "hypnat_omega_gt_SHNat";
val hypnat_of_nat_less_whn = thm "hypnat_of_nat_less_whn";
val hypnat_of_nat_le_whn = thm "hypnat_of_nat_le_whn";
val hypnat_zero_less_hypnat_omega = thm "hypnat_zero_less_hypnat_omega";
val hypnat_one_less_hypnat_omega = thm "hypnat_one_less_hypnat_omega";
val HNatInfinite_whn = thm "HNatInfinite_whn";
-val SHNat_not_HNatInfinite = thm "SHNat_not_HNatInfinite";
-val not_HNatInfinite_SHNat = thm "not_HNatInfinite_SHNat";
-val not_SHNat_HNatInfinite = thm "not_SHNat_HNatInfinite";
-val HNatInfinite_not_SHNat = thm "HNatInfinite_not_SHNat";
-val SHNat_not_HNatInfinite_iff = thm "SHNat_not_HNatInfinite_iff";
-val not_SHNat_HNatInfinite_iff = thm "not_SHNat_HNatInfinite_iff";
-val SHNat_HNatInfinite_disj = thm "SHNat_HNatInfinite_disj";
-val HNatInfinite_FreeUltrafilterNat_lemma = thm "HNatInfinite_FreeUltrafilterNat_lemma";
val HNatInfinite_iff = thm "HNatInfinite_iff";
val HNatInfinite_FreeUltrafilterNat = thm "HNatInfinite_FreeUltrafilterNat";
val FreeUltrafilterNat_HNatInfinite = thm "FreeUltrafilterNat_HNatInfinite";
@@ -1045,26 +909,16 @@
val HNatInfinite_SHNat_add = thm "HNatInfinite_SHNat_add";
val HNatInfinite_SHNat_diff = thm "HNatInfinite_SHNat_diff";
val HNatInfinite_add_one = thm "HNatInfinite_add_one";
-val HNatInfinite_minus_one = thm "HNatInfinite_minus_one";
val HNatInfinite_is_Suc = thm "HNatInfinite_is_Suc";
val HNat_hypreal_of_nat = thm "HNat_hypreal_of_nat";
-val HNat_add = thm "HNat_add";
-val HNat_mult = thm "HNat_mult";
-val lemma_hyprel_FUFN = thm "lemma_hyprel_FUFN";
val hypreal_of_hypnat = thm "hypreal_of_hypnat";
-val inj_hypreal_of_hypnat = thm "inj_hypreal_of_hypnat";
val hypreal_of_hypnat_zero = thm "hypreal_of_hypnat_zero";
val hypreal_of_hypnat_one = thm "hypreal_of_hypnat_one";
val hypreal_of_hypnat_add = thm "hypreal_of_hypnat_add";
val hypreal_of_hypnat_mult = thm "hypreal_of_hypnat_mult";
val hypreal_of_hypnat_less_iff = thm "hypreal_of_hypnat_less_iff";
-val hypreal_of_hypnat_eq_zero_iff = thm "hypreal_of_hypnat_eq_zero_iff";
val hypreal_of_hypnat_ge_zero = thm "hypreal_of_hypnat_ge_zero";
-val hypnat_eq_zero = thm "hypnat_eq_zero";
-val hypnat_not_all_eq_zero = thm "hypnat_not_all_eq_zero";
-val hypnat_le_one_eq_one = thm "hypnat_le_one_eq_one";
val HNatInfinite_inverse_Infinitesimal = thm "HNatInfinite_inverse_Infinitesimal";
-val HNatInfinite_inverse_not_zero = thm "HNatInfinite_inverse_not_zero";
*}
end
--- a/src/HOL/Hyperreal/HyperPow.thy Thu Feb 05 10:45:28 2004 +0100
+++ b/src/HOL/Hyperreal/HyperPow.thy Tue Feb 10 12:02:11 2004 +0100
@@ -163,8 +163,8 @@
lemma hyperpow_not_zero [rule_format (no_asm)]:
"r \<noteq> (0::hypreal) --> r pow n \<noteq> 0"
apply (simp (no_asm) add: hypreal_zero_def)
-apply (rule_tac z = n in eq_Abs_hypnat)
-apply (rule_tac z = r in eq_Abs_hypreal)
+apply (rule eq_Abs_hypnat [of n])
+apply (rule eq_Abs_hypreal [of r])
apply (auto simp add: hyperpow)
apply (drule FreeUltrafilterNat_Compl_mem, ultra)
done
@@ -172,29 +172,29 @@
lemma hyperpow_inverse:
"r \<noteq> (0::hypreal) --> inverse(r pow n) = (inverse r) pow n"
apply (simp (no_asm) add: hypreal_zero_def)
-apply (rule_tac z = n in eq_Abs_hypnat)
-apply (rule_tac z = r in eq_Abs_hypreal)
+apply (rule eq_Abs_hypnat [of n])
+apply (rule eq_Abs_hypreal [of r])
apply (auto dest!: FreeUltrafilterNat_Compl_mem simp add: hypreal_inverse hyperpow)
apply (rule FreeUltrafilterNat_subset)
apply (auto dest: realpow_not_zero intro: power_inverse)
done
lemma hyperpow_hrabs: "abs r pow n = abs (r pow n)"
-apply (rule_tac z = n in eq_Abs_hypnat)
-apply (rule_tac z = r in eq_Abs_hypreal)
+apply (rule eq_Abs_hypnat [of n])
+apply (rule eq_Abs_hypreal [of r])
apply (auto simp add: hypreal_hrabs hyperpow power_abs [symmetric])
done
lemma hyperpow_add: "r pow (n + m) = (r pow n) * (r pow m)"
-apply (rule_tac z = n in eq_Abs_hypnat)
-apply (rule_tac z = m in eq_Abs_hypnat)
-apply (rule_tac z = r in eq_Abs_hypreal)
+apply (rule eq_Abs_hypnat [of n])
+apply (rule eq_Abs_hypnat [of m])
+apply (rule eq_Abs_hypreal [of r])
apply (auto simp add: hyperpow hypnat_add hypreal_mult power_add)
done
lemma hyperpow_one: "r pow (1::hypnat) = r"
apply (unfold hypnat_one_def)
-apply (rule_tac z = r in eq_Abs_hypreal)
+apply (rule eq_Abs_hypreal [of r])
apply (auto simp add: hyperpow)
done
declare hyperpow_one [simp]
@@ -202,38 +202,38 @@
lemma hyperpow_two:
"r pow ((1::hypnat) + (1::hypnat)) = r * r"
apply (unfold hypnat_one_def)
-apply (rule_tac z = r in eq_Abs_hypreal)
+apply (rule eq_Abs_hypreal [of r])
apply (auto simp add: hyperpow hypnat_add hypreal_mult)
done
lemma hyperpow_gt_zero: "(0::hypreal) < r ==> 0 < r pow n"
apply (simp add: hypreal_zero_def)
-apply (rule_tac z = n in eq_Abs_hypnat)
-apply (rule_tac z = r in eq_Abs_hypreal)
+apply (rule eq_Abs_hypnat [of n])
+apply (rule eq_Abs_hypreal [of r])
apply (auto elim!: FreeUltrafilterNat_subset zero_less_power
simp add: hyperpow hypreal_less hypreal_le)
done
lemma hyperpow_ge_zero: "(0::hypreal) \<le> r ==> 0 \<le> r pow n"
apply (simp add: hypreal_zero_def)
-apply (rule_tac z = n in eq_Abs_hypnat)
-apply (rule_tac z = r in eq_Abs_hypreal)
+apply (rule eq_Abs_hypnat [of n])
+apply (rule eq_Abs_hypreal [of r])
apply (auto elim!: FreeUltrafilterNat_subset zero_le_power
simp add: hyperpow hypreal_le)
done
lemma hyperpow_le: "[|(0::hypreal) < x; x \<le> y|] ==> x pow n \<le> y pow n"
apply (simp add: hypreal_zero_def)
-apply (rule_tac z = n in eq_Abs_hypnat)
-apply (rule_tac z = x in eq_Abs_hypreal)
-apply (rule_tac z = y in eq_Abs_hypreal)
+apply (rule eq_Abs_hypnat [of n])
+apply (rule eq_Abs_hypreal [of x])
+apply (rule eq_Abs_hypreal [of y])
apply (auto simp add: hyperpow hypreal_le hypreal_less)
apply (erule FreeUltrafilterNat_Int [THEN FreeUltrafilterNat_subset], assumption)
apply (auto intro: power_mono)
done
lemma hyperpow_eq_one: "1 pow n = (1::hypreal)"
-apply (rule_tac z = n in eq_Abs_hypnat)
+apply (rule eq_Abs_hypnat [of n])
apply (auto simp add: hypreal_one_def hyperpow)
done
declare hyperpow_eq_one [simp]
@@ -241,15 +241,15 @@
lemma hrabs_hyperpow_minus_one: "abs(-1 pow n) = (1::hypreal)"
apply (subgoal_tac "abs ((- (1::hypreal)) pow n) = (1::hypreal) ")
apply simp
-apply (rule_tac z = n in eq_Abs_hypnat)
+apply (rule eq_Abs_hypnat [of n])
apply (auto simp add: hypreal_one_def hyperpow hypreal_minus hypreal_hrabs)
done
declare hrabs_hyperpow_minus_one [simp]
lemma hyperpow_mult: "(r * s) pow n = (r pow n) * (s pow n)"
-apply (rule_tac z = n in eq_Abs_hypnat)
-apply (rule_tac z = r in eq_Abs_hypreal)
-apply (rule_tac z = s in eq_Abs_hypreal)
+apply (rule eq_Abs_hypnat [of n])
+apply (rule eq_Abs_hypreal [of r])
+apply (rule eq_Abs_hypreal [of s])
apply (auto simp add: hyperpow hypreal_mult power_mult_distrib)
done
@@ -297,9 +297,9 @@
lemma hyperpow_less_le:
"[|(0::hypreal) \<le> r; r \<le> 1; n < N|] ==> r pow N \<le> r pow n"
-apply (rule_tac z = n in eq_Abs_hypnat)
-apply (rule_tac z = N in eq_Abs_hypnat)
-apply (rule_tac z = r in eq_Abs_hypreal)
+apply (rule eq_Abs_hypnat [of n])
+apply (rule eq_Abs_hypnat [of N])
+apply (rule eq_Abs_hypreal [of r])
apply (auto simp add: hyperpow hypreal_le hypreal_less hypnat_less
hypreal_zero_def hypreal_one_def)
apply (erule FreeUltrafilterNat_Int [THEN FreeUltrafilterNat_subset])
@@ -314,8 +314,7 @@
lemma hyperpow_realpow:
"(hypreal_of_real r) pow (hypnat_of_nat n) = hypreal_of_real (r ^ n)"
-apply (unfold hypreal_of_real_def hypnat_of_nat_def)
-apply (auto simp add: hyperpow)
+apply (simp add: hypreal_of_real_def hypnat_of_nat_eq hyperpow)
done
lemma hyperpow_SReal: "(hypreal_of_real r) pow (hypnat_of_nat n) \<in> Reals"
@@ -355,9 +354,8 @@
lemma hrealpow_hyperpow_Infinitesimal_iff:
"(x ^ n \<in> Infinitesimal) = (x pow (hypnat_of_nat n) \<in> Infinitesimal)"
-apply (unfold hypnat_of_nat_def)
-apply (rule_tac z = x in eq_Abs_hypreal)
-apply (auto simp add: hrealpow hyperpow)
+apply (rule eq_Abs_hypreal [of x])
+apply (simp add: hrealpow hyperpow hypnat_of_nat_eq)
done
lemma Infinitesimal_hrealpow:
--- a/src/HOL/Hyperreal/NSA.thy Thu Feb 05 10:45:28 2004 +0100
+++ b/src/HOL/Hyperreal/NSA.thy Tue Feb 10 12:02:11 2004 +0100
@@ -33,7 +33,7 @@
"x @= y == (x + -y) \<in> Infinitesimal"
-defs
+defs (overloaded)
(*standard real numbers as a subset of the hyperreals*)
SReal_def: "Reals == {x. \<exists>r. x = hypreal_of_real r}"
@@ -47,7 +47,8 @@
Closure laws for members of (embedded) set standard real Reals
--------------------------------------------------------------------*)
-lemma SReal_add: "[| (x::hypreal) \<in> Reals; y \<in> Reals |] ==> x + y \<in> Reals"
+lemma SReal_add [simp]:
+ "[| (x::hypreal) \<in> Reals; y \<in> Reals |] ==> x + y \<in> Reals"
apply (auto simp add: SReal_def)
apply (rule_tac x = "r + ra" in exI, simp)
done
@@ -1911,6 +1912,11 @@
apply (blast dest!: reals_Archimedean intro: order_less_trans)
done
+lemma of_nat_in_Reals [simp]: "(of_nat n::hypreal) \<in> \<real>"
+apply (induct n)
+apply (simp_all add: SReal_add);
+done
+
lemma lemma_Infinitesimal2: "(\<forall>r \<in> Reals. 0 < r --> x < r) =
(\<forall>n. x < inverse(hypreal_of_nat (Suc n)))"
apply safe
@@ -1918,13 +1924,14 @@
apply (simp (no_asm_use) add: SReal_inverse)
apply (rule real_of_nat_Suc_gt_zero [THEN positive_imp_inverse_positive, THEN hypreal_of_real_less_iff [THEN iffD2], THEN [2] impE])
prefer 2 apply assumption
-apply (simp add: real_of_nat_Suc_gt_zero hypreal_of_nat_def)
+apply (simp add: real_of_nat_Suc_gt_zero hypreal_of_nat_eq)
apply (auto dest!: reals_Archimedean simp add: SReal_iff)
apply (drule hypreal_of_real_less_iff [THEN iffD2])
-apply (simp add: real_of_nat_Suc_gt_zero hypreal_of_nat_def)
+apply (simp add: real_of_nat_Suc_gt_zero hypreal_of_nat_eq)
apply (blast intro: order_less_trans)
done
+
lemma Infinitesimal_hypreal_of_nat_iff:
"Infinitesimal = {x. \<forall>n. abs x < inverse (hypreal_of_nat (Suc n))}"
apply (simp add: Infinitesimal_def)
--- a/src/HOL/Hyperreal/NatStar.ML Thu Feb 05 10:45:28 2004 +0100
+++ b/src/HOL/Hyperreal/NatStar.ML Tue Feb 10 12:02:11 2004 +0100
@@ -6,6 +6,9 @@
nat=>nat functions
*)
+val hypnat_of_nat_eq = thm"hypnat_of_nat_eq";
+val SHNat_eq = thm"SHNat_eq";
+
Goalw [starsetNat_def]
"*sNat*(UNIV::nat set) = (UNIV::hypnat set)";
by (auto_tac (claset(), simpset() addsimps [FreeUltrafilterNat_Nat_set]));
@@ -111,28 +114,26 @@
by (REPEAT(blast_tac (claset() addIs [FreeUltrafilterNat_subset]) 1));
qed "NatStar_subset";
-Goalw [starsetNat_def,hypnat_of_nat_def]
- "a : A ==> hypnat_of_nat a : *sNat* A";
+Goal "a : A ==> hypnat_of_nat a : *sNat* A";
by (auto_tac (claset() addIs [FreeUltrafilterNat_subset],
- simpset()));
+ simpset() addsimps [starsetNat_def,hypnat_of_nat_eq]));
qed "NatStar_mem";
Goalw [starsetNat_def] "hypnat_of_nat ` A <= *sNat* A";
-by (auto_tac (claset(), simpset() addsimps [hypnat_of_nat_def]));
+by (auto_tac (claset(), simpset() addsimps [hypnat_of_nat_eq]));
by (blast_tac (claset() addIs [FreeUltrafilterNat_subset]) 1);
qed "NatStar_hypreal_of_real_image_subset";
Goal "Nats <= *sNat* (UNIV:: nat set)";
-by (simp_tac (simpset() addsimps [SHNat_hypnat_of_nat_iff,
- NatStar_hypreal_of_real_image_subset]) 1);
+by (auto_tac (claset(), simpset() addsimps [starsetNat_def,SHNat_eq,hypnat_of_nat_eq]));
qed "NatStar_SHNat_subset";
Goalw [starsetNat_def]
"*sNat* X Int Nats = hypnat_of_nat ` X";
by (auto_tac (claset(),
simpset() addsimps
- [hypnat_of_nat_def,SHNat_def]));
-by (fold_tac [hypnat_of_nat_def]);
+ [hypnat_of_nat_eq,SHNat_eq]));
+by (simp_tac (simpset() addsimps [hypnat_of_nat_eq RS sym]) 1);
by (rtac imageI 1 THEN rtac ccontr 1);
by (dtac bspec 1);
by (rtac lemma_hypnatrel_refl 1);
@@ -289,7 +290,7 @@
Goal "( *fNat2* (%x. k)) z = hypnat_of_nat k";
by (res_inst_tac [("z","z")] eq_Abs_hypnat 1);
-by (auto_tac (claset(), simpset() addsimps [starfunNat2, hypnat_of_nat_def]));
+by (auto_tac (claset(), simpset() addsimps [starfunNat2, hypnat_of_nat_eq]));
qed "starfunNat2_const_fun";
Addsimps [starfunNat2_const_fun];
@@ -312,13 +313,13 @@
Goal "( *fNat* f) (hypnat_of_nat a) = hypreal_of_real (f a)";
by (auto_tac (claset(),
- simpset() addsimps [starfunNat,hypnat_of_nat_def,hypreal_of_real_def]));
+ simpset() addsimps [starfunNat,hypnat_of_nat_eq,hypreal_of_real_def]));
qed "starfunNat_eq";
Addsimps [starfunNat_eq];
Goal "( *fNat2* f) (hypnat_of_nat a) = hypnat_of_nat (f a)";
-by (auto_tac (claset(), simpset() addsimps [starfunNat2,hypnat_of_nat_def]));
+by (auto_tac (claset(), simpset() addsimps [starfunNat2,hypnat_of_nat_eq]));
qed "starfunNat2_eq";
Addsimps [starfunNat2_eq];
@@ -337,7 +338,7 @@
by (Step_tac 1);
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
by (auto_tac (claset(),
- simpset() addsimps [starfunNat, hypnat_of_nat_def,hypreal_le,
+ simpset() addsimps [starfunNat, hypnat_of_nat_eq,hypreal_le,
hypreal_less, hypnat_le,hypnat_less]));
by (Ultra_tac 1);
by Auto_tac;
@@ -349,7 +350,7 @@
by (Step_tac 1);
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
by (auto_tac (claset(),
- simpset() addsimps [starfunNat, hypnat_of_nat_def,hypreal_le,
+ simpset() addsimps [starfunNat, hypnat_of_nat_eq,hypreal_le,
hypreal_less, hypnat_le,hypnat_less]));
by (Ultra_tac 1);
by Auto_tac;
@@ -384,12 +385,12 @@
Goal "( *fNat* (%n. (X n) ^ m)) N = ( *fNat* X) N pow hypnat_of_nat m";
by (res_inst_tac [("z","N")] eq_Abs_hypnat 1);
by (auto_tac (claset(),
- simpset() addsimps [hyperpow, hypnat_of_nat_def,starfunNat]));
+ simpset() addsimps [hyperpow, hypnat_of_nat_eq,starfunNat]));
qed "starfunNat_pow2";
-Goalw [hypnat_of_nat_def] "( *f* (%r. r ^ n)) R = (R) pow hypnat_of_nat n";
+Goal "( *f* (%r. r ^ n)) R = (R) pow hypnat_of_nat n";
by (res_inst_tac [("z","R")] eq_Abs_hypreal 1);
-by (auto_tac (claset(), simpset() addsimps [hyperpow,starfun]));
+by (auto_tac (claset(), simpset() addsimps [hyperpow,starfun,hypnat_of_nat_eq]));
qed "starfun_pow";
(*-----------------------------------------------------
@@ -469,7 +470,7 @@
qed "starfunNat_n_minus";
Goal "( *fNatn* f) (hypnat_of_nat n) = Abs_hypreal(hyprel `` {%i. f i n})";
-by (auto_tac (claset(), simpset() addsimps [starfunNat_n,hypnat_of_nat_def]));
+by (auto_tac (claset(), simpset() addsimps [starfunNat_n,hypnat_of_nat_eq]));
qed "starfunNat_n_eq";
Addsimps [starfunNat_n_eq];
@@ -477,7 +478,7 @@
by Auto_tac;
by (rtac ext 1 THEN rtac ccontr 1);
by (dres_inst_tac [("x","hypnat_of_nat(x)")] fun_cong 1);
-by (auto_tac (claset(), simpset() addsimps [starfunNat,hypnat_of_nat_def]));
+by (auto_tac (claset(), simpset() addsimps [starfunNat,hypnat_of_nat_eq]));
qed "starfun_eq_iff";
--- a/src/HOL/Hyperreal/SEQ.ML Thu Feb 05 10:45:28 2004 +0100
+++ b/src/HOL/Hyperreal/SEQ.ML Tue Feb 10 12:02:11 2004 +0100
@@ -4,6 +4,8 @@
Description : Theory of sequence and series of real numbers
*)
+val Nats_1 = thm"Nats_1";
+
fun CLAIM_SIMP str thms =
prove_goal (the_context()) str
(fn prems => [cut_facts_tac prems 1,
@@ -92,7 +94,7 @@
by (induct_tac "u" 1);
by (auto_tac (claset(),simpset() addsimps [lemma_NSLIMSEQ2]));
by (auto_tac (claset() addIs [(lemma_NSLIMSEQ3 RS finite_subset),
- finite_nat_le_segment], simpset()));
+ rewrite_rule [atMost_def] finite_atMost], simpset()));
by (dtac lemma_NSLIMSEQ1 1 THEN Step_tac 1);
by (ALLGOALS(Asm_simp_tac));
qed "NSLIMSEQ_finite_set";
@@ -1050,7 +1052,7 @@
simpset() addsimps [NSCauchy_def, NSLIMSEQ_def,starfunNat_shift_one]));
by (dtac bspec 1 THEN assume_tac 1);
by (dtac bspec 1 THEN assume_tac 1);
-by (dtac (SHNat_one RSN (2,HNatInfinite_SHNat_add)) 1);
+by (dtac (Nats_1 RSN (2,HNatInfinite_SHNat_add)) 1);
by (blast_tac (claset() addIs [approx_trans3]) 1);
qed "NSLIMSEQ_Suc";
@@ -1067,7 +1069,7 @@
simpset() addsimps [NSCauchy_def, NSLIMSEQ_def,starfunNat_shift_one]));
by (dtac bspec 1 THEN assume_tac 1);
by (dtac bspec 1 THEN assume_tac 1);
-by (ftac (SHNat_one RSN (2,HNatInfinite_SHNat_diff)) 1);
+by (ftac (Nats_1 RSN (2,HNatInfinite_SHNat_diff)) 1);
by (rotate_tac 2 1);
by (auto_tac (claset() addSDs [bspec] addIs [approx_trans3],
simpset()));
--- a/src/HOL/Hyperreal/Star.thy Thu Feb 05 10:45:28 2004 +0100
+++ b/src/HOL/Hyperreal/Star.thy Tue Feb 10 12:02:11 2004 +0100
@@ -456,14 +456,15 @@
In this theory since hypreal_hrabs proved here. (To Check:) Maybe
move both if possible?
-------------------------------------------------------------------*)
-lemma Infinitesimal_FreeUltrafilterNat_iff2: "(x:Infinitesimal) =
+lemma Infinitesimal_FreeUltrafilterNat_iff2:
+ "(x:Infinitesimal) =
(EX X:Rep_hypreal(x).
ALL m. {n. abs(X n) < inverse(real(Suc m))}
: FreeUltrafilterNat)"
-apply (rule_tac z = x in eq_Abs_hypreal)
+apply (rule eq_Abs_hypreal [of x])
apply (auto intro!: bexI lemma_hyprel_refl
- simp add: Infinitesimal_hypreal_of_nat_iff hypreal_of_real_def
- hypreal_inverse hypreal_hrabs hypreal_less hypreal_of_nat_def)
+ simp add: Infinitesimal_hypreal_of_nat_iff hypreal_of_real_def
+ hypreal_inverse hypreal_hrabs hypreal_less hypreal_of_nat_eq)
apply (drule_tac x = n in spec, ultra)
done
--- a/src/HOL/Integ/Bin.thy Thu Feb 05 10:45:28 2004 +0100
+++ b/src/HOL/Integ/Bin.thy Tue Feb 10 12:02:11 2004 +0100
@@ -8,7 +8,7 @@
header{*Arithmetic on Binary Integers*}
-theory Bin = Int + Numeral:
+theory Bin = IntDef + Numeral:
text{*The sign @{term Pls} stands for an infinite string of leading Falses.*}
text{*The sign @{term Min} stands for an infinite string of leading Trues.*}
@@ -258,7 +258,7 @@
lemma eq_number_of_eq:
"((number_of x::int) = number_of y) =
- iszero (number_of (bin_add x (bin_minus y)))"
+ iszero (number_of (bin_add x (bin_minus y)) :: int)"
apply (unfold iszero_def)
apply (simp add: compare_rls number_of_add number_of_minus)
done
@@ -272,14 +272,15 @@
done
lemma iszero_number_of_BIT:
- "iszero (number_of (w BIT x)) = (~x & iszero (number_of w::int))"
+ "iszero (number_of (w BIT x)::int) = (~x & iszero (number_of w::int))"
apply (unfold iszero_def)
apply (cases "(number_of w)::int" rule: int_cases)
apply (simp_all (no_asm_simp) add: compare_rls zero_reorient
zminus_zadd_distrib [symmetric] int_Suc0_eq_1 [symmetric] zadd_int)
done
-lemma iszero_number_of_0: "iszero (number_of (w BIT False)) = iszero (number_of w::int)"
+lemma iszero_number_of_0:
+ "iszero (number_of (w BIT False)::int) = iszero (number_of w::int)"
by (simp only: iszero_number_of_BIT simp_thms)
lemma iszero_number_of_1: "~ iszero (number_of (w BIT True)::int)"
@@ -291,24 +292,23 @@
lemma less_number_of_eq_neg:
"((number_of x::int) < number_of y)
- = neg (number_of (bin_add x (bin_minus y)))"
+ = neg (number_of (bin_add x (bin_minus y)) ::int )"
+by (simp add: neg_def number_of_add number_of_minus compare_rls)
-apply (unfold zless_def zdiff_def)
-apply (simp add: bin_mult_simps)
-done
(*But if Numeral0 is rewritten to 0 then this rule can't be applied:
Numeral0 IS (number_of Pls) *)
-lemma not_neg_number_of_Pls: "~ neg (number_of bin.Pls)"
-by (simp add: neg_eq_less_0)
+lemma not_neg_number_of_Pls: "~ neg (number_of bin.Pls ::int)"
+by (simp add: neg_def)
-lemma neg_number_of_Min: "neg (number_of bin.Min)"
-by (simp add: neg_eq_less_0 int_0_less_1)
+lemma neg_number_of_Min: "neg (number_of bin.Min ::int)"
+by (simp add: neg_def int_0_less_1)
-lemma neg_number_of_BIT: "neg (number_of (w BIT x)) = neg (number_of w)"
+lemma neg_number_of_BIT:
+ "neg (number_of (w BIT x)::int) = neg (number_of w ::int)"
apply simp
apply (cases "(number_of w)::int" rule: int_cases)
-apply (simp_all (no_asm_simp) add: int_Suc0_eq_1 [symmetric] zadd_int neg_eq_less_0 zdiff_def [symmetric] compare_rls)
+apply (simp_all (no_asm_simp) add: int_Suc0_eq_1 [symmetric] zadd_int neg_def zdiff_def [symmetric] compare_rls)
done
@@ -326,9 +326,7 @@
lemma zabs_number_of:
"abs(number_of x::int) =
(if number_of x < (0::int) then -number_of x else number_of x)"
-apply (unfold zabs_def)
-apply (rule refl)
-done
+by (simp add: zabs_def)
(*0 and 1 require special rewrites because they aren't numerals*)
lemma zabs_0: "abs (0::int) = 0"
--- a/src/HOL/Integ/Int.thy Thu Feb 05 10:45:28 2004 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,409 +0,0 @@
-(* Title: Integ/Int.thy
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1998 University of Cambridge
-*)
-
-header {*Type "int" is an Ordered Ring and Other Lemmas*}
-
-theory Int = IntDef:
-
-constdefs
- nat :: "int => nat"
- "nat(Z) == if neg Z then 0 else (THE m. Z = int m)"
-
-defs (overloaded)
- zabs_def: "abs(i::int) == if i < 0 then -i else i"
-
-
-lemma int_0 [simp]: "int 0 = (0::int)"
-by (simp add: Zero_int_def)
-
-lemma int_1 [simp]: "int 1 = 1"
-by (simp add: One_int_def)
-
-lemma int_Suc0_eq_1: "int (Suc 0) = 1"
-by (simp add: One_int_def One_nat_def)
-
-lemma neg_eq_less_0: "neg x = (x < 0)"
-by (unfold zdiff_def zless_def, auto)
-
-lemma not_neg_eq_ge_0: "(~neg x) = (0 \<le> x)"
-apply (unfold zle_def)
-apply (simp add: neg_eq_less_0)
-done
-
-subsection{*To simplify inequalities when Numeral1 can get simplified to 1*}
-
-lemma not_neg_0: "~ neg 0"
-by (simp add: One_int_def neg_eq_less_0)
-
-lemma not_neg_1: "~ neg 1"
-by (simp add: One_int_def neg_eq_less_0)
-
-lemma iszero_0: "iszero 0"
-by (simp add: iszero_def)
-
-lemma not_iszero_1: "~ iszero 1"
-by (simp only: Zero_int_def One_int_def One_nat_def iszero_def int_int_eq)
-
-
-subsection{*nat: magnitide of an integer, as a natural number*}
-
-lemma nat_int [simp]: "nat(int n) = n"
-by (unfold nat_def, auto)
-
-lemma nat_zero [simp]: "nat 0 = 0"
-apply (unfold Zero_int_def)
-apply (rule nat_int)
-done
-
-lemma neg_nat: "neg z ==> nat z = 0"
-by (unfold nat_def, auto)
-
-lemma not_neg_nat: "~ neg z ==> int (nat z) = z"
-apply (drule not_neg_eq_ge_0 [THEN iffD1])
-apply (drule zle_imp_zless_or_eq)
-apply (auto simp add: zless_iff_Suc_zadd)
-done
-
-lemma nat_0_le [simp]: "0 \<le> z ==> int (nat z) = z"
-by (simp add: neg_eq_less_0 zle_def not_neg_nat)
-
-lemma nat_le_0 [simp]: "z \<le> 0 ==> nat z = 0"
-by (auto simp add: order_le_less neg_eq_less_0 zle_def neg_nat)
-
-text{*An alternative condition is @{term "0 \<le> w"} *}
-lemma nat_mono_iff: "0 < z ==> (nat w < nat z) = (w < z)"
-apply (subst zless_int [symmetric])
-apply (simp (no_asm_simp) add: not_neg_nat not_neg_eq_ge_0 order_le_less)
-apply (case_tac "neg w")
- apply (simp add: neg_eq_less_0 neg_nat)
- apply (blast intro: order_less_trans)
-apply (simp add: not_neg_nat)
-done
-
-lemma zless_nat_conj: "(nat w < nat z) = (0 < z & w < z)"
-apply (case_tac "0 < z")
-apply (auto simp add: nat_mono_iff linorder_not_less)
-done
-
-subsection{*Monotonicity results*}
-
-text{*Most are available in theory @{text Ring_and_Field}, but they are
- not yet available: we must prove @{text zadd_zless_mono} before we
- can prove that the integers are a ring.*}
-
-lemma zadd_right_cancel_zless [simp]: "(v+z < w+z) = (v < (w::int))"
-by (simp add: zless_def zdiff_def zadd_ac)
-
-lemma zadd_left_cancel_zless [simp]: "(z+v < z+w) = (v < (w::int))"
-by (simp add: zless_def zdiff_def zadd_ac)
-
-lemma zadd_right_cancel_zle [simp] : "(v+z \<le> w+z) = (v \<le> (w::int))"
-by (simp add: linorder_not_less [symmetric])
-
-lemma zadd_left_cancel_zle [simp] : "(z+v \<le> z+w) = (v \<le> (w::int))"
-by (simp add: linorder_not_less [symmetric])
-
-(*"v\<le>w ==> v+z \<le> w+z"*)
-lemmas zadd_zless_mono1 = zadd_right_cancel_zless [THEN iffD2, standard]
-
-(*"v\<le>w ==> z+v \<le> z+w"*)
-lemmas zadd_zless_mono2 = zadd_left_cancel_zless [THEN iffD2, standard]
-
-(*"v\<le>w ==> v+z \<le> w+z"*)
-lemmas zadd_zle_mono1 = zadd_right_cancel_zle [THEN iffD2, standard]
-
-(*"v\<le>w ==> z+v \<le> z+w"*)
-lemmas zadd_zle_mono2 = zadd_left_cancel_zle [THEN iffD2, standard]
-
-lemma zadd_zle_mono: "[| w'\<le>w; z'\<le>z |] ==> w' + z' \<le> w + (z::int)"
-by (erule zadd_zle_mono1 [THEN zle_trans], simp)
-
-lemma zadd_zless_mono: "[| w'<w; z'\<le>z |] ==> w' + z' < w + (z::int)"
-by (erule zadd_zless_mono1 [THEN order_less_le_trans], simp)
-
-
-subsection{*Strict Monotonicity of Multiplication*}
-
-text{*strict, in 1st argument; proof is by induction on k>0*}
-lemma zmult_zless_mono2_lemma: "i<j ==> 0<k --> int k * i < int k * j"
-apply (induct_tac "k", simp)
-apply (simp add: int_Suc)
-apply (case_tac "n=0")
-apply (simp_all add: zadd_zmult_distrib int_Suc0_eq_1 order_le_less)
-apply (simp_all add: zadd_zless_mono int_Suc0_eq_1 order_le_less)
-done
-
-lemma zmult_zless_mono2: "[| i<j; (0::int) < k |] ==> k*i < k*j"
-apply (rule_tac t = k in not_neg_nat [THEN subst])
-apply (erule_tac [2] zmult_zless_mono2_lemma [THEN mp])
-apply (simp add: not_neg_eq_ge_0 order_le_less)
-apply (frule conjI [THEN zless_nat_conj [THEN iffD2]], auto)
-done
-
-
-text{*The Integers Form an Ordered Ring*}
-instance int :: ordered_ring
-proof
- fix i j k :: int
- show "0 < (1::int)" by (rule int_0_less_1)
- show "i \<le> j ==> k + i \<le> k + j" by simp
- show "i < j ==> 0 < k ==> k * i < k * j" by (simp add: zmult_zless_mono2)
- show "\<bar>i\<bar> = (if i < 0 then -i else i)" by (simp only: zabs_def)
-qed
-
-
-subsection{*Comparison laws*}
-
-text{*Legacy bindings: all are in theory @{text Ring_and_Field}.*}
-
-lemma zminus_zless_zminus: "(- x < - y) = (y < (x::int))"
- by (rule Ring_and_Field.neg_less_iff_less)
-
-lemma zminus_zle_zminus: "(- x \<le> - y) = (y \<le> (x::int))"
- by (rule Ring_and_Field.neg_le_iff_le)
-
-
-text{*The next several equations can make the simplifier loop!*}
-
-lemma zless_zminus: "(x < - y) = (y < - (x::int))"
- by (rule Ring_and_Field.less_minus_iff)
-
-lemma zminus_zless: "(- x < y) = (- y < (x::int))"
- by (rule Ring_and_Field.minus_less_iff)
-
-lemma zle_zminus: "(x \<le> - y) = (y \<le> - (x::int))"
- by (rule Ring_and_Field.le_minus_iff)
-
-lemma zminus_zle: "(- x \<le> y) = (- y \<le> (x::int))"
- by (rule Ring_and_Field.minus_le_iff)
-
-lemma equation_zminus: "(x = - y) = (y = - (x::int))"
- by (rule Ring_and_Field.equation_minus_iff)
-
-lemma zminus_equation: "(- x = y) = (- (y::int) = x)"
- by (rule Ring_and_Field.minus_equation_iff)
-
-
-subsection{*Lemmas about the Function @{term int} and Orderings*}
-
-lemma negative_zless_0: "- (int (Suc n)) < 0"
-by (simp add: zless_def)
-
-lemma negative_zless [iff]: "- (int (Suc n)) < int m"
-by (rule negative_zless_0 [THEN order_less_le_trans], simp)
-
-lemma negative_zle_0: "- int n \<le> 0"
-by (simp add: zminus_zle)
-
-lemma negative_zle [iff]: "- int n \<le> int m"
-by (simp add: zless_def zle_def zdiff_def zadd_int)
-
-lemma not_zle_0_negative [simp]: "~(0 \<le> - (int (Suc n)))"
-by (subst zle_zminus, simp)
-
-lemma int_zle_neg: "(int n \<le> - int m) = (n = 0 & m = 0)"
-apply safe
-apply (drule_tac [2] zle_zminus [THEN iffD1])
-apply (auto dest: zle_trans [OF _ negative_zle_0])
-done
-
-lemma not_int_zless_negative [simp]: "~(int n < - int m)"
-by (simp add: zle_def [symmetric])
-
-lemma negative_eq_positive [simp]: "(- int n = int m) = (n = 0 & m = 0)"
-apply (rule iffI)
-apply (rule int_zle_neg [THEN iffD1])
-apply (drule sym)
-apply (simp_all (no_asm_simp))
-done
-
-lemma zle_iff_zadd: "(w \<le> z) = (\<exists>n. z = w + int n)"
-by (force intro: exI [of _ "0::nat"]
- intro!: not_sym [THEN not0_implies_Suc]
- simp add: zless_iff_Suc_zadd int_le_less)
-
-lemma abs_int_eq [simp]: "abs (int m) = int m"
-by (simp add: zabs_def)
-
-text{*This version is proved for all ordered rings, not just integers!
- It is proved here because attribute @{text arith_split} is not available
- in theory @{text Ring_and_Field}.
- But is it really better than just rewriting with @{text abs_if}?*}
-lemma abs_split [arith_split]:
- "P(abs(a::'a::ordered_ring)) = ((0 \<le> a --> P a) & (a < 0 --> P(-a)))"
-by (force dest: order_less_le_trans simp add: abs_if linorder_not_less)
-
-
-subsection{*Misc Results*}
-
-lemma nat_zminus_int [simp]: "nat(- (int n)) = 0"
-apply (unfold nat_def)
-apply (auto simp add: neg_eq_less_0 zero_reorient zminus_zless)
-done
-
-lemma zless_nat_eq_int_zless: "(m < nat z) = (int m < z)"
-apply (case_tac "neg z")
-apply (erule_tac [2] not_neg_nat [THEN subst])
-apply (auto simp add: neg_nat)
-apply (auto dest: order_less_trans simp add: neg_eq_less_0)
-done
-
-lemma zless_eq_neg: "(w<z) = neg(w-z)"
-by (simp add: zless_def)
-
-lemma eq_eq_iszero: "(w=z) = iszero(w-z)"
-by (simp add: iszero_def diff_eq_eq)
-
-lemma zle_eq_not_neg: "(w\<le>z) = (~ neg(z-w))"
-by (simp add: zle_def zless_def)
-
-
-subsection{*Monotonicity of Multiplication*}
-
-lemma zmult_zle_mono1: "[| i \<le> j; (0::int) \<le> k |] ==> i*k \<le> j*k"
- by (rule Ring_and_Field.mult_right_mono)
-
-lemma zmult_zle_mono1_neg: "[| i \<le> j; k \<le> (0::int) |] ==> j*k \<le> i*k"
- by (rule Ring_and_Field.mult_right_mono_neg)
-
-lemma zmult_zle_mono2: "[| i \<le> j; (0::int) \<le> k |] ==> k*i \<le> k*j"
- by (rule Ring_and_Field.mult_left_mono)
-
-lemma zmult_zle_mono2_neg: "[| i \<le> j; k \<le> (0::int) |] ==> k*j \<le> k*i"
- by (rule Ring_and_Field.mult_left_mono_neg)
-
-(* \<le> monotonicity, BOTH arguments*)
-lemma zmult_zle_mono:
- "[| i \<le> j; k \<le> l; (0::int) \<le> j; (0::int) \<le> k |] ==> i*k \<le> j*l"
- by (rule Ring_and_Field.mult_mono)
-
-lemma zmult_zless_mono1: "[| i<j; (0::int) < k |] ==> i*k < j*k"
- by (rule Ring_and_Field.mult_strict_right_mono)
-
-lemma zmult_zless_mono1_neg: "[| i<j; k < (0::int) |] ==> j*k < i*k"
- by (rule Ring_and_Field.mult_strict_right_mono_neg)
-
-lemma zmult_zless_mono2_neg: "[| i<j; k < (0::int) |] ==> k*j < k*i"
- by (rule Ring_and_Field.mult_strict_left_mono_neg)
-
-lemma zmult_eq_0_iff [iff]: "(m*n = (0::int)) = (m = 0 | n = 0)"
- by simp
-
-lemma zmult_zless_cancel2: "(m*k < n*k) = (((0::int) < k & m<n) | (k<0 & n<m))"
- by (rule Ring_and_Field.mult_less_cancel_right)
-
-lemma zmult_zless_cancel1:
- "(k*m < k*n) = (((0::int) < k & m<n) | (k < 0 & n<m))"
- by (rule Ring_and_Field.mult_less_cancel_left)
-
-lemma zmult_zle_cancel2:
- "(m*k \<le> n*k) = (((0::int) < k --> m\<le>n) & (k < 0 --> n\<le>m))"
- by (rule Ring_and_Field.mult_le_cancel_right)
-
-lemma zmult_zle_cancel1:
- "(k*m \<le> k*n) = (((0::int) < k --> m\<le>n) & (k < 0 --> n\<le>m))"
- by (rule Ring_and_Field.mult_le_cancel_left)
-
-lemma zmult_cancel2: "(m*k = n*k) = (k = (0::int) | m=n)"
- by (rule Ring_and_Field.mult_cancel_right)
-
-lemma zmult_cancel1 [simp]: "(k*m = k*n) = (k = (0::int) | m=n)"
- by (rule Ring_and_Field.mult_cancel_left)
-
-
-text{*A case theorem distinguishing non-negative and negative int*}
-
-lemma negD: "neg x ==> \<exists>n. x = - (int (Suc n))"
-by (auto simp add: neg_eq_less_0 zless_iff_Suc_zadd
- diff_eq_eq [symmetric] zdiff_def)
-
-lemma int_cases [cases type: int, case_names nonneg neg]:
- "[|!! n. z = int n ==> P; !! n. z = - (int (Suc n)) ==> P |] ==> P"
-apply (case_tac "neg z")
-apply (fast dest!: negD)
-apply (drule not_neg_nat [symmetric], auto)
-done
-
-lemma int_induct [induct type: int, case_names nonneg neg]:
- "[|!! n. P (int n); !!n. P (- (int (Suc n))) |] ==> P z"
- by (cases z) auto
-
-
-(*Legacy ML bindings, but no longer the structure Int.*)
-ML
-{*
-val zabs_def = thm "zabs_def"
-val nat_def = thm "nat_def"
-
-val int_0 = thm "int_0";
-val int_1 = thm "int_1";
-val int_Suc0_eq_1 = thm "int_Suc0_eq_1";
-val neg_eq_less_0 = thm "neg_eq_less_0";
-val not_neg_eq_ge_0 = thm "not_neg_eq_ge_0";
-val not_neg_0 = thm "not_neg_0";
-val not_neg_1 = thm "not_neg_1";
-val iszero_0 = thm "iszero_0";
-val not_iszero_1 = thm "not_iszero_1";
-val int_0_less_1 = thm "int_0_less_1";
-val int_0_neq_1 = thm "int_0_neq_1";
-val zless_eq_neg = thm "zless_eq_neg";
-val eq_eq_iszero = thm "eq_eq_iszero";
-val zle_eq_not_neg = thm "zle_eq_not_neg";
-val zadd_right_cancel_zless = thm "zadd_right_cancel_zless";
-val zadd_left_cancel_zless = thm "zadd_left_cancel_zless";
-val zadd_right_cancel_zle = thm "zadd_right_cancel_zle";
-val zadd_left_cancel_zle = thm "zadd_left_cancel_zle";
-val zadd_zless_mono1 = thm "zadd_zless_mono1";
-val zadd_zless_mono2 = thm "zadd_zless_mono2";
-val zadd_zle_mono1 = thm "zadd_zle_mono1";
-val zadd_zle_mono2 = thm "zadd_zle_mono2";
-val zadd_zle_mono = thm "zadd_zle_mono";
-val zadd_zless_mono = thm "zadd_zless_mono";
-val zminus_zless_zminus = thm "zminus_zless_zminus";
-val zminus_zle_zminus = thm "zminus_zle_zminus";
-val zless_zminus = thm "zless_zminus";
-val zminus_zless = thm "zminus_zless";
-val zle_zminus = thm "zle_zminus";
-val zminus_zle = thm "zminus_zle";
-val equation_zminus = thm "equation_zminus";
-val zminus_equation = thm "zminus_equation";
-val negative_zless = thm "negative_zless";
-val negative_zle = thm "negative_zle";
-val not_zle_0_negative = thm "not_zle_0_negative";
-val not_int_zless_negative = thm "not_int_zless_negative";
-val negative_eq_positive = thm "negative_eq_positive";
-val zle_iff_zadd = thm "zle_iff_zadd";
-val abs_int_eq = thm "abs_int_eq";
-val abs_split = thm"abs_split";
-val nat_int = thm "nat_int";
-val nat_zminus_int = thm "nat_zminus_int";
-val nat_zero = thm "nat_zero";
-val not_neg_nat = thm "not_neg_nat";
-val neg_nat = thm "neg_nat";
-val zless_nat_eq_int_zless = thm "zless_nat_eq_int_zless";
-val nat_0_le = thm "nat_0_le";
-val nat_le_0 = thm "nat_le_0";
-val zless_nat_conj = thm "zless_nat_conj";
-val int_cases = thm "int_cases";
-val zmult_zle_mono1 = thm "zmult_zle_mono1";
-val zmult_zle_mono1_neg = thm "zmult_zle_mono1_neg";
-val zmult_zle_mono2 = thm "zmult_zle_mono2";
-val zmult_zle_mono2_neg = thm "zmult_zle_mono2_neg";
-val zmult_zle_mono = thm "zmult_zle_mono";
-val zmult_zless_mono2 = thm "zmult_zless_mono2";
-val zmult_zless_mono1 = thm "zmult_zless_mono1";
-val zmult_zless_mono1_neg = thm "zmult_zless_mono1_neg";
-val zmult_zless_mono2_neg = thm "zmult_zless_mono2_neg";
-val zmult_eq_0_iff = thm "zmult_eq_0_iff";
-val zmult_zless_cancel2 = thm "zmult_zless_cancel2";
-val zmult_zless_cancel1 = thm "zmult_zless_cancel1";
-val zmult_zle_cancel2 = thm "zmult_zle_cancel2";
-val zmult_zle_cancel1 = thm "zmult_zle_cancel1";
-val zmult_cancel2 = thm "zmult_cancel2";
-val zmult_cancel1 = thm "zmult_cancel1";
-*}
-
-end
--- a/src/HOL/Integ/IntArith.thy Thu Feb 05 10:45:28 2004 +0100
+++ b/src/HOL/Integ/IntArith.thy Tue Feb 10 12:02:11 2004 +0100
@@ -12,15 +12,11 @@
subsection{*Inequality Reasoning for the Arithmetic Simproc*}
lemma zless_imp_add1_zle: "w<z ==> w + (1::int) \<le> z"
- proof (auto simp add: zle_def zless_iff_Suc_zadd)
- fix m n
- assume "w + 1 = w + (1 + int m) + (1 + int n)"
- hence "(w + 1) + (1 + int (m + n)) = (w + 1) + 0"
- by (simp add: add_ac zadd_int [symmetric])
- hence "int (Suc(m+n)) = 0"
- by (simp only: Ring_and_Field.add_left_cancel int_Suc)
- thus False by (simp only: int_eq_0_conv)
- qed
+apply (rule eq_Abs_Integ [of z])
+apply (rule eq_Abs_Integ [of w])
+apply (simp add: linorder_not_le [symmetric] zle int_def zadd One_int_def)
+done
+
use "int_arith1.ML"
setup int_arith_setup
@@ -86,11 +82,11 @@
by (subst nat_eq_iff, simp)
lemma nat_less_eq_zless: "0 \<le> w ==> (nat w < nat z) = (w<z)"
-apply (case_tac "neg z")
+apply (case_tac "z < 0")
apply (auto simp add: nat_less_iff)
-apply (auto intro: zless_trans simp add: neg_eq_less_0 zle_def)
done
+
lemma nat_le_eq_zle: "0 < w | 0 \<le> z ==> (nat w \<le> nat z) = (w\<le>z)"
by (auto simp add: linorder_not_less [symmetric] zless_nat_conj)
@@ -229,12 +225,12 @@
lemma zmult_eq_self_iff: "(m = m*(n::int)) = (n = 1 | m = 0)"
apply auto
apply (subgoal_tac "m*1 = m*n")
-apply (drule zmult_cancel1 [THEN iffD1], auto)
+apply (drule mult_cancel_left [THEN iffD1], auto)
done
lemma zless_1_zmult: "[| 1 < m; 1 < n |] ==> 1 < m*(n::int)"
apply (rule_tac y = "1*n" in order_less_trans)
-apply (rule_tac [2] zmult_zless_mono1)
+apply (rule_tac [2] mult_strict_right_mono)
apply (simp_all (no_asm_simp))
done
--- a/src/HOL/Integ/IntDef.thy Thu Feb 05 10:45:28 2004 +0100
+++ b/src/HOL/Integ/IntDef.thy Tue Feb 10 12:02:11 2004 +0100
@@ -27,13 +27,6 @@
int :: "nat => int"
"int m == Abs_Integ(intrel `` {(m,0)})"
-
- neg :: "int => bool"
- "neg(Z) == \<exists>x y. x<y & (x,y::nat):Rep_Integ(Z)"
-
- (*For simplifying equalities*)
- iszero :: "int => bool"
- "iszero z == z = (0::int)"
defs (overloaded)
@@ -48,16 +41,17 @@
intrel``{(x1+x2, y1+y2)})"
zdiff_def: "z - (w::int) == z + (-w)"
-
- zless_def: "z<w == neg(z - w)"
-
- zle_def: "z <= (w::int) == ~(w < z)"
-
zmult_def:
"z * w ==
Abs_Integ(\<Union>(x1,y1) \<in> Rep_Integ(z). \<Union>(x2,y2) \<in> Rep_Integ(w).
intrel``{(x1*x2 + y1*y2, x1*y2 + y1*x2)})"
+ zless_def: "(z < (w::int)) == (z \<le> w & z \<noteq> w)"
+
+ zle_def:
+ "z \<le> (w::int) == \<exists>x1 y1 x2 y2. x1 + y2 \<le> x2 + y1 &
+ (x1,y1) \<in> Rep_Integ z & (x2,y2) \<in> Rep_Integ w"
+
lemma intrel_iff [simp]: "(((x1,y1),(x2,y2)) \<in> intrel) = (x1+y2 = x2+y1)"
by (unfold intrel_def, blast)
@@ -121,8 +115,8 @@
done
lemma zminus_zminus [simp]: "- (- z) = (z::int)"
-apply (rule_tac z = z in eq_Abs_Integ)
-apply (simp (no_asm_simp) add: zminus)
+apply (rule eq_Abs_Integ [of z])
+apply (simp add: zminus)
done
lemma inj_zminus: "inj(%z::int. -z)"
@@ -134,16 +128,6 @@
by (simp add: int_def Zero_int_def zminus)
-subsection{*neg: the test for negative integers*}
-
-
-lemma not_neg_int [simp]: "~ neg(int n)"
-by (simp add: neg_def int_def)
-
-lemma neg_zminus_int [simp]: "neg(- (int (Suc n)))"
-by (simp add: neg_def int_def zminus)
-
-
subsection{*zadd: addition on Integ*}
lemma zadd:
@@ -155,22 +139,22 @@
done
lemma zminus_zadd_distrib [simp]: "- (z + w) = (- z) + (- w::int)"
-apply (rule_tac z = z in eq_Abs_Integ)
-apply (rule_tac z = w in eq_Abs_Integ)
-apply (simp (no_asm_simp) add: zminus zadd)
+apply (rule eq_Abs_Integ [of z])
+apply (rule eq_Abs_Integ [of w])
+apply (simp add: zminus zadd)
done
lemma zadd_commute: "(z::int) + w = w + z"
-apply (rule_tac z = z in eq_Abs_Integ)
-apply (rule_tac z = w in eq_Abs_Integ)
-apply (simp (no_asm_simp) add: add_ac zadd)
+apply (rule eq_Abs_Integ [of z])
+apply (rule eq_Abs_Integ [of w])
+apply (simp add: add_ac zadd)
done
lemma zadd_assoc: "((z1::int) + z2) + z3 = z1 + (z2 + z3)"
-apply (rule_tac z = z1 in eq_Abs_Integ)
-apply (rule_tac z = z2 in eq_Abs_Integ)
-apply (rule_tac z = z3 in eq_Abs_Integ)
-apply (simp (no_asm_simp) add: zadd add_assoc)
+apply (rule eq_Abs_Integ [of z1])
+apply (rule eq_Abs_Integ [of z2])
+apply (rule eq_Abs_Integ [of z3])
+apply (simp add: zadd add_assoc)
done
(*For AC rewriting*)
@@ -197,8 +181,8 @@
(*also for the instance declaration int :: plus_ac0*)
lemma zadd_0 [simp]: "(0::int) + z = z"
apply (unfold Zero_int_def int_def)
-apply (rule_tac z = z in eq_Abs_Integ)
-apply (simp (no_asm_simp) add: zadd)
+apply (rule eq_Abs_Integ [of z])
+apply (simp add: zadd)
done
lemma zadd_0_right [simp]: "z + (0::int) = z"
@@ -206,8 +190,8 @@
lemma zadd_zminus_inverse [simp]: "z + (- z) = (0::int)"
apply (unfold int_def Zero_int_def)
-apply (rule_tac z = z in eq_Abs_Integ)
-apply (simp (no_asm_simp) add: zminus zadd add_commute)
+apply (rule eq_Abs_Integ [of z])
+apply (simp add: zminus zadd add_commute)
done
lemma zadd_zminus_inverse2 [simp]: "(- z) + z = (0::int)"
@@ -236,57 +220,52 @@
lemma zadd_assoc_cong: "(z::int) + v = z' + v' ==> z + (v + w) = z' + (v' + w)"
by (simp add: zadd_assoc [symmetric])
-lemma zadd_assoc_swap: "(z::int) + (v + w) = v + (z + w)"
-by (rule zadd_commute [THEN zadd_assoc_cong])
-
subsection{*zmult: multiplication on Integ*}
-(*Congruence property for multiplication*)
+text{*Congruence property for multiplication*}
lemma zmult_congruent2: "congruent2 intrel
(%p1 p2. (%(x1,y1). (%(x2,y2).
intrel``{(x1*x2 + y1*y2, x1*y2 + y1*x2)}) p2) p1)"
apply (rule equiv_intrel [THEN congruent2_commuteI])
-apply (rule_tac [2] p=w in PairE)
-apply (force simp add: add_ac mult_ac, clarify)
-apply (simp (no_asm_simp) del: equiv_intrel_iff add: add_ac mult_ac)
+ apply (force simp add: add_ac mult_ac)
+apply (clarify, simp del: equiv_intrel_iff add: add_ac mult_ac)
apply (rename_tac x1 x2 y1 y2 z1 z2)
apply (rule equiv_class_eq [OF equiv_intrel intrel_iff [THEN iffD2]])
-apply (simp add: intrel_def)
-apply (subgoal_tac "x1*z1 + y2*z1 = y1*z1 + x2*z1 & x1*z2 + y2*z2 = y1*z2 + x2*z2", arith)
+apply (subgoal_tac "x1*z1 + y2*z1 = y1*z1 + x2*z1 & x1*z2 + y2*z2 = y1*z2 + x2*z2")
+apply (simp add: mult_ac, arith)
apply (simp add: add_mult_distrib [symmetric])
done
lemma zmult:
"Abs_Integ((intrel``{(x1,y1)})) * Abs_Integ((intrel``{(x2,y2)})) =
Abs_Integ(intrel `` {(x1*x2 + y1*y2, x1*y2 + y1*x2)})"
-apply (unfold zmult_def)
-apply (simp (no_asm_simp) add: UN_UN_split_split_eq zmult_congruent2 equiv_intrel [THEN UN_equiv_class2])
-done
+by (simp add: zmult_def UN_UN_split_split_eq zmult_congruent2
+ equiv_intrel [THEN UN_equiv_class2])
lemma zmult_zminus: "(- z) * w = - (z * (w::int))"
-apply (rule_tac z = z in eq_Abs_Integ)
-apply (rule_tac z = w in eq_Abs_Integ)
-apply (simp (no_asm_simp) add: zminus zmult add_ac)
+apply (rule eq_Abs_Integ [of z])
+apply (rule eq_Abs_Integ [of w])
+apply (simp add: zminus zmult add_ac)
done
lemma zmult_commute: "(z::int) * w = w * z"
-apply (rule_tac z = z in eq_Abs_Integ)
-apply (rule_tac z = w in eq_Abs_Integ)
-apply (simp (no_asm_simp) add: zmult add_ac mult_ac)
+apply (rule eq_Abs_Integ [of z])
+apply (rule eq_Abs_Integ [of w])
+apply (simp add: zmult add_ac mult_ac)
done
lemma zmult_assoc: "((z1::int) * z2) * z3 = z1 * (z2 * z3)"
-apply (rule_tac z = z1 in eq_Abs_Integ)
-apply (rule_tac z = z2 in eq_Abs_Integ)
-apply (rule_tac z = z3 in eq_Abs_Integ)
-apply (simp (no_asm_simp) add: add_mult_distrib2 zmult add_ac mult_ac)
+apply (rule eq_Abs_Integ [of z1])
+apply (rule eq_Abs_Integ [of z2])
+apply (rule eq_Abs_Integ [of z3])
+apply (simp add: add_mult_distrib2 zmult add_ac mult_ac)
done
lemma zadd_zmult_distrib: "((z1::int) + z2) * w = (z1 * w) + (z2 * w)"
-apply (rule_tac z = z1 in eq_Abs_Integ)
-apply (rule_tac z = z2 in eq_Abs_Integ)
-apply (rule_tac z = w in eq_Abs_Integ)
+apply (rule eq_Abs_Integ [of z1])
+apply (rule eq_Abs_Integ [of z2])
+apply (rule eq_Abs_Integ [of w])
apply (simp add: add_mult_distrib2 zadd zmult add_ac mult_ac)
done
@@ -314,14 +293,14 @@
lemma zmult_0 [simp]: "0 * z = (0::int)"
apply (unfold Zero_int_def int_def)
-apply (rule_tac z = z in eq_Abs_Integ)
-apply (simp (no_asm_simp) add: zmult)
+apply (rule eq_Abs_Integ [of z])
+apply (simp add: zmult)
done
lemma zmult_1 [simp]: "(1::int) * z = z"
apply (unfold One_int_def int_def)
-apply (rule_tac z = z in eq_Abs_Integ)
-apply (simp (no_asm_simp) add: zmult)
+apply (rule eq_Abs_Integ [of z])
+apply (simp add: zmult)
done
lemma zmult_0_right [simp]: "z * 0 = (0::int)"
@@ -352,64 +331,73 @@
qed
-subsection{*Theorems about the Ordering*}
+subsection{*The @{text "\<le>"} Ordering*}
+
+lemma zle:
+ "(Abs_Integ(intrel``{(x1,y1)}) \<le> Abs_Integ(intrel``{(x2,y2)})) =
+ (x1 + y2 \<le> x2 + y1)"
+by (force simp add: zle_def)
+
+lemma zle_refl: "w \<le> (w::int)"
+apply (rule eq_Abs_Integ [of w])
+apply (force simp add: zle)
+done
+
+lemma zle_trans: "[| i \<le> j; j \<le> k |] ==> i \<le> (k::int)"
+apply (rule eq_Abs_Integ [of i])
+apply (rule eq_Abs_Integ [of j])
+apply (rule eq_Abs_Integ [of k])
+apply (simp add: zle)
+done
+
+lemma zle_anti_sym: "[| z \<le> w; w \<le> z |] ==> z = (w::int)"
+apply (rule eq_Abs_Integ [of w])
+apply (rule eq_Abs_Integ [of z])
+apply (simp add: zle)
+done
+
+(* Axiom 'order_less_le' of class 'order': *)
+lemma zless_le: "((w::int) < z) = (w \<le> z & w \<noteq> z)"
+by (simp add: zless_def)
+
+instance int :: order
+proof qed
+ (assumption |
+ rule zle_refl zle_trans zle_anti_sym zless_le)+
+
+(* Axiom 'linorder_linear' of class 'linorder': *)
+lemma zle_linear: "(z::int) \<le> w | w \<le> z"
+apply (rule eq_Abs_Integ [of z])
+apply (rule eq_Abs_Integ [of w])
+apply (simp add: zle linorder_linear)
+done
+
+instance int :: plus_ac0
+proof qed (rule zadd_commute zadd_assoc zadd_0)+
+
+instance int :: linorder
+proof qed (rule zle_linear)
+
+
+lemmas zless_linear = linorder_less_linear [where 'a = int]
+
+
+lemma int_eq_0_conv [simp]: "(int n = 0) = (n = 0)"
+by (simp add: Zero_int_def)
(*This lemma allows direct proofs of other <-properties*)
lemma zless_iff_Suc_zadd:
"(w < z) = (\<exists>n. z = w + int(Suc n))"
-apply (unfold zless_def neg_def zdiff_def int_def)
-apply (rule_tac z = z in eq_Abs_Integ)
-apply (rule_tac z = w in eq_Abs_Integ, clarify)
-apply (simp add: zadd zminus)
+apply (rule eq_Abs_Integ [of z])
+apply (rule eq_Abs_Integ [of w])
+apply (simp add: linorder_not_le [where 'a = int, symmetric]
+ linorder_not_le [where 'a = nat]
+ zle int_def zdiff_def zadd zminus)
apply (safe dest!: less_imp_Suc_add)
apply (rule_tac x = k in exI)
apply (simp_all add: add_ac)
done
-lemma zless_zadd_Suc: "z < z + int (Suc n)"
-by (auto simp add: zless_iff_Suc_zadd zadd_assoc zadd_int)
-
-lemma zless_trans: "[| z1<z2; z2<z3 |] ==> z1 < (z3::int)"
-by (auto simp add: zless_iff_Suc_zadd zadd_assoc zadd_int)
-
-lemma zless_not_sym: "!!w::int. z<w ==> ~w<z"
-apply (safe dest!: zless_iff_Suc_zadd [THEN iffD1])
-apply (rule_tac z = z in eq_Abs_Integ, safe)
-apply (simp add: int_def zadd)
-done
-
-(* [| n<m; ~P ==> m<n |] ==> P *)
-lemmas zless_asym = zless_not_sym [THEN swap, standard]
-
-lemma zless_not_refl: "!!z::int. ~ z<z"
-apply (rule zless_asym [THEN notI])
-apply (assumption+)
-done
-
-(* z<z ==> R *)
-lemmas zless_irrefl = zless_not_refl [THEN notE, standard, elim!]
-
-
-(*"Less than" is a linear ordering*)
-lemma zless_linear:
- "z<w | z=w | w<(z::int)"
-apply (unfold zless_def neg_def zdiff_def)
-apply (rule_tac z = z in eq_Abs_Integ)
-apply (rule_tac z = w in eq_Abs_Integ, safe)
-apply (simp add: zadd zminus Image_iff Bex_def)
-apply (rule_tac m1 = "x+ya" and n1 = "xa+y" in less_linear [THEN disjE])
-apply (force simp add: add_ac)+
-done
-
-lemma int_neq_iff: "!!w::int. (w ~= z) = (w<z | z<w)"
-by (cut_tac zless_linear, blast)
-
-(*** eliminates ~= in premises ***)
-lemmas int_neqE = int_neq_iff [THEN iffD1, THEN disjE, standard]
-
-lemma int_eq_0_conv [simp]: "(int n = 0) = (n = 0)"
-by (simp add: Zero_int_def)
-
lemma zless_int [simp]: "(int m < int n) = (m<n)"
by (simp add: less_iff_Suc_add zless_iff_Suc_zadd zadd_int)
@@ -425,84 +413,553 @@
lemma int_0_neq_1 [simp]: "0 \<noteq> (1::int)"
by (simp only: Zero_int_def One_int_def One_nat_def int_int_eq)
-
-subsection{*Properties of the @{text "\<le>"} Relation*}
+lemma zle_int [simp]: "(int m \<le> int n) = (m\<le>n)"
+by (simp add: linorder_not_less [symmetric])
-lemma zle_int [simp]: "(int m <= int n) = (m<=n)"
-by (simp add: zle_def le_def)
+lemma zero_zle_int [simp]: "(0 \<le> int n)"
+by (simp add: Zero_int_def)
-lemma zero_zle_int [simp]: "(0 <= int n)"
+lemma int_le_0_conv [simp]: "(int n \<le> 0) = (n = 0)"
+by (simp add: Zero_int_def)
+
+lemma int_0 [simp]: "int 0 = (0::int)"
by (simp add: Zero_int_def)
-lemma int_le_0_conv [simp]: "(int n <= 0) = (n = 0)"
-by (simp add: Zero_int_def)
+lemma int_1 [simp]: "int 1 = 1"
+by (simp add: One_int_def)
+
+lemma int_Suc0_eq_1: "int (Suc 0) = 1"
+by (simp add: One_int_def One_nat_def)
+
+subsection{*Monotonicity results*}
+
+lemma zadd_left_mono: "i \<le> j ==> k + i \<le> k + (j::int)"
+apply (rule eq_Abs_Integ [of i])
+apply (rule eq_Abs_Integ [of j])
+apply (rule eq_Abs_Integ [of k])
+apply (simp add: zle zadd)
+done
+
+lemma zadd_strict_right_mono: "i < j ==> i + k < j + (k::int)"
+apply (rule eq_Abs_Integ [of i])
+apply (rule eq_Abs_Integ [of j])
+apply (rule eq_Abs_Integ [of k])
+apply (simp add: linorder_not_le [where 'a = int, symmetric]
+ linorder_not_le [where 'a = nat] zle zadd)
+done
+
+lemma zadd_zless_mono: "[| w'<w; z'\<le>z |] ==> w' + z' < w + (z::int)"
+by (rule order_less_le_trans [OF zadd_strict_right_mono zadd_left_mono])
+
+
+subsection{*Strict Monotonicity of Multiplication*}
+
+text{*strict, in 1st argument; proof is by induction on k>0*}
+lemma zmult_zless_mono2_lemma [rule_format]:
+ "i<j ==> 0<k --> int k * i < int k * j"
+apply (induct_tac "k", simp)
+apply (simp add: int_Suc)
+apply (case_tac "n=0")
+apply (simp_all add: zadd_zmult_distrib int_Suc0_eq_1 order_le_less)
+apply (simp add: zadd_zless_mono int_Suc0_eq_1 order_le_less)
+done
-lemma zle_imp_zless_or_eq: "z <= w ==> z < w | z=(w::int)"
-apply (unfold zle_def)
-apply (cut_tac zless_linear)
-apply (blast elim: zless_asym)
+lemma zero_le_imp_eq_int: "0 \<le> k ==> \<exists>n. k = int n"
+apply (rule eq_Abs_Integ [of k])
+apply (auto simp add: zle zadd int_def Zero_int_def)
+apply (rule_tac x="x-y" in exI, simp)
+done
+
+lemma zmult_zless_mono2: "[| i<j; (0::int) < k |] ==> k*i < k*j"
+apply (frule order_less_imp_le [THEN zero_le_imp_eq_int])
+apply (auto simp add: zmult_zless_mono2_lemma)
+done
+
+
+defs (overloaded)
+ zabs_def: "abs(i::int) == if i < 0 then -i else i"
+
+
+text{*The Integers Form an Ordered Ring*}
+instance int :: ordered_ring
+proof
+ fix i j k :: int
+ show "0 < (1::int)" by (rule int_0_less_1)
+ show "i \<le> j ==> k + i \<le> k + j" by (rule zadd_left_mono)
+ show "i < j ==> 0 < k ==> k * i < k * j" by (rule zmult_zless_mono2)
+ show "\<bar>i\<bar> = (if i < 0 then -i else i)" by (simp only: zabs_def)
+qed
+
+
+subsection{*Magnitide of an Integer, as a Natural Number: @{term nat}*}
+
+constdefs
+ nat :: "int => nat"
+ "nat(Z) == if Z<0 then 0 else (THE m. Z = int m)"
+
+lemma nat_int [simp]: "nat(int n) = n"
+by (unfold nat_def, auto)
+
+lemma nat_zero [simp]: "nat 0 = 0"
+apply (unfold Zero_int_def)
+apply (rule nat_int)
+done
+
+lemma nat_0_le [simp]: "0 \<le> z ==> int (nat z) = z"
+apply (rule eq_Abs_Integ [of z])
+apply (simp add: nat_def linorder_not_le [symmetric] zle int_def Zero_int_def)
+apply (subgoal_tac "(THE m. x = m + y) = x-y")
+apply (auto simp add: the_equality)
done
-lemma zless_or_eq_imp_zle: "z<w | z=w ==> z <= (w::int)"
-apply (unfold zle_def)
-apply (cut_tac zless_linear)
-apply (blast elim: zless_asym)
+lemma nat_le_0 [simp]: "z \<le> 0 ==> nat z = 0"
+by (simp add: nat_def order_less_le eq_commute [of 0])
+
+text{*An alternative condition is @{term "0 \<le> w"} *}
+lemma nat_mono_iff: "0 < z ==> (nat w < nat z) = (w < z)"
+apply (subst zless_int [symmetric])
+apply (simp add: order_le_less)
+apply (case_tac "w < 0")
+ apply (simp add: order_less_imp_le)
+ apply (blast intro: order_less_trans)
+apply (simp add: linorder_not_less)
+done
+
+lemma zless_nat_conj: "(nat w < nat z) = (0 < z & w < z)"
+apply (case_tac "0 < z")
+apply (auto simp add: nat_mono_iff linorder_not_less)
+done
+
+
+subsection{*Lemmas about the Function @{term int} and Orderings*}
+
+lemma negative_zless_0: "- (int (Suc n)) < 0"
+by (simp add: zless_def)
+
+lemma negative_zless [iff]: "- (int (Suc n)) < int m"
+by (rule negative_zless_0 [THEN order_less_le_trans], simp)
+
+lemma negative_zle_0: "- int n \<le> 0"
+by (simp add: minus_le_iff)
+
+lemma negative_zle [iff]: "- int n \<le> int m"
+by (rule order_trans [OF negative_zle_0 zero_zle_int])
+
+lemma not_zle_0_negative [simp]: "~ (0 \<le> - (int (Suc n)))"
+by (subst le_minus_iff, simp)
+
+lemma int_zle_neg: "(int n \<le> - int m) = (n = 0 & m = 0)"
+apply safe
+apply (drule_tac [2] le_minus_iff [THEN iffD1])
+apply (auto dest: zle_trans [OF _ negative_zle_0])
done
-lemma int_le_less: "(x <= (y::int)) = (x < y | x=y)"
-apply (rule iffI)
-apply (erule zle_imp_zless_or_eq)
-apply (erule zless_or_eq_imp_zle)
+lemma not_int_zless_negative [simp]: "~ (int n < - int m)"
+by (simp add: linorder_not_less)
+
+lemma negative_eq_positive [simp]: "(- int n = int m) = (n = 0 & m = 0)"
+by (force simp add: order_eq_iff [of "- int n"] int_zle_neg)
+
+lemma zle_iff_zadd: "(w \<le> z) = (\<exists>n. z = w + int n)"
+by (force intro: exI [of _ "0::nat"]
+ intro!: not_sym [THEN not0_implies_Suc]
+ simp add: zless_iff_Suc_zadd order_le_less)
+
+
+text{*This version is proved for all ordered rings, not just integers!
+ It is proved here because attribute @{text arith_split} is not available
+ in theory @{text Ring_and_Field}.
+ But is it really better than just rewriting with @{text abs_if}?*}
+lemma abs_split [arith_split]:
+ "P(abs(a::'a::ordered_ring)) = ((0 \<le> a --> P a) & (a < 0 --> P(-a)))"
+by (force dest: order_less_le_trans simp add: abs_if linorder_not_less)
+
+lemma abs_int_eq [simp]: "abs (int m) = int m"
+by (simp add: zabs_def)
+
+
+subsection{*Misc Results*}
+
+lemma nat_zminus_int [simp]: "nat(- (int n)) = 0"
+by (auto simp add: nat_def zero_reorient minus_less_iff)
+
+lemma zless_nat_eq_int_zless: "(m < nat z) = (int m < z)"
+apply (case_tac "0 \<le> z")
+apply (erule nat_0_le [THEN subst], simp)
+apply (simp add: linorder_not_le)
+apply (auto dest: order_less_trans simp add: order_less_imp_le)
done
-lemma zle_refl: "w <= (w::int)"
-by (simp add: int_le_less)
+
+
+subsection{*Monotonicity of Multiplication*}
+
+lemma zmult_zle_mono2: "[| i \<le> j; (0::int) \<le> k |] ==> k*i \<le> k*j"
+ by (rule Ring_and_Field.mult_left_mono)
+
+lemma zmult_zless_cancel2: "(m*k < n*k) = (((0::int) < k & m<n) | (k<0 & n<m))"
+ by (rule Ring_and_Field.mult_less_cancel_right)
+
+lemma zmult_zless_cancel1:
+ "(k*m < k*n) = (((0::int) < k & m<n) | (k < 0 & n<m))"
+ by (rule Ring_and_Field.mult_less_cancel_left)
-(* Axiom 'linorder_linear' of class 'linorder': *)
-lemma zle_linear: "(z::int) <= w | w <= z"
-apply (simp add: int_le_less)
-apply (cut_tac zless_linear, blast)
+lemma zmult_zle_cancel1:
+ "(k*m \<le> k*n) = (((0::int) < k --> m\<le>n) & (k < 0 --> n\<le>m))"
+ by (rule Ring_and_Field.mult_le_cancel_left)
+
+
+
+text{*A case theorem distinguishing non-negative and negative int*}
+
+lemma negD: "x<0 ==> \<exists>n. x = - (int (Suc n))"
+by (auto simp add: zless_iff_Suc_zadd
+ diff_eq_eq [symmetric] zdiff_def)
+
+lemma int_cases [cases type: int, case_names nonneg neg]:
+ "[|!! n. z = int n ==> P; !! n. z = - (int (Suc n)) ==> P |] ==> P"
+apply (case_tac "z < 0", blast dest!: negD)
+apply (simp add: linorder_not_less)
+apply (blast dest: nat_0_le [THEN sym])
done
-(* Axiom 'order_trans of class 'order': *)
-lemma zle_trans: "[| i <= j; j <= k |] ==> i <= (k::int)"
-apply (drule zle_imp_zless_or_eq)
-apply (drule zle_imp_zless_or_eq)
-apply (rule zless_or_eq_imp_zle)
-apply (blast intro: zless_trans)
+lemma int_induct [induct type: int, case_names nonneg neg]:
+ "[|!! n. P (int n); !!n. P (- (int (Suc n))) |] ==> P z"
+ by (cases z) auto
+
+
+subsection{*The Constants @{term neg} and @{term iszero}*}
+
+constdefs
+
+ neg :: "'a::ordered_ring => bool"
+ "neg(Z) == Z < 0"
+
+ (*For simplifying equalities*)
+ iszero :: "'a::semiring => bool"
+ "iszero z == z = (0)"
+
+
+lemma not_neg_int [simp]: "~ neg(int n)"
+by (simp add: neg_def)
+
+lemma neg_zminus_int [simp]: "neg(- (int (Suc n)))"
+by (simp add: neg_def neg_less_0_iff_less)
+
+lemmas neg_eq_less_0 = neg_def
+
+lemma not_neg_eq_ge_0: "(~neg x) = (0 \<le> x)"
+by (simp add: neg_def linorder_not_less)
+
+subsection{*To simplify inequalities when Numeral1 can get simplified to 1*}
+
+lemma not_neg_0: "~ neg 0"
+by (simp add: One_int_def neg_def)
+
+lemma not_neg_1: "~ neg 1"
+by (simp add: neg_def linorder_not_less zero_le_one)
+
+lemma iszero_0: "iszero 0"
+by (simp add: iszero_def)
+
+lemma not_iszero_1: "~ iszero 1"
+by (simp add: iszero_def eq_commute)
+
+lemma neg_nat: "neg z ==> nat z = 0"
+by (simp add: nat_def neg_def)
+
+lemma not_neg_nat: "~ neg z ==> int (nat z) = z"
+by (simp add: linorder_not_less neg_def)
+
+
+subsection{*Embedding of the Naturals into any Semiring: @{term of_nat}*}
+
+consts of_nat :: "nat => 'a::semiring"
+
+primrec
+ of_nat_0: "of_nat 0 = 0"
+ of_nat_Suc: "of_nat (Suc m) = of_nat m + 1"
+
+lemma of_nat_1 [simp]: "of_nat 1 = 1"
+by simp
+
+lemma of_nat_add [simp]: "of_nat (m+n) = of_nat m + of_nat n"
+apply (induct m)
+apply (simp_all add: add_ac)
+done
+
+lemma of_nat_mult [simp]: "of_nat (m*n) = of_nat m * of_nat n"
+apply (induct m)
+apply (simp_all add: mult_ac add_ac right_distrib)
+done
+
+lemma zero_le_imp_of_nat: "0 \<le> (of_nat m::'a::ordered_semiring)"
+apply (induct m, simp_all)
+apply (erule order_trans)
+apply (rule less_add_one [THEN order_less_imp_le])
done
-lemma zle_anti_sym: "[| z <= w; w <= z |] ==> z = (w::int)"
-apply (drule zle_imp_zless_or_eq)
-apply (drule zle_imp_zless_or_eq)
-apply (blast elim: zless_asym)
+lemma less_imp_of_nat_less:
+ "m < n ==> of_nat m < (of_nat n::'a::ordered_semiring)"
+apply (induct m n rule: diff_induct, simp_all)
+apply (insert add_le_less_mono [OF zero_le_imp_of_nat zero_less_one], force)
+done
+
+lemma of_nat_less_imp_less:
+ "of_nat m < (of_nat n::'a::ordered_semiring) ==> m < n"
+apply (induct m n rule: diff_induct, simp_all)
+apply (insert zero_le_imp_of_nat)
+apply (force simp add: linorder_not_less [symmetric])
done
-(* Axiom 'order_less_le' of class 'order': *)
-lemma int_less_le: "((w::int) < z) = (w <= z & w ~= z)"
-apply (simp add: zle_def int_neq_iff)
-apply (blast elim!: zless_asym)
+lemma of_nat_less_iff [simp]:
+ "(of_nat m < (of_nat n::'a::ordered_semiring)) = (m<n)"
+by (blast intro: of_nat_less_imp_less less_imp_of_nat_less )
+
+text{*Special cases where either operand is zero*}
+declare of_nat_less_iff [of 0, simplified, simp]
+declare of_nat_less_iff [of _ 0, simplified, simp]
+
+lemma of_nat_le_iff [simp]:
+ "(of_nat m \<le> (of_nat n::'a::ordered_semiring)) = (m \<le> n)"
+by (simp add: linorder_not_less [symmetric])
+
+text{*Special cases where either operand is zero*}
+declare of_nat_le_iff [of 0, simplified, simp]
+declare of_nat_le_iff [of _ 0, simplified, simp]
+
+lemma of_nat_eq_iff [simp]:
+ "(of_nat m = (of_nat n::'a::ordered_semiring)) = (m = n)"
+by (simp add: order_eq_iff)
+
+text{*Special cases where either operand is zero*}
+declare of_nat_eq_iff [of 0, simplified, simp]
+declare of_nat_eq_iff [of _ 0, simplified, simp]
+
+lemma of_nat_diff [simp]:
+ "n \<le> m ==> of_nat (m - n) = of_nat m - (of_nat n :: 'a::ring)"
+by (simp del: of_nat_add
+ add: compare_rls of_nat_add [symmetric] split add: nat_diff_split)
+
+
+subsection{*The Set of Natural Numbers*}
+
+constdefs
+ Nats :: "'a::semiring set"
+ "Nats == range of_nat"
+
+syntax (xsymbols) Nats :: "'a set" ("\<nat>")
+
+lemma of_nat_in_Nats [simp]: "of_nat n \<in> Nats"
+by (simp add: Nats_def)
+
+lemma Nats_0 [simp]: "0 \<in> Nats"
+apply (simp add: Nats_def)
+apply (rule range_eqI)
+apply (rule of_nat_0 [symmetric])
+done
+
+lemma Nats_1 [simp]: "1 \<in> Nats"
+apply (simp add: Nats_def)
+apply (rule range_eqI)
+apply (rule of_nat_1 [symmetric])
+done
+
+lemma Nats_add [simp]: "[|a \<in> Nats; b \<in> Nats|] ==> a+b \<in> Nats"
+apply (auto simp add: Nats_def)
+apply (rule range_eqI)
+apply (rule of_nat_add [symmetric])
+done
+
+lemma Nats_mult [simp]: "[|a \<in> Nats; b \<in> Nats|] ==> a*b \<in> Nats"
+apply (auto simp add: Nats_def)
+apply (rule range_eqI)
+apply (rule of_nat_mult [symmetric])
done
-instance int :: order
-proof qed (assumption | rule zle_refl zle_trans zle_anti_sym int_less_le)+
+text{*Agreement with the specific embedding for the integers*}
+lemma int_eq_of_nat: "int = (of_nat :: nat => int)"
+proof
+ fix n
+ show "int n = of_nat n" by (induct n, simp_all add: int_Suc add_ac)
+qed
+
+
+subsection{*Embedding of the Integers into any Ring: @{term of_int}*}
+
+constdefs
+ of_int :: "int => 'a::ring"
+ "of_int z ==
+ (THE a. \<exists>i j. (i,j) \<in> Rep_Integ z & a = (of_nat i) - (of_nat j))"
+
+
+lemma of_int: "of_int (Abs_Integ (intrel `` {(i,j)})) = of_nat i - of_nat j"
+apply (simp add: of_int_def)
+apply (rule the_equality, auto)
+apply (simp add: compare_rls add_ac of_nat_add [symmetric]
+ del: of_nat_add)
+done
+
+lemma of_int_0 [simp]: "of_int 0 = 0"
+by (simp add: of_int Zero_int_def int_def)
+
+lemma of_int_1 [simp]: "of_int 1 = 1"
+by (simp add: of_int One_int_def int_def)
+
+lemma of_int_add [simp]: "of_int (w+z) = of_int w + of_int z"
+apply (rule eq_Abs_Integ [of w])
+apply (rule eq_Abs_Integ [of z])
+apply (simp add: compare_rls of_int zadd)
+done
+
+lemma of_int_minus [simp]: "of_int (-z) = - (of_int z)"
+apply (rule eq_Abs_Integ [of z])
+apply (simp add: compare_rls of_int zminus)
+done
-instance int :: plus_ac0
-proof qed (rule zadd_commute zadd_assoc zadd_0)+
+lemma of_int_diff [simp]: "of_int (w-z) = of_int w - of_int z"
+by (simp add: diff_minus)
+
+lemma of_int_mult [simp]: "of_int (w*z) = of_int w * of_int z"
+apply (rule eq_Abs_Integ [of w])
+apply (rule eq_Abs_Integ [of z])
+apply (simp add: compare_rls of_int left_diff_distrib right_diff_distrib
+ zmult add_ac)
+done
+
+lemma of_int_le_iff [simp]:
+ "(of_int w \<le> (of_int z::'a::ordered_ring)) = (w \<le> z)"
+apply (rule eq_Abs_Integ [of w])
+apply (rule eq_Abs_Integ [of z])
+apply (simp add: compare_rls of_int zle zdiff_def zadd zminus
+ of_nat_add [symmetric] del: of_nat_add)
+done
+
+text{*Special cases where either operand is zero*}
+declare of_int_le_iff [of 0, simplified, simp]
+declare of_int_le_iff [of _ 0, simplified, simp]
-instance int :: linorder
-proof qed (rule zle_linear)
+lemma of_int_less_iff [simp]:
+ "(of_int w < (of_int z::'a::ordered_ring)) = (w < z)"
+by (simp add: linorder_not_le [symmetric])
+
+text{*Special cases where either operand is zero*}
+declare of_int_less_iff [of 0, simplified, simp]
+declare of_int_less_iff [of _ 0, simplified, simp]
+
+lemma of_int_eq_iff [simp]:
+ "(of_int w = (of_int z::'a::ordered_ring)) = (w = z)"
+by (simp add: order_eq_iff)
+
+text{*Special cases where either operand is zero*}
+declare of_int_eq_iff [of 0, simplified, simp]
+declare of_int_eq_iff [of _ 0, simplified, simp]
+
+
+subsection{*The Set of Integers*}
+
+constdefs
+ Ints :: "'a::ring set"
+ "Ints == range of_int"
-lemma zadd_left_cancel [simp]: "!!w::int. (z + w' = z + w) = (w' = w)"
- by (rule add_left_cancel)
+syntax (xsymbols)
+ Ints :: "'a set" ("\<int>")
+
+lemma Ints_0 [simp]: "0 \<in> Ints"
+apply (simp add: Ints_def)
+apply (rule range_eqI)
+apply (rule of_int_0 [symmetric])
+done
+
+lemma Ints_1 [simp]: "1 \<in> Ints"
+apply (simp add: Ints_def)
+apply (rule range_eqI)
+apply (rule of_int_1 [symmetric])
+done
+
+lemma Ints_add [simp]: "[|a \<in> Ints; b \<in> Ints|] ==> a+b \<in> Ints"
+apply (auto simp add: Ints_def)
+apply (rule range_eqI)
+apply (rule of_int_add [symmetric])
+done
+
+lemma Ints_minus [simp]: "a \<in> Ints ==> -a \<in> Ints"
+apply (auto simp add: Ints_def)
+apply (rule range_eqI)
+apply (rule of_int_minus [symmetric])
+done
+
+lemma Ints_diff [simp]: "[|a \<in> Ints; b \<in> Ints|] ==> a-b \<in> Ints"
+apply (auto simp add: Ints_def)
+apply (rule range_eqI)
+apply (rule of_int_diff [symmetric])
+done
+
+lemma Ints_mult [simp]: "[|a \<in> Ints; b \<in> Ints|] ==> a*b \<in> Ints"
+apply (auto simp add: Ints_def)
+apply (rule range_eqI)
+apply (rule of_int_mult [symmetric])
+done
+
+text{*Collapse nested embeddings*}
+lemma of_int_of_nat_eq [simp]: "of_int (of_nat n) = of_nat n"
+by (induct n, auto)
+
+lemma of_int_int_eq [simp]: "of_int (int n) = int n"
+by (simp add: int_eq_of_nat)
+lemma Ints_cases [case_names of_int, cases set: Ints]:
+ "q \<in> \<int> ==> (!!z. q = of_int z ==> C) ==> C"
+proof (unfold Ints_def)
+ assume "!!z. q = of_int z ==> C"
+ assume "q \<in> range of_int" thus C ..
+qed
+
+lemma Ints_induct [case_names of_int, induct set: Ints]:
+ "q \<in> \<int> ==> (!!z. P (of_int z)) ==> P q"
+ by (rule Ints_cases) auto
+
+
+
+(*Legacy ML bindings, but no longer the structure Int.*)
ML
{*
+val zabs_def = thm "zabs_def"
+val nat_def = thm "nat_def"
+
+val int_0 = thm "int_0";
+val int_1 = thm "int_1";
+val int_Suc0_eq_1 = thm "int_Suc0_eq_1";
+val neg_eq_less_0 = thm "neg_eq_less_0";
+val not_neg_eq_ge_0 = thm "not_neg_eq_ge_0";
+val not_neg_0 = thm "not_neg_0";
+val not_neg_1 = thm "not_neg_1";
+val iszero_0 = thm "iszero_0";
+val not_iszero_1 = thm "not_iszero_1";
+val int_0_less_1 = thm "int_0_less_1";
+val int_0_neq_1 = thm "int_0_neq_1";
+val negative_zless = thm "negative_zless";
+val negative_zle = thm "negative_zle";
+val not_zle_0_negative = thm "not_zle_0_negative";
+val not_int_zless_negative = thm "not_int_zless_negative";
+val negative_eq_positive = thm "negative_eq_positive";
+val zle_iff_zadd = thm "zle_iff_zadd";
+val abs_int_eq = thm "abs_int_eq";
+val abs_split = thm"abs_split";
+val nat_int = thm "nat_int";
+val nat_zminus_int = thm "nat_zminus_int";
+val nat_zero = thm "nat_zero";
+val not_neg_nat = thm "not_neg_nat";
+val neg_nat = thm "neg_nat";
+val zless_nat_eq_int_zless = thm "zless_nat_eq_int_zless";
+val nat_0_le = thm "nat_0_le";
+val nat_le_0 = thm "nat_le_0";
+val zless_nat_conj = thm "zless_nat_conj";
+val int_cases = thm "int_cases";
+
val int_def = thm "int_def";
-val neg_def = thm "neg_def";
-val iszero_def = thm "iszero_def";
val Zero_int_def = thm "Zero_int_def";
val One_int_def = thm "One_int_def";
val zadd_def = thm "zadd_def";
@@ -524,8 +981,6 @@
val zminus_zminus = thm "zminus_zminus";
val inj_zminus = thm "inj_zminus";
val zminus_0 = thm "zminus_0";
-val not_neg_int = thm "not_neg_int";
-val neg_zminus_int = thm "neg_zminus_int";
val zadd = thm "zadd";
val zminus_zadd_distrib = thm "zminus_zadd_distrib";
val zadd_commute = thm "zadd_commute";
@@ -545,8 +1000,6 @@
val zdiff0 = thm "zdiff0";
val zdiff0_right = thm "zdiff0_right";
val zdiff_self = thm "zdiff_self";
-val zadd_assoc_cong = thm "zadd_assoc_cong";
-val zadd_assoc_swap = thm "zadd_assoc_swap";
val zmult_congruent2 = thm "zmult_congruent2";
val zmult = thm "zmult";
val zmult_zminus = thm "zmult_zminus";
@@ -564,15 +1017,6 @@
val zmult_0_right = thm "zmult_0_right";
val zmult_1_right = thm "zmult_1_right";
val zless_iff_Suc_zadd = thm "zless_iff_Suc_zadd";
-val zless_zadd_Suc = thm "zless_zadd_Suc";
-val zless_trans = thm "zless_trans";
-val zless_not_sym = thm "zless_not_sym";
-val zless_asym = thm "zless_asym";
-val zless_not_refl = thm "zless_not_refl";
-val zless_irrefl = thm "zless_irrefl";
-val zless_linear = thm "zless_linear";
-val int_neq_iff = thm "int_neq_iff";
-val int_neqE = thm "int_neqE";
val int_int_eq = thm "int_int_eq";
val int_eq_0_conv = thm "int_eq_0_conv";
val zless_int = thm "zless_int";
@@ -581,15 +1025,48 @@
val zle_int = thm "zle_int";
val zero_zle_int = thm "zero_zle_int";
val int_le_0_conv = thm "int_le_0_conv";
-val zle_imp_zless_or_eq = thm "zle_imp_zless_or_eq";
-val zless_or_eq_imp_zle = thm "zless_or_eq_imp_zle";
-val int_le_less = thm "int_le_less";
val zle_refl = thm "zle_refl";
val zle_linear = thm "zle_linear";
val zle_trans = thm "zle_trans";
val zle_anti_sym = thm "zle_anti_sym";
-val int_less_le = thm "int_less_le";
-val zadd_left_cancel = thm "zadd_left_cancel";
+
+val Ints_def = thm "Ints_def";
+val Nats_def = thm "Nats_def";
+
+val of_nat_0 = thm "of_nat_0";
+val of_nat_Suc = thm "of_nat_Suc";
+val of_nat_1 = thm "of_nat_1";
+val of_nat_add = thm "of_nat_add";
+val of_nat_mult = thm "of_nat_mult";
+val zero_le_imp_of_nat = thm "zero_le_imp_of_nat";
+val less_imp_of_nat_less = thm "less_imp_of_nat_less";
+val of_nat_less_imp_less = thm "of_nat_less_imp_less";
+val of_nat_less_iff = thm "of_nat_less_iff";
+val of_nat_le_iff = thm "of_nat_le_iff";
+val of_nat_eq_iff = thm "of_nat_eq_iff";
+val Nats_0 = thm "Nats_0";
+val Nats_1 = thm "Nats_1";
+val Nats_add = thm "Nats_add";
+val Nats_mult = thm "Nats_mult";
+val of_int = thm "of_int";
+val of_int_0 = thm "of_int_0";
+val of_int_1 = thm "of_int_1";
+val of_int_add = thm "of_int_add";
+val of_int_minus = thm "of_int_minus";
+val of_int_diff = thm "of_int_diff";
+val of_int_mult = thm "of_int_mult";
+val of_int_le_iff = thm "of_int_le_iff";
+val of_int_less_iff = thm "of_int_less_iff";
+val of_int_eq_iff = thm "of_int_eq_iff";
+val Ints_0 = thm "Ints_0";
+val Ints_1 = thm "Ints_1";
+val Ints_add = thm "Ints_add";
+val Ints_minus = thm "Ints_minus";
+val Ints_diff = thm "Ints_diff";
+val Ints_mult = thm "Ints_mult";
+val of_int_of_nat_eq = thm"of_int_of_nat_eq";
+val Ints_cases = thm "Ints_cases";
+val Ints_induct = thm "Ints_induct";
*}
end
--- a/src/HOL/Integ/IntDiv.thy Thu Feb 05 10:45:28 2004 +0100
+++ b/src/HOL/Integ/IntDiv.thy Tue Feb 10 12:02:11 2004 +0100
@@ -531,7 +531,7 @@
prefer 2 apply simp
apply (simp (no_asm_simp) add: zadd_zmult_distrib2)
apply (subst zadd_commute, rule zadd_zless_mono, arith)
-apply (rule zmult_zle_mono1, auto)
+apply (rule mult_right_mono, auto)
done
lemma zdiv_mono2:
@@ -561,7 +561,7 @@
apply (simp add: zmult_zless_cancel1)
apply (simp add: zadd_zmult_distrib2)
apply (subgoal_tac "b*q' \<le> b'*q'")
- prefer 2 apply (simp add: zmult_zle_mono1_neg)
+ prefer 2 apply (simp add: mult_right_mono_neg)
apply (subgoal_tac "b'*q' < b + b*q")
apply arith
apply simp
@@ -702,8 +702,8 @@
apply (subgoal_tac "b * (c - q mod c) < r * 1")
apply (simp add: zdiff_zmult_distrib2)
apply (rule order_le_less_trans)
-apply (erule_tac [2] zmult_zless_mono1)
-apply (rule zmult_zle_mono2_neg)
+apply (erule_tac [2] mult_strict_right_mono)
+apply (rule mult_left_mono_neg)
apply (auto simp add: compare_rls zadd_commute [of 1]
add1_zle_eq pos_mod_bound)
done
@@ -724,7 +724,7 @@
apply (subgoal_tac "r * 1 < b * (c - q mod c) ")
apply (simp add: zdiff_zmult_distrib2)
apply (rule order_less_le_trans)
-apply (erule zmult_zless_mono1)
+apply (erule mult_strict_right_mono)
apply (rule_tac [2] zmult_zle_mono2)
apply (auto simp add: compare_rls zadd_commute [of 1]
add1_zle_eq pos_mod_bound)
@@ -1111,7 +1111,7 @@
apply (unfold dvd_def, auto)
apply (subgoal_tac "0 < n")
prefer 2
- apply (blast intro: zless_trans)
+ apply (blast intro: order_less_trans)
apply (simp add: zero_less_mult_iff)
apply (subgoal_tac "n * k < n * 1")
apply (drule zmult_zless_cancel1 [THEN iffD1], auto)
@@ -1150,7 +1150,7 @@
lemma dvd_zminus_iff [iff]: "(z dvd -w) = (z dvd (w::int))"
apply (auto simp add: dvd_def)
- apply (drule zminus_equation [THEN iffD1])
+ apply (drule minus_equation_iff [THEN iffD1])
apply (rule_tac [!] x = "-k" in exI, auto)
done
--- a/src/HOL/Integ/NatBin.thy Thu Feb 05 10:45:28 2004 +0100
+++ b/src/HOL/Integ/NatBin.thy Tue Feb 10 12:02:11 2004 +0100
@@ -80,7 +80,7 @@
(*"neg" is used in rewrite rules for binary comparisons*)
lemma int_nat_number_of:
"int (number_of v :: nat) =
- (if neg (number_of v) then 0
+ (if neg (number_of v :: int) then 0
else (number_of v :: int))"
by (simp del: nat_number_of
add: neg_nat nat_number_of_def not_neg_nat add_assoc)
@@ -96,14 +96,14 @@
lemma Suc_nat_number_of_add:
"Suc (number_of v + n) =
- (if neg (number_of v) then 1+n else number_of (bin_succ v) + n)"
+ (if neg (number_of v :: int) then 1+n else number_of (bin_succ v) + n)"
by (simp del: nat_number_of
add: nat_number_of_def neg_nat
Suc_nat_eq_nat_zadd1 number_of_succ)
lemma Suc_nat_number_of:
"Suc (number_of v) =
- (if neg (number_of v) then 1 else number_of (bin_succ v))"
+ (if neg (number_of v :: int) then 1 else number_of (bin_succ v))"
apply (cut_tac n = 0 in Suc_nat_number_of_add)
apply (simp cong del: if_weak_cong)
done
@@ -115,8 +115,8 @@
(*"neg" is used in rewrite rules for binary comparisons*)
lemma add_nat_number_of:
"(number_of v :: nat) + number_of v' =
- (if neg (number_of v) then number_of v'
- else if neg (number_of v') then number_of v
+ (if neg (number_of v :: int) then number_of v'
+ else if neg (number_of v' :: int) then number_of v
else number_of (bin_add v v'))"
by (force dest!: neg_nat
simp del: nat_number_of
@@ -138,7 +138,7 @@
lemma diff_nat_number_of:
"(number_of v :: nat) - number_of v' =
- (if neg (number_of v') then number_of v
+ (if neg (number_of v' :: int) then number_of v
else let d = number_of (bin_add v (bin_minus v')) in
if neg d then 0 else nat d)"
by (simp del: nat_number_of add: diff_nat_eq_if nat_number_of_def)
@@ -150,7 +150,7 @@
lemma mult_nat_number_of:
"(number_of v :: nat) * number_of v' =
- (if neg (number_of v) then 0 else number_of (bin_mult v v'))"
+ (if neg (number_of v :: int) then 0 else number_of (bin_mult v v'))"
by (force dest!: neg_nat
simp del: nat_number_of
simp add: nat_number_of_def nat_mult_distrib [symmetric])
@@ -162,7 +162,7 @@
lemma div_nat_number_of:
"(number_of v :: nat) div number_of v' =
- (if neg (number_of v) then 0
+ (if neg (number_of v :: int) then 0
else nat (number_of v div number_of v'))"
by (force dest!: neg_nat
simp del: nat_number_of
@@ -175,8 +175,8 @@
lemma mod_nat_number_of:
"(number_of v :: nat) mod number_of v' =
- (if neg (number_of v) then 0
- else if neg (number_of v') then number_of v
+ (if neg (number_of v :: int) then 0
+ else if neg (number_of v' :: int) then number_of v
else nat (number_of v mod number_of v'))"
by (force dest!: neg_nat
simp del: nat_number_of
@@ -242,9 +242,9 @@
(*"neg" is used in rewrite rules for binary comparisons*)
lemma eq_nat_number_of:
"((number_of v :: nat) = number_of v') =
- (if neg (number_of v) then (iszero (number_of v') | neg (number_of v'))
- else if neg (number_of v') then iszero (number_of v)
- else iszero (number_of (bin_add v (bin_minus v'))))"
+ (if neg (number_of v :: int) then (iszero (number_of v' :: int) | neg (number_of v' :: int))
+ else if neg (number_of v' :: int) then iszero (number_of v :: int)
+ else iszero (number_of (bin_add v (bin_minus v')) :: int))"
apply (simp only: simp_thms neg_nat not_neg_eq_ge_0 nat_number_of_def
eq_nat_nat_iff eq_number_of_eq nat_0 iszero_def
split add: split_if cong add: imp_cong)
@@ -259,8 +259,8 @@
(*"neg" is used in rewrite rules for binary comparisons*)
lemma less_nat_number_of:
"((number_of v :: nat) < number_of v') =
- (if neg (number_of v) then neg (number_of (bin_minus v'))
- else neg (number_of (bin_add v (bin_minus v'))))"
+ (if neg (number_of v :: int) then neg (number_of (bin_minus v') :: int)
+ else neg (number_of (bin_add v (bin_minus v')) :: int))"
apply (simp only: simp_thms neg_nat not_neg_eq_ge_0 nat_number_of_def
nat_less_eq_zless less_number_of_eq_neg zless_nat_eq_int_zless
cong add: imp_cong, simp)
@@ -397,24 +397,24 @@
lemma eq_number_of_0:
"(number_of v = (0::nat)) =
- (if neg (number_of v) then True else iszero (number_of v))"
+ (if neg (number_of v :: int) then True else iszero (number_of v :: int))"
apply (simp add: numeral_0_eq_0 [symmetric] iszero_0)
done
lemma eq_0_number_of:
"((0::nat) = number_of v) =
- (if neg (number_of v) then True else iszero (number_of v))"
+ (if neg (number_of v :: int) then True else iszero (number_of v :: int))"
apply (rule trans [OF eq_sym_conv eq_number_of_0])
done
lemma less_0_number_of:
- "((0::nat) < number_of v) = neg (number_of (bin_minus v))"
+ "((0::nat) < number_of v) = neg (number_of (bin_minus v) :: int)"
by (simp add: numeral_0_eq_0 [symmetric])
(*Simplification already handles n<0, n<=0 and 0<=n.*)
declare eq_number_of_0 [simp] eq_0_number_of [simp] less_0_number_of [simp]
-lemma neg_imp_number_of_eq_0: "neg (number_of v) ==> number_of v = (0::nat)"
+lemma neg_imp_number_of_eq_0: "neg (number_of v :: int) ==> number_of v = (0::nat)"
by (simp add: numeral_0_eq_0 [symmetric] iszero_0)
@@ -530,7 +530,7 @@
lemma power_nat_number_of:
"(number_of v :: nat) ^ n =
- (if neg (number_of v) then 0^n else nat ((number_of v :: int) ^ n))"
+ (if neg (number_of v :: int) then 0^n else nat ((number_of v :: int) ^ n))"
by (simp only: simp_thms neg_nat not_neg_eq_ge_0 nat_number_of_def nat_power_eq
split add: split_if cong: imp_cong)
@@ -605,7 +605,7 @@
lemma nat_number_of_BIT_True:
"number_of (w BIT True) =
- (if neg (number_of w) then 0
+ (if neg (number_of w :: int) then 0
else let n = number_of w in Suc (n + n))"
apply (simp only: nat_number_of_def Let_def split: split_if)
apply (intro conjI impI)
@@ -618,7 +618,7 @@
lemma nat_number_of_BIT_False:
"number_of (w BIT False) = (let n::nat = number_of w in n + n)"
apply (simp only: nat_number_of_def Let_def)
- apply (cases "neg (number_of w)")
+ apply (cases "neg (number_of w :: int)")
apply (simp add: neg_nat neg_number_of_BIT)
apply (rule int_int_eq [THEN iffD1])
apply (simp only: not_neg_nat neg_number_of_BIT int_Suc zadd_int [symmetric] simp_thms)
@@ -637,8 +637,8 @@
lemma nat_number_of_add_left:
"number_of v + (number_of v' + (k::nat)) =
- (if neg (number_of v) then number_of v' + k
- else if neg (number_of v') then number_of v + k
+ (if neg (number_of v :: int) then number_of v' + k
+ else if neg (number_of v' :: int) then number_of v + k
else number_of (bin_add v v') + k)"
apply simp
done
@@ -831,6 +831,8 @@
"uminus" :: "int => int" ("`~")
"op +" :: "int => int => int" ("(_ `+/ _)")
"op *" :: "int => int => int" ("(_ `*/ _)")
+ "op <" :: "int => int => bool" ("(_ </ _)")
+ "op <=" :: "int => int => bool" ("(_ <=/ _)")
"neg" ("(_ < 0)")
end
--- a/src/HOL/Integ/NatSimprocs.thy Thu Feb 05 10:45:28 2004 +0100
+++ b/src/HOL/Integ/NatSimprocs.thy Tue Feb 10 12:02:11 2004 +0100
@@ -20,7 +20,7 @@
(*Now just instantiating n to (number_of v) does the right simplification,
but with some redundant inequality tests.*)
lemma neg_number_of_bin_pred_iff_0:
- "neg (number_of (bin_pred v)) = (number_of v = (0::nat))"
+ "neg (number_of (bin_pred v)::int) = (number_of v = (0::nat))"
apply (subgoal_tac "neg (number_of (bin_pred v)) = (number_of v < Suc 0) ")
apply (simp only: less_Suc_eq_le le_0_eq)
apply (subst less_number_of_Suc, simp)
@@ -29,7 +29,7 @@
text{*No longer required as a simprule because of the @{text inverse_fold}
simproc*}
lemma Suc_diff_number_of:
- "neg (number_of (bin_minus v)) ==>
+ "neg (number_of (bin_minus v)::int) ==>
Suc m - (number_of v) = m - (number_of (bin_pred v))"
apply (subst Suc_diff_eq_diff_pred, simp, simp)
apply (force simp only: diff_nat_number_of less_0_number_of [symmetric]
--- a/src/HOL/Integ/Presburger.thy Thu Feb 05 10:45:28 2004 +0100
+++ b/src/HOL/Integ/Presburger.thy Tue Feb 10 12:02:11 2004 +0100
@@ -961,7 +961,7 @@
apply (case_tac "0 \<le> k")
apply rules
apply (simp add: linorder_not_le)
- apply (drule zmult_zless_mono2_neg [OF iffD2 [OF zero_less_int_conv]])
+ apply (drule mult_strict_left_mono_neg [OF iffD2 [OF zero_less_int_conv]])
apply assumption
apply (simp add: mult_ac)
done
--- a/src/HOL/Integ/int_arith1.ML Thu Feb 05 10:45:28 2004 +0100
+++ b/src/HOL/Integ/int_arith1.ML Tue Feb 10 12:02:11 2004 +0100
@@ -28,6 +28,11 @@
val bin_mult_Min = thm"bin_mult_Min";
val bin_mult_BIT = thm"bin_mult_BIT";
+val neg_def = thm "neg_def";
+val iszero_def = thm "iszero_def";
+val not_neg_int = thm "not_neg_int";
+val neg_zminus_int = thm "neg_zminus_int";
+
val zadd_ac = thms "Ring_and_Field.add_ac"
val zmult_ac = thms "Ring_and_Field.mult_ac"
val NCons_Pls_0 = thm"NCons_Pls_0";
--- a/src/HOL/Integ/int_factor_simprocs.ML Thu Feb 05 10:45:28 2004 +0100
+++ b/src/HOL/Integ/int_factor_simprocs.ML Tue Feb 10 12:02:11 2004 +0100
@@ -5,25 +5,11 @@
Factor cancellation simprocs for the integers.
-This file can't be combined with int_arith1,2 because it requires IntDiv.thy.
+This file can't be combined with int_arith1 because it requires IntDiv.thy.
*)
(** Factor cancellation theorems for "int" **)
-Goal "!!k::int. (k*m <= k*n) = ((0 < k --> m<=n) & (k < 0 --> n<=m))";
-by (stac zmult_zle_cancel1 1);
-by Auto_tac;
-qed "int_mult_le_cancel1";
-
-Goal "!!k::int. (k*m < k*n) = ((0 < k & m<n) | (k < 0 & n<m))";
-by (stac zmult_zless_cancel1 1);
-by Auto_tac;
-qed "int_mult_less_cancel1";
-
-Goal "!!k::int. (k*m = k*n) = (k = 0 | m=n)";
-by Auto_tac;
-qed "int_mult_eq_cancel1";
-
Goal "!!k::int. k~=0 ==> (k*m) div (k*n) = (m div n)";
by (stac zdiv_zmult_zmult1 1);
by Auto_tac;
@@ -34,6 +20,7 @@
by (simp_tac (simpset() addsimps [int_mult_div_cancel1]) 1);
qed "int_mult_div_cancel_disj";
+
local
open Int_Numeral_Simprocs
in
@@ -65,7 +52,7 @@
val prove_conv = Bin_Simprocs.prove_conv
val mk_bal = HOLogic.mk_eq
val dest_bal = HOLogic.dest_bin "op =" HOLogic.intT
- val cancel = int_mult_eq_cancel1 RS trans
+ val cancel = mult_cancel_left RS trans
val neg_exchanges = false
)
@@ -74,7 +61,7 @@
val prove_conv = Bin_Simprocs.prove_conv
val mk_bal = HOLogic.mk_binrel "op <"
val dest_bal = HOLogic.dest_bin "op <" HOLogic.intT
- val cancel = int_mult_less_cancel1 RS trans
+ val cancel = mult_less_cancel_left RS trans
val neg_exchanges = true
)
@@ -83,7 +70,7 @@
val prove_conv = Bin_Simprocs.prove_conv
val mk_bal = HOLogic.mk_binrel "op <="
val dest_bal = HOLogic.dest_bin "op <=" HOLogic.intT
- val cancel = int_mult_le_cancel1 RS trans
+ val cancel = mult_le_cancel_left RS trans
val neg_exchanges = true
)
@@ -179,7 +166,7 @@
val prove_conv = Bin_Simprocs.prove_conv
val mk_bal = HOLogic.mk_eq
val dest_bal = HOLogic.dest_bin "op =" HOLogic.intT
- val simplify_meta_eq = cancel_simplify_meta_eq int_mult_eq_cancel1
+ val simplify_meta_eq = cancel_simplify_meta_eq mult_cancel_left
);
structure DivideCancelFactor = ExtractCommonTermFun
--- a/src/HOL/IsaMakefile Thu Feb 05 10:45:28 2004 +0100
+++ b/src/HOL/IsaMakefile Tue Feb 10 12:02:11 2004 +0100
@@ -86,7 +86,7 @@
Hilbert_Choice.thy Hilbert_Choice_lemmas.ML HOL.ML \
HOL.thy HOL_lemmas.ML Inductive.thy Integ/Bin.thy \
Integ/cooper_dec.ML Integ/cooper_proof.ML \
- Integ/Equiv.thy Integ/Int.thy Integ/IntArith.thy Integ/IntDef.thy \
+ Integ/Equiv.thy Integ/IntArith.thy Integ/IntDef.thy \
Integ/IntDiv.thy Integ/NatBin.thy Integ/NatSimprocs.thy Integ/int_arith1.ML \
Integ/int_factor_simprocs.ML Integ/nat_simprocs.ML \
Integ/Presburger.thy Integ/presburger.ML Integ/qelim.ML \
--- a/src/HOL/Isar_examples/document/root.bib Thu Feb 05 10:45:28 2004 +0100
+++ b/src/HOL/Isar_examples/document/root.bib Tue Feb 10 12:02:11 2004 +0100
@@ -71,7 +71,7 @@
institution = CUCL,
year = 1996,
number = 394,
- note = {\url{http://www.ftp.cl.cam.ac.uk/ftp/papers/reports/}}
+ note = {\url{http://www.cl.cam.ac.uk/users/lcp/papers/Reports/mutil.pdf}}
}
@Proceedings{tphols98,
--- a/src/HOL/NumberTheory/IntPrimes.thy Thu Feb 05 10:45:28 2004 +0100
+++ b/src/HOL/NumberTheory/IntPrimes.thy Tue Feb 10 12:02:11 2004 +0100
@@ -338,7 +338,7 @@
a < m ==> 0 \<le> b ==> b < m ==> [a = b] (mod m) ==> a = b"
apply (unfold zcong_def dvd_def, auto)
apply (drule_tac f = "\<lambda>z. z mod m" in arg_cong)
- apply (cut_tac z = a and w = b in zless_linear, auto)
+ apply (cut_tac x = a and y = b in linorder_less_linear, auto)
apply (subgoal_tac [2] "(a - b) mod m = a - b")
apply (rule_tac [3] mod_pos_pos_trivial, auto)
apply (subgoal_tac "(m + (a - b)) mod m = m + (a - b)")
--- a/src/HOL/Presburger.thy Thu Feb 05 10:45:28 2004 +0100
+++ b/src/HOL/Presburger.thy Tue Feb 10 12:02:11 2004 +0100
@@ -961,7 +961,7 @@
apply (case_tac "0 \<le> k")
apply rules
apply (simp add: linorder_not_le)
- apply (drule zmult_zless_mono2_neg [OF iffD2 [OF zero_less_int_conv]])
+ apply (drule mult_strict_left_mono_neg [OF iffD2 [OF zero_less_int_conv]])
apply assumption
apply (simp add: mult_ac)
done
--- a/src/HOL/Real/PReal.thy Thu Feb 05 10:45:28 2004 +0100
+++ b/src/HOL/Real/PReal.thy Tue Feb 10 12:02:11 2004 +0100
@@ -700,7 +700,7 @@
assumes A: "A \<in> preal"
and "\<forall>x\<in>A. x + u \<in> A"
and "0 \<le> z"
- shows "\<exists>b\<in>A. b + (rat z) * u \<in> A"
+ shows "\<exists>b\<in>A. b + (of_int z) * u \<in> A"
proof (cases z rule: int_cases)
case (nonneg n)
show ?thesis
@@ -709,8 +709,8 @@
from preal_nonempty [OF A]
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: prems)
+ from this obtain b where "b \<in> A" "b + of_int (int k) * u \<in> A" ..
+ hence "b + of_int (int k)*u + u \<in> A" by (simp add: prems)
thus ?case by (force simp add: left_distrib add_ac prems)
qed
next
@@ -718,7 +718,6 @@
with prems show ?thesis by simp
qed
-
lemma Gleason9_34_contra:
assumes A: "A \<in> preal"
shows "[|\<forall>x\<in>A. x + u \<in> A; 0 < u; 0 < y; y \<notin> A|] ==> False"
@@ -736,10 +735,10 @@
have apos [simp]: "0 < a"
by (simp add: zero_less_Fract_iff [OF bpos, symmetric] ypos)
let ?k = "a*d"
- have frle: "Fract a b \<le> rat ?k * (Fract c d)"
+ have frle: "Fract a b \<le> Fract ?k 1 * (Fract c d)"
proof -
have "?thesis = ((a * d * b * d) \<le> c * b * (a * d * b * d))"
- by (simp add: rat_def mult_rat le_rat order_less_imp_not_eq2 mult_ac)
+ by (simp add: mult_rat le_rat order_less_imp_not_eq2 mult_ac)
moreover
have "(1 * (a * d * b * d)) \<le> c * b * (a * d * b * d)"
by (rule mult_mono,
@@ -751,11 +750,11 @@
have k: "0 \<le> ?k" by (simp add: order_less_imp_le zero_less_mult_iff)
from Gleason9_34_exists [OF A closed k]
obtain z where z: "z \<in> A"
- and mem: "z + rat ?k * Fract c d \<in> A" ..
- have less: "z + rat ?k * Fract c d < Fract a b"
+ and mem: "z + of_int ?k * Fract c d \<in> A" ..
+ have less: "z + of_int ?k * Fract c d < Fract a b"
by (rule not_in_preal_ub [OF A notin mem ypos])
have "0<z" by (rule preal_imp_pos [OF A z])
- with frle and less show False by arith
+ with frle and less show False by (simp add: Fract_of_int_eq)
qed
--- a/src/HOL/Real/RatArith.thy Thu Feb 05 10:45:28 2004 +0100
+++ b/src/HOL/Real/RatArith.thy Tue Feb 10 12:02:11 2004 +0100
@@ -13,15 +13,11 @@
instance rat :: number ..
-defs
+defs (overloaded)
rat_number_of_def:
- "number_of v == Fract (number_of v) 1"
+ "(number_of v :: rat) == of_int (number_of v)"
(*::bin=>rat ::bin=>int*)
-theorem number_of_rat: "number_of b = rat (number_of b)"
- by (simp add: rat_number_of_def rat_def)
-
-declare number_of_rat [symmetric, simp]
lemma rat_numeral_0_eq_0: "Numeral0 = (0::rat)"
by (simp add: rat_number_of_def zero_rat [symmetric])
@@ -33,25 +29,26 @@
subsection{*Arithmetic Operations On Numerals*}
lemma add_rat_number_of [simp]:
- "(number_of v :: rat) + number_of v' = number_of (bin_add v v')"
-by (simp add: rat_number_of_def add_rat)
+ "(number_of v :: rat) + number_of v' = number_of (bin_add v v')"
+by (simp only: rat_number_of_def of_int_add number_of_add)
lemma minus_rat_number_of [simp]:
"- (number_of w :: rat) = number_of (bin_minus w)"
-by (simp add: rat_number_of_def minus_rat)
+by (simp only: rat_number_of_def of_int_minus number_of_minus)
lemma diff_rat_number_of [simp]:
"(number_of v :: rat) - number_of w = number_of (bin_add v (bin_minus w))"
-by (simp add: rat_number_of_def diff_rat)
+by (simp only: add_rat_number_of minus_rat_number_of diff_minus)
lemma mult_rat_number_of [simp]:
"(number_of v :: rat) * number_of v' = number_of (bin_mult v v')"
-by (simp add: rat_number_of_def mult_rat)
+by (simp only: rat_number_of_def of_int_mult number_of_mult)
text{*Lemmas for specialist use, NOT as default simprules*}
lemma rat_mult_2: "2 * z = (z+z::rat)"
proof -
- have eq: "(2::rat) = 1 + 1" by (simp add: rat_numeral_1_eq_1 [symmetric])
+ have eq: "(2::rat) = 1 + 1"
+ by (simp del: rat_number_of_def add: rat_numeral_1_eq_1 [symmetric])
thus ?thesis by (simp add: eq left_distrib)
qed
@@ -63,20 +60,20 @@
lemma eq_rat_number_of [simp]:
"((number_of v :: rat) = number_of v') =
- iszero (number_of (bin_add v (bin_minus v')))"
-by (simp add: rat_number_of_def eq_rat)
+ iszero (number_of (bin_add v (bin_minus v')) :: int)"
+by (simp add: rat_number_of_def)
text{*@{term neg} is used in rewrite rules for binary comparisons*}
lemma less_rat_number_of [simp]:
"((number_of v :: rat) < number_of v') =
- neg (number_of (bin_add v (bin_minus v')))"
-by (simp add: rat_number_of_def less_rat)
+ neg (number_of (bin_add v (bin_minus v')) :: int)"
+by (simp add: rat_number_of_def)
text{*New versions of existing theorems involving 0, 1*}
lemma rat_minus_1_eq_m1 [simp]: "- 1 = (-1::rat)"
-by (simp add: rat_numeral_1_eq_1 [symmetric])
+by (simp del: rat_number_of_def add: rat_numeral_1_eq_1 [symmetric])
lemma rat_mult_minus1 [simp]: "-1 * z = -(z::rat)"
proof -
@@ -143,13 +140,15 @@
lemma abs_nat_number_of [simp]:
"abs (number_of v :: rat) =
- (if neg (number_of v) then number_of (bin_minus v)
+ (if neg (number_of v :: int) then number_of (bin_minus v)
else number_of v)"
-by (simp add: abs_if)
+by (simp add: abs_if)
lemma abs_minus_one [simp]: "abs (-1) = (1::rat)"
by (simp add: abs_if)
+declare rat_number_of_def [simp]
+
ML
{*
--- a/src/HOL/Real/Rational.thy Thu Feb 05 10:45:28 2004 +0100
+++ b/src/HOL/Real/Rational.thy Tue Feb 10 12:02:11 2004 +0100
@@ -465,11 +465,11 @@
theorem less_rat: "b \<noteq> 0 ==> d \<noteq> 0 ==>
(Fract a b < Fract c d) = ((a * d) * (b * d) < (c * b) * (b * d))"
- by (simp add: less_rat_def le_rat eq_rat int_less_le)
+ by (simp add: less_rat_def le_rat eq_rat order_less_le)
theorem abs_rat: "b \<noteq> 0 ==> \<bar>Fract a b\<bar> = Fract \<bar>a\<bar> \<bar>b\<bar>"
by (simp add: abs_rat_def minus_rat zero_rat less_rat eq_rat)
- (auto simp add: mult_less_0_iff zero_less_mult_iff int_le_less
+ (auto simp add: mult_less_0_iff zero_less_mult_iff order_le_less
split: abs_split)
@@ -619,7 +619,7 @@
proof -
let ?E = "e * f" and ?F = "f * f"
from neq gt have "0 < ?E"
- by (auto simp add: zero_rat less_rat le_rat int_less_le eq_rat)
+ by (auto simp add: zero_rat less_rat le_rat order_less_le eq_rat)
moreover from neq have "0 < ?F"
by (auto simp add: zero_less_mult_iff)
moreover from neq le have "(a * d) * (b * d) < (c * b) * (b * d)"
@@ -642,72 +642,6 @@
qed
-subsection {* Embedding integers: The Injection @{term rat} *}
-
-constdefs
- rat :: "int => rat" (* FIXME generalize int to any numeric subtype (?) *)
- "rat z == Fract z 1"
- int_set :: "rat set" ("\<int>") (* FIXME generalize rat to any numeric supertype (?) *)
- "\<int> == range rat"
-
-lemma int_set_cases [case_names rat, cases set: int_set]:
- "q \<in> \<int> ==> (!!z. q = rat z ==> C) ==> C"
-proof (unfold int_set_def)
- assume "!!z. q = rat z ==> C"
- assume "q \<in> range rat" thus C ..
-qed
-
-lemma int_set_induct [case_names rat, induct set: int_set]:
- "q \<in> \<int> ==> (!!z. P (rat z)) ==> P q"
- by (rule int_set_cases) auto
-
-lemma rat_of_int_zero [simp]: "rat (0::int) = (0::rat)"
-by (simp add: rat_def zero_rat [symmetric])
-
-lemma rat_of_int_one [simp]: "rat (1::int) = (1::rat)"
-by (simp add: rat_def one_rat [symmetric])
-
-lemma rat_of_int_add_distrib [simp]: "rat (x + y) = rat (x::int) + rat y"
-by (simp add: rat_def add_rat)
-
-lemma rat_of_int_minus_distrib [simp]: "rat (-x) = -rat (x::int)"
-by (simp add: rat_def minus_rat)
-
-lemma rat_of_int_diff_distrib [simp]: "rat (x - y) = rat (x::int) - rat y"
-by (simp add: rat_def diff_rat)
-
-lemma rat_of_int_mult_distrib [simp]: "rat (x * y) = rat (x::int) * rat y"
-by (simp add: rat_def mult_rat)
-
-lemma rat_inject [simp]: "(rat z = rat w) = (z = w)"
-proof
- assume "rat z = rat w"
- hence "Fract z 1 = Fract w 1" by (unfold rat_def)
- hence "\<lfloor>fract z 1\<rfloor> = \<lfloor>fract w 1\<rfloor>" ..
- thus "z = w" by auto
-next
- assume "z = w"
- thus "rat z = rat w" by simp
-qed
-
-
-lemma rat_of_int_zero_cancel [simp]: "(rat x = 0) = (x = 0)"
-proof -
- have "(rat x = 0) = (rat x = rat 0)" by simp
- also have "... = (x = 0)" by (rule rat_inject)
- finally show ?thesis .
-qed
-
-lemma rat_of_int_less_iff [simp]: "rat (x::int) < rat y = (x < y)"
-by (simp add: rat_def less_rat)
-
-lemma rat_of_int_le_iff [simp]: "(rat (x::int) \<le> rat y) = (x \<le> y)"
-by (simp add: linorder_not_less [symmetric])
-
-lemma zero_less_rat_of_int_iff [simp]: "(0 < rat y) = (0 < y)"
-by (insert rat_of_int_less_iff [of 0 y], simp)
-
-
subsection {* Various Other Results *}
lemma minus_rat_cancel [simp]: "b \<noteq> 0 ==> Fract (-a) (-b) = Fract a b"
@@ -733,4 +667,30 @@
"0 < b ==> (0 < Fract a b) = (0 < a)"
by (simp add: zero_rat less_rat order_less_imp_not_eq2 zero_less_mult_iff)
+lemma Fract_add_one: "n \<noteq> 0 ==> Fract (m + n) n = Fract m n + 1"
+apply (insert add_rat [of concl: m n 1 1])
+apply (simp add: one_rat [symmetric])
+done
+
+lemma Fract_of_nat_eq: "Fract (of_nat k) 1 = of_nat k"
+apply (induct k)
+apply (simp add: zero_rat)
+apply (simp add: Fract_add_one)
+done
+
+lemma Fract_of_int_eq: "Fract k 1 = of_int k"
+proof (cases k rule: int_cases)
+ case (nonneg n)
+ thus ?thesis by (simp add: int_eq_of_nat Fract_of_nat_eq)
+next
+ case (neg n)
+ hence "Fract k 1 = - (Fract (of_nat (Suc n)) 1)"
+ by (simp only: minus_rat int_eq_of_nat)
+ also have "... = - (of_nat (Suc n))"
+ by (simp only: Fract_of_nat_eq)
+ finally show ?thesis
+ by (simp add: only: prems int_eq_of_nat of_int_minus of_int_of_nat_eq)
+qed
+
+
end
--- a/src/HOL/Real/RealArith.thy Thu Feb 05 10:45:28 2004 +0100
+++ b/src/HOL/Real/RealArith.thy Tue Feb 10 12:02:11 2004 +0100
@@ -62,13 +62,13 @@
lemma eq_real_number_of [simp]:
"((number_of v :: real) = number_of v') =
- iszero (number_of (bin_add v (bin_minus v')))"
+ iszero (number_of (bin_add v (bin_minus v')) :: int)"
by (simp only: real_number_of_def real_of_int_inject eq_number_of_eq)
text{*@{term neg} is used in rewrite rules for binary comparisons*}
lemma less_real_number_of [simp]:
"((number_of v :: real) < number_of v') =
- neg (number_of (bin_add v (bin_minus v')))"
+ neg (number_of (bin_add v (bin_minus v')) :: int)"
by (simp only: real_number_of_def real_of_int_less_iff less_number_of_eq_neg)
@@ -134,12 +134,12 @@
have. *}
lemma real_of_nat_number_of [simp]:
"real (number_of v :: nat) =
- (if neg (number_of v) then 0
+ (if neg (number_of v :: int) then 0
else (number_of v :: real))"
proof cases
- assume "neg (number_of v)" thus ?thesis by simp
+ assume "neg (number_of v :: int)" thus ?thesis by simp
next
- assume neg: "~ neg (number_of v)"
+ assume neg: "~ neg (number_of v :: int)"
thus ?thesis
by (simp only: nat_number_of_def real_of_nat_real_of_int [OF neg], simp)
qed
@@ -222,7 +222,7 @@
lemma abs_nat_number_of [simp]:
"abs (number_of v :: real) =
- (if neg (number_of v) then number_of (bin_minus v)
+ (if neg (number_of v :: int) then number_of (bin_minus v)
else number_of v)"
by (simp add: real_abs_def bin_arith_simps minus_real_number_of
less_real_number_of real_of_int_le_iff)
--- a/src/HOL/Real/RealDef.thy Thu Feb 05 10:45:28 2004 +0100
+++ b/src/HOL/Real/RealDef.thy Tue Feb 10 12:02:11 2004 +0100
@@ -23,9 +23,8 @@
instance real :: inverse ..
consts
- (*Overloaded constants denoting the Nat and Real subsets of enclosing
+ (*Overloaded constant denoting the Real subset of enclosing
types such as hypreal and complex*)
- Nats :: "'a set"
Reals :: "'a set"
(*overloaded constant for injecting other types into "real"*)
@@ -85,16 +84,6 @@
syntax (xsymbols)
Reals :: "'a set" ("\<real>")
- Nats :: "'a set" ("\<nat>")
-
-
-defs (overloaded)
- real_of_int_def:
- "real z == Abs_REAL(\<Union>(i,j) \<in> Rep_Integ z. realrel ``
- {(preal_of_rat(rat(int(Suc i))),
- preal_of_rat(rat(int(Suc j))))})"
-
- real_of_nat_def: "real n == real (int n)"
subsection{*Proving that realrel is an equivalence relation*}
@@ -172,30 +161,6 @@
apply (simp add: Rep_REAL_inverse)
done
-lemma real_eq_iff:
- "[|(x1,y1) \<in> Rep_REAL w; (x2,y2) \<in> Rep_REAL z|]
- ==> (z = w) = (x1+y2 = x2+y1)"
-apply (insert quotient_eq_iff
- [OF equiv_realrel,
- of "Rep_REAL w" "Rep_REAL z" "(x1,y1)" "(x2,y2)"])
-apply (simp add: Rep_REAL [unfolded REAL_def] Rep_REAL_inject eq_commute)
-done
-
-lemma mem_REAL_imp_eq:
- "[|R \<in> REAL; (x1,y1) \<in> R; (x2,y2) \<in> R|] ==> x1+y2 = x2+y1"
-apply (auto simp add: REAL_def realrel_def quotient_def)
-apply (blast dest: preal_trans_lemma)
-done
-
-lemma Rep_REAL_cancel_right:
- "((x + z, y + z) \<in> Rep_REAL R) = ((x, y) \<in> Rep_REAL R)"
-apply (rule_tac z = R in eq_Abs_REAL, simp)
-apply (rename_tac u v)
-apply (subgoal_tac "(u + (y + z) = x + z + v) = ((u + y) + z = (x + v) + z)")
- prefer 2 apply (simp add: preal_add_ac)
-apply (simp add: preal_add_right_cancel_iff)
-done
-
subsection{*Congruence property for addition*}
@@ -218,21 +183,21 @@
done
lemma real_add_commute: "(z::real) + w = w + z"
-apply (rule_tac z = z in eq_Abs_REAL)
-apply (rule_tac z = w in eq_Abs_REAL)
+apply (rule eq_Abs_REAL [of z])
+apply (rule eq_Abs_REAL [of w])
apply (simp add: preal_add_ac real_add)
done
lemma real_add_assoc: "((z1::real) + z2) + z3 = z1 + (z2 + z3)"
-apply (rule_tac z = z1 in eq_Abs_REAL)
-apply (rule_tac z = z2 in eq_Abs_REAL)
-apply (rule_tac z = z3 in eq_Abs_REAL)
+apply (rule eq_Abs_REAL [of z1])
+apply (rule eq_Abs_REAL [of z2])
+apply (rule eq_Abs_REAL [of z3])
apply (simp add: real_add preal_add_assoc)
done
lemma real_add_zero_left: "(0::real) + z = z"
apply (unfold real_of_preal_def real_zero_def)
-apply (rule_tac z = z in eq_Abs_REAL)
+apply (rule eq_Abs_REAL [of z])
apply (simp add: real_add preal_add_ac)
done
@@ -263,7 +228,7 @@
lemma real_add_minus_left: "(-z) + z = (0::real)"
apply (unfold real_zero_def)
-apply (rule_tac z = z in eq_Abs_REAL)
+apply (rule eq_Abs_REAL [of z])
apply (simp add: real_minus real_add preal_add_commute)
done
@@ -283,7 +248,7 @@
lemma real_mult_congruent2:
"congruent2 realrel (%p1 p2.
- (%(x1,y1). (%(x2,y2). realrel``{(x1*x2 + y1*y2, x1*y2+x2*y1)}) p2) p1)"
+ (%(x1,y1). (%(x2,y2). realrel``{(x1*x2 + y1*y2, x1*y2+x2*y1)}) p2) p1)"
apply (rule equiv_realrel [THEN congruent2_commuteI], clarify)
apply (unfold split_def)
apply (simp add: preal_mult_commute preal_add_commute)
@@ -298,29 +263,29 @@
done
lemma real_mult_commute: "(z::real) * w = w * z"
-apply (rule_tac z = z in eq_Abs_REAL)
-apply (rule_tac z = w in eq_Abs_REAL)
+apply (rule eq_Abs_REAL [of z])
+apply (rule eq_Abs_REAL [of w])
apply (simp add: real_mult preal_add_ac preal_mult_ac)
done
lemma real_mult_assoc: "((z1::real) * z2) * z3 = z1 * (z2 * z3)"
-apply (rule_tac z = z1 in eq_Abs_REAL)
-apply (rule_tac z = z2 in eq_Abs_REAL)
-apply (rule_tac z = z3 in eq_Abs_REAL)
+apply (rule eq_Abs_REAL [of z1])
+apply (rule eq_Abs_REAL [of z2])
+apply (rule eq_Abs_REAL [of z3])
apply (simp add: preal_add_mult_distrib2 real_mult preal_add_ac preal_mult_ac)
done
lemma real_mult_1: "(1::real) * z = z"
apply (unfold real_one_def)
-apply (rule_tac z = z in eq_Abs_REAL)
+apply (rule eq_Abs_REAL [of z])
apply (simp add: real_mult preal_add_mult_distrib2 preal_mult_1_right
preal_mult_ac preal_add_ac)
done
lemma real_add_mult_distrib: "((z1::real) + z2) * w = (z1 * w) + (z2 * w)"
-apply (rule_tac z = z1 in eq_Abs_REAL)
-apply (rule_tac z = z2 in eq_Abs_REAL)
-apply (rule_tac z = w in eq_Abs_REAL)
+apply (rule eq_Abs_REAL [of z1])
+apply (rule eq_Abs_REAL [of z2])
+apply (rule eq_Abs_REAL [of w])
apply (simp add: preal_add_mult_distrib2 real_add real_mult preal_add_ac preal_mult_ac)
done
@@ -344,7 +309,7 @@
lemma real_mult_inverse_left_ex: "x \<noteq> 0 ==> \<exists>y. y*x = (1::real)"
apply (unfold real_zero_def real_one_def)
-apply (rule_tac z = x in eq_Abs_REAL)
+apply (rule eq_Abs_REAL [of x])
apply (cut_tac x = xa and y = y in linorder_less_linear)
apply (auto dest!: less_add_left_Ex simp add: real_zero_iff)
apply (rule_tac
@@ -420,63 +385,69 @@
subsection{*The @{text "\<le>"} Ordering*}
lemma real_le_refl: "w \<le> (w::real)"
-apply (rule_tac z = w in eq_Abs_REAL)
+apply (rule eq_Abs_REAL [of w])
apply (force simp add: real_le_def)
done
-lemma real_le_trans_lemma:
- assumes le1: "x1 + y2 \<le> x2 + y1"
- and le2: "u1 + v2 \<le> u2 + v1"
- and eq: "x2 + v1 = u1 + y2"
- shows "x1 + v2 + u1 + y2 \<le> u2 + u1 + y2 + (y1::preal)"
+text{*The arithmetic decision procedure is not set up for type preal.
+ This lemma is currently unused, but it could simplify the proofs of the
+ following two lemmas.*}
+lemma preal_eq_le_imp_le:
+ assumes eq: "a+b = c+d" and le: "c \<le> a"
+ shows "b \<le> (d::preal)"
+proof -
+ have "c+d \<le> a+d" by (simp add: prems preal_cancels)
+ hence "a+b \<le> a+d" by (simp add: prems)
+ thus "b \<le> d" by (simp add: preal_cancels)
+qed
+
+lemma real_le_lemma:
+ assumes l: "u1 + v2 \<le> u2 + v1"
+ and "x1 + v1 = u1 + y1"
+ and "x2 + v2 = u2 + y2"
+ shows "x1 + y2 \<le> x2 + (y1::preal)"
proof -
- have "x1 + v2 + u1 + y2 = (x1 + y2) + (u1 + v2)" by (simp add: preal_add_ac)
- also have "... \<le> (x2 + y1) + (u1 + v2)"
- by (simp add: prems preal_add_le_cancel_right)
- also have "... \<le> (x2 + y1) + (u2 + v1)"
+ have "(x1+v1) + (u2+y2) = (u1+y1) + (x2+v2)" by (simp add: prems)
+ hence "(x1+y2) + (u2+v1) = (x2+y1) + (u1+v2)" by (simp add: preal_add_ac)
+ also have "... \<le> (x2+y1) + (u2+v1)"
by (simp add: prems preal_add_le_cancel_left)
- also have "... = (x2 + v1) + (u2 + y1)" by (simp add: preal_add_ac)
- also have "... = (u1 + y2) + (u2 + y1)" by (simp add: prems)
- also have "... = u2 + u1 + y2 + y1" by (simp add: preal_add_ac)
- finally show ?thesis .
+ finally show ?thesis by (simp add: preal_add_le_cancel_right)
+qed
+
+lemma real_le:
+ "(Abs_REAL(realrel``{(x1,y1)}) \<le> Abs_REAL(realrel``{(x2,y2)})) =
+ (x1 + y2 \<le> x2 + y1)"
+apply (simp add: real_le_def)
+apply (auto intro: real_le_lemma);
+done
+
+lemma real_le_anti_sym: "[| z \<le> w; w \<le> z |] ==> z = (w::real)"
+apply (rule eq_Abs_REAL [of z])
+apply (rule eq_Abs_REAL [of w])
+apply (simp add: real_le order_antisym)
+done
+
+lemma real_trans_lemma:
+ assumes "x + v \<le> u + y"
+ and "u + v' \<le> u' + v"
+ and "x2 + v2 = u2 + y2"
+ shows "x + v' \<le> u' + (y::preal)"
+proof -
+ have "(x+v') + (u+v) = (x+v) + (u+v')" by (simp add: preal_add_ac)
+ also have "... \<le> (u+y) + (u+v')"
+ by (simp add: preal_add_le_cancel_right prems)
+ also have "... \<le> (u+y) + (u'+v)"
+ by (simp add: preal_add_le_cancel_left prems)
+ also have "... = (u'+y) + (u+v)" by (simp add: preal_add_ac)
+ finally show ?thesis by (simp add: preal_add_le_cancel_right)
qed
lemma real_le_trans: "[| i \<le> j; j \<le> k |] ==> i \<le> (k::real)"
-apply (simp add: real_le_def, clarify)
-apply (rename_tac x1 u1 y1 v1 x2 u2 y2 v2)
-apply (drule mem_REAL_imp_eq [OF Rep_REAL], assumption)
-apply (rule_tac x=x1 in exI)
-apply (rule_tac x=y1 in exI)
-apply (rule_tac x="u2 + (x2 + v1)" in exI)
-apply (rule_tac x="v2 + (u1 + y2)" in exI)
-apply (simp add: Rep_REAL_cancel_right preal_add_le_cancel_right
- preal_add_assoc [symmetric] real_le_trans_lemma)
-done
-
-lemma real_le_anti_sym_lemma:
- assumes le1: "x1 + y2 \<le> x2 + y1"
- and le2: "u1 + v2 \<le> u2 + v1"
- and eq1: "x1 + v2 = u2 + y1"
- and eq2: "x2 + v1 = u1 + y2"
- shows "x2 + y1 = x1 + (y2::preal)"
-proof (rule order_antisym)
- show "x1 + y2 \<le> x2 + y1" .
- have "(x2 + y1) + (u1+u2) = x2 + u1 + (u2 + y1)" by (simp add: preal_add_ac)
- also have "... = x2 + u1 + (x1 + v2)" by (simp add: prems)
- also have "... = (x2 + x1) + (u1 + v2)" by (simp add: preal_add_ac)
- also have "... \<le> (x2 + x1) + (u2 + v1)"
- by (simp add: preal_add_le_cancel_left)
- also have "... = (x1 + u2) + (x2 + v1)" by (simp add: preal_add_ac)
- also have "... = (x1 + u2) + (u1 + y2)" by (simp add: prems)
- also have "... = (x1 + y2) + (u1 + u2)" by (simp add: preal_add_ac)
- finally show "x2 + y1 \<le> x1 + y2" by (simp add: preal_add_le_cancel_right)
-qed
-
-lemma real_le_anti_sym: "[| z \<le> w; w \<le> z |] ==> z = (w::real)"
-apply (simp add: real_le_def, clarify)
-apply (rule real_eq_iff [THEN iffD2], assumption+)
-apply (drule mem_REAL_imp_eq [OF Rep_REAL], assumption)+
-apply (blast intro: real_le_anti_sym_lemma)
+apply (rule eq_Abs_REAL [of i])
+apply (rule eq_Abs_REAL [of j])
+apply (rule eq_Abs_REAL [of k])
+apply (simp add: real_le)
+apply (blast intro: real_trans_lemma)
done
(* Axiom 'order_less_le' of class 'order': *)
@@ -488,124 +459,50 @@
(assumption |
rule real_le_refl real_le_trans real_le_anti_sym real_less_le)+
-text{*Simplifies a strange formula that occurs quantified.*}
-lemma preal_strange_le_eq: "(x1 + x2 \<le> x2 + y1) = (x1 \<le> (y1::preal))"
-by (simp add: preal_add_commute [of x1] preal_add_le_cancel_left)
-
-text{*This is the nicest way to prove linearity*}
-lemma real_le_linear_0: "(z::real) \<le> 0 | 0 \<le> z"
-apply (rule_tac z = z in eq_Abs_REAL)
-apply (auto simp add: real_le_def real_zero_def preal_add_ac
- preal_cancels preal_strange_le_eq)
-apply (cut_tac x=x and y=y in linorder_linear, auto)
-done
-
-lemma real_minus_zero_le_iff: "(0 \<le> -R) = (R \<le> (0::real))"
-apply (rule_tac z = R in eq_Abs_REAL)
-apply (force simp add: real_le_def real_zero_def real_minus preal_add_ac
- preal_cancels preal_strange_le_eq)
+(* Axiom 'linorder_linear' of class 'linorder': *)
+lemma real_le_linear: "(z::real) \<le> w | w \<le> z"
+apply (rule eq_Abs_REAL [of z])
+apply (rule eq_Abs_REAL [of w])
+apply (auto simp add: real_le real_zero_def preal_add_ac preal_cancels)
+apply (cut_tac x="x+ya" and y="xa+y" in linorder_linear)
+apply (auto );
done
-lemma real_le_imp_diff_le_0: "x \<le> y ==> x-y \<le> (0::real)"
-apply (rule_tac z = x in eq_Abs_REAL)
-apply (rule_tac z = y in eq_Abs_REAL)
-apply (auto simp add: real_le_def real_zero_def real_diff_def real_minus
- real_add preal_add_ac preal_cancels preal_strange_le_eq)
-apply (rule exI)+
-apply (rule conjI, assumption)
-apply (subgoal_tac " x + (x2 + y1 + ya) = (x + y1) + (x2 + ya)")
- prefer 2 apply (simp (no_asm) only: preal_add_ac)
-apply (subgoal_tac "x1 + y2 + (xa + y) = (x1 + y) + (xa + y2)")
- prefer 2 apply (simp (no_asm) only: preal_add_ac)
-apply simp
-done
-
-lemma real_diff_le_0_imp_le: "x-y \<le> (0::real) ==> x \<le> y"
-apply (rule_tac z = x in eq_Abs_REAL)
-apply (rule_tac z = y in eq_Abs_REAL)
-apply (auto simp add: real_le_def real_zero_def real_diff_def real_minus
- real_add preal_add_ac preal_cancels preal_strange_le_eq)
-apply (rule exI)+
-apply (rule conjI, rule_tac [2] conjI)
- apply (rule_tac [2] refl)+
-apply (subgoal_tac "(x + ya) + (x1 + y1) \<le> (xa + y) + (x1 + y1)")
-apply (simp add: preal_cancels)
-apply (subgoal_tac "x1 + (x + (y1 + ya)) \<le> y1 + (x1 + (xa + y))")
- apply (simp add: preal_add_ac)
-apply (simp add: preal_cancels)
-done
-
-lemma real_le_eq_diff: "(x \<le> y) = (x-y \<le> (0::real))"
-by (blast intro!: real_diff_le_0_imp_le real_le_imp_diff_le_0)
-
-
-(* Axiom 'linorder_linear' of class 'linorder': *)
-lemma real_le_linear: "(z::real) \<le> w | w \<le> z"
-apply (insert real_le_linear_0 [of "z-w"])
-apply (auto simp add: real_le_eq_diff [of w] real_le_eq_diff [of z]
- real_minus_zero_le_iff [symmetric])
-done
instance real :: linorder
by (intro_classes, rule real_le_linear)
+lemma real_le_eq_diff: "(x \<le> y) = (x-y \<le> (0::real))"
+apply (rule eq_Abs_REAL [of x])
+apply (rule eq_Abs_REAL [of y])
+apply (auto simp add: real_le real_zero_def real_diff_def real_add real_minus
+ preal_add_ac)
+apply (simp_all add: preal_add_assoc [symmetric] preal_cancels)
+done
+
lemma real_add_left_mono: "x \<le> y ==> z + x \<le> z + (y::real)"
apply (auto simp add: real_le_eq_diff [of x] real_le_eq_diff [of "z+x"])
apply (subgoal_tac "z + x - (z + y) = (z + -z) + (x - y)")
prefer 2 apply (simp add: diff_minus add_ac, simp)
done
-
-lemma real_minus_zero_le_iff2: "(-R \<le> 0) = (0 \<le> (R::real))"
-apply (rule_tac z = R in eq_Abs_REAL)
-apply (force simp add: real_le_def real_zero_def real_minus preal_add_ac
- preal_cancels preal_strange_le_eq)
-done
-
-lemma real_minus_zero_less_iff: "(0 < -R) = (R < (0::real))"
-by (simp add: linorder_not_le [symmetric] real_minus_zero_le_iff2)
-
-lemma real_minus_zero_less_iff2: "(-R < 0) = ((0::real) < R)"
-by (simp add: linorder_not_le [symmetric] real_minus_zero_le_iff)
-
lemma real_sum_gt_zero_less: "(0 < S + (-W::real)) ==> (W < S)"
by (simp add: linorder_not_le [symmetric] real_le_eq_diff [of S] diff_minus)
-text{*Used a few times in Lim and Transcendental*}
lemma real_less_sum_gt_zero: "(W < S) ==> (0 < S + (-W::real))"
by (simp add: linorder_not_le [symmetric] real_le_eq_diff [of S] diff_minus)
-text{*Handles other strange cases that arise in these proofs.*}
-lemma forall_imp_less: "\<forall>u v. u \<le> v \<longrightarrow> x + v \<noteq> u + (y::preal) ==> y < x";
-apply (drule_tac x=x in spec)
-apply (drule_tac x=y in spec)
-apply (simp add: preal_add_commute linorder_not_le)
-done
-
-text{*The arithmetic decision procedure is not set up for type preal.*}
-lemma preal_eq_le_imp_le:
- assumes eq: "a+b = c+d" and le: "c \<le> a"
- shows "b \<le> (d::preal)"
-proof -
- have "c+d \<le> a+d" by (simp add: prems preal_cancels)
- hence "a+b \<le> a+d" by (simp add: prems)
- thus "b \<le> d" by (simp add: preal_cancels)
-qed
-
lemma real_mult_order: "[| 0 < x; 0 < y |] ==> (0::real) < x * y"
-apply (simp add: linorder_not_le [symmetric])
+apply (rule eq_Abs_REAL [of x])
+apply (rule eq_Abs_REAL [of y])
+apply (simp add: linorder_not_le [where 'a = real, symmetric]
+ linorder_not_le [where 'a = preal]
+ real_zero_def real_le real_mult)
--{*Reduce to the (simpler) @{text "\<le>"} relation *}
-apply (rule_tac z = x in eq_Abs_REAL)
-apply (rule_tac z = y in eq_Abs_REAL)
-apply (auto simp add: real_zero_def real_le_def real_mult preal_add_ac
- preal_cancels preal_strange_le_eq)
-apply (drule preal_eq_le_imp_le, assumption)
-apply (auto dest!: forall_imp_less less_add_left_Ex
+apply (auto dest!: less_add_left_Ex
simp add: preal_add_ac preal_mult_ac
- preal_add_mult_distrib preal_add_mult_distrib2)
-apply (insert preal_self_less_add_right)
-apply (simp add: linorder_not_le [symmetric])
+ preal_add_mult_distrib2 preal_cancels preal_self_less_add_right)
done
lemma real_mult_less_mono2: "[| (0::real) < z; x < y |] ==> z * x < z * y"
@@ -617,13 +514,11 @@
text{*lemma for proving @{term "0<(1::real)"}*}
lemma real_zero_le_one: "0 \<le> (1::real)"
-apply (auto simp add: real_zero_def real_one_def real_le_def preal_add_ac
- preal_cancels)
-apply (rule_tac x="preal_of_rat 1 + preal_of_rat 1" in exI)
-apply (rule_tac x="preal_of_rat 1" in exI)
-apply (auto simp add: preal_add_ac preal_self_less_add_left order_less_imp_le)
+apply (simp add: real_zero_def real_one_def real_le
+ preal_self_less_add_left order_less_imp_le)
done
+
subsection{*The Reals Form an Ordered Field*}
instance real :: ordered_field
@@ -658,7 +553,7 @@
lemma real_of_preal_trichotomy:
"\<exists>m. (x::real) = real_of_preal m | x = 0 | x = -(real_of_preal m)"
apply (unfold real_of_preal_def real_zero_def)
-apply (rule_tac z = x in eq_Abs_REAL)
+apply (rule eq_Abs_REAL [of x])
apply (auto simp add: real_minus preal_add_ac)
apply (cut_tac x = x and y = y in linorder_less_linear)
apply (auto dest!: less_add_left_Ex simp add: preal_add_assoc [symmetric])
@@ -824,126 +719,43 @@
subsection{*Embedding the Integers into the Reals*}
-lemma real_of_int_congruent:
- "congruent intrel (%p. (%(i,j). realrel ``
- {(preal_of_rat (rat (int(Suc i))), preal_of_rat (rat (int(Suc j))))}) p)"
-apply (simp add: congruent_def add_ac del: int_Suc, clarify)
-(*OPTION raised if only is changed to add?????????*)
-apply (simp only: add_Suc_right zero_less_rat_of_int_iff zadd_int
- preal_of_rat_add [symmetric] rat_of_int_add_distrib [symmetric], simp)
-done
-
-lemma real_of_int:
- "real (Abs_Integ (intrel `` {(i, j)})) =
- Abs_REAL(realrel ``
- {(preal_of_rat (rat (int(Suc i))),
- preal_of_rat (rat (int(Suc j))))})"
-apply (unfold real_of_int_def)
-apply (rule_tac f = Abs_REAL in arg_cong)
-apply (simp del: int_Suc
- add: realrel_in_real [THEN Abs_REAL_inverse]
- UN_equiv_class [OF equiv_intrel real_of_int_congruent])
-done
-
-lemma inj_real_of_int: "inj(real :: int => real)"
-apply (rule inj_onI)
-apply (rule_tac z = x in eq_Abs_Integ)
-apply (rule_tac z = y in eq_Abs_Integ, clarify)
-apply (simp del: int_Suc
- add: real_of_int zadd_int preal_of_rat_eq_iff
- preal_of_rat_add [symmetric] rat_of_int_add_distrib [symmetric])
-done
-
-lemma real_of_int_int_zero: "real (int 0) = 0"
-by (simp add: int_def real_zero_def real_of_int preal_add_commute)
+defs (overloaded)
+ real_of_nat_def: "real z == of_nat z"
+ real_of_int_def: "real z == of_int z"
lemma real_of_int_zero [simp]: "real (0::int) = 0"
-by (insert real_of_int_int_zero, simp)
+by (simp add: real_of_int_def)
lemma real_of_one [simp]: "real (1::int) = (1::real)"
-apply (subst int_1 [symmetric])
-apply (simp add: int_def real_one_def)
-apply (simp add: real_of_int preal_of_rat_add [symmetric])
-done
+by (simp add: real_of_int_def)
lemma real_of_int_add: "real (x::int) + real y = real (x + y)"
-apply (rule_tac z = x in eq_Abs_Integ)
-apply (rule_tac z = y in eq_Abs_Integ, clarify)
-apply (simp del: int_Suc
- add: pos_add_strict real_of_int real_add zadd
- preal_of_rat_add [symmetric], simp)
-done
+by (simp add: real_of_int_def)
declare real_of_int_add [symmetric, simp]
lemma real_of_int_minus: "-real (x::int) = real (-x)"
-apply (rule_tac z = x in eq_Abs_Integ)
-apply (auto simp add: real_of_int real_minus zminus)
-done
+by (simp add: real_of_int_def)
declare real_of_int_minus [symmetric, simp]
lemma real_of_int_diff: "real (x::int) - real y = real (x - y)"
-by (simp only: zdiff_def real_diff_def real_of_int_add real_of_int_minus)
+by (simp add: real_of_int_def)
declare real_of_int_diff [symmetric, simp]
lemma real_of_int_mult: "real (x::int) * real y = real (x * y)"
-apply (rule_tac z = x in eq_Abs_Integ)
-apply (rule_tac z = y in eq_Abs_Integ)
-apply (rename_tac a b c d)
-apply (simp del: int_Suc
- add: pos_add_strict mult_pos real_of_int real_mult zmult
- preal_of_rat_add [symmetric] preal_of_rat_mult [symmetric])
-apply (rule_tac f=preal_of_rat in arg_cong)
-apply (simp only: int_Suc right_distrib add_ac mult_ac zadd_int zmult_int
- rat_of_int_add_distrib [symmetric] rat_of_int_mult_distrib [symmetric]
- rat_inject)
-done
+by (simp add: real_of_int_def)
declare real_of_int_mult [symmetric, simp]
-lemma real_of_int_Suc: "real (int (Suc n)) = real (int n) + (1::real)"
-by (simp only: real_of_one [symmetric] zadd_int add_ac int_Suc real_of_int_add)
-
lemma real_of_int_zero_cancel [simp]: "(real x = 0) = (x = (0::int))"
-by (auto intro: inj_real_of_int [THEN injD])
-
-lemma zero_le_real_of_int: "0 \<le> real y ==> 0 \<le> (y::int)"
-apply (rule_tac z = y in eq_Abs_Integ)
-apply (simp add: real_le_def, clarify)
-apply (rename_tac a b c d)
-apply (simp del: int_Suc zdiff_def [symmetric]
- add: real_zero_def real_of_int zle_def zless_def zdiff_def zadd
- zminus neg_def preal_add_ac preal_cancels)
-apply (drule sym, drule preal_eq_le_imp_le, assumption)
-apply (simp del: int_Suc add: preal_of_rat_le_iff)
-done
-
-lemma real_of_int_le_cancel:
- assumes le: "real (x::int) \<le> real y"
- shows "x \<le> y"
-proof -
- have "real x - real x \<le> real y - real x" using le
- by (simp only: diff_minus add_le_cancel_right)
- hence "0 \<le> real y - real x" by simp
- hence "0 \<le> y - x" by (simp only: real_of_int_diff zero_le_real_of_int)
- hence "0 + x \<le> (y - x) + x" by (simp only: add_le_cancel_right)
- thus "x \<le> y" by simp
-qed
+by (simp add: real_of_int_def)
lemma real_of_int_inject [iff]: "(real (x::int) = real y) = (x = y)"
-by (blast dest!: inj_real_of_int [THEN injD])
-
-lemma real_of_int_less_cancel: "real (x::int) < real y ==> x < y"
-by (auto simp add: order_less_le real_of_int_le_cancel)
-
-lemma real_of_int_less_mono: "x < y ==> (real (x::int) < real y)"
-apply (simp add: linorder_not_le [symmetric])
-apply (auto dest!: real_of_int_less_cancel simp add: order_le_less)
-done
+by (simp add: real_of_int_def)
lemma real_of_int_less_iff [iff]: "(real (x::int) < real y) = (x < y)"
-by (blast dest: real_of_int_less_cancel intro: real_of_int_less_mono)
+by (simp add: real_of_int_def)
lemma real_of_int_le_iff [simp]: "(real (x::int) \<le> real y) = (x \<le> y)"
-by (simp add: linorder_not_less [symmetric])
+by (simp add: real_of_int_def)
subsection{*Embedding the Naturals into the Reals*}
@@ -955,73 +767,64 @@
by (simp add: real_of_nat_def)
lemma real_of_nat_add [simp]: "real (m + n) = real (m::nat) + real n"
-by (simp add: real_of_nat_def add_ac)
+by (simp add: real_of_nat_def)
(*Not for addsimps: often the LHS is used to represent a positive natural*)
lemma real_of_nat_Suc: "real (Suc n) = real n + (1::real)"
-by (simp add: real_of_nat_def add_ac)
+by (simp add: real_of_nat_def)
lemma real_of_nat_less_iff [iff]:
"(real (n::nat) < real m) = (n < m)"
by (simp add: real_of_nat_def)
lemma real_of_nat_le_iff [iff]: "(real (n::nat) \<le> real m) = (n \<le> m)"
-by (simp add: linorder_not_less [symmetric])
-
-lemma inj_real_of_nat: "inj (real :: nat => real)"
-apply (rule inj_onI)
-apply (simp add: real_of_nat_def)
-done
+by (simp add: real_of_nat_def)
lemma real_of_nat_ge_zero [iff]: "0 \<le> real (n::nat)"
-apply (insert real_of_int_le_iff [of 0 "int n"])
-apply (simp add: real_of_nat_def)
-done
+by (simp add: real_of_nat_def zero_le_imp_of_nat)
lemma real_of_nat_Suc_gt_zero: "0 < real (Suc n)"
-by (insert real_of_nat_less_iff [of 0 "Suc n"], simp)
+by (simp add: real_of_nat_def del: of_nat_Suc)
lemma real_of_nat_mult [simp]: "real (m * n) = real (m::nat) * real n"
-by (simp add: real_of_nat_def zmult_int [symmetric])
+by (simp add: real_of_nat_def)
lemma real_of_nat_inject [iff]: "(real (n::nat) = real m) = (n = m)"
-by (auto dest: inj_real_of_nat [THEN injD])
+by (simp add: real_of_nat_def)
lemma real_of_nat_zero_iff: "(real (n::nat) = 0) = (n = 0)"
- proof
- assume "real n = 0"
- have "real n = real (0::nat)" by simp
- then show "n = 0" by (simp only: real_of_nat_inject)
- next
- show "n = 0 \<Longrightarrow> real n = 0" by simp
- qed
+by (simp add: real_of_nat_def)
lemma real_of_nat_diff: "n \<le> m ==> real (m - n) = real (m::nat) - real n"
-by (simp add: real_of_nat_def zdiff_int [symmetric])
-
-lemma real_of_nat_neg_int [simp]: "neg z ==> real (nat z) = 0"
-by (simp add: neg_nat)
+by (simp add: add: real_of_nat_def)
lemma real_of_nat_gt_zero_cancel_iff [simp]: "(0 < real (n::nat)) = (0 < n)"
-by (rule real_of_nat_less_iff [THEN subst], auto)
+by (simp add: add: real_of_nat_def)
lemma real_of_nat_le_zero_cancel_iff [simp]: "(real (n::nat) \<le> 0) = (n = 0)"
-apply (rule real_of_nat_zero [THEN subst])
-apply (simp only: real_of_nat_le_iff, simp)
-done
-
+by (simp add: add: real_of_nat_def)
lemma not_real_of_nat_less_zero [simp]: "~ real (n::nat) < 0"
-by (simp add: linorder_not_less real_of_nat_ge_zero)
+by (simp add: add: real_of_nat_def)
lemma real_of_nat_ge_zero_cancel_iff [simp]: "(0 \<le> real (n::nat)) = (0 \<le> n)"
-by (simp add: linorder_not_less)
+by (simp add: add: real_of_nat_def)
lemma real_of_int_real_of_nat: "real (int n) = real n"
-by (simp add: real_of_nat_def)
+by (simp add: real_of_nat_def real_of_int_def int_eq_of_nat)
+
+
+text{*Still needed for binary arith*}
lemma real_of_nat_real_of_int: "~neg z ==> real (nat z) = real z"
-by (simp add: not_neg_eq_ge_0 real_of_nat_def)
+proof (simp add: not_neg_eq_ge_0 real_of_nat_def real_of_int_def)
+ assume "0 \<le> z"
+ hence eq: "of_nat (nat z) = z"
+ by (simp add: nat_0_le int_eq_of_nat[symmetric])
+ have "of_nat (nat z) = of_int (of_nat (nat z))" by simp
+ also have "... = of_int z" by (simp add: eq)
+ finally show "of_nat (nat z) = of_int z" .
+qed
ML
{*
@@ -1031,7 +834,6 @@
val real_diff_def = thm "real_diff_def";
val real_divide_def = thm "real_divide_def";
-val preal_trans_lemma = thm"preal_trans_lemma";
val realrel_iff = thm"realrel_iff";
val realrel_refl = thm"realrel_refl";
val equiv_realrel = thm"equiv_realrel";
@@ -1099,20 +901,14 @@
val real_inverse_unique = thm "real_inverse_unique";
val real_inverse_gt_one = thm "real_inverse_gt_one";
-val real_of_int = thm"real_of_int";
-val inj_real_of_int = thm"inj_real_of_int";
val real_of_int_zero = thm"real_of_int_zero";
val real_of_one = thm"real_of_one";
val real_of_int_add = thm"real_of_int_add";
val real_of_int_minus = thm"real_of_int_minus";
val real_of_int_diff = thm"real_of_int_diff";
val real_of_int_mult = thm"real_of_int_mult";
-val real_of_int_Suc = thm"real_of_int_Suc";
val real_of_int_real_of_nat = thm"real_of_int_real_of_nat";
-val real_of_nat_real_of_int = thm"real_of_nat_real_of_int";
-val real_of_int_less_cancel = thm"real_of_int_less_cancel";
val real_of_int_inject = thm"real_of_int_inject";
-val real_of_int_less_mono = thm"real_of_int_less_mono";
val real_of_int_less_iff = thm"real_of_int_less_iff";
val real_of_int_le_iff = thm"real_of_int_le_iff";
val real_of_nat_zero = thm "real_of_nat_zero";
@@ -1121,14 +917,12 @@
val real_of_nat_Suc = thm "real_of_nat_Suc";
val real_of_nat_less_iff = thm "real_of_nat_less_iff";
val real_of_nat_le_iff = thm "real_of_nat_le_iff";
-val inj_real_of_nat = thm "inj_real_of_nat";
val real_of_nat_ge_zero = thm "real_of_nat_ge_zero";
val real_of_nat_Suc_gt_zero = thm "real_of_nat_Suc_gt_zero";
val real_of_nat_mult = thm "real_of_nat_mult";
val real_of_nat_inject = thm "real_of_nat_inject";
val real_of_nat_diff = thm "real_of_nat_diff";
val real_of_nat_zero_iff = thm "real_of_nat_zero_iff";
-val real_of_nat_neg_int = thm "real_of_nat_neg_int";
val real_of_nat_gt_zero_cancel_iff = thm "real_of_nat_gt_zero_cancel_iff";
val real_of_nat_le_zero_cancel_iff = thm "real_of_nat_le_zero_cancel_iff";
val not_real_of_nat_less_zero = thm "not_real_of_nat_less_zero";
--- a/src/HOL/Real/rat_arith.ML Thu Feb 05 10:45:28 2004 +0100
+++ b/src/HOL/Real/rat_arith.ML Tue Feb 10 12:02:11 2004 +0100
@@ -19,18 +19,6 @@
val rat_number_of_def = thm "rat_number_of_def";
val diff_rat_def = thm "diff_rat_def";
-val rat_of_int_zero = thm "rat_of_int_zero";
-val rat_of_int_one = thm "rat_of_int_one";
-val rat_of_int_add_distrib = thm "rat_of_int_add_distrib";
-val rat_of_int_minus_distrib = thm "rat_of_int_minus_distrib";
-val rat_of_int_diff_distrib = thm "rat_of_int_diff_distrib";
-val rat_of_int_mult_distrib = thm "rat_of_int_mult_distrib";
-val rat_inject = thm "rat_inject";
-val rat_of_int_zero_cancel = thm "rat_of_int_zero_cancel";
-val rat_of_int_less_iff = thm "rat_of_int_less_iff";
-val rat_of_int_le_iff = thm "rat_of_int_le_iff";
-
-val number_of_rat = thm "number_of_rat";
val rat_numeral_0_eq_0 = thm "rat_numeral_0_eq_0";
val rat_numeral_1_eq_1 = thm "rat_numeral_1_eq_1";
val add_rat_number_of = thm "add_rat_number_of";
@@ -615,9 +603,8 @@
val simps = [True_implies_equals,
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];
+ of_int_0, of_int_1, of_int_add, of_int_minus, of_int_diff,
+ of_int_mult, of_int_of_nat_eq, rat_number_of_def];
in
@@ -625,8 +612,11 @@
"fast_rat_arith" ["(m::rat) < n","(m::rat) <= n", "(m::rat) = n"]
Fast_Arith.lin_arith_prover;
-val int_inj_thms = [rat_of_int_le_iff RS iffD2, rat_of_int_less_iff RS iffD2,
- rat_inject RS iffD2];
+val nat_inj_thms = [of_nat_le_iff RS iffD2, of_nat_less_iff RS iffD2,
+ of_nat_eq_iff RS iffD2];
+
+val int_inj_thms = [of_int_le_iff RS iffD2, of_int_less_iff RS iffD2,
+ of_int_eq_iff RS iffD2];
val rat_arith_setup =
[Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset} =>
@@ -637,7 +627,8 @@
simpset = simpset addsimps add_rules
addsimps simps
addsimprocs simprocs}),
- arith_inj_const ("Rational.rat", HOLogic.intT --> Rat_Numeral_Simprocs.ratT),
+ arith_inj_const("IntDef.of_nat", HOLogic.natT --> Rat_Numeral_Simprocs.ratT),
+ arith_inj_const("IntDef.of_int", HOLogic.intT --> Rat_Numeral_Simprocs.ratT),
arith_discrete ("Rational.rat",false),
Simplifier.change_simpset_of (op addsimprocs) [fast_rat_arith_simproc]];
--- a/src/HOL/UNITY/Simple/Lift.thy Thu Feb 05 10:45:28 2004 +0100
+++ b/src/HOL/UNITY/Simple/Lift.thy Tue Feb 10 12:02:11 2004 +0100
@@ -215,13 +215,13 @@
lemma moving_up: "Lift \<in> Always moving_up"
apply (rule AlwaysI, force)
apply (unfold Lift_def, constrains)
-apply (auto dest: zle_imp_zless_or_eq simp add: add1_zle_eq)
+apply (auto dest: order_le_imp_less_or_eq simp add: add1_zle_eq)
done
lemma moving_down: "Lift \<in> Always moving_down"
apply (rule AlwaysI, force)
apply (unfold Lift_def, constrains)
-apply (blast dest: zle_imp_zless_or_eq)
+apply (blast dest: order_le_imp_less_or_eq)
done
lemma bounded: "Lift \<in> Always bounded"
@@ -290,7 +290,7 @@
"Lift \<in> (Req n \<inter> closed - (atFloor n - queueing))
LeadsTo ((closed \<inter> goingup \<inter> Req n) \<union>
(closed \<inter> goingdown \<inter> Req n))"
-by (auto intro!: subset_imp_LeadsTo elim!: int_neqE)
+by (auto intro!: subset_imp_LeadsTo simp add: linorder_neq_iff)
(*lift_2*)
lemma (in Floor) lift_2: "Lift \<in> (Req n \<inter> closed - (atFloor n - queueing))
--- a/src/HOL/ex/BinEx.thy Thu Feb 05 10:45:28 2004 +0100
+++ b/src/HOL/ex/BinEx.thy Tue Feb 10 12:02:11 2004 +0100
@@ -470,7 +470,7 @@
apply assumption
apply (simp add: normal_Pls_eq_0)
apply (simp only: number_of_minus zminus_0 iszero_def
- zminus_equation [of _ "0"])
+ minus_equation_iff [of _ "0"])
apply (simp add: eq_commute)
done