renamed forall_elim_vars_safe to gen_all;
authorwenzelm
Sat Jan 12 16:37:58 2002 +0100 (2002-01-12)
changeset 127257ede865e1fe5
parent 12724 beedc794bd67
child 12726 5ae4034883d5
renamed forall_elim_vars_safe to gen_all;
doc-src/Ref/simplifier.tex
src/FOL/simpdata.ML
src/HOL/simpdata.ML
src/Pure/Isar/object_logic.ML
src/Pure/drule.ML
src/Pure/tactic.ML
src/Sequents/simpdata.ML
src/ZF/Main.ML
src/ZF/OrdQuant.ML
src/ZF/Tools/inductive_package.ML
src/ZF/simpdata.ML
     1.1 --- a/doc-src/Ref/simplifier.tex	Fri Jan 11 18:49:25 2002 +0100
     1.2 +++ b/doc-src/Ref/simplifier.tex	Sat Jan 12 16:37:58 2002 +0100
     1.3 @@ -1335,7 +1335,7 @@
     1.4  automatically.  Preprocessing involves extracting atomic rewrites at the
     1.5  object-level, then reflecting them to the meta-level.
     1.6  
     1.7 -To start, the function \texttt{forall_elim_vars_safe} strips any meta-level
     1.8 +To start, the function \texttt{gen_all} strips any meta-level
     1.9  quantifiers from the front of the given theorem.
    1.10  
    1.11  The function \texttt{atomize} analyses a theorem in order to extract
    1.12 @@ -1398,7 +1398,7 @@
    1.13    | _                           => th RS iff_reflection_T;
    1.14  \end{ttbox}
    1.15  The 
    1.16 -three functions \texttt{forall_elim_vars_safe}, \texttt{atomize} and \texttt{mk_eq} 
    1.17 +three functions \texttt{gen_all}, \texttt{atomize} and \texttt{mk_eq} 
    1.18  will be composed together and supplied below to \texttt{setmksimps}.
    1.19  
    1.20  
    1.21 @@ -1427,7 +1427,7 @@
    1.22  %
    1.23  The basic simpset for intuitionistic FOL is \ttindexbold{FOL_basic_ss}.  It
    1.24  preprocess rewrites using 
    1.25 -{\tt forall_elim_vars_safe}, \texttt{atomize} and \texttt{mk_eq}.
    1.26 +{\tt gen_all}, \texttt{atomize} and \texttt{mk_eq}.
    1.27  It solves simplified subgoals using \texttt{triv_rls} and assumptions, and by
    1.28  detecting contradictions.  It uses \ttindex{asm_simp_tac} to tackle subgoals
    1.29  of conditional rewrites.
    1.30 @@ -1451,7 +1451,7 @@
    1.31                 addsimprocs [defALL_regroup, defEX_regroup]
    1.32                 setSSolver   safe_solver
    1.33                 setSolver  unsafe_solver
    1.34 -               setmksimps (map mk_eq o atomize o forall_elim_vars_safe)
    1.35 +               setmksimps (map mk_eq o atomize o gen_all)
    1.36                 setmkcong mk_meta_cong;
    1.37  
    1.38  val IFOL_ss = 
     2.1 --- a/src/FOL/simpdata.ML	Fri Jan 11 18:49:25 2002 +0100
     2.2 +++ b/src/FOL/simpdata.ML	Sat Jan 12 16:37:58 2002 +0100
     2.3 @@ -121,7 +121,7 @@
     2.4           | _ => [th])
     2.5    in atoms end;
     2.6  
     2.7 -fun mksimps pairs = (map mk_eq o mk_atomize pairs o forall_elim_vars_safe);
     2.8 +fun mksimps pairs = (map mk_eq o mk_atomize pairs o gen_all);
     2.9  
    2.10  (*** Classical laws ***)
    2.11  
     3.1 --- a/src/HOL/simpdata.ML	Fri Jan 11 18:49:25 2002 +0100
     3.2 +++ b/src/HOL/simpdata.ML	Sat Jan 12 16:37:58 2002 +0100
     3.3 @@ -221,7 +221,7 @@
     3.4    in atoms end;
     3.5  
     3.6  fun mksimps pairs =
     3.7 -  (mapfilter (try mk_eq) o mk_atomize pairs o forall_elim_vars_safe);
     3.8 +  (mapfilter (try mk_eq) o mk_atomize pairs o gen_all);
     3.9  
    3.10  fun unsafe_solver_tac prems =
    3.11    FIRST'[resolve_tac(reflexive_thm::TrueI::refl::prems), atac, etac FalseE];
     4.1 --- a/src/Pure/Isar/object_logic.ML	Fri Jan 11 18:49:25 2002 +0100
     4.2 +++ b/src/Pure/Isar/object_logic.ML	Sat Jan 12 16:37:58 2002 +0100
     4.3 @@ -139,7 +139,7 @@
     4.4  
     4.5  fun gen_rulify full thm =
     4.6    Tactic.simplify full (get_rulify (Thm.sign_of_thm thm)) thm
     4.7 -  |> Drule.forall_elim_vars_safe |> Drule.strip_shyps_warning |> Drule.zero_var_indexes;
     4.8 +  |> Drule.gen_all |> Drule.strip_shyps_warning |> Drule.zero_var_indexes;
     4.9  
    4.10  val rulify = gen_rulify true;
    4.11  val rulify_no_asm = gen_rulify false;
     5.1 --- a/src/Pure/drule.ML	Fri Jan 11 18:49:25 2002 +0100
     5.2 +++ b/src/Pure/drule.ML	Sat Jan 12 16:37:58 2002 +0100
     5.3 @@ -31,7 +31,7 @@
     5.4    val forall_elim_list  : cterm list -> thm -> thm
     5.5    val forall_elim_var   : int -> thm -> thm
     5.6    val forall_elim_vars  : int -> thm -> thm
     5.7 -  val forall_elim_vars_safe  : thm -> thm
     5.8 +  val gen_all           : thm -> thm
     5.9    val freeze_thaw       : thm -> thm * (thm -> thm)
    5.10    val implies_elim_list : thm -> thm list -> thm
    5.11    val implies_intr_list : cterm list -> thm -> thm
    5.12 @@ -315,7 +315,7 @@
    5.13  val forall_elim_var = PureThy.forall_elim_var;
    5.14  val forall_elim_vars = PureThy.forall_elim_vars;
    5.15  
    5.16 -fun forall_elim_vars_safe thm =
    5.17 +fun gen_all thm =
    5.18    let
    5.19      val {sign, prop, maxidx, ...} = Thm.rep_thm thm;
    5.20      fun elim (th, (x, T)) = Thm.forall_elim (Thm.cterm_of sign (Var ((x, maxidx + 1), T))) th;
     6.1 --- a/src/Pure/tactic.ML	Fri Jan 11 18:49:25 2002 +0100
     6.2 +++ b/src/Pure/tactic.ML	Sat Jan 12 16:37:58 2002 +0100
     6.3 @@ -524,7 +524,7 @@
     6.4  
     6.5  fun norm_hhf th =
     6.6    (if Logic.is_norm_hhf (#prop (Thm.rep_thm th)) then th else rewrite_rule [Drule.norm_hhf_eq] th)
     6.7 -  |> Drule.forall_elim_vars_safe;
     6.8 +  |> Drule.gen_all;
     6.9  
    6.10  val norm_hhf_tac = SUBGOAL (fn (t, i) =>
    6.11    if Logic.is_norm_hhf t then all_tac
     7.1 --- a/src/Sequents/simpdata.ML	Fri Jan 11 18:49:25 2002 +0100
     7.2 +++ b/src/Sequents/simpdata.ML	Sat Jan 12 16:37:58 2002 +0100
     7.3 @@ -240,7 +240,7 @@
     7.4    empty_ss setsubgoaler asm_simp_tac
     7.5      setSSolver (mk_solver "safe" safe_solver)
     7.6      setSolver (mk_solver "unsafe" unsafe_solver)
     7.7 -    setmksimps (map mk_meta_eq o atomize o forall_elim_vars_safe)
     7.8 +    setmksimps (map mk_meta_eq o atomize o gen_all)
     7.9      setmkcong mk_meta_cong;
    7.10  
    7.11  val LK_simps =
     8.1 --- a/src/ZF/Main.ML	Fri Jan 11 18:49:25 2002 +0100
     8.2 +++ b/src/ZF/Main.ML	Sat Jan 12 16:37:58 2002 +0100
     8.3 @@ -4,4 +4,4 @@
     8.4    val thy = the_context ();
     8.5  end;
     8.6  
     8.7 -simpset_ref() := simpset() setmksimps (map mk_eq o Ord_atomize o forall_elim_vars_safe);
     8.8 +simpset_ref() := simpset() setmksimps (map mk_eq o Ord_atomize o gen_all);
     9.1 --- a/src/ZF/OrdQuant.ML	Fri Jan 11 18:49:25 2002 +0100
     9.2 +++ b/src/ZF/OrdQuant.ML	Sat Jan 12 16:37:58 2002 +0100
     9.3 @@ -103,7 +103,7 @@
     9.4  
     9.5  val Ord_atomize = atomize (("OrdQuant.oall", [ospec])::ZF_conn_pairs, ZF_mem_pairs);
     9.6  
     9.7 -simpset_ref() := simpset() setmksimps (map mk_eq o Ord_atomize o forall_elim_vars_safe)
     9.8 +simpset_ref() := simpset() setmksimps (map mk_eq o Ord_atomize o gen_all)
     9.9                          addsimps [oall_simp, ltD RS beta]
    9.10                          addcongs [oall_cong, oex_cong, OUN_cong];
    9.11  
    10.1 --- a/src/ZF/Tools/inductive_package.ML	Fri Jan 11 18:49:25 2002 +0100
    10.2 +++ b/src/ZF/Tools/inductive_package.ML	Sat Jan 12 16:37:58 2002 +0100
    10.3 @@ -341,7 +341,7 @@
    10.4       (*We use a MINIMAL simpset. Even FOL_ss contains too many simpules.
    10.5         If the premises get simplified, then the proofs could fail.*)
    10.6       val min_ss = empty_ss
    10.7 -           setmksimps (map mk_eq o ZF_atomize o forall_elim_vars_safe)
    10.8 +           setmksimps (map mk_eq o ZF_atomize o gen_all)
    10.9             setSolver (mk_solver "minimal"
   10.10                        (fn prems => resolve_tac (triv_rls@prems)
   10.11                                     ORELSE' assume_tac
    11.1 --- a/src/ZF/simpdata.ML	Fri Jan 11 18:49:25 2002 +0100
    11.2 +++ b/src/ZF/simpdata.ML	Sat Jan 12 16:37:58 2002 +0100
    11.3 @@ -46,7 +46,7 @@
    11.4  val ZF_atomize = atomize (ZF_conn_pairs, ZF_mem_pairs);
    11.5  
    11.6  simpset_ref() :=
    11.7 -  simpset() setmksimps (map mk_eq o ZF_atomize o forall_elim_vars_safe)
    11.8 +  simpset() setmksimps (map mk_eq o ZF_atomize o gen_all)
    11.9    addcongs [if_weak_cong]
   11.10    addsplits [split_if]
   11.11    setSolver (mk_solver "types" (fn prems => TCSET' (fn tcset => type_solver_tac tcset prems)));