# HG changeset patch # User wenzelm # Date 1591645121 -7200 # Node ID bf085daea304e966a4b3f2dcb280338242dfc40c # Parent e5df9c8d9d4b2a59e13210df2550e5ef4517a1aa clarified sessions: "Notable Examples in Isabelle/HOL"; diff -r e5df9c8d9d4b -r bf085daea304 etc/settings --- a/etc/settings Mon Jun 08 15:09:57 2020 +0200 +++ b/etc/settings Mon Jun 08 21:38:41 2020 +0200 @@ -114,7 +114,7 @@ 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 diff -r e5df9c8d9d4b -r bf085daea304 src/Doc/Isar_Ref/Framework.thy --- a/src/Doc/Isar_Ref/Framework.thy Mon Jun 08 15:09:57 2020 +0200 +++ b/src/Doc/Isar_Ref/Framework.thy Mon Jun 08 21:38:41 2020 +0200 @@ -89,10 +89,11 @@ \<^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. diff -r e5df9c8d9d4b -r bf085daea304 src/Doc/System/Server.thy --- a/src/Doc/System/Server.thy Mon Jun 08 15:09:57 2020 +0200 +++ b/src/Doc/System/Server.thy Mon Jun 08 21:38:41 2020 +0200 @@ -515,9 +515,9 @@ \<^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: @@ -975,8 +975,8 @@ 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 @@ -1026,7 +1026,7 @@ 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 diff -r e5df9c8d9d4b -r bf085daea304 src/HOL/Examples/Cantor.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Examples/Cantor.thy Mon Jun 08 21:38:41 2020 +0200 @@ -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 -r e5df9c8d9d4b -r bf085daea304 src/HOL/Examples/Drinker.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Examples/Drinker.thy Mon Jun 08 21:38:41 2020 +0200 @@ -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 -r e5df9c8d9d4b -r bf085daea304 src/HOL/Examples/Knaster_Tarski.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Examples/Knaster_Tarski.thy Mon Jun 08 21:38:41 2020 +0200 @@ -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 -r e5df9c8d9d4b -r bf085daea304 src/HOL/Examples/ML.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Examples/ML.thy Mon Jun 08 21:38:41 2020 +0200 @@ -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 \