# HG changeset patch # User wenzelm # Date 1287003441 -3600 # Node ID da8c3fc5e314563cd5003886dca1ae3ff0cba398 # Parent cb6634eb89263f123691d4b4c15b5b9fb409e1a2 more on "Proof methods"; more examples; tuned; diff -r cb6634eb8926 -r da8c3fc5e314 doc-src/IsarImplementation/Thy/Isar.thy --- a/doc-src/IsarImplementation/Thy/Isar.thy Wed Oct 13 13:05:23 2010 +0100 +++ b/doc-src/IsarImplementation/Thy/Isar.thy Wed Oct 13 21:57:21 2010 +0100 @@ -171,16 +171,47 @@ section {* Proof methods *} -text {* Proof methods are syntactically embedded into the Isar proof - language as arguments to certain commands, e.g.\ @{command "by"} or - @{command apply}. User-space additions are reasonably easy by - plugging suitable method-valued parser functions into the framework. - - Operationally, a proof method is like a structurally enhanced - tactic: it operates on the full Isar goal configuration with - context, goal facts, and tactical goal state. Like a tactic, it +text {* A @{text "method"} is a function @{text "context \ thm\<^sup>* \ goal + \ (cases \ goal)\<^sup>*\<^sup>*"} that operates on the full Isar goal + configuration with context, goal facts, and tactical goal state and enumerates possible follow-up goal states, with the potential addition of named extensions of the proof context (\emph{cases}). + The latter feature is rarely used. + + This means a proof method is like a structurally enhanced tactic + (cf.\ \secref{sec:tactics}). The well-formedness conditions for + tactics need to hold for methods accordingly, with the following + additions. + + \begin{itemize} + + \item Goal addressing is further limited either to operate either + uniformly on \emph{all} subgoals, or specifically on the + \emph{first} subgoal. + + Exception: old-style tactic emulations that are embedded into the + method space, e.g.\ @{method rule_tac}. + + \item A non-trivial method always needs to make progress: an + identical follow-up goal state has to be avoided.\footnote{This + enables the user to write method expressions like @{text "meth\<^sup>+"} + without looping, while the trivial do-nothing case can be recovered + via @{text "meth\<^sup>?"}.} + + Exception: trivial stuttering steps, such as ``@{method -}'' or + @{method succeed}. + + \item Goal facts passed to the method must not be ignored. If there + is no sensible use of facts outside the goal state, facts should be + inserted into the subgoals that are addressed by the method. + + \end{itemize} + + \medskip Syntactically, the language of proof methods is embedded + into Isar as arguments to certain commands, e.g.\ @{command "by"} or + @{command apply}. User-space additions are reasonably easy by + plugging suitable method-valued parser functions into the framework, + using the @{command method_setup} command, for example. To get a better idea about the range of possibilities, consider the following Isar proof schemes. First some general form of structured @@ -216,40 +247,222 @@ \medskip \noindent The @{text "method\<^sub>1"} operates on the original claim - together while using @{text "facts\<^bsub>1\<^esub>"}. Since the @{command apply} + together while using @{text "facts\<^sub>1"}. Since the @{command apply} command structurally resets the facts, the @{text "method\<^sub>2"} will operate on the remaining goal state without facts. The @{text "method\<^sub>3"} will see again a collection of @{text "facts\<^sub>3"} that has been inserted into the script explicitly. - \medskip Empirically, Isar proof methods can be categorized as follows: + \medskip Empirically, Isar proof methods can be categorized as + follows. \begin{enumerate} - \item structured method with cases, e.g.\ @{method "induct"} - - \item regular method: strong emphasis on facts, e.g.\ @{method "rule"} + \item \emph{Special method with cases} with named context additions + associated with the follow-up goal state. - \item simple method: weak emphasis on facts, merely inserted into - subgoals, e.g.\ @{method "simp"} + Example: @{method "induct"}, which is also a ``raw'' method since it + operates on the internal representation of simultaneous claims as + Pure conjunction, instead of separate subgoals. - \item old-style tactic emulation, e.g. @{method "rule_tac"} + \item \emph{Structured method} with strong emphasis on facts outside + the goal state. + + Example: @{method "rule"}, which captures the key ideas behind + structured reasoning in Isar in purest form. - \begin{itemize} + \item \emph{Simple method} with weaker emphasis on facts, which are + inserted into subgoals to emulate old-style tactical as + ``premises''. - \item naming convention @{text "foo_tac"} + Examples: @{method "simp"}, @{method "blast"}, @{method "auto"}. - \item numeric goal addressing + \item \emph{Old-style tactic emulation} with detailed numeric goal + addressing and explicit references to entities of the internal goal + state (which are otherwise invisible from proper Isar proof text). + To make the special non-standard status clear, the naming convention + @{text "foo_tac"} needs to be observed. - \item explicit references to internal goal state (invisible from text!) - - \end{itemize} + Example: @{method "rule_tac"}. \end{enumerate} - FIXME + When implementing proof methods, it is advisable to study existing + implementations carefully and imitate the typical ``boiler plate'' + for context-sensitive parsing and further combinators to wrap-up + tactic expressions as methods.\footnote{Home-grown aliases or + abbreviations of the standard method combinators should be avoided. + Old user code often retains similar remains of complicated two-phase + method setup of Isabelle99 that was discontinued in Isabelle2009.} +*} + + +text %mlref {* + \begin{mldecls} + @{index_ML_type Proof.method} \\ + @{index_ML METHOD_CASES: "(thm list -> cases_tactic) -> Proof.method"} \\ + @{index_ML METHOD: "(thm list -> tactic) -> Proof.method"} \\ + @{index_ML SIMPLE_METHOD: "tactic -> Proof.method"} \\ + @{index_ML SIMPLE_METHOD': "(int -> tactic) -> Proof.method"} \\ + @{index_ML HEADGOAL: "(int -> tactic) -> tactic"} \\ + @{index_ML Method.insert_tac: "thm list -> int -> tactic"} \\ + @{index_ML Method.setup: "binding -> (Proof.context -> Proof.method) context_parser -> + string -> theory -> theory"} \\ + \end{mldecls} + + \begin{description} + + \item @{ML_type Proof.method} represents proof methods as abstract type. + + \item @{ML METHOD_CASES}~@{text "(fn facts => cases_tactic)"} wraps + @{text cases_tactic} depending on goal facts as proof method with + cases; the goal context is passed via method syntax. + + \item @{ML METHOD}~@{text "(fn facts => tactic)"} wraps @{text + tactic} depending on goal facts as regular proof method; the goal + context is passed via method syntax. + + \item @{ML SIMPLE_METHOD}~@{text "tactic"} wraps a tactic that + addresses all subgoals uniformly as simple proof method. Goal facts + are already inserted into all subgoals before @{text "tactic"} is + applied. + + \item @{ML SIMPLE_METHOD'}~@{text "tactic"} wraps a tactic that + addresses a specific subgoal as simple proof method. Goal facts are + already inserted into the first subgoal before @{text "tactic"} is + applied to the same. + + \item @{ML HEADGOAL}~@{text "tactic"} applies @{text "tactic"} to + the first subgoal. This is convenient to reproduce part the @{ML + SIMPLE_METHOD'} wrapping within regular @{ML METHOD}, for example. + + \item @{ML Method.insert_tac}~@{text "facts i"} inserts @{text + "facts"} into subgoal @{text "i"}. This is convenient to reproduce + part of the @{ML SIMPLE_METHOD} or @{ML SIMPLE_METHOD'} wrapping + within regular @{ML METHOD}, for example. + + \item @{ML Method.setup}~@{text "name parser description"} provides + the functionality of the Isar command @{command method_setup}~@{text + "name text description"} as ML function. + + \end{description} +*} + +text %mlex {* The following toy examples illustrate how goal facts and + goal state are passed to proof methods. The pre-defined proof + method called ``@{method tactic}'' wraps ML source of type @{ML_type + tactic} (abstracted over @{verbatim facts}). This allows immediate + experimentation without concrete syntax parsing. *} +example_proof + assume a: A and b: B + + have "A \ B" + apply (tactic {* rtac @{thm conjI} 1 *}) + using a apply (tactic {* resolve_tac facts 1 *}) + using b apply (tactic {* resolve_tac facts 1 *}) + done + + have "A \ B" + using a and b + ML_val "@{Isar.goal}" + apply (tactic {* Method.insert_tac facts 1 *}) + apply (tactic {* (rtac @{thm conjI} THEN_ALL_NEW atac) 1 *}) + done +qed + +text {* \medskip The subsequent example implements a method @{text + "my_simp"} that rewrites the first subgoal by rules declared in the + context. As a shortcut to rule management we use a cheap solution + via functor @{ML_functor Named_Thms} (see also @{"file" + "~~/src/Pure/Tools/named_thms.ML"}). +*} + +ML {* + structure My_Simps = + Named_Thms + (val name = "my_simp" val description = "my_simp rule") +*} +setup My_Simps.setup + +text {* \medskip\noindent This provides ML access to a list of + theorems in canonical declaration order via @{ML My_Simps.get}. The + user can add or delete rules via the attribute @{attribute my_simp}. + The actual proof method is now defined as follows: +*} + +method_setup my_simp = {* + Scan.succeed (fn ctxt => + SIMPLE_METHOD' (fn i => + CHANGED (asm_full_simp_tac + (HOL_basic_ss addsimps (My_Simps.get ctxt)) i))) +*} "rewrite subgoal by my_rewrite rules" + +text {* \medskip\noindent Now method @{method my_simp} can be used in + Isar proofs like this: *} + +example_proof + fix a b c + assume [my_simp]: "a \ b" + assume [my_simp]: "b \ c" + have "a \ c" by my_simp +qed + +text {* \medskip\noindent Note how the @{ML CHANGED} tactical is used + to ensure progress of simplification: identical goal states need to + be filtered out explicitly, because the internal Simplifier tactics + never fail. + + \medskip Further refinement of method syntax is illustrated below: + rules presented as explicit method arguments are included in the + collection of rewrite rules. +*} + +method_setup my_simp' = {* + Attrib.thms >> (fn my_simps => fn ctxt => + SIMPLE_METHOD' (fn i => + CHANGED (asm_full_simp_tac + (HOL_basic_ss addsimps (my_simps @ My_Simps.get ctxt)) i))) +*} "rewrite subgoal by my_rewrite rules" + +example_proof + fix a b c + assume a: "a \ b" + assume b: "b \ c" + have "a \ c" by (my_simp' a b) +qed + +text {* \medskip Both @{method my_simp} and @{method my_simp'} are + simple methods, i.e.\ the goal facts are merely inserted as goal + premises by the method wrapper. For proof methods that are similar + to the standard collection of @{method simp}, @{method blast}, + @{method auto} little more can be done here. + + Note that using the primary goal facts in the same manner as the + method parameters obtained by the context or concrete syntax does + not quite meet the requirement of ``strong emphasis on facts'' of + regular proof methods, because rewrite rules as used above can be + easily ignored. A proof text ``@{command using}~@{text + "foo"}~@{command "by"}~@{text "my_simp"}'' where @{text "foo"} is + not used would deceive the reader. + + \medskip The technical treatment of rules from the context requires + further attention. Above we rebuild a fresh @{ML_type simpset} from + the list of rules retrieved from the context on every invocation of + the method. This does not scale to really large collections of + rules. + + This is an inherent limitation of the above rule management via + functor @{ML_functor Named_Thms}, because that lacks tool-specific + storage and retrieval. More realistic applications require + efficient index-structures that organize theorems in a customized + manner, such as a discrimination net that is indexed by the + left-hand sides of rewrite rules. For variations on the Simplifier + it is possible to re-use the existing type @{ML_type simpset}, but + scalability requires it be maintained statically within the context + data, not dynamically on each tool invocation. *} + section {* Attributes *} diff -r cb6634eb8926 -r da8c3fc5e314 doc-src/IsarImplementation/Thy/Tactic.thy --- a/doc-src/IsarImplementation/Thy/Tactic.thy Wed Oct 13 13:05:23 2010 +0100 +++ b/doc-src/IsarImplementation/Thy/Tactic.thy Wed Oct 13 21:57:21 2010 +0100 @@ -86,7 +86,7 @@ *} -section {* Tactics *} +section {* Tactics\label{sec:tactics} *} text {* A @{text "tactic"} is a function @{text "goal \ goal\<^sup>*\<^sup>*"} that maps a given goal state (represented as a theorem, cf.\