# HG changeset patch # User wenzelm # Date 1425929613 -3600 # Node ID 49e498cedd02f9dd499018dc6da30cb344a0ee00 # Parent 2441a80fb6c1daa6f6fad7cb630a0f6fdcf0a7e2 support structural composition (THEN_ALL_NEW) for proof methods; clarified preparation for goal restriction: Goal.conjunction_tac only once; export Method.parse0, notably for Eisbach; more explicit type cases_state; diff -r 2441a80fb6c1 -r 49e498cedd02 NEWS --- a/NEWS Mon Mar 09 11:32:32 2015 +0100 +++ b/NEWS Mon Mar 09 20:33:33 2015 +0100 @@ -6,6 +6,9 @@ *** General *** +* Structural composition of proof methods (meth1; meth2) in Isar +corresponds to (tac1 THEN_ALL_NEW tac2) in ML. + * Generated schematic variables in standard format of exported facts are incremented to avoid material in the proof context. Rare INCOMPATIBILITY, explicit instantiation sometimes needs to refer to diff -r 2441a80fb6c1 -r 49e498cedd02 src/Doc/Isar_Ref/Proof.thy --- a/src/Doc/Isar_Ref/Proof.thy Mon Mar 09 11:32:32 2015 +0100 +++ b/src/Doc/Isar_Ref/Proof.thy Mon Mar 09 20:33:33 2015 +0100 @@ -531,38 +531,54 @@ subsection \Proof method expressions \label{sec:proof-meth}\ -text \Proof methods are either basic ones, or expressions composed - of methods via ``@{verbatim ","}'' (sequential composition), - ``@{verbatim "|"}'' (alternative choices), ``@{verbatim "?"}'' - (try), ``@{verbatim "+"}'' (repeat at least once), ``@{verbatim - "["}@{text n}@{verbatim "]"}'' (restriction to first @{text n} - sub-goals, with default @{text "n = 1"}). In practice, proof - methods are usually just a comma separated list of @{syntax - nameref}~@{syntax args} specifications. Note that parentheses may - be dropped for single method specifications (with no arguments). +text \Proof methods are either basic ones, or expressions composed of + methods via ``@{verbatim ","}'' (sequential composition), ``@{verbatim + ";"}'' (structural composition), ``@{verbatim "|"}'' (alternative + choices), ``@{verbatim "?"}'' (try), ``@{verbatim "+"}'' (repeat at least + once), ``@{verbatim "["}@{text n}@{verbatim "]"}'' (restriction to first + @{text n} subgoals). In practice, proof methods are usually just a comma + separated list of @{syntax nameref}~@{syntax args} specifications. Note + that parentheses may be dropped for single method specifications (with no + arguments). The syntactic precedence of method combinators is @{verbatim + "|"} @{verbatim ";"} @{verbatim ","} @{verbatim "[]"} @{verbatim "+"} + @{verbatim "?"} (from low to high). @{rail \ @{syntax_def method}: (@{syntax nameref} | '(' methods ')') (() | '?' | '+' | '[' @{syntax nat}? ']') ; - methods: (@{syntax nameref} @{syntax args} | @{syntax method}) + (',' | '|') + methods: (@{syntax nameref} @{syntax args} | @{syntax method}) + (',' | ';' | '|') \} - Proper Isar proof methods do \emph{not} admit arbitrary goal - addressing, but refer either to the first sub-goal or all sub-goals - uniformly. The goal restriction operator ``@{text "[n]"}'' - evaluates a method expression within a sandbox consisting of the - first @{text n} sub-goals (which need to exist). For example, the - method ``@{text "simp_all[3]"}'' simplifies the first three - sub-goals, while ``@{text "(rule foo, simp_all)[]"}'' simplifies all - new goals that emerge from applying rule @{text "foo"} to the - originally first one. + Regular Isar proof methods do \emph{not} admit direct goal addressing, but + refer to the first subgoal or to all subgoals uniformly. Nonetheless, + the subsequent mechanisms allow to imitate the effect of subgoal + addressing that is known from ML tactics. + + \medskip Goal \emph{restriction} means the proof state is wrapped-up in a + way that certain subgoals are exposed, and other subgoals are ``parked'' + elsewhere. Thus a proof method has no other chance than to operate on the + subgoals that are presently exposed. - Improper methods, notably tactic emulations, offer a separate - low-level goal addressing scheme as explicit argument to the - individual tactic being involved. Here ``@{text "[!]"}'' refers to - all goals, and ``@{text "[n-]"}'' to all goals starting from @{text - "n"}. + Structural composition ``@{text m\<^sub>1}@{verbatim ";"}~@{text m\<^sub>2}'' means + that method @{text m\<^sub>1} is applied with restriction to the first subgoal, + then @{text m\<^sub>2} is applied consecutively with restriction to each subgoal + that has newly emerged due to @{text m\<^sub>1}. This is analogous to the tactic + combinator @{ML THEN_ALL_NEW} in Isabelle/ML, see also @{cite + "isabelle-implementation"}. For example, @{text "(rule r; blast)"} applies + rule @{text "r"} and then solves all new subgoals by @{text blast}. + + Moreover, the explicit goal restriction operator ``@{text "[n]"}'' exposes + only the first @{text n} subgoals (which need to exist), with default + @{text "n = 1"}. For example, the method expression ``@{text + "simp_all[3]"}'' simplifies the first three subgoals, while ``@{text + "(rule r, simp_all)[]"}'' simplifies all new goals that emerge from + applying rule @{text "r"} to the originally first one. + + \medskip Improper methods, notably tactic emulations, offer low-level goal + addressing as explicit argument to the individual tactic being involved. + Here ``@{text "[!]"}'' refers to all goals, and ``@{text "[n-]"}'' to all + goals starting from @{text "n"}. @{rail \ @{syntax_def goal_spec}: diff -r 2441a80fb6c1 -r 49e498cedd02 src/Pure/Isar/method.ML --- a/src/Pure/Isar/method.ML Mon Mar 09 11:32:32 2015 +0100 +++ b/src/Pure/Isar/method.ML Mon Mar 09 20:33:33 2015 +0100 @@ -41,7 +41,7 @@ val set_tactic: (morphism -> thm list -> tactic) -> Context.generic -> Context.generic type combinator_info val no_combinator_info: combinator_info - datatype combinator = Then | Orelse | Try | Repeat1 | Select_Goals of int + datatype combinator = Then | Then_All_New | Orelse | Try | Repeat1 | Select_Goals of int datatype text = Source of Token.src | Basic of Proof.context -> method | @@ -75,6 +75,7 @@ val position: text_range option -> Position.T val reports_of: text_range -> Position.report list val report: text_range -> unit + val parse0: text_range parser val parse: text_range parser end; @@ -299,7 +300,7 @@ fun combinator_info keywords = Combinator_Info {keywords = keywords}; val no_combinator_info = combinator_info []; -datatype combinator = Then | Orelse | Try | Repeat1 | Select_Goals of int; +datatype combinator = Then | Then_All_New | Orelse | Try | Repeat1 | Select_Goals of int; datatype text = Source of Token.src | @@ -408,28 +409,40 @@ local -fun APPEND_CASES (meth: cases_tactic) (cases, st) = - meth st |> Seq.map (fn (cases', st') => (cases @ cases', st')); +fun APPEND_CASES (tac: cases_tactic) ((cases, st): cases_state) = + tac st |> Seq.map (fn (cases', st') => (cases @ cases', st')); -fun BYPASS_CASES (tac: tactic) (cases, st) = +fun BYPASS_CASES (tac: tactic) ((cases, st): cases_state) = tac st |> Seq.map (pair cases); val op THEN = Seq.THEN; -fun SELECT_GOALS n method = - BYPASS_CASES - (ALLGOALS Goal.conjunction_tac THEN PRIMITIVE (Goal.restrict 1 n) THEN Goal.conjunction_tac 1) - THEN method - THEN BYPASS_CASES (PRIMITIVE (Goal.unrestrict 1)); +val preparation = BYPASS_CASES (ALLGOALS Goal.conjunction_tac); + +fun RESTRICT_GOAL i n method = + BYPASS_CASES (PRIMITIVE (Goal.restrict i n)) THEN + method THEN + BYPASS_CASES (PRIMITIVE (Goal.unrestrict i)); + +fun SELECT_GOAL method i = RESTRICT_GOAL i 1 method; + +fun (method1 THEN_ALL_NEW method2) i (st: cases_state) = + st |> (method1 i THEN (fn st' => + Seq.INTERVAL method2 i (i + Thm.nprems_of (snd st') - Thm.nprems_of (snd st)) st')); fun COMBINATOR1 comb [meth] = comb meth | COMBINATOR1 _ _ = raise Fail "Method combinator requires exactly one argument"; fun combinator Then = Seq.EVERY + | combinator Then_All_New = + (fn [] => Seq.single + | methods => + preparation THEN foldl1 (op THEN_ALL_NEW) (map SELECT_GOAL methods) 1) | combinator Orelse = Seq.FIRST | combinator Try = COMBINATOR1 Seq.TRY | combinator Repeat1 = COMBINATOR1 Seq.REPEAT1 - | combinator (Select_Goals n) = COMBINATOR1 (SELECT_GOALS n); + | combinator (Select_Goals n) = + COMBINATOR1 (fn method => preparation THEN RESTRICT_GOAL 1 n method); in @@ -548,35 +561,38 @@ local -fun meth4 x = +fun meth5 x = (Parse.position Parse.xname >> (fn name => Source (Token.src name [])) || Scan.ahead Parse.cartouche |-- Parse.not_eof >> (fn tok => Source (Token.src ("cartouche", Token.pos_of tok) [tok])) || Parse.$$$ "(" |-- Parse.!!! (meth0 --| Parse.$$$ ")")) x -and meth3 x = - (meth4 -- Parse.position (Parse.$$$ "?") +and meth4 x = + (meth5 -- Parse.position (Parse.$$$ "?") >> (fn (m, (_, pos)) => Combinator (combinator_info [pos], Try, [m])) || - meth4 -- Parse.position (Parse.$$$ "+") + meth5 -- Parse.position (Parse.$$$ "+") >> (fn (m, (_, pos)) => Combinator (combinator_info [pos], Repeat1, [m])) || - meth4 -- + meth5 -- (Parse.position (Parse.$$$ "[") -- Scan.optional Parse.nat 1 -- Parse.position (Parse.$$$ "]")) >> (fn (m, (((_, pos1), n), (_, pos2))) => Combinator (combinator_info [pos1, pos2], Select_Goals n, [m])) || + meth5) x +and meth3 x = + (Parse.position Parse.xname -- Parse.args1 is_symid_meth >> (Source o uncurry Token.src) || meth4) x and meth2 x = - (Parse.position Parse.xname -- Parse.args1 is_symid_meth >> (Source o uncurry Token.src) || - meth3) x + (Parse.enum1_positions "," meth3 + >> (fn ([m], _) => m | (ms, ps) => Combinator (combinator_info ps, Then, ms))) x and meth1 x = - (Parse.enum1_positions "," meth2 - >> (fn ([m], _) => m | (ms, ps) => Combinator (combinator_info ps, Then, ms))) x + (Parse.enum1_positions ";" meth2 + >> (fn ([m], _) => m | (ms, ps) => Combinator (combinator_info ps, Then_All_New, ms))) x and meth0 x = (Parse.enum1_positions "|" meth1 >> (fn ([m], _) => m | (ms, ps) => Combinator (combinator_info ps, Orelse, ms))) x; in -val parse = - Scan.trace meth3 >> (fn (m, toks) => (m, Token.range_of toks)); +val parse0 = Scan.trace meth0 >> (fn (m, toks) => (m, Token.range_of toks)); +val parse = Scan.trace meth4 >> (fn (m, toks) => (m, Token.range_of toks)); end; diff -r 2441a80fb6c1 -r 49e498cedd02 src/Pure/Isar/rule_cases.ML --- a/src/Pure/Isar/rule_cases.ML Mon Mar 09 11:32:32 2015 +0100 +++ b/src/Pure/Isar/rule_cases.ML Mon Mar 09 20:33:33 2015 +0100 @@ -9,7 +9,8 @@ signature BASIC_RULE_CASES = sig type cases - type cases_tactic + type cases_state = cases * thm + type cases_tactic = thm -> cases_state Seq.seq val CASES: cases -> tactic -> cases_tactic val NO_CASES: tactic -> cases_tactic val SUBGOAL_CASES: ((term * int * thm) -> cases_tactic) -> int -> cases_tactic @@ -183,7 +184,8 @@ (** tactics with cases **) -type cases_tactic = thm -> (cases * thm) Seq.seq; +type cases_state = cases * thm; +type cases_tactic = thm -> cases_state Seq.seq; fun CASES cases tac st = Seq.map (pair cases) (tac st); fun NO_CASES tac = CASES [] tac; diff -r 2441a80fb6c1 -r 49e498cedd02 src/Pure/tactical.ML --- a/src/Pure/tactical.ML Mon Mar 09 11:32:32 2015 +0100 +++ b/src/Pure/tactical.ML Mon Mar 09 20:33:33 2015 +0100 @@ -351,7 +351,8 @@ (*Apply second tactic to all subgoals emerging from the first -- following usual convention for subgoal-based tactics.*) fun (tac1 THEN_ALL_NEW tac2) i st = - st |> (tac1 i THEN (fn st' => Seq.INTERVAL tac2 i (i + Thm.nprems_of st' - Thm.nprems_of st) st')); + st |> (tac1 i THEN (fn st' => + Seq.INTERVAL tac2 i (i + Thm.nprems_of st' - Thm.nprems_of st) st')); (*Repeatedly dig into any emerging subgoals.*) fun REPEAT_ALL_NEW tac =