--- a/src/HOL/Algebra/abstract/Ring.ML Fri Sep 15 12:39:57 2000 +0200
+++ b/src/HOL/Algebra/abstract/Ring.ML Fri Sep 15 15:30:50 2000 +0200
@@ -288,7 +288,7 @@
"!! a::'a::ring. a dvd <1> ==> a * inverse a = <1>";
by (Asm_simp_tac 1);
by (Clarify_tac 1);
-by (rtac selectI 1);
+by (rtac someI 1);
by (rtac sym 1);
by (assume_tac 1);
qed "r_inverse_ring";
--- a/src/HOL/Auth/Public.ML Fri Sep 15 12:39:57 2000 +0200
+++ b/src/HOL/Auth/Public.ML Fri Sep 15 15:30:50 2000 +0200
@@ -142,7 +142,7 @@
Goal "Nonce (@ N. Nonce N ~: used evs) ~: used evs";
by (rtac (lemma RS exE) 1);
-by (rtac selectI 1);
+by (rtac someI 1);
by (Fast_tac 1);
qed "Nonce_supply";
--- a/src/HOL/Auth/Shared.ML Fri Sep 15 12:39:57 2000 +0200
+++ b/src/HOL/Auth/Shared.ML Fri Sep 15 15:30:50 2000 +0200
@@ -158,7 +158,7 @@
Goal "Nonce (@ N. Nonce N ~: used evs) ~: used evs";
by (rtac (lemma RS exE) 1);
-by (rtac selectI 1);
+by (rtac someI 1);
by (Blast_tac 1);
qed "Nonce_supply";
@@ -192,7 +192,7 @@
Goal "Key (@ K. Key K ~: used evs) ~: used evs";
by (rtac (Finites.emptyI RS Key_supply_ax RS exE) 1);
-by (rtac selectI 1);
+by (rtac someI 1);
by (Blast_tac 1);
qed "Key_supply";
--- a/src/HOL/BCV/Kildall.ML Fri Sep 15 12:39:57 2000 +0200
+++ b/src/HOL/BCV/Kildall.ML Fri Sep 15 15:30:50 2000 +0200
@@ -185,7 +185,7 @@
by(asm_simp_tac (simpset() addsimps [same_fst_def,pres_type_def]) 1);
by(clarify_tac (claset() delrules [disjCI]) 1);
by(subgoal_tac "(@p. p:w) : w" 1);
- by (fast_tac (claset() addIs [selectI]) 2);
+ by (fast_tac (claset() addIs [someI]) 2);
by(subgoal_tac "ss : list (size ss) A" 1);
by (blast_tac (claset() addSIs [listI]) 2);
by(subgoal_tac "!q:set(succs (@ p. p : w)). q < size ss" 1);
@@ -213,7 +213,7 @@
by(rotate_tac ~1 1);
by(asm_full_simp_tac (simpset() addsimps [decomp_propa]) 1);
by(subgoal_tac "(@p. p:w) : w" 1);
- by (fast_tac (claset() addIs [selectI]) 2);
+ by (fast_tac (claset() addIs [someI]) 2);
by (blast_tac (claset() addDs [boundedD]) 1);
qed "iter_induct";
@@ -230,7 +230,7 @@
br impI 1;
by(stac decomp_propa 1);
by(subgoal_tac "(@p. p:w) : w" 1);
- by (fast_tac (claset() addIs [selectI]) 2);
+ by (fast_tac (claset() addIs [someI]) 2);
by (blast_tac (claset() addDs [boundedD]) 1);
by (Simp_tac 1);
qed "iter_unfold";
@@ -306,7 +306,7 @@
be impE 1;
by(asm_simp_tac (simpset() delsimps [listE_length]) 1);
by(subgoal_tac "(@p. p:w) : w" 1);
- by (fast_tac (claset() addIs [selectI]) 2);
+ by (fast_tac (claset() addIs [someI]) 2);
by(subgoal_tac "step (@ p. p : w) (ss ! (@ p. p : w)) : A" 1);
by (blast_tac (claset() addIs [pres_typeD,listE_nth_in]) 2);
be impE 1;
--- a/src/HOL/Fun.ML Fri Sep 15 12:39:57 2000 +0200
+++ b/src/HOL/Fun.ML Fri Sep 15 15:30:50 2000 +0200
@@ -24,7 +24,7 @@
(*"choice" is now proved in Tools/meson.ML*)
Goal "!!S. ALL x:S. EX y. Q x y ==> EX f. ALL x:S. Q x (f x)";
-by (fast_tac (claset() addEs [selectI]) 1);
+by (fast_tac (claset() addEs [someI]) 1);
qed "bchoice";
@@ -115,7 +115,7 @@
Goal "inj(f) ==> (@x. f(x)=f(y)) = y";
by (etac injD 1);
-by (rtac selectI 1);
+by (rtac someI 1);
by (rtac refl 1);
qed "inj_select";
@@ -212,7 +212,7 @@
qed "comp_inj_on";
Goalw [inv_def] "y : range(f) ==> f(inv f y) = y";
-by (fast_tac (claset() addIs [selectI]) 1);
+by (fast_tac (claset() addIs [someI]) 1);
qed "f_inv_f";
Goal "surj f ==> f(inv f y) = y";
--- a/src/HOL/HOL.ML Fri Sep 15 12:39:57 2000 +0200
+++ b/src/HOL/HOL.ML Fri Sep 15 15:30:50 2000 +0200
@@ -9,7 +9,7 @@
val refl = refl;
val subst = subst;
val ext = ext;
- val selectI = selectI;
+ val someI = someI;
val impI = impI;
val mp = mp;
val True_def = True_def;
--- a/src/HOL/HOL.thy Fri Sep 15 12:39:57 2000 +0200
+++ b/src/HOL/HOL.thy Fri Sep 15 15:30:50 2000 +0200
@@ -159,7 +159,7 @@
rule, and similar to the ABS rule of HOL.*)
ext: "(!!x::'a. (f x ::'b) = g x) ==> (%x. f x) = (%x. g x)"
- selectI: "P (x::'a) ==> P (@x. P x)"
+ someI: "P (x::'a) ==> P (@x. P x)"
impI: "(P ==> Q) ==> P-->Q"
mp: "[| P-->Q; P |] ==> Q"
--- a/src/HOL/HOL_lemmas.ML Fri Sep 15 12:39:57 2000 +0200
+++ b/src/HOL/HOL_lemmas.ML Fri Sep 15 15:30:50 2000 +0200
@@ -16,7 +16,7 @@
val refl = thm "refl";
val subst = thm "subst";
val ext = thm "ext";
-val selectI = thm "selectI";
+val someI = thm "someI";
val impI = thm "impI";
val mp = thm "mp";
val True_def = thm "True_def";
@@ -221,7 +221,7 @@
section "EX ";
Goalw [Ex_def] "P x ==> EX x::'a. P x";
-by (etac selectI 1) ;
+by (etac someI 1) ;
qed "exI";
val [major,minor] =
@@ -355,17 +355,17 @@
(** Select: Hilbert's Epsilon-operator **)
section "@";
-(*Easier to apply than selectI if witness ?a comes from an EX-formula*)
+(*Easier to apply than someI if witness ?a comes from an EX-formula*)
Goal "EX x. P x ==> P (SOME x. P x)";
by (etac exE 1);
-by (etac selectI 1);
+by (etac someI 1);
qed "ex_someI";
-(*Easier to apply than selectI: conclusion has only one occurrence of P*)
+(*Easier to apply than someI: conclusion has only one occurrence of P*)
val prems = Goal
"[| P a; !!x. P x ==> Q x |] ==> Q (@x. P x)";
by (resolve_tac prems 1);
-by (rtac selectI 1);
+by (rtac someI 1);
by (resolve_tac prems 1) ;
qed "someI2";
@@ -400,7 +400,7 @@
by (rtac iffI 1);
by (etac exI 1);
by (etac exE 1);
-by (etac selectI 1);
+by (etac someI 1);
qed "some_eq_ex";
Goal "(@y. y=x) = x";
--- a/src/HOL/MicroJava/BV/LBVCorrect.thy Fri Sep 15 12:39:57 2000 +0200
+++ b/src/HOL/MicroJava/BV/LBVCorrect.thy Fri Sep 15 15:30:50 2000 +0200
@@ -332,7 +332,7 @@
(\<epsilon>(Cl,x,y,mdecls). (Cl, x, y, mdecls) \<in> set G \<and> Cl = a))) mb) m"
by - (drule bspec, assumption,
clarsimp dest!: wtl_method_correct,
- clarsimp intro!: selectI simp add: unique_epsilon)
+ clarsimp intro!: someI simp add: unique_epsilon)
qed
qed (auto simp add: wtl_jvm_prog_def wf_prog_def wf_cdecl_def)
qed
--- a/src/HOL/MicroJava/J/State.ML Fri Sep 15 12:39:57 2000 +0200
+++ b/src/HOL/MicroJava/J/State.ML Fri Sep 15 15:30:50 2000 +0200
@@ -12,7 +12,7 @@
val new_AddrD = prove_goalw thy [new_Addr_def]
"\\<And>X. (a,x) = new_Addr h \\<Longrightarrow> h a = None \\<and> x = None | x = Some OutOfMemory" (K[
asm_full_simp_tac (simpset() addsimps [Pair_fst_snd_eq,select_split]) 1,
- rtac selectI 1,
+ rtac someI 1,
rtac disjI2 1,
res_inst_tac [("r","snd (a,Some OutOfMemory)")] trans 1,
Auto_tac ]);
--- a/src/HOL/WF.ML Fri Sep 15 12:39:57 2000 +0200
+++ b/src/HOL/WF.ML Fri Sep 15 15:30:50 2000 +0200
@@ -290,7 +290,7 @@
Goalw [the_recfun_def]
"is_recfun r H a f ==> is_recfun r H a (the_recfun r H a)";
-by (eres_inst_tac [("P", "is_recfun r H a")] selectI 1);
+by (eres_inst_tac [("P", "is_recfun r H a")] someI 1);
qed "is_the_recfun";
Goal "[| wf(r); trans(r) |] ==> is_recfun r H a (the_recfun r H a)";
--- a/src/HOL/meson_lemmas.ML Fri Sep 15 12:39:57 2000 +0200
+++ b/src/HOL/meson_lemmas.ML Fri Sep 15 15:30:50 2000 +0200
@@ -9,7 +9,7 @@
(* "Axiom" of Choice, proved using the description operator *)
Goal "ALL x. EX y. Q x y ==> EX f. ALL x. Q x (f x)";
-by (fast_tac (claset() addEs [selectI]) 1);
+by (fast_tac (claset() addEs [someI]) 1);
qed "choice";
--- a/src/HOLCF/IOA/meta_theory/RefCorrectness.ML Fri Sep 15 12:39:57 2000 +0200
+++ b/src/HOLCF/IOA/meta_theory/RefCorrectness.ML Fri Sep 15 15:30:50 2000 +0200
@@ -68,7 +68,7 @@
by (subgoal_tac "? ex. move A ex (f s) a (f t)" 1);
by (Asm_full_simp_tac 2);
by (etac exE 1);
-by (rtac selectI 1);
+by (rtac someI 1);
by (assume_tac 1);
qed"move_is_move";
--- a/src/HOLCF/IOA/meta_theory/SimCorrectness.ML Fri Sep 15 12:39:57 2000 +0200
+++ b/src/HOLCF/IOA/meta_theory/SimCorrectness.ML Fri Sep 15 15:30:50 2000 +0200
@@ -86,11 +86,11 @@
(* Go on as usual *)
by (etac exE 1);
by (dres_inst_tac [("x","t'"),
- ("P","%t'. ? ex.(t,t'):R & move A ex s' a t'")] selectI 1);
+ ("P","%t'. ? ex.(t,t'):R & move A ex s' a t'")] someI 1);
by (etac exE 1);
by (etac conjE 1);
by (asm_full_simp_tac (simpset() addsimps [Let_def]) 1);
-by (res_inst_tac [("x","ex")] selectI 1);
+by (res_inst_tac [("x","ex")] someI 1);
by (etac conjE 1);
by (assume_tac 1);
qed"move_is_move_sim";
--- a/src/HOLCF/Porder.ML Fri Sep 15 12:39:57 2000 +0200
+++ b/src/HOLCF/Porder.ML Fri Sep 15 15:30:50 2000 +0200
@@ -56,7 +56,7 @@
Goal "M <<| l ==> lub(M) = l";
by (rtac unique_lub 1);
by (stac lub 1);
-by (etac selectI 1);
+by (etac someI 1);
by (atac 1);
qed "thelubI";
@@ -130,7 +130,7 @@
Goalw [finite_chain_def]
"finite_chain(C) ==> range(C) <<| C(@ i. max_in_chain i C)";
by (rtac lub_finch1 1);
-by (best_tac (claset() addIs [selectI]) 2);
+by (best_tac (claset() addIs [someI]) 2);
by (Blast_tac 1);
qed "lub_finch2";