# 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 \ b" - assume b: "b \ c" - have "a \ 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 \ 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 "\"} and - @{text "\"} 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: "\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