1.1 --- a/src/HOL/Complex/CStar.ML Thu Feb 05 10:45:28 2004 +0100
1.2 +++ b/src/HOL/Complex/CStar.ML Tue Feb 10 12:02:11 2004 +0100
1.3 @@ -404,10 +404,9 @@
1.4 Goal "( *fcNat* (%n. z ^ n)) N = (hcomplex_of_complex z) hcpow N";
1.5 *)
1.6
1.7 -Goalw [hypnat_of_nat_def]
1.8 - "( *fc* (%z. z ^ n)) Z = Z hcpow hypnat_of_nat n";
1.9 +Goal "( *fc* (%z. z ^ n)) Z = Z hcpow hypnat_of_nat n";
1.10 by (res_inst_tac [("z","Z")] eq_Abs_hcomplex 1);
1.11 -by (auto_tac (claset(), simpset() addsimps [hcpow,starfunC]));
1.12 +by (auto_tac (claset(), simpset() addsimps [hcpow,starfunC,hypnat_of_nat_eq]));
1.13 qed "starfunC_hcpow";
1.14
1.15 Goal "( *fc* (%h. f (x + h))) xa = ( *fc* f) (hcomplex_of_complex x + xa)";
2.1 --- a/src/HOL/Complex/ComplexBin.ML Thu Feb 05 10:45:28 2004 +0100
2.2 +++ b/src/HOL/Complex/ComplexBin.ML Tue Feb 10 12:02:11 2004 +0100
2.3 @@ -70,7 +70,7 @@
2.4 (** Equals (=) **)
2.5
2.6 Goal "((number_of v :: complex) = number_of v') = \
2.7 -\ iszero (number_of (bin_add v (bin_minus v')))";
2.8 +\ iszero (number_of (bin_add v (bin_minus v')) :: int)";
2.9 by (simp_tac
2.10 (HOL_ss addsimps [complex_number_of_def,
2.11 complex_of_real_eq_iff, eq_real_number_of]) 1);
3.1 --- a/src/HOL/Complex/NSComplexBin.ML Thu Feb 05 10:45:28 2004 +0100
3.2 +++ b/src/HOL/Complex/NSComplexBin.ML Tue Feb 10 12:02:11 2004 +0100
3.3 @@ -100,7 +100,7 @@
3.4 (** Equals (=) **)
3.5
3.6 Goal "((number_of v :: hcomplex) = number_of v') = \
3.7 -\ iszero (number_of (bin_add v (bin_minus v')))";
3.8 +\ iszero (number_of (bin_add v (bin_minus v')) :: int)";
3.9 by (simp_tac
3.10 (HOL_ss addsimps [hcomplex_number_of_def,
3.11 hcomplex_of_complex_eq_iff, eq_complex_number_of]) 1);
4.1 --- a/src/HOL/Complex/NSInduct.ML Thu Feb 05 10:45:28 2004 +0100
4.2 +++ b/src/HOL/Complex/NSInduct.ML Tue Feb 10 12:02:11 2004 +0100
4.3 @@ -11,8 +11,8 @@
4.4 by (Ultra_tac 1);
4.5 qed "starPNat";
4.6
4.7 -Goalw [hypnat_of_nat_def] "( *pNat* P) (hypnat_of_nat n) = P n";
4.8 -by (auto_tac (claset(),simpset() addsimps [starPNat]));
4.9 +Goal "( *pNat* P) (hypnat_of_nat n) = P n";
4.10 +by (auto_tac (claset(),simpset() addsimps [starPNat, hypnat_of_nat_eq]));
4.11 qed "starPNat_hypnat_of_nat";
4.12 Addsimps [starPNat_hypnat_of_nat];
4.13
4.14 @@ -27,7 +27,7 @@
4.15 by (dres_inst_tac [("x","hypnat_of_nat n")] spec 1);
4.16 by (rtac ccontr 1);
4.17 by (auto_tac (claset(),simpset() addsimps [starPNat,
4.18 - hypnat_of_nat_def,hypnat_add]));
4.19 + hypnat_of_nat_eq,hypnat_add]));
4.20 qed "hypnat_induct_obj";
4.21
4.22 Goal
5.1 --- a/src/HOL/Complex/ex/NSPrimes.ML Thu Feb 05 10:45:28 2004 +0100
5.2 +++ b/src/HOL/Complex/ex/NSPrimes.ML Tue Feb 10 12:02:11 2004 +0100
5.3 @@ -175,7 +175,7 @@
5.4 (* behaves as expected! *)
5.5 Goal "( *sNat* insert x A) = insert (hypnat_of_nat x) ( *sNat* A)";
5.6 by (auto_tac (claset(),simpset() addsimps [starsetNat_def,
5.7 - hypnat_of_nat_def]));
5.8 + hypnat_of_nat_eq]));
5.9 by (ALLGOALS(res_inst_tac [("z","xa")] eq_Abs_hypnat));
5.10 by Auto_tac;
5.11 by (TRYALL(dtac bspec));
5.12 @@ -251,9 +251,8 @@
5.13 by Auto_tac;
5.14 qed "lemma_infinite_set_singleton";
5.15
5.16 -Goalw [SHNat_def,hypnat_of_nat_def]
5.17 - "inj f ==> Abs_hypnat(hypnatrel `` {f}) ~: Nats";
5.18 -by Auto_tac;
5.19 +Goal "inj f ==> Abs_hypnat(hypnatrel `` {f}) ~: Nats";
5.20 +by (auto_tac (claset(), simpset() addsimps [SHNat_eq,hypnat_of_nat_eq]));
5.21 by (subgoal_tac "ALL m n. m ~= n --> f n ~= f m" 1);
5.22 by Auto_tac;
5.23 by (dtac injD 2);
5.24 @@ -357,7 +356,7 @@
5.25 by Auto_tac;
5.26 by (dtac inj_fun_not_hypnat_in_SHNat 1);
5.27 by (dtac range_subset_mem_starsetNat 1);
5.28 -by (auto_tac (claset(),simpset() addsimps [SHNat_def]));
5.29 +by (auto_tac (claset(),simpset() addsimps [SHNat_eq]));
5.30 qed "hypnat_infinite_has_nonstandard";
5.31
5.32 Goal "*sNat* A = hypnat_of_nat ` A ==> finite A";
5.33 @@ -385,7 +384,7 @@
5.34 Goal "~ (ALL n:- {0}. hypnat_of_nat n hdvd 1)";
5.35 by Auto_tac;
5.36 by (res_inst_tac [("x","2")] bexI 1);
5.37 -by (auto_tac (claset(),simpset() addsimps [hypnat_of_nat_def,
5.38 +by (auto_tac (claset(),simpset() addsimps [hypnat_of_nat_eq,
5.39 hypnat_one_def,hdvd,dvd_def]));
5.40 val lemma_not_dvd_hypnat_one = result();
5.41 Addsimps [lemma_not_dvd_hypnat_one];
5.42 @@ -417,9 +416,9 @@
5.43 qed "zero_not_prime";
5.44 Addsimps [zero_not_prime];
5.45
5.46 -Goalw [starprime_def,starsetNat_def,hypnat_of_nat_def]
5.47 - "hypnat_of_nat 0 ~: starprime";
5.48 -by (auto_tac (claset() addSIs [bexI],simpset()));
5.49 +Goal "hypnat_of_nat 0 ~: starprime";
5.50 +by (auto_tac (claset() addSIs [bexI],
5.51 + simpset() addsimps [starprime_def,starsetNat_def,hypnat_of_nat_eq]));
5.52 qed "hypnat_of_nat_zero_not_prime";
5.53 Addsimps [hypnat_of_nat_zero_not_prime];
5.54
5.55 @@ -443,9 +442,9 @@
5.56 qed "one_not_prime2";
5.57 Addsimps [one_not_prime2];
5.58
5.59 -Goalw [starprime_def,starsetNat_def,hypnat_of_nat_def]
5.60 - "hypnat_of_nat 1 ~: starprime";
5.61 -by (auto_tac (claset() addSIs [bexI],simpset()));
5.62 +Goal "hypnat_of_nat 1 ~: starprime";
5.63 +by (auto_tac (claset() addSIs [bexI],
5.64 + simpset() addsimps [starprime_def,starsetNat_def,hypnat_of_nat_eq]));
5.65 qed "hypnat_of_nat_one_not_prime";
5.66 Addsimps [hypnat_of_nat_one_not_prime];
5.67
6.1 --- a/src/HOL/Hyperreal/HSeries.ML Thu Feb 05 10:45:28 2004 +0100
6.2 +++ b/src/HOL/Hyperreal/HSeries.ML Tue Feb 10 12:02:11 2004 +0100
6.3 @@ -5,6 +5,8 @@
6.4 for hyperreals
6.5 *)
6.6
6.7 +val hypreal_of_nat_eq = thm"hypreal_of_nat_eq";
6.8 +
6.9 Goalw [sumhr_def]
6.10 "sumhr(M,N,f) = \
6.11 \ Abs_hypreal(UN X:Rep_hypnat(M). UN Y: Rep_hypnat(N). \
6.12 @@ -125,12 +127,11 @@
6.13 qed "sumhr_hrabs";
6.14
6.15 (* other general version also needed *)
6.16 -Goalw [hypnat_of_nat_def]
6.17 - "(ALL r. m <= r & r < n --> f r = g r) --> \
6.18 +Goal "(ALL r. m <= r & r < n --> f r = g r) --> \
6.19 \ sumhr(hypnat_of_nat m, hypnat_of_nat n, f) = \
6.20 \ sumhr(hypnat_of_nat m, hypnat_of_nat n, g)";
6.21 by (Step_tac 1 THEN dtac sumr_fun_eq 1);
6.22 -by (auto_tac (claset(), simpset() addsimps [sumhr]));
6.23 +by (auto_tac (claset(), simpset() addsimps [sumhr, hypnat_of_nat_eq]));
6.24 qed "sumhr_fun_hypnat_eq";
6.25
6.26 Goalw [hypnat_zero_def,hypreal_of_real_def]
6.27 @@ -163,12 +164,11 @@
6.28 by (auto_tac (claset(), simpset() addsimps [sumhr, hypreal_minus,sumr_minus]));
6.29 qed "sumhr_minus";
6.30
6.31 -Goalw [hypnat_of_nat_def]
6.32 - "sumhr(m+hypnat_of_nat k,n+hypnat_of_nat k,f) = sumhr(m,n,%i. f(i + k))";
6.33 +Goal "sumhr(m+hypnat_of_nat k,n+hypnat_of_nat k,f) = sumhr(m,n,%i. f(i + k))";
6.34 by (res_inst_tac [("z","m")] eq_Abs_hypnat 1);
6.35 by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
6.36 by (auto_tac (claset(),
6.37 - simpset() addsimps [sumhr, hypnat_add,sumr_shift_bounds]));
6.38 + simpset() addsimps [sumhr, hypnat_add,sumr_shift_bounds, hypnat_of_nat_eq]));
6.39 qed "sumhr_shift_bounds";
6.40
6.41 (*------------------------------------------------------------------
6.42 @@ -196,12 +196,11 @@
6.43 qed "sumhr_minus_one_realpow_zero";
6.44 Addsimps [sumhr_minus_one_realpow_zero];
6.45
6.46 -Goalw [hypnat_of_nat_def,hypreal_of_real_def]
6.47 - "(ALL n. m <= Suc n --> f n = r) & m <= na \
6.48 +Goal "(ALL n. m <= Suc n --> f n = r) & m <= na \
6.49 \ ==> sumhr(hypnat_of_nat m,hypnat_of_nat na,f) = \
6.50 \ (hypreal_of_nat (na - m) * hypreal_of_real r)";
6.51 by (auto_tac (claset() addSDs [sumr_interval_const],
6.52 - simpset() addsimps [sumhr,hypreal_of_nat_def,
6.53 + simpset() addsimps [hypreal_of_real_def, sumhr,hypreal_of_nat_eq, hypnat_of_nat_eq,
6.54 hypreal_of_real_def, hypreal_mult]));
6.55 qed "sumhr_interval_const";
6.56
7.1 --- a/src/HOL/Hyperreal/HTranscendental.ML Thu Feb 05 10:45:28 2004 +0100
7.2 +++ b/src/HOL/Hyperreal/HTranscendental.ML Tue Feb 10 12:02:11 2004 +0100
7.3 @@ -122,7 +122,7 @@
7.4 Goal "( *f* sqrt)(x pow (hypnat_of_nat 2)) = abs(x)";
7.5 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
7.6 by (auto_tac (claset(),simpset() addsimps [starfun,
7.7 - hypreal_hrabs,hypnat_of_nat_def,hyperpow]));
7.8 + hypreal_hrabs,hypnat_of_nat_eq,hyperpow]));
7.9 qed "hypreal_sqrt_hyperpow_hrabs";
7.10 Addsimps [hypreal_sqrt_hyperpow_hrabs];
7.11
8.1 --- a/src/HOL/Hyperreal/HyperArith.thy Thu Feb 05 10:45:28 2004 +0100
8.2 +++ b/src/HOL/Hyperreal/HyperArith.thy Tue Feb 10 12:02:11 2004 +0100
8.3 @@ -77,7 +77,7 @@
8.4
8.5 lemma eq_hypreal_number_of [simp]:
8.6 "((number_of v :: hypreal) = number_of v') =
8.7 - iszero (number_of (bin_add v (bin_minus v')))"
8.8 + iszero (number_of (bin_add v (bin_minus v')) :: int)"
8.9 apply (simp only: hypreal_number_of_def hypreal_of_real_eq_iff eq_real_number_of)
8.10 done
8.11
8.12 @@ -87,7 +87,7 @@
8.13 (*"neg" is used in rewrite rules for binary comparisons*)
8.14 lemma less_hypreal_number_of [simp]:
8.15 "((number_of v :: hypreal) < number_of v') =
8.16 - neg (number_of (bin_add v (bin_minus v')))"
8.17 + neg (number_of (bin_add v (bin_minus v')) :: int)"
8.18 by (simp only: hypreal_number_of_def hypreal_of_real_less_iff less_real_number_of)
8.19
8.20
8.21 @@ -139,10 +139,6 @@
8.22
8.23 setup hypreal_arith_setup
8.24
8.25 -text{*Used once in NSA*}
8.26 -lemma hypreal_add_minus_eq_minus: "x + y = (0::hypreal) ==> x = -y"
8.27 -by arith
8.28 -
8.29 lemma hypreal_le_add_order: "[| 0 \<le> x; 0 \<le> y |] ==> (0::hypreal) \<le> x + y"
8.30 by arith
8.31
8.32 @@ -192,7 +188,7 @@
8.33
8.34 lemma hrabs_number_of [simp]:
8.35 "abs (number_of v :: hypreal) =
8.36 - (if neg (number_of v) then number_of (bin_minus v)
8.37 + (if neg (number_of v :: int) then number_of (bin_minus v)
8.38 else number_of v)"
8.39 by (simp add: hrabs_def)
8.40
8.41 @@ -229,8 +225,11 @@
8.42
8.43 constdefs
8.44
8.45 - hypreal_of_nat :: "nat => hypreal"
8.46 - "hypreal_of_nat (n::nat) == hypreal_of_real (real n)"
8.47 + hypreal_of_nat :: "nat => hypreal"
8.48 + "hypreal_of_nat m == of_nat m"
8.49 +
8.50 +lemma SNat_eq: "Nats = {n. \<exists>N. n = hypreal_of_nat N}"
8.51 +by (force simp add: hypreal_of_nat_def Nats_def)
8.52
8.53
8.54 lemma hypreal_of_nat_add [simp]:
8.55 @@ -252,46 +251,42 @@
8.56 (* is a hyperreal c.f. NS extension *)
8.57 (*------------------------------------------------------------*)
8.58
8.59 -lemma hypreal_of_nat_iff:
8.60 - "hypreal_of_nat m = Abs_hypreal(hyprel``{%n. real m})"
8.61 -by (simp add: hypreal_of_nat_def hypreal_of_real_def real_of_nat_def)
8.62 +lemma hypreal_of_nat_eq:
8.63 + "hypreal_of_nat (n::nat) = hypreal_of_real (real n)"
8.64 +apply (induct n)
8.65 +apply (simp_all add: hypreal_of_nat_def real_of_nat_def)
8.66 +done
8.67
8.68 -lemma inj_hypreal_of_nat: "inj hypreal_of_nat"
8.69 -by (simp add: inj_on_def hypreal_of_nat_def)
8.70 +lemma hypreal_of_nat:
8.71 + "hypreal_of_nat m = Abs_hypreal(hyprel``{%n. real m})"
8.72 +apply (induct m)
8.73 +apply (simp_all add: hypreal_of_nat_def real_of_nat_def hypreal_zero_def
8.74 + hypreal_one_def hypreal_add)
8.75 +done
8.76
8.77 lemma hypreal_of_nat_Suc:
8.78 "hypreal_of_nat (Suc n) = hypreal_of_nat n + (1::hypreal)"
8.79 -by (simp add: hypreal_of_nat_def real_of_nat_Suc)
8.80 +by (simp add: hypreal_of_nat_def)
8.81
8.82 (*"neg" is used in rewrite rules for binary comparisons*)
8.83 lemma hypreal_of_nat_number_of [simp]:
8.84 "hypreal_of_nat (number_of v :: nat) =
8.85 - (if neg (number_of v) then 0
8.86 + (if neg (number_of v :: int) then 0
8.87 else (number_of v :: hypreal))"
8.88 -by (simp add: hypreal_of_nat_def)
8.89 +by (simp add: hypreal_of_nat_eq)
8.90
8.91 lemma hypreal_of_nat_zero [simp]: "hypreal_of_nat 0 = 0"
8.92 -by (simp del: numeral_0_eq_0 add: numeral_0_eq_0 [symmetric])
8.93 +by (simp add: hypreal_of_nat_def)
8.94
8.95 lemma hypreal_of_nat_one [simp]: "hypreal_of_nat 1 = 1"
8.96 -by (simp add: hypreal_of_nat_Suc)
8.97 +by (simp add: hypreal_of_nat_def)
8.98
8.99 -lemma hypreal_of_nat: "hypreal_of_nat m = Abs_hypreal(hyprel `` {%n. real m})"
8.100 -apply (induct_tac "m")
8.101 -apply (auto simp add: hypreal_zero_def hypreal_of_nat_Suc hypreal_zero_num hypreal_one_num hypreal_add real_of_nat_Suc)
8.102 -done
8.103 +lemma hypreal_of_nat_le_iff [simp]:
8.104 + "(hypreal_of_nat n \<le> hypreal_of_nat m) = (n \<le> m)"
8.105 +by (simp add: hypreal_of_nat_def)
8.106
8.107 -lemma hypreal_of_nat_le_iff:
8.108 - "(hypreal_of_nat n \<le> hypreal_of_nat m) = (n \<le> m)"
8.109 -apply (auto simp add: linorder_not_less [symmetric])
8.110 -done
8.111 -declare hypreal_of_nat_le_iff [simp]
8.112 -
8.113 -lemma hypreal_of_nat_ge_zero: "0 \<le> hypreal_of_nat n"
8.114 -apply (simp (no_asm) add: hypreal_of_nat_zero [symmetric]
8.115 - del: hypreal_of_nat_zero)
8.116 -done
8.117 -declare hypreal_of_nat_ge_zero [simp]
8.118 +lemma hypreal_of_nat_ge_zero [simp]: "0 \<le> hypreal_of_nat n"
8.119 +by (simp add: hypreal_of_nat_def)
8.120
8.121
8.122 (*
8.123 @@ -302,7 +297,6 @@
8.124
8.125 ML
8.126 {*
8.127 -val hypreal_add_minus_eq_minus = thm "hypreal_add_minus_eq_minus";
8.128 val hypreal_le_add_order = thm"hypreal_le_add_order";
8.129
8.130 val hypreal_of_nat_def = thm"hypreal_of_nat_def";
8.131 @@ -316,8 +310,6 @@
8.132 val hypreal_of_nat_add = thm "hypreal_of_nat_add";
8.133 val hypreal_of_nat_mult = thm "hypreal_of_nat_mult";
8.134 val hypreal_of_nat_less_iff = thm "hypreal_of_nat_less_iff";
8.135 -val hypreal_of_nat_iff = thm "hypreal_of_nat_iff";
8.136 -val inj_hypreal_of_nat = thm "inj_hypreal_of_nat";
8.137 val hypreal_of_nat_Suc = thm "hypreal_of_nat_Suc";
8.138 val hypreal_of_nat_number_of = thm "hypreal_of_nat_number_of";
8.139 val hypreal_of_nat_zero = thm "hypreal_of_nat_zero";
9.1 --- a/src/HOL/Hyperreal/HyperDef.thy Thu Feb 05 10:45:28 2004 +0100
9.2 +++ b/src/HOL/Hyperreal/HyperDef.thy Tue Feb 10 12:02:11 2004 +0100
9.3 @@ -176,6 +176,11 @@
9.4 "(X: FreeUltrafilterNat) = (-X \<notin> FreeUltrafilterNat)"
9.5 by (auto simp add: FreeUltrafilterNat_Compl_iff1 [symmetric])
9.6
9.7 +lemma cofinite_mem_FreeUltrafilterNat: "finite (-X) ==> X \<in> FreeUltrafilterNat"
9.8 +apply (drule FreeUltrafilterNat_finite)
9.9 +apply (simp add: FreeUltrafilterNat_Compl_iff2 [symmetric])
9.10 +done
9.11 +
9.12 lemma FreeUltrafilterNat_UNIV [simp]: "(UNIV::nat set) \<in> FreeUltrafilterNat"
9.13 by (rule FreeUltrafilterNat_mem [THEN FreeUltrafilter_Ultrafilter, THEN Ultrafilter_Filter, THEN mem_FiltersetD4])
9.14
9.15 @@ -768,7 +773,7 @@
9.16
9.17 lemma lemma_omega_empty_singleton_disj: "{n::nat. x = real n} = {} |
9.18 (\<exists>y. {n::nat. x = real n} = {y})"
9.19 -by (force dest: inj_real_of_nat [THEN injD])
9.20 +by (force)
9.21
9.22 lemma lemma_finite_omega_set: "finite {n::nat. x = real n}"
9.23 by (cut_tac x = x in lemma_omega_empty_singleton_disj, auto)
9.24 @@ -789,7 +794,7 @@
9.25 lemma lemma_epsilon_empty_singleton_disj:
9.26 "{n::nat. x = inverse(real(Suc n))} = {} |
9.27 (\<exists>y. {n::nat. x = inverse(real(Suc n))} = {y})"
9.28 -by (auto simp add: inj_real_of_nat [THEN inj_eq])
9.29 +by (auto)
9.30
9.31 lemma lemma_finite_epsilon_set: "finite {n. x = inverse(real(Suc n))}"
9.32 by (cut_tac x = x in lemma_epsilon_empty_singleton_disj, auto)
10.1 --- a/src/HOL/Hyperreal/HyperNat.thy Thu Feb 05 10:45:28 2004 +0100
10.2 +++ b/src/HOL/Hyperreal/HyperNat.thy Tue Feb 10 12:02:11 2004 +0100
10.3 @@ -24,36 +24,9 @@
10.4
10.5 consts whn :: hypnat
10.6
10.7 -constdefs
10.8 -
10.9 - (* embedding the naturals in the hypernaturals *)
10.10 - hypnat_of_nat :: "nat => hypnat"
10.11 - "hypnat_of_nat m == Abs_hypnat(hypnatrel``{%n::nat. m})"
10.12 -
10.13 - (* hypernaturals as members of the hyperreals; the set is defined as *)
10.14 - (* the nonstandard extension of set of naturals embedded in the reals *)
10.15 - HNat :: "hypreal set"
10.16 - "HNat == *s* {n. \<exists>no::nat. n = real no}"
10.17 -
10.18 - (* the set of infinite hypernatural numbers *)
10.19 - HNatInfinite :: "hypnat set"
10.20 - "HNatInfinite == {n. n \<notin> Nats}"
10.21 -
10.22 - (* explicit embedding of the hypernaturals in the hyperreals *)
10.23 - hypreal_of_hypnat :: "hypnat => hypreal"
10.24 - "hypreal_of_hypnat N == Abs_hypreal(\<Union>X \<in> Rep_hypnat(N).
10.25 - hyprel``{%n::nat. real (X n)})"
10.26
10.27 defs (overloaded)
10.28
10.29 - (** the overloaded constant "Nats" **)
10.30 -
10.31 - (* set of naturals embedded in the hyperreals*)
10.32 - SNat_def: "Nats == {n. \<exists>N. n = hypreal_of_nat N}"
10.33 -
10.34 - (* set of naturals embedded in the hypernaturals*)
10.35 - SHNat_def: "Nats == {n. \<exists>N. n = hypnat_of_nat N}"
10.36 -
10.37 (** hypernatural arithmetic **)
10.38
10.39 hypnat_zero_def: "0 == Abs_hypnat(hypnatrel``{%n::nat. 0})"
10.40 @@ -151,18 +124,6 @@
10.41
10.42 declare Rep_hypnat_nonempty [simp]
10.43
10.44 -subsection{*@{term hypnat_of_nat}:
10.45 - the Injection from @{typ nat} to @{typ hypnat}*}
10.46 -
10.47 -lemma inj_hypnat_of_nat: "inj(hypnat_of_nat)"
10.48 -apply (rule inj_onI)
10.49 -apply (unfold hypnat_of_nat_def)
10.50 -apply (drule inj_on_Abs_hypnat [THEN inj_onD])
10.51 -apply (rule hypnatrel_in_hypnat)+
10.52 -apply (drule eq_equiv_class)
10.53 -apply (rule equiv_hypnatrel)
10.54 -apply (simp_all split: split_if_asm)
10.55 -done
10.56
10.57 lemma eq_Abs_hypnat:
10.58 "(!!x. z = Abs_hypnat(hypnatrel``{x}) ==> P) ==> P"
10.59 @@ -439,6 +400,13 @@
10.60 apply (auto simp add: hypnat_zero_def hypnat_mult, ultra+)
10.61 done
10.62
10.63 +lemma hypnat_diff_is_0_eq [simp]: "((m::hypnat) - n = 0) = (m \<le> n)"
10.64 +apply (rule eq_Abs_hypnat [of m])
10.65 +apply (rule eq_Abs_hypnat [of n])
10.66 +apply (simp add: hypnat_le hypnat_minus hypnat_zero_def)
10.67 +done
10.68 +
10.69 +
10.70
10.71 subsection{*Theorems for Ordering*}
10.72
10.73 @@ -496,42 +464,73 @@
10.74 apply (insert add_le_less_mono [OF _ zero_less_one, of 0], auto)
10.75 done
10.76
10.77 +lemma hypnat_add_self_not_less: "~ (x + y < (x::hypnat))"
10.78 +by (simp add: linorder_not_le [symmetric] add_commute [of x])
10.79 +
10.80 +lemma hypnat_diff_split:
10.81 + "P(a - b::hypnat) = ((a<b --> P 0) & (ALL d. a = b + d --> P d))"
10.82 + -- {* elimination of @{text -} on @{text hypnat} *}
10.83 +proof (cases "a<b" rule: case_split)
10.84 + case True
10.85 + thus ?thesis
10.86 + by (auto simp add: hypnat_add_self_not_less order_less_imp_le
10.87 + hypnat_diff_is_0_eq [THEN iffD2])
10.88 +next
10.89 + case False
10.90 + thus ?thesis
10.91 + by (auto simp add: linorder_not_less dest: order_le_less_trans);
10.92 +qed
10.93 +
10.94 +
10.95 subsection{*The Embedding @{term hypnat_of_nat} Preserves Ring and
10.96 Order Properties*}
10.97
10.98 +constdefs
10.99 +
10.100 + hypnat_of_nat :: "nat => hypnat"
10.101 + "hypnat_of_nat m == of_nat m"
10.102 +
10.103 + (* the set of infinite hypernatural numbers *)
10.104 + HNatInfinite :: "hypnat set"
10.105 + "HNatInfinite == {n. n \<notin> Nats}"
10.106 +
10.107 +
10.108 lemma hypnat_of_nat_add:
10.109 "hypnat_of_nat ((z::nat) + w) = hypnat_of_nat z + hypnat_of_nat w"
10.110 -by (simp add: hypnat_of_nat_def hypnat_add)
10.111 -
10.112 -lemma hypnat_of_nat_minus:
10.113 - "hypnat_of_nat ((z::nat) - w) = hypnat_of_nat z - hypnat_of_nat w"
10.114 -by (simp add: hypnat_of_nat_def hypnat_minus)
10.115 +by (simp add: hypnat_of_nat_def)
10.116
10.117 lemma hypnat_of_nat_mult:
10.118 "hypnat_of_nat (z * w) = hypnat_of_nat z * hypnat_of_nat w"
10.119 -by (simp add: hypnat_of_nat_def hypnat_mult)
10.120 +by (simp add: hypnat_of_nat_def)
10.121
10.122 lemma hypnat_of_nat_less_iff [simp]:
10.123 "(hypnat_of_nat z < hypnat_of_nat w) = (z < w)"
10.124 -by (simp add: hypnat_less hypnat_of_nat_def)
10.125 +by (simp add: hypnat_of_nat_def)
10.126
10.127 lemma hypnat_of_nat_le_iff [simp]:
10.128 "(hypnat_of_nat z \<le> hypnat_of_nat w) = (z \<le> w)"
10.129 -by (simp add: linorder_not_less [symmetric])
10.130 +by (simp add: hypnat_of_nat_def)
10.131
10.132 -lemma hypnat_of_nat_one: "hypnat_of_nat (Suc 0) = (1::hypnat)"
10.133 -by (simp add: hypnat_of_nat_def hypnat_one_def)
10.134 +lemma hypnat_of_nat_eq_iff [simp]:
10.135 + "(hypnat_of_nat z = hypnat_of_nat w) = (z = w)"
10.136 +by (simp add: hypnat_of_nat_def)
10.137
10.138 -lemma hypnat_of_nat_zero: "hypnat_of_nat 0 = 0"
10.139 -by (simp add: hypnat_of_nat_def hypnat_zero_def)
10.140 +lemma hypnat_of_nat_one [simp]: "hypnat_of_nat (Suc 0) = (1::hypnat)"
10.141 +by (simp add: hypnat_of_nat_def)
10.142
10.143 -lemma hypnat_of_nat_zero_iff: "(hypnat_of_nat n = 0) = (n = 0)"
10.144 -by (auto intro: FreeUltrafilterNat_P
10.145 - simp add: hypnat_of_nat_def hypnat_zero_def)
10.146 +lemma hypnat_of_nat_zero [simp]: "hypnat_of_nat 0 = 0"
10.147 +by (simp add: hypnat_of_nat_def)
10.148
10.149 -lemma hypnat_of_nat_Suc:
10.150 +lemma hypnat_of_nat_zero_iff [simp]: "(hypnat_of_nat n = 0) = (n = 0)"
10.151 +by (simp add: hypnat_of_nat_def)
10.152 +
10.153 +lemma hypnat_of_nat_Suc [simp]:
10.154 "hypnat_of_nat (Suc n) = hypnat_of_nat n + (1::hypnat)"
10.155 -by (auto simp add: hypnat_add hypnat_of_nat_def hypnat_one_def)
10.156 +by (simp add: hypnat_of_nat_def)
10.157 +
10.158 +lemma hypnat_of_nat_minus:
10.159 + "hypnat_of_nat ((j::nat) - k) = hypnat_of_nat j - hypnat_of_nat k"
10.160 +by (simp add: hypnat_of_nat_def split: nat_diff_split hypnat_diff_split)
10.161
10.162
10.163 subsection{*Existence of an Infinite Hypernatural Number*}
10.164 @@ -546,111 +545,64 @@
10.165 follows because member @{term FreeUltrafilterNat} is not finite.
10.166 See @{text HyperDef.thy} for similar argument.*}
10.167
10.168 -lemma not_ex_hypnat_of_nat_eq_omega:
10.169 - "~ (\<exists>x. hypnat_of_nat x = whn)"
10.170 -apply (simp add: hypnat_omega_def hypnat_of_nat_def)
10.171 -apply (auto dest: FreeUltrafilterNat_not_finite)
10.172 -done
10.173 -
10.174 -lemma hypnat_of_nat_not_eq_omega: "hypnat_of_nat x \<noteq> whn"
10.175 -by (cut_tac not_ex_hypnat_of_nat_eq_omega, auto)
10.176 -declare hypnat_of_nat_not_eq_omega [THEN not_sym, simp]
10.177 -
10.178
10.179 subsection{*Properties of the set @{term Nats} of Embedded Natural Numbers*}
10.180
10.181 -(* Infinite hypernatural not in embedded Nats *)
10.182 -lemma SHNAT_omega_not_mem [simp]: "whn \<notin> Nats"
10.183 -by (simp add: SHNat_def)
10.184 -
10.185 -(*-----------------------------------------------------------------------
10.186 - Closure laws for members of (embedded) set standard naturals Nats
10.187 - -----------------------------------------------------------------------*)
10.188 -lemma SHNat_add:
10.189 - "!!x::hypnat. [| x \<in> Nats; y \<in> Nats |] ==> x + y \<in> Nats"
10.190 -apply (simp add: SHNat_def, safe)
10.191 -apply (rule_tac x = "N + Na" in exI)
10.192 -apply (simp add: hypnat_of_nat_add)
10.193 +lemma of_nat_eq_add [rule_format]:
10.194 + "\<forall>d::hypnat. of_nat m = of_nat n + d --> d \<in> range of_nat"
10.195 +apply (induct n)
10.196 +apply (auto simp add: add_assoc)
10.197 +apply (case_tac x)
10.198 +apply (auto simp add: add_commute [of 1])
10.199 done
10.200
10.201 -lemma SHNat_minus:
10.202 - "!!x::hypnat. [| x \<in> Nats; y \<in> Nats |] ==> x - y \<in> Nats"
10.203 -apply (simp add: SHNat_def, safe)
10.204 -apply (rule_tac x = "N - Na" in exI)
10.205 -apply (simp add: hypnat_of_nat_minus)
10.206 -done
10.207 -
10.208 -lemma SHNat_mult:
10.209 - "!!x::hypnat. [| x \<in> Nats; y \<in> Nats |] ==> x * y \<in> Nats"
10.210 -apply (simp add: SHNat_def, safe)
10.211 -apply (rule_tac x = "N * Na" in exI)
10.212 -apply (simp (no_asm) add: hypnat_of_nat_mult)
10.213 -done
10.214 -
10.215 -lemma SHNat_add_cancel: "!!x::hypnat. [| x + y \<in> Nats; y \<in> Nats |] ==> x \<in> Nats"
10.216 -by (drule_tac x = "x+y" in SHNat_minus, auto)
10.217 -
10.218 -lemma SHNat_hypnat_of_nat [simp]: "hypnat_of_nat x \<in> Nats"
10.219 -by (simp add: SHNat_def, blast)
10.220 -
10.221 -lemma SHNat_hypnat_of_nat_one [simp]: "hypnat_of_nat (Suc 0) \<in> Nats"
10.222 -by simp
10.223 -
10.224 -lemma SHNat_hypnat_of_nat_zero [simp]: "hypnat_of_nat 0 \<in> Nats"
10.225 -by simp
10.226 -
10.227 -lemma SHNat_one [simp]: "(1::hypnat) \<in> Nats"
10.228 -by (simp add: hypnat_of_nat_one [symmetric])
10.229 -
10.230 -lemma SHNat_zero [simp]: "(0::hypnat) \<in> Nats"
10.231 -by (simp add: hypnat_of_nat_zero [symmetric])
10.232 -
10.233 -lemma SHNat_iff: "(x \<in> Nats) = (\<exists>y. x = hypnat_of_nat y)"
10.234 -by (simp add: SHNat_def)
10.235 -
10.236 -lemma SHNat_hypnat_of_nat_iff:
10.237 - "Nats = hypnat_of_nat ` (UNIV::nat set)"
10.238 -by (auto simp add: SHNat_def)
10.239 -
10.240 -lemma leSuc_Un_eq: "{n. n \<le> Suc m} = {n. n \<le> m} Un {n. n = Suc m}"
10.241 -by (auto simp add: le_Suc_eq)
10.242 -
10.243 -lemma finite_nat_le_segment: "finite {n::nat. n \<le> m}"
10.244 -apply (induct_tac "m")
10.245 -apply (auto simp add: leSuc_Un_eq)
10.246 +lemma Nats_diff [simp]: "[|a \<in> Nats; b \<in> Nats|] ==> (a-b :: hypnat) \<in> Nats"
10.247 +apply (auto simp add: of_nat_eq_add Nats_def split: hypnat_diff_split)
10.248 done
10.249
10.250 lemma lemma_unbounded_set [simp]: "{n::nat. m < n} \<in> FreeUltrafilterNat"
10.251 -by (insert finite_nat_le_segment
10.252 - [THEN FreeUltrafilterNat_finite,
10.253 - THEN FreeUltrafilterNat_Compl_mem, of m], ultra)
10.254 -
10.255 -(*????hyperdef*)
10.256 -lemma cofinite_mem_FreeUltrafilterNat: "finite (-X) ==> X \<in> FreeUltrafilterNat"
10.257 -apply (drule FreeUltrafilterNat_finite)
10.258 -apply (simp add: FreeUltrafilterNat_Compl_iff2 [symmetric])
10.259 +apply (insert finite_atMost [of m])
10.260 +apply (simp add: atMost_def)
10.261 +apply (drule FreeUltrafilterNat_finite)
10.262 +apply (drule FreeUltrafilterNat_Compl_mem)
10.263 +apply ultra
10.264 done
10.265
10.266 lemma Compl_Collect_le: "- {n::nat. N \<le> n} = {n. n < N}"
10.267 by (simp add: Collect_neg_eq [symmetric] linorder_not_le)
10.268
10.269 +
10.270 +lemma hypnat_of_nat_eq:
10.271 + "hypnat_of_nat m = Abs_hypnat(hypnatrel``{%n::nat. m})"
10.272 +apply (induct m)
10.273 +apply (simp_all add: hypnat_zero_def hypnat_one_def hypnat_add);
10.274 +done
10.275 +
10.276 +lemma SHNat_eq: "Nats = {n. \<exists>N. n = hypnat_of_nat N}"
10.277 +by (force simp add: hypnat_of_nat_def Nats_def)
10.278 +
10.279 lemma hypnat_omega_gt_SHNat:
10.280 "n \<in> Nats ==> n < whn"
10.281 -apply (auto simp add: SHNat_def hypnat_of_nat_def hypnat_less_def
10.282 - hypnat_le_def hypnat_omega_def)
10.283 +apply (auto simp add: hypnat_of_nat_eq hypnat_less_def hypnat_le_def
10.284 + hypnat_omega_def SHNat_eq)
10.285 prefer 2 apply (force dest: FreeUltrafilterNat_not_finite)
10.286 apply (auto intro!: exI)
10.287 apply (rule cofinite_mem_FreeUltrafilterNat)
10.288 apply (simp add: Compl_Collect_le finite_nat_segment)
10.289 done
10.290
10.291 -lemma hypnat_of_nat_less_whn: "hypnat_of_nat n < whn"
10.292 -by (insert hypnat_omega_gt_SHNat [of "hypnat_of_nat n"], auto)
10.293 -declare hypnat_of_nat_less_whn [simp]
10.294 +(* Infinite hypernatural not in embedded Nats *)
10.295 +lemma SHNAT_omega_not_mem [simp]: "whn \<notin> Nats"
10.296 +apply (blast dest: hypnat_omega_gt_SHNat)
10.297 +done
10.298
10.299 -lemma hypnat_of_nat_le_whn: "hypnat_of_nat n \<le> whn"
10.300 +lemma hypnat_of_nat_less_whn [simp]: "hypnat_of_nat n < whn"
10.301 +apply (insert hypnat_omega_gt_SHNat [of "hypnat_of_nat n"])
10.302 +apply (simp add: hypnat_of_nat_def)
10.303 +done
10.304 +
10.305 +lemma hypnat_of_nat_le_whn [simp]: "hypnat_of_nat n \<le> whn"
10.306 by (rule hypnat_of_nat_less_whn [THEN order_less_imp_le])
10.307 -declare hypnat_of_nat_le_whn [simp]
10.308
10.309 lemma hypnat_zero_less_hypnat_omega [simp]: "0 < whn"
10.310 by (simp add: hypnat_omega_gt_SHNat)
10.311 @@ -661,37 +613,22 @@
10.312
10.313 subsection{*Infinite Hypernatural Numbers -- @{term HNatInfinite}*}
10.314
10.315 -lemma HNatInfinite_whn: "whn \<in> HNatInfinite"
10.316 -by (simp add: HNatInfinite_def SHNat_def)
10.317 -declare HNatInfinite_whn [simp]
10.318 -
10.319 -lemma SHNat_not_HNatInfinite: "x \<in> Nats ==> x \<notin> HNatInfinite"
10.320 +lemma HNatInfinite_whn [simp]: "whn \<in> HNatInfinite"
10.321 by (simp add: HNatInfinite_def)
10.322
10.323 -lemma not_HNatInfinite_SHNat: "x \<notin> HNatInfinite ==> x \<in> Nats"
10.324 +lemma Nats_not_HNatInfinite_iff: "(x \<in> Nats) = (x \<notin> HNatInfinite)"
10.325 by (simp add: HNatInfinite_def)
10.326
10.327 -lemma not_SHNat_HNatInfinite: "x \<notin> Nats ==> x \<in> HNatInfinite"
10.328 +lemma HNatInfinite_not_Nats_iff: "(x \<in> HNatInfinite) = (x \<notin> Nats)"
10.329 by (simp add: HNatInfinite_def)
10.330
10.331 -lemma HNatInfinite_not_SHNat: "x \<in> HNatInfinite ==> x \<notin> Nats"
10.332 -by (simp add: HNatInfinite_def)
10.333 -
10.334 -lemma SHNat_not_HNatInfinite_iff: "(x \<in> Nats) = (x \<notin> HNatInfinite)"
10.335 -by (blast intro!: SHNat_not_HNatInfinite not_HNatInfinite_SHNat)
10.336 -
10.337 -lemma not_SHNat_HNatInfinite_iff: "(x \<notin> Nats) = (x \<in> HNatInfinite)"
10.338 -by (blast intro!: not_SHNat_HNatInfinite HNatInfinite_not_SHNat)
10.339 -
10.340 -lemma SHNat_HNatInfinite_disj: "x \<in> Nats | x \<in> HNatInfinite"
10.341 -by (simp add: SHNat_not_HNatInfinite_iff)
10.342 -
10.343
10.344 subsection{*Alternative Characterization of the Set of Infinite Hypernaturals:
10.345 @{term "HNatInfinite = {N. \<forall>n \<in> Nats. n < N}"}*}
10.346
10.347 (*??delete? similar reasoning in hypnat_omega_gt_SHNat above*)
10.348 -lemma HNatInfinite_FreeUltrafilterNat_lemma: "\<forall>N::nat. {n. f n \<noteq> N} \<in> FreeUltrafilterNat
10.349 +lemma HNatInfinite_FreeUltrafilterNat_lemma:
10.350 + "\<forall>N::nat. {n. f n \<noteq> N} \<in> FreeUltrafilterNat
10.351 ==> {n. N < f n} \<in> FreeUltrafilterNat"
10.352 apply (induct_tac "N")
10.353 apply (drule_tac x = 0 in spec)
10.354 @@ -700,15 +637,14 @@
10.355 done
10.356
10.357 lemma HNatInfinite_iff: "HNatInfinite = {N. \<forall>n \<in> Nats. n < N}"
10.358 -apply (unfold HNatInfinite_def SHNat_def hypnat_of_nat_def, safe)
10.359 -apply (drule_tac [2] x = "Abs_hypnat (hypnatrel `` {%n. N}) " in bspec)
10.360 +apply (auto simp add: HNatInfinite_def SHNat_eq hypnat_of_nat_eq)
10.361 apply (rule_tac z = x in eq_Abs_hypnat)
10.362 -apply (rule_tac z = n in eq_Abs_hypnat)
10.363 -apply (auto simp add: hypnat_less)
10.364 -apply (auto elim: HNatInfinite_FreeUltrafilterNat_lemma
10.365 - simp add: FreeUltrafilterNat_Compl_iff1 Collect_neg_eq [symmetric])
10.366 +apply (auto elim: HNatInfinite_FreeUltrafilterNat_lemma
10.367 + simp add: hypnat_less FreeUltrafilterNat_Compl_iff1
10.368 + Collect_neg_eq [symmetric])
10.369 done
10.370
10.371 +
10.372 subsection{*Alternative Characterization of @{term HNatInfinite} using
10.373 Free Ultrafilter*}
10.374
10.375 @@ -716,9 +652,8 @@
10.376 "x \<in> HNatInfinite
10.377 ==> \<exists>X \<in> Rep_hypnat x. \<forall>u. {n. u < X n}: FreeUltrafilterNat"
10.378 apply (rule eq_Abs_hypnat [of x])
10.379 -apply (auto simp add: HNatInfinite_iff SHNat_iff hypnat_of_nat_def)
10.380 +apply (auto simp add: HNatInfinite_iff SHNat_eq hypnat_of_nat_eq)
10.381 apply (rule bexI [OF _ lemma_hypnatrel_refl], clarify)
10.382 -apply (drule_tac x = "hypnat_of_nat u" in bspec, simp)
10.383 apply (auto simp add: hypnat_of_nat_def hypnat_less)
10.384 done
10.385
10.386 @@ -726,26 +661,24 @@
10.387 "\<exists>X \<in> Rep_hypnat x. \<forall>u. {n. u < X n}: FreeUltrafilterNat
10.388 ==> x \<in> HNatInfinite"
10.389 apply (rule eq_Abs_hypnat [of x])
10.390 -apply (auto simp add: hypnat_less HNatInfinite_iff SHNat_iff hypnat_of_nat_def)
10.391 +apply (auto simp add: hypnat_less HNatInfinite_iff SHNat_eq hypnat_of_nat_eq)
10.392 apply (drule spec, ultra, auto)
10.393 done
10.394
10.395 lemma HNatInfinite_FreeUltrafilterNat_iff:
10.396 "(x \<in> HNatInfinite) =
10.397 (\<exists>X \<in> Rep_hypnat x. \<forall>u. {n. u < X n}: FreeUltrafilterNat)"
10.398 -apply (blast intro: HNatInfinite_FreeUltrafilterNat FreeUltrafilterNat_HNatInfinite)
10.399 -done
10.400 +by (blast intro: HNatInfinite_FreeUltrafilterNat
10.401 + FreeUltrafilterNat_HNatInfinite)
10.402
10.403 -lemma HNatInfinite_gt_one: "x \<in> HNatInfinite ==> (1::hypnat) < x"
10.404 +lemma HNatInfinite_gt_one [simp]: "x \<in> HNatInfinite ==> (1::hypnat) < x"
10.405 by (auto simp add: HNatInfinite_iff)
10.406 -declare HNatInfinite_gt_one [simp]
10.407
10.408 -lemma zero_not_mem_HNatInfinite: "0 \<notin> HNatInfinite"
10.409 +lemma zero_not_mem_HNatInfinite [simp]: "0 \<notin> HNatInfinite"
10.410 apply (auto simp add: HNatInfinite_iff)
10.411 apply (drule_tac a = " (1::hypnat) " in equals0D)
10.412 apply simp
10.413 done
10.414 -declare zero_not_mem_HNatInfinite [simp]
10.415
10.416 lemma HNatInfinite_not_eq_zero: "x \<in> HNatInfinite ==> 0 < x"
10.417 apply (drule HNatInfinite_gt_one)
10.418 @@ -758,78 +691,60 @@
10.419
10.420 subsection{*Closure Rules*}
10.421
10.422 -lemma HNatInfinite_add: "[| x \<in> HNatInfinite; y \<in> HNatInfinite |]
10.423 - ==> x + y \<in> HNatInfinite"
10.424 +lemma HNatInfinite_add:
10.425 + "[| x \<in> HNatInfinite; y \<in> HNatInfinite |] ==> x + y \<in> HNatInfinite"
10.426 apply (auto simp add: HNatInfinite_iff)
10.427 apply (drule bspec, assumption)
10.428 -apply (drule bspec [OF _ SHNat_zero])
10.429 +apply (drule bspec [OF _ Nats_0])
10.430 apply (drule add_strict_mono, assumption, simp)
10.431 done
10.432
10.433 -lemma HNatInfinite_SHNat_add: "[| x \<in> HNatInfinite; y \<in> Nats |] ==> x + y \<in> HNatInfinite"
10.434 -apply (rule ccontr, drule not_HNatInfinite_SHNat)
10.435 -apply (drule_tac x = "x + y" in SHNat_minus)
10.436 -apply (auto simp add: SHNat_not_HNatInfinite_iff)
10.437 +lemma HNatInfinite_SHNat_add:
10.438 + "[| x \<in> HNatInfinite; y \<in> Nats |] ==> x + y \<in> HNatInfinite"
10.439 +apply (auto simp add: HNatInfinite_not_Nats_iff)
10.440 +apply (drule_tac a = "x + y" in Nats_diff)
10.441 +apply (auto );
10.442 done
10.443
10.444 -lemma HNatInfinite_SHNat_diff: "[| x \<in> HNatInfinite; y \<in> Nats |] ==> x - y \<in> HNatInfinite"
10.445 -apply (rule ccontr, drule not_HNatInfinite_SHNat)
10.446 -apply (drule_tac x = "x - y" in SHNat_add)
10.447 -apply (subgoal_tac [2] "y \<le> x")
10.448 -apply (auto dest!: hypnat_le_add_diff_inverse2 simp add: not_SHNat_HNatInfinite_iff [symmetric])
10.449 -apply (auto intro!: order_less_imp_le simp add: not_SHNat_HNatInfinite_iff HNatInfinite_iff)
10.450 -done
10.451 +lemma HNatInfinite_Nats_imp_less: "[| x \<in> HNatInfinite; y \<in> Nats |] ==> y < x"
10.452 +by (simp add: HNatInfinite_iff)
10.453 +
10.454 +lemma HNatInfinite_SHNat_diff:
10.455 + assumes x: "x \<in> HNatInfinite" and y: "y \<in> Nats"
10.456 + shows "x - y \<in> HNatInfinite"
10.457 +proof -
10.458 + have "y < x" by (simp add: HNatInfinite_Nats_imp_less prems)
10.459 + hence "x - y + y = x" by (simp add: order_less_imp_le)
10.460 + with x show ?thesis
10.461 + by (force simp add: HNatInfinite_not_Nats_iff
10.462 + dest: Nats_add [of "x-y", OF _ y])
10.463 +qed
10.464
10.465 lemma HNatInfinite_add_one: "x \<in> HNatInfinite ==> x + (1::hypnat) \<in> HNatInfinite"
10.466 by (auto intro: HNatInfinite_SHNat_add)
10.467
10.468 -lemma HNatInfinite_minus_one: "x \<in> HNatInfinite ==> x - (1::hypnat) \<in> HNatInfinite"
10.469 -apply (rule ccontr, drule not_HNatInfinite_SHNat)
10.470 -apply (drule_tac x = "x - (1::hypnat) " and y = " (1::hypnat) " in SHNat_add)
10.471 -apply (auto simp add: not_SHNat_HNatInfinite_iff [symmetric])
10.472 -done
10.473 -
10.474 lemma HNatInfinite_is_Suc: "x \<in> HNatInfinite ==> \<exists>y. x = y + (1::hypnat)"
10.475 apply (rule_tac x = "x - (1::hypnat) " in exI)
10.476 apply auto
10.477 done
10.478
10.479
10.480 -subsection{*@{term HNat}: the Hypernaturals Embedded in the Hyperreals*}
10.481 -
10.482 +subsection{*Embedding of the Hypernaturals into the Hyperreals*}
10.483 text{*Obtained using the nonstandard extension of the naturals*}
10.484
10.485 -lemma HNat_hypreal_of_nat: "hypreal_of_nat N \<in> HNat"
10.486 -apply (simp add: HNat_def starset_def hypreal_of_nat_def hypreal_of_real_def, auto, ultra)
10.487 -apply (rule_tac x = N in exI, auto)
10.488 -done
10.489 -declare HNat_hypreal_of_nat [simp]
10.490 +constdefs
10.491 + hypreal_of_hypnat :: "hypnat => hypreal"
10.492 + "hypreal_of_hypnat N ==
10.493 + Abs_hypreal(\<Union>X \<in> Rep_hypnat(N). hyprel``{%n::nat. real (X n)})"
10.494
10.495 -lemma HNat_add: "[| x \<in> HNat; y \<in> HNat |] ==> x + y \<in> HNat"
10.496 -apply (simp add: HNat_def starset_def)
10.497 -apply (rule_tac z = x in eq_Abs_hypreal)
10.498 -apply (rule_tac z = y in eq_Abs_hypreal)
10.499 -apply (auto dest!: bspec intro: lemma_hyprel_refl simp add: hypreal_add, ultra)
10.500 -apply (rule_tac x = "no+noa" in exI, auto)
10.501 -done
10.502
10.503 -lemma HNat_mult:
10.504 - "[| x \<in> HNat; y \<in> HNat |] ==> x * y \<in> HNat"
10.505 -apply (simp add: HNat_def starset_def)
10.506 -apply (rule_tac z = x in eq_Abs_hypreal)
10.507 -apply (rule_tac z = y in eq_Abs_hypreal)
10.508 -apply (auto dest!: bspec intro: lemma_hyprel_refl simp add: hypreal_mult, ultra)
10.509 -apply (rule_tac x = "no*noa" in exI, auto)
10.510 -done
10.511 -
10.512 -
10.513 -subsection{*Embedding of the Hypernaturals into the Hyperreals*}
10.514 +lemma HNat_hypreal_of_nat [simp]: "hypreal_of_nat N \<in> Nats"
10.515 +by (simp add: hypreal_of_nat_def)
10.516
10.517 (*WARNING: FRAGILE!*)
10.518 -lemma lemma_hyprel_FUFN: "(Ya \<in> hyprel ``{%n. f(n)}) =
10.519 - ({n. f n = Ya n} \<in> FreeUltrafilterNat)"
10.520 -apply auto
10.521 -done
10.522 +lemma lemma_hyprel_FUFN:
10.523 + "(Ya \<in> hyprel ``{%n. f(n)}) = ({n. f n = Ya n} \<in> FreeUltrafilterNat)"
10.524 +by force
10.525
10.526 lemma hypreal_of_hypnat:
10.527 "hypreal_of_hypnat (Abs_hypnat(hypnatrel``{%n. X n})) =
10.528 @@ -840,16 +755,13 @@
10.529 simp add: lemma_hyprel_FUFN)
10.530 done
10.531
10.532 -lemma inj_hypreal_of_hypnat: "inj(hypreal_of_hypnat)"
10.533 -apply (rule inj_onI)
10.534 -apply (rule_tac z = x in eq_Abs_hypnat)
10.535 -apply (rule_tac z = y in eq_Abs_hypnat)
10.536 +lemma hypreal_of_hypnat_inject [simp]:
10.537 + "(hypreal_of_hypnat m = hypreal_of_hypnat n) = (m=n)"
10.538 +apply (rule eq_Abs_hypnat [of m])
10.539 +apply (rule eq_Abs_hypnat [of n])
10.540 apply (auto simp add: hypreal_of_hypnat)
10.541 done
10.542
10.543 -declare inj_hypreal_of_hypnat [THEN inj_eq, simp]
10.544 -declare inj_hypnat_of_nat [THEN inj_eq, simp]
10.545 -
10.546 lemma hypreal_of_hypnat_zero: "hypreal_of_hypnat 0 = 0"
10.547 by (simp add: hypnat_zero_def hypreal_zero_def hypreal_of_hypnat)
10.548
10.549 @@ -886,43 +798,21 @@
10.550 apply (simp add: hypreal_of_hypnat hypreal_zero_num hypreal_le)
10.551 done
10.552
10.553 -(*????DELETE??*)
10.554 -lemma hypnat_eq_zero: "\<forall>n. N \<le> n ==> N = (0::hypnat)"
10.555 -apply (drule_tac x = 0 in spec)
10.556 -apply (rule_tac z = N in eq_Abs_hypnat)
10.557 -apply (auto simp add: hypnat_le hypnat_zero_def)
10.558 -done
10.559 -
10.560 -(*????DELETE??*)
10.561 -lemma hypnat_not_all_eq_zero: "~ (\<forall>n. n = (0::hypnat))"
10.562 -by auto
10.563 -
10.564 -(*????DELETE??*)
10.565 -lemma hypnat_le_one_eq_one: "n \<noteq> 0 ==> (n \<le> (1::hypnat)) = (n = (1::hypnat))"
10.566 -by (auto simp add: order_le_less)
10.567 -
10.568 -(*WHERE DO THESE BELONG???*)
10.569 -lemma HNatInfinite_inverse_Infinitesimal: "n \<in> HNatInfinite ==> inverse (hypreal_of_hypnat n) \<in> Infinitesimal"
10.570 +lemma HNatInfinite_inverse_Infinitesimal [simp]:
10.571 + "n \<in> HNatInfinite ==> inverse (hypreal_of_hypnat n) \<in> Infinitesimal"
10.572 apply (rule eq_Abs_hypnat [of n])
10.573 -apply (auto simp add: hypreal_of_hypnat hypreal_inverse HNatInfinite_FreeUltrafilterNat_iff Infinitesimal_FreeUltrafilterNat_iff2)
10.574 +apply (auto simp add: hypreal_of_hypnat hypreal_inverse
10.575 + HNatInfinite_FreeUltrafilterNat_iff Infinitesimal_FreeUltrafilterNat_iff2)
10.576 apply (rule bexI, rule_tac [2] lemma_hyprel_refl, auto)
10.577 apply (drule_tac x = "m + 1" in spec, ultra)
10.578 done
10.579 -declare HNatInfinite_inverse_Infinitesimal [simp]
10.580 -
10.581 -lemma HNatInfinite_inverse_not_zero: "n \<in> HNatInfinite ==> hypreal_of_hypnat n \<noteq> 0"
10.582 -by (simp add: HNatInfinite_not_eq_zero)
10.583 -
10.584
10.585
10.586 ML
10.587 {*
10.588 val hypnat_of_nat_def = thm"hypnat_of_nat_def";
10.589 -val HNat_def = thm"HNat_def";
10.590 val HNatInfinite_def = thm"HNatInfinite_def";
10.591 val hypreal_of_hypnat_def = thm"hypreal_of_hypnat_def";
10.592 -val SNat_def = thm"SNat_def";
10.593 -val SHNat_def = thm"SHNat_def";
10.594 val hypnat_zero_def = thm"hypnat_zero_def";
10.595 val hypnat_one_def = thm"hypnat_one_def";
10.596 val hypnat_omega_def = thm"hypnat_omega_def";
10.597 @@ -939,7 +829,6 @@
10.598 val lemma_hypnatrel_refl = thm "lemma_hypnatrel_refl";
10.599 val hypnat_empty_not_mem = thm "hypnat_empty_not_mem";
10.600 val Rep_hypnat_nonempty = thm "Rep_hypnat_nonempty";
10.601 -val inj_hypnat_of_nat = thm "inj_hypnat_of_nat";
10.602 val eq_Abs_hypnat = thm "eq_Abs_hypnat";
10.603 val hypnat_add_congruent2 = thm "hypnat_add_congruent2";
10.604 val hypnat_add = thm "hypnat_add";
10.605 @@ -1000,39 +889,14 @@
10.606 val hypnat_of_nat_Suc = thm "hypnat_of_nat_Suc";
10.607 val hypnat_omega = thm "hypnat_omega";
10.608 val Rep_hypnat_omega = thm "Rep_hypnat_omega";
10.609 -val not_ex_hypnat_of_nat_eq_omega = thm "not_ex_hypnat_of_nat_eq_omega";
10.610 -val hypnat_of_nat_not_eq_omega = thm "hypnat_of_nat_not_eq_omega";
10.611 val SHNAT_omega_not_mem = thm "SHNAT_omega_not_mem";
10.612 -val SHNat_add = thm "SHNat_add";
10.613 -val SHNat_minus = thm "SHNat_minus";
10.614 -val SHNat_mult = thm "SHNat_mult";
10.615 -val SHNat_add_cancel = thm "SHNat_add_cancel";
10.616 -val SHNat_hypnat_of_nat = thm "SHNat_hypnat_of_nat";
10.617 -val SHNat_hypnat_of_nat_one = thm "SHNat_hypnat_of_nat_one";
10.618 -val SHNat_hypnat_of_nat_zero = thm "SHNat_hypnat_of_nat_zero";
10.619 -val SHNat_one = thm "SHNat_one";
10.620 -val SHNat_zero = thm "SHNat_zero";
10.621 -val SHNat_iff = thm "SHNat_iff";
10.622 -val SHNat_hypnat_of_nat_iff = thm "SHNat_hypnat_of_nat_iff";
10.623 -val leSuc_Un_eq = thm "leSuc_Un_eq";
10.624 -val finite_nat_le_segment = thm "finite_nat_le_segment";
10.625 -val lemma_unbounded_set = thm "lemma_unbounded_set";
10.626 val cofinite_mem_FreeUltrafilterNat = thm "cofinite_mem_FreeUltrafilterNat";
10.627 -val Compl_Collect_le = thm "Compl_Collect_le";
10.628 val hypnat_omega_gt_SHNat = thm "hypnat_omega_gt_SHNat";
10.629 val hypnat_of_nat_less_whn = thm "hypnat_of_nat_less_whn";
10.630 val hypnat_of_nat_le_whn = thm "hypnat_of_nat_le_whn";
10.631 val hypnat_zero_less_hypnat_omega = thm "hypnat_zero_less_hypnat_omega";
10.632 val hypnat_one_less_hypnat_omega = thm "hypnat_one_less_hypnat_omega";
10.633 val HNatInfinite_whn = thm "HNatInfinite_whn";
10.634 -val SHNat_not_HNatInfinite = thm "SHNat_not_HNatInfinite";
10.635 -val not_HNatInfinite_SHNat = thm "not_HNatInfinite_SHNat";
10.636 -val not_SHNat_HNatInfinite = thm "not_SHNat_HNatInfinite";
10.637 -val HNatInfinite_not_SHNat = thm "HNatInfinite_not_SHNat";
10.638 -val SHNat_not_HNatInfinite_iff = thm "SHNat_not_HNatInfinite_iff";
10.639 -val not_SHNat_HNatInfinite_iff = thm "not_SHNat_HNatInfinite_iff";
10.640 -val SHNat_HNatInfinite_disj = thm "SHNat_HNatInfinite_disj";
10.641 -val HNatInfinite_FreeUltrafilterNat_lemma = thm "HNatInfinite_FreeUltrafilterNat_lemma";
10.642 val HNatInfinite_iff = thm "HNatInfinite_iff";
10.643 val HNatInfinite_FreeUltrafilterNat = thm "HNatInfinite_FreeUltrafilterNat";
10.644 val FreeUltrafilterNat_HNatInfinite = thm "FreeUltrafilterNat_HNatInfinite";
10.645 @@ -1045,26 +909,16 @@
10.646 val HNatInfinite_SHNat_add = thm "HNatInfinite_SHNat_add";
10.647 val HNatInfinite_SHNat_diff = thm "HNatInfinite_SHNat_diff";
10.648 val HNatInfinite_add_one = thm "HNatInfinite_add_one";
10.649 -val HNatInfinite_minus_one = thm "HNatInfinite_minus_one";
10.650 val HNatInfinite_is_Suc = thm "HNatInfinite_is_Suc";
10.651 val HNat_hypreal_of_nat = thm "HNat_hypreal_of_nat";
10.652 -val HNat_add = thm "HNat_add";
10.653 -val HNat_mult = thm "HNat_mult";
10.654 -val lemma_hyprel_FUFN = thm "lemma_hyprel_FUFN";
10.655 val hypreal_of_hypnat = thm "hypreal_of_hypnat";
10.656 -val inj_hypreal_of_hypnat = thm "inj_hypreal_of_hypnat";
10.657 val hypreal_of_hypnat_zero = thm "hypreal_of_hypnat_zero";
10.658 val hypreal_of_hypnat_one = thm "hypreal_of_hypnat_one";
10.659 val hypreal_of_hypnat_add = thm "hypreal_of_hypnat_add";
10.660 val hypreal_of_hypnat_mult = thm "hypreal_of_hypnat_mult";
10.661 val hypreal_of_hypnat_less_iff = thm "hypreal_of_hypnat_less_iff";
10.662 -val hypreal_of_hypnat_eq_zero_iff = thm "hypreal_of_hypnat_eq_zero_iff";
10.663 val hypreal_of_hypnat_ge_zero = thm "hypreal_of_hypnat_ge_zero";
10.664 -val hypnat_eq_zero = thm "hypnat_eq_zero";
10.665 -val hypnat_not_all_eq_zero = thm "hypnat_not_all_eq_zero";
10.666 -val hypnat_le_one_eq_one = thm "hypnat_le_one_eq_one";
10.667 val HNatInfinite_inverse_Infinitesimal = thm "HNatInfinite_inverse_Infinitesimal";
10.668 -val HNatInfinite_inverse_not_zero = thm "HNatInfinite_inverse_not_zero";
10.669 *}
10.670
10.671 end
11.1 --- a/src/HOL/Hyperreal/HyperPow.thy Thu Feb 05 10:45:28 2004 +0100
11.2 +++ b/src/HOL/Hyperreal/HyperPow.thy Tue Feb 10 12:02:11 2004 +0100
11.3 @@ -163,8 +163,8 @@
11.4 lemma hyperpow_not_zero [rule_format (no_asm)]:
11.5 "r \<noteq> (0::hypreal) --> r pow n \<noteq> 0"
11.6 apply (simp (no_asm) add: hypreal_zero_def)
11.7 -apply (rule_tac z = n in eq_Abs_hypnat)
11.8 -apply (rule_tac z = r in eq_Abs_hypreal)
11.9 +apply (rule eq_Abs_hypnat [of n])
11.10 +apply (rule eq_Abs_hypreal [of r])
11.11 apply (auto simp add: hyperpow)
11.12 apply (drule FreeUltrafilterNat_Compl_mem, ultra)
11.13 done
11.14 @@ -172,29 +172,29 @@
11.15 lemma hyperpow_inverse:
11.16 "r \<noteq> (0::hypreal) --> inverse(r pow n) = (inverse r) pow n"
11.17 apply (simp (no_asm) add: hypreal_zero_def)
11.18 -apply (rule_tac z = n in eq_Abs_hypnat)
11.19 -apply (rule_tac z = r in eq_Abs_hypreal)
11.20 +apply (rule eq_Abs_hypnat [of n])
11.21 +apply (rule eq_Abs_hypreal [of r])
11.22 apply (auto dest!: FreeUltrafilterNat_Compl_mem simp add: hypreal_inverse hyperpow)
11.23 apply (rule FreeUltrafilterNat_subset)
11.24 apply (auto dest: realpow_not_zero intro: power_inverse)
11.25 done
11.26
11.27 lemma hyperpow_hrabs: "abs r pow n = abs (r pow n)"
11.28 -apply (rule_tac z = n in eq_Abs_hypnat)
11.29 -apply (rule_tac z = r in eq_Abs_hypreal)
11.30 +apply (rule eq_Abs_hypnat [of n])
11.31 +apply (rule eq_Abs_hypreal [of r])
11.32 apply (auto simp add: hypreal_hrabs hyperpow power_abs [symmetric])
11.33 done
11.34
11.35 lemma hyperpow_add: "r pow (n + m) = (r pow n) * (r pow m)"
11.36 -apply (rule_tac z = n in eq_Abs_hypnat)
11.37 -apply (rule_tac z = m in eq_Abs_hypnat)
11.38 -apply (rule_tac z = r in eq_Abs_hypreal)
11.39 +apply (rule eq_Abs_hypnat [of n])
11.40 +apply (rule eq_Abs_hypnat [of m])
11.41 +apply (rule eq_Abs_hypreal [of r])
11.42 apply (auto simp add: hyperpow hypnat_add hypreal_mult power_add)
11.43 done
11.44
11.45 lemma hyperpow_one: "r pow (1::hypnat) = r"
11.46 apply (unfold hypnat_one_def)
11.47 -apply (rule_tac z = r in eq_Abs_hypreal)
11.48 +apply (rule eq_Abs_hypreal [of r])
11.49 apply (auto simp add: hyperpow)
11.50 done
11.51 declare hyperpow_one [simp]
11.52 @@ -202,38 +202,38 @@
11.53 lemma hyperpow_two:
11.54 "r pow ((1::hypnat) + (1::hypnat)) = r * r"
11.55 apply (unfold hypnat_one_def)
11.56 -apply (rule_tac z = r in eq_Abs_hypreal)
11.57 +apply (rule eq_Abs_hypreal [of r])
11.58 apply (auto simp add: hyperpow hypnat_add hypreal_mult)
11.59 done
11.60
11.61 lemma hyperpow_gt_zero: "(0::hypreal) < r ==> 0 < r pow n"
11.62 apply (simp add: hypreal_zero_def)
11.63 -apply (rule_tac z = n in eq_Abs_hypnat)
11.64 -apply (rule_tac z = r in eq_Abs_hypreal)
11.65 +apply (rule eq_Abs_hypnat [of n])
11.66 +apply (rule eq_Abs_hypreal [of r])
11.67 apply (auto elim!: FreeUltrafilterNat_subset zero_less_power
11.68 simp add: hyperpow hypreal_less hypreal_le)
11.69 done
11.70
11.71 lemma hyperpow_ge_zero: "(0::hypreal) \<le> r ==> 0 \<le> r pow n"
11.72 apply (simp add: hypreal_zero_def)
11.73 -apply (rule_tac z = n in eq_Abs_hypnat)
11.74 -apply (rule_tac z = r in eq_Abs_hypreal)
11.75 +apply (rule eq_Abs_hypnat [of n])
11.76 +apply (rule eq_Abs_hypreal [of r])
11.77 apply (auto elim!: FreeUltrafilterNat_subset zero_le_power
11.78 simp add: hyperpow hypreal_le)
11.79 done
11.80
11.81 lemma hyperpow_le: "[|(0::hypreal) < x; x \<le> y|] ==> x pow n \<le> y pow n"
11.82 apply (simp add: hypreal_zero_def)
11.83 -apply (rule_tac z = n in eq_Abs_hypnat)
11.84 -apply (rule_tac z = x in eq_Abs_hypreal)
11.85 -apply (rule_tac z = y in eq_Abs_hypreal)
11.86 +apply (rule eq_Abs_hypnat [of n])
11.87 +apply (rule eq_Abs_hypreal [of x])
11.88 +apply (rule eq_Abs_hypreal [of y])
11.89 apply (auto simp add: hyperpow hypreal_le hypreal_less)
11.90 apply (erule FreeUltrafilterNat_Int [THEN FreeUltrafilterNat_subset], assumption)
11.91 apply (auto intro: power_mono)
11.92 done
11.93
11.94 lemma hyperpow_eq_one: "1 pow n = (1::hypreal)"
11.95 -apply (rule_tac z = n in eq_Abs_hypnat)
11.96 +apply (rule eq_Abs_hypnat [of n])
11.97 apply (auto simp add: hypreal_one_def hyperpow)
11.98 done
11.99 declare hyperpow_eq_one [simp]
11.100 @@ -241,15 +241,15 @@
11.101 lemma hrabs_hyperpow_minus_one: "abs(-1 pow n) = (1::hypreal)"
11.102 apply (subgoal_tac "abs ((- (1::hypreal)) pow n) = (1::hypreal) ")
11.103 apply simp
11.104 -apply (rule_tac z = n in eq_Abs_hypnat)
11.105 +apply (rule eq_Abs_hypnat [of n])
11.106 apply (auto simp add: hypreal_one_def hyperpow hypreal_minus hypreal_hrabs)
11.107 done
11.108 declare hrabs_hyperpow_minus_one [simp]
11.109
11.110 lemma hyperpow_mult: "(r * s) pow n = (r pow n) * (s pow n)"
11.111 -apply (rule_tac z = n in eq_Abs_hypnat)
11.112 -apply (rule_tac z = r in eq_Abs_hypreal)
11.113 -apply (rule_tac z = s in eq_Abs_hypreal)
11.114 +apply (rule eq_Abs_hypnat [of n])
11.115 +apply (rule eq_Abs_hypreal [of r])
11.116 +apply (rule eq_Abs_hypreal [of s])
11.117 apply (auto simp add: hyperpow hypreal_mult power_mult_distrib)
11.118 done
11.119
11.120 @@ -297,9 +297,9 @@
11.121
11.122 lemma hyperpow_less_le:
11.123 "[|(0::hypreal) \<le> r; r \<le> 1; n < N|] ==> r pow N \<le> r pow n"
11.124 -apply (rule_tac z = n in eq_Abs_hypnat)
11.125 -apply (rule_tac z = N in eq_Abs_hypnat)
11.126 -apply (rule_tac z = r in eq_Abs_hypreal)
11.127 +apply (rule eq_Abs_hypnat [of n])
11.128 +apply (rule eq_Abs_hypnat [of N])
11.129 +apply (rule eq_Abs_hypreal [of r])
11.130 apply (auto simp add: hyperpow hypreal_le hypreal_less hypnat_less
11.131 hypreal_zero_def hypreal_one_def)
11.132 apply (erule FreeUltrafilterNat_Int [THEN FreeUltrafilterNat_subset])
11.133 @@ -314,8 +314,7 @@
11.134
11.135 lemma hyperpow_realpow:
11.136 "(hypreal_of_real r) pow (hypnat_of_nat n) = hypreal_of_real (r ^ n)"
11.137 -apply (unfold hypreal_of_real_def hypnat_of_nat_def)
11.138 -apply (auto simp add: hyperpow)
11.139 +apply (simp add: hypreal_of_real_def hypnat_of_nat_eq hyperpow)
11.140 done
11.141
11.142 lemma hyperpow_SReal: "(hypreal_of_real r) pow (hypnat_of_nat n) \<in> Reals"
11.143 @@ -355,9 +354,8 @@
11.144
11.145 lemma hrealpow_hyperpow_Infinitesimal_iff:
11.146 "(x ^ n \<in> Infinitesimal) = (x pow (hypnat_of_nat n) \<in> Infinitesimal)"
11.147 -apply (unfold hypnat_of_nat_def)
11.148 -apply (rule_tac z = x in eq_Abs_hypreal)
11.149 -apply (auto simp add: hrealpow hyperpow)
11.150 +apply (rule eq_Abs_hypreal [of x])
11.151 +apply (simp add: hrealpow hyperpow hypnat_of_nat_eq)
11.152 done
11.153
11.154 lemma Infinitesimal_hrealpow:
12.1 --- a/src/HOL/Hyperreal/NSA.thy Thu Feb 05 10:45:28 2004 +0100
12.2 +++ b/src/HOL/Hyperreal/NSA.thy Tue Feb 10 12:02:11 2004 +0100
12.3 @@ -33,7 +33,7 @@
12.4 "x @= y == (x + -y) \<in> Infinitesimal"
12.5
12.6
12.7 -defs
12.8 +defs (overloaded)
12.9
12.10 (*standard real numbers as a subset of the hyperreals*)
12.11 SReal_def: "Reals == {x. \<exists>r. x = hypreal_of_real r}"
12.12 @@ -47,7 +47,8 @@
12.13 Closure laws for members of (embedded) set standard real Reals
12.14 --------------------------------------------------------------------*)
12.15
12.16 -lemma SReal_add: "[| (x::hypreal) \<in> Reals; y \<in> Reals |] ==> x + y \<in> Reals"
12.17 +lemma SReal_add [simp]:
12.18 + "[| (x::hypreal) \<in> Reals; y \<in> Reals |] ==> x + y \<in> Reals"
12.19 apply (auto simp add: SReal_def)
12.20 apply (rule_tac x = "r + ra" in exI, simp)
12.21 done
12.22 @@ -1911,6 +1912,11 @@
12.23 apply (blast dest!: reals_Archimedean intro: order_less_trans)
12.24 done
12.25
12.26 +lemma of_nat_in_Reals [simp]: "(of_nat n::hypreal) \<in> \<real>"
12.27 +apply (induct n)
12.28 +apply (simp_all add: SReal_add);
12.29 +done
12.30 +
12.31 lemma lemma_Infinitesimal2: "(\<forall>r \<in> Reals. 0 < r --> x < r) =
12.32 (\<forall>n. x < inverse(hypreal_of_nat (Suc n)))"
12.33 apply safe
12.34 @@ -1918,13 +1924,14 @@
12.35 apply (simp (no_asm_use) add: SReal_inverse)
12.36 apply (rule real_of_nat_Suc_gt_zero [THEN positive_imp_inverse_positive, THEN hypreal_of_real_less_iff [THEN iffD2], THEN [2] impE])
12.37 prefer 2 apply assumption
12.38 -apply (simp add: real_of_nat_Suc_gt_zero hypreal_of_nat_def)
12.39 +apply (simp add: real_of_nat_Suc_gt_zero hypreal_of_nat_eq)
12.40 apply (auto dest!: reals_Archimedean simp add: SReal_iff)
12.41 apply (drule hypreal_of_real_less_iff [THEN iffD2])
12.42 -apply (simp add: real_of_nat_Suc_gt_zero hypreal_of_nat_def)
12.43 +apply (simp add: real_of_nat_Suc_gt_zero hypreal_of_nat_eq)
12.44 apply (blast intro: order_less_trans)
12.45 done
12.46
12.47 +
12.48 lemma Infinitesimal_hypreal_of_nat_iff:
12.49 "Infinitesimal = {x. \<forall>n. abs x < inverse (hypreal_of_nat (Suc n))}"
12.50 apply (simp add: Infinitesimal_def)
13.1 --- a/src/HOL/Hyperreal/NatStar.ML Thu Feb 05 10:45:28 2004 +0100
13.2 +++ b/src/HOL/Hyperreal/NatStar.ML Tue Feb 10 12:02:11 2004 +0100
13.3 @@ -6,6 +6,9 @@
13.4 nat=>nat functions
13.5 *)
13.6
13.7 +val hypnat_of_nat_eq = thm"hypnat_of_nat_eq";
13.8 +val SHNat_eq = thm"SHNat_eq";
13.9 +
13.10 Goalw [starsetNat_def]
13.11 "*sNat*(UNIV::nat set) = (UNIV::hypnat set)";
13.12 by (auto_tac (claset(), simpset() addsimps [FreeUltrafilterNat_Nat_set]));
13.13 @@ -111,28 +114,26 @@
13.14 by (REPEAT(blast_tac (claset() addIs [FreeUltrafilterNat_subset]) 1));
13.15 qed "NatStar_subset";
13.16
13.17 -Goalw [starsetNat_def,hypnat_of_nat_def]
13.18 - "a : A ==> hypnat_of_nat a : *sNat* A";
13.19 +Goal "a : A ==> hypnat_of_nat a : *sNat* A";
13.20 by (auto_tac (claset() addIs [FreeUltrafilterNat_subset],
13.21 - simpset()));
13.22 + simpset() addsimps [starsetNat_def,hypnat_of_nat_eq]));
13.23 qed "NatStar_mem";
13.24
13.25 Goalw [starsetNat_def] "hypnat_of_nat ` A <= *sNat* A";
13.26 -by (auto_tac (claset(), simpset() addsimps [hypnat_of_nat_def]));
13.27 +by (auto_tac (claset(), simpset() addsimps [hypnat_of_nat_eq]));
13.28 by (blast_tac (claset() addIs [FreeUltrafilterNat_subset]) 1);
13.29 qed "NatStar_hypreal_of_real_image_subset";
13.30
13.31 Goal "Nats <= *sNat* (UNIV:: nat set)";
13.32 -by (simp_tac (simpset() addsimps [SHNat_hypnat_of_nat_iff,
13.33 - NatStar_hypreal_of_real_image_subset]) 1);
13.34 +by (auto_tac (claset(), simpset() addsimps [starsetNat_def,SHNat_eq,hypnat_of_nat_eq]));
13.35 qed "NatStar_SHNat_subset";
13.36
13.37 Goalw [starsetNat_def]
13.38 "*sNat* X Int Nats = hypnat_of_nat ` X";
13.39 by (auto_tac (claset(),
13.40 simpset() addsimps
13.41 - [hypnat_of_nat_def,SHNat_def]));
13.42 -by (fold_tac [hypnat_of_nat_def]);
13.43 + [hypnat_of_nat_eq,SHNat_eq]));
13.44 +by (simp_tac (simpset() addsimps [hypnat_of_nat_eq RS sym]) 1);
13.45 by (rtac imageI 1 THEN rtac ccontr 1);
13.46 by (dtac bspec 1);
13.47 by (rtac lemma_hypnatrel_refl 1);
13.48 @@ -289,7 +290,7 @@
13.49
13.50 Goal "( *fNat2* (%x. k)) z = hypnat_of_nat k";
13.51 by (res_inst_tac [("z","z")] eq_Abs_hypnat 1);
13.52 -by (auto_tac (claset(), simpset() addsimps [starfunNat2, hypnat_of_nat_def]));
13.53 +by (auto_tac (claset(), simpset() addsimps [starfunNat2, hypnat_of_nat_eq]));
13.54 qed "starfunNat2_const_fun";
13.55
13.56 Addsimps [starfunNat2_const_fun];
13.57 @@ -312,13 +313,13 @@
13.58
13.59 Goal "( *fNat* f) (hypnat_of_nat a) = hypreal_of_real (f a)";
13.60 by (auto_tac (claset(),
13.61 - simpset() addsimps [starfunNat,hypnat_of_nat_def,hypreal_of_real_def]));
13.62 + simpset() addsimps [starfunNat,hypnat_of_nat_eq,hypreal_of_real_def]));
13.63 qed "starfunNat_eq";
13.64
13.65 Addsimps [starfunNat_eq];
13.66
13.67 Goal "( *fNat2* f) (hypnat_of_nat a) = hypnat_of_nat (f a)";
13.68 -by (auto_tac (claset(), simpset() addsimps [starfunNat2,hypnat_of_nat_def]));
13.69 +by (auto_tac (claset(), simpset() addsimps [starfunNat2,hypnat_of_nat_eq]));
13.70 qed "starfunNat2_eq";
13.71
13.72 Addsimps [starfunNat2_eq];
13.73 @@ -337,7 +338,7 @@
13.74 by (Step_tac 1);
13.75 by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
13.76 by (auto_tac (claset(),
13.77 - simpset() addsimps [starfunNat, hypnat_of_nat_def,hypreal_le,
13.78 + simpset() addsimps [starfunNat, hypnat_of_nat_eq,hypreal_le,
13.79 hypreal_less, hypnat_le,hypnat_less]));
13.80 by (Ultra_tac 1);
13.81 by Auto_tac;
13.82 @@ -349,7 +350,7 @@
13.83 by (Step_tac 1);
13.84 by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
13.85 by (auto_tac (claset(),
13.86 - simpset() addsimps [starfunNat, hypnat_of_nat_def,hypreal_le,
13.87 + simpset() addsimps [starfunNat, hypnat_of_nat_eq,hypreal_le,
13.88 hypreal_less, hypnat_le,hypnat_less]));
13.89 by (Ultra_tac 1);
13.90 by Auto_tac;
13.91 @@ -384,12 +385,12 @@
13.92 Goal "( *fNat* (%n. (X n) ^ m)) N = ( *fNat* X) N pow hypnat_of_nat m";
13.93 by (res_inst_tac [("z","N")] eq_Abs_hypnat 1);
13.94 by (auto_tac (claset(),
13.95 - simpset() addsimps [hyperpow, hypnat_of_nat_def,starfunNat]));
13.96 + simpset() addsimps [hyperpow, hypnat_of_nat_eq,starfunNat]));
13.97 qed "starfunNat_pow2";
13.98
13.99 -Goalw [hypnat_of_nat_def] "( *f* (%r. r ^ n)) R = (R) pow hypnat_of_nat n";
13.100 +Goal "( *f* (%r. r ^ n)) R = (R) pow hypnat_of_nat n";
13.101 by (res_inst_tac [("z","R")] eq_Abs_hypreal 1);
13.102 -by (auto_tac (claset(), simpset() addsimps [hyperpow,starfun]));
13.103 +by (auto_tac (claset(), simpset() addsimps [hyperpow,starfun,hypnat_of_nat_eq]));
13.104 qed "starfun_pow";
13.105
13.106 (*-----------------------------------------------------
13.107 @@ -469,7 +470,7 @@
13.108 qed "starfunNat_n_minus";
13.109
13.110 Goal "( *fNatn* f) (hypnat_of_nat n) = Abs_hypreal(hyprel `` {%i. f i n})";
13.111 -by (auto_tac (claset(), simpset() addsimps [starfunNat_n,hypnat_of_nat_def]));
13.112 +by (auto_tac (claset(), simpset() addsimps [starfunNat_n,hypnat_of_nat_eq]));
13.113 qed "starfunNat_n_eq";
13.114 Addsimps [starfunNat_n_eq];
13.115
13.116 @@ -477,7 +478,7 @@
13.117 by Auto_tac;
13.118 by (rtac ext 1 THEN rtac ccontr 1);
13.119 by (dres_inst_tac [("x","hypnat_of_nat(x)")] fun_cong 1);
13.120 -by (auto_tac (claset(), simpset() addsimps [starfunNat,hypnat_of_nat_def]));
13.121 +by (auto_tac (claset(), simpset() addsimps [starfunNat,hypnat_of_nat_eq]));
13.122 qed "starfun_eq_iff";
13.123
13.124
14.1 --- a/src/HOL/Hyperreal/SEQ.ML Thu Feb 05 10:45:28 2004 +0100
14.2 +++ b/src/HOL/Hyperreal/SEQ.ML Tue Feb 10 12:02:11 2004 +0100
14.3 @@ -4,6 +4,8 @@
14.4 Description : Theory of sequence and series of real numbers
14.5 *)
14.6
14.7 +val Nats_1 = thm"Nats_1";
14.8 +
14.9 fun CLAIM_SIMP str thms =
14.10 prove_goal (the_context()) str
14.11 (fn prems => [cut_facts_tac prems 1,
14.12 @@ -92,7 +94,7 @@
14.13 by (induct_tac "u" 1);
14.14 by (auto_tac (claset(),simpset() addsimps [lemma_NSLIMSEQ2]));
14.15 by (auto_tac (claset() addIs [(lemma_NSLIMSEQ3 RS finite_subset),
14.16 - finite_nat_le_segment], simpset()));
14.17 + rewrite_rule [atMost_def] finite_atMost], simpset()));
14.18 by (dtac lemma_NSLIMSEQ1 1 THEN Step_tac 1);
14.19 by (ALLGOALS(Asm_simp_tac));
14.20 qed "NSLIMSEQ_finite_set";
14.21 @@ -1050,7 +1052,7 @@
14.22 simpset() addsimps [NSCauchy_def, NSLIMSEQ_def,starfunNat_shift_one]));
14.23 by (dtac bspec 1 THEN assume_tac 1);
14.24 by (dtac bspec 1 THEN assume_tac 1);
14.25 -by (dtac (SHNat_one RSN (2,HNatInfinite_SHNat_add)) 1);
14.26 +by (dtac (Nats_1 RSN (2,HNatInfinite_SHNat_add)) 1);
14.27 by (blast_tac (claset() addIs [approx_trans3]) 1);
14.28 qed "NSLIMSEQ_Suc";
14.29
14.30 @@ -1067,7 +1069,7 @@
14.31 simpset() addsimps [NSCauchy_def, NSLIMSEQ_def,starfunNat_shift_one]));
14.32 by (dtac bspec 1 THEN assume_tac 1);
14.33 by (dtac bspec 1 THEN assume_tac 1);
14.34 -by (ftac (SHNat_one RSN (2,HNatInfinite_SHNat_diff)) 1);
14.35 +by (ftac (Nats_1 RSN (2,HNatInfinite_SHNat_diff)) 1);
14.36 by (rotate_tac 2 1);
14.37 by (auto_tac (claset() addSDs [bspec] addIs [approx_trans3],
14.38 simpset()));
15.1 --- a/src/HOL/Hyperreal/Star.thy Thu Feb 05 10:45:28 2004 +0100
15.2 +++ b/src/HOL/Hyperreal/Star.thy Tue Feb 10 12:02:11 2004 +0100
15.3 @@ -456,14 +456,15 @@
15.4 In this theory since hypreal_hrabs proved here. (To Check:) Maybe
15.5 move both if possible?
15.6 -------------------------------------------------------------------*)
15.7 -lemma Infinitesimal_FreeUltrafilterNat_iff2: "(x:Infinitesimal) =
15.8 +lemma Infinitesimal_FreeUltrafilterNat_iff2:
15.9 + "(x:Infinitesimal) =
15.10 (EX X:Rep_hypreal(x).
15.11 ALL m. {n. abs(X n) < inverse(real(Suc m))}
15.12 : FreeUltrafilterNat)"
15.13 -apply (rule_tac z = x in eq_Abs_hypreal)
15.14 +apply (rule eq_Abs_hypreal [of x])
15.15 apply (auto intro!: bexI lemma_hyprel_refl
15.16 - simp add: Infinitesimal_hypreal_of_nat_iff hypreal_of_real_def
15.17 - hypreal_inverse hypreal_hrabs hypreal_less hypreal_of_nat_def)
15.18 + simp add: Infinitesimal_hypreal_of_nat_iff hypreal_of_real_def
15.19 + hypreal_inverse hypreal_hrabs hypreal_less hypreal_of_nat_eq)
15.20 apply (drule_tac x = n in spec, ultra)
15.21 done
15.22
16.1 --- a/src/HOL/Integ/Bin.thy Thu Feb 05 10:45:28 2004 +0100
16.2 +++ b/src/HOL/Integ/Bin.thy Tue Feb 10 12:02:11 2004 +0100
16.3 @@ -8,7 +8,7 @@
16.4
16.5 header{*Arithmetic on Binary Integers*}
16.6
16.7 -theory Bin = Int + Numeral:
16.8 +theory Bin = IntDef + Numeral:
16.9
16.10 text{*The sign @{term Pls} stands for an infinite string of leading Falses.*}
16.11 text{*The sign @{term Min} stands for an infinite string of leading Trues.*}
16.12 @@ -258,7 +258,7 @@
16.13
16.14 lemma eq_number_of_eq:
16.15 "((number_of x::int) = number_of y) =
16.16 - iszero (number_of (bin_add x (bin_minus y)))"
16.17 + iszero (number_of (bin_add x (bin_minus y)) :: int)"
16.18 apply (unfold iszero_def)
16.19 apply (simp add: compare_rls number_of_add number_of_minus)
16.20 done
16.21 @@ -272,14 +272,15 @@
16.22 done
16.23
16.24 lemma iszero_number_of_BIT:
16.25 - "iszero (number_of (w BIT x)) = (~x & iszero (number_of w::int))"
16.26 + "iszero (number_of (w BIT x)::int) = (~x & iszero (number_of w::int))"
16.27 apply (unfold iszero_def)
16.28 apply (cases "(number_of w)::int" rule: int_cases)
16.29 apply (simp_all (no_asm_simp) add: compare_rls zero_reorient
16.30 zminus_zadd_distrib [symmetric] int_Suc0_eq_1 [symmetric] zadd_int)
16.31 done
16.32
16.33 -lemma iszero_number_of_0: "iszero (number_of (w BIT False)) = iszero (number_of w::int)"
16.34 +lemma iszero_number_of_0:
16.35 + "iszero (number_of (w BIT False)::int) = iszero (number_of w::int)"
16.36 by (simp only: iszero_number_of_BIT simp_thms)
16.37
16.38 lemma iszero_number_of_1: "~ iszero (number_of (w BIT True)::int)"
16.39 @@ -291,24 +292,23 @@
16.40
16.41 lemma less_number_of_eq_neg:
16.42 "((number_of x::int) < number_of y)
16.43 - = neg (number_of (bin_add x (bin_minus y)))"
16.44 + = neg (number_of (bin_add x (bin_minus y)) ::int )"
16.45 +by (simp add: neg_def number_of_add number_of_minus compare_rls)
16.46
16.47 -apply (unfold zless_def zdiff_def)
16.48 -apply (simp add: bin_mult_simps)
16.49 -done
16.50
16.51 (*But if Numeral0 is rewritten to 0 then this rule can't be applied:
16.52 Numeral0 IS (number_of Pls) *)
16.53 -lemma not_neg_number_of_Pls: "~ neg (number_of bin.Pls)"
16.54 -by (simp add: neg_eq_less_0)
16.55 +lemma not_neg_number_of_Pls: "~ neg (number_of bin.Pls ::int)"
16.56 +by (simp add: neg_def)
16.57
16.58 -lemma neg_number_of_Min: "neg (number_of bin.Min)"
16.59 -by (simp add: neg_eq_less_0 int_0_less_1)
16.60 +lemma neg_number_of_Min: "neg (number_of bin.Min ::int)"
16.61 +by (simp add: neg_def int_0_less_1)
16.62
16.63 -lemma neg_number_of_BIT: "neg (number_of (w BIT x)) = neg (number_of w)"
16.64 +lemma neg_number_of_BIT:
16.65 + "neg (number_of (w BIT x)::int) = neg (number_of w ::int)"
16.66 apply simp
16.67 apply (cases "(number_of w)::int" rule: int_cases)
16.68 -apply (simp_all (no_asm_simp) add: int_Suc0_eq_1 [symmetric] zadd_int neg_eq_less_0 zdiff_def [symmetric] compare_rls)
16.69 +apply (simp_all (no_asm_simp) add: int_Suc0_eq_1 [symmetric] zadd_int neg_def zdiff_def [symmetric] compare_rls)
16.70 done
16.71
16.72
16.73 @@ -326,9 +326,7 @@
16.74 lemma zabs_number_of:
16.75 "abs(number_of x::int) =
16.76 (if number_of x < (0::int) then -number_of x else number_of x)"
16.77 -apply (unfold zabs_def)
16.78 -apply (rule refl)
16.79 -done
16.80 +by (simp add: zabs_def)
16.81
16.82 (*0 and 1 require special rewrites because they aren't numerals*)
16.83 lemma zabs_0: "abs (0::int) = 0"
17.1 --- a/src/HOL/Integ/Int.thy Thu Feb 05 10:45:28 2004 +0100
17.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
17.3 @@ -1,409 +0,0 @@
17.4 -(* Title: Integ/Int.thy
17.5 - ID: $Id$
17.6 - Author: Lawrence C Paulson, Cambridge University Computer Laboratory
17.7 - Copyright 1998 University of Cambridge
17.8 -*)
17.9 -
17.10 -header {*Type "int" is an Ordered Ring and Other Lemmas*}
17.11 -
17.12 -theory Int = IntDef:
17.13 -
17.14 -constdefs
17.15 - nat :: "int => nat"
17.16 - "nat(Z) == if neg Z then 0 else (THE m. Z = int m)"
17.17 -
17.18 -defs (overloaded)
17.19 - zabs_def: "abs(i::int) == if i < 0 then -i else i"
17.20 -
17.21 -
17.22 -lemma int_0 [simp]: "int 0 = (0::int)"
17.23 -by (simp add: Zero_int_def)
17.24 -
17.25 -lemma int_1 [simp]: "int 1 = 1"
17.26 -by (simp add: One_int_def)
17.27 -
17.28 -lemma int_Suc0_eq_1: "int (Suc 0) = 1"
17.29 -by (simp add: One_int_def One_nat_def)
17.30 -
17.31 -lemma neg_eq_less_0: "neg x = (x < 0)"
17.32 -by (unfold zdiff_def zless_def, auto)
17.33 -
17.34 -lemma not_neg_eq_ge_0: "(~neg x) = (0 \<le> x)"
17.35 -apply (unfold zle_def)
17.36 -apply (simp add: neg_eq_less_0)
17.37 -done
17.38 -
17.39 -subsection{*To simplify inequalities when Numeral1 can get simplified to 1*}
17.40 -
17.41 -lemma not_neg_0: "~ neg 0"
17.42 -by (simp add: One_int_def neg_eq_less_0)
17.43 -
17.44 -lemma not_neg_1: "~ neg 1"
17.45 -by (simp add: One_int_def neg_eq_less_0)
17.46 -
17.47 -lemma iszero_0: "iszero 0"
17.48 -by (simp add: iszero_def)
17.49 -
17.50 -lemma not_iszero_1: "~ iszero 1"
17.51 -by (simp only: Zero_int_def One_int_def One_nat_def iszero_def int_int_eq)
17.52 -
17.53 -
17.54 -subsection{*nat: magnitide of an integer, as a natural number*}
17.55 -
17.56 -lemma nat_int [simp]: "nat(int n) = n"
17.57 -by (unfold nat_def, auto)
17.58 -
17.59 -lemma nat_zero [simp]: "nat 0 = 0"
17.60 -apply (unfold Zero_int_def)
17.61 -apply (rule nat_int)
17.62 -done
17.63 -
17.64 -lemma neg_nat: "neg z ==> nat z = 0"
17.65 -by (unfold nat_def, auto)
17.66 -
17.67 -lemma not_neg_nat: "~ neg z ==> int (nat z) = z"
17.68 -apply (drule not_neg_eq_ge_0 [THEN iffD1])
17.69 -apply (drule zle_imp_zless_or_eq)
17.70 -apply (auto simp add: zless_iff_Suc_zadd)
17.71 -done
17.72 -
17.73 -lemma nat_0_le [simp]: "0 \<le> z ==> int (nat z) = z"
17.74 -by (simp add: neg_eq_less_0 zle_def not_neg_nat)
17.75 -
17.76 -lemma nat_le_0 [simp]: "z \<le> 0 ==> nat z = 0"
17.77 -by (auto simp add: order_le_less neg_eq_less_0 zle_def neg_nat)
17.78 -
17.79 -text{*An alternative condition is @{term "0 \<le> w"} *}
17.80 -lemma nat_mono_iff: "0 < z ==> (nat w < nat z) = (w < z)"
17.81 -apply (subst zless_int [symmetric])
17.82 -apply (simp (no_asm_simp) add: not_neg_nat not_neg_eq_ge_0 order_le_less)
17.83 -apply (case_tac "neg w")
17.84 - apply (simp add: neg_eq_less_0 neg_nat)
17.85 - apply (blast intro: order_less_trans)
17.86 -apply (simp add: not_neg_nat)
17.87 -done
17.88 -
17.89 -lemma zless_nat_conj: "(nat w < nat z) = (0 < z & w < z)"
17.90 -apply (case_tac "0 < z")
17.91 -apply (auto simp add: nat_mono_iff linorder_not_less)
17.92 -done
17.93 -
17.94 -subsection{*Monotonicity results*}
17.95 -
17.96 -text{*Most are available in theory @{text Ring_and_Field}, but they are
17.97 - not yet available: we must prove @{text zadd_zless_mono} before we
17.98 - can prove that the integers are a ring.*}
17.99 -
17.100 -lemma zadd_right_cancel_zless [simp]: "(v+z < w+z) = (v < (w::int))"
17.101 -by (simp add: zless_def zdiff_def zadd_ac)
17.102 -
17.103 -lemma zadd_left_cancel_zless [simp]: "(z+v < z+w) = (v < (w::int))"
17.104 -by (simp add: zless_def zdiff_def zadd_ac)
17.105 -
17.106 -lemma zadd_right_cancel_zle [simp] : "(v+z \<le> w+z) = (v \<le> (w::int))"
17.107 -by (simp add: linorder_not_less [symmetric])
17.108 -
17.109 -lemma zadd_left_cancel_zle [simp] : "(z+v \<le> z+w) = (v \<le> (w::int))"
17.110 -by (simp add: linorder_not_less [symmetric])
17.111 -
17.112 -(*"v\<le>w ==> v+z \<le> w+z"*)
17.113 -lemmas zadd_zless_mono1 = zadd_right_cancel_zless [THEN iffD2, standard]
17.114 -
17.115 -(*"v\<le>w ==> z+v \<le> z+w"*)
17.116 -lemmas zadd_zless_mono2 = zadd_left_cancel_zless [THEN iffD2, standard]
17.117 -
17.118 -(*"v\<le>w ==> v+z \<le> w+z"*)
17.119 -lemmas zadd_zle_mono1 = zadd_right_cancel_zle [THEN iffD2, standard]
17.120 -
17.121 -(*"v\<le>w ==> z+v \<le> z+w"*)
17.122 -lemmas zadd_zle_mono2 = zadd_left_cancel_zle [THEN iffD2, standard]
17.123 -
17.124 -lemma zadd_zle_mono: "[| w'\<le>w; z'\<le>z |] ==> w' + z' \<le> w + (z::int)"
17.125 -by (erule zadd_zle_mono1 [THEN zle_trans], simp)
17.126 -
17.127 -lemma zadd_zless_mono: "[| w'<w; z'\<le>z |] ==> w' + z' < w + (z::int)"
17.128 -by (erule zadd_zless_mono1 [THEN order_less_le_trans], simp)
17.129 -
17.130 -
17.131 -subsection{*Strict Monotonicity of Multiplication*}
17.132 -
17.133 -text{*strict, in 1st argument; proof is by induction on k>0*}
17.134 -lemma zmult_zless_mono2_lemma: "i<j ==> 0<k --> int k * i < int k * j"
17.135 -apply (induct_tac "k", simp)
17.136 -apply (simp add: int_Suc)
17.137 -apply (case_tac "n=0")
17.138 -apply (simp_all add: zadd_zmult_distrib int_Suc0_eq_1 order_le_less)
17.139 -apply (simp_all add: zadd_zless_mono int_Suc0_eq_1 order_le_less)
17.140 -done
17.141 -
17.142 -lemma zmult_zless_mono2: "[| i<j; (0::int) < k |] ==> k*i < k*j"
17.143 -apply (rule_tac t = k in not_neg_nat [THEN subst])
17.144 -apply (erule_tac [2] zmult_zless_mono2_lemma [THEN mp])
17.145 -apply (simp add: not_neg_eq_ge_0 order_le_less)
17.146 -apply (frule conjI [THEN zless_nat_conj [THEN iffD2]], auto)
17.147 -done
17.148 -
17.149 -
17.150 -text{*The Integers Form an Ordered Ring*}
17.151 -instance int :: ordered_ring
17.152 -proof
17.153 - fix i j k :: int
17.154 - show "0 < (1::int)" by (rule int_0_less_1)
17.155 - show "i \<le> j ==> k + i \<le> k + j" by simp
17.156 - show "i < j ==> 0 < k ==> k * i < k * j" by (simp add: zmult_zless_mono2)
17.157 - show "\<bar>i\<bar> = (if i < 0 then -i else i)" by (simp only: zabs_def)
17.158 -qed
17.159 -
17.160 -
17.161 -subsection{*Comparison laws*}
17.162 -
17.163 -text{*Legacy bindings: all are in theory @{text Ring_and_Field}.*}
17.164 -
17.165 -lemma zminus_zless_zminus: "(- x < - y) = (y < (x::int))"
17.166 - by (rule Ring_and_Field.neg_less_iff_less)
17.167 -
17.168 -lemma zminus_zle_zminus: "(- x \<le> - y) = (y \<le> (x::int))"
17.169 - by (rule Ring_and_Field.neg_le_iff_le)
17.170 -
17.171 -
17.172 -text{*The next several equations can make the simplifier loop!*}
17.173 -
17.174 -lemma zless_zminus: "(x < - y) = (y < - (x::int))"
17.175 - by (rule Ring_and_Field.less_minus_iff)
17.176 -
17.177 -lemma zminus_zless: "(- x < y) = (- y < (x::int))"
17.178 - by (rule Ring_and_Field.minus_less_iff)
17.179 -
17.180 -lemma zle_zminus: "(x \<le> - y) = (y \<le> - (x::int))"
17.181 - by (rule Ring_and_Field.le_minus_iff)
17.182 -
17.183 -lemma zminus_zle: "(- x \<le> y) = (- y \<le> (x::int))"
17.184 - by (rule Ring_and_Field.minus_le_iff)
17.185 -
17.186 -lemma equation_zminus: "(x = - y) = (y = - (x::int))"
17.187 - by (rule Ring_and_Field.equation_minus_iff)
17.188 -
17.189 -lemma zminus_equation: "(- x = y) = (- (y::int) = x)"
17.190 - by (rule Ring_and_Field.minus_equation_iff)
17.191 -
17.192 -
17.193 -subsection{*Lemmas about the Function @{term int} and Orderings*}
17.194 -
17.195 -lemma negative_zless_0: "- (int (Suc n)) < 0"
17.196 -by (simp add: zless_def)
17.197 -
17.198 -lemma negative_zless [iff]: "- (int (Suc n)) < int m"
17.199 -by (rule negative_zless_0 [THEN order_less_le_trans], simp)
17.200 -
17.201 -lemma negative_zle_0: "- int n \<le> 0"
17.202 -by (simp add: zminus_zle)
17.203 -
17.204 -lemma negative_zle [iff]: "- int n \<le> int m"
17.205 -by (simp add: zless_def zle_def zdiff_def zadd_int)
17.206 -
17.207 -lemma not_zle_0_negative [simp]: "~(0 \<le> - (int (Suc n)))"
17.208 -by (subst zle_zminus, simp)
17.209 -
17.210 -lemma int_zle_neg: "(int n \<le> - int m) = (n = 0 & m = 0)"
17.211 -apply safe
17.212 -apply (drule_tac [2] zle_zminus [THEN iffD1])
17.213 -apply (auto dest: zle_trans [OF _ negative_zle_0])
17.214 -done
17.215 -
17.216 -lemma not_int_zless_negative [simp]: "~(int n < - int m)"
17.217 -by (simp add: zle_def [symmetric])
17.218 -
17.219 -lemma negative_eq_positive [simp]: "(- int n = int m) = (n = 0 & m = 0)"
17.220 -apply (rule iffI)
17.221 -apply (rule int_zle_neg [THEN iffD1])
17.222 -apply (drule sym)
17.223 -apply (simp_all (no_asm_simp))
17.224 -done
17.225 -
17.226 -lemma zle_iff_zadd: "(w \<le> z) = (\<exists>n. z = w + int n)"
17.227 -by (force intro: exI [of _ "0::nat"]
17.228 - intro!: not_sym [THEN not0_implies_Suc]
17.229 - simp add: zless_iff_Suc_zadd int_le_less)
17.230 -
17.231 -lemma abs_int_eq [simp]: "abs (int m) = int m"
17.232 -by (simp add: zabs_def)
17.233 -
17.234 -text{*This version is proved for all ordered rings, not just integers!
17.235 - It is proved here because attribute @{text arith_split} is not available
17.236 - in theory @{text Ring_and_Field}.
17.237 - But is it really better than just rewriting with @{text abs_if}?*}
17.238 -lemma abs_split [arith_split]:
17.239 - "P(abs(a::'a::ordered_ring)) = ((0 \<le> a --> P a) & (a < 0 --> P(-a)))"
17.240 -by (force dest: order_less_le_trans simp add: abs_if linorder_not_less)
17.241 -
17.242 -
17.243 -subsection{*Misc Results*}
17.244 -
17.245 -lemma nat_zminus_int [simp]: "nat(- (int n)) = 0"
17.246 -apply (unfold nat_def)
17.247 -apply (auto simp add: neg_eq_less_0 zero_reorient zminus_zless)
17.248 -done
17.249 -
17.250 -lemma zless_nat_eq_int_zless: "(m < nat z) = (int m < z)"
17.251 -apply (case_tac "neg z")
17.252 -apply (erule_tac [2] not_neg_nat [THEN subst])
17.253 -apply (auto simp add: neg_nat)
17.254 -apply (auto dest: order_less_trans simp add: neg_eq_less_0)
17.255 -done
17.256 -
17.257 -lemma zless_eq_neg: "(w<z) = neg(w-z)"
17.258 -by (simp add: zless_def)
17.259 -
17.260 -lemma eq_eq_iszero: "(w=z) = iszero(w-z)"
17.261 -by (simp add: iszero_def diff_eq_eq)
17.262 -
17.263 -lemma zle_eq_not_neg: "(w\<le>z) = (~ neg(z-w))"
17.264 -by (simp add: zle_def zless_def)
17.265 -
17.266 -
17.267 -subsection{*Monotonicity of Multiplication*}
17.268 -
17.269 -lemma zmult_zle_mono1: "[| i \<le> j; (0::int) \<le> k |] ==> i*k \<le> j*k"
17.270 - by (rule Ring_and_Field.mult_right_mono)
17.271 -
17.272 -lemma zmult_zle_mono1_neg: "[| i \<le> j; k \<le> (0::int) |] ==> j*k \<le> i*k"
17.273 - by (rule Ring_and_Field.mult_right_mono_neg)
17.274 -
17.275 -lemma zmult_zle_mono2: "[| i \<le> j; (0::int) \<le> k |] ==> k*i \<le> k*j"
17.276 - by (rule Ring_and_Field.mult_left_mono)
17.277 -
17.278 -lemma zmult_zle_mono2_neg: "[| i \<le> j; k \<le> (0::int) |] ==> k*j \<le> k*i"
17.279 - by (rule Ring_and_Field.mult_left_mono_neg)
17.280 -
17.281 -(* \<le> monotonicity, BOTH arguments*)
17.282 -lemma zmult_zle_mono:
17.283 - "[| i \<le> j; k \<le> l; (0::int) \<le> j; (0::int) \<le> k |] ==> i*k \<le> j*l"
17.284 - by (rule Ring_and_Field.mult_mono)
17.285 -
17.286 -lemma zmult_zless_mono1: "[| i<j; (0::int) < k |] ==> i*k < j*k"
17.287 - by (rule Ring_and_Field.mult_strict_right_mono)
17.288 -
17.289 -lemma zmult_zless_mono1_neg: "[| i<j; k < (0::int) |] ==> j*k < i*k"
17.290 - by (rule Ring_and_Field.mult_strict_right_mono_neg)
17.291 -
17.292 -lemma zmult_zless_mono2_neg: "[| i<j; k < (0::int) |] ==> k*j < k*i"
17.293 - by (rule Ring_and_Field.mult_strict_left_mono_neg)
17.294 -
17.295 -lemma zmult_eq_0_iff [iff]: "(m*n = (0::int)) = (m = 0 | n = 0)"
17.296 - by simp
17.297 -
17.298 -lemma zmult_zless_cancel2: "(m*k < n*k) = (((0::int) < k & m<n) | (k<0 & n<m))"
17.299 - by (rule Ring_and_Field.mult_less_cancel_right)
17.300 -
17.301 -lemma zmult_zless_cancel1:
17.302 - "(k*m < k*n) = (((0::int) < k & m<n) | (k < 0 & n<m))"
17.303 - by (rule Ring_and_Field.mult_less_cancel_left)
17.304 -
17.305 -lemma zmult_zle_cancel2:
17.306 - "(m*k \<le> n*k) = (((0::int) < k --> m\<le>n) & (k < 0 --> n\<le>m))"
17.307 - by (rule Ring_and_Field.mult_le_cancel_right)
17.308 -
17.309 -lemma zmult_zle_cancel1:
17.310 - "(k*m \<le> k*n) = (((0::int) < k --> m\<le>n) & (k < 0 --> n\<le>m))"
17.311 - by (rule Ring_and_Field.mult_le_cancel_left)
17.312 -
17.313 -lemma zmult_cancel2: "(m*k = n*k) = (k = (0::int) | m=n)"
17.314 - by (rule Ring_and_Field.mult_cancel_right)
17.315 -
17.316 -lemma zmult_cancel1 [simp]: "(k*m = k*n) = (k = (0::int) | m=n)"
17.317 - by (rule Ring_and_Field.mult_cancel_left)
17.318 -
17.319 -
17.320 -text{*A case theorem distinguishing non-negative and negative int*}
17.321 -
17.322 -lemma negD: "neg x ==> \<exists>n. x = - (int (Suc n))"
17.323 -by (auto simp add: neg_eq_less_0 zless_iff_Suc_zadd
17.324 - diff_eq_eq [symmetric] zdiff_def)
17.325 -
17.326 -lemma int_cases [cases type: int, case_names nonneg neg]:
17.327 - "[|!! n. z = int n ==> P; !! n. z = - (int (Suc n)) ==> P |] ==> P"
17.328 -apply (case_tac "neg z")
17.329 -apply (fast dest!: negD)
17.330 -apply (drule not_neg_nat [symmetric], auto)
17.331 -done
17.332 -
17.333 -lemma int_induct [induct type: int, case_names nonneg neg]:
17.334 - "[|!! n. P (int n); !!n. P (- (int (Suc n))) |] ==> P z"
17.335 - by (cases z) auto
17.336 -
17.337 -
17.338 -(*Legacy ML bindings, but no longer the structure Int.*)
17.339 -ML
17.340 -{*
17.341 -val zabs_def = thm "zabs_def"
17.342 -val nat_def = thm "nat_def"
17.343 -
17.344 -val int_0 = thm "int_0";
17.345 -val int_1 = thm "int_1";
17.346 -val int_Suc0_eq_1 = thm "int_Suc0_eq_1";
17.347 -val neg_eq_less_0 = thm "neg_eq_less_0";
17.348 -val not_neg_eq_ge_0 = thm "not_neg_eq_ge_0";
17.349 -val not_neg_0 = thm "not_neg_0";
17.350 -val not_neg_1 = thm "not_neg_1";
17.351 -val iszero_0 = thm "iszero_0";
17.352 -val not_iszero_1 = thm "not_iszero_1";
17.353 -val int_0_less_1 = thm "int_0_less_1";
17.354 -val int_0_neq_1 = thm "int_0_neq_1";
17.355 -val zless_eq_neg = thm "zless_eq_neg";
17.356 -val eq_eq_iszero = thm "eq_eq_iszero";
17.357 -val zle_eq_not_neg = thm "zle_eq_not_neg";
17.358 -val zadd_right_cancel_zless = thm "zadd_right_cancel_zless";
17.359 -val zadd_left_cancel_zless = thm "zadd_left_cancel_zless";
17.360 -val zadd_right_cancel_zle = thm "zadd_right_cancel_zle";
17.361 -val zadd_left_cancel_zle = thm "zadd_left_cancel_zle";
17.362 -val zadd_zless_mono1 = thm "zadd_zless_mono1";
17.363 -val zadd_zless_mono2 = thm "zadd_zless_mono2";
17.364 -val zadd_zle_mono1 = thm "zadd_zle_mono1";
17.365 -val zadd_zle_mono2 = thm "zadd_zle_mono2";
17.366 -val zadd_zle_mono = thm "zadd_zle_mono";
17.367 -val zadd_zless_mono = thm "zadd_zless_mono";
17.368 -val zminus_zless_zminus = thm "zminus_zless_zminus";
17.369 -val zminus_zle_zminus = thm "zminus_zle_zminus";
17.370 -val zless_zminus = thm "zless_zminus";
17.371 -val zminus_zless = thm "zminus_zless";
17.372 -val zle_zminus = thm "zle_zminus";
17.373 -val zminus_zle = thm "zminus_zle";
17.374 -val equation_zminus = thm "equation_zminus";
17.375 -val zminus_equation = thm "zminus_equation";
17.376 -val negative_zless = thm "negative_zless";
17.377 -val negative_zle = thm "negative_zle";
17.378 -val not_zle_0_negative = thm "not_zle_0_negative";
17.379 -val not_int_zless_negative = thm "not_int_zless_negative";
17.380 -val negative_eq_positive = thm "negative_eq_positive";
17.381 -val zle_iff_zadd = thm "zle_iff_zadd";
17.382 -val abs_int_eq = thm "abs_int_eq";
17.383 -val abs_split = thm"abs_split";
17.384 -val nat_int = thm "nat_int";
17.385 -val nat_zminus_int = thm "nat_zminus_int";
17.386 -val nat_zero = thm "nat_zero";
17.387 -val not_neg_nat = thm "not_neg_nat";
17.388 -val neg_nat = thm "neg_nat";
17.389 -val zless_nat_eq_int_zless = thm "zless_nat_eq_int_zless";
17.390 -val nat_0_le = thm "nat_0_le";
17.391 -val nat_le_0 = thm "nat_le_0";
17.392 -val zless_nat_conj = thm "zless_nat_conj";
17.393 -val int_cases = thm "int_cases";
17.394 -val zmult_zle_mono1 = thm "zmult_zle_mono1";
17.395 -val zmult_zle_mono1_neg = thm "zmult_zle_mono1_neg";
17.396 -val zmult_zle_mono2 = thm "zmult_zle_mono2";
17.397 -val zmult_zle_mono2_neg = thm "zmult_zle_mono2_neg";
17.398 -val zmult_zle_mono = thm "zmult_zle_mono";
17.399 -val zmult_zless_mono2 = thm "zmult_zless_mono2";
17.400 -val zmult_zless_mono1 = thm "zmult_zless_mono1";
17.401 -val zmult_zless_mono1_neg = thm "zmult_zless_mono1_neg";
17.402 -val zmult_zless_mono2_neg = thm "zmult_zless_mono2_neg";
17.403 -val zmult_eq_0_iff = thm "zmult_eq_0_iff";
17.404 -val zmult_zless_cancel2 = thm "zmult_zless_cancel2";
17.405 -val zmult_zless_cancel1 = thm "zmult_zless_cancel1";
17.406 -val zmult_zle_cancel2 = thm "zmult_zle_cancel2";
17.407 -val zmult_zle_cancel1 = thm "zmult_zle_cancel1";
17.408 -val zmult_cancel2 = thm "zmult_cancel2";
17.409 -val zmult_cancel1 = thm "zmult_cancel1";
17.410 -*}
17.411 -
17.412 -end
18.1 --- a/src/HOL/Integ/IntArith.thy Thu Feb 05 10:45:28 2004 +0100
18.2 +++ b/src/HOL/Integ/IntArith.thy Tue Feb 10 12:02:11 2004 +0100
18.3 @@ -12,15 +12,11 @@
18.4 subsection{*Inequality Reasoning for the Arithmetic Simproc*}
18.5
18.6 lemma zless_imp_add1_zle: "w<z ==> w + (1::int) \<le> z"
18.7 - proof (auto simp add: zle_def zless_iff_Suc_zadd)
18.8 - fix m n
18.9 - assume "w + 1 = w + (1 + int m) + (1 + int n)"
18.10 - hence "(w + 1) + (1 + int (m + n)) = (w + 1) + 0"
18.11 - by (simp add: add_ac zadd_int [symmetric])
18.12 - hence "int (Suc(m+n)) = 0"
18.13 - by (simp only: Ring_and_Field.add_left_cancel int_Suc)
18.14 - thus False by (simp only: int_eq_0_conv)
18.15 - qed
18.16 +apply (rule eq_Abs_Integ [of z])
18.17 +apply (rule eq_Abs_Integ [of w])
18.18 +apply (simp add: linorder_not_le [symmetric] zle int_def zadd One_int_def)
18.19 +done
18.20 +
18.21
18.22 use "int_arith1.ML"
18.23 setup int_arith_setup
18.24 @@ -86,11 +82,11 @@
18.25 by (subst nat_eq_iff, simp)
18.26
18.27 lemma nat_less_eq_zless: "0 \<le> w ==> (nat w < nat z) = (w<z)"
18.28 -apply (case_tac "neg z")
18.29 +apply (case_tac "z < 0")
18.30 apply (auto simp add: nat_less_iff)
18.31 -apply (auto intro: zless_trans simp add: neg_eq_less_0 zle_def)
18.32 done
18.33
18.34 +
18.35 lemma nat_le_eq_zle: "0 < w | 0 \<le> z ==> (nat w \<le> nat z) = (w\<le>z)"
18.36 by (auto simp add: linorder_not_less [symmetric] zless_nat_conj)
18.37
18.38 @@ -229,12 +225,12 @@
18.39 lemma zmult_eq_self_iff: "(m = m*(n::int)) = (n = 1 | m = 0)"
18.40 apply auto
18.41 apply (subgoal_tac "m*1 = m*n")
18.42 -apply (drule zmult_cancel1 [THEN iffD1], auto)
18.43 +apply (drule mult_cancel_left [THEN iffD1], auto)
18.44 done
18.45
18.46 lemma zless_1_zmult: "[| 1 < m; 1 < n |] ==> 1 < m*(n::int)"
18.47 apply (rule_tac y = "1*n" in order_less_trans)
18.48 -apply (rule_tac [2] zmult_zless_mono1)
18.49 +apply (rule_tac [2] mult_strict_right_mono)
18.50 apply (simp_all (no_asm_simp))
18.51 done
18.52
19.1 --- a/src/HOL/Integ/IntDef.thy Thu Feb 05 10:45:28 2004 +0100
19.2 +++ b/src/HOL/Integ/IntDef.thy Tue Feb 10 12:02:11 2004 +0100
19.3 @@ -27,13 +27,6 @@
19.4
19.5 int :: "nat => int"
19.6 "int m == Abs_Integ(intrel `` {(m,0)})"
19.7 -
19.8 - neg :: "int => bool"
19.9 - "neg(Z) == \<exists>x y. x<y & (x,y::nat):Rep_Integ(Z)"
19.10 -
19.11 - (*For simplifying equalities*)
19.12 - iszero :: "int => bool"
19.13 - "iszero z == z = (0::int)"
19.14
19.15 defs (overloaded)
19.16
19.17 @@ -48,16 +41,17 @@
19.18 intrel``{(x1+x2, y1+y2)})"
19.19
19.20 zdiff_def: "z - (w::int) == z + (-w)"
19.21 -
19.22 - zless_def: "z<w == neg(z - w)"
19.23 -
19.24 - zle_def: "z <= (w::int) == ~(w < z)"
19.25 -
19.26 zmult_def:
19.27 "z * w ==
19.28 Abs_Integ(\<Union>(x1,y1) \<in> Rep_Integ(z). \<Union>(x2,y2) \<in> Rep_Integ(w).
19.29 intrel``{(x1*x2 + y1*y2, x1*y2 + y1*x2)})"
19.30
19.31 + zless_def: "(z < (w::int)) == (z \<le> w & z \<noteq> w)"
19.32 +
19.33 + zle_def:
19.34 + "z \<le> (w::int) == \<exists>x1 y1 x2 y2. x1 + y2 \<le> x2 + y1 &
19.35 + (x1,y1) \<in> Rep_Integ z & (x2,y2) \<in> Rep_Integ w"
19.36 +
19.37 lemma intrel_iff [simp]: "(((x1,y1),(x2,y2)) \<in> intrel) = (x1+y2 = x2+y1)"
19.38 by (unfold intrel_def, blast)
19.39
19.40 @@ -121,8 +115,8 @@
19.41 done
19.42
19.43 lemma zminus_zminus [simp]: "- (- z) = (z::int)"
19.44 -apply (rule_tac z = z in eq_Abs_Integ)
19.45 -apply (simp (no_asm_simp) add: zminus)
19.46 +apply (rule eq_Abs_Integ [of z])
19.47 +apply (simp add: zminus)
19.48 done
19.49
19.50 lemma inj_zminus: "inj(%z::int. -z)"
19.51 @@ -134,16 +128,6 @@
19.52 by (simp add: int_def Zero_int_def zminus)
19.53
19.54
19.55 -subsection{*neg: the test for negative integers*}
19.56 -
19.57 -
19.58 -lemma not_neg_int [simp]: "~ neg(int n)"
19.59 -by (simp add: neg_def int_def)
19.60 -
19.61 -lemma neg_zminus_int [simp]: "neg(- (int (Suc n)))"
19.62 -by (simp add: neg_def int_def zminus)
19.63 -
19.64 -
19.65 subsection{*zadd: addition on Integ*}
19.66
19.67 lemma zadd:
19.68 @@ -155,22 +139,22 @@
19.69 done
19.70
19.71 lemma zminus_zadd_distrib [simp]: "- (z + w) = (- z) + (- w::int)"
19.72 -apply (rule_tac z = z in eq_Abs_Integ)
19.73 -apply (rule_tac z = w in eq_Abs_Integ)
19.74 -apply (simp (no_asm_simp) add: zminus zadd)
19.75 +apply (rule eq_Abs_Integ [of z])
19.76 +apply (rule eq_Abs_Integ [of w])
19.77 +apply (simp add: zminus zadd)
19.78 done
19.79
19.80 lemma zadd_commute: "(z::int) + w = w + z"
19.81 -apply (rule_tac z = z in eq_Abs_Integ)
19.82 -apply (rule_tac z = w in eq_Abs_Integ)
19.83 -apply (simp (no_asm_simp) add: add_ac zadd)
19.84 +apply (rule eq_Abs_Integ [of z])
19.85 +apply (rule eq_Abs_Integ [of w])
19.86 +apply (simp add: add_ac zadd)
19.87 done
19.88
19.89 lemma zadd_assoc: "((z1::int) + z2) + z3 = z1 + (z2 + z3)"
19.90 -apply (rule_tac z = z1 in eq_Abs_Integ)
19.91 -apply (rule_tac z = z2 in eq_Abs_Integ)
19.92 -apply (rule_tac z = z3 in eq_Abs_Integ)
19.93 -apply (simp (no_asm_simp) add: zadd add_assoc)
19.94 +apply (rule eq_Abs_Integ [of z1])
19.95 +apply (rule eq_Abs_Integ [of z2])
19.96 +apply (rule eq_Abs_Integ [of z3])
19.97 +apply (simp add: zadd add_assoc)
19.98 done
19.99
19.100 (*For AC rewriting*)
19.101 @@ -197,8 +181,8 @@
19.102 (*also for the instance declaration int :: plus_ac0*)
19.103 lemma zadd_0 [simp]: "(0::int) + z = z"
19.104 apply (unfold Zero_int_def int_def)
19.105 -apply (rule_tac z = z in eq_Abs_Integ)
19.106 -apply (simp (no_asm_simp) add: zadd)
19.107 +apply (rule eq_Abs_Integ [of z])
19.108 +apply (simp add: zadd)
19.109 done
19.110
19.111 lemma zadd_0_right [simp]: "z + (0::int) = z"
19.112 @@ -206,8 +190,8 @@
19.113
19.114 lemma zadd_zminus_inverse [simp]: "z + (- z) = (0::int)"
19.115 apply (unfold int_def Zero_int_def)
19.116 -apply (rule_tac z = z in eq_Abs_Integ)
19.117 -apply (simp (no_asm_simp) add: zminus zadd add_commute)
19.118 +apply (rule eq_Abs_Integ [of z])
19.119 +apply (simp add: zminus zadd add_commute)
19.120 done
19.121
19.122 lemma zadd_zminus_inverse2 [simp]: "(- z) + z = (0::int)"
19.123 @@ -236,57 +220,52 @@
19.124 lemma zadd_assoc_cong: "(z::int) + v = z' + v' ==> z + (v + w) = z' + (v' + w)"
19.125 by (simp add: zadd_assoc [symmetric])
19.126
19.127 -lemma zadd_assoc_swap: "(z::int) + (v + w) = v + (z + w)"
19.128 -by (rule zadd_commute [THEN zadd_assoc_cong])
19.129 -
19.130
19.131 subsection{*zmult: multiplication on Integ*}
19.132
19.133 -(*Congruence property for multiplication*)
19.134 +text{*Congruence property for multiplication*}
19.135 lemma zmult_congruent2: "congruent2 intrel
19.136 (%p1 p2. (%(x1,y1). (%(x2,y2).
19.137 intrel``{(x1*x2 + y1*y2, x1*y2 + y1*x2)}) p2) p1)"
19.138 apply (rule equiv_intrel [THEN congruent2_commuteI])
19.139 -apply (rule_tac [2] p=w in PairE)
19.140 -apply (force simp add: add_ac mult_ac, clarify)
19.141 -apply (simp (no_asm_simp) del: equiv_intrel_iff add: add_ac mult_ac)
19.142 + apply (force simp add: add_ac mult_ac)
19.143 +apply (clarify, simp del: equiv_intrel_iff add: add_ac mult_ac)
19.144 apply (rename_tac x1 x2 y1 y2 z1 z2)
19.145 apply (rule equiv_class_eq [OF equiv_intrel intrel_iff [THEN iffD2]])
19.146 -apply (simp add: intrel_def)
19.147 -apply (subgoal_tac "x1*z1 + y2*z1 = y1*z1 + x2*z1 & x1*z2 + y2*z2 = y1*z2 + x2*z2", arith)
19.148 +apply (subgoal_tac "x1*z1 + y2*z1 = y1*z1 + x2*z1 & x1*z2 + y2*z2 = y1*z2 + x2*z2")
19.149 +apply (simp add: mult_ac, arith)
19.150 apply (simp add: add_mult_distrib [symmetric])
19.151 done
19.152
19.153 lemma zmult:
19.154 "Abs_Integ((intrel``{(x1,y1)})) * Abs_Integ((intrel``{(x2,y2)})) =
19.155 Abs_Integ(intrel `` {(x1*x2 + y1*y2, x1*y2 + y1*x2)})"
19.156 -apply (unfold zmult_def)
19.157 -apply (simp (no_asm_simp) add: UN_UN_split_split_eq zmult_congruent2 equiv_intrel [THEN UN_equiv_class2])
19.158 -done
19.159 +by (simp add: zmult_def UN_UN_split_split_eq zmult_congruent2
19.160 + equiv_intrel [THEN UN_equiv_class2])
19.161
19.162 lemma zmult_zminus: "(- z) * w = - (z * (w::int))"
19.163 -apply (rule_tac z = z in eq_Abs_Integ)
19.164 -apply (rule_tac z = w in eq_Abs_Integ)
19.165 -apply (simp (no_asm_simp) add: zminus zmult add_ac)
19.166 +apply (rule eq_Abs_Integ [of z])
19.167 +apply (rule eq_Abs_Integ [of w])
19.168 +apply (simp add: zminus zmult add_ac)
19.169 done
19.170
19.171 lemma zmult_commute: "(z::int) * w = w * z"
19.172 -apply (rule_tac z = z in eq_Abs_Integ)
19.173 -apply (rule_tac z = w in eq_Abs_Integ)
19.174 -apply (simp (no_asm_simp) add: zmult add_ac mult_ac)
19.175 +apply (rule eq_Abs_Integ [of z])
19.176 +apply (rule eq_Abs_Integ [of w])
19.177 +apply (simp add: zmult add_ac mult_ac)
19.178 done
19.179
19.180 lemma zmult_assoc: "((z1::int) * z2) * z3 = z1 * (z2 * z3)"
19.181 -apply (rule_tac z = z1 in eq_Abs_Integ)
19.182 -apply (rule_tac z = z2 in eq_Abs_Integ)
19.183 -apply (rule_tac z = z3 in eq_Abs_Integ)
19.184 -apply (simp (no_asm_simp) add: add_mult_distrib2 zmult add_ac mult_ac)
19.185 +apply (rule eq_Abs_Integ [of z1])
19.186 +apply (rule eq_Abs_Integ [of z2])
19.187 +apply (rule eq_Abs_Integ [of z3])
19.188 +apply (simp add: add_mult_distrib2 zmult add_ac mult_ac)
19.189 done
19.190
19.191 lemma zadd_zmult_distrib: "((z1::int) + z2) * w = (z1 * w) + (z2 * w)"
19.192 -apply (rule_tac z = z1 in eq_Abs_Integ)
19.193 -apply (rule_tac z = z2 in eq_Abs_Integ)
19.194 -apply (rule_tac z = w in eq_Abs_Integ)
19.195 +apply (rule eq_Abs_Integ [of z1])
19.196 +apply (rule eq_Abs_Integ [of z2])
19.197 +apply (rule eq_Abs_Integ [of w])
19.198 apply (simp add: add_mult_distrib2 zadd zmult add_ac mult_ac)
19.199 done
19.200
19.201 @@ -314,14 +293,14 @@
19.202
19.203 lemma zmult_0 [simp]: "0 * z = (0::int)"
19.204 apply (unfold Zero_int_def int_def)
19.205 -apply (rule_tac z = z in eq_Abs_Integ)
19.206 -apply (simp (no_asm_simp) add: zmult)
19.207 +apply (rule eq_Abs_Integ [of z])
19.208 +apply (simp add: zmult)
19.209 done
19.210
19.211 lemma zmult_1 [simp]: "(1::int) * z = z"
19.212 apply (unfold One_int_def int_def)
19.213 -apply (rule_tac z = z in eq_Abs_Integ)
19.214 -apply (simp (no_asm_simp) add: zmult)
19.215 +apply (rule eq_Abs_Integ [of z])
19.216 +apply (simp add: zmult)
19.217 done
19.218
19.219 lemma zmult_0_right [simp]: "z * 0 = (0::int)"
19.220 @@ -352,64 +331,73 @@
19.221 qed
19.222
19.223
19.224 -subsection{*Theorems about the Ordering*}
19.225 +subsection{*The @{text "\<le>"} Ordering*}
19.226 +
19.227 +lemma zle:
19.228 + "(Abs_Integ(intrel``{(x1,y1)}) \<le> Abs_Integ(intrel``{(x2,y2)})) =
19.229 + (x1 + y2 \<le> x2 + y1)"
19.230 +by (force simp add: zle_def)
19.231 +
19.232 +lemma zle_refl: "w \<le> (w::int)"
19.233 +apply (rule eq_Abs_Integ [of w])
19.234 +apply (force simp add: zle)
19.235 +done
19.236 +
19.237 +lemma zle_trans: "[| i \<le> j; j \<le> k |] ==> i \<le> (k::int)"
19.238 +apply (rule eq_Abs_Integ [of i])
19.239 +apply (rule eq_Abs_Integ [of j])
19.240 +apply (rule eq_Abs_Integ [of k])
19.241 +apply (simp add: zle)
19.242 +done
19.243 +
19.244 +lemma zle_anti_sym: "[| z \<le> w; w \<le> z |] ==> z = (w::int)"
19.245 +apply (rule eq_Abs_Integ [of w])
19.246 +apply (rule eq_Abs_Integ [of z])
19.247 +apply (simp add: zle)
19.248 +done
19.249 +
19.250 +(* Axiom 'order_less_le' of class 'order': *)
19.251 +lemma zless_le: "((w::int) < z) = (w \<le> z & w \<noteq> z)"
19.252 +by (simp add: zless_def)
19.253 +
19.254 +instance int :: order
19.255 +proof qed
19.256 + (assumption |
19.257 + rule zle_refl zle_trans zle_anti_sym zless_le)+
19.258 +
19.259 +(* Axiom 'linorder_linear' of class 'linorder': *)
19.260 +lemma zle_linear: "(z::int) \<le> w | w \<le> z"
19.261 +apply (rule eq_Abs_Integ [of z])
19.262 +apply (rule eq_Abs_Integ [of w])
19.263 +apply (simp add: zle linorder_linear)
19.264 +done
19.265 +
19.266 +instance int :: plus_ac0
19.267 +proof qed (rule zadd_commute zadd_assoc zadd_0)+
19.268 +
19.269 +instance int :: linorder
19.270 +proof qed (rule zle_linear)
19.271 +
19.272 +
19.273 +lemmas zless_linear = linorder_less_linear [where 'a = int]
19.274 +
19.275 +
19.276 +lemma int_eq_0_conv [simp]: "(int n = 0) = (n = 0)"
19.277 +by (simp add: Zero_int_def)
19.278
19.279 (*This lemma allows direct proofs of other <-properties*)
19.280 lemma zless_iff_Suc_zadd:
19.281 "(w < z) = (\<exists>n. z = w + int(Suc n))"
19.282 -apply (unfold zless_def neg_def zdiff_def int_def)
19.283 -apply (rule_tac z = z in eq_Abs_Integ)
19.284 -apply (rule_tac z = w in eq_Abs_Integ, clarify)
19.285 -apply (simp add: zadd zminus)
19.286 +apply (rule eq_Abs_Integ [of z])
19.287 +apply (rule eq_Abs_Integ [of w])
19.288 +apply (simp add: linorder_not_le [where 'a = int, symmetric]
19.289 + linorder_not_le [where 'a = nat]
19.290 + zle int_def zdiff_def zadd zminus)
19.291 apply (safe dest!: less_imp_Suc_add)
19.292 apply (rule_tac x = k in exI)
19.293 apply (simp_all add: add_ac)
19.294 done
19.295
19.296 -lemma zless_zadd_Suc: "z < z + int (Suc n)"
19.297 -by (auto simp add: zless_iff_Suc_zadd zadd_assoc zadd_int)
19.298 -
19.299 -lemma zless_trans: "[| z1<z2; z2<z3 |] ==> z1 < (z3::int)"
19.300 -by (auto simp add: zless_iff_Suc_zadd zadd_assoc zadd_int)
19.301 -
19.302 -lemma zless_not_sym: "!!w::int. z<w ==> ~w<z"
19.303 -apply (safe dest!: zless_iff_Suc_zadd [THEN iffD1])
19.304 -apply (rule_tac z = z in eq_Abs_Integ, safe)
19.305 -apply (simp add: int_def zadd)
19.306 -done
19.307 -
19.308 -(* [| n<m; ~P ==> m<n |] ==> P *)
19.309 -lemmas zless_asym = zless_not_sym [THEN swap, standard]
19.310 -
19.311 -lemma zless_not_refl: "!!z::int. ~ z<z"
19.312 -apply (rule zless_asym [THEN notI])
19.313 -apply (assumption+)
19.314 -done
19.315 -
19.316 -(* z<z ==> R *)
19.317 -lemmas zless_irrefl = zless_not_refl [THEN notE, standard, elim!]
19.318 -
19.319 -
19.320 -(*"Less than" is a linear ordering*)
19.321 -lemma zless_linear:
19.322 - "z<w | z=w | w<(z::int)"
19.323 -apply (unfold zless_def neg_def zdiff_def)
19.324 -apply (rule_tac z = z in eq_Abs_Integ)
19.325 -apply (rule_tac z = w in eq_Abs_Integ, safe)
19.326 -apply (simp add: zadd zminus Image_iff Bex_def)
19.327 -apply (rule_tac m1 = "x+ya" and n1 = "xa+y" in less_linear [THEN disjE])
19.328 -apply (force simp add: add_ac)+
19.329 -done
19.330 -
19.331 -lemma int_neq_iff: "!!w::int. (w ~= z) = (w<z | z<w)"
19.332 -by (cut_tac zless_linear, blast)
19.333 -
19.334 -(*** eliminates ~= in premises ***)
19.335 -lemmas int_neqE = int_neq_iff [THEN iffD1, THEN disjE, standard]
19.336 -
19.337 -lemma int_eq_0_conv [simp]: "(int n = 0) = (n = 0)"
19.338 -by (simp add: Zero_int_def)
19.339 -
19.340 lemma zless_int [simp]: "(int m < int n) = (m<n)"
19.341 by (simp add: less_iff_Suc_add zless_iff_Suc_zadd zadd_int)
19.342
19.343 @@ -425,84 +413,553 @@
19.344 lemma int_0_neq_1 [simp]: "0 \<noteq> (1::int)"
19.345 by (simp only: Zero_int_def One_int_def One_nat_def int_int_eq)
19.346
19.347 +lemma zle_int [simp]: "(int m \<le> int n) = (m\<le>n)"
19.348 +by (simp add: linorder_not_less [symmetric])
19.349
19.350 -subsection{*Properties of the @{text "\<le>"} Relation*}
19.351 -
19.352 -lemma zle_int [simp]: "(int m <= int n) = (m<=n)"
19.353 -by (simp add: zle_def le_def)
19.354 -
19.355 -lemma zero_zle_int [simp]: "(0 <= int n)"
19.356 +lemma zero_zle_int [simp]: "(0 \<le> int n)"
19.357 by (simp add: Zero_int_def)
19.358
19.359 -lemma int_le_0_conv [simp]: "(int n <= 0) = (n = 0)"
19.360 +lemma int_le_0_conv [simp]: "(int n \<le> 0) = (n = 0)"
19.361 by (simp add: Zero_int_def)
19.362
19.363 -lemma zle_imp_zless_or_eq: "z <= w ==> z < w | z=(w::int)"
19.364 -apply (unfold zle_def)
19.365 -apply (cut_tac zless_linear)
19.366 -apply (blast elim: zless_asym)
19.367 +lemma int_0 [simp]: "int 0 = (0::int)"
19.368 +by (simp add: Zero_int_def)
19.369 +
19.370 +lemma int_1 [simp]: "int 1 = 1"
19.371 +by (simp add: One_int_def)
19.372 +
19.373 +lemma int_Suc0_eq_1: "int (Suc 0) = 1"
19.374 +by (simp add: One_int_def One_nat_def)
19.375 +
19.376 +subsection{*Monotonicity results*}
19.377 +
19.378 +lemma zadd_left_mono: "i \<le> j ==> k + i \<le> k + (j::int)"
19.379 +apply (rule eq_Abs_Integ [of i])
19.380 +apply (rule eq_Abs_Integ [of j])
19.381 +apply (rule eq_Abs_Integ [of k])
19.382 +apply (simp add: zle zadd)
19.383 done
19.384
19.385 -lemma zless_or_eq_imp_zle: "z<w | z=w ==> z <= (w::int)"
19.386 -apply (unfold zle_def)
19.387 -apply (cut_tac zless_linear)
19.388 -apply (blast elim: zless_asym)
19.389 +lemma zadd_strict_right_mono: "i < j ==> i + k < j + (k::int)"
19.390 +apply (rule eq_Abs_Integ [of i])
19.391 +apply (rule eq_Abs_Integ [of j])
19.392 +apply (rule eq_Abs_Integ [of k])
19.393 +apply (simp add: linorder_not_le [where 'a = int, symmetric]
19.394 + linorder_not_le [where 'a = nat] zle zadd)
19.395 done
19.396
19.397 -lemma int_le_less: "(x <= (y::int)) = (x < y | x=y)"
19.398 -apply (rule iffI)
19.399 -apply (erule zle_imp_zless_or_eq)
19.400 -apply (erule zless_or_eq_imp_zle)
19.401 +lemma zadd_zless_mono: "[| w'<w; z'\<le>z |] ==> w' + z' < w + (z::int)"
19.402 +by (rule order_less_le_trans [OF zadd_strict_right_mono zadd_left_mono])
19.403 +
19.404 +
19.405 +subsection{*Strict Monotonicity of Multiplication*}
19.406 +
19.407 +text{*strict, in 1st argument; proof is by induction on k>0*}
19.408 +lemma zmult_zless_mono2_lemma [rule_format]:
19.409 + "i<j ==> 0<k --> int k * i < int k * j"
19.410 +apply (induct_tac "k", simp)
19.411 +apply (simp add: int_Suc)
19.412 +apply (case_tac "n=0")
19.413 +apply (simp_all add: zadd_zmult_distrib int_Suc0_eq_1 order_le_less)
19.414 +apply (simp add: zadd_zless_mono int_Suc0_eq_1 order_le_less)
19.415 done
19.416
19.417 -lemma zle_refl: "w <= (w::int)"
19.418 -by (simp add: int_le_less)
19.419 -
19.420 -(* Axiom 'linorder_linear' of class 'linorder': *)
19.421 -lemma zle_linear: "(z::int) <= w | w <= z"
19.422 -apply (simp add: int_le_less)
19.423 -apply (cut_tac zless_linear, blast)
19.424 +lemma zero_le_imp_eq_int: "0 \<le> k ==> \<exists>n. k = int n"
19.425 +apply (rule eq_Abs_Integ [of k])
19.426 +apply (auto simp add: zle zadd int_def Zero_int_def)
19.427 +apply (rule_tac x="x-y" in exI, simp)
19.428 done
19.429
19.430 -(* Axiom 'order_trans of class 'order': *)
19.431 -lemma zle_trans: "[| i <= j; j <= k |] ==> i <= (k::int)"
19.432 -apply (drule zle_imp_zless_or_eq)
19.433 -apply (drule zle_imp_zless_or_eq)
19.434 -apply (rule zless_or_eq_imp_zle)
19.435 -apply (blast intro: zless_trans)
19.436 +lemma zmult_zless_mono2: "[| i<j; (0::int) < k |] ==> k*i < k*j"
19.437 +apply (frule order_less_imp_le [THEN zero_le_imp_eq_int])
19.438 +apply (auto simp add: zmult_zless_mono2_lemma)
19.439 done
19.440
19.441 -lemma zle_anti_sym: "[| z <= w; w <= z |] ==> z = (w::int)"
19.442 -apply (drule zle_imp_zless_or_eq)
19.443 -apply (drule zle_imp_zless_or_eq)
19.444 -apply (blast elim: zless_asym)
19.445 +
19.446 +defs (overloaded)
19.447 + zabs_def: "abs(i::int) == if i < 0 then -i else i"
19.448 +
19.449 +
19.450 +text{*The Integers Form an Ordered Ring*}
19.451 +instance int :: ordered_ring
19.452 +proof
19.453 + fix i j k :: int
19.454 + show "0 < (1::int)" by (rule int_0_less_1)
19.455 + show "i \<le> j ==> k + i \<le> k + j" by (rule zadd_left_mono)
19.456 + show "i < j ==> 0 < k ==> k * i < k * j" by (rule zmult_zless_mono2)
19.457 + show "\<bar>i\<bar> = (if i < 0 then -i else i)" by (simp only: zabs_def)
19.458 +qed
19.459 +
19.460 +
19.461 +subsection{*Magnitide of an Integer, as a Natural Number: @{term nat}*}
19.462 +
19.463 +constdefs
19.464 + nat :: "int => nat"
19.465 + "nat(Z) == if Z<0 then 0 else (THE m. Z = int m)"
19.466 +
19.467 +lemma nat_int [simp]: "nat(int n) = n"
19.468 +by (unfold nat_def, auto)
19.469 +
19.470 +lemma nat_zero [simp]: "nat 0 = 0"
19.471 +apply (unfold Zero_int_def)
19.472 +apply (rule nat_int)
19.473 done
19.474
19.475 -(* Axiom 'order_less_le' of class 'order': *)
19.476 -lemma int_less_le: "((w::int) < z) = (w <= z & w ~= z)"
19.477 -apply (simp add: zle_def int_neq_iff)
19.478 -apply (blast elim!: zless_asym)
19.479 +lemma nat_0_le [simp]: "0 \<le> z ==> int (nat z) = z"
19.480 +apply (rule eq_Abs_Integ [of z])
19.481 +apply (simp add: nat_def linorder_not_le [symmetric] zle int_def Zero_int_def)
19.482 +apply (subgoal_tac "(THE m. x = m + y) = x-y")
19.483 +apply (auto simp add: the_equality)
19.484 done
19.485
19.486 -instance int :: order
19.487 -proof qed (assumption | rule zle_refl zle_trans zle_anti_sym int_less_le)+
19.488 +lemma nat_le_0 [simp]: "z \<le> 0 ==> nat z = 0"
19.489 +by (simp add: nat_def order_less_le eq_commute [of 0])
19.490
19.491 -instance int :: plus_ac0
19.492 -proof qed (rule zadd_commute zadd_assoc zadd_0)+
19.493 +text{*An alternative condition is @{term "0 \<le> w"} *}
19.494 +lemma nat_mono_iff: "0 < z ==> (nat w < nat z) = (w < z)"
19.495 +apply (subst zless_int [symmetric])
19.496 +apply (simp add: order_le_less)
19.497 +apply (case_tac "w < 0")
19.498 + apply (simp add: order_less_imp_le)
19.499 + apply (blast intro: order_less_trans)
19.500 +apply (simp add: linorder_not_less)
19.501 +done
19.502
19.503 -instance int :: linorder
19.504 -proof qed (rule zle_linear)
19.505 +lemma zless_nat_conj: "(nat w < nat z) = (0 < z & w < z)"
19.506 +apply (case_tac "0 < z")
19.507 +apply (auto simp add: nat_mono_iff linorder_not_less)
19.508 +done
19.509
19.510
19.511 -lemma zadd_left_cancel [simp]: "!!w::int. (z + w' = z + w) = (w' = w)"
19.512 - by (rule add_left_cancel)
19.513 +subsection{*Lemmas about the Function @{term int} and Orderings*}
19.514
19.515 +lemma negative_zless_0: "- (int (Suc n)) < 0"
19.516 +by (simp add: zless_def)
19.517
19.518 +lemma negative_zless [iff]: "- (int (Suc n)) < int m"
19.519 +by (rule negative_zless_0 [THEN order_less_le_trans], simp)
19.520 +
19.521 +lemma negative_zle_0: "- int n \<le> 0"
19.522 +by (simp add: minus_le_iff)
19.523 +
19.524 +lemma negative_zle [iff]: "- int n \<le> int m"
19.525 +by (rule order_trans [OF negative_zle_0 zero_zle_int])
19.526 +
19.527 +lemma not_zle_0_negative [simp]: "~ (0 \<le> - (int (Suc n)))"
19.528 +by (subst le_minus_iff, simp)
19.529 +
19.530 +lemma int_zle_neg: "(int n \<le> - int m) = (n = 0 & m = 0)"
19.531 +apply safe
19.532 +apply (drule_tac [2] le_minus_iff [THEN iffD1])
19.533 +apply (auto dest: zle_trans [OF _ negative_zle_0])
19.534 +done
19.535 +
19.536 +lemma not_int_zless_negative [simp]: "~ (int n < - int m)"
19.537 +by (simp add: linorder_not_less)
19.538 +
19.539 +lemma negative_eq_positive [simp]: "(- int n = int m) = (n = 0 & m = 0)"
19.540 +by (force simp add: order_eq_iff [of "- int n"] int_zle_neg)
19.541 +
19.542 +lemma zle_iff_zadd: "(w \<le> z) = (\<exists>n. z = w + int n)"
19.543 +by (force intro: exI [of _ "0::nat"]
19.544 + intro!: not_sym [THEN not0_implies_Suc]
19.545 + simp add: zless_iff_Suc_zadd order_le_less)
19.546 +
19.547 +
19.548 +text{*This version is proved for all ordered rings, not just integers!
19.549 + It is proved here because attribute @{text arith_split} is not available
19.550 + in theory @{text Ring_and_Field}.
19.551 + But is it really better than just rewriting with @{text abs_if}?*}
19.552 +lemma abs_split [arith_split]:
19.553 + "P(abs(a::'a::ordered_ring)) = ((0 \<le> a --> P a) & (a < 0 --> P(-a)))"
19.554 +by (force dest: order_less_le_trans simp add: abs_if linorder_not_less)
19.555 +
19.556 +lemma abs_int_eq [simp]: "abs (int m) = int m"
19.557 +by (simp add: zabs_def)
19.558 +
19.559 +
19.560 +subsection{*Misc Results*}
19.561 +
19.562 +lemma nat_zminus_int [simp]: "nat(- (int n)) = 0"
19.563 +by (auto simp add: nat_def zero_reorient minus_less_iff)
19.564 +
19.565 +lemma zless_nat_eq_int_zless: "(m < nat z) = (int m < z)"
19.566 +apply (case_tac "0 \<le> z")
19.567 +apply (erule nat_0_le [THEN subst], simp)
19.568 +apply (simp add: linorder_not_le)
19.569 +apply (auto dest: order_less_trans simp add: order_less_imp_le)
19.570 +done
19.571 +
19.572 +
19.573 +
19.574 +subsection{*Monotonicity of Multiplication*}
19.575 +
19.576 +lemma zmult_zle_mono2: "[| i \<le> j; (0::int) \<le> k |] ==> k*i \<le> k*j"
19.577 + by (rule Ring_and_Field.mult_left_mono)
19.578 +
19.579 +lemma zmult_zless_cancel2: "(m*k < n*k) = (((0::int) < k & m<n) | (k<0 & n<m))"
19.580 + by (rule Ring_and_Field.mult_less_cancel_right)
19.581 +
19.582 +lemma zmult_zless_cancel1:
19.583 + "(k*m < k*n) = (((0::int) < k & m<n) | (k < 0 & n<m))"
19.584 + by (rule Ring_and_Field.mult_less_cancel_left)
19.585 +
19.586 +lemma zmult_zle_cancel1:
19.587 + "(k*m \<le> k*n) = (((0::int) < k --> m\<le>n) & (k < 0 --> n\<le>m))"
19.588 + by (rule Ring_and_Field.mult_le_cancel_left)
19.589 +
19.590 +
19.591 +
19.592 +text{*A case theorem distinguishing non-negative and negative int*}
19.593 +
19.594 +lemma negD: "x<0 ==> \<exists>n. x = - (int (Suc n))"
19.595 +by (auto simp add: zless_iff_Suc_zadd
19.596 + diff_eq_eq [symmetric] zdiff_def)
19.597 +
19.598 +lemma int_cases [cases type: int, case_names nonneg neg]:
19.599 + "[|!! n. z = int n ==> P; !! n. z = - (int (Suc n)) ==> P |] ==> P"
19.600 +apply (case_tac "z < 0", blast dest!: negD)
19.601 +apply (simp add: linorder_not_less)
19.602 +apply (blast dest: nat_0_le [THEN sym])
19.603 +done
19.604 +
19.605 +lemma int_induct [induct type: int, case_names nonneg neg]:
19.606 + "[|!! n. P (int n); !!n. P (- (int (Suc n))) |] ==> P z"
19.607 + by (cases z) auto
19.608 +
19.609 +
19.610 +subsection{*The Constants @{term neg} and @{term iszero}*}
19.611 +
19.612 +constdefs
19.613 +
19.614 + neg :: "'a::ordered_ring => bool"
19.615 + "neg(Z) == Z < 0"
19.616 +
19.617 + (*For simplifying equalities*)
19.618 + iszero :: "'a::semiring => bool"
19.619 + "iszero z == z = (0)"
19.620 +
19.621 +
19.622 +lemma not_neg_int [simp]: "~ neg(int n)"
19.623 +by (simp add: neg_def)
19.624 +
19.625 +lemma neg_zminus_int [simp]: "neg(- (int (Suc n)))"
19.626 +by (simp add: neg_def neg_less_0_iff_less)
19.627 +
19.628 +lemmas neg_eq_less_0 = neg_def
19.629 +
19.630 +lemma not_neg_eq_ge_0: "(~neg x) = (0 \<le> x)"
19.631 +by (simp add: neg_def linorder_not_less)
19.632 +
19.633 +subsection{*To simplify inequalities when Numeral1 can get simplified to 1*}
19.634 +
19.635 +lemma not_neg_0: "~ neg 0"
19.636 +by (simp add: One_int_def neg_def)
19.637 +
19.638 +lemma not_neg_1: "~ neg 1"
19.639 +by (simp add: neg_def linorder_not_less zero_le_one)
19.640 +
19.641 +lemma iszero_0: "iszero 0"
19.642 +by (simp add: iszero_def)
19.643 +
19.644 +lemma not_iszero_1: "~ iszero 1"
19.645 +by (simp add: iszero_def eq_commute)
19.646 +
19.647 +lemma neg_nat: "neg z ==> nat z = 0"
19.648 +by (simp add: nat_def neg_def)
19.649 +
19.650 +lemma not_neg_nat: "~ neg z ==> int (nat z) = z"
19.651 +by (simp add: linorder_not_less neg_def)
19.652 +
19.653 +
19.654 +subsection{*Embedding of the Naturals into any Semiring: @{term of_nat}*}
19.655 +
19.656 +consts of_nat :: "nat => 'a::semiring"
19.657 +
19.658 +primrec
19.659 + of_nat_0: "of_nat 0 = 0"
19.660 + of_nat_Suc: "of_nat (Suc m) = of_nat m + 1"
19.661 +
19.662 +lemma of_nat_1 [simp]: "of_nat 1 = 1"
19.663 +by simp
19.664 +
19.665 +lemma of_nat_add [simp]: "of_nat (m+n) = of_nat m + of_nat n"
19.666 +apply (induct m)
19.667 +apply (simp_all add: add_ac)
19.668 +done
19.669 +
19.670 +lemma of_nat_mult [simp]: "of_nat (m*n) = of_nat m * of_nat n"
19.671 +apply (induct m)
19.672 +apply (simp_all add: mult_ac add_ac right_distrib)
19.673 +done
19.674 +
19.675 +lemma zero_le_imp_of_nat: "0 \<le> (of_nat m::'a::ordered_semiring)"
19.676 +apply (induct m, simp_all)
19.677 +apply (erule order_trans)
19.678 +apply (rule less_add_one [THEN order_less_imp_le])
19.679 +done
19.680 +
19.681 +lemma less_imp_of_nat_less:
19.682 + "m < n ==> of_nat m < (of_nat n::'a::ordered_semiring)"
19.683 +apply (induct m n rule: diff_induct, simp_all)
19.684 +apply (insert add_le_less_mono [OF zero_le_imp_of_nat zero_less_one], force)
19.685 +done
19.686 +
19.687 +lemma of_nat_less_imp_less:
19.688 + "of_nat m < (of_nat n::'a::ordered_semiring) ==> m < n"
19.689 +apply (induct m n rule: diff_induct, simp_all)
19.690 +apply (insert zero_le_imp_of_nat)
19.691 +apply (force simp add: linorder_not_less [symmetric])
19.692 +done
19.693 +
19.694 +lemma of_nat_less_iff [simp]:
19.695 + "(of_nat m < (of_nat n::'a::ordered_semiring)) = (m<n)"
19.696 +by (blast intro: of_nat_less_imp_less less_imp_of_nat_less )
19.697 +
19.698 +text{*Special cases where either operand is zero*}
19.699 +declare of_nat_less_iff [of 0, simplified, simp]
19.700 +declare of_nat_less_iff [of _ 0, simplified, simp]
19.701 +
19.702 +lemma of_nat_le_iff [simp]:
19.703 + "(of_nat m \<le> (of_nat n::'a::ordered_semiring)) = (m \<le> n)"
19.704 +by (simp add: linorder_not_less [symmetric])
19.705 +
19.706 +text{*Special cases where either operand is zero*}
19.707 +declare of_nat_le_iff [of 0, simplified, simp]
19.708 +declare of_nat_le_iff [of _ 0, simplified, simp]
19.709 +
19.710 +lemma of_nat_eq_iff [simp]:
19.711 + "(of_nat m = (of_nat n::'a::ordered_semiring)) = (m = n)"
19.712 +by (simp add: order_eq_iff)
19.713 +
19.714 +text{*Special cases where either operand is zero*}
19.715 +declare of_nat_eq_iff [of 0, simplified, simp]
19.716 +declare of_nat_eq_iff [of _ 0, simplified, simp]
19.717 +
19.718 +lemma of_nat_diff [simp]:
19.719 + "n \<le> m ==> of_nat (m - n) = of_nat m - (of_nat n :: 'a::ring)"
19.720 +by (simp del: of_nat_add
19.721 + add: compare_rls of_nat_add [symmetric] split add: nat_diff_split)
19.722 +
19.723 +
19.724 +subsection{*The Set of Natural Numbers*}
19.725 +
19.726 +constdefs
19.727 + Nats :: "'a::semiring set"
19.728 + "Nats == range of_nat"
19.729 +
19.730 +syntax (xsymbols) Nats :: "'a set" ("\<nat>")
19.731 +
19.732 +lemma of_nat_in_Nats [simp]: "of_nat n \<in> Nats"
19.733 +by (simp add: Nats_def)
19.734 +
19.735 +lemma Nats_0 [simp]: "0 \<in> Nats"
19.736 +apply (simp add: Nats_def)
19.737 +apply (rule range_eqI)
19.738 +apply (rule of_nat_0 [symmetric])
19.739 +done
19.740 +
19.741 +lemma Nats_1 [simp]: "1 \<in> Nats"
19.742 +apply (simp add: Nats_def)
19.743 +apply (rule range_eqI)
19.744 +apply (rule of_nat_1 [symmetric])
19.745 +done
19.746 +
19.747 +lemma Nats_add [simp]: "[|a \<in> Nats; b \<in> Nats|] ==> a+b \<in> Nats"
19.748 +apply (auto simp add: Nats_def)
19.749 +apply (rule range_eqI)
19.750 +apply (rule of_nat_add [symmetric])
19.751 +done
19.752 +
19.753 +lemma Nats_mult [simp]: "[|a \<in> Nats; b \<in> Nats|] ==> a*b \<in> Nats"
19.754 +apply (auto simp add: Nats_def)
19.755 +apply (rule range_eqI)
19.756 +apply (rule of_nat_mult [symmetric])
19.757 +done
19.758 +
19.759 +text{*Agreement with the specific embedding for the integers*}
19.760 +lemma int_eq_of_nat: "int = (of_nat :: nat => int)"
19.761 +proof
19.762 + fix n
19.763 + show "int n = of_nat n" by (induct n, simp_all add: int_Suc add_ac)
19.764 +qed
19.765 +
19.766 +
19.767 +subsection{*Embedding of the Integers into any Ring: @{term of_int}*}
19.768 +
19.769 +constdefs
19.770 + of_int :: "int => 'a::ring"
19.771 + "of_int z ==
19.772 + (THE a. \<exists>i j. (i,j) \<in> Rep_Integ z & a = (of_nat i) - (of_nat j))"
19.773 +
19.774 +
19.775 +lemma of_int: "of_int (Abs_Integ (intrel `` {(i,j)})) = of_nat i - of_nat j"
19.776 +apply (simp add: of_int_def)
19.777 +apply (rule the_equality, auto)
19.778 +apply (simp add: compare_rls add_ac of_nat_add [symmetric]
19.779 + del: of_nat_add)
19.780 +done
19.781 +
19.782 +lemma of_int_0 [simp]: "of_int 0 = 0"
19.783 +by (simp add: of_int Zero_int_def int_def)
19.784 +
19.785 +lemma of_int_1 [simp]: "of_int 1 = 1"
19.786 +by (simp add: of_int One_int_def int_def)
19.787 +
19.788 +lemma of_int_add [simp]: "of_int (w+z) = of_int w + of_int z"
19.789 +apply (rule eq_Abs_Integ [of w])
19.790 +apply (rule eq_Abs_Integ [of z])
19.791 +apply (simp add: compare_rls of_int zadd)
19.792 +done
19.793 +
19.794 +lemma of_int_minus [simp]: "of_int (-z) = - (of_int z)"
19.795 +apply (rule eq_Abs_Integ [of z])
19.796 +apply (simp add: compare_rls of_int zminus)
19.797 +done
19.798 +
19.799 +lemma of_int_diff [simp]: "of_int (w-z) = of_int w - of_int z"
19.800 +by (simp add: diff_minus)
19.801 +
19.802 +lemma of_int_mult [simp]: "of_int (w*z) = of_int w * of_int z"
19.803 +apply (rule eq_Abs_Integ [of w])
19.804 +apply (rule eq_Abs_Integ [of z])
19.805 +apply (simp add: compare_rls of_int left_diff_distrib right_diff_distrib
19.806 + zmult add_ac)
19.807 +done
19.808 +
19.809 +lemma of_int_le_iff [simp]:
19.810 + "(of_int w \<le> (of_int z::'a::ordered_ring)) = (w \<le> z)"
19.811 +apply (rule eq_Abs_Integ [of w])
19.812 +apply (rule eq_Abs_Integ [of z])
19.813 +apply (simp add: compare_rls of_int zle zdiff_def zadd zminus
19.814 + of_nat_add [symmetric] del: of_nat_add)
19.815 +done
19.816 +
19.817 +text{*Special cases where either operand is zero*}
19.818 +declare of_int_le_iff [of 0, simplified, simp]
19.819 +declare of_int_le_iff [of _ 0, simplified, simp]
19.820 +
19.821 +lemma of_int_less_iff [simp]:
19.822 + "(of_int w < (of_int z::'a::ordered_ring)) = (w < z)"
19.823 +by (simp add: linorder_not_le [symmetric])
19.824 +
19.825 +text{*Special cases where either operand is zero*}
19.826 +declare of_int_less_iff [of 0, simplified, simp]
19.827 +declare of_int_less_iff [of _ 0, simplified, simp]
19.828 +
19.829 +lemma of_int_eq_iff [simp]:
19.830 + "(of_int w = (of_int z::'a::ordered_ring)) = (w = z)"
19.831 +by (simp add: order_eq_iff)
19.832 +
19.833 +text{*Special cases where either operand is zero*}
19.834 +declare of_int_eq_iff [of 0, simplified, simp]
19.835 +declare of_int_eq_iff [of _ 0, simplified, simp]
19.836 +
19.837 +
19.838 +subsection{*The Set of Integers*}
19.839 +
19.840 +constdefs
19.841 + Ints :: "'a::ring set"
19.842 + "Ints == range of_int"
19.843 +
19.844 +
19.845 +syntax (xsymbols)
19.846 + Ints :: "'a set" ("\<int>")
19.847 +
19.848 +lemma Ints_0 [simp]: "0 \<in> Ints"
19.849 +apply (simp add: Ints_def)
19.850 +apply (rule range_eqI)
19.851 +apply (rule of_int_0 [symmetric])
19.852 +done
19.853 +
19.854 +lemma Ints_1 [simp]: "1 \<in> Ints"
19.855 +apply (simp add: Ints_def)
19.856 +apply (rule range_eqI)
19.857 +apply (rule of_int_1 [symmetric])
19.858 +done
19.859 +
19.860 +lemma Ints_add [simp]: "[|a \<in> Ints; b \<in> Ints|] ==> a+b \<in> Ints"
19.861 +apply (auto simp add: Ints_def)
19.862 +apply (rule range_eqI)
19.863 +apply (rule of_int_add [symmetric])
19.864 +done
19.865 +
19.866 +lemma Ints_minus [simp]: "a \<in> Ints ==> -a \<in> Ints"
19.867 +apply (auto simp add: Ints_def)
19.868 +apply (rule range_eqI)
19.869 +apply (rule of_int_minus [symmetric])
19.870 +done
19.871 +
19.872 +lemma Ints_diff [simp]: "[|a \<in> Ints; b \<in> Ints|] ==> a-b \<in> Ints"
19.873 +apply (auto simp add: Ints_def)
19.874 +apply (rule range_eqI)
19.875 +apply (rule of_int_diff [symmetric])
19.876 +done
19.877 +
19.878 +lemma Ints_mult [simp]: "[|a \<in> Ints; b \<in> Ints|] ==> a*b \<in> Ints"
19.879 +apply (auto simp add: Ints_def)
19.880 +apply (rule range_eqI)
19.881 +apply (rule of_int_mult [symmetric])
19.882 +done
19.883 +
19.884 +text{*Collapse nested embeddings*}
19.885 +lemma of_int_of_nat_eq [simp]: "of_int (of_nat n) = of_nat n"
19.886 +by (induct n, auto)
19.887 +
19.888 +lemma of_int_int_eq [simp]: "of_int (int n) = int n"
19.889 +by (simp add: int_eq_of_nat)
19.890 +
19.891 +
19.892 +lemma Ints_cases [case_names of_int, cases set: Ints]:
19.893 + "q \<in> \<int> ==> (!!z. q = of_int z ==> C) ==> C"
19.894 +proof (unfold Ints_def)
19.895 + assume "!!z. q = of_int z ==> C"
19.896 + assume "q \<in> range of_int" thus C ..
19.897 +qed
19.898 +
19.899 +lemma Ints_induct [case_names of_int, induct set: Ints]:
19.900 + "q \<in> \<int> ==> (!!z. P (of_int z)) ==> P q"
19.901 + by (rule Ints_cases) auto
19.902 +
19.903 +
19.904 +
19.905 +(*Legacy ML bindings, but no longer the structure Int.*)
19.906 ML
19.907 {*
19.908 +val zabs_def = thm "zabs_def"
19.909 +val nat_def = thm "nat_def"
19.910 +
19.911 +val int_0 = thm "int_0";
19.912 +val int_1 = thm "int_1";
19.913 +val int_Suc0_eq_1 = thm "int_Suc0_eq_1";
19.914 +val neg_eq_less_0 = thm "neg_eq_less_0";
19.915 +val not_neg_eq_ge_0 = thm "not_neg_eq_ge_0";
19.916 +val not_neg_0 = thm "not_neg_0";
19.917 +val not_neg_1 = thm "not_neg_1";
19.918 +val iszero_0 = thm "iszero_0";
19.919 +val not_iszero_1 = thm "not_iszero_1";
19.920 +val int_0_less_1 = thm "int_0_less_1";
19.921 +val int_0_neq_1 = thm "int_0_neq_1";
19.922 +val negative_zless = thm "negative_zless";
19.923 +val negative_zle = thm "negative_zle";
19.924 +val not_zle_0_negative = thm "not_zle_0_negative";
19.925 +val not_int_zless_negative = thm "not_int_zless_negative";
19.926 +val negative_eq_positive = thm "negative_eq_positive";
19.927 +val zle_iff_zadd = thm "zle_iff_zadd";
19.928 +val abs_int_eq = thm "abs_int_eq";
19.929 +val abs_split = thm"abs_split";
19.930 +val nat_int = thm "nat_int";
19.931 +val nat_zminus_int = thm "nat_zminus_int";
19.932 +val nat_zero = thm "nat_zero";
19.933 +val not_neg_nat = thm "not_neg_nat";
19.934 +val neg_nat = thm "neg_nat";
19.935 +val zless_nat_eq_int_zless = thm "zless_nat_eq_int_zless";
19.936 +val nat_0_le = thm "nat_0_le";
19.937 +val nat_le_0 = thm "nat_le_0";
19.938 +val zless_nat_conj = thm "zless_nat_conj";
19.939 +val int_cases = thm "int_cases";
19.940 +
19.941 val int_def = thm "int_def";
19.942 -val neg_def = thm "neg_def";
19.943 -val iszero_def = thm "iszero_def";
19.944 val Zero_int_def = thm "Zero_int_def";
19.945 val One_int_def = thm "One_int_def";
19.946 val zadd_def = thm "zadd_def";
19.947 @@ -524,8 +981,6 @@
19.948 val zminus_zminus = thm "zminus_zminus";
19.949 val inj_zminus = thm "inj_zminus";
19.950 val zminus_0 = thm "zminus_0";
19.951 -val not_neg_int = thm "not_neg_int";
19.952 -val neg_zminus_int = thm "neg_zminus_int";
19.953 val zadd = thm "zadd";
19.954 val zminus_zadd_distrib = thm "zminus_zadd_distrib";
19.955 val zadd_commute = thm "zadd_commute";
19.956 @@ -545,8 +1000,6 @@
19.957 val zdiff0 = thm "zdiff0";
19.958 val zdiff0_right = thm "zdiff0_right";
19.959 val zdiff_self = thm "zdiff_self";
19.960 -val zadd_assoc_cong = thm "zadd_assoc_cong";
19.961 -val zadd_assoc_swap = thm "zadd_assoc_swap";
19.962 val zmult_congruent2 = thm "zmult_congruent2";
19.963 val zmult = thm "zmult";
19.964 val zmult_zminus = thm "zmult_zminus";
19.965 @@ -564,15 +1017,6 @@
19.966 val zmult_0_right = thm "zmult_0_right";
19.967 val zmult_1_right = thm "zmult_1_right";
19.968 val zless_iff_Suc_zadd = thm "zless_iff_Suc_zadd";
19.969 -val zless_zadd_Suc = thm "zless_zadd_Suc";
19.970 -val zless_trans = thm "zless_trans";
19.971 -val zless_not_sym = thm "zless_not_sym";
19.972 -val zless_asym = thm "zless_asym";
19.973 -val zless_not_refl = thm "zless_not_refl";
19.974 -val zless_irrefl = thm "zless_irrefl";
19.975 -val zless_linear = thm "zless_linear";
19.976 -val int_neq_iff = thm "int_neq_iff";
19.977 -val int_neqE = thm "int_neqE";
19.978 val int_int_eq = thm "int_int_eq";
19.979 val int_eq_0_conv = thm "int_eq_0_conv";
19.980 val zless_int = thm "zless_int";
19.981 @@ -581,15 +1025,48 @@
19.982 val zle_int = thm "zle_int";
19.983 val zero_zle_int = thm "zero_zle_int";
19.984 val int_le_0_conv = thm "int_le_0_conv";
19.985 -val zle_imp_zless_or_eq = thm "zle_imp_zless_or_eq";
19.986 -val zless_or_eq_imp_zle = thm "zless_or_eq_imp_zle";
19.987 -val int_le_less = thm "int_le_less";
19.988 val zle_refl = thm "zle_refl";
19.989 val zle_linear = thm "zle_linear";
19.990 val zle_trans = thm "zle_trans";
19.991 val zle_anti_sym = thm "zle_anti_sym";
19.992 -val int_less_le = thm "int_less_le";
19.993 -val zadd_left_cancel = thm "zadd_left_cancel";
19.994 +
19.995 +val Ints_def = thm "Ints_def";
19.996 +val Nats_def = thm "Nats_def";
19.997 +
19.998 +val of_nat_0 = thm "of_nat_0";
19.999 +val of_nat_Suc = thm "of_nat_Suc";
19.1000 +val of_nat_1 = thm "of_nat_1";
19.1001 +val of_nat_add = thm "of_nat_add";
19.1002 +val of_nat_mult = thm "of_nat_mult";
19.1003 +val zero_le_imp_of_nat = thm "zero_le_imp_of_nat";
19.1004 +val less_imp_of_nat_less = thm "less_imp_of_nat_less";
19.1005 +val of_nat_less_imp_less = thm "of_nat_less_imp_less";
19.1006 +val of_nat_less_iff = thm "of_nat_less_iff";
19.1007 +val of_nat_le_iff = thm "of_nat_le_iff";
19.1008 +val of_nat_eq_iff = thm "of_nat_eq_iff";
19.1009 +val Nats_0 = thm "Nats_0";
19.1010 +val Nats_1 = thm "Nats_1";
19.1011 +val Nats_add = thm "Nats_add";
19.1012 +val Nats_mult = thm "Nats_mult";
19.1013 +val of_int = thm "of_int";
19.1014 +val of_int_0 = thm "of_int_0";
19.1015 +val of_int_1 = thm "of_int_1";
19.1016 +val of_int_add = thm "of_int_add";
19.1017 +val of_int_minus = thm "of_int_minus";
19.1018 +val of_int_diff = thm "of_int_diff";
19.1019 +val of_int_mult = thm "of_int_mult";
19.1020 +val of_int_le_iff = thm "of_int_le_iff";
19.1021 +val of_int_less_iff = thm "of_int_less_iff";
19.1022 +val of_int_eq_iff = thm "of_int_eq_iff";
19.1023 +val Ints_0 = thm "Ints_0";
19.1024 +val Ints_1 = thm "Ints_1";
19.1025 +val Ints_add = thm "Ints_add";
19.1026 +val Ints_minus = thm "Ints_minus";
19.1027 +val Ints_diff = thm "Ints_diff";
19.1028 +val Ints_mult = thm "Ints_mult";
19.1029 +val of_int_of_nat_eq = thm"of_int_of_nat_eq";
19.1030 +val Ints_cases = thm "Ints_cases";
19.1031 +val Ints_induct = thm "Ints_induct";
19.1032 *}
19.1033
19.1034 end
20.1 --- a/src/HOL/Integ/IntDiv.thy Thu Feb 05 10:45:28 2004 +0100
20.2 +++ b/src/HOL/Integ/IntDiv.thy Tue Feb 10 12:02:11 2004 +0100
20.3 @@ -531,7 +531,7 @@
20.4 prefer 2 apply simp
20.5 apply (simp (no_asm_simp) add: zadd_zmult_distrib2)
20.6 apply (subst zadd_commute, rule zadd_zless_mono, arith)
20.7 -apply (rule zmult_zle_mono1, auto)
20.8 +apply (rule mult_right_mono, auto)
20.9 done
20.10
20.11 lemma zdiv_mono2:
20.12 @@ -561,7 +561,7 @@
20.13 apply (simp add: zmult_zless_cancel1)
20.14 apply (simp add: zadd_zmult_distrib2)
20.15 apply (subgoal_tac "b*q' \<le> b'*q'")
20.16 - prefer 2 apply (simp add: zmult_zle_mono1_neg)
20.17 + prefer 2 apply (simp add: mult_right_mono_neg)
20.18 apply (subgoal_tac "b'*q' < b + b*q")
20.19 apply arith
20.20 apply simp
20.21 @@ -702,8 +702,8 @@
20.22 apply (subgoal_tac "b * (c - q mod c) < r * 1")
20.23 apply (simp add: zdiff_zmult_distrib2)
20.24 apply (rule order_le_less_trans)
20.25 -apply (erule_tac [2] zmult_zless_mono1)
20.26 -apply (rule zmult_zle_mono2_neg)
20.27 +apply (erule_tac [2] mult_strict_right_mono)
20.28 +apply (rule mult_left_mono_neg)
20.29 apply (auto simp add: compare_rls zadd_commute [of 1]
20.30 add1_zle_eq pos_mod_bound)
20.31 done
20.32 @@ -724,7 +724,7 @@
20.33 apply (subgoal_tac "r * 1 < b * (c - q mod c) ")
20.34 apply (simp add: zdiff_zmult_distrib2)
20.35 apply (rule order_less_le_trans)
20.36 -apply (erule zmult_zless_mono1)
20.37 +apply (erule mult_strict_right_mono)
20.38 apply (rule_tac [2] zmult_zle_mono2)
20.39 apply (auto simp add: compare_rls zadd_commute [of 1]
20.40 add1_zle_eq pos_mod_bound)
20.41 @@ -1111,7 +1111,7 @@
20.42 apply (unfold dvd_def, auto)
20.43 apply (subgoal_tac "0 < n")
20.44 prefer 2
20.45 - apply (blast intro: zless_trans)
20.46 + apply (blast intro: order_less_trans)
20.47 apply (simp add: zero_less_mult_iff)
20.48 apply (subgoal_tac "n * k < n * 1")
20.49 apply (drule zmult_zless_cancel1 [THEN iffD1], auto)
20.50 @@ -1150,7 +1150,7 @@
20.51
20.52 lemma dvd_zminus_iff [iff]: "(z dvd -w) = (z dvd (w::int))"
20.53 apply (auto simp add: dvd_def)
20.54 - apply (drule zminus_equation [THEN iffD1])
20.55 + apply (drule minus_equation_iff [THEN iffD1])
20.56 apply (rule_tac [!] x = "-k" in exI, auto)
20.57 done
20.58
21.1 --- a/src/HOL/Integ/NatBin.thy Thu Feb 05 10:45:28 2004 +0100
21.2 +++ b/src/HOL/Integ/NatBin.thy Tue Feb 10 12:02:11 2004 +0100
21.3 @@ -80,7 +80,7 @@
21.4 (*"neg" is used in rewrite rules for binary comparisons*)
21.5 lemma int_nat_number_of:
21.6 "int (number_of v :: nat) =
21.7 - (if neg (number_of v) then 0
21.8 + (if neg (number_of v :: int) then 0
21.9 else (number_of v :: int))"
21.10 by (simp del: nat_number_of
21.11 add: neg_nat nat_number_of_def not_neg_nat add_assoc)
21.12 @@ -96,14 +96,14 @@
21.13
21.14 lemma Suc_nat_number_of_add:
21.15 "Suc (number_of v + n) =
21.16 - (if neg (number_of v) then 1+n else number_of (bin_succ v) + n)"
21.17 + (if neg (number_of v :: int) then 1+n else number_of (bin_succ v) + n)"
21.18 by (simp del: nat_number_of
21.19 add: nat_number_of_def neg_nat
21.20 Suc_nat_eq_nat_zadd1 number_of_succ)
21.21
21.22 lemma Suc_nat_number_of:
21.23 "Suc (number_of v) =
21.24 - (if neg (number_of v) then 1 else number_of (bin_succ v))"
21.25 + (if neg (number_of v :: int) then 1 else number_of (bin_succ v))"
21.26 apply (cut_tac n = 0 in Suc_nat_number_of_add)
21.27 apply (simp cong del: if_weak_cong)
21.28 done
21.29 @@ -115,8 +115,8 @@
21.30 (*"neg" is used in rewrite rules for binary comparisons*)
21.31 lemma add_nat_number_of:
21.32 "(number_of v :: nat) + number_of v' =
21.33 - (if neg (number_of v) then number_of v'
21.34 - else if neg (number_of v') then number_of v
21.35 + (if neg (number_of v :: int) then number_of v'
21.36 + else if neg (number_of v' :: int) then number_of v
21.37 else number_of (bin_add v v'))"
21.38 by (force dest!: neg_nat
21.39 simp del: nat_number_of
21.40 @@ -138,7 +138,7 @@
21.41
21.42 lemma diff_nat_number_of:
21.43 "(number_of v :: nat) - number_of v' =
21.44 - (if neg (number_of v') then number_of v
21.45 + (if neg (number_of v' :: int) then number_of v
21.46 else let d = number_of (bin_add v (bin_minus v')) in
21.47 if neg d then 0 else nat d)"
21.48 by (simp del: nat_number_of add: diff_nat_eq_if nat_number_of_def)
21.49 @@ -150,7 +150,7 @@
21.50
21.51 lemma mult_nat_number_of:
21.52 "(number_of v :: nat) * number_of v' =
21.53 - (if neg (number_of v) then 0 else number_of (bin_mult v v'))"
21.54 + (if neg (number_of v :: int) then 0 else number_of (bin_mult v v'))"
21.55 by (force dest!: neg_nat
21.56 simp del: nat_number_of
21.57 simp add: nat_number_of_def nat_mult_distrib [symmetric])
21.58 @@ -162,7 +162,7 @@
21.59
21.60 lemma div_nat_number_of:
21.61 "(number_of v :: nat) div number_of v' =
21.62 - (if neg (number_of v) then 0
21.63 + (if neg (number_of v :: int) then 0
21.64 else nat (number_of v div number_of v'))"
21.65 by (force dest!: neg_nat
21.66 simp del: nat_number_of
21.67 @@ -175,8 +175,8 @@
21.68
21.69 lemma mod_nat_number_of:
21.70 "(number_of v :: nat) mod number_of v' =
21.71 - (if neg (number_of v) then 0
21.72 - else if neg (number_of v') then number_of v
21.73 + (if neg (number_of v :: int) then 0
21.74 + else if neg (number_of v' :: int) then number_of v
21.75 else nat (number_of v mod number_of v'))"
21.76 by (force dest!: neg_nat
21.77 simp del: nat_number_of
21.78 @@ -242,9 +242,9 @@
21.79 (*"neg" is used in rewrite rules for binary comparisons*)
21.80 lemma eq_nat_number_of:
21.81 "((number_of v :: nat) = number_of v') =
21.82 - (if neg (number_of v) then (iszero (number_of v') | neg (number_of v'))
21.83 - else if neg (number_of v') then iszero (number_of v)
21.84 - else iszero (number_of (bin_add v (bin_minus v'))))"
21.85 + (if neg (number_of v :: int) then (iszero (number_of v' :: int) | neg (number_of v' :: int))
21.86 + else if neg (number_of v' :: int) then iszero (number_of v :: int)
21.87 + else iszero (number_of (bin_add v (bin_minus v')) :: int))"
21.88 apply (simp only: simp_thms neg_nat not_neg_eq_ge_0 nat_number_of_def
21.89 eq_nat_nat_iff eq_number_of_eq nat_0 iszero_def
21.90 split add: split_if cong add: imp_cong)
21.91 @@ -259,8 +259,8 @@
21.92 (*"neg" is used in rewrite rules for binary comparisons*)
21.93 lemma less_nat_number_of:
21.94 "((number_of v :: nat) < number_of v') =
21.95 - (if neg (number_of v) then neg (number_of (bin_minus v'))
21.96 - else neg (number_of (bin_add v (bin_minus v'))))"
21.97 + (if neg (number_of v :: int) then neg (number_of (bin_minus v') :: int)
21.98 + else neg (number_of (bin_add v (bin_minus v')) :: int))"
21.99 apply (simp only: simp_thms neg_nat not_neg_eq_ge_0 nat_number_of_def
21.100 nat_less_eq_zless less_number_of_eq_neg zless_nat_eq_int_zless
21.101 cong add: imp_cong, simp)
21.102 @@ -397,24 +397,24 @@
21.103
21.104 lemma eq_number_of_0:
21.105 "(number_of v = (0::nat)) =
21.106 - (if neg (number_of v) then True else iszero (number_of v))"
21.107 + (if neg (number_of v :: int) then True else iszero (number_of v :: int))"
21.108 apply (simp add: numeral_0_eq_0 [symmetric] iszero_0)
21.109 done
21.110
21.111 lemma eq_0_number_of:
21.112 "((0::nat) = number_of v) =
21.113 - (if neg (number_of v) then True else iszero (number_of v))"
21.114 + (if neg (number_of v :: int) then True else iszero (number_of v :: int))"
21.115 apply (rule trans [OF eq_sym_conv eq_number_of_0])
21.116 done
21.117
21.118 lemma less_0_number_of:
21.119 - "((0::nat) < number_of v) = neg (number_of (bin_minus v))"
21.120 + "((0::nat) < number_of v) = neg (number_of (bin_minus v) :: int)"
21.121 by (simp add: numeral_0_eq_0 [symmetric])
21.122
21.123 (*Simplification already handles n<0, n<=0 and 0<=n.*)
21.124 declare eq_number_of_0 [simp] eq_0_number_of [simp] less_0_number_of [simp]
21.125
21.126 -lemma neg_imp_number_of_eq_0: "neg (number_of v) ==> number_of v = (0::nat)"
21.127 +lemma neg_imp_number_of_eq_0: "neg (number_of v :: int) ==> number_of v = (0::nat)"
21.128 by (simp add: numeral_0_eq_0 [symmetric] iszero_0)
21.129
21.130
21.131 @@ -530,7 +530,7 @@
21.132
21.133 lemma power_nat_number_of:
21.134 "(number_of v :: nat) ^ n =
21.135 - (if neg (number_of v) then 0^n else nat ((number_of v :: int) ^ n))"
21.136 + (if neg (number_of v :: int) then 0^n else nat ((number_of v :: int) ^ n))"
21.137 by (simp only: simp_thms neg_nat not_neg_eq_ge_0 nat_number_of_def nat_power_eq
21.138 split add: split_if cong: imp_cong)
21.139
21.140 @@ -605,7 +605,7 @@
21.141
21.142 lemma nat_number_of_BIT_True:
21.143 "number_of (w BIT True) =
21.144 - (if neg (number_of w) then 0
21.145 + (if neg (number_of w :: int) then 0
21.146 else let n = number_of w in Suc (n + n))"
21.147 apply (simp only: nat_number_of_def Let_def split: split_if)
21.148 apply (intro conjI impI)
21.149 @@ -618,7 +618,7 @@
21.150 lemma nat_number_of_BIT_False:
21.151 "number_of (w BIT False) = (let n::nat = number_of w in n + n)"
21.152 apply (simp only: nat_number_of_def Let_def)
21.153 - apply (cases "neg (number_of w)")
21.154 + apply (cases "neg (number_of w :: int)")
21.155 apply (simp add: neg_nat neg_number_of_BIT)
21.156 apply (rule int_int_eq [THEN iffD1])
21.157 apply (simp only: not_neg_nat neg_number_of_BIT int_Suc zadd_int [symmetric] simp_thms)
21.158 @@ -637,8 +637,8 @@
21.159
21.160 lemma nat_number_of_add_left:
21.161 "number_of v + (number_of v' + (k::nat)) =
21.162 - (if neg (number_of v) then number_of v' + k
21.163 - else if neg (number_of v') then number_of v + k
21.164 + (if neg (number_of v :: int) then number_of v' + k
21.165 + else if neg (number_of v' :: int) then number_of v + k
21.166 else number_of (bin_add v v') + k)"
21.167 apply simp
21.168 done
21.169 @@ -831,6 +831,8 @@
21.170 "uminus" :: "int => int" ("`~")
21.171 "op +" :: "int => int => int" ("(_ `+/ _)")
21.172 "op *" :: "int => int => int" ("(_ `*/ _)")
21.173 + "op <" :: "int => int => bool" ("(_ </ _)")
21.174 + "op <=" :: "int => int => bool" ("(_ <=/ _)")
21.175 "neg" ("(_ < 0)")
21.176
21.177 end
22.1 --- a/src/HOL/Integ/NatSimprocs.thy Thu Feb 05 10:45:28 2004 +0100
22.2 +++ b/src/HOL/Integ/NatSimprocs.thy Tue Feb 10 12:02:11 2004 +0100
22.3 @@ -20,7 +20,7 @@
22.4 (*Now just instantiating n to (number_of v) does the right simplification,
22.5 but with some redundant inequality tests.*)
22.6 lemma neg_number_of_bin_pred_iff_0:
22.7 - "neg (number_of (bin_pred v)) = (number_of v = (0::nat))"
22.8 + "neg (number_of (bin_pred v)::int) = (number_of v = (0::nat))"
22.9 apply (subgoal_tac "neg (number_of (bin_pred v)) = (number_of v < Suc 0) ")
22.10 apply (simp only: less_Suc_eq_le le_0_eq)
22.11 apply (subst less_number_of_Suc, simp)
22.12 @@ -29,7 +29,7 @@
22.13 text{*No longer required as a simprule because of the @{text inverse_fold}
22.14 simproc*}
22.15 lemma Suc_diff_number_of:
22.16 - "neg (number_of (bin_minus v)) ==>
22.17 + "neg (number_of (bin_minus v)::int) ==>
22.18 Suc m - (number_of v) = m - (number_of (bin_pred v))"
22.19 apply (subst Suc_diff_eq_diff_pred, simp, simp)
22.20 apply (force simp only: diff_nat_number_of less_0_number_of [symmetric]
23.1 --- a/src/HOL/Integ/Presburger.thy Thu Feb 05 10:45:28 2004 +0100
23.2 +++ b/src/HOL/Integ/Presburger.thy Tue Feb 10 12:02:11 2004 +0100
23.3 @@ -961,7 +961,7 @@
23.4 apply (case_tac "0 \<le> k")
23.5 apply rules
23.6 apply (simp add: linorder_not_le)
23.7 - apply (drule zmult_zless_mono2_neg [OF iffD2 [OF zero_less_int_conv]])
23.8 + apply (drule mult_strict_left_mono_neg [OF iffD2 [OF zero_less_int_conv]])
23.9 apply assumption
23.10 apply (simp add: mult_ac)
23.11 done
24.1 --- a/src/HOL/Integ/int_arith1.ML Thu Feb 05 10:45:28 2004 +0100
24.2 +++ b/src/HOL/Integ/int_arith1.ML Tue Feb 10 12:02:11 2004 +0100
24.3 @@ -28,6 +28,11 @@
24.4 val bin_mult_Min = thm"bin_mult_Min";
24.5 val bin_mult_BIT = thm"bin_mult_BIT";
24.6
24.7 +val neg_def = thm "neg_def";
24.8 +val iszero_def = thm "iszero_def";
24.9 +val not_neg_int = thm "not_neg_int";
24.10 +val neg_zminus_int = thm "neg_zminus_int";
24.11 +
24.12 val zadd_ac = thms "Ring_and_Field.add_ac"
24.13 val zmult_ac = thms "Ring_and_Field.mult_ac"
24.14 val NCons_Pls_0 = thm"NCons_Pls_0";
25.1 --- a/src/HOL/Integ/int_factor_simprocs.ML Thu Feb 05 10:45:28 2004 +0100
25.2 +++ b/src/HOL/Integ/int_factor_simprocs.ML Tue Feb 10 12:02:11 2004 +0100
25.3 @@ -5,25 +5,11 @@
25.4
25.5 Factor cancellation simprocs for the integers.
25.6
25.7 -This file can't be combined with int_arith1,2 because it requires IntDiv.thy.
25.8 +This file can't be combined with int_arith1 because it requires IntDiv.thy.
25.9 *)
25.10
25.11 (** Factor cancellation theorems for "int" **)
25.12
25.13 -Goal "!!k::int. (k*m <= k*n) = ((0 < k --> m<=n) & (k < 0 --> n<=m))";
25.14 -by (stac zmult_zle_cancel1 1);
25.15 -by Auto_tac;
25.16 -qed "int_mult_le_cancel1";
25.17 -
25.18 -Goal "!!k::int. (k*m < k*n) = ((0 < k & m<n) | (k < 0 & n<m))";
25.19 -by (stac zmult_zless_cancel1 1);
25.20 -by Auto_tac;
25.21 -qed "int_mult_less_cancel1";
25.22 -
25.23 -Goal "!!k::int. (k*m = k*n) = (k = 0 | m=n)";
25.24 -by Auto_tac;
25.25 -qed "int_mult_eq_cancel1";
25.26 -
25.27 Goal "!!k::int. k~=0 ==> (k*m) div (k*n) = (m div n)";
25.28 by (stac zdiv_zmult_zmult1 1);
25.29 by Auto_tac;
25.30 @@ -34,6 +20,7 @@
25.31 by (simp_tac (simpset() addsimps [int_mult_div_cancel1]) 1);
25.32 qed "int_mult_div_cancel_disj";
25.33
25.34 +
25.35 local
25.36 open Int_Numeral_Simprocs
25.37 in
25.38 @@ -65,7 +52,7 @@
25.39 val prove_conv = Bin_Simprocs.prove_conv
25.40 val mk_bal = HOLogic.mk_eq
25.41 val dest_bal = HOLogic.dest_bin "op =" HOLogic.intT
25.42 - val cancel = int_mult_eq_cancel1 RS trans
25.43 + val cancel = mult_cancel_left RS trans
25.44 val neg_exchanges = false
25.45 )
25.46
25.47 @@ -74,7 +61,7 @@
25.48 val prove_conv = Bin_Simprocs.prove_conv
25.49 val mk_bal = HOLogic.mk_binrel "op <"
25.50 val dest_bal = HOLogic.dest_bin "op <" HOLogic.intT
25.51 - val cancel = int_mult_less_cancel1 RS trans
25.52 + val cancel = mult_less_cancel_left RS trans
25.53 val neg_exchanges = true
25.54 )
25.55
25.56 @@ -83,7 +70,7 @@
25.57 val prove_conv = Bin_Simprocs.prove_conv
25.58 val mk_bal = HOLogic.mk_binrel "op <="
25.59 val dest_bal = HOLogic.dest_bin "op <=" HOLogic.intT
25.60 - val cancel = int_mult_le_cancel1 RS trans
25.61 + val cancel = mult_le_cancel_left RS trans
25.62 val neg_exchanges = true
25.63 )
25.64
25.65 @@ -179,7 +166,7 @@
25.66 val prove_conv = Bin_Simprocs.prove_conv
25.67 val mk_bal = HOLogic.mk_eq
25.68 val dest_bal = HOLogic.dest_bin "op =" HOLogic.intT
25.69 - val simplify_meta_eq = cancel_simplify_meta_eq int_mult_eq_cancel1
25.70 + val simplify_meta_eq = cancel_simplify_meta_eq mult_cancel_left
25.71 );
25.72
25.73 structure DivideCancelFactor = ExtractCommonTermFun
26.1 --- a/src/HOL/IsaMakefile Thu Feb 05 10:45:28 2004 +0100
26.2 +++ b/src/HOL/IsaMakefile Tue Feb 10 12:02:11 2004 +0100
26.3 @@ -86,7 +86,7 @@
26.4 Hilbert_Choice.thy Hilbert_Choice_lemmas.ML HOL.ML \
26.5 HOL.thy HOL_lemmas.ML Inductive.thy Integ/Bin.thy \
26.6 Integ/cooper_dec.ML Integ/cooper_proof.ML \
26.7 - Integ/Equiv.thy Integ/Int.thy Integ/IntArith.thy Integ/IntDef.thy \
26.8 + Integ/Equiv.thy Integ/IntArith.thy Integ/IntDef.thy \
26.9 Integ/IntDiv.thy Integ/NatBin.thy Integ/NatSimprocs.thy Integ/int_arith1.ML \
26.10 Integ/int_factor_simprocs.ML Integ/nat_simprocs.ML \
26.11 Integ/Presburger.thy Integ/presburger.ML Integ/qelim.ML \
27.1 --- a/src/HOL/Isar_examples/document/root.bib Thu Feb 05 10:45:28 2004 +0100
27.2 +++ b/src/HOL/Isar_examples/document/root.bib Tue Feb 10 12:02:11 2004 +0100
27.3 @@ -71,7 +71,7 @@
27.4 institution = CUCL,
27.5 year = 1996,
27.6 number = 394,
27.7 - note = {\url{http://www.ftp.cl.cam.ac.uk/ftp/papers/reports/}}
27.8 + note = {\url{http://www.cl.cam.ac.uk/users/lcp/papers/Reports/mutil.pdf}}
27.9 }
27.10
27.11 @Proceedings{tphols98,
28.1 --- a/src/HOL/NumberTheory/IntPrimes.thy Thu Feb 05 10:45:28 2004 +0100
28.2 +++ b/src/HOL/NumberTheory/IntPrimes.thy Tue Feb 10 12:02:11 2004 +0100
28.3 @@ -338,7 +338,7 @@
28.4 a < m ==> 0 \<le> b ==> b < m ==> [a = b] (mod m) ==> a = b"
28.5 apply (unfold zcong_def dvd_def, auto)
28.6 apply (drule_tac f = "\<lambda>z. z mod m" in arg_cong)
28.7 - apply (cut_tac z = a and w = b in zless_linear, auto)
28.8 + apply (cut_tac x = a and y = b in linorder_less_linear, auto)
28.9 apply (subgoal_tac [2] "(a - b) mod m = a - b")
28.10 apply (rule_tac [3] mod_pos_pos_trivial, auto)
28.11 apply (subgoal_tac "(m + (a - b)) mod m = m + (a - b)")
29.1 --- a/src/HOL/Presburger.thy Thu Feb 05 10:45:28 2004 +0100
29.2 +++ b/src/HOL/Presburger.thy Tue Feb 10 12:02:11 2004 +0100
29.3 @@ -961,7 +961,7 @@
29.4 apply (case_tac "0 \<le> k")
29.5 apply rules
29.6 apply (simp add: linorder_not_le)
29.7 - apply (drule zmult_zless_mono2_neg [OF iffD2 [OF zero_less_int_conv]])
29.8 + apply (drule mult_strict_left_mono_neg [OF iffD2 [OF zero_less_int_conv]])
29.9 apply assumption
29.10 apply (simp add: mult_ac)
29.11 done
30.1 --- a/src/HOL/Real/PReal.thy Thu Feb 05 10:45:28 2004 +0100
30.2 +++ b/src/HOL/Real/PReal.thy Tue Feb 10 12:02:11 2004 +0100
30.3 @@ -700,7 +700,7 @@
30.4 assumes A: "A \<in> preal"
30.5 and "\<forall>x\<in>A. x + u \<in> A"
30.6 and "0 \<le> z"
30.7 - shows "\<exists>b\<in>A. b + (rat z) * u \<in> A"
30.8 + shows "\<exists>b\<in>A. b + (of_int z) * u \<in> A"
30.9 proof (cases z rule: int_cases)
30.10 case (nonneg n)
30.11 show ?thesis
30.12 @@ -709,8 +709,8 @@
30.13 from preal_nonempty [OF A]
30.14 show ?case by force
30.15 case (Suc k)
30.16 - from this obtain b where "b \<in> A" "b + rat (int k) * u \<in> A" ..
30.17 - hence "b + rat (int k)*u + u \<in> A" by (simp add: prems)
30.18 + from this obtain b where "b \<in> A" "b + of_int (int k) * u \<in> A" ..
30.19 + hence "b + of_int (int k)*u + u \<in> A" by (simp add: prems)
30.20 thus ?case by (force simp add: left_distrib add_ac prems)
30.21 qed
30.22 next
30.23 @@ -718,7 +718,6 @@
30.24 with prems show ?thesis by simp
30.25 qed
30.26
30.27 -
30.28 lemma Gleason9_34_contra:
30.29 assumes A: "A \<in> preal"
30.30 shows "[|\<forall>x\<in>A. x + u \<in> A; 0 < u; 0 < y; y \<notin> A|] ==> False"
30.31 @@ -736,10 +735,10 @@
30.32 have apos [simp]: "0 < a"
30.33 by (simp add: zero_less_Fract_iff [OF bpos, symmetric] ypos)
30.34 let ?k = "a*d"
30.35 - have frle: "Fract a b \<le> rat ?k * (Fract c d)"
30.36 + have frle: "Fract a b \<le> Fract ?k 1 * (Fract c d)"
30.37 proof -
30.38 have "?thesis = ((a * d * b * d) \<le> c * b * (a * d * b * d))"
30.39 - by (simp add: rat_def mult_rat le_rat order_less_imp_not_eq2 mult_ac)
30.40 + by (simp add: mult_rat le_rat order_less_imp_not_eq2 mult_ac)
30.41 moreover
30.42 have "(1 * (a * d * b * d)) \<le> c * b * (a * d * b * d)"
30.43 by (rule mult_mono,
30.44 @@ -751,11 +750,11 @@
30.45 have k: "0 \<le> ?k" by (simp add: order_less_imp_le zero_less_mult_iff)
30.46 from Gleason9_34_exists [OF A closed k]
30.47 obtain z where z: "z \<in> A"
30.48 - and mem: "z + rat ?k * Fract c d \<in> A" ..
30.49 - have less: "z + rat ?k * Fract c d < Fract a b"
30.50 + and mem: "z + of_int ?k * Fract c d \<in> A" ..
30.51 + have less: "z + of_int ?k * Fract c d < Fract a b"
30.52 by (rule not_in_preal_ub [OF A notin mem ypos])
30.53 have "0<z" by (rule preal_imp_pos [OF A z])
30.54 - with frle and less show False by arith
30.55 + with frle and less show False by (simp add: Fract_of_int_eq)
30.56 qed
30.57
30.58
31.1 --- a/src/HOL/Real/RatArith.thy Thu Feb 05 10:45:28 2004 +0100
31.2 +++ b/src/HOL/Real/RatArith.thy Tue Feb 10 12:02:11 2004 +0100
31.3 @@ -13,15 +13,11 @@
31.4
31.5 instance rat :: number ..
31.6
31.7 -defs
31.8 +defs (overloaded)
31.9 rat_number_of_def:
31.10 - "number_of v == Fract (number_of v) 1"
31.11 + "(number_of v :: rat) == of_int (number_of v)"
31.12 (*::bin=>rat ::bin=>int*)
31.13
31.14 -theorem number_of_rat: "number_of b = rat (number_of b)"
31.15 - by (simp add: rat_number_of_def rat_def)
31.16 -
31.17 -declare number_of_rat [symmetric, simp]
31.18
31.19 lemma rat_numeral_0_eq_0: "Numeral0 = (0::rat)"
31.20 by (simp add: rat_number_of_def zero_rat [symmetric])
31.21 @@ -33,25 +29,26 @@
31.22 subsection{*Arithmetic Operations On Numerals*}
31.23
31.24 lemma add_rat_number_of [simp]:
31.25 - "(number_of v :: rat) + number_of v' = number_of (bin_add v v')"
31.26 -by (simp add: rat_number_of_def add_rat)
31.27 + "(number_of v :: rat) + number_of v' = number_of (bin_add v v')"
31.28 +by (simp only: rat_number_of_def of_int_add number_of_add)
31.29
31.30 lemma minus_rat_number_of [simp]:
31.31 "- (number_of w :: rat) = number_of (bin_minus w)"
31.32 -by (simp add: rat_number_of_def minus_rat)
31.33 +by (simp only: rat_number_of_def of_int_minus number_of_minus)
31.34
31.35 lemma diff_rat_number_of [simp]:
31.36 "(number_of v :: rat) - number_of w = number_of (bin_add v (bin_minus w))"
31.37 -by (simp add: rat_number_of_def diff_rat)
31.38 +by (simp only: add_rat_number_of minus_rat_number_of diff_minus)
31.39
31.40 lemma mult_rat_number_of [simp]:
31.41 "(number_of v :: rat) * number_of v' = number_of (bin_mult v v')"
31.42 -by (simp add: rat_number_of_def mult_rat)
31.43 +by (simp only: rat_number_of_def of_int_mult number_of_mult)
31.44
31.45 text{*Lemmas for specialist use, NOT as default simprules*}
31.46 lemma rat_mult_2: "2 * z = (z+z::rat)"
31.47 proof -
31.48 - have eq: "(2::rat) = 1 + 1" by (simp add: rat_numeral_1_eq_1 [symmetric])
31.49 + have eq: "(2::rat) = 1 + 1"
31.50 + by (simp del: rat_number_of_def add: rat_numeral_1_eq_1 [symmetric])
31.51 thus ?thesis by (simp add: eq left_distrib)
31.52 qed
31.53
31.54 @@ -63,20 +60,20 @@
31.55
31.56 lemma eq_rat_number_of [simp]:
31.57 "((number_of v :: rat) = number_of v') =
31.58 - iszero (number_of (bin_add v (bin_minus v')))"
31.59 -by (simp add: rat_number_of_def eq_rat)
31.60 + iszero (number_of (bin_add v (bin_minus v')) :: int)"
31.61 +by (simp add: rat_number_of_def)
31.62
31.63 text{*@{term neg} is used in rewrite rules for binary comparisons*}
31.64 lemma less_rat_number_of [simp]:
31.65 "((number_of v :: rat) < number_of v') =
31.66 - neg (number_of (bin_add v (bin_minus v')))"
31.67 -by (simp add: rat_number_of_def less_rat)
31.68 + neg (number_of (bin_add v (bin_minus v')) :: int)"
31.69 +by (simp add: rat_number_of_def)
31.70
31.71
31.72 text{*New versions of existing theorems involving 0, 1*}
31.73
31.74 lemma rat_minus_1_eq_m1 [simp]: "- 1 = (-1::rat)"
31.75 -by (simp add: rat_numeral_1_eq_1 [symmetric])
31.76 +by (simp del: rat_number_of_def add: rat_numeral_1_eq_1 [symmetric])
31.77
31.78 lemma rat_mult_minus1 [simp]: "-1 * z = -(z::rat)"
31.79 proof -
31.80 @@ -143,13 +140,15 @@
31.81
31.82 lemma abs_nat_number_of [simp]:
31.83 "abs (number_of v :: rat) =
31.84 - (if neg (number_of v) then number_of (bin_minus v)
31.85 + (if neg (number_of v :: int) then number_of (bin_minus v)
31.86 else number_of v)"
31.87 -by (simp add: abs_if)
31.88 +by (simp add: abs_if)
31.89
31.90 lemma abs_minus_one [simp]: "abs (-1) = (1::rat)"
31.91 by (simp add: abs_if)
31.92
31.93 +declare rat_number_of_def [simp]
31.94 +
31.95
31.96 ML
31.97 {*
32.1 --- a/src/HOL/Real/Rational.thy Thu Feb 05 10:45:28 2004 +0100
32.2 +++ b/src/HOL/Real/Rational.thy Tue Feb 10 12:02:11 2004 +0100
32.3 @@ -465,11 +465,11 @@
32.4
32.5 theorem less_rat: "b \<noteq> 0 ==> d \<noteq> 0 ==>
32.6 (Fract a b < Fract c d) = ((a * d) * (b * d) < (c * b) * (b * d))"
32.7 - by (simp add: less_rat_def le_rat eq_rat int_less_le)
32.8 + by (simp add: less_rat_def le_rat eq_rat order_less_le)
32.9
32.10 theorem abs_rat: "b \<noteq> 0 ==> \<bar>Fract a b\<bar> = Fract \<bar>a\<bar> \<bar>b\<bar>"
32.11 by (simp add: abs_rat_def minus_rat zero_rat less_rat eq_rat)
32.12 - (auto simp add: mult_less_0_iff zero_less_mult_iff int_le_less
32.13 + (auto simp add: mult_less_0_iff zero_less_mult_iff order_le_less
32.14 split: abs_split)
32.15
32.16
32.17 @@ -619,7 +619,7 @@
32.18 proof -
32.19 let ?E = "e * f" and ?F = "f * f"
32.20 from neq gt have "0 < ?E"
32.21 - by (auto simp add: zero_rat less_rat le_rat int_less_le eq_rat)
32.22 + by (auto simp add: zero_rat less_rat le_rat order_less_le eq_rat)
32.23 moreover from neq have "0 < ?F"
32.24 by (auto simp add: zero_less_mult_iff)
32.25 moreover from neq le have "(a * d) * (b * d) < (c * b) * (b * d)"
32.26 @@ -642,72 +642,6 @@
32.27 qed
32.28
32.29
32.30 -subsection {* Embedding integers: The Injection @{term rat} *}
32.31 -
32.32 -constdefs
32.33 - rat :: "int => rat" (* FIXME generalize int to any numeric subtype (?) *)
32.34 - "rat z == Fract z 1"
32.35 - int_set :: "rat set" ("\<int>") (* FIXME generalize rat to any numeric supertype (?) *)
32.36 - "\<int> == range rat"
32.37 -
32.38 -lemma int_set_cases [case_names rat, cases set: int_set]:
32.39 - "q \<in> \<int> ==> (!!z. q = rat z ==> C) ==> C"
32.40 -proof (unfold int_set_def)
32.41 - assume "!!z. q = rat z ==> C"
32.42 - assume "q \<in> range rat" thus C ..
32.43 -qed
32.44 -
32.45 -lemma int_set_induct [case_names rat, induct set: int_set]:
32.46 - "q \<in> \<int> ==> (!!z. P (rat z)) ==> P q"
32.47 - by (rule int_set_cases) auto
32.48 -
32.49 -lemma rat_of_int_zero [simp]: "rat (0::int) = (0::rat)"
32.50 -by (simp add: rat_def zero_rat [symmetric])
32.51 -
32.52 -lemma rat_of_int_one [simp]: "rat (1::int) = (1::rat)"
32.53 -by (simp add: rat_def one_rat [symmetric])
32.54 -
32.55 -lemma rat_of_int_add_distrib [simp]: "rat (x + y) = rat (x::int) + rat y"
32.56 -by (simp add: rat_def add_rat)
32.57 -
32.58 -lemma rat_of_int_minus_distrib [simp]: "rat (-x) = -rat (x::int)"
32.59 -by (simp add: rat_def minus_rat)
32.60 -
32.61 -lemma rat_of_int_diff_distrib [simp]: "rat (x - y) = rat (x::int) - rat y"
32.62 -by (simp add: rat_def diff_rat)
32.63 -
32.64 -lemma rat_of_int_mult_distrib [simp]: "rat (x * y) = rat (x::int) * rat y"
32.65 -by (simp add: rat_def mult_rat)
32.66 -
32.67 -lemma rat_inject [simp]: "(rat z = rat w) = (z = w)"
32.68 -proof
32.69 - assume "rat z = rat w"
32.70 - hence "Fract z 1 = Fract w 1" by (unfold rat_def)
32.71 - hence "\<lfloor>fract z 1\<rfloor> = \<lfloor>fract w 1\<rfloor>" ..
32.72 - thus "z = w" by auto
32.73 -next
32.74 - assume "z = w"
32.75 - thus "rat z = rat w" by simp
32.76 -qed
32.77 -
32.78 -
32.79 -lemma rat_of_int_zero_cancel [simp]: "(rat x = 0) = (x = 0)"
32.80 -proof -
32.81 - have "(rat x = 0) = (rat x = rat 0)" by simp
32.82 - also have "... = (x = 0)" by (rule rat_inject)
32.83 - finally show ?thesis .
32.84 -qed
32.85 -
32.86 -lemma rat_of_int_less_iff [simp]: "rat (x::int) < rat y = (x < y)"
32.87 -by (simp add: rat_def less_rat)
32.88 -
32.89 -lemma rat_of_int_le_iff [simp]: "(rat (x::int) \<le> rat y) = (x \<le> y)"
32.90 -by (simp add: linorder_not_less [symmetric])
32.91 -
32.92 -lemma zero_less_rat_of_int_iff [simp]: "(0 < rat y) = (0 < y)"
32.93 -by (insert rat_of_int_less_iff [of 0 y], simp)
32.94 -
32.95 -
32.96 subsection {* Various Other Results *}
32.97
32.98 lemma minus_rat_cancel [simp]: "b \<noteq> 0 ==> Fract (-a) (-b) = Fract a b"
32.99 @@ -733,4 +667,30 @@
32.100 "0 < b ==> (0 < Fract a b) = (0 < a)"
32.101 by (simp add: zero_rat less_rat order_less_imp_not_eq2 zero_less_mult_iff)
32.102
32.103 +lemma Fract_add_one: "n \<noteq> 0 ==> Fract (m + n) n = Fract m n + 1"
32.104 +apply (insert add_rat [of concl: m n 1 1])
32.105 +apply (simp add: one_rat [symmetric])
32.106 +done
32.107 +
32.108 +lemma Fract_of_nat_eq: "Fract (of_nat k) 1 = of_nat k"
32.109 +apply (induct k)
32.110 +apply (simp add: zero_rat)
32.111 +apply (simp add: Fract_add_one)
32.112 +done
32.113 +
32.114 +lemma Fract_of_int_eq: "Fract k 1 = of_int k"
32.115 +proof (cases k rule: int_cases)
32.116 + case (nonneg n)
32.117 + thus ?thesis by (simp add: int_eq_of_nat Fract_of_nat_eq)
32.118 +next
32.119 + case (neg n)
32.120 + hence "Fract k 1 = - (Fract (of_nat (Suc n)) 1)"
32.121 + by (simp only: minus_rat int_eq_of_nat)
32.122 + also have "... = - (of_nat (Suc n))"
32.123 + by (simp only: Fract_of_nat_eq)
32.124 + finally show ?thesis
32.125 + by (simp add: only: prems int_eq_of_nat of_int_minus of_int_of_nat_eq)
32.126 +qed
32.127 +
32.128 +
32.129 end
33.1 --- a/src/HOL/Real/RealArith.thy Thu Feb 05 10:45:28 2004 +0100
33.2 +++ b/src/HOL/Real/RealArith.thy Tue Feb 10 12:02:11 2004 +0100
33.3 @@ -62,13 +62,13 @@
33.4
33.5 lemma eq_real_number_of [simp]:
33.6 "((number_of v :: real) = number_of v') =
33.7 - iszero (number_of (bin_add v (bin_minus v')))"
33.8 + iszero (number_of (bin_add v (bin_minus v')) :: int)"
33.9 by (simp only: real_number_of_def real_of_int_inject eq_number_of_eq)
33.10
33.11 text{*@{term neg} is used in rewrite rules for binary comparisons*}
33.12 lemma less_real_number_of [simp]:
33.13 "((number_of v :: real) < number_of v') =
33.14 - neg (number_of (bin_add v (bin_minus v')))"
33.15 + neg (number_of (bin_add v (bin_minus v')) :: int)"
33.16 by (simp only: real_number_of_def real_of_int_less_iff less_number_of_eq_neg)
33.17
33.18
33.19 @@ -134,12 +134,12 @@
33.20 have. *}
33.21 lemma real_of_nat_number_of [simp]:
33.22 "real (number_of v :: nat) =
33.23 - (if neg (number_of v) then 0
33.24 + (if neg (number_of v :: int) then 0
33.25 else (number_of v :: real))"
33.26 proof cases
33.27 - assume "neg (number_of v)" thus ?thesis by simp
33.28 + assume "neg (number_of v :: int)" thus ?thesis by simp
33.29 next
33.30 - assume neg: "~ neg (number_of v)"
33.31 + assume neg: "~ neg (number_of v :: int)"
33.32 thus ?thesis
33.33 by (simp only: nat_number_of_def real_of_nat_real_of_int [OF neg], simp)
33.34 qed
33.35 @@ -222,7 +222,7 @@
33.36
33.37 lemma abs_nat_number_of [simp]:
33.38 "abs (number_of v :: real) =
33.39 - (if neg (number_of v) then number_of (bin_minus v)
33.40 + (if neg (number_of v :: int) then number_of (bin_minus v)
33.41 else number_of v)"
33.42 by (simp add: real_abs_def bin_arith_simps minus_real_number_of
33.43 less_real_number_of real_of_int_le_iff)
34.1 --- a/src/HOL/Real/RealDef.thy Thu Feb 05 10:45:28 2004 +0100
34.2 +++ b/src/HOL/Real/RealDef.thy Tue Feb 10 12:02:11 2004 +0100
34.3 @@ -23,9 +23,8 @@
34.4 instance real :: inverse ..
34.5
34.6 consts
34.7 - (*Overloaded constants denoting the Nat and Real subsets of enclosing
34.8 + (*Overloaded constant denoting the Real subset of enclosing
34.9 types such as hypreal and complex*)
34.10 - Nats :: "'a set"
34.11 Reals :: "'a set"
34.12
34.13 (*overloaded constant for injecting other types into "real"*)
34.14 @@ -85,16 +84,6 @@
34.15
34.16 syntax (xsymbols)
34.17 Reals :: "'a set" ("\<real>")
34.18 - Nats :: "'a set" ("\<nat>")
34.19 -
34.20 -
34.21 -defs (overloaded)
34.22 - real_of_int_def:
34.23 - "real z == Abs_REAL(\<Union>(i,j) \<in> Rep_Integ z. realrel ``
34.24 - {(preal_of_rat(rat(int(Suc i))),
34.25 - preal_of_rat(rat(int(Suc j))))})"
34.26 -
34.27 - real_of_nat_def: "real n == real (int n)"
34.28
34.29
34.30 subsection{*Proving that realrel is an equivalence relation*}
34.31 @@ -172,30 +161,6 @@
34.32 apply (simp add: Rep_REAL_inverse)
34.33 done
34.34
34.35 -lemma real_eq_iff:
34.36 - "[|(x1,y1) \<in> Rep_REAL w; (x2,y2) \<in> Rep_REAL z|]
34.37 - ==> (z = w) = (x1+y2 = x2+y1)"
34.38 -apply (insert quotient_eq_iff
34.39 - [OF equiv_realrel,
34.40 - of "Rep_REAL w" "Rep_REAL z" "(x1,y1)" "(x2,y2)"])
34.41 -apply (simp add: Rep_REAL [unfolded REAL_def] Rep_REAL_inject eq_commute)
34.42 -done
34.43 -
34.44 -lemma mem_REAL_imp_eq:
34.45 - "[|R \<in> REAL; (x1,y1) \<in> R; (x2,y2) \<in> R|] ==> x1+y2 = x2+y1"
34.46 -apply (auto simp add: REAL_def realrel_def quotient_def)
34.47 -apply (blast dest: preal_trans_lemma)
34.48 -done
34.49 -
34.50 -lemma Rep_REAL_cancel_right:
34.51 - "((x + z, y + z) \<in> Rep_REAL R) = ((x, y) \<in> Rep_REAL R)"
34.52 -apply (rule_tac z = R in eq_Abs_REAL, simp)
34.53 -apply (rename_tac u v)
34.54 -apply (subgoal_tac "(u + (y + z) = x + z + v) = ((u + y) + z = (x + v) + z)")
34.55 - prefer 2 apply (simp add: preal_add_ac)
34.56 -apply (simp add: preal_add_right_cancel_iff)
34.57 -done
34.58 -
34.59
34.60 subsection{*Congruence property for addition*}
34.61
34.62 @@ -218,21 +183,21 @@
34.63 done
34.64
34.65 lemma real_add_commute: "(z::real) + w = w + z"
34.66 -apply (rule_tac z = z in eq_Abs_REAL)
34.67 -apply (rule_tac z = w in eq_Abs_REAL)
34.68 +apply (rule eq_Abs_REAL [of z])
34.69 +apply (rule eq_Abs_REAL [of w])
34.70 apply (simp add: preal_add_ac real_add)
34.71 done
34.72
34.73 lemma real_add_assoc: "((z1::real) + z2) + z3 = z1 + (z2 + z3)"
34.74 -apply (rule_tac z = z1 in eq_Abs_REAL)
34.75 -apply (rule_tac z = z2 in eq_Abs_REAL)
34.76 -apply (rule_tac z = z3 in eq_Abs_REAL)
34.77 +apply (rule eq_Abs_REAL [of z1])
34.78 +apply (rule eq_Abs_REAL [of z2])
34.79 +apply (rule eq_Abs_REAL [of z3])
34.80 apply (simp add: real_add preal_add_assoc)
34.81 done
34.82
34.83 lemma real_add_zero_left: "(0::real) + z = z"
34.84 apply (unfold real_of_preal_def real_zero_def)
34.85 -apply (rule_tac z = z in eq_Abs_REAL)
34.86 +apply (rule eq_Abs_REAL [of z])
34.87 apply (simp add: real_add preal_add_ac)
34.88 done
34.89
34.90 @@ -263,7 +228,7 @@
34.91
34.92 lemma real_add_minus_left: "(-z) + z = (0::real)"
34.93 apply (unfold real_zero_def)
34.94 -apply (rule_tac z = z in eq_Abs_REAL)
34.95 +apply (rule eq_Abs_REAL [of z])
34.96 apply (simp add: real_minus real_add preal_add_commute)
34.97 done
34.98
34.99 @@ -283,7 +248,7 @@
34.100
34.101 lemma real_mult_congruent2:
34.102 "congruent2 realrel (%p1 p2.
34.103 - (%(x1,y1). (%(x2,y2). realrel``{(x1*x2 + y1*y2, x1*y2+x2*y1)}) p2) p1)"
34.104 + (%(x1,y1). (%(x2,y2). realrel``{(x1*x2 + y1*y2, x1*y2+x2*y1)}) p2) p1)"
34.105 apply (rule equiv_realrel [THEN congruent2_commuteI], clarify)
34.106 apply (unfold split_def)
34.107 apply (simp add: preal_mult_commute preal_add_commute)
34.108 @@ -298,29 +263,29 @@
34.109 done
34.110
34.111 lemma real_mult_commute: "(z::real) * w = w * z"
34.112 -apply (rule_tac z = z in eq_Abs_REAL)
34.113 -apply (rule_tac z = w in eq_Abs_REAL)
34.114 +apply (rule eq_Abs_REAL [of z])
34.115 +apply (rule eq_Abs_REAL [of w])
34.116 apply (simp add: real_mult preal_add_ac preal_mult_ac)
34.117 done
34.118
34.119 lemma real_mult_assoc: "((z1::real) * z2) * z3 = z1 * (z2 * z3)"
34.120 -apply (rule_tac z = z1 in eq_Abs_REAL)
34.121 -apply (rule_tac z = z2 in eq_Abs_REAL)
34.122 -apply (rule_tac z = z3 in eq_Abs_REAL)
34.123 +apply (rule eq_Abs_REAL [of z1])
34.124 +apply (rule eq_Abs_REAL [of z2])
34.125 +apply (rule eq_Abs_REAL [of z3])
34.126 apply (simp add: preal_add_mult_distrib2 real_mult preal_add_ac preal_mult_ac)
34.127 done
34.128
34.129 lemma real_mult_1: "(1::real) * z = z"
34.130 apply (unfold real_one_def)
34.131 -apply (rule_tac z = z in eq_Abs_REAL)
34.132 +apply (rule eq_Abs_REAL [of z])
34.133 apply (simp add: real_mult preal_add_mult_distrib2 preal_mult_1_right
34.134 preal_mult_ac preal_add_ac)
34.135 done
34.136
34.137 lemma real_add_mult_distrib: "((z1::real) + z2) * w = (z1 * w) + (z2 * w)"
34.138 -apply (rule_tac z = z1 in eq_Abs_REAL)
34.139 -apply (rule_tac z = z2 in eq_Abs_REAL)
34.140 -apply (rule_tac z = w in eq_Abs_REAL)
34.141 +apply (rule eq_Abs_REAL [of z1])
34.142 +apply (rule eq_Abs_REAL [of z2])
34.143 +apply (rule eq_Abs_REAL [of w])
34.144 apply (simp add: preal_add_mult_distrib2 real_add real_mult preal_add_ac preal_mult_ac)
34.145 done
34.146
34.147 @@ -344,7 +309,7 @@
34.148
34.149 lemma real_mult_inverse_left_ex: "x \<noteq> 0 ==> \<exists>y. y*x = (1::real)"
34.150 apply (unfold real_zero_def real_one_def)
34.151 -apply (rule_tac z = x in eq_Abs_REAL)
34.152 +apply (rule eq_Abs_REAL [of x])
34.153 apply (cut_tac x = xa and y = y in linorder_less_linear)
34.154 apply (auto dest!: less_add_left_Ex simp add: real_zero_iff)
34.155 apply (rule_tac
34.156 @@ -420,63 +385,69 @@
34.157 subsection{*The @{text "\<le>"} Ordering*}
34.158
34.159 lemma real_le_refl: "w \<le> (w::real)"
34.160 -apply (rule_tac z = w in eq_Abs_REAL)
34.161 +apply (rule eq_Abs_REAL [of w])
34.162 apply (force simp add: real_le_def)
34.163 done
34.164
34.165 -lemma real_le_trans_lemma:
34.166 - assumes le1: "x1 + y2 \<le> x2 + y1"
34.167 - and le2: "u1 + v2 \<le> u2 + v1"
34.168 - and eq: "x2 + v1 = u1 + y2"
34.169 - shows "x1 + v2 + u1 + y2 \<le> u2 + u1 + y2 + (y1::preal)"
34.170 +text{*The arithmetic decision procedure is not set up for type preal.
34.171 + This lemma is currently unused, but it could simplify the proofs of the
34.172 + following two lemmas.*}
34.173 +lemma preal_eq_le_imp_le:
34.174 + assumes eq: "a+b = c+d" and le: "c \<le> a"
34.175 + shows "b \<le> (d::preal)"
34.176 proof -
34.177 - have "x1 + v2 + u1 + y2 = (x1 + y2) + (u1 + v2)" by (simp add: preal_add_ac)
34.178 - also have "... \<le> (x2 + y1) + (u1 + v2)"
34.179 - by (simp add: prems preal_add_le_cancel_right)
34.180 - also have "... \<le> (x2 + y1) + (u2 + v1)"
34.181 + have "c+d \<le> a+d" by (simp add: prems preal_cancels)
34.182 + hence "a+b \<le> a+d" by (simp add: prems)
34.183 + thus "b \<le> d" by (simp add: preal_cancels)
34.184 +qed
34.185 +
34.186 +lemma real_le_lemma:
34.187 + assumes l: "u1 + v2 \<le> u2 + v1"
34.188 + and "x1 + v1 = u1 + y1"
34.189 + and "x2 + v2 = u2 + y2"
34.190 + shows "x1 + y2 \<le> x2 + (y1::preal)"
34.191 +proof -
34.192 + have "(x1+v1) + (u2+y2) = (u1+y1) + (x2+v2)" by (simp add: prems)
34.193 + hence "(x1+y2) + (u2+v1) = (x2+y1) + (u1+v2)" by (simp add: preal_add_ac)
34.194 + also have "... \<le> (x2+y1) + (u2+v1)"
34.195 by (simp add: prems preal_add_le_cancel_left)
34.196 - also have "... = (x2 + v1) + (u2 + y1)" by (simp add: preal_add_ac)
34.197 - also have "... = (u1 + y2) + (u2 + y1)" by (simp add: prems)
34.198 - also have "... = u2 + u1 + y2 + y1" by (simp add: preal_add_ac)
34.199 - finally show ?thesis .
34.200 + finally show ?thesis by (simp add: preal_add_le_cancel_right)
34.201 +qed
34.202 +
34.203 +lemma real_le:
34.204 + "(Abs_REAL(realrel``{(x1,y1)}) \<le> Abs_REAL(realrel``{(x2,y2)})) =
34.205 + (x1 + y2 \<le> x2 + y1)"
34.206 +apply (simp add: real_le_def)
34.207 +apply (auto intro: real_le_lemma);
34.208 +done
34.209 +
34.210 +lemma real_le_anti_sym: "[| z \<le> w; w \<le> z |] ==> z = (w::real)"
34.211 +apply (rule eq_Abs_REAL [of z])
34.212 +apply (rule eq_Abs_REAL [of w])
34.213 +apply (simp add: real_le order_antisym)
34.214 +done
34.215 +
34.216 +lemma real_trans_lemma:
34.217 + assumes "x + v \<le> u + y"
34.218 + and "u + v' \<le> u' + v"
34.219 + and "x2 + v2 = u2 + y2"
34.220 + shows "x + v' \<le> u' + (y::preal)"
34.221 +proof -
34.222 + have "(x+v') + (u+v) = (x+v) + (u+v')" by (simp add: preal_add_ac)
34.223 + also have "... \<le> (u+y) + (u+v')"
34.224 + by (simp add: preal_add_le_cancel_right prems)
34.225 + also have "... \<le> (u+y) + (u'+v)"
34.226 + by (simp add: preal_add_le_cancel_left prems)
34.227 + also have "... = (u'+y) + (u+v)" by (simp add: preal_add_ac)
34.228 + finally show ?thesis by (simp add: preal_add_le_cancel_right)
34.229 qed
34.230
34.231 lemma real_le_trans: "[| i \<le> j; j \<le> k |] ==> i \<le> (k::real)"
34.232 -apply (simp add: real_le_def, clarify)
34.233 -apply (rename_tac x1 u1 y1 v1 x2 u2 y2 v2)
34.234 -apply (drule mem_REAL_imp_eq [OF Rep_REAL], assumption)
34.235 -apply (rule_tac x=x1 in exI)
34.236 -apply (rule_tac x=y1 in exI)
34.237 -apply (rule_tac x="u2 + (x2 + v1)" in exI)
34.238 -apply (rule_tac x="v2 + (u1 + y2)" in exI)
34.239 -apply (simp add: Rep_REAL_cancel_right preal_add_le_cancel_right
34.240 - preal_add_assoc [symmetric] real_le_trans_lemma)
34.241 -done
34.242 -
34.243 -lemma real_le_anti_sym_lemma:
34.244 - assumes le1: "x1 + y2 \<le> x2 + y1"
34.245 - and le2: "u1 + v2 \<le> u2 + v1"
34.246 - and eq1: "x1 + v2 = u2 + y1"
34.247 - and eq2: "x2 + v1 = u1 + y2"
34.248 - shows "x2 + y1 = x1 + (y2::preal)"
34.249 -proof (rule order_antisym)
34.250 - show "x1 + y2 \<le> x2 + y1" .
34.251 - have "(x2 + y1) + (u1+u2) = x2 + u1 + (u2 + y1)" by (simp add: preal_add_ac)
34.252 - also have "... = x2 + u1 + (x1 + v2)" by (simp add: prems)
34.253 - also have "... = (x2 + x1) + (u1 + v2)" by (simp add: preal_add_ac)
34.254 - also have "... \<le> (x2 + x1) + (u2 + v1)"
34.255 - by (simp add: preal_add_le_cancel_left)
34.256 - also have "... = (x1 + u2) + (x2 + v1)" by (simp add: preal_add_ac)
34.257 - also have "... = (x1 + u2) + (u1 + y2)" by (simp add: prems)
34.258 - also have "... = (x1 + y2) + (u1 + u2)" by (simp add: preal_add_ac)
34.259 - finally show "x2 + y1 \<le> x1 + y2" by (simp add: preal_add_le_cancel_right)
34.260 -qed
34.261 -
34.262 -lemma real_le_anti_sym: "[| z \<le> w; w \<le> z |] ==> z = (w::real)"
34.263 -apply (simp add: real_le_def, clarify)
34.264 -apply (rule real_eq_iff [THEN iffD2], assumption+)
34.265 -apply (drule mem_REAL_imp_eq [OF Rep_REAL], assumption)+
34.266 -apply (blast intro: real_le_anti_sym_lemma)
34.267 +apply (rule eq_Abs_REAL [of i])
34.268 +apply (rule eq_Abs_REAL [of j])
34.269 +apply (rule eq_Abs_REAL [of k])
34.270 +apply (simp add: real_le)
34.271 +apply (blast intro: real_trans_lemma)
34.272 done
34.273
34.274 (* Axiom 'order_less_le' of class 'order': *)
34.275 @@ -488,124 +459,50 @@
34.276 (assumption |
34.277 rule real_le_refl real_le_trans real_le_anti_sym real_less_le)+
34.278
34.279 -text{*Simplifies a strange formula that occurs quantified.*}
34.280 -lemma preal_strange_le_eq: "(x1 + x2 \<le> x2 + y1) = (x1 \<le> (y1::preal))"
34.281 -by (simp add: preal_add_commute [of x1] preal_add_le_cancel_left)
34.282 -
34.283 -text{*This is the nicest way to prove linearity*}
34.284 -lemma real_le_linear_0: "(z::real) \<le> 0 | 0 \<le> z"
34.285 -apply (rule_tac z = z in eq_Abs_REAL)
34.286 -apply (auto simp add: real_le_def real_zero_def preal_add_ac
34.287 - preal_cancels preal_strange_le_eq)
34.288 -apply (cut_tac x=x and y=y in linorder_linear, auto)
34.289 +(* Axiom 'linorder_linear' of class 'linorder': *)
34.290 +lemma real_le_linear: "(z::real) \<le> w | w \<le> z"
34.291 +apply (rule eq_Abs_REAL [of z])
34.292 +apply (rule eq_Abs_REAL [of w])
34.293 +apply (auto simp add: real_le real_zero_def preal_add_ac preal_cancels)
34.294 +apply (cut_tac x="x+ya" and y="xa+y" in linorder_linear)
34.295 +apply (auto );
34.296 done
34.297
34.298 -lemma real_minus_zero_le_iff: "(0 \<le> -R) = (R \<le> (0::real))"
34.299 -apply (rule_tac z = R in eq_Abs_REAL)
34.300 -apply (force simp add: real_le_def real_zero_def real_minus preal_add_ac
34.301 - preal_cancels preal_strange_le_eq)
34.302 -done
34.303 -
34.304 -lemma real_le_imp_diff_le_0: "x \<le> y ==> x-y \<le> (0::real)"
34.305 -apply (rule_tac z = x in eq_Abs_REAL)
34.306 -apply (rule_tac z = y in eq_Abs_REAL)
34.307 -apply (auto simp add: real_le_def real_zero_def real_diff_def real_minus
34.308 - real_add preal_add_ac preal_cancels preal_strange_le_eq)
34.309 -apply (rule exI)+
34.310 -apply (rule conjI, assumption)
34.311 -apply (subgoal_tac " x + (x2 + y1 + ya) = (x + y1) + (x2 + ya)")
34.312 - prefer 2 apply (simp (no_asm) only: preal_add_ac)
34.313 -apply (subgoal_tac "x1 + y2 + (xa + y) = (x1 + y) + (xa + y2)")
34.314 - prefer 2 apply (simp (no_asm) only: preal_add_ac)
34.315 -apply simp
34.316 -done
34.317 -
34.318 -lemma real_diff_le_0_imp_le: "x-y \<le> (0::real) ==> x \<le> y"
34.319 -apply (rule_tac z = x in eq_Abs_REAL)
34.320 -apply (rule_tac z = y in eq_Abs_REAL)
34.321 -apply (auto simp add: real_le_def real_zero_def real_diff_def real_minus
34.322 - real_add preal_add_ac preal_cancels preal_strange_le_eq)
34.323 -apply (rule exI)+
34.324 -apply (rule conjI, rule_tac [2] conjI)
34.325 - apply (rule_tac [2] refl)+
34.326 -apply (subgoal_tac "(x + ya) + (x1 + y1) \<le> (xa + y) + (x1 + y1)")
34.327 -apply (simp add: preal_cancels)
34.328 -apply (subgoal_tac "x1 + (x + (y1 + ya)) \<le> y1 + (x1 + (xa + y))")
34.329 - apply (simp add: preal_add_ac)
34.330 -apply (simp add: preal_cancels)
34.331 -done
34.332 -
34.333 -lemma real_le_eq_diff: "(x \<le> y) = (x-y \<le> (0::real))"
34.334 -by (blast intro!: real_diff_le_0_imp_le real_le_imp_diff_le_0)
34.335 -
34.336 -
34.337 -(* Axiom 'linorder_linear' of class 'linorder': *)
34.338 -lemma real_le_linear: "(z::real) \<le> w | w \<le> z"
34.339 -apply (insert real_le_linear_0 [of "z-w"])
34.340 -apply (auto simp add: real_le_eq_diff [of w] real_le_eq_diff [of z]
34.341 - real_minus_zero_le_iff [symmetric])
34.342 -done
34.343
34.344 instance real :: linorder
34.345 by (intro_classes, rule real_le_linear)
34.346
34.347
34.348 +lemma real_le_eq_diff: "(x \<le> y) = (x-y \<le> (0::real))"
34.349 +apply (rule eq_Abs_REAL [of x])
34.350 +apply (rule eq_Abs_REAL [of y])
34.351 +apply (auto simp add: real_le real_zero_def real_diff_def real_add real_minus
34.352 + preal_add_ac)
34.353 +apply (simp_all add: preal_add_assoc [symmetric] preal_cancels)
34.354 +done
34.355 +
34.356 lemma real_add_left_mono: "x \<le> y ==> z + x \<le> z + (y::real)"
34.357 apply (auto simp add: real_le_eq_diff [of x] real_le_eq_diff [of "z+x"])
34.358 apply (subgoal_tac "z + x - (z + y) = (z + -z) + (x - y)")
34.359 prefer 2 apply (simp add: diff_minus add_ac, simp)
34.360 done
34.361
34.362 -
34.363 -lemma real_minus_zero_le_iff2: "(-R \<le> 0) = (0 \<le> (R::real))"
34.364 -apply (rule_tac z = R in eq_Abs_REAL)
34.365 -apply (force simp add: real_le_def real_zero_def real_minus preal_add_ac
34.366 - preal_cancels preal_strange_le_eq)
34.367 -done
34.368 -
34.369 -lemma real_minus_zero_less_iff: "(0 < -R) = (R < (0::real))"
34.370 -by (simp add: linorder_not_le [symmetric] real_minus_zero_le_iff2)
34.371 -
34.372 -lemma real_minus_zero_less_iff2: "(-R < 0) = ((0::real) < R)"
34.373 -by (simp add: linorder_not_le [symmetric] real_minus_zero_le_iff)
34.374 -
34.375 lemma real_sum_gt_zero_less: "(0 < S + (-W::real)) ==> (W < S)"
34.376 by (simp add: linorder_not_le [symmetric] real_le_eq_diff [of S] diff_minus)
34.377
34.378 -text{*Used a few times in Lim and Transcendental*}
34.379 lemma real_less_sum_gt_zero: "(W < S) ==> (0 < S + (-W::real))"
34.380 by (simp add: linorder_not_le [symmetric] real_le_eq_diff [of S] diff_minus)
34.381
34.382 -text{*Handles other strange cases that arise in these proofs.*}
34.383 -lemma forall_imp_less: "\<forall>u v. u \<le> v \<longrightarrow> x + v \<noteq> u + (y::preal) ==> y < x";
34.384 -apply (drule_tac x=x in spec)
34.385 -apply (drule_tac x=y in spec)
34.386 -apply (simp add: preal_add_commute linorder_not_le)
34.387 -done
34.388 -
34.389 -text{*The arithmetic decision procedure is not set up for type preal.*}
34.390 -lemma preal_eq_le_imp_le:
34.391 - assumes eq: "a+b = c+d" and le: "c \<le> a"
34.392 - shows "b \<le> (d::preal)"
34.393 -proof -
34.394 - have "c+d \<le> a+d" by (simp add: prems preal_cancels)
34.395 - hence "a+b \<le> a+d" by (simp add: prems)
34.396 - thus "b \<le> d" by (simp add: preal_cancels)
34.397 -qed
34.398 -
34.399 lemma real_mult_order: "[| 0 < x; 0 < y |] ==> (0::real) < x * y"
34.400 -apply (simp add: linorder_not_le [symmetric])
34.401 +apply (rule eq_Abs_REAL [of x])
34.402 +apply (rule eq_Abs_REAL [of y])
34.403 +apply (simp add: linorder_not_le [where 'a = real, symmetric]
34.404 + linorder_not_le [where 'a = preal]
34.405 + real_zero_def real_le real_mult)
34.406 --{*Reduce to the (simpler) @{text "\<le>"} relation *}
34.407 -apply (rule_tac z = x in eq_Abs_REAL)
34.408 -apply (rule_tac z = y in eq_Abs_REAL)
34.409 -apply (auto simp add: real_zero_def real_le_def real_mult preal_add_ac
34.410 - preal_cancels preal_strange_le_eq)
34.411 -apply (drule preal_eq_le_imp_le, assumption)
34.412 -apply (auto dest!: forall_imp_less less_add_left_Ex
34.413 +apply (auto dest!: less_add_left_Ex
34.414 simp add: preal_add_ac preal_mult_ac
34.415 - preal_add_mult_distrib preal_add_mult_distrib2)
34.416 -apply (insert preal_self_less_add_right)
34.417 -apply (simp add: linorder_not_le [symmetric])
34.418 + preal_add_mult_distrib2 preal_cancels preal_self_less_add_right)
34.419 done
34.420
34.421 lemma real_mult_less_mono2: "[| (0::real) < z; x < y |] ==> z * x < z * y"
34.422 @@ -617,13 +514,11 @@
34.423
34.424 text{*lemma for proving @{term "0<(1::real)"}*}
34.425 lemma real_zero_le_one: "0 \<le> (1::real)"
34.426 -apply (auto simp add: real_zero_def real_one_def real_le_def preal_add_ac
34.427 - preal_cancels)
34.428 -apply (rule_tac x="preal_of_rat 1 + preal_of_rat 1" in exI)
34.429 -apply (rule_tac x="preal_of_rat 1" in exI)
34.430 -apply (auto simp add: preal_add_ac preal_self_less_add_left order_less_imp_le)
34.431 +apply (simp add: real_zero_def real_one_def real_le
34.432 + preal_self_less_add_left order_less_imp_le)
34.433 done
34.434
34.435 +
34.436 subsection{*The Reals Form an Ordered Field*}
34.437
34.438 instance real :: ordered_field
34.439 @@ -658,7 +553,7 @@
34.440 lemma real_of_preal_trichotomy:
34.441 "\<exists>m. (x::real) = real_of_preal m | x = 0 | x = -(real_of_preal m)"
34.442 apply (unfold real_of_preal_def real_zero_def)
34.443 -apply (rule_tac z = x in eq_Abs_REAL)
34.444 +apply (rule eq_Abs_REAL [of x])
34.445 apply (auto simp add: real_minus preal_add_ac)
34.446 apply (cut_tac x = x and y = y in linorder_less_linear)
34.447 apply (auto dest!: less_add_left_Ex simp add: preal_add_assoc [symmetric])
34.448 @@ -824,126 +719,43 @@
34.449
34.450 subsection{*Embedding the Integers into the Reals*}
34.451
34.452 -lemma real_of_int_congruent:
34.453 - "congruent intrel (%p. (%(i,j). realrel ``
34.454 - {(preal_of_rat (rat (int(Suc i))), preal_of_rat (rat (int(Suc j))))}) p)"
34.455 -apply (simp add: congruent_def add_ac del: int_Suc, clarify)
34.456 -(*OPTION raised if only is changed to add?????????*)
34.457 -apply (simp only: add_Suc_right zero_less_rat_of_int_iff zadd_int
34.458 - preal_of_rat_add [symmetric] rat_of_int_add_distrib [symmetric], simp)
34.459 -done
34.460 -
34.461 -lemma real_of_int:
34.462 - "real (Abs_Integ (intrel `` {(i, j)})) =
34.463 - Abs_REAL(realrel ``
34.464 - {(preal_of_rat (rat (int(Suc i))),
34.465 - preal_of_rat (rat (int(Suc j))))})"
34.466 -apply (unfold real_of_int_def)
34.467 -apply (rule_tac f = Abs_REAL in arg_cong)
34.468 -apply (simp del: int_Suc
34.469 - add: realrel_in_real [THEN Abs_REAL_inverse]
34.470 - UN_equiv_class [OF equiv_intrel real_of_int_congruent])
34.471 -done
34.472 -
34.473 -lemma inj_real_of_int: "inj(real :: int => real)"
34.474 -apply (rule inj_onI)
34.475 -apply (rule_tac z = x in eq_Abs_Integ)
34.476 -apply (rule_tac z = y in eq_Abs_Integ, clarify)
34.477 -apply (simp del: int_Suc
34.478 - add: real_of_int zadd_int preal_of_rat_eq_iff
34.479 - preal_of_rat_add [symmetric] rat_of_int_add_distrib [symmetric])
34.480 -done
34.481 -
34.482 -lemma real_of_int_int_zero: "real (int 0) = 0"
34.483 -by (simp add: int_def real_zero_def real_of_int preal_add_commute)
34.484 +defs (overloaded)
34.485 + real_of_nat_def: "real z == of_nat z"
34.486 + real_of_int_def: "real z == of_int z"
34.487
34.488 lemma real_of_int_zero [simp]: "real (0::int) = 0"
34.489 -by (insert real_of_int_int_zero, simp)
34.490 +by (simp add: real_of_int_def)
34.491
34.492 lemma real_of_one [simp]: "real (1::int) = (1::real)"
34.493 -apply (subst int_1 [symmetric])
34.494 -apply (simp add: int_def real_one_def)
34.495 -apply (simp add: real_of_int preal_of_rat_add [symmetric])
34.496 -done
34.497 +by (simp add: real_of_int_def)
34.498
34.499 lemma real_of_int_add: "real (x::int) + real y = real (x + y)"
34.500 -apply (rule_tac z = x in eq_Abs_Integ)
34.501 -apply (rule_tac z = y in eq_Abs_Integ, clarify)
34.502 -apply (simp del: int_Suc
34.503 - add: pos_add_strict real_of_int real_add zadd
34.504 - preal_of_rat_add [symmetric], simp)
34.505 -done
34.506 +by (simp add: real_of_int_def)
34.507 declare real_of_int_add [symmetric, simp]
34.508
34.509 lemma real_of_int_minus: "-real (x::int) = real (-x)"
34.510 -apply (rule_tac z = x in eq_Abs_Integ)
34.511 -apply (auto simp add: real_of_int real_minus zminus)
34.512 -done
34.513 +by (simp add: real_of_int_def)
34.514 declare real_of_int_minus [symmetric, simp]
34.515
34.516 lemma real_of_int_diff: "real (x::int) - real y = real (x - y)"
34.517 -by (simp only: zdiff_def real_diff_def real_of_int_add real_of_int_minus)
34.518 +by (simp add: real_of_int_def)
34.519 declare real_of_int_diff [symmetric, simp]
34.520
34.521 lemma real_of_int_mult: "real (x::int) * real y = real (x * y)"
34.522 -apply (rule_tac z = x in eq_Abs_Integ)
34.523 -apply (rule_tac z = y in eq_Abs_Integ)
34.524 -apply (rename_tac a b c d)
34.525 -apply (simp del: int_Suc
34.526 - add: pos_add_strict mult_pos real_of_int real_mult zmult
34.527 - preal_of_rat_add [symmetric] preal_of_rat_mult [symmetric])
34.528 -apply (rule_tac f=preal_of_rat in arg_cong)
34.529 -apply (simp only: int_Suc right_distrib add_ac mult_ac zadd_int zmult_int
34.530 - rat_of_int_add_distrib [symmetric] rat_of_int_mult_distrib [symmetric]
34.531 - rat_inject)
34.532 -done
34.533 +by (simp add: real_of_int_def)
34.534 declare real_of_int_mult [symmetric, simp]
34.535
34.536 -lemma real_of_int_Suc: "real (int (Suc n)) = real (int n) + (1::real)"
34.537 -by (simp only: real_of_one [symmetric] zadd_int add_ac int_Suc real_of_int_add)
34.538 -
34.539 lemma real_of_int_zero_cancel [simp]: "(real x = 0) = (x = (0::int))"
34.540 -by (auto intro: inj_real_of_int [THEN injD])
34.541 -
34.542 -lemma zero_le_real_of_int: "0 \<le> real y ==> 0 \<le> (y::int)"
34.543 -apply (rule_tac z = y in eq_Abs_Integ)
34.544 -apply (simp add: real_le_def, clarify)
34.545 -apply (rename_tac a b c d)
34.546 -apply (simp del: int_Suc zdiff_def [symmetric]
34.547 - add: real_zero_def real_of_int zle_def zless_def zdiff_def zadd
34.548 - zminus neg_def preal_add_ac preal_cancels)
34.549 -apply (drule sym, drule preal_eq_le_imp_le, assumption)
34.550 -apply (simp del: int_Suc add: preal_of_rat_le_iff)
34.551 -done
34.552 -
34.553 -lemma real_of_int_le_cancel:
34.554 - assumes le: "real (x::int) \<le> real y"
34.555 - shows "x \<le> y"
34.556 -proof -
34.557 - have "real x - real x \<le> real y - real x" using le
34.558 - by (simp only: diff_minus add_le_cancel_right)
34.559 - hence "0 \<le> real y - real x" by simp
34.560 - hence "0 \<le> y - x" by (simp only: real_of_int_diff zero_le_real_of_int)
34.561 - hence "0 + x \<le> (y - x) + x" by (simp only: add_le_cancel_right)
34.562 - thus "x \<le> y" by simp
34.563 -qed
34.564 +by (simp add: real_of_int_def)
34.565
34.566 lemma real_of_int_inject [iff]: "(real (x::int) = real y) = (x = y)"
34.567 -by (blast dest!: inj_real_of_int [THEN injD])
34.568 -
34.569 -lemma real_of_int_less_cancel: "real (x::int) < real y ==> x < y"
34.570 -by (auto simp add: order_less_le real_of_int_le_cancel)
34.571 -
34.572 -lemma real_of_int_less_mono: "x < y ==> (real (x::int) < real y)"
34.573 -apply (simp add: linorder_not_le [symmetric])
34.574 -apply (auto dest!: real_of_int_less_cancel simp add: order_le_less)
34.575 -done
34.576 +by (simp add: real_of_int_def)
34.577
34.578 lemma real_of_int_less_iff [iff]: "(real (x::int) < real y) = (x < y)"
34.579 -by (blast dest: real_of_int_less_cancel intro: real_of_int_less_mono)
34.580 +by (simp add: real_of_int_def)
34.581
34.582 lemma real_of_int_le_iff [simp]: "(real (x::int) \<le> real y) = (x \<le> y)"
34.583 -by (simp add: linorder_not_less [symmetric])
34.584 +by (simp add: real_of_int_def)
34.585
34.586
34.587 subsection{*Embedding the Naturals into the Reals*}
34.588 @@ -955,73 +767,64 @@
34.589 by (simp add: real_of_nat_def)
34.590
34.591 lemma real_of_nat_add [simp]: "real (m + n) = real (m::nat) + real n"
34.592 -by (simp add: real_of_nat_def add_ac)
34.593 +by (simp add: real_of_nat_def)
34.594
34.595 (*Not for addsimps: often the LHS is used to represent a positive natural*)
34.596 lemma real_of_nat_Suc: "real (Suc n) = real n + (1::real)"
34.597 -by (simp add: real_of_nat_def add_ac)
34.598 +by (simp add: real_of_nat_def)
34.599
34.600 lemma real_of_nat_less_iff [iff]:
34.601 "(real (n::nat) < real m) = (n < m)"
34.602 by (simp add: real_of_nat_def)
34.603
34.604 lemma real_of_nat_le_iff [iff]: "(real (n::nat) \<le> real m) = (n \<le> m)"
34.605 -by (simp add: linorder_not_less [symmetric])
34.606 -
34.607 -lemma inj_real_of_nat: "inj (real :: nat => real)"
34.608 -apply (rule inj_onI)
34.609 -apply (simp add: real_of_nat_def)
34.610 -done
34.611 +by (simp add: real_of_nat_def)
34.612
34.613 lemma real_of_nat_ge_zero [iff]: "0 \<le> real (n::nat)"
34.614 -apply (insert real_of_int_le_iff [of 0 "int n"])
34.615 -apply (simp add: real_of_nat_def)
34.616 -done
34.617 +by (simp add: real_of_nat_def zero_le_imp_of_nat)
34.618
34.619 lemma real_of_nat_Suc_gt_zero: "0 < real (Suc n)"
34.620 -by (insert real_of_nat_less_iff [of 0 "Suc n"], simp)
34.621 +by (simp add: real_of_nat_def del: of_nat_Suc)
34.622
34.623 lemma real_of_nat_mult [simp]: "real (m * n) = real (m::nat) * real n"
34.624 -by (simp add: real_of_nat_def zmult_int [symmetric])
34.625 +by (simp add: real_of_nat_def)
34.626
34.627 lemma real_of_nat_inject [iff]: "(real (n::nat) = real m) = (n = m)"
34.628 -by (auto dest: inj_real_of_nat [THEN injD])
34.629 +by (simp add: real_of_nat_def)
34.630
34.631 lemma real_of_nat_zero_iff: "(real (n::nat) = 0) = (n = 0)"
34.632 - proof
34.633 - assume "real n = 0"
34.634 - have "real n = real (0::nat)" by simp
34.635 - then show "n = 0" by (simp only: real_of_nat_inject)
34.636 - next
34.637 - show "n = 0 \<Longrightarrow> real n = 0" by simp
34.638 - qed
34.639 +by (simp add: real_of_nat_def)
34.640
34.641 lemma real_of_nat_diff: "n \<le> m ==> real (m - n) = real (m::nat) - real n"
34.642 -by (simp add: real_of_nat_def zdiff_int [symmetric])
34.643 -
34.644 -lemma real_of_nat_neg_int [simp]: "neg z ==> real (nat z) = 0"
34.645 -by (simp add: neg_nat)
34.646 +by (simp add: add: real_of_nat_def)
34.647
34.648 lemma real_of_nat_gt_zero_cancel_iff [simp]: "(0 < real (n::nat)) = (0 < n)"
34.649 -by (rule real_of_nat_less_iff [THEN subst], auto)
34.650 +by (simp add: add: real_of_nat_def)
34.651
34.652 lemma real_of_nat_le_zero_cancel_iff [simp]: "(real (n::nat) \<le> 0) = (n = 0)"
34.653 -apply (rule real_of_nat_zero [THEN subst])
34.654 -apply (simp only: real_of_nat_le_iff, simp)
34.655 -done
34.656 -
34.657 +by (simp add: add: real_of_nat_def)
34.658
34.659 lemma not_real_of_nat_less_zero [simp]: "~ real (n::nat) < 0"
34.660 -by (simp add: linorder_not_less real_of_nat_ge_zero)
34.661 +by (simp add: add: real_of_nat_def)
34.662
34.663 lemma real_of_nat_ge_zero_cancel_iff [simp]: "(0 \<le> real (n::nat)) = (0 \<le> n)"
34.664 -by (simp add: linorder_not_less)
34.665 +by (simp add: add: real_of_nat_def)
34.666
34.667 lemma real_of_int_real_of_nat: "real (int n) = real n"
34.668 -by (simp add: real_of_nat_def)
34.669 +by (simp add: real_of_nat_def real_of_int_def int_eq_of_nat)
34.670
34.671 +
34.672 +
34.673 +text{*Still needed for binary arith*}
34.674 lemma real_of_nat_real_of_int: "~neg z ==> real (nat z) = real z"
34.675 -by (simp add: not_neg_eq_ge_0 real_of_nat_def)
34.676 +proof (simp add: not_neg_eq_ge_0 real_of_nat_def real_of_int_def)
34.677 + assume "0 \<le> z"
34.678 + hence eq: "of_nat (nat z) = z"
34.679 + by (simp add: nat_0_le int_eq_of_nat[symmetric])
34.680 + have "of_nat (nat z) = of_int (of_nat (nat z))" by simp
34.681 + also have "... = of_int z" by (simp add: eq)
34.682 + finally show "of_nat (nat z) = of_int z" .
34.683 +qed
34.684
34.685 ML
34.686 {*
34.687 @@ -1031,7 +834,6 @@
34.688 val real_diff_def = thm "real_diff_def";
34.689 val real_divide_def = thm "real_divide_def";
34.690
34.691 -val preal_trans_lemma = thm"preal_trans_lemma";
34.692 val realrel_iff = thm"realrel_iff";
34.693 val realrel_refl = thm"realrel_refl";
34.694 val equiv_realrel = thm"equiv_realrel";
34.695 @@ -1099,20 +901,14 @@
34.696 val real_inverse_unique = thm "real_inverse_unique";
34.697 val real_inverse_gt_one = thm "real_inverse_gt_one";
34.698
34.699 -val real_of_int = thm"real_of_int";
34.700 -val inj_real_of_int = thm"inj_real_of_int";
34.701 val real_of_int_zero = thm"real_of_int_zero";
34.702 val real_of_one = thm"real_of_one";
34.703 val real_of_int_add = thm"real_of_int_add";
34.704 val real_of_int_minus = thm"real_of_int_minus";
34.705 val real_of_int_diff = thm"real_of_int_diff";
34.706 val real_of_int_mult = thm"real_of_int_mult";
34.707 -val real_of_int_Suc = thm"real_of_int_Suc";
34.708 val real_of_int_real_of_nat = thm"real_of_int_real_of_nat";
34.709 -val real_of_nat_real_of_int = thm"real_of_nat_real_of_int";
34.710 -val real_of_int_less_cancel = thm"real_of_int_less_cancel";
34.711 val real_of_int_inject = thm"real_of_int_inject";
34.712 -val real_of_int_less_mono = thm"real_of_int_less_mono";
34.713 val real_of_int_less_iff = thm"real_of_int_less_iff";
34.714 val real_of_int_le_iff = thm"real_of_int_le_iff";
34.715 val real_of_nat_zero = thm "real_of_nat_zero";
34.716 @@ -1121,14 +917,12 @@
34.717 val real_of_nat_Suc = thm "real_of_nat_Suc";
34.718 val real_of_nat_less_iff = thm "real_of_nat_less_iff";
34.719 val real_of_nat_le_iff = thm "real_of_nat_le_iff";
34.720 -val inj_real_of_nat = thm "inj_real_of_nat";
34.721 val real_of_nat_ge_zero = thm "real_of_nat_ge_zero";
34.722 val real_of_nat_Suc_gt_zero = thm "real_of_nat_Suc_gt_zero";
34.723 val real_of_nat_mult = thm "real_of_nat_mult";
34.724 val real_of_nat_inject = thm "real_of_nat_inject";
34.725 val real_of_nat_diff = thm "real_of_nat_diff";
34.726 val real_of_nat_zero_iff = thm "real_of_nat_zero_iff";
34.727 -val real_of_nat_neg_int = thm "real_of_nat_neg_int";
34.728 val real_of_nat_gt_zero_cancel_iff = thm "real_of_nat_gt_zero_cancel_iff";
34.729 val real_of_nat_le_zero_cancel_iff = thm "real_of_nat_le_zero_cancel_iff";
34.730 val not_real_of_nat_less_zero = thm "not_real_of_nat_less_zero";
35.1 --- a/src/HOL/Real/rat_arith.ML Thu Feb 05 10:45:28 2004 +0100
35.2 +++ b/src/HOL/Real/rat_arith.ML Tue Feb 10 12:02:11 2004 +0100
35.3 @@ -19,18 +19,6 @@
35.4 val rat_number_of_def = thm "rat_number_of_def";
35.5 val diff_rat_def = thm "diff_rat_def";
35.6
35.7 -val rat_of_int_zero = thm "rat_of_int_zero";
35.8 -val rat_of_int_one = thm "rat_of_int_one";
35.9 -val rat_of_int_add_distrib = thm "rat_of_int_add_distrib";
35.10 -val rat_of_int_minus_distrib = thm "rat_of_int_minus_distrib";
35.11 -val rat_of_int_diff_distrib = thm "rat_of_int_diff_distrib";
35.12 -val rat_of_int_mult_distrib = thm "rat_of_int_mult_distrib";
35.13 -val rat_inject = thm "rat_inject";
35.14 -val rat_of_int_zero_cancel = thm "rat_of_int_zero_cancel";
35.15 -val rat_of_int_less_iff = thm "rat_of_int_less_iff";
35.16 -val rat_of_int_le_iff = thm "rat_of_int_le_iff";
35.17 -
35.18 -val number_of_rat = thm "number_of_rat";
35.19 val rat_numeral_0_eq_0 = thm "rat_numeral_0_eq_0";
35.20 val rat_numeral_1_eq_1 = thm "rat_numeral_1_eq_1";
35.21 val add_rat_number_of = thm "add_rat_number_of";
35.22 @@ -615,9 +603,8 @@
35.23 val simps = [True_implies_equals,
35.24 inst "a" "(number_of ?v)" right_distrib,
35.25 divide_1, times_divide_eq_right, times_divide_eq_left,
35.26 - rat_of_int_zero, rat_of_int_one, rat_of_int_add_distrib,
35.27 - rat_of_int_minus_distrib, rat_of_int_diff_distrib,
35.28 - rat_of_int_mult_distrib, number_of_rat RS sym];
35.29 + of_int_0, of_int_1, of_int_add, of_int_minus, of_int_diff,
35.30 + of_int_mult, of_int_of_nat_eq, rat_number_of_def];
35.31
35.32 in
35.33
35.34 @@ -625,8 +612,11 @@
35.35 "fast_rat_arith" ["(m::rat) < n","(m::rat) <= n", "(m::rat) = n"]
35.36 Fast_Arith.lin_arith_prover;
35.37
35.38 -val int_inj_thms = [rat_of_int_le_iff RS iffD2, rat_of_int_less_iff RS iffD2,
35.39 - rat_inject RS iffD2];
35.40 +val nat_inj_thms = [of_nat_le_iff RS iffD2, of_nat_less_iff RS iffD2,
35.41 + of_nat_eq_iff RS iffD2];
35.42 +
35.43 +val int_inj_thms = [of_int_le_iff RS iffD2, of_int_less_iff RS iffD2,
35.44 + of_int_eq_iff RS iffD2];
35.45
35.46 val rat_arith_setup =
35.47 [Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset} =>
35.48 @@ -637,7 +627,8 @@
35.49 simpset = simpset addsimps add_rules
35.50 addsimps simps
35.51 addsimprocs simprocs}),
35.52 - arith_inj_const ("Rational.rat", HOLogic.intT --> Rat_Numeral_Simprocs.ratT),
35.53 + arith_inj_const("IntDef.of_nat", HOLogic.natT --> Rat_Numeral_Simprocs.ratT),
35.54 + arith_inj_const("IntDef.of_int", HOLogic.intT --> Rat_Numeral_Simprocs.ratT),
35.55 arith_discrete ("Rational.rat",false),
35.56 Simplifier.change_simpset_of (op addsimprocs) [fast_rat_arith_simproc]];
35.57
36.1 --- a/src/HOL/UNITY/Simple/Lift.thy Thu Feb 05 10:45:28 2004 +0100
36.2 +++ b/src/HOL/UNITY/Simple/Lift.thy Tue Feb 10 12:02:11 2004 +0100
36.3 @@ -215,13 +215,13 @@
36.4 lemma moving_up: "Lift \<in> Always moving_up"
36.5 apply (rule AlwaysI, force)
36.6 apply (unfold Lift_def, constrains)
36.7 -apply (auto dest: zle_imp_zless_or_eq simp add: add1_zle_eq)
36.8 +apply (auto dest: order_le_imp_less_or_eq simp add: add1_zle_eq)
36.9 done
36.10
36.11 lemma moving_down: "Lift \<in> Always moving_down"
36.12 apply (rule AlwaysI, force)
36.13 apply (unfold Lift_def, constrains)
36.14 -apply (blast dest: zle_imp_zless_or_eq)
36.15 +apply (blast dest: order_le_imp_less_or_eq)
36.16 done
36.17
36.18 lemma bounded: "Lift \<in> Always bounded"
36.19 @@ -290,7 +290,7 @@
36.20 "Lift \<in> (Req n \<inter> closed - (atFloor n - queueing))
36.21 LeadsTo ((closed \<inter> goingup \<inter> Req n) \<union>
36.22 (closed \<inter> goingdown \<inter> Req n))"
36.23 -by (auto intro!: subset_imp_LeadsTo elim!: int_neqE)
36.24 +by (auto intro!: subset_imp_LeadsTo simp add: linorder_neq_iff)
36.25
36.26 (*lift_2*)
36.27 lemma (in Floor) lift_2: "Lift \<in> (Req n \<inter> closed - (atFloor n - queueing))
37.1 --- a/src/HOL/ex/BinEx.thy Thu Feb 05 10:45:28 2004 +0100
37.2 +++ b/src/HOL/ex/BinEx.thy Tue Feb 10 12:02:11 2004 +0100
37.3 @@ -470,7 +470,7 @@
37.4 apply assumption
37.5 apply (simp add: normal_Pls_eq_0)
37.6 apply (simp only: number_of_minus zminus_0 iszero_def
37.7 - zminus_equation [of _ "0"])
37.8 + minus_equation_iff [of _ "0"])
37.9 apply (simp add: eq_commute)
37.10 done
37.11