--- a/doc-src/Ref/simplifier.tex Fri Jan 11 18:49:25 2002 +0100
+++ b/doc-src/Ref/simplifier.tex Sat Jan 12 16:37:58 2002 +0100
@@ -1335,7 +1335,7 @@
automatically. Preprocessing involves extracting atomic rewrites at the
object-level, then reflecting them to the meta-level.
-To start, the function \texttt{forall_elim_vars_safe} strips any meta-level
+To start, the function \texttt{gen_all} strips any meta-level
quantifiers from the front of the given theorem.
The function \texttt{atomize} analyses a theorem in order to extract
@@ -1398,7 +1398,7 @@
| _ => th RS iff_reflection_T;
\end{ttbox}
The
-three functions \texttt{forall_elim_vars_safe}, \texttt{atomize} and \texttt{mk_eq}
+three functions \texttt{gen_all}, \texttt{atomize} and \texttt{mk_eq}
will be composed together and supplied below to \texttt{setmksimps}.
@@ -1427,7 +1427,7 @@
%
The basic simpset for intuitionistic FOL is \ttindexbold{FOL_basic_ss}. It
preprocess rewrites using
-{\tt forall_elim_vars_safe}, \texttt{atomize} and \texttt{mk_eq}.
+{\tt gen_all}, \texttt{atomize} and \texttt{mk_eq}.
It solves simplified subgoals using \texttt{triv_rls} and assumptions, and by
detecting contradictions. It uses \ttindex{asm_simp_tac} to tackle subgoals
of conditional rewrites.
@@ -1451,7 +1451,7 @@
addsimprocs [defALL_regroup, defEX_regroup]
setSSolver safe_solver
setSolver unsafe_solver
- setmksimps (map mk_eq o atomize o forall_elim_vars_safe)
+ setmksimps (map mk_eq o atomize o gen_all)
setmkcong mk_meta_cong;
val IFOL_ss =
--- a/src/FOL/simpdata.ML Fri Jan 11 18:49:25 2002 +0100
+++ b/src/FOL/simpdata.ML Sat Jan 12 16:37:58 2002 +0100
@@ -121,7 +121,7 @@
| _ => [th])
in atoms end;
-fun mksimps pairs = (map mk_eq o mk_atomize pairs o forall_elim_vars_safe);
+fun mksimps pairs = (map mk_eq o mk_atomize pairs o gen_all);
(*** Classical laws ***)
--- a/src/HOL/simpdata.ML Fri Jan 11 18:49:25 2002 +0100
+++ b/src/HOL/simpdata.ML Sat Jan 12 16:37:58 2002 +0100
@@ -221,7 +221,7 @@
in atoms end;
fun mksimps pairs =
- (mapfilter (try mk_eq) o mk_atomize pairs o forall_elim_vars_safe);
+ (mapfilter (try mk_eq) o mk_atomize pairs o gen_all);
fun unsafe_solver_tac prems =
FIRST'[resolve_tac(reflexive_thm::TrueI::refl::prems), atac, etac FalseE];
--- a/src/Pure/Isar/object_logic.ML Fri Jan 11 18:49:25 2002 +0100
+++ b/src/Pure/Isar/object_logic.ML Sat Jan 12 16:37:58 2002 +0100
@@ -139,7 +139,7 @@
fun gen_rulify full thm =
Tactic.simplify full (get_rulify (Thm.sign_of_thm thm)) thm
- |> Drule.forall_elim_vars_safe |> Drule.strip_shyps_warning |> Drule.zero_var_indexes;
+ |> Drule.gen_all |> Drule.strip_shyps_warning |> Drule.zero_var_indexes;
val rulify = gen_rulify true;
val rulify_no_asm = gen_rulify false;
--- a/src/Pure/drule.ML Fri Jan 11 18:49:25 2002 +0100
+++ b/src/Pure/drule.ML Sat Jan 12 16:37:58 2002 +0100
@@ -31,7 +31,7 @@
val forall_elim_list : cterm list -> thm -> thm
val forall_elim_var : int -> thm -> thm
val forall_elim_vars : int -> thm -> thm
- val forall_elim_vars_safe : thm -> thm
+ val gen_all : thm -> thm
val freeze_thaw : thm -> thm * (thm -> thm)
val implies_elim_list : thm -> thm list -> thm
val implies_intr_list : cterm list -> thm -> thm
@@ -315,7 +315,7 @@
val forall_elim_var = PureThy.forall_elim_var;
val forall_elim_vars = PureThy.forall_elim_vars;
-fun forall_elim_vars_safe thm =
+fun gen_all thm =
let
val {sign, prop, maxidx, ...} = Thm.rep_thm thm;
fun elim (th, (x, T)) = Thm.forall_elim (Thm.cterm_of sign (Var ((x, maxidx + 1), T))) th;
--- a/src/Pure/tactic.ML Fri Jan 11 18:49:25 2002 +0100
+++ b/src/Pure/tactic.ML Sat Jan 12 16:37:58 2002 +0100
@@ -524,7 +524,7 @@
fun norm_hhf th =
(if Logic.is_norm_hhf (#prop (Thm.rep_thm th)) then th else rewrite_rule [Drule.norm_hhf_eq] th)
- |> Drule.forall_elim_vars_safe;
+ |> Drule.gen_all;
val norm_hhf_tac = SUBGOAL (fn (t, i) =>
if Logic.is_norm_hhf t then all_tac
--- a/src/Sequents/simpdata.ML Fri Jan 11 18:49:25 2002 +0100
+++ b/src/Sequents/simpdata.ML Sat Jan 12 16:37:58 2002 +0100
@@ -240,7 +240,7 @@
empty_ss setsubgoaler asm_simp_tac
setSSolver (mk_solver "safe" safe_solver)
setSolver (mk_solver "unsafe" unsafe_solver)
- setmksimps (map mk_meta_eq o atomize o forall_elim_vars_safe)
+ setmksimps (map mk_meta_eq o atomize o gen_all)
setmkcong mk_meta_cong;
val LK_simps =
--- a/src/ZF/Main.ML Fri Jan 11 18:49:25 2002 +0100
+++ b/src/ZF/Main.ML Sat Jan 12 16:37:58 2002 +0100
@@ -4,4 +4,4 @@
val thy = the_context ();
end;
-simpset_ref() := simpset() setmksimps (map mk_eq o Ord_atomize o forall_elim_vars_safe);
+simpset_ref() := simpset() setmksimps (map mk_eq o Ord_atomize o gen_all);
--- a/src/ZF/OrdQuant.ML Fri Jan 11 18:49:25 2002 +0100
+++ b/src/ZF/OrdQuant.ML Sat Jan 12 16:37:58 2002 +0100
@@ -103,7 +103,7 @@
val Ord_atomize = atomize (("OrdQuant.oall", [ospec])::ZF_conn_pairs, ZF_mem_pairs);
-simpset_ref() := simpset() setmksimps (map mk_eq o Ord_atomize o forall_elim_vars_safe)
+simpset_ref() := simpset() setmksimps (map mk_eq o Ord_atomize o gen_all)
addsimps [oall_simp, ltD RS beta]
addcongs [oall_cong, oex_cong, OUN_cong];
--- a/src/ZF/Tools/inductive_package.ML Fri Jan 11 18:49:25 2002 +0100
+++ b/src/ZF/Tools/inductive_package.ML Sat Jan 12 16:37:58 2002 +0100
@@ -341,7 +341,7 @@
(*We use a MINIMAL simpset. Even FOL_ss contains too many simpules.
If the premises get simplified, then the proofs could fail.*)
val min_ss = empty_ss
- setmksimps (map mk_eq o ZF_atomize o forall_elim_vars_safe)
+ setmksimps (map mk_eq o ZF_atomize o gen_all)
setSolver (mk_solver "minimal"
(fn prems => resolve_tac (triv_rls@prems)
ORELSE' assume_tac
--- a/src/ZF/simpdata.ML Fri Jan 11 18:49:25 2002 +0100
+++ b/src/ZF/simpdata.ML Sat Jan 12 16:37:58 2002 +0100
@@ -46,7 +46,7 @@
val ZF_atomize = atomize (ZF_conn_pairs, ZF_mem_pairs);
simpset_ref() :=
- simpset() setmksimps (map mk_eq o ZF_atomize o forall_elim_vars_safe)
+ simpset() setmksimps (map mk_eq o ZF_atomize o gen_all)
addcongs [if_weak_cong]
addsplits [split_if]
setSolver (mk_solver "types" (fn prems => TCSET' (fn tcset => type_solver_tac tcset prems)));