# HG changeset patch # User oheimb # Date 891530342 -7200 # Node ID 8c7e7eaffbdfc2b6f16f01a436456a3beb339ae9 # Parent f1bacbbe02a8d7c3829e7498b2ac39a16088b9d0 split_all_tac now fails if there is nothing to split split_all_tac has moved within claset() from usafe wrappers to safe wrappers diff -r f1bacbbe02a8 -r 8c7e7eaffbdf src/HOL/IMP/Transition.ML --- a/src/HOL/IMP/Transition.ML Thu Apr 02 13:49:04 1998 +0200 +++ b/src/HOL/IMP/Transition.ML Thu Apr 02 17:19:02 1998 +0200 @@ -33,12 +33,8 @@ "!s t u c d. (c,s) -n-> (SKIP,t) --> (d,t) -*-> (SKIP,u) --> \ \ (c;d, s) -*-> (SKIP, u)"; by (nat_ind_tac "n" 1); - (* case n = 0 *) by (fast_tac (claset() addIs [rtrancl_into_rtrancl2])1); -(* induction step *) -by (safe_tac (claset() addSDs [rel_pow_Suc_D2])); -by (split_all_tac 1); -by (fast_tac (claset() addIs [rtrancl_into_rtrancl2]) 1); +by (fast_tac (claset() addIs [rtrancl_into_rtrancl2]addSDs [rel_pow_Suc_D2])1); qed_spec_mp "lemma1"; diff -r f1bacbbe02a8 -r 8c7e7eaffbdf src/HOL/IOA/IOA.ML --- a/src/HOL/IOA/IOA.ML Thu Apr 02 13:49:04 1998 +0200 +++ b/src/HOL/IOA/IOA.ML Thu Apr 02 17:19:02 1998 +0200 @@ -56,18 +56,19 @@ "!!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; - by (res_inst_tac [("x","(%i. if i invariant A P"; by (rewrite_goals_tac(reachable_def::Let_def::exec_rws)); by Safe_tac; - by (res_inst_tac [("Q","reachable A (snd ex n)")] conjunct1 1); + by (rename_tac "n ex1 ex2" 1); + by (res_inst_tac [("Q","reachable A (ex2 n)")] conjunct1 1); + by (Asm_full_simp_tac 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 (fast_tac (claset() addIs [p1,reachable_0]) 1); + by (eres_inst_tac[("x","n")] allE 1); + by (exhaust_tac "ex1 n" 1 THEN ALLGOALS Asm_full_simp_tac); by Safe_tac; - by (etac (p2 RS mp) 1); - by (ALLGOALS(fast_tac(claset() addDs [reachable_n]))); + by (etac (p2 RS mp) 1); + by (ALLGOALS(fast_tac(claset() addDs [reachable_n]))); qed "invariantI"; val [p1,p2] = goal IOA.thy diff -r f1bacbbe02a8 -r 8c7e7eaffbdf src/HOL/IOA/Solve.ML --- a/src/HOL/IOA/Solve.ML Thu Apr 02 13:49:04 1998 +0200 +++ b/src/HOL/IOA/Solve.ML Thu Apr 02 17:19:02 1998 +0200 @@ -16,16 +16,17 @@ by (simp_tac(simpset() addsimps [has_trace_def])1); by Safe_tac; + by (rename_tac "f ex1 ex2" 1); (* choose same trace, therefore same NF *) - by (res_inst_tac[("x","mk_trace C (fst ex)")] exI 1); + by (res_inst_tac[("x","mk_trace C ex1")] exI 1); by (Asm_full_simp_tac 1); (* give execution of abstract automata *) - by (res_inst_tac[("x","(mk_trace A (fst ex),%i. f(snd ex i))")] bexI 1); + by (res_inst_tac[("x","(mk_trace A ex1,%i. f (ex2 i))")] bexI 1); (* Traces coincide *) - by (asm_simp_tac (simpset() addsimps [mk_trace_def,filter_oseq_idemp])1); + by (asm_simp_tac (simpset() addsimps [mk_trace_def,filter_oseq_idemp])1); (* Use lemma *) by (forward_tac [states_of_exec_reachable] 1); @@ -42,8 +43,8 @@ by (asm_full_simp_tac (simpset() addsimps [is_execution_fragment_def])1); by Safe_tac; - by (eres_inst_tac [("x","snd ex n")] allE 1); - by (eres_inst_tac [("x","snd ex (Suc n)")] allE 1); + by (eres_inst_tac [("x","ex2 n")] allE 1); + by (eres_inst_tac [("x","ex2 (Suc n)")] allE 1); by (eres_inst_tac [("x","a")] allE 1); by (Asm_full_simp_tac 1); qed "trace_inclusion"; @@ -73,7 +74,7 @@ \ %i. fst (snd ex i))")] bexI 1); (* fst(s) is in projected execution *) by (Simp_tac 1); - by (fast_tac (claset() delWrapper "split_all_tac") 1); + by (fast_tac (claset() delSWrapper "split_all_tac") 1); (* projected execution is indeed an execution *) by (asm_full_simp_tac (simpset() addsimps [executions_def,is_execution_fragment_def, @@ -93,7 +94,7 @@ \ %i. snd (snd ex i))")] bexI 1); (* fst(s) is in projected execution *) by (Simp_tac 1); - by (fast_tac (claset() delWrapper "split_all_tac") 1); + by (fast_tac (claset() delSWrapper "split_all_tac") 1); (* projected execution is indeed an execution *) by (asm_full_simp_tac (simpset() addsimps [executions_def,is_execution_fragment_def, diff -r f1bacbbe02a8 -r 8c7e7eaffbdf src/HOL/Integ/Integ.ML --- a/src/HOL/Integ/Integ.ML Thu Apr 02 13:49:04 1998 +0200 +++ b/src/HOL/Integ/Integ.ML Thu Apr 02 17:19:02 1998 +0200 @@ -321,9 +321,10 @@ \ 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; -by (rewtac split_def); -by (simp_tac (simpset() addsimps add_ac@mult_ac) 1); + by Safe_tac; + by (rewtac split_def); + by (simp_tac (simpset() addsimps add_ac@mult_ac) 1); +by (rename_tac "x1 y1 x2 y2 z1 z2" 1); by (asm_simp_tac (simpset() delsimps [equiv_intrel_iff] addsimps add_ac@mult_ac) 1); by (rtac (intrelI RS(equiv_intrel RS equiv_class_eq)) 1); diff -r f1bacbbe02a8 -r 8c7e7eaffbdf src/HOL/Prod.ML --- a/src/HOL/Prod.ML Thu Apr 02 13:49:04 1998 +0200 +++ b/src/HOL/Prod.ML Thu Apr 02 17:19:02 1998 +0200 @@ -72,7 +72,7 @@ in -val split_all_tac = REPEAT o SUBGOAL (fn (prem,i) => +val split_all_tac = REPEAT1 o SUBGOAL (fn (prem,i) => case find_pair_param prem of None => no_tac | Some x => EVERY[res_inst_tac[("p",x)] PairE i, @@ -80,8 +80,7 @@ end; -(* consider addSbefore ?? *) -claset_ref() := claset() addbefore ("split_all_tac",split_all_tac); +claset_ref() := claset() addSaltern ("split_all_tac", split_all_tac); (*** lemmas for splitting paired `!!' Does not work with simplifier because it also affects premises in @@ -446,7 +445,7 @@ (*Attempts to remove occurrences of split, and pair-valued parameters*) val remove_split = rewrite_rule [split RS eq_reflection] o - rule_by_tactic (ALLGOALS split_all_tac); + rule_by_tactic (TRYALL split_all_tac); (*Uncurries any Var of function type in the rule*) fun split_rule_var (t as Var(v, Type("fun",[T1,T2])), rl) = diff -r f1bacbbe02a8 -r 8c7e7eaffbdf src/HOL/Trancl.ML --- a/src/HOL/Trancl.ML Thu Apr 02 13:49:04 1998 +0200 +++ b/src/HOL/Trancl.ML Thu Apr 02 17:19:02 1998 +0200 @@ -153,10 +153,7 @@ qed "rtrancl_converseI"; goal Trancl.thy "(r^-1)^* = (r^*)^-1"; -by (safe_tac (claset() addSIs [rtrancl_converseI])); -by (res_inst_tac [("p","x")] PairE 1); -by (hyp_subst_tac 1); -by (etac rtrancl_converseD 1); +by (safe_tac (claset() addSDs [rtrancl_converseD] addSIs [rtrancl_converseI])); qed "rtrancl_converse"; val major::prems = goal Trancl.thy @@ -336,9 +333,8 @@ goal Trancl.thy "(r^+)^= = r^*"; by Safe_tac; by (etac trancl_into_rtrancl 1); -by (split_all_tac 1); by (etac rtranclE 1); -auto(); +by (Auto_tac ); by (etac rtrancl_into_trancl1 1); ba 1; qed "reflcl_trancl"; @@ -348,7 +344,6 @@ by Safe_tac; by (dtac trancl_into_rtrancl 1); by (Asm_full_simp_tac 1); -by (split_all_tac 1); by (etac rtranclE 1); by Safe_tac; by (rtac r_into_trancl 1);