# HG changeset patch # User wenzelm # Date 1444676965 -7200 # Node ID e39b85325b413fbf3496f1c49774740d335280d8 # Parent b9a3324e4e62974ef47a9d87c14b712842ba555a proper imports; more symbols; avoid special latex tricks; diff -r b9a3324e4e62 -r e39b85325b41 src/Doc/Eisbach/Manual.thy --- a/src/Doc/Eisbach/Manual.thy Mon Oct 12 20:58:58 2015 +0200 +++ b/src/Doc/Eisbach/Manual.thy Mon Oct 12 21:09:25 2015 +0200 @@ -1,7 +1,7 @@ (*:wrap=hard:maxLineLen=78:*) theory Manual -imports Base "../Eisbach_Tools" +imports Base "~~/src/HOL/Eisbach/Eisbach_Tools" begin chapter \The method command\ @@ -13,7 +13,8 @@ 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 \ @@ -177,7 +178,7 @@ @{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. \ -text_raw\\vbox{\ + method conj_with uses rule = (intro conjI ; intro rule) @@ -185,7 +186,7 @@ assumes A: "P" shows "P \ P \ P" by (conj_with rule: A) -text_raw\}\ + text \ Method definitions may take other methods as arguments, and thus implement method combinators with prefix syntax. For example, to more usefully exploit @@ -243,7 +244,8 @@ 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.\ @@ -278,7 +280,8 @@ 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 \ @@ -363,7 +366,8 @@ 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 @@ -526,13 +530,13 @@ forming a static closure, allowing the @{attribute "where"} attribute to perform an instantiation at run-time. \ -text_raw\\vbox{\ + lemma assumes A: "Q \ False" shows "\ Q" by (match intros in X: "\P. (P \ False) \ \ P" \ \rule X [where P = Q, OF A]\) -text_raw\}\ + text \ Subgoal focusing converts the outermost quantifiers of premises into schematics when lifting them to hypothetical facts. This allows us to @@ -713,7 +717,7 @@ text \ 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. \ @@ -806,12 +810,11 @@ via meta-implication @{text "_ \ _"}. \ -text_raw \\vbox{\ lemma assumes asms: "D \ B \ C" "D \ A" shows "D \ B \ C \ A" by (match asms in H: "D \ _" (multi) \ \prop_solver elims: H\) -text_raw \}\ + text \ For the first member of @{text asms} the dummy pattern successfully matches against @{term "B \ C"} and so the proof is successful. diff -r b9a3324e4e62 -r e39b85325b41 src/Doc/Eisbach/Preface.thy --- a/src/Doc/Eisbach/Preface.thy Mon Oct 12 20:58:58 2015 +0200 +++ b/src/Doc/Eisbach/Preface.thy Mon Oct 12 21:09:25 2015 +0200 @@ -1,7 +1,7 @@ (*:wrap=hard:maxLineLen=78:*) theory Preface -imports Base "../Eisbach_Tools" +imports Base "~~/src/HOL/Eisbach/Eisbach_Tools" begin text \ @@ -26,7 +26,8 @@ Traditionally proof methods have been written in Isabelle/ML, which poses a high barrier-to-entry for many users. - \medskip This manual is written for users familiar with Isabelle/Isar, but + \<^medskip> + This manual is written for users familiar with Isabelle/Isar, but not necessarily Isabelle/ML. It covers the usage of the @{command method} as well as the @{method match} method, as well as discussing their integration with existing Isar concepts such as @{command named_theorems}.