--- a/src/HOL/Algebra/abstract/Ideal.ML Tue Oct 17 08:41:42 2000 +0200
+++ b/src/HOL/Algebra/abstract/Ideal.ML Tue Oct 17 10:20:43 2000 +0200
@@ -199,8 +199,8 @@
Goal "~ (a dvd b) ==> ideal_of {a::'a::ring} < ideal_of {a, b}";
by (asm_simp_tac (simpset() addsimps [psubset_eq, ideal_of_mono]) 1);
-by (simp_tac (simpset() addsimps [ideal_of_2_structure]) 1);
-by (etac contrapos 1);
+by (etac contrapos_pp 1);
+by (full_simp_tac (simpset() addsimps [ideal_of_2_structure]) 1);
by (rtac in_pideal_imp_dvd 1);
by (Asm_simp_tac 1);
by (res_inst_tac [("x", "<0>")] exI 1);
--- a/src/HOL/Algebra/abstract/Ring.ML Tue Oct 17 08:41:42 2000 +0200
+++ b/src/HOL/Algebra/abstract/Ring.ML Tue Oct 17 10:20:43 2000 +0200
@@ -308,10 +308,7 @@
qed "l_integral";
Goal "!! a::'a::domain. [| a ~= <0>; b ~= <0> |] ==> a * b ~= <0>";
-by (etac contrapos 1);
-by (rtac l_integral 1);
-by (assume_tac 1);
-by (assume_tac 1);
+by (blast_tac (claset() addIs [l_integral]) 1);
qed "not_integral";
Addsimps [not_integral];
--- a/src/HOL/Algebra/poly/Degree.ML Tue Oct 17 08:41:42 2000 +0200
+++ b/src/HOL/Algebra/poly/Degree.ML Tue Oct 17 10:20:43 2000 +0200
@@ -6,13 +6,9 @@
(* Relating degree and bound *)
-goal ProtoPoly.thy
- "!! f. [| bound m f; f n ~= <0> |] ==> n <= m";
-by (rtac classical 1);
-by (dtac not_leE 1);
-by (dtac boundD 1 THEN atac 1);
-by (etac notE 1);
-by (assume_tac 1);
+Goal "[| bound m f; f n ~= <0> |] ==> n <= m";
+by (force_tac (claset() addDs [inst "m" "n" boundD],
+ simpset()) 1);
qed "below_bound";
goal UnivPoly.thy "bound (LEAST n. bound n (Rep_UP p)) (Rep_UP p)";
@@ -61,7 +57,7 @@
Goalw [deg_def, coeff_def]
"deg p = Suc y ==> coeff (deg p) p ~= <0>";
-by (rtac classical 1);
+by (rtac ccontr 1);
by (dtac notnotD 1);
by (cut_inst_tac [("p", "p")] Least_is_bound 1);
by (subgoal_tac "bound y (Rep_UP p)" 1);
@@ -94,10 +90,9 @@
qed "deg_lcoeff";
Goal "p ~= <0> ==> coeff (deg p) p ~= <0>";
-by (etac contrapos 1);
-by (ftac contrapos2 1);
-by (rtac deg_lcoeff 1);
-by (assume_tac 1);
+by (etac contrapos_np 1);
+by (case_tac "deg p = 0" 1);
+by (blast_tac (claset() addSDs [deg_lcoeff]) 2);
by (rtac up_eqI 1);
by (case_tac "n=0" 1);
by (rotate_tac ~2 1);
--- a/src/HOL/Algebra/poly/PolyRing.ML Tue Oct 17 08:41:42 2000 +0200
+++ b/src/HOL/Algebra/poly/PolyRing.ML Tue Oct 17 10:20:43 2000 +0200
@@ -67,30 +67,4 @@
val smult_minus = [smult_l_minus, smult_r_minus];
-(* Integrity of smult *)
-(*
-Goal
- "!! a::'a::domain. a *s b = <0> ==> a = <0> | b = <0>";
-by (simp_tac (simpset() addsimps [disj_commute]) 1);
-
-by (rtac (disj_commute RS trans) 1);
-by (rtac contrapos2 1);
-by (assume_tac 1);
-by (rtac up_neqI 1);
-by (Full_simp_tac 1);
-by (etac conjE 1);
-by (rtac not_integral 1);
-by (assume_tac 1);
-by (etac contrapos 1);
-back();
-by (rtac up_eqI 1);
-by (Simp_tac 1);
-
-by (rtac integral 1);
-
-by (etac conjE 1);
-
-by (rtac disjCI 1);
-*)
-
Addsimps [smult_one, smult_l_null, smult_r_null];
--- a/src/HOL/Real/Hyperreal/NSA.ML Tue Oct 17 08:41:42 2000 +0200
+++ b/src/HOL/Real/Hyperreal/NSA.ML Tue Oct 17 10:20:43 2000 +0200
@@ -430,48 +430,48 @@
simpset()));
qed "HFinite_sum_squares";
-Goal "!!x. x ~: Infinitesimal ==> x ~= 0";
+Goal "x ~: Infinitesimal ==> x ~= 0";
by (Auto_tac);
qed "not_Infinitesimal_not_zero";
-Goal "!!x. x: HFinite - Infinitesimal ==> x ~= 0";
+Goal "x: HFinite - Infinitesimal ==> x ~= 0";
by (Auto_tac);
qed "not_Infinitesimal_not_zero2";
-Goal "!!x. x : Infinitesimal ==> abs x : Infinitesimal";
+Goal "x : Infinitesimal ==> abs x : Infinitesimal";
by (res_inst_tac [("x1","x")] (hrabs_disj RS disjE) 1);
by (auto_tac (claset(),simpset() addsimps [Infinitesimal_minus_iff RS sym]));
qed "Infinitesimal_hrabs";
-Goal "!!x. x ~: Infinitesimal ==> abs x ~: Infinitesimal";
+Goal "x ~: Infinitesimal ==> abs x ~: Infinitesimal";
by (res_inst_tac [("x1","x")] (hrabs_disj RS disjE) 1);
by (auto_tac (claset(),simpset() addsimps [Infinitesimal_minus_iff RS sym]));
qed "not_Infinitesimal_hrabs";
-Goal "!!x. abs x : Infinitesimal ==> x : Infinitesimal";
+Goal "abs x : Infinitesimal ==> x : Infinitesimal";
by (rtac ccontr 1);
by (blast_tac (claset() addDs [not_Infinitesimal_hrabs]) 1);
qed "hrabs_Infinitesimal_Infinitesimal";
-Goal "!!x. x : HFinite - Infinitesimal ==> abs x : HFinite - Infinitesimal";
+Goal "x : HFinite - Infinitesimal ==> abs x : HFinite - Infinitesimal";
by (fast_tac (set_cs addSEs [HFinite_hrabs,not_Infinitesimal_hrabs]) 1);
qed "HFinite_diff_Infinitesimal_hrabs";
Goalw [Infinitesimal_def]
- "!!x. [| e : Infinitesimal; abs x < e |] ==> x : Infinitesimal";
+ "[| e : Infinitesimal; abs x < e |] ==> x : Infinitesimal";
by (auto_tac (claset() addSDs [bspec],simpset()));
by (dres_inst_tac [("i","e")] (hrabs_ge_self RS hypreal_le_less_trans) 1);
by (fast_tac (claset() addIs [hypreal_less_trans]) 1);
qed "hrabs_less_Infinitesimal";
Goal
- "!!x. [| e : Infinitesimal; abs x <= e |] ==> x : Infinitesimal";
+ "[| e : Infinitesimal; abs x <= e |] ==> x : Infinitesimal";
by (blast_tac (claset() addDs [hypreal_le_imp_less_or_eq] addIs
[hrabs_Infinitesimal_Infinitesimal,hrabs_less_Infinitesimal]) 1);
qed "hrabs_le_Infinitesimal";
Goalw [Infinitesimal_def]
- "!!x. [| e : Infinitesimal; \
+ "[| e : Infinitesimal; \
\ e' : Infinitesimal; \
\ e' < x ; x < e |] ==> x : Infinitesimal";
by (auto_tac (claset() addSDs [bspec],simpset()));
@@ -524,12 +524,12 @@
addSEs [(hypreal_zero_less_one RSN (2,impE))]) 1);
qed "Infinitesimal_subset_HFinite";
-Goal "!!x. x: Infinitesimal ==> x * hypreal_of_real r : Infinitesimal";
+Goal "x: Infinitesimal ==> x * hypreal_of_real r : Infinitesimal";
by (etac (HFinite_hypreal_of_real RSN
(2,Infinitesimal_HFinite_mult)) 1);
qed "Infinitesimal_hypreal_of_real_mult";
-Goal "!!x. x: Infinitesimal ==> hypreal_of_real r * x: Infinitesimal";
+Goal "x: Infinitesimal ==> hypreal_of_real r * x: Infinitesimal";
by (etac (HFinite_hypreal_of_real RSN
(2,Infinitesimal_HFinite_mult2)) 1);
qed "Infinitesimal_hypreal_of_real_mult2";
@@ -657,7 +657,7 @@
by (Asm_simp_tac 1);
qed "inf_close_eq_imp";
-Goal "!!x. x: Infinitesimal ==> -x @= x";
+Goal "x: Infinitesimal ==> -x @= x";
by (fast_tac (HOL_cs addIs [Infinitesimal_minus_iff RS iffD1,
mem_infmal_iff RS iffD1,inf_close_trans2]) 1);
qed "Infinitesimal_minus_inf_close";
@@ -671,7 +671,7 @@
bex_Infinitesimal_iff RS sym]) 1);
qed "bex_Infinitesimal_iff2";
-Goal "!!x. [| y: Infinitesimal; x + y = z |] ==> x @= z";
+Goal "[| y: Infinitesimal; x + y = z |] ==> x @= z";
by (rtac (bex_Infinitesimal_iff RS iffD1) 1);
by (dtac (Infinitesimal_minus_iff RS iffD1) 1);
by (auto_tac (claset(),simpset() addsimps [hypreal_minus_add_distrib,
@@ -695,13 +695,13 @@
Infinitesimal_minus_iff RS iffD1]) 1);
qed "Infinitesimal_add_minus_inf_close_self";
-Goal "!!x. [| y: Infinitesimal; x+y @= z|] ==> x @= z";
+Goal "[| y: Infinitesimal; x+y @= z|] ==> x @= z";
by (dres_inst_tac [("x","x")] (Infinitesimal_add_inf_close_self RS inf_close_sym) 1);
by (etac (inf_close_trans3 RS inf_close_sym) 1);
by (assume_tac 1);
qed "Infinitesimal_add_cancel";
-Goal "!!x. [| y: Infinitesimal; x @= z + y|] ==> x @= z";
+Goal "[| y: Infinitesimal; x @= z + y|] ==> x @= z";
by (dres_inst_tac [("x","z")] (Infinitesimal_add_inf_close_self2 RS inf_close_sym) 1);
by (etac (inf_close_trans3 RS inf_close_sym) 1);
by (asm_full_simp_tac (simpset() addsimps [hypreal_add_commute]) 1);
@@ -746,7 +746,7 @@
Addsimps [inf_close_add_right_iff];
-Goal "!!x. [| x: HFinite; x @= y |] ==> y: HFinite";
+Goal "[| x: HFinite; x @= y |] ==> y: HFinite";
by (dtac (bex_Infinitesimal_iff2 RS iffD2) 1);
by (Step_tac 1);
by (dtac (Infinitesimal_subset_HFinite RS subsetD
@@ -755,7 +755,7 @@
by (auto_tac (claset(),simpset() addsimps [hypreal_add_assoc]));
qed "inf_close_HFinite";
-Goal "!!x. x @= hypreal_of_real D ==> x: HFinite";
+Goal "x @= hypreal_of_real D ==> x: HFinite";
by (rtac (inf_close_sym RSN (2,inf_close_HFinite)) 1);
by (Auto_tac);
qed "inf_close_hypreal_of_real_HFinite";
@@ -864,18 +864,18 @@
by (simp_tac (simpset() addsimps [SReal_zero]) 1);
qed "zero_mem_SReal_Int_Infinitesimal";
-Goal "!!x. [| x: SReal; x: Infinitesimal|] ==> x = 0";
+Goal "[| x: SReal; x: Infinitesimal|] ==> x = 0";
by (cut_facts_tac [SReal_Int_Infinitesimal_zero] 1);
by (blast_tac (claset() addEs [equalityE]) 1);
qed "SReal_Infinitesimal_zero";
-Goal "!!x. [| x : SReal; x ~= 0 |] \
+Goal "[| x : SReal; x ~= 0 |] \
\ ==> x : HFinite - Infinitesimal";
by (auto_tac (claset() addDs [SReal_Infinitesimal_zero,
SReal_subset_HFinite RS subsetD],simpset()));
qed "SReal_HFinite_diff_Infinitesimal";
-Goal "!!x. hypreal_of_real x ~= 0 ==> hypreal_of_real x : HFinite - Infinitesimal";
+Goal "hypreal_of_real x ~= 0 ==> hypreal_of_real x : HFinite - Infinitesimal";
by (rtac SReal_HFinite_diff_Infinitesimal 1);
by (Auto_tac);
qed "hypreal_of_real_HFinite_diff_Infinitesimal";
@@ -891,19 +891,19 @@
qed "hypreal_one_not_Infinitesimal";
Addsimps [hypreal_one_not_Infinitesimal];
-Goal "!!x. [| y: SReal; x @= y; y~= 0 |] ==> x ~= 0";
+Goal "[| y: SReal; x @= y; y~= 0 |] ==> x ~= 0";
by (cut_inst_tac [("x","y")] hypreal_trichotomy 1);
by (blast_tac (claset() addDs
[inf_close_sym RS (mem_infmal_iff RS iffD2),
SReal_not_Infinitesimal,SReal_minus_not_Infinitesimal]) 1);
qed "inf_close_SReal_not_zero";
-Goal "!!x. [| x @= hypreal_of_real y; hypreal_of_real y ~= 0 |] ==> x ~= 0";
+Goal "[| x @= hypreal_of_real y; hypreal_of_real y ~= 0 |] ==> x ~= 0";
by (rtac inf_close_SReal_not_zero 1);
by (Auto_tac);
qed "inf_close_hypreal_of_real_not_zero";
-Goal "!!x. [| x @= y; y : HFinite - Infinitesimal |] \
+Goal "[| x @= y; y : HFinite - Infinitesimal |] \
\ ==> x : HFinite - Infinitesimal";
by (auto_tac (claset() addIs [inf_close_sym RSN (2,inf_close_HFinite)],
simpset() addsimps [mem_infmal_iff]));
@@ -911,7 +911,7 @@
by (blast_tac (claset() addDs [inf_close_sym]) 1);
qed "HFinite_diff_Infinitesimal_inf_close";
-Goal "!!x. [| y ~= 0; y: Infinitesimal; \
+Goal "[| y ~= 0; y: Infinitesimal; \
\ x*hrinv(y) : HFinite \
\ |] ==> x : Infinitesimal";
by (dtac Infinitesimal_HFinite_mult2 1);
@@ -928,7 +928,7 @@
Uniqueness: Two infinitely close reals are equal
------------------------------------------------------------------*)
-Goal "!!x. [|x: SReal; y: SReal|] ==> (x @= y) = (x = y)";
+Goal "[|x: SReal; y: SReal|] ==> (x @= y) = (x = y)";
by (auto_tac (claset(),simpset() addsimps [inf_close_refl]));
by (rewrite_goals_tac [inf_close_def]);
by (dres_inst_tac [("x","y")] SReal_minus 1);
@@ -961,14 +961,14 @@
addSDs [isLub_le_isUb]) 1);
qed "hypreal_isLub_unique";
-Goal "!!x. x: HFinite ==> EX u. isUb SReal {s. s: SReal & s < x} u";
+Goal "x: HFinite ==> EX u. isUb SReal {s. s: SReal & s < x} u";
by (dtac HFiniteD 1 THEN Step_tac 1);
by (rtac exI 1 THEN rtac isUbI 1 THEN assume_tac 2);
by (auto_tac (claset() addIs [hypreal_less_imp_le,setleI,isUbI,
hypreal_less_trans],simpset() addsimps [hrabs_interval_iff]));
qed "lemma_st_part_ub";
-Goal "!!x. x: HFinite ==> EX y. y: {s. s: SReal & s < x}";
+Goal "x: HFinite ==> EX y. y: {s. s: SReal & s < x}";
by (dtac HFiniteD 1 THEN Step_tac 1);
by (dtac SReal_minus 1);
by (auto_tac (claset(),simpset() addsimps [hrabs_interval_iff]));
@@ -978,7 +978,7 @@
by (Auto_tac);
qed "lemma_st_part_subset";
-Goal "!!x. x: HFinite ==> EX t. isLub SReal {s. s: SReal & s < x} t";
+Goal "x: HFinite ==> EX t. isLub SReal {s. s: SReal & s < x} t";
by (blast_tac (claset() addSIs [SReal_complete,lemma_st_part_ub,
lemma_st_part_nonempty, lemma_st_part_subset]) 1);
qed "lemma_st_part_lub";
@@ -990,7 +990,7 @@
by (auto_tac (claset(),simpset() addsimps [hypreal_add_assoc RS sym]));
qed "lemma_hypreal_le_left_cancel";
-Goal "!!x. [| x: HFinite; \
+Goal "[| x: HFinite; \
\ isLub SReal {s. s: SReal & s < x} t; \
\ r: SReal; 0 < r \
\ |] ==> x <= t + r";
@@ -1013,7 +1013,7 @@
by (blast_tac (claset() addIs [hypreal_setle_less_trans]) 1);
qed "hypreal_gt_isUb";
-Goal "!!x. [| x: HFinite; x < y; y: SReal |] \
+Goal "[| x: HFinite; x < y; y: SReal |] \
\ ==> isUb SReal {s. s: SReal & s < x} y";
by (auto_tac (claset() addDs [hypreal_less_trans]
addIs [hypreal_less_imp_le] addSIs [isUbI,setleI],simpset()));
@@ -1241,20 +1241,20 @@
simpset() addsimps [hypreal_mult_assoc]));
qed "inf_close_hrinv";
-Goal "!!x. [| x: HFinite - Infinitesimal; \
+Goal "[| x: HFinite - Infinitesimal; \
\ h : Infinitesimal |] ==> hrinv(x + h) @= hrinv x";
by (auto_tac (claset() addIs [inf_close_hrinv,
Infinitesimal_add_inf_close_self,inf_close_sym],simpset()));
qed "hrinv_add_Infinitesimal_inf_close";
-Goal "!!x. [| x: HFinite - Infinitesimal; \
+Goal "[| x: HFinite - Infinitesimal; \
\ h : Infinitesimal |] ==> hrinv(h + x) @= hrinv x";
by (rtac (hypreal_add_commute RS subst) 1);
by (blast_tac (claset() addIs [hrinv_add_Infinitesimal_inf_close]) 1);
qed "hrinv_add_Infinitesimal_inf_close2";
Goal
- "!!x. [| x: HFinite - Infinitesimal; \
+ "[| x: HFinite - Infinitesimal; \
\ h : Infinitesimal |] ==> hrinv(x + h) + -hrinv x @= h";
by (rtac inf_close_trans2 1);
by (auto_tac (claset() addIs [hrinv_add_Infinitesimal_inf_close,
@@ -1506,7 +1506,7 @@
Goalw [hypreal_le_def]
"[| xa: Infinitesimal; hypreal_of_real x + xa <= hypreal_of_real y |] \
\ ==> hypreal_of_real x <= hypreal_of_real y";
-by (EVERY1[rtac notI, rtac swap, assume_tac]);
+by (EVERY1[rtac notI, rtac contrapos_np, assume_tac]);
by (res_inst_tac [("C","-xa")] hypreal_less_add_right_cancel 1);
by (auto_tac (claset() addDs [Infinitesimal_minus_iff RS iffD1]
addIs [Infinitesimal_add_hypreal_of_real_less],
@@ -1523,7 +1523,7 @@
"!!xa. [| xa: Infinitesimal; ya: Infinitesimal; \
\ hypreal_of_real x + xa <= hypreal_of_real y + ya \
\ |] ==> hypreal_of_real x <= hypreal_of_real y";
-by (EVERY1[rtac notI, rtac swap, assume_tac]);
+by (EVERY1[rtac notI, rtac contrapos_np, assume_tac]);
by (res_inst_tac [("C","-xa")] hypreal_less_add_right_cancel 1);
by (dtac (Infinitesimal_minus_iff RS iffD1) 1);
by (dtac Infinitesimal_add 1 THEN assume_tac 1);
@@ -1545,7 +1545,7 @@
by (auto_tac (claset(),simpset() addsimps [hypreal_less_not_refl]));
qed "hypreal_of_real_less_Infinitesimal_le_zero";
-Goal "!!x. [| h: Infinitesimal; x ~= 0 |] \
+Goal "[| h: Infinitesimal; x ~= 0 |] \
\ ==> hypreal_of_real x + h ~= 0";
by (res_inst_tac [("t","h")] (hypreal_minus_minus RS subst) 1);
by (rtac (not_sym RS (hypreal_not_eq_minus_iff RS iffD1)) 1);
@@ -1687,7 +1687,7 @@
st_eq_inf_close]) 1);
qed "st_eq_inf_close_iff";
-Goal "!!x. [| x: SReal; e: Infinitesimal |] ==> st(x + e) = x";
+Goal "[| x: SReal; e: Infinitesimal |] ==> st(x + e) = x";
by (forward_tac [st_SReal_eq RS subst] 1);
by (assume_tac 2);
by (forward_tac [SReal_subset_HFinite RS subsetD] 1);
@@ -1744,7 +1744,7 @@
by (auto_tac (claset(),simpset() addsimps hypreal_add_ac));
qed "st_minus";
-Goal "!!x. [| x: HFinite; y: HFinite |] \
+Goal "[| x: HFinite; y: HFinite |] \
\ ==> st (x + -y) = st(x) + -st(y)";
by (forw_inst_tac [("y1","y")] (st_minus RS sym) 1);
by (dres_inst_tac [("x1","y")] (HFinite_minus_iff RS iffD1) 1);
@@ -1752,7 +1752,7 @@
qed "st_add_minus";
(* lemma *)
-Goal "!!x. [| x: HFinite; y: HFinite; \
+Goal "[| x: HFinite; y: HFinite; \
\ e: Infinitesimal; \
\ ea : Infinitesimal \
\ |] ==> e*y + x*ea + e*ea: Infinitesimal";
@@ -1763,7 +1763,7 @@
simpset() addsimps hypreal_add_ac @ hypreal_mult_ac));
qed "lemma_st_mult";
-Goal "!!x. [| x: HFinite; y: HFinite |] \
+Goal "[| x: HFinite; y: HFinite |] \
\ ==> st (x * y) = st(x) * st(y)";
by (forward_tac [HFinite_st_Infinitesimal_add] 1);
by (forw_inst_tac [("x","y")] HFinite_st_Infinitesimal_add 1);
@@ -1788,7 +1788,7 @@
by (fast_tac (claset() addIs [st_zero]) 1);
qed "st_not_zero";
-Goal "!!x. x: Infinitesimal ==> st x = 0";
+Goal "x: Infinitesimal ==> st x = 0";
by (rtac (st_zero RS subst) 1);
by (rtac inf_close_st_eq 1);
by (auto_tac (claset() addIs [Infinitesimal_subset_HFinite
@@ -1814,7 +1814,7 @@
st_mult,prem2,st_not_Infinitesimal,HFinite_hrinv,prem1,st_hrinv]));
qed "st_mult_hrinv";
-Goal "!!x. x: HFinite ==> st(st(x)) = st(x)";
+Goal "x: HFinite ==> st(st(x)) = st(x)";
by (blast_tac (claset() addIs [st_HFinite,
st_inf_close_self,inf_close_st_eq]) 1);
qed "st_idempotent";
@@ -1877,7 +1877,7 @@
Alternative definitions for HFinite using Free ultrafilter
--------------------------------------------------------------------*)
-Goal "!!x. [| X: Rep_hypreal x; Y: Rep_hypreal x |] \
+Goal "[| X: Rep_hypreal x; Y: Rep_hypreal x |] \
\ ==> {n. X n = Y n} : FreeUltrafilterNat";
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
by (Auto_tac);
@@ -1949,7 +1949,7 @@
Exclude this type of sets from free
ultrafilter for Infinite numbers!
-------------------------------------*)
-Goal "!!x. [| xa: Rep_hypreal x; \
+Goal "[| xa: Rep_hypreal x; \
\ {n. abs (xa n) = u} : FreeUltrafilterNat \
\ |] ==> x: HFinite";
by (rtac FreeUltrafilterNat_HFinite 1);
@@ -1987,7 +1987,7 @@
by (auto_tac (claset() addIs [real_less_asym],simpset()));
qed "lemma_Int_HIa";
-Goal "!!x. EX X: Rep_hypreal x. ALL u. \
+Goal "EX X: Rep_hypreal x. ALL u. \
\ {n. u < abs (X n)}: FreeUltrafilterNat\
\ ==> x : HInfinite";
by (rtac (HInfinite_HFinite_iff RS iffD2) 1);
@@ -2021,7 +2021,7 @@
qed "lemma_free5";
Goalw [Infinitesimal_def]
- "!!x. x : Infinitesimal ==> EX X: Rep_hypreal x. \
+ "x : Infinitesimal ==> EX X: Rep_hypreal x. \
\ ALL u. 0 < u --> {n. abs (X n) < u}: FreeUltrafilterNat";
by (auto_tac (claset(),simpset() addsimps [hrabs_interval_iff]));
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
@@ -2036,7 +2036,7 @@
qed "Infinitesimal_FreeUltrafilterNat";
Goalw [Infinitesimal_def]
- "!!x. EX X: Rep_hypreal x. \
+ "EX X: Rep_hypreal x. \
\ ALL u. 0 < u --> \
\ {n. abs (X n) < u}: FreeUltrafilterNat \
\ ==> x : Infinitesimal";
--- a/src/HOLCF/Cfun3.ML Tue Oct 17 08:41:42 2000 +0200
+++ b/src/HOLCF/Cfun3.ML Tue Oct 17 10:20:43 2000 +0200
@@ -335,8 +335,7 @@
Goal "[|!x. rep`(ab`x)=x;!y. ab`(rep`y)=y; z~=UU|] ==> rep`z ~= UU";
-by (etac swap 1);
-by (dtac notnotD 1);
+by (etac contrapos_nn 1);
by (dres_inst_tac [("f","ab")] cfun_arg_cong 1);
by (etac box_equals 1);
by (fast_tac HOL_cs 1);
@@ -345,8 +344,7 @@
qed "isorep_defined";
Goal "[|!x. rep`(ab`x) = x;!y. ab`(rep`y)=y ; z~=UU|] ==> ab`z ~= UU";
-by (etac swap 1);
-by (dtac notnotD 1);
+by (etac contrapos_nn 1);
by (dres_inst_tac [("f","rep")] cfun_arg_cong 1);
by (etac box_equals 1);
by (fast_tac HOL_cs 1);
--- a/src/HOLCF/Fix.ML Tue Oct 17 08:41:42 2000 +0200
+++ b/src/HOLCF/Fix.ML Tue Oct 17 10:20:43 2000 +0200
@@ -367,7 +367,7 @@
(* an admissible formula is also weak admissible *)
(* ------------------------------------------------------------------------ *)
-Goalw [admw_def] "!!P. adm(P)==>admw(P)";
+Goalw [admw_def] "adm(P)==>admw(P)";
by (strip_tac 1);
by (etac admD 1);
by (rtac chain_iterate 1);
@@ -483,7 +483,7 @@
qed "adm_less";
Addsimps [adm_less];
-Goal "!!P. [| adm P; adm Q |] ==> adm(%x. P x & Q x)";
+Goal "[| adm P; adm Q |] ==> adm(%x. P x & Q x)";
by (fast_tac (HOL_cs addEs [admD] addIs [admI]) 1);
qed "adm_conj";
Addsimps [adm_conj];
@@ -493,9 +493,9 @@
qed "adm_not_free";
Addsimps [adm_not_free];
-Goalw [adm_def] "!!t. cont t ==> adm(%x.~ (t x) << u)";
+Goalw [adm_def] "cont t ==> adm(%x.~ (t x) << u)";
by (strip_tac 1);
-by (rtac contrapos 1);
+by (rtac contrapos_nn 1);
by (etac spec 1);
by (rtac trans_less 1);
by (atac 2);
@@ -504,13 +504,13 @@
by (atac 1);
qed "adm_not_less";
-Goal "!!P. !y. adm(P y) ==> adm(%x.!y. P y x)";
+Goal "!y. adm(P y) ==> adm(%x.!y. P y x)";
by (fast_tac (HOL_cs addIs [admI] addEs [admD]) 1);
qed "adm_all";
bind_thm ("adm_all2", allI RS adm_all);
-Goal "!!P. [|cont t; adm P|] ==> adm(%x. P (t x))";
+Goal "[|cont t; adm P|] ==> adm(%x. P (t x))";
by (rtac admI 1);
by (stac (cont2contlub RS contlubE RS spec RS mp) 1);
by (atac 1);
@@ -528,7 +528,7 @@
Goalw [adm_def] "cont(t)==> adm(%x.~ (t x) = UU)";
by (strip_tac 1);
-by (rtac contrapos 1);
+by (rtac contrapos_nn 1);
by (etac spec 1);
by (rtac (chain_UU_I RS spec) 1);
by (etac (cont2mono RS ch2ch_monofun) 1);
@@ -678,7 +678,7 @@
by (atac 1);
qed "adm_lemma11";
-Goal "!!P. [| adm P; adm Q |] ==> adm(%x. P x | Q x)";
+Goal "[| adm P; adm Q |] ==> adm(%x. P x | Q x)";
by (rtac admI 1);
by (rtac (adm_disj_lemma1 RS disjE) 1);
by (atac 1);
@@ -696,7 +696,7 @@
bind_thm("adm_lemma11",adm_lemma11);
bind_thm("adm_disj",adm_disj);
-Goal "!!P. [| adm(%x.~(P x)); adm Q |] ==> adm(%x. P x --> Q x)";
+Goal "[| adm(%x.~(P x)); adm Q |] ==> adm(%x. P x --> Q x)";
by (subgoal_tac "(%x. P x --> Q x) = (%x. ~P x | Q x)" 1);
by (etac ssubst 1);
by (etac adm_disj 1);
--- a/src/HOLCF/IOA/meta_theory/CompoTraces.ML Tue Oct 17 08:41:42 2000 +0200
+++ b/src/HOLCF/IOA/meta_theory/CompoTraces.ML Tue Oct 17 10:20:43 2000 +0200
@@ -451,8 +451,7 @@
qed"FiniteConcUU1";
Goal "~ Finite ((x::'a Seq)@@UU)";
-by (rtac (FiniteConcUU1 COMP rev_contrapos) 1);
-by Auto_tac;
+by (auto_tac (claset() addDs [FiniteConcUU1], simpset()));
qed"FiniteConcUU";
finiteR_mksch
@@ -968,10 +967,10 @@
by (subgoal_tac "schB=UU" 1);
by (Asm_simp_tac 1);
(* first side: mksch = UU *)
-by (SELECT_GOAL (auto_tac (claset() addSIs [ForallQFilterPUU,
- (finiteR_mksch RS mp COMP rev_contrapos),
- ForallAnBmksch],
- simpset())) 1);
+by (force_tac (claset() addSIs [ForallQFilterPUU,
+ (finiteR_mksch RS mp COMP rev_contrapos),
+ ForallAnBmksch],
+ simpset()) 1);
(* schA = UU *)
by (eres_inst_tac [("A","B")] LastActExtimplUU 1);
by (Asm_simp_tac 1);
--- a/src/HOLCF/Sprod0.ML Tue Oct 17 08:41:42 2000 +0200
+++ b/src/HOLCF/Sprod0.ML Tue Oct 17 10:20:43 2000 +0200
@@ -87,7 +87,7 @@
Goal "~Ispair x y = Ispair UU UU ==> ~x=UU & ~y=UU";
by (rtac (de_Morgan_disj RS subst) 1);
-by (etac contrapos 1);
+by (etac contrapos_nn 1);
by (etac strict_Ispair 1);
qed "strict_Ispair_rev";
@@ -101,7 +101,7 @@
qed "defined_Ispair_rev";
Goal "[|a~=UU; b~=UU|] ==> (Ispair a b) ~= (Ispair UU UU)";
-by (rtac contrapos 1);
+by (rtac contrapos_nn 1);
by (etac defined_Ispair_rev 2);
by (rtac (de_Morgan_disj RS iffD2) 1);
by (etac conjI 1);
--- a/src/HOLCF/Sprod3.ML Tue Oct 17 08:41:42 2000 +0200
+++ b/src/HOLCF/Sprod3.ML Tue Oct 17 10:20:43 2000 +0200
@@ -195,7 +195,7 @@
by (rtac chain_UU_I_inverse 1);
by (rtac allI 1);
by (rtac strict_Isfst 1);
-by (rtac swap 1);
+by (rtac contrapos_np 1);
by (etac (defined_IsfstIssnd RS conjunct2) 2);
by (fast_tac (HOL_cs addSDs [monofun_Issnd RS ch2ch_monofun RS chain_UU_I RS spec]) 1);
qed "contlub_Isfst";
@@ -214,7 +214,7 @@
by (rtac chain_UU_I_inverse 1);
by (rtac allI 1);
by (rtac strict_Issnd 1);
-by (rtac swap 1);
+by (rtac contrapos_np 1);
by (etac (defined_IsfstIssnd RS conjunct1) 2);
by (fast_tac (HOL_cs addSDs [monofun_Isfst RS ch2ch_monofun RS chain_UU_I RS spec]) 1);
qed "contlub_Issnd";
--- a/src/HOLCF/Ssum0.ML Tue Oct 17 08:41:42 2000 +0200
+++ b/src/HOLCF/Ssum0.ML Tue Oct 17 10:20:43 2000 +0200
@@ -11,17 +11,11 @@
(* ------------------------------------------------------------------------ *)
Goalw [Ssum_def] "Sinl_Rep(a):Ssum";
-by (rtac CollectI 1);
-by (rtac disjI1 1);
-by (rtac exI 1);
-by (rtac refl 1);
+by (Blast_tac 1);
qed "SsumIl";
Goalw [Ssum_def] "Sinr_Rep(a):Ssum";
-by (rtac CollectI 1);
-by (rtac disjI2 1);
-by (rtac exI 1);
-by (rtac refl 1);
+by (Blast_tac 1);
qed "SsumIr";
Goal "inj_on Abs_Ssum Ssum";
@@ -129,16 +123,14 @@
by (rtac SsumIr 1);
qed "inject_Isinr";
+AddSDs [inject_Isinl, inject_Isinr];
+
Goal "a1~=a2 ==> Isinl(a1) ~= Isinl(a2)";
-by (rtac contrapos 1);
-by (etac inject_Isinl 2);
-by (atac 1);
+by (Blast_tac 1);
qed "inject_Isinl_rev";
Goal "b1~=b2 ==> Isinr(b1) ~= Isinr(b2)";
-by (rtac contrapos 1);
-by (etac inject_Isinr 2);
-by (atac 1);
+by (Blast_tac 1);
qed "inject_Isinr_rev";
(* ------------------------------------------------------------------------ *)
@@ -159,9 +151,9 @@
by (rtac conjI 1);
by (rtac (Rep_Ssum_inverse RS sym RS trans) 1);
by (etac arg_cong 1);
-by (res_inst_tac [("Q","Sinl_Rep(a)=Sinl_Rep(UU)")] contrapos 1);
+by (res_inst_tac [("Q","Sinl_Rep(a)=Sinl_Rep(UU)")] contrapos_nn 1);
by (etac arg_cong 2);
-by (etac contrapos 1);
+by (etac contrapos_nn 1);
by (rtac (Rep_Ssum_inverse RS sym RS trans) 1);
by (rtac trans 1);
by (etac arg_cong 1);
@@ -175,10 +167,10 @@
by (rtac conjI 1);
by (rtac (Rep_Ssum_inverse RS sym RS trans) 1);
by (etac arg_cong 1);
-by (res_inst_tac [("Q","Sinr_Rep(b)=Sinl_Rep(UU)")] contrapos 1);
+by (res_inst_tac [("Q","Sinr_Rep(b)=Sinl_Rep(UU)")] contrapos_nn 1);
by (hyp_subst_tac 2);
by (rtac (strict_SinlSinr_Rep RS sym) 2);
-by (etac contrapos 1);
+by (etac contrapos_nn 1);
by (rtac (Rep_Ssum_inverse RS sym RS trans) 1);
by (rtac trans 1);
by (etac arg_cong 1);
@@ -262,7 +254,7 @@
by (strip_tac 1);
by (res_inst_tac [("P","Isinl(x) = Isinr(b)")] notE 1);
by (fast_tac HOL_cs 2);
-by (rtac contrapos 1);
+by (rtac contrapos_nn 1);
by (etac noteq_IsinlIsinr 2);
by (fast_tac HOL_cs 1);
qed "Iwhen2";
@@ -282,7 +274,7 @@
by (strip_tac 1);
by (res_inst_tac [("P","Isinr(y) = Isinl(a)")] notE 1);
by (fast_tac HOL_cs 2);
-by (rtac contrapos 1);
+by (rtac contrapos_nn 1);
by (etac (sym RS noteq_IsinlIsinr) 2);
by (fast_tac HOL_cs 1);
by (strip_tac 1);
--- a/src/HOLCF/Ssum3.ML Tue Oct 17 08:41:42 2000 +0200
+++ b/src/HOLCF/Ssum3.ML Tue Oct 17 10:20:43 2000 +0200
@@ -205,7 +205,7 @@
by (atac 2);
by (rtac chain_UU_I_inverse2 1);
by (stac inst_ssum_pcpo 1);
-by (etac swap 1);
+by (etac contrapos_np 1);
by (rtac inject_Isinl 1);
by (rtac trans 1);
by (etac sym 1);
@@ -253,7 +253,7 @@
by (atac 2);
by (rtac chain_UU_I_inverse2 1);
by (stac inst_ssum_pcpo 1);
-by (etac swap 1);
+by (etac contrapos_np 1);
by (rtac inject_Isinr 1);
by (rtac trans 1);
by (etac sym 1);
@@ -323,50 +323,44 @@
by (simp_tac (Ssum0_ss addsimps [cont_Isinl]) 1);
by (rtac (inst_ssum_pcpo RS sym) 1);
qed "strict_sinl";
+Addsimps [strict_sinl];
Goalw [sinr_def] "sinr`UU=UU";
by (simp_tac (Ssum0_ss addsimps [cont_Isinr]) 1);
by (rtac (inst_ssum_pcpo RS sym) 1);
qed "strict_sinr";
+Addsimps [strict_sinr];
Goalw [sinl_def,sinr_def]
"sinl`a=sinr`b ==> a=UU & b=UU";
-by (rtac noteq_IsinlIsinr 1);
-by (etac box_equals 1);
-by (asm_simp_tac (Ssum0_ss addsimps [cont_Isinr,cont_Isinl]) 1);
-by (asm_simp_tac (Ssum0_ss addsimps [cont_Isinr,cont_Isinl]) 1);
+by (auto_tac (claset() addSDs [noteq_IsinlIsinr], simpset()));
qed "noteq_sinlsinr";
Goalw [sinl_def,sinr_def]
"sinl`a1=sinl`a2==> a1=a2";
-by (rtac inject_Isinl 1);
-by (etac box_equals 1);
-by (asm_simp_tac (Ssum0_ss addsimps [cont_Isinr,cont_Isinl]) 1);
-by (asm_simp_tac (Ssum0_ss addsimps [cont_Isinr,cont_Isinl]) 1);
+by Auto_tac;
qed "inject_sinl";
Goalw [sinl_def,sinr_def]
"sinr`a1=sinr`a2==> a1=a2";
-by (rtac inject_Isinr 1);
-by (etac box_equals 1);
-by (asm_simp_tac (Ssum0_ss addsimps [cont_Isinr,cont_Isinl]) 1);
-by (asm_simp_tac (Ssum0_ss addsimps [cont_Isinr,cont_Isinl]) 1);
+by Auto_tac;
qed "inject_sinr";
+AddSDs [inject_sinl, inject_sinr];
Goal "x~=UU ==> sinl`x ~= UU";
-by (etac swap 1);
+by (etac contrapos_nn 1);
by (rtac inject_sinl 1);
-by (stac strict_sinl 1);
-by (etac notnotD 1);
+by Auto_tac;
qed "defined_sinl";
+Addsimps [defined_sinl];
Goal "x~=UU ==> sinr`x ~= UU";
-by (etac swap 1);
+by (etac contrapos_nn 1);
by (rtac inject_sinr 1);
-by (stac strict_sinr 1);
-by (etac notnotD 1);
+by Auto_tac;
qed "defined_sinr";
+Addsimps [defined_sinr];
Goalw [sinl_def,sinr_def]
"z=UU | (? a. z=sinl`a & a~=UU) | (? b. z=sinr`b & b~=UU)";
@@ -415,6 +409,7 @@
by tac;
by (simp_tac Ssum0_ss 1);
qed "sscase1";
+Addsimps [sscase1];
val tac = (REPEAT (resolve_tac (cont_lemmas1 @ [cont_Iwhen1,cont_Iwhen2,
@@ -432,6 +427,7 @@
by tac;
by (asm_simp_tac Ssum0_ss 1);
qed "sscase2";
+Addsimps [sscase2];
Goalw [sscase_def,sinl_def,sinr_def]
"x~=UU==> sscase`f`g`(sinr`x) = g`x";
@@ -445,6 +441,7 @@
by tac;
by (asm_simp_tac Ssum0_ss 1);
qed "sscase3";
+Addsimps [sscase3];
Goalw [sinl_def,sinr_def]
@@ -561,12 +558,9 @@
by (atac 1);
qed "thelub_ssum3";
-
Goal "sscase`sinl`sinr`z=z";
by (res_inst_tac [("p","z")] ssumE 1);
-by (asm_simp_tac ((simpset_of Cfun3.thy) addsimps [sscase1,sscase2,sscase3]) 1);
-by (asm_simp_tac ((simpset_of Cfun3.thy) addsimps [sscase1,sscase2,sscase3]) 1);
-by (asm_simp_tac ((simpset_of Cfun3.thy) addsimps [sscase1,sscase2,sscase3]) 1);
+by Auto_tac;
qed "sscase4";
@@ -576,6 +570,3 @@
val Ssum_rews = [strict_sinl,strict_sinr,defined_sinl,defined_sinr,
sscase1,sscase2,sscase3];
-
-Addsimps [strict_sinl,strict_sinr,defined_sinl,defined_sinr,
- sscase1,sscase2,sscase3];
--- a/src/HOLCF/Up3.ML Tue Oct 17 08:41:42 2000 +0200
+++ b/src/HOLCF/Up3.ML Tue Oct 17 10:20:43 2000 +0200
@@ -24,6 +24,7 @@
by (stac inst_up_pcpo 1);
by (rtac defined_Iup 1);
qed "defined_Iup2";
+AddIffs [defined_Iup2];
(* ------------------------------------------------------------------------ *)
(* continuity for Iup *)
@@ -49,7 +50,7 @@
by (rtac monofun_Iup 1);
by (rtac contlub_Iup 1);
qed "cont_Iup";
-
+AddIffs [cont_Iup];
(* ------------------------------------------------------------------------ *)
(* continuity for Ifup *)
@@ -132,7 +133,7 @@
(* continuous versions of lemmas for ('a)u *)
(* ------------------------------------------------------------------------ *)
-Goalw [up_def] "z = UU | (? x. z = up`x)";
+Goalw [up_def] "z = UU | (EX x. z = up`x)";
by (simp_tac (Up0_ss addsimps [cont_Iup]) 1);
by (stac inst_up_pcpo 1);
by (rtac Exh_Up 1);
@@ -140,14 +141,11 @@
Goalw [up_def] "up`x=up`y ==> x=y";
by (rtac inject_Iup 1);
-by (etac box_equals 1);
-by (simp_tac (Up0_ss addsimps [cont_Iup]) 1);
-by (simp_tac (Up0_ss addsimps [cont_Iup]) 1);
+by Auto_tac;
qed "inject_up";
Goalw [up_def] " up`x ~= UU";
-by (simp_tac (Up0_ss addsimps [cont_Iup]) 1);
-by (rtac defined_Iup2 1);
+by Auto_tac;
qed "defined_up";
val prems = Goalw [up_def]
@@ -193,7 +191,7 @@
qed "less_up4c";
Goalw [up_def,fup_def]
-"[| chain(Y); ? i x. Y(i) = up`x |] ==>\
+"[| chain(Y); EX i x. Y(i) = up`x |] ==>\
\ lub(range(Y)) = up`(lub(range(%i. fup`(LAM x. x)`(Y i))))";
by (stac beta_cfun 1);
by tac;
@@ -222,16 +220,11 @@
by (strip_tac 1);
by (dtac spec 1);
by (dtac spec 1);
-by (rtac swap 1);
-by (atac 1);
-by (dtac notnotD 1);
-by (etac box_equals 1);
-by (rtac refl 1);
-by (simp_tac (Up0_ss addsimps [cont_Iup]) 1);
+by (asm_full_simp_tac (Up0_ss addsimps [cont_Iup]) 1);
qed "thelub_up2b";
-Goal "(? x. z = up`x) = (z~=UU)";
+Goal "(EX x. z = up`x) = (z~=UU)";
by (rtac iffI 1);
by (etac exE 1);
by (hyp_subst_tac 1);
@@ -243,7 +236,7 @@
qed "up_lemma2";
-Goal "[| chain(Y); lub(range(Y)) = up`x |] ==> ? i x. Y(i) = up`x";
+Goal "[| chain(Y); lub(range(Y)) = up`x |] ==> EX i x. Y(i) = up`x";
by (rtac exE 1);
by (rtac chain_UU_I_inverse2 1);
by (rtac (up_lemma2 RS iffD1) 1);
@@ -254,11 +247,8 @@
qed "thelub_up2a_rev";
Goal "[| chain(Y); lub(range(Y)) = UU |] ==> ! i x. Y(i) ~= up`x";
-by (rtac allI 1);
-by (rtac (not_ex RS iffD1) 1);
-by (rtac contrapos 1);
-by (etac (up_lemma2 RS iffD1) 2);
-by (fast_tac (HOL_cs addSDs [chain_UU_I RS spec]) 1);
+by (blast_tac (claset() addSDs [chain_UU_I RS spec,
+ exI RS (up_lemma2 RS iffD1)]) 1);
qed "thelub_up2b_rev";
--- a/src/HOLCF/domain/theorems.ML Tue Oct 17 08:41:42 2000 +0200
+++ b/src/HOLCF/domain/theorems.ML Tue Oct 17 10:20:43 2000 +0200
@@ -43,10 +43,9 @@
cut_facts_tac prems 1,
fast_tac HOL_cs 1]);
-val dist_eqI = prove_goal Porder.thy "~(x::'a::po) << y ==> x ~= y" (fn prems => [
- rtac rev_contrapos 1,
- etac (antisym_less_inverse RS conjunct1) 1,
- resolve_tac prems 1]);
+val dist_eqI = prove_goal Porder.thy "!!x::'a::po. ~ x << y ==> x ~= y"
+ (fn prems => [
+ (blast_tac (claset() addDs [antisym_less_inverse]) 1)]);
(*
infixr 0 y;
val b = 0;
--- a/src/HOLCF/ex/Stream.ML Tue Oct 17 08:41:42 2000 +0200
+++ b/src/HOLCF/ex/Stream.ML Tue Oct 17 10:20:43 2000 +0200
@@ -24,7 +24,7 @@
Goal "a && s = UU = (a = UU)";
by Safe_tac;
-by (etac contrapos2 1);
+by (etac contrapos_pp 1);
by (safe_tac (claset() addSIs stream.con_rews));
qed "scons_eq_UU";