# HG changeset patch # User paulson # Date 878732626 -3600 # Node ID e534c4c32d54f35fbe16c086ac060555dcb8f484 # Parent 451104c223e2369855e0b46f0509451f7f32279f Ran expandshort, especially to introduce Safe_tac diff -r 451104c223e2 -r e534c4c32d54 src/HOL/Auth/Yahalom2.ML --- a/src/HOL/Auth/Yahalom2.ML Wed Nov 05 13:14:15 1997 +0100 +++ b/src/HOL/Auth/Yahalom2.ML Wed Nov 05 13:23:46 1997 +0100 @@ -400,7 +400,7 @@ \ ==> EX X. Says A B {|X, Crypt K (Nonce NB)|} : set evs"; by (etac (Says_imp_spies RS parts.Inj RS MPair_parts) 1); by (dtac B_trusts_YM4_shrK 1); -by (safe_tac (claset())); +by Safe_tac; by (rtac lemma 1); by (rtac Spy_not_see_encrypted_key 2); by (REPEAT_FIRST assume_tac); diff -r 451104c223e2 -r e534c4c32d54 src/HOL/AxClasses/Lattice/CLattice.ML --- a/src/HOL/AxClasses/Lattice/CLattice.ML Wed Nov 05 13:14:15 1997 +0100 +++ b/src/HOL/AxClasses/Lattice/CLattice.ML Wed Nov 05 13:23:46 1997 +0100 @@ -7,46 +7,46 @@ (* unique existence *) goalw thy [Inf_def] "is_Inf A (Inf A)"; - br (ex_Inf RS spec RS selectI1) 1; + by (rtac (ex_Inf RS spec RS selectI1) 1); qed "Inf_is_Inf"; goal thy "is_Inf A inf --> Inf A = inf"; - br impI 1; - br (is_Inf_uniq RS mp) 1; - br conjI 1; - br Inf_is_Inf 1; - ba 1; + by (rtac impI 1); + by (rtac (is_Inf_uniq RS mp) 1); + by (rtac conjI 1); + by (rtac Inf_is_Inf 1); + by (assume_tac 1); qed "Inf_uniq"; goalw thy [Ex1_def] "ALL A. EX! inf::'a::clattice. is_Inf A inf"; - by (safe_tac (claset())); + by Safe_tac; by (Step_tac 1); by (Step_tac 1); - br Inf_is_Inf 1; - br (Inf_uniq RS mp RS sym) 1; - ba 1; + by (rtac Inf_is_Inf 1); + by (rtac (Inf_uniq RS mp RS sym) 1); + by (assume_tac 1); qed "ex1_Inf"; goalw thy [Sup_def] "is_Sup A (Sup A)"; - br (ex_Sup RS spec RS selectI1) 1; + by (rtac (ex_Sup RS spec RS selectI1) 1); qed "Sup_is_Sup"; goal thy "is_Sup A sup --> Sup A = sup"; - br impI 1; - br (is_Sup_uniq RS mp) 1; - br conjI 1; - br Sup_is_Sup 1; - ba 1; + by (rtac impI 1); + by (rtac (is_Sup_uniq RS mp) 1); + by (rtac conjI 1); + by (rtac Sup_is_Sup 1); + by (assume_tac 1); qed "Sup_uniq"; goalw thy [Ex1_def] "ALL A. EX! sup::'a::clattice. is_Sup A sup"; - by (safe_tac (claset())); + by Safe_tac; by (Step_tac 1); by (Step_tac 1); - br Sup_is_Sup 1; - br (Sup_uniq RS mp RS sym) 1; - ba 1; + by (rtac Sup_is_Sup 1); + by (rtac (Sup_uniq RS mp RS sym) 1); + by (assume_tac 1); qed "ex1_Sup"; @@ -54,68 +54,68 @@ val prems = goalw thy [Inf_def] "x:A ==> Inf A [= x"; by (cut_facts_tac prems 1); - br selectI2 1; - br Inf_is_Inf 1; + by (rtac selectI2 1); + by (rtac Inf_is_Inf 1); by (rewtac is_Inf_def); by (Fast_tac 1); qed "Inf_lb"; val [prem] = goalw thy [Inf_def] "(!!x. x:A ==> z [= x) ==> z [= Inf A"; - br selectI2 1; - br Inf_is_Inf 1; + by (rtac selectI2 1); + by (rtac Inf_is_Inf 1); by (rewtac is_Inf_def); by (Step_tac 1); by (Step_tac 1); - be mp 1; - br ballI 1; - be prem 1; + by (etac mp 1); + by (rtac ballI 1); + by (etac prem 1); qed "Inf_ub_lbs"; val prems = goalw thy [Sup_def] "x:A ==> x [= Sup A"; by (cut_facts_tac prems 1); - br selectI2 1; - br Sup_is_Sup 1; + by (rtac selectI2 1); + by (rtac Sup_is_Sup 1); by (rewtac is_Sup_def); by (Fast_tac 1); qed "Sup_ub"; val [prem] = goalw thy [Sup_def] "(!!x. x:A ==> x [= z) ==> Sup A [= z"; - br selectI2 1; - br Sup_is_Sup 1; + by (rtac selectI2 1); + by (rtac Sup_is_Sup 1); by (rewtac is_Sup_def); by (Step_tac 1); by (Step_tac 1); - be mp 1; - br ballI 1; - be prem 1; + by (etac mp 1); + by (rtac ballI 1); + by (etac prem 1); qed "Sup_lb_ubs"; (** minorized Infs / majorized Sups **) goal thy "(x [= Inf A) = (ALL y:A. x [= y)"; - br iffI 1; + by (rtac iffI 1); (*==>*) - br ballI 1; - br (le_trans RS mp) 1; - be conjI 1; - be Inf_lb 1; + by (rtac ballI 1); + by (rtac (le_trans RS mp) 1); + by (etac conjI 1); + by (etac Inf_lb 1); (*<==*) - br Inf_ub_lbs 1; + by (rtac Inf_ub_lbs 1); by (Fast_tac 1); qed "le_Inf_eq"; goal thy "(Sup A [= x) = (ALL y:A. y [= x)"; - br iffI 1; + by (rtac iffI 1); (*==>*) - br ballI 1; - br (le_trans RS mp) 1; - br conjI 1; - be Sup_ub 1; - ba 1; + by (rtac ballI 1); + by (rtac (le_trans RS mp) 1); + by (rtac conjI 1); + by (etac Sup_ub 1); + by (assume_tac 1); (*<==*) - br Sup_lb_ubs 1; + by (rtac Sup_lb_ubs 1); by (Fast_tac 1); qed "ge_Sup_eq"; @@ -124,60 +124,60 @@ (** Subsets and limits **) goal thy "A <= B --> Inf B [= Inf A"; - br impI 1; + by (rtac impI 1); by (stac le_Inf_eq 1); by (rewtac Ball_def); - by (safe_tac (claset())); - bd subsetD 1; - ba 1; - be Inf_lb 1; + by Safe_tac; + by (dtac subsetD 1); + by (assume_tac 1); + by (etac Inf_lb 1); qed "Inf_subset_antimon"; goal thy "A <= B --> Sup A [= Sup B"; - br impI 1; + by (rtac impI 1); by (stac ge_Sup_eq 1); by (rewtac Ball_def); - by (safe_tac (claset())); - bd subsetD 1; - ba 1; - be Sup_ub 1; + by Safe_tac; + by (dtac subsetD 1); + by (assume_tac 1); + by (etac Sup_ub 1); qed "Sup_subset_mon"; (** singleton / empty limits **) goal thy "Inf {x} = x"; - br (Inf_uniq RS mp) 1; + by (rtac (Inf_uniq RS mp) 1); by (rewtac is_Inf_def); - by (safe_tac (claset())); - br le_refl 1; + by Safe_tac; + by (rtac le_refl 1); by (Fast_tac 1); qed "sing_Inf_eq"; goal thy "Sup {x} = x"; - br (Sup_uniq RS mp) 1; + by (rtac (Sup_uniq RS mp) 1); by (rewtac is_Sup_def); - by (safe_tac (claset())); - br le_refl 1; + by Safe_tac; + by (rtac le_refl 1); by (Fast_tac 1); qed "sing_Sup_eq"; goal thy "Inf {} = Sup {x. True}"; - br (Inf_uniq RS mp) 1; + by (rtac (Inf_uniq RS mp) 1); by (rewtac is_Inf_def); - by (safe_tac (claset())); - br (sing_Sup_eq RS subst) 1; + by Safe_tac; + by (rtac (sing_Sup_eq RS subst) 1); back(); - br (Sup_subset_mon RS mp) 1; + by (rtac (Sup_subset_mon RS mp) 1); by (Fast_tac 1); qed "empty_Inf_eq"; goal thy "Sup {} = Inf {x. True}"; - br (Sup_uniq RS mp) 1; + by (rtac (Sup_uniq RS mp) 1); by (rewtac is_Sup_def); - by (safe_tac (claset())); - br (sing_Inf_eq RS subst) 1; - br (Inf_subset_antimon RS mp) 1; + by Safe_tac; + by (rtac (sing_Inf_eq RS subst) 1); + by (rtac (Inf_subset_antimon RS mp) 1); by (Fast_tac 1); qed "empty_Sup_eq"; diff -r 451104c223e2 -r e534c4c32d54 src/HOL/AxClasses/Lattice/LatInsts.ML --- a/src/HOL/AxClasses/Lattice/LatInsts.ML Wed Nov 05 13:14:15 1997 +0100 +++ b/src/HOL/AxClasses/Lattice/LatInsts.ML Wed Nov 05 13:23:46 1997 +0100 @@ -3,15 +3,15 @@ goal thy "Inf {x, y} = x && y"; - br (Inf_uniq RS mp) 1; + by (rtac (Inf_uniq RS mp) 1); by (stac bin_is_Inf_eq 1); - br inf_is_inf 1; + by (rtac inf_is_inf 1); qed "bin_Inf_eq"; goal thy "Sup {x, y} = x || y"; - br (Sup_uniq RS mp) 1; + by (rtac (Sup_uniq RS mp) 1); by (stac bin_is_Sup_eq 1); - br sup_is_sup 1; + by (rtac sup_is_sup 1); qed "bin_Sup_eq"; @@ -19,39 +19,39 @@ (* Unions and limits *) goal thy "Inf (A Un B) = Inf A && Inf B"; - br (Inf_uniq RS mp) 1; + by (rtac (Inf_uniq RS mp) 1); by (rewtac is_Inf_def); - by (safe_tac (claset())); + by Safe_tac; - br (conjI RS (le_trans RS mp)) 1; - br inf_lb1 1; - be Inf_lb 1; + by (rtac (conjI RS (le_trans RS mp)) 1); + by (rtac inf_lb1 1); + by (etac Inf_lb 1); - br (conjI RS (le_trans RS mp)) 1; - br inf_lb2 1; - be Inf_lb 1; + by (rtac (conjI RS (le_trans RS mp)) 1); + by (rtac inf_lb2 1); + by (etac Inf_lb 1); by (stac le_inf_eq 1); - br conjI 1; - br Inf_ub_lbs 1; + by (rtac conjI 1); + by (rtac Inf_ub_lbs 1); by (Fast_tac 1); - br Inf_ub_lbs 1; + by (rtac Inf_ub_lbs 1); by (Fast_tac 1); qed "Inf_Un_eq"; goal thy "Inf (UN i:A. B i) = Inf {Inf (B i) |i. i:A}"; - br (Inf_uniq RS mp) 1; + by (rtac (Inf_uniq RS mp) 1); by (rewtac is_Inf_def); - by (safe_tac (claset())); + by Safe_tac; (*level 3*) - br (conjI RS (le_trans RS mp)) 1; - be Inf_lb 2; - br (sing_Inf_eq RS subst) 1; - br (Inf_subset_antimon RS mp) 1; + by (rtac (conjI RS (le_trans RS mp)) 1); + by (etac Inf_lb 2); + by (rtac (sing_Inf_eq RS subst) 1); + by (rtac (Inf_subset_antimon RS mp) 1); by (Fast_tac 1); (*level 8*) by (stac le_Inf_eq 1); - by (safe_tac (claset())); + by Safe_tac; by (stac le_Inf_eq 1); by (Fast_tac 1); qed "Inf_UN_eq"; @@ -59,40 +59,40 @@ goal thy "Sup (A Un B) = Sup A || Sup B"; - br (Sup_uniq RS mp) 1; + by (rtac (Sup_uniq RS mp) 1); by (rewtac is_Sup_def); - by (safe_tac (claset())); + by Safe_tac; - br (conjI RS (le_trans RS mp)) 1; - be Sup_ub 1; - br sup_ub1 1; + by (rtac (conjI RS (le_trans RS mp)) 1); + by (etac Sup_ub 1); + by (rtac sup_ub1 1); - br (conjI RS (le_trans RS mp)) 1; - be Sup_ub 1; - br sup_ub2 1; + by (rtac (conjI RS (le_trans RS mp)) 1); + by (etac Sup_ub 1); + by (rtac sup_ub2 1); by (stac ge_sup_eq 1); - br conjI 1; - br Sup_lb_ubs 1; + by (rtac conjI 1); + by (rtac Sup_lb_ubs 1); by (Fast_tac 1); - br Sup_lb_ubs 1; + by (rtac Sup_lb_ubs 1); by (Fast_tac 1); qed "Sup_Un_eq"; goal thy "Sup (UN i:A. B i) = Sup {Sup (B i) |i. i:A}"; - br (Sup_uniq RS mp) 1; + by (rtac (Sup_uniq RS mp) 1); by (rewtac is_Sup_def); - by (safe_tac (claset())); + by Safe_tac; (*level 3*) - br (conjI RS (le_trans RS mp)) 1; - be Sup_ub 1; - br (sing_Sup_eq RS subst) 1; + by (rtac (conjI RS (le_trans RS mp)) 1); + by (etac Sup_ub 1); + by (rtac (sing_Sup_eq RS subst) 1); back(); - br (Sup_subset_mon RS mp) 1; + by (rtac (Sup_subset_mon RS mp) 1); by (Fast_tac 1); (*level 8*) by (stac ge_Sup_eq 1); - by (safe_tac (claset())); + by Safe_tac; by (stac ge_Sup_eq 1); by (Fast_tac 1); qed "Sup_UN_eq"; diff -r 451104c223e2 -r e534c4c32d54 src/HOL/AxClasses/Lattice/LatMorph.ML --- a/src/HOL/AxClasses/Lattice/LatMorph.ML Wed Nov 05 13:14:15 1997 +0100 +++ b/src/HOL/AxClasses/Lattice/LatMorph.ML Wed Nov 05 13:23:46 1997 +0100 @@ -5,49 +5,49 @@ (** monotone functions vs. "&&"- / "||"-semi-morphisms **) goalw thy [is_mono_def] "is_mono f = (ALL x y. f (x && y) [= f x && f y)"; - by (safe_tac (claset())); + by Safe_tac; (*==> (level 1)*) by (stac le_inf_eq 1); - br conjI 1; + by (rtac conjI 1); by (Step_tac 1); by (Step_tac 1); - be mp 1; - br inf_lb1 1; + by (etac mp 1); + by (rtac inf_lb1 1); by (Step_tac 1); by (Step_tac 1); - be mp 1; - br inf_lb2 1; + by (etac mp 1); + by (rtac inf_lb2 1); (*==> (level 11)*) - br (conjI RS (le_trans RS mp)) 1; - br inf_lb2 2; + by (rtac (conjI RS (le_trans RS mp)) 1); + by (rtac inf_lb2 2); by (subgoal_tac "x && y = x" 1); - be subst 1; + by (etac subst 1); by (Fast_tac 1); by (stac inf_connect 1); - ba 1; + by (assume_tac 1); qed "mono_inf_eq"; goalw thy [is_mono_def] "is_mono f = (ALL x y. f x || f y [= f (x || y))"; - by (safe_tac (claset())); + by Safe_tac; (*==> (level 1)*) by (stac ge_sup_eq 1); - br conjI 1; + by (rtac conjI 1); by (Step_tac 1); by (Step_tac 1); - be mp 1; - br sup_ub1 1; + by (etac mp 1); + by (rtac sup_ub1 1); by (Step_tac 1); by (Step_tac 1); - be mp 1; - br sup_ub2 1; + by (etac mp 1); + by (rtac sup_ub2 1); (*==> (level 11)*) - br (conjI RS (le_trans RS mp)) 1; - br sup_ub1 1; + by (rtac (conjI RS (le_trans RS mp)) 1); + by (rtac sup_ub1 1); by (subgoal_tac "x || y = y" 1); - be subst 1; + by (etac subst 1); by (Fast_tac 1); by (stac sup_connect 1); - ba 1; + by (assume_tac 1); qed "mono_sup_eq"; diff -r 451104c223e2 -r e534c4c32d54 src/HOL/AxClasses/Lattice/LatPreInsts.ML --- a/src/HOL/AxClasses/Lattice/LatPreInsts.ML Wed Nov 05 13:14:15 1997 +0100 +++ b/src/HOL/AxClasses/Lattice/LatPreInsts.ML Wed Nov 05 13:23:46 1997 +0100 @@ -5,13 +5,13 @@ (** complete lattices **) goal thy "is_inf x y (Inf {x, y})"; - br (bin_is_Inf_eq RS subst) 1; - br Inf_is_Inf 1; + by (rtac (bin_is_Inf_eq RS subst) 1); + by (rtac Inf_is_Inf 1); qed "Inf_is_inf"; goal thy "is_sup x y (Sup {x, y})"; - br (bin_is_Sup_eq RS subst) 1; - br Sup_is_Sup 1; + by (rtac (bin_is_Sup_eq RS subst) 1); + by (rtac Sup_is_Sup 1); qed "Sup_is_sup"; @@ -22,13 +22,13 @@ goalw thy [is_inf_def, le_prod_def] "is_inf p q (fst p && fst q, snd p && snd q)"; by (Simp_tac 1); - by (safe_tac (claset())); + by Safe_tac; by (REPEAT_FIRST (fn i => resolve_tac [inf_lb1, inf_lb2, inf_ub_lbs] i ORELSE atac i)); qed "prod_is_inf"; goalw thy [is_sup_def, le_prod_def] "is_sup p q (fst p || fst q, snd p || snd q)"; by (Simp_tac 1); - by (safe_tac (claset())); + by Safe_tac; by (REPEAT_FIRST (fn i => resolve_tac [sup_ub1, sup_ub2, sup_lb_ubs] i ORELSE atac i)); qed "prod_is_sup"; @@ -36,18 +36,18 @@ (* functions *) goalw thy [is_inf_def, le_fun_def] "is_inf f g (%x. f x && g x)"; - by (safe_tac (claset())); - br inf_lb1 1; - br inf_lb2 1; - br inf_ub_lbs 1; + by Safe_tac; + by (rtac inf_lb1 1); + by (rtac inf_lb2 1); + by (rtac inf_ub_lbs 1); by (REPEAT_FIRST (Fast_tac)); qed "fun_is_inf"; goalw thy [is_sup_def, le_fun_def] "is_sup f g (%x. f x || g x)"; - by (safe_tac (claset())); - br sup_ub1 1; - br sup_ub2 1; - br sup_lb_ubs 1; + by Safe_tac; + by (rtac sup_ub1 1); + by (rtac sup_ub2 1); + by (rtac sup_lb_ubs 1); by (REPEAT_FIRST (Fast_tac)); qed "fun_is_sup"; @@ -57,20 +57,20 @@ goalw thy [is_inf_def, le_dual_def] "is_inf x y (Abs_dual (Rep_dual x || Rep_dual y))"; by (stac Abs_dual_inverse' 1); - by (safe_tac (claset())); - br sup_ub1 1; - br sup_ub2 1; - br sup_lb_ubs 1; - ba 1; - ba 1; + by Safe_tac; + by (rtac sup_ub1 1); + by (rtac sup_ub2 1); + by (rtac sup_lb_ubs 1); + by (assume_tac 1); + by (assume_tac 1); qed "dual_is_inf"; goalw thy [is_sup_def, le_dual_def] "is_sup x y (Abs_dual (Rep_dual x && Rep_dual y))"; by (stac Abs_dual_inverse' 1); - by (safe_tac (claset())); - br inf_lb1 1; - br inf_lb2 1; - br inf_ub_lbs 1; - ba 1; - ba 1; + by Safe_tac; + by (rtac inf_lb1 1); + by (rtac inf_lb2 1); + by (rtac inf_ub_lbs 1); + by (assume_tac 1); + by (assume_tac 1); qed "dual_is_sup"; diff -r 451104c223e2 -r e534c4c32d54 src/HOL/AxClasses/Lattice/Lattice.ML --- a/src/HOL/AxClasses/Lattice/Lattice.ML Wed Nov 05 13:14:15 1997 +0100 +++ b/src/HOL/AxClasses/Lattice/Lattice.ML Wed Nov 05 13:23:46 1997 +0100 @@ -7,46 +7,46 @@ (* unique existence *) goalw thy [inf_def] "is_inf x y (x && y)"; - br (ex_inf RS spec RS spec RS selectI1) 1; + by (rtac (ex_inf RS spec RS spec RS selectI1) 1); qed "inf_is_inf"; goal thy "is_inf x y inf --> x && y = inf"; - br impI 1; - br (is_inf_uniq RS mp) 1; - br conjI 1; - br inf_is_inf 1; - ba 1; + by (rtac impI 1); + by (rtac (is_inf_uniq RS mp) 1); + by (rtac conjI 1); + by (rtac inf_is_inf 1); + by (assume_tac 1); qed "inf_uniq"; goalw thy [Ex1_def] "ALL x y. EX! inf::'a::lattice. is_inf x y inf"; - by (safe_tac (claset())); + by Safe_tac; by (Step_tac 1); by (Step_tac 1); - br inf_is_inf 1; - br (inf_uniq RS mp RS sym) 1; - ba 1; + by (rtac inf_is_inf 1); + by (rtac (inf_uniq RS mp RS sym) 1); + by (assume_tac 1); qed "ex1_inf"; goalw thy [sup_def] "is_sup x y (x || y)"; - br (ex_sup RS spec RS spec RS selectI1) 1; + by (rtac (ex_sup RS spec RS spec RS selectI1) 1); qed "sup_is_sup"; goal thy "is_sup x y sup --> x || y = sup"; - br impI 1; - br (is_sup_uniq RS mp) 1; - br conjI 1; - br sup_is_sup 1; - ba 1; + by (rtac impI 1); + by (rtac (is_sup_uniq RS mp) 1); + by (rtac conjI 1); + by (rtac sup_is_sup 1); + by (assume_tac 1); qed "sup_uniq"; goalw thy [Ex1_def] "ALL x y. EX! sup::'a::lattice. is_sup x y sup"; - by (safe_tac (claset())); + by Safe_tac; by (Step_tac 1); by (Step_tac 1); - br sup_is_sup 1; - br (sup_uniq RS mp RS sym) 1; - ba 1; + by (rtac sup_is_sup 1); + by (rtac (sup_uniq RS mp RS sym) 1); + by (assume_tac 1); qed "ex1_sup"; @@ -96,30 +96,30 @@ (* the Connection Theorems: "[=" expressed via "&&" or "||" *) goal thy "(x && y = x) = (x [= y)"; - br iffI 1; + by (rtac iffI 1); (*==>*) - be subst 1; - br inf_lb2 1; + by (etac subst 1); + by (rtac inf_lb2 1); (*<==*) - br (inf_uniq RS mp) 1; + by (rtac (inf_uniq RS mp) 1); by (rewtac is_inf_def); by (REPEAT_FIRST (rtac conjI)); - br le_refl 1; - ba 1; + by (rtac le_refl 1); + by (assume_tac 1); by (Fast_tac 1); qed "inf_connect"; goal thy "(x || y = y) = (x [= y)"; - br iffI 1; + by (rtac iffI 1); (*==>*) - be subst 1; - br sup_ub1 1; + by (etac subst 1); + by (rtac sup_ub1 1); (*<==*) - br (sup_uniq RS mp) 1; + by (rtac (sup_uniq RS mp) 1); by (rewtac is_sup_def); by (REPEAT_FIRST (rtac conjI)); - ba 1; - br le_refl 1; + by (assume_tac 1); + by (rtac le_refl 1); by (Fast_tac 1); qed "sup_connect"; @@ -127,37 +127,37 @@ (* minorized infs / majorized sups *) goal thy "(x [= y && z) = (x [= y & x [= z)"; - br iffI 1; + by (rtac iffI 1); (*==> (level 1)*) by (cut_facts_tac [inf_lb1, inf_lb2] 1); - br conjI 1; - br (le_trans RS mp) 1; - be conjI 1; - ba 1; - br (le_trans RS mp) 1; - be conjI 1; - ba 1; + by (rtac conjI 1); + by (rtac (le_trans RS mp) 1); + by (etac conjI 1); + by (assume_tac 1); + by (rtac (le_trans RS mp) 1); + by (etac conjI 1); + by (assume_tac 1); (*<== (level 9)*) - be conjE 1; - be inf_ub_lbs 1; - ba 1; + by (etac conjE 1); + by (etac inf_ub_lbs 1); + by (assume_tac 1); qed "le_inf_eq"; goal thy "(x || y [= z) = (x [= z & y [= z)"; - br iffI 1; + by (rtac iffI 1); (*==> (level 1)*) by (cut_facts_tac [sup_ub1, sup_ub2] 1); - br conjI 1; - br (le_trans RS mp) 1; - be conjI 1; - ba 1; - br (le_trans RS mp) 1; - be conjI 1; - ba 1; + by (rtac conjI 1); + by (rtac (le_trans RS mp) 1); + by (etac conjI 1); + by (assume_tac 1); + by (rtac (le_trans RS mp) 1); + by (etac conjI 1); + by (assume_tac 1); (*<== (level 9)*) - be conjE 1; - be sup_lb_ubs 1; - ba 1; + by (etac conjE 1); + by (etac sup_lb_ubs 1); + by (assume_tac 1); qed "ge_sup_eq"; @@ -175,8 +175,8 @@ back(); back(); back(); - br refl 2; - br (is_inf_assoc RS mp) 1; + by (rtac refl 2); + by (rtac (is_inf_assoc RS mp) 1); by (REPEAT_FIRST (rtac conjI)); by (REPEAT_FIRST (rtac inf_is_inf)); qed "inf_assoc"; @@ -191,8 +191,8 @@ back(); back(); back(); - br refl 2; - br (is_sup_assoc RS mp) 1; + by (rtac refl 2); + by (rtac (is_sup_assoc RS mp) 1); by (REPEAT_FIRST (rtac conjI)); by (REPEAT_FIRST (rtac sup_is_sup)); qed "sup_assoc"; @@ -202,12 +202,12 @@ goalw thy [inf_def] "x && y = y && x"; by (stac (is_inf_commut RS ext) 1); - br refl 1; + by (rtac refl 1); qed "inf_commut"; goalw thy [sup_def] "x || y = y || x"; by (stac (is_sup_commut RS ext) 1); - br refl 1; + by (rtac refl 1); qed "sup_commut"; @@ -215,12 +215,12 @@ goal thy "x && x = x"; by (stac inf_connect 1); - br le_refl 1; + by (rtac le_refl 1); qed "inf_idemp"; goal thy "x || x = x"; by (stac sup_connect 1); - br le_refl 1; + by (rtac le_refl 1); qed "sup_idemp"; @@ -229,12 +229,12 @@ goal thy "x || (x && y) = x"; by (stac sup_commut 1); by (stac sup_connect 1); - br inf_lb1 1; + by (rtac inf_lb1 1); qed "sup_inf_absorb"; goal thy "x && (x || y) = x"; by (stac inf_connect 1); - br sup_ub1 1; + by (rtac sup_ub1 1); qed "inf_sup_absorb"; @@ -243,27 +243,27 @@ val prems = goal thy "[| a [= b; x [= y |] ==> a && x [= b && y"; by (cut_facts_tac prems 1); by (stac le_inf_eq 1); - br conjI 1; - br (le_trans RS mp) 1; - br conjI 1; - br inf_lb1 1; - ba 1; - br (le_trans RS mp) 1; - br conjI 1; - br inf_lb2 1; - ba 1; + by (rtac conjI 1); + by (rtac (le_trans RS mp) 1); + by (rtac conjI 1); + by (rtac inf_lb1 1); + by (assume_tac 1); + by (rtac (le_trans RS mp) 1); + by (rtac conjI 1); + by (rtac inf_lb2 1); + by (assume_tac 1); qed "inf_mon"; val prems = goal thy "[| a [= b; x [= y |] ==> a || x [= b || y"; by (cut_facts_tac prems 1); by (stac ge_sup_eq 1); - br conjI 1; - br (le_trans RS mp) 1; - br conjI 1; - ba 1; - br sup_ub1 1; - br (le_trans RS mp) 1; - br conjI 1; - ba 1; - br sup_ub2 1; + by (rtac conjI 1); + by (rtac (le_trans RS mp) 1); + by (rtac conjI 1); + by (assume_tac 1); + by (rtac sup_ub1 1); + by (rtac (le_trans RS mp) 1); + by (rtac conjI 1); + by (assume_tac 1); + by (rtac sup_ub2 1); qed "sup_mon"; diff -r 451104c223e2 -r e534c4c32d54 src/HOL/AxClasses/Lattice/OrdDefs.ML --- a/src/HOL/AxClasses/Lattice/OrdDefs.ML Wed Nov 05 13:14:15 1997 +0100 +++ b/src/HOL/AxClasses/Lattice/OrdDefs.ML Wed Nov 05 13:23:46 1997 +0100 @@ -7,47 +7,47 @@ (* pairs *) goalw thy [le_prod_def] "x [= (x::'a::quasi_order*'b::quasi_order)"; - br conjI 1; - br le_refl 1; - br le_refl 1; + by (rtac conjI 1); + by (rtac le_refl 1); + by (rtac le_refl 1); qed "le_prod_refl"; goalw thy [le_prod_def] "x [= y & y [= z --> x [= (z::'a::quasi_order*'b::quasi_order)"; - by (safe_tac (claset())); - be (conjI RS (le_trans RS mp)) 1; - ba 1; - be (conjI RS (le_trans RS mp)) 1; - ba 1; + by Safe_tac; + by (etac (conjI RS (le_trans RS mp)) 1); + by (assume_tac 1); + by (etac (conjI RS (le_trans RS mp)) 1); + by (assume_tac 1); qed "le_prod_trans"; goalw thy [le_prod_def] "x [= y & y [= x --> x = (y::'a::partial_order*'b::partial_order)"; - by (safe_tac (claset())); + by Safe_tac; by (stac Pair_fst_snd_eq 1); - br conjI 1; - be (conjI RS (le_antisym RS mp)) 1; - ba 1; - be (conjI RS (le_antisym RS mp)) 1; - ba 1; + by (rtac conjI 1); + by (etac (conjI RS (le_antisym RS mp)) 1); + by (assume_tac 1); + by (etac (conjI RS (le_antisym RS mp)) 1); + by (assume_tac 1); qed "le_prod_antisym"; (* functions *) goalw thy [le_fun_def] "f [= (f::'a=>'b::quasi_order)"; - br allI 1; - br le_refl 1; + by (rtac allI 1); + by (rtac le_refl 1); qed "le_fun_refl"; goalw thy [le_fun_def] "f [= g & g [= h --> f [= (h::'a=>'b::quasi_order)"; - by (safe_tac (claset())); - br (le_trans RS mp) 1; + by Safe_tac; + by (rtac (le_trans RS mp) 1); by (Fast_tac 1); qed "le_fun_trans"; goalw thy [le_fun_def] "f [= g & g [= f --> f = (g::'a=>'b::partial_order)"; - by (safe_tac (claset())); - br ext 1; - br (le_antisym RS mp) 1; + by Safe_tac; + by (rtac ext 1); + by (rtac (le_antisym RS mp) 1); by (Fast_tac 1); qed "le_fun_antisym"; @@ -57,32 +57,32 @@ (*"'a dual" is even an isotype*) goal thy "Rep_dual (Abs_dual y) = y"; - br Abs_dual_inverse 1; + by (rtac Abs_dual_inverse 1); by (rewtac dual_def); by (Fast_tac 1); qed "Abs_dual_inverse'"; goalw thy [le_dual_def] "x [= (x::'a::quasi_order dual)"; - br le_refl 1; + by (rtac le_refl 1); qed "le_dual_refl"; goalw thy [le_dual_def] "x [= y & y [= z --> x [= (z::'a::quasi_order dual)"; by (stac conj_commut 1); - br le_trans 1; + by (rtac le_trans 1); qed "le_dual_trans"; goalw thy [le_dual_def] "x [= y & y [= x --> x = (y::'a::partial_order dual)"; - by (safe_tac (claset())); - br (Rep_dual_inverse RS subst) 1; - br sym 1; - br (Rep_dual_inverse RS subst) 1; - br arg_cong 1; + by Safe_tac; + by (rtac (Rep_dual_inverse RS subst) 1); + by (rtac sym 1); + by (rtac (Rep_dual_inverse RS subst) 1); + by (rtac arg_cong 1); back(); - be (conjI RS (le_antisym RS mp)) 1; - ba 1; + by (etac (conjI RS (le_antisym RS mp)) 1); + by (assume_tac 1); qed "le_dual_antisym"; goalw thy [le_dual_def] "x [= y | y [= (x::'a::linear_order dual)"; - br le_linear 1; + by (rtac le_linear 1); qed "le_dual_linear"; diff -r 451104c223e2 -r e534c4c32d54 src/HOL/AxClasses/Lattice/Order.ML --- a/src/HOL/AxClasses/Lattice/Order.ML Wed Nov 05 13:14:15 1997 +0100 +++ b/src/HOL/AxClasses/Lattice/Order.ML Wed Nov 05 13:23:46 1997 +0100 @@ -45,70 +45,70 @@ (* associativity *) goalw thy [is_inf_def] "is_inf x y xy & is_inf y z yz & is_inf xy z xyz --> is_inf x yz xyz"; - by (safe_tac (claset())); + by Safe_tac; (*level 1*) - br (le_trans RS mp) 1; - be conjI 1; - ba 1; + by (rtac (le_trans RS mp) 1); + by (etac conjI 1); + by (assume_tac 1); (*level 4*) by (Step_tac 1); back(); - be mp 1; - br conjI 1; - br (le_trans RS mp) 1; - be conjI 1; - ba 1; - ba 1; + by (etac mp 1); + by (rtac conjI 1); + by (rtac (le_trans RS mp) 1); + by (etac conjI 1); + by (assume_tac 1); + by (assume_tac 1); (*level 11*) by (Step_tac 1); back(); back(); - be mp 1; - br conjI 1; + by (etac mp 1); + by (rtac conjI 1); by (Step_tac 1); - be mp 1; - be conjI 1; - br (le_trans RS mp) 1; - be conjI 1; - ba 1; - br (le_trans RS mp) 1; - be conjI 1; + by (etac mp 1); + by (etac conjI 1); + by (rtac (le_trans RS mp) 1); + by (etac conjI 1); + by (assume_tac 1); + by (rtac (le_trans RS mp) 1); + by (etac conjI 1); back(); (* !! *) - ba 1; + by (assume_tac 1); qed "is_inf_assoc"; goalw thy [is_sup_def] "is_sup x y xy & is_sup y z yz & is_sup xy z xyz --> is_sup x yz xyz"; - by (safe_tac (claset())); + by Safe_tac; (*level 1*) - br (le_trans RS mp) 1; - be conjI 1; - ba 1; + by (rtac (le_trans RS mp) 1); + by (etac conjI 1); + by (assume_tac 1); (*level 4*) by (Step_tac 1); back(); - be mp 1; - br conjI 1; - br (le_trans RS mp) 1; - be conjI 1; - ba 1; - ba 1; + by (etac mp 1); + by (rtac conjI 1); + by (rtac (le_trans RS mp) 1); + by (etac conjI 1); + by (assume_tac 1); + by (assume_tac 1); (*level 11*) by (Step_tac 1); back(); back(); - be mp 1; - br conjI 1; + by (etac mp 1); + by (rtac conjI 1); by (Step_tac 1); - be mp 1; - be conjI 1; - br (le_trans RS mp) 1; - be conjI 1; + by (etac mp 1); + by (etac conjI 1); + by (rtac (le_trans RS mp) 1); + by (etac conjI 1); back(); (* !! *) - ba 1; - br (le_trans RS mp) 1; - be conjI 1; - ba 1; + by (assume_tac 1); + by (rtac (le_trans RS mp) 1); + by (etac conjI 1); + by (assume_tac 1); qed "is_sup_assoc"; @@ -118,15 +118,15 @@ by (stac expand_if 1); by (REPEAT_FIRST (resolve_tac [conjI, impI])); (*case "x [= y"*) - br le_refl 1; - ba 1; + by (rtac le_refl 1); + by (assume_tac 1); by (Fast_tac 1); (*case "~ x [= y"*) - br (le_linear RS disjE) 1; - ba 1; - be notE 1; - ba 1; - br le_refl 1; + by (rtac (le_linear RS disjE) 1); + by (assume_tac 1); + by (etac notE 1); + by (assume_tac 1); + by (rtac le_refl 1); by (Fast_tac 1); qed "min_is_inf"; @@ -134,15 +134,15 @@ by (stac expand_if 1); by (REPEAT_FIRST (resolve_tac [conjI, impI])); (*case "x [= y"*) - ba 1; - br le_refl 1; + by (assume_tac 1); + by (rtac le_refl 1); by (Fast_tac 1); (*case "~ x [= y"*) - br le_refl 1; - br (le_linear RS disjE) 1; - ba 1; - be notE 1; - ba 1; + by (rtac le_refl 1); + by (rtac (le_linear RS disjE) 1); + by (assume_tac 1); + by (etac notE 1); + by (assume_tac 1); by (Fast_tac 1); qed "max_is_sup"; @@ -151,23 +151,23 @@ (** general vs. binary limits **) goalw thy [is_inf_def, is_Inf_def] "is_Inf {x, y} inf = is_inf x y inf"; - br iffI 1; + by (rtac iffI 1); (*==>*) by (Fast_tac 1); (*<==*) - by (safe_tac (claset())); + by Safe_tac; by (Step_tac 1); - be mp 1; + by (etac mp 1); by (Fast_tac 1); qed "bin_is_Inf_eq"; goalw thy [is_sup_def, is_Sup_def] "is_Sup {x, y} sup = is_sup x y sup"; - br iffI 1; + by (rtac iffI 1); (*==>*) by (Fast_tac 1); (*<==*) - by (safe_tac (claset())); + by Safe_tac; by (Step_tac 1); - be mp 1; + by (etac mp 1); by (Fast_tac 1); qed "bin_is_Sup_eq"; diff -r 451104c223e2 -r e534c4c32d54 src/HOL/Finite.ML --- a/src/HOL/Finite.ML Wed Nov 05 13:14:15 1997 +0100 +++ b/src/HOL/Finite.ML Wed Nov 05 13:23:46 1997 +0100 @@ -154,8 +154,8 @@ val [prem] = goal Finite.thy "finite A ==> (!a:A. finite(B a)) --> finite(UN a:A. B a)"; -br (prem RS finite_induct) 1; -by(ALLGOALS Asm_simp_tac); +by (rtac (prem RS finite_induct) 1); +by (ALLGOALS Asm_simp_tac); bind_thm("finite_UnionI", ballI RSN (2, result() RS mp)); Addsimps [finite_UnionI]; @@ -163,7 +163,7 @@ goalw Finite.thy [Sigma_def] "!!A. [| finite A; !a:A. finite(B a) |] ==> finite(SIGMA a:A. B a)"; -by(blast_tac (claset() addSIs [finite_UnionI]) 1); +by (blast_tac (claset() addSIs [finite_UnionI]) 1); bind_thm("finite_SigmaI", ballI RSN (2,result())); Addsimps [finite_SigmaI]; @@ -250,15 +250,15 @@ by (etac equalityE 1); by (asm_full_simp_tac (simpset() addsimps [subset_insert,Collect_conv_insert, less_Suc_eq]) 1); -by (safe_tac (claset())); +by Safe_tac; by (Asm_full_simp_tac 1); by (res_inst_tac [("x","%i. if f i = f m then a else f i")] exI 1); - by (SELECT_GOAL(safe_tac (claset()))1); + by (SELECT_GOAL Safe_tac 1); by (subgoal_tac "x ~= f m" 1); by (Blast_tac 2); by (subgoal_tac "? k. f k = x & k ?Y")] rev_mp 1); by (res_inst_tac [("x","s")] spec 1); by (res_inst_tac [("n","n")] less_induct 1); by (strip_tac 1); diff -r 451104c223e2 -r e534c4c32d54 src/HOL/IOA/IOA.ML --- a/src/HOL/IOA/IOA.ML Wed Nov 05 13:14:15 1997 +0100 +++ b/src/HOL/IOA/IOA.ML Wed Nov 05 13:23:46 1997 +0100 @@ -55,7 +55,7 @@ goalw IOA.thy (reachable_def::exec_rws) "!!A. [| reachable A s; (s,a,t) : trans_of(A) |] ==> reachable A t"; by (asm_full_simp_tac (simpset() delsimps bex_simps) 1); - by (safe_tac (claset())); + by Safe_tac; by (res_inst_tac [("x","(%i. if i (s,a,t): trans_of(A) --> P(t) |] \ \ ==> invariant A P"; by (rewrite_goals_tac(reachable_def::Let_def::exec_rws)); - by (safe_tac (claset())); + by Safe_tac; by (res_inst_tac [("Q","reachable A (snd ex n)")] conjunct1 1); by (nat_ind_tac "n" 1); by (fast_tac (claset() addIs [p1,reachable_0]) 1); by (eres_inst_tac[("x","n")]allE 1); by (exhaust_tac "fst ex n" 1 THEN ALLGOALS Asm_full_simp_tac); - by (safe_tac (claset())); + by Safe_tac; by (etac (p2 RS mp) 1); by (ALLGOALS(fast_tac(claset() addDs [reachable_n]))); qed "invariantI"; diff -r 451104c223e2 -r e534c4c32d54 src/HOL/IOA/Solve.ML --- a/src/HOL/IOA/Solve.ML Wed Nov 05 13:14:15 1997 +0100 +++ b/src/HOL/IOA/Solve.ML Wed Nov 05 13:23:46 1997 +0100 @@ -15,7 +15,7 @@ \ is_weak_pmap f C A |] ==> traces(C) <= traces(A)"; by (simp_tac(simpset() addsimps [has_trace_def])1); - by (safe_tac (claset())); + by Safe_tac; (* choose same trace, therefore same NF *) by (res_inst_tac[("x","mk_trace C (fst ex)")] exI 1); @@ -32,7 +32,7 @@ (* Now show that it's an execution *) by (asm_full_simp_tac(simpset() addsimps [executions_def]) 1); - by (safe_tac (claset())); + by Safe_tac; (* Start states map to start states *) by (dtac bspec 1); @@ -40,7 +40,7 @@ (* Show that it's an execution fragment *) by (asm_full_simp_tac (simpset() addsimps [is_execution_fragment_def])1); - by (safe_tac (claset())); + by Safe_tac; by (eres_inst_tac [("x","snd ex n")] allE 1); by (eres_inst_tac [("x","snd ex (Suc n)")] allE 1); @@ -51,7 +51,7 @@ (* Lemmata *) val prems = goal HOL.thy "(P ==> Q-->R) ==> P&Q --> R"; - by(fast_tac (claset() addDs prems) 1); + by (fast_tac (claset() addDs prems) 1); val imp_conj_lemma = result(); @@ -120,7 +120,7 @@ by (simp_tac (simpset() addsimps [externals_of_par_extra]) 1); by (simp_tac (simpset() addsimps [par_def]) 1); by (asm_full_simp_tac (simpset() addsimps [trans_of_def]) 1); -by (rtac (expand_if RS ssubst) 1); +by (stac expand_if 1); by (rtac conjI 1); by (rtac impI 1); by (etac disjE 1); @@ -142,7 +142,7 @@ by (Fast_tac 2); by (simp_tac (simpset() addsimps [conj_disj_distribR] addcongs [conj_cong] addsplits [expand_if]) 1); -by(REPEAT((resolve_tac [conjI,impI] 1 ORELSE etac conjE 1) THEN +by (REPEAT((resolve_tac [conjI,impI] 1 ORELSE etac conjE 1) THEN asm_full_simp_tac(simpset() addsimps[comp1_reachable, comp2_reachable])1)); qed"fxg_is_weak_pmap_of_product_IOA"; @@ -174,8 +174,8 @@ by (rtac imp_conj_lemma 1); by (simp_tac (simpset() addsimps [rename_def]) 1); by (asm_full_simp_tac (simpset() addsimps [externals_def,asig_inputs_def,asig_outputs_def,asig_of_def,trans_of_def]) 1); -by (safe_tac (claset())); -by (rtac (expand_if RS ssubst) 1); +by Safe_tac; +by (stac expand_if 1); by (rtac conjI 1); by (rtac impI 1); by (etac disjE 1); diff -r 451104c223e2 -r e534c4c32d54 src/HOL/MiniML/Generalize.ML --- a/src/HOL/MiniML/Generalize.ML Wed Nov 05 13:14:15 1997 +0100 +++ b/src/HOL/MiniML/Generalize.ML Wed Nov 05 13:23:46 1997 +0100 @@ -95,7 +95,7 @@ goalw Generalize.thy [le_type_scheme_def,is_bound_typ_instance] "gen ($ S A) ($ S t) <= $ S (gen A t)"; -by (safe_tac (claset())); +by Safe_tac; by (rename_tac "R" 1); by (res_inst_tac [("x", "(%a. bound_typ_inst R (gen ($S A) (S a)))")] exI 1); by (typ.induct_tac "t" 1); @@ -105,7 +105,7 @@ goalw Generalize.thy [le_type_scheme_def,is_bound_typ_instance] "!!A B. free_tv B <= free_tv A ==> gen A t <= gen B t"; -by (safe_tac (claset())); +by Safe_tac; by (rename_tac "S" 1); by (res_inst_tac [("x","%b. if b:free_tv A then TVar b else S b")] exI 1); by (typ.induct_tac "t" 1); diff -r 451104c223e2 -r e534c4c32d54 src/HOL/MiniML/Instance.ML --- a/src/HOL/MiniML/Instance.ML Wed Nov 05 13:14:15 1997 +0100 +++ b/src/HOL/MiniML/Instance.ML Wed Nov 05 13:23:46 1997 +0100 @@ -50,7 +50,7 @@ \ (? S. !x:bound_tv sch. B x = mk_scheme (S x))"; by (type_scheme.induct_tac "sch" 1); by (Simp_tac 1); -by (safe_tac (claset())); +by Safe_tac; by (rtac exI 1); by (rtac ballI 1); by (rtac sym 1); @@ -62,10 +62,10 @@ by (dtac sym 1); by (dtac sym 1); by (REPEAT ((dtac mp 1) THEN (Fast_tac 1))); -by (safe_tac (claset())); +by Safe_tac; by (rename_tac "S1 S2" 1); by (res_inst_tac [("x","%x. if x:bound_tv type_scheme1 then (S1 x) else (S2 x)")] exI 1); -by (safe_tac (claset())); +by Safe_tac; by (asm_simp_tac (simpset() addsplits [expand_if]) 1); by (asm_simp_tac (simpset() addsplits [expand_if]) 1); by (strip_tac 1); @@ -123,7 +123,7 @@ by (asm_full_simp_tac (simpset() addsimps [subst_to_scheme_inverse]) 1); by (res_inst_tac [("x","(subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k)) o S")] exI 1); by (asm_simp_tac (simpset() addsimps [aux2]) 1); -by (safe_tac (claset())); +by Safe_tac; by (res_inst_tac [("x","%n. bound_typ_inst S (B n)")] exI 1); by (type_scheme.induct_tac "sch" 1); by (Simp_tac 1); @@ -162,7 +162,7 @@ "(sch # A <= sch' # B) = (sch <= (sch'::type_scheme) & A <= B)"; by (Simp_tac 1); by (rtac iffI 1); - by (SELECT_GOAL(safe_tac (claset()))1); + by (SELECT_GOAL Safe_tac 1); by (eres_inst_tac [("x","0")] allE 1); by (Asm_full_simp_tac 1); by (eres_inst_tac [("x","Suc i")] allE 1); @@ -220,7 +220,7 @@ by (type_scheme.induct_tac "sch" 1); by (Simp_tac 1); by (Simp_tac 1); - by (SELECT_GOAL(safe_tac(claset()))1); + by (SELECT_GOAL Safe_tac 1); by (eres_inst_tac [("x","TVar n -> TVar n")] allE 1); by (Asm_full_simp_tac 1); by (Fast_tac 1); diff -r 451104c223e2 -r e534c4c32d54 src/HOL/MiniML/Type.ML --- a/src/HOL/MiniML/Type.ML Wed Nov 05 13:14:15 1997 +0100 +++ b/src/HOL/MiniML/Type.ML Wed Nov 05 13:23:46 1997 +0100 @@ -444,7 +444,7 @@ (* all greater variables are also new *) goalw thy [new_tv_def] "!!n m. n<=m ==> new_tv n t ==> new_tv m t"; -by (safe_tac (claset())); +by Safe_tac; by (dtac spec 1); by (mp_tac 1); by (trans_tac 1); @@ -547,7 +547,7 @@ goalw thy [max_def] "!!n::nat. m < n ==> m < max n n'"; by (simp_tac (simpset() addsplits [expand_if]) 1); -by (safe_tac (claset())); +by Safe_tac; by (trans_tac 1); qed "less_maxL"; diff -r 451104c223e2 -r e534c4c32d54 src/HOL/NatDef.ML --- a/src/HOL/NatDef.ML Wed Nov 05 13:14:15 1997 +0100 +++ b/src/HOL/NatDef.ML Wed Nov 05 13:23:46 1997 +0100 @@ -628,11 +628,11 @@ hyp_subst_tac 1, rewtac Least_nat_def, rtac (select_equality RS arg_cong RS sym) 1, - safe_tac (claset()), + Safe_tac, dtac Suc_mono 1, Blast_tac 1, cut_facts_tac [less_linear] 1, - safe_tac (claset()), + Safe_tac, atac 2, Blast_tac 2, dtac Suc_mono 1, diff -r 451104c223e2 -r e534c4c32d54 src/HOL/Subst/Unify.ML --- a/src/HOL/Subst/Unify.ML Wed Nov 05 13:14:15 1997 +0100 +++ b/src/HOL/Subst/Unify.ML Wed Nov 05 13:23:46 1997 +0100 @@ -225,7 +225,7 @@ by (rotate_tac ~2 1); by (asm_full_simp_tac (simpset() addsimps [MGUnifier_def, Unifier_def, MoreGeneral_def]) 1); -by (safe_tac (claset()) THEN rename_tac "theta sigma gamma" 1); +by (Safe_tac THEN rename_tac "theta sigma gamma" 1); by (eres_inst_tac [("x","gamma")] allE 1 THEN mp_tac 1); by (etac exE 1 THEN rename_tac "delta" 1); by (eres_inst_tac [("x","delta")] allE 1); @@ -248,7 +248,7 @@ (simpset() addsimps [Var_Idem] addsplits [expand_if,split_option_case]))); (*Comb-Comb case*) -by (safe_tac (claset())); +by Safe_tac; by (REPEAT (dtac spec 1 THEN mp_tac 1)); by (safe_tac (claset() addSDs [rewrite_rule [MGUnifier_def] unify_gives_MGU])); by (rtac Idem_comp 1); diff -r 451104c223e2 -r e534c4c32d54 src/HOL/Trancl.ML --- a/src/HOL/Trancl.ML Wed Nov 05 13:14:15 1997 +0100 +++ b/src/HOL/Trancl.ML Wed Nov 05 13:23:46 1997 +0100 @@ -78,7 +78,7 @@ (*transitivity of transitive closure!! -- by induction.*) goalw Trancl.thy [trans_def] "trans(r^*)"; -by (safe_tac (claset())); +by Safe_tac; by (eres_inst_tac [("b","z")] rtrancl_induct 1); by (ALLGOALS(blast_tac (claset() addIs [rtrancl_into_rtrancl]))); qed "trans_rtrancl"; diff -r 451104c223e2 -r e534c4c32d54 src/HOL/Univ.ML --- a/src/HOL/Univ.ML Wed Nov 05 13:14:15 1997 +0100 +++ b/src/HOL/Univ.ML Wed Nov 05 13:23:46 1997 +0100 @@ -226,7 +226,7 @@ "ndepth (Push_Node i n) = Suc(ndepth(n))"; by (stac (Rep_Node RS Node_Push_I RS Abs_Node_inverse) 1); by (cut_facts_tac [rewrite_rule [Node_def] Rep_Node] 1); -by (safe_tac (claset())); +by Safe_tac; by (etac ssubst 1); (*instantiates type variables!*) by (Simp_tac 1); by (rtac Least_equality 1); @@ -546,7 +546,7 @@ (*Dependent version*) goal Univ.thy "(Sigma A B <**> Sigma C D) <= Sigma (A<*>C) (Split(%x y. B(x)<*>D(y)))"; -by (safe_tac (claset())); +by Safe_tac; by (stac Split 1); by (Blast_tac 1); qed "dprod_subset_Sigma2"; diff -r 451104c223e2 -r e534c4c32d54 src/HOL/WF.ML --- a/src/HOL/WF.ML Wed Nov 05 13:14:15 1997 +0100 +++ b/src/HOL/WF.ML Wed Nov 05 13:23:46 1997 +0100 @@ -111,7 +111,7 @@ by (blast_tac (claset() addEs [wf_trancl RS wf_irrefl] addIs [rtrancl_into_trancl1,wf_subset,impOfSubs rtrancl_mono]) 1); by (asm_full_simp_tac (simpset() addsimps [wf_eq_minimal]) 1); -by (safe_tac (claset())); +by Safe_tac; by (EVERY1[rtac allE, atac, etac impE, Blast_tac]); by (etac bexE 1); by (rename_tac "a" 1); @@ -327,5 +327,5 @@ goal WF.thy "!M R f. (f=wfrec R M) --> wf R --> (!x. f x = M (cut f R x) x)"; by (Clarify_tac 1); -be wfrec 1; +by (etac wfrec 1); qed "tfl_wfrec"; diff -r 451104c223e2 -r e534c4c32d54 src/HOL/ex/MT.ML --- a/src/HOL/ex/MT.ML Wed Nov 05 13:14:15 1997 +0100 +++ b/src/HOL/ex/MT.ML Wed Nov 05 13:23:46 1997 +0100 @@ -230,7 +230,7 @@ by (rtac eval_fun_mono 1); by (rewtac eval_fun_def); by (dtac CollectD 1); -by (safe_tac (claset())); +by Safe_tac; by (ALLGOALS (resolve_tac prems)); by (ALLGOALS (Blast_tac)); qed "eval_ind0"; @@ -336,7 +336,7 @@ by (rtac elab_fun_mono 1); by (rewtac elab_fun_def); by (dtac CollectD 1); -by (safe_tac (claset())); +by Safe_tac; by (ALLGOALS (resolve_tac prems)); by (ALLGOALS (Blast_tac)); qed "elab_ind0"; @@ -387,7 +387,7 @@ by (rtac elab_fun_mono 1); by (rewtac elab_fun_def); by (dtac CollectD 1); -by (safe_tac (claset())); +by Safe_tac; by (ALLGOALS (resolve_tac prems)); by (ALLGOALS (Blast_tac)); qed "elab_elim0"; @@ -552,7 +552,7 @@ by (rewtac hasty_fun_def); by (dtac CollectD 1); by (fold_goals_tac [hasty_fun_def]); -by (safe_tac (claset())); +by Safe_tac; by (REPEAT (ares_tac prems 1)); qed "hasty_rel_elim0"; @@ -690,7 +690,7 @@ \ |] ==> \ \ v_const(c_app c1 c2) hasty t"; by (dtac elab_app_elim 1); -by (safe_tac (claset())); +by Safe_tac; by (rtac hasty_const 1); by (rtac isof_app 1); by (rtac hasty_elim_const 1); @@ -711,7 +711,7 @@ \ |] ==> \ \ v hasty t"; by (dtac elab_app_elim 1); -by (safe_tac (claset())); +by Safe_tac; by ((etac allE 1) THEN (etac allE 1) THEN (etac impE 1)); by (assume_tac 1); by (etac impE 1); @@ -721,7 +721,7 @@ by (etac impE 1); by (assume_tac 1); by (dtac hasty_elim_clos 1); -by (safe_tac (claset())); +by Safe_tac; by (dtac elab_fn_elim 1); by (blast_tac (claset() addIs [hasty_env1] addSDs [t_fun_inj]) 1); qed "consistency_app2"; @@ -733,7 +733,7 @@ (* Proof by induction on the structure of evaluations *) by (rtac (major RS eval_ind) 1); -by (safe_tac (claset())); +by Safe_tac; by (DEPTH_SOLVE (ares_tac [consistency_const, consistency_var, consistency_fn, consistency_fix, consistency_app1, consistency_app2] 1)); @@ -746,7 +746,7 @@ val prems = goalw MT.thy [isof_env_def,hasty_env_def] "ve isofenv te ==> ve hastyenv te"; by (cut_facts_tac prems 1); -by (safe_tac (claset())); +by Safe_tac; by (etac allE 1); by (etac impE 1); by (assume_tac 1); diff -r 451104c223e2 -r e534c4c32d54 src/HOL/ex/Primrec.ML --- a/src/HOL/ex/Primrec.ML Wed Nov 05 13:14:15 1997 +0100 +++ b/src/HOL/ex/Primrec.ML Wed Nov 05 13:23:46 1997 +0100 @@ -200,7 +200,7 @@ \ ==> EX k. ALL l. list_add (map(%f. f l) fs) < ack(k, list_add l)"; by (etac lists.induct 1); by (res_inst_tac [("x","0")] exI 1 THEN Asm_simp_tac 1); -by (safe_tac (claset())); +by Safe_tac; by (Asm_simp_tac 1); by (blast_tac (claset() addIs [add_less_mono, ack_add_bound, less_trans]) 1); qed "COMP_map_lemma"; diff -r 451104c223e2 -r e534c4c32d54 src/HOL/ex/cla.ML --- a/src/HOL/ex/cla.ML Wed Nov 05 13:14:15 1997 +0100 +++ b/src/HOL/ex/cla.ML Wed Nov 05 13:23:46 1997 +0100 @@ -381,7 +381,7 @@ the type constraint ensures that x,y,z have the same type as a,b,u. *) goal HOL.thy "(? x y::'a. ! z. z=x | z=y) & P(a) & P(b) & (~a=b) \ \ --> (! u::'a. P(u))"; -by (Classical.safe_tac (claset())); +by (Classical.Safe_tac); by (res_inst_tac [("x","a")] allE 1); by (assume_tac 1); by (res_inst_tac [("x","b")] allE 1); diff -r 451104c223e2 -r e534c4c32d54 src/HOL/ex/meson.ML --- a/src/HOL/ex/meson.ML Wed Nov 05 13:14:15 1997 +0100 +++ b/src/HOL/ex/meson.ML Wed Nov 05 13:23:46 1997 +0100 @@ -430,7 +430,7 @@ (*First, breaks the goal into independent units*) val safe_best_meson_tac = - SELECT_GOAL (TRY (safe_tac (claset())) THEN + SELECT_GOAL (TRY Safe_tac THEN TRYALL (best_meson_tac size_of_subgoals)); (** Depth-first search version **) @@ -464,7 +464,7 @@ (prolog_step_tac' (make_horns cls)))); val safe_meson_tac = - SELECT_GOAL (TRY (safe_tac (claset())) THEN + SELECT_GOAL (TRY Safe_tac THEN TRYALL (iter_deepen_meson_tac)); diff -r 451104c223e2 -r e534c4c32d54 src/HOL/ex/set.ML --- a/src/HOL/ex/set.ML Wed Nov 05 13:14:15 1997 +0100 +++ b/src/HOL/ex/set.ML Wed Nov 05 13:23:46 1997 +0100 @@ -9,15 +9,14 @@ writeln"File HOL/ex/set."; -context Set.thy; +context Lfp.thy; -(*Nice demonstration of blast_tac--and its overloading problems*) +(*Nice demonstration of blast_tac--and its limitations*) goal Set.thy "!!S::'a set set. ALL x:S. ALL y:S. x<=y ==> EX z. S <= {z}"; -let val insertCI' = read_instantiate [("'a", "?'a set")] insertCI -in (*Type instantiation is required so that blast_tac can apply equalityI - to the subgoal arising from insertCI*) -by(blast_tac (claset() addSIs [insertCI']) 1) -end; +(*for some unfathomable reason, UNIV_I increases the search space greatly*) +by (blast_tac (claset() delrules [UNIV_I]) 1); +result(); + (*** A unique fixpoint theorem --- fast/best/meson all fail ***)