# HG changeset patch # User paulson # Date 905441396 -7200 # Node ID 1dbaf888f4e75a6625525f8005a002b9b656b19e # Parent 0e26af5975ba91b8ce835d628951e12d0f609c3a well-formed asym rules; misc. tidying diff -r 0e26af5975ba -r 1dbaf888f4e7 src/HOL/Real/PNat.ML --- a/src/HOL/Real/PNat.ML Thu Sep 10 17:28:36 1998 +0200 +++ b/src/HOL/Real/PNat.ML Thu Sep 10 17:29:56 1998 +0200 @@ -246,8 +246,8 @@ by (etac less_not_sym 1); qed "pnat_less_not_sym"; -(* [| x < y; y < x |] ==> P *) -bind_thm ("pnat_less_asym",pnat_less_not_sym RS notE); +(* [| x < y; ~P ==> y < x |] ==> P *) +bind_thm ("pnat_less_asym", pnat_less_not_sym RS swap); Goalw [pnat_less_def] "~ y < (y::pnat)"; by Auto_tac; diff -r 0e26af5975ba -r 1dbaf888f4e7 src/HOL/Real/PRat.ML --- a/src/HOL/Real/PRat.ML Thu Sep 10 17:28:36 1998 +0200 +++ b/src/HOL/Real/PRat.ML Thu Sep 10 17:29:56 1998 +0200 @@ -395,14 +395,14 @@ (*** y < y ==> P ***) bind_thm("prat_less_irrefl",prat_less_not_refl RS notE); -Goal "!! (q1::prat). [| q1 < q2; q2 < q1 |] ==> P"; +Goal "!! (q1::prat). q1 < q2 ==> ~ q2 < q1"; +by (rtac notI 1); by (dtac prat_less_trans 1 THEN assume_tac 1); by (asm_full_simp_tac (simpset() addsimps [prat_less_not_refl]) 1); -qed "prat_less_asym"; +qed "prat_less_not_sym"; -Goal "!! (q1::prat). q1 < q2 ==> ~ q2 < q1"; -by (auto_tac (claset() addSDs [prat_less_asym],simpset())); -qed "prat_less_not_sym"; +(* [| x < y; ~P ==> y < x |] ==> P *) +bind_thm ("prat_less_asym", prat_less_not_sym RS swap); (* half of positive fraction exists- Gleason p. 120- Proposition 9-2.6(i)*) Goal "!(q::prat). ? x. x + x = q"; diff -r 0e26af5975ba -r 1dbaf888f4e7 src/HOL/Real/PReal.ML --- a/src/HOL/Real/PReal.ML Thu Sep 10 17:28:36 1998 +0200 +++ b/src/HOL/Real/PReal.ML Thu Sep 10 17:29:56 1998 +0200 @@ -137,10 +137,10 @@ by Auto_tac; by (dtac prat_dense 1 THEN etac exE 1); by (eres_inst_tac [("c","xa")] equalityCE 1); -by (auto_tac (claset() addDs [prat_less_asym],simpset())); +by (auto_tac (claset() addDs [prat_less_not_sym],simpset())); by (dtac prat_dense 1 THEN etac exE 1); by (eres_inst_tac [("c","xa")] equalityCE 1); -by (auto_tac (claset() addDs [prat_less_asym],simpset())); +by (auto_tac (claset() addDs [prat_less_not_sym],simpset())); qed "lemma_prat_set_eq"; Goal "inj(preal_prat)"; @@ -203,10 +203,14 @@ simpset() addsimps [psubset_def])); qed "preal_less_trans"; -Goal "!! (q1::preal). [| q1 < q2; q2 < q1 |] ==> P"; +Goal "!! (q1::preal). q1 < q2 ==> ~ q2 < q1"; +by (rtac notI 1); by (dtac preal_less_trans 1 THEN assume_tac 1); by (asm_full_simp_tac (simpset() addsimps [preal_less_not_refl]) 1); -qed "preal_less_asym"; +qed "preal_less_not_sym"; + +(* [| x < y; ~P ==> y < x |] ==> P *) +bind_thm ("preal_less_asym", preal_less_not_sym RS swap); Goalw [preal_less_def] "(r1::preal) < r2 | r1 = r2 | r2 < r1"; @@ -217,9 +221,8 @@ by (fast_tac (claset() addDs [not_in_preal_ub]) 1); qed "preal_linear"; -Goal - "!!(r1::preal). [| r1 < r2 ==> P; r1 = r2 ==> P; \ -\ r2 < r1 ==> P |] ==> P"; +Goal "!!(r1::preal). [| r1 < r2 ==> P; r1 = r2 ==> P; \ +\ r2 < r1 ==> P |] ==> P"; by (cut_inst_tac [("r1.0","r1"),("r2.0","r2")] preal_linear 1); by Auto_tac; qed "preal_linear_less2"; diff -r 0e26af5975ba -r 1dbaf888f4e7 src/HOL/Real/Real.ML --- a/src/HOL/Real/Real.ML Thu Sep 10 17:28:36 1998 +0200 +++ b/src/HOL/Real/Real.ML Thu Sep 10 17:29:56 1998 +0200 @@ -4,8 +4,6 @@ Description : The reals *) -open Real; - (*** Proving that realrel is an equivalence relation ***) Goal "[| (x1::preal) + y2 = x2 + y1; x2 + y3 = x3 + y2 |] \ @@ -22,18 +20,18 @@ Goalw [realrel_def] "(((x1,y1),(x2,y2)): realrel) = (x1 + y2 = x2 + y1)"; -by (Fast_tac 1); +by (Blast_tac 1); qed "realrel_iff"; Goalw [realrel_def] "[| x1 + y2 = x2 + y1 |] ==> ((x1,y1),(x2,y2)): realrel"; -by (Fast_tac 1); +by (Blast_tac 1); qed "realrelI"; Goalw [realrel_def] "p: realrel --> (EX x1 y1 x2 y2. \ \ p = ((x1,y1),(x2,y2)) & x1 + y2 = x2 + y1)"; -by (Fast_tac 1); +by (Blast_tac 1); qed "realrelE_lemma"; val [major,minor] = goal thy @@ -90,7 +88,7 @@ by (REPEAT (rtac realrel_in_real 1)); by (dtac eq_equiv_class 1); by (rtac equiv_realrel 1); -by (Fast_tac 1); +by (Blast_tac 1); by Safe_tac; by (Asm_full_simp_tac 1); qed "inj_real_preal"; @@ -219,7 +217,7 @@ qed "real_add_minus_left"; Goal "? y. (x::real) + y = 0r"; -by (fast_tac (claset() addIs [real_add_minus]) 1); +by (blast_tac (claset() addIs [real_add_minus]) 1); qed "real_minus_ex"; Goal "?! y. (x::real) + y = 0r"; @@ -247,7 +245,7 @@ Goal "? y. x = %~y"; by (cut_inst_tac [("x","x")] real_minus_ex 1); by (etac exE 1 THEN dtac real_add_minus_eq_minus 1); -by (Fast_tac 1); +by (Blast_tac 1); qed "real_as_add_inverse_ex"; (* real_minus_add_distrib *) @@ -499,13 +497,13 @@ "P < (Q::real) = (EX x1 y1 x2 y2. x1 + y2 < x2 + y1 & \ \ (x1,y1::preal):Rep_real(P) & \ \ (x2,y2):Rep_real(Q))"; -by (Fast_tac 1); +by (Blast_tac 1); qed "real_less_iff"; Goalw [real_less_def] "[| x1 + y2 < x2 + y1; (x1,y1::preal):Rep_real(P); \ \ (x2,y2):Rep_real(Q) |] ==> P < (Q::real)"; -by (Fast_tac 1); +by (Blast_tac 1); qed "real_lessI"; Goalw [real_less_def] @@ -521,7 +519,7 @@ "R1 < (R2::real) ==> (EX x1 y1 x2 y2. x1 + y2 < x2 + y1 & \ \ (x1,y1::preal):Rep_real(R1) & \ \ (x2,y2):Rep_real(R2))"; -by (Fast_tac 1); +by (Blast_tac 1); qed "real_lessD"; (* real_less is a strong order i.e nonreflexive and transitive *) @@ -621,7 +619,7 @@ qed "real_preal_ExD"; Goal "(? m. Abs_real (realrel ^^ {(x,y)}) = %#m) = (y < x)"; -by (fast_tac (claset() addSIs [real_preal_ExI,real_preal_ExD]) 1); +by (blast_tac (claset() addSIs [real_preal_ExI,real_preal_ExD]) 1); qed "real_preal_iff"; (*** Gleason prop 9-4.4 p 127 ***) @@ -654,13 +652,13 @@ real_preal_def,real_less_def])); by (REPEAT(rtac exI 1)); by (EVERY[rtac conjI 1, rtac conjI 2]); -by (REPEAT(Fast_tac 2)); +by (REPEAT(Blast_tac 2)); by (simp_tac (simpset() addsimps [preal_self_less_add_left] delsimps [preal_add_less_iff2]) 1); qed "real_preal_lessI"; Goal "(%#m1 < %#m2) = (m1 < m2)"; -by (fast_tac (claset() addIs [real_preal_lessI,real_preal_lessD]) 1); +by (blast_tac (claset() addIs [real_preal_lessI,real_preal_lessD]) 1); qed "real_preal_less_iff1"; Addsimps [real_preal_less_iff1]; @@ -670,7 +668,7 @@ [real_preal_def,real_less_def,real_minus])); by (REPEAT(rtac exI 1)); by (EVERY[rtac conjI 1, rtac conjI 2]); -by (REPEAT(Fast_tac 2)); +by (REPEAT(Blast_tac 2)); by (full_simp_tac (simpset() addsimps preal_add_ac) 1); by (full_simp_tac (simpset() addsimps [preal_self_less_add_right, preal_add_assoc RS sym]) 1); @@ -681,15 +679,15 @@ [real_preal_def,real_less_def,real_minus])); by (REPEAT(rtac exI 1)); by (EVERY[rtac conjI 1, rtac conjI 2]); -by (REPEAT(Fast_tac 2)); +by (REPEAT(Blast_tac 2)); by (full_simp_tac (simpset() addsimps [preal_self_less_add_right] @ preal_add_ac) 1); qed "real_preal_minus_less_zero"; Goal "~ 0r < %~ %#m"; by (cut_facts_tac [real_preal_minus_less_zero] 1); -by (fast_tac (claset() addDs [real_less_trans] - addEs [real_less_irrefl]) 1); +by (blast_tac (claset() addDs [real_less_trans] + addEs [real_less_irrefl]) 1); qed "real_preal_not_minus_gt_zero"; Goalw [real_zero_def] " 0r < %#m"; @@ -697,14 +695,14 @@ [real_preal_def,real_less_def,real_minus])); by (REPEAT(rtac exI 1)); by (EVERY[rtac conjI 1, rtac conjI 2]); -by (REPEAT(Fast_tac 2)); +by (REPEAT(Blast_tac 2)); by (full_simp_tac (simpset() addsimps [preal_self_less_add_right] @ preal_add_ac) 1); qed "real_preal_zero_less"; Goal "~ %#m < 0r"; by (cut_facts_tac [real_preal_zero_less] 1); -by (fast_tac (claset() addDs [real_less_trans] +by (blast_tac (claset() addDs [real_less_trans] addEs [real_less_irrefl]) 1); qed "real_preal_not_less_zero"; @@ -719,7 +717,7 @@ [real_preal_def,real_less_def,real_add])); by (REPEAT(rtac exI 1)); by (EVERY[rtac conjI 1, rtac conjI 2]); -by (REPEAT(Fast_tac 2)); +by (REPEAT(Blast_tac 2)); by (full_simp_tac (simpset() addsimps preal_add_ac) 1); by (full_simp_tac (simpset() addsimps [preal_self_less_add_right, preal_add_assoc RS sym]) 1); @@ -730,7 +728,7 @@ [real_preal_def,real_less_def,real_minus])); by (REPEAT(rtac exI 1)); by (EVERY[rtac conjI 1, rtac conjI 2]); -by (REPEAT(Fast_tac 2)); +by (REPEAT(Blast_tac 2)); by (full_simp_tac (simpset() addsimps preal_add_ac) 1); by (full_simp_tac (simpset() addsimps [preal_self_less_add_right, preal_add_assoc RS sym]) 1); @@ -738,7 +736,7 @@ Goal "~ %#m < %~ %#m1"; by (cut_facts_tac [real_preal_minus_less_all] 1); -by (fast_tac (claset() addDs [real_less_trans] +by (blast_tac (claset() addDs [real_less_trans] addEs [real_less_irrefl]) 1); qed "real_preal_not_minus_gt_all"; @@ -747,7 +745,7 @@ [real_preal_def,real_less_def,real_minus])); by (REPEAT(rtac exI 1)); by (EVERY[rtac conjI 1, rtac conjI 2]); -by (REPEAT(Fast_tac 2)); +by (REPEAT(Blast_tac 2)); by (auto_tac (claset(),simpset() addsimps preal_add_ac)); by (asm_full_simp_tac (simpset() addsimps [preal_add_assoc RS sym]) 1); by (auto_tac (claset(),simpset() addsimps preal_add_ac)); @@ -758,7 +756,7 @@ [real_preal_def,real_less_def,real_minus])); by (REPEAT(rtac exI 1)); by (EVERY[rtac conjI 1, rtac conjI 2]); -by (REPEAT(Fast_tac 2)); +by (REPEAT(Blast_tac 2)); by (auto_tac (claset(),simpset() addsimps preal_add_ac)); by (asm_full_simp_tac (simpset() addsimps [preal_add_assoc RS sym]) 1); by (auto_tac (claset(),simpset() addsimps preal_add_ac)); @@ -799,25 +797,25 @@ val real_leE = make_elim real_leD; Goal "(~(w < z)) = (z <= (w::real))"; -by (fast_tac (claset() addSIs [real_leI,real_leD]) 1); +by (blast_tac (claset() addSIs [real_leI,real_leD]) 1); qed "real_less_le_iff"; Goalw [real_le_def] "~ z <= w ==> w<(z::real)"; -by (Fast_tac 1); +by (Blast_tac 1); qed "not_real_leE"; Goalw [real_le_def] "z < w ==> z <= (w::real)"; -by (fast_tac (claset() addEs [real_less_asym]) 1); +by (blast_tac (claset() addEs [real_less_asym]) 1); qed "real_less_imp_le"; Goalw [real_le_def] "!!(x::real). x <= y ==> x < y | x = y"; by (cut_facts_tac [real_linear] 1); -by (fast_tac (claset() addEs [real_less_irrefl,real_less_asym]) 1); +by (blast_tac (claset() addEs [real_less_irrefl,real_less_asym]) 1); qed "real_le_imp_less_or_eq"; Goalw [real_le_def] "z z <=(w::real)"; by (cut_facts_tac [real_linear] 1); -by (fast_tac (claset() addEs [real_less_irrefl,real_less_asym]) 1); +by (blast_tac (claset() addEs [real_less_irrefl,real_less_asym]) 1); qed "real_less_or_eq_imp_le"; Goal "(x <= (y::real)) = (x < y | x=y)"; @@ -830,27 +828,27 @@ val prems = goal Real.thy "!!i. [| i <= j; j < k |] ==> i < (k::real)"; by (dtac real_le_imp_less_or_eq 1); -by (fast_tac (claset() addIs [real_less_trans]) 1); +by (blast_tac (claset() addIs [real_less_trans]) 1); qed "real_le_less_trans"; Goal "!! (i::real). [| i < j; j <= k |] ==> i < k"; by (dtac real_le_imp_less_or_eq 1); -by (fast_tac (claset() addIs [real_less_trans]) 1); +by (blast_tac (claset() addIs [real_less_trans]) 1); qed "real_less_le_trans"; Goal "[| i <= j; j <= k |] ==> i <= (k::real)"; by (EVERY1 [dtac real_le_imp_less_or_eq, dtac real_le_imp_less_or_eq, - rtac real_less_or_eq_imp_le, fast_tac (claset() addIs [real_less_trans])]); + rtac real_less_or_eq_imp_le, blast_tac (claset() addIs [real_less_trans])]); qed "real_le_trans"; Goal "[| z <= w; w <= z |] ==> z = (w::real)"; by (EVERY1 [dtac real_le_imp_less_or_eq, dtac real_le_imp_less_or_eq, - fast_tac (claset() addEs [real_less_irrefl,real_less_asym])]); + blast_tac (claset() addEs [real_less_irrefl,real_less_asym])]); qed "real_le_anti_sym"; Goal "[| ~ y < x; y ~= x |] ==> x < (y::real)"; by (rtac not_real_leE 1); -by (fast_tac (claset() addDs [real_le_imp_less_or_eq]) 1); +by (blast_tac (claset() addDs [real_le_imp_less_or_eq]) 1); qed "not_less_not_eq_real_less"; Goal "(0r < %~R) = (R < 0r)"; @@ -964,7 +962,7 @@ qed "real_sum_gt_zero_less"; Goal "(0r < S + %~W) = (W < S)"; -by (fast_tac (claset() addIs [real_less_sum_gt_zero, +by (blast_tac (claset() addIs [real_less_sum_gt_zero, real_sum_gt_zero_less]) 1); qed "real_less_sum_gt_0_iff"; @@ -986,17 +984,17 @@ (*** alternative definition for real_less ***) Goal "!!(R::real). (? T. 0r < T & R + T = S) = (R < S)"; -by (fast_tac (claset() addSIs [real_less_add_positive_left_Ex, +by (blast_tac (claset() addSIs [real_less_add_positive_left_Ex, real_ex_add_positive_left_less]) 1); qed "real_less_iffdef"; Goal "(0r < x) = (%~x < x)"; -by (Step_tac 1); +by Safe_tac; by (rtac ccontr 2 THEN forward_tac [real_leI RS real_le_imp_less_or_eq] 2); by (Step_tac 2); by (dtac (real_minus_zero_less_iff RS iffD2) 2); -by (fast_tac (claset() addDs [real_less_trans]) 2); +by (blast_tac (claset() addIs [real_less_trans]) 2); by (auto_tac (claset(),simpset() addsimps [real_gt_zero_preal_Ex,real_preal_minus_less_self])); qed "real_gt_zero_iff"; @@ -1120,9 +1118,9 @@ by (forward_tac [real_sup_lemma2] 2 THEN Auto_tac); by (forward_tac [real_sup_lemma2] 1 THEN Auto_tac); by (rtac (preal_complete RS spec RS iffD2 RS bexE) 1); -by (Fast_tac 3); -by (Fast_tac 1); -by (Fast_tac 1); +by (Blast_tac 3); +by (Blast_tac 1); +by (Blast_tac 1); by (Blast_tac 1); qed "posreal_complete"; diff -r 0e26af5975ba -r 1dbaf888f4e7 src/HOL/Real/RealAbs.ML --- a/src/HOL/Real/RealAbs.ML Thu Sep 10 17:28:36 1998 +0200 +++ b/src/HOL/Real/RealAbs.ML Thu Sep 10 17:29:56 1998 +0200 @@ -11,7 +11,7 @@ (adapted version of previously proved theorems about abs) ----------------------------------------------------------------------------*) Goalw [rabs_def] "rabs r = (if 0r<=r then r else %~r)"; -by (Step_tac 1); +by Auto_tac; qed "rabs_iff"; Goalw [rabs_def] "rabs 0r = 0r"; @@ -39,7 +39,7 @@ Goal "x<=0r ==> rabs x = %~x"; by (dtac real_le_imp_less_or_eq 1); -by (fast_tac (HOL_cs addIs [rabs_minus_zero,rabs_minus_eqI2]) 1); +by (blast_tac (HOL_cs addIs [rabs_minus_zero,rabs_minus_eqI2]) 1); qed "rabs_minus_eqI1"; Goalw [rabs_def,real_le_def] "0r<= rabs x"; @@ -154,13 +154,14 @@ qed "real_mult_0_less"; Goal "[| 0r y*x y*x r < rabs(x*y)"; -by (fast_tac (HOL_cs addIs [rabs_mult_le, real_less_le_trans]) 1); +by (blast_tac (HOL_cs addIs [rabs_mult_le, real_less_le_trans]) 1); qed "rabs_mult_gt"; Goal "rabs(x) 0r