reorganized structure Tactic vs. MetaSimplifier;
--- a/TFL/casesplit.ML Thu Dec 07 21:44:13 2006 +0100
+++ b/TFL/casesplit.ML Thu Dec 07 23:16:55 2006 +0100
@@ -80,8 +80,8 @@
functor CaseSplitFUN(Data : CASE_SPLIT_DATA) =
struct
-val rulify_goals = Tactic.rewrite_goals_rule Data.rulify;
-val atomize_goals = Tactic.rewrite_goals_rule Data.atomize;
+val rulify_goals = MetaSimplifier.rewrite_goals_rule Data.rulify;
+val atomize_goals = MetaSimplifier.rewrite_goals_rule Data.atomize;
(* beta-eta contract the theorem *)
fun beta_eta_contract thm =
--- a/src/HOL/Hyperreal/transfer.ML Thu Dec 07 21:44:13 2006 +0100
+++ b/src/HOL/Hyperreal/transfer.ML Thu Dec 07 23:16:55 2006 +0100
@@ -62,7 +62,7 @@
val {intros,unfolds,refolds,consts} = TransferData.get (Context.Proof ctxt)
val meta = LocalDefs.meta_rewrite_rule ctxt
val unfolds' = map meta unfolds and refolds' = map meta refolds;
- val (_$_$t') = concl_of (Tactic.rewrite true unfolds' (cterm_of thy t))
+ val (_$_$t') = concl_of (MetaSimplifier.rewrite true unfolds' (cterm_of thy t))
val u = unstar_term consts t'
val tac =
rewrite_goals_tac (ths @ refolds' @ unfolds') THEN
--- a/src/HOL/Integ/presburger.ML Thu Dec 07 21:44:13 2006 +0100
+++ b/src/HOL/Integ/presburger.ML Thu Dec 07 23:16:55 2006 +0100
@@ -56,7 +56,7 @@
val powerarith =
(map thm ["nat_number_of", "zpower_number_of_even",
"zpower_Pls", "zpower_Min"]) @
- [(Tactic.simplify true [thm "zero_eq_Numeral0_nring",
+ [(MetaSimplifier.simplify true [thm "zero_eq_Numeral0_nring",
thm "one_eq_Numeral1_nring"]
(thm "zpower_number_of_odd"))]
--- a/src/HOL/Real/ferrante_rackoff.ML Thu Dec 07 21:44:13 2006 +0100
+++ b/src/HOL/Real/ferrante_rackoff.ML Thu Dec 07 23:16:55 2006 +0100
@@ -42,7 +42,7 @@
val powerarith =
map thm ["nat_number_of", "zpower_number_of_even",
"zpower_Pls", "zpower_Min"]
- @ [Tactic.simplify true [thm "zero_eq_Numeral0_nring", thm "one_eq_Numeral1_nring"]
+ @ [MetaSimplifier.simplify true [thm "zero_eq_Numeral0_nring", thm "one_eq_Numeral1_nring"]
(thm "zpower_number_of_odd")]
val comp_arith = binarith @ intarith @ intarithrel @ natarith
--- a/src/HOL/Tools/Presburger/presburger.ML Thu Dec 07 21:44:13 2006 +0100
+++ b/src/HOL/Tools/Presburger/presburger.ML Thu Dec 07 23:16:55 2006 +0100
@@ -56,7 +56,7 @@
val powerarith =
(map thm ["nat_number_of", "zpower_number_of_even",
"zpower_Pls", "zpower_Min"]) @
- [(Tactic.simplify true [thm "zero_eq_Numeral0_nring",
+ [(MetaSimplifier.simplify true [thm "zero_eq_Numeral0_nring",
thm "one_eq_Numeral1_nring"]
(thm "zpower_number_of_odd"))]
--- a/src/HOL/Tools/datatype_codegen.ML Thu Dec 07 21:44:13 2006 +0100
+++ b/src/HOL/Tools/datatype_codegen.ML Thu Dec 07 23:16:55 2006 +0100
@@ -375,7 +375,7 @@
in map mk_dist (sym_product cos) end;
local
- val bool_eq_implies = thm "iffD1";
+ val bool_eq_implies = iffD1;
val rew_eq = thm "HOL.atomize_eq" |> Thm.symmetric;
val rew_conj = thm "HOL.atomize_conj" |> Thm.symmetric;
val not_false_true = iffD2 OF [nth (thms "HOL.simp_thms") 7, TrueI];
@@ -387,7 +387,7 @@
val SOME (vs, cs) = DatatypePackage.get_datatype_spec thy dtco;
val inject = (#inject o DatatypePackage.the_datatype thy) dtco
|> map (fn thm => bool_eq_implies OF [thm] )
- |> map (Tactic.rewrite_rule [rew_eq, rew_conj]);
+ |> map (MetaSimplifier.rewrite_rule [rew_eq, rew_conj]);
val ctxt = ProofContext.init thy;
val simpset = Simplifier.context ctxt
(MetaSimplifier.empty_ss addsimprocs [DatatypePackage.distinct_simproc]);
--- a/src/HOL/Tools/record_package.ML Thu Dec 07 21:44:13 2006 +0100
+++ b/src/HOL/Tools/record_package.ML Thu Dec 07 23:16:55 2006 +0100
@@ -1428,7 +1428,7 @@
let
val SOME { Abs_induct = abs_induct,
Abs_inject=abs_inject, Abs_inverse = abs_inverse, ...} = TypedefPackage.get_info thy name;
- val rewrite_rule = Tactic.rewrite_rule [rec_UNIV_I, rec_True_simp];
+ val rewrite_rule = MetaSimplifier.rewrite_rule [rec_UNIV_I, rec_True_simp];
in map rewrite_rule [abs_inject, abs_inverse, abs_induct] end;
in
thy
--- a/src/HOL/Tools/typecopy_package.ML Thu Dec 07 21:44:13 2006 +0100
+++ b/src/HOL/Tools/typecopy_package.ML Thu Dec 07 23:16:55 2006 +0100
@@ -96,7 +96,7 @@
val tac = Tactic.rtac UNIV_witness 1;
fun add_info tyco ( { abs_type = ty_abs, rep_type = ty_rep, Abs_name = c_abs,
Rep_name = c_rep, Abs_inject = inject,
- Abs_inverse = inverse, ... } : TypedefPackage.info ) thy =
+ Abs_inverse = inverse, ... } : TypedefPackage.info ) thy =
let
val exists_thm =
UNIV_I
@@ -146,16 +146,16 @@
in (vs, [(constr, [typ])]) end;
local
- val bool_eq_implies = thm "iffD1";
+ val bool_eq_implies = iffD1;
val rew_eq = thm "HOL.atomize_eq" |> Thm.symmetric;
in fun get_cert thy tyco =
- Tactic.rewrite_rule [rew_eq] (bool_eq_implies OF [get_eq thy tyco])
+ MetaSimplifier.rewrite_rule [rew_eq] (bool_eq_implies OF [get_eq thy tyco])
end; (*local*)
(* hook for projection function code *)
-fun add_project (_ , { proj_def, ...} : info) =
+fun add_project (_ , {proj_def, ...} : info) =
CodegenData.add_func proj_def;
val setup =
--- a/src/Provers/eqsubst.ML Thu Dec 07 21:44:13 2006 +0100
+++ b/src/Provers/eqsubst.ML Thu Dec 07 23:16:55 2006 +0100
@@ -415,7 +415,7 @@
val th2 = Thm.rotate_rule (j - 1) i th; (* put premice first *)
val preelimrule =
(RWInst.rw m rule pth)
- |> (Seq.hd o Tactic.prune_params_tac)
+ |> (Seq.hd o prune_params_tac)
|> Thm.permute_prems 0 ~1 (* put old asm first *)
|> IsaND.unfix_frees cfvs (* unfix any global params *)
|> RWInst.beta_eta_contract; (* normal form *)
--- a/src/Provers/induct_method.ML Thu Dec 07 21:44:13 2006 +0100
+++ b/src/Provers/induct_method.ML Thu Dec 07 23:16:55 2006 +0100
@@ -160,7 +160,7 @@
MetaSimplifier.rewrite_term thy Data.atomize []
#> ObjectLogic.drop_judgment thy;
-val atomize_cterm = Tactic.rewrite true Data.atomize;
+val atomize_cterm = MetaSimplifier.rewrite true Data.atomize;
val atomize_tac = Goal.rewrite_goal_tac Data.atomize;
@@ -312,7 +312,7 @@
fun miniscope_tac p i = PRIMITIVE (Drule.fconv_rule
(Drule.goals_conv (Library.equal i)
- (Drule.forall_conv p (Tactic.rewrite true [Thm.symmetric Drule.norm_hhf_eq]))));
+ (Drule.forall_conv p (MetaSimplifier.rewrite true [Thm.symmetric Drule.norm_hhf_eq]))));
in
--- a/src/Pure/Isar/local_defs.ML Thu Dec 07 21:44:13 2006 +0100
+++ b/src/Pure/Isar/local_defs.ML Thu Dec 07 23:16:55 2006 +0100
@@ -161,11 +161,11 @@
fun meta f ctxt = f o map (meta_rewrite_rule ctxt);
-val unfold = meta Tactic.rewrite_rule;
-val unfold_goals = meta Tactic.rewrite_goals_rule;
-val unfold_tac = meta Tactic.rewrite_goals_tac;
-val fold = meta Tactic.fold_rule;
-val fold_tac = meta Tactic.fold_goals_tac;
+val unfold = meta MetaSimplifier.rewrite_rule;
+val unfold_goals = meta MetaSimplifier.rewrite_goals_rule;
+val unfold_tac = meta MetaSimplifier.rewrite_goals_tac;
+val fold = meta MetaSimplifier.fold_rule;
+val fold_tac = meta MetaSimplifier.fold_goals_tac;
(* derived defs -- potentially within the object-logic *)
@@ -186,7 +186,7 @@
Goal.prove ctxt' frees [] prop (K (ALLGOALS
(meta_rewrite_tac ctxt' THEN'
Goal.rewrite_goal_tac [def] THEN'
- Tactic.resolve_tac [Drule.reflexive_thm])))
+ resolve_tac [Drule.reflexive_thm])))
handle ERROR msg => cat_error msg "Failed to prove definitional specification."
end;
in (((c, T), rhs), prove) end;
--- a/src/Pure/Isar/locale.ML Thu Dec 07 21:44:13 2006 +0100
+++ b/src/Pure/Isar/locale.ML Thu Dec 07 23:16:55 2006 +0100
@@ -1648,17 +1648,17 @@
val cert = Thm.cterm_of defs_thy;
val intro = Goal.prove_global defs_thy [] norm_ts statement (fn _ =>
- Tactic.rewrite_goals_tac [pred_def] THEN
+ MetaSimplifier.rewrite_goals_tac [pred_def] THEN
Tactic.compose_tac (false, body_eq RS Drule.equal_elim_rule1, 1) 1 THEN
Tactic.compose_tac (false, Conjunction.intr_list (map (Thm.assume o cert) norm_ts), 0) 1);
val conjuncts =
(Drule.equal_elim_rule2 OF [body_eq,
- Tactic.rewrite_rule [pred_def] (Thm.assume (cert statement))])
+ MetaSimplifier.rewrite_rule [pred_def] (Thm.assume (cert statement))])
|> Conjunction.elim_precise [length ts] |> hd;
val axioms = ts ~~ conjuncts |> map (fn (t, ax) =>
Element.prove_witness defs_ctxt t
- (Tactic.rewrite_goals_tac defs THEN
+ (MetaSimplifier.rewrite_goals_tac defs THEN
Tactic.compose_tac (false, ax, 0) 1));
in ((statement, intro, axioms), defs_thy) end;
--- a/src/Pure/Isar/object_logic.ML Thu Dec 07 21:44:13 2006 +0100
+++ b/src/Pure/Isar/object_logic.ML Thu Dec 07 23:16:55 2006 +0100
@@ -148,12 +148,12 @@
fun rewrite_prems_tac rews i = PRIMITIVE (Drule.fconv_rule
(Drule.goals_conv (Library.equal i)
(Drule.forall_conv ~1
- (Drule.goals_conv (K true) (Tactic.rewrite true rews)))));
+ (Drule.goals_conv (K true) (MetaSimplifier.rewrite true rews)))));
fun atomize_term thy =
drop_judgment thy o MetaSimplifier.rewrite_term thy (get_atomize thy) [];
-fun atomize_cterm ct = Tactic.rewrite true (get_atomize (Thm.theory_of_cterm ct)) ct;
+fun atomize_cterm ct = MetaSimplifier.rewrite true (get_atomize (Thm.theory_of_cterm ct)) ct;
fun atomize_thm th = rewrite_rule (get_atomize (Thm.theory_of_thm th)) th;
fun atomize_tac i st =
@@ -174,7 +174,7 @@
fun rulify_tac i st = Goal.rewrite_goal_tac (get_rulify (Thm.theory_of_thm st)) i st;
fun gen_rulify full thm =
- Tactic.simplify full (get_rulify (Thm.theory_of_thm thm)) thm
+ MetaSimplifier.simplify full (get_rulify (Thm.theory_of_thm thm)) thm
|> Drule.gen_all |> Thm.strip_shyps |> Drule.zero_var_indexes;
val rulify = gen_rulify true;
--- a/src/Pure/Isar/rule_cases.ML Thu Dec 07 21:44:13 2006 +0100
+++ b/src/Pure/Isar/rule_cases.ML Thu Dec 07 23:16:55 2006 +0100
@@ -189,14 +189,14 @@
fun unfold_prems n defs th =
if null defs then th
- else Drule.fconv_rule (Drule.goals_conv (fn i => i <= n) (Tactic.rewrite true defs)) th;
+ else Drule.fconv_rule (Drule.goals_conv (fn i => i <= n) (MetaSimplifier.rewrite true defs)) th;
fun unfold_prems_concls defs th =
if null defs orelse not (can Logic.dest_conjunction (Thm.concl_of th)) then th
else
Drule.fconv_rule
(Drule.concl_conv ~1 (Conjunction.conv ~1
- (K (Drule.prems_conv ~1 (K (Tactic.rewrite true defs)))))) th;
+ (K (Drule.prems_conv ~1 (K (MetaSimplifier.rewrite true defs)))))) th;
in
--- a/src/Pure/Isar/theory_target.ML Thu Dec 07 21:44:13 2006 +0100
+++ b/src/Pure/Isar/theory_target.ML Thu Dec 07 23:16:55 2006 +0100
@@ -92,7 +92,7 @@
val thy_ctxt = ProofContext.init thy;
val ct = Thm.cterm_of thy t;
val (defs, ct') = LocalDefs.export ctxt thy_ctxt (Drule.mk_term ct) ||> Drule.dest_term;
- in (Thm.term_of ct', Tactic.rewrite true defs ct) end;
+ in (Thm.term_of ct', MetaSimplifier.rewrite true defs ct) end;
fun add_def (name, prop) =
Theory.add_defs_i false false [(name, prop)] #>
@@ -171,8 +171,8 @@
(*export assumes/defines*)
val th = Goal.norm_result raw_th;
val (defs, th') = LocalDefs.export ctxt thy_ctxt th;
- val concl_conv = Tactic.rewrite true defs (Thm.cprop_of th);
- val assms = map (Tactic.rewrite_rule defs o Thm.assume) (Assumption.assms_of ctxt);
+ val concl_conv = MetaSimplifier.rewrite true defs (Thm.cprop_of th);
+ val assms = map (MetaSimplifier.rewrite_rule defs o Thm.assume) (Assumption.assms_of ctxt);
val nprems = Thm.nprems_of th' - Thm.nprems_of th;
(*export fixes*)
--- a/src/Pure/ROOT.ML Thu Dec 07 21:44:13 2006 +0100
+++ b/src/Pure/ROOT.ML Thu Dec 07 23:16:55 2006 +0100
@@ -55,8 +55,8 @@
use "variable.ML";
use "tctical.ML";
use "search.ML";
+use "tactic.ML";
use "meta_simplifier.ML";
-use "tactic.ML";
use "conjunction.ML";
use "assumption.ML";
use "goal.ML";
--- a/src/Pure/Tools/class_package.ML Thu Dec 07 21:44:13 2006 +0100
+++ b/src/Pure/Tools/class_package.ML Thu Dec 07 23:16:55 2006 +0100
@@ -185,7 +185,7 @@
val class = loc (*FIXME*);
val thms = (#defs o fst o the_class_data thy) class;
in
- Tactic.rewrite_rule thms
+ MetaSimplifier.rewrite_rule thms
end;
--- a/src/Pure/Tools/codegen_data.ML Thu Dec 07 21:44:13 2006 +0100
+++ b/src/Pure/Tools/codegen_data.ML Thu Dec 07 23:16:55 2006 +0100
@@ -524,7 +524,7 @@
fun rewrite_func rewrites thm =
let
- val rewrite = Tactic.rewrite false rewrites;
+ val rewrite = MetaSimplifier.rewrite false rewrites;
val (ct_eq, [ct_lhs, ct_rhs]) = (Drule.strip_comb o Thm.cprop_of) thm;
val Const ("==", _) = Thm.term_of ct_eq;
val (ct_f, ct_args) = Drule.strip_comb ct_lhs;
@@ -715,7 +715,7 @@
((fn [args, rhs] => rhs :: (snd o Drule.strip_comb) args) o snd o Drule.strip_comb o Thm.cprop_of))
(fn rews => map (rewrite_func rews));
val apply_inline_proc_cterm = gen_apply_inline_proc single
- (Tactic.rewrite false);
+ (MetaSimplifier.rewrite false);
fun apply_preproc thy f [] = []
| apply_preproc thy f (thms as (thm :: _)) =
@@ -746,8 +746,10 @@
fun preprocess_cterm thy ct =
ct
|> Thm.reflexive
- |> fold (rhs_conv o Tactic.rewrite false o single) ((#inlines o the_preproc o get_exec) thy)
- |> fold (fn (_, f) => rhs_conv (apply_inline_proc_cterm thy f)) ((#inline_procs o the_preproc o get_exec) thy)
+ |> fold (rhs_conv o MetaSimplifier.rewrite false o single)
+ ((#inlines o the_preproc o get_exec) thy)
+ |> fold (fn (_, f) => rhs_conv (apply_inline_proc_cterm thy f))
+ ((#inline_procs o the_preproc o get_exec) thy)
end; (*local*)
--- a/src/Pure/Tools/nbe.ML Thu Dec 07 21:44:13 2006 +0100
+++ b/src/Pure/Tools/nbe.ML Thu Dec 07 23:16:55 2006 +0100
@@ -78,7 +78,7 @@
let
val ctxt = ProofContext.init thy;
val posts = (map (LocalDefs.meta_rewrite_rule ctxt) o snd) (NBE_Rewrite.get thy)
- in Tactic.rewrite false posts end
+ in MetaSimplifier.rewrite false posts end
(* code store *)
--- a/src/Pure/meta_simplifier.ML Thu Dec 07 21:44:13 2006 +0100
+++ b/src/Pure/meta_simplifier.ML Thu Dec 07 23:16:55 2006 +0100
@@ -72,6 +72,16 @@
val addSSolver: simpset * solver -> simpset
val setSolver: simpset * solver -> simpset
val addSolver: simpset * solver -> simpset
+
+ 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 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;
signature META_SIMPLIFIER =
@@ -94,16 +104,15 @@
val set_solvers: solver list -> simpset -> simpset
val rewrite_cterm: bool * bool * bool ->
(simpset -> thm -> thm option) -> simpset -> cterm -> thm
- val rewrite_aux: (simpset -> thm -> thm option) -> bool -> thm list -> cterm -> thm
- val simplify_aux: (simpset -> thm -> thm option) -> bool -> thm list -> thm -> thm
val rewrite_term: theory -> thm list -> (term -> term option) list -> term -> term
val rewrite_thm: bool * bool * bool ->
(simpset -> thm -> thm option) -> simpset -> thm -> thm
- val rewrite_goals_rule_aux: (simpset -> thm -> thm option) -> thm list -> thm -> thm
val rewrite_goal_rule: bool * bool * bool ->
(simpset -> thm -> thm option) -> simpset -> int -> thm -> thm
val norm_hhf: thm -> thm
val norm_hhf_protect: thm -> thm
+ val rewrite: bool -> thm list -> cterm -> thm
+ val simplify: bool -> thm list -> thm -> thm
end;
structure MetaSimplifier: META_SIMPLIFIER =
@@ -1189,18 +1198,23 @@
in dec simp_depth; res end
handle exn => (dec simp_depth; raise exn); (* FIXME avoid handling of generic exceptions *)
+val simple_prover =
+ SINGLE o (fn ss => ALLGOALS (resolve_tac (prems_of_ss ss)));
+
(*Rewrite a cterm*)
-fun rewrite_aux _ _ [] ct = Thm.reflexive ct
- | rewrite_aux prover full thms ct =
- rewrite_cterm (full, false, false) prover
- (theory_context (Thm.theory_of_cterm ct) empty_ss addsimps thms) ct;
+fun rewrite _ [] ct = Thm.reflexive ct
+ | rewrite full thms ct =
+ rewrite_cterm (full, false, false) simple_prover
+ (theory_context (Thm.theory_of_cterm ct) empty_ss addsimps thms) ct;
(*Rewrite a theorem*)
-fun simplify_aux _ _ [] th = th
- | simplify_aux prover full thms th =
- Drule.fconv_rule (rewrite_cterm (full, false, false) prover
+fun simplify _ [] th = th
+ | simplify full thms th =
+ Drule.fconv_rule (rewrite_cterm (full, false, false) simple_prover
(theory_context (Thm.theory_of_thm th) empty_ss addsimps thms)) th;
+val rewrite_rule = simplify true;
+
(*simple term rewriting -- no proof*)
fun rewrite_term thy rules procs =
Pattern.rewrite_term thy (map decomp_simp' rules) procs;
@@ -1208,8 +1222,8 @@
fun rewrite_thm mode prover ss = Drule.fconv_rule (rewrite_cterm mode prover ss);
(*Rewrite the subgoals of a proof state (represented by a theorem) *)
-fun rewrite_goals_rule_aux prover thms th =
- Drule.fconv_rule (Drule.goals_conv (K true) (rewrite_cterm (true, true, true) prover
+fun rewrite_goals_rule thms th =
+ Drule.fconv_rule (Drule.goals_conv (K true) (rewrite_cterm (true, true, true) simple_prover
(theory_context (Thm.theory_of_thm th) empty_ss addsimps thms))) th;
(*Rewrite the subgoal of a proof state (represented by a theorem)*)
@@ -1219,6 +1233,44 @@
else raise THM("rewrite_goal_rule",i,[thm]);
+(** meta-rewriting tactics **)
+
+(*Rewrite throughout proof state. *)
+fun rewrite_tac defs = PRIMITIVE(rewrite_rule defs);
+
+(*Rewrite subgoals only, not main goal. *)
+fun rewrite_goals_tac defs = PRIMITIVE (rewrite_goals_rule defs);
+fun rewtac def = rewrite_goals_tac [def];
+
+(*Prunes all redundant parameters from the proof state by rewriting.
+ DOES NOT rewrite main goal, where quantification over an unused bound
+ variable is sometimes done to avoid the need for cut_facts_tac.*)
+val prune_params_tac = rewrite_goals_tac [triv_forall_equality];
+
+
+(* for folding definitions, handling critical pairs *)
+
+(*The depth of nesting in a term*)
+fun term_depth (Abs(a,T,t)) = 1 + term_depth t
+ | term_depth (f$t) = 1 + Int.max(term_depth f, term_depth t)
+ | term_depth _ = 0;
+
+val lhs_of_thm = #1 o Logic.dest_equals o prop_of;
+
+(*folding should handle critical pairs! E.g. K == Inl(0), S == Inr(Inl(0))
+ Returns longest lhs first to avoid folding its subexpressions.*)
+fun sort_lhs_depths defs =
+ let val keylist = AList.make (term_depth o lhs_of_thm) defs
+ val keys = sort_distinct (rev_order o int_ord) (map #2 keylist)
+ in map (AList.find (op =) keylist) keys end;
+
+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));
+
+
(* HHF normal form: !! before ==>, outermost !! generalized *)
local
--- a/src/Pure/simplifier.ML Thu Dec 07 21:44:13 2006 +0100
+++ b/src/Pure/simplifier.ML Thu Dec 07 23:16:55 2006 +0100
@@ -80,6 +80,9 @@
structure Simplifier: SIMPLIFIER =
struct
+open MetaSimplifier;
+
+
(** simpset data **)
(* global simpsets *)
@@ -348,9 +351,6 @@
thy
end);
-
-open MetaSimplifier;
-
end;
structure BasicSimplifier: BASIC_SIMPLIFIER = Simplifier;
--- a/src/Pure/tactic.ML Thu Dec 07 21:44:13 2006 +0100
+++ b/src/Pure/tactic.ML Thu Dec 07 23:16:55 2006 +0100
@@ -47,9 +47,6 @@
val filter_thms : (term*term->bool) -> int*term*thm list -> thm list
val filt_resolve_tac : thm list -> int -> int -> tactic
val flexflex_tac : tactic
- val fold_goals_tac : thm list -> tactic
- val fold_rule : thm list -> thm -> thm
- val fold_tac : thm list -> tactic
val forward_tac : thm list -> int -> tactic
val forw_inst_tac : (string*string)list -> thm -> int -> tactic
val ftac : thm -> int ->tactic
@@ -69,18 +66,12 @@
val net_biresolve_tac : (bool*thm) list -> int -> tactic
val net_match_tac : thm list -> int -> tactic
val net_resolve_tac : thm list -> int -> tactic
- val prune_params_tac : tactic
val rename_params_tac : string list -> int -> tactic
val rename_tac : string -> int -> tactic
val rename_last_tac : string -> string list -> int -> tactic
val resolve_from_net_tac : (int*thm) Net.net -> int -> tactic
val resolve_tac : thm list -> int -> tactic
val res_inst_tac : (string*string)list -> thm -> int -> tactic
- val rewrite_goals_rule: thm list -> thm -> thm
- val rewrite_rule : thm list -> thm -> thm
- val rewrite_goals_tac : thm list -> tactic
- val rewrite_tac : thm list -> tactic
- val rewtac : thm -> tactic
val rotate_tac : int -> int -> tactic
val rtac : thm -> int -> tactic
val rule_by_tactic : tactic -> thm -> thm
@@ -103,8 +94,6 @@
val untaglist: (int * 'a) list -> 'a list
val eq_kbrl: ('a * (bool * thm)) * ('a * (bool * thm)) -> bool
val orderlist: (int * 'a) list -> 'a list
- val rewrite: bool -> thm list -> cterm -> thm
- val simplify: bool -> thm list -> thm -> thm
val compose_inst_tac' : (indexname * string) list -> (bool * thm * int) ->
int -> tactic
val lift_inst_rule' : thm * int * (indexname * string) list * thm -> thm
@@ -512,47 +501,6 @@
fun lessb (brl1,brl2) = subgoals_of_brl brl1 < subgoals_of_brl brl2;
-(*** Meta-Rewriting Tactics ***)
-
-val simple_prover =
- SINGLE o (fn ss => ALLGOALS (resolve_tac (MetaSimplifier.prems_of_ss ss)));
-
-val rewrite = MetaSimplifier.rewrite_aux simple_prover;
-val simplify = MetaSimplifier.simplify_aux simple_prover;
-val rewrite_rule = simplify true;
-val rewrite_goals_rule = MetaSimplifier.rewrite_goals_rule_aux simple_prover;
-
-(*Rewrite throughout proof state. *)
-fun rewrite_tac defs = PRIMITIVE(rewrite_rule defs);
-
-(*Rewrite subgoals only, not main goal. *)
-fun rewrite_goals_tac defs = PRIMITIVE (rewrite_goals_rule defs);
-fun rewtac def = rewrite_goals_tac [def];
-
-
-(*** for folding definitions, handling critical pairs ***)
-
-(*The depth of nesting in a term*)
-fun term_depth (Abs(a,T,t)) = 1 + term_depth t
- | term_depth (f$t) = 1 + Int.max(term_depth f, term_depth t)
- | term_depth _ = 0;
-
-val lhs_of_thm = #1 o Logic.dest_equals o prop_of;
-
-(*folding should handle critical pairs! E.g. K == Inl(0), S == Inr(Inl(0))
- Returns longest lhs first to avoid folding its subexpressions.*)
-fun sort_lhs_depths defs =
- let val keylist = AList.make (term_depth o lhs_of_thm) defs
- val keys = sort_distinct (rev_order o int_ord) (map #2 keylist)
- in map (AList.find (op =) keylist) keys end;
-
-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));
-
-
(*** Renaming of parameters in a subgoal
Names may contain letters, digits or primes and must be
separated by blanks ***)
@@ -582,11 +530,6 @@
else all_tac
end;
-(*Prunes all redundant parameters from the proof state by rewriting.
- DOES NOT rewrite main goal, where quantification over an unused bound
- variable is sometimes done to avoid the need for cut_facts_tac.*)
-val prune_params_tac = rewrite_goals_tac [triv_forall_equality];
-
(*rotate_tac n i: rotate the assumptions of subgoal i by n positions, from
right to left if n is positive, and from left to right if n is negative.*)
fun rotate_tac 0 i = all_tac