--- a/src/FOL/simpdata.ML Wed Jun 29 20:39:41 2011 +0200
+++ b/src/FOL/simpdata.ML Wed Jun 29 21:34:16 2011 +0200
@@ -108,11 +108,12 @@
val triv_rls = [@{thm TrueI}, @{thm refl}, reflexive_thm, @{thm iff_refl}, @{thm notFalseI}];
-fun unsafe_solver ss = FIRST'[resolve_tac (triv_rls @ prems_of_ss ss),
- atac, etac @{thm FalseE}];
+fun unsafe_solver ss =
+ FIRST' [resolve_tac (triv_rls @ Simplifier.prems_of ss), atac, etac @{thm FalseE}];
+
(*No premature instantiation of variables during simplification*)
-fun safe_solver ss = FIRST'[match_tac (triv_rls @ prems_of_ss ss),
- eq_assume_tac, ematch_tac [@{thm FalseE}]];
+fun safe_solver ss =
+ FIRST' [match_tac (triv_rls @ Simplifier.prems_of ss), eq_assume_tac, ematch_tac @{thms FalseE}];
(*No simprules, but basic infastructure for simplification*)
val FOL_basic_ss =
--- a/src/HOL/HOL.thy Wed Jun 29 20:39:41 2011 +0200
+++ b/src/HOL/HOL.thy Wed Jun 29 21:34:16 2011 +0200
@@ -1232,7 +1232,7 @@
fun proc ss ct =
(case Thm.term_of ct of
eq $ lhs $ rhs =>
- (case find_first (is_neq eq lhs rhs) (Simplifier.prems_of_ss ss) of
+ (case find_first (is_neq eq lhs rhs) (Simplifier.prems_of ss) of
SOME thm => SOME (thm RS neq_to_EQ_False)
| NONE => NONE)
| _ => NONE);
--- a/src/HOL/Orderings.thy Wed Jun 29 20:39:41 2011 +0200
+++ b/src/HOL/Orderings.thy Wed Jun 29 21:34:16 2011 +0200
@@ -534,7 +534,7 @@
fun prp t thm = (#prop (rep_thm thm) = t);
fun prove_antisym_le sg ss ((le as Const(_,T)) $ r $ s) =
- let val prems = prems_of_ss ss;
+ let val prems = Simplifier.prems_of ss;
val less = Const (@{const_name less}, T);
val t = HOLogic.mk_Trueprop(le $ s $ r);
in case find_first (prp t) prems of
@@ -549,7 +549,7 @@
handle THM _ => NONE;
fun prove_antisym_less sg ss (NotC $ ((less as Const(_,T)) $ r $ s)) =
- let val prems = prems_of_ss ss;
+ let val prems = Simplifier.prems_of ss;
val le = Const (@{const_name less_eq}, T);
val t = HOLogic.mk_Trueprop(le $ r $ s);
in case find_first (prp t) prems of
@@ -570,7 +570,7 @@
fun add_solver name tac =
Simplifier.map_simpset_global (fn ss => ss addSolver
- mk_solver name (fn ss => tac (Simplifier.the_context ss) (prems_of_ss ss)));
+ mk_solver name (fn ss => tac (Simplifier.the_context ss) (Simplifier.prems_of ss)));
in
add_simprocs [
--- a/src/HOL/Tools/SMT/z3_proof_tools.ML Wed Jun 29 20:39:41 2011 +0200
+++ b/src/HOL/Tools/SMT/z3_proof_tools.ML Wed Jun 29 21:34:16 2011 +0200
@@ -307,7 +307,7 @@
let
val (le, r, s) = dest_binop t
val less = Const (@{const_name less}, Term.fastype_of le)
- val prems = Simplifier.prems_of_ss ss
+ val prems = Simplifier.prems_of ss
in
(case find_first (eq_prop (le $ s $ r)) prems of
NONE =>
@@ -321,7 +321,7 @@
let
val (less, r, s) = dest_binop (HOLogic.dest_not t)
val le = Const (@{const_name less_eq}, Term.fastype_of less)
- val prems = prems_of_ss ss
+ val prems = Simplifier.prems_of ss
in
(case find_first (eq_prop (le $ r $ s)) prems of
NONE =>
--- a/src/HOL/Tools/TFL/rules.ML Wed Jun 29 20:39:41 2011 +0200
+++ b/src/HOL/Tools/TFL/rules.ML Wed Jun 29 21:34:16 2011 +0200
@@ -657,7 +657,7 @@
fun prover used ss thm =
let fun cong_prover ss thm =
let val dummy = say "cong_prover:"
- val cntxt = Simplifier.prems_of_ss ss
+ val cntxt = Simplifier.prems_of ss
val dummy = print_thms "cntxt:" cntxt
val dummy = say "cong rule:"
val dummy = say (Display.string_of_thm_without_context thm)
@@ -739,7 +739,7 @@
fun restrict_prover ss thm =
let val dummy = say "restrict_prover:"
- val cntxt = rev(Simplifier.prems_of_ss ss)
+ val cntxt = rev (Simplifier.prems_of ss)
val dummy = print_thms "cntxt:" cntxt
val thy = Thm.theory_of_thm thm
val Const("==>",_) $ (Const(@{const_name Trueprop},_) $ A) $ _ = Thm.prop_of thm
--- a/src/HOL/Tools/simpdata.ML Wed Jun 29 20:39:41 2011 +0200
+++ b/src/HOL/Tools/simpdata.ML Wed Jun 29 21:34:16 2011 +0200
@@ -114,8 +114,8 @@
fun unsafe_solver_tac ss =
(fn i => REPEAT_DETERM (match_tac @{thms simp_impliesI} i)) THEN'
- FIRST' [resolve_tac (reflexive_thm :: @{thm TrueI} :: @{thm refl} :: prems_of_ss ss), atac,
- etac @{thm FalseE}];
+ FIRST' [resolve_tac (reflexive_thm :: @{thm TrueI} :: @{thm refl} :: Simplifier.prems_of ss),
+ atac, etac @{thm FalseE}];
val unsafe_solver = mk_solver "HOL unsafe" unsafe_solver_tac;
@@ -123,8 +123,8 @@
(*No premature instantiation of variables during simplification*)
fun safe_solver_tac ss =
(fn i => REPEAT_DETERM (match_tac @{thms simp_impliesI} i)) THEN'
- FIRST' [match_tac (reflexive_thm :: @{thm TrueI} :: @{thm refl} :: prems_of_ss ss),
- eq_assume_tac, ematch_tac @{thms FalseE}];
+ FIRST' [match_tac (reflexive_thm :: @{thm TrueI} :: @{thm refl} :: Simplifier.prems_of ss),
+ eq_assume_tac, ematch_tac @{thms FalseE}];
val safe_solver = mk_solver "HOL safe" safe_solver_tac;
--- a/src/Provers/Arith/cancel_numeral_factor.ML Wed Jun 29 20:39:41 2011 +0200
+++ b/src/Provers/Arith/cancel_numeral_factor.ML Wed Jun 29 21:34:16 2011 +0200
@@ -47,7 +47,7 @@
fun proc ss t =
let
val ctxt = Simplifier.the_context ss;
- val prems = prems_of_ss ss;
+ val prems = Simplifier.prems_of ss;
val ([t'], ctxt') = Variable.import_terms true [t] ctxt
val export = singleton (Variable.export ctxt' ctxt)
--- a/src/Provers/Arith/cancel_numerals.ML Wed Jun 29 20:39:41 2011 +0200
+++ b/src/Provers/Arith/cancel_numerals.ML Wed Jun 29 21:34:16 2011 +0200
@@ -68,7 +68,7 @@
fun proc ss t =
let
val ctxt = Simplifier.the_context ss
- val prems = prems_of_ss ss
+ val prems = Simplifier.prems_of ss
val ([t'], ctxt') = Variable.import_terms true [t] ctxt
val export = singleton (Variable.export ctxt' ctxt)
--- a/src/Provers/Arith/extract_common_term.ML Wed Jun 29 20:39:41 2011 +0200
+++ b/src/Provers/Arith/extract_common_term.ML Wed Jun 29 21:34:16 2011 +0200
@@ -49,7 +49,7 @@
fun proc ss t =
let
val ctxt = Simplifier.the_context ss;
- val prems = prems_of_ss ss;
+ val prems = Simplifier.prems_of ss;
val ([t'], ctxt') = Variable.import_terms true [t] ctxt
val export = singleton (Variable.export ctxt' ctxt)
--- a/src/Provers/Arith/fast_lin_arith.ML Wed Jun 29 20:39:41 2011 +0200
+++ b/src/Provers/Arith/fast_lin_arith.ML Wed Jun 29 21:34:16 2011 +0200
@@ -835,7 +835,7 @@
end);
fun cut_lin_arith_tac ss =
- cut_facts_tac (Simplifier.prems_of_ss ss) THEN'
+ cut_facts_tac (Simplifier.prems_of ss) THEN'
simpset_lin_arith_tac ss false;
fun lin_arith_tac ctxt =
@@ -916,7 +916,7 @@
fun lin_arith_simproc ss concl =
let
val ctxt = Simplifier.the_context ss
- val thms = maps LA_Logic.atomize (Simplifier.prems_of_ss ss)
+ val thms = maps LA_Logic.atomize (Simplifier.prems_of ss)
val Hs = map Thm.prop_of thms
val Tconcl = LA_Logic.mk_Trueprop concl
in
--- a/src/Pure/raw_simplifier.ML Wed Jun 29 20:39:41 2011 +0200
+++ b/src/Pure/raw_simplifier.ML Wed Jun 29 21:34:16 2011 +0200
@@ -37,7 +37,6 @@
val make_simproc: {name: string, lhss: cterm list,
proc: morphism -> simpset -> cterm -> thm option, identifier: thm list} -> simproc
val mk_simproc: string -> cterm list -> (theory -> simpset -> term -> thm option) -> simproc
- val prems_of_ss: simpset -> thm list
val addsimps: simpset * thm list -> simpset
val delsimps: simpset * thm list -> simpset
val addeqcongs: simpset * thm list -> simpset
@@ -97,6 +96,7 @@
subgoal_tac: simpset -> int -> tactic,
loop_tacs: (string * (simpset -> int -> tactic)) list,
solvers: solver list * solver list}
+ val prems_of: simpset -> thm list
val add_simp: thm -> simpset -> simpset
val del_simp: thm -> simpset -> simpset
val solver: simpset -> solver -> int -> tactic
@@ -235,7 +235,7 @@
fun map_simpset1 f (Simpset (r1, r2)) = Simpset (map_ss1 f r1, r2);
fun map_simpset2 f (Simpset (r1, r2)) = Simpset (r1, map_ss2 f r2);
-fun prems_of_ss (Simpset ({prems, ...}, _)) = prems;
+fun prems_of (Simpset ({prems, ...}, _)) = prems;
fun eq_procid ((s1: stamp, ths1: thm list), (s2, ths2)) =
s1 = s2 andalso eq_list Thm.eq_thm (ths1, ths2);
@@ -562,7 +562,7 @@
fun is_full_cong thm =
let
- val prems = prems_of thm and concl = concl_of thm;
+ val prems = Thm.prems_of thm and concl = Thm.concl_of thm;
val (lhs, rhs) = Logic.dest_equals concl;
val (f, xs) = strip_comb lhs and (g, ys) = strip_comb rhs;
in
@@ -1278,7 +1278,7 @@
in bottomc (mode, Option.map Drule.flexflex_unique oo prover, thy, maxidx) ss ct end;
val simple_prover =
- SINGLE o (fn ss => ALLGOALS (resolve_tac (prems_of_ss ss)));
+ SINGLE o (fn ss => ALLGOALS (resolve_tac (prems_of ss)));
fun rewrite _ [] ct = Thm.reflexive ct
| rewrite full thms ct = rewrite_cterm (full, false, false) simple_prover
--- a/src/Pure/simplifier.ML Wed Jun 29 20:39:41 2011 +0200
+++ b/src/Pure/simplifier.ML Wed Jun 29 21:34:16 2011 +0200
@@ -34,6 +34,7 @@
val pretty_ss: Proof.context -> simpset -> Pretty.T
val clear_ss: simpset -> simpset
val debug_bounds: bool Unsynchronized.ref
+ val prems_of: simpset -> thm list
val add_simp: thm -> simpset -> simpset
val del_simp: thm -> simpset -> simpset
val add_prems: thm list -> simpset -> simpset
@@ -396,11 +397,13 @@
let
val trivialities = Drule.reflexive_thm :: trivs;
- fun unsafe_solver_tac ss = FIRST' [resolve_tac (trivialities @ prems_of_ss ss), assume_tac];
+ fun unsafe_solver_tac ss =
+ FIRST' [resolve_tac (trivialities @ Raw_Simplifier.prems_of ss), assume_tac];
val unsafe_solver = mk_solver "easy unsafe" unsafe_solver_tac;
(*no premature instantiation of variables during simplification*)
- fun safe_solver_tac ss = FIRST' [match_tac (trivialities @ prems_of_ss ss), eq_assume_tac];
+ fun safe_solver_tac ss =
+ FIRST' [match_tac (trivialities @ Raw_Simplifier.prems_of ss), eq_assume_tac];
val safe_solver = mk_solver "easy safe" safe_solver_tac;
fun mk_eq thm =
--- a/src/Sequents/simpdata.ML Wed Jun 29 20:39:41 2011 +0200
+++ b/src/Sequents/simpdata.ML Wed Jun 29 21:34:16 2011 +0200
@@ -59,11 +59,11 @@
@{thm iff_refl}, reflexive_thm];
fun unsafe_solver ss =
- FIRST' [resolve_tac (triv_rls @ prems_of_ss ss), assume_tac];
+ FIRST' [resolve_tac (triv_rls @ Simplifier.prems_of ss), assume_tac];
(*No premature instantiation of variables during simplification*)
fun safe_solver ss =
- FIRST' [fn i => DETERM (match_tac (triv_rls @ prems_of_ss ss) i), eq_assume_tac];
+ FIRST' [fn i => DETERM (match_tac (triv_rls @ Simplifier.prems_of ss) i), eq_assume_tac];
(*No simprules, but basic infrastructure for simplification*)
val LK_basic_ss =
--- a/src/ZF/Tools/inductive_package.ML Wed Jun 29 20:39:41 2011 +0200
+++ b/src/ZF/Tools/inductive_package.ML Wed Jun 29 21:34:16 2011 +0200
@@ -329,7 +329,7 @@
val min_ss = Simplifier.global_context thy empty_ss
setmksimps (K (map mk_eq o ZF_atomize o gen_all))
setSolver (mk_solver "minimal"
- (fn ss => resolve_tac (triv_rls @ prems_of_ss ss)
+ (fn ss => resolve_tac (triv_rls @ Simplifier.prems_of ss)
ORELSE' assume_tac
ORELSE' etac @{thm FalseE}));
--- a/src/ZF/Tools/typechk.ML Wed Jun 29 20:39:41 2011 +0200
+++ b/src/ZF/Tools/typechk.ML Wed Jun 29 21:34:16 2011 +0200
@@ -107,7 +107,7 @@
val type_solver =
Simplifier.mk_solver "ZF typecheck" (fn ss =>
- type_solver_tac (Simplifier.the_context ss) (prems_of_ss ss));
+ type_solver_tac (Simplifier.the_context ss) (Simplifier.prems_of ss));
(* concrete syntax *)