--- a/doc-src/IsarImplementation/Thy/Isar.thy Fri Oct 15 19:19:41 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/Isar.thy Fri Oct 15 19:54:34 2010 +0100
@@ -351,7 +351,10 @@
\end{description}
*}
-text %mlex {* The following toy examples illustrate how the goal facts
+text %mlex {* See also @{command method_setup} in
+ \cite{isabelle-isar-ref} which includes some abstract examples.
+
+ \medskip The following toy examples illustrate how the goal facts
and 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
@@ -406,9 +409,28 @@
example_proof
fix a b c
- assume a: "a \<equiv> b"
- assume b: "b \<equiv> c"
- have "a \<equiv> c" by (my_simp a b)
+ assume a: "a = b"
+ assume b: "b = c"
+ have "a = c" by (my_simp a b)
+qed
+
+text {* Here is a similar method that operates on all subgoals,
+ instead of just the first one. *}
+
+method_setup my_simp_all = {*
+ Attrib.thms >> (fn thms => fn ctxt =>
+ SIMPLE_METHOD
+ (CHANGED
+ (ALLGOALS (asm_full_simp_tac
+ (HOL_basic_ss addsimps thms)))))
+*} "rewrite all subgoals by given rules"
+
+example_proof
+ fix a b c
+ assume a: "a = b"
+ assume b: "b = c"
+ have "a = c" and "c = b" by (my_simp_all a b)
+
qed
text {* \medskip Apart from explicit arguments, common proof methods
@@ -450,11 +472,12 @@
have "a \<equiv> c" by my_simp'
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 @{ML SIMPLE_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.
+text {* \medskip The @{method my_simp} variants defined above are
+ ``simple'' methods, i.e.\ the goal facts are merely inserted as goal
+ premises by the @{ML SIMPLE_METHOD'} or @{ML SIMPLE_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 arguments obtained via concrete syntax or the context does
--- a/doc-src/IsarImplementation/Thy/ML.thy Fri Oct 15 19:19:41 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/ML.thy Fri Oct 15 19:54:34 2010 +0100
@@ -100,11 +100,11 @@
*}
example_proof
- ML_prf {* val a = 1 *}
+ ML_prf %"ML" {* val a = 1 *}
{ -- {* Isar block structure ignored by ML environment *}
- ML_prf {* val b = a + 1 *}
+ ML_prf %"ML" {* val b = a + 1 *}
} -- {* Isar block structure ignored by ML environment *}
- ML_prf {* val c = b + 1 *}
+ ML_prf %"ML" {* val c = b + 1 *}
qed
text {* \noindent By side-stepping the normal scoping rules for Isar
--- a/doc-src/IsarImplementation/Thy/Proof.thy Fri Oct 15 19:19:41 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/Proof.thy Fri Oct 15 19:54:34 2010 +0100
@@ -382,11 +382,10 @@
conclusion: the proof demonstrates that the context may be augmented
by parameters and assumptions, without affecting any conclusions
that do not mention these parameters. See also
- \cite{isabelle-isar-ref} for the user-level @{text "\<OBTAIN>"} and
- @{text "\<GUESS>"} elements. Final results, which may not refer to
+ \cite{isabelle-isar-ref} for the user-level @{command obtain} and
+ @{command guess} elements. Final results, which may not refer to
the parameters in the conclusion, need to exported explicitly into
- the original context.
-*}
+ the original context. *}
text %mlref {*
\begin{mldecls}
@@ -444,4 +443,25 @@
\end{description}
*}
+text %mlex {* The following example demonstrates forward-elimination
+ in a local context, using @{ML Obtain.result}.
+*}
+
+example_proof
+ assume ex: "\<exists>x. B x"
+
+ ML_prf %"ML" {*
+ val ctxt0 = @{context};
+ val (([(_, x)], [B]), ctxt1) = ctxt0
+ |> Obtain.result (fn _ => etac @{thm exE} 1) [@{thm ex}];
+ *}
+ ML_prf %"ML" {*
+ singleton (ProofContext.export ctxt1 ctxt0) @{thm refl};
+ *}
+ ML_prf %"ML" {*
+ ProofContext.export ctxt1 ctxt0 [Thm.reflexive x]
+ handle ERROR msg => (warning msg; []);
+ *}
+qed
+
end