# HG changeset patch # User wenzelm # Date 1116773467 -7200 # Node ID 0e1405402d53a8ede88857158a3824ac8352a424 # Parent 3e4e077af2e783dd9e4b3915eaf1cd0c9a69d2ae Simplifier already setup in Pure; diff -r 3e4e077af2e7 -r 0e1405402d53 doc-src/Ref/simplifier.tex --- a/doc-src/Ref/simplifier.tex Sun May 22 16:51:06 2005 +0200 +++ b/doc-src/Ref/simplifier.tex Sun May 22 16:51:07 2005 +0200 @@ -1224,12 +1224,10 @@ first-order logic; the code is largely taken from {\tt FOL/simpdata.ML} of the Isabelle sources. -The simplifier and the case splitting tactic, which reside on separate files, -are not part of Pure Isabelle. They must be loaded explicitly by the -object-logic as follows (below \texttt{\~\relax\~\relax} refers to -\texttt{\$ISABELLE_HOME}): +The case splitting tactic, which resides on a separate files, is not part of +Pure Isabelle. It needs to be loaded explicitly by the object-logic as +follows (below \texttt{\~\relax\~\relax} refers to \texttt{\$ISABELLE_HOME}): \begin{ttbox} -use "\~\relax\~\relax/src/Provers/simplifier.ML"; use "\~\relax\~\relax/src/Provers/splitter.ML"; \end{ttbox} @@ -1461,23 +1459,6 @@ \end{ttbox} -\subsection{Theory setup}\index{simplification!setting up the theory} -\begin{ttbox}\indexbold{*Simplifier.setup}\index{*setup!simplifier} -Simplifier.setup: (theory -> theory) list -\end{ttbox} - -Advanced theory related features of the simplifier (e.g.\ implicit -simpset support) have to be set up explicitly. The simplifier already -provides a suitable setup function definition. This has to be -installed into the base theory of any new object-logic via a -\texttt{setup} declaration. - -For example, this is done in \texttt{FOL/IFOL.thy} as follows: -\begin{ttbox} -setup Simplifier.setup -\end{ttbox} - - \index{simplification|)} diff -r 3e4e077af2e7 -r 0e1405402d53 src/FOL/IFOL.thy --- a/src/FOL/IFOL.thy Sun May 22 16:51:06 2005 +0200 +++ b/src/FOL/IFOL.thy Sun May 22 16:51:07 2005 +0200 @@ -140,7 +140,6 @@ subsection {* Lemmas and proof tools *} -setup Simplifier.setup use "IFOL_lemmas.ML" use "fologic.ML" diff -r 3e4e077af2e7 -r 0e1405402d53 src/FOL/IsaMakefile --- a/src/FOL/IsaMakefile Sun May 22 16:51:06 2005 +0200 +++ b/src/FOL/IsaMakefile Sun May 22 16:51:07 2005 +0200 @@ -28,15 +28,15 @@ $(OUT)/Pure: Pure -$(OUT)/FOL: $(OUT)/Pure $(SRC)/Provers/blast.ML $(SRC)/Provers/make_elim.ML \ - $(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML \ - $(SRC)/Provers/hypsubst.ML $(SRC)/Provers/ind.ML $(SRC)/Provers/induct_method.ML \ - $(SRC)/Provers/simplifier.ML $(SRC)/Provers/splitter.ML $(SRC)/Provers/quantifier1.ML\ - $(SRC)/Provers/eqsubst.ML\ - eqrule_FOL_data.ML\ - FOL.ML FOL.thy FOL_lemmas1.ML IFOL.ML IFOL.thy \ - IFOL_lemmas.ML ROOT.ML blastdata.ML cladata.ML document/root.tex \ - fologic.ML hypsubstdata.ML intprover.ML simpdata.ML +$(OUT)/FOL: $(OUT)/Pure $(SRC)/Provers/blast.ML \ + $(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML \ + $(SRC)/Provers/eqsubst.ML $(SRC)/Provers/hypsubst.ML \ + $(SRC)/Provers/ind.ML $(SRC)/Provers/induct_method.ML \ + $(SRC)/Provers/make_elim.ML $(SRC)/Provers/quantifier1.ML \ + $(SRC)/Provers/splitter.ML FOL.ML FOL.thy FOL_lemmas1.ML IFOL.ML \ + IFOL.thy IFOL_lemmas.ML ROOT.ML blastdata.ML cladata.ML \ + document/root.tex eqrule_FOL_data.ML fologic.ML hypsubstdata.ML \ + intprover.ML simpdata.ML @$(ISATOOL) usedir -b $(OUT)/Pure FOL diff -r 3e4e077af2e7 -r 0e1405402d53 src/FOL/ROOT.ML --- a/src/FOL/ROOT.ML Sun May 22 16:51:06 2005 +0200 +++ b/src/FOL/ROOT.ML Sun May 22 16:51:07 2005 +0200 @@ -10,7 +10,6 @@ print_depth 1; -use "~~/src/Provers/simplifier.ML"; use "~~/src/Provers/splitter.ML"; use "~~/src/Provers/ind.ML"; use "~~/src/Provers/hypsubst.ML"; diff -r 3e4e077af2e7 -r 0e1405402d53 src/FOL/simpdata.ML --- a/src/FOL/simpdata.ML Sun May 22 16:51:06 2005 +0200 +++ b/src/FOL/simpdata.ML Sun May 22 16:51:07 2005 +0200 @@ -105,10 +105,10 @@ [("op -->", [mp]), ("op &", [conjunct1,conjunct2]), ("All", [spec]), ("True", []), ("False", [])]; -(* ###FIXME: move to Provers/simplifier.ML +(* ###FIXME: move to simplifier.ML val mk_atomize: (string * thm list) list -> thm -> thm list *) -(* ###FIXME: move to Provers/simplifier.ML *) +(* ###FIXME: move to simplifier.ML *) fun mk_atomize pairs = let fun atoms th = (case concl_of th of diff -r 3e4e077af2e7 -r 0e1405402d53 src/HOL/HOL.thy --- a/src/HOL/HOL.thy Sun May 22 16:51:06 2005 +0200 +++ b/src/HOL/HOL.thy Sun May 22 16:51:07 2005 +0200 @@ -1124,7 +1124,6 @@ subsubsection {* Actual Installation of the Simplifier *} use "simpdata.ML" -setup Simplifier.setup setup "Simplifier.method_setup Splitter.split_modifiers" setup simpsetup setup Splitter.setup setup Clasimp.setup diff -r 3e4e077af2e7 -r 0e1405402d53 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Sun May 22 16:51:06 2005 +0200 +++ b/src/HOL/IsaMakefile Sun May 22 16:51:07 2005 +0200 @@ -61,64 +61,59 @@ Pure: @cd $(SRC)/Pure; $(ISATOOL) make Pure -$(OUT)/HOL: $(OUT)/Pure $(SRC)/Provers/quantifier1.ML \ - $(SRC)/Provers/Arith/abel_cancel.ML \ - $(SRC)/Provers/Arith/assoc_fold.ML \ - $(SRC)/Provers/Arith/cancel_numerals.ML \ - $(SRC)/Provers/Arith/cancel_sums.ML \ - $(SRC)/Provers/Arith/combine_numerals.ML \ - $(SRC)/Provers/Arith/cancel_numeral_factor.ML \ - $(SRC)/Provers/Arith/extract_common_term.ML \ - $(SRC)/Provers/Arith/cancel_div_mod.ML \ - $(SRC)/Provers/Arith/fast_lin_arith.ML $(SRC)/Provers/blast.ML \ - $(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML \ - $(SRC)/Provers/hypsubst.ML $(SRC)/Provers/induct_method.ML \ - $(SRC)/Provers/make_elim.ML $(SRC)/Provers/order.ML $(SRC)/Provers/quasi.ML\ - $(SRC)/Provers/simplifier.ML $(SRC)/Provers/splitter.ML \ - $(SRC)/Provers/trancl.ML \ - $(SRC)/TFL/casesplit.ML \ - $(SRC)/TFL/dcterm.ML $(SRC)/TFL/post.ML $(SRC)/TFL/rules.ML \ - $(SRC)/TFL/tfl.ML $(SRC)/TFL/thms.ML $(SRC)/TFL/thry.ML \ - $(SRC)/TFL/usyntax.ML $(SRC)/TFL/utils.ML \ - $(SRC)/Provers/eqsubst.ML\ - eqrule_HOL_data.ML\ - Datatype.ML Datatype.thy Datatype_Universe.thy \ - Divides.thy Equiv_Relations.thy Extraction.thy Finite_Set.ML Finite_Set.thy \ - Fun.thy Gfp.thy Hilbert_Choice.thy HOL.ML \ - HOL.thy Inductive.thy Infinite_Set.thy Integ/Numeral.thy \ - Integ/cooper_dec.ML Integ/cooper_proof.ML \ - Integ/IntArith.thy Integ/IntDef.thy \ - Integ/IntDiv.thy Integ/NatBin.thy Integ/NatSimprocs.thy Integ/Parity.thy \ - Integ/int_arith1.ML Integ/int_factor_simprocs.ML Integ/nat_simprocs.ML \ - Integ/Presburger.thy Integ/presburger.ML Integ/qelim.ML \ - Lattice_Locales.thy Lfp.thy List.ML List.thy Main.ML Main.thy Map.thy\ - Nat.ML Nat.thy NatArith.thy Power.thy PreList.thy Product_Type.thy \ - Refute.thy ROOT.ML \ - Recdef.thy Reconstruction.thy Record.thy Relation.ML Relation.thy \ - Relation_Power.thy LOrder.thy OrderedGroup.thy OrderedGroup.ML \ - Orderings.ML Orderings.thy Ring_and_Field.thy\ - Set.ML Set.thy SetInterval.thy \ - Sum_Type.thy Tools/datatype_abs_proofs.ML Tools/datatype_aux.ML \ - Tools/datatype_codegen.ML Tools/datatype_package.ML Tools/datatype_prop.ML \ - Tools/datatype_realizer.ML Tools/datatype_rep_proofs.ML \ - Tools/inductive_codegen.ML Tools/inductive_package.ML Tools/inductive_realizer.ML \ - Tools/meson.ML Tools/numeral_syntax.ML \ - Tools/primrec_package.ML Tools/prop_logic.ML \ - Tools/recdef_package.ML Tools/recfun_codegen.ML Tools/record_package.ML \ - Tools/reconstruction.ML Tools/refute.ML Tools/refute_isar.ML \ - Tools/rewrite_hol_proof.ML Tools/sat_solver.ML Tools/specification_package.ML \ - Tools/split_rule.ML Tools/typedef_package.ML \ - Transitive_Closure.thy Transitive_Closure.ML Typedef.thy \ - Wellfounded_Recursion.thy Wellfounded_Relations.thy arith_data.ML antisym_setup.ML \ - blastdata.ML cladata.ML \ - Tools/res_lib.ML Tools/res_clause.ML Tools/res_skolem_function.ML\ - Tools/res_axioms.ML Tools/res_types_sorts.ML \ - Tools/ATP/recon_prelim.ML Tools/ATP/recon_order_clauses.ML\ - Tools/ATP/recon_translate_proof.ML Tools/ATP/recon_parse.ML \ - Tools/ATP/recon_transfer_proof.ML Tools/ATP/res_clasimpset.ML \ - Tools/ATP/VampireCommunication.ML Tools/ATP/SpassCommunication.ML Tools/ATP/modUnix.ML \ - Tools/ATP/watcher.sig Tools/ATP/watcher.ML Tools/res_atp.ML\ - document/root.tex hologic.ML simpdata.ML thy_syntax.ML +$(OUT)/HOL: $(OUT)/Pure $(SRC)/Provers/Arith/abel_cancel.ML \ + $(SRC)/Provers/Arith/assoc_fold.ML \ + $(SRC)/Provers/Arith/cancel_div_mod.ML \ + $(SRC)/Provers/Arith/cancel_numeral_factor.ML \ + $(SRC)/Provers/Arith/cancel_numerals.ML \ + $(SRC)/Provers/Arith/cancel_sums.ML \ + $(SRC)/Provers/Arith/combine_numerals.ML \ + $(SRC)/Provers/Arith/extract_common_term.ML \ + $(SRC)/Provers/Arith/fast_lin_arith.ML $(SRC)/Provers/blast.ML \ + $(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML \ + $(SRC)/Provers/eqsubst.ML $(SRC)/Provers/hypsubst.ML \ + $(SRC)/Provers/induct_method.ML $(SRC)/Provers/make_elim.ML \ + $(SRC)/Provers/order.ML $(SRC)/Provers/quantifier1.ML \ + $(SRC)/Provers/quasi.ML $(SRC)/Provers/splitter.ML $(SRC)/Provers/trancl.ML \ + $(SRC)/TFL/casesplit.ML $(SRC)/TFL/dcterm.ML $(SRC)/TFL/post.ML \ + $(SRC)/TFL/rules.ML $(SRC)/TFL/tfl.ML $(SRC)/TFL/thms.ML \ + $(SRC)/TFL/thry.ML $(SRC)/TFL/usyntax.ML $(SRC)/TFL/utils.ML \ + Datatype.ML Datatype.thy Datatype_Universe.thy Divides.thy \ + Equiv_Relations.thy Extraction.thy Finite_Set.ML Finite_Set.thy \ + Fun.thy Gfp.thy HOL.ML HOL.thy Hilbert_Choice.thy Inductive.thy \ + Infinite_Set.thy Integ/IntArith.thy Integ/IntDef.thy Integ/IntDiv.thy \ + Integ/NatBin.thy Integ/NatSimprocs.thy Integ/Numeral.thy \ + Integ/Parity.thy Integ/Presburger.thy Integ/cooper_dec.ML \ + Integ/cooper_proof.ML Integ/int_arith1.ML Integ/int_factor_simprocs.ML \ + Integ/nat_simprocs.ML Integ/presburger.ML Integ/qelim.ML LOrder.thy \ + Lattice_Locales.thy Lfp.thy List.ML List.thy Main.ML Main.thy Map.thy \ + Nat.ML Nat.thy NatArith.thy OrderedGroup.ML OrderedGroup.thy \ + Orderings.ML Orderings.thy Power.thy PreList.thy Product_Type.thy \ + ROOT.ML Recdef.thy Reconstruction.thy Record.thy Refute.thy \ + Relation.ML Relation.thy Relation_Power.thy Ring_and_Field.thy Set.ML \ + Set.thy SetInterval.thy Sum_Type.thy Tools/ATP/SpassCommunication.ML \ + Tools/ATP/VampireCommunication.ML Tools/ATP/modUnix.ML \ + Tools/ATP/recon_order_clauses.ML Tools/ATP/recon_parse.ML \ + Tools/ATP/recon_prelim.ML Tools/ATP/recon_transfer_proof.ML \ + Tools/ATP/recon_translate_proof.ML Tools/ATP/res_clasimpset.ML \ + Tools/ATP/watcher.ML Tools/ATP/watcher.sig \ + Tools/datatype_abs_proofs.ML Tools/datatype_aux.ML \ + Tools/datatype_codegen.ML Tools/datatype_package.ML \ + Tools/datatype_prop.ML Tools/datatype_realizer.ML \ + Tools/datatype_rep_proofs.ML Tools/inductive_codegen.ML \ + Tools/inductive_package.ML Tools/inductive_realizer.ML Tools/meson.ML \ + Tools/numeral_syntax.ML Tools/primrec_package.ML Tools/prop_logic.ML \ + Tools/recdef_package.ML Tools/recfun_codegen.ML \ + Tools/reconstruction.ML Tools/record_package.ML Tools/refute.ML \ + Tools/refute_isar.ML Tools/res_atp.ML Tools/res_axioms.ML \ + Tools/res_clause.ML Tools/res_lib.ML Tools/res_skolem_function.ML \ + Tools/res_types_sorts.ML Tools/rewrite_hol_proof.ML \ + Tools/sat_solver.ML Tools/specification_package.ML Tools/split_rule.ML \ + Tools/typedef_package.ML Transitive_Closure.ML Transitive_Closure.thy \ + Typedef.thy Wellfounded_Recursion.thy Wellfounded_Relations.thy \ + antisym_setup.ML arith_data.ML blastdata.ML cladata.ML \ + document/root.tex eqrule_HOL_data.ML hologic.ML simpdata.ML \ + thy_syntax.ML @$(ISATOOL) usedir -b -g true $(HOL_PROOF_OBJECTS) $(OUT)/Pure HOL @@ -126,14 +121,15 @@ HOL-Complex-HahnBanach: HOL-Complex $(LOG)/HOL-Complex-HahnBanach.gz -$(LOG)/HOL-Complex-HahnBanach.gz: $(OUT)/HOL-Complex Real/HahnBanach/Bounds.thy Real/HahnBanach/FunctionNorm.thy \ - Real/HahnBanach/FunctionOrder.thy Real/HahnBanach/HahnBanach.thy \ - Real/HahnBanach/HahnBanachExtLemmas.thy \ - Real/HahnBanach/HahnBanachSupLemmas.thy \ - Real/HahnBanach/Linearform.thy Real/HahnBanach/NormedSpace.thy \ - Real/HahnBanach/README.html Real/HahnBanach/ROOT.ML \ - Real/HahnBanach/Subspace.thy Real/HahnBanach/VectorSpace.thy \ - Real/HahnBanach/ZornLemma.thy Real/HahnBanach/document/root.bib \ +$(LOG)/HOL-Complex-HahnBanach.gz: $(OUT)/HOL-Complex \ + Real/HahnBanach/Bounds.thy Real/HahnBanach/FunctionNorm.thy \ + Real/HahnBanach/FunctionOrder.thy Real/HahnBanach/HahnBanach.thy \ + Real/HahnBanach/HahnBanachExtLemmas.thy \ + Real/HahnBanach/HahnBanachSupLemmas.thy \ + Real/HahnBanach/Linearform.thy Real/HahnBanach/NormedSpace.thy \ + Real/HahnBanach/README.html Real/HahnBanach/ROOT.ML \ + Real/HahnBanach/Subspace.thy Real/HahnBanach/VectorSpace.thy \ + Real/HahnBanach/ZornLemma.thy Real/HahnBanach/document/root.bib \ Real/HahnBanach/document/root.tex @cd Real; $(ISATOOL) usedir -g true $(OUT)/HOL-Complex HahnBanach @@ -142,24 +138,23 @@ HOL-Complex: HOL $(OUT)/HOL-Complex -$(OUT)/HOL-Complex: $(OUT)/HOL Complex/ROOT.ML\ - Library/Zorn.thy\ - Real/Lubs.thy Real/rat_arith.ML\ - Real/Rational.thy Real/PReal.thy Real/RComplete.thy \ - Real/ROOT.ML Real/Real.thy Real/real_arith.ML Real/RealDef.thy \ - Real/RealPow.thy Real/document/root.tex\ - Hyperreal/EvenOdd.thy Hyperreal/Fact.thy Hyperreal/HLog.thy\ - Hyperreal/Filter.thy Hyperreal/HSeries.thy\ - Hyperreal/HTranscendental.thy Hyperreal/HyperArith.thy\ - Hyperreal/HyperDef.thy Hyperreal/HyperNat.thy\ - Hyperreal/HyperPow.thy Hyperreal/Hyperreal.thy\ - Hyperreal/Integration.thy Hyperreal/Lim.thy Hyperreal/Log.thy\ - Hyperreal/MacLaurin.thy Hyperreal/NatStar.thy\ - Hyperreal/NSA.thy Hyperreal/NthRoot.thy Hyperreal/Poly.thy\ - Hyperreal/SEQ.thy Hyperreal/Series.thy Hyperreal/Star.thy \ - Hyperreal/Transcendental.thy Hyperreal/fuf.ML Hyperreal/hypreal_arith.ML \ - Complex/Complex_Main.thy Complex/CLim.thy Complex/CSeries.thy\ - Complex/CStar.thy Complex/Complex.thy Complex/ComplexBin.thy\ +$(OUT)/HOL-Complex: $(OUT)/HOL Complex/ROOT.ML Library/Zorn.thy \ + Real/Lubs.thy Real/rat_arith.ML \ + Real/Rational.thy Real/PReal.thy Real/RComplete.thy \ + Real/ROOT.ML Real/Real.thy Real/real_arith.ML Real/RealDef.thy \ + Real/RealPow.thy Real/document/root.tex \ + Hyperreal/EvenOdd.thy Hyperreal/Fact.thy Hyperreal/HLog.thy \ + Hyperreal/Filter.thy Hyperreal/HSeries.thy \ + Hyperreal/HTranscendental.thy Hyperreal/HyperArith.thy \ + Hyperreal/HyperDef.thy Hyperreal/HyperNat.thy \ + Hyperreal/HyperPow.thy Hyperreal/Hyperreal.thy \ + Hyperreal/Integration.thy Hyperreal/Lim.thy Hyperreal/Log.thy \ + Hyperreal/MacLaurin.thy Hyperreal/NatStar.thy \ + Hyperreal/NSA.thy Hyperreal/NthRoot.thy Hyperreal/Poly.thy \ + Hyperreal/SEQ.thy Hyperreal/Series.thy Hyperreal/Star.thy \ + Hyperreal/Transcendental.thy Hyperreal/fuf.ML Hyperreal/hypreal_arith.ML \ + Complex/Complex_Main.thy Complex/CLim.thy Complex/CSeries.thy \ + Complex/CStar.thy Complex/Complex.thy Complex/ComplexBin.thy \ Complex/NSCA.thy Complex/NSComplex.thy Complex/document/root.tex @cd Complex; $(ISATOOL) usedir -b -g true $(OUT)/HOL HOL-Complex diff -r 3e4e077af2e7 -r 0e1405402d53 src/HOL/ROOT.ML --- a/src/HOL/ROOT.ML Sun May 22 16:51:06 2005 +0200 +++ b/src/HOL/ROOT.ML Sun May 22 16:51:07 2005 +0200 @@ -16,7 +16,6 @@ use "hologic.ML"; -use "~~/src/Provers/simplifier.ML"; use "~~/src/Provers/splitter.ML"; use "~~/src/Provers/hypsubst.ML"; use "~~/src/Provers/induct_method.ML"; diff -r 3e4e077af2e7 -r 0e1405402d53 src/Provers/README --- a/src/Provers/README Sun May 22 16:51:06 2005 +0200 +++ b/src/Provers/README Sun May 22 16:51:07 2005 +0200 @@ -14,9 +14,8 @@ linorder.ML transitivity reasoner for linear (total) orders quantifier1.ML simplification procedures for "1 point rules" simp.ML powerful but slow simplifier - simplifier.ML fast simplifier split_paired_all.ML turn surjective pairing into split rule - splitter.ML performs case splits for simplifier.ML + splitter.ML performs case splits for simplifier typedsimp.ML basic simplifier for explicitly typed logics directory Arith: diff -r 3e4e077af2e7 -r 0e1405402d53 src/Provers/clasimp.ML --- a/src/Provers/clasimp.ML Sun May 22 16:51:06 2005 +0200 +++ b/src/Provers/clasimp.ML Sun May 22 16:51:07 2005 +0200 @@ -3,7 +3,7 @@ Author: David von Oheimb, TU Muenchen Combination of classical reasoner and simplifier (depends on -simplifier.ML, splitter.ML classical.ML, blast.ML). +splitter.ML, classical.ML, blast.ML). *) infix 4 addSIs2 addSEs2 addSDs2 addIs2 addEs2 addDs2 addsimps2 delsimps2 diff -r 3e4e077af2e7 -r 0e1405402d53 src/Sequents/LK0.thy --- a/src/Sequents/LK0.thy Sun May 22 16:51:06 2005 +0200 +++ b/src/Sequents/LK0.thy Sun May 22 16:51:07 2005 +0200 @@ -123,10 +123,6 @@ If :: [o, 'a, 'a] => 'a ("(if (_)/ then (_)/ else (_))" 10) "If(P,x,y) == THE z::'a. (P --> z=x) & (~P --> z=y)" - -setup - Simplifier.setup - setup prover_setup diff -r 3e4e077af2e7 -r 0e1405402d53 src/Sequents/ROOT.ML --- a/src/Sequents/ROOT.ML Sun May 22 16:51:06 2005 +0200 +++ b/src/Sequents/ROOT.ML Sun May 22 16:51:07 2005 +0200 @@ -14,8 +14,6 @@ Unify.trace_bound:= 20; Unify.search_bound := 40; -use "~~/src/Provers/simplifier.ML"; - use_thy "Sequents"; use "prover.ML";