1.1 --- a/doc-src/IsarImplementation/Thy/Isar.thy Wed Oct 13 13:05:23 2010 +0100
1.2 +++ b/doc-src/IsarImplementation/Thy/Isar.thy Wed Oct 13 21:57:21 2010 +0100
1.3 @@ -171,16 +171,47 @@
1.4
1.5 section {* Proof methods *}
1.6
1.7 -text {* Proof methods are syntactically embedded into the Isar proof
1.8 - language as arguments to certain commands, e.g.\ @{command "by"} or
1.9 - @{command apply}. User-space additions are reasonably easy by
1.10 - plugging suitable method-valued parser functions into the framework.
1.11 -
1.12 - Operationally, a proof method is like a structurally enhanced
1.13 - tactic: it operates on the full Isar goal configuration with
1.14 - context, goal facts, and tactical goal state. Like a tactic, it
1.15 +text {* A @{text "method"} is a function @{text "context \<rightarrow> thm\<^sup>* \<rightarrow> goal
1.16 + \<rightarrow> (cases \<times> goal)\<^sup>*\<^sup>*"} that operates on the full Isar goal
1.17 + configuration with context, goal facts, and tactical goal state and
1.18 enumerates possible follow-up goal states, with the potential
1.19 addition of named extensions of the proof context (\emph{cases}).
1.20 + The latter feature is rarely used.
1.21 +
1.22 + This means a proof method is like a structurally enhanced tactic
1.23 + (cf.\ \secref{sec:tactics}). The well-formedness conditions for
1.24 + tactics need to hold for methods accordingly, with the following
1.25 + additions.
1.26 +
1.27 + \begin{itemize}
1.28 +
1.29 + \item Goal addressing is further limited either to operate either
1.30 + uniformly on \emph{all} subgoals, or specifically on the
1.31 + \emph{first} subgoal.
1.32 +
1.33 + Exception: old-style tactic emulations that are embedded into the
1.34 + method space, e.g.\ @{method rule_tac}.
1.35 +
1.36 + \item A non-trivial method always needs to make progress: an
1.37 + identical follow-up goal state has to be avoided.\footnote{This
1.38 + enables the user to write method expressions like @{text "meth\<^sup>+"}
1.39 + without looping, while the trivial do-nothing case can be recovered
1.40 + via @{text "meth\<^sup>?"}.}
1.41 +
1.42 + Exception: trivial stuttering steps, such as ``@{method -}'' or
1.43 + @{method succeed}.
1.44 +
1.45 + \item Goal facts passed to the method must not be ignored. If there
1.46 + is no sensible use of facts outside the goal state, facts should be
1.47 + inserted into the subgoals that are addressed by the method.
1.48 +
1.49 + \end{itemize}
1.50 +
1.51 + \medskip Syntactically, the language of proof methods is embedded
1.52 + into Isar as arguments to certain commands, e.g.\ @{command "by"} or
1.53 + @{command apply}. User-space additions are reasonably easy by
1.54 + plugging suitable method-valued parser functions into the framework,
1.55 + using the @{command method_setup} command, for example.
1.56
1.57 To get a better idea about the range of possibilities, consider the
1.58 following Isar proof schemes. First some general form of structured
1.59 @@ -216,41 +247,223 @@
1.60 \medskip
1.61
1.62 \noindent The @{text "method\<^sub>1"} operates on the original claim
1.63 - together while using @{text "facts\<^bsub>1\<^esub>"}. Since the @{command apply}
1.64 + together while using @{text "facts\<^sub>1"}. Since the @{command apply}
1.65 command structurally resets the facts, the @{text "method\<^sub>2"} will
1.66 operate on the remaining goal state without facts. The @{text
1.67 "method\<^sub>3"} will see again a collection of @{text "facts\<^sub>3"} that has
1.68 been inserted into the script explicitly.
1.69
1.70 - \medskip Empirically, Isar proof methods can be categorized as follows:
1.71 + \medskip Empirically, Isar proof methods can be categorized as
1.72 + follows.
1.73
1.74 \begin{enumerate}
1.75
1.76 - \item structured method with cases, e.g.\ @{method "induct"}
1.77 + \item \emph{Special method with cases} with named context additions
1.78 + associated with the follow-up goal state.
1.79
1.80 - \item regular method: strong emphasis on facts, e.g.\ @{method "rule"}
1.81 + Example: @{method "induct"}, which is also a ``raw'' method since it
1.82 + operates on the internal representation of simultaneous claims as
1.83 + Pure conjunction, instead of separate subgoals.
1.84
1.85 - \item simple method: weak emphasis on facts, merely inserted into
1.86 - subgoals, e.g.\ @{method "simp"}
1.87 + \item \emph{Structured method} with strong emphasis on facts outside
1.88 + the goal state.
1.89
1.90 - \item old-style tactic emulation, e.g. @{method "rule_tac"}
1.91 + Example: @{method "rule"}, which captures the key ideas behind
1.92 + structured reasoning in Isar in purest form.
1.93
1.94 - \begin{itemize}
1.95 + \item \emph{Simple method} with weaker emphasis on facts, which are
1.96 + inserted into subgoals to emulate old-style tactical as
1.97 + ``premises''.
1.98
1.99 - \item naming convention @{text "foo_tac"}
1.100 + Examples: @{method "simp"}, @{method "blast"}, @{method "auto"}.
1.101
1.102 - \item numeric goal addressing
1.103 + \item \emph{Old-style tactic emulation} with detailed numeric goal
1.104 + addressing and explicit references to entities of the internal goal
1.105 + state (which are otherwise invisible from proper Isar proof text).
1.106 + To make the special non-standard status clear, the naming convention
1.107 + @{text "foo_tac"} needs to be observed.
1.108
1.109 - \item explicit references to internal goal state (invisible from text!)
1.110 -
1.111 - \end{itemize}
1.112 + Example: @{method "rule_tac"}.
1.113
1.114 \end{enumerate}
1.115
1.116 - FIXME
1.117 + When implementing proof methods, it is advisable to study existing
1.118 + implementations carefully and imitate the typical ``boiler plate''
1.119 + for context-sensitive parsing and further combinators to wrap-up
1.120 + tactic expressions as methods.\footnote{Home-grown aliases or
1.121 + abbreviations of the standard method combinators should be avoided.
1.122 + Old user code often retains similar remains of complicated two-phase
1.123 + method setup of Isabelle99 that was discontinued in Isabelle2009.}
1.124 *}
1.125
1.126
1.127 +text %mlref {*
1.128 + \begin{mldecls}
1.129 + @{index_ML_type Proof.method} \\
1.130 + @{index_ML METHOD_CASES: "(thm list -> cases_tactic) -> Proof.method"} \\
1.131 + @{index_ML METHOD: "(thm list -> tactic) -> Proof.method"} \\
1.132 + @{index_ML SIMPLE_METHOD: "tactic -> Proof.method"} \\
1.133 + @{index_ML SIMPLE_METHOD': "(int -> tactic) -> Proof.method"} \\
1.134 + @{index_ML HEADGOAL: "(int -> tactic) -> tactic"} \\
1.135 + @{index_ML Method.insert_tac: "thm list -> int -> tactic"} \\
1.136 + @{index_ML Method.setup: "binding -> (Proof.context -> Proof.method) context_parser ->
1.137 + string -> theory -> theory"} \\
1.138 + \end{mldecls}
1.139 +
1.140 + \begin{description}
1.141 +
1.142 + \item @{ML_type Proof.method} represents proof methods as abstract type.
1.143 +
1.144 + \item @{ML METHOD_CASES}~@{text "(fn facts => cases_tactic)"} wraps
1.145 + @{text cases_tactic} depending on goal facts as proof method with
1.146 + cases; the goal context is passed via method syntax.
1.147 +
1.148 + \item @{ML METHOD}~@{text "(fn facts => tactic)"} wraps @{text
1.149 + tactic} depending on goal facts as regular proof method; the goal
1.150 + context is passed via method syntax.
1.151 +
1.152 + \item @{ML SIMPLE_METHOD}~@{text "tactic"} wraps a tactic that
1.153 + addresses all subgoals uniformly as simple proof method. Goal facts
1.154 + are already inserted into all subgoals before @{text "tactic"} is
1.155 + applied.
1.156 +
1.157 + \item @{ML SIMPLE_METHOD'}~@{text "tactic"} wraps a tactic that
1.158 + addresses a specific subgoal as simple proof method. Goal facts are
1.159 + already inserted into the first subgoal before @{text "tactic"} is
1.160 + applied to the same.
1.161 +
1.162 + \item @{ML HEADGOAL}~@{text "tactic"} applies @{text "tactic"} to
1.163 + the first subgoal. This is convenient to reproduce part the @{ML
1.164 + SIMPLE_METHOD'} wrapping within regular @{ML METHOD}, for example.
1.165 +
1.166 + \item @{ML Method.insert_tac}~@{text "facts i"} inserts @{text
1.167 + "facts"} into subgoal @{text "i"}. This is convenient to reproduce
1.168 + part of the @{ML SIMPLE_METHOD} or @{ML SIMPLE_METHOD'} wrapping
1.169 + within regular @{ML METHOD}, for example.
1.170 +
1.171 + \item @{ML Method.setup}~@{text "name parser description"} provides
1.172 + the functionality of the Isar command @{command method_setup}~@{text
1.173 + "name text description"} as ML function.
1.174 +
1.175 + \end{description}
1.176 +*}
1.177 +
1.178 +text %mlex {* The following toy examples illustrate how goal facts and
1.179 + goal state are passed to proof methods. The pre-defined proof
1.180 + method called ``@{method tactic}'' wraps ML source of type @{ML_type
1.181 + tactic} (abstracted over @{verbatim facts}). This allows immediate
1.182 + experimentation without concrete syntax parsing.
1.183 +*}
1.184 +
1.185 +example_proof
1.186 + assume a: A and b: B
1.187 +
1.188 + have "A \<and> B"
1.189 + apply (tactic {* rtac @{thm conjI} 1 *})
1.190 + using a apply (tactic {* resolve_tac facts 1 *})
1.191 + using b apply (tactic {* resolve_tac facts 1 *})
1.192 + done
1.193 +
1.194 + have "A \<and> B"
1.195 + using a and b
1.196 + ML_val "@{Isar.goal}"
1.197 + apply (tactic {* Method.insert_tac facts 1 *})
1.198 + apply (tactic {* (rtac @{thm conjI} THEN_ALL_NEW atac) 1 *})
1.199 + done
1.200 +qed
1.201 +
1.202 +text {* \medskip The subsequent example implements a method @{text
1.203 + "my_simp"} that rewrites the first subgoal by rules declared in the
1.204 + context. As a shortcut to rule management we use a cheap solution
1.205 + via functor @{ML_functor Named_Thms} (see also @{"file"
1.206 + "~~/src/Pure/Tools/named_thms.ML"}).
1.207 +*}
1.208 +
1.209 +ML {*
1.210 + structure My_Simps =
1.211 + Named_Thms
1.212 + (val name = "my_simp" val description = "my_simp rule")
1.213 +*}
1.214 +setup My_Simps.setup
1.215 +
1.216 +text {* \medskip\noindent This provides ML access to a list of
1.217 + theorems in canonical declaration order via @{ML My_Simps.get}. The
1.218 + user can add or delete rules via the attribute @{attribute my_simp}.
1.219 + The actual proof method is now defined as follows:
1.220 +*}
1.221 +
1.222 +method_setup my_simp = {*
1.223 + Scan.succeed (fn ctxt =>
1.224 + SIMPLE_METHOD' (fn i =>
1.225 + CHANGED (asm_full_simp_tac
1.226 + (HOL_basic_ss addsimps (My_Simps.get ctxt)) i)))
1.227 +*} "rewrite subgoal by my_rewrite rules"
1.228 +
1.229 +text {* \medskip\noindent Now method @{method my_simp} can be used in
1.230 + Isar proofs like this: *}
1.231 +
1.232 +example_proof
1.233 + fix a b c
1.234 + assume [my_simp]: "a \<equiv> b"
1.235 + assume [my_simp]: "b \<equiv> c"
1.236 + have "a \<equiv> c" by my_simp
1.237 +qed
1.238 +
1.239 +text {* \medskip\noindent Note how the @{ML CHANGED} tactical is used
1.240 + to ensure progress of simplification: identical goal states need to
1.241 + be filtered out explicitly, because the internal Simplifier tactics
1.242 + never fail.
1.243 +
1.244 + \medskip Further refinement of method syntax is illustrated below:
1.245 + rules presented as explicit method arguments are included in the
1.246 + collection of rewrite rules.
1.247 +*}
1.248 +
1.249 +method_setup my_simp' = {*
1.250 + Attrib.thms >> (fn my_simps => fn ctxt =>
1.251 + SIMPLE_METHOD' (fn i =>
1.252 + CHANGED (asm_full_simp_tac
1.253 + (HOL_basic_ss addsimps (my_simps @ My_Simps.get ctxt)) i)))
1.254 +*} "rewrite subgoal by my_rewrite rules"
1.255 +
1.256 +example_proof
1.257 + fix a b c
1.258 + assume a: "a \<equiv> b"
1.259 + assume b: "b \<equiv> c"
1.260 + have "a \<equiv> c" by (my_simp' a b)
1.261 +qed
1.262 +
1.263 +text {* \medskip Both @{method my_simp} and @{method my_simp'} are
1.264 + simple methods, i.e.\ the goal facts are merely inserted as goal
1.265 + premises by the method wrapper. For proof methods that are similar
1.266 + to the standard collection of @{method simp}, @{method blast},
1.267 + @{method auto} little more can be done here.
1.268 +
1.269 + Note that using the primary goal facts in the same manner as the
1.270 + method parameters obtained by the context or concrete syntax does
1.271 + not quite meet the requirement of ``strong emphasis on facts'' of
1.272 + regular proof methods, because rewrite rules as used above can be
1.273 + easily ignored. A proof text ``@{command using}~@{text
1.274 + "foo"}~@{command "by"}~@{text "my_simp"}'' where @{text "foo"} is
1.275 + not used would deceive the reader.
1.276 +
1.277 + \medskip The technical treatment of rules from the context requires
1.278 + further attention. Above we rebuild a fresh @{ML_type simpset} from
1.279 + the list of rules retrieved from the context on every invocation of
1.280 + the method. This does not scale to really large collections of
1.281 + rules.
1.282 +
1.283 + This is an inherent limitation of the above rule management via
1.284 + functor @{ML_functor Named_Thms}, because that lacks tool-specific
1.285 + storage and retrieval. More realistic applications require
1.286 + efficient index-structures that organize theorems in a customized
1.287 + manner, such as a discrimination net that is indexed by the
1.288 + left-hand sides of rewrite rules. For variations on the Simplifier
1.289 + it is possible to re-use the existing type @{ML_type simpset}, but
1.290 + scalability requires it be maintained statically within the context
1.291 + data, not dynamically on each tool invocation. *}
1.292 +
1.293 +
1.294 section {* Attributes *}
1.295
1.296 text FIXME
2.1 --- a/doc-src/IsarImplementation/Thy/Tactic.thy Wed Oct 13 13:05:23 2010 +0100
2.2 +++ b/doc-src/IsarImplementation/Thy/Tactic.thy Wed Oct 13 21:57:21 2010 +0100
2.3 @@ -86,7 +86,7 @@
2.4 *}
2.5
2.6
2.7 -section {* Tactics *}
2.8 +section {* Tactics\label{sec:tactics} *}
2.9
2.10 text {* A @{text "tactic"} is a function @{text "goal \<rightarrow> goal\<^sup>*\<^sup>*"} that
2.11 maps a given goal state (represented as a theorem, cf.\