# HG changeset patch # User berghofe # Date 838740806 -7200 # Node ID c2c8279d40f0c47773802db8b88af3cc31045c8a # Parent fa58f4a06f21bea50528e745cbc2460da27dd118 Classical tactics now use default claset. diff -r fa58f4a06f21 -r c2c8279d40f0 src/HOL/IOA/ABP/Correctness.ML --- a/src/HOL/IOA/ABP/Correctness.ML Mon Jul 29 18:31:39 1996 +0200 +++ b/src/HOL/IOA/ABP/Correctness.ML Tue Jul 30 17:33:26 1996 +0200 @@ -9,7 +9,7 @@ open Impl; open Impl_finite; goal Abschannel.thy "(? x.x=P & Q(x)) = Q(P)"; -by (fast_tac HOL_cs 1); +by (Fast_tac 1); qed"exis_elim"; Delsimps [split_paired_All]; @@ -47,7 +47,7 @@ goal Correctness.thy "(reduce(l)=[]) = (l=[])"; by (rtac iffI 1); by (subgoal_tac "(l~=[]) --> (reduce(l)~=[])" 1); - by (fast_tac HOL_cs 1); + by (Fast_tac 1); by (List.list.induct_tac "l" 1); by (Simp_tac 1); by (Simp_tac 1); @@ -139,7 +139,7 @@ by (case_tac "list=[]" 1); by (asm_full_simp_tac (!simpset addsimps [reverse_Nil,reverse_Cons]) 1); by (rtac (expand_if RS ssubst) 1); - by (fast_tac HOL_cs 1); + by (Fast_tac 1); by (rtac impI 1); by (Simp_tac 1); by (cut_inst_tac [("l","list")] cons_not_nil 1); @@ -230,7 +230,7 @@ by (TRY( (rtac conjI 1) THEN (* start states *) - (fast_tac set_cs 1))); + (Fast_tac 1))); (* main-part *) by (REPEAT (rtac allI 1)); by (rtac imp_conj_lemma 1); @@ -246,7 +246,7 @@ by (TRY( (rtac conjI 1) THEN (* start states *) - (fast_tac set_cs 1))); + (Fast_tac 1))); (* main-part *) by (REPEAT (rtac allI 1)); by (rtac imp_conj_lemma 1); @@ -261,7 +261,7 @@ by (TRY( (rtac conjI 1) THEN (* start states *) - (fast_tac set_cs 1))); + (Fast_tac 1))); (* main-part *) by (REPEAT (rtac allI 1)); by (rtac imp_conj_lemma 1); diff -r fa58f4a06f21 -r c2c8279d40f0 src/HOL/IOA/ABP/Lemmas.ML --- a/src/HOL/IOA/ABP/Lemmas.ML Mon Jul 29 18:31:39 1996 +0200 +++ b/src/HOL/IOA/ABP/Lemmas.ML Tue Jul 30 17:33:26 1996 +0200 @@ -8,22 +8,22 @@ (* Logic *) val prems = goal HOL.thy "(P ==> Q-->R) ==> P&Q --> R"; - by(fast_tac (HOL_cs addDs prems) 1); + by(fast_tac (!claset addDs prems) 1); qed "imp_conj_lemma"; goal HOL.thy "(~(A&B)) = ((~A)&B| ~B)"; -by (fast_tac HOL_cs 1); +by (Fast_tac 1); val and_de_morgan_and_absorbe = result(); goal HOL.thy "(if C then A else B) --> (A|B)"; by (rtac (expand_if RS ssubst) 1); -by (fast_tac HOL_cs 1); +by (Fast_tac 1); val bool_if_impl_or = result(); (* Sets *) val set_lemmas = - map (fn s => prove_goal Set.thy s (fn _ => [fast_tac set_cs 1])) + map (fn s => prove_goal Set.thy s (fn _ => [Fast_tac 1])) ["f(x) : (UN x. {f(x)})", "f x y : (UN x y. {f x y})", "!!a. (!x. a ~= f(x)) ==> a ~: (UN x. {f(x)})", @@ -33,11 +33,11 @@ namely for Intersections and the empty list (compatibility of IOA!) *) goal Set.thy "(UN b.{x.x=f(b)})= (UN b.{f(b)})"; by (rtac set_ext 1); - by (fast_tac set_cs 1); + by (Fast_tac 1); val singleton_set =result(); goal HOL.thy "((A|B)=False) = ((~A)&(~B))"; - by (fast_tac HOL_cs 1); + by (Fast_tac 1); val de_morgan = result(); (* Lists *) @@ -53,5 +53,5 @@ goal List.thy "l ~= [] --> (? x xs. l = (x#xs))"; by (List.list.induct_tac "l" 1); by (simp_tac list_ss 1); - by (fast_tac HOL_cs 1); + by (Fast_tac 1); qed"cons_not_nil"; diff -r fa58f4a06f21 -r c2c8279d40f0 src/HOL/IOA/NTP/Correctness.ML --- a/src/HOL/IOA/NTP/Correctness.ML Mon Jul 29 18:31:39 1996 +0200 +++ b/src/HOL/IOA/NTP/Correctness.ML Tue Jul 30 17:33:26 1996 +0200 @@ -106,7 +106,7 @@ by(case_tac "sq(sen(s))=[]" 1); by(asm_full_simp_tac ss' 1); -by(fast_tac (HOL_cs addSDs [add_leD1 RS leD]) 1); +by(fast_tac (!claset addSDs [add_leD1 RS leD]) 1); by(case_tac "m = hd(sq(sen(s)))" 1); @@ -114,7 +114,7 @@ [imp_ex_equiv,neq_Nil_conv,ex_all_equiv]) 1); by(Asm_full_simp_tac 1); -by(fast_tac (HOL_cs addSDs [add_leD1 RS leD]) 1); +by(fast_tac (!claset addSDs [add_leD1 RS leD]) 1); by(Asm_full_simp_tac 1); qed"ntp_correct"; diff -r fa58f4a06f21 -r c2c8279d40f0 src/HOL/IOA/NTP/Impl.ML --- a/src/HOL/IOA/NTP/Impl.ML Mon Jul 29 18:31:39 1996 +0200 +++ b/src/HOL/IOA/NTP/Impl.ML Tue Jul 30 17:33:26 1996 +0200 @@ -182,14 +182,14 @@ by (forward_tac [rewrite_rule [Impl.inv1_def] (inv1 RS invariantE) RS conjunct1] 1); by (tac2 1); - by (fast_tac (HOL_cs addDs [add_leD1,leD]) 1); + by (fast_tac (!claset addDs [add_leD1,leD]) 1); (* 3 *) by (forward_tac [rewrite_rule [Impl.inv1_def] (inv1 RS invariantE)] 1); by (tac2 1); by (fold_tac [rewrite_rule [Packet.hdr_def]Impl.hdr_sum_def]); - by (fast_tac (HOL_cs addDs [add_leD1,leD]) 1); + by (fast_tac (!claset addDs [add_leD1,leD]) 1); (* 2 *) by (tac2 1); @@ -245,7 +245,7 @@ (* 7 *) by (tac3 1); by (tac_ren 1); - by (fast_tac HOL_cs 1); + by (Fast_tac 1); (* 6 - 3 *) diff -r fa58f4a06f21 -r c2c8279d40f0 src/HOL/IOA/NTP/Lemmas.ML --- a/src/HOL/IOA/NTP/Lemmas.ML Mon Jul 29 18:31:39 1996 +0200 +++ b/src/HOL/IOA/NTP/Lemmas.ML Tue Jul 30 17:33:26 1996 +0200 @@ -10,43 +10,43 @@ (* Logic *) val prems = goal HOL.thy "(P ==> Q-->R) ==> P&Q --> R"; - by(fast_tac (HOL_cs addDs prems) 1); + by(fast_tac (!claset addDs prems) 1); qed "imp_conj_lemma"; goal HOL.thy "(P --> (? x. Q(x))) = (? x. P --> Q(x))"; - by(fast_tac HOL_cs 1); + by(Fast_tac 1); qed "imp_ex_equiv"; goal HOL.thy "(A --> B & C) = ((A --> B) & (A --> C))"; - by (fast_tac HOL_cs 1); + by (Fast_tac 1); qed "fork_lemma"; goal HOL.thy "((A --> B) & (C --> B)) = ((A | C) --> B)"; - by (fast_tac HOL_cs 1); + by (Fast_tac 1); qed "imp_or_lem"; goal HOL.thy "(X = (~ Y)) = ((~X) = Y)"; - by (fast_tac HOL_cs 1); + by (Fast_tac 1); qed "neg_flip"; goal HOL.thy "P --> Q(M) --> Q(if P then M else N)"; by (rtac impI 1); by (rtac impI 1); by (rtac (expand_if RS iffD2) 1); - by (fast_tac HOL_cs 1); + by (Fast_tac 1); qed "imp_true_decompose"; goal HOL.thy "(~P) --> Q(N) --> Q(if P then M else N)"; by (rtac impI 1); by (rtac impI 1); by (rtac (expand_if RS iffD2) 1); - by (fast_tac HOL_cs 1); + by (Fast_tac 1); qed "imp_false_decompose"; (* Sets *) val set_lemmas = - map (fn s => prove_goal Set.thy s (fn _ => [fast_tac set_cs 1])) + map (fn s => prove_goal Set.thy s (fn _ => [Fast_tac 1])) ["f(x) : (UN x. {f(x)})", "f x y : (UN x y. {f x y})", "!!a. (!x. a ~= f(x)) ==> a ~: (UN x. {f(x)})", @@ -75,7 +75,7 @@ by (nat_ind_tac "x" 1); by (Simp_tac 1); by (Asm_simp_tac 1); - by (fast_tac HOL_cs 1); + by (Fast_tac 1); qed "nonzero_is_succ"; goal Arith.thy "(m::nat) < n --> m + p < n + p"; @@ -96,7 +96,7 @@ by (Asm_simp_tac 1); by (rtac impI 1); by (dtac Suc_leD 1); - by (fast_tac HOL_cs 1); + by (Fast_tac 1); qed "left_add_leq"; goal Arith.thy "(A::nat) < B --> C < D --> A + C < B + D"; @@ -115,7 +115,7 @@ by (rtac impI 1); by (rtac impI 1); by (asm_full_simp_tac (!simpset addsimps [le_eq_less_or_eq]) 1); - by (safe_tac HOL_cs); + by (safe_tac (!claset)); by (rtac (less_add_cong RS mp RS mp) 1); by (assume_tac 1); by (assume_tac 1); @@ -143,21 +143,21 @@ by (Simp_tac 1); by (rtac iffI 1); by (Asm_full_simp_tac 1); - by (fast_tac HOL_cs 1); + by (Fast_tac 1); qed "suc_not_zero"; goal Arith.thy "Suc(x) <= y --> (? z. y = Suc(z))"; by (rtac impI 1); by (asm_full_simp_tac (!simpset addsimps [le_eq_less_or_eq]) 1); - by (safe_tac HOL_cs); - by (fast_tac HOL_cs 2); + by (safe_tac (!claset)); + by (Fast_tac 2); by (asm_simp_tac (!simpset addsimps [suc_not_zero]) 1); qed "suc_leq_suc"; goal Arith.thy "~0 n = 0"; by (nat_ind_tac "n" 1); by (Asm_simp_tac 1); - by (safe_tac HOL_cs); + by (safe_tac (!claset)); by (Asm_full_simp_tac 1); by (Asm_full_simp_tac 1); qed "zero_eq"; @@ -165,7 +165,7 @@ goal Arith.thy "x < Suc(y) --> x<=y"; by (nat_ind_tac "n" 1); by (asm_simp_tac (!simpset addsimps [less_Suc_eq]) 1); - by (safe_tac HOL_cs); + by (safe_tac (!claset)); by (etac less_imp_le 1); qed "less_suc_imp_leq"; diff -r fa58f4a06f21 -r c2c8279d40f0 src/HOL/IOA/NTP/Multiset.ML --- a/src/HOL/IOA/NTP/Multiset.ML Mon Jul 29 18:31:39 1996 +0200 +++ b/src/HOL/IOA/NTP/Multiset.ML Tue Jul 30 17:33:26 1996 +0200 @@ -34,7 +34,7 @@ addsimps [Multiset.delm_nonempty_def, Multiset.countm_nonempty_def] setloop (split_tac [expand_if])) 1); - by (safe_tac HOL_cs); + by (safe_tac (!claset)); by (Asm_full_simp_tac 1); qed "count_delm_simp"; diff -r fa58f4a06f21 -r c2c8279d40f0 src/HOL/IOA/meta_theory/IOA.ML --- a/src/HOL/IOA/meta_theory/IOA.ML Mon Jul 29 18:31:39 1996 +0200 +++ b/src/HOL/IOA/meta_theory/IOA.ML Tue Jul 30 17:33:26 1996 +0200 @@ -41,7 +41,7 @@ \ (s(n)=Some(a) & a : externals(asig_of(A)))"; by (Option.option.induct_tac "s(n)" 1); by (ALLGOALS (simp_tac (!simpset setloop (split_tac [expand_if])))); - by (fast_tac HOL_cs 1); + by (Fast_tac 1); qed "mk_trace_thm"; goalw IOA.thy [reachable_def] "!!A. s:starts_of(A) ==> reachable A s"; @@ -53,7 +53,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 1); - by(safe_tac set_cs); + by(safe_tac (!claset)); 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 set_cs); + by (safe_tac (!claset)); by (res_inst_tac [("Q","reachable A (snd ex n)")] conjunct1 1); by (nat_ind_tac "n" 1); - by (fast_tac (set_cs addIs [p1,reachable_0]) 1); + by (fast_tac (!claset addIs [p1,reachable_0]) 1); by (eres_inst_tac[("x","n1")]allE 1); by (eres_inst_tac[("P","%x.!a.?Q x a"), ("opt","fst ex n1")] optE 1); by (Asm_simp_tac 1); - by (safe_tac HOL_cs); + by (safe_tac (!claset)); by (etac (p2 RS mp) 1); - by (ALLGOALS(fast_tac(set_cs addDs [hd Option.option.inject RS iffD1, + by (ALLGOALS(fast_tac(!claset addDs [hd Option.option.inject RS iffD1, reachable_n]))); qed "invariantI"; @@ -93,7 +93,7 @@ "[| !!s. s : starts_of(A) ==> P(s); \ \ !!s t a. reachable A s ==> P(s) --> (s,a,t):trans_of(A) --> P(t) \ \ |] ==> invariant A P"; - by (fast_tac (HOL_cs addSIs [invariantI] addSDs [p1,p2]) 1); + by (fast_tac (!claset addSIs [invariantI] addSDs [p1,p2]) 1); qed "invariantI1"; val [p1,p2] = goalw IOA.thy [invariant_def] @@ -116,7 +116,7 @@ (* Every state in an execution is reachable *) goalw IOA.thy [reachable_def] "!!A. ex:executions(A) ==> !n. reachable A (snd ex n)"; - by (fast_tac set_cs 1); + by (Fast_tac 1); qed "states_of_exec_reachable"; @@ -155,19 +155,19 @@ \ (externals(asig_of(A1)) Un externals(asig_of(A2)))"; by (asm_full_simp_tac (!simpset addsimps [externals_def,asig_of_par,asig_comp_def,asig_inputs_def,asig_outputs_def,Un_def,set_diff_def]) 1); by (rtac set_ext 1); -by (fast_tac set_cs 1); +by (Fast_tac 1); qed"externals_of_par"; goalw IOA.thy [externals_def,actions_def,compat_ioas_def,compat_asigs_def] "!! a. [| compat_ioas A1 A2; a:externals(asig_of(A1))|] ==> a~:internals(asig_of(A2))"; by (Asm_full_simp_tac 1); -by (best_tac (set_cs addEs [equalityCE]) 1); +by (best_tac (!claset addEs [equalityCE]) 1); qed"ext1_is_not_int2"; goalw IOA.thy [externals_def,actions_def,compat_ioas_def,compat_asigs_def] "!! a. [| compat_ioas A2 A1 ; a:externals(asig_of(A1))|] ==> a~:internals(asig_of(A2))"; by (Asm_full_simp_tac 1); -by (best_tac (set_cs addEs [equalityCE]) 1); +by (best_tac (!claset addEs [equalityCE]) 1); qed"ext2_is_not_int1"; val ext1_ext2_is_not_act2 = ext1_is_not_int2 RS int_and_ext_is_act; diff -r fa58f4a06f21 -r c2c8279d40f0 src/HOL/IOA/meta_theory/Option.ML --- a/src/HOL/IOA/meta_theory/Option.ML Mon Jul 29 18:31:39 1996 +0200 +++ b/src/HOL/IOA/meta_theory/Option.ML Tue Jul 30 17:33:26 1996 +0200 @@ -11,7 +11,7 @@ val [prem] = goal Option.thy "P(opt) ==> P(None) | (? x. P(Some(x)))"; br (prem RS rev_mp) 1; by (Option.option.induct_tac "opt" 1); - by (ALLGOALS(fast_tac HOL_cs)); + by (ALLGOALS(Fast_tac)); val optE = store_thm("optE", standard(result() RS disjE)); goal Option.thy "x=None | (? y.x=Some(y))"; diff -r fa58f4a06f21 -r c2c8279d40f0 src/HOL/IOA/meta_theory/Solve.ML --- a/src/HOL/IOA/meta_theory/Solve.ML Mon Jul 29 18:31:39 1996 +0200 +++ b/src/HOL/IOA/meta_theory/Solve.ML Tue Jul 30 17:33:26 1996 +0200 @@ -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 set_cs); + by (safe_tac (!claset)); (* 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 set_cs); + by (safe_tac (!claset)); (* 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 HOL_cs); + by (safe_tac (!claset)); 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 (HOL_cs addDs prems) 1); + by(fast_tac (!claset addDs prems) 1); val imp_conj_lemma = result(); @@ -61,7 +61,7 @@ \ a:externals(asig_of(A1)) & a~:externals(asig_of(A2)) | \ \ a~:externals(asig_of(A1)) & a:externals(asig_of(A2)))"; by (asm_full_simp_tac (!simpset addsimps [externals_def,asig_of_par,asig_comp_def,asig_inputs_def,asig_outputs_def]) 1); - by (fast_tac set_cs 1); + by (Fast_tac 1); val externals_of_par_extra = result(); goal Solve.thy "!!s.[| reachable (C1||C2) s |] ==> reachable C1 (fst s)"; @@ -73,7 +73,7 @@ \ %i.fst (snd ex i))")] bexI 1); (* fst(s) is in projected execution *) by (Simp_tac 1); - by (fast_tac HOL_cs 1); + by (Fast_tac 1); (* projected execution is indeed an execution *) by (asm_full_simp_tac (!simpset addsimps [executions_def,is_execution_fragment_def, par_def, starts_of_def,trans_of_def]) 1); @@ -108,7 +108,7 @@ \ %i.snd (snd ex i))")] bexI 1); (* fst(s) is in projected execution *) by (Simp_tac 1); - by (fast_tac HOL_cs 1); + by (Fast_tac 1); (* projected execution is indeed an execution *) by (asm_full_simp_tac (!simpset addsimps [executions_def,is_execution_fragment_def, par_def, starts_of_def,trans_of_def]) 1); @@ -138,7 +138,7 @@ by (rtac conjI 1); (* start_states *) by (asm_full_simp_tac (!simpset addsimps [par_def, starts_of_def]) 1); - by (fast_tac set_cs 1); + by (Fast_tac 1); (* transitions *) by (REPEAT (rtac allI 1)); by (rtac imp_conj_lemma 1); @@ -165,7 +165,7 @@ by (subgoal_tac "a~:externals(asig_of(A1)) & a~:externals(asig_of(A2))" 1); (* delete auxiliary subgoal *) by (Asm_full_simp_tac 2); -by (fast_tac HOL_cs 2); +by (Fast_tac 2); by (simp_tac (!simpset addsimps [conj_disj_distribR] addcongs [conj_cong] setloop (split_tac [expand_if])) 1); by(REPEAT((resolve_tac [conjI,impI] 1 ORELSE etac conjE 1) THEN @@ -202,19 +202,19 @@ by (dtac sym 1); by (dtac sym 1); by (Asm_full_simp_tac 1); -by (safe_tac HOL_cs); +by (safe_tac (!claset)); qed"reachable_rename_ioa"; (* HOL Lemmata - must already exist ! *) goal HOL.thy "(~(A|B)) =(~A&~B)"; - by (fast_tac HOL_cs 1); + by (Fast_tac 1); val disj_demorgan = result(); goal HOL.thy "(~(A&B)) =(~A|~B)"; - by (fast_tac HOL_cs 1); + by (Fast_tac 1); val conj_demorgan = result(); goal HOL.thy "(~(? x.P x)) =(! x. (~ (P x)))"; - by (fast_tac HOL_cs 1); + by (Fast_tac 1); val neg_ex = result(); @@ -227,7 +227,7 @@ 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 set_cs); +by (safe_tac (!claset)); by (rtac (expand_if RS ssubst) 1); by (rtac conjI 1); by (rtac impI 1); diff -r fa58f4a06f21 -r c2c8279d40f0 src/HOL/Integ/Bin.ML --- a/src/HOL/Integ/Bin.ML Mon Jul 29 18:31:39 1996 +0200 +++ b/src/HOL/Integ/Bin.ML Tue Jul 30 17:33:26 1996 +0200 @@ -54,7 +54,7 @@ (* SHOULD THIS THEOREM BE ADDED TO HOL_SS ? *) val my = prove_goal HOL.thy "(False = (~P)) = P" - (fn prem => [(fast_tac HOL_cs 1)]); + (fn prem => [(Fast_tac 1)]); qed_goal "bin_add_Bcons_Bcons0" Bin.thy "bin_add (Bcons v False) (Bcons w y) = norm_Bcons (bin_add v w) y" (fn prem => [(simp_tac (!simpset addsimps [my]) 1)]); @@ -141,7 +141,7 @@ goal Bin.thy "integ_of_bin(bin_add v w) = integ_of_bin v + integ_of_bin w"; by (cut_facts_tac [integ_of_bin_add_lemma] 1); -by (fast_tac HOL_cs 1); +by (Fast_tac 1); qed "integ_of_bin_add"; val bin_mult_simps = [integ_of_bin_minus, integ_of_bin_add,integ_of_bin_norm_Bcons]; diff -r fa58f4a06f21 -r c2c8279d40f0 src/HOL/Integ/Equiv.ML --- a/src/HOL/Integ/Equiv.ML Mon Jul 29 18:31:39 1996 +0200 +++ b/src/HOL/Integ/Equiv.ML Tue Jul 30 17:33:26 1996 +0200 @@ -10,18 +10,20 @@ open Equiv; +Delrules [equalityI]; + (*** Suppes, Theorem 70: r is an equiv relation iff converse(r) O r = r ***) (** first half: equiv A r ==> converse(r) O r = r **) goalw Equiv.thy [trans_def,sym_def,converse_def] "!!r. [| sym(r); trans(r) |] ==> converse(r) O r <= r"; -by (fast_tac (comp_cs addSEs [converseD]) 1); +by (fast_tac (!claset addSEs [converseD]) 1); qed "sym_trans_comp_subset"; goalw Equiv.thy [refl_def] "!!A r. refl A r ==> r <= converse(r) O r"; -by (fast_tac (rel_cs addIs [compI]) 1); +by (fast_tac (!claset addIs [compI]) 1); qed "refl_comp_subset"; goalw Equiv.thy [equiv_def] @@ -36,9 +38,9 @@ "!!A r. [| converse(r) O r = r; Domain(r) = A |] ==> equiv A r"; by (etac equalityE 1); by (subgoal_tac "ALL x y. (x,y) : r --> (y,x) : r" 1); -by (safe_tac set_cs); -by (fast_tac (set_cs addSIs [converseI] addIs [compI]) 3); -by (ALLGOALS (fast_tac (rel_cs addIs [compI] addSEs [compE]))); +by (safe_tac (!claset)); +by (fast_tac (!claset addSIs [converseI] addIs [compI]) 3); +by (ALLGOALS (fast_tac (!claset addIs [compI] addSEs [compE]))); qed "comp_equivI"; (** Equivalence classes **) @@ -46,28 +48,28 @@ (*Lemma for the next result*) goalw Equiv.thy [equiv_def,trans_def,sym_def] "!!A r. [| equiv A r; (a,b): r |] ==> r^^{a} <= r^^{b}"; -by (safe_tac rel_cs); +by (safe_tac (!claset)); by (rtac ImageI 1); -by (fast_tac rel_cs 2); -by (fast_tac rel_cs 1); +by (Fast_tac 2); +by (Fast_tac 1); qed "equiv_class_subset"; goal Equiv.thy "!!A r. [| equiv A r; (a,b): r |] ==> r^^{a} = r^^{b}"; by (REPEAT (ares_tac [equalityI, equiv_class_subset] 1)); by (rewrite_goals_tac [equiv_def,sym_def]); -by (fast_tac rel_cs 1); +by (Fast_tac 1); qed "equiv_class_eq"; val prems = goalw Equiv.thy [equiv_def,refl_def] "[| equiv A r; a: A |] ==> a: r^^{a}"; by (cut_facts_tac prems 1); -by (fast_tac rel_cs 1); +by (Fast_tac 1); qed "equiv_class_self"; (*Lemma for the next result*) goalw Equiv.thy [equiv_def,refl_def] "!!A r. [| equiv A r; r^^{b} <= r^^{a}; b: A |] ==> (a,b): r"; -by (fast_tac rel_cs 1); +by (Fast_tac 1); qed "subset_equiv_class"; val prems = goal Equiv.thy @@ -78,7 +80,7 @@ (*thus r^^{a} = r^^{b} as well*) goalw Equiv.thy [equiv_def,trans_def,sym_def] "!!A r. [| equiv A r; x: (r^^{a} Int r^^{b}) |] ==> (a,b): r"; -by (fast_tac rel_cs 1); +by (Fast_tac 1); qed "equiv_class_nondisjoint"; val [major] = goalw Equiv.thy [equiv_def,refl_def] @@ -88,7 +90,7 @@ goal Equiv.thy "!!A r. equiv A r ==> ((x,y): r) = (r^^{x} = r^^{y} & x:A & y:A)"; -by (safe_tac rel_cs); +by (safe_tac (!claset)); by ((rtac equiv_class_eq 1) THEN (assume_tac 1) THEN (assume_tac 1)); by ((rtac eq_equiv_class 3) THEN (assume_tac 4) THEN (assume_tac 4) THEN (assume_tac 3)); @@ -100,7 +102,7 @@ goal Equiv.thy "!!A r. [| equiv A r; x: A; y: A |] ==> (r^^{x} = r^^{y}) = ((x,y): r)"; -by (safe_tac rel_cs); +by (safe_tac (!claset)); by ((rtac eq_equiv_class 1) THEN (assume_tac 1) THEN (assume_tac 1) THEN (assume_tac 1)); by ((rtac equiv_class_eq 1) THEN @@ -123,7 +125,7 @@ by (resolve_tac [major RS UN_E] 1); by (rtac minor 1); by (assume_tac 2); -by (fast_tac rel_cs 1); +by (Fast_tac 1); qed "quotientE"; (** Not needed by Theory Integ --> bypassed **) @@ -136,10 +138,10 @@ (** Not needed by Theory Integ --> bypassed **) (*goalw Equiv.thy [quotient_def] "!!A r. [| equiv A r; X: A/r; Y: A/r |] ==> X=Y | (X Int Y <= 0)"; -by (safe_tac (ZF_cs addSIs [equiv_class_eq])); +by (safe_tac (!claset addSIs [equiv_class_eq])); by (assume_tac 1); by (rewrite_goals_tac [equiv_def,trans_def,sym_def]); -by (fast_tac ZF_cs 1); +by (Fast_tac 1); qed "quotient_disj"; **) @@ -147,7 +149,7 @@ (* theorem needed to prove UN_equiv_class *) goal Set.thy "!!A. [| a:A; ! y:A. b(y)=b(a) |] ==> (UN y:A. b(y))=b(a)"; -by (fast_tac (!claset addSEs [equalityE]) 1); +by (fast_tac (!claset addSEs [equalityE] addSIs [equalityI]) 1); qed "UN_singleton_lemma"; val UN_singleton = ballI RSN (2,UN_singleton_lemma); @@ -165,7 +167,7 @@ by (assume_tac 1); by (assume_tac 1); by (rewrite_goals_tac [equiv_def,congruent_def,sym_def]); -by (fast_tac rel_cs 1); +by (Fast_tac 1); qed "UN_equiv_class"; (*Resolve th against the "local" premises*) @@ -177,7 +179,7 @@ \ !!x. x : A ==> b(x) : B |] \ \ ==> (UN x:X. b(x)) : B"; by (cut_facts_tac prems 1); -by (safe_tac rel_cs); +by (safe_tac (!claset)); by (rtac (localize UN_equiv_class RS ssubst) 1); by (REPEAT (ares_tac prems 1)); qed "UN_equiv_class_type"; @@ -191,7 +193,7 @@ \ !!x y. [| x:A; y:A; b(x)=b(y) |] ==> (x,y):r |] \ \ ==> X=Y"; by (cut_facts_tac prems 1); -by (safe_tac rel_cs); +by (safe_tac ((!claset) delrules [equalityI])); by (rtac (equivA RS equiv_class_eq) 1); by (REPEAT (ares_tac prems 1)); by (etac box_equals 1); @@ -204,20 +206,20 @@ goalw Equiv.thy [congruent_def,congruent2_def,equiv_def,refl_def] "!!A r. [| equiv A r; congruent2 r b; a: A |] ==> congruent r (b a)"; -by (fast_tac rel_cs 1); +by (Fast_tac 1); qed "congruent2_implies_congruent"; val equivA::prems = goalw Equiv.thy [congruent_def] "[| equiv A r; congruent2 r b; a: A |] ==> \ \ congruent r (%x1. UN x2:r^^{a}. b x1 x2)"; by (cut_facts_tac (equivA::prems) 1); -by (safe_tac rel_cs); +by (safe_tac (!claset)); by (rtac (equivA RS equiv_type RS subsetD RS SigmaE2) 1); by (assume_tac 1); by (asm_simp_tac (!simpset addsimps [equivA RS UN_equiv_class, congruent2_implies_congruent]) 1); by (rewrite_goals_tac [congruent2_def,equiv_def,refl_def]); -by (fast_tac rel_cs 1); +by (Fast_tac 1); qed "congruent2_implies_congruent_UN"; val prems as equivA::_ = goal Equiv.thy @@ -236,7 +238,7 @@ \ !!x1 x2. [| x1: A; x2: A |] ==> b x1 x2 : B |] \ \ ==> (UN x1:X1. UN x2:X2. b x1 x2) : B"; by (cut_facts_tac prems 1); -by (safe_tac rel_cs); +by (safe_tac (!claset)); by (REPEAT (ares_tac (prems@[UN_equiv_class_type, congruent2_implies_congruent_UN, congruent2_implies_congruent, quotientI]) 1)); @@ -251,7 +253,7 @@ \ !! y z w. [| w: A; (y,z) : r |] ==> b w y = b w z \ \ |] ==> congruent2 r b"; by (cut_facts_tac prems 1); -by (safe_tac rel_cs); +by (safe_tac (!claset)); by (rtac trans 1); by (REPEAT (ares_tac prems 1 ORELSE etac (subsetD RS SigmaE2) 1 THEN assume_tac 2 THEN assume_tac 1)); diff -r fa58f4a06f21 -r c2c8279d40f0 src/HOL/Integ/Integ.ML --- a/src/HOL/Integ/Integ.ML Mon Jul 29 18:31:39 1996 +0200 +++ b/src/HOL/Integ/Integ.ML Tue Jul 30 17:33:26 1996 +0200 @@ -16,6 +16,8 @@ open Integ; +Delrules [equalityI]; + (*** Proving that intrel is an equivalence relation ***) @@ -35,14 +37,14 @@ val prems = goalw Integ.thy [intrel_def] "[| x1+y2 = x2+y1|] ==> \ \ ((x1,y1),(x2,y2)): intrel"; -by (fast_tac (rel_cs addIs prems) 1); +by (fast_tac (!claset addIs prems) 1); qed "intrelI"; (*intrelE is hard to derive because fast_tac tries hyp_subst_tac so soon*) goalw Integ.thy [intrel_def] "p: intrel --> (EX x1 y1 x2 y2. \ \ p = ((x1,y1),(x2,y2)) & x1+y2 = x2+y1)"; -by (fast_tac rel_cs 1); +by (Fast_tac 1); qed "intrelE_lemma"; val [major,minor] = goal Integ.thy @@ -53,10 +55,11 @@ by (REPEAT (eresolve_tac [asm_rl,exE,conjE,minor] 1)); qed "intrelE"; -val intrel_cs = rel_cs addSIs [intrelI] addSEs [intrelE]; +AddSIs [intrelI]; +AddSEs [intrelE]; goal Integ.thy "((x1,y1),(x2,y2)): intrel = (x1+y2 = x2+y1)"; -by (fast_tac intrel_cs 1); +by (Fast_tac 1); qed "intrel_iff"; goal Integ.thy "(x,x): intrel"; @@ -65,7 +68,7 @@ goalw Integ.thy [equiv_def, refl_def, sym_def, trans_def] "equiv {x::(nat*nat).True} intrel"; -by (fast_tac (intrel_cs addSIs [intrel_refl] +by (fast_tac (!claset addSIs [intrel_refl] addSEs [sym, integ_trans_lemma]) 1); qed "equiv_intrel"; @@ -75,7 +78,7 @@ (equiv_intrel RS eq_equiv_class_iff)); goalw Integ.thy [Integ_def,intrel_def,quotient_def] "intrel^^{(x,y)}:Integ"; -by (fast_tac set_cs 1); +by (Fast_tac 1); qed "intrel_in_integ"; goal Integ.thy "inj_onto Abs_Integ Integ"; @@ -103,8 +106,8 @@ by (REPEAT (rtac intrel_in_integ 1)); by (dtac eq_equiv_class 1); by (rtac equiv_intrel 1); -by (fast_tac set_cs 1); -by (safe_tac intrel_cs); +by (Fast_tac 1); +by (safe_tac (!claset)); by (Asm_full_simp_tac 1); qed "inj_znat"; @@ -113,7 +116,7 @@ goalw Integ.thy [congruent_def] "congruent intrel (%p. split (%x y. intrel^^{(y,x)}) p)"; -by (safe_tac intrel_cs); +by (safe_tac (!claset)); by (asm_simp_tac (!simpset addsimps add_ac) 1); qed "zminus_congruent"; @@ -168,12 +171,12 @@ goalw Integ.thy [znegative_def, znat_def] "~ znegative($# n)"; by (Simp_tac 1); -by (safe_tac intrel_cs); +by (safe_tac (!claset)); by (rtac ccontr 1); by (etac notE 1); by (Asm_full_simp_tac 1); by (dtac not_znegative_znat_lemma 1); -by (fast_tac (HOL_cs addDs [leD]) 1); +by (fast_tac (!claset addDs [leD]) 1); qed "not_znegative_znat"; goalw Integ.thy [znegative_def, znat_def] "znegative($~ $# Suc(n))"; @@ -200,7 +203,7 @@ goalw Integ.thy [congruent_def] "congruent intrel (split (%x y. intrel^^{((y-x) + (x-(y::nat)),0)}))"; -by (safe_tac intrel_cs); +by (safe_tac (!claset)); by (Asm_simp_tac 1); by (etac rev_mp 1); by (res_inst_tac [("m","x1"),("n","y1")] diff_induct 1); @@ -245,7 +248,7 @@ "congruent2 intrel (%p1 p2. \ \ split (%x1 y1. split (%x2 y2. intrel^^{(x1+x2, y1+y2)}) p2) p1)"; (*Proof via congruent2_commuteI seems longer*) -by (safe_tac intrel_cs); +by (safe_tac (!claset)); by (asm_simp_tac (!simpset addsimps [add_assoc]) 1); (*The rest should be trivial, but rearranging terms is hard*) by (res_inst_tac [("x1","x1a")] (add_left_commute RS ssubst) 1); @@ -332,7 +335,7 @@ \ split (%x1 y1. split (%x2 y2. \ \ intrel^^{(x1*x2 + y1*y2, x1*y2 + y1*x2)}) p2) p1)"; by (rtac (equiv_intrel RS congruent2_commuteI) 1); -by (safe_tac intrel_cs); +by (safe_tac (!claset)); by (rewtac split_def); by (simp_tac (!simpset addsimps add_ac@mult_ac) 1); by (asm_simp_tac (!simpset delsimps [equiv_intrel_iff] @@ -466,31 +469,31 @@ qed "zsuc_zpred"; goal Integ.thy "(zpred(z)=w) = (z=zsuc(w))"; -by (safe_tac HOL_cs); +by (safe_tac (!claset)); by (rtac (zsuc_zpred RS sym) 1); by (rtac zpred_zsuc 1); qed "zpred_to_zsuc"; goal Integ.thy "(zsuc(z)=w)=(z=zpred(w))"; -by (safe_tac HOL_cs); +by (safe_tac (!claset)); by (rtac (zpred_zsuc RS sym) 1); by (rtac zsuc_zpred 1); qed "zsuc_to_zpred"; goal Integ.thy "($~ z = w) = (z = $~ w)"; -by (safe_tac HOL_cs); +by (safe_tac (!claset)); by (rtac (zminus_zminus RS sym) 1); by (rtac zminus_zminus 1); qed "zminus_exchange"; goal Integ.thy"(zsuc(z)=zsuc(w)) = (z=w)"; -by (safe_tac intrel_cs); +by (safe_tac (!claset)); by (dres_inst_tac [("f","zpred")] arg_cong 1); by (asm_full_simp_tac (!simpset addsimps [zpred_zsuc]) 1); qed "bijective_zsuc"; goal Integ.thy"(zpred(z)=zpred(w)) = (z=w)"; -by (safe_tac intrel_cs); +by (safe_tac (!claset)); by (dres_inst_tac [("f","zsuc")] arg_cong 1); by (asm_full_simp_tac (!simpset addsimps [zsuc_zpred]) 1); qed "bijective_zpred"; @@ -549,7 +552,7 @@ val zsuc_n_not_n = n_not_zsuc_n RS not_sym; goal Integ.thy "w ~= zpred(w)"; -by (safe_tac HOL_cs); +by (safe_tac (!claset)); by (dres_inst_tac [("x","w"),("f","zsuc")] arg_cong 1); by (asm_full_simp_tac (!simpset addsimps [zsuc_zpred,zsuc_n_not_n]) 1); qed "n_not_zpred_n"; @@ -563,9 +566,9 @@ "!!w. w ? n. z = w + $#(Suc(n))"; by (res_inst_tac [("z","z")] eq_Abs_Integ 1); by (res_inst_tac [("z","w")] eq_Abs_Integ 1); -by (safe_tac intrel_cs); +by (safe_tac (!claset)); by (asm_full_simp_tac (!simpset addsimps [zadd, zminus]) 1); -by (safe_tac (intrel_cs addSDs [less_eq_Suc_add])); +by (safe_tac (!claset addSDs [less_eq_Suc_add])); by (res_inst_tac [("x","k")] exI 1); by (asm_full_simp_tac (!simpset delsimps [add_Suc, add_Suc_right] addsimps ([add_Suc RS sym] @ add_ac)) 1); @@ -578,7 +581,7 @@ goalw Integ.thy [zless_def, znegative_def, zdiff_def, znat_def] "z < z + $#(Suc(n))"; by (res_inst_tac [("z","z")] eq_Abs_Integ 1); -by (safe_tac intrel_cs); +by (safe_tac (!claset)); by (simp_tac (!simpset addsimps [zadd, zminus]) 1); by (REPEAT_SOME (ares_tac [refl, exI, singletonI, ImageI, conjI, intrelI])); by (rtac le_less_trans 1); @@ -587,7 +590,7 @@ qed "zless_zadd_Suc"; goal Integ.thy "!!z1 z2 z3. [| z1 z1 < (z3::int)"; -by (safe_tac (HOL_cs addSDs [zless_eq_zadd_Suc])); +by (safe_tac (!claset addSDs [zless_eq_zadd_Suc])); by (simp_tac (!simpset addsimps [zadd_assoc, zless_zadd_Suc, znat_add RS sym]) 1); qed "zless_trans"; @@ -599,9 +602,9 @@ val zless_zsucI = zlessI RSN (2,zless_trans); goal Integ.thy "!!z w::int. z ~w w ~= (z::int)"; -by(fast_tac (HOL_cs addEs [zless_irrefl]) 1); +by(fast_tac (!claset addEs [zless_irrefl]) 1); qed "zless_not_refl2"; @@ -631,7 +634,7 @@ "z w<(z::int)"; -by (fast_tac HOL_cs 1); +by (Fast_tac 1); qed "not_zleE"; goalw Integ.thy [zle_def] "!!z. z < w ==> z <= (w::int)"; -by (fast_tac (HOL_cs addEs [zless_asym]) 1); +by (fast_tac (!claset addEs [zless_asym]) 1); qed "zless_imp_zle"; goalw Integ.thy [zle_def] "!!z. z <= w ==> z < w | z=(w::int)"; by (cut_facts_tac [zless_linear] 1); -by (fast_tac (HOL_cs addEs [zless_irrefl,zless_asym]) 1); +by (fast_tac (!claset addEs [zless_irrefl,zless_asym]) 1); qed "zle_imp_zless_or_eq"; goalw Integ.thy [zle_def] "!!z. z z <=(w::int)"; by (cut_facts_tac [zless_linear] 1); -by (fast_tac (HOL_cs addEs [zless_irrefl,zless_asym]) 1); +by (fast_tac (!claset addEs [zless_irrefl,zless_asym]) 1); qed "zless_or_eq_imp_zle"; goal Integ.thy "(x <= (y::int)) = (x < y | x=y)"; @@ -696,17 +699,17 @@ val prems = goal Integ.thy "!!i. [| i <= j; j < k |] ==> i < (k::int)"; by (dtac zle_imp_zless_or_eq 1); -by (fast_tac (HOL_cs addIs [zless_trans]) 1); +by (fast_tac (!claset addIs [zless_trans]) 1); qed "zle_zless_trans"; goal Integ.thy "!!i. [| i <= j; j <= k |] ==> i <= (k::int)"; by (EVERY1 [dtac zle_imp_zless_or_eq, dtac zle_imp_zless_or_eq, - rtac zless_or_eq_imp_zle, fast_tac (HOL_cs addIs [zless_trans])]); + rtac zless_or_eq_imp_zle, fast_tac (!claset addIs [zless_trans])]); qed "zle_trans"; goal Integ.thy "!!z. [| z <= w; w <= z |] ==> z = (w::int)"; by (EVERY1 [dtac zle_imp_zless_or_eq, dtac zle_imp_zless_or_eq, - fast_tac (HOL_cs addEs [zless_irrefl,zless_asym])]); + fast_tac (!claset addEs [zless_irrefl,zless_asym])]); qed "zle_anti_sym"; @@ -719,13 +722,13 @@ (*** Monotonicity results ***) goal Integ.thy "!!v w z::int. v < w ==> v + z < w + z"; -by (safe_tac (HOL_cs addSDs [zless_eq_zadd_Suc])); +by (safe_tac (!claset addSDs [zless_eq_zadd_Suc])); by (simp_tac (!simpset addsimps zadd_ac) 1); by (simp_tac (!simpset addsimps [zadd_assoc RS sym, zless_zadd_Suc]) 1); qed "zadd_zless_mono1"; goal Integ.thy "!!v w z::int. (v+z < w+z) = (v < w)"; -by (safe_tac (HOL_cs addSEs [zadd_zless_mono1])); +by (safe_tac (!claset addSEs [zadd_zless_mono1])); by (dres_inst_tac [("z", "$~z")] zadd_zless_mono1 1); by (asm_full_simp_tac (!simpset addsimps [zadd_assoc]) 1); qed "zadd_left_cancel_zless"; diff -r fa58f4a06f21 -r c2c8279d40f0 src/HOL/Lex/Auto.ML --- a/src/HOL/Lex/Auto.ML Mon Jul 29 18:31:39 1996 +0200 +++ b/src/HOL/Lex/Auto.ML Tue Jul 30 17:33:26 1996 +0200 @@ -24,16 +24,16 @@ goalw Auto.thy [acc_prefix_def] "acc_prefix A s (x#xs) = (fin A (next A s x) | acc_prefix A (next A s x) xs)"; by(simp_tac (!simpset addsimps [prefix_Cons]) 1); -by(safe_tac HOL_cs); +by(safe_tac (!claset)); by(Asm_full_simp_tac 1); by (case_tac "zs=[]" 1); by(hyp_subst_tac 1); by(Asm_full_simp_tac 1); - by(fast_tac (HOL_cs addSEs [Cons_neq_Nil]) 1); + by(fast_tac (!claset addSEs [Cons_neq_Nil]) 1); by(res_inst_tac [("x","[x]")] exI 1); by(asm_simp_tac (!simpset addsimps [eq_sym_conv]) 1); by(res_inst_tac [("x","x#us")] exI 1); by(Asm_simp_tac 1); -by (fast_tac HOL_cs 1); +by (Fast_tac 1); qed"acc_prefix_Cons"; Addsimps [acc_prefix_Cons]; diff -r fa58f4a06f21 -r c2c8279d40f0 src/HOL/Lex/AutoChopper.ML --- a/src/HOL/Lex/AutoChopper.ML Mon Jul 29 18:31:39 1996 +0200 +++ b/src/HOL/Lex/AutoChopper.ML Tue Jul 30 17:33:26 1996 +0200 @@ -28,7 +28,7 @@ by (simp_tac (!simpset setloop (split_tac[expand_if])) 1); by (strip_tac 1); by (rtac conjI 1); -by (fast_tac HOL_cs 1); +by (Fast_tac 1); by(simp_tac (!simpset addsimps [prefix_Cons] addcongs [conj_cong]) 1); by (strip_tac 1); by(REPEAT(eresolve_tac [conjE,exE] 1)); @@ -36,13 +36,13 @@ by (Simp_tac 1); by (case_tac "zsa = []" 1); by (Asm_simp_tac 1); -by (fast_tac HOL_cs 1); +by (Fast_tac 1); bind_thm("no_acc", result() RS spec RS spec RS mp); val [prem] = goal HOL.thy "? x.P(f(x)) ==> ? y.P(y)"; by (cut_facts_tac [prem] 1); -by (fast_tac HOL_cs 1); +by (Fast_tac 1); val ex_special = result(); @@ -59,7 +59,7 @@ by (res_inst_tac[("xs","vss")] list_eq_cases 1); by(hyp_subst_tac 1); by(Simp_tac 1); - by (fast_tac (HOL_cs addSDs [no_acc]) 1); + by (fast_tac (!claset addSDs [no_acc]) 1); by(hyp_subst_tac 1); by (asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1); val step2_a = (result() repeat_RS spec) RS mp; @@ -74,7 +74,7 @@ by (simp_tac (!simpset setloop (split_tac [expand_if])) 1); by (list.induct_tac "xs" 1); by (simp_tac (!simpset addcongs [conj_cong] setloop (split_tac [expand_if])) 1); - by (fast_tac HOL_cs 1); + by (Fast_tac 1); by (asm_simp_tac (!simpset addcongs [conj_cong] setloop (split_tac [expand_if])) 1); by(res_inst_tac [("p","acc list (start A) [] [] ([],list) A")] PairE 1); by(rename_tac "vss lrst" 1); @@ -83,7 +83,7 @@ by (case_tac "acc_prefix A (next A st a) list" 1); by(Asm_simp_tac 1); by (subgoal_tac "r @ [a] ~= []" 1); - by (fast_tac HOL_cs 1); + by (Fast_tac 1); by (Simp_tac 1); val step2_b = (result() repeat_RS spec) RS mp; @@ -97,7 +97,7 @@ by (simp_tac (!simpset setloop (split_tac [expand_if])) 1); by (list.induct_tac "xs" 1); by (simp_tac (!simpset addcongs [conj_cong] setloop (split_tac [expand_if])) 1); - by (fast_tac HOL_cs 1); + by (Fast_tac 1); by (asm_simp_tac (!simpset addcongs [conj_cong] setloop (split_tac [expand_if])) 1); by (strip_tac 1); by (rtac conjI 1); @@ -110,20 +110,20 @@ by (Simp_tac 1); by (res_inst_tac [("t","%k.ys=r@a#k"),("s","%k.ys=(r@[a])@k")] subst 1); by (Simp_tac 1); - by (fast_tac HOL_cs 1); + by (Fast_tac 1); by (strip_tac 1); by (res_inst_tac [("x","[a]")] exI 1); by (Asm_simp_tac 1); by (subgoal_tac "r @ [a] ~= []" 1); br sym 1; - by (fast_tac HOL_cs 1); + by (Fast_tac 1); by (Simp_tac 1); by (strip_tac 1); by (res_inst_tac [("f","%k.a#k")] ex_special 1); by (Simp_tac 1); by (res_inst_tac [("t","%k.ys=r@a#k"),("s","%k.ys=(r@[a])@k")] subst 1); by (Simp_tac 1); -by (fast_tac HOL_cs 1); +by (Fast_tac 1); val step2_c = (result() repeat_RS spec) RS mp; @@ -136,7 +136,7 @@ by (simp_tac (!simpset setloop (split_tac [expand_if])) 1); by (list.induct_tac "xs" 1); by (simp_tac (!simpset addcongs [conj_cong] setloop (split_tac [expand_if])) 1); - by (fast_tac HOL_cs 1); + by (Fast_tac 1); by (asm_simp_tac (!simpset addcongs [conj_cong] setloop (split_tac [expand_if])) 1); by(res_inst_tac [("p","acc list (start A) [] [] ([],list) A")] PairE 1); by(rename_tac "vss lrst" 1); @@ -147,7 +147,7 @@ by (subgoal_tac "acc list (start A) [] [] ([],list) A = (yss,zs)" 1); by (Asm_simp_tac 2); by (subgoal_tac "r@[a] ~= []" 2); - by (fast_tac HOL_cs 2); + by (Fast_tac 2); by (Simp_tac 2); by (subgoal_tac "flat(yss) @ zs = list" 1); by(hyp_subst_tac 1); @@ -155,7 +155,7 @@ by (case_tac "yss = []" 1); by (Asm_simp_tac 1); by (hyp_subst_tac 1); - by (fast_tac (HOL_cs addSDs [no_acc]) 1); + by (fast_tac (!claset addSDs [no_acc]) 1); by (etac ((neq_Nil_conv RS iffD1) RS exE) 1); by (etac exE 1); by (hyp_subst_tac 1); @@ -175,7 +175,7 @@ by (simp_tac (!simpset setloop (split_tac [expand_if])) 1); by (list.induct_tac "xs" 1); by (simp_tac (!simpset addcongs [conj_cong] setloop (split_tac [expand_if])) 1); - by (fast_tac HOL_cs 1); + by (Fast_tac 1); by (asm_simp_tac (!simpset addcongs [conj_cong] setloop (split_tac [expand_if])) 1); by (strip_tac 1); by (case_tac "acc_prefix A (next A st a) list" 1); @@ -207,13 +207,13 @@ by (res_inst_tac [("x","[a]")] exI 1); by (rtac conjI 1); by (subgoal_tac "r @ [a] ~= []" 1); - by (fast_tac HOL_cs 1); + by (Fast_tac 1); by (Simp_tac 1); by (rtac list_cases 1); by (Simp_tac 1); by (asm_full_simp_tac (!simpset addsimps [acc_prefix_def] addcongs[conj_cong]) 1); by (etac thin_rl 1); (* speed up *) -by (fast_tac HOL_cs 1); +by (Fast_tac 1); val step2_e = (result() repeat_RS spec) RS mp; Addsimps[split_paired_All]; @@ -228,7 +228,7 @@ br mp 1; be step2_c 2; by (simp_tac (!simpset setloop (split_tac [expand_if])) 1); - by (fast_tac HOL_cs 1); + by (Fast_tac 1); by (rtac conjI 1); by (asm_simp_tac (!simpset addsimps [step2_a] setloop (split_tac [expand_if])) 1); by (rtac conjI 1); @@ -238,5 +238,5 @@ by (rtac mp 1); be step2_e 2; by (simp_tac (!simpset setloop (split_tac [expand_if])) 1); -by (fast_tac HOL_cs 1); +by (Fast_tac 1); qed"auto_chopper_is_auto_chopper"; diff -r fa58f4a06f21 -r c2c8279d40f0 src/HOL/Lex/Prefix.ML --- a/src/HOL/Lex/Prefix.ML Mon Jul 29 18:31:39 1996 +0200 +++ b/src/HOL/Lex/Prefix.ML Tue Jul 30 17:33:26 1996 +0200 @@ -21,7 +21,7 @@ goalw Prefix.thy [prefix_def] "(xs <= []) = (xs = [])"; by (list.induct_tac "xs" 1); by (Simp_tac 1); -by (fast_tac HOL_cs 1); +by (Fast_tac 1); by (Simp_tac 1); qed "prefix_Nil"; Addsimps [prefix_Nil]; @@ -31,13 +31,13 @@ "(xs <= y#ys) = (xs=[] | (? zs. xs=y#zs & zs <= ys))"; by (list.induct_tac "xs" 1); by (Simp_tac 1); -by (fast_tac HOL_cs 1); +by (Fast_tac 1); by (Simp_tac 1); -by (fast_tac HOL_cs 1); +by (Fast_tac 1); qed "prefix_Cons"; goalw Prefix.thy [prefix_def] "(x#xs <= y#ys) = (x=y & xs<=ys)"; by(Simp_tac 1); -by (fast_tac HOL_cs 1); +by (Fast_tac 1); qed"Cons_prefix_Cons"; Addsimps [Cons_prefix_Cons];