diff --git a/etc/settings b/etc/settings --- a/etc/settings +++ b/etc/settings @@ -1,172 +1,172 @@ # -*- shell-script -*- :mode=shellscript: # # Isabelle system settings. # # Important notes: # * See the "system" manual for explanations on Isabelle settings # * User settings go into $ISABELLE_HOME_USER/etc/settings # * DO NOT EDIT the repository copy of this file! # * DO NOT COPY this file into the $ISABELLE_HOME_USER directory! ### ### Isabelle/Scala ### ISABELLE_JAVA_SYSTEM_OPTIONS="-server -Dfile.encoding=UTF-8 -Disabelle.threads=0 -Djdk.gtk.version=2.2" ISABELLE_TOOL_JAVA_OPTIONS="-Djava.awt.headless=true -Xms512m -Xmx4g -Xss16m" ISABELLE_SCALAC_OPTIONS="-encoding UTF-8 -nowarn -target:jvm-1.8 -Xmax-classfile-name 130 -J-Xms512m -J-Xmx4g -J-Xss16m" classpath "$ISABELLE_HOME/lib/classes/Pure.jar" isabelle_scala_service 'isabelle.Tools' [ -d "$ISABELLE_HOME/Admin" ] && isabelle_scala_service 'isabelle.Admin_Tools' isabelle_scala_service 'isabelle.Functions' isabelle_scala_service 'isabelle.Bibtex$File_Format' #paranoia settings -- avoid intrusion of alien options unset "_JAVA_OPTIONS" unset "JAVA_TOOL_OPTIONS" #paranoia settings -- avoid problems of Java/Swing versus XIM/IBus etc. unset XMODIFIERS ### ### Interactive sessions (cf. isabelle console) ### ISABELLE_LINE_EDITOR="rlwrap" ### ### Batch sessions (cf. isabelle build) ### ISABELLE_BUILD_OPTIONS="" ### ### Document preparation (cf. isabelle latex/document) ### ISABELLE_LATEX="latex -file-line-error" ISABELLE_PDFLATEX="pdflatex -file-line-error" ISABELLE_BIBTEX="bibtex" ISABELLE_MAKEINDEX="makeindex" ISABELLE_EPSTOPDF="epstopdf" if [ "$ISABELLE_PLATFORM_FAMILY" = "windows" ]; then ISABELLE_LATEX="latex -c-style-errors" ISABELLE_PDFLATEX="pdflatex -c-style-errors" fi ### ### Misc path settings ### ISABELLE_COMPONENT_REPOSITORY="https://isabelle.in.tum.de/components" ISABELLE_COMPONENTS_BASE="$USER_HOME/.isabelle/contrib" # The place for user configuration, heap files, etc. if [ -z "$ISABELLE_IDENTIFIER" ]; then ISABELLE_HOME_USER="$USER_HOME/.isabelle" else ISABELLE_HOME_USER="$USER_HOME/.isabelle/$ISABELLE_IDENTIFIER" fi # Where to look for isabelle tools (multiple dirs separated by ':'). ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools" # Location for temporary files (should be on a local file system). ISABELLE_TMP_PREFIX="${TMPDIR:-/tmp}/isabelle-$USER" # Heap locations. ISABELLE_HEAPS="$ISABELLE_HOME_USER/heaps" ISABELLE_HEAPS_SYSTEM="$ISABELLE_HOME/heaps" # HTML browser info. ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info" ISABELLE_BROWSER_INFO_SYSTEM="$ISABELLE_HOME/browser_info" # Site settings check -- just to make it a little bit harder to copy this file verbatim! [ -n "$ISABELLE_SITE_SETTINGS_PRESENT" ] && \ { echo >&2 "### Isabelle site settings already present! Maybe copied etc/settings in full?"; } ISABELLE_SITE_SETTINGS_PRESENT=true ### ### Default logic ### ISABELLE_LOGIC=HOL ### ### Docs ### # Where to look for docs (multiple dirs separated by ':'). ISABELLE_DOCS="$ISABELLE_HOME/doc" ISABELLE_DOCS_RELEASE_NOTES="~~/ANNOUNCE:~~/README:~~/NEWS:~~/COPYRIGHT:~~/CONTRIBUTORS:~~/contrib/README:~~/src/Tools/jEdit/README:~~/README_REPOSITORY" -ISABELLE_DOCS_EXAMPLES="~~/src/HOL/ex/Seq.thy:~~/src/HOL/ex/ML.thy:~~/src/HOL/Unix/Unix.thy:~~/src/HOL/Isar_Examples/Drinker.thy:~~/src/Tools/SML/Examples.thy:~~/src/Pure/ROOT.ML" +ISABELLE_DOCS_EXAMPLES="~~/src/HOL/Examples/Seq.thy:~~/src/HOL/Examples/Drinker.thy:~~/src/HOL/Examples/ML.thy:~~/src/HOL/Unix/Unix.thy:~~/src/Tools/SML/Examples.thy:~~/src/Pure/ROOT.ML" # "open" within desktop environment (potentially asynchronous) case "$ISABELLE_PLATFORM_FAMILY" in linux) ISABELLE_OPEN="xdg-open" ;; macos) ISABELLE_OPEN="open" ;; windows) ISABELLE_OPEN="cygstart" ;; esac PDF_VIEWER="$ISABELLE_OPEN" DVI_VIEWER="$ISABELLE_OPEN" ### ### Symbol rendering ### ISABELLE_SYMBOLS="$ISABELLE_HOME/etc/symbols:$ISABELLE_HOME_USER/etc/symbols" ### ### OCaml ### ISABELLE_OPAM_ROOT="$USER_HOME/.opam" ISABELLE_OCAML_VERSION="ocaml-base-compiler.4.05.0" ### ### Haskell ### ISABELLE_STACK_ROOT="$USER_HOME/.stack" ISABELLE_STACK_RESOLVER="lts-13.19" ISABELLE_GHC_VERSION="ghc-8.6.4" ### ### Misc settings ### ISABELLE_GNUPLOT="gnuplot" ISABELLE_FONTFORGE="fontforge" #ISABELLE_MLTON="/usr/bin/mlton" #ISABELLE_SMLNJ="/usr/bin/sml" #ISABELLE_SWIPL="/usr/bin/swipl" diff --git a/src/Doc/Isar_Ref/Framework.thy b/src/Doc/Isar_Ref/Framework.thy --- a/src/Doc/Isar_Ref/Framework.thy +++ b/src/Doc/Isar_Ref/Framework.thy @@ -1,1031 +1,1032 @@ (*:maxLineLen=78:*) theory Framework imports Main Base begin chapter \The Isabelle/Isar Framework \label{ch:isar-framework}\ text \ Isabelle/Isar @{cite "Wenzel:1999:TPHOL" and "Wenzel-PhD" and "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. 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.\ \\\-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} \textbf{Inferences:} \begin{center} \begin{tabular}{l@ {\qquad}l} \infer{\B\}{\A \ B\ & \A\} & \infer{\A \ B\}{\infer*{\B\}{\[A]\}} \\ \end{tabular} \end{center} \textbf{Isabelle/Pure:} \begin{center} \begin{tabular}{l@ {\qquad}l} \(A \ B) \ A \ B\ & \(A \ B) \ A \ B\ \end{tabular} \end{center} \textbf{Isabelle/Isar:} \begin{center} \begin{minipage}[t]{0.4\textwidth} @{theory_text [display, indent = 2] \have "A \ B" \ also have A \ finally have B .\} \end{minipage} \begin{minipage}[t]{0.4\textwidth} @{theory_text [display, indent = 2] \have "A \ B" proof assume A then show B \ qed\} \end{minipage} \end{center} \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> 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 - \<^dir>\~~/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 + commonly used; elementary examples are given in the directories + \<^dir>\~~/src/Pure/Examples\ and \<^dir>\~~/src/HOL/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/Pure/Examples/Higher_Order_Logic.thy\). Isabelle/FOL @{cite "isabelle-logics"} and Isabelle/ZF @{cite "isabelle-ZF"} also work, but are much less developed. 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 (\\\, \\\, \\\, \\\, etc.), only the resulting reasoning principles are relevant to the user. There are similar rules available for set-theory operators (\\\, \\\, \\\, \\\, 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 \\\-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. \ text_raw \\medskip\begin{minipage}{0.6\textwidth}\ (*<*) notepad begin fix x :: 'a and A B (*>*) assume "x \ A" and "x \ B" then have "x \ A \ B" .. (*<*) end (*>*) text_raw \\end{minipage}\begin{minipage}{0.4\textwidth}\ text \ \infer{\x \ A \ B\}{\x \ A\ & \x \ B\} \ text_raw \\end{minipage}\ text \ \<^medskip> Note that \<^theory_text>\assume\ augments the proof context, \<^theory_text>\then\ indicates that the current fact shall be used in the next step, and \<^theory_text>\have\ states an intermediate goal. The two dots ``\<^theory_text>\..\'' 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>\by\ command: \ (*<*) notepad begin fix x :: 'a and A B (*>*) assume "x \ A" and "x \ B" then have "x \ A \ B" by (rule IntI) (*<*) end (*>*) text \ The format of the \\\-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 of \\\\, the intersection of all sets within a given set. This requires a nested proof of set membership within a local context, where \A\ is an arbitrary-but-fixed member of the collection: \ text_raw \\medskip\begin{minipage}{0.6\textwidth}\ (*<*) notepad begin fix x :: 'a and \ (*>*) have "x \ \\" proof fix A assume "A \ \" show "x \ A" \ qed (*<*) end (*>*) text_raw \\end{minipage}\begin{minipage}{0.4\textwidth}\ text \ \infer{\x \ \\\}{\infer*{\x \ A\}{\[A][A \ \]\}} \ text_raw \\end{minipage}\ text \ \<^medskip> This Isar reasoning pattern again refers to the primitive rule depicted above. The system determines it in the ``\<^theory_text>\proof\'' step, which could have been spelled out more explicitly as ``\<^theory_text>\proof (rule InterI)\''. Note that the rule involves both a local parameter \A\ and an assumption \A \ \\ 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>\fix\-\<^theory_text>\assume\-\<^theory_text>\show\ outline of nested subproofs that is typical for Isar. The final \<^theory_text>\show\ is like \<^theory_text>\have\ followed by an additional refinement of the enclosing claim, using the rule derived from the proof body. \<^medskip> The next example involves \\\\, which can be characterized as the set of all \x\ such that \\A. x \ A \ A \ \\. The elimination rule for \x \ \\\ does not mention \\\ and \\\ at all, but admits to obtain directly a local \A\ such that \x \ A\ and \A \ \\ hold. This corresponds to the following Isar proof and inference rule, respectively: \ text_raw \\medskip\begin{minipage}{0.6\textwidth}\ (*<*) notepad begin fix x :: 'a and \ C (*>*) assume "x \ \\" then have C proof fix A assume "x \ A" and "A \ \" show C \ qed (*<*) end (*>*) text_raw \\end{minipage}\begin{minipage}{0.4\textwidth}\ text \ \infer{\C\}{\x \ \\\ & \infer*{\C\~}{\[A][x \ A, A \ \]\}} \ text_raw \\end{minipage}\ text \ \<^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 \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 \<^theory_text>\obtain\, which is able to perform the same elimination proof more conveniently: \ (*<*) notepad begin fix x :: 'a and \ (*>*) assume "x \ \\" then obtain A where "x \ A" and "A \ \" .. (*<*) end (*>*) text \ Here we avoid to mention the final conclusion \C\ and return to plain forward reasoning. The rule involved in the ``\<^theory_text>\..\'' proof is the same as before. \ section \The Pure framework \label{sec:framework-pure}\ text \ 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 \\\-calculus with corresponding arrows \\\/\\\/\\\: \<^medskip> \begin{tabular}{ll} \\ \ \\ & syntactic function space (terms depending on terms) \\ \\x. B(x)\ & universal quantification (proofs depending on terms) \\ \A \ B\ & implication (proofs depending on proofs) \\ \end{tabular} \<^medskip> Here only the types of syntactic terms, and the propositions of proof terms have been shown. The \\\-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>\proof irrelevance\. 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 \\\ and \\\. Combining such rule statements may involve higher-order unification @{cite "paulson-natural"}. \ subsection \Primitive inferences\ text \ Term syntax provides explicit notation for abstraction \\x :: \. b(x)\ and application \b a\, while types are usually implicit thanks to type-inference; terms of type \prop\ are called propositions. Logical statements are composed via \\x :: \. B(x)\ and \A \ B\. Primitive reasoning operates on judgments of the form \\ \ \\, with standard introduction and elimination rules for \\\ and \\\ that refer to fixed parameters \x\<^sub>1, \, x\<^sub>m\ and hypotheses \A\<^sub>1, \, A\<^sub>n\ from the context \\\; the corresponding proof terms are left implicit. The subsequent inference rules define \\ \ \\ inductively, relative to a collection of axioms from the implicit background theory: \[ \infer{\\ A\}{\A\ \mbox{~is axiom}} \qquad \infer{\A \ A\}{} \] \[ \infer{\\ \ \x. B(x)\}{\\ \ B(x)\ & \x \ \\} \qquad \infer{\\ \ B(a)\}{\\ \ \x. B(x)\} \] \[ \infer{\\ - A \ A \ B\}{\\ \ B\} \qquad \infer{\\\<^sub>1 \ \\<^sub>2 \ B\}{\\\<^sub>1 \ A \ B\ & \\\<^sub>2 \ A\} \] Furthermore, Pure provides a built-in equality \\ :: \ \ \ \ prop\ with axioms for reflexivity, substitution, extensionality, and \\\\\-conversion on \\\-terms. \<^medskip> An object-logic introduces another layer on top of Pure, e.g.\ with types \i\ for individuals and \o\ for propositions, term constants \Trueprop :: o \ prop\ as (implicit) derivability judgment and connectives like \\ :: o \ o \ o\ or \\ :: (i \ o) \ o\, and axioms for object-level rules such as \conjI: A \ B \ A \ B\ or \allI: (\x. B x) \ \x. B x\. 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>\definition\, \<^theory_text>\inductive\, \<^theory_text>\fun\, \<^theory_text>\function\). \ subsection \Reasoning with rules \label{sec:framework-resolution}\ text \ Primitive inferences mostly serve foundational purposes. The main reasoning mechanisms of Pure operate on nested natural deduction rules expressed as formulae, using \\\ to bind local parameters and \\\ to express entailment. Multiple parameters and premises are represented by repeating these connectives in a right-associative manner. Thanks to the Pure theorem \<^prop>\(A \ (\x. B x)) \ (\x. A \ B x)\ the connectives \\\ and \\\ 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>\Hereditary Harrop Formula\ @{cite "Miller:1991"} which is of the form \\x\<^sub>1 \ x\<^sub>m. H\<^sub>1 \ \ H\<^sub>n \ A\ for \m, n \ 0\, and \A\ atomic, and \H\<^sub>1, \, H\<^sub>n\ being recursively of the same format. Following the convention that outermost quantifiers are implicit, Horn clauses \A\<^sub>1 \ \ A\<^sub>n \ A\ are a special case of this. For example, the \\\-introduction rule encountered before is represented as a Pure theorem as follows: \[ \IntI:\~\<^prop>\x \ A \ x \ B \ x \ A \ B\ \] This is a plain Horn clause, since no further nesting on the left is involved. The general \\\-introduction corresponds to a Hereditary Harrop Formula with one additional level of nesting: \[ \InterI:\~\<^prop>\(\A. A \ \ \ x \ A) \ x \ \\\ \] \<^medskip> Goals are also represented as rules: \A\<^sub>1 \ \ A\<^sub>n \ C\ states that the subgoals \A\<^sub>1, \, A\<^sub>n\ entail the result \C\; for \n = 0\ the goal is finished. To allow \C\ being a rule statement itself, there is an internal protective marker \# :: prop \ prop\, which is defined as identity and hidden from the user. We initialize and finish goal states as follows: \[ \begin{array}{c@ {\qquad}c} \infer[(@{inference_def init})]{\C \ #C\}{} & \infer[(@{inference_def finish})]{\C\}{\#C\} \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 subgoal (replacing it by zero or more subgoals), and @{inference assumption}, for solving a subgoal (finding a short-circuit with local assumptions). Below \\<^vec>x\ stands for \x\<^sub>1, \, x\<^sub>n\ (for \n \ 0\). \[ \infer[(@{inference_def resolution})] {\(\\<^vec>x. \<^vec>H \<^vec>x \ \<^vec>A (\<^vec>a \<^vec>x))\ \ C\\} {\begin{tabular}{rl} \rule:\ & \\<^vec>A \<^vec>a \ B \<^vec>a\ \\ \goal:\ & \(\\<^vec>x. \<^vec>H \<^vec>x \ B' \<^vec>x) \ C\ \\ \goal unifier:\ & \(\\<^vec>x. B (\<^vec>a \<^vec>x))\ = B'\\ \\ \end{tabular}} \] \<^medskip> \[ \infer[(@{inference_def assumption})]{\C\\} {\begin{tabular}{rl} \goal:\ & \(\\<^vec>x. \<^vec>H \<^vec>x \ A \<^vec>x) \ C\ \\ \assm unifier:\ & \A\ = H\<^sub>i\\~~\mbox{for some~\H\<^sub>i\} \\ \end{tabular}} \] The following trace illustrates goal-oriented reasoning in Isabelle/Pure: {\footnotesize \<^medskip> \begin{tabular}{r@ {\quad}l} \(A \ B \ B \ A) \ #(A \ B \ B \ A)\ & \(init)\ \\ \(A \ B \ B) \ (A \ B \ A) \ #\\ & \(resolution B \ A \ B \ A)\ \\ \(A \ B \ A \ B) \ (A \ B \ A) \ #\\ & \(resolution A \ B \ B)\ \\ \(A \ B \ A) \ #\\ & \(assumption)\ \\ \(A \ B \ A \ B) \ #\\ & \(resolution A \ B \ A)\ \\ \#\\ & \(assumption)\ \\ \A \ B \ B \ A\ & \(finish)\ \\ \end{tabular} \<^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 combined refinement rule as follows:\footnote{For simplicity and clarity, the presentation ignores \<^emph>\weak premises\ as introduced via \<^theory_text>\presume\ or \<^theory_text>\show \ when\.} {\small \[ \infer[(@{inference refinement})] {\C\\} {\begin{tabular}{rl} \subgoal:\ & \(\\<^vec>x. \<^vec>H \<^vec>x \ B' \<^vec>x) \ C\ \\ \subproof:\ & \\<^vec>G \<^vec>a \ B \<^vec>a\ \quad for schematic \\<^vec>a\ \\ \concl unifier:\ & \(\\<^vec>x. B (\<^vec>a \<^vec>x))\ = B'\\ \\ \assm unifiers:\ & \(\\<^vec>x. G\<^sub>j (\<^vec>a \<^vec>x))\ = H\<^sub>i\\ \quad for each \G\<^sub>j\ some \H\<^sub>i\ \\ \end{tabular}} \]} Here the \subproof\ rule stems from the main \<^theory_text>\fix\-\<^theory_text>\assume\-\<^theory_text>\show\ outline of Isar (cf.\ \secref{sec:framework-subproof}): each assumption indicated in the text results in a marked premise \G\ above. Consequently, \<^theory_text>\fix\-\<^theory_text>\assume\-\<^theory_text>\show\ 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}). \ section \The Isar proof language \label{sec:framework-isar}\ text \ 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. The main grammar of the Isar proof language is given in \figref{fig:isar-syntax}. \begin{figure}[htb] \begin{center} \begin{tabular}{rcl} \main\ & \=\ & \<^theory_text>\notepad begin "statement\<^sup>*" end\ \\ & \|\ & \<^theory_text>\theorem name: props if name: props for vars\ \\ & \|\ & \<^theory_text>\theorem name:\ \\ & & \quad\<^theory_text>\fixes vars\ \\ & & \quad\<^theory_text>\assumes name: props\ \\ & & \quad\<^theory_text>\shows name: props "proof"\ \\ & \|\ & \<^theory_text>\theorem name:\ \\ & & \quad\<^theory_text>\fixes vars\ \\ & & \quad\<^theory_text>\assumes name: props\ \\ & & \quad\<^theory_text>\obtains (name) clause "\<^bold>|" \ "proof"\ \\ \proof\ & \=\ & \<^theory_text>\"refinement\<^sup>* proper_proof"\ \\ \refinement\ & \=\ & \<^theory_text>\apply method\ \\ & \|\ & \<^theory_text>\supply name = thms\ \\ & \|\ & \<^theory_text>\subgoal premises name for vars "proof"\ \\ & \|\ & \<^theory_text>\using thms\ \\ & \|\ & \<^theory_text>\unfolding thms\ \\ \proper_proof\ & \=\ & \<^theory_text>\proof "method\<^sup>?" "statement\<^sup>*" qed "method\<^sup>?"\ \\ & \|\ & \<^theory_text>\by method method\~~~\|\~~~\<^theory_text>\..\~~~\|\~~~\<^theory_text>\.\~~~\|\~~~\<^theory_text>\sorry\~~~\|\~~~\<^theory_text>\done\ \\ \statement\ & \=\ & \<^theory_text>\{ "statement\<^sup>*" }\~~~\|\~~~\<^theory_text>\next\ \\ & \|\ & \<^theory_text>\note name = thms\ \\ & \|\ & \<^theory_text>\let "term" = "term"\ \\ & \|\ & \<^theory_text>\write name (mixfix)\ \\ & \|\ & \<^theory_text>\fix vars\ \\ & \|\ & \<^theory_text>\assume name: props if props for vars\ \\ & \|\ & \<^theory_text>\presume name: props if props for vars\ \\ & \|\ & \<^theory_text>\define clause\ \\ & \|\ & \<^theory_text>\case name: "case"\ \\ & \|\ & \<^theory_text>\then"\<^sup>?" goal\ \\ & \|\ & \<^theory_text>\from thms goal\ \\ & \|\ & \<^theory_text>\with thms goal\ \\ & \|\ & \<^theory_text>\also\~~~\|\~~~\<^theory_text>\finally goal\ \\ & \|\ & \<^theory_text>\moreover\~~~\|\~~~\<^theory_text>\ultimately goal\ \\ \goal\ & \=\ & \<^theory_text>\have name: props if name: props for vars "proof"\ \\ & \|\ & \<^theory_text>\show name: props if name: props for vars "proof"\ \\ & \|\ & \<^theory_text>\show name: props when name: props for vars "proof"\ \\ & \|\ & \<^theory_text>\consider (name) clause "\<^bold>|" \ "proof"\ \\ & \|\ & \<^theory_text>\obtain (name) clause "proof"\ \\ \clause\ & \=\ & \<^theory_text>\vars where name: props if props for vars\ \\ \end{tabular} \end{center} \caption{Main grammar of the Isar proof language}\label{fig:isar-syntax} \end{figure} The construction of the Isar proof language proceeds in a bottom-up fashion, as an exercise in purity and minimalism. The grammar in \appref{ap:main-grammar} describes the primitive parts of the core language (category \proof\), which is embedded into the main outer theory syntax via elements that require a proof (e.g.\ \<^theory_text>\theorem\, \<^theory_text>\lemma\, \<^theory_text>\function\, \<^theory_text>\termination\). The syntax for terms and propositions is inherited from Pure (and the object-logic). A \pattern\ is a \term\ with schematic variables, to be bound by higher-order matching. Simultaneous propositions or facts may be separated by the \<^theory_text>\and\ keyword. \<^medskip> Facts may be referenced by name or proposition. For example, the result of ``\<^theory_text>\have a: A \\'' becomes accessible both via the name \a\ and the literal proposition \\A\\. Moreover, fact expressions may involve attributes that modify either the theorem or the background context. For example, the expression ``\a [OF b]\'' refers to the composition of two facts according to the @{inference resolution} inference of \secref{sec:framework-resolution}, while ``\a [intro]\'' 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>\note\, \<^theory_text>\assume\, \<^theory_text>\have\, or \<^theory_text>\show\. Since \<^theory_text>\note\ occurs frequently together with \<^theory_text>\then\, there are some abbreviations: \<^medskip> \begin{tabular}{rcl} \<^theory_text>\from a\ & \\\ & \<^theory_text>\note a then\ \\ \<^theory_text>\with a\ & \\\ & \<^theory_text>\from a and this\ \\ \end{tabular} \<^medskip> The \method\ category is essentially a parameter of the Isar language and may be populated later. The command \<^theory_text>\method_setup\ 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 \<^dir>\~~/src/HOL/Eisbach\. Methods use the facts indicated by \<^theory_text>\then\ or \<^theory_text>\using\, 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 ``\(rule a)\'', 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>\proof\ is ``@{method standard}'' (which subsumes @{method rule} with arguments picked from the context), for \<^theory_text>\qed\ it is ``@{method "succeed"}''. Further abbreviations for terminal proof steps are ``\<^theory_text>\by method\<^sub>1 method\<^sub>2\'' for ``\<^theory_text>\proof method\<^sub>1 qed method\<^sub>2\'', and ``\<^theory_text>\..\'' for ``\<^theory_text>\by standard\, and ``\<^theory_text>\.\'' for ``\<^theory_text>\by this\''. The command ``\<^theory_text>\unfolding facts\'' operates directly on the goal by applying equalities. \<^medskip> Block structure can be indicated explicitly by ``\<^theory_text>\{ \ }\'', although the body of a subproof ``\<^theory_text>\proof \ qed\'' already provides implicit nesting. In both situations, \<^theory_text>\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 connection to subgoals here! The commands \<^theory_text>\fix\ and \<^theory_text>\assume\ build up a local context (see \secref{sec:framework-context}), while \<^theory_text>\show\ 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}). \ subsection \Context elements \label{sec:framework-context}\ text \ In judgments \\ \ \\ of the primitive framework, \\\ 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 \<^theory_text>\fix x :: \\ declares a local parameter, i.e.\ an arbitrary-but-fixed entity of a given type; in results exported from the context, \x\ may become anything. The \<^theory_text>\assume \inference\\ element provides a general interface to hypotheses: \<^theory_text>\assume \inference\ A\ produces \A \ A\ locally, while the included inference tells how to discharge \A\ from results \A \ B\ later on. There is no surface syntax for \\inference\\, i.e.\ it may only occur internally when derived commands are defined in ML. The default inference for \<^theory_text>\assume\ is @{inference export} as given below. The derived element \<^theory_text>\define x where "x \ a"\ is defined as \<^theory_text>\fix x assume \expand\ x \ a\, with the subsequent inference @{inference expand}. \[ \infer[(@{inference_def export})]{\\\ - A \ A \ B\}{\\\ \ B\} \qquad \infer[(@{inference_def expand})]{\\\ - (x \ a) \ B a\}{\\\ \ B x\} \] \<^medskip> The most interesting derived context element in Isar is \<^theory_text>\obtain\ @{cite \\S5.3\ "Wenzel-PhD"}, which supports generalized elimination steps in a purely forward manner. The \<^theory_text>\obtain\ command takes a specification of parameters \\<^vec>x\ and assumptions \\<^vec>A\ 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} \<^theory_text>\\facts\ obtain "\<^vec>x" where "\<^vec>A" "\<^vec>x" \ \\ \\[0.5ex] \quad \<^theory_text>\have "case": "\thesis. (\\<^vec>x. \<^vec>A \<^vec>x \ thesis) \ thesis"\ \\ \quad \<^theory_text>\proof -\ \\ \qquad \<^theory_text>\fix thesis\ \\ \qquad \<^theory_text>\assume [intro]: "\\<^vec>x. \<^vec>A \<^vec>x \ thesis"\ \\ \qquad \<^theory_text>\show thesis using \facts\ \\ \\ \quad \<^theory_text>\qed\ \\ \quad \<^theory_text>\fix "\<^vec>x" assume \elimination "case"\ "\<^vec>A \<^vec>x"\ \\ \end{tabular} \<^medskip> \[ \infer[(@{inference elimination})]{\\ \ B\}{ \begin{tabular}{rl} \case:\ & \\ \ \thesis. (\\<^vec>x. \<^vec>A \<^vec>x \ thesis) \ thesis\ \\[0.2ex] \result:\ & \\ \ \<^vec>A \<^vec>y \ B\ \\[0.2ex] \end{tabular}} \] Here the name ``\thesis\'' is a specific convention for an arbitrary-but-fixed proposition; in the primitive natural deduction rules shown before we have occasionally used \C\. The whole statement of ``\<^theory_text>\obtain x where A x\'' can be read as a claim that \A x\ may be assumed for some arbitrary-but-fixed \x\. Also note that ``\<^theory_text>\obtain A and B\'' without parameters is similar to ``\<^theory_text>\have A and B\'', 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, the exported result is indicated via \<^theory_text>\note\. \ (*<*) theorem True proof (*>*) text_raw \\begin{minipage}[t]{0.45\textwidth}\ { fix x have "B x" \ } note \\x. B x\ text_raw \\end{minipage}\quad\begin{minipage}[t]{0.45\textwidth}\(*<*)next(*>*) { assume A have B \ } note \A \ B\ text_raw \\end{minipage}\\[3ex]\begin{minipage}[t]{0.45\textwidth}\(*<*)next(*>*) { define x where "x \ a" have "B x" \ } note \B a\ text_raw \\end{minipage}\quad\begin{minipage}[t]{0.45\textwidth}\(*<*)next(*>*) { obtain x where "A x" \ have B \ } note \B\ text_raw \\end{minipage}\ (*<*) qed (*>*) text \ \<^bigskip> This explains the meaning of Isar context elements without, without goal states getting in the way. \ subsection \Structured statements \label{sec:framework-stmt}\ text \ The syntax of top-level theorem statements is defined as follows: \<^medskip> \begin{tabular}{rcl} \statement\ & \\\ & \<^theory_text>\name: props and \\ \\ & \|\ & \context\<^sup>* conclusion\ \\[0.5ex] \context\ & \\\ & \<^theory_text>\fixes vars and \\ \\ & \|\ & \<^theory_text>\assumes name: props and \\ \\ \conclusion\ & \\\ & \<^theory_text>\shows name: props and \\ \\ & \|\ & \<^theory_text>\obtains vars and \ where name: props and \\ \\ & & \quad \\ \\ \\ \end{tabular} \<^medskip> A simple statement consists of named propositions. The full form admits local context elements followed by the actual conclusions, such as ``\<^theory_text>\fixes x assumes A x shows B x\''. The final result emerges as a Pure rule after discharging the context: \<^prop>\\x. A x \ B x\. The \<^theory_text>\obtains\ variant is another abbreviation defined below; unlike \<^theory_text>\obtain\ (cf.\ \secref{sec:framework-context}) there may be several ``cases'' separated by ``\\\'', each consisting of several parameters (\vars\) and several premises (\props\). This specifies multi-branch elimination rules. \<^medskip> \begin{tabular}{l} \<^theory_text>\obtains "\<^vec>x" where "\<^vec>A" "\<^vec>x" "\" \ \\ \\[0.5ex] \quad \<^theory_text>\fixes thesis\ \\ \quad \<^theory_text>\assumes [intro]: "\\<^vec>x. \<^vec>A \<^vec>x \ thesis" and \\ \\ \quad \<^theory_text>\shows thesis\ \\ \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 \<^theory_text>\shows\ and \<^theory_text>\obtains\, respectively: \ text_raw \\begin{minipage}{0.5\textwidth}\ theorem fixes x and y assumes "A x" and "B y" shows "C x y" proof - from \A x\ and \B y\ show "C x y" \ qed text_raw \\end{minipage}\begin{minipage}{0.5\textwidth}\ theorem obtains x and y where "A x" and "B y" proof - have "A a" and "B b" \ then show thesis .. qed text_raw \\end{minipage}\ text \ \<^medskip> Here local facts \\A x\\ and \\B y\\ are referenced immediately; there is no need to decompose the logical rule structure again. In the second proof the final ``\<^theory_text>\then show thesis ..\'' involves the local rule case \\x y. A x \ B y \ thesis\ for the particular instance of terms \a\ and \b\ produced in the body. \ subsection \Structured proof refinement \label{sec:framework-subproof}\ text \ 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: \(a + b) \ c\ then corresponds to a sequence of single transitions for each symbol \(, a, +, b, ), \, c\. 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}). \begin{figure}[htb] \begin{center} \includegraphics[width=0.8\textwidth]{isar-vm} \end{center} \caption{Isar/VM modes}\label{fig:isar-vm} \end{figure} For example, in \state\ mode Isar acts like a mathematical scratch-pad, accepting declarations like \<^theory_text>\fix\, \<^theory_text>\assume\, and claims like \<^theory_text>\have\, \<^theory_text>\show\. A goal statement changes the mode to \prove\, which means that we may now refine the problem via \<^theory_text>\unfolding\ or \<^theory_text>\proof\. Then we are again in \state\ mode of a proof body, which may issue \<^theory_text>\show\ statements to solve pending subgoals. A concluding \<^theory_text>\qed\ will return to the original \state\ mode one level upwards. The subsequent Isar/VM trace indicates block structure, linguistic mode, goal state, and inferences: \ text_raw \\begingroup\footnotesize\ (*<*)notepad begin (*>*) text_raw \\begin{minipage}[t]{0.18\textwidth}\ have "A \ B" proof assume A show B \ qed text_raw \\end{minipage}\quad \begin{minipage}[t]{0.06\textwidth} \begin\ \\ \\ \\ \begin\ \\ \end\ \\ \end\ \\ \end{minipage} \begin{minipage}[t]{0.08\textwidth} \prove\ \\ \state\ \\ \state\ \\ \prove\ \\ \state\ \\ \state\ \\ \end{minipage}\begin{minipage}[t]{0.35\textwidth} \(A \ B) \ #(A \ B)\ \\ \(A \ B) \ #(A \ B)\ \\ \\ \\ \#(A \ B)\ \\ \A \ B\ \\ \end{minipage}\begin{minipage}[t]{0.4\textwidth} \(init)\ \\ \(resolution impI)\ \\ \\ \\ \(refinement #A \ B)\ \\ \(finish)\ \\ \end{minipage}\ (*<*) end (*>*) text_raw \\endgroup\ text \ Here the @{inference refinement} inference from \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: \ text_raw \\begin{minipage}{0.5\textwidth}\ (*<*) notepad begin (*>*) have "\x y. A x \ B y \ C x y" proof - fix x and y assume "A x" and "B y" show "C x y" \ qed text_raw \\end{minipage}\begin{minipage}{0.5\textwidth}\ (*<*) next (*>*) have "\x y. A x \ B y \ C x y" proof - fix x assume "A x" fix y assume "B y" show "C x y" \ qed text_raw \\end{minipage}\\[3ex]\begin{minipage}{0.5\textwidth}\ (*<*) next (*>*) have "\x y. A x \ B y \ C x y" proof - fix y assume "B y" fix x assume "A x" show "C x y" \ qed text_raw \\end{minipage}\begin{minipage}{0.5\textwidth}\ (*<*) next (*>*) have "\x y. A x \ B y \ C x y" proof - fix y assume "B y" fix x show "C x y" \ qed (*<*) end (*>*) text_raw \\end{minipage}\ text \ \<^medskip> 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 involved, just plain unification. \ subsection \Calculational reasoning \label{sec:framework-calc}\ text \ 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 \=\, \<\, \\\, \\\, \\\ 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 \\S6\ "Wenzel-PhD"} and @{cite "Bauer-Wenzel:2001"}. The generic calculational mechanism is based on the observation that rules such as \trans:\~\<^prop>\x = y \ y = z \ 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 \trans\ represents to a suitable rule from the context: \begin{matharray}{rcl} \<^theory_text>\also"\<^sub>0"\ & \equiv & \<^theory_text>\note calculation = this\ \\ \<^theory_text>\also"\<^sub>n\<^sub>+\<^sub>1"\ & \equiv & \<^theory_text>\note calculation = trans [OF calculation this]\ \\[0.5ex] \<^theory_text>\finally\ & \equiv & \<^theory_text>\also from calculation\ \\ \end{matharray} The start of a calculation is determined implicitly in the text: here \<^theory_text>\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 \<^theory_text>\finally\, where the final result is exposed for use in a concluding claim. Here is a canonical proof pattern, using \<^theory_text>\have\ to establish the intermediate results: \ (*<*) notepad begin fix a b c d :: 'a (*>*) have "a = b" \ also have "\ = c" \ also have "\ = d" \ finally have "a = d" . (*<*) end (*>*) text \ The term ``\\\'' (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 \ 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 ``\a [symmetric]\'', or single-step proofs ``\<^theory_text>\assume "x = y" then have "y = x" ..\''. \ end diff --git a/src/Doc/System/Server.thy b/src/Doc/System/Server.thy --- a/src/Doc/System/Server.thy +++ b/src/Doc/System/Server.thy @@ -1,1109 +1,1109 @@ (*:maxLineLen=78:*) theory Server imports Base begin chapter \The Isabelle server\ text \ An Isabelle session requires at least two processes, which are both rather heavy: Isabelle/Scala for the system infrastructure and Isabelle/ML for the logic session (e.g.\ HOL). In principle, these processes can be invoked directly on the command-line, e.g.\ via @{tool java}, @{tool scala}, @{tool process}, @{tool console}, but this approach is inadequate for reactive applications that require quick responses from the prover. In contrast, the Isabelle server exposes Isabelle/Scala as a ``terminate-stay-resident'' application that manages multiple logic \<^emph>\sessions\ and concurrent tasks to use \<^emph>\theories\. This provides an analogous to \<^ML>\Thy_Info.use_theories\ in Isabelle/ML, but with full concurrency and Isabelle/PIDE markup. The client/server arrangement via TCP sockets also opens possibilities for remote Isabelle services that are accessed by local applications, e.g.\ via an SSH tunnel. \ section \Command-line tools\ subsection \Server \label{sec:tool-server}\ text \ The @{tool_def server} tool manages resident server processes: @{verbatim [display] \Usage: isabelle server [OPTIONS] Options are: -L FILE logging on FILE -c console interaction with specified server -l list servers (alternative operation) -n NAME explicit server name (default: isabelle) -p PORT explicit server port -s assume existing server, no implicit startup -x exit specified server (alternative operation) Manage resident Isabelle servers.\} The main operation of \<^verbatim>\isabelle server\ is to ensure that a named server is running, either by finding an already running process (according to the central database file \<^path>\$ISABELLE_HOME_USER/servers.db\) or by becoming itself a new server that accepts connections on a particular TCP socket. The server name and its address are printed as initial output line. If another server instance is already running, the current \<^verbatim>\isabelle server\ process will terminate; otherwise, it keeps running as a new server process until an explicit \<^verbatim>\shutdown\ command is received. Further details of the server socket protocol are explained in \secref{sec:server-protocol}. Other server management operations are invoked via options \<^verbatim>\-l\ and \<^verbatim>\-x\ (see below). \<^medskip> Option \<^verbatim>\-n\ specifies an alternative server name: at most one process for each name may run, but each server instance supports multiple connections and logic sessions. \<^medskip> Option \<^verbatim>\-p\ specifies an explicit TCP port for the server socket (which is always on \<^verbatim>\localhost\): the default is to let the operating system assign a free port number. \<^medskip> Option \<^verbatim>\-s\ strictly assumes that the specified server process is already running, skipping the optional server startup phase. \<^medskip> Option \<^verbatim>\-c\ connects the console in/out channels after the initial check for a suitable server process. Also note that the @{tool client} tool (\secref{sec:tool-client}) provides a command-line editor to interact with the server. \<^medskip> Option \<^verbatim>\-L\ specifies a log file for exceptional output of internal server and session operations. \<^medskip> Operation \<^verbatim>\-l\ lists all active server processes with their connection details. \<^medskip> Operation \<^verbatim>\-x\ exits the specified server process by sending it a \<^verbatim>\shutdown\ command. \ subsection \Client \label{sec:tool-client}\ text \ The @{tool_def client} tool provides console interaction for Isabelle servers: @{verbatim [display] \Usage: isabelle client [OPTIONS] Options are: -n NAME explicit server name -p PORT explicit server port Console interaction for Isabelle server (with line-editor).\} This is a wrapper to \<^verbatim>\isabelle server -s -c\ for interactive experimentation, which uses @{setting ISABELLE_LINE_EDITOR} if available. The server name is sufficient for identification, as the client can determine the connection details from the local database of active servers. \<^medskip> Option \<^verbatim>\-n\ specifies an explicit server name as in @{tool server}. \<^medskip> Option \<^verbatim>\-p\ specifies an explicit server port as in @{tool server}. \ subsection \Examples\ text \ Ensure that a particular server instance is running in the background: @{verbatim [display] \isabelle server -n test &\} The first line of output presents the connection details:\<^footnote>\This information may be used in other TCP clients, without access to Isabelle/Scala and the underlying database of running servers.\ @{verbatim [display] \server "test" = 127.0.0.1:4711 (password "XYZ")\} \<^medskip> List available server processes: @{verbatim [display] \isabelle server -l\} \<^medskip> Connect the command-line client to the above test server: @{verbatim [display] \isabelle client -n test\} Interaction now works on a line-by-line basis, with commands like \<^verbatim>\help\ or \<^verbatim>\echo\. For example, some JSON values may be echoed like this: @{verbatim [display] \echo 42 echo [1, 2, 3] echo {"a": "text", "b": true, "c": 42}\} Closing the connection (via CTRL-D) leaves the server running: it is possible to reconnect again, and have multiple connections at the same time. \<^medskip> Exit the named server on the command-line: @{verbatim [display] \isabelle server -n test -x\} \ section \Protocol messages \label{sec:server-protocol}\ text \ The Isabelle server listens on a regular TCP socket, using a line-oriented protocol of structured messages. Input \<^emph>\commands\ and output \<^emph>\results\ (via \<^verbatim>\OK\ or \<^verbatim>\ERROR\) are strictly alternating on the toplevel, but commands may also return a \<^emph>\task\ identifier to indicate an ongoing asynchronous process that is joined later (via \<^verbatim>\FINISHED\ or \<^verbatim>\FAILED\). Asynchronous \<^verbatim>\NOTE\ messages may occur at any time: they are independent of the main command-result protocol. For example, the synchronous \<^verbatim>\echo\ command immediately returns its argument as \<^verbatim>\OK\ result. In contrast, the asynchronous \<^verbatim>\session_build\ command returns \<^verbatim>\OK {"task":\\id\\<^verbatim>\}\ and continues in the background. It will eventually produce \<^verbatim>\FINISHED {"task":\\id\\<^verbatim>\,\\\\\<^verbatim>\}\ or \<^verbatim>\FAILED {"task":\\id\\<^verbatim>\,\\\\\<^verbatim>\}\ with the final result. Intermediately, it may emit asynchronous messages of the form \<^verbatim>\NOTE {"task":\\id\\<^verbatim>\,\\\\\<^verbatim>\}\ to inform about its progress. Due to the explicit task identifier, the client can show these messages in the proper context, e.g.\ a GUI window for this particular session build job. \medskip Subsequently, the protocol message formats are described in further detail. \ subsection \Byte messages \label{sec:byte-messages}\ text \ The client-server connection is a raw byte-channel for bidirectional communication, but the Isabelle server always works with messages of a particular length. Messages are written as a single chunk that is flushed immediately. Message boundaries are determined as follows: \<^item> A \<^emph>\short message\ consists of a single line: it is a sequence of arbitrary bytes excluding CR (13) and LF (10), and terminated by CR-LF or just LF. \<^item> A \<^emph>\long message\ starts with a single that consists only of decimal digits: these are interpreted as length of the subsequent block of arbitrary bytes. A final line-terminator (as above) may be included here, but is not required. Messages in JSON format (see below) always fit on a single line, due to escaping of newline characters within string literals. This is convenient for interactive experimentation, but it can impact performance for very long messages. If the message byte-length is given on the preceding line, the server can read the message more efficiently as a single block. \ subsection \Text messages\ text \ Messages are read and written as byte streams (with byte lengths), but the content is always interpreted as plain text in terms of the UTF-8 encoding.\<^footnote>\See also the ``UTF-8 Everywhere Manifesto'' \<^url>\https://utf8everywhere.org\.\ Note that line-endings and other formatting characters are invariant wrt. UTF-8 representation of text: thus implementations are free to determine the overall message structure before or after applying the text encoding. \ subsection \Input and output messages \label{sec:input-output-messages}\ text \ Server input and output messages have a uniform format as follows: \<^item> \name argument\ such that: \<^item> \name\ is the longest prefix consisting of ASCII letters, digits, ``\<^verbatim>\_\'', ``\<^verbatim>\.\'', \<^item> the separator between \name\ and \argument\ is the longest possible sequence of ASCII blanks (it could be empty, e.g.\ when the argument starts with a quote or bracket), \<^item> \argument\ is the rest of the message without line terminator. \<^medskip> Input messages are sent from the client to the server. Here the \name\ specifies a \<^emph>\server command\: the list of known commands may be retrieved via the \<^verbatim>\help\ command. \<^medskip> Output messages are sent from the server to the client. Here the \name\ specifies the \<^emph>\server reply\, which always has a specific meaning as follows: \<^item> synchronous results: \<^verbatim>\OK\ or \<^verbatim>\ERROR\ \<^item> asynchronous results: \<^verbatim>\FINISHED\ or \<^verbatim>\FAILED\ \<^item> intermediate notifications: \<^verbatim>\NOTE\ \<^medskip> The \argument\ format is uniform for both input and output messages: \<^item> empty argument (Scala type \<^verbatim>\Unit\) \<^item> XML element in YXML notation (Scala type \<^verbatim>\XML.Elem\) \<^item> JSON value (Scala type \<^verbatim>\JSON.T\) JSON values may consist of objects (records), arrays (lists), strings, numbers, bools, null.\<^footnote>\See also the official specification \<^url>\https://www.json.org\ and unofficial explorations ``Parsing JSON is a Minefield'' \<^url>\http://seriot.ch/parsing_json.php\.\ Since JSON requires explicit quotes and backslash-escapes to represent arbitrary text, the YXML notation for XML trees (\secref{sec:yxml-vs-xml}) works better for large messages with a lot of PIDE markup. Nonetheless, the most common commands use JSON by default: big chunks of text (theory sources etc.) are taken from the underlying file-system and results are pre-formatted for plain-text output, without PIDE markup information. This is a concession to simplicity: the server imitates the appearance of command-line tools on top of the Isabelle/PIDE infrastructure. \ subsection \Initial password exchange\ text \ Whenever a new client opens the server socket, the initial message needs to be its unique password as a single line, without length indication (i.e.\ a ``short message'' in the sense of \secref{sec:byte-messages}). The server replies either with \<^verbatim>\OK\ (and some information about the Isabelle version) or by silent disconnection of what is considered an illegal connection attempt. Note that @{tool client} already presents the correct password internally. Server passwords are created as Universally Unique Identifier (UUID) in Isabelle/Scala and stored in a per-user database, with restricted file-system access only for the current user. The Isabelle/Scala server implementation is careful to expose the password only on private output channels, and not on a process command-line (which is accessible to other users, e.g.\ via the \<^verbatim>\ps\ command). \ subsection \Synchronous commands\ text \ A \<^emph>\synchronous command\ corresponds to regular function application in Isabelle/Scala, with single argument and result (regular or error). Both the argument and the result may consist of type \<^verbatim>\Unit\, \<^verbatim>\XML.Elem\, \<^verbatim>\JSON.T\. An error result typically consists of a JSON object with error message and potentially further result fields (this resembles exceptions in Scala). These are the protocol exchanges for both cases of command execution: \begin{center} \begin{tabular}{rl} \<^bold>\input:\ & \command argument\ \\ (a) regular \<^bold>\output:\ & \<^verbatim>\OK\ \result\ \\ (b) error \<^bold>\output:\ & \<^verbatim>\ERROR\ \result\ \\ \end{tabular} \end{center} \ subsection \Asynchronous commands\ text \ An \<^emph>\asynchronous command\ corresponds to an ongoing process that finishes or fails eventually, while emitting arbitrary notifications in between. Formally, it starts as synchronous command with immediate result \<^verbatim>\OK\ giving the \<^verbatim>\task\ identifier, or an immediate \<^verbatim>\ERROR\ that indicates bad command syntax. For a running task, the termination is indicated later by \<^verbatim>\FINISHED\ or \<^verbatim>\FAILED\, together with its ultimate result value. These are the protocol exchanges for various cases of command task execution: \begin{center} \begin{tabular}{rl} \<^bold>\input:\ & \command argument\ \\ immediate \<^bold>\output:\ & \<^verbatim>\OK {"task":\\id\\<^verbatim>\}\ \\ intermediate \<^bold>\output:\ & \<^verbatim>\NOTE {"task":\\id\\<^verbatim>\,\\\\\<^verbatim>\}\ \\ (a) regular \<^bold>\output:\ & \<^verbatim>\FINISHED {"task":\\id\\<^verbatim>\,\\\\\<^verbatim>\}\ \\ (b) error \<^bold>\output:\ & \<^verbatim>\FAILED {"task":\\id\\<^verbatim>\,\\\\\<^verbatim>\}\ \\[3ex] \<^bold>\input:\ & \command argument\ \\ immediate \<^bold>\output:\ & \<^verbatim>\ERROR\~\\\ \\ \end{tabular} \end{center} All asynchronous messages are decorated with the task identifier that was revealed in the immediate (synchronous) result. Thus the client can invoke further asynchronous commands and still dispatch the resulting stream of asynchronous messages properly. The synchronous command \<^verbatim>\cancel {"task":\~\id\\<^verbatim>\}\ tells the specified task to terminate prematurely: usually causing a \<^verbatim>\FAILED\ result, but this is not guaranteed: the cancel event may come too late or the running process may just ignore it. \ section \Types for JSON values \label{sec:json-types}\ text \ In order to specify concrete JSON types for command arguments and result messages, the following type definition language shall be used: \<^rail>\ @{syntax type_def}: @'type' @{syntax name} '=' @{syntax type} ; @{syntax type}: @{syntax name} | @{syntax value} | 'any' | 'null' | 'bool' | 'int' | 'long' | 'double' | 'string' | '[' @{syntax type} ']' | '{' (@{syntax field_type} ',' *) '}' | @{syntax type} '\' @{syntax type} | @{syntax type} '|' @{syntax type} | '(' @{syntax type} ')' ; @{syntax field_type}: @{syntax name} ('?'?) ':' @{syntax type} \ This is a simplified variation of TypeScript interfaces.\<^footnote>\\<^url>\https://www.typescriptlang.org/docs/handbook/interfaces.html\\ The meaning of these types is specified wrt. the Isabelle/Scala implementation as follows. \<^item> A \name\ refers to a type defined elsewhere. The environment of type definitions is given informally: put into proper foundational order, it needs to specify a strongly normalizing system of syntactic abbreviations; type definitions may not be recursive. \<^item> A \value\ in JSON notation represents the singleton type of the given item. For example, the string \<^verbatim>\"error"\ can be used as type for a slot that is guaranteed to contain that constant. \<^item> Type \any\ is the super type of all other types: it is an untyped slot in the specification and corresponds to \<^verbatim>\Any\ or \<^verbatim>\JSON.T\ in Isabelle/Scala. \<^item> Type \null\ is the type of the improper value \null\; it corresponds to type \<^verbatim>\Null\ in Scala and is normally not used in Isabelle/Scala.\<^footnote>\See also ``Null References: The Billion Dollar Mistake'' by Tony Hoare \<^url>\https://www.infoq.com/presentations/Null-References-The-Billion-Dollar-Mistake-Tony-Hoare\.\ \<^item> Type \bool\ is the type of the truth values \<^verbatim>\true\ and \<^verbatim>\false\; it corresponds to \<^verbatim>\Boolean\ in Scala. \<^item> Types \int\, \long\, \double\ are specific versions of the generic \number\ type, corresponding to \<^verbatim>\Int\, \<^verbatim>\Long\, \<^verbatim>\Double\ in Scala, but \<^verbatim>\Long\ is limited to 53 bit precision.\<^footnote>\Implementations of JSON typically standardize \number\ to \<^verbatim>\Double\, which can absorb \<^verbatim>\Int\ faithfully, but not all of \<^verbatim>\Long\.\ \<^item> Type \string\ represents Unicode text; it corresponds to type \<^verbatim>\String\ in Scala. \<^item> Type \[t]\ is the array (or list) type over \t\; it corresponds to \<^verbatim>\List[t]\ in Scala. The list type is co-variant as usual (i.e.\ monotonic wrt. the subtype relation). \<^item> Object types describe the possible content of JSON records, with field names and types. A question mark after a field name means that it is optional. In Scala this could refer to an explicit type \<^verbatim>\Option[t]\, e.g.\ \{a: int, b?: string}\ corresponding to a Scala case class with arguments \<^verbatim>\a: Int\, \<^verbatim>\b: Option[String]\. Alternatively, optional fields can have a default value. If nothing else is specified, a standard ``empty value'' is used for each type, i.e.\ \<^verbatim>\0\ for the number types, \<^verbatim>\false\ for \bool\, or the empty string, array, object etc. Object types are \<^emph>\permissive\ in the sense that only the specified field names need to conform to the given types, but unspecified fields may be present as well. \<^item> The type expression \t\<^sub>1 \ t\<^sub>2\ only works for two object types with disjoint field names: it is the concatenation of the respective @{syntax field_type} specifications taken together. For example: \{task: string} \ {ok: bool}\ is the equivalent to \{task: string, ok: bool}\. \<^item> The type expression \t\<^sub>1 | t\<^sub>2\ is the disjoint union of two types, either one of the two cases may occur. \<^item> Parentheses \(t)\ merely group type expressions syntactically. These types correspond to JSON values in an obvious manner, which is not further described here. For example, the JSON array \<^verbatim>\[1, 2, 3]\ conforms to types \[int]\, \[long]\, \[double]\, \[any]\, \any\. Note that JSON objects require field names to be quoted, but the type language omits quotes for clarity. Thus the object \<^verbatim>\{"a": 42, "b": "xyz"}\ conforms to the type \{a: int, b: string}\, for example. \<^medskip> The absence of an argument or result is represented by the Scala type \<^verbatim>\Unit\: it is written as empty text in the message \argument\ (\secref{sec:input-output-messages}). This is not part of the JSON language. Server replies have name tags like \<^verbatim>\OK\, \<^verbatim>\ERROR\: these are used literally together with type specifications to indicate the particular name with the type of its argument, e.g.\ \<^verbatim>\OK\~\[string]\ for a regular result that is a list (JSON array) of strings. \<^bigskip> Here are some common type definitions, for use in particular specifications of command arguments and results. \<^item> \<^bold>\type\~\position = {line?: int, offset?: int, end_offset?: int, file?: string, id?: long}\ describes a source position within Isabelle text. Only the \line\ and \file\ fields make immediate sense to external programs. Detailed \offset\ and \end_offset\ positions are counted according to Isabelle symbols, see \<^ML_type>\Symbol.symbol\ in Isabelle/ML @{cite "isabelle-implementation"}. The position \id\ belongs to the representation of command transactions in the Isabelle/PIDE protocol: it normally does not occur in externalized positions. \<^item> \<^bold>\type\~\message = {kind: string, message: string, pos?: position}\ where the \kind\ provides some hint about the role and importance of the message. The main message kinds are \<^verbatim>\writeln\ (for regular output), \<^verbatim>\warning\, \<^verbatim>\error\. \<^item> \<^bold>\type\~\error_message = {kind:\~\<^verbatim>\"error"\\, message: string}\ refers to error messages in particular. These occur routinely with \<^verbatim>\ERROR\ or \<^verbatim>\FAILED\ replies, but also as initial command syntax errors (which are omitted in the command specifications below). \<^item> \<^bold>\type\~\theory_progress = {kind:\~\<^verbatim>\"writeln"\\, message: string, theory: string, session: string, percentage?: int}\ reports formal progress in loading theories (e.g.\ when building a session image). Apart from a regular output message, it also reveals the formal theory name (e.g.\ \<^verbatim>\"HOL.Nat"\) and session name (e.g.\ \<^verbatim>\"HOL"\). Note that some rare theory names lack a proper session prefix, e.g.\ theory \<^verbatim>\"Main"\ in session \<^verbatim>\"HOL"\. The optional percentage has the same meaning as in \<^bold>\type\~\node_status\ below. \<^item> \<^bold>\type\~\timing = {elapsed: double, cpu: double, gc: double}\ refers to common Isabelle timing information in seconds, usually with a precision of three digits after the point (whole milliseconds). \<^item> \<^bold>\type\~\uuid = string\ refers to a Universally Unique Identifier (UUID) as plain text.\<^footnote>\See \<^url>\https://www.ietf.org/rfc/rfc4122.txt\ and \<^url>\https://docs.oracle.com/en/java/javase/11/docs/api/java.base/java/util/UUID.html\.\ Such identifiers are created as private random numbers of the server and only revealed to the client that creates a certain resource (e.g.\ task or session). A client may disclose this information for use in a different client connection: this allows to share sessions between multiple connections. Client commands need to provide syntactically wellformed UUIDs: this is trivial to achieve by using only identifiers that have been produced by the server beforehand. \<^item> \<^bold>\type\~\task = {task: uuid}\ identifies a newly created asynchronous task and thus allows the client to control it by the \<^verbatim>\cancel\ command. The same task identification is included in all messages produced by this task. \<^item> \<^bold>\type\ \session_id = {session_id: uuid}\ identifies a newly created PIDE session managed by the server. Sessions are independent of client connections and may be shared by different clients, as long as the internal session identifier is known. \<^item> \<^bold>\type\ \node = {node_name: string, theory_name: string}\ represents the internal node name of a theory. The \node_name\ is derived from the - canonical theory file-name (e.g.\ \<^verbatim>\"~~/src/HOL/ex/Seq.thy"\ after + canonical theory file-name (e.g.\ \<^verbatim>\"~~/src/HOL/Examples/Seq.thy"\ after normalization within the file-system). The \theory_name\ is the - session-qualified theory name (e.g.\ \<^verbatim>\HOL-ex.Seq\). + session-qualified theory name (e.g.\ \<^verbatim>\HOL-Examples.Seq\). \<^item> \<^bold>\type\ \node_status = {ok: bool, total: int, unprocessed: int, running: int, warned: int, failed: int, finished: int, canceled: bool, consolidated: bool, percentage: int}\ represents a formal theory node status of the PIDE document model as follows. \<^item> Fields \total\, \unprocessed\, \running\, \warned\, \failed\, \finished\ account for individual commands within a theory node; \ok\ is an abstraction for \failed = 0\. \<^item> The \canceled\ flag tells if some command in the theory has been spontaneously canceled (by an Interrupt exception that could also indicate resource problems). \<^item> The \consolidated\ flag indicates whether the outermost theory command structure has finished (or failed) and the final \<^theory_text>\end\ command has been checked. \<^item> The \percentage\ field tells how far the node has been processed. It ranges between 0 and 99 in normal operation, and reaches 100 when the node has been formally consolidated as described above. \ section \Server commands and results\ text \ Here follows an overview of particular Isabelle server commands with their results, which are usually represented as JSON values with types according to \secref{sec:json-types}. The general format of input and output messages is described in \secref{sec:input-output-messages}. The relevant Isabelle/Scala source files are: \<^medskip> \begin{tabular}{l} \<^file>\$ISABELLE_HOME/src/Pure/Tools/server_commands.scala\ \\ \<^file>\$ISABELLE_HOME/src/Pure/Tools/server.scala\ \\ \<^file>\$ISABELLE_HOME/src/Pure/General/json.scala\ \\ \end{tabular} \ subsection \Command \<^verbatim>\help\\ text \ \begin{tabular}{ll} regular result: & \<^verbatim>\OK\ \[string]\ \\ \end{tabular} \<^medskip> The \<^verbatim>\help\ command has no argument and returns the list of server command names. This is occasionally useful for interactive experimentation (see also @{tool client} in \secref{sec:tool-client}). \ subsection \Command \<^verbatim>\echo\\ text \ \begin{tabular}{ll} argument: & \any\ \\ regular result: & \<^verbatim>\OK\ \any\ \\ \end{tabular} \<^medskip> The \<^verbatim>\echo\ command is the identity function: it returns its argument as regular result. This is occasionally useful for testing and interactive experimentation (see also @{tool client} in \secref{sec:tool-client}). The Scala type of \<^verbatim>\echo\ is actually more general than given above: \<^verbatim>\Unit\, \<^verbatim>\XML.Elem\, \<^verbatim>\JSON.T\ work uniformly. Note that \<^verbatim>\XML.Elem\ might be difficult to type on the console in its YXML syntax (\secref{sec:yxml-vs-xml}). \ subsection \Command \<^verbatim>\shutdown\\ text \ \begin{tabular}{ll} regular result: & \<^verbatim>\OK\ \\ \end{tabular} \<^medskip> The \<^verbatim>\shutdown\ command has no argument and result value. It forces a shutdown of the connected server process, stopping all open sessions and closing the server socket. This may disrupt pending commands on other connections! \<^medskip> The command-line invocation \<^verbatim>\isabelle server -x\ opens a server connection and issues a \<^verbatim>\shutdown\ command (see also \secref{sec:tool-server}). \ subsection \Command \<^verbatim>\cancel\\ text \ \begin{tabular}{ll} argument: & \task\ \\ regular result: & \<^verbatim>\OK\ \\ \end{tabular} \<^medskip> The command \<^verbatim>\cancel {"task":\~\id\\<^verbatim>\}\ attempts to cancel the specified task. Cancellation is merely a hint that the client prefers an ongoing process to be stopped. The command always succeeds formally, but it may get ignored by a task that is still running; it might also refer to a non-existing or no-longer existing task (without producing an error). Successful cancellation typically leads to an asynchronous failure of type \<^verbatim>\FAILED {\\task: uuid, message:\~\<^verbatim>\"Interrupt"}\. A different message is also possible, depending how the task handles the event. \ subsection \Command \<^verbatim>\session_build\ \label{sec:command-session-build}\ text \ \begin{tabular}{lll} argument: & \session_build_args\ \\ immediate result: & \<^verbatim>\OK\ \task\ \\ notifications: & \<^verbatim>\NOTE\ \task \ (theory_progress | message)\ \\ regular result: & \<^verbatim>\FINISHED\ \task \ session_build_results\ \\ error result: & \<^verbatim>\FAILED\ \task \ error_message \ session_build_results\ \\[2ex] \end{tabular} \begin{tabular}{lll} \<^bold>\type\ \session_build_args =\ \\ \quad\{session: string,\ \\ \quad~~\preferences?: string,\ & \<^bold>\default:\ server preferences \\ \quad~~\options?: [string],\ \\ \quad~~\dirs?: [string],\ \\ \quad~~\include_sessions: [string],\ \\ \quad~~\verbose?: bool}\ \\[2ex] \end{tabular} \begin{tabular}{ll} \<^bold>\type\ \session_build_result =\ \\ \quad\{session: string,\ \\ \quad~~\ok: bool,\ \\ \quad~~\return_code: int,\ \\ \quad~~\timeout: bool,\ \\ \quad~~\timing: timing}\ \\[2ex] \<^bold>\type\ \session_build_results =\ \\ \quad\{ok: bool,\ \\ \quad~~\return_code: int,\ \\ \quad~~\sessions: [session_build_result]}\ \\ \end{tabular} \ text \ The \<^verbatim>\session_build\ command prepares a session image for interactive use of theories. This is a limited version of command-line tool @{tool build} (\secref{sec:tool-build}), with specific options to request a formal context for an interactive PIDE session. The build process is asynchronous, with notifications that inform about the progress of loaded theories. Some further informative messages are output as well. Coordination of independent build processes is at the discretion of the client (or end-user), just as for @{tool build} and @{tool jedit}. There is no built-in coordination of conflicting builds with overlapping hierarchies of session images. In the worst case, a session image produced by one task may get overwritten by another task! \ subsubsection \Arguments\ text \ The \session\ field specifies the target session name. The build process will produce all required ancestor images according to the overall session graph. \<^medskip> The environment of Isabelle system options is determined from \preferences\ that are augmented by \options\, which is a list individual updates of the form the \name\\<^verbatim>\=\\value\ or \name\ (the latter abbreviates \name\\<^verbatim>\=true\); see also command-line option \<^verbatim>\-o\ for @{tool build}. The preferences are loaded from the file \<^path>\$ISABELLE_HOME_USER/etc/preferences\ by default, but the client may provide alternative contents for it (as text, not a file-name). This could be relevant in situations where client and server run in different operating-system contexts. \<^medskip> The \dirs\ field specifies additional directories for session ROOT and ROOTS files (\secref{sec:session-root}). This augments the name space of available sessions; see also option \<^verbatim>\-d\ in @{tool build}. \<^medskip> The \include_sessions\ field specifies sessions whose theories should be included in the overall name space of session-qualified theory names. This corresponds to a \<^bold>\sessions\ specification in ROOT files (\secref{sec:session-root}). It enables the \<^verbatim>\use_theories\ command (\secref{sec:command-use-theories}) to refer to sources from other sessions in a robust manner, instead of relying on directory locations. \<^medskip> The \verbose\ field set to \<^verbatim>\true\ yields extra verbosity. The effect is similar to option \<^verbatim>\-v\ in @{tool build}. \ subsubsection \Intermediate output\ text \ The asynchronous notifications of command \<^verbatim>\session_build\ mainly serve as progress indicator: the output resembles that of the session build window of Isabelle/jEdit after startup @{cite "isabelle-jedit"}. For the client it is usually sufficient to print the messages in plain text, but note that \theory_progress\ also reveals formal \theory\ and \session\ names directly. \ subsubsection \Results\ text \ The overall \session_build_results\ contain both a summary and an entry \session_build_result\ for each session in the build hierarchy. The result is always provided, independently of overall success (\<^verbatim>\FINISHED\ task) or failure (\<^verbatim>\FAILED\ task). The \ok\ field tells abstractly, whether all required session builds came out as \ok\, i.e.\ with zero \return_code\. A non-zero \return_code\ indicates an error according to usual POSIX conventions for process exit. The individual \session_build_result\ entries provide extra fields: \<^item> \timeout\ tells if the build process was aborted after running too long, \<^item> \timing\ gives the overall process timing in the usual Isabelle format with elapsed, CPU, GC time. \ subsubsection \Examples\ text \ Build of a session image from the Isabelle distribution: @{verbatim [display] \session_build {"session": "HOL-Word"}\} Build a session image from the Archive of Formal Proofs: @{verbatim [display] \session_build {"session": "Coinductive", "dirs": ["$AFP_BASE/thys"]}\} \ subsection \Command \<^verbatim>\session_start\ \label{sec:command-session-start}\ text \ \begin{tabular}{lll} argument: & \session_build_args \ {print_mode?: [string]}\ \\ immediate result: & \<^verbatim>\OK\ \task\ \\ notifications: & \<^verbatim>\NOTE\ \task \ (theory_progress | message)\ \\ regular result: & \<^verbatim>\FINISHED\ \task \ session_id \ {tmp_dir: string}\ \\ error result: & \<^verbatim>\FAILED\ \task \ error_message\ \\[2ex] \end{tabular} \<^medskip> The \<^verbatim>\session_start\ command starts a new Isabelle/PIDE session with underlying Isabelle/ML process, based on a session image that it produces on demand using \<^verbatim>\session_build\. Thus it accepts all \session_build_args\ and produces similar notifications, but the detailed \session_build_results\ are omitted. The session build and startup process is asynchronous: when the task is finished, the session remains active for commands, until a \<^verbatim>\session_stop\ or \<^verbatim>\shutdown\ command is sent to the server. Sessions are independent of client connections: it is possible to start a session and later apply \<^verbatim>\use_theories\ on different connections, as long as the internal session identifier is known: shared theory imports will be used only once (and persist until purged explicitly). \ subsubsection \Arguments\ text \ Most arguments are shared with \<^verbatim>\session_build\ (\secref{sec:command-session-build}). \<^medskip> The \print_mode\ field adds identifiers of print modes to be made active for this session. For example, \<^verbatim>\"print_mode": ["ASCII"]\ prefers ASCII replacement syntax over mathematical Isabelle symbols. See also option \<^verbatim>\-m\ in @{tool process} (\secref{sec:tool-process}). \ subsubsection \Results\ text \ The \session_id\ provides the internal identification of the session object within the sever process. It can remain active as long as the server is running, independently of the current client connection. \<^medskip> The \tmp_dir\ field refers to a temporary directory that is specifically created for this session and deleted after it has been stopped. This may serve as auxiliary file-space for the \<^verbatim>\use_theories\ command, but concurrent use requires some care in naming temporary files, e.g.\ by using sub-directories with globally unique names. As \tmp_dir\ is the default \master_dir\ for commands \<^verbatim>\use_theories\ and \<^verbatim>\purge_theories\, theory files copied there may be used without further path specification. \ subsubsection \Examples\ text \ Start a default Isabelle/HOL session: @{verbatim [display] \session_start {"session": "HOL"}\} Start a session from the Archive of Formal Proofs: @{verbatim [display] \session_start {"session": "Coinductive", "dirs": ["$AFP_BASE/thys"]}\} \ subsection \Command \<^verbatim>\session_stop\\ text \ \begin{tabular}{ll} argument: & \session_id\ \\ immediate result: & \<^verbatim>\OK\ \task\ \\ regular result: & \<^verbatim>\FINISHED\ \task \ session_stop_result\ \\ error result: & \<^verbatim>\FAILED\ \task \ error_message \ session_stop_result\ \\[2ex] \end{tabular} \begin{tabular}{l} \<^bold>\type\ \session_stop_result = {ok: bool, return_code: int}\ \end{tabular} \<^medskip> The \<^verbatim>\session_stop\ command forces a shutdown of the identified PIDE session. This asynchronous tasks usually finishes quickly. Failure only happens in unusual situations, according to the return code of the underlying Isabelle/ML process. \ subsubsection \Arguments\ text \ The \session_id\ provides the UUID originally created by the server for this session. \ subsubsection \Results\ text \ The \ok\ field tells abstractly, whether the Isabelle/ML process has terminated properly. The \return_code\ field expresses this information according to usual POSIX conventions for process exit. \ subsection \Command \<^verbatim>\use_theories\ \label{sec:command-use-theories}\ text \ \begin{tabular}{ll} argument: & \use_theories_arguments\ \\ immediate result: & \<^verbatim>\OK\ \task\ \\ regular result: & \<^verbatim>\FINISHED\ \use_theories_results\ \\ \end{tabular} \begin{tabular}{ll} \<^bold>\type\ \use_theories_arguments =\ \\ \quad\{session_id: uuid,\ \\ \quad~~\theories: [string],\ \\ \quad~~\master_dir?: string,\ & \<^bold>\default:\ session \tmp_dir\ \\ \quad~~\pretty_margin?: double,\ & \<^bold>\default:\ \<^verbatim>\76\ \\ \quad~~\unicode_symbols?: bool,\ \\ \quad~~\export_pattern?: string,\ \\ \quad~~\check_delay?: double,\ & \<^bold>\default:\ \<^verbatim>\0.5\ \\ \quad~~\check_limit?: int,\ \\ \quad~~\watchdog_timeout?: double,\ & \<^bold>\default:\ \<^verbatim>\600.0\ \\ \quad~~\nodes_status_delay?: double}\ & \<^bold>\default:\ \<^verbatim>\-1.0\ \\ \end{tabular} \begin{tabular}{ll} \<^bold>\type\ \export =\ \\ \quad~~\{name: string, base64: bool, body: string}\ \\ \<^bold>\type\ \node_results =\ \\ \quad~~\{status: node_status, messages: [message], exports: [export]}\ \\ \<^bold>\type\ \nodes_status =\ \\ \quad~~\[node \ {status: node_status}]\ \\ \<^bold>\type\ \use_theories_results =\ \\ \quad\{ok: bool,\ \\ \quad~~\errors: [message],\ \\ \quad~~\nodes: [node \ node_results]}\ \\ \end{tabular} \<^medskip> The \<^verbatim>\use_theories\ command updates the identified session by adding the current version of theory files to it, while dependencies are resolved implicitly. The command succeeds eventually, when all theories have status \<^emph>\terminated\ or \<^emph>\consolidated\ in the sense of \node_status\ (\secref{sec:json-types}). Already used theories persist in the session until purged explicitly (\secref{sec:command-purge-theories}). This also means that repeated invocations of \<^verbatim>\use_theories\ are idempotent: it could make sense to do that with different values for \pretty_margin\ or \unicode_symbols\ to get different formatting for \errors\ or \messages\. \<^medskip> A non-empty \export_pattern\ means that theory \exports\ are retrieved (see \secref{sec:tool-export}). An \export\ \name\ roughly follows file-system standards: ``\<^verbatim>\/\'' separated list of base names (excluding special names like ``\<^verbatim>\.\'' or ``\<^verbatim>\..\''). The \base64\ field specifies the format of the \body\ string: it is true for a byte vector that cannot be represented as plain text in UTF-8 encoding, which means the string needs to be decoded as in \<^verbatim>\java.util.Base64.getDecoder.decode(String)\. \<^medskip> The status of PIDE processing is checked every \check_delay\ seconds, and bounded by \check_limit\ attempts (default: 0, i.e.\ unbounded). A \check_limit > 0\ effectively specifies a global timeout of \check_delay \ check_limit\ seconds. \<^medskip> If \watchdog_timeout\ is greater than 0, it specifies the timespan (in seconds) after the last command status change of Isabelle/PIDE, before finishing with a potentially non-terminating or deadlocked execution. \<^medskip> A non-negative \nodes_status_delay\ enables continuous notifications of kind \nodes_status\, with a field of name and type \nodes_status\. The time interval is specified in seconds; by default it is negative and thus disabled. \ subsubsection \Arguments\ text \ The \session_id\ is the identifier provided by the server, when the session was created (possibly on a different client connection). \<^medskip> The \theories\ field specifies theory names as in theory \<^theory_text>\imports\ or in ROOT \<^bold>\theories\. \<^medskip> The \master_dir\ field specifies the master directory of imported theories: it acts like the ``current working directory'' for locating theory files. This is irrelevant for \theories\ with an absolute path name (e.g.\ - \<^verbatim>\"~~/src/HOL/ex/Seq.thy"\) or session-qualified theory name (e.g.\ - \<^verbatim>\"HOL-ex/Seq"\). + \<^verbatim>\"~~/src/HOL/Examples/Seq.thy"\) or session-qualified theory name (e.g.\ + \<^verbatim>\"HOL-Examples.Seq"\). \<^medskip> The \pretty_margin\ field specifies the line width for pretty-printing. The default is suitable for classic console output. Formatting happens at the end of \<^verbatim>\use_theories\, when all prover messages are exported to the client. \<^medskip> The \unicode_symbols\ field set to \<^verbatim>\true\ renders message output for direct output on a Unicode capable channel, ideally with the Isabelle fonts as in Isabelle/jEdit. The default is to keep the symbolic representation of Isabelle text, e.g.\ \<^verbatim>\\\ instead of its rendering as \\\. This means the client needs to perform its own rendering before presenting it to the end-user. \ subsubsection \Results\ text \ The \ok\ field indicates overall success of processing the specified theories with all their dependencies. When \ok\ is \<^verbatim>\false\, the \errors\ field lists all errors cumulatively (including imported theories). The messages contain position information for the original theory nodes. \<^medskip> The \nodes\ field provides detailed information about each imported theory node. The individual fields are as follows: \<^item> \node_name\: the canonical name for the theory node, based on its file-system location; \<^item> \theory_name\: the logical theory name; \<^item> \status\: the overall node status, e.g.\ see the visualization in the \Theories\ panel of Isabelle/jEdit @{cite "isabelle-jedit"}; \<^item> \messages\: the main bulk of prover messages produced in this theory (with kind \<^verbatim>\writeln\, \<^verbatim>\warning\, \<^verbatim>\error\). \ subsubsection \Examples\ text \ Process some example theory from the Isabelle distribution, within the context of an already started session for Isabelle/HOL (see also \secref{sec:command-session-start}): - @{verbatim [display] \use_theories {"session_id": ..., "theories": ["~~/src/HOL/ex/Seq"]}\} + @{verbatim [display] \use_theories {"session_id": ..., "theories": ["~~/src/HOL/Examples/Seq"]}\} \<^medskip> Process some example theories in the context of their (single) parent session: @{verbatim [display] \session_start {"session": "HOL-Library"} use_theories {"session_id": ..., "theories": ["~~/src/HOL/Unix/Unix"]} session_stop {"session_id": ...}\} \<^medskip> Process some example theories that import other theories via session-qualified theory names: @{verbatim [display] \session_start {"session": "HOL", "include_sessions": ["HOL-Unix"]} use_theories {"session_id": ..., "theories": ["HOL-Unix.Unix"]} session_stop {"session_id": ...}\} \ subsection \Command \<^verbatim>\purge_theories\ \label{sec:command-purge-theories}\ text \ \begin{tabular}{ll} argument: & \purge_theories_arguments\ \\ regular result: & \<^verbatim>\OK\ \purge_theories_result\ \\ \end{tabular} \begin{tabular}{lll} \<^bold>\type\ \purge_theories_arguments =\ \\ \quad\{session_id: uuid,\ \\ \quad~~\theories: [string],\ \\ \quad~~\master_dir?: string,\ & \<^bold>\default:\ session \tmp_dir\ \\ \quad~~\all?: bool}\ \\[2ex] \end{tabular} \begin{tabular}{ll} \<^bold>\type\ \purge_theories_result = {purged: [string]}\ \\ \end{tabular} \<^medskip> The \<^verbatim>\purge_theories\ command updates the identified session by removing theories that are no longer required: theories that are used in pending \<^verbatim>\use_theories\ tasks or imported by other theories are retained. \ subsubsection \Arguments\ text \ The \session_id\ is the identifier provided by the server, when the session was created (possibly on a different client connection). \<^medskip> The \theories\ field specifies theory names to be purged: imported dependencies are \<^emph>\not\ completed. Instead it is possible to provide the already completed import graph returned by \<^verbatim>\use_theories\ as \nodes\ / \node_name\. \<^medskip> The \master_dir\ field specifies the master directory as in \<^verbatim>\use_theories\. This is irrelevant, when passing fully-qualified theory node names (e.g.\ \node_name\ from \nodes\ in \use_theories_results\). \<^medskip> The \all\ field set to \<^verbatim>\true\ attempts to purge all presently loaded theories. \ subsubsection \Results\ text \ The \purged\ field gives the theory nodes that were actually removed. \<^medskip> The \retained\ field gives the remaining theory nodes, i.e.\ the complement of \purged\. \ end diff --git a/src/HOL/Examples/Cantor.thy b/src/HOL/Examples/Cantor.thy new file mode 100644 --- /dev/null +++ b/src/HOL/Examples/Cantor.thy @@ -0,0 +1,136 @@ +(* Title: HOL/Examples/Cantor.thy + Author: Makarius +*) + +section \Cantor's Theorem\ + +theory Cantor + imports Main +begin + +subsection \Mathematical statement and proof\ + +text \ + Cantor's Theorem states that there is no surjection from + a set to its powerset. The proof works by diagonalization. E.g.\ see + \<^item> \<^url>\http://mathworld.wolfram.com/CantorDiagonalMethod.html\ + \<^item> \<^url>\https://en.wikipedia.org/wiki/Cantor's_diagonal_argument\ +\ + +theorem Cantor: "\f :: 'a \ 'a set. \A. \x. A = f x" +proof + assume "\f :: 'a \ 'a set. \A. \x. A = f x" + then obtain f :: "'a \ 'a set" where *: "\A. \x. A = f x" .. + let ?D = "{x. x \ f x}" + from * obtain a where "?D = f a" by blast + moreover have "a \ ?D \ a \ f a" by blast + ultimately show False by blast +qed + + +subsection \Automated proofs\ + +text \ + These automated proofs are much shorter, but lack information why and how it + works. +\ + +theorem "\f :: 'a \ 'a set. \A. \x. f x = A" + by best + +theorem "\f :: 'a \ 'a set. \A. \x. f x = A" + by force + + +subsection \Elementary version in higher-order predicate logic\ + +text \ + The subsequent formulation bypasses set notation of HOL; it uses elementary + \\\-calculus and predicate logic, with standard introduction and elimination + rules. This also shows that the proof does not require classical reasoning. +\ + +lemma iff_contradiction: + assumes *: "\ A \ A" + shows False +proof (rule notE) + show "\ A" + proof + assume A + with * have "\ A" .. + from this and \A\ show False .. + qed + with * show A .. +qed + +theorem Cantor': "\f :: 'a \ 'a \ bool. \A. \x. A = f x" +proof + assume "\f :: 'a \ 'a \ bool. \A. \x. A = f x" + then obtain f :: "'a \ 'a \ bool" where *: "\A. \x. A = f x" .. + let ?D = "\x. \ f x x" + from * have "\x. ?D = f x" .. + then obtain a where "?D = f a" .. + then have "?D a \ f a a" by (rule arg_cong) + then have "\ f a a \ f a a" . + then show False by (rule iff_contradiction) +qed + + +subsection \Classic Isabelle/HOL example\ + +text \ + The following treatment of Cantor's Theorem follows the classic example from + the early 1990s, e.g.\ see the file \<^verbatim>\92/HOL/ex/set.ML\ in + Isabelle92 or @{cite \\S18.7\ "paulson-isa-book"}. The old tactic scripts + synthesize key information of the proof by refinement of schematic goal + states. In contrast, the Isar proof needs to say explicitly what is proven. + + \<^bigskip> + Cantor's Theorem states that every set has more subsets than it has + elements. It has become a favourite basic example in pure higher-order logic + since it is so easily expressed: + + @{text [display] + \\f::\ \ \ \ bool. \S::\ \ bool. \x::\. f x \ S\} + + Viewing types as sets, \\ \ bool\ represents the powerset of \\\. This + version of the theorem states that for every function from \\\ to its + powerset, some subset is outside its range. The Isabelle/Isar proofs below + uses HOL's set theory, with the type \\ set\ and the operator \range :: (\ \ + \) \ \ set\. +\ + +theorem "\S. S \ range (f :: 'a \ 'a set)" +proof + let ?S = "{x. x \ f x}" + show "?S \ range f" + proof + assume "?S \ range f" + then obtain y where "?S = f y" .. + then show False + proof (rule equalityCE) + assume "y \ f y" + assume "y \ ?S" + then have "y \ f y" .. + with \y \ f y\ show ?thesis by contradiction + next + assume "y \ ?S" + assume "y \ f y" + then have "y \ ?S" .. + with \y \ ?S\ show ?thesis by contradiction + qed + qed +qed + +text \ + How much creativity is required? As it happens, Isabelle can prove this + theorem automatically using best-first search. Depth-first search would + diverge, but best-first search successfully navigates through the large + search space. The context of Isabelle's classical prover contains rules for + the relevant constructs of HOL's set theory. +\ + +theorem "\S. S \ range (f :: 'a \ 'a set)" + by best + +end diff --git a/src/HOL/Examples/Drinker.thy b/src/HOL/Examples/Drinker.thy new file mode 100644 --- /dev/null +++ b/src/HOL/Examples/Drinker.thy @@ -0,0 +1,52 @@ +(* Title: HOL/Examples/Drinker.thy + Author: Makarius +*) + +section \The Drinker's Principle\ + +theory Drinker + imports Main +begin + +text \ + Here is another example of classical reasoning: the Drinker's Principle says + that for some person, if he is drunk, everybody else is drunk! + + We first prove a classical part of de-Morgan's law. +\ + +lemma de_Morgan: + assumes "\ (\x. P x)" + shows "\x. \ P x" +proof (rule classical) + assume "\x. \ P x" + have "\x. P x" + proof + fix x show "P x" + proof (rule classical) + assume "\ P x" + then have "\x. \ P x" .. + with \\x. \ P x\ show ?thesis by contradiction + qed + qed + with \\ (\x. P x)\ show ?thesis by contradiction +qed + +theorem Drinker's_Principle: "\x. drunk x \ (\x. drunk x)" +proof cases + assume "\x. drunk x" + then have "drunk a \ (\x. drunk x)" for a .. + then show ?thesis .. +next + assume "\ (\x. drunk x)" + then have "\x. \ drunk x" by (rule de_Morgan) + then obtain a where "\ drunk a" .. + have "drunk a \ (\x. drunk x)" + proof + assume "drunk a" + with \\ drunk a\ show "\x. drunk x" by contradiction + qed + then show ?thesis .. +qed + +end diff --git a/src/HOL/Examples/Knaster_Tarski.thy b/src/HOL/Examples/Knaster_Tarski.thy new file mode 100644 --- /dev/null +++ b/src/HOL/Examples/Knaster_Tarski.thy @@ -0,0 +1,107 @@ +(* Title: HOL/Examples/Knaster_Tarski.thy + Author: Makarius + +Typical textbook proof example. +*) + +section \Textbook-style reasoning: the Knaster-Tarski Theorem\ + +theory Knaster_Tarski + imports Main "HOL-Library.Lattice_Syntax" +begin + + +subsection \Prose version\ + +text \ + According to the textbook @{cite \pages 93--94\ "davey-priestley"}, the + Knaster-Tarski fixpoint theorem is as follows.\<^footnote>\We have dualized the + argument, and tuned the notation a little bit.\ + + \<^bold>\The Knaster-Tarski Fixpoint Theorem.\ Let \L\ be a complete lattice and + \f: L \ L\ an order-preserving map. Then \\{x \ L | f(x) \ x}\ is a fixpoint + of \f\. + + \<^bold>\Proof.\ Let \H = {x \ L | f(x) \ x}\ and \a = \H\. For all \x \ H\ we have + \a \ x\, so \f(a) \ f(x) \ x\. Thus \f(a)\ is a lower bound of \H\, whence + \f(a) \ a\. We now use this inequality to prove the reverse one (!) and + thereby complete the proof that \a\ is a fixpoint. Since \f\ is + order-preserving, \f(f(a)) \ f(a)\. This says \f(a) \ H\, so \a \ f(a)\.\ + + +subsection \Formal versions\ + +text \ + The Isar proof below closely follows the original presentation. Virtually + all of the prose narration has been rephrased in terms of formal Isar + language elements. Just as many textbook-style proofs, there is a strong + bias towards forward proof, and several bends in the course of reasoning. +\ + +theorem Knaster_Tarski: + fixes f :: "'a::complete_lattice \ 'a" + assumes "mono f" + shows "\a. f a = a" +proof + let ?H = "{u. f u \ u}" + let ?a = "\?H" + show "f ?a = ?a" + proof - + { + fix x + assume "x \ ?H" + then have "?a \ x" by (rule Inf_lower) + with \mono f\ have "f ?a \ f x" .. + also from \x \ ?H\ have "\ \ x" .. + finally have "f ?a \ x" . + } + then have "f ?a \ ?a" by (rule Inf_greatest) + { + also presume "\ \ f ?a" + finally (order_antisym) show ?thesis . + } + from \mono f\ and \f ?a \ ?a\ have "f (f ?a) \ f ?a" .. + then have "f ?a \ ?H" .. + then show "?a \ f ?a" by (rule Inf_lower) + qed +qed + +text \ + Above we have used several advanced Isar language elements, such as explicit + block structure and weak assumptions. Thus we have mimicked the particular + way of reasoning of the original text. + + In the subsequent version the order of reasoning is changed to achieve + structured top-down decomposition of the problem at the outer level, while + only the inner steps of reasoning are done in a forward manner. We are + certainly more at ease here, requiring only the most basic features of the + Isar language. +\ + +theorem Knaster_Tarski': + fixes f :: "'a::complete_lattice \ 'a" + assumes "mono f" + shows "\a. f a = a" +proof + let ?H = "{u. f u \ u}" + let ?a = "\?H" + show "f ?a = ?a" + proof (rule order_antisym) + show "f ?a \ ?a" + proof (rule Inf_greatest) + fix x + assume "x \ ?H" + then have "?a \ x" by (rule Inf_lower) + with \mono f\ have "f ?a \ f x" .. + also from \x \ ?H\ have "\ \ x" .. + finally show "f ?a \ x" . + qed + show "?a \ f ?a" + proof (rule Inf_lower) + from \mono f\ and \f ?a \ ?a\ have "f (f ?a) \ f ?a" .. + then show "f ?a \ ?H" .. + qed + qed +qed + +end diff --git a/src/HOL/Examples/ML.thy b/src/HOL/Examples/ML.thy new file mode 100644 --- /dev/null +++ b/src/HOL/Examples/ML.thy @@ -0,0 +1,157 @@ +(* Title: HOL/Examples/ML.thy + Author: Makarius +*) + +section \Isabelle/ML basics\ + +theory "ML" +imports Main +begin + +section \ML expressions\ + +text \ + The Isabelle command \<^theory_text>\ML\ allows to embed Isabelle/ML source into the + formal text. It is type-checked, compiled, and run within that environment. + + Note that side-effects should be avoided, unless the intention is to change + global parameters of the run-time environment (rare). + + ML top-level bindings are managed within the theory context. +\ + +ML \1 + 1\ + +ML \val a = 1\ +ML \val b = 1\ +ML \val c = a + b\ + + +section \Antiquotations\ + +text \ + There are some language extensions (via antiquotations), as explained in the + ``Isabelle/Isar implementation manual'', chapter 0. +\ + +ML \length []\ +ML \\<^assert> (length [] = 0)\ + + +text \Formal entities from the surrounding context may be referenced as + follows:\ + +term "1 + 1" \ \term within theory source\ + +ML \\<^term>\1 + 1\ (* term as symbolic ML datatype value *)\ + +ML \\<^term>\1 + (1::int)\\ + + +ML \ + (* formal source with position information *) + val s = \1 + 1\; + + (* read term via old-style string interface *) + val t = Syntax.read_term \<^context> (Syntax.implode_input s); +\ + + +section \Recursive ML evaluation\ + +ML \ + ML \ML \val a = @{thm refl}\\; + ML \val b = @{thm sym}\; + val c = @{thm trans} + val thms = [a, b, c]; +\ + + +section \IDE support\ + +text \ + ML embedded into the Isabelle environment is connected to the Prover IDE. + Poly/ML provides: + + \<^item> precise positions for warnings / errors + \<^item> markup for defining positions of identifiers + \<^item> markup for inferred types of sub-expressions + \<^item> pretty-printing of ML values with markup + \<^item> completion of ML names + \<^item> source-level debugger +\ + +ML \fn i => fn list => length list + i\ + + +section \Example: factorial and ackermann function in Isabelle/ML\ + +ML \ + fun factorial 0 = 1 + | factorial n = n * factorial (n - 1) +\ + +ML \factorial 42\ +ML \factorial 10000 div factorial 9999\ + +text \See \<^url>\http://mathworld.wolfram.com/AckermannFunction.html\.\ + +ML \ + fun ackermann 0 n = n + 1 + | ackermann m 0 = ackermann (m - 1) 1 + | ackermann m n = ackermann (m - 1) (ackermann m (n - 1)) +\ + +ML \timeit (fn () => ackermann 3 10)\ + + +section \Parallel Isabelle/ML\ + +text \ + Future.fork/join/cancel manage parallel evaluation. + + Note that within Isabelle theory documents, the top-level command boundary + may not be transgressed without special precautions. This is normally + managed by the system when performing parallel proof checking. +\ + +ML \ + val x = Future.fork (fn () => ackermann 3 10); + val y = Future.fork (fn () => ackermann 3 10); + val z = Future.join x + Future.join y +\ + +text \ + The \<^ML_structure>\Par_List\ module provides high-level combinators for + parallel list operations. +\ + +ML \timeit (fn () => map (fn n => ackermann 3 n) (1 upto 10))\ +ML \timeit (fn () => Par_List.map (fn n => ackermann 3 n) (1 upto 10))\ + + +section \Function specifications in Isabelle/HOL\ + +fun factorial :: "nat \ nat" +where + "factorial 0 = 1" +| "factorial (Suc n) = Suc n * factorial n" + +term "factorial 4" \ \symbolic term\ +value "factorial 4" \ \evaluation via ML code generation in the background\ + +declare [[ML_source_trace]] +ML \\<^term>\factorial 4\\ \ \symbolic term in ML\ +ML \@{code "factorial"}\ \ \ML code from function specification\ + + +fun ackermann :: "nat \ nat \ nat" +where + "ackermann 0 n = n + 1" +| "ackermann (Suc m) 0 = ackermann m 1" +| "ackermann (Suc m) (Suc n) = ackermann m (ackermann (Suc m) n)" + +value "ackermann 3 5" + +end + diff --git a/src/HOL/Examples/Peirce.thy b/src/HOL/Examples/Peirce.thy new file mode 100644 --- /dev/null +++ b/src/HOL/Examples/Peirce.thy @@ -0,0 +1,86 @@ +(* Title: HOL/Examples/Peirce.thy + Author: Makarius +*) + +section \Peirce's Law\ + +theory Peirce + imports Main +begin + +text \ + We consider Peirce's Law: \((A \ B) \ A) \ A\. This is an inherently + non-intuitionistic statement, so its proof will certainly involve some form + of classical contradiction. + + The first proof is again a well-balanced combination of plain backward and + forward reasoning. The actual classical step is where the negated goal may + be introduced as additional assumption. This eventually leads to a + contradiction.\<^footnote>\The rule involved there is negation elimination; it holds in + intuitionistic logic as well.\\ + +theorem "((A \ B) \ A) \ A" +proof + assume "(A \ B) \ A" + show A + proof (rule classical) + assume "\ A" + have "A \ B" + proof + assume A + with \\ A\ show B by contradiction + qed + with \(A \ B) \ A\ show A .. + qed +qed + +text \ + In the subsequent version the reasoning is rearranged by means of ``weak + assumptions'' (as introduced by \<^theory_text>\presume\). Before assuming the negated + goal \\ A\, its intended consequence \A \ B\ is put into place in order to + solve the main problem. Nevertheless, we do not get anything for free, but + have to establish \A \ B\ later on. The overall effect is that of a logical + \<^emph>\cut\. + + Technically speaking, whenever some goal is solved by \<^theory_text>\show\ in the context + of weak assumptions then the latter give rise to new subgoals, which may be + established separately. In contrast, strong assumptions (as introduced by + \<^theory_text>\assume\) are solved immediately. +\ + +theorem "((A \ B) \ A) \ A" +proof + assume "(A \ B) \ A" + show A + proof (rule classical) + presume "A \ B" + with \(A \ B) \ A\ show A .. + next + assume "\ A" + show "A \ B" + proof + assume A + with \\ A\ show B by contradiction + qed + qed +qed + +text \ + Note that the goals stemming from weak assumptions may be even left until + qed time, where they get eventually solved ``by assumption'' as well. In + that case there is really no fundamental difference between the two kinds of + assumptions, apart from the order of reducing the individual parts of the + proof configuration. + + Nevertheless, the ``strong'' mode of plain assumptions is quite important in + practice to achieve robustness of proof text interpretation. By forcing both + the conclusion \<^emph>\and\ the assumptions to unify with the pending goal to be + solved, goal selection becomes quite deterministic. For example, + decomposition with rules of the ``case-analysis'' type usually gives rise to + several goals that only differ in there local contexts. With strong + assumptions these may be still solved in any order in a predictable way, + while weak ones would quickly lead to great confusion, eventually demanding + even some backtracking. +\ + +end diff --git a/src/HOL/Examples/Seq.thy b/src/HOL/Examples/Seq.thy new file mode 100644 --- /dev/null +++ b/src/HOL/Examples/Seq.thy @@ -0,0 +1,35 @@ +(* Title: HOL/Examples/Seq.thy + Author: Makarius +*) + +section \Finite sequences\ + +theory Seq +imports Main +begin + +datatype 'a seq = Empty | Seq 'a "'a seq" + +fun conc :: "'a seq \ 'a seq \ 'a seq" +where + "conc Empty ys = ys" +| "conc (Seq x xs) ys = Seq x (conc xs ys)" + +fun reverse :: "'a seq \ 'a seq" +where + "reverse Empty = Empty" +| "reverse (Seq x xs) = conc (reverse xs) (Seq x Empty)" + +lemma conc_empty: "conc xs Empty = xs" + by (induct xs) simp_all + +lemma conc_assoc: "conc (conc xs ys) zs = conc xs (conc ys zs)" + by (induct xs) simp_all + +lemma reverse_conc: "reverse (conc xs ys) = conc (reverse ys) (reverse xs)" + by (induct xs) (simp_all add: conc_empty conc_assoc) + +lemma reverse_reverse: "reverse (reverse xs) = xs" + by (induct xs) (simp_all add: reverse_conc) + +end diff --git a/src/HOL/Examples/document/root.bib b/src/HOL/Examples/document/root.bib new file mode 100644 --- /dev/null +++ b/src/HOL/Examples/document/root.bib @@ -0,0 +1,114 @@ + +@string{CUCL="Comp. Lab., Univ. Camb."} +@string{CUP="Cambridge University Press"} +@string{Springer="Springer-Verlag"} +@string{TUM="TU Munich"} + +@article{church40, + author = "Alonzo Church", + title = "A Formulation of the Simple Theory of Types", + journal = "Journal of Symbolic Logic", + year = 1940, + volume = 5, + pages = "56-68"} + +@Book{Concrete-Math, + author = {R. L. Graham and D. E. Knuth and O. Patashnik}, + title = {Concrete Mathematics}, + publisher = {Addison-Wesley}, + year = 1989 +} + +@InProceedings{Naraschewski-Wenzel:1998:HOOL, + author = {Wolfgang Naraschewski and Markus Wenzel}, + title = {Object-Oriented Verification based on Record Subtyping in + {H}igher-{O}rder {L}ogic}, + crossref = {tphols98}} + +@Article{Nipkow:1998:Winskel, + author = {Tobias Nipkow}, + title = {Winskel is (almost) Right: Towards a Mechanized Semantics Textbook}, + journal = {Formal Aspects of Computing}, + year = 1998, + volume = 10, + pages = {171--186} +} + +@InProceedings{Wenzel:1999:TPHOL, + author = {Markus Wenzel}, + title = {{Isar} --- a Generic Interpretative Approach to Readable Formal Proof Documents}, + crossref = {tphols99}} + +@Book{Winskel:1993, + author = {G. Winskel}, + title = {The Formal Semantics of Programming Languages}, + publisher = {MIT Press}, + year = 1993 +} + +@Book{davey-priestley, + author = {B. A. Davey and H. A. Priestley}, + title = {Introduction to Lattices and Order}, + publisher = CUP, + year = 1990} + +@TechReport{Gordon:1985:HOL, + author = {M. J. C. Gordon}, + title = {{HOL}: A machine oriented formulation of higher order logic}, + institution = {University of Cambridge Computer Laboratory}, + year = 1985, + number = 68 +} + +@manual{isabelle-HOL, + author = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel}, + title = {{Isabelle}'s Logics: {HOL}}, + institution = {Institut f\"ur Informatik, Technische Universi\"at + M\"unchen and Computer Laboratory, University of Cambridge}} + +@manual{isabelle-intro, + author = {Lawrence C. Paulson}, + title = {Introduction to {Isabelle}}, + institution = CUCL} + +@manual{isabelle-isar-ref, + author = {Markus Wenzel}, + title = {The {Isabelle/Isar} Reference Manual}, + institution = TUM} + +@manual{isabelle-ref, + author = {Lawrence C. Paulson}, + title = {The {Isabelle} Reference Manual}, + institution = CUCL} + +@Book{paulson-isa-book, + author = {Lawrence C. Paulson}, + title = {Isabelle: A Generic Theorem Prover}, + publisher = {Springer}, + year = 1994, + note = {LNCS 828}} + +@TechReport{paulson-mutilated-board, + author = {Lawrence C. Paulson}, + title = {A Simple Formalization and Proof for the Mutilated Chess Board}, + institution = CUCL, + year = 1996, + number = 394, + note = {\url{http://www.cl.cam.ac.uk/users/lcp/papers/Reports/mutil.pdf}} +} + +@Proceedings{tphols98, + title = {Theorem Proving in Higher Order Logics: {TPHOLs} '98}, + booktitle = {Theorem Proving in Higher Order Logics: {TPHOLs} '98}, + editor = {Jim Grundy and Malcom Newey}, + series = {LNCS}, + volume = 1479, + year = 1998} + +@Proceedings{tphols99, + title = {Theorem Proving in Higher Order Logics: {TPHOLs} '99}, + booktitle = {Theorem Proving in Higher Order Logics: {TPHOLs} '99}, + editor = {Bertot, Y. and Dowek, G. and Hirschowitz, A. and + Paulin, C. and Thery, L.}, + series = {LNCS 1690}, + year = 1999} diff --git a/src/HOL/Examples/document/root.tex b/src/HOL/Examples/document/root.tex new file mode 100644 --- /dev/null +++ b/src/HOL/Examples/document/root.tex @@ -0,0 +1,25 @@ +\documentclass[11pt,a4paper]{article} +\usepackage[utf8]{inputenc} +\usepackage[T1]{fontenc} +\usepackage[only,bigsqcap]{stmaryrd} +\usepackage{ifthen,proof,amssymb,isabelle,isabellesym} + +\isabellestyle{literal} +\usepackage{pdfsetup}\urlstyle{rm} + + +\hyphenation{Isabelle} + +\begin{document} + +\title{Notable Examples in Isabelle/HOL} +\maketitle + +\parindent 0pt \parskip 0.5ex + +\input{session} + +\bibliographystyle{abbrv} +\bibliography{root} + +\end{document} diff --git a/src/HOL/Isar_Examples/Cantor.thy b/src/HOL/Isar_Examples/Cantor.thy deleted file mode 100644 --- a/src/HOL/Isar_Examples/Cantor.thy +++ /dev/null @@ -1,136 +0,0 @@ -(* Title: HOL/Isar_Examples/Cantor.thy - Author: Makarius -*) - -section \Cantor's Theorem\ - -theory Cantor - imports Main -begin - -subsection \Mathematical statement and proof\ - -text \ - Cantor's Theorem states that there is no surjection from - a set to its powerset. The proof works by diagonalization. E.g.\ see - \<^item> \<^url>\http://mathworld.wolfram.com/CantorDiagonalMethod.html\ - \<^item> \<^url>\https://en.wikipedia.org/wiki/Cantor's_diagonal_argument\ -\ - -theorem Cantor: "\f :: 'a \ 'a set. \A. \x. A = f x" -proof - assume "\f :: 'a \ 'a set. \A. \x. A = f x" - then obtain f :: "'a \ 'a set" where *: "\A. \x. A = f x" .. - let ?D = "{x. x \ f x}" - from * obtain a where "?D = f a" by blast - moreover have "a \ ?D \ a \ f a" by blast - ultimately show False by blast -qed - - -subsection \Automated proofs\ - -text \ - These automated proofs are much shorter, but lack information why and how it - works. -\ - -theorem "\f :: 'a \ 'a set. \A. \x. f x = A" - by best - -theorem "\f :: 'a \ 'a set. \A. \x. f x = A" - by force - - -subsection \Elementary version in higher-order predicate logic\ - -text \ - The subsequent formulation bypasses set notation of HOL; it uses elementary - \\\-calculus and predicate logic, with standard introduction and elimination - rules. This also shows that the proof does not require classical reasoning. -\ - -lemma iff_contradiction: - assumes *: "\ A \ A" - shows False -proof (rule notE) - show "\ A" - proof - assume A - with * have "\ A" .. - from this and \A\ show False .. - qed - with * show A .. -qed - -theorem Cantor': "\f :: 'a \ 'a \ bool. \A. \x. A = f x" -proof - assume "\f :: 'a \ 'a \ bool. \A. \x. A = f x" - then obtain f :: "'a \ 'a \ bool" where *: "\A. \x. A = f x" .. - let ?D = "\x. \ f x x" - from * have "\x. ?D = f x" .. - then obtain a where "?D = f a" .. - then have "?D a \ f a a" by (rule arg_cong) - then have "\ f a a \ f a a" . - then show False by (rule iff_contradiction) -qed - - -subsection \Classic Isabelle/HOL example\ - -text \ - The following treatment of Cantor's Theorem follows the classic example from - the early 1990s, e.g.\ see the file \<^verbatim>\92/HOL/ex/set.ML\ in - Isabelle92 or @{cite \\S18.7\ "paulson-isa-book"}. The old tactic scripts - synthesize key information of the proof by refinement of schematic goal - states. In contrast, the Isar proof needs to say explicitly what is proven. - - \<^bigskip> - Cantor's Theorem states that every set has more subsets than it has - elements. It has become a favourite basic example in pure higher-order logic - since it is so easily expressed: - - @{text [display] - \\f::\ \ \ \ bool. \S::\ \ bool. \x::\. f x \ S\} - - Viewing types as sets, \\ \ bool\ represents the powerset of \\\. This - version of the theorem states that for every function from \\\ to its - powerset, some subset is outside its range. The Isabelle/Isar proofs below - uses HOL's set theory, with the type \\ set\ and the operator \range :: (\ \ - \) \ \ set\. -\ - -theorem "\S. S \ range (f :: 'a \ 'a set)" -proof - let ?S = "{x. x \ f x}" - show "?S \ range f" - proof - assume "?S \ range f" - then obtain y where "?S = f y" .. - then show False - proof (rule equalityCE) - assume "y \ f y" - assume "y \ ?S" - then have "y \ f y" .. - with \y \ f y\ show ?thesis by contradiction - next - assume "y \ ?S" - assume "y \ f y" - then have "y \ ?S" .. - with \y \ ?S\ show ?thesis by contradiction - qed - qed -qed - -text \ - How much creativity is required? As it happens, Isabelle can prove this - theorem automatically using best-first search. Depth-first search would - diverge, but best-first search successfully navigates through the large - search space. The context of Isabelle's classical prover contains rules for - the relevant constructs of HOL's set theory. -\ - -theorem "\S. S \ range (f :: 'a \ 'a set)" - by best - -end diff --git a/src/HOL/Isar_Examples/Drinker.thy b/src/HOL/Isar_Examples/Drinker.thy deleted file mode 100644 --- a/src/HOL/Isar_Examples/Drinker.thy +++ /dev/null @@ -1,52 +0,0 @@ -(* Title: HOL/Isar_Examples/Drinker.thy - Author: Makarius -*) - -section \The Drinker's Principle\ - -theory Drinker - imports Main -begin - -text \ - Here is another example of classical reasoning: the Drinker's Principle says - that for some person, if he is drunk, everybody else is drunk! - - We first prove a classical part of de-Morgan's law. -\ - -lemma de_Morgan: - assumes "\ (\x. P x)" - shows "\x. \ P x" -proof (rule classical) - assume "\x. \ P x" - have "\x. P x" - proof - fix x show "P x" - proof (rule classical) - assume "\ P x" - then have "\x. \ P x" .. - with \\x. \ P x\ show ?thesis by contradiction - qed - qed - with \\ (\x. P x)\ show ?thesis by contradiction -qed - -theorem Drinker's_Principle: "\x. drunk x \ (\x. drunk x)" -proof cases - assume "\x. drunk x" - then have "drunk a \ (\x. drunk x)" for a .. - then show ?thesis .. -next - assume "\ (\x. drunk x)" - then have "\x. \ drunk x" by (rule de_Morgan) - then obtain a where "\ drunk a" .. - have "drunk a \ (\x. drunk x)" - proof - assume "drunk a" - with \\ drunk a\ show "\x. drunk x" by contradiction - qed - then show ?thesis .. -qed - -end diff --git a/src/HOL/Isar_Examples/Knaster_Tarski.thy b/src/HOL/Isar_Examples/Knaster_Tarski.thy deleted file mode 100644 --- a/src/HOL/Isar_Examples/Knaster_Tarski.thy +++ /dev/null @@ -1,107 +0,0 @@ -(* Title: HOL/Isar_Examples/Knaster_Tarski.thy - Author: Makarius - -Typical textbook proof example. -*) - -section \Textbook-style reasoning: the Knaster-Tarski Theorem\ - -theory Knaster_Tarski - imports Main "HOL-Library.Lattice_Syntax" -begin - - -subsection \Prose version\ - -text \ - According to the textbook @{cite \pages 93--94\ "davey-priestley"}, the - Knaster-Tarski fixpoint theorem is as follows.\<^footnote>\We have dualized the - argument, and tuned the notation a little bit.\ - - \<^bold>\The Knaster-Tarski Fixpoint Theorem.\ Let \L\ be a complete lattice and - \f: L \ L\ an order-preserving map. Then \\{x \ L | f(x) \ x}\ is a fixpoint - of \f\. - - \<^bold>\Proof.\ Let \H = {x \ L | f(x) \ x}\ and \a = \H\. For all \x \ H\ we have - \a \ x\, so \f(a) \ f(x) \ x\. Thus \f(a)\ is a lower bound of \H\, whence - \f(a) \ a\. We now use this inequality to prove the reverse one (!) and - thereby complete the proof that \a\ is a fixpoint. Since \f\ is - order-preserving, \f(f(a)) \ f(a)\. This says \f(a) \ H\, so \a \ f(a)\.\ - - -subsection \Formal versions\ - -text \ - The Isar proof below closely follows the original presentation. Virtually - all of the prose narration has been rephrased in terms of formal Isar - language elements. Just as many textbook-style proofs, there is a strong - bias towards forward proof, and several bends in the course of reasoning. -\ - -theorem Knaster_Tarski: - fixes f :: "'a::complete_lattice \ 'a" - assumes "mono f" - shows "\a. f a = a" -proof - let ?H = "{u. f u \ u}" - let ?a = "\?H" - show "f ?a = ?a" - proof - - { - fix x - assume "x \ ?H" - then have "?a \ x" by (rule Inf_lower) - with \mono f\ have "f ?a \ f x" .. - also from \x \ ?H\ have "\ \ x" .. - finally have "f ?a \ x" . - } - then have "f ?a \ ?a" by (rule Inf_greatest) - { - also presume "\ \ f ?a" - finally (order_antisym) show ?thesis . - } - from \mono f\ and \f ?a \ ?a\ have "f (f ?a) \ f ?a" .. - then have "f ?a \ ?H" .. - then show "?a \ f ?a" by (rule Inf_lower) - qed -qed - -text \ - Above we have used several advanced Isar language elements, such as explicit - block structure and weak assumptions. Thus we have mimicked the particular - way of reasoning of the original text. - - In the subsequent version the order of reasoning is changed to achieve - structured top-down decomposition of the problem at the outer level, while - only the inner steps of reasoning are done in a forward manner. We are - certainly more at ease here, requiring only the most basic features of the - Isar language. -\ - -theorem Knaster_Tarski': - fixes f :: "'a::complete_lattice \ 'a" - assumes "mono f" - shows "\a. f a = a" -proof - let ?H = "{u. f u \ u}" - let ?a = "\?H" - show "f ?a = ?a" - proof (rule order_antisym) - show "f ?a \ ?a" - proof (rule Inf_greatest) - fix x - assume "x \ ?H" - then have "?a \ x" by (rule Inf_lower) - with \mono f\ have "f ?a \ f x" .. - also from \x \ ?H\ have "\ \ x" .. - finally show "f ?a \ x" . - qed - show "?a \ f ?a" - proof (rule Inf_lower) - from \mono f\ and \f ?a \ ?a\ have "f (f ?a) \ f ?a" .. - then show "f ?a \ ?H" .. - qed - qed -qed - -end diff --git a/src/HOL/Isar_Examples/Peirce.thy b/src/HOL/Isar_Examples/Peirce.thy deleted file mode 100644 --- a/src/HOL/Isar_Examples/Peirce.thy +++ /dev/null @@ -1,86 +0,0 @@ -(* Title: HOL/Isar_Examples/Peirce.thy - Author: Makarius -*) - -section \Peirce's Law\ - -theory Peirce - imports Main -begin - -text \ - We consider Peirce's Law: \((A \ B) \ A) \ A\. This is an inherently - non-intuitionistic statement, so its proof will certainly involve some form - of classical contradiction. - - The first proof is again a well-balanced combination of plain backward and - forward reasoning. The actual classical step is where the negated goal may - be introduced as additional assumption. This eventually leads to a - contradiction.\<^footnote>\The rule involved there is negation elimination; it holds in - intuitionistic logic as well.\\ - -theorem "((A \ B) \ A) \ A" -proof - assume "(A \ B) \ A" - show A - proof (rule classical) - assume "\ A" - have "A \ B" - proof - assume A - with \\ A\ show B by contradiction - qed - with \(A \ B) \ A\ show A .. - qed -qed - -text \ - In the subsequent version the reasoning is rearranged by means of ``weak - assumptions'' (as introduced by \<^theory_text>\presume\). Before assuming the negated - goal \\ A\, its intended consequence \A \ B\ is put into place in order to - solve the main problem. Nevertheless, we do not get anything for free, but - have to establish \A \ B\ later on. The overall effect is that of a logical - \<^emph>\cut\. - - Technically speaking, whenever some goal is solved by \<^theory_text>\show\ in the context - of weak assumptions then the latter give rise to new subgoals, which may be - established separately. In contrast, strong assumptions (as introduced by - \<^theory_text>\assume\) are solved immediately. -\ - -theorem "((A \ B) \ A) \ A" -proof - assume "(A \ B) \ A" - show A - proof (rule classical) - presume "A \ B" - with \(A \ B) \ A\ show A .. - next - assume "\ A" - show "A \ B" - proof - assume A - with \\ A\ show B by contradiction - qed - qed -qed - -text \ - Note that the goals stemming from weak assumptions may be even left until - qed time, where they get eventually solved ``by assumption'' as well. In - that case there is really no fundamental difference between the two kinds of - assumptions, apart from the order of reducing the individual parts of the - proof configuration. - - Nevertheless, the ``strong'' mode of plain assumptions is quite important in - practice to achieve robustness of proof text interpretation. By forcing both - the conclusion \<^emph>\and\ the assumptions to unify with the pending goal to be - solved, goal selection becomes quite deterministic. For example, - decomposition with rules of the ``case-analysis'' type usually gives rise to - several goals that only differ in there local contexts. With strong - assumptions these may be still solved in any order in a predictable way, - while weak ones would quickly lead to great confusion, eventually demanding - even some backtracking. -\ - -end diff --git a/src/HOL/Proofs/ex/XML_Data.thy b/src/HOL/Proofs/ex/XML_Data.thy --- a/src/HOL/Proofs/ex/XML_Data.thy +++ b/src/HOL/Proofs/ex/XML_Data.thy @@ -1,58 +1,58 @@ (* Title: HOL/Proofs/ex/XML_Data.thy Author: Makarius Author: Stefan Berghofer XML data representation of proof terms. *) theory XML_Data - imports "HOL-Isar_Examples.Drinker" + imports "HOL-Examples.Drinker" begin subsection \Export and re-import of global proof terms\ ML \ fun export_proof thy thm = thm |> Proof_Syntax.standard_proof_of {full = true, expand_name = Thm.expand_name thm} |> Proofterm.encode (Sign.consts_of thy); fun import_proof thy xml = let val prf = Proofterm.decode (Sign.consts_of thy) xml; val (prf', _) = Proofterm.freeze_thaw_prf prf; in Drule.export_without_context (Proof_Checker.thm_of_proof thy prf') end; \ subsection \Examples\ ML \val thy1 = \<^theory>\ lemma ex: "A \ A" .. ML_val \ val xml = export_proof thy1 @{thm ex}; val thm = import_proof thy1 xml; \ ML_val \ val xml = export_proof thy1 @{thm de_Morgan}; val thm = import_proof thy1 xml; \ ML_val \ val xml = export_proof thy1 @{thm Drinker's_Principle}; val thm = import_proof thy1 xml; \ text \Some fairly large proof:\ ML_val \ val xml = export_proof thy1 @{thm abs_less_iff}; val thm = import_proof thy1 xml; val xml_size = size (YXML.string_of_body xml); \<^assert> (xml_size > 100000); \ end diff --git a/src/HOL/ROOT b/src/HOL/ROOT --- a/src/HOL/ROOT +++ b/src/HOL/ROOT @@ -1,1153 +1,1165 @@ chapter HOL session HOL (main) = Pure + description " Classical Higher-order Logic. " options [strict_facts] sessions Tools theories Main (global) Complex_Main (global) document_files "root.bib" "root.tex" +session "HOL-Examples" in Examples = HOL + + description " + Notable Examples in Isabelle/HOL. + " + sessions + "HOL-Library" + theories + Knaster_Tarski + Peirce + Drinker + Cantor + Seq + "ML" + document_files + "root.bib" + "root.tex" + + session "HOL-Proofs" (timing) in Proofs = Pure + description " HOL-Main with explicit proof terms. " options [quick_and_dirty = false, record_proofs = 2, parallel_limit = 500] sessions "HOL-Library" theories "HOL-Library.Realizers" session "HOL-Library" (main timing) in Library = HOL + description " Classical Higher-order Logic -- batteries included. " theories Library (*conflicting type class instantiations and dependent applications*) Finite_Lattice List_Lexorder List_Lenlexorder Prefix_Order Product_Lexorder Product_Order Subseq_Order (*conflicting syntax*) Datatype_Records (*data refinements and dependent applications*) AList_Mapping Code_Binary_Nat Code_Prolog Code_Real_Approx_By_Float Code_Target_Numeral DAList DAList_Multiset RBT_Mapping RBT_Set (*printing modifications*) OptionalSugar (*prototypic tools*) Predicate_Compile_Quickcheck Quantified_Premise_Simproc (*legacy tools*) Old_Datatype Old_Recdef Realizers Refute document_files "root.bib" "root.tex" session "HOL-Analysis" (main timing) in Analysis = HOL + options [document_tags = "theorem%important,corollary%important,proposition%important,class%important,instantiation%important,subsubsection%unimportant,%unimportant", document_variants = "document:manual=-proof,-ML,-unimportant"] sessions "HOL-Library" "HOL-Computational_Algebra" theories Analysis document_files "root.tex" "root.bib" session "HOL-Complex_Analysis" (main timing) in Complex_Analysis = "HOL-Analysis" + options [document_tags = "theorem%important,corollary%important,proposition%important,class%important,instantiation%important,subsubsection%unimportant,%unimportant", document_variants = "document:manual=-proof,-ML,-unimportant"] theories Complex_Analysis document_files "root.tex" "root.bib" session "HOL-Analysis-ex" in "Analysis/ex" = "HOL-Analysis" + theories Approximations Metric_Arith_Examples session "HOL-Homology" (timing) in Homology = "HOL-Analysis" + options [document_tags = "theorem%important,corollary%important,proposition%important,class%important,instantiation%important,subsubsection%unimportant,%unimportant", document_variants = "document:manual=-proof,-ML,-unimportant"] sessions "HOL-Algebra" theories Homology document_files "root.tex" session "HOL-Computational_Algebra" (main timing) in "Computational_Algebra" = "HOL-Library" + theories Computational_Algebra (*conflicting type class instantiations and dependent applications*) Field_as_Ring session "HOL-Real_Asymp" in Real_Asymp = HOL + sessions "HOL-Decision_Procs" theories Real_Asymp Real_Asymp_Approx Real_Asymp_Examples session "HOL-Real_Asymp-Manual" in "Real_Asymp/Manual" = "HOL-Real_Asymp" + theories Real_Asymp_Doc document_files (in "~~/src/Doc") "iman.sty" "extra.sty" "isar.sty" document_files "root.tex" "style.sty" session "HOL-Hahn_Banach" in Hahn_Banach = HOL + description " Author: Gertrud Bauer, TU Munich The Hahn-Banach theorem for real vector spaces. This is the proof of the Hahn-Banach theorem for real vectorspaces, following H. Heuser, Funktionalanalysis, p. 228 -232. The Hahn-Banach theorem is one of the fundamental theorems of functional analysis. It is a conclusion of Zorn's lemma. Two different formaulations of the theorem are presented, one for general real vectorspaces and its application to normed vectorspaces. The theorem says, that every continous linearform, defined on arbitrary subspaces (not only one-dimensional subspaces), can be extended to a continous linearform on the whole vectorspace. " sessions "HOL-Analysis" theories Hahn_Banach document_files "root.bib" "root.tex" session "HOL-Induct" in Induct = HOL + description " Examples of (Co)Inductive Definitions. Comb proves the Church-Rosser theorem for combinators (see http://www.cl.cam.ac.uk/ftp/papers/reports/TR396-lcp-generic-automatic-proof-tools.ps.gz). Mutil is the famous Mutilated Chess Board problem (see http://www.cl.cam.ac.uk/ftp/papers/reports/TR394-lcp-mutilated-chess-board.dvi.gz). PropLog proves the completeness of a formalization of propositional logic (see http://www.cl.cam.ac.uk/Research/Reports/TR312-lcp-set-II.ps.gz). Exp demonstrates the use of iterated inductive definitions to reason about mutually recursive relations. " sessions "HOL-Library" theories [quick_and_dirty] Common_Patterns theories Nested_Datatype QuoDataType QuoNestedDataType Term SList ABexp Infinitely_Branching_Tree Ordinals Sigma_Algebra Comb PropLog Com document_files "root.tex" session "HOL-IMP" (timing) in IMP = "HOL-Library" + options [document_variants = document] theories BExp ASM Finite_Reachable Denotational Compiler2 Poly_Types Sec_Typing Sec_TypingT Def_Init_Big Def_Init_Small Fold Live Live_True Hoare_Examples Hoare_Sound_Complete VCG Hoare_Total VCG_Total_EX VCG_Total_EX2 Collecting1 Collecting_Examples Abs_Int_Tests Abs_Int1_parity Abs_Int1_const Abs_Int3 Procs_Dyn_Vars_Dyn Procs_Stat_Vars_Dyn Procs_Stat_Vars_Stat C_like OO document_files "root.bib" "root.tex" session "HOL-IMPP" in IMPP = HOL + description \ Author: David von Oheimb Copyright 1999 TUM IMPP -- An imperative language with procedures. This is an extension of IMP with local variables and mutually recursive procedures. For documentation see "Hoare Logic for Mutual Recursion and Local Variables" (https://isabelle.in.tum.de/Bali/papers/FSTTCS99.html). \ theories EvenOdd session "HOL-Data_Structures" (timing) in Data_Structures = HOL + options [document_variants = document] sessions "HOL-Number_Theory" theories [document = false] Less_False theories Sorting Balance Tree_Map Interval_Tree AVL_Map AVL_Bal_Set AVL_Bal2_Set Height_Balanced_Tree RBT_Set2 RBT_Map Tree23_Map Tree234_Map Brother12_Map AA_Map Set2_Join_RBT Array_Braun Trie_Fun Trie_Map Tries_Binary Leftist_Heap Binomial_Heap document_files "root.tex" "root.bib" session "HOL-Import" in Import = HOL + theories HOL_Light_Maps theories [condition = HOL_LIGHT_BUNDLE] HOL_Light_Import session "HOL-Number_Theory" (main timing) in Number_Theory = "HOL-Computational_Algebra" + description " Fundamental Theorem of Arithmetic, Chinese Remainder Theorem, Fermat/Euler Theorem, Wilson's Theorem, some lemmas for Quadratic Reciprocity. " sessions "HOL-Algebra" theories Number_Theory document_files "root.tex" session "HOL-Hoare" in Hoare = HOL + description " Verification of imperative programs (verification conditions are generated automatically from pre/post conditions and loop invariants). " theories Hoare document_files "root.bib" "root.tex" session "HOL-Hoare_Parallel" (timing) in Hoare_Parallel = HOL + description " Verification of shared-variable imperative programs a la Owicki-Gries. (verification conditions are generated automatically). " theories Hoare_Parallel document_files "root.bib" "root.tex" session "HOL-Codegenerator_Test" in Codegenerator_Test = "HOL-Number_Theory" + sessions "HOL-Data_Structures" "HOL-ex" theories Generate Generate_Binary_Nat Generate_Target_Nat Generate_Efficient_Datastructures Code_Lazy_Test Code_Test_PolyML Code_Test_Scala theories [condition = ISABELLE_GHC] Code_Test_GHC theories [condition = ISABELLE_MLTON] Code_Test_MLton theories [condition = ISABELLE_OCAMLFIND] Code_Test_OCaml theories [condition = ISABELLE_SMLNJ] Code_Test_SMLNJ session "HOL-Metis_Examples" (timing) in Metis_Examples = "HOL-Library" + description " Author: Lawrence C Paulson, Cambridge University Computer Laboratory Author: Jasmin Blanchette, TU Muenchen Testing Metis and Sledgehammer. " sessions "HOL-Decision_Procs" theories Abstraction Big_O Binary_Tree Clausification Message Proxies Tarski Trans_Closure Sets session "HOL-Nitpick_Examples" in Nitpick_Examples = "HOL-Library" + description " Author: Jasmin Blanchette, TU Muenchen Copyright 2009 " theories [quick_and_dirty] Nitpick_Examples session "HOL-Algebra" (main timing) in Algebra = "HOL-Computational_Algebra" + description " Author: Clemens Ballarin, started 24 September 1999, and many others The Isabelle Algebraic Library. " sessions "HOL-Cardinals" theories (* Orders and Lattices *) Galois_Connection (* Knaster-Tarski theorem and Galois connections *) (* Groups *) FiniteProduct (* Product operator for commutative groups *) Sylow (* Sylow's theorem *) Bij (* Automorphism Groups *) Multiplicative_Group Zassenhaus (* The Zassenhaus lemma *) (* Rings *) Divisibility (* Rings *) IntRing (* Ideals and residue classes *) UnivPoly (* Polynomials *) (* Main theory *) Algebra document_files "root.bib" "root.tex" session "HOL-Auth" (timing) in Auth = HOL + description " A new approach to verifying authentication protocols. " sessions "HOL-Library" directories "Smartcard" "Guard" theories Auth_Shared Auth_Public "Smartcard/Auth_Smartcard" "Guard/Auth_Guard_Shared" "Guard/Auth_Guard_Public" document_files "root.tex" session "HOL-UNITY" (timing) in UNITY = "HOL-Auth" + description " Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1998 University of Cambridge Verifying security protocols using Chandy and Misra's UNITY formalism. " directories "Simple" "Comp" theories (*Basic meta-theory*) UNITY_Main (*Simple examples: no composition*) "Simple/Deadlock" "Simple/Common" "Simple/Network" "Simple/Token" "Simple/Channel" "Simple/Lift" "Simple/Mutex" "Simple/Reach" "Simple/Reachability" (*Verifying security protocols using UNITY*) "Simple/NSP_Bad" (*Example of composition*) "Comp/Handshake" (*Universal properties examples*) "Comp/Counter" "Comp/Counterc" "Comp/Priority" "Comp/TimerArray" "Comp/Progress" "Comp/Alloc" "Comp/AllocImpl" "Comp/Client" (*obsolete*) ELT document_files "root.tex" session "HOL-Unix" in Unix = HOL + options [print_mode = "no_brackets,no_type_brackets"] sessions "HOL-Library" theories Unix document_files "root.bib" "root.tex" session "HOL-ZF" in ZF = HOL + sessions "HOL-Library" theories MainZF Games document_files "root.tex" session "HOL-Imperative_HOL" (timing) in Imperative_HOL = HOL + options [print_mode = "iff,no_brackets"] sessions "HOL-Library" directories "ex" theories Imperative_HOL_ex document_files "root.bib" "root.tex" session "HOL-Decision_Procs" (timing) in Decision_Procs = "HOL-Algebra" + description " Various decision procedures, typically involving reflection. " directories "ex" theories Decision_Procs session "HOL-Proofs-ex" in "Proofs/ex" = "HOL-Proofs" + sessions "HOL-Isar_Examples" theories Hilbert_Classical Proof_Terms XML_Data session "HOL-Proofs-Extraction" (timing) in "Proofs/Extraction" = "HOL-Proofs" + description " Examples for program extraction in Higher-Order Logic. " options [quick_and_dirty = false] sessions "HOL-Computational_Algebra" theories Greatest_Common_Divisor Warshall Higman_Extraction Pigeonhole Euclid document_files "root.bib" "root.tex" session "HOL-Proofs-Lambda" (timing) in "Proofs/Lambda" = "HOL-Proofs" + description \ Lambda Calculus in de Bruijn's Notation. This session defines lambda-calculus terms with de Bruijn indixes and proves confluence of beta, eta and beta+eta. 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", quick_and_dirty = false] sessions "HOL-Library" theories Eta StrongNorm Standardization WeakNorm document_files "root.bib" "root.tex" session "HOL-Prolog" in Prolog = HOL + description " Author: David von Oheimb (based on a lecture on Lambda Prolog by Nadathur) A bare-bones implementation of Lambda-Prolog. This is a simple exploratory implementation of Lambda-Prolog in HOL, including some minimal examples (in Test.thy) and a more typical example of a little functional language and its type system. " theories Test Type session "HOL-MicroJava" (timing) in MicroJava = HOL + description " Formalization of a fragment of Java, together with a corresponding virtual machine and a specification of its bytecode verifier and a lightweight bytecode verifier, including proofs of type-safety. " sessions "HOL-Library" "HOL-Eisbach" directories "BV" "Comp" "DFA" "J" "JVM" theories MicroJava document_files "introduction.tex" "root.bib" "root.tex" session "HOL-NanoJava" in NanoJava = HOL + description " Hoare Logic for a tiny fragment of Java. " theories Example document_files "root.bib" "root.tex" session "HOL-Bali" (timing) in Bali = HOL + sessions "HOL-Library" theories AxExample AxSound AxCompl Trans TypeSafe document_files "root.tex" session "HOL-IOA" in IOA = HOL + description \ Author: Tobias Nipkow and Konrad Slind and Olaf Müller Copyright 1994--1996 TU Muenchen The meta-theory of I/O-Automata in HOL. This formalization has been significantly changed and extended, see HOLCF/IOA. There are also the proofs of two communication protocols which formerly have been here. @inproceedings{Nipkow-Slind-IOA, author={Tobias Nipkow and Konrad Slind}, title={{I/O} Automata in {Isabelle/HOL}}, booktitle={Proc.\ TYPES Workshop 1994}, publisher=Springer, series=LNCS, note={To appear}} ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/ioa.ps.gz and @inproceedings{Mueller-Nipkow, author={Olaf M\"uller and Tobias Nipkow}, title={Combining Model Checking and Deduction for {I/O}-Automata}, booktitle={Proc.\ TACAS Workshop}, organization={Aarhus University, BRICS report}, year=1995} ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/tacas.dvi.gz \ theories Solve session "HOL-Lattice" in Lattice = HOL + description " Author: Markus Wenzel, TU Muenchen Basic theory of lattices and orders. " theories CompleteLattice document_files "root.tex" session "HOL-ex" (timing) in ex = "HOL-Number_Theory" + description " Miscellaneous examples for Higher-Order Logic. " theories Adhoc_Overloading_Examples Antiquote Argo_Examples Arith_Examples Ballot BinEx Birthday_Paradox Bit_Lists Bubblesort CTL Cartouche_Examples Case_Product Chinese Classical Code_Binary_Nat_examples Code_Lazy_Demo Code_Timing Coercion_Examples Coherent Commands Computations Conditional_Parametricity_Examples Cubic_Quartic Datatype_Record_Examples Dedekind_Real Erdoes_Szekeres Eval_Examples Executable_Relation Execute_Choice Functions Function_Growth Gauge_Integration Groebner_Examples Guess HarmonicSeries Hebrew Hex_Bin_Examples IArray_Examples Iff_Oracle Induction_Schema Intuitionistic Join_Theory Lagrange List_to_Set_Comprehension_Examples LocaleTest2 - "ML" MergeSort MonoidGroup Multiquote NatSum Normalization_by_Evaluation PER Parallel_Example Peano_Axioms Perm_Fragments PresburgerEx Primrec Pythagoras Quicksort Radix_Sort Records Reflection_Examples Refute_Examples Residue_Ring Rewrite_Examples SOS SOS_Cert - Seq Serbian Set_Comprehension_Pointfree_Examples Set_Theory Simproc_Tests Simps_Case_Conv_Examples Sketch_and_Explore Sorting_Algorithms_Examples Sqrt Sqrt_Script Sudoku Sum_of_Powers Tarski Termination ThreeDivides Transfer_Debug Transfer_Int_Nat Transitive_Closure_Table_Ex Tree23 Triangular_Numbers Unification While_Combinator_Example Word veriT_Preprocessing theories [skip_proofs = false] SAT_Examples Meson_Test session "HOL-Isar_Examples" in Isar_Examples = "HOL-Computational_Algebra" + description " Miscellaneous Isabelle/Isar examples. " options [quick_and_dirty] theories - Knaster_Tarski - Peirce - Drinker - Cantor Structured_Statements Basic_Logic Expr_Compiler Fibonacci Group Group_Context Group_Notepad Hoare_Ex Mutilated_Checkerboard Puzzle Summation document_files "root.bib" "root.tex" session "HOL-Eisbach" in Eisbach = HOL + description \ The Eisbach proof method language and "match" method. \ sessions FOL "HOL-Analysis" theories Eisbach Tests Examples Examples_FOL Example_Metric session "HOL-SET_Protocol" (timing) in SET_Protocol = HOL + description " Verification of the SET Protocol. " sessions "HOL-Library" theories SET_Protocol document_files "root.tex" session "HOL-Matrix_LP" in Matrix_LP = HOL + description " Two-dimensional matrices and linear programming. " sessions "HOL-Library" directories "Compute_Oracle" theories Cplex document_files "root.tex" session "HOL-TLA" in TLA = HOL + description " Lamport's Temporal Logic of Actions. " theories TLA session "HOL-TLA-Inc" in "TLA/Inc" = "HOL-TLA" + theories Inc session "HOL-TLA-Buffer" in "TLA/Buffer" = "HOL-TLA" + theories DBuffer session "HOL-TLA-Memory" in "TLA/Memory" = "HOL-TLA" + theories MemoryImplementation session "HOL-TPTP" in TPTP = HOL + description " Author: Jasmin Blanchette, TU Muenchen Author: Nik Sultana, University of Cambridge Copyright 2011 TPTP-related extensions. " sessions "HOL-Library" theories ATP_Theory_Export MaSh_Eval TPTP_Interpret THF_Arith TPTP_Proof_Reconstruction theories ATP_Problem_Import session "HOL-Probability" (main timing) in "Probability" = "HOL-Analysis" + theories Probability document_files "root.tex" session "HOL-Probability-ex" (timing) in "Probability/ex" = "HOL-Probability" + theories Dining_Cryptographers Koepf_Duermuth_Countermeasure Measure_Not_CCC session "HOL-Nominal" in Nominal = HOL + sessions "HOL-Library" theories Nominal session "HOL-Nominal-Examples" (timing) in "Nominal/Examples" = "HOL-Nominal" + theories Class3 CK_Machine Compile Contexts Crary CR_Takahashi CR Fsub Height Lambda_mu Lam_Funs LocalWeakening Pattern SN SOS Standardization Support Type_Preservation Weakening W theories [quick_and_dirty] VC_Condition session "HOL-Cardinals" (timing) in Cardinals = HOL + description " Ordinals and Cardinals, Full Theories. " theories Cardinals Bounded_Set document_files "intro.tex" "root.tex" "root.bib" session "HOL-Datatype_Examples" (timing) in Datatype_Examples = "HOL-Library" + description " (Co)datatype Examples. " directories "Derivation_Trees" theories Compat Lambda_Term Process TreeFsetI "Derivation_Trees/Gram_Lang" "Derivation_Trees/Parallel_Composition" Koenig Lift_BNF Milner_Tofte Stream_Processor Cyclic_List Free_Idempotent_Monoid LDL TLList Misc_Codatatype Misc_Datatype Misc_Primcorec Misc_Primrec Datatype_Simproc_Tests session "HOL-Corec_Examples" (timing) in Corec_Examples = "HOL-Library" + description " Corecursion Examples. " directories "Tests" theories LFilter Paper_Examples Stream_Processor "Tests/Simple_Nesting" "Tests/Iterate_GPV" theories [quick_and_dirty] "Tests/GPV_Bare_Bones" "Tests/Merge_D" "Tests/Merge_Poly" "Tests/Misc_Mono" "Tests/Misc_Poly" "Tests/Small_Concrete" "Tests/Stream_Friends" "Tests/TLList_Friends" "Tests/Type_Class" session "HOL-Word" (main timing) in Word = HOL + sessions "HOL-Library" theories Word More_Word Word_Examples document_files "root.bib" "root.tex" session "HOL-Statespace" in Statespace = HOL + theories [skip_proofs = false] StateSpaceEx document_files "root.tex" session "HOL-Nonstandard_Analysis" (timing) in Nonstandard_Analysis = "HOL-Computational_Algebra" + description " Nonstandard analysis. " theories Nonstandard_Analysis document_files "root.tex" session "HOL-Nonstandard_Analysis-Examples" (timing) in "Nonstandard_Analysis/Examples" = "HOL-Nonstandard_Analysis" + theories NSPrimes session "HOL-Mirabelle" in Mirabelle = HOL + theories Mirabelle_Test session "HOL-Mirabelle-ex" in "Mirabelle/ex" = "HOL-Mirabelle" + options [timeout = 60] theories Ex session "HOL-Word-SMT_Examples" (timing) in SMT_Examples = "HOL-Word" + options [quick_and_dirty] theories Boogie SMT_Examples SMT_Word_Examples SMT_Tests session "HOL-SPARK" in "SPARK" = "HOL-Word" + theories SPARK session "HOL-SPARK-Examples" in "SPARK/Examples" = "HOL-SPARK" + directories "Gcd" "Liseq" "RIPEMD-160" "Sqrt" theories "Gcd/Greatest_Common_Divisor" "Liseq/Longest_Increasing_Subsequence" "RIPEMD-160/F" "RIPEMD-160/Hash" "RIPEMD-160/K_L" "RIPEMD-160/K_R" "RIPEMD-160/R_L" "RIPEMD-160/Round" "RIPEMD-160/R_R" "RIPEMD-160/S_L" "RIPEMD-160/S_R" "Sqrt/Sqrt" export_files (in ".") "*:**.prv" session "HOL-SPARK-Manual" in "SPARK/Manual" = "HOL-SPARK" + options [show_question_marks = false] sessions "HOL-SPARK-Examples" theories Example_Verification VC_Principles Reference Complex_Types document_files "complex_types.ads" "complex_types_app.adb" "complex_types_app.ads" "Gcd.adb" "Gcd.ads" "intro.tex" "loop_invariant.adb" "loop_invariant.ads" "root.bib" "root.tex" "Simple_Gcd.adb" "Simple_Gcd.ads" session "HOL-Mutabelle" in Mutabelle = HOL + sessions "HOL-Library" theories MutabelleExtra session "HOL-Quickcheck_Examples" (timing) in Quickcheck_Examples = HOL + sessions "HOL-Library" theories Quickcheck_Examples Quickcheck_Lattice_Examples Completeness Quickcheck_Interfaces Quickcheck_Nesting_Example theories [condition = ISABELLE_GHC] Hotel_Example Quickcheck_Narrowing_Examples session "HOL-Quotient_Examples" (timing) in Quotient_Examples = "HOL-Algebra" + description " Author: Cezary Kaliszyk and Christian Urban " theories DList Quotient_FSet Quotient_Int Quotient_Message Lift_FSet Lift_Set Lift_Fun Quotient_Rat Lift_DList Int_Pow Lifting_Code_Dt_Test session "HOL-Predicate_Compile_Examples" (timing) in Predicate_Compile_Examples = HOL + sessions "HOL-Library" theories Examples Predicate_Compile_Tests Predicate_Compile_Quickcheck_Examples Specialisation_Examples IMP_1 IMP_2 (* FIXME since 21-Jul-2011 Hotel_Example_Small_Generator *) IMP_3 IMP_4 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] Reg_Exp_Example session "HOL-Types_To_Sets" in Types_To_Sets = HOL + description " Experimental extension of Higher-Order Logic to allow translation of types to sets. " directories "Examples" theories Types_To_Sets "Examples/Prerequisites" "Examples/Finite" "Examples/T2_Spaces" "Examples/Unoverload_Def" "Examples/Linear_Algebra_On" session HOLCF (main timing) in HOLCF = HOL + description " Author: Franz Regensburger Author: Brian Huffman HOLCF -- a semantic extension of HOL by the LCF logic. " sessions "HOL-Library" theories HOLCF (global) document_files "root.tex" session "HOLCF-Tutorial" in "HOLCF/Tutorial" = HOLCF + theories Domain_ex Fixrec_ex New_Domain document_files "root.tex" session "HOLCF-Library" in "HOLCF/Library" = HOLCF + theories HOLCF_Library HOL_Cpo session "HOLCF-IMP" in "HOLCF/IMP" = HOLCF + description " IMP -- A WHILE-language and its Semantics. This is the HOLCF-based denotational semantics of a simple WHILE-language. " sessions "HOL-IMP" theories HoareEx document_files "isaverbatimwrite.sty" "root.tex" "root.bib" session "HOLCF-ex" in "HOLCF/ex" = "HOLCF-Library" + description " Miscellaneous examples for HOLCF. " theories Dnat Dagstuhl Focus_ex Fix2 Hoare Concurrency_Monad Loop Powerdomain_ex Domain_Proofs Letrec Pattern_Match session "HOLCF-FOCUS" in "HOLCF/FOCUS" = "HOLCF-Library" + description \ FOCUS: a theory of stream-processing functions Isabelle/HOLCF. For introductions to FOCUS, see "The Design of Distributed Systems - An Introduction to FOCUS" http://www4.in.tum.de/publ/html.php?e=2 "Specification and Refinement of a Buffer of Length One" http://www4.in.tum.de/publ/html.php?e=15 "Specification and Development of Interactive Systems: Focus on Streams, Interfaces, and Refinement" http://www4.in.tum.de/publ/html.php?e=321 \ theories Fstreams FOCUS Buffer_adm session IOA (timing) in "HOLCF/IOA" = HOLCF + description " Author: Olaf Mueller Copyright 1997 TU München A formalization of I/O automata in HOLCF. The distribution contains simulation relations, temporal logic, and an abstraction theory. Everything is based upon a domain-theoretic model of finite and infinite sequences. " theories Abstraction session "IOA-ABP" in "HOLCF/IOA/ABP" = IOA + description " Author: Olaf Mueller The Alternating Bit Protocol performed in I/O-Automata. " theories Correctness Spec session "IOA-NTP" in "HOLCF/IOA/NTP" = IOA + description " Author: Tobias Nipkow & Konrad Slind A network transmission protocol, performed in the I/O automata formalization by Olaf Mueller. " theories Correctness session "IOA-Storage" in "HOLCF/IOA/Storage" = IOA + description " Author: Olaf Mueller Memory storage case study. " theories Correctness session "IOA-ex" in "HOLCF/IOA/ex" = IOA + description " Author: Olaf Mueller " theories TrivEx TrivEx2 diff --git a/src/HOL/ex/ML.thy b/src/HOL/ex/ML.thy deleted file mode 100644 --- a/src/HOL/ex/ML.thy +++ /dev/null @@ -1,157 +0,0 @@ -(* Title: HOL/ex/ML.thy - Author: Makarius -*) - -section \Isabelle/ML basics\ - -theory "ML" -imports Main -begin - -section \ML expressions\ - -text \ - The Isabelle command \<^theory_text>\ML\ allows to embed Isabelle/ML source into the - formal text. It is type-checked, compiled, and run within that environment. - - Note that side-effects should be avoided, unless the intention is to change - global parameters of the run-time environment (rare). - - ML top-level bindings are managed within the theory context. -\ - -ML \1 + 1\ - -ML \val a = 1\ -ML \val b = 1\ -ML \val c = a + b\ - - -section \Antiquotations\ - -text \ - There are some language extensions (via antiquotations), as explained in the - ``Isabelle/Isar implementation manual'', chapter 0. -\ - -ML \length []\ -ML \\<^assert> (length [] = 0)\ - - -text \Formal entities from the surrounding context may be referenced as - follows:\ - -term "1 + 1" \ \term within theory source\ - -ML \\<^term>\1 + 1\ (* term as symbolic ML datatype value *)\ - -ML \\<^term>\1 + (1::int)\\ - - -ML \ - (* formal source with position information *) - val s = \1 + 1\; - - (* read term via old-style string interface *) - val t = Syntax.read_term \<^context> (Syntax.implode_input s); -\ - - -section \Recursive ML evaluation\ - -ML \ - ML \ML \val a = @{thm refl}\\; - ML \val b = @{thm sym}\; - val c = @{thm trans} - val thms = [a, b, c]; -\ - - -section \IDE support\ - -text \ - ML embedded into the Isabelle environment is connected to the Prover IDE. - Poly/ML provides: - - \<^item> precise positions for warnings / errors - \<^item> markup for defining positions of identifiers - \<^item> markup for inferred types of sub-expressions - \<^item> pretty-printing of ML values with markup - \<^item> completion of ML names - \<^item> source-level debugger -\ - -ML \fn i => fn list => length list + i\ - - -section \Example: factorial and ackermann function in Isabelle/ML\ - -ML \ - fun factorial 0 = 1 - | factorial n = n * factorial (n - 1) -\ - -ML \factorial 42\ -ML \factorial 10000 div factorial 9999\ - -text \See \<^url>\http://mathworld.wolfram.com/AckermannFunction.html\.\ - -ML \ - fun ackermann 0 n = n + 1 - | ackermann m 0 = ackermann (m - 1) 1 - | ackermann m n = ackermann (m - 1) (ackermann m (n - 1)) -\ - -ML \timeit (fn () => ackermann 3 10)\ - - -section \Parallel Isabelle/ML\ - -text \ - Future.fork/join/cancel manage parallel evaluation. - - Note that within Isabelle theory documents, the top-level command boundary - may not be transgressed without special precautions. This is normally - managed by the system when performing parallel proof checking. -\ - -ML \ - val x = Future.fork (fn () => ackermann 3 10); - val y = Future.fork (fn () => ackermann 3 10); - val z = Future.join x + Future.join y -\ - -text \ - The \<^ML_structure>\Par_List\ module provides high-level combinators for - parallel list operations. -\ - -ML \timeit (fn () => map (fn n => ackermann 3 n) (1 upto 10))\ -ML \timeit (fn () => Par_List.map (fn n => ackermann 3 n) (1 upto 10))\ - - -section \Function specifications in Isabelle/HOL\ - -fun factorial :: "nat \ nat" -where - "factorial 0 = 1" -| "factorial (Suc n) = Suc n * factorial n" - -term "factorial 4" \ \symbolic term\ -value "factorial 4" \ \evaluation via ML code generation in the background\ - -declare [[ML_source_trace]] -ML \\<^term>\factorial 4\\ \ \symbolic term in ML\ -ML \@{code "factorial"}\ \ \ML code from function specification\ - - -fun ackermann :: "nat \ nat \ nat" -where - "ackermann 0 n = n + 1" -| "ackermann (Suc m) 0 = ackermann m 1" -| "ackermann (Suc m) (Suc n) = ackermann m (ackermann (Suc m) n)" - -value "ackermann 3 5" - -end - diff --git a/src/HOL/ex/Seq.thy b/src/HOL/ex/Seq.thy deleted file mode 100644 --- a/src/HOL/ex/Seq.thy +++ /dev/null @@ -1,35 +0,0 @@ -(* Title: HOL/ex/Seq.thy - Author: Makarius -*) - -section \Finite sequences\ - -theory Seq -imports Main -begin - -datatype 'a seq = Empty | Seq 'a "'a seq" - -fun conc :: "'a seq \ 'a seq \ 'a seq" -where - "conc Empty ys = ys" -| "conc (Seq x xs) ys = Seq x (conc xs ys)" - -fun reverse :: "'a seq \ 'a seq" -where - "reverse Empty = Empty" -| "reverse (Seq x xs) = conc (reverse xs) (Seq x Empty)" - -lemma conc_empty: "conc xs Empty = xs" - by (induct xs) simp_all - -lemma conc_assoc: "conc (conc xs ys) zs = conc xs (conc ys zs)" - by (induct xs) simp_all - -lemma reverse_conc: "reverse (conc xs ys) = conc (reverse ys) (reverse xs)" - by (induct xs) (simp_all add: conc_empty conc_assoc) - -lemma reverse_reverse: "reverse (reverse xs) = xs" - by (induct xs) (simp_all add: reverse_conc) - -end