--- a/NEWS Wed Jul 20 11:11:07 2016 +0200
+++ b/NEWS Wed Jul 20 11:44:11 2016 +0200
@@ -145,8 +145,8 @@
"method_facts". This is particularly useful for Eisbach method
definitions.
-* Eisbach provides method "use" to modify the main facts of a given
-method expression, e.g.
+* Proof method "use" allows to modify the main facts of a given method
+expression, e.g.
(use facts in simp)
(use facts in \<open>simp add: ...\<close>)
--- a/src/Doc/Isar_Ref/Proof.thy Wed Jul 20 11:11:07 2016 +0200
+++ b/src/Doc/Isar_Ref/Proof.thy Wed Jul 20 11:44:11 2016 +0200
@@ -283,6 +283,8 @@
@{command_def "with"} & : & \<open>proof(state) \<rightarrow> proof(chain)\<close> \\
@{command_def "using"} & : & \<open>proof(prove) \<rightarrow> proof(prove)\<close> \\
@{command_def "unfolding"} & : & \<open>proof(prove) \<rightarrow> proof(prove)\<close> \\
+ @{method_def "use"} & : & \<open>method\<close> \\
+ @{fact_def "method_facts"} & : & \<open>fact\<close> \\
\end{matharray}
New facts are established either by assumption or proof of local statements.
@@ -300,6 +302,8 @@
;
(@@{command from} | @@{command with} | @@{command using} | @@{command unfolding})
(@{syntax thms} + @'and')
+ ;
+ @{method use} @{syntax thms} @'in' @{syntax method}
\<close>}
\<^descr> @{command "note"}~\<open>a = b\<^sub>1 \<dots> b\<^sub>n\<close> recalls existing facts \<open>b\<^sub>1, \<dots>, b\<^sub>n\<close>,
@@ -323,14 +327,22 @@
\<AND> this\<close>''; thus the forward chaining is from earlier facts together
with the current ones.
- \<^descr> @{command "using"}~\<open>b\<^sub>1 \<dots> b\<^sub>n\<close> augments the facts being currently
- indicated for use by a subsequent refinement step (such as @{command_ref
- "apply"} or @{command_ref "proof"}).
+ \<^descr> @{command "using"}~\<open>b\<^sub>1 \<dots> b\<^sub>n\<close> augments the facts to be used by a
+ subsequent refinement step (such as @{command_ref "apply"} or @{command_ref
+ "proof"}).
\<^descr> @{command "unfolding"}~\<open>b\<^sub>1 \<dots> b\<^sub>n\<close> is structurally similar to @{command
- "using"}, but unfolds definitional equations \<open>b\<^sub>1, \<dots> b\<^sub>n\<close> throughout the
+ "using"}, but unfolds definitional equations \<open>b\<^sub>1 \<dots> b\<^sub>n\<close> throughout the
goal state and facts.
+ \<^descr> \<^theory_text>\<open>(use b\<^sub>1 \<dots> b\<^sub>n in method)\<close> uses the facts in the given method
+ expression. The facts provided by the proof state (via @{command "using"}
+ etc.) are ignored, but it is possible to refer to @{fact method_facts}
+ explicitly.
+
+ \<^descr> @{fact method_facts} is a dynamic fact that refers to the currently used
+ facts of the goal state.
+
Forward chaining with an empty list of theorems is the same as not chaining
at all. Thus ``@{command "from"}~\<open>nothing\<close>'' has no effect apart from
--- a/src/HOL/Eisbach/Eisbach.thy Wed Jul 20 11:11:07 2016 +0200
+++ b/src/HOL/Eisbach/Eisbach.thy Wed Jul 20 11:44:11 2016 +0200
@@ -22,9 +22,4 @@
method solves methods m = (m; fail)
-method_setup use = \<open>
- Attrib.thms -- (Scan.lift @{keyword "in"} |-- Method_Closure.method_text) >>
- (fn (thms, text) => fn ctxt => fn _ => Method_Closure.method_evaluate text ctxt thms)
-\<close> \<open>indicate method facts and context for method expression\<close>
-
end
--- a/src/HOL/Eisbach/Eisbach_Tools.thy Wed Jul 20 11:11:07 2016 +0200
+++ b/src/HOL/Eisbach/Eisbach_Tools.thy Wed Jul 20 11:44:11 2016 +0200
@@ -55,11 +55,11 @@
\<close>
method_setup catch = \<open>
- Method_Closure.method_text -- Method_Closure.method_text >>
+ Method.text_closure -- Method.text_closure >>
(fn (text, text') => fn ctxt => fn using => fn st =>
let
- val method = Method_Closure.method_evaluate text ctxt using;
- val backup_results = Method_Closure.method_evaluate text' ctxt using st;
+ val method = Method.evaluate_runtime text ctxt using;
+ val backup_results = Method.evaluate_runtime text' ctxt using st;
in
(case try method st of
SOME seq => try_map backup_results seq
--- a/src/HOL/Eisbach/match_method.ML Wed Jul 20 11:11:07 2016 +0200
+++ b/src/HOL/Eisbach/match_method.ML Wed Jul 20 11:44:11 2016 +0200
@@ -100,7 +100,7 @@
(case Token.get_value body of
SOME (Token.Source src) =>
let
- val text = Method_Closure.read ctxt src;
+ val text = Method.read ctxt src;
val ts' =
map
(fn (b, (Parse_Tools.Real_Val v, match_args)) =>
@@ -201,7 +201,7 @@
|> (fn ctxt => fold2 upd_ctxt binds pats ([], ctxt) |> apfst rev)
||> Proof_Context.restore_mode ctxt;
- val (text, src) = Method_Closure.read_closure_input ctxt6 (Token.input_of body);
+ val (text, src) = Method.read_closure_input ctxt6 (Token.input_of body);
val morphism =
Variable.export_morphism ctxt6
@@ -645,12 +645,12 @@
Match_Fact net =>
make_fact_matches goal_ctxt (Item_Net.retrieve net)
|> Seq.map (fn (text, ctxt') =>
- Method_Closure.method_evaluate text ctxt' using (ctxt', st)
+ Method.evaluate_runtime text ctxt' using (ctxt', st)
|> Seq.filter_results |> Seq.map (fn (_, thm) => (outer_ctxt, thm)))
| Match_Term net =>
make_term_matches goal_ctxt (Item_Net.retrieve net)
|> Seq.map (fn (text, ctxt') =>
- Method_Closure.method_evaluate text ctxt' using (ctxt', st)
+ Method.evaluate_runtime text ctxt' using (ctxt', st)
|> Seq.filter_results |> Seq.map (fn (_, thm) => (outer_ctxt, thm)))
| match_kind =>
if Thm.no_prems st then Seq.empty
@@ -721,7 +721,7 @@
end;
fun apply_text (text, ctxt') =
- Method_Closure.method_evaluate text ctxt' using (ctxt', focused_goal)
+ Method.evaluate_runtime text ctxt' using (ctxt', focused_goal)
|> Seq.filter_results
|> Seq.maps (Seq.DETERM do_retrofit)
--- a/src/HOL/Eisbach/method_closure.ML Wed Jul 20 11:11:07 2016 +0200
+++ b/src/HOL/Eisbach/method_closure.ML Wed Jul 20 11:44:11 2016 +0200
@@ -10,11 +10,6 @@
signature METHOD_CLOSURE =
sig
- val read: Proof.context -> Token.src -> Method.text
- val read_closure: Proof.context -> Token.src -> Method.text * Token.src
- val read_closure_input: Proof.context -> Input.source -> Method.text * Token.src
- val method_text: Method.text context_parser
- val method_evaluate: Method.text -> Proof.context -> Method.method
val apply_method: Proof.context -> string -> term list -> thm list list ->
(Proof.context -> Method.method) list -> Proof.context -> thm list -> context_tactic
val method: binding -> (binding * typ option * mixfix) list -> binding list ->
@@ -82,51 +77,7 @@
end;
-(* read method text *)
-
-fun read ctxt src =
- (case Scan.read Token.stopper (Parse.!!! (Method.parser 0 --| Scan.ahead Parse.eof)) src of
- SOME (text, range) =>
- if Method.checked_text text then text
- else (Method.report (text, range); Method.check_text ctxt text)
- | NONE => error ("Failed to parse method" ^ Position.here (#1 (Token.range_of src))));
-
-fun read_closure ctxt src0 =
- let
- val src1 = map Token.init_assignable src0;
- val text = read ctxt src1 |> Method.map_source (Method.method_closure ctxt);
- val src2 = map Token.closure src1;
- in (text, src2) end;
-
-fun read_closure_input ctxt =
- Input.source_explode #>
- Token.read_no_commands (Thy_Header.get_keywords' ctxt) (Scan.one Token.not_eof) #>
- read_closure ctxt;
-
-val method_text =
- Args.context -- Scan.lift (Parse.token Parse.text) >> (fn (ctxt, tok) =>
- (case Token.get_value tok of
- SOME (Token.Source src) => read ctxt src
- | _ =>
- let
- val (text, src) = read_closure_input ctxt (Token.input_of tok);
- val _ = Token.assign (SOME (Token.Source src)) tok;
- in text end));
-
-
-(* evaluate method text *)
-
-fun method_evaluate text ctxt =
- let
- val text' =
- text |> (Method.map_source o map o Token.map_facts)
- (fn SOME name =>
- (case Proof_Context.lookup_fact ctxt name of
- SOME {dynamic = true, thms} => K thms
- | _ => I)
- | NONE => I);
- val ctxt' = Config.put Method.closure false ctxt;
- in fn facts => Method.RUNTIME (fn st => Method.evaluate text' ctxt' facts st) end;
+(* instantiate and evaluate method text *)
fun method_instantiate vars body ts ctxt =
let
@@ -134,7 +85,7 @@
val subst = fold (Pattern.match thy) (vars ~~ ts) (Vartab.empty, Vartab.empty);
val morphism = Morphism.term_morphism "method_instantiate" (Envir.subst_term subst);
val body' = (Method.map_source o map) (Token.transform morphism) body;
- in method_evaluate body' ctxt end;
+ in Method.evaluate_runtime body' ctxt end;
@@ -215,12 +166,12 @@
let
fun bind_method (name, text) ctxt =
let
- val method = method_evaluate text;
+ val method = Method.evaluate_runtime text;
val inner_update = method o update_dynamic_method (name, K (method ctxt));
in update_dynamic_method (name, inner_update) ctxt end;
fun rep [] x = Scan.succeed [] x
- | rep (m :: ms) x = ((method_text >> pair m) ::: rep ms) x;
+ | rep (m :: ms) x = ((Method.text_closure >> pair m) ::: rep ms) x;
in rep method_args >> fold bind_method end;
fun gen_method add_fixes name vars uses declares methods source lthy =
@@ -256,7 +207,7 @@
|> put_recursive_method (full_name, fn _ => fn _ => Method.fail);
val (text, src) =
- read_closure (Config.put Proof_Context.dynamic_facts_dummy true lthy3) source;
+ Method.read_closure (Config.put Proof_Context.dynamic_facts_dummy true lthy3) source;
val morphism =
Variable.export_morphism lthy3
@@ -273,7 +224,7 @@
|> Proof_Context.restore_naming lthy
|> put_closure name
{vars = term_args', named_thms = named_thms, methods = method_args, body = text'}
- |> Method.local_setup name
+ |> Method.local_setup name
(Args.context :|-- (fn ctxt =>
let val {body, vars, ...} = get_closure ctxt full_name in
parser vars (recursive_method full_name vars body) end)) ""
--- a/src/Pure/Isar/method.ML Wed Jul 20 11:11:07 2016 +0200
+++ b/src/Pure/Isar/method.ML Wed Jul 20 11:44:11 2016 +0200
@@ -92,6 +92,7 @@
val RUNTIME: context_tactic -> context_tactic
val sleep: Time.time -> context_tactic
val evaluate: text -> Proof.context -> method
+ val evaluate_runtime: text -> Proof.context -> method
type modifier = {init: Proof.context -> Proof.context, attribute: attribute, pos: Position.T}
val modifier: attribute -> Position.T -> modifier
val old_section_parser: bool Config.T
@@ -103,6 +104,10 @@
val report: text_range -> unit
val parser: int -> text_range parser
val parse: text_range parser
+ val read: Proof.context -> Token.src -> text
+ val read_closure: Proof.context -> Token.src -> text * Token.src
+ val read_closure_input: Proof.context -> Input.source -> text * Token.src
+ val text_closure: text context_parser
end;
structure Method: METHOD =
@@ -576,6 +581,18 @@
end;
+fun evaluate_runtime text ctxt =
+ let
+ val text' =
+ text |> (map_source o map o Token.map_facts)
+ (fn SOME name =>
+ (case Proof_Context.lookup_fact ctxt name of
+ SOME {dynamic = true, thms} => K thms
+ | _ => I)
+ | NONE => I);
+ val ctxt' = Config.put closure false ctxt;
+ in fn facts => RUNTIME (fn st => evaluate text' ctxt' facts st) end;
+
(** concrete syntax **)
@@ -743,6 +760,38 @@
end;
+(* read method text *)
+
+fun read ctxt src =
+ (case Scan.read Token.stopper (Parse.!!! (parser 0 --| Scan.ahead Parse.eof)) src of
+ SOME (text, range) =>
+ if checked_text text then text
+ else (report (text, range); check_text ctxt text)
+ | NONE => error ("Failed to parse method" ^ Position.here (#1 (Token.range_of src))));
+
+fun read_closure ctxt src0 =
+ let
+ val src1 = map Token.init_assignable src0;
+ val text = read ctxt src1 |> map_source (method_closure ctxt);
+ val src2 = map Token.closure src1;
+ in (text, src2) end;
+
+fun read_closure_input ctxt =
+ Input.source_explode #>
+ Token.read_no_commands (Thy_Header.get_keywords' ctxt) (Scan.one Token.not_eof) #>
+ read_closure ctxt;
+
+val text_closure =
+ Args.context -- Scan.lift (Parse.token Parse.text) >> (fn (ctxt, tok) =>
+ (case Token.get_value tok of
+ SOME (Token.Source src) => read ctxt src
+ | _ =>
+ let
+ val (text, src) = read_closure_input ctxt (Token.input_of tok);
+ val _ = Token.assign (SOME (Token.Source src)) tok;
+ in text end));
+
+
(* theory setup *)
val _ = Theory.setup
@@ -792,7 +841,11 @@
setup @{binding tactic} (parse_tactic >> (K o METHOD))
"ML tactic as proof method" #>
setup @{binding raw_tactic} (parse_tactic >> (fn tac => fn _ => CONTEXT_TACTIC o tac))
- "ML tactic as raw proof method");
+ "ML tactic as raw proof method" #>
+ setup @{binding use}
+ (Attrib.thms -- (Scan.lift (Parse.$$$ "in") |-- text_closure) >>
+ (fn (thms, text) => fn ctxt => fn _ => evaluate_runtime text ctxt thms))
+ "indicate method facts and context for method expression");
(*final declarations of this structure!*)