# HG changeset patch # User wenzelm # Date 1469007851 -7200 # Node ID 59eff6e56d816e98db711c21be16fc597236a5f7 # Parent f8213afea07f2575f6fd3b178d4d90bff249061c moved method "use" to Pure; more documentation; diff -r f8213afea07f -r 59eff6e56d81 NEWS --- 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 \simp add: ...\) diff -r f8213afea07f -r 59eff6e56d81 src/Doc/Isar_Ref/Proof.thy --- 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"} & : & \proof(state) \ proof(chain)\ \\ @{command_def "using"} & : & \proof(prove) \ proof(prove)\ \\ @{command_def "unfolding"} & : & \proof(prove) \ proof(prove)\ \\ + @{method_def "use"} & : & \method\ \\ + @{fact_def "method_facts"} & : & \fact\ \\ \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} \} \<^descr> @{command "note"}~\a = b\<^sub>1 \ b\<^sub>n\ recalls existing facts \b\<^sub>1, \, b\<^sub>n\, @@ -323,14 +327,22 @@ \ this\''; thus the forward chaining is from earlier facts together with the current ones. - \<^descr> @{command "using"}~\b\<^sub>1 \ b\<^sub>n\ 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"}~\b\<^sub>1 \ b\<^sub>n\ augments the facts to be used by a + subsequent refinement step (such as @{command_ref "apply"} or @{command_ref + "proof"}). \<^descr> @{command "unfolding"}~\b\<^sub>1 \ b\<^sub>n\ is structurally similar to @{command - "using"}, but unfolds definitional equations \b\<^sub>1, \ b\<^sub>n\ throughout the + "using"}, but unfolds definitional equations \b\<^sub>1 \ b\<^sub>n\ throughout the goal state and facts. + \<^descr> \<^theory_text>\(use b\<^sub>1 \ b\<^sub>n in method)\ 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"}~\nothing\'' has no effect apart from diff -r f8213afea07f -r 59eff6e56d81 src/HOL/Eisbach/Eisbach.thy --- 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 = \ - Attrib.thms -- (Scan.lift @{keyword "in"} |-- Method_Closure.method_text) >> - (fn (thms, text) => fn ctxt => fn _ => Method_Closure.method_evaluate text ctxt thms) -\ \indicate method facts and context for method expression\ - end diff -r f8213afea07f -r 59eff6e56d81 src/HOL/Eisbach/Eisbach_Tools.thy --- 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 @@ \ method_setup catch = \ - 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 diff -r f8213afea07f -r 59eff6e56d81 src/HOL/Eisbach/match_method.ML --- 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) diff -r f8213afea07f -r 59eff6e56d81 src/HOL/Eisbach/method_closure.ML --- 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)) "" diff -r f8213afea07f -r 59eff6e56d81 src/Pure/Isar/method.ML --- 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!*)