# HG changeset patch # User paulson # Date 969024650 -7200 # Node ID dfe4747c8318110f715b9489f38747d74c24e936 # Parent 4753185f1dd24ddbf405a94647388b56814b49cb the final renaming: selectI -> someI diff -r 4753185f1dd2 -r dfe4747c8318 src/HOL/Algebra/abstract/Ring.ML --- 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"; diff -r 4753185f1dd2 -r dfe4747c8318 src/HOL/Auth/Public.ML --- 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"; diff -r 4753185f1dd2 -r dfe4747c8318 src/HOL/Auth/Shared.ML --- 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"; diff -r 4753185f1dd2 -r dfe4747c8318 src/HOL/BCV/Kildall.ML --- 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; diff -r 4753185f1dd2 -r dfe4747c8318 src/HOL/Fun.ML --- 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"; diff -r 4753185f1dd2 -r dfe4747c8318 src/HOL/HOL.ML --- 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; diff -r 4753185f1dd2 -r dfe4747c8318 src/HOL/HOL.thy --- 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" diff -r 4753185f1dd2 -r dfe4747c8318 src/HOL/HOL_lemmas.ML --- 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"; diff -r 4753185f1dd2 -r dfe4747c8318 src/HOL/MicroJava/BV/LBVCorrect.thy --- 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 @@ (\(Cl,x,y,mdecls). (Cl, x, y, mdecls) \ set G \ 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 diff -r 4753185f1dd2 -r dfe4747c8318 src/HOL/MicroJava/J/State.ML --- 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] "\\X. (a,x) = new_Addr h \\ h a = None \\ 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 ]); diff -r 4753185f1dd2 -r dfe4747c8318 src/HOL/WF.ML --- 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)"; diff -r 4753185f1dd2 -r dfe4747c8318 src/HOL/meson_lemmas.ML --- 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"; diff -r 4753185f1dd2 -r dfe4747c8318 src/HOLCF/IOA/meta_theory/RefCorrectness.ML --- 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"; diff -r 4753185f1dd2 -r dfe4747c8318 src/HOLCF/IOA/meta_theory/SimCorrectness.ML --- 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"; diff -r 4753185f1dd2 -r dfe4747c8318 src/HOLCF/Porder.ML --- 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";