--- 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"
--- 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"
--- 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.
--- 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.
--- 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
--- 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}
--- 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"
--- 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
--- 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;
--- 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 ***)
--- 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}
--- 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:"
--- 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;
--- 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();
--- 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";
--- 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
--- 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
--- 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;
--- 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 =
--- 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]),
--- 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
--- 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
--- 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"), []),
--- 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 *)
--- 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!
--- 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)
)
--- 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);
--- 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);
--- 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";
--- 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;
--- 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) ());
--- 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;
--- 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;
--- 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;
--- 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
--- 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
--- 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;
--- 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 =
--- 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);
--- 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;
--- 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
--- 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";
--- 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 ****)
--- 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 ^ "]")];
--- 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;
-
--- 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]));
--- /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;
+
--- 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;
--- 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;
--- 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;
--- /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;
--- 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;
--- 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)) [[]]
--- 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;
--- 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 _ =