--- a/.hgtags Wed Feb 10 15:49:05 2016 +0100
+++ b/.hgtags Fri Feb 12 22:36:48 2016 +0100
@@ -32,3 +32,7 @@
5ae2a2e74c93eafeb00b1ddeef0404256745ebba Isabelle2015
e18444532fce734c2508ccffd84a4b9f166901e3 Isabelle2016-RC0
155d30f721dd7e465b9640b550b7f44ecf8b1970 Isabelle2016-RC1
+5d513565749e6818ce3bbd1b40739ddc314e17a5 Isabelle2016-RC2
+81cbea2babd968353655a825645914672529b310 Isabelle2016-RC3
+f4baefee57768cf00b1a9e003770c7573b5d7378 Isabelle2016-RC4
+45adb8dc84e1279f415cc00ee7c5e0a542fd339e Isabelle2016-RC5
--- a/Admin/Release/CHECKLIST Wed Feb 10 15:49:05 2016 +0100
+++ b/Admin/Release/CHECKLIST Fri Feb 12 22:36:48 2016 +0100
@@ -28,9 +28,9 @@
- update https://bitbucket.org/isabelle_project/isabelle-website
-- maintain doc/Contents;
+- check doc/Contents, src/Tools/jEdit/dist/doc/Contents;
-- maintain Logics:
+- check Logics:
ROOTS
lib/html/library_index_content.template
--- a/Admin/components/components.sha1 Wed Feb 10 15:49:05 2016 +0100
+++ b/Admin/components/components.sha1 Fri Feb 12 22:36:48 2016 +0100
@@ -112,10 +112,12 @@
b4b624fb5f34d1dc814fb4fb469fafd7d7ea018a polyml-5.5.3-20150908.tar.gz
b668e1f43a41608a8eb365c5e19db6c54c72748a polyml-5.5.3-20150911.tar.gz
1f5cd9b1390dab13861f90dfc06d4180cc107587 polyml-5.5.3-20150916.tar.gz
+f78896e588e8ebb4da57bf0c95210b0f0fa9e551 polyml-5.6-1.tar.gz
03ba81e595fa6d6df069532d67ad3195c37d9046 polyml-5.6-20151123.tar.gz
822f489c18e38ce5ef979ec21dccce4473e09be6 polyml-5.6-20151206.tar.gz
bd6a448f0e0d5787747f4f30ca661f9c1868e4a7 polyml-5.6-20151223.tar.gz
5b70c12c95a90d858f90c1945011289944ea8e17 polyml-5.6-20160118.tar.gz
+5b19dc93082803b82aa553a5cfb3e914606c0ffd polyml-5.6.tar.gz
8ee375cfc38972f080dbc78f07b68dac03efe968 ProofGeneral-3.7.1.1.tar.gz
847b52c0676b5eb0fbf0476f64fc08c2d72afd0c ProofGeneral-4.1.tar.gz
8e0b2b432755ef11d964e20637d1bc567d1c0477 ProofGeneral-4.2-1.tar.gz
--- a/Admin/components/main Wed Feb 10 15:49:05 2016 +0100
+++ b/Admin/components/main Fri Feb 12 22:36:48 2016 +0100
@@ -10,7 +10,7 @@
jfreechart-1.0.14-1
jortho-1.0-2
kodkodi-1.5.2
-polyml-5.6-20160118
+polyml-5.6-1
scala-2.11.7
spass-3.8ds
xz-java-1.2-1
--- a/Admin/polyml/README Wed Feb 10 15:49:05 2016 +0100
+++ b/Admin/polyml/README Fri Feb 12 22:36:48 2016 +0100
@@ -1,8 +1,19 @@
Poly/ML for Isabelle
====================
-This is a preview of Poly/ML 5.6, based on
-https://github.com/polyml/polyml/ commit 72a1c60e3d00.
+This compilation of Poly/ML 5.6 (http://www.polyml.org) is based on the source
+distribution from https://github.com/polyml/polyml/releases/tag/v5.6/.
+
+On Linux the sources have changed as follows, in order to evade a
+potential conflict of /bin/bash versus /bin/sh -> dash (notably on
+Ubuntu and Debian):
+
+diff -r src-orig/libpolyml/process_env.cpp src/libpolyml/process_env.cpp
+228c228
+< execve("/bin/sh", argv, environ);
+---
+> execvp("bash", argv);
+
The included build script is used like this:
@@ -14,8 +25,8 @@
./build src x86_64-windows --with-gmp
Also note that the separate "sha1" library module is required for
-efficient digesting of strings according to SHA-1.
+efficient digestion of strings according to SHA-1.
Makarius
- 18-Jan-2016
+ 11-Feb-2016
--- a/CONTRIBUTORS Wed Feb 10 15:49:05 2016 +0100
+++ b/CONTRIBUTORS Fri Feb 12 22:36:48 2016 +0100
@@ -14,10 +14,6 @@
Support for real exponentiation ("powr") in the "approximation" method.
(This was removed in Isabelle 2015 due to a changed definition of "powr")
-* Summer 2014: Jeremy Avigad, Luke Serafin, CMU, and Johannes Hölzl, TUM
- Proof of the central limit theorem: includes weak convergence,
- characteristic functions, and Levy's uniqueness and continuity theorem.
-
* Summer 2015 - Winter 2016: Lawrence C Paulson, Cambridge
General, homology form of Cauchy's integral theorem and supporting material
(ported from HOL Light).
@@ -25,6 +21,13 @@
* Winter 2015/16: Gerwin Klein, NICTA
New print_record command.
+* May - December 2015: Makarius Wenzel
+ Prover IDE improvements.
+ More Isar language elements.
+ Document language refinements.
+ Poly/ML debugger integration.
+ Improved multi-platform and multi-architecture support.
+
* Winter 2015: Manuel Eberl, TUM
The radius of convergence of power series and various summability tests.
Harmonic numbers and the Euler-Mascheroni constant.
@@ -63,6 +66,10 @@
Command to lift a BNF structure on the raw type to the abstract type for
typedefs.
+* Summer 2014: Jeremy Avigad, Luke Serafin, CMU, and Johannes Hölzl, TUM
+ Proof of the central limit theorem: includes weak convergence,
+ characteristic functions, and Levy's uniqueness and continuity theorem.
+
Contributions to Isabelle2015
-----------------------------
--- a/NEWS Wed Feb 10 15:49:05 2016 +0100
+++ b/NEWS Fri Feb 12 22:36:48 2016 +0100
@@ -66,13 +66,13 @@
*** Prover IDE -- Isabelle/Scala/jEdit ***
* IDE support for the source-level debugger of Poly/ML, to work with
-Isabelle/ML and official Standard ML. Configuration option "ML_debugger"
-and commands 'ML_file_debug', 'ML_file_no_debug', 'SML_file_debug',
-'SML_file_no_debug' control compilation of sources with debugging
-information. The Debugger panel allows to set breakpoints (via context
-menu), step through stopped threads, evaluate local ML expressions etc.
-At least one Debugger view needs to be active to have any effect on the
-running ML program.
+Isabelle/ML and official Standard ML. Option "ML_debugger" and commands
+'ML_file_debug', 'ML_file_no_debug', 'SML_file_debug',
+'SML_file_no_debug' control compilation of sources with or without
+debugging information. The Debugger panel allows to set breakpoints (via
+context menu), step through stopped threads, evaluate local ML
+expressions etc. At least one Debugger view needs to be active to have
+any effect on the running ML program.
* The State panel manages explicit proof state output, with dynamic
auto-update according to cursor movement. Alternatively, the jEdit
@@ -95,8 +95,8 @@
due to ad-hoc updates by auxiliary GUI components, such as the State
panel.
-* Improved scheduling for urgent print tasks (e.g. command state output,
-interactive queries) wrt. long-running background tasks.
+* Slightly improved scheduling for urgent print tasks (e.g. command
+state output, interactive queries) wrt. long-running background tasks.
* Completion of symbols via prefix of \<name> or \<^name> or \name is
always possible, independently of the language context. It is never
@@ -106,6 +106,11 @@
$ISABELLE_HOME/etc/abbrevs and $ISABELLE_HOME_USER/etc/abbrevs, with
support for simple templates using ASCII 007 (bell) as placeholder.
+* Symbols \<oplus>, \<Oplus>, \<otimes>, \<Otimes>, \<odot>, \<Odot>, \<ominus>, \<oslash> no longer provide abbreviations for
+completion like "+o", "*o", ".o" etc. -- due to conflicts with other
+ASCII syntax. INCOMPATIBILITY, use plain backslash-completion or define
+suitable abbreviations in $ISABELLE_HOME_USER/etc/abbrevs.
+
* Action "isabelle-emph" (with keyboard shortcut C+e LEFT) controls
emphasized text style; the effect is visible in document output, not in
the editor.
@@ -183,8 +188,8 @@
* Antiquotation @{verbatim [display]} supports option "indent".
* Antiquotation @{theory_text} prints uninterpreted theory source text
-(outer syntax with command keywords etc.). This may be used in the short
-form \<^theory_text>\<open>...\<close>. @{theory_text [display]} supports option "indent".
+(Isar outer syntax with command keywords etc.). This may be used in the
+short form \<^theory_text>\<open>...\<close>. @{theory_text [display]} supports option "indent".
* Antiquotation @{doc ENTRY} provides a reference to the given
documentation, with a hyperlink in the Prover IDE.
@@ -594,8 +599,8 @@
- New commands "lift_bnf" and "copy_bnf" for lifting (copying) a BNF
structure on the raw type to an abstract type defined using typedef.
- Always generate "case_transfer" theorem.
- - For mutual types, generate slightly stronger "rel_induct", "rel_coinduct",
- and "coinduct" theorems. INCOMPATIBLITY.
+ - For mutual types, generate slightly stronger "rel_induct",
+ "rel_coinduct", and "coinduct" theorems. INCOMPATIBLITY.
- Allow discriminators and selectors with the same name as the type
being defined.
- Avoid various internal name clashes (e.g., 'datatype f = f').
@@ -682,8 +687,8 @@
less_eq_multiset.rep_eq ~> subseteq_mset_def
INCOMPATIBILITY
- Removed lemmas generated by lift_definition:
- less_eq_multiset.abs_eq, less_eq_multiset.rsp less_eq_multiset.transfer
- less_eq_multiset_def
+ less_eq_multiset.abs_eq, less_eq_multiset.rsp,
+ less_eq_multiset.transfer, less_eq_multiset_def
INCOMPATIBILITY
* Library/Omega_Words_Fun: Infinite words modeled as functions nat \<Rightarrow> 'a.
@@ -708,6 +713,9 @@
import of parent, as for general 'locale' expressions. INCOMPATIBILITY,
remove '!' and add '?' as required.
+* HOL-Decision_Procs: The "approximation" method works with "powr"
+(exponentiation on real numbers) again.
+
* HOL-Multivariate_Analysis: theory Cauchy_Integral_Thm with Contour
integrals (= complex path integrals), Cauchy's integral theorem, winding
numbers and Cauchy's integral formula, Liouville theorem, Fundamental
@@ -1249,9 +1257,6 @@
method. See HOL/Decision_Procs/ex/Approximation_Quickcheck_Ex.thy for
examples.
-* HOL-Decision_Procs: The "approximation" method works with "powr"
- (exponentiation on real numbers) again.
-
* HOL-Probability: Reworked measurability prover
- applies destructor rules repeatedly
- removed application splitting (replaced by destructor rule)
--- a/etc/settings Wed Feb 10 15:49:05 2016 +0100
+++ b/etc/settings Fri Feb 12 22:36:48 2016 +0100
@@ -14,7 +14,7 @@
ISABELLE_SCALA_BUILD_OPTIONS="-encoding UTF-8 -nowarn -target:jvm-1.7 -Xmax-classfile-name 130"
-ISABELLE_JAVA_SYSTEM_OPTIONS="-server -XX:+UseConcMarkSweepGC -XX:+CMSParallelRemarkEnabled -Dfile.encoding=UTF-8 -Disabelle.threads=0"
+ISABELLE_JAVA_SYSTEM_OPTIONS="-server -Dfile.encoding=UTF-8 -Disabelle.threads=0"
classpath "$ISABELLE_HOME/lib/classes/Pure.jar"
--- a/etc/symbols Wed Feb 10 15:49:05 2016 +0100
+++ b/etc/symbols Fri Feb 12 22:36:48 2016 +0100
@@ -295,14 +295,14 @@
\<triangleright> code: 0x0025b9 group: relation
\<triangle> code: 0x0025b3 group: relation
\<triangleq> code: 0x00225c group: relation
-\<oplus> code: 0x002295 group: operator abbrev: +o
-\<Oplus> code: 0x002a01 group: operator abbrev: +O
-\<otimes> code: 0x002297 group: operator abbrev: *o
-\<Otimes> code: 0x002a02 group: operator abbrev: *O
-\<odot> code: 0x002299 group: operator abbrev: .o
-\<Odot> code: 0x002a00 group: operator abbrev: .O
-\<ominus> code: 0x002296 group: operator abbrev: -o
-\<oslash> code: 0x002298 group: operator abbrev: /o
+\<oplus> code: 0x002295 group: operator
+\<Oplus> code: 0x002a01 group: operator
+\<otimes> code: 0x002297 group: operator
+\<Otimes> code: 0x002a02 group: operator
+\<odot> code: 0x002299 group: operator
+\<Odot> code: 0x002a00 group: operator
+\<ominus> code: 0x002296 group: operator
+\<oslash> code: 0x002298 group: operator
\<dots> code: 0x002026 group: punctuation abbrev: ...
\<cdots> code: 0x0022ef group: punctuation
\<Sum> code: 0x002211 group: operator abbrev: SUM
@@ -357,7 +357,7 @@
\<some> code: 0x0003f5
\<hole> code: 0x002311
\<newline> code: 0x0023ce
-\<comment> code: 0x002015 font: IsabelleText
+\<comment> code: 0x002015 group: document font: IsabelleText
\<open> code: 0x002039 group: punctuation font: IsabelleText abbrev: <<
\<close> code: 0x00203a group: punctuation font: IsabelleText abbrev: >>
\<here> code: 0x002302 font: IsabelleText
--- a/src/Doc/Isar_Ref/Base.thy Wed Feb 10 15:49:05 2016 +0100
+++ b/src/Doc/Isar_Ref/Base.thy Fri Feb 12 22:36:48 2016 +0100
@@ -2,8 +2,14 @@
theory Base
imports Pure
+keywords "\<proof>" :: "qed" % "proof"
begin
+ML \<open>
+ Outer_Syntax.command @{command_keyword "\<proof>"} "dummy proof"
+ (Scan.succeed Isar_Cmd.skip_proof);
+\<close>
+
ML_file "../antiquote_setup.ML"
end
--- a/src/Doc/Isar_Ref/Document_Preparation.thy Wed Feb 10 15:49:05 2016 +0100
+++ b/src/Doc/Isar_Ref/Document_Preparation.thy Fri Feb 12 22:36:48 2016 +0100
@@ -409,6 +409,49 @@
\<close>
+section \<open>Markdown-like text structure\<close>
+
+text \<open>
+ The markup commands @{command_ref text}, @{command_ref txt}, @{command_ref
+ text_raw} (\secref{sec:markup}) consist of plain text. Its internal
+ structure consists of paragraphs and (nested) lists, using special Isabelle
+ symbols and some rules for indentation and blank lines. This quasi-visual
+ format resembles \<^emph>\<open>Markdown\<close>\<^footnote>\<open>@{url "http://commonmark.org"}\<close>, but the
+ full complexity of that notation is avoided.
+
+ This is a summary of the main principles of minimal Markdown in Isabelle:
+
+ \<^item> List items start with the following markers
+ \<^descr>[itemize:] \<^verbatim>\<open>\<^item>\<close>
+ \<^descr>[enumerate:] \<^verbatim>\<open>\<^enum>\<close>
+ \<^descr>[description:] \<^verbatim>\<open>\<^descr>\<close>
+
+ \<^item> Adjacent list items with same indentation and same marker are grouped
+ into a single list.
+
+ \<^item> Singleton blank lines separate paragraphs.
+
+ \<^item> Multiple blank lines escape from the current list hierarchy.
+
+ Notable differences to official Markdown:
+
+ \<^item> Indentation of list items needs to match exactly.
+
+ \<^item> Indentation is unlimited (official Markdown interprets four spaces as
+ block quote).
+
+ \<^item> List items always consist of paragraphs --- there is no notion of
+ ``tight'' list.
+
+ \<^item> Section headings are expressed via Isar document markup commands
+ (\secref{sec:markup}).
+
+ \<^item> URLs, font styles, other special content is expressed via antiquotations
+ (\secref{sec:antiq}), usually with proper nesting of sub-languages via
+ text cartouches.
+\<close>
+
+
section \<open>Markup via command tags \label{sec:tags}\<close>
text \<open>
--- a/src/Doc/Isar_Ref/First_Order_Logic.thy Wed Feb 10 15:49:05 2016 +0100
+++ b/src/Doc/Isar_Ref/First_Order_Logic.thy Fri Feb 12 22:36:48 2016 +0100
@@ -7,24 +7,21 @@
begin
text \<open>
- In order to commence a new object-logic within
- Isabelle/Pure we introduce abstract syntactic categories \<open>i\<close>
- for individuals and \<open>o\<close> for object-propositions. The latter
- is embedded into the language of Pure propositions by means of a
- separate judgment.
+ In order to commence a new object-logic within Isabelle/Pure we introduce
+ abstract syntactic categories \<open>i\<close> for individuals and \<open>o\<close> for
+ object-propositions. The latter is embedded into the language of Pure
+ propositions by means of a separate judgment.
\<close>
typedecl i
typedecl o
-judgment
- Trueprop :: "o \<Rightarrow> prop" ("_" 5)
+judgment Trueprop :: "o \<Rightarrow> prop" ("_" 5)
text \<open>
- Note that the object-logic judgment is implicit in the
- syntax: writing @{prop A} produces @{term "Trueprop A"} internally.
- From the Pure perspective this means ``@{prop A} is derivable in the
- object-logic''.
+ Note that the object-logic judgment is implicit in the syntax: writing
+ @{prop A} produces @{term "Trueprop A"} internally. From the Pure
+ perspective this means ``@{prop A} is derivable in the object-logic''.
\<close>
@@ -32,23 +29,20 @@
text \<open>
Equality is axiomatized as a binary predicate on individuals, with
- reflexivity as introduction, and substitution as elimination
- principle. Note that the latter is particularly convenient in a
- framework like Isabelle, because syntactic congruences are
- implicitly produced by unification of @{term "B x"} against
- expressions containing occurrences of @{term x}.
+ reflexivity as introduction, and substitution as elimination principle. Note
+ that the latter is particularly convenient in a framework like Isabelle,
+ because syntactic congruences are implicitly produced by unification of
+ \<open>B x\<close> against expressions containing occurrences of \<open>x\<close>.
\<close>
-axiomatization
- equal :: "i \<Rightarrow> i \<Rightarrow> o" (infix "=" 50)
-where
- refl [intro]: "x = x" and
- subst [elim]: "x = y \<Longrightarrow> B x \<Longrightarrow> B y"
+axiomatization equal :: "i \<Rightarrow> i \<Rightarrow> o" (infix "=" 50)
+ where refl [intro]: "x = x"
+ and subst [elim]: "x = y \<Longrightarrow> B x \<Longrightarrow> B y"
text \<open>
- Substitution is very powerful, but also hard to control in
- full generality. We derive some common symmetry~/ transitivity
- schemes of @{term equal} as particular consequences.
+ Substitution is very powerful, but also hard to control in full generality.
+ We derive some common symmetry~/ transitivity schemes of @{term equal} as
+ particular consequences.
\<close>
theorem sym [sym]:
@@ -87,10 +81,9 @@
subsection \<open>Basic group theory\<close>
text \<open>
- As an example for equational reasoning we consider some bits of
- group theory. The subsequent locale definition postulates group
- operations and axioms; we also derive some consequences of this
- specification.
+ As an example for equational reasoning we consider some bits of group
+ theory. The subsequent locale definition postulates group operations and
+ axioms; we also derive some consequences of this specification.
\<close>
locale group =
@@ -125,20 +118,19 @@
qed
text \<open>
- Reasoning from basic axioms is often tedious. Our proofs
- work by producing various instances of the given rules (potentially
- the symmetric form) using the pattern ``@{command have}~\<open>eq\<close>~@{command "by"}~\<open>(rule r)\<close>'' and composing the chain of
- results via @{command also}/@{command finally}. These steps may
- involve any of the transitivity rules declared in
- \secref{sec:framework-ex-equal}, namely @{thm trans} in combining
- the first two results in @{thm right_inv} and in the final steps of
- both proofs, @{thm forw_subst} in the first combination of @{thm
+ Reasoning from basic axioms is often tedious. Our proofs work by producing
+ various instances of the given rules (potentially the symmetric form) using
+ the pattern ``\<^theory_text>\<open>have eq by (rule r)\<close>'' and composing the chain of results
+ via \<^theory_text>\<open>also\<close>/\<^theory_text>\<open>finally\<close>. These steps may involve any of the transitivity
+ rules declared in \secref{sec:framework-ex-equal}, namely @{thm trans} in
+ combining the first two results in @{thm right_inv} and in the final steps
+ of both proofs, @{thm forw_subst} in the first combination of @{thm
right_unit}, and @{thm back_subst} in all other calculational steps.
- Occasional substitutions in calculations are adequate, but should
- not be over-emphasized. The other extreme is to compose a chain by
- plain transitivity only, with replacements occurring always in
- topmost position. For example:
+ Occasional substitutions in calculations are adequate, but should not be
+ over-emphasized. The other extreme is to compose a chain by plain
+ transitivity only, with replacements occurring always in topmost position.
+ For example:
\<close>
(*<*)
@@ -157,12 +149,11 @@
(*>*)
text \<open>
- Here we have re-used the built-in mechanism for unfolding
- definitions in order to normalize each equational problem. A more
- realistic object-logic would include proper setup for the Simplifier
- (\secref{sec:simplifier}), the main automated tool for equational
- reasoning in Isabelle. Then ``@{command unfolding}~@{thm
- left_inv}~@{command ".."}'' would become ``@{command "by"}~\<open>(simp only: left_inv)\<close>'' etc.
+ Here we have re-used the built-in mechanism for unfolding definitions in
+ order to normalize each equational problem. A more realistic object-logic
+ would include proper setup for the Simplifier (\secref{sec:simplifier}), the
+ main automated tool for equational reasoning in Isabelle. Then ``\<^theory_text>\<open>unfolding
+ left_inv ..\<close>'' would become ``\<^theory_text>\<open>by (simp only: left_inv)\<close>'' etc.
\<close>
end
@@ -172,33 +163,29 @@
text \<open>
We axiomatize basic connectives of propositional logic: implication,
- disjunction, and conjunction. The associated rules are modeled
- after Gentzen's system of Natural Deduction @{cite "Gentzen:1935"}.
+ disjunction, and conjunction. The associated rules are modeled after
+ Gentzen's system of Natural Deduction @{cite "Gentzen:1935"}.
\<close>
-axiomatization
- imp :: "o \<Rightarrow> o \<Rightarrow> o" (infixr "\<longrightarrow>" 25) where
- impI [intro]: "(A \<Longrightarrow> B) \<Longrightarrow> A \<longrightarrow> B" and
- impD [dest]: "(A \<longrightarrow> B) \<Longrightarrow> A \<Longrightarrow> B"
+axiomatization imp :: "o \<Rightarrow> o \<Rightarrow> o" (infixr "\<longrightarrow>" 25)
+ where impI [intro]: "(A \<Longrightarrow> B) \<Longrightarrow> A \<longrightarrow> B"
+ and impD [dest]: "(A \<longrightarrow> B) \<Longrightarrow> A \<Longrightarrow> B"
-axiomatization
- disj :: "o \<Rightarrow> o \<Rightarrow> o" (infixr "\<or>" 30) where
- disjI\<^sub>1 [intro]: "A \<Longrightarrow> A \<or> B" and
- disjI\<^sub>2 [intro]: "B \<Longrightarrow> A \<or> B" and
- disjE [elim]: "A \<or> B \<Longrightarrow> (A \<Longrightarrow> C) \<Longrightarrow> (B \<Longrightarrow> C) \<Longrightarrow> C"
+axiomatization disj :: "o \<Rightarrow> o \<Rightarrow> o" (infixr "\<or>" 30)
+ where disjI\<^sub>1 [intro]: "A \<Longrightarrow> A \<or> B"
+ and disjI\<^sub>2 [intro]: "B \<Longrightarrow> A \<or> B"
+ and disjE [elim]: "A \<or> B \<Longrightarrow> (A \<Longrightarrow> C) \<Longrightarrow> (B \<Longrightarrow> C) \<Longrightarrow> C"
-axiomatization
- conj :: "o \<Rightarrow> o \<Rightarrow> o" (infixr "\<and>" 35) where
- conjI [intro]: "A \<Longrightarrow> B \<Longrightarrow> A \<and> B" and
- conjD\<^sub>1: "A \<and> B \<Longrightarrow> A" and
- conjD\<^sub>2: "A \<and> B \<Longrightarrow> B"
+axiomatization conj :: "o \<Rightarrow> o \<Rightarrow> o" (infixr "\<and>" 35)
+ where conjI [intro]: "A \<Longrightarrow> B \<Longrightarrow> A \<and> B"
+ and conjD\<^sub>1: "A \<and> B \<Longrightarrow> A"
+ and conjD\<^sub>2: "A \<and> B \<Longrightarrow> B"
text \<open>
- The conjunctive destructions have the disadvantage that
- decomposing @{prop "A \<and> B"} involves an immediate decision which
- component should be projected. The more convenient simultaneous
- elimination @{prop "A \<and> B \<Longrightarrow> (A \<Longrightarrow> B \<Longrightarrow> C) \<Longrightarrow> C"} can be derived as
- follows:
+ The conjunctive destructions have the disadvantage that decomposing @{prop
+ "A \<and> B"} involves an immediate decision which component should be projected.
+ The more convenient simultaneous elimination @{prop "A \<and> B \<Longrightarrow> (A \<Longrightarrow> B \<Longrightarrow> C) \<Longrightarrow>
+ C"} can be derived as follows:
\<close>
theorem conjE [elim]:
@@ -210,13 +197,14 @@
qed
text \<open>
- Here is an example of swapping conjuncts with a single
- intermediate elimination step:
+ Here is an example of swapping conjuncts with a single intermediate
+ elimination step:
\<close>
(*<*)
lemma "\<And>A. PROP A \<Longrightarrow> PROP A"
proof -
+ fix A B
(*>*)
assume "A \<and> B"
then obtain B and A ..
@@ -226,23 +214,21 @@
(*>*)
text \<open>
- Note that the analogous elimination rule for disjunction
- ``\<open>\<ASSUMES> A \<or> B \<OBTAINS> A \<BBAR> B\<close>'' coincides with
- the original axiomatization of @{thm disjE}.
+ Note that the analogous elimination rule for disjunction ``\<^theory_text>\<open>assumes "A \<or> B"
+ obtains A \<BBAR> B\<close>'' coincides with the original axiomatization of @{thm
+ disjE}.
\<^medskip>
- We continue propositional logic by introducing absurdity
- with its characteristic elimination. Plain truth may then be
- defined as a proposition that is trivially true.
+ We continue propositional logic by introducing absurdity with its
+ characteristic elimination. Plain truth may then be defined as a proposition
+ that is trivially true.
\<close>
-axiomatization
- false :: o ("\<bottom>") where
- falseE [elim]: "\<bottom> \<Longrightarrow> A"
+axiomatization false :: o ("\<bottom>")
+ where falseE [elim]: "\<bottom> \<Longrightarrow> A"
-definition
- true :: o ("\<top>") where
- "\<top> \<equiv> \<bottom> \<longrightarrow> \<bottom>"
+definition true :: o ("\<top>")
+ where "\<top> \<equiv> \<bottom> \<longrightarrow> \<bottom>"
theorem trueI [intro]: \<top>
unfolding true_def ..
@@ -252,9 +238,8 @@
Now negation represents an implication towards absurdity:
\<close>
-definition
- not :: "o \<Rightarrow> o" ("\<not> _" [40] 40) where
- "\<not> A \<equiv> A \<longrightarrow> \<bottom>"
+definition not :: "o \<Rightarrow> o" ("\<not> _" [40] 40)
+ where "\<not> A \<equiv> A \<longrightarrow> \<bottom>"
theorem notI [intro]:
assumes "A \<Longrightarrow> \<bottom>"
@@ -278,10 +263,10 @@
subsection \<open>Classical logic\<close>
text \<open>
- Subsequently we state the principle of classical contradiction as a
- local assumption. Thus we refrain from forcing the object-logic
- into the classical perspective. Within that context, we may derive
- well-known consequences of the classical principle.
+ Subsequently we state the principle of classical contradiction as a local
+ assumption. Thus we refrain from forcing the object-logic into the classical
+ perspective. Within that context, we may derive well-known consequences of
+ the classical principle.
\<close>
locale classical =
@@ -312,17 +297,15 @@
qed
text \<open>
- These examples illustrate both classical reasoning and
- non-trivial propositional proofs in general. All three rules
- characterize classical logic independently, but the original rule is
- already the most convenient to use, because it leaves the conclusion
- unchanged. Note that @{prop "(\<not> C \<Longrightarrow> C) \<Longrightarrow> C"} fits again into our
- format for eliminations, despite the additional twist that the
- context refers to the main conclusion. So we may write @{thm
- classical} as the Isar statement ``\<open>\<OBTAINS> \<not> thesis\<close>''.
- This also explains nicely how classical reasoning really works:
- whatever the main \<open>thesis\<close> might be, we may always assume its
- negation!
+ These examples illustrate both classical reasoning and non-trivial
+ propositional proofs in general. All three rules characterize classical
+ logic independently, but the original rule is already the most convenient to
+ use, because it leaves the conclusion unchanged. Note that @{prop "(\<not> C \<Longrightarrow> C)
+ \<Longrightarrow> C"} fits again into our format for eliminations, despite the additional
+ twist that the context refers to the main conclusion. So we may write @{thm
+ classical} as the Isar statement ``\<^theory_text>\<open>obtains \<not> thesis\<close>''. This also explains
+ nicely how classical reasoning really works: whatever the main \<open>thesis\<close>
+ might be, we may always assume its negation!
\<close>
end
@@ -331,28 +314,25 @@
subsection \<open>Quantifiers \label{sec:framework-ex-quant}\<close>
text \<open>
- Representing quantifiers is easy, thanks to the higher-order nature
- of the underlying framework. According to the well-known technique
- introduced by Church @{cite "church40"}, quantifiers are operators on
- predicates, which are syntactically represented as \<open>\<lambda>\<close>-terms
- of type @{typ "i \<Rightarrow> o"}. Binder notation turns \<open>All (\<lambda>x. B
- x)\<close> into \<open>\<forall>x. B x\<close> etc.
+ Representing quantifiers is easy, thanks to the higher-order nature of the
+ underlying framework. According to the well-known technique introduced by
+ Church @{cite "church40"}, quantifiers are operators on predicates, which
+ are syntactically represented as \<open>\<lambda>\<close>-terms of type @{typ "i \<Rightarrow> o"}. Binder
+ notation turns \<open>All (\<lambda>x. B x)\<close> into \<open>\<forall>x. B x\<close> etc.
\<close>
-axiomatization
- All :: "(i \<Rightarrow> o) \<Rightarrow> o" (binder "\<forall>" 10) where
- allI [intro]: "(\<And>x. B x) \<Longrightarrow> \<forall>x. B x" and
- allD [dest]: "(\<forall>x. B x) \<Longrightarrow> B a"
+axiomatization All :: "(i \<Rightarrow> o) \<Rightarrow> o" (binder "\<forall>" 10)
+ where allI [intro]: "(\<And>x. B x) \<Longrightarrow> \<forall>x. B x"
+ and allD [dest]: "(\<forall>x. B x) \<Longrightarrow> B a"
-axiomatization
- Ex :: "(i \<Rightarrow> o) \<Rightarrow> o" (binder "\<exists>" 10) where
- exI [intro]: "B a \<Longrightarrow> (\<exists>x. B x)" and
- exE [elim]: "(\<exists>x. B x) \<Longrightarrow> (\<And>x. B x \<Longrightarrow> C) \<Longrightarrow> C"
+axiomatization Ex :: "(i \<Rightarrow> o) \<Rightarrow> o" (binder "\<exists>" 10)
+ where exI [intro]: "B a \<Longrightarrow> (\<exists>x. B x)"
+ and exE [elim]: "(\<exists>x. B x) \<Longrightarrow> (\<And>x. B x \<Longrightarrow> C) \<Longrightarrow> C"
text \<open>
- The statement of @{thm exE} corresponds to ``\<open>\<ASSUMES> \<exists>x. B x \<OBTAINS> x \<WHERE> B x\<close>'' in Isar. In the
- subsequent example we illustrate quantifier reasoning involving all
- four rules:
+ The statement of @{thm exE} corresponds to ``\<^theory_text>\<open>assumes "\<exists>x. B x" obtains x
+ where "B x"\<close>'' in Isar. In the subsequent example we illustrate quantifier
+ reasoning involving all four rules:
\<close>
theorem
@@ -369,43 +349,42 @@
text \<open>
The main rules of first-order predicate logic from
- \secref{sec:framework-ex-prop} and \secref{sec:framework-ex-quant}
- can now be summarized as follows, using the native Isar statement
- format of \secref{sec:framework-stmt}.
+ \secref{sec:framework-ex-prop} and \secref{sec:framework-ex-quant} can now
+ be summarized as follows, using the native Isar statement format of
+ \secref{sec:framework-stmt}.
\<^medskip>
\begin{tabular}{l}
- \<open>impI: \<ASSUMES> A \<Longrightarrow> B \<SHOWS> A \<longrightarrow> B\<close> \\
- \<open>impD: \<ASSUMES> A \<longrightarrow> B \<AND> A \<SHOWS> B\<close> \\[1ex]
+ \<^theory_text>\<open>impI: assumes "A \<Longrightarrow> B" shows "A \<longrightarrow> B"\<close> \\
+ \<^theory_text>\<open>impD: assumes "A \<longrightarrow> B" and A shows B\<close> \\[1ex]
- \<open>disjI\<^sub>1: \<ASSUMES> A \<SHOWS> A \<or> B\<close> \\
- \<open>disjI\<^sub>2: \<ASSUMES> B \<SHOWS> A \<or> B\<close> \\
- \<open>disjE: \<ASSUMES> A \<or> B \<OBTAINS> A \<BBAR> B\<close> \\[1ex]
+ \<^theory_text>\<open>disjI\<^sub>1: assumes A shows "A \<or> B"\<close> \\
+ \<^theory_text>\<open>disjI\<^sub>2: assumes B shows "A \<or> B"\<close> \\
+ \<^theory_text>\<open>disjE: assumes "A \<or> B" obtains A \<BBAR> B\<close> \\[1ex]
- \<open>conjI: \<ASSUMES> A \<AND> B \<SHOWS> A \<and> B\<close> \\
- \<open>conjE: \<ASSUMES> A \<and> B \<OBTAINS> A \<AND> B\<close> \\[1ex]
+ \<^theory_text>\<open>conjI: assumes A and B shows A \<and> B\<close> \\
+ \<^theory_text>\<open>conjE: assumes "A \<and> B" obtains A and B\<close> \\[1ex]
- \<open>falseE: \<ASSUMES> \<bottom> \<SHOWS> A\<close> \\
- \<open>trueI: \<SHOWS> \<top>\<close> \\[1ex]
+ \<^theory_text>\<open>falseE: assumes \<bottom> shows A\<close> \\
+ \<^theory_text>\<open>trueI: shows \<top>\<close> \\[1ex]
- \<open>notI: \<ASSUMES> A \<Longrightarrow> \<bottom> \<SHOWS> \<not> A\<close> \\
- \<open>notE: \<ASSUMES> \<not> A \<AND> A \<SHOWS> B\<close> \\[1ex]
+ \<^theory_text>\<open>notI: assumes "A \<Longrightarrow> \<bottom>" shows "\<not> A"\<close> \\
+ \<^theory_text>\<open>notE: assumes "\<not> A" and A shows B\<close> \\[1ex]
- \<open>allI: \<ASSUMES> \<And>x. B x \<SHOWS> \<forall>x. B x\<close> \\
- \<open>allE: \<ASSUMES> \<forall>x. B x \<SHOWS> B a\<close> \\[1ex]
+ \<^theory_text>\<open>allI: assumes "\<And>x. B x" shows "\<forall>x. B x"\<close> \\
+ \<^theory_text>\<open>allE: assumes "\<forall>x. B x" shows "B a"\<close> \\[1ex]
- \<open>exI: \<ASSUMES> B a \<SHOWS> \<exists>x. B x\<close> \\
- \<open>exE: \<ASSUMES> \<exists>x. B x \<OBTAINS> a \<WHERE> B a\<close>
+ \<^theory_text>\<open>exI: assumes "B a" shows "\<exists>x. B x"\<close> \\
+ \<^theory_text>\<open>exE: assumes "\<exists>x. B x" obtains a where "B a"\<close>
\end{tabular}
\<^medskip>
- This essentially provides a declarative reading of Pure
- rules as Isar reasoning patterns: the rule statements tells how a
- canonical proof outline shall look like. Since the above rules have
- already been declared as @{attribute (Pure) intro}, @{attribute
- (Pure) elim}, @{attribute (Pure) dest} --- each according to its
- particular shape --- we can immediately write Isar proof texts as
- follows:
+ This essentially provides a declarative reading of Pure rules as Isar
+ reasoning patterns: the rule statements tells how a canonical proof outline
+ shall look like. Since the above rules have already been declared as
+ @{attribute (Pure) intro}, @{attribute (Pure) elim}, @{attribute (Pure)
+ dest} --- each according to its particular shape --- we can immediately
+ write Isar proof texts as follows:
\<close>
(*<*)
@@ -418,47 +397,47 @@
have "A \<longrightarrow> B"
proof
assume A
- show B sorry %noproof
+ show B \<proof>
qed
text_raw \<open>\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*)
- have "A \<longrightarrow> B" and A sorry %noproof
+ have "A \<longrightarrow> B" and A \<proof>
then have B ..
text_raw \<open>\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*)
- have A sorry %noproof
+ have A \<proof>
then have "A \<or> B" ..
- have B sorry %noproof
+ have B \<proof>
then have "A \<or> B" ..
text_raw \<open>\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*)
- have "A \<or> B" sorry %noproof
+ have "A \<or> B" \<proof>
then have C
proof
assume A
- then show C sorry %noproof
+ then show C \<proof>
next
assume B
- then show C sorry %noproof
+ then show C \<proof>
qed
text_raw \<open>\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*)
- have A and B sorry %noproof
+ have A and B \<proof>
then have "A \<and> B" ..
text_raw \<open>\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*)
- have "A \<and> B" sorry %noproof
+ have "A \<and> B" \<proof>
then obtain A and B ..
text_raw \<open>\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*)
- have "\<bottom>" sorry %noproof
+ have "\<bottom>" \<proof>
then have A ..
text_raw \<open>\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*)
@@ -470,12 +449,12 @@
have "\<not> A"
proof
assume A
- then show "\<bottom>" sorry %noproof
+ then show "\<bottom>" \<proof>
qed
text_raw \<open>\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*)
- have "\<not> A" and A sorry %noproof
+ have "\<not> A" and A \<proof>
then have B ..
text_raw \<open>\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*)
@@ -483,24 +462,24 @@
have "\<forall>x. B x"
proof
fix x
- show "B x" sorry %noproof
+ show "B x" \<proof>
qed
text_raw \<open>\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*)
- have "\<forall>x. B x" sorry %noproof
+ have "\<forall>x. B x" \<proof>
then have "B a" ..
text_raw \<open>\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*)
have "\<exists>x. B x"
proof
- show "B a" sorry %noproof
+ show "B a" \<proof>
qed
text_raw \<open>\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*)
- have "\<exists>x. B x" sorry %noproof
+ have "\<exists>x. B x" \<proof>
then obtain a where "B a" ..
text_raw \<open>\end{minipage}\<close>
@@ -511,11 +490,10 @@
text \<open>
\<^bigskip>
- Of course, these proofs are merely examples. As
- sketched in \secref{sec:framework-subproof}, there is a fair amount
- of flexibility in expressing Pure deductions in Isar. Here the user
- is asked to express himself adequately, aiming at proof texts of
- literary quality.
+ Of course, these proofs are merely examples. As sketched in
+ \secref{sec:framework-subproof}, there is a fair amount of flexibility in
+ expressing Pure deductions in Isar. Here the user is asked to express
+ himself adequately, aiming at proof texts of literary quality.
\<close>
end %visible
--- a/src/Doc/Isar_Ref/Framework.thy Wed Feb 10 15:49:05 2016 +0100
+++ b/src/Doc/Isar_Ref/Framework.thy Fri Feb 12 22:36:48 2016 +0100
@@ -8,75 +8,115 @@
text \<open>
Isabelle/Isar @{cite "Wenzel:1999:TPHOL" and "Wenzel-PhD" and
- "Nipkow-TYPES02" and "Wenzel-Paulson:2006" and "Wenzel:2006:Festschrift"}
- is intended as a generic framework for developing formal
- mathematical documents with full proof checking. Definitions and
- proofs are organized as theories. An assembly of theory sources may
- be presented as a printed document; see also
- \chref{ch:document-prep}.
+ "Nipkow-TYPES02" and "Wiedijk:1999:Mizar" and "Wenzel-Paulson:2006" and
+ "Wenzel:2006:Festschrift"} is a generic framework for developing formal
+ mathematical documents with full proof checking. Definitions, statements and
+ proofs are organized as theories. A collection of theories sources may be
+ presented as a printed document; see also \chref{ch:document-prep}.
+
+ The main concern of Isar is the design of a human-readable structured proof
+ language, which is called the ``primary proof format'' in Isar terminology.
+ Such a primary proof language is somewhere in the middle between the
+ extremes of primitive proof objects and actual natural language.
- The main objective of Isar is the design of a human-readable
- structured proof language, which is called the ``primary proof
- format'' in Isar terminology. Such a primary proof language is
- somewhere in the middle between the extremes of primitive proof
- objects and actual natural language. In this respect, Isar is a bit
- more formalistic than Mizar @{cite "Trybulec:1993:MizarFeatures" and
- "Rudnicki:1992:MizarOverview" and "Wiedijk:1999:Mizar"},
- using logical symbols for certain reasoning schemes where Mizar
- would prefer English words; see @{cite "Wenzel-Wiedijk:2002"} for
- further comparisons of these systems.
+ Thus Isar challenges the traditional way of recording informal proofs in
+ mathematical prose, as well as the common tendency to see fully formal
+ proofs directly as objects of some logical calculus (e.g.\ \<open>\<lambda>\<close>-terms in a
+ version of type theory). Technically, Isar is an interpreter of a simple
+ block-structured language for describing the data flow of local facts and
+ goals, interspersed with occasional invocations of proof methods. Everything
+ is reduced to logical inferences internally, but these steps are somewhat
+ marginal compared to the overall bookkeeping of the interpretation process.
+ Thanks to careful design of the syntax and semantics of Isar language
+ elements, a formal record of Isar commands may later appear as an
+ intelligible text to the human reader.
+
+ The Isar proof language has emerged from careful analysis of some inherent
+ virtues of the logical framework Isabelle/Pure @{cite "paulson-found" and
+ "paulson700"}, notably composition of higher-order natural deduction rules,
+ which is a generalization of Gentzen's original calculus @{cite
+ "Gentzen:1935"}. The approach of generic inference systems in Pure is
+ continued by Isar towards actual proof texts. See also
+ \figref{fig:natural-deduction}
+
+ \begin{figure}[htb]
+
+ \begin{center}
+ \begin{minipage}[t]{0.9\textwidth}
- So Isar challenges the traditional way of recording informal proofs
- in mathematical prose, as well as the common tendency to see fully
- formal proofs directly as objects of some logical calculus (e.g.\
- \<open>\<lambda>\<close>-terms in a version of type theory). In fact, Isar is
- better understood as an interpreter of a simple block-structured
- language for describing the data flow of local facts and goals,
- interspersed with occasional invocations of proof methods.
- Everything is reduced to logical inferences internally, but these
- steps are somewhat marginal compared to the overall bookkeeping of
- the interpretation process. Thanks to careful design of the syntax
- and semantics of Isar language elements, a formal record of Isar
- instructions may later appear as an intelligible text to the
- attentive reader.
+ \textbf{Inferences:}
+ \begin{center}
+ \begin{tabular}{l@ {\qquad}l}
+ \infer{\<open>B\<close>}{\<open>A \<longrightarrow> B\<close> & \<open>A\<close>} &
+ \infer{\<open>A \<longrightarrow> B\<close>}{\infer*{\<open>B\<close>}{\<open>[A]\<close>}} \\
+ \end{tabular}
+ \end{center}
+
+ \textbf{Isabelle/Pure:}
+ \begin{center}
+ \begin{tabular}{l@ {\qquad}l}
+ \<open>(A \<longrightarrow> B) \<Longrightarrow> A \<Longrightarrow> B\<close> &
+ \<open>(A \<Longrightarrow> B) \<Longrightarrow> A \<longrightarrow> B\<close>
+ \end{tabular}
+ \end{center}
- The Isar proof language has emerged from careful analysis of some
- inherent virtues of the existing logical framework of Isabelle/Pure
- @{cite "paulson-found" and "paulson700"}, notably composition of higher-order
- natural deduction rules, which is a generalization of Gentzen's
- original calculus @{cite "Gentzen:1935"}. The approach of generic
- inference systems in Pure is continued by Isar towards actual proof
- texts.
+ \textbf{Isabelle/Isar:}
+ \begin{center}
+ \begin{minipage}[t]{0.4\textwidth}
+ @{theory_text [display, indent = 2]
+ \<open>have "A \<longrightarrow> B" \<proof>
+also have A \<proof>
+finally have B .\<close>}
+ \end{minipage}
+ \begin{minipage}[t]{0.4\textwidth}
+ @{theory_text [display, indent = 2]
+ \<open>have "A \<longrightarrow> B"
+proof
+ assume A
+ then show B \<proof>
+qed\<close>}
+ \end{minipage}
+ \end{center}
- Concrete applications require another intermediate layer: an
- object-logic. Isabelle/HOL @{cite "isa-tutorial"} (simply-typed
- set-theory) is being used most of the time; Isabelle/ZF
- @{cite "isabelle-ZF"} is less extensively developed, although it would
- probably fit better for classical mathematics.
+ \end{minipage}
+ \end{center}
+
+ \caption{Natural Deduction via inferences according to Gentzen, rules in
+ Isabelle/Pure, and proofs in Isabelle/Isar}\label{fig:natural-deduction}
+
+ \end{figure}
\<^medskip>
- In order to illustrate natural deduction in Isar, we shall
- refer to the background theory and library of Isabelle/HOL. This
- includes common notions of predicate logic, naive set-theory etc.\
- using fairly standard mathematical notation. From the perspective
- of generic natural deduction there is nothing special about the
- logical connectives of HOL (\<open>\<and>\<close>, \<open>\<or>\<close>, \<open>\<forall>\<close>,
- \<open>\<exists>\<close>, etc.), only the resulting reasoning principles are
- relevant to the user. There are similar rules available for
- set-theory operators (\<open>\<inter>\<close>, \<open>\<union>\<close>, \<open>\<Inter>\<close>, \<open>\<Union>\<close>, etc.), or any other theory developed in the library (lattice
- theory, topology etc.).
+ Concrete applications require another intermediate layer: an object-logic.
+ Isabelle/HOL @{cite "isa-tutorial"} (simply-typed set-theory) is most
+ commonly used; elementary examples are given in the directory @{file
+ "~~/src/HOL/Isar_Examples"}. Some examples demonstrate how to start a fresh
+ object-logic from Isabelle/Pure, and use Isar proofs from the very start,
+ despite the lack of advanced proof tools at such an early stage (e.g.\ see
+ @{file "~~/src/HOL/Isar_Examples/Higher_Order_Logic.thy"}). Isabelle/FOL
+ @{cite "isabelle-logics"} and Isabelle/ZF @{cite "isabelle-ZF"} also work,
+ but are much less developed.
- Subsequently we briefly review fragments of Isar proof texts
- corresponding directly to such general deduction schemes. The
- examples shall refer to set-theory, to minimize the danger of
- understanding connectives of predicate logic as something special.
+ In order to illustrate natural deduction in Isar, we shall subsequently
+ refer to the background theory and library of Isabelle/HOL. This includes
+ common notions of predicate logic, naive set-theory etc.\ using fairly
+ standard mathematical notation. From the perspective of generic natural
+ deduction there is nothing special about the logical connectives of HOL
+ (\<open>\<and>\<close>, \<open>\<or>\<close>, \<open>\<forall>\<close>, \<open>\<exists>\<close>, etc.), only the resulting reasoning principles are
+ relevant to the user. There are similar rules available for set-theory
+ operators (\<open>\<inter>\<close>, \<open>\<union>\<close>, \<open>\<Inter>\<close>, \<open>\<Union>\<close>, etc.), or any other theory developed in the
+ library (lattice theory, topology etc.).
+
+ Subsequently we briefly review fragments of Isar proof texts corresponding
+ directly to such general deduction schemes. The examples shall refer to
+ set-theory, to minimize the danger of understanding connectives of predicate
+ logic as something special.
\<^medskip>
- The following deduction performs \<open>\<inter>\<close>-introduction,
- working forwards from assumptions towards the conclusion. We give
- both the Isar text, and depict the primitive rule involved, as
- determined by unification of the problem against rules that are
- declared in the library context.
+ The following deduction performs \<open>\<inter>\<close>-introduction, working forwards from
+ assumptions towards the conclusion. We give both the Isar text, and depict
+ the primitive rule involved, as determined by unification of fact and goal
+ statements against rules that are declared in the library context.
\<close>
text_raw \<open>\medskip\begin{minipage}{0.6\textwidth}\<close>
@@ -84,6 +124,7 @@
(*<*)
notepad
begin
+ fix x :: 'a and A B
(*>*)
assume "x \<in> A" and "x \<in> B"
then have "x \<in> A \<inter> B" ..
@@ -94,25 +135,25 @@
text_raw \<open>\end{minipage}\begin{minipage}{0.4\textwidth}\<close>
text \<open>
- \infer{@{prop "x \<in> A \<inter> B"}}{@{prop "x \<in> A"} & @{prop "x \<in> B"}}
+ \infer{\<open>x \<in> A \<inter> B\<close>}{\<open>x \<in> A\<close> & \<open>x \<in> B\<close>}
\<close>
text_raw \<open>\end{minipage}\<close>
text \<open>
\<^medskip>
- Note that @{command assume} augments the proof
- context, @{command then} indicates that the current fact shall be
- used in the next step, and @{command have} states an intermediate
- goal. The two dots ``@{command ".."}'' refer to a complete proof of
- this claim, using the indicated facts and a canonical rule from the
- context. We could have been more explicit here by spelling out the
- final proof step via the @{command "by"} command:
+ Note that \<^theory_text>\<open>assume\<close> augments the proof context, \<^theory_text>\<open>then\<close> indicates that the
+ current fact shall be used in the next step, and \<^theory_text>\<open>have\<close> states an
+ intermediate goal. The two dots ``\<^theory_text>\<open>..\<close>'' refer to a complete proof of this
+ claim, using the indicated facts and a canonical rule from the context. We
+ could have been more explicit here by spelling out the final proof step via
+ the \<^theory_text>\<open>by\<close> command:
\<close>
(*<*)
notepad
begin
+ fix x :: 'a and A B
(*>*)
assume "x \<in> A" and "x \<in> B"
then have "x \<in> A \<inter> B" by (rule IntI)
@@ -121,14 +162,14 @@
(*>*)
text \<open>
- The format of the \<open>\<inter>\<close>-introduction rule represents
- the most basic inference, which proceeds from given premises to a
- conclusion, without any nested proof context involved.
+ The format of the \<open>\<inter>\<close>-introduction rule represents the most basic inference,
+ which proceeds from given premises to a conclusion, without any nested proof
+ context involved.
- The next example performs backwards introduction on @{term "\<Inter>\<A>"},
- the intersection of all sets within a given set. This requires a
- nested proof of set membership within a local context, where @{term
- A} is an arbitrary-but-fixed member of the collection:
+ The next example performs backwards introduction of \<open>\<Inter>\<A>\<close>, the intersection
+ of all sets within a given set. This requires a nested proof of set
+ membership within a local context, where \<open>A\<close> is an arbitrary-but-fixed
+ member of the collection:
\<close>
text_raw \<open>\medskip\begin{minipage}{0.6\textwidth}\<close>
@@ -136,12 +177,13 @@
(*<*)
notepad
begin
+ fix x :: 'a and \<A>
(*>*)
have "x \<in> \<Inter>\<A>"
proof
fix A
assume "A \<in> \<A>"
- show "x \<in> A" sorry %noproof
+ show "x \<in> A" \<proof>
qed
(*<*)
end
@@ -150,35 +192,30 @@
text_raw \<open>\end{minipage}\begin{minipage}{0.4\textwidth}\<close>
text \<open>
- \infer{@{prop "x \<in> \<Inter>\<A>"}}{\infer*{@{prop "x \<in> A"}}{\<open>[A][A \<in> \<A>]\<close>}}
+ \infer{\<open>x \<in> \<Inter>\<A>\<close>}{\infer*{\<open>x \<in> A\<close>}{\<open>[A][A \<in> \<A>]\<close>}}
\<close>
text_raw \<open>\end{minipage}\<close>
text \<open>
\<^medskip>
- This Isar reasoning pattern again refers to the
- primitive rule depicted above. The system determines it in the
- ``@{command proof}'' step, which could have been spelled out more
- explicitly as ``@{command proof}~\<open>(rule InterI)\<close>''. Note
- that the rule involves both a local parameter @{term "A"} and an
- assumption @{prop "A \<in> \<A>"} in the nested reasoning. This kind of
- compound rule typically demands a genuine sub-proof in Isar, working
- backwards rather than forwards as seen before. In the proof body we
- encounter the @{command fix}-@{command assume}-@{command show}
- outline of nested sub-proofs that is typical for Isar. The final
- @{command show} is like @{command have} followed by an additional
- refinement of the enclosing claim, using the rule derived from the
- proof body.
+ This Isar reasoning pattern again refers to the primitive rule depicted
+ above. The system determines it in the ``\<^theory_text>\<open>proof\<close>'' step, which could have
+ been spelled out more explicitly as ``\<^theory_text>\<open>proof (rule InterI)\<close>''. Note that
+ the rule involves both a local parameter \<open>A\<close> and an assumption \<open>A \<in> \<A>\<close> in
+ the nested reasoning. Such compound rules typically demands a genuine
+ subproof in Isar, working backwards rather than forwards as seen before. In
+ the proof body we encounter the \<^theory_text>\<open>fix\<close>-\<^theory_text>\<open>assume\<close>-\<^theory_text>\<open>show\<close> outline of nested
+ subproofs that is typical for Isar. The final \<^theory_text>\<open>show\<close> is like \<^theory_text>\<open>have\<close>
+ followed by an additional refinement of the enclosing claim, using the rule
+ derived from the proof body.
\<^medskip>
- The next example involves @{term "\<Union>\<A>"}, which can be
- characterized as the set of all @{term "x"} such that @{prop "\<exists>A. x
- \<in> A \<and> A \<in> \<A>"}. The elimination rule for @{prop "x \<in> \<Union>\<A>"} does
- not mention \<open>\<exists>\<close> and \<open>\<and>\<close> at all, but admits to obtain
- directly a local @{term "A"} such that @{prop "x \<in> A"} and @{prop "A
- \<in> \<A>"} hold. This corresponds to the following Isar proof and
- inference rule, respectively:
+ The next example involves \<open>\<Union>\<A>\<close>, which can be characterized as the set of
+ all \<open>x\<close> such that \<open>\<exists>A. x \<in> A \<and> A \<in> \<A>\<close>. The elimination rule for \<open>x \<in> \<Union>\<A>\<close>
+ does not mention \<open>\<exists>\<close> and \<open>\<and>\<close> at all, but admits to obtain directly a local
+ \<open>A\<close> such that \<open>x \<in> A\<close> and \<open>A \<in> \<A>\<close> hold. This corresponds to the following
+ Isar proof and inference rule, respectively:
\<close>
text_raw \<open>\medskip\begin{minipage}{0.6\textwidth}\<close>
@@ -186,13 +223,14 @@
(*<*)
notepad
begin
+ fix x :: 'a and \<A> C
(*>*)
assume "x \<in> \<Union>\<A>"
then have C
proof
fix A
assume "x \<in> A" and "A \<in> \<A>"
- show C sorry %noproof
+ show C \<proof>
qed
(*<*)
end
@@ -201,26 +239,25 @@
text_raw \<open>\end{minipage}\begin{minipage}{0.4\textwidth}\<close>
text \<open>
- \infer{@{prop "C"}}{@{prop "x \<in> \<Union>\<A>"} & \infer*{@{prop "C"}~}{\<open>[A][x \<in> A, A \<in> \<A>]\<close>}}
+ \infer{\<open>C\<close>}{\<open>x \<in> \<Union>\<A>\<close> & \infer*{\<open>C\<close>~}{\<open>[A][x \<in> A, A \<in> \<A>]\<close>}}
\<close>
text_raw \<open>\end{minipage}\<close>
text \<open>
\<^medskip>
- Although the Isar proof follows the natural
- deduction rule closely, the text reads not as natural as
- anticipated. There is a double occurrence of an arbitrary
- conclusion @{prop "C"}, which represents the final result, but is
- irrelevant for now. This issue arises for any elimination rule
- involving local parameters. Isar provides the derived language
- element @{command obtain}, which is able to perform the same
- elimination proof more conveniently:
+ Although the Isar proof follows the natural deduction rule closely, the text
+ reads not as natural as anticipated. There is a double occurrence of an
+ arbitrary conclusion \<open>C\<close>, which represents the final result, but is
+ irrelevant for now. This issue arises for any elimination rule involving
+ local parameters. Isar provides the derived language element \<^theory_text>\<open>obtain\<close>,
+ which is able to perform the same elimination proof more conveniently:
\<close>
(*<*)
notepad
begin
+ fix x :: 'a and \<A>
(*>*)
assume "x \<in> \<Union>\<A>"
then obtain A where "x \<in> A" and "A \<in> \<A>" ..
@@ -229,9 +266,9 @@
(*>*)
text \<open>
- Here we avoid to mention the final conclusion @{prop "C"}
- and return to plain forward reasoning. The rule involved in the
- ``@{command ".."}'' proof is the same as before.
+ Here we avoid to mention the final conclusion \<open>C\<close> and return to plain
+ forward reasoning. The rule involved in the ``\<^theory_text>\<open>..\<close>'' proof is the same as
+ before.
\<close>
@@ -239,9 +276,9 @@
text \<open>
The Pure logic @{cite "paulson-found" and "paulson700"} is an intuitionistic
- fragment of higher-order logic @{cite "church40"}. In type-theoretic
- parlance, there are three levels of \<open>\<lambda>\<close>-calculus with
- corresponding arrows \<open>\<Rightarrow>\<close>/\<open>\<And>\<close>/\<open>\<Longrightarrow>\<close>:
+ fragment of higher-order logic @{cite "church40"}. In type-theoretic
+ parlance, there are three levels of \<open>\<lambda>\<close>-calculus with corresponding arrows
+ \<open>\<Rightarrow>\<close>/\<open>\<And>\<close>/\<open>\<Longrightarrow>\<close>:
\<^medskip>
\begin{tabular}{ll}
@@ -251,39 +288,35 @@
\end{tabular}
\<^medskip>
- Here only the types of syntactic terms, and the
- propositions of proof terms have been shown. The \<open>\<lambda>\<close>-structure of proofs can be recorded as an optional feature of
- the Pure inference kernel @{cite "Berghofer-Nipkow:2000:TPHOL"}, but
- the formal system can never depend on them due to \<^emph>\<open>proof
- irrelevance\<close>.
+ Here only the types of syntactic terms, and the propositions of proof terms
+ have been shown. The \<open>\<lambda>\<close>-structure of proofs can be recorded as an optional
+ feature of the Pure inference kernel @{cite "Berghofer-Nipkow:2000:TPHOL"},
+ but the formal system can never depend on them due to \<^emph>\<open>proof irrelevance\<close>.
- On top of this most primitive layer of proofs, Pure implements a
- generic calculus for nested natural deduction rules, similar to
- @{cite "Schroeder-Heister:1984"}. Here object-logic inferences are
- internalized as formulae over \<open>\<And>\<close> and \<open>\<Longrightarrow>\<close>.
- Combining such rule statements may involve higher-order unification
- @{cite "paulson-natural"}.
+ On top of this most primitive layer of proofs, Pure implements a generic
+ calculus for nested natural deduction rules, similar to @{cite
+ "Schroeder-Heister:1984"}. Here object-logic inferences are internalized as
+ formulae over \<open>\<And>\<close> and \<open>\<Longrightarrow>\<close>. Combining such rule statements may involve
+ higher-order unification @{cite "paulson-natural"}.
\<close>
subsection \<open>Primitive inferences\<close>
text \<open>
- Term syntax provides explicit notation for abstraction \<open>\<lambda>x ::
- \<alpha>. b(x)\<close> and application \<open>b a\<close>, while types are usually
- implicit thanks to type-inference; terms of type \<open>prop\<close> are
- called propositions. Logical statements are composed via \<open>\<And>x
- :: \<alpha>. B(x)\<close> and \<open>A \<Longrightarrow> B\<close>. Primitive reasoning operates on
- judgments of the form \<open>\<Gamma> \<turnstile> \<phi>\<close>, with standard introduction
- and elimination rules for \<open>\<And>\<close> and \<open>\<Longrightarrow>\<close> that refer to
- fixed parameters \<open>x\<^sub>1, \<dots>, x\<^sub>m\<close> and hypotheses
- \<open>A\<^sub>1, \<dots>, A\<^sub>n\<close> from the context \<open>\<Gamma>\<close>;
- the corresponding proof terms are left implicit. The subsequent
- inference rules define \<open>\<Gamma> \<turnstile> \<phi>\<close> inductively, relative to a
- collection of axioms:
+ Term syntax provides explicit notation for abstraction \<open>\<lambda>x :: \<alpha>. b(x)\<close> and
+ application \<open>b a\<close>, while types are usually implicit thanks to
+ type-inference; terms of type \<open>prop\<close> are called propositions. Logical
+ statements are composed via \<open>\<And>x :: \<alpha>. B(x)\<close> and \<open>A \<Longrightarrow> B\<close>. Primitive reasoning
+ operates on judgments of the form \<open>\<Gamma> \<turnstile> \<phi>\<close>, with standard introduction and
+ elimination rules for \<open>\<And>\<close> and \<open>\<Longrightarrow>\<close> that refer to fixed parameters \<open>x\<^sub>1, \<dots>,
+ x\<^sub>m\<close> and hypotheses \<open>A\<^sub>1, \<dots>, A\<^sub>n\<close> from the context \<open>\<Gamma>\<close>; the corresponding
+ proof terms are left implicit. The subsequent inference rules define \<open>\<Gamma> \<turnstile> \<phi>\<close>
+ inductively, relative to a collection of axioms from the implicit background
+ theory:
\[
- \infer{\<open>\<turnstile> A\<close>}{(\<open>A\<close> \mbox{~axiom})}
+ \infer{\<open>\<turnstile> A\<close>}{\<open>A\<close> \mbox{~is axiom}}
\qquad
\infer{\<open>A \<turnstile> A\<close>}{}
\]
@@ -300,68 +333,61 @@
\infer{\<open>\<Gamma>\<^sub>1 \<union> \<Gamma>\<^sub>2 \<turnstile> B\<close>}{\<open>\<Gamma>\<^sub>1 \<turnstile> A \<Longrightarrow> B\<close> & \<open>\<Gamma>\<^sub>2 \<turnstile> A\<close>}
\]
- Furthermore, Pure provides a built-in equality \<open>\<equiv> :: \<alpha> \<Rightarrow> \<alpha> \<Rightarrow>
- prop\<close> with axioms for reflexivity, substitution, extensionality,
- and \<open>\<alpha>\<beta>\<eta>\<close>-conversion on \<open>\<lambda>\<close>-terms.
+ Furthermore, Pure provides a built-in equality \<open>\<equiv> :: \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> prop\<close> with
+ axioms for reflexivity, substitution, extensionality, and \<open>\<alpha>\<beta>\<eta>\<close>-conversion
+ on \<open>\<lambda>\<close>-terms.
\<^medskip>
- An object-logic introduces another layer on top of Pure,
- e.g.\ with types \<open>i\<close> for individuals and \<open>o\<close> for
- propositions, term constants \<open>Trueprop :: o \<Rightarrow> prop\<close> as
- (implicit) derivability judgment and connectives like \<open>\<and> :: o
- \<Rightarrow> o \<Rightarrow> o\<close> or \<open>\<forall> :: (i \<Rightarrow> o) \<Rightarrow> o\<close>, and axioms for object-level
- rules such as \<open>conjI: A \<Longrightarrow> B \<Longrightarrow> A \<and> B\<close> or \<open>allI: (\<And>x. B
- x) \<Longrightarrow> \<forall>x. B x\<close>. Derived object rules are represented as theorems of
- Pure. After the initial object-logic setup, further axiomatizations
- are usually avoided; plain definitions and derived principles are
- used exclusively.
+
+ An object-logic introduces another layer on top of Pure, e.g.\ with types
+ \<open>i\<close> for individuals and \<open>o\<close> for propositions, term constants \<open>Trueprop :: o
+ \<Rightarrow> prop\<close> as (implicit) derivability judgment and connectives like \<open>\<and> :: o \<Rightarrow> o
+ \<Rightarrow> o\<close> or \<open>\<forall> :: (i \<Rightarrow> o) \<Rightarrow> o\<close>, and axioms for object-level rules such as
+ \<open>conjI: A \<Longrightarrow> B \<Longrightarrow> A \<and> B\<close> or \<open>allI: (\<And>x. B x) \<Longrightarrow> \<forall>x. B x\<close>. Derived object rules
+ are represented as theorems of Pure. After the initial object-logic setup,
+ further axiomatizations are usually avoided: definitional principles are
+ used instead (e.g.\ \<^theory_text>\<open>definition\<close>, \<^theory_text>\<open>inductive\<close>, \<^theory_text>\<open>fun\<close>, \<^theory_text>\<open>function\<close>).
\<close>
subsection \<open>Reasoning with rules \label{sec:framework-resolution}\<close>
text \<open>
- Primitive inferences mostly serve foundational purposes. The main
- reasoning mechanisms of Pure operate on nested natural deduction
- rules expressed as formulae, using \<open>\<And>\<close> to bind local
- parameters and \<open>\<Longrightarrow>\<close> to express entailment. Multiple
- parameters and premises are represented by repeating these
+ Primitive inferences mostly serve foundational purposes. The main reasoning
+ mechanisms of Pure operate on nested natural deduction rules expressed as
+ formulae, using \<open>\<And>\<close> to bind local parameters and \<open>\<Longrightarrow>\<close> to express entailment.
+ Multiple parameters and premises are represented by repeating these
connectives in a right-associative manner.
- Since \<open>\<And>\<close> and \<open>\<Longrightarrow>\<close> commute thanks to the theorem
- @{prop "(A \<Longrightarrow> (\<And>x. B x)) \<equiv> (\<And>x. A \<Longrightarrow> B x)"}, we may assume w.l.o.g.\
- that rule statements always observe the normal form where
- quantifiers are pulled in front of implications at each level of
- nesting. This means that any Pure proposition may be presented as a
- \<^emph>\<open>Hereditary Harrop Formula\<close> @{cite "Miller:1991"} which is of the
- form \<open>\<And>x\<^sub>1 \<dots> x\<^sub>m. H\<^sub>1 \<Longrightarrow> \<dots> H\<^sub>n \<Longrightarrow>
- A\<close> for \<open>m, n \<ge> 0\<close>, and \<open>A\<close> atomic, and \<open>H\<^sub>1, \<dots>, H\<^sub>n\<close> being recursively of the same format.
- Following the convention that outermost quantifiers are implicit,
- Horn clauses \<open>A\<^sub>1 \<Longrightarrow> \<dots> A\<^sub>n \<Longrightarrow> A\<close> are a special
- case of this.
+ Thanks to the Pure theorem @{prop "(A \<Longrightarrow> (\<And>x. B x)) \<equiv> (\<And>x. A \<Longrightarrow> B x)"} the
+ connectives \<open>\<And>\<close> and \<open>\<Longrightarrow>\<close> commute. So we may assume w.l.o.g.\ that rule
+ statements always observe the normal form where quantifiers are pulled in
+ front of implications at each level of nesting. This means that any Pure
+ proposition may be presented as a \<^emph>\<open>Hereditary Harrop Formula\<close> @{cite
+ "Miller:1991"} which is of the form \<open>\<And>x\<^sub>1 \<dots> x\<^sub>m. H\<^sub>1 \<Longrightarrow> \<dots> H\<^sub>n \<Longrightarrow> A\<close> for \<open>m, n
+ \<ge> 0\<close>, and \<open>A\<close> atomic, and \<open>H\<^sub>1, \<dots>, H\<^sub>n\<close> being recursively of the same
+ format. Following the convention that outermost quantifiers are implicit,
+ Horn clauses \<open>A\<^sub>1 \<Longrightarrow> \<dots> A\<^sub>n \<Longrightarrow> A\<close> are a special case of this.
- For example, \<open>\<inter>\<close>-introduction rule encountered before is
- represented as a Pure theorem as follows:
+ For example, the \<open>\<inter>\<close>-introduction rule encountered before is represented as
+ a Pure theorem as follows:
\[
\<open>IntI:\<close>~@{prop "x \<in> A \<Longrightarrow> x \<in> B \<Longrightarrow> x \<in> A \<inter> B"}
\]
- This is a plain Horn clause, since no further nesting on
- the left is involved. The general \<open>\<Inter>\<close>-introduction
- corresponds to a Hereditary Harrop Formula with one additional level
- of nesting:
+ This is a plain Horn clause, since no further nesting on the left is
+ involved. The general \<open>\<Inter>\<close>-introduction corresponds to a Hereditary Harrop
+ Formula with one additional level of nesting:
\[
\<open>InterI:\<close>~@{prop "(\<And>A. A \<in> \<A> \<Longrightarrow> x \<in> A) \<Longrightarrow> x \<in> \<Inter>\<A>"}
\]
\<^medskip>
- Goals are also represented as rules: \<open>A\<^sub>1 \<Longrightarrow>
- \<dots> A\<^sub>n \<Longrightarrow> C\<close> states that the sub-goals \<open>A\<^sub>1, \<dots>,
- A\<^sub>n\<close> entail the result \<open>C\<close>; for \<open>n = 0\<close> the
- goal is finished. To allow \<open>C\<close> being a rule statement
- itself, we introduce the protective marker \<open># :: prop \<Rightarrow>
- prop\<close>, which is defined as identity and hidden from the user. We
- initialize and finish goal states as follows:
+ Goals are also represented as rules: \<open>A\<^sub>1 \<Longrightarrow> \<dots> A\<^sub>n \<Longrightarrow> C\<close> states that the
+ subgoals \<open>A\<^sub>1, \<dots>, A\<^sub>n\<close> entail the result \<open>C\<close>; for \<open>n = 0\<close> the goal is
+ finished. To allow \<open>C\<close> being a rule statement itself, there is an internal
+ protective marker \<open># :: prop \<Rightarrow> prop\<close>, which is defined as identity and
+ hidden from the user. We initialize and finish goal states as follows:
\[
\begin{array}{c@ {\qquad}c}
@@ -370,12 +396,12 @@
\end{array}
\]
- Goal states are refined in intermediate proof steps until
- a finished form is achieved. Here the two main reasoning principles
- are @{inference resolution}, for back-chaining a rule against a
- sub-goal (replacing it by zero or more sub-goals), and @{inference
- assumption}, for solving a sub-goal (finding a short-circuit with
- local assumptions). Below \<open>\<^vec>x\<close> stands for \<open>x\<^sub>1, \<dots>, x\<^sub>n\<close> (\<open>n \<ge> 0\<close>).
+ Goal states are refined in intermediate proof steps until a finished form is
+ achieved. Here the two main reasoning principles are @{inference
+ resolution}, for back-chaining a rule against a subgoal (replacing it by
+ zero or more subgoals), and @{inference assumption}, for solving a subgoal
+ (finding a short-circuit with local assumptions). Below \<open>\<^vec>x\<close> stands
+ for \<open>x\<^sub>1, \<dots>, x\<^sub>n\<close> (for \<open>n \<ge> 0\<close>).
\[
\infer[(@{inference_def resolution})]
@@ -397,7 +423,7 @@
{\begin{tabular}{rl}
\<open>goal:\<close> &
\<open>(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> A \<^vec>x) \<Longrightarrow> C\<close> \\
- \<open>assm unifier:\<close> & \<open>A\<vartheta> = H\<^sub>i\<vartheta>\<close>~~\mbox{(for some~\<open>H\<^sub>i\<close>)} \\
+ \<open>assm unifier:\<close> & \<open>A\<vartheta> = H\<^sub>i\<vartheta>\<close>~~\mbox{for some~\<open>H\<^sub>i\<close>} \\
\end{tabular}}
\]
@@ -418,215 +444,166 @@
\<^medskip>
}
- Compositions of @{inference assumption} after @{inference
- resolution} occurs quite often, typically in elimination steps.
- Traditional Isabelle tactics accommodate this by a combined
- @{inference_def elim_resolution} principle. In contrast, Isar uses
- a slightly more refined combination, where the assumptions to be
- closed are marked explicitly, using again the protective marker
- \<open>#\<close>:
+ Compositions of @{inference assumption} after @{inference resolution} occurs
+ quite often, typically in elimination steps. Traditional Isabelle tactics
+ accommodate this by a combined @{inference_def elim_resolution} principle.
+ In contrast, Isar uses a combined refinement rule as follows:\footnote{For
+ simplicity and clarity, the presentation ignores \<^emph>\<open>weak premises\<close> as
+ introduced via \<^theory_text>\<open>presume\<close> or \<^theory_text>\<open>show \<dots> when\<close>.}
+ {\small
\[
\infer[(@{inference refinement})]
- {\<open>(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> \<^vec>G' (\<^vec>a \<^vec>x))\<vartheta> \<Longrightarrow> C\<vartheta>\<close>}
+ {\<open>C\<vartheta>\<close>}
{\begin{tabular}{rl}
- \<open>sub\<hyphen>proof:\<close> &
- \<open>\<^vec>G \<^vec>a \<Longrightarrow> B \<^vec>a\<close> \\
- \<open>goal:\<close> &
+ \<open>subgoal:\<close> &
\<open>(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> B' \<^vec>x) \<Longrightarrow> C\<close> \\
- \<open>goal unifier:\<close> &
+ \<open>subproof:\<close> &
+ \<open>\<^vec>G \<^vec>a \<Longrightarrow> B \<^vec>a\<close> \quad for schematic \<open>\<^vec>a\<close> \\
+ \<open>concl unifier:\<close> &
\<open>(\<lambda>\<^vec>x. B (\<^vec>a \<^vec>x))\<vartheta> = B'\<vartheta>\<close> \\
\<open>assm unifiers:\<close> &
- \<open>(\<lambda>\<^vec>x. G\<^sub>j (\<^vec>a \<^vec>x))\<vartheta> = #H\<^sub>i\<vartheta>\<close> \\
- & \quad (for each marked \<open>G\<^sub>j\<close> some \<open>#H\<^sub>i\<close>) \\
+ \<open>(\<lambda>\<^vec>x. G\<^sub>j (\<^vec>a \<^vec>x))\<vartheta> = H\<^sub>i\<vartheta>\<close> \quad for each \<open>G\<^sub>j\<close> some \<open>H\<^sub>i\<close> \\
\end{tabular}}
- \]
+ \]}
- Here the \<open>sub\<hyphen>proof\<close> rule stems from the
- main @{command fix}-@{command assume}-@{command show} outline of
- Isar (cf.\ \secref{sec:framework-subproof}): each assumption
- indicated in the text results in a marked premise \<open>G\<close> above.
- The marking enforces resolution against one of the sub-goal's
- premises. Consequently, @{command fix}-@{command assume}-@{command
- show} enables to fit the result of a sub-proof quite robustly into a
- pending sub-goal, while maintaining a good measure of flexibility.
+ Here the \<open>subproof\<close> rule stems from the main \<^theory_text>\<open>fix\<close>-\<^theory_text>\<open>assume\<close>-\<^theory_text>\<open>show\<close>
+ outline of Isar (cf.\ \secref{sec:framework-subproof}): each assumption
+ indicated in the text results in a marked premise \<open>G\<close> above. Consequently,
+ \<^theory_text>\<open>fix\<close>-\<^theory_text>\<open>assume\<close>-\<^theory_text>\<open>show\<close> enables to fit the result of a subproof quite
+ robustly into a pending subgoal, while maintaining a good measure of
+ flexibility: the subproof only needs to fit modulo unification, and its
+ assumptions may be a proper subset of the subgoal premises (see
+ \secref{sec:framework-subproof}).
\<close>
section \<open>The Isar proof language \label{sec:framework-isar}\<close>
text \<open>
- Structured proofs are presented as high-level expressions for
- composing entities of Pure (propositions, facts, and goals). The
- Isar proof language allows to organize reasoning within the
- underlying rule calculus of Pure, but Isar is not another logical
- calculus!
+ Structured proofs are presented as high-level expressions for composing
+ entities of Pure (propositions, facts, and goals). The Isar proof language
+ allows to organize reasoning within the underlying rule calculus of Pure,
+ but Isar is not another logical calculus. Isar merely imposes certain
+ structure and policies on Pure inferences.
+
+ Isar is intended as an exercise in minimalism. Approximately half of the
+ language is introduced as primitive, the rest defined as derived concepts.
+ The grammar in \appref{ap:main-grammar} describes the core language
+ (category \<open>proof\<close>), which is embedded into the main outer theory syntax via
+ elements that require a proof (e.g.\ \<^theory_text>\<open>theorem\<close>, \<^theory_text>\<open>lemma\<close>, \<^theory_text>\<open>function\<close>,
+ \<^theory_text>\<open>termination\<close>).
- Isar is an exercise in sound minimalism. Approximately half of the
- language is introduced as primitive, the rest defined as derived
- concepts. The following grammar describes the core language
- (category \<open>proof\<close>), which is embedded into theory
- specification elements such as @{command theorem}; see also
- \secref{sec:framework-stmt} for the separate category \<open>statement\<close>.
+ The syntax for terms and propositions is inherited from Pure (and the
+ object-logic). A \<open>pattern\<close> is a \<open>term\<close> with schematic variables, to be bound
+ by higher-order matching. Simultaneous propositions or facts may be
+ separated by the \<^theory_text>\<open>and\<close> keyword.
+
+ \<^medskip>
+ Facts may be referenced by name or proposition. For example, the result of
+ ``\<^theory_text>\<open>have a: A \<proof>\<close>'' becomes accessible both via the name \<open>a\<close> and the
+ literal proposition \<open>\<open>A\<close>\<close>. Moreover, fact expressions may involve attributes
+ that modify either the theorem or the background context. For example, the
+ expression ``\<open>a [OF b]\<close>'' refers to the composition of two facts according
+ to the @{inference resolution} inference of
+ \secref{sec:framework-resolution}, while ``\<open>a [intro]\<close>'' declares a fact as
+ introduction rule in the context.
+
+ The special fact called ``@{fact this}'' always refers to the last result,
+ as produced by \<^theory_text>\<open>note\<close>, \<^theory_text>\<open>assume\<close>, \<^theory_text>\<open>have\<close>, or \<^theory_text>\<open>show\<close>. Since \<^theory_text>\<open>note\<close> occurs
+ frequently together with \<^theory_text>\<open>then\<close>, there are some abbreviations:
\<^medskip>
\begin{tabular}{rcl}
- \<open>theory\<hyphen>stmt\<close> & = & @{command "theorem"}~\<open>statement proof |\<close>~~@{command "definition"}~\<open>\<dots> | \<dots>\<close> \\[1ex]
-
- \<open>proof\<close> & = & \<open>prfx\<^sup>*\<close>~@{command "proof"}~\<open>method\<^sup>? stmt\<^sup>*\<close>~@{command "qed"}~\<open>method\<^sup>?\<close> \\[1ex]
-
- \<open>prfx\<close> & = & @{command "using"}~\<open>facts\<close> \\
- & \<open>|\<close> & @{command "unfolding"}~\<open>facts\<close> \\
-
- \<open>stmt\<close> & = & @{command "{"}~\<open>stmt\<^sup>*\<close>~@{command "}"} \\
- & \<open>|\<close> & @{command "next"} \\
- & \<open>|\<close> & @{command "note"}~\<open>name = facts\<close> \\
- & \<open>|\<close> & @{command "let"}~\<open>term = term\<close> \\
- & \<open>|\<close> & @{command "fix"}~\<open>var\<^sup>+\<close> \\
- & \<open>|\<close> & @{command assume}~\<open>\<guillemotleft>inference\<guillemotright> name: props\<close> \\
- & \<open>|\<close> & @{command "then"}\<open>\<^sup>?\<close>~\<open>goal\<close> \\
- \<open>goal\<close> & = & @{command "have"}~\<open>name: props proof\<close> \\
- & \<open>|\<close> & @{command "show"}~\<open>name: props proof\<close> \\
- \end{tabular}
-
- \<^medskip>
- Simultaneous propositions or facts may be separated by the
- @{keyword "and"} keyword.
-
- \<^medskip>
- The syntax for terms and propositions is inherited from
- Pure (and the object-logic). A \<open>pattern\<close> is a \<open>term\<close> with schematic variables, to be bound by higher-order
- matching.
-
- \<^medskip>
- Facts may be referenced by name or proposition. For
- example, the result of ``@{command have}~\<open>a: A \<langle>proof\<rangle>\<close>''
- becomes available both as \<open>a\<close> and
- \isacharbackquoteopen\<open>A\<close>\isacharbackquoteclose. Moreover,
- fact expressions may involve attributes that modify either the
- theorem or the background context. For example, the expression
- ``\<open>a [OF b]\<close>'' refers to the composition of two facts
- according to the @{inference resolution} inference of
- \secref{sec:framework-resolution}, while ``\<open>a [intro]\<close>''
- declares a fact as introduction rule in the context.
-
- The special fact called ``@{fact this}'' always refers to the last
- result, as produced by @{command note}, @{command assume}, @{command
- have}, or @{command show}. Since @{command note} occurs
- frequently together with @{command then} we provide some
- abbreviations:
-
- \<^medskip>
- \begin{tabular}{rcl}
- @{command from}~\<open>a\<close> & \<open>\<equiv>\<close> & @{command note}~\<open>a\<close>~@{command then} \\
- @{command with}~\<open>a\<close> & \<open>\<equiv>\<close> & @{command from}~\<open>a \<AND> this\<close> \\
+ \<^theory_text>\<open>from a\<close> & \<open>\<equiv>\<close> & \<^theory_text>\<open>note a then\<close> \\
+ \<^theory_text>\<open>with a\<close> & \<open>\<equiv>\<close> & \<^theory_text>\<open>from a and this\<close> \\
\end{tabular}
\<^medskip>
- The \<open>method\<close> category is essentially a parameter and may be
- populated later. Methods use the facts indicated by @{command
- "then"} or @{command using}, and then operate on the goal state.
- Some basic methods are predefined: ``@{method "-"}'' leaves the goal
- unchanged, ``@{method this}'' applies the facts as rules to the
- goal, ``@{method (Pure) "rule"}'' applies the facts to another rule and the
- result to the goal (both ``@{method this}'' and ``@{method (Pure) rule}''
- refer to @{inference resolution} of
- \secref{sec:framework-resolution}). The secondary arguments to
- ``@{method (Pure) rule}'' may be specified explicitly as in ``\<open>(rule
- a)\<close>'', or picked from the context. In the latter case, the system
- first tries rules declared as @{attribute (Pure) elim} or
- @{attribute (Pure) dest}, followed by those declared as @{attribute
- (Pure) intro}.
+ The \<open>method\<close> category is essentially a parameter of the Isar language and
+ may be populated later. The command \<^theory_text>\<open>method_setup\<close> allows to define proof
+ methods semantically in Isabelle/ML. The Eisbach language allows to define
+ proof methods symbolically, as recursive expressions over existing methods
+ @{cite "Matichuk-et-al:2014"}; see also @{file "~~/src/HOL/Eisbach"}.
- The default method for @{command proof} is ``@{method standard}''
- (arguments picked from the context), for @{command qed} it is
- ``@{method "succeed"}''. Further abbreviations for terminal proof steps
- are ``@{command "by"}~\<open>method\<^sub>1 method\<^sub>2\<close>'' for
- ``@{command proof}~\<open>method\<^sub>1\<close>~@{command qed}~\<open>method\<^sub>2\<close>'', and ``@{command ".."}'' for ``@{command
- "by"}~@{method standard}, and ``@{command "."}'' for ``@{command
- "by"}~@{method this}''. The @{command unfolding} element operates
- directly on the current facts and goal by applying equalities.
+ Methods use the facts indicated by \<^theory_text>\<open>then\<close> or \<^theory_text>\<open>using\<close>, and then operate on
+ the goal state. Some basic methods are predefined in Pure: ``@{method "-"}''
+ leaves the goal unchanged, ``@{method this}'' applies the facts as rules to
+ the goal, ``@{method (Pure) "rule"}'' applies the facts to another rule and
+ the result to the goal (both ``@{method this}'' and ``@{method (Pure)
+ rule}'' refer to @{inference resolution} of
+ \secref{sec:framework-resolution}). The secondary arguments to ``@{method
+ (Pure) rule}'' may be specified explicitly as in ``\<open>(rule a)\<close>'', or picked
+ from the context. In the latter case, the system first tries rules declared
+ as @{attribute (Pure) elim} or @{attribute (Pure) dest}, followed by those
+ declared as @{attribute (Pure) intro}.
+
+ The default method for \<^theory_text>\<open>proof\<close> is ``@{method standard}'' (which subsumes
+ @{method rule} with arguments picked from the context), for \<^theory_text>\<open>qed\<close> it is
+ ``@{method "succeed"}''. Further abbreviations for terminal proof steps are
+ ``\<^theory_text>\<open>by method\<^sub>1 method\<^sub>2\<close>'' for ``\<^theory_text>\<open>proof method\<^sub>1 qed method\<^sub>2\<close>'', and
+ ``\<^theory_text>\<open>..\<close>'' for ``\<^theory_text>\<open>by standard\<close>, and ``\<^theory_text>\<open>.\<close>'' for ``\<^theory_text>\<open>by this\<close>''. The command
+ ``\<^theory_text>\<open>unfolding facts\<close>'' operates directly on the goal by applying equalities.
\<^medskip>
- Block structure can be indicated explicitly by ``@{command
- "{"}~\<open>\<dots>\<close>~@{command "}"}'', although the body of a sub-proof
- already involves implicit nesting. In any case, @{command next}
- jumps into the next section of a block, i.e.\ it acts like closing
- an implicit block scope and opening another one; there is no direct
- correspondence to subgoals here.
+ Block structure can be indicated explicitly by ``\<^theory_text>\<open>{ \<dots> }\<close>'', although the
+ body of a subproof ``\<^theory_text>\<open>proof \<dots> qed\<close>'' already provides implicit nesting. In
+ both situations, \<^theory_text>\<open>next\<close> jumps into the next section of a block, i.e.\ it
+ acts like closing an implicit block scope and opening another one. There is
+ no direct connection to subgoals here!
- The remaining elements @{command fix} and @{command assume} build up
- a local context (see \secref{sec:framework-context}), while
- @{command show} refines a pending sub-goal by the rule resulting
- from a nested sub-proof (see \secref{sec:framework-subproof}).
- Further derived concepts will support calculational reasoning (see
- \secref{sec:framework-calc}).
+ The commands \<^theory_text>\<open>fix\<close> and \<^theory_text>\<open>assume\<close> build up a local context (see
+ \secref{sec:framework-context}), while \<^theory_text>\<open>show\<close> refines a pending subgoal by
+ the rule resulting from a nested subproof (see
+ \secref{sec:framework-subproof}). Further derived concepts will support
+ calculational reasoning (see \secref{sec:framework-calc}).
\<close>
subsection \<open>Context elements \label{sec:framework-context}\<close>
text \<open>
- In judgments \<open>\<Gamma> \<turnstile> \<phi>\<close> of the primitive framework, \<open>\<Gamma>\<close>
- essentially acts like a proof context. Isar elaborates this idea
- towards a higher-level notion, with additional information for
- type-inference, term abbreviations, local facts, hypotheses etc.
+ In judgments \<open>\<Gamma> \<turnstile> \<phi>\<close> of the primitive framework, \<open>\<Gamma>\<close> essentially acts like a
+ proof context. Isar elaborates this idea towards a more advanced concept,
+ with additional information for type-inference, term abbreviations, local
+ facts, hypotheses etc.
- The element @{command fix}~\<open>x :: \<alpha>\<close> declares a local
- parameter, i.e.\ an arbitrary-but-fixed entity of a given type; in
- results exported from the context, \<open>x\<close> may become anything.
- The @{command assume}~\<open>\<guillemotleft>inference\<guillemotright>\<close> element provides a
- general interface to hypotheses: ``@{command assume}~\<open>\<guillemotleft>inference\<guillemotright> A\<close>'' produces \<open>A \<turnstile> A\<close> locally, while the
- included inference tells how to discharge \<open>A\<close> from results
- \<open>A \<turnstile> B\<close> later on. There is no user-syntax for \<open>\<guillemotleft>inference\<guillemotright>\<close>, i.e.\ it may only occur internally when derived
- commands are defined in ML.
+ The element \<^theory_text>\<open>fix x :: \<alpha>\<close> declares a local parameter, i.e.\ an
+ arbitrary-but-fixed entity of a given type; in results exported from the
+ context, \<open>x\<close> may become anything. The \<^theory_text>\<open>assume \<guillemotleft>inference\<guillemotright>\<close> element provides
+ a general interface to hypotheses: \<^theory_text>\<open>assume \<guillemotleft>inference\<guillemotright> A\<close> produces \<open>A \<turnstile> A\<close>
+ locally, while the included inference tells how to discharge \<open>A\<close> from
+ results \<open>A \<turnstile> B\<close> later on. There is no surface syntax for \<open>\<guillemotleft>inference\<guillemotright>\<close>,
+ i.e.\ it may only occur internally when derived commands are defined in ML.
- At the user-level, the default inference for @{command assume} is
- @{inference discharge} as given below. The additional variants
- @{command presume} and @{command def} are defined as follows:
-
- \<^medskip>
- \begin{tabular}{rcl}
- @{command presume}~\<open>A\<close> & \<open>\<equiv>\<close> & @{command assume}~\<open>\<guillemotleft>weak\<hyphen>discharge\<guillemotright> A\<close> \\
- @{command def}~\<open>x \<equiv> a\<close> & \<open>\<equiv>\<close> & @{command fix}~\<open>x\<close>~@{command assume}~\<open>\<guillemotleft>expansion\<guillemotright> x \<equiv> a\<close> \\
- \end{tabular}
- \<^medskip>
+ The default inference for \<^theory_text>\<open>assume\<close> is @{inference export} as given below.
+ The derived element \<^theory_text>\<open>def x \<equiv> a\<close> is defined as \<^theory_text>\<open>fix x assume \<guillemotleft>expand\<guillemotright> x \<equiv>
+ a\<close>, with the subsequent inference @{inference expand}.
\[
- \infer[(@{inference_def discharge})]{\<open>\<strut>\<Gamma> - A \<turnstile> #A \<Longrightarrow> B\<close>}{\<open>\<strut>\<Gamma> \<turnstile> B\<close>}
- \]
- \[
- \infer[(@{inference_def "weak\<hyphen>discharge"})]{\<open>\<strut>\<Gamma> - A \<turnstile> A \<Longrightarrow> B\<close>}{\<open>\<strut>\<Gamma> \<turnstile> B\<close>}
- \]
- \[
- \infer[(@{inference_def expansion})]{\<open>\<strut>\<Gamma> - (x \<equiv> a) \<turnstile> B a\<close>}{\<open>\<strut>\<Gamma> \<turnstile> B x\<close>}
+ \infer[(@{inference_def export})]{\<open>\<strut>\<Gamma> - A \<turnstile> A \<Longrightarrow> B\<close>}{\<open>\<strut>\<Gamma> \<turnstile> B\<close>}
+ \qquad
+ \infer[(@{inference_def expand})]{\<open>\<strut>\<Gamma> - (x \<equiv> a) \<turnstile> B a\<close>}{\<open>\<strut>\<Gamma> \<turnstile> B x\<close>}
\]
\<^medskip>
- Note that @{inference discharge} and @{inference
- "weak\<hyphen>discharge"} differ in the marker for @{prop A}, which is
- relevant when the result of a @{command fix}-@{command
- assume}-@{command show} outline is composed with a pending goal,
- cf.\ \secref{sec:framework-subproof}.
-
- The most interesting derived context element in Isar is @{command
- obtain} @{cite \<open>\S5.3\<close> "Wenzel-PhD"}, which supports generalized
- elimination steps in a purely forward manner. The @{command obtain}
- command takes a specification of parameters \<open>\<^vec>x\<close> and
- assumptions \<open>\<^vec>A\<close> to be added to the context, together
- with a proof of a case rule stating that this extension is
+ The most interesting derived context element in Isar is \<^theory_text>\<open>obtain\<close> @{cite
+ \<open>\S5.3\<close> "Wenzel-PhD"}, which supports generalized elimination steps in a
+ purely forward manner. The \<^theory_text>\<open>obtain\<close> command takes a specification of
+ parameters \<open>\<^vec>x\<close> and assumptions \<open>\<^vec>A\<close> to be added to the context,
+ together with a proof of a case rule stating that this extension is
conservative (i.e.\ may be removed from closed results later on):
\<^medskip>
\begin{tabular}{l}
- \<open>\<langle>facts\<rangle>\<close>~~@{command obtain}~\<open>\<^vec>x \<WHERE> \<^vec>A \<^vec>x \<langle>proof\<rangle> \<equiv>\<close> \\[0.5ex]
- \quad @{command have}~\<open>case: \<And>thesis. (\<And>\<^vec>x. \<^vec>A \<^vec>x \<Longrightarrow> thesis) \<Longrightarrow> thesis\<rangle>\<close> \\
- \quad @{command proof}~@{method "-"} \\
- \qquad @{command fix}~\<open>thesis\<close> \\
- \qquad @{command assume}~\<open>[intro]: \<And>\<^vec>x. \<^vec>A \<^vec>x \<Longrightarrow> thesis\<close> \\
- \qquad @{command show}~\<open>thesis\<close>~@{command using}~\<open>\<langle>facts\<rangle> \<langle>proof\<rangle>\<close> \\
- \quad @{command qed} \\
- \quad @{command fix}~\<open>\<^vec>x\<close>~@{command assume}~\<open>\<guillemotleft>elimination case\<guillemotright> \<^vec>A \<^vec>x\<close> \\
+ \<^theory_text>\<open>\<langle>facts\<rangle> obtain "\<^vec>x" where "\<^vec>A" "\<^vec>x" \<proof> \<equiv>\<close> \\[0.5ex]
+ \quad \<^theory_text>\<open>have "case": "\<And>thesis. (\<And>\<^vec>x. \<^vec>A \<^vec>x \<Longrightarrow> thesis) \<Longrightarrow> thesis"\<close> \\
+ \quad \<^theory_text>\<open>proof -\<close> \\
+ \qquad \<^theory_text>\<open>fix thesis\<close> \\
+ \qquad \<^theory_text>\<open>assume [intro]: "\<And>\<^vec>x. \<^vec>A \<^vec>x \<Longrightarrow> thesis"\<close> \\
+ \qquad \<^theory_text>\<open>show thesis using \<langle>facts\<rangle> \<proof>\<close> \\
+ \quad \<^theory_text>\<open>qed\<close> \\
+ \quad \<^theory_text>\<open>fix "\<^vec>x" assume \<guillemotleft>elimination "case"\<guillemotright> "\<^vec>A \<^vec>x"\<close> \\
\end{tabular}
\<^medskip>
@@ -640,21 +617,18 @@
\end{tabular}}
\]
- Here the name ``\<open>thesis\<close>'' is a specific convention
- for an arbitrary-but-fixed proposition; in the primitive natural
- deduction rules shown before we have occasionally used \<open>C\<close>.
- The whole statement of ``@{command obtain}~\<open>x\<close>~@{keyword
- "where"}~\<open>A x\<close>'' may be read as a claim that \<open>A x\<close>
- may be assumed for some arbitrary-but-fixed \<open>x\<close>. Also note
- that ``@{command obtain}~\<open>A \<AND> B\<close>'' without parameters
- is similar to ``@{command have}~\<open>A \<AND> B\<close>'', but the
- latter involves multiple sub-goals.
+ Here the name ``\<open>thesis\<close>'' is a specific convention for an
+ arbitrary-but-fixed proposition; in the primitive natural deduction rules
+ shown before we have occasionally used \<open>C\<close>. The whole statement of
+ ``\<^theory_text>\<open>obtain x where A x\<close>'' can be read as a claim that \<open>A x\<close> may be assumed
+ for some arbitrary-but-fixed \<open>x\<close>. Also note that ``\<^theory_text>\<open>obtain A and B\<close>''
+ without parameters is similar to ``\<^theory_text>\<open>have A and B\<close>'', but the latter
+ involves multiple subgoals that need to be proven separately.
\<^medskip>
- The subsequent Isar proof texts explain all context
- elements introduced above using the formal proof language itself.
- After finishing a local proof within a block, we indicate the
- exported result via @{command note}.
+ The subsequent Isar proof texts explain all context elements introduced
+ above using the formal proof language itself. After finishing a local proof
+ within a block, the exported result is indicated via \<^theory_text>\<open>note\<close>.
\<close>
(*<*)
@@ -664,25 +638,25 @@
text_raw \<open>\begin{minipage}[t]{0.45\textwidth}\<close>
{
fix x
- have "B x" sorry %noproof
+ have "B x" \<proof>
}
note \<open>\<And>x. B x\<close>
text_raw \<open>\end{minipage}\quad\begin{minipage}[t]{0.45\textwidth}\<close>(*<*)next(*>*)
{
assume A
- have B sorry %noproof
+ have B \<proof>
}
note \<open>A \<Longrightarrow> B\<close>
text_raw \<open>\end{minipage}\\[3ex]\begin{minipage}[t]{0.45\textwidth}\<close>(*<*)next(*>*)
{
def x \<equiv> a
- have "B x" sorry %noproof
+ have "B x" \<proof>
}
note \<open>B a\<close>
text_raw \<open>\end{minipage}\quad\begin{minipage}[t]{0.45\textwidth}\<close>(*<*)next(*>*)
{
- obtain x where "A x" sorry %noproof
- have B sorry %noproof
+ obtain x where "A x" \<proof>
+ have B \<proof>
}
note \<open>B\<close>
text_raw \<open>\end{minipage}\<close>
@@ -692,118 +666,110 @@
text \<open>
\<^bigskip>
- This illustrates the meaning of Isar context
- elements without goals getting in between.
+ This explains the meaning of Isar context elements without, without goal
+ states getting in the way.
\<close>
subsection \<open>Structured statements \label{sec:framework-stmt}\<close>
text \<open>
- The category \<open>statement\<close> of top-level theorem specifications
- is defined as follows:
+ The syntax of top-level theorem statements is defined as follows:
\<^medskip>
\begin{tabular}{rcl}
- \<open>statement\<close> & \<open>\<equiv>\<close> & \<open>name: props \<AND> \<dots>\<close> \\
+ \<open>statement\<close> & \<open>\<equiv>\<close> & \<^theory_text>\<open>name: props and \<dots>\<close> \\
& \<open>|\<close> & \<open>context\<^sup>* conclusion\<close> \\[0.5ex]
- \<open>context\<close> & \<open>\<equiv>\<close> & \<open>\<FIXES> vars \<AND> \<dots>\<close> \\
- & \<open>|\<close> & \<open>\<ASSUMES> name: props \<AND> \<dots>\<close> \\
+ \<open>context\<close> & \<open>\<equiv>\<close> & \<^theory_text>\<open>fixes vars and \<dots>\<close> \\
+ & \<open>|\<close> & \<^theory_text>\<open>assumes name: props and \<dots>\<close> \\
- \<open>conclusion\<close> & \<open>\<equiv>\<close> & \<open>\<SHOWS> name: props \<AND> \<dots>\<close> \\
- & \<open>|\<close> & \<open>\<OBTAINS> vars \<AND> \<dots> \<WHERE> name: props \<AND> \<dots>\<close> \\
+ \<open>conclusion\<close> & \<open>\<equiv>\<close> & \<^theory_text>\<open>shows name: props and \<dots>\<close> \\
+ & \<open>|\<close> & \<^theory_text>\<open>obtains vars and \<dots> where name: props and \<dots>\<close> \\
& & \quad \<open>\<BBAR> \<dots>\<close> \\
\end{tabular}
\<^medskip>
- A simple \<open>statement\<close> consists of named
- propositions. The full form admits local context elements followed
- by the actual conclusions, such as ``@{keyword "fixes"}~\<open>x\<close>~@{keyword "assumes"}~\<open>A x\<close>~@{keyword "shows"}~\<open>B
- x\<close>''. The final result emerges as a Pure rule after discharging
- the context: @{prop "\<And>x. A x \<Longrightarrow> B x"}.
+ A simple statement consists of named propositions. The full form admits
+ local context elements followed by the actual conclusions, such as ``\<^theory_text>\<open>fixes
+ x assumes A x shows B x\<close>''. The final result emerges as a Pure rule after
+ discharging the context: @{prop "\<And>x. A x \<Longrightarrow> B x"}.
- The @{keyword "obtains"} variant is another abbreviation defined
- below; unlike @{command obtain} (cf.\
- \secref{sec:framework-context}) there may be several ``cases''
- separated by ``\<open>\<BBAR>\<close>'', each consisting of several
- parameters (\<open>vars\<close>) and several premises (\<open>props\<close>).
- This specifies multi-branch elimination rules.
+ The \<^theory_text>\<open>obtains\<close> variant is another abbreviation defined below; unlike
+ \<^theory_text>\<open>obtain\<close> (cf.\ \secref{sec:framework-context}) there may be several
+ ``cases'' separated by ``\<open>\<BBAR>\<close>'', each consisting of several parameters
+ (\<open>vars\<close>) and several premises (\<open>props\<close>). This specifies multi-branch
+ elimination rules.
\<^medskip>
\begin{tabular}{l}
- \<open>\<OBTAINS> \<^vec>x \<WHERE> \<^vec>A \<^vec>x \<BBAR> \<dots> \<equiv>\<close> \\[0.5ex]
- \quad \<open>\<FIXES> thesis\<close> \\
- \quad \<open>\<ASSUMES> [intro]: \<And>\<^vec>x. \<^vec>A \<^vec>x \<Longrightarrow> thesis \<AND> \<dots>\<close> \\
- \quad \<open>\<SHOWS> thesis\<close> \\
+ \<^theory_text>\<open>obtains "\<^vec>x" where "\<^vec>A" "\<^vec>x" "\<BBAR>" \<dots> \<equiv>\<close> \\[0.5ex]
+ \quad \<^theory_text>\<open>fixes thesis\<close> \\
+ \quad \<^theory_text>\<open>assumes [intro]: "\<And>\<^vec>x. \<^vec>A \<^vec>x \<Longrightarrow> thesis" and \<dots>\<close> \\
+ \quad \<^theory_text>\<open>shows thesis\<close> \\
\end{tabular}
\<^medskip>
Presenting structured statements in such an ``open'' format usually
- simplifies the subsequent proof, because the outer structure of the
- problem is already laid out directly. E.g.\ consider the following
- canonical patterns for \<open>\<SHOWS>\<close> and \<open>\<OBTAINS>\<close>,
- respectively:
+ simplifies the subsequent proof, because the outer structure of the problem
+ is already laid out directly. E.g.\ consider the following canonical
+ patterns for \<^theory_text>\<open>shows\<close> and \<^theory_text>\<open>obtains\<close>, respectively:
\<close>
text_raw \<open>\begin{minipage}{0.5\textwidth}\<close>
-theorem
- fixes x and y
- assumes "A x" and "B y"
- shows "C x y"
-proof -
- from \<open>A x\<close> and \<open>B y\<close>
- show "C x y" sorry %noproof
-qed
+ theorem
+ fixes x and y
+ assumes "A x" and "B y"
+ shows "C x y"
+ proof -
+ from \<open>A x\<close> and \<open>B y\<close>
+ show "C x y" \<proof>
+ qed
text_raw \<open>\end{minipage}\begin{minipage}{0.5\textwidth}\<close>
-theorem
- obtains x and y
- where "A x" and "B y"
-proof -
- have "A a" and "B b" sorry %noproof
- then show thesis ..
-qed
+ theorem
+ obtains x and y
+ where "A x" and "B y"
+ proof -
+ have "A a" and "B b" \<proof>
+ then show thesis ..
+ qed
text_raw \<open>\end{minipage}\<close>
text \<open>
\<^medskip>
- Here local facts \isacharbackquoteopen\<open>A
- x\<close>\isacharbackquoteclose\ and \isacharbackquoteopen\<open>B
- y\<close>\isacharbackquoteclose\ are referenced immediately; there is no
- need to decompose the logical rule structure again. In the second
- proof the final ``@{command then}~@{command show}~\<open>thesis\<close>~@{command ".."}'' involves the local rule case \<open>\<And>x
- y. A x \<Longrightarrow> B y \<Longrightarrow> thesis\<close> for the particular instance of terms \<open>a\<close> and \<open>b\<close> produced in the body.
+ Here local facts \<open>\<open>A x\<close>\<close> and \<open>\<open>B y\<close>\<close> are referenced immediately; there is no
+ need to decompose the logical rule structure again. In the second proof the
+ final ``\<^theory_text>\<open>then show thesis ..\<close>'' involves the local rule case \<open>\<And>x y. A x \<Longrightarrow> B
+ y \<Longrightarrow> thesis\<close> for the particular instance of terms \<open>a\<close> and \<open>b\<close> produced in the
+ body.
\<close>
subsection \<open>Structured proof refinement \label{sec:framework-subproof}\<close>
text \<open>
- By breaking up the grammar for the Isar proof language, we may
- understand a proof text as a linear sequence of individual proof
- commands. These are interpreted as transitions of the Isar virtual
- machine (Isar/VM), which operates on a block-structured
- configuration in single steps. This allows users to write proof
- texts in an incremental manner, and inspect intermediate
- configurations for debugging.
+ By breaking up the grammar for the Isar proof language, we may understand a
+ proof text as a linear sequence of individual proof commands. These are
+ interpreted as transitions of the Isar virtual machine (Isar/VM), which
+ operates on a block-structured configuration in single steps. This allows
+ users to write proof texts in an incremental manner, and inspect
+ intermediate configurations for debugging.
- The basic idea is analogous to evaluating algebraic expressions on a
- stack machine: \<open>(a + b) \<cdot> c\<close> then corresponds to a sequence
- of single transitions for each symbol \<open>(, a, +, b, ), \<cdot>, c\<close>.
- In Isar the algebraic values are facts or goals, and the operations
- are inferences.
+ The basic idea is analogous to evaluating algebraic expressions on a stack
+ machine: \<open>(a + b) \<cdot> c\<close> then corresponds to a sequence of single transitions
+ for each symbol \<open>(, a, +, b, ), \<cdot>, c\<close>. In Isar the algebraic values are
+ facts or goals, and the operations are inferences.
\<^medskip>
- The Isar/VM state maintains a stack of nodes, each node
- contains the local proof context, the linguistic mode, and a pending
- goal (optional). The mode determines the type of transition that
- may be performed next, it essentially alternates between forward and
- backward reasoning, with an intermediate stage for chained facts
- (see \figref{fig:isar-vm}).
+ The Isar/VM state maintains a stack of nodes, each node contains the local
+ proof context, the linguistic mode, and a pending goal (optional). The mode
+ determines the type of transition that may be performed next, it essentially
+ alternates between forward and backward reasoning, with an intermediate
+ stage for chained facts (see \figref{fig:isar-vm}).
\begin{figure}[htb]
\begin{center}
@@ -812,17 +778,14 @@
\caption{Isar/VM modes}\label{fig:isar-vm}
\end{figure}
- For example, in \<open>state\<close> mode Isar acts like a mathematical
- scratch-pad, accepting declarations like @{command fix}, @{command
- assume}, and claims like @{command have}, @{command show}. A goal
- statement changes the mode to \<open>prove\<close>, which means that we
- may now refine the problem via @{command unfolding} or @{command
- proof}. Then we are again in \<open>state\<close> mode of a proof body,
- which may issue @{command show} statements to solve pending
- sub-goals. A concluding @{command qed} will return to the original
- \<open>state\<close> mode one level upwards. The subsequent Isar/VM
- trace indicates block structure, linguistic mode, goal state, and
- inferences:
+ For example, in \<open>state\<close> mode Isar acts like a mathematical scratch-pad,
+ accepting declarations like \<^theory_text>\<open>fix\<close>, \<^theory_text>\<open>assume\<close>, and claims like \<^theory_text>\<open>have\<close>,
+ \<^theory_text>\<open>show\<close>. A goal statement changes the mode to \<open>prove\<close>, which means that we
+ may now refine the problem via \<^theory_text>\<open>unfolding\<close> or \<^theory_text>\<open>proof\<close>. Then we are again
+ in \<open>state\<close> mode of a proof body, which may issue \<^theory_text>\<open>show\<close> statements to solve
+ pending subgoals. A concluding \<^theory_text>\<open>qed\<close> will return to the original \<open>state\<close>
+ mode one level upwards. The subsequent Isar/VM trace indicates block
+ structure, linguistic mode, goal state, and inferences:
\<close>
text_raw \<open>\begingroup\footnotesize\<close>
@@ -833,7 +796,7 @@
proof
assume A
show B
- sorry %noproof
+ \<proof>
qed
text_raw \<open>\end{minipage}\quad
\begin{minipage}[t]{0.06\textwidth}
@@ -873,13 +836,12 @@
text \<open>
Here the @{inference refinement} inference from
- \secref{sec:framework-resolution} mediates composition of Isar
- sub-proofs nicely. Observe that this principle incorporates some
- degree of freedom in proof composition. In particular, the proof
- body allows parameters and assumptions to be re-ordered, or commuted
- according to Hereditary Harrop Form. Moreover, context elements
- that are not used in a sub-proof may be omitted altogether. For
- example:
+ \secref{sec:framework-resolution} mediates composition of Isar subproofs
+ nicely. Observe that this principle incorporates some degree of freedom in
+ proof composition. In particular, the proof body allows parameters and
+ assumptions to be re-ordered, or commuted according to Hereditary Harrop
+ Form. Moreover, context elements that are not used in a subproof may be
+ omitted altogether. For example:
\<close>
text_raw \<open>\begin{minipage}{0.5\textwidth}\<close>
@@ -892,7 +854,7 @@
proof -
fix x and y
assume "A x" and "B y"
- show "C x y" sorry %noproof
+ show "C x y" \<proof>
qed
text_raw \<open>\end{minipage}\begin{minipage}{0.5\textwidth}\<close>
@@ -904,7 +866,7 @@
proof -
fix x assume "A x"
fix y assume "B y"
- show "C x y" sorry %noproof
+ show "C x y" \<proof>
qed
text_raw \<open>\end{minipage}\\[3ex]\begin{minipage}{0.5\textwidth}\<close>
@@ -916,7 +878,7 @@
proof -
fix y assume "B y"
fix x assume "A x"
- show "C x y" sorry
+ show "C x y" \<proof>
qed
text_raw \<open>\end{minipage}\begin{minipage}{0.5\textwidth}\<close>
@@ -927,7 +889,7 @@
proof -
fix y assume "B y"
fix x
- show "C x y" sorry
+ show "C x y" \<proof>
qed
(*<*)
end
@@ -937,17 +899,15 @@
text \<open>
\<^medskip>
- Such ``peephole optimizations'' of Isar texts are
- practically important to improve readability, by rearranging
- contexts elements according to the natural flow of reasoning in the
- body, while still observing the overall scoping rules.
+ Such fine-tuning of Isar text is practically important to improve
+ readability. Contexts elements are rearranged according to the natural flow
+ of reasoning in the body, while still observing the overall scoping rules.
\<^medskip>
- This illustrates the basic idea of structured proof
- processing in Isar. The main mechanisms are based on natural
- deduction rule composition within the Pure framework. In
- particular, there are no direct operations on goal states within the
- proof body. Moreover, there is no hidden automated reasoning
+ This illustrates the basic idea of structured proof processing in Isar. The
+ main mechanisms are based on natural deduction rule composition within the
+ Pure framework. In particular, there are no direct operations on goal states
+ within the proof body. Moreover, there is no hidden automated reasoning
involved, just plain unification.
\<close>
@@ -956,73 +916,69 @@
text \<open>
The existing Isar infrastructure is sufficiently flexible to support
- calculational reasoning (chains of transitivity steps) as derived
- concept. The generic proof elements introduced below depend on
- rules declared as @{attribute trans} in the context. It is left to
- the object-logic to provide a suitable rule collection for mixed
- relations of \<open>=\<close>, \<open><\<close>, \<open>\<le>\<close>, \<open>\<subset>\<close>,
- \<open>\<subseteq>\<close> etc. Due to the flexibility of rule composition
- (\secref{sec:framework-resolution}), substitution of equals by
- equals is covered as well, even substitution of inequalities
- involving monotonicity conditions; see also @{cite \<open>\S6\<close> "Wenzel-PhD"}
- and @{cite "Bauer-Wenzel:2001"}.
+ calculational reasoning (chains of transitivity steps) as derived concept.
+ The generic proof elements introduced below depend on rules declared as
+ @{attribute trans} in the context. It is left to the object-logic to provide
+ a suitable rule collection for mixed relations of \<open>=\<close>, \<open><\<close>, \<open>\<le>\<close>, \<open>\<subset>\<close>, \<open>\<subseteq>\<close>
+ etc. Due to the flexibility of rule composition
+ (\secref{sec:framework-resolution}), substitution of equals by equals is
+ covered as well, even substitution of inequalities involving monotonicity
+ conditions; see also @{cite \<open>\S6\<close> "Wenzel-PhD"} and @{cite
+ "Bauer-Wenzel:2001"}.
- The generic calculational mechanism is based on the observation that
- rules such as \<open>trans:\<close>~@{prop "x = y \<Longrightarrow> y = z \<Longrightarrow> x = z"}
- proceed from the premises towards the conclusion in a deterministic
- fashion. Thus we may reason in forward mode, feeding intermediate
- results into rules selected from the context. The course of
- reasoning is organized by maintaining a secondary fact called
- ``@{fact calculation}'', apart from the primary ``@{fact this}''
- already provided by the Isar primitives. In the definitions below,
+ The generic calculational mechanism is based on the observation that rules
+ such as \<open>trans:\<close>~@{prop "x = y \<Longrightarrow> y = z \<Longrightarrow> x = z"} proceed from the premises
+ towards the conclusion in a deterministic fashion. Thus we may reason in
+ forward mode, feeding intermediate results into rules selected from the
+ context. The course of reasoning is organized by maintaining a secondary
+ fact called ``@{fact calculation}'', apart from the primary ``@{fact this}''
+ already provided by the Isar primitives. In the definitions below,
@{attribute OF} refers to @{inference resolution}
- (\secref{sec:framework-resolution}) with multiple rule arguments,
- and \<open>trans\<close> represents to a suitable rule from the context:
+ (\secref{sec:framework-resolution}) with multiple rule arguments, and
+ \<open>trans\<close> represents to a suitable rule from the context:
\begin{matharray}{rcl}
- @{command "also"}\<open>\<^sub>0\<close> & \equiv & @{command "note"}~\<open>calculation = this\<close> \\
- @{command "also"}\<open>\<^sub>n\<^sub>+\<^sub>1\<close> & \equiv & @{command "note"}~\<open>calculation = trans [OF calculation this]\<close> \\[0.5ex]
- @{command "finally"} & \equiv & @{command "also"}~@{command "from"}~\<open>calculation\<close> \\
+ \<^theory_text>\<open>also"\<^sub>0"\<close> & \equiv & \<^theory_text>\<open>note calculation = this\<close> \\
+ \<^theory_text>\<open>also"\<^sub>n\<^sub>+\<^sub>1"\<close> & \equiv & \<^theory_text>\<open>note calculation = trans [OF calculation this]\<close> \\[0.5ex]
+ \<^theory_text>\<open>finally\<close> & \equiv & \<^theory_text>\<open>also from calculation\<close> \\
\end{matharray}
- The start of a calculation is determined implicitly in the
- text: here @{command also} sets @{fact calculation} to the current
- result; any subsequent occurrence will update @{fact calculation} by
- combination with the next result and a transitivity rule. The
- calculational sequence is concluded via @{command finally}, where
- the final result is exposed for use in a concluding claim.
+ The start of a calculation is determined implicitly in the text: here
+ \<^theory_text>\<open>also\<close> sets @{fact calculation} to the current result; any subsequent
+ occurrence will update @{fact calculation} by combination with the next
+ result and a transitivity rule. The calculational sequence is concluded via
+ \<^theory_text>\<open>finally\<close>, where the final result is exposed for use in a concluding claim.
- Here is a canonical proof pattern, using @{command have} to
- establish the intermediate results:
+ Here is a canonical proof pattern, using \<^theory_text>\<open>have\<close> to establish the
+ intermediate results:
\<close>
(*<*)
notepad
begin
+ fix a b c d :: 'a
(*>*)
- have "a = b" sorry
- also have "\<dots> = c" sorry
- also have "\<dots> = d" sorry
+ have "a = b" \<proof>
+ also have "\<dots> = c" \<proof>
+ also have "\<dots> = d" \<proof>
finally have "a = d" .
(*<*)
end
(*>*)
text \<open>
- The term ``\<open>\<dots>\<close>'' above is a special abbreviation
- provided by the Isabelle/Isar syntax layer: it statically refers to
- the right-hand side argument of the previous statement given in the
- text. Thus it happens to coincide with relevant sub-expressions in
- the calculational chain, but the exact correspondence is dependent
- on the transitivity rules being involved.
+ The term ``\<open>\<dots>\<close>'' (literal ellipsis) is a special abbreviation provided by
+ the Isabelle/Isar term syntax: it statically refers to the right-hand side
+ argument of the previous statement given in the text. Thus it happens to
+ coincide with relevant sub-expressions in the calculational chain, but the
+ exact correspondence is dependent on the transitivity rules being involved.
\<^medskip>
- Symmetry rules such as @{prop "x = y \<Longrightarrow> y = x"} are like
- transitivities with only one premise. Isar maintains a separate
- rule collection declared via the @{attribute sym} attribute, to be
- used in fact expressions ``\<open>a [symmetric]\<close>'', or single-step
- proofs ``@{command assume}~\<open>x = y\<close>~@{command then}~@{command
- have}~\<open>y = x\<close>~@{command ".."}''.
+ Symmetry rules such as @{prop "x = y \<Longrightarrow> y = x"} are like transitivities with
+ only one premise. Isar maintains a separate rule collection declared via the
+ @{attribute sym} attribute, to be used in fact expressions ``\<open>a
+ [symmetric]\<close>'', or single-step proofs ``\<^theory_text>\<open>assume "x = y" then have "y = x"
+ ..\<close>''.
\<close>
end
\ No newline at end of file
--- a/src/Doc/Isar_Ref/HOL_Specific.thy Wed Feb 10 15:49:05 2016 +0100
+++ b/src/Doc/Isar_Ref/HOL_Specific.thy Fri Feb 12 22:36:48 2016 +0100
@@ -642,14 +642,15 @@
\<close>}
\<^descr> @{command (HOL) "recdef"} defines general well-founded
- recursive functions (using the TFL package), see also
- @{cite "isabelle-HOL"}. The ``\<open>(permissive)\<close>'' option tells
- TFL to recover from failed proof attempts, returning unfinished
- results. The \<open>recdef_simp\<close>, \<open>recdef_cong\<close>, and \<open>recdef_wf\<close> hints refer to auxiliary rules to be used in the internal
- automated proof process of TFL. Additional @{syntax clasimpmod}
- declarations may be given to tune the context of the Simplifier
- (cf.\ \secref{sec:simplifier}) and Classical reasoner (cf.\
- \secref{sec:classical}).
+ recursive functions (using the TFL package). The
+ ``\<open>(permissive)\<close>'' option tells TFL to recover from
+ failed proof attempts, returning unfinished results. The
+ \<open>recdef_simp\<close>, \<open>recdef_cong\<close>, and
+ \<open>recdef_wf\<close> hints refer to auxiliary rules to be used
+ in the internal automated proof process of TFL. Additional
+ @{syntax clasimpmod} declarations may be given to tune the context
+ of the Simplifier (cf.\ \secref{sec:simplifier}) and Classical
+ reasoner (cf.\ \secref{sec:classical}).
\<^medskip>
@@ -763,9 +764,8 @@
These commands are mostly obsolete; @{command (HOL) "datatype"}
should be used instead.
- See @{cite "isabelle-HOL"} for more details on datatypes, but beware of
- the old-style theory syntax being used there! Apart from proper
- proof methods for case-analysis and induction, there are also
+ See @{cite "isabelle-datatypes"} for more details on datatypes. Apart from proper
+ proof methods for case analysis and induction, there are also
emulations of ML tactics @{method (HOL) case_tac} and @{method (HOL)
induct_tac} available, see \secref{sec:hol-induct-tac}; these admit
to refer directly to the internal structure of subgoals (including
--- a/src/Doc/Isar_Ref/Proof.thy Wed Feb 10 15:49:05 2016 +0100
+++ b/src/Doc/Isar_Ref/Proof.thy Fri Feb 12 22:36:48 2016 +0100
@@ -210,7 +210,7 @@
Abbreviations may be either bound by explicit @{command "let"}~\<open>p \<equiv> t\<close>
statements, or by annotating assumptions or goal statements with a list of
- patterns ``\<open>(\<IS> p\<^sub>1 \<dots> p\<^sub>n)\<close>''. In both cases, higher-order matching is
+ patterns ``\<^theory_text>\<open>(is p\<^sub>1 \<dots> p\<^sub>n)\<close>''. In both cases, higher-order matching is
invoked to bind extra-logical term variables, which may be either named
schematic variables of the form \<open>?x\<close>, or nameless dummies ``@{variable _}''
(underscore). Note that in the @{command "let"} form the patterns occur on
@@ -239,13 +239,13 @@
The syntax of @{keyword "is"} patterns follows @{syntax term_pat} or
@{syntax prop_pat} (see \secref{sec:term-decls}).
- \<^descr> @{command "let"}~\<open>p\<^sub>1 = t\<^sub>1 \<AND> \<dots> p\<^sub>n = t\<^sub>n\<close> binds any text variables
- in patterns \<open>p\<^sub>1, \<dots>, p\<^sub>n\<close> by simultaneous higher-order matching against
- terms \<open>t\<^sub>1, \<dots>, t\<^sub>n\<close>.
+ \<^descr> \<^theory_text>\<open>let p\<^sub>1 = t\<^sub>1 and \<dots> p\<^sub>n = t\<^sub>n\<close> binds any text variables in patterns
+ \<open>p\<^sub>1, \<dots>, p\<^sub>n\<close> by simultaneous higher-order matching against terms \<open>t\<^sub>1, \<dots>,
+ t\<^sub>n\<close>.
- \<^descr> \<open>(\<IS> p\<^sub>1 \<dots> p\<^sub>n)\<close> resembles @{command "let"}, but matches \<open>p\<^sub>1, \<dots>,
- p\<^sub>n\<close> against the preceding statement. Also note that @{keyword "is"} is
- not a separate command, but part of others (such as @{command "assume"},
+ \<^descr> \<^theory_text>\<open>(is p\<^sub>1 \<dots> p\<^sub>n)\<close> resembles @{command "let"}, but matches \<open>p\<^sub>1, \<dots>, p\<^sub>n\<close>
+ against the preceding statement. Also note that @{keyword "is"} is not a
+ separate command, but part of others (such as @{command "assume"},
@{command "have"} etc.).
Some \<^emph>\<open>implicit\<close> term abbreviations\index{term abbreviations} for goals and
@@ -441,14 +441,10 @@
warning beforehand. Watch out for the following message:
@{verbatim [display] \<open>Local statement fails to refine any pending goal\<close>}
- \<^descr> @{command "hence"} abbreviates ``@{command "then"}~@{command "have"}'',
- i.e.\ claims a local goal to be proven by forward chaining the current
- facts. Note that @{command "hence"} is also equivalent to ``@{command
- "from"}~\<open>this\<close>~@{command "have"}''.
-
- \<^descr> @{command "thus"} abbreviates ``@{command "then"}~@{command "show"}''.
- Note that @{command "thus"} is also equivalent to ``@{command
- "from"}~\<open>this\<close>~@{command "show"}''.
+ \<^descr> @{command "hence"} expands to ``@{command "then"}~@{command "have"}'' and
+ @{command "thus"} expands to ``@{command "then"}~@{command "show"}''. These
+ conflations are left-over from early history of Isar. The expanded syntax is
+ more orthogonal and improves readability and maintainability of proofs.
\<^descr> @{command "print_statement"}~\<open>a\<close> prints facts from the current theory or
proof context in long statement form, according to the syntax for @{command
@@ -682,11 +678,11 @@
forward chaining are passed if so indicated by \<open>proof(chain)\<close> mode.
\<^descr> @{command "qed"}~\<open>m\<^sub>2\<close> refines any remaining goals by proof method \<open>m\<^sub>2\<close>
- and concludes the sub-proof by assumption. If the goal had been \<open>show\<close> (or
- \<open>thus\<close>), some pending sub-goal is solved as well by the rule resulting from
- the result \<^emph>\<open>exported\<close> into the enclosing goal context. Thus \<open>qed\<close> may fail
- for two reasons: either \<open>m\<^sub>2\<close> fails, or the resulting rule does not fit to
- any pending goal\<^footnote>\<open>This includes any additional ``strong'' assumptions as
+ and concludes the sub-proof by assumption. If the goal had been \<open>show\<close>, some
+ pending sub-goal is solved as well by the rule resulting from the result
+ \<^emph>\<open>exported\<close> into the enclosing goal context. Thus \<open>qed\<close> may fail for two
+ reasons: either \<open>m\<^sub>2\<close> fails, or the resulting rule does not fit to any
+ pending goal\<^footnote>\<open>This includes any additional ``strong'' assumptions as
introduced by @{command "assume"}.\<close> of the enclosing context. Debugging such
a situation might involve temporarily changing @{command "show"} into
@{command "have"}, or weakening the local context by replacing occurrences
--- a/src/Doc/Isar_Ref/Proof_Script.thy Wed Feb 10 15:49:05 2016 +0100
+++ b/src/Doc/Isar_Ref/Proof_Script.thy Fri Feb 12 22:36:48 2016 +0100
@@ -13,10 +13,13 @@
Nonetheless, it is possible to emulate proof scripts by sequential
refinements of a proof state in backwards mode, notably with the @{command
- apply} command (see \secref{sec:tactic-commands}). There are also various
- proof methods that allow to refer to implicit goal state information that is
- normally not accessible to structured Isar proofs (see
- \secref{sec:tactics}).
+ apply} command (see \secref{sec:tactic-commands}).
+
+ There are also various proof methods that allow to refer to implicit goal
+ state information that is not accessible to structured Isar proofs (see
+ \secref{sec:tactics}). Note that the @{command subgoal}
+ (\secref{sec:subgoal}) command usually eliminates the need for implicit goal
+ state references.
\<close>
@@ -82,7 +85,7 @@
\<close>
-section \<open>Explicit subgoal structure\<close>
+section \<open>Explicit subgoal structure \label{sec:subgoal}\<close>
text \<open>
\begin{matharray}{rcl}
@@ -130,24 +133,24 @@
lemma "\<And>x y z. A x \<Longrightarrow> B y \<Longrightarrow> C z"
and "\<And>u v. X u \<Longrightarrow> Y v"
- subgoal sorry
- subgoal sorry
+ subgoal \<proof>
+ subgoal \<proof>
done
lemma "\<And>x y z. A x \<Longrightarrow> B y \<Longrightarrow> C z"
and "\<And>u v. X u \<Longrightarrow> Y v"
- subgoal for x y z sorry
- subgoal for u v sorry
+ subgoal for x y z \<proof>
+ subgoal for u v \<proof>
done
lemma "\<And>x y z. A x \<Longrightarrow> B y \<Longrightarrow> C z"
and "\<And>u v. X u \<Longrightarrow> Y v"
subgoal premises for x y z
using \<open>A x\<close> \<open>B y\<close>
- sorry
+ \<proof>
subgoal premises for u v
using \<open>X u\<close>
- sorry
+ \<proof>
done
lemma "\<And>x y z. A x \<Longrightarrow> B y \<Longrightarrow> C z"
@@ -156,21 +159,21 @@
proof -
have "A x" by (fact prems)
moreover have "B y" by (fact prems)
- ultimately show ?thesis sorry
+ ultimately show ?thesis \<proof>
qed
subgoal premises prems for u v
proof -
have "\<And>x y z. A x \<Longrightarrow> B y \<Longrightarrow> C z" by (fact r)
moreover
have "X u" by (fact prems)
- ultimately show ?thesis sorry
+ ultimately show ?thesis \<proof>
qed
done
lemma "\<And>x y z. A x \<Longrightarrow> B y \<Longrightarrow> C z"
subgoal premises prems for \<dots> z
proof -
- from prems show "C z" sorry
+ from prems show "C z" \<proof>
qed
done
--- a/src/Doc/Isar_Ref/Quick_Reference.thy Wed Feb 10 15:49:05 2016 +0100
+++ b/src/Doc/Isar_Ref/Quick_Reference.thy Fri Feb 12 22:36:48 2016 +0100
@@ -8,43 +8,58 @@
section \<open>Proof commands\<close>
-subsection \<open>Primitives and basic syntax\<close>
+subsection \<open>Main grammar \label{ap:main-grammar}\<close>
+
+text \<open>
+ \begin{tabular}{rcl}
+ \<open>main\<close> & = & \<^theory_text>\<open>notepad begin "statement\<^sup>*" end\<close> \\
+ & \<open>|\<close> & \<^theory_text>\<open>theorem name: props "proof"\<close> \\
+ & \<open>|\<close> & \<^theory_text>\<open>theorem name:\<close> \\
+ & & \quad\<^theory_text>\<open>fixes "var\<^sup>+"\<close> \\
+ & & \quad\<^theory_text>\<open>assumes name: props\<close> \\
+ & & \quad\<^theory_text>\<open>shows name: props "proof"\<close> \\
+ \<open>proof\<close> & = & \<^theory_text>\<open>"refinement\<^sup>*" proof "method\<^sup>?" "statement\<^sup>*" qed "method\<^sup>?"\<close> \\
+ & \<open>|\<close> & \<^theory_text>\<open>"refinement\<^sup>*" done\<close> \\
+ \<open>refinement\<close> & = & \<^theory_text>\<open>apply method\<close> \\
+ & \<open>|\<close> & \<^theory_text>\<open>supply facts\<close> \\
+ & \<open>|\<close> & \<^theory_text>\<open>subgoal "proof"\<close> \\
+ & \<open>|\<close> & \<^theory_text>\<open>subgoal for "var\<^sup>+" "proof"\<close> \\
+ & \<open>|\<close> & \<^theory_text>\<open>using facts\<close> \\
+ & \<open>|\<close> & \<^theory_text>\<open>unfolding facts\<close> \\
+ \<open>statement\<close> & = & \<^theory_text>\<open>{ "statement\<^sup>*" }\<close> \\
+ & \<open>|\<close> & \<^theory_text>\<open>next\<close> \\
+ & \<open>|\<close> & \<^theory_text>\<open>note name = facts\<close> \\
+ & \<open>|\<close> & \<^theory_text>\<open>let "term" = "term"\<close> \\
+ & \<open>|\<close> & \<^theory_text>\<open>write name (mixfix)\<close> \\
+ & \<open>|\<close> & \<^theory_text>\<open>fix "var\<^sup>+"\<close> \\
+ & \<open>|\<close> & \<^theory_text>\<open>assume name: props\<close> \\
+ & \<open>|\<close> & \<^theory_text>\<open>assume name: props if name: props for "var\<^sup>+"\<close> \\
+ & \<open>|\<close> & \<^theory_text>\<open>then"\<^sup>?" goal\<close> \\
+ \<open>goal\<close> & = & \<^theory_text>\<open>have name: props "proof"\<close> \\
+ & \<open>|\<close> & \<^theory_text>\<open>have name: props if name: props for "var\<^sup>+" "proof"\<close> \\
+ & \<open>|\<close> & \<^theory_text>\<open>show name: props "proof"\<close> \\
+ & \<open>|\<close> & \<^theory_text>\<open>show name: props if name: props for "var\<^sup>+" "proof"\<close> \\
+ \end{tabular}
+\<close>
+
+
+subsection \<open>Primitives\<close>
text \<open>
\begin{tabular}{ll}
- @{command "fix"}~\<open>x\<close> & augment context by \<open>\<And>x. \<box>\<close> \\
- @{command "assume"}~\<open>a: \<phi>\<close> & augment context by \<open>\<phi> \<Longrightarrow> \<box>\<close> \\
- @{command "then"} & indicate forward chaining of facts \\
- @{command "have"}~\<open>a: \<phi>\<close> & prove local result \\
- @{command "show"}~\<open>a: \<phi>\<close> & prove local result, refining some goal \\
- @{command "using"}~\<open>a\<close> & indicate use of additional facts \\
- @{command "unfolding"}~\<open>a\<close> & unfold definitional equations \\
- @{command "proof"}~\<open>m\<^sub>1\<close>~\dots~@{command "qed"}~\<open>m\<^sub>2\<close> & indicate proof structure and refinements \\
- @{command "{"}~\<open>\<dots>\<close>~@{command "}"} & indicate explicit blocks \\
- @{command "next"} & switch blocks \\
- @{command "note"}~\<open>a = b\<close> & reconsider facts \\
- @{command "let"}~\<open>p = t\<close> & abbreviate terms by higher-order matching \\
- @{command "write"}~\<open>c (mx)\<close> & declare local mixfix syntax \\
- \end{tabular}
-
- \<^medskip>
-
- \begin{tabular}{rcl}
- \<open>proof\<close> & = & \<open>prfx\<^sup>*\<close>~@{command "proof"}~\<open>method\<^sup>? stmt\<^sup>*\<close>~@{command "qed"}~\<open>method\<^sup>?\<close> \\
- & \<open>|\<close> & \<open>prfx\<^sup>*\<close>~@{command "done"} \\
- \<open>prfx\<close> & = & @{command "apply"}~\<open>method\<close> \\
- & \<open>|\<close> & @{command "using"}~\<open>facts\<close> \\
- & \<open>|\<close> & @{command "unfolding"}~\<open>facts\<close> \\
- \<open>stmt\<close> & = & @{command "{"}~\<open>stmt\<^sup>*\<close>~@{command "}"} \\
- & \<open>|\<close> & @{command "next"} \\
- & \<open>|\<close> & @{command "note"}~\<open>name = facts\<close> \\
- & \<open>|\<close> & @{command "let"}~\<open>term = term\<close> \\
- & \<open>|\<close> & @{command "write"}~\<open>name (mixfix)\<close> \\
- & \<open>|\<close> & @{command "fix"}~\<open>var\<^sup>+\<close> \\
- & \<open>|\<close> & @{command "assume"}~\<open>name: props\<close> \\
- & \<open>|\<close> & @{command "then"}\<open>\<^sup>?\<close>~\<open>goal\<close> \\
- \<open>goal\<close> & = & @{command "have"}~\<open>name: props proof\<close> \\
- & \<open>|\<close> & @{command "show"}~\<open>name: props proof\<close> \\
+ \<^theory_text>\<open>fix x\<close> & augment context by \<open>\<And>x. \<box>\<close> \\
+ \<^theory_text>\<open>assume a: A\<close> & augment context by \<open>A \<Longrightarrow> \<box>\<close> \\
+ \<^theory_text>\<open>then\<close> & indicate forward chaining of facts \\
+ \<^theory_text>\<open>have a: A\<close> & prove local result \\
+ \<^theory_text>\<open>show a: A\<close> & prove local result, refining some goal \\
+ \<^theory_text>\<open>using a\<close> & indicate use of additional facts \\
+ \<^theory_text>\<open>unfolding a\<close> & unfold definitional equations \\
+ \<^theory_text>\<open>proof m\<^sub>1 \<dots> qed m\<^sub>2\<close> & indicate proof structure and refinements \\
+ \<^theory_text>\<open>{ \<dots> }\<close> & indicate explicit blocks \\
+ \<^theory_text>\<open>next\<close> & switch proof blocks \\
+ \<^theory_text>\<open>note a = b\<close> & reconsider and declare facts \\
+ \<^theory_text>\<open>let p = t\<close> & abbreviate terms by higher-order matching \\
+ \<^theory_text>\<open>write c (mx)\<close> & declare local mixfix syntax \\
\end{tabular}
\<close>
@@ -53,17 +68,12 @@
text \<open>
\begin{tabular}{rcl}
- @{command "by"}~\<open>m\<^sub>1 m\<^sub>2\<close> & \<open>\<equiv>\<close> &
- @{command "proof"}~\<open>m\<^sub>1\<close>~@{command "qed"}~\<open>m\<^sub>2\<close> \\
- @{command ".."} & \<open>\<equiv>\<close> & @{command "by"}~\<open>standard\<close> \\
- @{command "."} & \<open>\<equiv>\<close> & @{command "by"}~\<open>this\<close> \\
- @{command "hence"} & \<open>\<equiv>\<close> & @{command "then"}~@{command "have"} \\
- @{command "thus"} & \<open>\<equiv>\<close> & @{command "then"}~@{command "show"} \\
- @{command "from"}~\<open>a\<close> & \<open>\<equiv>\<close> & @{command "note"}~\<open>a\<close>~@{command "then"} \\
- @{command "with"}~\<open>a\<close> & \<open>\<equiv>\<close> & @{command "from"}~\<open>a \<AND> this\<close> \\
- @{command "from"}~\<open>this\<close> & \<open>\<equiv>\<close> & @{command "then"} \\
- @{command "from"}~\<open>this\<close>~@{command "have"} & \<open>\<equiv>\<close> & @{command "hence"} \\
- @{command "from"}~\<open>this\<close>~@{command "show"} & \<open>\<equiv>\<close> & @{command "thus"} \\
+ \<^theory_text>\<open>by m\<^sub>1 m\<^sub>2\<close> & \<open>\<equiv>\<close> & \<^theory_text>\<open>proof m\<^sub>1 qed m\<^sub>2\<close> \\
+ \<^theory_text>\<open>..\<close> & \<open>\<equiv>\<close> & \<^theory_text>\<open>by standard\<close> \\
+ \<^theory_text>\<open>.\<close> & \<open>\<equiv>\<close> & \<^theory_text>\<open>by this\<close> \\
+ \<^theory_text>\<open>from a\<close> & \<open>\<equiv>\<close> & \<^theory_text>\<open>note a then\<close> \\
+ \<^theory_text>\<open>with a\<close> & \<open>\<equiv>\<close> & \<^theory_text>\<open>from a and this\<close> \\
+ \<^theory_text>\<open>from this\<close> & \<open>\<equiv>\<close> & \<^theory_text>\<open>then\<close> \\
\end{tabular}
\<close>
@@ -72,26 +82,19 @@
text \<open>
\begin{tabular}{rcl}
- @{command "also"}\<open>\<^sub>0\<close> & \<open>\<approx>\<close> &
- @{command "note"}~\<open>calculation = this\<close> \\
- @{command "also"}\<open>\<^sub>n\<^sub>+\<^sub>1\<close> & \<open>\<approx>\<close> &
- @{command "note"}~\<open>calculation = trans [OF calculation this]\<close> \\
- @{command "finally"} & \<open>\<approx>\<close> &
- @{command "also"}~@{command "from"}~\<open>calculation\<close> \\[0.5ex]
- @{command "moreover"} & \<open>\<approx>\<close> &
- @{command "note"}~\<open>calculation = calculation this\<close> \\
- @{command "ultimately"} & \<open>\<approx>\<close> &
- @{command "moreover"}~@{command "from"}~\<open>calculation\<close> \\[0.5ex]
- @{command "presume"}~\<open>a: \<phi>\<close> & \<open>\<approx>\<close> &
- @{command "assume"}~\<open>a: \<phi>\<close> \\
- @{command "def"}~\<open>a: x \<equiv> t\<close> & \<open>\<approx>\<close> &
- @{command "fix"}~\<open>x\<close>~@{command "assume"}~\<open>a: x \<equiv> t\<close> \\
- @{command "obtain"}~\<open>x \<WHERE> a: \<phi>\<close> & \<open>\<approx>\<close> &
- \<open>\<dots>\<close>~@{command "fix"}~\<open>x\<close>~@{command "assume"}~\<open>a: \<phi>\<close> \\
- @{command "case"}~\<open>c\<close> & \<open>\<approx>\<close> &
- @{command "fix"}~\<open>x\<close>~@{command "assume"}~\<open>c: \<phi>\<close> \\
- @{command "sorry"} & \<open>\<approx>\<close> &
- @{command "by"}~\<open>cheating\<close> \\
+ \<^theory_text>\<open>also"\<^sub>0"\<close> & \<open>\<approx>\<close> & \<^theory_text>\<open>note calculation = this\<close> \\
+ \<^theory_text>\<open>also"\<^sub>n\<^sub>+\<^sub>1"\<close> & \<open>\<approx>\<close> & \<^theory_text>\<open>note calculation = trans [OF calculation this]\<close> \\
+ \<^theory_text>\<open>finally\<close> & \<open>\<approx>\<close> & \<^theory_text>\<open>also from calculation\<close> \\[0.5ex]
+ \<^theory_text>\<open>moreover\<close> & \<open>\<approx>\<close> & \<^theory_text>\<open>note calculation = calculation this\<close> \\
+ \<^theory_text>\<open>ultimately\<close> & \<open>\<approx>\<close> & \<^theory_text>\<open>moreover from calculation\<close> \\[0.5ex]
+ \<^theory_text>\<open>presume a: A\<close> & \<open>\<approx>\<close> & \<^theory_text>\<open>assume a: A\<close> \\
+ \<^theory_text>\<open>def "x \<equiv> t"\<close> & \<open>\<approx>\<close> & \<^theory_text>\<open>fix x assume x_def: "x \<equiv> t"\<close> \\
+ \<^theory_text>\<open>consider x where A | \<dots>\<close> & \<open>\<approx>\<close> & \<^theory_text>\<open>have thesis\<close> \\
+ & & \quad \<^theory_text>\<open>if "\<And>x. A \<Longrightarrow> thesis" and \<dots> for thesis\<close> \\
+ \<^theory_text>\<open>obtain x where a: A \<proof>\<close> & \<open>\<approx>\<close> & \<^theory_text>\<open>consider x where A \<proof>\<close> \\
+ & & \<^theory_text>\<open>fix x assume a: A\<close> \\
+ \<^theory_text>\<open>case c\<close> & \<open>\<approx>\<close> & \<^theory_text>\<open>fix x assume c: A\<close> \\
+ \<^theory_text>\<open>sorry\<close> & \<open>\<approx>\<close> & \<^theory_text>\<open>by cheating\<close> \\
\end{tabular}
\<close>
@@ -100,12 +103,11 @@
text \<open>
\begin{tabular}{ll}
- @{command "print_state"} & print proof state \\
- @{command "print_statement"} & print fact in long statement form \\
- @{command "thm"}~\<open>a\<close> & print fact \\
- @{command "prop"}~\<open>\<phi>\<close> & print proposition \\
- @{command "term"}~\<open>t\<close> & print term \\
- @{command "typ"}~\<open>\<tau>\<close> & print type \\
+ \<^theory_text>\<open>typ \<tau>\<close> & print type \\
+ \<^theory_text>\<open>term t\<close> & print term \\
+ \<^theory_text>\<open>prop \<phi>\<close> & print proposition \\
+ \<^theory_text>\<open>thm a\<close> & print fact \\
+ \<^theory_text>\<open>print_statement a\<close> & print fact in long statement form \\
\end{tabular}
\<close>
@@ -115,7 +117,7 @@
text \<open>
\begin{tabular}{ll}
\multicolumn{2}{l}{\<^bold>\<open>Single steps (forward-chaining facts)\<close>} \\[0.5ex]
- @{method assumption} & apply some assumption \\
+ @{method assumption} & apply some goal assumption \\
@{method this} & apply current facts \\
@{method rule}~\<open>a\<close> & apply some rule \\
@{method standard} & apply standard rule (default for @{command "proof"}) \\
@@ -127,6 +129,8 @@
@{method "-"} & no rules \\
@{method intro}~\<open>a\<close> & introduction rules \\
@{method intro_classes} & class introduction rules \\
+ @{method intro_locales} & locale introduction rules (without body) \\
+ @{method unfold_locales} & locale introduction rules (with body) \\
@{method elim}~\<open>a\<close> & elimination rules \\
@{method unfold}~\<open>a\<close> & definitional rewrite rules \\[2ex]
@@ -195,18 +199,20 @@
\<close>
-section \<open>Emulating tactic scripts\<close>
+section \<open>Proof scripts\<close>
subsection \<open>Commands\<close>
text \<open>
\begin{tabular}{ll}
- @{command "apply"}~\<open>m\<close> & apply proof method at initial position \\
- @{command "apply_end"}~\<open>m\<close> & apply proof method near terminal position \\
- @{command "done"} & complete proof \\
- @{command "defer"}~\<open>n\<close> & move subgoal to end \\
- @{command "prefer"}~\<open>n\<close> & move subgoal to beginning \\
- @{command "back"} & backtrack last command \\
+ \<^theory_text>\<open>apply m\<close> & apply proof method during backwards refinement \\
+ \<^theory_text>\<open>apply_end m\<close> & apply proof method (as if in terminal position) \\
+ \<^theory_text>\<open>supply a\<close> & supply facts during backwards refinement \\
+ \<^theory_text>\<open>subgoal\<close> & nested proof during backwards refinement \\
+ \<^theory_text>\<open>defer n\<close> & move subgoal to end \\
+ \<^theory_text>\<open>prefer n\<close> & move subgoal to start \\
+ \<^theory_text>\<open>back\<close> & backtrack last command \\
+ \<^theory_text>\<open>done\<close> & complete proof \\
\end{tabular}
\<close>
--- a/src/Doc/Isar_Ref/Synopsis.thy Wed Feb 10 15:49:05 2016 +0100
+++ b/src/Doc/Isar_Ref/Synopsis.thy Fri Feb 12 22:36:48 2016 +0100
@@ -53,7 +53,7 @@
assume a: A
txt \<open>Via proof (``let''):\<close>
- have b: B sorry
+ have b: B \<proof>
txt \<open>Via abbreviation (``let''):\<close>
note c = a b
@@ -156,8 +156,8 @@
notepad
begin
{
- have a: A sorry
- have b: B sorry
+ have a: A \<proof>
+ have b: B \<proof>
note a b
}
note this
@@ -174,15 +174,15 @@
begin
{
- have a: A sorry
+ have a: A \<proof>
next
have b: B
proof -
- show B sorry
+ show B \<proof>
next
- have c: C sorry
+ have c: C \<proof>
next
- have d: D sorry
+ have d: D \<proof>
qed
}
@@ -190,19 +190,19 @@
{
{
- have a: A sorry
+ have a: A \<proof>
}
{
have b: B
proof -
{
- show B sorry
+ show B \<proof>
}
{
- have c: C sorry
+ have c: C \<proof>
}
{
- have d: D sorry
+ have d: D \<proof>
}
qed
}
@@ -235,7 +235,7 @@
have "x = y"
proof -
term ?thesis
- show ?thesis sorry
+ show ?thesis \<proof>
term ?thesis \<comment> \<open>static!\<close>
qed
term "\<dots>"
@@ -260,31 +260,31 @@
notepad
begin
txt \<open>Plain bottom-up calculation:\<close>
- have "a = b" sorry
+ have "a = b" \<proof>
also
- have "b = c" sorry
+ have "b = c" \<proof>
also
- have "c = d" sorry
+ have "c = d" \<proof>
finally
have "a = d" .
txt \<open>Variant using the \<open>\<dots>\<close> abbreviation:\<close>
- have "a = b" sorry
+ have "a = b" \<proof>
also
- have "\<dots> = c" sorry
+ have "\<dots> = c" \<proof>
also
- have "\<dots> = d" sorry
+ have "\<dots> = d" \<proof>
finally
have "a = d" .
txt \<open>Top-down version with explicit claim at the head:\<close>
have "a = d"
proof -
- have "a = b" sorry
+ have "a = b" \<proof>
also
- have "\<dots> = c" sorry
+ have "\<dots> = c" \<proof>
also
- have "\<dots> = d" sorry
+ have "\<dots> = d" \<proof>
finally
show ?thesis .
qed
@@ -292,11 +292,11 @@
txt \<open>Mixed inequalities (require suitable base type):\<close>
fix a b c d :: nat
- have "a < b" sorry
+ have "a < b" \<proof>
also
- have "b \<le> c" sorry
+ have "b \<le> c" \<proof>
also
- have "c = d" sorry
+ have "c = d" \<proof>
finally
have "a < d" .
end
@@ -313,43 +313,35 @@
\<close>
-subsection \<open>Degenerate calculations and bigstep reasoning\<close>
+subsection \<open>Degenerate calculations\<close>
-text \<open>The Idea is to append \<open>this\<close> to \<open>calculation\<close>,
- without rule composition.\<close>
+text \<open>The Idea is to append \<open>this\<close> to \<open>calculation\<close>, without rule composition.
+ This is occasionally useful to avoid naming intermediate facts.\<close>
notepad
begin
txt \<open>A vacuous proof:\<close>
- have A sorry
+ have A \<proof>
moreover
- have B sorry
+ have B \<proof>
moreover
- have C sorry
+ have C \<proof>
ultimately
have A and B and C .
next
txt \<open>Slightly more content (trivial bigstep reasoning):\<close>
- have A sorry
+ have A \<proof>
moreover
- have B sorry
+ have B \<proof>
moreover
- have C sorry
+ have C \<proof>
ultimately
have "A \<and> B \<and> C" by blast
-next
- txt \<open>More ambitious bigstep reasoning involving structured results:\<close>
- have "A \<or> B \<or> C" sorry
- moreover
- { assume A have R sorry }
- moreover
- { assume B have R sorry }
- moreover
- { assume C have R sorry }
- ultimately
- have R by blast \<comment> \<open>``big-bang integration'' of proof blocks (occasionally fragile)\<close>
end
+text \<open>Note that For multi-branch case splitting, it is better to use @{command
+ consider}.\<close>
+
section \<open>Induction\<close>
@@ -367,11 +359,11 @@
fix n :: nat
have "P n"
proof (rule nat.induct) \<comment> \<open>fragile rule application!\<close>
- show "P 0" sorry
+ show "P 0" \<proof>
next
fix n :: nat
assume "P n"
- show "P (Suc n)" sorry
+ show "P (Suc n)" \<proof>
qed
end
@@ -394,10 +386,10 @@
have "P n"
proof (induct n)
case 0
- show ?case sorry
+ show ?case \<proof>
next
case (Suc n)
- from Suc.hyps show ?case sorry
+ from Suc.hyps show ?case \<proof>
qed
end
@@ -456,29 +448,29 @@
have "P n"
proof (induct n)
case 0
- show "P 0" sorry
+ show "P 0" \<proof>
next
case (Suc n)
- from \<open>P n\<close> show "P (Suc n)" sorry
+ from \<open>P n\<close> show "P (Suc n)" \<proof>
qed
have "A n \<Longrightarrow> P n"
proof (induct n)
case 0
- from \<open>A 0\<close> show "P 0" sorry
+ from \<open>A 0\<close> show "P 0" \<proof>
next
case (Suc n)
from \<open>A n \<Longrightarrow> P n\<close>
- and \<open>A (Suc n)\<close> show "P (Suc n)" sorry
+ and \<open>A (Suc n)\<close> show "P (Suc n)" \<proof>
qed
have "\<And>x. Q x n"
proof (induct n)
case 0
- show "Q x 0" sorry
+ show "Q x 0" \<proof>
next
case (Suc n)
- from \<open>\<And>x. Q x n\<close> show "Q x (Suc n)" sorry
+ from \<open>\<And>x. Q x n\<close> show "Q x (Suc n)" \<proof>
txt \<open>Local quantification admits arbitrary instances:\<close>
note \<open>Q a n\<close> and \<open>Q b n\<close>
qed
@@ -502,11 +494,11 @@
then have "Q x n"
proof (induct n arbitrary: x)
case 0
- from \<open>A x 0\<close> show "Q x 0" sorry
+ from \<open>A x 0\<close> show "Q x 0" \<proof>
next
case (Suc n)
from \<open>\<And>x. A x n \<Longrightarrow> Q x n\<close> \<comment> \<open>arbitrary instances can be produced here\<close>
- and \<open>A x (Suc n)\<close> show "Q x (Suc n)" sorry
+ and \<open>A x (Suc n)\<close> show "Q x (Suc n)" \<proof>
qed
end
@@ -532,13 +524,13 @@
case 0
note prem = \<open>A (a x)\<close>
and defn = \<open>0 = a x\<close>
- show "P (a x)" sorry
+ show "P (a x)" \<proof>
next
case (Suc n)
note hyp = \<open>\<And>x. n = a x \<Longrightarrow> A (a x) \<Longrightarrow> P (a x)\<close>
and prem = \<open>A (a x)\<close>
and defn = \<open>Suc n = a x\<close>
- show "P (a x)" sorry
+ show "P (a x)" \<proof>
qed
end
@@ -628,7 +620,7 @@
begin
{
fix x
- have "B x" sorry
+ have "B x" \<proof>
}
have "\<And>x. B x" by fact
@@ -636,7 +628,7 @@
{
assume A
- have B sorry
+ have B \<proof>
}
have "A \<Longrightarrow> B" by fact
@@ -644,15 +636,15 @@
{
def x \<equiv> t
- have "B x" sorry
+ have "B x" \<proof>
}
have "B t" by fact
next
{
- obtain x :: 'a where "B x" sorry
- have C sorry
+ obtain x :: 'a where "B x" \<proof>
+ have C \<proof>
}
have C by fact
@@ -703,7 +695,7 @@
proof -
fix x
assume "A x"
- show "B x" sorry
+ show "B x" \<proof>
qed
have "\<And>x. A x \<Longrightarrow> B x"
@@ -711,7 +703,7 @@
{
fix x
assume "A x"
- show "B x" sorry
+ show "B x" \<proof>
} \<comment> "implicit block structure made explicit"
note \<open>\<And>x. A x \<Longrightarrow> B x\<close>
\<comment> "side exit for the resulting rule"
@@ -728,41 +720,41 @@
notepad
begin
- assume r1: "A \<Longrightarrow> B \<Longrightarrow> C" \<comment> \<open>simple rule (Horn clause)\<close>
+ assume r\<^sub>1: "A \<Longrightarrow> B \<Longrightarrow> C" \<comment> \<open>simple rule (Horn clause)\<close>
- have A sorry \<comment> "prefix of facts via outer sub-proof"
+ have A \<proof> \<comment> "prefix of facts via outer sub-proof"
then have C
- proof (rule r1)
- show B sorry \<comment> "remaining rule premises via inner sub-proof"
+ proof (rule r\<^sub>1)
+ show B \<proof> \<comment> "remaining rule premises via inner sub-proof"
qed
have C
- proof (rule r1)
- show A sorry
- show B sorry
+ proof (rule r\<^sub>1)
+ show A \<proof>
+ show B \<proof>
qed
- have A and B sorry
+ have A and B \<proof>
then have C
- proof (rule r1)
+ proof (rule r\<^sub>1)
qed
- have A and B sorry
- then have C by (rule r1)
+ have A and B \<proof>
+ then have C by (rule r\<^sub>1)
next
- assume r2: "A \<Longrightarrow> (\<And>x. B1 x \<Longrightarrow> B2 x) \<Longrightarrow> C" \<comment> \<open>nested rule\<close>
+ assume r\<^sub>2: "A \<Longrightarrow> (\<And>x. B\<^sub>1 x \<Longrightarrow> B\<^sub>2 x) \<Longrightarrow> C" \<comment> \<open>nested rule\<close>
- have A sorry
+ have A \<proof>
then have C
- proof (rule r2)
+ proof (rule r\<^sub>2)
fix x
- assume "B1 x"
- show "B2 x" sorry
+ assume "B\<^sub>1 x"
+ show "B\<^sub>2 x" \<proof>
qed
- txt \<open>The compound rule premise @{prop "\<And>x. B1 x \<Longrightarrow> B2 x"} is better
+ txt \<open>The compound rule premise @{prop "\<And>x. B\<^sub>1 x \<Longrightarrow> B\<^sub>2 x"} is better
addressed via @{command fix}~/ @{command assume}~/ @{command show}
in the nested proof body.\<close>
end
@@ -777,35 +769,35 @@
notepad
begin
- have "A \<longrightarrow> B" and A sorry
+ have "A \<longrightarrow> B" and A \<proof>
then have B ..
- have A sorry
+ have A \<proof>
then have "A \<or> B" ..
- have B sorry
+ have B \<proof>
then have "A \<or> B" ..
- have "A \<or> B" sorry
+ have "A \<or> B" \<proof>
then have C
proof
assume A
- then show C sorry
+ then show C \<proof>
next
assume B
- then show C sorry
+ then show C \<proof>
qed
- have A and B sorry
+ have A and B \<proof>
then have "A \<and> B" ..
- have "A \<and> B" sorry
+ have "A \<and> B" \<proof>
then have A ..
- have "A \<and> B" sorry
+ have "A \<and> B" \<proof>
then have B ..
- have False sorry
+ have False \<proof>
then have A ..
have True ..
@@ -813,36 +805,36 @@
have "\<not> A"
proof
assume A
- then show False sorry
+ then show False \<proof>
qed
- have "\<not> A" and A sorry
+ have "\<not> A" and A \<proof>
then have B ..
have "\<forall>x. P x"
proof
fix x
- show "P x" sorry
+ show "P x" \<proof>
qed
- have "\<forall>x. P x" sorry
+ have "\<forall>x. P x" \<proof>
then have "P a" ..
have "\<exists>x. P x"
proof
- show "P a" sorry
+ show "P a" \<proof>
qed
- have "\<exists>x. P x" sorry
+ have "\<exists>x. P x" \<proof>
then have C
proof
fix a
assume "P a"
- show C sorry
+ show C \<proof>
qed
txt \<open>Less awkward version using @{command obtain}:\<close>
- have "\<exists>x. P x" sorry
+ have "\<exists>x. P x" \<proof>
then obtain a where "P a" ..
end
@@ -853,32 +845,32 @@
begin
have "A \<and> B"
proof \<comment> \<open>two strictly isolated subproofs\<close>
- show A sorry
+ show A \<proof>
next
- show B sorry
+ show B \<proof>
qed
have "A \<and> B"
proof \<comment> \<open>one simultaneous sub-proof\<close>
- show A and B sorry
+ show A and B \<proof>
qed
have "A \<and> B"
proof \<comment> \<open>two subproofs in the same context\<close>
- show A sorry
- show B sorry
+ show A \<proof>
+ show B \<proof>
qed
have "A \<and> B"
proof \<comment> \<open>swapped order\<close>
- show B sorry
- show A sorry
+ show B \<proof>
+ show A \<proof>
qed
have "A \<and> B"
proof \<comment> \<open>sequential subproofs\<close>
- show A sorry
- show B using \<open>A\<close> sorry
+ show A \<proof>
+ show B using \<open>A\<close> \<proof>
qed
end
@@ -893,23 +885,23 @@
notepad
begin
- have "x \<in> A" and "x \<in> B" sorry
+ have "x \<in> A" and "x \<in> B" \<proof>
then have "x \<in> A \<inter> B" ..
- have "x \<in> A" sorry
+ have "x \<in> A" \<proof>
then have "x \<in> A \<union> B" ..
- have "x \<in> B" sorry
+ have "x \<in> B" \<proof>
then have "x \<in> A \<union> B" ..
- have "x \<in> A \<union> B" sorry
+ have "x \<in> A \<union> B" \<proof>
then have C
proof
assume "x \<in> A"
- then show C sorry
+ then show C \<proof>
next
assume "x \<in> B"
- then show C sorry
+ then show C \<proof>
qed
next
@@ -917,19 +909,19 @@
proof
fix a
assume "a \<in> A"
- show "x \<in> a" sorry
+ show "x \<in> a" \<proof>
qed
- have "x \<in> \<Inter>A" sorry
+ have "x \<in> \<Inter>A" \<proof>
then have "x \<in> a"
proof
- show "a \<in> A" sorry
+ show "a \<in> A" \<proof>
qed
- have "a \<in> A" and "x \<in> a" sorry
+ have "a \<in> A" and "x \<in> a" \<proof>
then have "x \<in> \<Union>A" ..
- have "x \<in> \<Union>A" sorry
+ have "x \<in> \<Union>A" \<proof>
then obtain a where "a \<in> A" and "x \<in> a" ..
end
@@ -960,21 +952,21 @@
notepad
begin
assume r:
- "A1 \<Longrightarrow> A2 \<Longrightarrow> (* assumptions *)
- (\<And>x y. B1 x y \<Longrightarrow> C1 x y \<Longrightarrow> R) \<Longrightarrow> (* case 1 *)
- (\<And>x y. B2 x y \<Longrightarrow> C2 x y \<Longrightarrow> R) \<Longrightarrow> (* case 2 *)
+ "A\<^sub>1 \<Longrightarrow> A\<^sub>2 \<Longrightarrow> (* assumptions *)
+ (\<And>x y. B\<^sub>1 x y \<Longrightarrow> C\<^sub>1 x y \<Longrightarrow> R) \<Longrightarrow> (* case 1 *)
+ (\<And>x y. B\<^sub>2 x y \<Longrightarrow> C\<^sub>2 x y \<Longrightarrow> R) \<Longrightarrow> (* case 2 *)
R (* main conclusion *)"
- have A1 and A2 sorry
+ have A\<^sub>1 and A\<^sub>2 \<proof>
then have R
proof (rule r)
fix x y
- assume "B1 x y" and "C1 x y"
- show ?thesis sorry
+ assume "B\<^sub>1 x y" and "C\<^sub>1 x y"
+ show ?thesis \<proof>
next
fix x y
- assume "B2 x y" and "C2 x y"
- show ?thesis sorry
+ assume "B\<^sub>2 x y" and "C\<^sub>2 x y"
+ show ?thesis \<proof>
qed
end
@@ -1003,11 +995,11 @@
print_statement disjE
lemma
- assumes A1 and A2 \<comment> \<open>assumptions\<close>
+ assumes A\<^sub>1 and A\<^sub>2 \<comment> \<open>assumptions\<close>
obtains
- (case1) x y where "B1 x y" and "C1 x y"
- | (case2) x y where "B2 x y" and "C2 x y"
- sorry
+ (case\<^sub>1) x y where "B\<^sub>1 x y" and "C\<^sub>1 x y"
+ | (case\<^sub>2) x y where "B\<^sub>2 x y" and "C\<^sub>2 x y"
+ \<proof>
subsubsection \<open>Example\<close>
@@ -1024,10 +1016,10 @@
have C
proof (cases "x = y" rule: tertium_non_datur)
case T
- from \<open>x = y\<close> show ?thesis sorry
+ from \<open>x = y\<close> show ?thesis \<proof>
next
case F
- from \<open>x \<noteq> y\<close> show ?thesis sorry
+ from \<open>x \<noteq> y\<close> show ?thesis \<proof>
qed
end
@@ -1047,14 +1039,44 @@
have C
proof (cases x)
case Foo
- from \<open>x = Foo\<close> show ?thesis sorry
+ from \<open>x = Foo\<close> show ?thesis \<proof>
next
case (Bar a)
- from \<open>x = Bar a\<close> show ?thesis sorry
+ from \<open>x = Bar a\<close> show ?thesis \<proof>
qed
end
+subsection \<open>Elimination statements and case-splitting\<close>
+
+text \<open>
+ The @{command consider} states rules for generalized elimination and case
+ splitting. This is like a toplevel statement \<^theory_text>\<open>theorem obtains\<close> used within
+ a proof body; or like a multi-branch \<^theory_text>\<open>obtain\<close> without activation of the
+ local context elements yet.
+
+ The proof method @{method cases} is able to use such rules with
+ forward-chaining (e.g.\ via \<^theory_text>\<open>then\<close>). This leads to the subsequent pattern
+ for case-splitting in a particular situation within a proof.
+\<close>
+
+notepad
+begin
+ consider (a) A | (b) B | (c) C
+ \<proof> \<comment> \<open>typically \<^theory_text>\<open>by auto\<close>, \<^theory_text>\<open>by blast\<close> etc.\<close>
+ then have something
+ proof cases
+ case a
+ then show ?thesis \<proof>
+ next
+ case b
+ then show ?thesis \<proof>
+ next
+ case c
+ then show ?thesis \<proof>
+ qed
+end
+
subsection \<open>Obtaining local contexts\<close>
text \<open>A single ``case'' branch may be inlined into Isar proof text
@@ -1065,13 +1087,13 @@
begin
fix B :: "'a \<Rightarrow> bool"
- obtain x where "B x" sorry
+ obtain x where "B x" \<proof>
note \<open>B x\<close>
txt \<open>Conclusions from this context may not mention @{term x} again!\<close>
{
- obtain x where "B x" sorry
- from \<open>B x\<close> have C sorry
+ obtain x where "B x" \<proof>
+ from \<open>B x\<close> have C \<proof>
}
note \<open>C\<close>
end
--- a/src/Doc/Isar_Ref/document/style.sty Wed Feb 10 15:49:05 2016 +0100
+++ b/src/Doc/Isar_Ref/document/style.sty Fri Feb 12 22:36:48 2016 +0100
@@ -16,9 +16,11 @@
%% Isar
\newcommand{\isasymBBAR}{{\,\newdimen{\tmpheight}\settoheight\tmpheight{\isacharbar}\rule{1pt}{\tmpheight}\,}}
-\isafoldtag{noproof}\def\isafoldnoproof{~\isafold{proof}}
\renewcommand{\isacommand}[1]{\isakeyword{\isadigitreset#1}}
+\newcommand{\isasymproof}{\isamath{\,\langle\mathit{proof}\rangle}}
+
+
%% ML
\newenvironment{mldecls}{\par\noindent\begingroup\def\isanewline{\\}\begin{tabular}{ll}}{\end{tabular}\medskip\endgroup}
--- a/src/Doc/JEdit/JEdit.thy Wed Feb 10 15:49:05 2016 +0100
+++ b/src/Doc/JEdit/JEdit.thy Fri Feb 12 22:36:48 2016 +0100
@@ -1016,16 +1016,15 @@
text \<open>
The \<^emph>\<open>Query\<close> panel provides various GUI forms to request extra information
- from the prover. In old times the user would have issued some diagnostic
- command like @{command find_theorems} and inspected its output, but this is
- now integrated into the Prover IDE.
+ from the prover, as a replacement of old-style diagnostic commands like
+ @{command find_theorems}. There are input fields and buttons for a
+ particular query command, with output in a dedicated text area.
- A \<^emph>\<open>Query\<close> window provides some input fields and buttons for a particular
- query command, with output in a dedicated text area. There are various query
- modes: \<^emph>\<open>Find Theorems\<close>, \<^emph>\<open>Find Constants\<close>, \<^emph>\<open>Print Context\<close>, e.g.\ see
- \figref{fig:query}. As usual in jEdit, multiple \<^emph>\<open>Query\<close> windows may be
- active at the same time: any number of floating instances, but at most one
- docked instance (which is used by default).
+ The main query modes are presented as separate tabs: \<^emph>\<open>Find Theorems\<close>,
+ \<^emph>\<open>Find Constants\<close>, \<^emph>\<open>Print Context\<close>, e.g.\ see \figref{fig:query}. As usual
+ in jEdit, multiple \<^emph>\<open>Query\<close> windows may be active at the same time: any
+ number of floating instances, but at most one docked instance (which is used
+ by default).
\begin{figure}[!htb]
\begin{center}
@@ -1101,20 +1100,20 @@
The \<^emph>\<open>Query\<close> panel in \<^emph>\<open>Print Context\<close> mode prints information from the
theory or proof context, or proof state. See also the Isar commands
@{command_ref print_context}, @{command_ref print_cases}, @{command_ref
- print_term_bindings}, @{command_ref print_theorems}, @{command_ref
- print_state} described in @{cite "isabelle-isar-ref"}.
+ print_term_bindings}, @{command_ref print_theorems}, described in @{cite
+ "isabelle-isar-ref"}.
\<close>
section \<open>Tooltips and hyperlinks \label{sec:tooltips-hyperlinks}\<close>
text \<open>
- Formally processed text (prover input or output) contains rich markup
- information that can be explored further by using the \<^verbatim>\<open>CONTROL\<close> modifier
- key on Linux and Windows, or \<^verbatim>\<open>COMMAND\<close> on Mac OS X. Hovering with the mouse
- while the modifier is pressed reveals a \<^emph>\<open>tooltip\<close> (grey box over the text
- with a yellow popup) and/or a \<^emph>\<open>hyperlink\<close> (black rectangle over the text
- with change of mouse pointer); see also \figref{fig:tooltip}.
+ Formally processed text (prover input or output) contains rich markup that
+ can be explored by using the \<^verbatim>\<open>CONTROL\<close> modifier key on Linux and Windows,
+ or \<^verbatim>\<open>COMMAND\<close> on Mac OS X. Hovering with the mouse while the modifier is
+ pressed reveals a \<^emph>\<open>tooltip\<close> (grey box over the text with a yellow popup)
+ and/or a \<^emph>\<open>hyperlink\<close> (black rectangle over the text with change of mouse
+ pointer); see also \figref{fig:tooltip}.
\begin{figure}[!htb]
\begin{center}
@@ -1124,7 +1123,7 @@
\label{fig:tooltip}
\end{figure}
- Tooltip popups use the same rendering mechanisms as the main text area, and
+ Tooltip popups use the same rendering technology as the main text area, and
further tooltips and/or hyperlinks may be exposed recursively by the same
mechanism; see \figref{fig:nested-tooltips}.
@@ -1146,13 +1145,12 @@
a mouse click (while the \<^verbatim>\<open>CONTROL\<close> or \<^verbatim>\<open>COMMAND\<close> modifier key is still
pressed). Such jumps to other text locations are recorded by the
\<^emph>\<open>Navigator\<close> plugin, which is bundled with Isabelle/jEdit and enabled by
- default, including navigation arrows in the main jEdit toolbar.
+ default. There are usually navigation arrows in the main jEdit toolbar.
- Also note that the link target may be a file that is itself not subject to
- formal document processing of the editor session and thus prevents further
+ Note that the link target may be a file that is itself not subject to formal
+ document processing of the editor session and thus prevents further
exploration: the chain of hyperlinks may end in some source file of the
- underlying logic image, or within the ML bootstrap sources of
- Isabelle/Pure.
+ underlying logic image, or within the ML bootstrap sources of Isabelle/Pure.
\<close>
@@ -1263,6 +1261,17 @@
syntax keyword. Non-word abbreviations like \<^verbatim>\<open>-->\<close> are inserted more
aggressively, except for single-character abbreviations like \<^verbatim>\<open>!\<close> above.
+ Completion via abbreviations like \<^verbatim>\<open>ALL\<close> or \<^verbatim>\<open>-->\<close> depends on the semantic
+ language context (\secref{sec:completion-context}). In contrast, backslash
+ sequences like \<^verbatim>\<open>\forall\<close> \<^verbatim>\<open>\<forall>\<close> are always possible, but require
+ additional interaction to confirm (via popup).
+
+ The latter is important in ambiguous situations, e.g.\ for Isabelle document
+ source, which may contain formal symbols or informal {\LaTeX} macros.
+ Backslash sequences also help when input is broken, and thus escapes its
+ normal semantic context: e.g.\ antiquotations or string literals in ML,
+ which do not allow arbitrary backslash sequences.
+
\<^medskip>
Additional abbreviations may be specified in @{file
"$ISABELLE_HOME/etc/abbrevs"} and @{file_unchecked
@@ -1272,13 +1281,6 @@
than just one symbol; otherwise the meaning is the same as a symbol
specification ``\<open>sym\<close>~\<^verbatim>\<open>abbrev:\<close>~\<open>abbrev\<close>'' within @{file_unchecked
"etc/symbols"}.
-
- \<^medskip>
- Symbol completion depends on the semantic language context
- (\secref{sec:completion-context}), to enable or disable that aspect for a
- particular sub-language of Isabelle. For example, symbol completion is
- suppressed within document source to avoid confusion with {\LaTeX} macros
- that use similar notation.
\<close>
@@ -1310,13 +1312,12 @@
subsubsection \<open>File-system paths\<close>
text \<open>
- Depending on prover markup about file-system path specifications in the
- source text, e.g.\ for the argument of a load command
- (\secref{sec:aux-files}), the completion mechanism explores the directory
- content and offers the result as completion popup. Relative path
- specifications are understood wrt.\ the \<^emph>\<open>master directory\<close> of the document
- node (\secref{sec:buffer-node}) of the enclosing editor buffer; this
- requires a proper theory, not an auxiliary file.
+ Depending on prover markup about file-system paths in the source text, e.g.\
+ for the argument of a load command (\secref{sec:aux-files}), the completion
+ mechanism explores the directory content and offers the result as completion
+ popup. Relative path specifications are understood wrt.\ the \<^emph>\<open>master
+ directory\<close> of the document node (\secref{sec:buffer-node}) of the enclosing
+ editor buffer; this requires a proper theory, not an auxiliary file.
A suffix of slashes may be used to continue the exploration of an already
recognized directory name.
@@ -1351,8 +1352,8 @@
\<^medskip>
Dictionary lookup uses some educated guesses about lower-case, upper-case,
and capitalized words. This is oriented on common use in English, where this
- aspect is not decisive for proper spelling, in contrast to German, for
- example.
+ aspect is not decisive for proper spelling (in contrast to German, for
+ example).
\<close>
@@ -1366,22 +1367,17 @@
editor mode (see also \secref{sec:buffer-node}).
The semantic \<^emph>\<open>language context\<close> provides information about nested
- sub-languages of Isabelle: keywords are only completed for outer syntax,
- symbols or antiquotations for languages that support them. E.g.\ there is no
- symbol completion for ML source, but within ML strings, comments,
- antiquotations.
+ sub-languages of Isabelle: keywords are only completed for outer syntax, and
+ antiquotations for languages that support them. Symbol abbreviations only
+ work for specific sub-languages: e.g.\ ``\<^verbatim>\<open>=>\<close>'' is \<^emph>\<open>not\<close> completed in
+ regular ML source, but is completed within ML strings, comments,
+ antiquotations. Backslash representations of symbols like ``\<^verbatim>\<open>\foobar\<close>'' or
+ ``\<^verbatim>\<open>\<foobar>\<close>'' work in any context --- after additional confirmation.
The prover may produce \<^emph>\<open>no completion\<close> markup in exceptional situations, to
tell that some language keywords should be excluded from further completion
- attempts. For example, \<^verbatim>\<open>:\<close> within accepted Isar syntax looses its meaning
- as abbreviation for symbol \<open>\<in>\<close>.
-
- \<^medskip>
- The completion context is \<^emph>\<open>ignored\<close> for built-in templates and symbols in
- their explicit form ``\<^verbatim>\<open>\<foobar>\<close>''; see also
- \secref{sec:completion-varieties}. This allows to complete within broken
- input that escapes its normal semantic context, e.g.\ antiquotations or
- string literals in ML, which do not allow arbitrary backslash sequences.
+ attempts. For example, ``\<^verbatim>\<open>:\<close>'' within accepted Isar syntax looses its
+ meaning as abbreviation for symbol ``\<open>\<in>\<close>''.
\<close>
@@ -1420,7 +1416,7 @@
(enabled by default) controls whether replacement text should be inserted
immediately without popup, regardless of @{system_option
jedit_completion_delay}. This aggressive mode of completion is restricted
- to Isabelle symbols and their abbreviations (\secref{sec:symbols}).
+ to symbol abbreviations that are not plain words (\secref{sec:symbols}).
\<^enum> Completion of symbol abbreviations with only one relevant character in
the text always enforces an explicit popup, regardless of
@@ -1439,7 +1435,7 @@
\<^verbatim>\<open>PAGE_DOWN\<close>, but all other key events are passed to the underlying text
area. This allows to ignore unwanted completions most of the time and
continue typing quickly. Thus the popup serves as a mechanism of
- confirmation of proposed items, but the default is to continue without
+ confirmation of proposed items, while the default is to continue without
completion.
The meaning of special keys is as follows:
@@ -1534,7 +1530,7 @@
A @{system_option jedit_completion_delay}~\<^verbatim>\<open>> 0\<close> postpones the processing of
key events, until after the user has stopped typing for the given time span,
- but @{system_option jedit_completion_immediate}~\<^verbatim>\<open>"= true\<close> means that
+ but @{system_option jedit_completion_immediate}~\<^verbatim>\<open>= true\<close> means that
abbreviations of Isabelle symbols are handled nonetheless.
\<^item> @{system_option_def jedit_completion_path_ignore} specifies ``glob''
@@ -1562,10 +1558,10 @@
text \<open>
Continuous document processing works asynchronously in the background.
Visible document source that has been evaluated may get augmented by
- additional results of \<^emph>\<open>asynchronous print functions\<close>. The canonical example
- is proof state output, which is always enabled. More heavy-weight print
- functions may be applied, in order to prove or disprove parts of the formal
- text by other means.
+ additional results of \<^emph>\<open>asynchronous print functions\<close>. An example for that
+ is proof state output, if that is enabled in the Output panel
+ (\secref{sec:output}). More heavy-weight print functions may be applied as
+ well, e.g.\ to prove or disprove parts of the formal text by other means.
Isabelle/HOL provides various automatically tried tools that operate on
outermost goal statements (e.g.\ @{command lemma}, @{command theorem}),
@@ -1575,8 +1571,8 @@
information sign in the gutter (see \figref{fig:auto-tools}). The message
content may be shown as for other output (see also \secref{sec:output}).
Some tools produce output with \<^emph>\<open>sendback\<close> markup, which means that clicking
- on certain parts of the output inserts that text into the source in the
- proper place.
+ on certain parts of the text inserts that into the source in the proper
+ place.
\begin{figure}[!htb]
\begin{center}
@@ -1722,8 +1718,11 @@
section \<open>Markdown structure\<close>
text \<open>
- FIXME
- \figref{fig:markdown-document}
+ Document text is internally structured in paragraphs and nested lists, using
+ notation that is similar to Markdown\<^footnote>\<open>@{url "http://commonmark.org"}\<close>. There
+ are special control symbols for items of different kinds of lists,
+ corresponding to \<^verbatim>\<open>itemize\<close>, \<^verbatim>\<open>enumerate\<close>, \<^verbatim>\<open>description\<close> in {\LaTeX}. This
+ is illustrated in for \<^verbatim>\<open>itemize\<close> in \figref{fig:markdown-document}.
\begin{figure}[!htb]
\begin{center}
@@ -1732,6 +1731,12 @@
\caption{Markdown structure within document text}
\label{fig:markdown-document}
\end{figure}
+
+ Items take colour according to the depth of nested lists. This helps to
+ explore the implicit rules for list structure interactively. There is also
+ markup for individual paragraphs in the text: it may be explored via mouse
+ hovering with \<^verbatim>\<open>CONTROL\<close> / \<^verbatim>\<open>COMMAND\<close> as usual
+ (\secref{sec:tooltips-hyperlinks}).
\<close>
@@ -1774,19 +1779,95 @@
\<close>
-chapter \<open>ML debugger\<close>
+chapter \<open>ML debugging within the Prover IDE\<close>
text \<open>
- FIXME
- \figref{fig:ml-debugger}
+ Isabelle/ML is based on Poly/ML\<^footnote>\<open>@{url "http://www.polyml.org"}\<close> and thus
+ benefits from the source-level debugger of that implementation of Standard
+ ML. The Prover IDE provides the \<^emph>\<open>Debugger\<close> dockable to connect to running
+ ML threads, inspect the stack frame with local ML bindings, and evaluate ML
+ expressions in a particular run-time context. A typical debugger session is
+ shown in \figref{fig:ml-debugger}.
+
+ ML debugging depends on the following pre-requisites.
+
+ \<^enum> ML source needs to be compiled with debugging enabled. This may be
+ controlled for particular chunks of ML sources using any of the subsequent
+ facilities.
+
+ \<^enum> The system option @{system_option_ref ML_debugger} as implicit state
+ of the Isabelle process. It may be changed in the menu \<^emph>\<open>Plugins /
+ Plugin Options / Isabelle / General\<close>. ML modules need to be reloaded and
+ recompiled to pick up that option as intended.
+
+ \<^enum> The configuration option @{attribute_ref ML_debugger}, with an
+ attribute of the same name, to update a global or local context (e.g.\
+ with the @{command declare} command).
+
+ \<^enum> Commands that modify @{attribute ML_debugger} state for individual
+ files: @{command_ref ML_file_debug}, @{command_ref ML_file_no_debug},
+ @{command_ref SML_file_debug}, @{command_ref SML_file_no_debug}.
+
+ The instrumentation of ML code for debugging causes minor run-time
+ overhead. ML modules that implement critical system infrastructure may
+ lead to deadlocks or other undefined behaviour, when put under debugger
+ control!
+
+ \<^enum> The \<^emph>\<open>Debugger\<close> panel needs to be active, otherwise the program ignores
+ debugger instrumentation of the compiler and runs unmanaged. It is also
+ possible to start debugging with the panel open, and later undock it, to
+ let the program continue unhindered.
+
+ \<^enum> The ML program needs to be stopped at a suitable breakpoint, which may
+ be activated individually or globally as follows.
+
+ For ML sources that have been compiled with debugger support, the IDE
+ visualizes possible breakpoints in the text. A breakpoint may be toggled
+ by pointing accurately with the mouse, with a right-click to activate
+ jEdit's context menu and its \<^emph>\<open>Toggle Breakpoint\<close> item. Alternatively, the
+ \<^emph>\<open>Break\<close> checkbox in the \<^emph>\<open>Debugger\<close> panel may be enabled to stop ML
+ threads always at the next possible breakpoint.
+
+ Note that the state of individual breakpoints \<^emph>\<open>gets lost\<close> when the
+ coresponding ML source is re-compiled! This may happen unintentionally,
+ e.g.\ when following hyperlinks into ML modules that have not been loaded
+ into the IDE before.
\begin{figure}[!htb]
\begin{center}
\includegraphics[scale=0.333]{ml-debugger}
\end{center}
- \caption{ML debugger}
+ \caption{ML debugger session}
\label{fig:ml-debugger}
\end{figure}
+
+ The debugger panel (\figref{fig:ml-debugger}) shows a list of all threads
+ that are presently stopped. Each thread shows a stack of all function
+ invocations that lead to the current breakpoint at the top.
+
+ It is possible to jump between stack positions freely, by clicking on this
+ list. The current situation is displayed in the big output window, as a
+ local ML environment with names and printed values.
+
+ ML expressions may be evaluated in the current context by entering snippets
+ of source into the text fields labeled \<open>Context\<close> and \<open>ML\<close>, and pushing the
+ \<open>Eval\<close> button. By default, the source is interpreted as Isabelle/ML with the
+ usual support for antiquotations (like @{command ML}, @{command ML_file}).
+ Alternatively, strict Standard ML may be enforced via the \<^emph>\<open>SML\<close> checkbox
+ (like @{command SML_file}).
+
+ The context for Isabelle/ML is optional, it may evaluate to a value of type
+ @{ML_type theory}, @{ML_type Proof.context}, or @{ML_type Context.generic}.
+ Thus the given ML expression (with its antiquotations) may be subject to the
+ intended dynamic run-time context, instead of the static compile-time
+ context.
+
+ \<^medskip>
+ The buttons labeled \<^emph>\<open>Continue\<close>, \<^emph>\<open>Step\<close>, \<^emph>\<open>Step over\<close>, \<^emph>\<open>Step out\<close>
+ recommence execution of the program, with different policies concerning
+ nested function invocations. The debugger always moves the cursor within the
+ ML source to the next breakpoint position, and offers new stack frames as
+ before.
\<close>
@@ -1812,10 +1893,10 @@
It is also possible to reveal individual timing information via some tooltip
for the corresponding command keyword, using the technique of mouse hovering
- with \<^verbatim>\<open>CONTROL\<close>~/ \<^verbatim>\<open>COMMAND\<close> modifier key as explained in
- \secref{sec:tooltips-hyperlinks}. Actual display of timing depends on the
- global option @{system_option_ref jedit_timing_threshold}, which can be
- configured in \<^emph>\<open>Plugin Options~/ Isabelle~/ General\<close>.
+ with \<^verbatim>\<open>CONTROL\<close>~/ \<^verbatim>\<open>COMMAND\<close> modifier (\secref{sec:tooltips-hyperlinks}).
+ Actual display of timing depends on the global option @{system_option_ref
+ jedit_timing_threshold}, which can be configured in \<^emph>\<open>Plugin Options~/
+ Isabelle~/ General\<close>.
\<^medskip>
The \<^emph>\<open>Monitor\<close> panel visualizes various data collections about recent
@@ -1831,11 +1912,11 @@
section \<open>Low-level output\<close>
text \<open>
- Prover output is normally shown directly in the main text area or secondary
- \<^emph>\<open>Output\<close> panels, as explained in \secref{sec:output}.
-
- Beyond this, it is occasionally useful to inspect low-level output channels
- via some of the following additional panels:
+ Prover output is normally shown directly in the main text area or specific
+ panels like \<^emph>\<open>Output\<close> (\secref{sec:output}) or \<^emph>\<open>State\<close>
+ (\secref{sec:state-output}). Beyond this, it is occasionally useful to
+ inspect low-level output channels via some of the following additional
+ panels:
\<^item> \<^emph>\<open>Protocol\<close> shows internal messages between the Isabelle/Scala and
Isabelle/ML side of the PIDE document editing protocol. Recording of
@@ -1914,8 +1995,16 @@
\<^item> \<^bold>\<open>Problem:\<close> Mac OS X system fonts sometimes lead to character drop-outs in
the main text area.
- \<^bold>\<open>Workaround:\<close> Use the default \<^verbatim>\<open>IsabelleText\<close> font. (Do not install that
- font on the system.)
+ \<^bold>\<open>Workaround:\<close> Use the default \<^verbatim>\<open>IsabelleText\<close> font.
+
+ \<^item> \<^bold>\<open>Problem:\<close> Mac OS X with Retina display has problems to determine the
+ font metrics of \<^verbatim>\<open>IsabelleText\<close> accurately, notably in plain Swing text
+ fields (e.g.\ in the \<^emph>\<open>Search and Replace\<close> dialog).
+
+ \<^bold>\<open>Workaround:\<close> Install \<^verbatim>\<open>IsabelleText\<close> and \<^verbatim>\<open>IsabelleTextBold\<close> on the system
+ with \<^emph>\<open>Font Book\<close>, despite the warnings in \secref{sec:symbols} against
+ that! The \<^verbatim>\<open>.ttf\<close> font files reside in some directory @{file_unchecked
+ "$ISABELLE_HOME/contrib/isabelle_fonts-XYZ"}.
\<^item> \<^bold>\<open>Problem:\<close> Some Linux/X11 input methods such as IBus tend to disrupt key
event handling of Java/AWT/Swing.
--- a/src/Doc/ROOT Wed Feb 10 15:49:05 2016 +0100
+++ b/src/Doc/ROOT Fri Feb 12 22:36:48 2016 +0100
@@ -126,7 +126,7 @@
"root.tex"
session Implementation (doc) in "Implementation" = "HOL-Proofs" +
- options [document_variants = "implementation", quick_and_dirty]
+ options [condition = ML_SYSTEM_POLYML, document_variants = "implementation", quick_and_dirty]
theories
Eq
Integration
--- a/src/Doc/manual.bib Wed Feb 10 15:49:05 2016 +0100
+++ b/src/Doc/manual.bib Fri Feb 12 22:36:48 2016 +0100
@@ -306,6 +306,12 @@
series = LNCS,
publisher = Springer}
+@manual{isabelle-datatypes,
+ author = {Julian Biendarra and Jasmin Christian Blanchette and Martin Desharnais and Lorenz Panny and Andrei Popescu and Dmitriy Traytel},
+ title = {Defining (Co)datatypes and Primitively (Co)recursive Functions in {Isabelle\slash HOL}},
+ institution = {TU Munich},
+ note = {\url{http://isabelle.in.tum.de/doc/datatypes.pdf}}}
+
@book{Bird-Wadler,author="Richard Bird and Philip Wadler",
title="Introduction to Functional Programming",publisher=PH,year=1988}
@@ -373,12 +379,6 @@
pages = "93--110"
}
-@manual{isabelle-datatypes,
- author = {Jasmin Christian Blanchette and Martin Desharnais and Lorenz Panny and Andrei Popescu and Dmitriy Traytel},
- title = {Defining (Co)datatypes in Isabelle/HOL},
- institution = {TU Munich},
- note = {\url{http://isabelle.in.tum.de/doc/datatypes.pdf}}}
-
@inproceedings{why3,
author = {Fran\c{c}ois Bobot and Jean-Christophe Filli\^atre and Claude March\'e and Andrei Paskevich},
title = {{Why3}: Shepherd Your Herd of Provers},
@@ -1121,6 +1121,22 @@
year = 1984,
publisher = {Bibliopolis}}
+@inproceedings{Matichuk-et-al:2014,
+ author = {Daniel Matichuk and Makarius Wenzel and Toby C. Murray},
+ title = {An {Isabelle} Proof Method Language},
+ editor = {Gerwin Klein and Ruben Gamboa},
+ booktitle = {Interactive Theorem Proving - 5th International Conference, {ITP}
+ 2014, Held as Part of the Vienna Summer of Logic, {VSL} 2014, Vienna,
+ Austria},
+ year = {2014},
+ url = {http://dx.doi.org/10.1007/978-3-319-08970-6_25},
+ doi = {10.1007/978-3-319-08970-6_25},
+ series = LNCS,
+ volume = {8558},
+ publisher = {Springer},
+ year = {2014},
+}
+
@incollection{melham89,
author = {Thomas F. Melham},
title = {Automating Recursive Type Definitions in Higher Order
--- a/src/HOL/Isar_Examples/Cantor.thy Wed Feb 10 15:49:05 2016 +0100
+++ b/src/HOL/Isar_Examples/Cantor.thy Fri Feb 12 22:36:48 2016 +0100
@@ -71,6 +71,7 @@
from * have "\<exists>x. ?D = f x" ..
then obtain a where "?D = f a" ..
then have "?D a \<longleftrightarrow> f a a" by (rule arg_cong)
+ then have "\<not> f a a \<longleftrightarrow> f a a" .
then show False by (rule iff_contradiction)
qed
--- a/src/HOL/Isar_Examples/Higher_Order_Logic.thy Wed Feb 10 15:49:05 2016 +0100
+++ b/src/HOL/Isar_Examples/Higher_Order_Logic.thy Fri Feb 12 22:36:48 2016 +0100
@@ -282,6 +282,7 @@
from * have "\<exists>x. ?D = f x" ..
then obtain a where "?D = f a" ..
then have "?D a \<longleftrightarrow> f a a" using refl by (rule subst)
+ then have "\<not> f a a \<longleftrightarrow> f a a" .
then show \<bottom> by (rule iff_contradiction)
qed
--- a/src/HOL/Mirabelle/lib/scripts/mirabelle.pl Wed Feb 10 15:49:05 2016 +0100
+++ b/src/HOL/Mirabelle/lib/scripts/mirabelle.pl Fri Feb 12 22:36:48 2016 +0100
@@ -157,8 +157,11 @@
if ($output_log) { print "Mirabelle: $thy_file\n"; }
-my $result = system "\"$ENV{'ISABELLE_PROCESS'}\" " .
- "-o quick_and_dirty -e 'Multithreading.max_threads_setmp 1 use_thy \"$path/$new_thy_name\" handle _ => exit 1;\n' -q $mirabelle_logic" . $quiet;
+my $cmd =
+ "\"$ENV{'ISABELLE_PROCESS'}\" " .
+ "-o quick_and_dirty -e 'Multithreading.max_threads_setmp 1 use_thy \"$path/$new_thy_name\" handle _ => exit 1;\n' -q $mirabelle_logic" .
+ $quiet;
+my $result = system "bash", "-c", $cmd;
if ($output_log) {
my $outcome = ($result ? "failure" : "success");
--- a/src/HOL/ROOT Wed Feb 10 15:49:05 2016 +0100
+++ b/src/HOL/ROOT Fri Feb 12 22:36:48 2016 +0100
@@ -18,7 +18,7 @@
description {*
HOL-Main with explicit proof terms.
*}
- options [document = false, quick_and_dirty = false]
+ options [condition = ML_SYSTEM_POLYML, document = false, quick_and_dirty = false]
theories Proofs (*sequential change of global flag!*)
theories "~~/src/HOL/Library/Old_Datatype"
files
@@ -252,17 +252,17 @@
Generate_Target_Nat
Generate_Efficient_Datastructures
Generate_Pretty_Char
- theories [condition = ISABELLE_GHC]
+ theories [condition = "ML_SYSTEM_POLYML,ISABELLE_GHC"]
Code_Test_GHC
- theories [condition = ISABELLE_MLTON]
+ theories [condition = "ML_SYSTEM_POLYML,ISABELLE_MLTON"]
Code_Test_MLton
- theories [condition = ISABELLE_OCAMLC]
+ theories [condition = "ML_SYSTEM_POLYML,ISABELLE_OCAMLC"]
Code_Test_OCaml
- theories [condition = ISABELLE_POLYML]
+ theories [condition = "ML_SYSTEM_POLYML,ISABELLE_POLYML"]
Code_Test_PolyML
- theories [condition = ISABELLE_SCALA]
+ theories [condition = "ML_SYSTEM_POLYML,ISABELLE_SCALA"]
Code_Test_Scala
- theories [condition = ISABELLE_SMLNJ]
+ theories [condition = "ML_SYSTEM_POLYML,ISABELLE_SMLNJ"]
Code_Test_SMLNJ
session "HOL-Metis_Examples" in Metis_Examples = HOL +
@@ -398,7 +398,7 @@
theories Decision_Procs
session "HOL-Proofs-ex" in "Proofs/ex" = "HOL-Proofs" +
- options [document = false, parallel_proofs = 0]
+ options [condition = ML_SYSTEM_POLYML, document = false, parallel_proofs = 0]
theories
Hilbert_Classical
XML_Data
@@ -432,7 +432,8 @@
The paper "More Church-Rosser Proofs (in Isabelle/HOL)" describes the whole
theory (see http://www.in.tum.de/~nipkow/pubs/jar2001.html).
*}
- options [print_mode = "no_brackets", parallel_proofs = 0, quick_and_dirty = false]
+ options [condition = ML_SYSTEM_POLYML, print_mode = "no_brackets",
+ parallel_proofs = 0, quick_and_dirty = false]
theories [document = false]
"~~/src/HOL/Library/Code_Target_Int"
theories
@@ -845,7 +846,7 @@
theories Ex
session "HOL-Word-SMT_Examples" in SMT_Examples = "HOL-Word" +
- options [document = false, quick_and_dirty]
+ options [condition = ML_SYSTEM_POLYML, document = false, quick_and_dirty]
theories
Boogie
SMT_Examples
@@ -992,7 +993,7 @@
session "HOL-Predicate_Compile_Examples" in Predicate_Compile_Examples = HOL +
options [document = false]
- theories
+ theories [condition = ML_SYSTEM_POLYML]
Examples
Predicate_Compile_Tests
Predicate_Compile_Quickcheck_Examples
@@ -1003,13 +1004,13 @@
Hotel_Example_Small_Generator *)
IMP_3
IMP_4
- theories [condition = "ISABELLE_SWIPL"]
+ theories [condition = ISABELLE_SWIPL]
Code_Prolog_Examples
Context_Free_Grammar_Example
Hotel_Example_Prolog
Lambda_Example
List_Examples
- theories [condition = "ISABELLE_SWIPL", quick_and_dirty]
+ theories [condition = ISABELLE_SWIPL, quick_and_dirty]
Reg_Exp_Example
session HOLCF (main) in HOLCF = HOL +
--- a/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML Wed Feb 10 15:49:05 2016 +0100
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML Fri Feb 12 22:36:48 2016 +0100
@@ -1070,9 +1070,7 @@
rec_inf_tac)
end)
fun ignore_interpretation_exn f x = SOME (f x)
- handle
- INTERPRET_INFERENCE => NONE
- | exn => reraise exn
+ handle INTERPRET_INFERENCE => NONE
in
if List.null skel then
raise SKELETON
--- a/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy Wed Feb 10 15:49:05 2016 +0100
+++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy Fri Feb 12 22:36:48 2016 +0100
@@ -875,8 +875,8 @@
in
use_candidate target_ty params' (candidate_param :: acc) val_ty
end
- handle TYPE ("dest_funT", _, _) => NONE
- | DEST_LIST => NONE
+ handle TYPE ("dest_funT", _, _) => NONE (* FIXME fragile *)
+ | _ => NONE (* FIXME avoid catch-all handler *)
val (skolem_const_ty, params') = skolem_const_info_of conclusion
--- a/src/HOL/ex/Cubic_Quartic.thy Wed Feb 10 15:49:05 2016 +0100
+++ b/src/HOL/ex/Cubic_Quartic.thy Fri Feb 12 22:36:48 2016 +0100
@@ -2,7 +2,7 @@
Author: Amine Chaieb
*)
-header "The Cubic and Quartic Root Formulas"
+section "The Cubic and Quartic Root Formulas"
theory Cubic_Quartic
imports Complex_Main
--- a/src/HOL/ex/Pythagoras.thy Wed Feb 10 15:49:05 2016 +0100
+++ b/src/HOL/ex/Pythagoras.thy Fri Feb 12 22:36:48 2016 +0100
@@ -2,7 +2,7 @@
Author: Amine Chaieb
*)
-header "The Pythagorean Theorem"
+section "The Pythagorean Theorem"
theory Pythagoras
imports Complex_Main
--- a/src/Pure/Concurrent/event_timer.ML Wed Feb 10 15:49:05 2016 +0100
+++ b/src/Pure/Concurrent/event_timer.ML Fri Feb 12 22:36:48 2016 +0100
@@ -110,7 +110,7 @@
fun shutdown () =
uninterruptible (fn restore_attributes => fn () =>
- if Synchronized.change_result state (fn st as State {requests, status, manager} =>
+ if Synchronized.change_result state (fn st as State {requests, manager, ...} =>
if is_shutdown Normal st then (false, st)
else if is_shutdown Shutdown_Ack st orelse is_shutdown_req st then
raise Fail "Concurrent attempt to shutdown event timer"
--- a/src/Pure/Concurrent/future.scala Wed Feb 10 15:49:05 2016 +0100
+++ b/src/Pure/Concurrent/future.scala Fri Feb 12 22:36:48 2016 +0100
@@ -88,7 +88,7 @@
status.change(_ => Finished(if (Thread.interrupted) Exn.Exn(Exn.Interrupt()) else result))
}
}
- private val task = Standard_Thread.pool.submit(new Callable[A] { def call = body })
+ private val task = Standard_Thread.pool.submit(new Callable[Unit] { def call = try_run() })
def join_result: Exn.Result[A] =
{
--- a/src/Pure/Concurrent/standard_thread.scala Wed Feb 10 15:49:05 2016 +0100
+++ b/src/Pure/Concurrent/standard_thread.scala Fri Feb 12 22:36:48 2016 +0100
@@ -56,8 +56,7 @@
/* delayed events */
- final class Delay private [Standard_Thread](
- first: Boolean, delay: => Time, cancel: () => Unit, event: => Unit)
+ final class Delay private [Standard_Thread](first: Boolean, delay: => Time, event: => Unit)
{
private var running: Option[Event_Timer.Request] = None
@@ -73,8 +72,8 @@
{
val new_run =
running match {
- case Some(request) => if (first) false else { request.cancel; cancel(); true }
- case None => cancel(); true
+ case Some(request) => if (first) false else { request.cancel; true }
+ case None => true
}
if (new_run)
running = Some(Event_Timer.request(Time.now() + delay)(run))
@@ -83,8 +82,8 @@
def revoke(): Unit = synchronized
{
running match {
- case Some(request) => request.cancel; cancel(); running = None
- case None => cancel()
+ case Some(request) => request.cancel; running = None
+ case None =>
}
}
@@ -94,20 +93,16 @@
case Some(request) =>
val alt_time = Time.now() + alt_delay
if (request.time < alt_time && request.cancel) {
- cancel()
running = Some(Event_Timer.request(alt_time)(run))
}
- else cancel()
- case None => cancel()
+ case None =>
}
}
}
// delayed event after first invocation
- def delay_first(delay: => Time, cancel: () => Unit = () => ())(event: => Unit): Delay =
- new Delay(true, delay, cancel, event)
+ def delay_first(delay: => Time)(event: => Unit): Delay = new Delay(true, delay, event)
// delayed event after last invocation
- def delay_last(delay: => Time, cancel: () => Unit = () => ())(event: => Unit): Delay =
- new Delay(false, delay, cancel, event)
+ def delay_last(delay: => Time)(event: => Unit): Delay = new Delay(false, delay, event)
}
--- a/src/Pure/GUI/gui_thread.scala Wed Feb 10 15:49:05 2016 +0100
+++ b/src/Pure/GUI/gui_thread.scala Fri Feb 12 22:36:48 2016 +0100
@@ -49,9 +49,9 @@
/* delayed events */
- def delay_first(delay: => Time, cancel: () => Unit = () => ())(event: => Unit)
- : Standard_Thread.Delay = Standard_Thread.delay_first(delay, cancel) { later { event } }
+ def delay_first(delay: => Time)(event: => Unit): Standard_Thread.Delay =
+ Standard_Thread.delay_first(delay) { later { event } }
- def delay_last(delay: => Time, cancel: () => Unit = () => ())(event: => Unit)
- : Standard_Thread.Delay = Standard_Thread.delay_last(delay, cancel) { later { event } }
+ def delay_last(delay: => Time)(event: => Unit): Standard_Thread.Delay =
+ Standard_Thread.delay_last(delay) { later { event } }
}
--- a/src/Pure/General/binding.ML Wed Feb 10 15:49:05 2016 +0100
+++ b/src/Pure/General/binding.ML Fri Feb 12 22:36:48 2016 +0100
@@ -31,7 +31,7 @@
val prefix_of: binding -> (string * bool) list
val map_prefix: ((string * bool) list -> (string * bool) list) -> binding -> binding
val prefix: bool -> string -> binding -> binding
- val restricted_default: (bool * scope) option -> binding -> binding
+ val restricted: (bool * scope) option -> binding -> binding
val concealed: binding -> binding
val pretty: binding -> Pretty.T
val print: binding -> string
@@ -135,14 +135,9 @@
(* visibility flags *)
-fun restricted strict scope =
- map_binding (fn (_, concealed, prefix, qualifier, name, pos) =>
- (SOME (strict, scope), concealed, prefix, qualifier, name, pos));
-
-fun restricted_default restricted' =
+fun restricted default =
map_binding (fn (restricted, concealed, prefix, qualifier, name, pos) =>
- (if is_some restricted then restricted else restricted',
- concealed, prefix, qualifier, name, pos));
+ (if is_some restricted then restricted else default, concealed, prefix, qualifier, name, pos));
val concealed =
map_binding (fn (restricted, _, prefix, qualifier, name, pos) =>
--- a/src/Pure/General/completion.scala Wed Feb 10 15:49:05 2016 +0100
+++ b/src/Pure/General/completion.scala Fri Feb 12 22:36:48 2016 +0100
@@ -322,7 +322,9 @@
if path.is_file
entry <- Abbrevs_Parser.parse_file(path)
} yield entry
- symbol_abbrevs ::: more_abbrevs
+ val remove_abbrevs = (for { (a, b) <- more_abbrevs if b == "" } yield a).toSet
+
+ (symbol_abbrevs ::: more_abbrevs).filterNot({ case (a, _) => remove_abbrevs.contains(a) })
}
private val caret_indicator = '\u0007'
--- a/src/Pure/General/name_space.ML Wed Feb 10 15:49:05 2016 +0100
+++ b/src/Pure/General/name_space.ML Fri Feb 12 22:36:48 2016 +0100
@@ -389,7 +389,7 @@
concealed' ? concealed;
fun transform_binding (Naming {restricted, concealed, ...}) =
- Binding.restricted_default restricted #>
+ Binding.restricted restricted #>
concealed ? Binding.concealed;
--- a/src/Pure/General/symbol.scala Wed Feb 10 15:49:05 2016 +0100
+++ b/src/Pure/General/symbol.scala Fri Feb 12 22:36:48 2016 +0100
@@ -255,7 +255,7 @@
tab.get(x) match {
case None => tab += (x -> y)
case Some(z) =>
- error("Duplicate mapping of " + quote(x) + " to " + quote(y) + " vs. " + quote(z))
+ error("Duplicate symbol mapping of " + quote(x) + " to " + quote(y) + " vs. " + quote(z))
}
}
tab
--- a/src/Pure/General/symbol_pos.ML Wed Feb 10 15:49:05 2016 +0100
+++ b/src/Pure/General/symbol_pos.ML Fri Feb 12 22:36:48 2016 +0100
@@ -71,7 +71,7 @@
fun split syms =
(case take_prefix (fn (s, _) => s <> "\n") syms of
(line, []) => [line]
- | (line, nl :: rest) => line :: split rest);
+ | (line, _ :: rest) => line :: split rest);
in split list end;
val trim_blanks = trim (Symbol.is_blank o symbol);
--- a/src/Pure/General/url.scala Wed Feb 10 15:49:05 2016 +0100
+++ b/src/Pure/General/url.scala Fri Feb 12 22:36:48 2016 +0100
@@ -12,6 +12,9 @@
object Url
{
+ def escape(name: String): String =
+ (for (c <- name.iterator) yield if (c == '\'') "%27" else new String(Array(c))).mkString
+
def apply(name: String): URL =
{
try { new URL(name) }
--- a/src/Pure/Isar/named_target.ML Wed Feb 10 15:49:05 2016 +0100
+++ b/src/Pure/Isar/named_target.ML Fri Feb 12 22:36:48 2016 +0100
@@ -86,7 +86,7 @@
| abbrev (locale, false) = Generic_Target.locale_abbrev locale
| abbrev (class, true) = Class.abbrev class;
-fun declaration ("", _) flags decl = Generic_Target.theory_declaration decl
+fun declaration ("", _) _ decl = Generic_Target.theory_declaration decl
| declaration (locale, _) flags decl = Generic_Target.locale_declaration locale flags decl;
fun theory_registration ("", _) = Generic_Target.theory_registration
--- a/src/Pure/Isar/outer_syntax.scala Wed Feb 10 15:49:05 2016 +0100
+++ b/src/Pure/Isar/outer_syntax.scala Fri Feb 12 22:36:48 2016 +0100
@@ -166,9 +166,9 @@
if (tok.is_command) {
if (tok.is_command_kind(keywords, Keyword.theory_goal)) (2, 1)
else if (tok.is_command_kind(keywords, Keyword.theory)) (1, 0)
+ else if (tok.is_command_kind(keywords, Keyword.proof_open)) (y + 2, y + 1)
else if (tok.is_command_kind(keywords, Keyword.PRF_BLOCK == _)) (y + 2, y + 1)
- else if (tok.is_command_kind(keywords, Keyword.QED_BLOCK == _)) (y + 1, y - 3)
- else if (tok.is_command_kind(keywords, Keyword.proof_open)) (y + 2, y + 1)
+ else if (tok.is_command_kind(keywords, Keyword.QED_BLOCK == _)) (y + 1, y - 2)
else if (tok.is_command_kind(keywords, Keyword.proof_close)) (y + 1, y - 1)
else if (tok.is_command_kind(keywords, Keyword.qed_global)) (1, 0)
else (x, y)
--- a/src/Pure/Isar/toplevel.ML Wed Feb 10 15:49:05 2016 +0100
+++ b/src/Pure/Isar/toplevel.ML Fri Feb 12 22:36:48 2016 +0100
@@ -212,10 +212,6 @@
fun reset_presentation (Theory (gthy, _)) = Theory (gthy, NONE)
| reset_presentation node = node;
-fun map_theory f (Theory (gthy, ctxt)) =
- Theory (Context.mapping f (Local_Theory.raw_theory f) gthy, ctxt)
- | map_theory _ node = node;
-
in
fun apply_transaction f g node =
--- a/src/Pure/ML/ml_antiquotations.ML Wed Feb 10 15:49:05 2016 +0100
+++ b/src/Pure/ML/ml_antiquotations.ML Fri Feb 12 22:36:48 2016 +0100
@@ -11,7 +11,7 @@
val _ = Theory.setup
(ML_Antiquotation.value @{binding cartouche}
- (Args.context -- Scan.lift (Parse.position Args.cartouche_input) >> (fn (ctxt, (source, pos)) =>
+ (Scan.lift Args.cartouche_input >> (fn source =>
"Input.source true " ^ ML_Syntax.print_string (Input.text_of source) ^ " " ^
ML_Syntax.atomic (ML_Syntax.print_range (Input.range_of source)))) #>
--- a/src/Pure/PIDE/markup.ML Wed Feb 10 15:49:05 2016 +0100
+++ b/src/Pure/PIDE/markup.ML Fri Feb 12 22:36:48 2016 +0100
@@ -28,7 +28,7 @@
val is_delimited: Properties.T -> bool
val language: {name: string, symbols: bool, antiquotes: bool, delimited: bool} -> T
val language': {name: string, symbols: bool, antiquotes: bool} -> bool -> T
- val language_outer: bool -> T
+ val language_Isar: bool -> T
val language_method: T
val language_attribute: T
val language_sort: bool -> T
@@ -301,7 +301,7 @@
fun language' {name, symbols, antiquotes} delimited =
language {name = name, symbols = symbols, antiquotes = antiquotes, delimited = delimited};
-val language_outer = language' {name = "", symbols = true, antiquotes = false};
+val language_Isar = language' {name = "Isar", symbols = true, antiquotes = false};
val language_method =
language {name = "method", symbols = true, antiquotes = false, delimited = false};
val language_attribute =
--- a/src/Pure/Syntax/syntax_phases.ML Wed Feb 10 15:49:05 2016 +0100
+++ b/src/Pure/Syntax/syntax_phases.ML Fri Feb 12 22:36:48 2016 +0100
@@ -581,7 +581,7 @@
(mark Ts t1 $ mark Ts t2);
in mark [] tm end;
-fun prune_types ctxt tm =
+fun prune_types tm =
let
fun regard t t' seen =
if Type_Annotation.is_omitted (Type_Annotation.fastype_of [] t) then (t, seen)
@@ -651,7 +651,7 @@
in Ast.mk_appl (constrain (c $ Syntax.free x) X) (map ast_of ts) end
| (Const ("_idtdummy", T), ts) =>
Ast.mk_appl (constrain (Syntax.const "_idtdummy") T) (map ast_of ts)
- | (const as Const (c, T), ts) => trans c (Type_Annotation.smash T) ts
+ | (Const (c, T), ts) => trans c (Type_Annotation.smash T) ts
| (t, ts) => Ast.mk_appl (simple_ast_of ctxt t) (map ast_of ts))
and trans a T args = ast_of (trf a ctxt T args)
@@ -672,7 +672,7 @@
in
tm
|> mark_aprop
- |> show_types ? prune_types ctxt
+ |> show_types ? prune_types
|> Variable.revert_bounds ctxt
|> mark_atoms is_syntax_const ctxt
|> ast_of
--- a/src/Pure/System/options.scala Wed Feb 10 15:49:05 2016 +0100
+++ b/src/Pure/System/options.scala Fri Feb 12 22:36:48 2016 +0100
@@ -387,48 +387,52 @@
class Options_Variable
{
- private var options = Options.empty
+ private var options: Option[Options] = None
+
+ def store(new_options: Options): Unit = synchronized { options = Some(new_options) }
- def value: Options = synchronized { options }
- def update(new_options: Options): Unit = synchronized { options = new_options }
+ def value: Options = synchronized {
+ options match {
+ case Some(opts) => opts
+ case None => error("Uninitialized Isabelle system options")
+ }
+ }
- def + (name: String, x: String): Unit = synchronized { options = options + (name, x) }
+ private def upd(f: Options => Options): Unit = synchronized { options = Some(f(value)) }
+
+ def + (name: String, x: String): Unit = upd(opts => opts + (name, x))
class Bool_Access
{
- def apply(name: String): Boolean = synchronized { options.bool(name) }
- def update(name: String, x: Boolean): Unit =
- synchronized { options = options.bool.update(name, x) }
+ def apply(name: String): Boolean = value.bool(name)
+ def update(name: String, x: Boolean): Unit = upd(opts => opts.bool.update(name, x))
}
val bool = new Bool_Access
class Int_Access
{
- def apply(name: String): Int = synchronized { options.int(name) }
- def update(name: String, x: Int): Unit =
- synchronized { options = options.int.update(name, x) }
+ def apply(name: String): Int = value.int(name)
+ def update(name: String, x: Int): Unit = upd(opts => opts.int.update(name, x))
}
val int = new Int_Access
class Real_Access
{
- def apply(name: String): Double = synchronized { options.real(name) }
- def update(name: String, x: Double): Unit =
- synchronized { options = options.real.update(name, x) }
+ def apply(name: String): Double = value.real(name)
+ def update(name: String, x: Double): Unit = upd(opts => opts.real.update(name, x))
}
val real = new Real_Access
class String_Access
{
- def apply(name: String): String = synchronized { options.string(name) }
- def update(name: String, x: String): Unit =
- synchronized { options = options.string.update(name, x) }
+ def apply(name: String): String = value.string(name)
+ def update(name: String, x: String): Unit = upd(opts => opts.string.update(name, x))
}
val string = new String_Access
class Seconds_Access
{
- def apply(name: String): Time = synchronized { options.seconds(name) }
+ def apply(name: String): Time = value.seconds(name)
}
val seconds = new Seconds_Access
}
--- a/src/Pure/Thy/document_antiquotations.ML Wed Feb 10 15:49:05 2016 +0100
+++ b/src/Pure/Thy/document_antiquotations.ML Fri Feb 12 22:36:48 2016 +0100
@@ -87,7 +87,7 @@
let
val _ =
Context_Position.report ctxt (Input.pos_of source)
- (Markup.language_outer (Input.is_delimited source));
+ (Markup.language_Isar (Input.is_delimited source));
val keywords = Thy_Header.get_keywords' ctxt;
val toks =
@@ -217,7 +217,9 @@
Theory.setup
(entity_antiquotation @{binding command} Outer_Syntax.check_command
(enclose "\\isacommand{" "}" o Output.output) #>
- entity_antiquotation @{binding method} Method.check_name Output.output #>
- entity_antiquotation @{binding attribute} Attrib.check_name Output.output);
+ entity_antiquotation @{binding method} Method.check_name
+ (enclose "\\isa{" "}" o Output.output) #>
+ entity_antiquotation @{binding attribute} Attrib.check_name
+ (enclose "\\isa{" "}" o Output.output));
end;
--- a/src/Pure/Tools/check_source.scala Wed Feb 10 15:49:05 2016 +0100
+++ b/src/Pure/Tools/check_source.scala Fri Feb 12 22:36:48 2016 +0100
@@ -44,7 +44,7 @@
Isabelle_System.hg("--repository " + File.shell_path(root) + " root").check_error
for {
file <- Isabelle_System.hg("manifest", root).check_error.out_lines
- if file.endsWith(".thy") || file.endsWith(".ML")
+ if file.endsWith(".thy") || file.endsWith(".ML") || file.endsWith("/ROOT")
} check_file(root + Path.explode(file))
}
--- a/src/Pure/Tools/main.scala Wed Feb 10 15:49:05 2016 +0100
+++ b/src/Pure/Tools/main.scala Fri Feb 12 22:36:48 2016 +0100
@@ -105,6 +105,7 @@
val env = env0.asInstanceOf[java.util.Map[String, String]]
env.put("ISABELLE_HOME", File.platform_path(isabelle_home))
env.put("ISABELLE_HOME_USER", File.platform_path(isabelle_home_user))
+ env.remove("ISABELLE_ROOT")
}
}
--- a/src/Tools/jEdit/src/context_menu.scala Wed Feb 10 15:49:05 2016 +0100
+++ b/src/Tools/jEdit/src/context_menu.scala Fri Feb 12 22:36:48 2016 +0100
@@ -21,22 +21,23 @@
class Context_Menu extends DynamicContextMenuService
{
def createMenu(text_area: JEditTextArea, evt: MouseEvent): Array[JMenuItem] =
- {
- PIDE.dismissed_popups(text_area.getView)
+ if (evt == null) null
+ else {
+ PIDE.dismissed_popups(text_area.getView)
- val items1 =
- if (evt != null && evt.getSource == text_area.getPainter) {
- val offset = text_area.xyToOffset(evt.getX, evt.getY)
- if (offset >= 0)
- Spell_Checker.context_menu(text_area, offset) :::
- Debugger_Dockable.context_menu(text_area, offset)
+ val items1 =
+ if (evt != null && evt.getSource == text_area.getPainter) {
+ val offset = text_area.xyToOffset(evt.getX, evt.getY)
+ if (offset >= 0)
+ Spell_Checker.context_menu(text_area, offset) :::
+ Debugger_Dockable.context_menu(text_area, offset)
+ else Nil
+ }
else Nil
- }
- else Nil
+
+ val items2 = Bibtex_JEdit.context_menu(text_area)
- val items2 = Bibtex_JEdit.context_menu(text_area)
-
- val items = items1 ::: items2
- if (items.isEmpty) null else items.toArray
+ val items = items1 ::: items2
+ if (items.isEmpty) null else items.toArray
}
}
--- a/src/Tools/jEdit/src/document_model.scala Wed Feb 10 15:49:05 2016 +0100
+++ b/src/Tools/jEdit/src/document_model.scala Fri Feb 12 22:36:48 2016 +0100
@@ -309,6 +309,7 @@
for (text_area <- JEdit_Lib.jedit_text_areas(buffer))
Untyped.method(Class.forName("org.gjt.sp.jedit.textarea.TextArea"), "foldStructureChanged").
invoke(text_area)
+ buffer.invalidateCachedFoldLevels
}
private def init_token_marker()
--- a/src/Tools/jEdit/src/jedit_editor.scala Wed Feb 10 15:49:05 2016 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala Fri Feb 12 22:36:48 2016 +0100
@@ -223,7 +223,7 @@
val external = true
def follow(view: View): Unit =
Standard_Thread.fork("hyperlink_url") {
- try { Isabelle_System.open(name) }
+ try { Isabelle_System.open(Url.escape(name)) }
catch {
case exn: Throwable =>
GUI_Thread.later {
--- a/src/Tools/jEdit/src/jedit_lib.scala Wed Feb 10 15:49:05 2016 +0100
+++ b/src/Tools/jEdit/src/jedit_lib.scala Fri Feb 12 22:36:48 2016 +0100
@@ -16,7 +16,7 @@
import scala.annotation.tailrec
import scala.util.parsing.input.CharSequenceReader
-import org.gjt.sp.jedit.{jEdit, Buffer, View, GUIUtilities, Debug}
+import org.gjt.sp.jedit.{jEdit, Buffer, View, GUIUtilities, Debug, EditPane}
import org.gjt.sp.jedit.gui.KeyEventWorkaround
import org.gjt.sp.jedit.buffer.{JEditBuffer, LineManager}
import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaPainter}
@@ -130,6 +130,10 @@
def jedit_views(): Iterator[View] = jEdit.getViews().iterator
+ def jedit_edit_panes(view: View): Iterator[EditPane] =
+ if (view == null) Iterator.empty
+ else view.getEditPanes().iterator.filter(_ != null)
+
def jedit_text_areas(view: View): Iterator[JEditTextArea] =
if (view == null) Iterator.empty
else view.getEditPanes().iterator.filter(_ != null).map(_.getTextArea).filter(_ != null)
--- a/src/Tools/jEdit/src/jedit_options.scala Wed Feb 10 15:49:05 2016 +0100
+++ b/src/Tools/jEdit/src/jedit_options.scala Fri Feb 12 22:36:48 2016 +0100
@@ -96,7 +96,7 @@
val title = opt_title
def load = text = value.check_name(opt_name).value
def save =
- try { update(value + (opt_name, text)) }
+ try { store(value + (opt_name, text)) }
catch {
case ERROR(msg) =>
GUI.error_dialog(this.peer, "Failed to update options",
--- a/src/Tools/jEdit/src/output_dockable.scala Wed Feb 10 15:49:05 2016 +0100
+++ b/src/Tools/jEdit/src/output_dockable.scala Fri Feb 12 22:36:48 2016 +0100
@@ -129,6 +129,7 @@
Session.Consumer[Any](getClass.getName) {
case _: Session.Global_Options =>
GUI_Thread.later {
+ handle_resize()
output_state_button.selected = output_state
handle_update(do_update, None)
}
--- a/src/Tools/jEdit/src/plugin.scala Wed Feb 10 15:49:05 2016 +0100
+++ b/src/Tools/jEdit/src/plugin.scala Fri Feb 12 22:36:48 2016 +0100
@@ -19,8 +19,8 @@
import org.gjt.sp.jedit.buffer.JEditBuffer
import org.gjt.sp.jedit.syntax.ModeProvider
import org.gjt.sp.jedit.msg.{EditorStarted, BufferUpdate, EditPaneUpdate, PropertiesChanged}
-
import org.gjt.sp.util.SyntaxUtilities
+import org.gjt.sp.util.Log
object PIDE
@@ -377,6 +377,15 @@
}
case msg: PropertiesChanged =>
+ for {
+ view <- JEdit_Lib.jedit_views
+ edit_pane <- JEdit_Lib.jedit_edit_panes(view)
+ } {
+ val buffer = edit_pane.getBuffer
+ val text_area = edit_pane.getTextArea
+ if (buffer != null && text_area != null) PIDE.init_view(buffer, text_area)
+ }
+
PIDE.spell_checker.update(PIDE.options.value)
PIDE.session.update_options(PIDE.options.value)
@@ -391,7 +400,7 @@
Debug.DISABLE_SEARCH_DIALOG_POOL = true
PIDE.plugin = this
- PIDE.options.update(Options.init())
+ PIDE.options.store(Options.init())
PIDE.completion_history.load()
PIDE.spell_checker.update(PIDE.options.value)
@@ -420,6 +429,7 @@
case exn: Throwable =>
PIDE.startup_failure = Some(exn)
PIDE.startup_notified = false
+ Log.log(Log.ERROR, this, exn)
}
}
--- a/src/Tools/jEdit/src/text_overview.scala Wed Feb 10 15:49:05 2016 +0100
+++ b/src/Tools/jEdit/src/text_overview.scala Fri Feb 12 22:36:48 2016 +0100
@@ -72,6 +72,9 @@
private var current_overview = Overview()
private var current_colors: List[(Color, Int, Int)] = Nil
+ private val delay_repaint =
+ GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { repaint() }
+
override def paintComponent(gfx: Graphics)
{
super.paintComponent(gfx)
@@ -83,7 +86,7 @@
val overview = get_overview()
if (rendering.snapshot.is_outdated || overview != current_overview) {
- invoke()
+ delay_repaint.invoke()
gfx.setColor(rendering.outdated_color)
gfx.asInstanceOf[Graphics2D].fill(gfx.getClipBounds)
@@ -103,23 +106,21 @@
/* asynchronous refresh */
- private var future_refresh: Option[Future[Unit]] = None
- private def cancel(): Unit = future_refresh.map(_.cancel)
+ private val future_refresh = Synchronized(Future.value(()))
+ private def is_running(): Boolean = !future_refresh.value.is_finished
def invoke(): Unit = delay_refresh.invoke()
- def revoke(): Unit = delay_refresh.revoke()
+ def revoke(): Unit = { delay_refresh.revoke(); future_refresh.change(x => { x.cancel; x }) }
private val delay_refresh =
- GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay"), cancel _) {
+ GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) {
doc_view.rich_text_area.robust_body(()) {
JEdit_Lib.buffer_lock(buffer) {
val rendering = doc_view.get_rendering()
val overview = get_overview()
- if (rendering.snapshot.is_outdated) invoke()
+ if (rendering.snapshot.is_outdated || is_running()) invoke()
else {
- cancel()
-
val line_offsets =
{
val line_manager = JEdit_Lib.buffer_line_manager(buffer)
@@ -128,8 +129,8 @@
a
}
- future_refresh =
- Some(Future.fork {
+ future_refresh.change(_ =>
+ Future.fork {
val line_count = overview.line_count
val char_count = overview.char_count
val L = overview.L
@@ -170,7 +171,8 @@
current_colors = new_colors
repaint()
}
- })
+ }
+ )
}
}
}