--- a/src/HOL/Statespace/distinct_tree_prover.ML Thu Jan 01 22:57:42 2009 +0100
+++ b/src/HOL/Statespace/distinct_tree_prover.ML Thu Jan 01 23:31:49 2009 +0100
@@ -5,23 +5,20 @@
signature DISTINCT_TREE_PROVER =
sig
datatype Direction = Left | Right
- val mk_tree : ('a -> Term.term) -> Term.typ -> 'a list -> Term.term
- val dest_tree : Term.term -> Term.term list
- val find_tree :
- Term.term -> Term.term -> Direction list option
+ val mk_tree : ('a -> term) -> typ -> 'a list -> term
+ val dest_tree : term -> term list
+ val find_tree : term -> term -> Direction list option
- val neq_to_eq_False : Thm.thm
- val distinctTreeProver : Thm.thm -> Direction list -> Direction list -> Thm.thm
- val neq_x_y :
- Proof.context -> Term.term -> Term.term -> string -> Thm.thm option
- val distinctFieldSolver : string list -> MetaSimplifier.solver
- val distinctTree_tac :
- string list -> Proof.context -> Term.term * int -> Tactical.tactic
- val distinct_implProver : Thm.thm -> Thm.cterm -> Thm.thm
- val subtractProver : Term.term -> Thm.cterm -> Thm.thm -> Thm.thm
- val distinct_simproc : string list -> MetaSimplifier.simproc
+ val neq_to_eq_False : thm
+ val distinctTreeProver : thm -> Direction list -> Direction list -> thm
+ val neq_x_y : Proof.context -> term -> term -> string -> thm option
+ val distinctFieldSolver : string list -> solver
+ val distinctTree_tac : string list -> Proof.context -> term * int -> tactic
+ val distinct_implProver : thm -> cterm -> thm
+ val subtractProver : term -> cterm -> thm -> thm
+ val distinct_simproc : string list -> simproc
- val discharge : Thm.thm list -> Thm.thm -> Thm.thm
+ val discharge : thm list -> thm -> thm
end;
structure DistinctTreeProver : DISTINCT_TREE_PROVER =
--- a/src/HOL/Statespace/state_fun.ML Thu Jan 01 22:57:42 2009 +0100
+++ b/src/HOL/Statespace/state_fun.ML Thu Jan 01 23:31:49 2009 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/Statespace/state_fun.ML
- ID: $Id$
Author: Norbert Schirmer, TU Muenchen
*)
@@ -8,17 +7,17 @@
val lookupN : string
val updateN : string
- val mk_constr : Context.theory -> Term.typ -> Term.term
- val mk_destr : Context.theory -> Term.typ -> Term.term
+ val mk_constr : theory -> typ -> term
+ val mk_destr : theory -> typ -> term
- val lookup_simproc : MetaSimplifier.simproc
- val update_simproc : MetaSimplifier.simproc
- val ex_lookup_eq_simproc : MetaSimplifier.simproc
- val ex_lookup_ss : MetaSimplifier.simpset
- val lazy_conj_simproc : MetaSimplifier.simproc
- val string_eq_simp_tac : int -> Tactical.tactic
+ val lookup_simproc : simproc
+ val update_simproc : simproc
+ val ex_lookup_eq_simproc : simproc
+ val ex_lookup_ss : simpset
+ val lazy_conj_simproc : simproc
+ val string_eq_simp_tac : int -> tactic
- val setup : Context.theory -> Context.theory
+ val setup : theory -> theory
end;
structure StateFun: STATE_FUN =
--- a/src/HOL/Tools/TFL/rules.ML Thu Jan 01 22:57:42 2009 +0100
+++ b/src/HOL/Tools/TFL/rules.ML Thu Jan 01 23:31:49 2009 +0100
@@ -674,7 +674,7 @@
fun prover used ss thm =
let fun cong_prover ss thm =
let val dummy = say "cong_prover:"
- val cntxt = MetaSimplifier.prems_of_ss ss
+ val cntxt = Simplifier.prems_of_ss ss
val dummy = print_thms "cntxt:" cntxt
val dummy = say "cong rule:"
val dummy = say (Display.string_of_thm thm)
@@ -687,7 +687,7 @@
val ants = map tych (Logic.strip_imp_prems imp)
val eq = Logic.strip_imp_concl imp
val lhs = tych(get_lhs eq)
- val ss' = MetaSimplifier.add_prems (map ASSUME ants) ss
+ val ss' = Simplifier.add_prems (map ASSUME ants) ss
val lhs_eq_lhs1 = MetaSimplifier.rewrite_cterm (false,true,false) (prover used) ss' lhs
handle U.ERR _ => Thm.reflexive lhs
val dummy = print_thms "proven:" [lhs_eq_lhs1]
@@ -708,7 +708,7 @@
val Q = get_lhs eq1
val QeqQ1 = pbeta_reduce (tych Q)
val Q1 = #2(D.dest_eq(cconcl QeqQ1))
- val ss' = MetaSimplifier.add_prems (map ASSUME ants1) ss
+ val ss' = Simplifier.add_prems (map ASSUME ants1) ss
val Q1eeqQ2 = MetaSimplifier.rewrite_cterm (false,true,false) (prover used') ss' Q1
handle U.ERR _ => Thm.reflexive Q1
val Q2 = #2 (Logic.dest_equals (Thm.prop_of Q1eeqQ2))
@@ -758,7 +758,7 @@
fun restrict_prover ss thm =
let val dummy = say "restrict_prover:"
- val cntxt = rev(MetaSimplifier.prems_of_ss ss)
+ val cntxt = rev(Simplifier.prems_of_ss ss)
val dummy = print_thms "cntxt:" cntxt
val thy = Thm.theory_of_thm thm
val Const("==>",_) $ (Const("Trueprop",_) $ A) $ _ = Thm.prop_of thm
--- a/src/HOL/Tools/arith_data.ML Thu Jan 01 22:57:42 2009 +0100
+++ b/src/HOL/Tools/arith_data.ML Thu Jan 01 23:31:49 2009 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/arith_data.ML
- ID: $Id$
Author: Markus Wenzel, Stefan Berghofer, and Tobias Nipkow
Basic arithmetic proof tools.
@@ -7,9 +6,8 @@
signature ARITH_DATA =
sig
- val prove_conv: tactic -> (MetaSimplifier.simpset -> tactic)
- -> MetaSimplifier.simpset -> term * term -> thm
- val simp_all_tac: thm list -> MetaSimplifier.simpset -> tactic
+ val prove_conv: tactic -> (simpset -> tactic) -> simpset -> term * term -> thm
+ val simp_all_tac: thm list -> simpset -> tactic
val mk_sum: term list -> term
val mk_norm_sum: term list -> term
--- a/src/HOL/Tools/datatype_codegen.ML Thu Jan 01 22:57:42 2009 +0100
+++ b/src/HOL/Tools/datatype_codegen.ML Thu Jan 01 23:31:49 2009 +0100
@@ -413,7 +413,7 @@
val inject2 = (#inject o DatatypePackage.the_datatype thy) dtco;
val ctxt = ProofContext.init thy;
val simpset = Simplifier.context ctxt
- (MetaSimplifier.empty_ss addsimprocs [DatatypePackage.distinct_simproc]);
+ (Simplifier.empty_ss addsimprocs [DatatypePackage.distinct_simproc]);
val cos = map (fn (co, tys) =>
(Const (co, tys ---> Type (dtco, map TFree vs)), tys)) cs;
val tac = ALLGOALS (simp_tac simpset)
--- a/src/HOL/Tools/function_package/fundef_lib.ML Thu Jan 01 22:57:42 2009 +0100
+++ b/src/HOL/Tools/function_package/fundef_lib.ML Thu Jan 01 23:31:49 2009 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/Tools/function_package/fundef_lib.ML
- ID: $Id$
Author: Alexander Krauss, TU Muenchen
A package for general recursive function definitions.
@@ -163,7 +162,7 @@
else if js = []
then mk (foldr1 mk (map (nth xs) is), Const (neu, ty))
else mk (foldr1 mk (map (nth xs) is), foldr1 mk (map (nth xs) js)))))
- (K (MetaSimplifier.rewrite_goals_tac ac
+ (K (rewrite_goals_tac ac
THEN rtac Drule.reflexive_thm 1))
end
--- a/src/Pure/Isar/code.ML Thu Jan 01 22:57:42 2009 +0100
+++ b/src/Pure/Isar/code.ML Thu Jan 01 23:31:49 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/Isar/code.ML
- ID: $Id$
Author: Florian Haftmann, TU Muenchen
Abstract executable content of theory. Management of data dependent on
@@ -16,8 +15,8 @@
val del_eqn: thm -> theory -> theory
val del_eqns: string -> theory -> theory
val add_eqnl: string * (thm * bool) list lazy -> theory -> theory
- val map_pre: (MetaSimplifier.simpset -> MetaSimplifier.simpset) -> theory -> theory
- val map_post: (MetaSimplifier.simpset -> MetaSimplifier.simpset) -> theory -> theory
+ val map_pre: (simpset -> simpset) -> theory -> theory
+ val map_post: (simpset -> simpset) -> theory -> theory
val add_inline: thm -> theory -> theory
val add_functrans: string * (theory -> (thm * bool) list -> (thm * bool) list option) -> theory -> theory
val del_functrans: string -> theory -> theory
@@ -186,8 +185,8 @@
(* pre- and postprocessor *)
datatype thmproc = Thmproc of {
- pre: MetaSimplifier.simpset,
- post: MetaSimplifier.simpset,
+ pre: simpset,
+ post: simpset,
functrans: (string * (serial * (theory -> (thm * bool) list -> (thm * bool) list option))) list
};
@@ -198,8 +197,8 @@
fun merge_thmproc (Thmproc { pre = pre1, post = post1, functrans = functrans1 },
Thmproc { pre = pre2, post = post2, functrans = functrans2 }) =
let
- val pre = MetaSimplifier.merge_ss (pre1, pre2);
- val post = MetaSimplifier.merge_ss (post1, post2);
+ val pre = Simplifier.merge_ss (pre1, pre2);
+ val post = Simplifier.merge_ss (post1, post2);
val functrans = AList.merge (op =) (eq_fst (op =)) (functrans1, functrans2);
in mk_thmproc ((pre, post), functrans) end;
@@ -221,7 +220,7 @@
val thmproc = merge_thmproc (thmproc1, thmproc2);
val spec = merge_spec (spec1, spec2);
in mk_exec (thmproc, spec) end;
-val empty_exec = mk_exec (mk_thmproc ((MetaSimplifier.empty_ss, MetaSimplifier.empty_ss), []),
+val empty_exec = mk_exec (mk_thmproc ((Simplifier.empty_ss, Simplifier.empty_ss), []),
mk_spec ((false, Symtab.empty), (Symtab.empty, (Symtab.empty, Symtab.empty))));
fun the_thmproc (Exec { thmproc = Thmproc x, ...}) = x;
@@ -417,12 +416,12 @@
Pretty.block [
Pretty.str "preprocessing simpset:",
Pretty.fbrk,
- MetaSimplifier.pretty_ss pre
+ Simplifier.pretty_ss pre
],
Pretty.block [
Pretty.str "postprocessing simpset:",
Pretty.fbrk,
- MetaSimplifier.pretty_ss post
+ Simplifier.pretty_ss post
],
Pretty.block (
Pretty.str "function transformers:"
--- a/src/Pure/Isar/find_theorems.ML Thu Jan 01 22:57:42 2009 +0100
+++ b/src/Pure/Isar/find_theorems.ML Thu Jan 01 23:31:49 2009 +0100
@@ -165,7 +165,7 @@
fun filter_simp ctxt t (_, thm) =
let
val (_, {mk_rews = {mk, ...}, ...}) =
- MetaSimplifier.rep_ss (Simplifier.local_simpset_of ctxt);
+ Simplifier.rep_ss (Simplifier.local_simpset_of ctxt);
val extract_simp =
(map Thm.full_prop_of o mk, #1 o Logic.dest_equals o Logic.strip_imp_concl);
val ss = is_matching_thm extract_simp ctxt false t thm
--- a/src/ZF/Tools/inductive_package.ML Thu Jan 01 22:57:42 2009 +0100
+++ b/src/ZF/Tools/inductive_package.ML Thu Jan 01 23:31:49 2009 +0100
@@ -249,7 +249,7 @@
|> ListPair.map (fn (t, tacs) =>
Goal.prove_global thy1 [] [] t
(fn _ => EVERY (rewrite_goals_tac part_rec_defs :: tacs)))
- handle MetaSimplifier.SIMPLIFIER (msg, thm) => (Display.print_thm thm; error msg);
+ handle Simplifier.SIMPLIFIER (msg, thm) => (Display.print_thm thm; error msg);
(********)
val dummy = writeln " Proving the elimination rule...";