# HG changeset patch
# User wenzelm
# Date 1287168874 -3600
# Node ID 7219a771ab63a3338d639f3715de4751f2fe07a8
# Parent  f4c614ece7eda648b53d13e8163459b1e4c87d7a
more examples;
tuned;

diff -r f4c614ece7ed -r 7219a771ab63 doc-src/IsarImplementation/Thy/Isar.thy
--- 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
diff -r f4c614ece7ed -r 7219a771ab63 doc-src/IsarImplementation/Thy/ML.thy
--- 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
diff -r f4c614ece7ed -r 7219a771ab63 doc-src/IsarImplementation/Thy/Proof.thy
--- 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