--- a/src/FOL/ex/Iff_Oracle.thy Thu Mar 26 14:10:48 2009 +0000
+++ b/src/FOL/ex/Iff_Oracle.thy Thu Mar 26 14:30:20 2009 +0000
@@ -34,7 +34,7 @@
ML {* iff_oracle (@{theory}, 2) *}
ML {* iff_oracle (@{theory}, 10) *}
-ML {* Thm.proof_of (iff_oracle (@{theory}, 10)) *}
+ML {* Thm.proof_body_of (iff_oracle (@{theory}, 10)) *}
text {* These oracle calls had better fail. *}
--- a/src/HOL/Algebra/ringsimp.ML Thu Mar 26 14:10:48 2009 +0000
+++ b/src/HOL/Algebra/ringsimp.ML Thu Mar 26 14:30:20 2009 +0000
@@ -62,11 +62,13 @@
Thm.declaration_attribute
(fn _ => Data.map (AList.delete struct_eq s));
-val attribute =
- Scan.lift ((Args.add >> K true || Args.del >> K false) --| Args.colon ||
- Scan.succeed true) -- Scan.lift Args.name --
- Scan.repeat Args.term
- >> (fn ((b, n), ts) => if b then add_struct_thm (n, ts) else del_struct (n, ts));
+val attrib_setup =
+ Attrib.setup @{binding algebra}
+ (Scan.lift ((Args.add >> K true || Args.del >> K false) --| Args.colon || Scan.succeed true)
+ -- Scan.lift Args.name -- Scan.repeat Args.term
+ >> (fn ((b, n), ts) => if b then add_struct_thm (n, ts) else del_struct (n, ts)))
+ "theorems controlling algebra method";
+
(** Setup **)
@@ -74,6 +76,6 @@
val setup =
Method.setup @{binding algebra} (Scan.succeed (SIMPLE_METHOD' o algebra_tac))
"normalisation of algebraic structure" #>
- Attrib.setup @{binding algebra} attribute "theorems controlling algebra method";
+ attrib_setup;
end;
--- a/src/HOL/Orderings.thy Thu Mar 26 14:10:48 2009 +0000
+++ b/src/HOL/Orderings.thy Thu Mar 26 14:30:20 2009 +0000
@@ -372,13 +372,14 @@
Thm.declaration_attribute
(fn _ => Data.map (AList.delete struct_eq s));
-val attribute =
- Scan.lift ((Args.add -- Args.name >> (fn (_, s) => SOME s) ||
- Args.del >> K NONE) --| Args.colon (* FIXME ||
- Scan.succeed true *) ) -- Scan.lift Args.name --
- Scan.repeat Args.term
- >> (fn ((SOME tag, n), ts) => add_struct_thm (n, ts) tag
- | ((NONE, n), ts) => del_struct (n, ts));
+val attrib_setup =
+ Attrib.setup @{binding order}
+ (Scan.lift ((Args.add -- Args.name >> (fn (_, s) => SOME s) || Args.del >> K NONE) --|
+ Args.colon (* FIXME || Scan.succeed true *) ) -- Scan.lift Args.name --
+ Scan.repeat Args.term
+ >> (fn ((SOME tag, n), ts) => add_struct_thm (n, ts) tag
+ | ((NONE, n), ts) => del_struct (n, ts)))
+ "theorems controlling transitivity reasoner";
(** Diagnostic command **)
@@ -397,8 +398,9 @@
(** Setup **)
val setup =
- Method.setup @{binding order} (Scan.succeed (SIMPLE_METHOD' o order_tac [])) "transitivity reasoner" #>
- Attrib.setup @{binding order} attribute "theorems controlling transitivity reasoner";
+ Method.setup @{binding order} (Scan.succeed (SIMPLE_METHOD' o order_tac []))
+ "transitivity reasoner" #>
+ attrib_setup;
end;
--- a/src/HOL/Tools/Groebner_Basis/normalizer_data.ML Thu Mar 26 14:10:48 2009 +0000
+++ b/src/HOL/Tools/Groebner_Basis/normalizer_data.ML Thu Mar 26 14:30:20 2009 +0000
@@ -191,16 +191,17 @@
in
-val attribute =
- Scan.lift (Args.$$$ delN >> K del) ||
- ((keyword2 semiringN opsN |-- terms) --
- (keyword2 semiringN rulesN |-- thms)) --
- (optional (keyword2 ringN opsN |-- terms) --
- optional (keyword2 ringN rulesN |-- thms)) --
- optional (keyword2 idomN rulesN |-- thms) --
- optional (keyword2 idealN rulesN |-- thms)
- >> (fn (((sr, r), id), idl) =>
- add {semiring = sr, ring = r, idom = id, ideal = idl});
+val normalizer_setup =
+ Attrib.setup @{binding normalizer}
+ (Scan.lift (Args.$$$ delN >> K del) ||
+ ((keyword2 semiringN opsN |-- terms) --
+ (keyword2 semiringN rulesN |-- thms)) --
+ (optional (keyword2 ringN opsN |-- terms) --
+ optional (keyword2 ringN rulesN |-- thms)) --
+ optional (keyword2 idomN rulesN |-- thms) --
+ optional (keyword2 idealN rulesN |-- thms)
+ >> (fn (((sr, r), id), idl) => add {semiring = sr, ring = r, idom = id, ideal = idl}))
+ "semiring normalizer data";
end;
@@ -208,7 +209,7 @@
(* theory setup *)
val setup =
- Attrib.setup @{binding normalizer} attribute "semiring normalizer data" #>
+ normalizer_setup #>
Attrib.setup @{binding algebra} (Attrib.add_del add_ss del_ss) "pre-simplification for algebra";
end;
--- a/src/HOL/Tools/Qelim/cooper_data.ML Thu Mar 26 14:10:48 2009 +0000
+++ b/src/HOL/Tools/Qelim/cooper_data.ML Thu Mar 26 14:30:20 2009 +0000
@@ -67,6 +67,7 @@
(* concrete syntax *)
local
+
fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ();
val constsN = "consts";
@@ -77,14 +78,17 @@
fun optional scan = Scan.optional scan [];
in
-val attribute =
- (Scan.lift (Args.$$$ "del") |-- optional (keyword constsN |-- terms)) >> del ||
- optional (keyword constsN |-- terms) >> add
+
+val presburger_setup =
+ Attrib.setup @{binding presburger}
+ ((Scan.lift (Args.$$$ "del") |-- optional (keyword constsN |-- terms)) >> del ||
+ optional (keyword constsN |-- terms) >> add) "Cooper data";
+
end;
(* theory setup *)
-val setup = Attrib.setup @{binding presburger} attribute "Cooper data";
+val setup = presburger_setup;
end;
--- a/src/HOL/Tools/Qelim/ferrante_rackoff_data.ML Thu Mar 26 14:10:48 2009 +0000
+++ b/src/HOL/Tools/Qelim/ferrante_rackoff_data.ML Thu Mar 26 14:30:20 2009 +0000
@@ -122,26 +122,28 @@
val terms = thms >> map Drule.dest_term;
in
-val attribute =
- (keyword minfN |-- thms)
+val ferrak_setup =
+ Attrib.setup @{binding ferrack}
+ ((keyword minfN |-- thms)
-- (keyword pinfN |-- thms)
-- (keyword nmiN |-- thms)
-- (keyword npiN |-- thms)
-- (keyword lin_denseN |-- thms)
-- (keyword qeN |-- thms)
- -- (keyword atomsN |-- terms) >>
- (fn ((((((minf,pinf),nmi),npi),lin_dense),qe), atoms)=>
- if length qe = 1 then
- add ({minf = minf, pinf = pinf, nmi = nmi, npi = npi, ld = lin_dense,
- qe = hd qe, atoms = atoms},
- {isolate_conv = undefined, whatis = undefined, simpset = HOL_ss})
- else error "only one theorem for qe!")
+ -- (keyword atomsN |-- terms) >>
+ (fn ((((((minf,pinf),nmi),npi),lin_dense),qe), atoms)=>
+ if length qe = 1 then
+ add ({minf = minf, pinf = pinf, nmi = nmi, npi = npi, ld = lin_dense,
+ qe = hd qe, atoms = atoms},
+ {isolate_conv = undefined, whatis = undefined, simpset = HOL_ss})
+ else error "only one theorem for qe!"))
+ "Ferrante Rackoff data";
end;
(* theory setup *)
-val setup = Attrib.setup @{binding ferrack} attribute "Ferrante Rackoff data";
+val setup = ferrak_setup;
end;
--- a/src/HOL/Tools/Qelim/langford_data.ML Thu Mar 26 14:10:48 2009 +0000
+++ b/src/HOL/Tools/Qelim/langford_data.ML Thu Mar 26 14:30:20 2009 +0000
@@ -85,25 +85,28 @@
val terms = thms >> map Drule.dest_term;
in
-val attribute =
- (keyword qeN |-- thms)
+val langford_setup =
+ Attrib.setup @{binding langford}
+ ((keyword qeN |-- thms)
-- (keyword gatherN |-- thms)
- -- (keyword atomsN |-- terms) >>
- (fn ((qes,gs), atoms) =>
- if length qes = 3 andalso length gs > 1 then
- let
- val [q1,q2,q3] = qes
- val gst::gss = gs
- val entry = {qe_bnds = q1, qe_nolb = q2,
- qe_noub = q3, gs = gss, gst = gst, atoms = atoms}
- in add entry end
- else error "Need 3 theorems for qe and at least one for gs")
+ -- (keyword atomsN |-- terms) >>
+ (fn ((qes,gs), atoms) =>
+ if length qes = 3 andalso length gs > 1 then
+ let
+ val [q1,q2,q3] = qes
+ val gst::gss = gs
+ val entry = {qe_bnds = q1, qe_nolb = q2,
+ qe_noub = q3, gs = gss, gst = gst, atoms = atoms}
+ in add entry end
+ else error "Need 3 theorems for qe and at least one for gs"))
+ "Langford data";
+
end;
(* theory setup *)
val setup =
- Attrib.setup @{binding langford} attribute "Langford data" #>
+ langford_setup #>
Attrib.setup @{binding langfordsimp} (Attrib.add_del add_simp del_simp) "Langford simpset";
end;
--- a/src/HOL/Tools/arith_data.ML Thu Mar 26 14:10:48 2009 +0000
+++ b/src/HOL/Tools/arith_data.ML Thu Mar 26 14:30:20 2009 +0000
@@ -57,12 +57,13 @@
val arith_tac = gen_arith_tac false;
val verbose_arith_tac = gen_arith_tac true;
-val arith_method = Args.bang_facts >> (fn prems => fn ctxt =>
- METHOD (fn facts => HEADGOAL (Method.insert_tac (prems @ get_arith_facts ctxt @ facts)
- THEN' verbose_arith_tac ctxt)));
-
-val setup = Arith_Facts.setup
- #> Method.setup @{binding arith} arith_method "various arithmetic decision procedures";
+val setup =
+ Arith_Facts.setup #>
+ Method.setup @{binding arith}
+ (Args.bang_facts >> (fn prems => fn ctxt =>
+ METHOD (fn facts => HEADGOAL (Method.insert_tac (prems @ get_arith_facts ctxt @ facts)
+ THEN' verbose_arith_tac ctxt))))
+ "various arithmetic decision procedures";
(* various auxiliary and legacy *)
--- a/src/HOL/Tools/inductive_package.ML Thu Mar 26 14:10:48 2009 +0000
+++ b/src/HOL/Tools/inductive_package.ML Thu Mar 26 14:30:20 2009 +0000
@@ -460,17 +460,18 @@
val inductive_cases_i = gen_inductive_cases (K I) Syntax.check_prop;
-val ind_cases =
- Scan.lift (Scan.repeat1 Args.name_source --
- Scan.optional (Args.$$$ "for" |-- Scan.repeat1 Args.name) []) >>
- (fn (raw_props, fixes) => fn ctxt =>
- let
- val (_, ctxt') = Variable.add_fixes fixes ctxt;
- val props = Syntax.read_props ctxt' raw_props;
- val ctxt'' = fold Variable.declare_term props ctxt';
- val rules = ProofContext.export ctxt'' ctxt (map (mk_cases ctxt'') props)
- in Method.erule 0 rules end);
-
+val ind_cases_setup =
+ Method.setup @{binding ind_cases}
+ (Scan.lift (Scan.repeat1 Args.name_source --
+ Scan.optional (Args.$$$ "for" |-- Scan.repeat1 Args.name) []) >>
+ (fn (raw_props, fixes) => fn ctxt =>
+ let
+ val (_, ctxt') = Variable.add_fixes fixes ctxt;
+ val props = Syntax.read_props ctxt' raw_props;
+ val ctxt'' = fold Variable.declare_term props ctxt';
+ val rules = ProofContext.export ctxt'' ctxt (map (mk_cases ctxt'') props)
+ in Method.erule 0 rules end))
+ "dynamic case analysis on predicates";
(* prove induction rule *)
@@ -934,7 +935,7 @@
(* setup theory *)
val setup =
- Method.setup @{binding ind_cases} ind_cases "dynamic case analysis on predicates" #>
+ ind_cases_setup #>
Attrib.setup @{binding mono} (Attrib.add_del mono_add mono_del)
"declaration of monotonicity rule";
--- a/src/HOL/Tools/inductive_realizer.ML Thu Mar 26 14:10:48 2009 +0000
+++ b/src/HOL/Tools/inductive_realizer.ML Thu Mar 26 14:30:20 2009 +0000
@@ -505,13 +505,11 @@
| SOME (SOME sets') => sets \\ sets')
end I);
-val ind_realizer =
- (Scan.option (Scan.lift (Args.$$$ "irrelevant") |--
- Scan.option (Scan.lift (Args.colon) |--
- Scan.repeat1 Args.const))) >> rlz_attrib;
-
val setup =
- Attrib.setup @{binding ind_realizer} ind_realizer "add realizers for inductive set";
+ Attrib.setup @{binding ind_realizer}
+ ((Scan.option (Scan.lift (Args.$$$ "irrelevant") |--
+ Scan.option (Scan.lift (Args.colon) |-- Scan.repeat1 Args.const))) >> rlz_attrib)
+ "add realizers for inductive set";
end;
--- a/src/HOL/Tools/lin_arith.ML Thu Mar 26 14:10:48 2009 +0000
+++ b/src/HOL/Tools/lin_arith.ML Thu Mar 26 14:30:20 2009 +0000
@@ -882,10 +882,6 @@
val linear_arith_tac = gen_linear_arith_tac true;
-val linarith_method = Args.bang_facts >> (fn prems => fn ctxt =>
- METHOD (fn facts => HEADGOAL (Method.insert_tac (prems @ Arith_Data.get_arith_facts ctxt @ facts)
- THEN' linear_arith_tac ctxt)));
-
end;
@@ -899,7 +895,11 @@
Context.mapping
(setup_options #>
Arith_Data.add_tactic "linear arithmetic" gen_linear_arith_tac #>
- Method.setup @{binding linarith} linarith_method "linear arithmetic" #>
+ Method.setup @{binding linarith}
+ (Args.bang_facts >> (fn prems => fn ctxt =>
+ METHOD (fn facts =>
+ HEADGOAL (Method.insert_tac (prems @ Arith_Data.get_arith_facts ctxt @ facts)
+ THEN' linear_arith_tac ctxt)))) "linear arithmetic" #>
Attrib.setup @{binding arith_split} (Scan.succeed arith_split_add)
"declaration of split rules for arithmetic procedure") I;
--- a/src/HOL/Tools/res_axioms.ML Thu Mar 26 14:10:48 2009 +0000
+++ b/src/HOL/Tools/res_axioms.ML Thu Mar 26 14:30:20 2009 +0000
@@ -521,18 +521,19 @@
REPEAT_DETERM_N (length ts) o (etac thin_rl)]
end);
-val setup_methods =
+val neg_clausify_setup =
Method.setup @{binding neg_clausify} (Scan.succeed (K (SIMPLE_METHOD' neg_clausify_tac)))
"conversion of goal to conjecture clauses";
(** Attribute for converting a theorem into clauses **)
-val clausify = Scan.lift OuterParse.nat >>
- (fn i => Thm.rule_attribute (fn context => fn th =>
- Meson.make_meta_clause (nth (cnf_axiom (Context.theory_of context) th) i)));
-
-val setup_attrs = Attrib.setup @{binding clausify} clausify "conversion of theorem to clauses";
+val clausify_setup =
+ Attrib.setup @{binding clausify}
+ (Scan.lift OuterParse.nat >>
+ (fn i => Thm.rule_attribute (fn context => fn th =>
+ Meson.make_meta_clause (nth (cnf_axiom (Context.theory_of context) th) i))))
+ "conversion of theorem to clauses";
@@ -540,8 +541,8 @@
val setup =
meson_method_setup #>
- setup_methods #>
- setup_attrs #>
+ neg_clausify_setup #>
+ clausify_setup #>
perhaps saturate_skolem_cache #>
Theory.at_end clause_cache_endtheory;
--- a/src/HOL/Tools/split_rule.ML Thu Mar 26 14:10:48 2009 +0000
+++ b/src/HOL/Tools/split_rule.ML Thu Mar 26 14:30:20 2009 +0000
@@ -141,18 +141,18 @@
|> RuleCases.save rl
end;
+
(* attribute syntax *)
(* FIXME dynamically scoped due to Args.name_source/pair_tac *)
-val split_format = Scan.lift
- (Args.parens (Args.$$$ "complete") >> K (Thm.rule_attribute (K complete_split_rule)) ||
- OuterParse.and_list1 (Scan.repeat Args.name_source)
- >> (fn xss => Thm.rule_attribute (fn context =>
- split_rule_goal (Context.proof_of context) xss)));
-
val setup =
- Attrib.setup @{binding split_format} split_format
+ Attrib.setup @{binding split_format}
+ (Scan.lift
+ (Args.parens (Args.$$$ "complete") >> K (Thm.rule_attribute (K complete_split_rule)) ||
+ OuterParse.and_list1 (Scan.repeat Args.name_source)
+ >> (fn xss => Thm.rule_attribute (fn context =>
+ split_rule_goal (Context.proof_of context) xss))))
"split pair-typed subterms in premises, or function arguments" #>
Attrib.setup @{binding split_rule} (Scan.succeed (Thm.rule_attribute (K split_rule)))
"curries ALL function variables occurring in a rule's conclusion";
--- a/src/Provers/blast.ML Thu Mar 26 14:10:48 2009 +0000
+++ b/src/Provers/blast.ML Thu Mar 26 14:30:20 2009 +0000
@@ -1302,14 +1302,13 @@
(** method setup **)
-val blast_method =
- Args.bang_facts -- Scan.lift (Scan.option OuterParse.nat) --|
- Method.sections Data.cla_modifiers >>
- (fn (prems, NONE) => Data.cla_meth' blast_tac prems
- | (prems, SOME lim) => Data.cla_meth' (fn cs => depth_tac cs lim) prems);
-
val setup =
setup_depth_limit #>
- Method.setup @{binding blast} blast_method "tableau prover";
+ Method.setup @{binding blast}
+ (Args.bang_facts -- Scan.lift (Scan.option OuterParse.nat) --|
+ Method.sections Data.cla_modifiers >>
+ (fn (prems, NONE) => Data.cla_meth' blast_tac prems
+ | (prems, SOME lim) => Data.cla_meth' (fn cs => depth_tac cs lim) prems))
+ "classical tableau prover";
end;
--- a/src/Provers/splitter.ML Thu Mar 26 14:10:48 2009 +0000
+++ b/src/Provers/splitter.ML Thu Mar 26 14:30:20 2009 +0000
@@ -467,14 +467,13 @@
Args.$$$ splitN -- Args.add -- Args.colon >> K (I, split_add),
Args.$$$ splitN -- Args.del -- Args.colon >> K (I, split_del)];
-fun split_meth parser = (Attrib.thms >>
- (fn ths => K (SIMPLE_METHOD' (CHANGED_PROP o gen_split_tac ths)))) parser;
-
(* theory setup *)
val setup =
Attrib.setup @{binding split} (Attrib.add_del split_add split_del) "declare case split rule" #>
- Method.setup @{binding split} split_meth "apply case split rule";
+ Method.setup @{binding split}
+ (Attrib.thms >> (fn ths => K (SIMPLE_METHOD' (CHANGED_PROP o gen_split_tac ths))))
+ "apply case split rule";
end;
--- a/src/Pure/Isar/code.ML Thu Mar 26 14:10:48 2009 +0000
+++ b/src/Pure/Isar/code.ML Thu Mar 26 14:30:20 2009 +0000
@@ -98,14 +98,12 @@
then error ("Code attribute " ^ name ^ " already declared") else add_parser attr attrs)
end;
-val _ =
- let
- val code_attr = Scan.peek (fn context =>
- List.foldr op || Scan.fail (map snd (CodeAttr.get (Context.theory_of context))));
- in
- Context.>> (Context.map_theory
- (Attrib.setup (Binding.name "code") code_attr "declare theorems for code generation"))
- end;
+val _ = Context.>> (Context.map_theory
+ (Attrib.setup (Binding.name "code")
+ (Scan.peek (fn context =>
+ List.foldr op || Scan.fail (map snd (CodeAttr.get (Context.theory_of context)))))
+ "declare theorems for code generation"));
+
(** logical and syntactical specification of executable code **)
--- a/src/Pure/Isar/rule_insts.ML Thu Mar 26 14:10:48 2009 +0000
+++ b/src/Pure/Isar/rule_insts.ML Thu Mar 26 14:30:20 2009 +0000
@@ -220,8 +220,11 @@
in
-fun where_att x = (Scan.lift (P.and_list inst) >> (fn args =>
- Thm.rule_attribute (fn context => read_instantiate_mixed (Context.proof_of context) args))) x;
+val _ = Context.>> (Context.map_theory
+ (Attrib.setup (Binding.name "where")
+ (Scan.lift (P.and_list inst) >> (fn args =>
+ Thm.rule_attribute (fn context => read_instantiate_mixed (Context.proof_of context) args)))
+ "named instantiation of theorem"));
end;
@@ -243,19 +246,15 @@
in
-fun of_att x = (Scan.lift insts >> (fn args =>
- Thm.rule_attribute (fn context => read_instantiate_mixed' (Context.proof_of context) args))) x;
+val _ = Context.>> (Context.map_theory
+ (Attrib.setup (Binding.name "of")
+ (Scan.lift insts >> (fn args =>
+ Thm.rule_attribute (fn context => read_instantiate_mixed' (Context.proof_of context) args)))
+ "positional instantiation of theorem"));
end;
-(* setup *)
-
-val _ = Context.>> (Context.map_theory
- (Attrib.setup (Binding.name "where") where_att "named instantiation of theorem" #>
- Attrib.setup (Binding.name "of") of_att "positional instantiation of theorem"));
-
-
(** tactics **)
--- a/src/Pure/Isar/spec_parse.ML Thu Mar 26 14:10:48 2009 +0000
+++ b/src/Pure/Isar/spec_parse.ML Thu Mar 26 14:30:20 2009 +0000
@@ -112,10 +112,10 @@
val locale_expression =
let
- fun expr2 x = P.xname x;
- fun expr1 x = (Scan.optional prefix ("", false) -- expr2 --
- Scan.optional instance (Expression.Named []) >> (fn ((p, l), i) => (l, (p, i)))) x;
- fun expr0 x = (plus1_unless locale_keyword expr1) x;
+ val expr2 = P.xname;
+ val expr1 = Scan.optional prefix ("", false) -- expr2 --
+ Scan.optional instance (Expression.Named []) >> (fn ((p, l), i) => (l, (p, i)));
+ val expr0 = plus1_unless locale_keyword expr1;
in expr0 -- Scan.optional (P.$$$ "for" |-- P.!!! locale_fixes) [] end;
val context_element = P.group "context element" loc_element;
--- a/src/Pure/ML/ml_antiquote.ML Thu Mar 26 14:10:48 2009 +0000
+++ b/src/Pure/ML/ml_antiquote.ML Thu Mar 26 14:30:20 2009 +0000
@@ -59,7 +59,7 @@
structure P = OuterParse;
-val _ = inline "binding"
+val _ = value "binding"
(Scan.lift (P.position Args.name) >> (fn name => ML_Syntax.atomic (ML_Syntax.make_binding name)));
val _ = value "theory"
--- a/src/Pure/Proof/extraction.ML Thu Mar 26 14:10:48 2009 +0000
+++ b/src/Pure/Proof/extraction.ML Thu Mar 26 14:30:20 2009 +0000
@@ -568,7 +568,7 @@
(proof_combt
(PThm (serial (),
((corr_name name vs', corr_prop, SOME (map TVar (OldTerm.term_tvars corr_prop))),
- Future.value (make_proof_body corr_prf))), vfs_of corr_prop))
+ Future.value (approximate_proof_body corr_prf))), vfs_of corr_prop))
(map (get_var_type corr_prop) (vfs_of prop))
in
((name, (vs', ((nullt, nullt), (corr_prf, corr_prf')))) :: defs'',
@@ -679,7 +679,7 @@
(proof_combt
(PThm (serial (),
((corr_name s vs', corr_prop, SOME (map TVar (OldTerm.term_tvars corr_prop))),
- Future.value (make_proof_body corr_prf'))), vfs_of corr_prop))
+ Future.value (approximate_proof_body corr_prf'))), vfs_of corr_prop))
(map (get_var_type corr_prop) (vfs_of prop));
in
((s, (vs', ((t', u), (corr_prf', corr_prf'')))) :: defs'',
--- a/src/Pure/Tools/xml_syntax.ML Thu Mar 26 14:10:48 2009 +0000
+++ b/src/Pure/Tools/xml_syntax.ML Thu Mar 26 14:30:20 2009 +0000
@@ -158,7 +158,7 @@
| proof_of_xml (XML.Elem ("PThm", [("name", s)], term :: opttypes)) =
(* FIXME? *)
PThm (serial (), ((s, term_of_xml term, opttypes_of_xml opttypes),
- Future.value (Proofterm.make_proof_body MinProof)))
+ Future.value (Proofterm.approximate_proof_body MinProof)))
| proof_of_xml (XML.Elem ("PAxm", [("name", s)], term :: opttypes)) =
PAxm (s, term_of_xml term, opttypes_of_xml opttypes)
| proof_of_xml (XML.Elem ("Oracle", [("name", s)], term :: opttypes)) =
--- a/src/Pure/proofterm.ML Thu Mar 26 14:10:48 2009 +0000
+++ b/src/Pure/proofterm.ML Thu Mar 26 14:30:20 2009 +0000
@@ -46,11 +46,10 @@
val oracle_ord: oracle * oracle -> order
val thm_ord: pthm * pthm -> order
- val make_proof_body: proof -> proof_body
val merge_oracles: oracle OrdList.T -> oracle OrdList.T -> oracle OrdList.T
- val make_oracles: proof -> oracle OrdList.T
val merge_thms: pthm OrdList.T -> pthm OrdList.T -> pthm OrdList.T
- val make_thms: proof -> pthm OrdList.T
+ val all_oracles_of: proof_body -> oracle OrdList.T
+ val approximate_proof_body: proof -> proof_body
(** primitive operations **)
val proof_combt: proof * term list -> proof
@@ -107,11 +106,11 @@
val equal_intr: term -> term -> proof -> proof -> proof
val equal_elim: term -> term -> proof -> proof -> proof
val axm_proof: string -> term -> proof
- val oracle_proof: string -> term -> proof
+ val oracle_proof: string -> term -> oracle * proof
val promise_proof: theory -> serial -> term -> proof
- val fulfill_proof: theory -> (serial * proof) list -> proof_body -> proof_body
+ val fulfill_proof: theory -> (serial * proof_body) list -> proof_body -> proof_body
val thm_proof: theory -> string -> term list -> term ->
- (serial * proof future) list -> proof_body -> pthm * proof
+ (serial * proof_body future) list -> proof_body -> pthm * proof
val get_name: term list -> term -> proof -> string
(** rewriting on proof terms **)
@@ -214,26 +213,32 @@
val oracle_ord = prod_ord fast_string_ord TermOrd.fast_term_ord;
fun thm_ord ((i, _): pthm, (j, _)) = int_ord (j, i);
-fun make_body prf =
+val merge_oracles = OrdList.union oracle_ord;
+val merge_thms = OrdList.union thm_ord;
+
+val all_oracles_of =
+ let
+ fun collect (PBody {oracles, thms, ...}) = thms |> fold (fn (i, (_, _, body)) => fn (x, seen) =>
+ if Inttab.defined seen i then (x, seen)
+ else
+ let
+ val body' = Future.join body;
+ val (x', seen') = collect body' (x, Inttab.update (i, ()) seen);
+ in (merge_oracles oracles x', seen') end);
+ in fn body => #1 (collect body ([], Inttab.empty)) end;
+
+fun approximate_proof_body prf =
let
val (oracles, thms) = fold_proof_atoms false
(fn Oracle (s, prop, _) => apfst (cons (s, prop))
| PThm (i, ((name, prop, _), body)) => apsnd (cons (i, (name, prop, body)))
| _ => I) [prf] ([], []);
- in (OrdList.make oracle_ord oracles, OrdList.make thm_ord thms) end;
-
-fun make_proof_body prf =
- let val (oracles, thms) = make_body prf
- in PBody {oracles = oracles, thms = thms, proof = prf} end;
-
-val make_oracles = #1 o make_body;
-val make_thms = #2 o make_body;
-
-val merge_oracles = OrdList.union oracle_ord;
-val merge_thms = OrdList.union thm_ord;
-
-fun merge_body (oracles1, thms1) (oracles2, thms2) =
- (merge_oracles oracles1 oracles2, merge_thms thms1 thms2);
+ in
+ PBody
+ {oracles = OrdList.make oracle_ord oracles,
+ thms = OrdList.make thm_ord thms,
+ proof = prf}
+ end;
(***** proof objects with different levels of detail *****)
@@ -930,8 +935,8 @@
val dummy = Const (Term.dummy_patternN, dummyT);
fun oracle_proof name prop =
- if !proofs = 0 then Oracle (name, dummy, NONE)
- else gen_axm_proof Oracle name prop;
+ if ! proofs = 0 then ((name, dummy), Oracle (name, dummy, NONE))
+ else ((name, prop), gen_axm_proof Oracle name prop);
fun shrink_proof thy =
let
@@ -1235,16 +1240,17 @@
in Promise (i, prop, map TVar (Term.add_tvars prop [])) end;
fun fulfill_proof _ [] body0 = body0
- | fulfill_proof thy promises body0 =
+ | fulfill_proof thy ps body0 =
let
val PBody {oracles = oracles0, thms = thms0, proof = proof0} = body0;
- val (oracles, thms) = fold (merge_body o make_body o #2) promises (oracles0, thms0);
+ val oracles = fold (fn (_, PBody {oracles, ...}) => merge_oracles oracles) ps oracles0;
+ val thms = fold (fn (_, PBody {thms, ...}) => merge_thms thms) ps thms0;
+ val proofs = fold (fn (i, PBody {proof, ...}) => Inttab.update (i, proof)) ps Inttab.empty;
- val tab = Inttab.make promises;
fun fill (Promise (i, prop, Ts)) =
- (case Inttab.lookup tab i of
+ (case Inttab.lookup proofs i of
NONE => NONE
- | SOME p => SOME (instantiate (Term.add_tvars prop [] ~~ Ts, []) p))
+ | SOME prf => SOME (instantiate (Term.add_tvars prop [] ~~ Ts, []) prf))
| fill _ = NONE;
val (rules, procs) = get_data thy;
val proof = rewrite_prf fst (rules, K fill :: procs) proof0;
--- a/src/Pure/thm.ML Thu Mar 26 14:10:48 2009 +0000
+++ b/src/Pure/thm.ML Thu Mar 26 14:30:20 2009 +0000
@@ -1662,7 +1662,7 @@
fun proof_body_of (Thm (Deriv {open_promises, promises, body, ...}, {thy_ref, ...})) =
let
val _ = Exn.release_all (map (Future.join_result o #2) (rev open_promises));
- val ps = map (apsnd (raw_proof_of o Future.join)) promises;
+ val ps = map (apsnd (raw_proof_body_of o Future.join)) promises;
in Pt.fulfill_proof (Theory.deref thy_ref) ps body end;
val proof_of = Proofterm.proof_of o proof_body_of;
@@ -1680,7 +1680,7 @@
val {thy_ref, hyps, prop, tpairs, ...} = args;
val _ = null tpairs orelse raise THM ("put_name: unsolved flex-flex constraints", 0, [thm]);
- val ps = map (apsnd (Future.map proof_of)) promises;
+ val ps = map (apsnd (Future.map proof_body_of)) promises;
val thy = Theory.deref thy_ref;
val (pthm, proof) = Pt.thm_proof thy name hyps prop ps body;
@@ -1701,8 +1701,8 @@
if T <> propT then
raise THM ("Oracle's result must have type prop: " ^ name, 0, [])
else
- let val prf = Pt.oracle_proof name prop in
- Thm (make_deriv ~1 [] [] (Pt.make_oracles prf) [] prf,
+ let val (ora, prf) = Pt.oracle_proof name prop in
+ Thm (make_deriv ~1 [] [] [ora] [] prf,
{thy_ref = Theory.merge_refs (thy_ref1, thy_ref2),
tags = [],
maxidx = maxidx,
--- a/src/Tools/induct.ML Thu Mar 26 14:10:48 2009 +0000
+++ b/src/Tools/induct.ML Thu Mar 26 14:30:20 2009 +0000
@@ -259,16 +259,15 @@
spec setN Args.const >> add_pred ||
Scan.lift Args.del >> K del;
-val cases_att = attrib cases_type cases_pred cases_del;
-val induct_att = attrib induct_type induct_pred induct_del;
-val coinduct_att = attrib coinduct_type coinduct_pred coinduct_del;
-
in
val attrib_setup =
- Attrib.setup @{binding cases} cases_att "declaration of cases rule" #>
- Attrib.setup @{binding induct} induct_att "declaration of induction rule" #>
- Attrib.setup @{binding coinduct} coinduct_att "declaration of coinduction rule";
+ Attrib.setup @{binding cases} (attrib cases_type cases_pred cases_del)
+ "declaration of cases rule" #>
+ Attrib.setup @{binding induct} (attrib induct_type induct_pred induct_del)
+ "declaration of induction rule" #>
+ Attrib.setup @{binding coinduct} (attrib coinduct_type coinduct_pred coinduct_del)
+ "declaration of coinduction rule";
end;
@@ -735,23 +734,29 @@
in
-val cases_meth =
- P.and_list' (Scan.repeat (unless_more_args inst)) -- Scan.option cases_rule >>
- (fn (insts, opt_rule) => fn ctxt =>
- METHOD_CASES (fn facts => Seq.DETERM (HEADGOAL (cases_tac ctxt insts opt_rule facts))));
+val cases_setup =
+ Method.setup @{binding cases}
+ (P.and_list' (Scan.repeat (unless_more_args inst)) -- Scan.option cases_rule >>
+ (fn (insts, opt_rule) => fn ctxt =>
+ METHOD_CASES (fn facts => Seq.DETERM (HEADGOAL (cases_tac ctxt insts opt_rule facts)))))
+ "case analysis on types or predicates/sets";
-val induct_meth =
- P.and_list' (Scan.repeat (unless_more_args def_inst)) --
- (arbitrary -- taking -- Scan.option induct_rule) >>
- (fn (insts, ((arbitrary, taking), opt_rule)) => fn ctxt =>
- RAW_METHOD_CASES (fn facts =>
- Seq.DETERM (HEADGOAL (induct_tac ctxt insts arbitrary taking opt_rule facts))));
+val induct_setup =
+ Method.setup @{binding induct}
+ (P.and_list' (Scan.repeat (unless_more_args def_inst)) --
+ (arbitrary -- taking -- Scan.option induct_rule) >>
+ (fn (insts, ((arbitrary, taking), opt_rule)) => fn ctxt =>
+ RAW_METHOD_CASES (fn facts =>
+ Seq.DETERM (HEADGOAL (induct_tac ctxt insts arbitrary taking opt_rule facts)))))
+ "induction on types or predicates/sets";
-val coinduct_meth =
- Scan.repeat (unless_more_args inst) -- taking -- Scan.option coinduct_rule >>
- (fn ((insts, taking), opt_rule) => fn ctxt =>
- RAW_METHOD_CASES (fn facts =>
- Seq.DETERM (HEADGOAL (coinduct_tac ctxt insts taking opt_rule facts))));
+val coinduct_setup =
+ Method.setup @{binding coinduct}
+ (Scan.repeat (unless_more_args inst) -- taking -- Scan.option coinduct_rule >>
+ (fn ((insts, taking), opt_rule) => fn ctxt =>
+ RAW_METHOD_CASES (fn facts =>
+ Seq.DETERM (HEADGOAL (coinduct_tac ctxt insts taking opt_rule facts)))))
+ "coinduction on types or predicates/sets";
end;
@@ -759,10 +764,6 @@
(** theory setup **)
-val setup =
- attrib_setup #>
- Method.setup @{binding cases} cases_meth "case analysis on types or predicates/sets" #>
- Method.setup @{binding induct} induct_meth "induction on types or predicates/sets" #>
- Method.setup @{binding coinduct} coinduct_meth "coinduction on types or predicates/sets";
+val setup = attrib_setup #> cases_setup #> induct_setup #> coinduct_setup;
end;
--- a/src/ZF/Tools/ind_cases.ML Thu Mar 26 14:10:48 2009 +0000
+++ b/src/ZF/Tools/ind_cases.ML Thu Mar 26 14:30:20 2009 +0000
@@ -57,14 +57,14 @@
(* ind_cases method *)
-val mk_cases_meth = Scan.lift (Scan.repeat1 Args.name_source) >>
- (fn props => fn ctxt =>
- props
- |> map (smart_cases (ProofContext.theory_of ctxt) (local_simpset_of ctxt) (Syntax.read_prop ctxt))
- |> Method.erule 0);
-
val setup =
- Method.setup @{binding "ind_cases"} mk_cases_meth "dynamic case analysis on sets";
+ Method.setup @{binding "ind_cases"}
+ (Scan.lift (Scan.repeat1 Args.name_source) >>
+ (fn props => fn ctxt =>
+ props
+ |> map (smart_cases (ProofContext.theory_of ctxt) (local_simpset_of ctxt) (Syntax.read_prop ctxt))
+ |> Method.erule 0))
+ "dynamic case analysis on sets";
(* outer syntax *)
--- a/src/ZF/Tools/typechk.ML Thu Mar 26 14:10:48 2009 +0000
+++ b/src/ZF/Tools/typechk.ML Thu Mar 26 14:30:20 2009 +0000
@@ -109,11 +109,13 @@
(* concrete syntax *)
-val typecheck_meth =
- 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))));
+val typecheck_setup =
+ Method.setup @{binding typecheck}
+ (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)))))
+ "ZF type-checking";
val _ =
OuterSyntax.improper_command "print_tcset" "print context of ZF typecheck" OuterKeyword.diag
@@ -125,7 +127,7 @@
val setup =
Attrib.setup @{binding TC} (Attrib.add_del TC_add TC_del) "declaration of type-checking rule" #>
- Method.setup @{binding typecheck} typecheck_meth "ZF type-checking" #>
+ typecheck_setup #>
Simplifier.map_simpset (fn ss => ss setSolver type_solver);
end;