--- 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);
--- 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";
--- 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";
--- 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";
--- 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";
--- 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";
--- 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";
--- 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";
--- 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<m" 1);
by (Blast_tac 2);
- by (SELECT_GOAL(safe_tac (claset()))1);
+ by (SELECT_GOAL Safe_tac 1);
by (res_inst_tac [("x","k")] exI 1);
by (Asm_simp_tac 1);
by (simp_tac (simpset() addsplits [expand_if]) 1);
@@ -267,18 +267,18 @@
by (rotate_tac ~1 1);
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<m" 1);
by (Blast_tac 2);
- by (SELECT_GOAL(safe_tac (claset()))1);
+ by (SELECT_GOAL Safe_tac 1);
by (res_inst_tac [("x","k")] exI 1);
by (Asm_simp_tac 1);
by (simp_tac (simpset() addsplits [expand_if]) 1);
by (Blast_tac 1);
by (res_inst_tac [("x","%j. if f j = f i then f m else f j")] exI 1);
-by (SELECT_GOAL(safe_tac (claset()))1);
+by (SELECT_GOAL Safe_tac 1);
by (subgoal_tac "x ~= f i" 1);
by (Blast_tac 2);
by (case_tac "x = f m" 1);
@@ -286,7 +286,7 @@
by (Asm_simp_tac 1);
by (subgoal_tac "? k. f k = x & k<m" 1);
by (Blast_tac 2);
- by (SELECT_GOAL(safe_tac (claset()))1);
+ by (SELECT_GOAL Safe_tac 1);
by (res_inst_tac [("x","k")] exI 1);
by (Asm_simp_tac 1);
by (simp_tac (simpset() addsplits [expand_if]) 1);
@@ -335,7 +335,7 @@
by (Clarify_tac 1);
by (case_tac "x:B" 1);
by (dres_inst_tac [("A","B")] mk_disjoint_insert 1);
- by (SELECT_GOAL(safe_tac (claset()))1);
+ by (SELECT_GOAL Safe_tac 1);
by (rotate_tac ~1 1);
by (asm_full_simp_tac (simpset() addsimps [subset_insert_iff,finite_subset]) 1);
by (rotate_tac ~1 1);
--- a/src/HOL/Hoare/Examples.ML Wed Nov 05 13:14:15 1997 +0100
+++ b/src/HOL/Hoare/Examples.ML Wed Nov 05 13:23:46 1997 +0100
@@ -36,7 +36,7 @@
by (hoare_tac 1);
(*Now prove the verification conditions*)
-by (safe_tac (claset()));
+by Safe_tac;
by (etac less_imp_diff_positive 1);
by (asm_simp_tac (simpset() addsimps [less_imp_le, gcd_diff_r]) 1);
by (asm_full_simp_tac (simpset() addsimps [not_less_iff_le, gcd_diff_l]) 2);
@@ -67,7 +67,7 @@
by (simp_tac ((simpset_of Arith.thy) addsimps [pow_0]) 3);
-by (safe_tac (claset()));
+by Safe_tac;
by (subgoal_tac "a*a=a pow 2" 1);
by (Asm_simp_tac 1);
@@ -103,7 +103,7 @@
\ {b = fac A}";
by (hoare_tac 1);
-by (safe_tac (claset()));
+by Safe_tac;
by (res_inst_tac [("n","a")] natE 1);
by (ALLGOALS
(asm_simp_tac
--- a/src/HOL/Hoare/List_Examples.ML Wed Nov 05 13:14:15 1997 +0100
+++ b/src/HOL/Hoare/List_Examples.ML Wed Nov 05 13:23:46 1997 +0100
@@ -8,7 +8,7 @@
\{y=rev(X)}";
by (hoare_tac 1);
by (asm_full_simp_tac (simpset() addsimps [neq_Nil_conv]) 1);
-by (safe_tac (claset()));
+by Safe_tac;
by (Asm_full_simp_tac 1);
by (Asm_full_simp_tac 1);
qed "imperative_reverse";
@@ -23,7 +23,7 @@
\{y = X@Y}";
by (hoare_tac 1);
by (asm_full_simp_tac (simpset() addsimps [neq_Nil_conv]) 1);
-by (safe_tac (claset()));
+by Safe_tac;
by (Asm_full_simp_tac 1);
by (Asm_full_simp_tac 1);
qed "imperative_append";
--- a/src/HOL/IMP/Hoare.ML Wed Nov 05 13:14:15 1997 +0100
+++ b/src/HOL/IMP/Hoare.ML Wed Nov 05 13:23:46 1997 +0100
@@ -71,7 +71,7 @@
by (rtac iffI 1);
by (rtac weak_coinduct 1);
by (etac CollectI 1);
- by (safe_tac (claset()));
+ by Safe_tac;
by (rotate_tac ~1 1);
by (Asm_full_simp_tac 1);
by (rotate_tac ~1 1);
--- a/src/HOL/IMP/Transition.ML Wed Nov 05 13:14:15 1997 +0100
+++ b/src/HOL/IMP/Transition.ML Wed Nov 05 13:23:46 1997 +0100
@@ -87,7 +87,7 @@
(* ASSIGN *)
by (fast_tac (claset() addSDs [hlemma] addSEs [rel_pow_E2]
- addss simpset()) 1);
+ addss simpset()) 1);
(* SEMI *)
by (fast_tac (claset() addSDs [lemma2,rel_pow_imp_rtrancl]) 1);
@@ -98,8 +98,7 @@
by (fast_tac (claset() addSDs [rel_pow_imp_rtrancl]) 1);
(* WHILE, induction on the length of the computation *)
-by (rotate_tac 1 1);
-by (etac rev_mp 1);
+by (eres_inst_tac [("P","?X -n-> ?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);
--- 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<n then fst ex i \
\ else (if i=n then Some a else None), \
\ %i. if i<Suc n then snd ex i else t)")] bexI 1);
@@ -77,13 +77,13 @@
\ !!s t a. [|reachable A s; P(s)|] ==> (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";
--- 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);
--- 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);
--- 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);
--- 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";
--- 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,
--- 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);
--- 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";
--- 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";
--- 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";
--- 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);
--- 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";
--- 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);
--- 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));
--- 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 ***)