diff -r 4f169d2cf6f3 -r 782f0b662cae src/Doc/Isar_Ref/Generic.thy --- a/src/Doc/Isar_Ref/Generic.thy Tue Oct 07 21:28:24 2014 +0200 +++ b/src/Doc/Isar_Ref/Generic.thy Tue Oct 07 21:29:59 2014 +0200 @@ -2,11 +2,11 @@ imports Base Main begin -chapter {* Generic tools and packages \label{ch:gen-tools} *} +chapter \Generic tools and packages \label{ch:gen-tools}\ -section {* Configuration options \label{sec:config} *} +section \Configuration options \label{sec:config}\ -text {* Isabelle/Pure maintains a record of named configuration +text \Isabelle/Pure maintains a record of named configuration options within the theory or proof context, with values of type @{ML_type bool}, @{ML_type int}, @{ML_type real}, or @{ML_type string}. Tools may declare options in ML, and then refer to these @@ -16,7 +16,7 @@ name. This form of context declaration works particularly well with commands such as @{command "declare"} or @{command "using"} like this: -*} +\ declare [[show_main_goal = false]] @@ -25,7 +25,7 @@ note [[show_main_goal = true]] end -text {* For historical reasons, some tools cannot take the full proof +text \For historical reasons, some tools cannot take the full proof context into account and merely refer to the background theory. This is accommodated by configuration options being declared as ``global'', which may not be changed within a local context. @@ -49,14 +49,14 @@ attempt to change a global option in a local context is ignored. \end{description} -*} +\ -section {* Basic proof tools *} +section \Basic proof tools\ -subsection {* Miscellaneous methods and attributes \label{sec:misc-meth-att} *} +subsection \Miscellaneous methods and attributes \label{sec:misc-meth-att}\ -text {* +text \ \begin{matharray}{rcl} @{method_def unfold} & : & @{text method} \\ @{method_def fold} & : & @{text method} \\ @@ -183,12 +183,12 @@ ones; this is mainly for tuning output of pretty printed theorems. \end{description} -*} +\ -subsection {* Low-level equational reasoning *} +subsection \Low-level equational reasoning\ -text {* +text \ \begin{matharray}{rcl} @{method_def subst} & : & @{text method} \\ @{method_def hypsubst} & : & @{text method} \\ @@ -251,12 +251,12 @@ @{attribute split}, for example. \end{description} -*} +\ -subsection {* Further tactic emulations \label{sec:tactics} *} +subsection \Further tactic emulations \label{sec:tactics}\ -text {* +text \ The following improper proof methods emulate traditional tactics. These admit direct access to the goal state, which is normally considered harmful! In particular, this may involve both numbered @@ -366,12 +366,12 @@ appear in production theories. \end{description} -*} +\ -section {* The Simplifier \label{sec:simplifier} *} +section \The Simplifier \label{sec:simplifier}\ -text {* The Simplifier performs conditional and unconditional +text \The Simplifier performs conditional and unconditional rewriting and uses contextual information: rule declarations in the background theory or local proof context are taken into account, as well as chained facts and subgoal premises (``local assumptions''). @@ -389,12 +389,12 @@ engaging into the internal structures. Thus it serves as general-purpose proof tool with the main focus on equational reasoning, and a bit more than that. -*} +\ -subsection {* Simplification methods \label{sec:simp-meth} *} +subsection \Simplification methods \label{sec:simp-meth}\ -text {* +text \ \begin{tabular}{rcll} @{method_def simp} & : & @{text method} \\ @{method_def simp_all} & : & @{text method} \\ @@ -505,38 +505,38 @@ \end{supertabular} \end{center} -*} +\ -subsubsection {* Examples *} +subsubsection \Examples\ -text {* We consider basic algebraic simplifications in Isabelle/HOL. +text \We consider basic algebraic simplifications in Isabelle/HOL. The rather trivial goal @{prop "0 + (x + 0) = x + 0 + 0"} looks like a good candidate to be solved by a single call of @{method simp}: -*} +\ lemma "0 + (x + 0) = x + 0 + 0" apply simp? oops -text {* The above attempt \emph{fails}, because @{term "0"} and @{term +text \The above attempt \emph{fails}, because @{term "0"} and @{term "op +"} in the HOL library are declared as generic type class operations, without stating any algebraic laws yet. More specific types are required to get access to certain standard simplifications - of the theory context, e.g.\ like this: *} + of the theory context, e.g.\ like this:\ lemma fixes x :: nat shows "0 + (x + 0) = x + 0 + 0" by simp lemma fixes x :: int shows "0 + (x + 0) = x + 0 + 0" by simp lemma fixes x :: "'a :: monoid_add" shows "0 + (x + 0) = x + 0 + 0" by simp -text {* +text \ \medskip In many cases, assumptions of a subgoal are also needed in the simplification process. For example: -*} +\ lemma fixes x :: nat shows "x = 0 \ x + x = 0" by simp lemma fixes x :: nat assumes "x = 0" shows "x + x = 0" apply simp oops lemma fixes x :: nat assumes "x = 0" shows "x + x = 0" using assms by simp -text {* As seen above, local assumptions that shall contribute to +text \As seen above, local assumptions that shall contribute to simplification need to be part of the subgoal already, or indicated explicitly for use by the subsequent method invocation. Both too little or too much information can make simplification fail, for @@ -550,19 +550,19 @@ nontermination, but not this one. The problem can be solved nonetheless, by ignoring assumptions via special options as explained before: -*} +\ lemma "(\x::nat. f x = g (f (g x))) \ f 0 = f 0 + 0" by (simp (no_asm)) -text {* The latter form is typical for long unstructured proof +text \The latter form is typical for long unstructured proof scripts, where the control over the goal content is limited. In structured proofs it is usually better to avoid pushing too many facts into the goal state in the first place. Assumptions in the Isar proof context do not intrude the reasoning if not used explicitly. This is illustrated for a toplevel statement and a local proof body as follows: -*} +\ lemma assumes "\x::nat. f x = g (f (g x))" @@ -574,7 +574,7 @@ have "f 0 = f 0 + 0" by simp end -text {* \medskip Because assumptions may simplify each other, there +text \\medskip Because assumptions may simplify each other, there can be very subtle cases of nontermination. For example, the regular @{method simp} method applied to @{prop "P (f x) \ y = x \ f x = f y \ Q"} gives rise to the infinite reduction sequence @@ -585,21 +585,21 @@ \] whereas applying the same to @{prop "y = x \ f x = f y \ P (f x) \ Q"} terminates (without solving the goal): -*} +\ lemma "y = x \ f x = f y \ P (f x) \ Q" apply simp oops -text {* See also \secref{sec:simp-trace} for options to enable +text \See also \secref{sec:simp-trace} for options to enable Simplifier trace mode, which often helps to diagnose problems with rewrite systems. -*} +\ -subsection {* Declaring rules \label{sec:simp-rules} *} +subsection \Declaring rules \label{sec:simp-rules}\ -text {* +text \ \begin{matharray}{rcl} @{attribute_def simp} & : & @{text attribute} \\ @{attribute_def split} & : & @{text attribute} \\ @@ -762,12 +762,12 @@ will contain the unwanted rules, and thus have to be deleted again in the theory body. \end{warn} -*} +\ -subsection {* Ordered rewriting with permutative rules *} +subsection \Ordered rewriting with permutative rules\ -text {* A rewrite rule is \emph{permutative} if the left-hand side and +text \A rewrite rule is \emph{permutative} if the left-hand side and right-hand side are the equal up to renaming of variables. The most common permutative rule is commutativity: @{text "?x + ?y = ?y + ?x"}. Other examples include @{text "(?x - ?y) - ?z = (?x - ?z) - @@ -790,12 +790,12 @@ \medskip Permutative rewrite rules are declared to the Simplifier just like other rewrite rules. Their special status is recognized automatically, and their application is guarded by the term ordering - accordingly. *} + accordingly.\ -subsubsection {* Rewriting with AC operators *} +subsubsection \Rewriting with AC operators\ -text {* Ordered rewriting is particularly effective in the case of +text \Ordered rewriting is particularly effective in the case of associative-commutative operators. (Associativity by itself is not permutative.) When dealing with an AC-operator @{text "f"}, keep the following points in mind: @@ -815,7 +815,7 @@ Ordered rewriting with the combination of A, C, and LC sorts a term lexicographically --- the rewriting engine imitates bubble-sort. -*} +\ locale AC_example = fixes f :: "'a \ 'a \ 'a" (infix "\" 60) @@ -831,13 +831,13 @@ lemmas AC_rules = assoc commute left_commute -text {* Thus the Simplifier is able to establish equalities with +text \Thus the Simplifier is able to establish equalities with arbitrary permutations of subterms, by normalizing to a common - standard form. For example: *} + standard form. For example:\ lemma "(b \ c) \ a = xxx" apply (simp only: AC_rules) - txt {* @{subgoals} *} + txt \@{subgoals}\ oops lemma "(b \ c) \ a = a \ (b \ c)" by (simp only: AC_rules) @@ -846,27 +846,27 @@ end -text {* Martin and Nipkow @{cite "martin-nipkow"} discuss the theory and +text \Martin and Nipkow @{cite "martin-nipkow"} discuss the theory and give many examples; other algebraic structures are amenable to ordered rewriting, such as Boolean rings. The Boyer-Moore theorem prover @{cite bm88book} also employs ordered rewriting. -*} +\ -subsubsection {* Re-orienting equalities *} +subsubsection \Re-orienting equalities\ -text {* Another application of ordered rewriting uses the derived rule +text \Another application of ordered rewriting uses the derived rule @{thm [source] eq_commute}: @{thm [source = false] eq_commute} to reverse equations. This is occasionally useful to re-orient local assumptions according to the term ordering, when other built-in mechanisms of - reorientation and mutual simplification fail to apply. *} + reorientation and mutual simplification fail to apply.\ -subsection {* Simplifier tracing and debugging \label{sec:simp-trace} *} +subsection \Simplifier tracing and debugging \label{sec:simp-trace}\ -text {* +text \ \begin{tabular}{rcll} @{attribute_def simp_trace} & : & @{text attribute} & default @{text false} \\ @{attribute_def simp_trace_depth_limit} & : & @{text attribute} & default @{text 1} \\ @@ -921,15 +921,15 @@ rewrite step. For example: \end{description} -*} +\ declare conjI [simp_break] declare [[simp_break "?x \ ?y"]] -subsection {* Simplification procedures \label{sec:simproc} *} +subsection \Simplification procedures \label{sec:simproc}\ -text {* Simplification procedures are ML functions that produce proven +text \Simplification procedures are ML functions that produce proven rewrite rules on demand. They are associated with higher-order patterns that approximate the left-hand sides of equations. The Simplifier first matches the current redex against one of the LHS @@ -985,43 +985,43 @@ already adds the new simproc to the subsequent context. \end{description} -*} +\ -subsubsection {* Example *} +subsubsection \Example\ -text {* The following simplification procedure for @{thm +text \The following simplification procedure for @{thm [source=false, show_types] unit_eq} in HOL performs fine-grained control over rule application, beyond higher-order pattern matching. Declaring @{thm unit_eq} as @{attribute simp} directly would make the Simplifier loop! Note that a version of this simplification - procedure is already active in Isabelle/HOL. *} + procedure is already active in Isabelle/HOL.\ -simproc_setup unit ("x::unit") = {* +simproc_setup unit ("x::unit") = \ fn _ => fn _ => fn ct => if HOLogic.is_unit (term_of ct) then NONE else SOME (mk_meta_eq @{thm unit_eq}) -*} +\ -text {* Since the Simplifier applies simplification procedures +text \Since the Simplifier applies simplification procedures frequently, it is important to make the failure check in ML - reasonably fast. *} + reasonably fast.\ -subsection {* Configurable Simplifier strategies \label{sec:simp-strategies} *} +subsection \Configurable Simplifier strategies \label{sec:simp-strategies}\ -text {* The core term-rewriting engine of the Simplifier is normally +text \The core term-rewriting engine of the Simplifier is normally used in combination with some add-on components that modify the strategy and allow to integrate other non-Simplifier proof tools. These may be reconfigured in ML as explained below. Even if the default strategies of object-logics like Isabelle/HOL are used unchanged, it helps to understand how the standard Simplifier - strategies work. *} + strategies work.\ -subsubsection {* The subgoaler *} +subsubsection \The subgoaler\ -text {* +text \ \begin{mldecls} @{index_ML Simplifier.set_subgoaler: "(Proof.context -> int -> tactic) -> Proof.context -> Proof.context"} \\ @@ -1049,23 +1049,23 @@ \end{description} As an example, consider the following alternative subgoaler: -*} +\ -ML {* +ML \ fun subgoaler_tac ctxt = assume_tac ORELSE' resolve_tac (Simplifier.prems_of ctxt) ORELSE' asm_simp_tac ctxt -*} +\ -text {* This tactic first tries to solve the subgoal by assumption or +text \This tactic first tries to solve the subgoal by assumption or by resolving with with one of the premises, calling simplification - only if that fails. *} + only if that fails.\ -subsubsection {* The solver *} +subsubsection \The solver\ -text {* +text \ \begin{mldecls} @{index_ML_type solver} \\ @{index_ML Simplifier.mk_solver: "string -> @@ -1162,12 +1162,12 @@ @{text "t = ?x"}. Otherwise it indicates that some congruence rule, or possibly the subgoaler or solver, is faulty. \end{warn} -*} +\ -subsubsection {* The looper *} +subsubsection \The looper\ -text {* +text \ \begin{mldecls} @{index_ML_op setloop: "Proof.context * (Proof.context -> int -> tactic) -> Proof.context"} \\ @@ -1246,12 +1246,12 @@ in tactic expressions that silently assume 0 or 1 subgoals after simplification. \end{warn} -*} +\ -subsection {* Forward simplification \label{sec:simp-forward} *} +subsection \Forward simplification \label{sec:simp-forward}\ -text {* +text \ \begin{matharray}{rcl} @{attribute_def simplified} & : & @{text attribute} \\ \end{matharray} @@ -1279,14 +1279,14 @@ under normal circumstances. \end{description} -*} +\ -section {* The Classical Reasoner \label{sec:classical} *} +section \The Classical Reasoner \label{sec:classical}\ -subsection {* Basic concepts *} +subsection \Basic concepts\ -text {* Although Isabelle is generic, many users will be working in +text \Although Isabelle is generic, many users will be working in some extension of classical first-order logic. Isabelle/ZF is built upon theory FOL, while Isabelle/HOL conceptually contains first-order logic as a fragment. Theorem-proving in predicate logic @@ -1300,7 +1300,7 @@ with high-end automated theorem provers, but they can save considerable time and effort in practice. They can prove theorems such as Pelletier's @{cite pelletier86} problems 40 and 41 in a few - milliseconds (including full proof reconstruction): *} + milliseconds (including full proof reconstruction):\ lemma "(\y. \x. F x y \ F x x) \ \ (\x. \y. \z. F z y \ \ F z x)" by blast @@ -1308,16 +1308,16 @@ lemma "(\z. \y. \x. f x y \ f x z \ \ f x x) \ \ (\z. \x. f x z)" by blast -text {* The proof tools are generic. They are not restricted to +text \The proof tools are generic. They are not restricted to first-order logic, and have been heavily used in the development of the Isabelle/HOL library and applications. The tactics can be traced, and their components can be called directly; in this manner, - any proof can be viewed interactively. *} + any proof can be viewed interactively.\ -subsubsection {* The sequent calculus *} +subsubsection \The sequent calculus\ -text {* Isabelle supports natural deduction, which is easy to use for +text \Isabelle supports natural deduction, which is easy to use for interactive proof. But natural deduction does not easily lend itself to automation, and has a bias towards intuitionism. For certain proofs in classical logic, it can not be called natural. @@ -1371,12 +1371,12 @@ manner. This yields a surprisingly effective proof procedure. Quantifiers add only few complications, since Isabelle handles parameters and schematic variables. See @{cite \Chapter 10\ - "paulson-ml2"} for further discussion. *} + "paulson-ml2"} for further discussion.\ -subsubsection {* Simulating sequents by natural deduction *} +subsubsection \Simulating sequents by natural deduction\ -text {* Isabelle can represent sequents directly, as in the +text \Isabelle can represent sequents directly, as in the object-logic LK. But natural deduction is easier to work with, and most object-logics employ it. Fortunately, we can simulate the sequent @{text "P\<^sub>1, \, P\<^sub>m \ Q\<^sub>1, \, Q\<^sub>n"} by the Isabelle formula @@ -1417,12 +1417,12 @@ regard for readability of intermediate goal states, we could treat the right side more uniformly by representing sequents as @{text [display] "P\<^sub>1 \ \ \ P\<^sub>m \ \ Q\<^sub>1 \ \ \ \ Q\<^sub>n \ \"} -*} +\ -subsubsection {* Extra rules for the sequent calculus *} +subsubsection \Extra rules for the sequent calculus\ -text {* As mentioned, destruction rules such as @{text "(\E1, 2)"} and +text \As mentioned, destruction rules such as @{text "(\E1, 2)"} and @{text "(\E)"} must be replaced by sequent-style elimination rules. In addition, we need rules to embody the classical equivalence between @{text "P \ Q"} and @{text "\ P \ Q"}. The introduction @@ -1472,12 +1472,12 @@ Depth-first search may well go down a blind alley; best-first search is better behaved in an infinite search space. However, quantifier replication is too expensive to prove any but the simplest theorems. -*} +\ -subsection {* Rule declarations *} +subsection \Rule declarations\ -text {* The proof tools of the Classical Reasoner depend on +text \The proof tools of the Classical Reasoner depend on collections of rules declared in the context, which are classified as introduction, elimination or destruction and as \emph{safe} or \emph{unsafe}. In general, safe rules can be attempted blindly, @@ -1578,12 +1578,12 @@ internally as explained above. \end{description} -*} +\ -subsection {* Structured methods *} +subsection \Structured methods\ -text {* +text \ \begin{matharray}{rcl} @{method_def rule} & : & @{text method} \\ @{method_def contradiction} & : & @{text method} \\ @@ -1611,12 +1611,12 @@ order. \end{description} -*} +\ -subsection {* Fully automated methods *} +subsection \Fully automated methods\ -text {* +text \ \begin{matharray}{rcl} @{method_def blast} & : & @{text method} \\ @{method_def auto} & : & @{text method} \\ @@ -1746,12 +1746,12 @@ semantics of these ad-hoc rule declarations is analogous to the attributes given before. Facts provided by forward chaining are inserted into the goal before commencing proof search. -*} +\ -subsection {* Partially automated methods *} +subsection \Partially automated methods\ -text {* These proof methods may help in situations when the +text \These proof methods may help in situations when the fully-automated tools fail. The result is a simpler subgoal that can be tackled by other means, such as by manual instantiation of quantifiers. @@ -1781,12 +1781,12 @@ splitter for the premises, the subgoal may still be split. \end{description} -*} +\ -subsection {* Single-step tactics *} +subsection \Single-step tactics\ -text {* +text \ \begin{matharray}{rcl} @{method_def safe_step} & : & @{text method} \\ @{method_def inst_step} & : & @{text method} \\ @@ -1827,12 +1827,12 @@ be eliminated. The safe wrapper tactical is applied. \end{description} -*} +\ -subsection {* Modifying the search step *} +subsection \Modifying the search step\ -text {* +text \ \begin{mldecls} @{index_ML_type wrapper: "(int -> tactic) -> (int -> tactic)"} \\[0.5ex] @{index_ML_op addSWrapper: "Proof.context * @@ -1919,12 +1919,12 @@ the each unsafe step of the search. \end{description} -*} +\ -section {* Object-logic setup \label{sec:object-logic} *} +section \Object-logic setup \label{sec:object-logic}\ -text {* +text \ \begin{matharray}{rcl} @{command_def "judgment"} & : & @{text "theory \ theory"} \\ @{method_def atomize} & : & @{text method} \\ @@ -1999,12 +1999,12 @@ rule statements over @{text "\"} and @{text "\"}. \end{description} -*} +\ -section {* Tracing higher-order unification *} +section \Tracing higher-order unification\ -text {* +text \ \begin{tabular}{rcll} @{attribute_def unify_trace_simp} & : & @{text "attribute"} & default @{text "false"} \\ @{attribute_def unify_trace_types} & : & @{text "attribute"} & default @{text "false"} \\ @@ -2044,6 +2044,6 @@ Options for unification cannot be modified in a local context. Only the global theory content is taken into account. \end{warn} -*} +\ end