# HG changeset patch # User haftmann # Date 1248587668 -7200 # Node ID d64a1820431d6e995032639e803505e4da9f6ea1 # Parent bda40fb76a65ef21b35f20fe7779ee1db2f005d2# Parent b2e93cda0be8de816a3074ecc8ca307a36d96023 merged diff -r b2e93cda0be8 -r d64a1820431d Admin/isatest/settings/mac-poly-M4 --- a/Admin/isatest/settings/mac-poly-M4 Sat Jul 25 18:44:55 2009 +0200 +++ b/Admin/isatest/settings/mac-poly-M4 Sun Jul 26 07:54:28 2009 +0200 @@ -23,6 +23,6 @@ ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps" ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info" -ISABELLE_USEDIR_OPTIONS="-i false -d false -M 4" +ISABELLE_USEDIR_OPTIONS="-i false -d false -M 4 -t true" HOL_USEDIR_OPTIONS="-p 2 -q 0" diff -r b2e93cda0be8 -r d64a1820431d Admin/isatest/settings/mac-poly-M8 --- a/Admin/isatest/settings/mac-poly-M8 Sat Jul 25 18:44:55 2009 +0200 +++ b/Admin/isatest/settings/mac-poly-M8 Sun Jul 26 07:54:28 2009 +0200 @@ -23,6 +23,6 @@ ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps" ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info" -ISABELLE_USEDIR_OPTIONS="-i false -d false -M 8" +ISABELLE_USEDIR_OPTIONS="-i false -d false -M 8 -t true" HOL_USEDIR_OPTIONS="-p 2 -q 0" diff -r b2e93cda0be8 -r d64a1820431d doc-src/IsarImplementation/Thy/Integration.thy --- a/doc-src/IsarImplementation/Thy/Integration.thy Sat Jul 25 18:44:55 2009 +0200 +++ b/doc-src/IsarImplementation/Thy/Integration.thy Sun Jul 26 07:54:28 2009 +0200 @@ -239,20 +239,20 @@ text %mlref {* \begin{mldecls} - @{index_ML the_context: "unit -> theory"} \\ + @{index_ML ML_Context.the_generic_context: "unit -> Context.generic"} \\ @{index_ML "Context.>> ": "(Context.generic -> Context.generic) -> unit"} \\ \end{mldecls} \begin{description} - \item @{ML "the_context ()"} refers to the theory context of the - {\ML} toplevel --- at compile time! {\ML} code needs to take care - to refer to @{ML "the_context ()"} correctly. Recall that - evaluation of a function body is delayed until actual runtime. - Moreover, persistent {\ML} toplevel bindings to an unfinished theory - should be avoided: code should either project out the desired - information immediately, or produce an explicit @{ML_type - theory_ref} (cf.\ \secref{sec:context-theory}). + \item @{ML "ML_Context.the_generic_context ()"} refers to the theory + context of the {\ML} toplevel --- at compile time! {\ML} code needs + to take care to refer to @{ML "ML_Context.the_generic_context ()"} + correctly. Recall that evaluation of a function body is delayed + until actual runtime. Moreover, persistent {\ML} toplevel bindings + to an unfinished theory should be avoided: code should either + project out the desired information immediately, or produce an + explicit @{ML_type theory_ref} (cf.\ \secref{sec:context-theory}). \item @{ML "Context.>>"}~@{text f} applies context transformation @{text f} to the implicit context of the {\ML} toplevel. diff -r b2e93cda0be8 -r d64a1820431d doc-src/IsarImplementation/Thy/document/Integration.tex --- a/doc-src/IsarImplementation/Thy/document/Integration.tex Sat Jul 25 18:44:55 2009 +0200 +++ b/doc-src/IsarImplementation/Thy/document/Integration.tex Sun Jul 26 07:54:28 2009 +0200 @@ -300,19 +300,20 @@ % \begin{isamarkuptext}% \begin{mldecls} - \indexdef{}{ML}{the\_context}\verb|the_context: unit -> theory| \\ + \indexdef{}{ML}{ML\_Context.the\_generic\_context}\verb|ML_Context.the_generic_context: unit -> Context.generic| \\ \indexdef{}{ML}{Context.$>$$>$ }\verb|Context.>> : (Context.generic -> Context.generic) -> unit| \\ \end{mldecls} \begin{description} - \item \verb|the_context ()| refers to the theory context of the - {\ML} toplevel --- at compile time! {\ML} code needs to take care - to refer to \verb|the_context ()| correctly. Recall that - evaluation of a function body is delayed until actual runtime. - Moreover, persistent {\ML} toplevel bindings to an unfinished theory - should be avoided: code should either project out the desired - information immediately, or produce an explicit \verb|theory_ref| (cf.\ \secref{sec:context-theory}). + \item \verb|ML_Context.the_generic_context ()| refers to the theory + context of the {\ML} toplevel --- at compile time! {\ML} code needs + to take care to refer to \verb|ML_Context.the_generic_context ()| + correctly. Recall that evaluation of a function body is delayed + until actual runtime. Moreover, persistent {\ML} toplevel bindings + to an unfinished theory should be avoided: code should either + project out the desired information immediately, or produce an + explicit \verb|theory_ref| (cf.\ \secref{sec:context-theory}). \item \verb|Context.>>|~\isa{f} applies context transformation \isa{f} to the implicit context of the {\ML} toplevel. diff -r b2e93cda0be8 -r d64a1820431d src/CCL/CCL.thy --- a/src/CCL/CCL.thy Sat Jul 25 18:44:55 2009 +0200 +++ b/src/CCL/CCL.thy Sun Jul 26 07:54:28 2009 +0200 @@ -255,14 +255,20 @@ val caseB_lemmas = mk_lemmas @{thms caseBs} val ccl_dstncts = - let fun mk_raw_dstnct_thm rls s = - prove_goal @{theory} s (fn _=> [rtac notI 1,eresolve_tac rls 1]) - in map (mk_raw_dstnct_thm caseB_lemmas) - (mk_dstnct_rls @{theory} ["bot","true","false","pair","lambda"]) end + let + fun mk_raw_dstnct_thm rls s = + Goal.prove_global @{theory} [] [] (Syntax.read_prop_global @{theory} s) + (fn _=> rtac notI 1 THEN eresolve_tac rls 1) + in map (mk_raw_dstnct_thm caseB_lemmas) + (mk_dstnct_rls @{theory} ["bot","true","false","pair","lambda"]) end fun mk_dstnct_thms thy defs inj_rls xs = - let fun mk_dstnct_thm rls s = prove_goalw thy defs s - (fn _ => [simp_tac (global_simpset_of thy addsimps (rls@inj_rls)) 1]) + let + fun mk_dstnct_thm rls s = + Goal.prove_global thy [] [] (Syntax.read_prop_global thy s) + (fn _ => + rewrite_goals_tac defs THEN + simp_tac (global_simpset_of thy addsimps (rls @ inj_rls)) 1) in map (mk_dstnct_thm ccl_dstncts) (mk_dstnct_rls thy xs) end fun mkall_dstnct_thms thy defs i_rls xss = maps (mk_dstnct_thms thy defs i_rls) xss diff -r b2e93cda0be8 -r d64a1820431d src/FOL/FOL.thy --- a/src/FOL/FOL.thy Sat Jul 25 18:44:55 2009 +0200 +++ b/src/FOL/FOL.thy Sun Jul 26 07:54:28 2009 +0200 @@ -12,7 +12,6 @@ "~~/src/Provers/clasimp.ML" "~~/src/Tools/induct.ML" ("cladata.ML") - ("blastdata.ML") ("simpdata.ML") begin @@ -171,7 +170,25 @@ setup Cla.setup setup cla_setup -use "blastdata.ML" +ML {* + structure Blast = Blast + ( + val thy = @{theory} + type claset = Cla.claset + val equality_name = @{const_name "op ="} + val not_name = @{const_name Not} + val notE = @{thm notE} + val ccontr = @{thm ccontr} + val contr_tac = Cla.contr_tac + val dup_intr = Cla.dup_intr + val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac + val rep_cs = Cla.rep_cs + val cla_modifiers = Cla.cla_modifiers + val cla_meth' = Cla.cla_meth' + ); + val blast_tac = Blast.blast_tac; +*} + setup Blast.setup @@ -360,7 +377,7 @@ text {* Method setup. *} ML {* - structure Induct = InductFun + structure Induct = Induct ( val cases_default = @{thm case_split} val atomize = @{thms induct_atomize} diff -r b2e93cda0be8 -r d64a1820431d src/FOL/IFOL.thy --- a/src/FOL/IFOL.thy Sat Jul 25 18:44:55 2009 +0200 +++ b/src/FOL/IFOL.thy Sun Jul 26 07:54:28 2009 +0200 @@ -591,12 +591,12 @@ done ML {* -structure ProjectRule = ProjectRuleFun -(struct +structure Project_Rule = Project_Rule +( val conjunct1 = @{thm conjunct1} val conjunct2 = @{thm conjunct2} val mp = @{thm mp} -end) +) *} use "fologic.ML" diff -r b2e93cda0be8 -r d64a1820431d src/FOL/IsaMakefile --- a/src/FOL/IsaMakefile Sat Jul 25 18:44:55 2009 +0200 +++ b/src/FOL/IsaMakefile Sun Jul 26 07:54:28 2009 +0200 @@ -36,8 +36,8 @@ $(SRC)/Provers/hypsubst.ML $(SRC)/Tools/induct.ML \ $(SRC)/Tools/intuitionistic.ML $(SRC)/Tools/atomize_elim.ML \ $(SRC)/Tools/project_rule.ML $(SRC)/Provers/quantifier1.ML \ - $(SRC)/Provers/splitter.ML FOL.thy IFOL.thy ROOT.ML blastdata.ML \ - cladata.ML document/root.tex fologic.ML hypsubstdata.ML intprover.ML \ + $(SRC)/Provers/splitter.ML FOL.thy IFOL.thy ROOT.ML cladata.ML \ + document/root.tex fologic.ML hypsubstdata.ML intprover.ML \ simpdata.ML @$(ISABELLE_TOOL) usedir -p 2 -b $(OUT)/Pure FOL diff -r b2e93cda0be8 -r d64a1820431d src/FOL/blastdata.ML --- a/src/FOL/blastdata.ML Sat Jul 25 18:44:55 2009 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,19 +0,0 @@ - -(*** Applying BlastFun to create blast_tac ***) -structure Blast_Data = - struct - type claset = Cla.claset - val equality_name = @{const_name "op ="} - val not_name = @{const_name Not} - val notE = @{thm notE} - val ccontr = @{thm ccontr} - val contr_tac = Cla.contr_tac - val dup_intr = Cla.dup_intr - val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac - val rep_cs = Cla.rep_cs - val cla_modifiers = Cla.cla_modifiers; - val cla_meth' = Cla.cla_meth' - end; - -structure Blast = BlastFun(Blast_Data); -val blast_tac = Blast.blast_tac; diff -r b2e93cda0be8 -r d64a1820431d src/FOL/simpdata.ML --- a/src/FOL/simpdata.ML Sat Jul 25 18:44:55 2009 +0200 +++ b/src/FOL/simpdata.ML Sun Jul 26 07:54:28 2009 +0200 @@ -95,27 +95,25 @@ (*** Case splitting ***) -structure SplitterData = - struct - structure Simplifier = Simplifier - val mk_eq = mk_eq +structure Splitter = Splitter +( + val thy = @{theory} + val mk_eq = mk_eq val meta_eq_to_iff = @{thm meta_eq_to_iff} - val iffD = @{thm iffD2} - val disjE = @{thm disjE} - val conjE = @{thm conjE} - val exE = @{thm exE} - val contrapos = @{thm contrapos} - val contrapos2 = @{thm contrapos2} - val notnotD = @{thm notnotD} - end; + val iffD = @{thm iffD2} + val disjE = @{thm disjE} + val conjE = @{thm conjE} + val exE = @{thm exE} + val contrapos = @{thm contrapos} + val contrapos2 = @{thm contrapos2} + val notnotD = @{thm notnotD} +); -structure Splitter = SplitterFun(SplitterData); - -val split_tac = Splitter.split_tac; +val split_tac = Splitter.split_tac; val split_inside_tac = Splitter.split_inside_tac; -val split_asm_tac = Splitter.split_asm_tac; -val op addsplits = Splitter.addsplits; -val op delsplits = Splitter.delsplits; +val split_asm_tac = Splitter.split_asm_tac; +val op addsplits = Splitter.addsplits; +val op delsplits = Splitter.delsplits; (*** Standard simpsets ***) diff -r b2e93cda0be8 -r d64a1820431d src/HOL/HOL.thy --- a/src/HOL/HOL.thy Sat Jul 25 18:44:55 2009 +0200 +++ b/src/HOL/HOL.thy Sun Jul 26 07:54:28 2009 +0200 @@ -910,8 +910,9 @@ done ML {* -structure Blast = BlastFun +structure Blast = Blast ( + val thy = @{theory} type claset = Classical.claset val equality_name = @{const_name "op ="} val not_name = @{const_name Not} @@ -1390,7 +1391,7 @@ text {* Rule projections: *} ML {* -structure ProjectRule = ProjectRuleFun +structure Project_Rule = Project_Rule ( val conjunct1 = @{thm conjunct1} val conjunct2 = @{thm conjunct2} @@ -1446,7 +1447,7 @@ text {* Method setup. *} ML {* -structure Induct = InductFun +structure Induct = Induct ( val cases_default = @{thm case_split} val atomize = @{thms induct_atomize} diff -r b2e93cda0be8 -r d64a1820431d src/HOL/Import/proof_kernel.ML --- a/src/HOL/Import/proof_kernel.ML Sat Jul 25 18:44:55 2009 +0200 +++ b/src/HOL/Import/proof_kernel.ML Sun Jul 26 07:54:28 2009 +0200 @@ -245,7 +245,8 @@ fun prth th = writeln (PrintMode.setmp [] Display.string_of_thm_without_context th) fun prc ct = writeln (PrintMode.setmp [] Display.string_of_cterm ct) -fun prin t = writeln (PrintMode.setmp [] (fn () => Syntax.string_of_term_global (the_context ()) t) ()); +fun prin t = writeln (PrintMode.setmp [] + (fn () => Syntax.string_of_term (ML_Context.the_local_context ()) t) ()); fun pth (HOLThm(ren,thm)) = let (*val _ = writeln "Renaming:" diff -r b2e93cda0be8 -r d64a1820431d src/HOL/Modelcheck/MuckeSyn.thy --- a/src/HOL/Modelcheck/MuckeSyn.thy Sat Jul 25 18:44:55 2009 +0200 +++ b/src/HOL/Modelcheck/MuckeSyn.thy Sun Jul 26 07:54:28 2009 +0200 @@ -118,7 +118,7 @@ local - val move_thm = prove_goal @{theory} "[| a = b ==> P a; a = b |] ==> P b" + val move_thm = OldGoals.prove_goal @{theory} "[| a = b ==> P a; a = b |] ==> P b" (fn prems => [cut_facts_tac prems 1, dtac sym 1, hyp_subst_tac 1, REPEAT (resolve_tac prems 1)]); @@ -159,9 +159,9 @@ (* transforming fun-defs into lambda-defs *) -val [eq] = goal Pure.thy "(!! x. f x == g x) ==> f == g"; - by (rtac (extensional eq) 1); -qed "ext_rl"; +val [eq] = OldGoals.goal Pure.thy "(!! x. f x == g x) ==> f == g"; + OldGoals.by (rtac (extensional eq) 1); +OldGoals.qed "ext_rl"; infix cc; @@ -196,7 +196,7 @@ val rhs = Syntax.string_of_term_global thy (freeze_thaw RHS) val gl = delete_bold_string (fnam ^" == % " ^ (getargs LHS) ^" . " ^ rhs); in - SOME (prove_goal thy gl (fn prems => + SOME (OldGoals.prove_goal thy gl (fn prems => [(REPEAT (rtac ext_rl 1)), (rtac t 1) ])) end | mk_lam_def [] _ t= NONE; diff -r b2e93cda0be8 -r d64a1820431d src/HOL/Modelcheck/mucke_oracle.ML --- a/src/HOL/Modelcheck/mucke_oracle.ML Sat Jul 25 18:44:55 2009 +0200 +++ b/src/HOL/Modelcheck/mucke_oracle.ML Sun Jul 26 07:54:28 2009 +0200 @@ -109,9 +109,9 @@ ( OldGoals.push_proof(); OldGoals.goalw_cterm [] (cterm_of sign trm); -by (simp_tac (global_simpset_of sign) 1); +OldGoals.by (simp_tac (global_simpset_of sign) 1); let - val if_tmp_result = result() + val if_tmp_result = OldGoals.result() in ( OldGoals.pop_proof(); diff -r b2e93cda0be8 -r d64a1820431d src/HOL/Nominal/nominal_datatype.ML --- a/src/HOL/Nominal/nominal_datatype.ML Sat Jul 25 18:44:55 2009 +0200 +++ b/src/HOL/Nominal/nominal_datatype.ML Sun Jul 26 07:54:28 2009 +0200 @@ -152,7 +152,7 @@ val meta_spec = thm "meta_spec"; fun projections rule = - ProjectRule.projections (ProofContext.init (Thm.theory_of_thm rule)) rule + Project_Rule.projections (ProofContext.init (Thm.theory_of_thm rule)) rule |> map (standard #> RuleCases.save rule); val supp_prod = thm "supp_prod"; diff -r b2e93cda0be8 -r d64a1820431d src/HOL/Nominal/nominal_inductive.ML --- a/src/HOL/Nominal/nominal_inductive.ML Sat Jul 25 18:44:55 2009 +0200 +++ b/src/HOL/Nominal/nominal_inductive.ML Sun Jul 26 07:54:28 2009 +0200 @@ -566,7 +566,7 @@ map (Attrib.internal o K) (#2 strong_induct)), [#1 strong_induct]) ctxt; val strong_inducts = - ProjectRule.projects ctxt (1 upto length names) strong_induct' + Project_Rule.projects ctxt (1 upto length names) strong_induct' in ctxt' |> LocalTheory.note Thm.generatedK diff -r b2e93cda0be8 -r d64a1820431d src/HOL/Nominal/nominal_inductive2.ML --- a/src/HOL/Nominal/nominal_inductive2.ML Sat Jul 25 18:44:55 2009 +0200 +++ b/src/HOL/Nominal/nominal_inductive2.ML Sun Jul 26 07:54:28 2009 +0200 @@ -466,7 +466,7 @@ map (Attrib.internal o K) (#2 strong_induct)), [#1 strong_induct]) ctxt; val strong_inducts = - ProjectRule.projects ctxt' (1 upto length names) strong_induct' + Project_Rule.projects ctxt' (1 upto length names) strong_induct' in ctxt' |> LocalTheory.note Thm.generatedK diff -r b2e93cda0be8 -r d64a1820431d src/HOL/Nominal/nominal_primrec.ML --- a/src/HOL/Nominal/nominal_primrec.ML Sat Jul 25 18:44:55 2009 +0200 +++ b/src/HOL/Nominal/nominal_primrec.ML Sun Jul 26 07:54:28 2009 +0200 @@ -380,7 +380,7 @@ [goals] |> Proof.apply (Method.Basic (fn _ => RAW_METHOD (fn _ => rewrite_goals_tac defs_thms THEN - compose_tac (false, rule, length rule_prems) 1), Position.none)) |> + compose_tac (false, rule, length rule_prems) 1))) |> Seq.hd end; diff -r b2e93cda0be8 -r d64a1820431d src/HOL/Statespace/state_space.ML --- a/src/HOL/Statespace/state_space.ML Sat Jul 25 18:44:55 2009 +0200 +++ b/src/HOL/Statespace/state_space.ML Sun Jul 26 07:54:28 2009 +0200 @@ -149,7 +149,7 @@ thy |> Expression.sublocale_cmd name expr |> Proof.global_terminal_proof - (Method.Basic (fn ctxt => SIMPLE_METHOD (ctxt_tac ctxt),Position.none), NONE) + (Method.Basic (fn ctxt => SIMPLE_METHOD (ctxt_tac ctxt)), NONE) |> ProofContext.theory_of fun add_locale name expr elems thy = diff -r b2e93cda0be8 -r d64a1820431d src/HOL/Tools/Datatype/datatype.ML --- a/src/HOL/Tools/Datatype/datatype.ML Sat Jul 25 18:44:55 2009 +0200 +++ b/src/HOL/Tools/Datatype/datatype.ML Sun Jul 26 07:54:28 2009 +0200 @@ -191,7 +191,7 @@ fun add_cases_induct infos induction thy = let - val inducts = ProjectRule.projections (ProofContext.init thy) induction; + val inducts = Project_Rule.projections (ProofContext.init thy) induction; fun named_rules (name, {index, exhaustion, ...}: info) = [((Binding.empty, nth inducts index), [Induct.induct_type name]), diff -r b2e93cda0be8 -r d64a1820431d src/HOL/Tools/Function/fundef_datatype.ML --- a/src/HOL/Tools/Function/fundef_datatype.ML Sat Jul 25 18:44:55 2009 +0200 +++ b/src/HOL/Tools/Function/fundef_datatype.ML Sun Jul 26 07:54:28 2009 +0200 @@ -208,13 +208,12 @@ val by_pat_completeness_auto = Proof.global_future_terminal_proof - (Method.Basic (pat_completeness, Position.none), + (Method.Basic pat_completeness, SOME (Method.Source_i (Args.src (("HOL.auto", []), Position.none)))) fun termination_by method int = Fundef.termination_proof NONE - #> Proof.global_future_terminal_proof - (Method.Basic (method, Position.none), NONE) int + #> Proof.global_future_terminal_proof (Method.Basic method, NONE) int fun mk_catchall fixes arity_of = let diff -r b2e93cda0be8 -r d64a1820431d src/HOL/Tools/Function/lexicographic_order.ML --- a/src/HOL/Tools/Function/lexicographic_order.ML Sat Jul 25 18:44:55 2009 +0200 +++ b/src/HOL/Tools/Function/lexicographic_order.ML Sun Jul 26 07:54:28 2009 +0200 @@ -140,7 +140,7 @@ fun pr_table table = writeln (cat_lines (map (fn r => concat (map pr_cell r)) table)) fun pr_goals ctxt st = - Display_Goal.pretty_goals ctxt Markup.none (true, false) (Thm.nprems_of st) st + Goal_Display.pretty_goals ctxt {total = true, main = false, maxgoals = Thm.nprems_of st} st |> Pretty.chunks |> Pretty.string_of diff -r b2e93cda0be8 -r d64a1820431d src/HOL/Tools/inductive.ML --- a/src/HOL/Tools/inductive.ML Sat Jul 25 18:44:55 2009 +0200 +++ b/src/HOL/Tools/inductive.ML Sun Jul 26 07:54:28 2009 +0200 @@ -96,11 +96,12 @@ val notTrueE = TrueI RSN (2, notE); val notFalseI = Seq.hd (atac 1 notI); -val simp_thms' = map (fn s => mk_meta_eq (the (find_first - (equal (OldGoals.read_prop @{theory HOL} s) o prop_of) simp_thms))) - ["(~True) = False", "(~False) = True", - "(True --> ?P) = ?P", "(False --> ?P) = True", - "(?P & True) = ?P", "(True & ?P) = ?P"]; + +val simp_thms' = map mk_meta_eq + @{lemma "(~True) = False" "(~False) = True" + "(True --> P) = P" "(False --> P) = True" + "(P & True) = P" "(True & P) = P" + by (fact simp_thms)+}; @@ -712,7 +713,7 @@ map (Attrib.internal o K) (#2 induct)), [rulify (#1 induct)]); val ctxt3 = if no_ind orelse coind then ctxt2 else - let val inducts = cnames ~~ ProjectRule.projects ctxt2 (1 upto length cnames) induct' + let val inducts = cnames ~~ Project_Rule.projects ctxt2 (1 upto length cnames) induct' in ctxt2 |> LocalTheory.notes kind [((rec_qualified (Binding.name "inducts"), []), diff -r b2e93cda0be8 -r d64a1820431d src/HOL/Tools/simpdata.ML --- a/src/HOL/Tools/simpdata.ML Sat Jul 25 18:44:55 2009 +0200 +++ b/src/HOL/Tools/simpdata.ML Sun Jul 26 07:54:28 2009 +0200 @@ -126,27 +126,25 @@ val safe_solver = mk_solver "HOL safe" safe_solver_tac; -structure SplitterData = -struct - structure Simplifier = Simplifier - val mk_eq = mk_eq - val meta_eq_to_iff = @{thm meta_eq_to_obj_eq} - val iffD = @{thm iffD2} - val disjE = @{thm disjE} - val conjE = @{thm conjE} - val exE = @{thm exE} - val contrapos = @{thm contrapos_nn} - val contrapos2 = @{thm contrapos_pp} - val notnotD = @{thm notnotD} -end; +structure Splitter = Splitter +( + val thy = @{theory} + val mk_eq = mk_eq + val meta_eq_to_iff = @{thm meta_eq_to_obj_eq} + val iffD = @{thm iffD2} + val disjE = @{thm disjE} + val conjE = @{thm conjE} + val exE = @{thm exE} + val contrapos = @{thm contrapos_nn} + val contrapos2 = @{thm contrapos_pp} + val notnotD = @{thm notnotD} +); -structure Splitter = SplitterFun(SplitterData); - -val split_tac = Splitter.split_tac; +val split_tac = Splitter.split_tac; val split_inside_tac = Splitter.split_inside_tac; -val op addsplits = Splitter.addsplits; -val op delsplits = Splitter.delsplits; +val op addsplits = Splitter.addsplits; +val op delsplits = Splitter.delsplits; (* integration of simplifier with classical reasoner *) diff -r b2e93cda0be8 -r d64a1820431d src/HOL/ex/Meson_Test.thy --- a/src/HOL/ex/Meson_Test.thy Sat Jul 25 18:44:55 2009 +0200 +++ b/src/HOL/ex/Meson_Test.thy Sun Jul 26 07:54:28 2009 +0200 @@ -5,6 +5,12 @@ imports Main begin +ML {* + val Goal = OldGoals.Goal; + val by = OldGoals.by; + val gethyps = OldGoals.gethyps; +*} + text {* WARNING: there are many potential conflicts between variables used below and constants declared in HOL! diff -r b2e93cda0be8 -r d64a1820431d src/HOLCF/IOA/Modelcheck/MuIOA.thy --- a/src/HOLCF/IOA/Modelcheck/MuIOA.thy Sat Jul 25 18:44:55 2009 +0200 +++ b/src/HOLCF/IOA/Modelcheck/MuIOA.thy Sun Jul 26 07:54:28 2009 +0200 @@ -246,7 +246,7 @@ in ( OldGoals.push_proof(); -Goal +OldGoals.Goal ( "(Internal_of_A = (% a::(" ^ action_type_str ^ "). a:(" ^ ia_str^ "))) --> (Internal_of_C = (% a::(" ^ action_type_str ^ "). a:(" ^ ic_str ^ "))) --> (Start_of_A = (% (" ^ abs_pre_tupel_typed ^ @@ -275,21 +275,21 @@ ") --> (! " ^ con_pre_str_typed ^ ". ! " ^ abs_pre_str_typed ^ ". (Start_of_C (" ^ con_pre_tupel ^ ") & Start_of_A (" ^ abs_pre_tupel ^ ")) --> isSimCA(" ^ con_pre_tupel ^ "," ^ abs_pre_tupel ^ "))"); -by (REPEAT (rtac impI 1)); -by (REPEAT (dtac eq_reflection 1)); +OldGoals.by (REPEAT (rtac impI 1)); +OldGoals.by (REPEAT (dtac eq_reflection 1)); (* Bis hierher wird im Kapitel 4 erl"autert, ab hier im Kapitel 5 *) -by (full_simp_tac ((global_simpset_of sign delcongs (if_weak_cong :: weak_case_congs) +OldGoals.by (full_simp_tac ((global_simpset_of sign delcongs (if_weak_cong :: weak_case_congs) delsimps [not_iff,split_part]) addsimps (thl @ comp_simps @ restrict_simps @ hide_simps @ rename_simps @ ioa_simps @ asig_simps)) 1); -by (full_simp_tac +OldGoals.by (full_simp_tac (Mucke_ss delcongs (if_weak_cong :: weak_case_congs) delsimps [not_iff,split_part]) 1); -by (REPEAT (if_full_simp_tac +OldGoals.by (REPEAT (if_full_simp_tac (global_simpset_of sign delcongs (if_weak_cong :: weak_case_congs) delsimps [not_iff,split_part]) 1)); -by (call_mucke_tac 1); +OldGoals.by (call_mucke_tac 1); (* Bis hierher wird im Kapitel 5 erl"autert, ab hier wieder im Kapitel 4 *) -by (atac 1); -result(); +OldGoals.by (atac 1); +OldGoals.result(); OldGoals.pop_proof(); Thm.cterm_of sign (Logic.strip_imp_concl subgoal) ) diff -r b2e93cda0be8 -r d64a1820431d src/HOLCF/Tools/Domain/domain_theorems.ML --- a/src/HOLCF/Tools/Domain/domain_theorems.ML Sat Jul 25 18:44:55 2009 +0200 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML Sun Jul 26 07:54:28 2009 +0200 @@ -1033,7 +1033,7 @@ in pg [] goal (K tacs) end; end; (* local *) -val inducts = ProjectRule.projections (ProofContext.init thy) ind; +val inducts = Project_Rule.projections (ProofContext.init thy) ind; fun ind_rule (dname, rule) = ((Binding.empty, [rule]), [Induct.induct_type dname]); val induct_failed = (Thm.prop_of ind = Thm.prop_of TrueI); diff -r b2e93cda0be8 -r d64a1820431d src/Provers/blast.ML --- a/src/Provers/blast.ML Sat Jul 25 18:44:55 2009 +0200 +++ b/src/Provers/blast.ML Sun Jul 26 07:54:28 2009 +0200 @@ -39,7 +39,8 @@ type netpair = (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net; signature BLAST_DATA = - sig +sig + val thy: theory type claset val equality_name: string val not_name: string @@ -57,11 +58,10 @@ haz_netpair: netpair, dup_netpair: netpair, xtra_netpair: ContextRules.netpair} val cla_modifiers: Method.modifier parser list val cla_meth': (claset -> int -> tactic) -> thm list -> Proof.context -> Proof.method - end; - +end; signature BLAST = - sig +sig type claset exception TRANS of string (*reports translation errors*) datatype term = @@ -90,10 +90,10 @@ val tryInThy : theory -> claset -> int -> string -> (int->tactic) list * branch list list * (int*int*exn) list val normBr : branch -> branch - end; +end; -functor BlastFun(Data: BLAST_DATA) : BLAST = +functor Blast(Data: BLAST_DATA) : BLAST = struct type claset = Data.claset; @@ -181,8 +181,8 @@ fun isGoal (Const ("*Goal*", _) $ _) = true | isGoal _ = false; -val TruepropC = ObjectLogic.judgment_name (the_context ()); -val TruepropT = Sign.the_const_type (the_context ()) TruepropC; +val TruepropC = ObjectLogic.judgment_name Data.thy; +val TruepropT = Sign.the_const_type Data.thy TruepropC; fun mk_Trueprop t = Term.$ (Term.Const (TruepropC, TruepropT), t); diff -r b2e93cda0be8 -r d64a1820431d src/Provers/splitter.ML --- a/src/Provers/splitter.ML Sat Jul 25 18:44:55 2009 +0200 +++ b/src/Provers/splitter.ML Sun Jul 26 07:54:28 2009 +0200 @@ -1,5 +1,4 @@ -(* Title: Provers/splitter - ID: $Id$ +(* Title: Provers/splitter.ML Author: Tobias Nipkow Copyright 1995 TU Munich @@ -12,6 +11,7 @@ signature SPLITTER_DATA = sig + val thy : theory val mk_eq : thm -> thm val meta_eq_to_iff: thm (* "x == y ==> x = y" *) val iffD : thm (* "[| P = Q; Q |] ==> P" *) @@ -41,18 +41,18 @@ val setup: theory -> theory end; -functor SplitterFun(Data: SPLITTER_DATA): SPLITTER = +functor Splitter(Data: SPLITTER_DATA): SPLITTER = struct val Const (const_not, _) $ _ = - ObjectLogic.drop_judgment (the_context ()) + ObjectLogic.drop_judgment Data.thy (#1 (Logic.dest_implies (Thm.prop_of Data.notnotD))); val Const (const_or , _) $ _ $ _ = - ObjectLogic.drop_judgment (the_context ()) + ObjectLogic.drop_judgment Data.thy (#1 (Logic.dest_implies (Thm.prop_of Data.disjE))); -val const_Trueprop = ObjectLogic.judgment_name (the_context ()); +val const_Trueprop = ObjectLogic.judgment_name Data.thy; fun split_format_err () = error "Wrong format for split rule"; diff -r b2e93cda0be8 -r d64a1820431d src/Pure/Concurrent/future.ML --- a/src/Pure/Concurrent/future.ML Sat Jul 25 18:44:55 2009 +0200 +++ b/src/Pure/Concurrent/future.ML Sun Jul 26 07:54:28 2009 +0200 @@ -138,7 +138,7 @@ fun count_active ws = fold (fn (_, active) => fn i => if active then i + 1 else i) ws 0; -fun trace_active () = Multithreading.tracing 1 (fn () => +fun trace_active () = Multithreading.tracing 6 (fn () => let val ws = ! workers; val m = string_of_int (length ws); @@ -222,7 +222,7 @@ fun scheduler_next () = (*requires SYNCHRONIZED*) let (*queue status*) - val _ = Multithreading.tracing 1 (fn () => + val _ = Multithreading.tracing 6 (fn () => let val {ready, pending, running} = Task_Queue.status (! queue) in "SCHEDULE: " ^ string_of_int ready ^ " ready, " ^ @@ -338,8 +338,12 @@ if SYNCHRONIZED "join_wait" (fn () => is_finished x orelse (if worker then worker_wait () else wait (); false)) then () else join_wait x; - val _ = List.app join_wait xs; + val _ = xs |> List.app (fn x => + let val time = Multithreading.real_time join_wait x in + Multithreading.tracing_time true time + (fn () => "joined after " ^ Time.toString time) + end); in map get_result xs end) (); end; diff -r b2e93cda0be8 -r d64a1820431d src/Pure/Concurrent/simple_thread.ML --- a/src/Pure/Concurrent/simple_thread.ML Sat Jul 25 18:44:55 2009 +0200 +++ b/src/Pure/Concurrent/simple_thread.ML Sun Jul 26 07:54:28 2009 +0200 @@ -28,13 +28,15 @@ val immediate = if Mutex.trylock lock then true else - (Multithreading.tracing 3 (fn () => name ^ ": locking ..."); - Mutex.lock lock; - Multithreading.tracing 3 (fn () => name ^ ": locked"); - false); + let + val _ = Multithreading.tracing 5 (fn () => name ^ ": locking ..."); + val time = Multithreading.real_time Mutex.lock lock; + val _ = Multithreading.tracing_time true time + (fn () => name ^ ": locked after " ^ Time.toString time); + in false end; val result = Exn.capture (restore_attributes e) (); val _ = - if immediate then () else Multithreading.tracing 3 (fn () => name ^ ": unlocking ..."); + if immediate then () else Multithreading.tracing 5 (fn () => name ^ ": unlocking ..."); val _ = Mutex.unlock lock; in result end) ()); diff -r b2e93cda0be8 -r d64a1820431d src/Pure/Concurrent/task_queue.ML --- a/src/Pure/Concurrent/task_queue.ML Sat Jul 25 18:44:55 2009 +0200 +++ b/src/Pure/Concurrent/task_queue.ML Sun Jul 26 07:54:28 2009 +0200 @@ -94,9 +94,6 @@ fun get_job (jobs: jobs) task = #2 (Task_Graph.get_node jobs task); fun set_job task job (jobs: jobs) = Task_Graph.map_node task (fn (group, _) => (group, job)) jobs; -fun add_job task dep (jobs: jobs) = - Task_Graph.add_edge (dep, task) jobs handle Task_Graph.UNDEF _ => jobs; - (* queue of grouped jobs *) @@ -150,6 +147,12 @@ (* enqueue *) +fun add_job task dep (jobs: jobs) = + Task_Graph.add_edge (dep, task) jobs handle Task_Graph.UNDEF _ => jobs; + +fun get_deps (jobs: jobs) task = + Task_Graph.imm_preds jobs task handle Task_Graph.UNDEF _ => []; + fun enqueue group deps pri job (Queue {groups, jobs, cache}) = let val task = new_task pri; @@ -157,7 +160,8 @@ |> fold (fn gid => Inttab.cons_list (gid, task)) (group_ancestry group); val jobs' = jobs |> Task_Graph.new_node (task, (group, Job [job])) - |> fold (add_job task) deps; + |> fold (add_job task) deps + |> fold (fold (add_job task) o get_deps jobs) deps; val cache' = (case cache of Result last => @@ -205,7 +209,6 @@ then SOME (task, group, rev list) else NONE | _ => NONE); - val tasks = filter (can (Task_Graph.get_node jobs)) deps; fun result (res as (task, _, _)) = let @@ -216,7 +219,7 @@ (case get_first ready tasks of SOME res => result res | NONE => - (case get_first ready (Task_Graph.all_preds jobs tasks) of + (case get_first (get_first ready o Task_Graph.imm_preds jobs) tasks of SOME res => result res | NONE => (NONE, queue))) end; diff -r b2e93cda0be8 -r d64a1820431d src/Pure/General/position.ML --- a/src/Pure/General/position.ML Sat Jul 25 18:44:55 2009 +0200 +++ b/src/Pure/General/position.ML Sun Jul 26 07:54:28 2009 +0200 @@ -36,7 +36,6 @@ val range: T -> T -> range val thread_data: unit -> T val setmp_thread_data: T -> ('a -> 'b) -> 'a -> 'b - val setmp_thread_data_seq: T -> ('a -> 'b Seq.seq) -> 'a -> 'b Seq.seq end; structure Position: POSITION = @@ -176,9 +175,6 @@ if ! Output.debugging then f x else Library.setmp_thread_data tag (thread_data ()) pos f x; -fun setmp_thread_data_seq pos f x = - setmp_thread_data pos f x |> Seq.wrap (fn pull => setmp_thread_data pos pull ()); - end; end; diff -r b2e93cda0be8 -r d64a1820431d src/Pure/General/seq.ML --- a/src/Pure/General/seq.ML Sat Jul 25 18:44:55 2009 +0200 +++ b/src/Pure/General/seq.ML Sun Jul 26 07:54:28 2009 +0200 @@ -33,7 +33,6 @@ val lift: ('a -> 'b -> 'c) -> 'a seq -> 'b -> 'c seq val lifts: ('a -> 'b -> 'c seq) -> 'a seq -> 'b -> 'c seq val singleton: ('a list -> 'b list seq) -> 'a -> 'b seq - val wrap: ((unit -> ('a * 'a seq) option) -> ('a * 'a seq) option) -> 'a seq -> 'a seq val print: (int -> 'a -> unit) -> int -> 'a seq -> unit val it_right : ('a * 'b seq -> 'b seq) -> 'a seq * 'b seq -> 'b seq val succeed: 'a -> 'a seq @@ -170,13 +169,6 @@ fun singleton f x = f [x] |> map (fn [y] => y | _ => raise Empty); -(*wrapped lazy evaluation*) -fun wrap f xq = - make (fn () => - (case f (fn () => pull xq) of - NONE => NONE - | SOME (x, xq') => SOME (x, wrap f xq'))); - (*print a sequence, up to "count" elements*) fun print print_elem count = let @@ -200,7 +192,7 @@ -(** sequence functions **) (*cf. Pure/tctical.ML*) +(** sequence functions **) (*cf. Pure/tactical.ML*) fun succeed x = single x; fun fail _ = empty; diff -r b2e93cda0be8 -r d64a1820431d src/Pure/IsaMakefile --- a/src/Pure/IsaMakefile Sat Jul 25 18:44:55 2009 +0200 +++ b/src/Pure/IsaMakefile Sun Jul 26 07:54:28 2009 +0200 @@ -90,11 +90,11 @@ Tools/find_theorems.ML Tools/named_thms.ML Tools/xml_syntax.ML \ assumption.ML axclass.ML codegen.ML config.ML conjunction.ML \ consts.ML context.ML context_position.ML conv.ML defs.ML display.ML \ - display_goal.ML drule.ML envir.ML facts.ML goal.ML interpretation.ML \ + drule.ML envir.ML facts.ML goal.ML goal_display.ML interpretation.ML \ item_net.ML library.ML logic.ML meta_simplifier.ML more_thm.ML \ morphism.ML name.ML net.ML old_goals.ML old_term.ML pattern.ML \ primitive_defs.ML proofterm.ML pure_setup.ML pure_thy.ML search.ML \ - sign.ML simplifier.ML sorts.ML subgoal.ML tactic.ML tctical.ML \ + sign.ML simplifier.ML sorts.ML subgoal.ML tactic.ML tactical.ML \ term.ML term_ord.ML term_subst.ML theory.ML thm.ML type.ML \ type_infer.ML unify.ML variable.ML @./mk diff -r b2e93cda0be8 -r d64a1820431d src/Pure/Isar/element.ML --- a/src/Pure/Isar/element.ML Sat Jul 25 18:44:55 2009 +0200 +++ b/src/Pure/Isar/element.ML Sun Jul 26 07:54:28 2009 +0200 @@ -272,7 +272,7 @@ Proof.refine (Method.Basic (K (RAW_METHOD (K (ALLGOALS (CONJUNCTS (ALLGOALS - (CONJUNCTS (TRYALL (Tactic.rtac Drule.protectI)))))))), Position.none)); + (CONJUNCTS (TRYALL (Tactic.rtac Drule.protectI)))))))))); fun gen_witness_proof proof after_qed wit_propss eq_props = let diff -r b2e93cda0be8 -r d64a1820431d src/Pure/Isar/method.ML --- a/src/Pure/Isar/method.ML Sat Jul 25 18:44:55 2009 +0200 +++ b/src/Pure/Isar/method.ML Sun Jul 26 07:54:28 2009 +0200 @@ -15,7 +15,7 @@ sig include BASIC_METHOD type method - val apply: Position.T -> (Proof.context -> method) -> Proof.context -> thm list -> cases_tactic + val apply: (Proof.context -> method) -> Proof.context -> thm list -> cases_tactic val RAW_METHOD_CASES: (thm list -> cases_tactic) -> method val RAW_METHOD: (thm list -> tactic) -> method val METHOD_CASES: (thm list -> cases_tactic) -> method @@ -55,7 +55,7 @@ val raw_tactic: string * Position.T -> Proof.context -> method type src = Args.src datatype text = - Basic of (Proof.context -> method) * Position.T | + Basic of Proof.context -> method | Source of src | Source_i of src | Then of text list | @@ -69,7 +69,7 @@ val this_text: text val done_text: text val sorry_text: bool -> text - val finish_text: text option * bool -> Position.T -> text + val finish_text: text option * bool -> text val print_methods: theory -> unit val intern: theory -> xstring -> string val defined: theory -> string -> bool @@ -106,8 +106,7 @@ datatype method = Meth of thm list -> cases_tactic; -fun apply pos meth_fun ctxt facts goal = Position.setmp_thread_data_seq pos - (fn () => let val Meth meth = meth_fun ctxt in meth facts goal end) (); +fun apply meth ctxt = let val Meth m = meth ctxt in m end; val RAW_METHOD_CASES = Meth; @@ -297,7 +296,7 @@ type src = Args.src; datatype text = - Basic of (Proof.context -> method) * Position.T | + Basic of Proof.context -> method | Source of src | Source_i of src | Then of text list | @@ -306,15 +305,15 @@ Repeat1 of text | SelectGoals of int * text; -fun primitive_text r = Basic (K (SIMPLE_METHOD (PRIMITIVE r)), Position.none); -val succeed_text = Basic (K succeed, Position.none); +fun primitive_text r = Basic (K (SIMPLE_METHOD (PRIMITIVE r))); +val succeed_text = Basic (K succeed); val default_text = Source (Args.src (("default", []), Position.none)); -val this_text = Basic (K this, Position.none); -val done_text = Basic (K (SIMPLE_METHOD all_tac), Position.none); -fun sorry_text int = Basic (cheating int, Position.none); +val this_text = Basic (K this); +val done_text = Basic (K (SIMPLE_METHOD all_tac)); +fun sorry_text int = Basic (cheating int); -fun finish_text (NONE, immed) pos = Basic (close immed, pos) - | finish_text (SOME txt, immed) pos = Then [txt, Basic (close immed, pos)]; +fun finish_text (NONE, immed) = Basic (close immed) + | finish_text (SOME txt, immed) = Then [txt, Basic (close immed)]; (* method definitions *) @@ -477,8 +476,8 @@ end; -structure BasicMethod: BASIC_METHOD = Method; -open BasicMethod; +structure Basic_Method: BASIC_METHOD = Method; +open Basic_Method; val RAW_METHOD_CASES = Method.RAW_METHOD_CASES; val RAW_METHOD = Method.RAW_METHOD; diff -r b2e93cda0be8 -r d64a1820431d src/Pure/Isar/proof.ML --- a/src/Pure/Isar/proof.ML Sat Jul 25 18:44:55 2009 +0200 +++ b/src/Pure/Isar/proof.ML Sun Jul 26 07:54:28 2009 +0200 @@ -344,8 +344,8 @@ (if mode <> Backward orelse null using then NONE else SOME using) @ [Pretty.str ("goal" ^ description [levels_up (i div 2), subgoals (Thm.nprems_of goal)] ^ ":")] @ - Display_Goal.pretty_goals ctxt Markup.subgoal - (true, ! show_main_goal) (! Display.goals_limit) goal @ + Goal_Display.pretty_goals ctxt + {total = true, main = ! show_main_goal, maxgoals = ! Display.goals_limit} goal @ (map (fn msg => Position.setmp_thread_data pos msg ()) (rev messages)) | prt_goal NONE = []; @@ -365,8 +365,10 @@ end; fun pretty_goals main state = - let val (ctxt, (_, goal)) = get_goal state - in Display_Goal.pretty_goals ctxt Markup.none (false, main) (! Display.goals_limit) goal end; + let val (ctxt, (_, goal)) = get_goal state in + Goal_Display.pretty_goals ctxt + {total = false, main = main, maxgoals = ! Display.goals_limit} goal + end; @@ -384,13 +386,13 @@ fun goal_cases st = RuleCases.make_common true (Thm.theory_of_thm st, Thm.prop_of st) (map (rpair []) (goals st)); -fun apply_method current_context pos meth state = +fun apply_method current_context meth state = let val (goal_ctxt, (_, {statement, messages = _, using, goal, before_qed, after_qed})) = find_goal state; val ctxt = if current_context then context_of state else goal_ctxt; in - Method.apply pos meth ctxt using goal |> Seq.map (fn (meth_cases, goal') => + Method.apply meth ctxt using goal |> Seq.map (fn (meth_cases, goal') => state |> map_goal (ProofContext.add_cases false (no_goal_cases goal @ goal_cases goal') #> @@ -408,16 +410,15 @@ |> Seq.maps meth |> Seq.maps (fn state' => state' |> Seq.lift set_goal (Goal.retrofit 1 n (#2 (#2 (get_goal state'))) goal)) - |> Seq.maps (apply_method true Position.none (K Method.succeed))); + |> Seq.maps (apply_method true (K Method.succeed))); fun apply_text cc text state = let val thy = theory_of state; - val pos_of = #2 o Args.dest_src; - fun eval (Method.Basic (m, pos)) = apply_method cc pos m - | eval (Method.Source src) = apply_method cc (pos_of src) (Method.method thy src) - | eval (Method.Source_i src) = apply_method cc (pos_of src) (Method.method_i thy src) + fun eval (Method.Basic m) = apply_method cc m + | eval (Method.Source src) = apply_method cc (Method.method thy src) + | eval (Method.Source_i src) = apply_method cc (Method.method_i thy src) | eval (Method.Then txts) = Seq.EVERY (map eval txts) | eval (Method.Orelse txts) = Seq.FIRST (map eval txts) | eval (Method.Try txt) = Seq.TRY (eval txt) @@ -431,7 +432,7 @@ val refine_end = apply_text false; fun refine_insert [] = I - | refine_insert ths = Seq.hd o refine (Method.Basic (K (Method.insert ths), Position.none)); + | refine_insert ths = Seq.hd o refine (Method.Basic (K (Method.insert ths))); end; @@ -472,8 +473,8 @@ val ngoals = Thm.nprems_of goal; val _ = ngoals = 0 orelse error (Pretty.string_of (Pretty.chunks - (Display_Goal.pretty_goals ctxt Markup.none - (true, ! show_main_goal) (! Display.goals_limit) goal @ + (Goal_Display.pretty_goals ctxt + {total = true, main = ! show_main_goal, maxgoals = ! Display.goals_limit} goal @ [Pretty.str (string_of_int ngoals ^ " unsolved goal(s)!")]))); val extra_hyps = Assumption.extra_hyps ctxt goal; @@ -748,7 +749,7 @@ |> assert_current_goal true |> using_facts [] |> `before_qed |-> (refine o the_default Method.succeed_text) - |> Seq.maps (refine (Method.finish_text txt (Position.thread_data ()))); + |> Seq.maps (refine (Method.finish_text txt)); fun check_result msg sq = (case Seq.pull sq of @@ -760,8 +761,8 @@ (* unstructured refinement *) -fun defer i = assert_no_chain #> refine (Method.Basic (K (Method.defer i), Position.none)); -fun prefer i = assert_no_chain #> refine (Method.Basic (K (Method.prefer i), Position.none)); +fun defer i = assert_no_chain #> refine (Method.Basic (K (Method.defer i))); +fun prefer i = assert_no_chain #> refine (Method.Basic (K (Method.prefer i))); fun apply text = assert_backward #> refine text #> Seq.map (using_facts []); fun apply_end text = assert_forward #> refine_end text; @@ -787,7 +788,7 @@ fun refine_terms n = refine (Method.Basic (K (RAW_METHOD (K (HEADGOAL (PRECISE_CONJUNCTS n - (HEADGOAL (CONJUNCTS (ALLGOALS (rtac Drule.termI)))))))), Position.none)) + (HEADGOAL (CONJUNCTS (ALLGOALS (rtac Drule.termI)))))))))) #> Seq.hd; in @@ -830,7 +831,7 @@ |> put_goal NONE |> enter_backward |> not (null vars) ? refine_terms (length goal_propss) - |> null props ? (refine (Method.Basic (Method.assumption, Position.none)) #> Seq.hd) + |> null props ? (refine (Method.Basic Method.assumption) #> Seq.hd) end; fun generic_qed after_ctxt state = diff -r b2e93cda0be8 -r d64a1820431d src/Pure/ML-Systems/multithreading.ML --- a/src/Pure/ML-Systems/multithreading.ML Sat Jul 25 18:44:55 2009 +0200 +++ b/src/Pure/ML-Systems/multithreading.ML Sun Jul 26 07:54:28 2009 +0200 @@ -15,6 +15,8 @@ include BASIC_MULTITHREADING val trace: int ref val tracing: int -> (unit -> string) -> unit + val tracing_time: bool -> Time.time -> (unit -> string) -> unit + val real_time: ('a -> unit) -> 'a -> Time.time val available: bool val max_threads: int ref val max_threads_value: unit -> int @@ -31,10 +33,15 @@ structure Multithreading: MULTITHREADING = struct -(* options *) +(* tracing *) val trace = ref (0: int); fun tracing _ _ = (); +fun tracing_time _ _ _ = (); +fun real_time f x = (f x; Time.zeroTime); + + +(* options *) val available = false; val max_threads = ref (1: int); diff -r b2e93cda0be8 -r d64a1820431d src/Pure/ML-Systems/multithreading_polyml.ML --- a/src/Pure/ML-Systems/multithreading_polyml.ML Sat Jul 25 18:44:55 2009 +0200 +++ b/src/Pure/ML-Systems/multithreading_polyml.ML Sun Jul 26 07:54:28 2009 +0200 @@ -27,7 +27,7 @@ structure Multithreading: MULTITHREADING = struct -(* options *) +(* tracing *) val trace = ref 0; @@ -36,6 +36,24 @@ else (TextIO.output (TextIO.stdErr, (">>> " ^ msg () ^ "\n")); TextIO.flushOut TextIO.stdErr) handle _ (*sic*) => (); +fun tracing_time detailed time = + tracing + (if not detailed then 5 + else if Time.>= (time, Time.fromMilliseconds 1000) then 1 + else if Time.>= (time, Time.fromMilliseconds 100) then 2 + else if Time.>= (time, Time.fromMilliseconds 10) then 3 + else if Time.>= (time, Time.fromMilliseconds 1) then 4 else 5); + +fun real_time f x = + let + val timer = Timer.startRealTimer (); + val () = f x; + val time = Timer.checkRealTimer timer; + in time end; + + +(* options *) + val available = true; val max_threads = ref 0; @@ -205,22 +223,16 @@ fun NAMED_CRITICAL name e = if self_critical () then e () else - uninterruptible (fn restore_attributes => fn () => + Exn.release (uninterruptible (fn restore_attributes => fn () => let val name' = ! critical_name; val _ = if Mutex.trylock critical_lock then () else let - val timer = Timer.startRealTimer (); - val _ = tracing 4 (fn () => "CRITICAL" ^ show name ^ show' name' ^ ": waiting"); - val _ = Mutex.lock critical_lock; - val time = Timer.checkRealTimer timer; - val trace_time = - if Time.>= (time, Time.fromMilliseconds 1000) then 1 - else if Time.>= (time, Time.fromMilliseconds 100) then 2 - else if Time.>= (time, Time.fromMilliseconds 10) then 3 else 4; - val _ = tracing trace_time (fn () => + val _ = tracing 5 (fn () => "CRITICAL" ^ show name ^ show' name' ^ ": waiting"); + val time = real_time Mutex.lock critical_lock; + val _ = tracing_time true time (fn () => "CRITICAL" ^ show name ^ show' name' ^ ": passed after " ^ Time.toString time); in () end; val _ = critical_thread := SOME (Thread.self ()); @@ -229,7 +241,7 @@ val _ = critical_name := ""; val _ = critical_thread := NONE; val _ = Mutex.unlock critical_lock; - in Exn.release result end) (); + in result end) ()); fun CRITICAL e = NAMED_CRITICAL "" e; diff -r b2e93cda0be8 -r d64a1820431d src/Pure/Proof/reconstruct.ML --- a/src/Pure/Proof/reconstruct.ML Sat Jul 25 18:44:55 2009 +0200 +++ b/src/Pure/Proof/reconstruct.ML Sun Jul 26 07:54:28 2009 +0200 @@ -255,7 +255,7 @@ let fun search env [] = error ("Unsolvable constraints:\n" ^ Pretty.string_of (Pretty.chunks (map (fn (_, p, _) => - Display_Goal.pretty_flexpair (Syntax.init_pretty_global thy) (pairself + Goal_Display.pretty_flexpair (Syntax.init_pretty_global thy) (pairself (Envir.norm_term bigenv) p)) cs))) | search env ((u, p as (t1, t2), vs)::ps) = if u then diff -r b2e93cda0be8 -r d64a1820431d src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Sat Jul 25 18:44:55 2009 +0200 +++ b/src/Pure/ROOT.ML Sun Jul 26 07:54:28 2009 +0200 @@ -119,8 +119,8 @@ use "morphism.ML"; use "variable.ML"; use "conv.ML"; -use "display_goal.ML"; -use "tctical.ML"; +use "goal_display.ML"; +use "tactical.ML"; use "search.ML"; use "tactic.ML"; use "meta_simplifier.ML"; diff -r b2e93cda0be8 -r d64a1820431d src/Pure/codegen.ML --- a/src/Pure/codegen.ML Sat Jul 25 18:44:55 2009 +0200 +++ b/src/Pure/codegen.ML Sun Jul 26 07:54:28 2009 +0200 @@ -831,7 +831,8 @@ end; val generate_code_i = gen_generate_code Sign.cert_term; -val generate_code = gen_generate_code OldGoals.read_term; +val generate_code = + gen_generate_code (Syntax.read_term o ProofContext.allow_dummies o ProofContext.init); (**** Reflection ****) diff -r b2e93cda0be8 -r d64a1820431d src/Pure/display.ML --- a/src/Pure/display.ML Sat Jul 25 18:44:55 2009 +0200 +++ b/src/Pure/display.ML Sun Jul 26 07:54:28 2009 +0200 @@ -42,8 +42,8 @@ (** options **) -val goals_limit = Display_Goal.goals_limit; -val show_consts = Display_Goal.show_consts; +val goals_limit = Goal_Display.goals_limit; +val show_consts = Goal_Display.show_consts; val show_hyps = ref false; (*false: print meta-hypotheses as dots*) val show_tags = ref false; (*false: suppress tags*) @@ -87,7 +87,7 @@ if hlen = 0 andalso status = "" then [] else if ! show_hyps orelse show_hyps' then [Pretty.brk 2, Pretty.list "[" "]" - (map (q o Display_Goal.pretty_flexpair ctxt) tpairs @ map prt_term hyps' @ + (map (q o Goal_Display.pretty_flexpair ctxt) tpairs @ map prt_term hyps' @ map (Syntax.pretty_sort ctxt) xshyps @ (if status = "" then [] else [Pretty.str status]))] else [Pretty.brk 2, Pretty.str ("[" ^ implode (replicate hlen ".") ^ status ^ "]")]; diff -r b2e93cda0be8 -r d64a1820431d src/Pure/display_goal.ML --- a/src/Pure/display_goal.ML Sat Jul 25 18:44:55 2009 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,126 +0,0 @@ -(* Title: Pure/display_goal.ML - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Author: Makarius - -Display tactical goal state. -*) - -signature DISPLAY_GOAL = -sig - val goals_limit: int ref - val show_consts: bool ref - val pretty_flexpair: Proof.context -> term * term -> Pretty.T - val pretty_goals: Proof.context -> Markup.T -> bool * bool -> int -> thm -> Pretty.T list - val pretty_goals_without_context: int -> thm -> Pretty.T list - val print_goals_without_context: int -> thm -> unit -end; - -structure Display_Goal: DISPLAY_GOAL = -struct - -val goals_limit = ref 10; (*max number of goals to print*) -val show_consts = ref false; (*true: show consts with types in proof state output*) - -fun pretty_flexpair ctxt (t, u) = Pretty.block - [Syntax.pretty_term ctxt t, Pretty.str " =?=", Pretty.brk 1, Syntax.pretty_term ctxt u]; - - -(*print thm A1,...,An/B in "goal style" -- premises as numbered subgoals*) - -local - -fun ins_entry (x, y) = - AList.default (op =) (x, []) #> - AList.map_entry (op =) x (insert (op =) y); - -val add_consts = Term.fold_aterms - (fn Const (c, T) => ins_entry (T, (c, T)) - | _ => I); - -val add_vars = Term.fold_aterms - (fn Free (x, T) => ins_entry (T, (x, ~1)) - | Var (xi, T) => ins_entry (T, xi) - | _ => I); - -val add_varsT = Term.fold_atyps - (fn TFree (x, S) => ins_entry (S, (x, ~1)) - | TVar (xi, S) => ins_entry (S, xi) - | _ => I); - -fun sort_idxs vs = map (apsnd (sort (prod_ord string_ord int_ord))) vs; -fun sort_cnsts cs = map (apsnd (sort_wrt fst)) cs; - -fun consts_of t = sort_cnsts (add_consts t []); -fun vars_of t = sort_idxs (add_vars t []); -fun varsT_of t = rev (sort_idxs (Term.fold_types add_varsT t [])); - -in - -fun pretty_goals ctxt markup (msg, main) maxgoals state = - let - val prt_sort = Syntax.pretty_sort ctxt; - val prt_typ = Syntax.pretty_typ ctxt; - val prt_term = Syntax.pretty_term ctxt; - - fun prt_atoms prt prtT (X, xs) = Pretty.block - [Pretty.block (Pretty.commas (map prt xs)), Pretty.str " ::", - Pretty.brk 1, prtT X]; - - fun prt_var (x, ~1) = prt_term (Syntax.free x) - | prt_var xi = prt_term (Syntax.var xi); - - fun prt_varT (x, ~1) = prt_typ (TFree (x, [])) - | prt_varT xi = prt_typ (TVar (xi, [])); - - val prt_consts = prt_atoms (prt_term o Const) prt_typ; - val prt_vars = prt_atoms prt_var prt_typ; - val prt_varsT = prt_atoms prt_varT prt_sort; - - - fun pretty_list _ _ [] = [] - | pretty_list name prt lst = [Pretty.big_list name (map prt lst)]; - - fun pretty_subgoal (n, A) = Pretty.markup markup - [Pretty.str (" " ^ string_of_int n ^ ". "), prt_term A]; - fun pretty_subgoals As = map pretty_subgoal (1 upto length As ~~ As); - - val pretty_ffpairs = pretty_list "flex-flex pairs:" (pretty_flexpair ctxt); - - val pretty_consts = pretty_list "constants:" prt_consts o consts_of; - val pretty_vars = pretty_list "variables:" prt_vars o vars_of; - val pretty_varsT = pretty_list "type variables:" prt_varsT o varsT_of; - - - val {prop, tpairs, ...} = Thm.rep_thm state; - val (As, B) = Logic.strip_horn prop; - val ngoals = length As; - - fun pretty_gs (types, sorts) = - (if main then [prt_term B] else []) @ - (if ngoals = 0 then [Pretty.str "No subgoals!"] - else if ngoals > maxgoals then - pretty_subgoals (Library.take (maxgoals, As)) @ - (if msg then [Pretty.str ("A total of " ^ string_of_int ngoals ^ " subgoals...")] - else []) - else pretty_subgoals As) @ - pretty_ffpairs tpairs @ - (if ! show_consts then pretty_consts prop else []) @ - (if types then pretty_vars prop else []) @ - (if sorts then pretty_varsT prop else []); - in - setmp show_no_free_types true - (setmp show_types (! show_types orelse ! show_sorts orelse ! show_all_types) - (setmp show_sorts false pretty_gs)) - (! show_types orelse ! show_sorts orelse ! show_all_types, ! show_sorts) - end; - -fun pretty_goals_without_context n th = - pretty_goals (Syntax.init_pretty_global (Thm.theory_of_thm th)) Markup.none (true, true) n th; - -val print_goals_without_context = - (Pretty.writeln o Pretty.chunks) oo pretty_goals_without_context; - -end; - -end; - diff -r b2e93cda0be8 -r d64a1820431d src/Pure/goal.ML --- a/src/Pure/goal.ML Sat Jul 25 18:44:55 2009 +0200 +++ b/src/Pure/goal.ML Sun Jul 26 07:54:28 2009 +0200 @@ -78,7 +78,7 @@ (case Thm.nprems_of th of 0 => conclude th | n => raise THM ("Proof failed.\n" ^ - Pretty.string_of (Pretty.chunks (Display_Goal.pretty_goals_without_context n th)) ^ + Pretty.string_of (Pretty.chunks (Goal_Display.pretty_goals_without_context n th)) ^ ("\n" ^ string_of_int n ^ " unsolved goal(s)!"), 0, [th])); diff -r b2e93cda0be8 -r d64a1820431d src/Pure/goal_display.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/goal_display.ML Sun Jul 26 07:54:28 2009 +0200 @@ -0,0 +1,124 @@ +(* Title: Pure/goal_display.ML + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Author: Makarius + +Display tactical goal state. +*) + +signature GOAL_DISPLAY = +sig + val goals_limit: int ref + val show_consts: bool ref + val pretty_flexpair: Proof.context -> term * term -> Pretty.T + val pretty_goals: Proof.context -> {total: bool, main: bool, maxgoals: int} -> + thm -> Pretty.T list + val pretty_goals_without_context: int -> thm -> Pretty.T list +end; + +structure Goal_Display: GOAL_DISPLAY = +struct + +val goals_limit = ref 10; (*max number of goals to print*) +val show_consts = ref false; (*true: show consts with types in proof state output*) + +fun pretty_flexpair ctxt (t, u) = Pretty.block + [Syntax.pretty_term ctxt t, Pretty.str " =?=", Pretty.brk 1, Syntax.pretty_term ctxt u]; + + +(*print thm A1,...,An/B in "goal style" -- premises as numbered subgoals*) + +local + +fun ins_entry (x, y) = + AList.default (op =) (x, []) #> + AList.map_entry (op =) x (insert (op =) y); + +val add_consts = Term.fold_aterms + (fn Const (c, T) => ins_entry (T, (c, T)) + | _ => I); + +val add_vars = Term.fold_aterms + (fn Free (x, T) => ins_entry (T, (x, ~1)) + | Var (xi, T) => ins_entry (T, xi) + | _ => I); + +val add_varsT = Term.fold_atyps + (fn TFree (x, S) => ins_entry (S, (x, ~1)) + | TVar (xi, S) => ins_entry (S, xi) + | _ => I); + +fun sort_idxs vs = map (apsnd (sort (prod_ord string_ord int_ord))) vs; +fun sort_cnsts cs = map (apsnd (sort_wrt fst)) cs; + +fun consts_of t = sort_cnsts (add_consts t []); +fun vars_of t = sort_idxs (add_vars t []); +fun varsT_of t = rev (sort_idxs (Term.fold_types add_varsT t [])); + +in + +fun pretty_goals ctxt {total, main, maxgoals} state = + let + val prt_sort = Syntax.pretty_sort ctxt; + val prt_typ = Syntax.pretty_typ ctxt; + val prt_term = Syntax.pretty_term ctxt; + + fun prt_atoms prt prtT (X, xs) = Pretty.block + [Pretty.block (Pretty.commas (map prt xs)), Pretty.str " ::", + Pretty.brk 1, prtT X]; + + fun prt_var (x, ~1) = prt_term (Syntax.free x) + | prt_var xi = prt_term (Syntax.var xi); + + fun prt_varT (x, ~1) = prt_typ (TFree (x, [])) + | prt_varT xi = prt_typ (TVar (xi, [])); + + val prt_consts = prt_atoms (prt_term o Const) prt_typ; + val prt_vars = prt_atoms prt_var prt_typ; + val prt_varsT = prt_atoms prt_varT prt_sort; + + + fun pretty_list _ _ [] = [] + | pretty_list name prt lst = [Pretty.big_list name (map prt lst)]; + + fun pretty_subgoal (n, A) = Pretty.markup Markup.subgoal + [Pretty.str (" " ^ string_of_int n ^ ". "), prt_term A]; + fun pretty_subgoals As = map pretty_subgoal (1 upto length As ~~ As); + + val pretty_ffpairs = pretty_list "flex-flex pairs:" (pretty_flexpair ctxt); + + val pretty_consts = pretty_list "constants:" prt_consts o consts_of; + val pretty_vars = pretty_list "variables:" prt_vars o vars_of; + val pretty_varsT = pretty_list "type variables:" prt_varsT o varsT_of; + + + val {prop, tpairs, ...} = Thm.rep_thm state; + val (As, B) = Logic.strip_horn prop; + val ngoals = length As; + + fun pretty_gs (types, sorts) = + (if main then [prt_term B] else []) @ + (if ngoals = 0 then [Pretty.str "No subgoals!"] + else if ngoals > maxgoals then + pretty_subgoals (Library.take (maxgoals, As)) @ + (if total then [Pretty.str ("A total of " ^ string_of_int ngoals ^ " subgoals...")] + else []) + else pretty_subgoals As) @ + pretty_ffpairs tpairs @ + (if ! show_consts then pretty_consts prop else []) @ + (if types then pretty_vars prop else []) @ + (if sorts then pretty_varsT prop else []); + in + setmp show_no_free_types true + (setmp show_types (! show_types orelse ! show_sorts orelse ! show_all_types) + (setmp show_sorts false pretty_gs)) + (! show_types orelse ! show_sorts orelse ! show_all_types, ! show_sorts) + end; + +fun pretty_goals_without_context n th = + pretty_goals (Syntax.init_pretty_global (Thm.theory_of_thm th)) + {total = true, main = true, maxgoals = n} th; + +end; + +end; + diff -r b2e93cda0be8 -r d64a1820431d src/Pure/library.ML --- a/src/Pure/library.ML Sat Jul 25 18:44:55 2009 +0200 +++ b/src/Pure/library.ML Sun Jul 26 07:54:28 2009 +0200 @@ -109,7 +109,6 @@ val split_list: ('a * 'b) list -> 'a list * 'b list val map_product: ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list val fold_product: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c - val multiply: 'a list -> 'a list list -> 'a list list val separate: 'a -> 'a list -> 'a list val surround: 'a -> 'a list -> 'a list val replicate: int -> 'a -> 'a list @@ -552,9 +551,6 @@ else rep (n, []) end; -(*multiply [a, b, c, ...] * [xs, ys, zs, ...]*) -fun multiply [] _ = [] - | multiply (x :: xs) yss = map (cons x) yss @ multiply xs yss; (* direct product *) @@ -1138,5 +1134,5 @@ end; -structure BasicLibrary: BASIC_LIBRARY = Library; -open BasicLibrary; +structure Basic_Library: BASIC_LIBRARY = Library; +open Basic_Library; diff -r b2e93cda0be8 -r d64a1820431d src/Pure/old_goals.ML --- a/src/Pure/old_goals.ML Sat Jul 25 18:44:55 2009 +0200 +++ b/src/Pure/old_goals.ML Sun Jul 26 07:54:28 2009 +0200 @@ -8,28 +8,47 @@ may be a stack of pending proofs. *) -signature GOALS = +signature OLD_GOALS = sig - val the_context: unit -> theory + val simple_read_term: theory -> typ -> string -> term + val read_term: theory -> string -> term + val read_prop: theory -> string -> term + type proof val premises: unit -> thm list + val reset_goals: unit -> unit + val result_error_fn: (thm -> string -> thm) ref + val print_sign_exn: theory -> exn -> 'a + val prove_goalw_cterm: thm list->cterm->(thm list->tactic list)->thm + val prove_goalw_cterm_nocheck: thm list->cterm->(thm list->tactic list)->thm + val prove_goalw: theory -> thm list -> string -> (thm list -> tactic list) -> thm val prove_goal: theory -> string -> (thm list -> tactic list) -> thm - val prove_goalw: theory -> thm list -> string -> (thm list -> tactic list) -> thm val topthm: unit -> thm val result: unit -> thm val uresult: unit -> thm val getgoal: int -> term val gethyps: int -> thm list + val print_exn: exn -> 'a + val filter_goal: (term*term->bool) -> thm list -> int -> thm list val prlev: int -> unit val pr: unit -> unit val prlim: int -> unit + val goalw_cterm: thm list -> cterm -> thm list + val goalw: theory -> thm list -> string -> thm list val goal: theory -> string -> thm list - val goalw: theory -> thm list -> string -> thm list + val Goalw: thm list -> string -> thm list val Goal: string -> thm list - val Goalw: thm list -> string -> thm list + val simple_prove_goal_cterm: cterm->(thm list->tactic list)->thm val by: tactic -> unit + val byev: tactic list -> unit val back: unit -> unit val choplev: int -> unit + val chop: unit -> unit val undo: unit -> unit + val save_proof: unit -> proof + val restore_proof: proof -> thm list + val push_proof: unit -> unit + val pop_proof: unit -> thm list + val rotate_proof: unit -> thm list val qed: string -> unit val qed_goal: string -> theory -> string -> (thm list -> tactic list) -> unit val qed_goalw: string -> theory -> thm list -> string @@ -40,39 +59,9 @@ -> (thm list -> tactic list) -> unit end; -signature OLD_GOALS = -sig - include GOALS - val simple_read_term: theory -> typ -> string -> term - val read_term: theory -> string -> term - val read_prop: theory -> string -> term - type proof - val chop: unit -> unit - val reset_goals: unit -> unit - val result_error_fn: (thm -> string -> thm) ref - val print_sign_exn: theory -> exn -> 'a - val prove_goalw_cterm: thm list->cterm->(thm list->tactic list)->thm - val prove_goalw_cterm_nocheck: thm list->cterm->(thm list->tactic list)->thm - val print_exn: exn -> 'a - val filter_goal: (term*term->bool) -> thm list -> int -> thm list - val goalw_cterm: thm list -> cterm -> thm list - val simple_prove_goal_cterm: cterm->(thm list->tactic list)->thm - val byev: tactic list -> unit - val save_proof: unit -> proof - val restore_proof: proof -> thm list - val push_proof: unit -> unit - val pop_proof: unit -> thm list - val rotate_proof: unit -> thm list -end; - structure OldGoals: OLD_GOALS = struct -(* global context *) - -val the_context = ML_Context.the_global_context; - - (* old ways of reading terms *) fun simple_read_term thy T s = @@ -136,7 +125,7 @@ special applications.*) fun result_error_default state msg : thm = Pretty.str "Bad final proof state:" :: - Display_Goal.pretty_goals_without_context (!goals_limit) state @ + Goal_Display.pretty_goals_without_context (!goals_limit) state @ [Pretty.str msg, Pretty.str "Proof failed!"] |> Pretty.chunks |> Pretty.string_of |> error; val result_error_fn = ref result_error_default; @@ -278,7 +267,7 @@ (if ngoals > 0 then " (" ^ string_of_int ngoals ^ " subgoal" ^ (if ngoals <> 1 then "s" else "") ^ ")" else ""))] @ - Display_Goal.pretty_goals_without_context m th + Goal_Display.pretty_goals_without_context m th end |> Pretty.chunks |> Pretty.writeln; (*Printing can raise exceptions, so the assignment occurs last. @@ -457,12 +446,13 @@ in proofstack := ps; pr(); prems end; (* rotate the stack so that the top element goes to the bottom *) -fun rotate_proof() = let val (p,ps) = top_proof() - in proofstack := ps@[save_proof()]; - restore_proof p; - pr(); - !curr_prems - end; +fun rotate_proof() = + let val (p,ps) = top_proof() + in proofstack := ps@[save_proof()]; + restore_proof p; + pr(); + !curr_prems + end; (** theorem bindings **) @@ -480,5 +470,3 @@ end; -structure Goals: GOALS = OldGoals; -open Goals; diff -r b2e93cda0be8 -r d64a1820431d src/Pure/proofterm.ML --- a/src/Pure/proofterm.ML Sat Jul 25 18:44:55 2009 +0200 +++ b/src/Pure/proofterm.ML Sun Jul 26 07:54:28 2009 +0200 @@ -1334,8 +1334,7 @@ fun get_name hyps prop prf = let val prop = Logic.list_implies (hyps, prop) in (case strip_combt (fst (strip_combP prf)) of - (PAxm (name, prop', _), _) => if prop = prop' then name else "" (* FIXME !? *) - | (PThm (_, ((name, prop', _), _)), _) => if prop = prop' then name else "" + (PThm (_, ((name, prop', _), _)), _) => if prop = prop' then name else "" | _ => "") end; diff -r b2e93cda0be8 -r d64a1820431d src/Pure/tactical.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/tactical.ML Sun Jul 26 07:54:28 2009 +0200 @@ -0,0 +1,524 @@ +(* Title: Pure/tactical.ML + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + +Tacticals. +*) + +infix 1 THEN THEN' THEN_ALL_NEW; +infix 0 ORELSE APPEND INTLEAVE ORELSE' APPEND' INTLEAVE'; +infix 0 THEN_ELSE; + +signature TACTICAL = +sig + type tactic = thm -> thm Seq.seq + val THEN: tactic * tactic -> tactic + val ORELSE: tactic * tactic -> tactic + val APPEND: tactic * tactic -> tactic + val INTLEAVE: tactic * tactic -> tactic + val THEN_ELSE: tactic * (tactic*tactic) -> tactic + val THEN': ('a -> tactic) * ('a -> tactic) -> 'a -> tactic + val ORELSE': ('a -> tactic) * ('a -> tactic) -> 'a -> tactic + val APPEND': ('a -> tactic) * ('a -> tactic) -> 'a -> tactic + val INTLEAVE': ('a -> tactic) * ('a -> tactic) -> 'a -> tactic + val all_tac: tactic + val no_tac: tactic + val DETERM: tactic -> tactic + val COND: (thm -> bool) -> tactic -> tactic -> tactic + val TRY: tactic -> tactic + val EVERY: tactic list -> tactic + val EVERY': ('a -> tactic) list -> 'a -> tactic + val EVERY1: (int -> tactic) list -> tactic + val FIRST: tactic list -> tactic + val FIRST': ('a -> tactic) list -> 'a -> tactic + val FIRST1: (int -> tactic) list -> tactic + val RANGE: (int -> tactic) list -> int -> tactic + val print_tac: string -> tactic + val pause_tac: tactic + val trace_REPEAT: bool ref + val suppress_tracing: bool ref + val tracify: bool ref -> tactic -> tactic + val traced_tac: (thm -> (thm * thm Seq.seq) option) -> tactic + val DETERM_UNTIL: (thm -> bool) -> tactic -> tactic + val REPEAT_DETERM_N: int -> tactic -> tactic + val REPEAT_DETERM: tactic -> tactic + val REPEAT: tactic -> tactic + val REPEAT_DETERM1: tactic -> tactic + val REPEAT1: tactic -> tactic + val FILTER: (thm -> bool) -> tactic -> tactic + val CHANGED: tactic -> tactic + val CHANGED_PROP: tactic -> tactic + val ALLGOALS: (int -> tactic) -> tactic + val SOMEGOAL: (int -> tactic) -> tactic + val FIRSTGOAL: (int -> tactic) -> tactic + val REPEAT_SOME: (int -> tactic) -> tactic + val REPEAT_DETERM_SOME: (int -> tactic) -> tactic + val REPEAT_FIRST: (int -> tactic) -> tactic + val REPEAT_DETERM_FIRST: (int -> tactic) -> tactic + val TRYALL: (int -> tactic) -> tactic + val CSUBGOAL: ((cterm * int) -> tactic) -> int -> tactic + val SUBGOAL: ((term * int) -> tactic) -> int -> tactic + val CHANGED_GOAL: (int -> tactic) -> int -> tactic + val THEN_ALL_NEW: (int -> tactic) * (int -> tactic) -> int -> tactic + val REPEAT_ALL_NEW: (int -> tactic) -> int -> tactic + val strip_context: term -> (string * typ) list * term list * term + val metahyps_thms: int -> thm -> thm list option + val METAHYPS: (thm list -> tactic) -> int -> tactic + val PRIMSEQ: (thm -> thm Seq.seq) -> tactic + val PRIMITIVE: (thm -> thm) -> tactic + val SINGLE: tactic -> thm -> thm option + val CONVERSION: conv -> int -> tactic +end; + +structure Tactical : TACTICAL = +struct + +(**** Tactics ****) + +(*A tactic maps a proof tree to a sequence of proof trees: + if length of sequence = 0 then the tactic does not apply; + if length > 1 then backtracking on the alternatives can occur.*) + +type tactic = thm -> thm Seq.seq; + + +(*** LCF-style tacticals ***) + +(*the tactical THEN performs one tactic followed by another*) +fun (tac1 THEN tac2) st = Seq.maps tac2 (tac1 st); + + +(*The tactical ORELSE uses the first tactic that returns a nonempty sequence. + Like in LCF, ORELSE commits to either tac1 or tac2 immediately. + Does not backtrack to tac2 if tac1 was initially chosen. *) +fun (tac1 ORELSE tac2) st = + case Seq.pull(tac1 st) of + NONE => tac2 st + | sequencecell => Seq.make(fn()=> sequencecell); + + +(*The tactical APPEND combines the results of two tactics. + Like ORELSE, but allows backtracking on both tac1 and tac2. + The tactic tac2 is not applied until needed.*) +fun (tac1 APPEND tac2) st = + Seq.append (tac1 st) (Seq.make(fn()=> Seq.pull (tac2 st))); + +(*Like APPEND, but interleaves results of tac1 and tac2.*) +fun (tac1 INTLEAVE tac2) st = + Seq.interleave(tac1 st, + Seq.make(fn()=> Seq.pull (tac2 st))); + +(*Conditional tactic. + tac1 ORELSE tac2 = tac1 THEN_ELSE (all_tac, tac2) + tac1 THEN tac2 = tac1 THEN_ELSE (tac2, no_tac) +*) +fun (tac THEN_ELSE (tac1, tac2)) st = + case Seq.pull(tac st) of + NONE => tac2 st (*failed; try tactic 2*) + | seqcell => Seq.maps tac1 (Seq.make(fn()=> seqcell)); (*succeeded; use tactic 1*) + + +(*Versions for combining tactic-valued functions, as in + SOMEGOAL (resolve_tac rls THEN' assume_tac) *) +fun (tac1 THEN' tac2) x = tac1 x THEN tac2 x; +fun (tac1 ORELSE' tac2) x = tac1 x ORELSE tac2 x; +fun (tac1 APPEND' tac2) x = tac1 x APPEND tac2 x; +fun (tac1 INTLEAVE' tac2) x = tac1 x INTLEAVE tac2 x; + +(*passes all proofs through unchanged; identity of THEN*) +fun all_tac st = Seq.single st; + +(*passes no proofs through; identity of ORELSE and APPEND*) +fun no_tac st = Seq.empty; + + +(*Make a tactic deterministic by chopping the tail of the proof sequence*) +fun DETERM tac = Seq.DETERM tac; + +(*Conditional tactical: testfun controls which tactic to use next. + Beware: due to eager evaluation, both thentac and elsetac are evaluated.*) +fun COND testfun thenf elsef = (fn prf => + if testfun prf then thenf prf else elsef prf); + +(*Do the tactic or else do nothing*) +fun TRY tac = tac ORELSE all_tac; + +(*** List-oriented tactics ***) + +local + (*This version of EVERY avoids backtracking over repeated states*) + + fun EVY (trail, []) st = + Seq.make (fn()=> SOME(st, + Seq.make (fn()=> Seq.pull (evyBack trail)))) + | EVY (trail, tac::tacs) st = + case Seq.pull(tac st) of + NONE => evyBack trail (*failed: backtrack*) + | SOME(st',q) => EVY ((st',q,tacs)::trail, tacs) st' + and evyBack [] = Seq.empty (*no alternatives*) + | evyBack ((st',q,tacs)::trail) = + case Seq.pull q of + NONE => evyBack trail + | SOME(st,q') => if Thm.eq_thm (st',st) + then evyBack ((st',q',tacs)::trail) + else EVY ((st,q',tacs)::trail, tacs) st +in + +(* EVERY [tac1,...,tacn] equals tac1 THEN ... THEN tacn *) +fun EVERY tacs = EVY ([], tacs); +end; + + +(* EVERY' [tac1,...,tacn] i equals tac1 i THEN ... THEN tacn i *) +fun EVERY' tacs i = EVERY (map (fn f => f i) tacs); + +(*Apply every tactic to 1*) +fun EVERY1 tacs = EVERY' tacs 1; + +(* FIRST [tac1,...,tacn] equals tac1 ORELSE ... ORELSE tacn *) +fun FIRST tacs = fold_rev (curry op ORELSE) tacs no_tac; + +(* FIRST' [tac1,...,tacn] i equals tac1 i ORELSE ... ORELSE tacn i *) +fun FIRST' tacs = fold_rev (curry op ORELSE') tacs (K no_tac); + +(*Apply first tactic to 1*) +fun FIRST1 tacs = FIRST' tacs 1; + +(*Apply tactics on consecutive subgoals*) +fun RANGE [] _ = all_tac + | RANGE (tac :: tacs) i = RANGE tacs (i + 1) THEN tac i; + + +(*** Tracing tactics ***) + +(*Print the current proof state and pass it on.*) +fun print_tac msg st = + (tracing (msg ^ "\n" ^ + Pretty.string_of (Pretty.chunks + (Goal_Display.pretty_goals_without_context (! Goal_Display.goals_limit) st))); + Seq.single st); + +(*Pause until a line is typed -- if non-empty then fail. *) +fun pause_tac st = + (tracing "** Press RETURN to continue:"; + if TextIO.inputLine TextIO.stdIn = SOME "\n" then Seq.single st + else (tracing "Goodbye"; Seq.empty)); + +exception TRACE_EXIT of thm +and TRACE_QUIT; + +(*Tracing flags*) +val trace_REPEAT= ref false +and suppress_tracing = ref false; + +(*Handle all tracing commands for current state and tactic *) +fun exec_trace_command flag (tac, st) = + case TextIO.inputLine TextIO.stdIn of + SOME "\n" => tac st + | SOME "f\n" => Seq.empty + | SOME "o\n" => (flag:=false; tac st) + | SOME "s\n" => (suppress_tracing:=true; tac st) + | SOME "x\n" => (tracing "Exiting now"; raise (TRACE_EXIT st)) + | SOME "quit\n" => raise TRACE_QUIT + | _ => (tracing +"Type RETURN to continue or...\n\ +\ f - to fail here\n\ +\ o - to switch tracing off\n\ +\ s - to suppress tracing until next entry to a tactical\n\ +\ x - to exit at this point\n\ +\ quit - to abort this tracing run\n\ +\** Well? " ; exec_trace_command flag (tac, st)); + + +(*Extract from a tactic, a thm->thm seq function that handles tracing*) +fun tracify flag tac st = + if !flag andalso not (!suppress_tracing) then + (tracing (Pretty.string_of (Pretty.chunks + (Goal_Display.pretty_goals_without_context (! Goal_Display.goals_limit) st @ + [Pretty.str "** Press RETURN to continue:"]))); + exec_trace_command flag (tac, st)) + else tac st; + +(*Create a tactic whose outcome is given by seqf, handling TRACE_EXIT*) +fun traced_tac seqf st = + (suppress_tracing := false; + Seq.make (fn()=> seqf st + handle TRACE_EXIT st' => SOME(st', Seq.empty))); + + +(*Deterministic DO..UNTIL: only retains the first outcome; tail recursive. + Forces repitition until predicate on state is fulfilled.*) +fun DETERM_UNTIL p tac = +let val tac = tracify trace_REPEAT tac + fun drep st = if p st then SOME (st, Seq.empty) + else (case Seq.pull(tac st) of + NONE => NONE + | SOME(st',_) => drep st') +in traced_tac drep end; + +(*Deterministic REPEAT: only retains the first outcome; + uses less space than REPEAT; tail recursive. + If non-negative, n bounds the number of repetitions.*) +fun REPEAT_DETERM_N n tac = + let val tac = tracify trace_REPEAT tac + fun drep 0 st = SOME(st, Seq.empty) + | drep n st = + (case Seq.pull(tac st) of + NONE => SOME(st, Seq.empty) + | SOME(st',_) => drep (n-1) st') + in traced_tac (drep n) end; + +(*Allows any number of repetitions*) +val REPEAT_DETERM = REPEAT_DETERM_N ~1; + +(*General REPEAT: maintains a stack of alternatives; tail recursive*) +fun REPEAT tac = + let val tac = tracify trace_REPEAT tac + fun rep qs st = + case Seq.pull(tac st) of + NONE => SOME(st, Seq.make(fn()=> repq qs)) + | SOME(st',q) => rep (q::qs) st' + and repq [] = NONE + | repq(q::qs) = case Seq.pull q of + NONE => repq qs + | SOME(st,q) => rep (q::qs) st + in traced_tac (rep []) end; + +(*Repeat 1 or more times*) +fun REPEAT_DETERM1 tac = DETERM tac THEN REPEAT_DETERM tac; +fun REPEAT1 tac = tac THEN REPEAT tac; + + +(** Filtering tacticals **) + +fun FILTER pred tac st = Seq.filter pred (tac st); + +(*Accept only next states that change the theorem somehow*) +fun CHANGED tac st = + let fun diff st' = not (Thm.eq_thm (st, st')); + in Seq.filter diff (tac st) end; + +(*Accept only next states that change the theorem's prop field + (changes to signature, hyps, etc. don't count)*) +fun CHANGED_PROP tac st = + let fun diff st' = not (Thm.eq_thm_prop (st, st')); + in Seq.filter diff (tac st) end; + + +(*** Tacticals based on subgoal numbering ***) + +(*For n subgoals, performs tac(n) THEN ... THEN tac(1) + Essential to work backwards since tac(i) may add/delete subgoals at i. *) +fun ALLGOALS tac st = + let fun doall 0 = all_tac + | doall n = tac(n) THEN doall(n-1) + in doall(nprems_of st)st end; + +(*For n subgoals, performs tac(n) ORELSE ... ORELSE tac(1) *) +fun SOMEGOAL tac st = + let fun find 0 = no_tac + | find n = tac(n) ORELSE find(n-1) + in find(nprems_of st)st end; + +(*For n subgoals, performs tac(1) ORELSE ... ORELSE tac(n). + More appropriate than SOMEGOAL in some cases.*) +fun FIRSTGOAL tac st = + let fun find (i,n) = if i>n then no_tac else tac(i) ORELSE find (i+1,n) + in find(1, nprems_of st)st end; + +(*Repeatedly solve some using tac. *) +fun REPEAT_SOME tac = REPEAT1 (SOMEGOAL (REPEAT1 o tac)); +fun REPEAT_DETERM_SOME tac = REPEAT_DETERM1 (SOMEGOAL (REPEAT_DETERM1 o tac)); + +(*Repeatedly solve the first possible subgoal using tac. *) +fun REPEAT_FIRST tac = REPEAT1 (FIRSTGOAL (REPEAT1 o tac)); +fun REPEAT_DETERM_FIRST tac = REPEAT_DETERM1 (FIRSTGOAL (REPEAT_DETERM1 o tac)); + +(*For n subgoals, tries to apply tac to n,...1 *) +fun TRYALL tac = ALLGOALS (TRY o tac); + + +(*Make a tactic for subgoal i, if there is one. *) +fun CSUBGOAL goalfun i st = + (case SOME (Thm.cprem_of st i) handle THM _ => NONE of + SOME goal => goalfun (goal, i) st + | NONE => Seq.empty); + +fun SUBGOAL goalfun = + CSUBGOAL (fn (goal, i) => goalfun (Thm.term_of goal, i)); + +(*Returns all states that have changed in subgoal i, counted from the LAST + subgoal. For stac, for example.*) +fun CHANGED_GOAL tac i st = + let val np = Thm.nprems_of st + val d = np-i (*distance from END*) + val t = Thm.term_of (Thm.cprem_of st i) + fun diff st' = + Thm.nprems_of st' - d <= 0 (*the subgoal no longer exists*) + orelse + not (Pattern.aeconv (t, Thm.term_of (Thm.cprem_of st' (Thm.nprems_of st' - d)))) + in Seq.filter diff (tac i st) end + handle Subscript => Seq.empty (*no subgoal i*); + +fun (tac1 THEN_ALL_NEW tac2) i st = + st |> (tac1 i THEN (fn st' => Seq.INTERVAL tac2 i (i + nprems_of st' - nprems_of st) st')); + +(*repeatedly dig into any emerging subgoals*) +fun REPEAT_ALL_NEW tac = + tac THEN_ALL_NEW (TRY o (fn i => REPEAT_ALL_NEW tac i)); + + +(*Strips assumptions in goal yielding ( [x1,...,xm], [H1,...,Hn], B ) + H1,...,Hn are the hypotheses; x1...xm are variants of the parameters. + Main difference from strip_assums concerns parameters: + it replaces the bound variables by free variables. *) +fun strip_context_aux (params, Hs, Const("==>", _) $ H $ B) = + strip_context_aux (params, H::Hs, B) + | strip_context_aux (params, Hs, Const("all",_)$Abs(a,T,t)) = + let val (b,u) = Syntax.variant_abs(a,T,t) + in strip_context_aux ((b,T)::params, Hs, u) end + | strip_context_aux (params, Hs, B) = (rev params, rev Hs, B); + +fun strip_context A = strip_context_aux ([],[],A); + + +(**** METAHYPS -- tactical for using hypotheses as meta-level assumptions + METAHYPS (fn prems => tac prems) i + +converts subgoal i, of the form !!x1...xm. [| A1;...;An] ==> A into a new +proof state A==>A, supplying A1,...,An as meta-level assumptions (in +"prems"). The parameters x1,...,xm become free variables. If the +resulting proof state is [| B1;...;Bk] ==> C (possibly assuming A1,...,An) +then it is lifted back into the original context, yielding k subgoals. + +Replaces unknowns in the context by Frees having the prefix METAHYP_ +New unknowns in [| B1;...;Bk] ==> C are lifted over x1,...,xm. +DOES NOT HANDLE TYPE UNKNOWNS. +****) + +local + + (*Left-to-right replacements: ctpairs = [...,(vi,ti),...]. + Instantiates distinct free variables by terms of same type.*) + fun free_instantiate ctpairs = + forall_elim_list (map snd ctpairs) o forall_intr_list (map fst ctpairs); + + fun free_of s ((a, i), T) = + Free (s ^ (case i of 0 => a | _ => a ^ "_" ^ string_of_int i), T) + + fun mk_inst v = (Var v, free_of "METAHYP1_" v) +in + +(*Common code for METAHYPS and metahyps_thms*) +fun metahyps_split_prem prem = + let (*find all vars in the hyps -- should find tvars also!*) + val hyps_vars = fold Term.add_vars (Logic.strip_assums_hyp prem) [] + val insts = map mk_inst hyps_vars + (*replace the hyps_vars by Frees*) + val prem' = subst_atomic insts prem + val (params,hyps,concl) = strip_context prem' + in (insts,params,hyps,concl) end; + +fun metahyps_aux_tac tacf (prem,gno) state = + let val (insts,params,hyps,concl) = metahyps_split_prem prem + val maxidx = Thm.maxidx_of state + val cterm = Thm.cterm_of (Thm.theory_of_thm state) + val chyps = map cterm hyps + val hypths = map assume chyps + val subprems = map (Thm.forall_elim_vars 0) hypths + val fparams = map Free params + val cparams = map cterm fparams + fun swap_ctpair (t,u) = (cterm u, cterm t) + (*Subgoal variables: make Free; lift type over params*) + fun mk_subgoal_inst concl_vars (v, T) = + if member (op =) concl_vars (v, T) + then ((v, T), true, free_of "METAHYP2_" (v, T)) + else ((v, T), false, free_of "METAHYP2_" (v, map #2 params ---> T)) + (*Instantiate subgoal vars by Free applied to params*) + fun mk_ctpair (v, in_concl, u) = + if in_concl then (cterm (Var v), cterm u) + else (cterm (Var v), cterm (list_comb (u, fparams))) + (*Restore Vars with higher type and index*) + fun mk_subgoal_swap_ctpair (((a, i), T), in_concl, u as Free (_, U)) = + if in_concl then (cterm u, cterm (Var ((a, i), T))) + else (cterm u, cterm (Var ((a, i + maxidx), U))) + (*Embed B in the original context of params and hyps*) + fun embed B = list_all_free (params, Logic.list_implies (hyps, B)) + (*Strip the context using elimination rules*) + fun elim Bhyp = implies_elim_list (forall_elim_list cparams Bhyp) hypths + (*A form of lifting that discharges assumptions.*) + fun relift st = + let val prop = Thm.prop_of st + val subgoal_vars = (*Vars introduced in the subgoals*) + fold Term.add_vars (Logic.strip_imp_prems prop) [] + and concl_vars = Term.add_vars (Logic.strip_imp_concl prop) [] + val subgoal_insts = map (mk_subgoal_inst concl_vars) subgoal_vars + val st' = Thm.instantiate ([], map mk_ctpair subgoal_insts) st + val emBs = map (cterm o embed) (prems_of st') + val Cth = implies_elim_list st' (map (elim o assume) emBs) + in (*restore the unknowns to the hypotheses*) + free_instantiate (map swap_ctpair insts @ + map mk_subgoal_swap_ctpair subgoal_insts) + (*discharge assumptions from state in same order*) + (implies_intr_list emBs + (forall_intr_list cparams (implies_intr_list chyps Cth))) + end + (*function to replace the current subgoal*) + fun next st = Thm.bicompose false (false, relift st, nprems_of st) gno state + in Seq.maps next (tacf subprems (trivial (cterm concl))) end; + +end; + +(*Returns the theorem list that METAHYPS would supply to its tactic*) +fun metahyps_thms i state = + let val prem = Logic.nth_prem (i, Thm.prop_of state) + and cterm = cterm_of (Thm.theory_of_thm state) + val (_,_,hyps,_) = metahyps_split_prem prem + in SOME (map (Thm.forall_elim_vars 0 o Thm.assume o cterm) hyps) end + handle TERM ("nth_prem", [A]) => NONE; + +local + +fun print_vars_terms thy (n,thm) = + let + fun typed ty = " has type: " ^ Syntax.string_of_typ_global thy ty; + fun find_vars thy (Const (c, ty)) = + if null (Term.add_tvarsT ty []) then I + else insert (op =) (c ^ typed ty) + | find_vars thy (Var (xi, ty)) = insert (op =) (Term.string_of_vname xi ^ typed ty) + | find_vars _ (Free _) = I + | find_vars _ (Bound _) = I + | find_vars thy (Abs (_, _, t)) = find_vars thy t + | find_vars thy (t1 $ t2) = + find_vars thy t1 #> find_vars thy t1; + val prem = Logic.nth_prem (n, Thm.prop_of thm) + val tms = find_vars thy prem [] + in + (warning "Found schematic vars in assumptions:"; warning (cat_lines tms)) + end; + +in + +fun METAHYPS tacf n thm = SUBGOAL (metahyps_aux_tac tacf) n thm + handle THM("assume: variables",_,_) => (print_vars_terms (theory_of_thm thm) (n,thm); Seq.empty) + +end; + +(*Makes a tactic whose effect on a state is given by thmfun: thm->thm seq.*) +fun PRIMSEQ thmfun st = thmfun st handle THM _ => Seq.empty; + +(*Makes a tactic whose effect on a state is given by thmfun: thm->thm.*) +fun PRIMITIVE thmfun = PRIMSEQ (Seq.single o thmfun); + +(*Inverse (more or less) of PRIMITIVE*) +fun SINGLE tacf = Option.map fst o Seq.pull o tacf + +(*Conversions as tactics*) +fun CONVERSION cv i st = Seq.single (Conv.gconv_rule cv i st) + handle THM _ => Seq.empty + | CTERM _ => Seq.empty + | TERM _ => Seq.empty + | TYPE _ => Seq.empty; + +end; + +open Tactical; diff -r b2e93cda0be8 -r d64a1820431d src/Pure/tctical.ML --- a/src/Pure/tctical.ML Sat Jul 25 18:44:55 2009 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,523 +0,0 @@ -(* Title: Pure/tctical.ML - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - -Tacticals. -*) - -infix 1 THEN THEN' THEN_ALL_NEW; -infix 0 ORELSE APPEND INTLEAVE ORELSE' APPEND' INTLEAVE'; -infix 0 THEN_ELSE; - -signature TACTICAL = -sig - type tactic = thm -> thm Seq.seq - val THEN: tactic * tactic -> tactic - val ORELSE: tactic * tactic -> tactic - val APPEND: tactic * tactic -> tactic - val INTLEAVE: tactic * tactic -> tactic - val THEN_ELSE: tactic * (tactic*tactic) -> tactic - val THEN': ('a -> tactic) * ('a -> tactic) -> 'a -> tactic - val ORELSE': ('a -> tactic) * ('a -> tactic) -> 'a -> tactic - val APPEND': ('a -> tactic) * ('a -> tactic) -> 'a -> tactic - val INTLEAVE': ('a -> tactic) * ('a -> tactic) -> 'a -> tactic - val all_tac: tactic - val no_tac: tactic - val DETERM: tactic -> tactic - val COND: (thm -> bool) -> tactic -> tactic -> tactic - val TRY: tactic -> tactic - val EVERY: tactic list -> tactic - val EVERY': ('a -> tactic) list -> 'a -> tactic - val EVERY1: (int -> tactic) list -> tactic - val FIRST: tactic list -> tactic - val FIRST': ('a -> tactic) list -> 'a -> tactic - val FIRST1: (int -> tactic) list -> tactic - val RANGE: (int -> tactic) list -> int -> tactic - val print_tac: string -> tactic - val pause_tac: tactic - val trace_REPEAT: bool ref - val suppress_tracing: bool ref - val tracify: bool ref -> tactic -> tactic - val traced_tac: (thm -> (thm * thm Seq.seq) option) -> tactic - val DETERM_UNTIL: (thm -> bool) -> tactic -> tactic - val REPEAT_DETERM_N: int -> tactic -> tactic - val REPEAT_DETERM: tactic -> tactic - val REPEAT: tactic -> tactic - val REPEAT_DETERM1: tactic -> tactic - val REPEAT1: tactic -> tactic - val FILTER: (thm -> bool) -> tactic -> tactic - val CHANGED: tactic -> tactic - val CHANGED_PROP: tactic -> tactic - val ALLGOALS: (int -> tactic) -> tactic - val SOMEGOAL: (int -> tactic) -> tactic - val FIRSTGOAL: (int -> tactic) -> tactic - val REPEAT_SOME: (int -> tactic) -> tactic - val REPEAT_DETERM_SOME: (int -> tactic) -> tactic - val REPEAT_FIRST: (int -> tactic) -> tactic - val REPEAT_DETERM_FIRST: (int -> tactic) -> tactic - val TRYALL: (int -> tactic) -> tactic - val CSUBGOAL: ((cterm * int) -> tactic) -> int -> tactic - val SUBGOAL: ((term * int) -> tactic) -> int -> tactic - val CHANGED_GOAL: (int -> tactic) -> int -> tactic - val THEN_ALL_NEW: (int -> tactic) * (int -> tactic) -> int -> tactic - val REPEAT_ALL_NEW: (int -> tactic) -> int -> tactic - val strip_context: term -> (string * typ) list * term list * term - val metahyps_thms: int -> thm -> thm list option - val METAHYPS: (thm list -> tactic) -> int -> tactic - val PRIMSEQ: (thm -> thm Seq.seq) -> tactic - val PRIMITIVE: (thm -> thm) -> tactic - val SINGLE: tactic -> thm -> thm option - val CONVERSION: conv -> int -> tactic -end; - -structure Tactical : TACTICAL = -struct - -(**** Tactics ****) - -(*A tactic maps a proof tree to a sequence of proof trees: - if length of sequence = 0 then the tactic does not apply; - if length > 1 then backtracking on the alternatives can occur.*) - -type tactic = thm -> thm Seq.seq; - - -(*** LCF-style tacticals ***) - -(*the tactical THEN performs one tactic followed by another*) -fun (tac1 THEN tac2) st = Seq.maps tac2 (tac1 st); - - -(*The tactical ORELSE uses the first tactic that returns a nonempty sequence. - Like in LCF, ORELSE commits to either tac1 or tac2 immediately. - Does not backtrack to tac2 if tac1 was initially chosen. *) -fun (tac1 ORELSE tac2) st = - case Seq.pull(tac1 st) of - NONE => tac2 st - | sequencecell => Seq.make(fn()=> sequencecell); - - -(*The tactical APPEND combines the results of two tactics. - Like ORELSE, but allows backtracking on both tac1 and tac2. - The tactic tac2 is not applied until needed.*) -fun (tac1 APPEND tac2) st = - Seq.append (tac1 st) (Seq.make(fn()=> Seq.pull (tac2 st))); - -(*Like APPEND, but interleaves results of tac1 and tac2.*) -fun (tac1 INTLEAVE tac2) st = - Seq.interleave(tac1 st, - Seq.make(fn()=> Seq.pull (tac2 st))); - -(*Conditional tactic. - tac1 ORELSE tac2 = tac1 THEN_ELSE (all_tac, tac2) - tac1 THEN tac2 = tac1 THEN_ELSE (tac2, no_tac) -*) -fun (tac THEN_ELSE (tac1, tac2)) st = - case Seq.pull(tac st) of - NONE => tac2 st (*failed; try tactic 2*) - | seqcell => Seq.maps tac1 (Seq.make(fn()=> seqcell)); (*succeeded; use tactic 1*) - - -(*Versions for combining tactic-valued functions, as in - SOMEGOAL (resolve_tac rls THEN' assume_tac) *) -fun (tac1 THEN' tac2) x = tac1 x THEN tac2 x; -fun (tac1 ORELSE' tac2) x = tac1 x ORELSE tac2 x; -fun (tac1 APPEND' tac2) x = tac1 x APPEND tac2 x; -fun (tac1 INTLEAVE' tac2) x = tac1 x INTLEAVE tac2 x; - -(*passes all proofs through unchanged; identity of THEN*) -fun all_tac st = Seq.single st; - -(*passes no proofs through; identity of ORELSE and APPEND*) -fun no_tac st = Seq.empty; - - -(*Make a tactic deterministic by chopping the tail of the proof sequence*) -fun DETERM tac = Seq.DETERM tac; - -(*Conditional tactical: testfun controls which tactic to use next. - Beware: due to eager evaluation, both thentac and elsetac are evaluated.*) -fun COND testfun thenf elsef = (fn prf => - if testfun prf then thenf prf else elsef prf); - -(*Do the tactic or else do nothing*) -fun TRY tac = tac ORELSE all_tac; - -(*** List-oriented tactics ***) - -local - (*This version of EVERY avoids backtracking over repeated states*) - - fun EVY (trail, []) st = - Seq.make (fn()=> SOME(st, - Seq.make (fn()=> Seq.pull (evyBack trail)))) - | EVY (trail, tac::tacs) st = - case Seq.pull(tac st) of - NONE => evyBack trail (*failed: backtrack*) - | SOME(st',q) => EVY ((st',q,tacs)::trail, tacs) st' - and evyBack [] = Seq.empty (*no alternatives*) - | evyBack ((st',q,tacs)::trail) = - case Seq.pull q of - NONE => evyBack trail - | SOME(st,q') => if Thm.eq_thm (st',st) - then evyBack ((st',q',tacs)::trail) - else EVY ((st,q',tacs)::trail, tacs) st -in - -(* EVERY [tac1,...,tacn] equals tac1 THEN ... THEN tacn *) -fun EVERY tacs = EVY ([], tacs); -end; - - -(* EVERY' [tac1,...,tacn] i equals tac1 i THEN ... THEN tacn i *) -fun EVERY' tacs i = EVERY (map (fn f => f i) tacs); - -(*Apply every tactic to 1*) -fun EVERY1 tacs = EVERY' tacs 1; - -(* FIRST [tac1,...,tacn] equals tac1 ORELSE ... ORELSE tacn *) -fun FIRST tacs = fold_rev (curry op ORELSE) tacs no_tac; - -(* FIRST' [tac1,...,tacn] i equals tac1 i ORELSE ... ORELSE tacn i *) -fun FIRST' tacs = fold_rev (curry op ORELSE') tacs (K no_tac); - -(*Apply first tactic to 1*) -fun FIRST1 tacs = FIRST' tacs 1; - -(*Apply tactics on consecutive subgoals*) -fun RANGE [] _ = all_tac - | RANGE (tac :: tacs) i = RANGE tacs (i + 1) THEN tac i; - - -(*** Tracing tactics ***) - -(*Print the current proof state and pass it on.*) -fun print_tac msg st = - (tracing (msg ^ "\n" ^ - Pretty.string_of (Pretty.chunks - (Display_Goal.pretty_goals_without_context (! Display_Goal.goals_limit) st))); - Seq.single st); - -(*Pause until a line is typed -- if non-empty then fail. *) -fun pause_tac st = - (tracing "** Press RETURN to continue:"; - if TextIO.inputLine TextIO.stdIn = SOME "\n" then Seq.single st - else (tracing "Goodbye"; Seq.empty)); - -exception TRACE_EXIT of thm -and TRACE_QUIT; - -(*Tracing flags*) -val trace_REPEAT= ref false -and suppress_tracing = ref false; - -(*Handle all tracing commands for current state and tactic *) -fun exec_trace_command flag (tac, st) = - case TextIO.inputLine TextIO.stdIn of - SOME "\n" => tac st - | SOME "f\n" => Seq.empty - | SOME "o\n" => (flag:=false; tac st) - | SOME "s\n" => (suppress_tracing:=true; tac st) - | SOME "x\n" => (tracing "Exiting now"; raise (TRACE_EXIT st)) - | SOME "quit\n" => raise TRACE_QUIT - | _ => (tracing -"Type RETURN to continue or...\n\ -\ f - to fail here\n\ -\ o - to switch tracing off\n\ -\ s - to suppress tracing until next entry to a tactical\n\ -\ x - to exit at this point\n\ -\ quit - to abort this tracing run\n\ -\** Well? " ; exec_trace_command flag (tac, st)); - - -(*Extract from a tactic, a thm->thm seq function that handles tracing*) -fun tracify flag tac st = - if !flag andalso not (!suppress_tracing) then - (Display_Goal.print_goals_without_context (! Display_Goal.goals_limit) st; - tracing "** Press RETURN to continue:"; - exec_trace_command flag (tac, st)) - else tac st; - -(*Create a tactic whose outcome is given by seqf, handling TRACE_EXIT*) -fun traced_tac seqf st = - (suppress_tracing := false; - Seq.make (fn()=> seqf st - handle TRACE_EXIT st' => SOME(st', Seq.empty))); - - -(*Deterministic DO..UNTIL: only retains the first outcome; tail recursive. - Forces repitition until predicate on state is fulfilled.*) -fun DETERM_UNTIL p tac = -let val tac = tracify trace_REPEAT tac - fun drep st = if p st then SOME (st, Seq.empty) - else (case Seq.pull(tac st) of - NONE => NONE - | SOME(st',_) => drep st') -in traced_tac drep end; - -(*Deterministic REPEAT: only retains the first outcome; - uses less space than REPEAT; tail recursive. - If non-negative, n bounds the number of repetitions.*) -fun REPEAT_DETERM_N n tac = - let val tac = tracify trace_REPEAT tac - fun drep 0 st = SOME(st, Seq.empty) - | drep n st = - (case Seq.pull(tac st) of - NONE => SOME(st, Seq.empty) - | SOME(st',_) => drep (n-1) st') - in traced_tac (drep n) end; - -(*Allows any number of repetitions*) -val REPEAT_DETERM = REPEAT_DETERM_N ~1; - -(*General REPEAT: maintains a stack of alternatives; tail recursive*) -fun REPEAT tac = - let val tac = tracify trace_REPEAT tac - fun rep qs st = - case Seq.pull(tac st) of - NONE => SOME(st, Seq.make(fn()=> repq qs)) - | SOME(st',q) => rep (q::qs) st' - and repq [] = NONE - | repq(q::qs) = case Seq.pull q of - NONE => repq qs - | SOME(st,q) => rep (q::qs) st - in traced_tac (rep []) end; - -(*Repeat 1 or more times*) -fun REPEAT_DETERM1 tac = DETERM tac THEN REPEAT_DETERM tac; -fun REPEAT1 tac = tac THEN REPEAT tac; - - -(** Filtering tacticals **) - -fun FILTER pred tac st = Seq.filter pred (tac st); - -(*Accept only next states that change the theorem somehow*) -fun CHANGED tac st = - let fun diff st' = not (Thm.eq_thm (st, st')); - in Seq.filter diff (tac st) end; - -(*Accept only next states that change the theorem's prop field - (changes to signature, hyps, etc. don't count)*) -fun CHANGED_PROP tac st = - let fun diff st' = not (Thm.eq_thm_prop (st, st')); - in Seq.filter diff (tac st) end; - - -(*** Tacticals based on subgoal numbering ***) - -(*For n subgoals, performs tac(n) THEN ... THEN tac(1) - Essential to work backwards since tac(i) may add/delete subgoals at i. *) -fun ALLGOALS tac st = - let fun doall 0 = all_tac - | doall n = tac(n) THEN doall(n-1) - in doall(nprems_of st)st end; - -(*For n subgoals, performs tac(n) ORELSE ... ORELSE tac(1) *) -fun SOMEGOAL tac st = - let fun find 0 = no_tac - | find n = tac(n) ORELSE find(n-1) - in find(nprems_of st)st end; - -(*For n subgoals, performs tac(1) ORELSE ... ORELSE tac(n). - More appropriate than SOMEGOAL in some cases.*) -fun FIRSTGOAL tac st = - let fun find (i,n) = if i>n then no_tac else tac(i) ORELSE find (i+1,n) - in find(1, nprems_of st)st end; - -(*Repeatedly solve some using tac. *) -fun REPEAT_SOME tac = REPEAT1 (SOMEGOAL (REPEAT1 o tac)); -fun REPEAT_DETERM_SOME tac = REPEAT_DETERM1 (SOMEGOAL (REPEAT_DETERM1 o tac)); - -(*Repeatedly solve the first possible subgoal using tac. *) -fun REPEAT_FIRST tac = REPEAT1 (FIRSTGOAL (REPEAT1 o tac)); -fun REPEAT_DETERM_FIRST tac = REPEAT_DETERM1 (FIRSTGOAL (REPEAT_DETERM1 o tac)); - -(*For n subgoals, tries to apply tac to n,...1 *) -fun TRYALL tac = ALLGOALS (TRY o tac); - - -(*Make a tactic for subgoal i, if there is one. *) -fun CSUBGOAL goalfun i st = - (case SOME (Thm.cprem_of st i) handle THM _ => NONE of - SOME goal => goalfun (goal, i) st - | NONE => Seq.empty); - -fun SUBGOAL goalfun = - CSUBGOAL (fn (goal, i) => goalfun (Thm.term_of goal, i)); - -(*Returns all states that have changed in subgoal i, counted from the LAST - subgoal. For stac, for example.*) -fun CHANGED_GOAL tac i st = - let val np = Thm.nprems_of st - val d = np-i (*distance from END*) - val t = Thm.term_of (Thm.cprem_of st i) - fun diff st' = - Thm.nprems_of st' - d <= 0 (*the subgoal no longer exists*) - orelse - not (Pattern.aeconv (t, Thm.term_of (Thm.cprem_of st' (Thm.nprems_of st' - d)))) - in Seq.filter diff (tac i st) end - handle Subscript => Seq.empty (*no subgoal i*); - -fun (tac1 THEN_ALL_NEW tac2) i st = - st |> (tac1 i THEN (fn st' => Seq.INTERVAL tac2 i (i + nprems_of st' - nprems_of st) st')); - -(*repeatedly dig into any emerging subgoals*) -fun REPEAT_ALL_NEW tac = - tac THEN_ALL_NEW (TRY o (fn i => REPEAT_ALL_NEW tac i)); - - -(*Strips assumptions in goal yielding ( [x1,...,xm], [H1,...,Hn], B ) - H1,...,Hn are the hypotheses; x1...xm are variants of the parameters. - Main difference from strip_assums concerns parameters: - it replaces the bound variables by free variables. *) -fun strip_context_aux (params, Hs, Const("==>", _) $ H $ B) = - strip_context_aux (params, H::Hs, B) - | strip_context_aux (params, Hs, Const("all",_)$Abs(a,T,t)) = - let val (b,u) = Syntax.variant_abs(a,T,t) - in strip_context_aux ((b,T)::params, Hs, u) end - | strip_context_aux (params, Hs, B) = (rev params, rev Hs, B); - -fun strip_context A = strip_context_aux ([],[],A); - - -(**** METAHYPS -- tactical for using hypotheses as meta-level assumptions - METAHYPS (fn prems => tac prems) i - -converts subgoal i, of the form !!x1...xm. [| A1;...;An] ==> A into a new -proof state A==>A, supplying A1,...,An as meta-level assumptions (in -"prems"). The parameters x1,...,xm become free variables. If the -resulting proof state is [| B1;...;Bk] ==> C (possibly assuming A1,...,An) -then it is lifted back into the original context, yielding k subgoals. - -Replaces unknowns in the context by Frees having the prefix METAHYP_ -New unknowns in [| B1;...;Bk] ==> C are lifted over x1,...,xm. -DOES NOT HANDLE TYPE UNKNOWNS. -****) - -local - - (*Left-to-right replacements: ctpairs = [...,(vi,ti),...]. - Instantiates distinct free variables by terms of same type.*) - fun free_instantiate ctpairs = - forall_elim_list (map snd ctpairs) o forall_intr_list (map fst ctpairs); - - fun free_of s ((a, i), T) = - Free (s ^ (case i of 0 => a | _ => a ^ "_" ^ string_of_int i), T) - - fun mk_inst v = (Var v, free_of "METAHYP1_" v) -in - -(*Common code for METAHYPS and metahyps_thms*) -fun metahyps_split_prem prem = - let (*find all vars in the hyps -- should find tvars also!*) - val hyps_vars = fold Term.add_vars (Logic.strip_assums_hyp prem) [] - val insts = map mk_inst hyps_vars - (*replace the hyps_vars by Frees*) - val prem' = subst_atomic insts prem - val (params,hyps,concl) = strip_context prem' - in (insts,params,hyps,concl) end; - -fun metahyps_aux_tac tacf (prem,gno) state = - let val (insts,params,hyps,concl) = metahyps_split_prem prem - val maxidx = Thm.maxidx_of state - val cterm = Thm.cterm_of (Thm.theory_of_thm state) - val chyps = map cterm hyps - val hypths = map assume chyps - val subprems = map (Thm.forall_elim_vars 0) hypths - val fparams = map Free params - val cparams = map cterm fparams - fun swap_ctpair (t,u) = (cterm u, cterm t) - (*Subgoal variables: make Free; lift type over params*) - fun mk_subgoal_inst concl_vars (v, T) = - if member (op =) concl_vars (v, T) - then ((v, T), true, free_of "METAHYP2_" (v, T)) - else ((v, T), false, free_of "METAHYP2_" (v, map #2 params ---> T)) - (*Instantiate subgoal vars by Free applied to params*) - fun mk_ctpair (v, in_concl, u) = - if in_concl then (cterm (Var v), cterm u) - else (cterm (Var v), cterm (list_comb (u, fparams))) - (*Restore Vars with higher type and index*) - fun mk_subgoal_swap_ctpair (((a, i), T), in_concl, u as Free (_, U)) = - if in_concl then (cterm u, cterm (Var ((a, i), T))) - else (cterm u, cterm (Var ((a, i + maxidx), U))) - (*Embed B in the original context of params and hyps*) - fun embed B = list_all_free (params, Logic.list_implies (hyps, B)) - (*Strip the context using elimination rules*) - fun elim Bhyp = implies_elim_list (forall_elim_list cparams Bhyp) hypths - (*A form of lifting that discharges assumptions.*) - fun relift st = - let val prop = Thm.prop_of st - val subgoal_vars = (*Vars introduced in the subgoals*) - fold Term.add_vars (Logic.strip_imp_prems prop) [] - and concl_vars = Term.add_vars (Logic.strip_imp_concl prop) [] - val subgoal_insts = map (mk_subgoal_inst concl_vars) subgoal_vars - val st' = Thm.instantiate ([], map mk_ctpair subgoal_insts) st - val emBs = map (cterm o embed) (prems_of st') - val Cth = implies_elim_list st' (map (elim o assume) emBs) - in (*restore the unknowns to the hypotheses*) - free_instantiate (map swap_ctpair insts @ - map mk_subgoal_swap_ctpair subgoal_insts) - (*discharge assumptions from state in same order*) - (implies_intr_list emBs - (forall_intr_list cparams (implies_intr_list chyps Cth))) - end - (*function to replace the current subgoal*) - fun next st = Thm.bicompose false (false, relift st, nprems_of st) gno state - in Seq.maps next (tacf subprems (trivial (cterm concl))) end; - -end; - -(*Returns the theorem list that METAHYPS would supply to its tactic*) -fun metahyps_thms i state = - let val prem = Logic.nth_prem (i, Thm.prop_of state) - and cterm = cterm_of (Thm.theory_of_thm state) - val (_,_,hyps,_) = metahyps_split_prem prem - in SOME (map (Thm.forall_elim_vars 0 o Thm.assume o cterm) hyps) end - handle TERM ("nth_prem", [A]) => NONE; - -local - -fun print_vars_terms thy (n,thm) = - let - fun typed ty = " has type: " ^ Syntax.string_of_typ_global thy ty; - fun find_vars thy (Const (c, ty)) = - if null (Term.add_tvarsT ty []) then I - else insert (op =) (c ^ typed ty) - | find_vars thy (Var (xi, ty)) = insert (op =) (Term.string_of_vname xi ^ typed ty) - | find_vars _ (Free _) = I - | find_vars _ (Bound _) = I - | find_vars thy (Abs (_, _, t)) = find_vars thy t - | find_vars thy (t1 $ t2) = - find_vars thy t1 #> find_vars thy t1; - val prem = Logic.nth_prem (n, Thm.prop_of thm) - val tms = find_vars thy prem [] - in - (warning "Found schematic vars in assumptions:"; warning (cat_lines tms)) - end; - -in - -fun METAHYPS tacf n thm = SUBGOAL (metahyps_aux_tac tacf) n thm - handle THM("assume: variables",_,_) => (print_vars_terms (theory_of_thm thm) (n,thm); Seq.empty) - -end; - -(*Makes a tactic whose effect on a state is given by thmfun: thm->thm seq.*) -fun PRIMSEQ thmfun st = thmfun st handle THM _ => Seq.empty; - -(*Makes a tactic whose effect on a state is given by thmfun: thm->thm.*) -fun PRIMITIVE thmfun = PRIMSEQ (Seq.single o thmfun); - -(*Inverse (more or less) of PRIMITIVE*) -fun SINGLE tacf = Option.map fst o Seq.pull o tacf - -(*Conversions as tactics*) -fun CONVERSION cv i st = Seq.single (Conv.gconv_rule cv i st) - handle THM _ => Seq.empty - | CTERM _ => Seq.empty - | TERM _ => Seq.empty - | TYPE _ => Seq.empty; - -end; - -open Tactical; diff -r b2e93cda0be8 -r d64a1820431d src/Tools/induct.ML --- a/src/Tools/induct.ML Sat Jul 25 18:44:55 2009 +0200 +++ b/src/Tools/induct.ML Sun Jul 26 07:54:28 2009 +0200 @@ -70,7 +70,7 @@ val setup: theory -> theory end; -functor InductFun(Data: INDUCT_DATA): INDUCT = +functor Induct(Data: INDUCT_DATA): INDUCT = struct @@ -568,7 +568,7 @@ *) fun get_inductT ctxt insts = - fold_rev multiply (insts |> map + fold_rev (map_product cons) (insts |> map ((fn [] => NONE | ts => List.last ts) #> (fn NONE => TVar (("'a", 0), []) | SOME t => Term.fastype_of t) #> find_inductT ctxt)) [[]] diff -r b2e93cda0be8 -r d64a1820431d src/Tools/project_rule.ML --- a/src/Tools/project_rule.ML Sat Jul 25 18:44:55 2009 +0200 +++ b/src/Tools/project_rule.ML Sun Jul 26 07:54:28 2009 +0200 @@ -24,7 +24,7 @@ val projections: Proof.context -> thm -> thm list end; -functor ProjectRuleFun(Data: PROJECT_RULE_DATA): PROJECT_RULE = +functor Project_Rule(Data: PROJECT_RULE_DATA): PROJECT_RULE = struct fun conj1 th = th RS Data.conjunct1; diff -r b2e93cda0be8 -r d64a1820431d src/ZF/Tools/typechk.ML --- a/src/ZF/Tools/typechk.ML Sat Jul 25 18:44:55 2009 +0200 +++ b/src/ZF/Tools/typechk.ML Sun Jul 26 07:54:28 2009 +0200 @@ -116,7 +116,7 @@ (Method.sections [Args.add -- Args.colon >> K (I, TC_add), Args.del -- Args.colon >> K (I, TC_del)] - >> (K (fn ctxt => SIMPLE_METHOD (CHANGED (typecheck_tac ctxt))))) + >> K (fn ctxt => SIMPLE_METHOD (CHANGED (typecheck_tac ctxt)))) "ZF type-checking"; val _ =