# HG changeset patch # User wenzelm # Date 957990870 -7200 # Node ID 435187ffc64e288254f06e4483b3897c8abd7355 # Parent ef4848bb0696a82dbc5eb94f80651c3912e505d0 fixed theory deps; diff -r ef4848bb0696 -r 435187ffc64e src/HOL/Real/Hyperreal/Filter.ML --- a/src/HOL/Real/Hyperreal/Filter.ML Wed May 10 21:04:16 2000 +0200 +++ b/src/HOL/Real/Hyperreal/Filter.ML Wed May 10 22:34:30 2000 +0200 @@ -552,5 +552,3 @@ val FreeUltrafilter_Ex = export FreeUltrafilter_ex; Close_locale "UFT"; - - diff -r ef4848bb0696 -r 435187ffc64e src/HOL/Real/Hyperreal/HyperDef.ML --- a/src/HOL/Real/Hyperreal/HyperDef.ML Wed May 10 21:04:16 2000 +0200 +++ b/src/HOL/Real/Hyperreal/HyperDef.ML Wed May 10 22:34:30 2000 +0200 @@ -1857,371 +1857,3 @@ "hypreal_of_nat n = hypreal_of_real (real_of_nat n)"; by (simp_tac (simpset() addsimps [hypreal_add,hypreal_minus]) 1); qed "hypreal_of_nat_real_of_nat"; - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - diff -r ef4848bb0696 -r 435187ffc64e src/HOL/Real/Hyperreal/Zorn.ML --- a/src/HOL/Real/Hyperreal/Zorn.ML Wed May 10 21:04:16 2000 +0200 +++ b/src/HOL/Real/Hyperreal/Zorn.ML Wed May 10 22:34:30 2000 +0200 @@ -289,4 +289,3 @@ Goal "x : Union(c) ==> EX m:c. x:m"; by (Blast_tac 1); qed "mem_UnionD"; - diff -r ef4848bb0696 -r 435187ffc64e src/HOL/Real/PNat.ML --- a/src/HOL/Real/PNat.ML Wed May 10 21:04:16 2000 +0200 +++ b/src/HOL/Real/PNat.ML Wed May 10 22:34:30 2000 +0200 @@ -226,7 +226,8 @@ by (auto_tac (claset() addDs [(inj_on_Abs_pnat RS inj_onD)] addSDs [add_eq_self_zero], simpset() addsimps [sum_Rep_pnat, Rep_pnat,Abs_pnat_inverse, - Rep_pnat_gt_zero RS less_not_refl2])); + Rep_pnat_gt_zero RS less_not_refl2] + delsimprocs Nat_Numeral_Simprocs.cancel_numerals)); qed "pnat_no_add_ident"; diff -r ef4848bb0696 -r 435187ffc64e src/HOL/Real/PNat.thy --- a/src/HOL/Real/PNat.thy Wed May 10 21:04:16 2000 +0200 +++ b/src/HOL/Real/PNat.thy Wed May 10 22:34:30 2000 +0200 @@ -6,7 +6,7 @@ *) -PNat = Arith + +PNat = Main + typedef pnat = "lfp(%X. {1} Un (Suc``X))" (lfp_def) diff -r ef4848bb0696 -r 435187ffc64e src/HOL/Real/PRat.thy --- a/src/HOL/Real/PRat.thy Wed May 10 21:04:16 2000 +0200 +++ b/src/HOL/Real/PRat.thy Wed May 10 22:34:30 2000 +0200 @@ -5,7 +5,7 @@ Description : The positive rationals *) -PRat = PNat + Equiv + +PRat = PNat + constdefs ratrel :: "((pnat * pnat) * (pnat * pnat)) set" diff -r ef4848bb0696 -r 435187ffc64e src/HOL/Real/ROOT.ML --- a/src/HOL/Real/ROOT.ML Wed May 10 21:04:16 2000 +0200 +++ b/src/HOL/Real/ROOT.ML Wed May 10 22:34:30 2000 +0200 @@ -13,7 +13,6 @@ time_use_thy "RealDef"; use "simproc.ML"; time_use_thy "Real"; -time_use_thy "Hyperreal/Filter"; time_use_thy "Hyperreal/HyperDef"; (*FIXME: move to RealBin and eliminate all references to 0r, 1r in diff -r ef4848bb0696 -r 435187ffc64e src/HOL/Real/RealAbs.thy --- a/src/HOL/Real/RealAbs.thy Wed May 10 21:04:16 2000 +0200 +++ b/src/HOL/Real/RealAbs.thy Wed May 10 22:34:30 2000 +0200 @@ -5,6 +5,6 @@ Description : Absolute value function for the reals *) -RealAbs = RealOrd + RealBin + +RealAbs = RealBin + end diff -r ef4848bb0696 -r 435187ffc64e src/HOL/Real/RealBin.thy --- a/src/HOL/Real/RealBin.thy Wed May 10 21:04:16 2000 +0200 +++ b/src/HOL/Real/RealBin.thy Wed May 10 22:34:30 2000 +0200 @@ -8,7 +8,7 @@ This case is reduced to that for the integers *) -RealBin = RealInt + IntArith + +RealBin = RealInt + instance real :: number diff -r ef4848bb0696 -r 435187ffc64e src/HOL/Real/RealInt.ML --- a/src/HOL/Real/RealInt.ML Wed May 10 21:04:16 2000 +0200 +++ b/src/HOL/Real/RealInt.ML Wed May 10 22:34:30 2000 +0200 @@ -80,14 +80,15 @@ Goal "real_of_int (int (Suc n)) = real_of_int (int n) + 1r"; by (simp_tac (simpset() addsimps [real_of_int_one RS sym, - real_of_int_add,zadd_int]) 1); + real_of_int_add,zadd_int] @ zadd_ac) 1); qed "real_of_int_Suc"; (* relating two of the embeddings *) Goal "real_of_int (int n) = real_of_nat n"; by (induct_tac "n" 1); -by (auto_tac (claset(),simpset() addsimps [real_of_int_zero, - real_of_nat_zero,real_of_int_Suc,real_of_nat_Suc])); +by (ALLGOALS (simp_tac (HOL_ss addsimps [real_of_int_zero, + real_of_nat_zero,real_of_int_Suc,real_of_nat_Suc]))); +by (Simp_tac 1); qed "real_of_int_real_of_nat"; Goal "~neg z ==> real_of_nat (nat z) = real_of_int z"; @@ -104,7 +105,7 @@ Goal "(real_of_int x = 0r) = (x = int 0)"; by (auto_tac (claset() addIs [inj_real_of_int RS injD], - simpset() addsimps [real_of_int_zero])); + HOL_ss addsimps [real_of_int_zero])); qed "real_of_int_zero_cancel"; Addsimps [real_of_int_zero_cancel]; @@ -118,7 +119,7 @@ Goal "x < y ==> (real_of_int x < real_of_int y)"; by (auto_tac (claset(), - simpset() addsimps [zless_iff_Suc_zadd, real_of_int_add RS sym, + HOL_ss addsimps [zless_iff_Suc_zadd, real_of_int_add RS sym, real_of_int_real_of_nat, real_of_nat_Suc])); by (simp_tac (simpset() addsimps [real_of_nat_one RS diff -r ef4848bb0696 -r 435187ffc64e src/HOL/Real/RealInt.thy --- a/src/HOL/Real/RealInt.thy Wed May 10 21:04:16 2000 +0200 +++ b/src/HOL/Real/RealInt.thy Wed May 10 22:34:30 2000 +0200 @@ -5,7 +5,7 @@ Description: Embedding the integers in the reals *) -RealInt = RealOrd + Int + +RealInt = RealOrd + constdefs real_of_int :: int => real diff -r ef4848bb0696 -r 435187ffc64e src/HOL/Real/RealOrd.ML --- a/src/HOL/Real/RealOrd.ML Wed May 10 21:04:16 2000 +0200 +++ b/src/HOL/Real/RealOrd.ML Wed May 10 22:34:30 2000 +0200 @@ -812,7 +812,8 @@ by (dtac lemma_nat_not_dense 1); by (auto_tac (claset(), simpset() addsimps [real_of_nat_Suc, real_of_nat_zero] @ - real_add_ac)); + real_add_ac + delsimprocs Nat_Numeral_Simprocs.cancel_numerals)); by (asm_full_simp_tac (simpset() addsimps [real_of_nat_one RS sym, real_of_nat_add,Suc_diff_n]) 1); qed "real_of_nat_minus"; diff -r ef4848bb0696 -r 435187ffc64e src/HOL/Real/RealPow.thy --- a/src/HOL/Real/RealPow.thy Wed May 10 21:04:16 2000 +0200 +++ b/src/HOL/Real/RealPow.thy Wed May 10 22:34:30 2000 +0200 @@ -6,11 +6,11 @@ *) -RealPow = WF_Rel + RealAbs + +RealPow = RealAbs + instance real :: {power} -primrec +primrec (realpow) realpow_0 "r ^ 0 = 1r" realpow_Suc "r ^ (Suc n) = (r::real) * (r ^ n)"