src/Doc/Eisbach/Manual.thy

 (*:wrap=hard:maxLineLen=78:*)
 
 theory Manual
-imports Base "../Eisbach_Tools"
+imports Base "~~/src/HOL/Eisbach/Eisbach_Tools"
 begin
 
 chapter \<open>The method command\<close>
 
 text \<open>

   methods by combining existing ones with their usual syntax. Specifically it
   allows compound proof methods to be named, and to extend the name space of
   basic methods accordingly. Method definitions may abstract over parameters:
   terms, facts, or other methods.
 
-  \medskip The syntax diagram below refers to some syntactic categories that
+  \<^medskip>
+  The syntax diagram below refers to some syntactic categories that
   are further defined in @{cite "isabelle-isar-ref"}.
 
   @{rail \<open>
     @@{command method} name args @'=' method
     ;

   Eisbach. It is similar to ``@{text "method\<^sub>1, method\<^sub>2"}'', but @{text
   method\<^sub>2} is invoked on on \emph{all} subgoals that have newly emerged from
   @{text method\<^sub>1}. This is useful to handle cases where the number of
   subgoals produced by a method is determined dynamically at run-time.
 \<close>
-text_raw\<open>\vbox{\<close>
+
     method conj_with uses rule =
       (intro conjI ; intro rule)
 
     lemma
       assumes A: "P"
       shows "P \<and> P \<and> P"
       by (conj_with rule: A)
-text_raw\<open>}\<close>
+
 text \<open>
   Method definitions may take other methods as arguments, and thus implement
   method combinators with prefix syntax. For example, to more usefully exploit
   Isabelle's backtracking, the explicit requirement that a method solve all
   produced subgoals is frequently useful. This can easily be written as a

   "intros"}, @{text "elims"}, and @{text "subst"}, are managed by declarations
   in the current proof context. They will therefore be passed to any recursive
   call to @{method prop_solver} and, more generally, any invocation of a
   method which declares these named theorems.
 
-  \medskip After declaring some standard rules to the context, the @{method
+  \<^medskip>
+  After declaring some standard rules to the context, the @{method
   prop_solver} becomes capable of solving non-trivial propositional
   tautologies.\<close>
 
     lemmas [intros] =
       conjI  --  \<open>@{thm conjI}\<close>

   provides more direct access to the higher-order matching facility at the
   core of Isabelle. It is implemented as a separate proof method (in
   Isabelle/ML), and thus can be directly applied to proofs, however it is most
   useful when applied in the context of writing Eisbach method definitions.
 
-  \medskip The syntax diagram below refers to some syntactic categories that
+  \<^medskip>
+  The syntax diagram below refers to some syntactic categories that
   are further defined in @{cite "isabelle-isar-ref"}.
 
   @{rail \<open>
     @@{method match} kind @'in' (pattern '\<Rightarrow>' cartouche + '\<bar>')
     ;

 
   Schematic terms like @{text "?P"} may also be used to specify match
   variables, but the result of the match is not bound, and thus cannot be used
   in the inner method body.
 
-  \medskip In the following example we extract the predicate of an
+  \<^medskip>
+  In the following example we extract the predicate of an
   existentially quantified conclusion in the current subgoal and search the
   current premises for a matching fact. If both matches are successful, we
   then instantiate the existential introduction rule with both the witness and
   predicate, solving with the matched premise.
 \<close>

   requirement that a matching fact must have a schematic variable at that
   point. This gives a corresponding name to this ``slot'' for the purposes of
   forming a static closure, allowing the @{attribute "where"} attribute to
   perform an instantiation at run-time.
 \<close>
-text_raw\<open>\vbox{\<close>
+
     lemma
       assumes A: "Q \<Longrightarrow> False"
       shows "\<not> Q"
       by (match intros in X: "\<And>P. (P \<Longrightarrow> False) \<Longrightarrow> \<not> P" \<Rightarrow>
             \<open>rule X [where P = Q, OF A]\<close>)
-text_raw\<open>}\<close>
+
 text \<open>
   Subgoal focusing converts the outermost quantifiers of premises into
   schematics when lifting them to hypothetical facts. This allows us to
   instantiate them with @{attribute "where"} when using an appropriate match
   pattern.

 
 subsection \<open>Cut\<close>
 
 text \<open>
   Backtracking may be controlled more precisely by marking individual patterns
-  as \emph{cut}. This causes backtracking to not progress beyond this pattern:
+  as @{text cut}. This causes backtracking to not progress beyond this pattern:
   once a match is found no others will be considered.
 \<close>
 
     method foo\<^sub>2 =
       (match premises in I: "P \<and> Q" (cut) and I': "P \<longrightarrow> ?U" for P Q \<Rightarrow>

   targets. Each pattern is simply matched against the shallow structure of a
   fact or term. Most facts are in \emph{normal form}, which curries premises
   via meta-implication @{text "_ \<Longrightarrow> _"}.
 \<close>
 
-text_raw \<open>\vbox{\<close>
     lemma
       assumes asms: "D \<Longrightarrow> B \<Longrightarrow> C"  "D \<Longrightarrow> A"
       shows "D \<Longrightarrow> B \<Longrightarrow> C \<and> A"
       by (match asms in H: "D \<Longrightarrow> _" (multi) \<Rightarrow> \<open>prop_solver elims: H\<close>)
-text_raw \<open>}\<close>
+
 text \<open>
   For the first member of @{text asms} the dummy pattern successfully matches
   against @{term "B \<Longrightarrow> C"} and so the proof is successful.
 \<close>