1.1 --- a/doc-src/IsarImplementation/Thy/Isar.thy Wed Oct 13 21:57:21 2010 +0100
1.2 +++ b/doc-src/IsarImplementation/Thy/Isar.thy Thu Oct 14 21:05:21 2010 +0100
1.3 @@ -290,13 +290,13 @@
1.4 When implementing proof methods, it is advisable to study existing
1.5 implementations carefully and imitate the typical ``boiler plate''
1.6 for context-sensitive parsing and further combinators to wrap-up
1.7 - tactic expressions as methods.\footnote{Home-grown aliases or
1.8 - abbreviations of the standard method combinators should be avoided.
1.9 - Old user code often retains similar remains of complicated two-phase
1.10 - method setup of Isabelle99 that was discontinued in Isabelle2009.}
1.11 + tactic expressions as methods.\footnote{Aliases or abbreviations of
1.12 + the standard method combinators should be avoided. Note that from
1.13 + Isabelle99 until Isabelle2009 the system did provide various odd
1.14 + combinations of method wrappers that made user applications more
1.15 + complicated than necessary.}
1.16 *}
1.17
1.18 -
1.19 text %mlref {*
1.20 \begin{mldecls}
1.21 @{index_ML_type Proof.method} \\
1.22 @@ -342,18 +342,17 @@
1.23 within regular @{ML METHOD}, for example.
1.24
1.25 \item @{ML Method.setup}~@{text "name parser description"} provides
1.26 - the functionality of the Isar command @{command method_setup}~@{text
1.27 - "name text description"} as ML function.
1.28 + the functionality of the Isar command @{command method_setup} as ML
1.29 + function.
1.30
1.31 \end{description}
1.32 *}
1.33
1.34 -text %mlex {* The following toy examples illustrate how goal facts and
1.35 - goal state are passed to proof methods. The pre-defined proof
1.36 - method called ``@{method tactic}'' wraps ML source of type @{ML_type
1.37 +text %mlex {* The following toy examples illustrate how the goal facts
1.38 + and state are passed to proof methods. The pre-defined proof method
1.39 + called ``@{method tactic}'' wraps ML source of type @{ML_type
1.40 tactic} (abstracted over @{verbatim facts}). This allows immediate
1.41 - experimentation without concrete syntax parsing.
1.42 -*}
1.43 + experimentation without parsing of concrete syntax. *}
1.44
1.45 example_proof
1.46 assume a: A and b: B
1.47 @@ -372,13 +371,49 @@
1.48 done
1.49 qed
1.50
1.51 -text {* \medskip The subsequent example implements a method @{text
1.52 - "my_simp"} that rewrites the first subgoal by rules declared in the
1.53 - context. As a shortcut to rule management we use a cheap solution
1.54 - via functor @{ML_functor Named_Thms} (see also @{"file"
1.55 - "~~/src/Pure/Tools/named_thms.ML"}).
1.56 +text {* \medskip The next example implements a method that simplifies
1.57 + the first subgoal by rewrite rules given as arguments. *}
1.58 +
1.59 +method_setup my_simp = {*
1.60 + Attrib.thms >> (fn thms => fn ctxt =>
1.61 + SIMPLE_METHOD' (fn i =>
1.62 + CHANGED (asm_full_simp_tac
1.63 + (HOL_basic_ss addsimps thms) i)))
1.64 +*} "rewrite subgoal by given rules"
1.65 +
1.66 +text {* The concrete syntax wrapping of @{command method_setup} always
1.67 + passes-through the proof context at the end of parsing, but it is
1.68 + not used in this example.
1.69 +
1.70 + The @{ML Attrib.thms} parser produces a list of theorems from the
1.71 + usual Isar syntax involving attribute expressions etc.\ (syntax
1.72 + category @{syntax thmrefs}). The resulting @{verbatim thms} are
1.73 + added to @{ML HOL_basic_ss} which already contains the basic
1.74 + Simplifier setup for HOL.
1.75 +
1.76 + The tactic @{ML asm_full_simp_tac} is the one that is also used in
1.77 + method @{method simp} by default. The extra wrapping by the @{ML
1.78 + CHANGED} tactical ensures progress of simplification: identical goal
1.79 + states are filtered out explicitly to make the raw tactic conform to
1.80 + standard Isar method behaviour.
1.81 +
1.82 + \medskip Method @{method my_simp} can be used in Isar proofs like
1.83 + this:
1.84 *}
1.85
1.86 +example_proof
1.87 + fix a b c
1.88 + assume a: "a \<equiv> b"
1.89 + assume b: "b \<equiv> c"
1.90 + have "a \<equiv> c" by (my_simp a b)
1.91 +qed
1.92 +
1.93 +text {* \medskip Apart from explicit arguments, common proof methods
1.94 + typically work with a default configuration provided by the context.
1.95 + As a shortcut to rule management we use a cheap solution via functor
1.96 + @{ML_functor Named_Thms} (see also @{"file"
1.97 + "~~/src/Pure/Tools/named_thms.ML"}). *}
1.98 +
1.99 ML {*
1.100 structure My_Simps =
1.101 Named_Thms
1.102 @@ -389,77 +424,57 @@
1.103 text {* \medskip\noindent This provides ML access to a list of
1.104 theorems in canonical declaration order via @{ML My_Simps.get}. The
1.105 user can add or delete rules via the attribute @{attribute my_simp}.
1.106 - The actual proof method is now defined as follows:
1.107 + The actual proof method is now defined as before, but we append the
1.108 + explicit arguments and the rules from the context.
1.109 *}
1.110
1.111 -method_setup my_simp = {*
1.112 - Scan.succeed (fn ctxt =>
1.113 +method_setup my_simp' = {*
1.114 + Attrib.thms >> (fn thms => fn ctxt =>
1.115 SIMPLE_METHOD' (fn i =>
1.116 CHANGED (asm_full_simp_tac
1.117 - (HOL_basic_ss addsimps (My_Simps.get ctxt)) i)))
1.118 -*} "rewrite subgoal by my_rewrite rules"
1.119 + (HOL_basic_ss addsimps (thms @ My_Simps.get ctxt)) i)))
1.120 +*} "rewrite subgoal by given rules and my_simp rules from the context"
1.121
1.122 -text {* \medskip\noindent Now method @{method my_simp} can be used in
1.123 - Isar proofs like this: *}
1.124 +text {*
1.125 + \medskip Method @{method my_simp'} can be used in Isar proofs
1.126 + like this:
1.127 +*}
1.128
1.129 example_proof
1.130 fix a b c
1.131 assume [my_simp]: "a \<equiv> b"
1.132 assume [my_simp]: "b \<equiv> c"
1.133 - have "a \<equiv> c" by my_simp
1.134 -qed
1.135 -
1.136 -text {* \medskip\noindent Note how the @{ML CHANGED} tactical is used
1.137 - to ensure progress of simplification: identical goal states need to
1.138 - be filtered out explicitly, because the internal Simplifier tactics
1.139 - never fail.
1.140 -
1.141 - \medskip Further refinement of method syntax is illustrated below:
1.142 - rules presented as explicit method arguments are included in the
1.143 - collection of rewrite rules.
1.144 -*}
1.145 -
1.146 -method_setup my_simp' = {*
1.147 - Attrib.thms >> (fn my_simps => fn ctxt =>
1.148 - SIMPLE_METHOD' (fn i =>
1.149 - CHANGED (asm_full_simp_tac
1.150 - (HOL_basic_ss addsimps (my_simps @ My_Simps.get ctxt)) i)))
1.151 -*} "rewrite subgoal by my_rewrite rules"
1.152 -
1.153 -example_proof
1.154 - fix a b c
1.155 - assume a: "a \<equiv> b"
1.156 - assume b: "b \<equiv> c"
1.157 - have "a \<equiv> c" by (my_simp' a b)
1.158 + have "a \<equiv> c" by my_simp'
1.159 qed
1.160
1.161 text {* \medskip Both @{method my_simp} and @{method my_simp'} are
1.162 simple methods, i.e.\ the goal facts are merely inserted as goal
1.163 - premises by the method wrapper. For proof methods that are similar
1.164 - to the standard collection of @{method simp}, @{method blast},
1.165 - @{method auto} little more can be done here.
1.166 + premises by the @{ML SIMPLE_METHOD'} wrapper. For proof methods
1.167 + that are similar to the standard collection of @{method simp},
1.168 + @{method blast}, @{method auto} little more can be done here.
1.169
1.170 Note that using the primary goal facts in the same manner as the
1.171 - method parameters obtained by the context or concrete syntax does
1.172 - not quite meet the requirement of ``strong emphasis on facts'' of
1.173 - regular proof methods, because rewrite rules as used above can be
1.174 - easily ignored. A proof text ``@{command using}~@{text
1.175 - "foo"}~@{command "by"}~@{text "my_simp"}'' where @{text "foo"} is
1.176 - not used would deceive the reader.
1.177 + method arguments obtained via concrete syntax or the context does
1.178 + not meet the requirement of ``strong emphasis on facts'' of regular
1.179 + proof methods, because rewrite rules as used above can be easily
1.180 + ignored. A proof text ``@{command using}~@{text "foo"}~@{command
1.181 + "by"}~@{text "my_simp"}'' where @{text "foo"} is not used would
1.182 + deceive the reader.
1.183
1.184 \medskip The technical treatment of rules from the context requires
1.185 further attention. Above we rebuild a fresh @{ML_type simpset} from
1.186 - the list of rules retrieved from the context on every invocation of
1.187 - the method. This does not scale to really large collections of
1.188 - rules.
1.189 + the arguments and \emph{all} rules retrieved from the context on
1.190 + every invocation of the method. This does not scale to really large
1.191 + collections of rules, which easily emerges in the context of a big
1.192 + theory library, for example.
1.193
1.194 - This is an inherent limitation of the above rule management via
1.195 - functor @{ML_functor Named_Thms}, because that lacks tool-specific
1.196 + This is an inherent limitation of the simplistic rule management via
1.197 + functor @{ML_functor Named_Thms}, because it lacks tool-specific
1.198 storage and retrieval. More realistic applications require
1.199 efficient index-structures that organize theorems in a customized
1.200 manner, such as a discrimination net that is indexed by the
1.201 - left-hand sides of rewrite rules. For variations on the Simplifier
1.202 - it is possible to re-use the existing type @{ML_type simpset}, but
1.203 + left-hand sides of rewrite rules. For variations on the Simplifier,
1.204 + re-use of the existing type @{ML_type simpset} is adequate, but
1.205 scalability requires it be maintained statically within the context
1.206 data, not dynamically on each tool invocation. *}
1.207