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