# 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 \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 -r e5df9c8d9d4b -r bf085daea304 src/HOL/Examples/Peirce.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Examples/Peirce.thy Mon Jun 08 21:38:41 2020 +0200 @@ -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 -r e5df9c8d9d4b -r bf085daea304 src/HOL/Examples/Seq.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Examples/Seq.thy Mon Jun 08 21:38:41 2020 +0200 @@ -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 -r e5df9c8d9d4b -r bf085daea304 src/HOL/Examples/document/root.bib --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Examples/document/root.bib Mon Jun 08 21:38:41 2020 +0200 @@ -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 -r e5df9c8d9d4b -r bf085daea304 src/HOL/Examples/document/root.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Examples/document/root.tex Mon Jun 08 21:38:41 2020 +0200 @@ -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 -r e5df9c8d9d4b -r bf085daea304 src/HOL/Isar_Examples/Cantor.thy --- a/src/HOL/Isar_Examples/Cantor.thy Mon Jun 08 15:09:57 2020 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -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 -r e5df9c8d9d4b -r bf085daea304 src/HOL/Isar_Examples/Drinker.thy --- a/src/HOL/Isar_Examples/Drinker.thy Mon Jun 08 15:09:57 2020 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -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 -r e5df9c8d9d4b -r bf085daea304 src/HOL/Isar_Examples/Knaster_Tarski.thy --- a/src/HOL/Isar_Examples/Knaster_Tarski.thy Mon Jun 08 15:09:57 2020 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -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 -r e5df9c8d9d4b -r bf085daea304 src/HOL/Isar_Examples/Peirce.thy --- a/src/HOL/Isar_Examples/Peirce.thy Mon Jun 08 15:09:57 2020 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -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 -r e5df9c8d9d4b -r bf085daea304 src/HOL/Proofs/ex/XML_Data.thy --- a/src/HOL/Proofs/ex/XML_Data.thy Mon Jun 08 15:09:57 2020 +0200 +++ b/src/HOL/Proofs/ex/XML_Data.thy Mon Jun 08 21:38:41 2020 +0200 @@ -6,7 +6,7 @@ *) theory XML_Data - imports "HOL-Isar_Examples.Drinker" + imports "HOL-Examples.Drinker" begin subsection \Export and re-import of global proof terms\ diff -r e5df9c8d9d4b -r bf085daea304 src/HOL/ROOT --- a/src/HOL/ROOT Mon Jun 08 15:09:57 2020 +0200 +++ b/src/HOL/ROOT Mon Jun 08 21:38:41 2020 +0200 @@ -13,6 +13,24 @@ "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. @@ -631,7 +649,6 @@ Lagrange List_to_Set_Comprehension_Examples LocaleTest2 - "ML" MergeSort MonoidGroup Multiquote @@ -653,7 +670,6 @@ Rewrite_Examples SOS SOS_Cert - Seq Serbian Set_Comprehension_Pointfree_Examples Set_Theory @@ -687,10 +703,6 @@ " options [quick_and_dirty] theories - Knaster_Tarski - Peirce - Drinker - Cantor Structured_Statements Basic_Logic Expr_Compiler diff -r e5df9c8d9d4b -r bf085daea304 src/HOL/ex/ML.thy --- a/src/HOL/ex/ML.thy Mon Jun 08 15:09:57 2020 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -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 -r e5df9c8d9d4b -r bf085daea304 src/HOL/ex/Seq.thy --- a/src/HOL/ex/Seq.thy Mon Jun 08 15:09:57 2020 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -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