# HG changeset patch # User wenzelm # Date 1227029142 -3600 # Node ID 32d498cf75956e2c65303a73b98d86a0b4900efc # Parent d5db6dfcb34a0fd26f8d3c4b161f64ef81dbe22c eliminated rewrite_tac/fold_tac, which are not well-formed tactics due to change of main conclusion; eliminated obsolete alias rewtac for rewrite_goals_tac; diff -r d5db6dfcb34a -r 32d498cf7595 src/HOL/Tools/datatype_abs_proofs.ML --- a/src/HOL/Tools/datatype_abs_proofs.ML Tue Nov 18 18:25:10 2008 +0100 +++ b/src/HOL/Tools/datatype_abs_proofs.ML Tue Nov 18 18:25:42 2008 +0100 @@ -214,7 +214,7 @@ (map cert insts)) induct; val (tac, _) = Library.foldl mk_unique_tac (((rtac induct' THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1 - THEN rewtac (mk_meta_eq choice_eq), rec_intrs), + THEN rewrite_goals_tac [mk_meta_eq choice_eq], rec_intrs), descr' ~~ rec_elims ~~ recTs ~~ rec_result_Ts); in split_conj_thm (SkipProof.prove_global thy1 [] [] diff -r d5db6dfcb34a -r 32d498cf7595 src/HOL/Tools/inductive_package.ML --- a/src/HOL/Tools/inductive_package.ML Tue Nov 18 18:25:10 2008 +0100 +++ b/src/HOL/Tools/inductive_package.ML Tue Nov 18 18:25:42 2008 +0100 @@ -33,9 +33,9 @@ val inductive_forall_name: string val inductive_forall_def: thm val rulify: thm -> thm - val inductive_cases: (Attrib.binding * string list) list -> Proof.context -> + val inductive_cases: (Attrib.binding * string list) list -> local_theory -> thm list list * local_theory - val inductive_cases_i: (Attrib.binding * term list) list -> Proof.context -> + val inductive_cases_i: (Attrib.binding * term list) list -> local_theory -> thm list list * local_theory type inductive_flags val add_inductive_i: @@ -753,9 +753,10 @@ if coind then singleton (ProofContext.export (snd (Variable.add_fixes (map (fst o dest_Free) params) ctxt1)) ctxt1) - (rotate_prems ~1 (ObjectLogic.rulify (rule_by_tactic - (rewrite_tac [le_fun_def, le_bool_def, sup_fun_eq, sup_bool_eq] THEN - fold_tac rec_preds_defs) (mono RS (fp_def RS def_coinduct))))) + (rotate_prems ~1 (ObjectLogic.rulify + (fold_rule rec_preds_defs + (rewrite_rule [le_fun_def, le_bool_def, sup_fun_eq, sup_bool_eq] + (mono RS (fp_def RS def_coinduct)))))) else prove_indrule quiet_mode cs argTs bs xs rec_const params intr_ts mono fp_def rec_preds_defs ctxt1); diff -r d5db6dfcb34a -r 32d498cf7595 src/HOLCF/IOA/NTP/Impl.thy --- a/src/HOLCF/IOA/NTP/Impl.thy Tue Nov 18 18:25:10 2008 +0100 +++ b/src/HOLCF/IOA/NTP/Impl.thy Tue Nov 18 18:25:42 2008 +0100 @@ -220,7 +220,7 @@ (@{thm raw_inv1} RS @{thm invariantE})] 1 *}) apply (tactic "tac2 1") - apply (tactic {* fold_tac [rewrite_rule [@{thm Packet.hdr_def}] + apply (tactic {* fold_goals_tac [rewrite_rule [@{thm Packet.hdr_def}] (@{thm Impl.hdr_sum_def})] *}) apply arith @@ -238,7 +238,7 @@ (@{thm raw_inv1} RS @{thm invariantE}) RS conjunct2] 1 *}) apply (intro strip) apply (erule conjE)+ - apply (tactic {* fold_tac [rewrite_rule [@{thm Packet.hdr_def}] (@{thm Impl.hdr_sum_def})] *}) + apply (tactic {* fold_goals_tac [rewrite_rule [@{thm Packet.hdr_def}] (@{thm Impl.hdr_sum_def})] *}) apply simp done diff -r d5db6dfcb34a -r 32d498cf7595 src/Provers/splitter.ML --- a/src/Provers/splitter.ML Tue Nov 18 18:25:10 2008 +0100 +++ b/src/Provers/splitter.ML Tue Nov 18 18:25:42 2008 +0100 @@ -105,7 +105,7 @@ val lift = Goal.prove_global Pure.thy ["P", "Q", "R"] [Syntax.read_prop_global Pure.thy "!!x :: 'b. Q(x) == R(x) :: 'c"] (Syntax.read_prop_global Pure.thy "P(%x. Q(x)) == P(%x. R(x))") - (fn {prems = [prem], ...} => rewtac prem THEN rtac reflexive_thm 1) + (fn {prems, ...} => rewrite_goals_tac prems THEN rtac reflexive_thm 1) val trlift = lift RS transitive_thm; val _ $ (P $ _) $ _ = concl_of trlift; diff -r d5db6dfcb34a -r 32d498cf7595 src/Pure/meta_simplifier.ML --- a/src/Pure/meta_simplifier.ML Tue Nov 18 18:25:10 2008 +0100 +++ b/src/Pure/meta_simplifier.ML Tue Nov 18 18:25:42 2008 +0100 @@ -79,12 +79,10 @@ val rewrite_rule: thm list -> thm -> thm val rewrite_goals_rule: thm list -> thm -> thm val rewrite_goals_tac: thm list -> tactic - val rewrite_tac: thm list -> tactic val rewrite_goal_tac: thm list -> int -> tactic val rewtac: thm -> tactic val prune_params_tac: tactic val fold_rule: thm list -> thm -> thm - val fold_tac: thm list -> tactic val fold_goals_tac: thm list -> tactic end; @@ -1285,14 +1283,11 @@ (** meta-rewriting tactics **) -(*Rewrite throughout proof state. *) -fun rewrite_tac defs = PRIMITIVE (rewrite_rule defs); - -(*Rewrite subgoals only, not main goal. *) +(*Rewrite all subgoals*) fun rewrite_goals_tac defs = PRIMITIVE (rewrite_goals_rule defs); fun rewtac def = rewrite_goals_tac [def]; -(*Rewrite subgoal i only.*) +(*Rewrite one subgoal*) fun asm_rewrite_goal_tac mode prover_tac ss i thm = if 0 < i andalso i <= Thm.nprems_of thm then Seq.single (Conv.gconv_rule (rewrite_cterm mode (SINGLE o prover_tac) ss) i thm) @@ -1329,7 +1324,6 @@ val rev_defs = sort_lhs_depths o map symmetric; fun fold_rule defs = fold rewrite_rule (rev_defs defs); -fun fold_tac defs = EVERY (map rewrite_tac (rev_defs defs)); fun fold_goals_tac defs = EVERY (map rewrite_goals_tac (rev_defs defs)); diff -r d5db6dfcb34a -r 32d498cf7595 src/ZF/Tools/datatype_package.ML --- a/src/ZF/Tools/datatype_package.ML Tue Nov 18 18:25:10 2008 +0100 +++ b/src/ZF/Tools/datatype_package.ML Tue Nov 18 18:25:42 2008 +0100 @@ -291,7 +291,7 @@ (Ind_Syntax.traceIt "next case equation = " thy1 (mk_case_eqn arg)) (*Proves a single case equation. Could use simp_tac, but it's slower!*) (fn _ => EVERY - [rewtac con_def, + [rewrite_goals_tac [con_def], rtac case_trans 1, REPEAT (resolve_tac [refl, split_trans, Su.case_inl RS trans, Su.case_inr RS trans] 1)]); diff -r d5db6dfcb34a -r 32d498cf7595 src/ZF/Tools/inductive_package.ML --- a/src/ZF/Tools/inductive_package.ML Tue Nov 18 18:25:10 2008 +0100 +++ b/src/ZF/Tools/inductive_package.ML Tue Nov 18 18:25:42 2008 +0100 @@ -262,7 +262,7 @@ ORELSE' bound_hyp_subst_tac)) THEN prune_params_tac (*Mutual recursion: collapse references to Part(D,h)*) - THEN fold_tac part_rec_defs; + THEN (PRIMITIVE (fold_rule part_rec_defs)); (*Elimination*) val elim = rule_by_tactic basic_elim_tac