--- 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
--- 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>\<open>~~/src/HOL/Isar_Examples\<close>. 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>\<open>~~/src/Pure/Examples\<close> and \<^dir>\<open>~~/src/HOL/Examples\<close>. 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>\<open>~~/src/Pure/Examples/Higher_Order_Logic.thy\<close>). Isabelle/FOL @{cite
"isabelle-logics"} and Isabelle/ZF @{cite "isabelle-ZF"} also work, but are
much less developed.
--- 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>\<open>type\<close> \<open>node = {node_name: string, theory_name: string}\<close> represents the
internal node name of a theory. The \<open>node_name\<close> is derived from the
- canonical theory file-name (e.g.\ \<^verbatim>\<open>"~~/src/HOL/ex/Seq.thy"\<close> after
+ canonical theory file-name (e.g.\ \<^verbatim>\<open>"~~/src/HOL/Examples/Seq.thy"\<close> after
normalization within the file-system). The \<open>theory_name\<close> is the
- session-qualified theory name (e.g.\ \<^verbatim>\<open>HOL-ex.Seq\<close>).
+ session-qualified theory name (e.g.\ \<^verbatim>\<open>HOL-Examples.Seq\<close>).
\<^item> \<^bold>\<open>type\<close> \<open>node_status = {ok: bool, total: int, unprocessed: int, running:
int, warned: int, failed: int, finished: int, canceled: bool, consolidated:
@@ -975,8 +975,8 @@
The \<open>master_dir\<close> field specifies the master directory of imported theories:
it acts like the ``current working directory'' for locating theory files.
This is irrelevant for \<open>theories\<close> with an absolute path name (e.g.\
- \<^verbatim>\<open>"~~/src/HOL/ex/Seq.thy"\<close>) or session-qualified theory name (e.g.\
- \<^verbatim>\<open>"HOL-ex/Seq"\<close>).
+ \<^verbatim>\<open>"~~/src/HOL/Examples/Seq.thy"\<close>) or session-qualified theory name (e.g.\
+ \<^verbatim>\<open>"HOL-Examples.Seq"\<close>).
\<^medskip>
The \<open>pretty_margin\<close> 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] \<open>use_theories {"session_id": ..., "theories": ["~~/src/HOL/ex/Seq"]}\<close>}
+ @{verbatim [display] \<open>use_theories {"session_id": ..., "theories": ["~~/src/HOL/Examples/Seq"]}\<close>}
\<^medskip>
Process some example theories in the context of their (single) parent
--- /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 \<open>Cantor's Theorem\<close>
+
+theory Cantor
+ imports Main
+begin
+
+subsection \<open>Mathematical statement and proof\<close>
+
+text \<open>
+ 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>\<open>http://mathworld.wolfram.com/CantorDiagonalMethod.html\<close>
+ \<^item> \<^url>\<open>https://en.wikipedia.org/wiki/Cantor's_diagonal_argument\<close>
+\<close>
+
+theorem Cantor: "\<nexists>f :: 'a \<Rightarrow> 'a set. \<forall>A. \<exists>x. A = f x"
+proof
+ assume "\<exists>f :: 'a \<Rightarrow> 'a set. \<forall>A. \<exists>x. A = f x"
+ then obtain f :: "'a \<Rightarrow> 'a set" where *: "\<forall>A. \<exists>x. A = f x" ..
+ let ?D = "{x. x \<notin> f x}"
+ from * obtain a where "?D = f a" by blast
+ moreover have "a \<in> ?D \<longleftrightarrow> a \<notin> f a" by blast
+ ultimately show False by blast
+qed
+
+
+subsection \<open>Automated proofs\<close>
+
+text \<open>
+ These automated proofs are much shorter, but lack information why and how it
+ works.
+\<close>
+
+theorem "\<nexists>f :: 'a \<Rightarrow> 'a set. \<forall>A. \<exists>x. f x = A"
+ by best
+
+theorem "\<nexists>f :: 'a \<Rightarrow> 'a set. \<forall>A. \<exists>x. f x = A"
+ by force
+
+
+subsection \<open>Elementary version in higher-order predicate logic\<close>
+
+text \<open>
+ The subsequent formulation bypasses set notation of HOL; it uses elementary
+ \<open>\<lambda>\<close>-calculus and predicate logic, with standard introduction and elimination
+ rules. This also shows that the proof does not require classical reasoning.
+\<close>
+
+lemma iff_contradiction:
+ assumes *: "\<not> A \<longleftrightarrow> A"
+ shows False
+proof (rule notE)
+ show "\<not> A"
+ proof
+ assume A
+ with * have "\<not> A" ..
+ from this and \<open>A\<close> show False ..
+ qed
+ with * show A ..
+qed
+
+theorem Cantor': "\<nexists>f :: 'a \<Rightarrow> 'a \<Rightarrow> bool. \<forall>A. \<exists>x. A = f x"
+proof
+ assume "\<exists>f :: 'a \<Rightarrow> 'a \<Rightarrow> bool. \<forall>A. \<exists>x. A = f x"
+ then obtain f :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where *: "\<forall>A. \<exists>x. A = f x" ..
+ let ?D = "\<lambda>x. \<not> f x x"
+ from * have "\<exists>x. ?D = f x" ..
+ then obtain a where "?D = f a" ..
+ then have "?D a \<longleftrightarrow> f a a" by (rule arg_cong)
+ then have "\<not> f a a \<longleftrightarrow> f a a" .
+ then show False by (rule iff_contradiction)
+qed
+
+
+subsection \<open>Classic Isabelle/HOL example\<close>
+
+text \<open>
+ The following treatment of Cantor's Theorem follows the classic example from
+ the early 1990s, e.g.\ see the file \<^verbatim>\<open>92/HOL/ex/set.ML\<close> in
+ Isabelle92 or @{cite \<open>\S18.7\<close> "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]
+ \<open>\<forall>f::\<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool. \<exists>S::\<alpha> \<Rightarrow> bool. \<forall>x::\<alpha>. f x \<noteq> S\<close>}
+
+ Viewing types as sets, \<open>\<alpha> \<Rightarrow> bool\<close> represents the powerset of \<open>\<alpha>\<close>. This
+ version of the theorem states that for every function from \<open>\<alpha>\<close> to its
+ powerset, some subset is outside its range. The Isabelle/Isar proofs below
+ uses HOL's set theory, with the type \<open>\<alpha> set\<close> and the operator \<open>range :: (\<alpha> \<Rightarrow>
+ \<beta>) \<Rightarrow> \<beta> set\<close>.
+\<close>
+
+theorem "\<exists>S. S \<notin> range (f :: 'a \<Rightarrow> 'a set)"
+proof
+ let ?S = "{x. x \<notin> f x}"
+ show "?S \<notin> range f"
+ proof
+ assume "?S \<in> range f"
+ then obtain y where "?S = f y" ..
+ then show False
+ proof (rule equalityCE)
+ assume "y \<in> f y"
+ assume "y \<in> ?S"
+ then have "y \<notin> f y" ..
+ with \<open>y \<in> f y\<close> show ?thesis by contradiction
+ next
+ assume "y \<notin> ?S"
+ assume "y \<notin> f y"
+ then have "y \<in> ?S" ..
+ with \<open>y \<notin> ?S\<close> show ?thesis by contradiction
+ qed
+ qed
+qed
+
+text \<open>
+ 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.
+\<close>
+
+theorem "\<exists>S. S \<notin> range (f :: 'a \<Rightarrow> 'a set)"
+ by best
+
+end
--- /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 \<open>The Drinker's Principle\<close>
+
+theory Drinker
+ imports Main
+begin
+
+text \<open>
+ 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.
+\<close>
+
+lemma de_Morgan:
+ assumes "\<not> (\<forall>x. P x)"
+ shows "\<exists>x. \<not> P x"
+proof (rule classical)
+ assume "\<nexists>x. \<not> P x"
+ have "\<forall>x. P x"
+ proof
+ fix x show "P x"
+ proof (rule classical)
+ assume "\<not> P x"
+ then have "\<exists>x. \<not> P x" ..
+ with \<open>\<nexists>x. \<not> P x\<close> show ?thesis by contradiction
+ qed
+ qed
+ with \<open>\<not> (\<forall>x. P x)\<close> show ?thesis by contradiction
+qed
+
+theorem Drinker's_Principle: "\<exists>x. drunk x \<longrightarrow> (\<forall>x. drunk x)"
+proof cases
+ assume "\<forall>x. drunk x"
+ then have "drunk a \<longrightarrow> (\<forall>x. drunk x)" for a ..
+ then show ?thesis ..
+next
+ assume "\<not> (\<forall>x. drunk x)"
+ then have "\<exists>x. \<not> drunk x" by (rule de_Morgan)
+ then obtain a where "\<not> drunk a" ..
+ have "drunk a \<longrightarrow> (\<forall>x. drunk x)"
+ proof
+ assume "drunk a"
+ with \<open>\<not> drunk a\<close> show "\<forall>x. drunk x" by contradiction
+ qed
+ then show ?thesis ..
+qed
+
+end
--- /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 \<open>Textbook-style reasoning: the Knaster-Tarski Theorem\<close>
+
+theory Knaster_Tarski
+ imports Main "HOL-Library.Lattice_Syntax"
+begin
+
+
+subsection \<open>Prose version\<close>
+
+text \<open>
+ According to the textbook @{cite \<open>pages 93--94\<close> "davey-priestley"}, the
+ Knaster-Tarski fixpoint theorem is as follows.\<^footnote>\<open>We have dualized the
+ argument, and tuned the notation a little bit.\<close>
+
+ \<^bold>\<open>The Knaster-Tarski Fixpoint Theorem.\<close> Let \<open>L\<close> be a complete lattice and
+ \<open>f: L \<rightarrow> L\<close> an order-preserving map. Then \<open>\<Sqinter>{x \<in> L | f(x) \<le> x}\<close> is a fixpoint
+ of \<open>f\<close>.
+
+ \<^bold>\<open>Proof.\<close> Let \<open>H = {x \<in> L | f(x) \<le> x}\<close> and \<open>a = \<Sqinter>H\<close>. For all \<open>x \<in> H\<close> we have
+ \<open>a \<le> x\<close>, so \<open>f(a) \<le> f(x) \<le> x\<close>. Thus \<open>f(a)\<close> is a lower bound of \<open>H\<close>, whence
+ \<open>f(a) \<le> a\<close>. We now use this inequality to prove the reverse one (!) and
+ thereby complete the proof that \<open>a\<close> is a fixpoint. Since \<open>f\<close> is
+ order-preserving, \<open>f(f(a)) \<le> f(a)\<close>. This says \<open>f(a) \<in> H\<close>, so \<open>a \<le> f(a)\<close>.\<close>
+
+
+subsection \<open>Formal versions\<close>
+
+text \<open>
+ 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.
+\<close>
+
+theorem Knaster_Tarski:
+ fixes f :: "'a::complete_lattice \<Rightarrow> 'a"
+ assumes "mono f"
+ shows "\<exists>a. f a = a"
+proof
+ let ?H = "{u. f u \<le> u}"
+ let ?a = "\<Sqinter>?H"
+ show "f ?a = ?a"
+ proof -
+ {
+ fix x
+ assume "x \<in> ?H"
+ then have "?a \<le> x" by (rule Inf_lower)
+ with \<open>mono f\<close> have "f ?a \<le> f x" ..
+ also from \<open>x \<in> ?H\<close> have "\<dots> \<le> x" ..
+ finally have "f ?a \<le> x" .
+ }
+ then have "f ?a \<le> ?a" by (rule Inf_greatest)
+ {
+ also presume "\<dots> \<le> f ?a"
+ finally (order_antisym) show ?thesis .
+ }
+ from \<open>mono f\<close> and \<open>f ?a \<le> ?a\<close> have "f (f ?a) \<le> f ?a" ..
+ then have "f ?a \<in> ?H" ..
+ then show "?a \<le> f ?a" by (rule Inf_lower)
+ qed
+qed
+
+text \<open>
+ 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.
+\<close>
+
+theorem Knaster_Tarski':
+ fixes f :: "'a::complete_lattice \<Rightarrow> 'a"
+ assumes "mono f"
+ shows "\<exists>a. f a = a"
+proof
+ let ?H = "{u. f u \<le> u}"
+ let ?a = "\<Sqinter>?H"
+ show "f ?a = ?a"
+ proof (rule order_antisym)
+ show "f ?a \<le> ?a"
+ proof (rule Inf_greatest)
+ fix x
+ assume "x \<in> ?H"
+ then have "?a \<le> x" by (rule Inf_lower)
+ with \<open>mono f\<close> have "f ?a \<le> f x" ..
+ also from \<open>x \<in> ?H\<close> have "\<dots> \<le> x" ..
+ finally show "f ?a \<le> x" .
+ qed
+ show "?a \<le> f ?a"
+ proof (rule Inf_lower)
+ from \<open>mono f\<close> and \<open>f ?a \<le> ?a\<close> have "f (f ?a) \<le> f ?a" ..
+ then show "f ?a \<in> ?H" ..
+ qed
+ qed
+qed
+
+end
--- /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 \<open>Isabelle/ML basics\<close>
+
+theory "ML"
+imports Main
+begin
+
+section \<open>ML expressions\<close>
+
+text \<open>
+ The Isabelle command \<^theory_text>\<open>ML\<close> 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.
+\<close>
+
+ML \<open>1 + 1\<close>
+
+ML \<open>val a = 1\<close>
+ML \<open>val b = 1\<close>
+ML \<open>val c = a + b\<close>
+
+
+section \<open>Antiquotations\<close>
+
+text \<open>
+ There are some language extensions (via antiquotations), as explained in the
+ ``Isabelle/Isar implementation manual'', chapter 0.
+\<close>
+
+ML \<open>length []\<close>
+ML \<open>\<^assert> (length [] = 0)\<close>
+
+
+text \<open>Formal entities from the surrounding context may be referenced as
+ follows:\<close>
+
+term "1 + 1" \<comment> \<open>term within theory source\<close>
+
+ML \<open>\<^term>\<open>1 + 1\<close> (* term as symbolic ML datatype value *)\<close>
+
+ML \<open>\<^term>\<open>1 + (1::int)\<close>\<close>
+
+
+ML \<open>
+ (* formal source with position information *)
+ val s = \<open>1 + 1\<close>;
+
+ (* read term via old-style string interface *)
+ val t = Syntax.read_term \<^context> (Syntax.implode_input s);
+\<close>
+
+
+section \<open>Recursive ML evaluation\<close>
+
+ML \<open>
+ ML \<open>ML \<open>val a = @{thm refl}\<close>\<close>;
+ ML \<open>val b = @{thm sym}\<close>;
+ val c = @{thm trans}
+ val thms = [a, b, c];
+\<close>
+
+
+section \<open>IDE support\<close>
+
+text \<open>
+ 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
+\<close>
+
+ML \<open>fn i => fn list => length list + i\<close>
+
+
+section \<open>Example: factorial and ackermann function in Isabelle/ML\<close>
+
+ML \<open>
+ fun factorial 0 = 1
+ | factorial n = n * factorial (n - 1)
+\<close>
+
+ML \<open>factorial 42\<close>
+ML \<open>factorial 10000 div factorial 9999\<close>
+
+text \<open>See \<^url>\<open>http://mathworld.wolfram.com/AckermannFunction.html\<close>.\<close>
+
+ML \<open>
+ fun ackermann 0 n = n + 1
+ | ackermann m 0 = ackermann (m - 1) 1
+ | ackermann m n = ackermann (m - 1) (ackermann m (n - 1))
+\<close>
+
+ML \<open>timeit (fn () => ackermann 3 10)\<close>
+
+
+section \<open>Parallel Isabelle/ML\<close>
+
+text \<open>
+ 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.
+\<close>
+
+ML \<open>
+ val x = Future.fork (fn () => ackermann 3 10);
+ val y = Future.fork (fn () => ackermann 3 10);
+ val z = Future.join x + Future.join y
+\<close>
+
+text \<open>
+ The \<^ML_structure>\<open>Par_List\<close> module provides high-level combinators for
+ parallel list operations.
+\<close>
+
+ML \<open>timeit (fn () => map (fn n => ackermann 3 n) (1 upto 10))\<close>
+ML \<open>timeit (fn () => Par_List.map (fn n => ackermann 3 n) (1 upto 10))\<close>
+
+
+section \<open>Function specifications in Isabelle/HOL\<close>
+
+fun factorial :: "nat \<Rightarrow> nat"
+where
+ "factorial 0 = 1"
+| "factorial (Suc n) = Suc n * factorial n"
+
+term "factorial 4" \<comment> \<open>symbolic term\<close>
+value "factorial 4" \<comment> \<open>evaluation via ML code generation in the background\<close>
+
+declare [[ML_source_trace]]
+ML \<open>\<^term>\<open>factorial 4\<close>\<close> \<comment> \<open>symbolic term in ML\<close>
+ML \<open>@{code "factorial"}\<close> \<comment> \<open>ML code from function specification\<close>
+
+
+fun ackermann :: "nat \<Rightarrow> nat \<Rightarrow> 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
+
--- /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 \<open>Peirce's Law\<close>
+
+theory Peirce
+ imports Main
+begin
+
+text \<open>
+ We consider Peirce's Law: \<open>((A \<longrightarrow> B) \<longrightarrow> A) \<longrightarrow> A\<close>. 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>\<open>The rule involved there is negation elimination; it holds in
+ intuitionistic logic as well.\<close>\<close>
+
+theorem "((A \<longrightarrow> B) \<longrightarrow> A) \<longrightarrow> A"
+proof
+ assume "(A \<longrightarrow> B) \<longrightarrow> A"
+ show A
+ proof (rule classical)
+ assume "\<not> A"
+ have "A \<longrightarrow> B"
+ proof
+ assume A
+ with \<open>\<not> A\<close> show B by contradiction
+ qed
+ with \<open>(A \<longrightarrow> B) \<longrightarrow> A\<close> show A ..
+ qed
+qed
+
+text \<open>
+ In the subsequent version the reasoning is rearranged by means of ``weak
+ assumptions'' (as introduced by \<^theory_text>\<open>presume\<close>). Before assuming the negated
+ goal \<open>\<not> A\<close>, its intended consequence \<open>A \<longrightarrow> B\<close> is put into place in order to
+ solve the main problem. Nevertheless, we do not get anything for free, but
+ have to establish \<open>A \<longrightarrow> B\<close> later on. The overall effect is that of a logical
+ \<^emph>\<open>cut\<close>.
+
+ Technically speaking, whenever some goal is solved by \<^theory_text>\<open>show\<close> 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>\<open>assume\<close>) are solved immediately.
+\<close>
+
+theorem "((A \<longrightarrow> B) \<longrightarrow> A) \<longrightarrow> A"
+proof
+ assume "(A \<longrightarrow> B) \<longrightarrow> A"
+ show A
+ proof (rule classical)
+ presume "A \<longrightarrow> B"
+ with \<open>(A \<longrightarrow> B) \<longrightarrow> A\<close> show A ..
+ next
+ assume "\<not> A"
+ show "A \<longrightarrow> B"
+ proof
+ assume A
+ with \<open>\<not> A\<close> show B by contradiction
+ qed
+ qed
+qed
+
+text \<open>
+ 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>\<open>and\<close> 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.
+\<close>
+
+end
--- /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 \<open>Finite sequences\<close>
+
+theory Seq
+imports Main
+begin
+
+datatype 'a seq = Empty | Seq 'a "'a seq"
+
+fun conc :: "'a seq \<Rightarrow> 'a seq \<Rightarrow> 'a seq"
+where
+ "conc Empty ys = ys"
+| "conc (Seq x xs) ys = Seq x (conc xs ys)"
+
+fun reverse :: "'a seq \<Rightarrow> '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
--- /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}
--- /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}
--- 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 \<open>Cantor's Theorem\<close>
-
-theory Cantor
- imports Main
-begin
-
-subsection \<open>Mathematical statement and proof\<close>
-
-text \<open>
- 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>\<open>http://mathworld.wolfram.com/CantorDiagonalMethod.html\<close>
- \<^item> \<^url>\<open>https://en.wikipedia.org/wiki/Cantor's_diagonal_argument\<close>
-\<close>
-
-theorem Cantor: "\<nexists>f :: 'a \<Rightarrow> 'a set. \<forall>A. \<exists>x. A = f x"
-proof
- assume "\<exists>f :: 'a \<Rightarrow> 'a set. \<forall>A. \<exists>x. A = f x"
- then obtain f :: "'a \<Rightarrow> 'a set" where *: "\<forall>A. \<exists>x. A = f x" ..
- let ?D = "{x. x \<notin> f x}"
- from * obtain a where "?D = f a" by blast
- moreover have "a \<in> ?D \<longleftrightarrow> a \<notin> f a" by blast
- ultimately show False by blast
-qed
-
-
-subsection \<open>Automated proofs\<close>
-
-text \<open>
- These automated proofs are much shorter, but lack information why and how it
- works.
-\<close>
-
-theorem "\<nexists>f :: 'a \<Rightarrow> 'a set. \<forall>A. \<exists>x. f x = A"
- by best
-
-theorem "\<nexists>f :: 'a \<Rightarrow> 'a set. \<forall>A. \<exists>x. f x = A"
- by force
-
-
-subsection \<open>Elementary version in higher-order predicate logic\<close>
-
-text \<open>
- The subsequent formulation bypasses set notation of HOL; it uses elementary
- \<open>\<lambda>\<close>-calculus and predicate logic, with standard introduction and elimination
- rules. This also shows that the proof does not require classical reasoning.
-\<close>
-
-lemma iff_contradiction:
- assumes *: "\<not> A \<longleftrightarrow> A"
- shows False
-proof (rule notE)
- show "\<not> A"
- proof
- assume A
- with * have "\<not> A" ..
- from this and \<open>A\<close> show False ..
- qed
- with * show A ..
-qed
-
-theorem Cantor': "\<nexists>f :: 'a \<Rightarrow> 'a \<Rightarrow> bool. \<forall>A. \<exists>x. A = f x"
-proof
- assume "\<exists>f :: 'a \<Rightarrow> 'a \<Rightarrow> bool. \<forall>A. \<exists>x. A = f x"
- then obtain f :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where *: "\<forall>A. \<exists>x. A = f x" ..
- let ?D = "\<lambda>x. \<not> f x x"
- from * have "\<exists>x. ?D = f x" ..
- then obtain a where "?D = f a" ..
- then have "?D a \<longleftrightarrow> f a a" by (rule arg_cong)
- then have "\<not> f a a \<longleftrightarrow> f a a" .
- then show False by (rule iff_contradiction)
-qed
-
-
-subsection \<open>Classic Isabelle/HOL example\<close>
-
-text \<open>
- The following treatment of Cantor's Theorem follows the classic example from
- the early 1990s, e.g.\ see the file \<^verbatim>\<open>92/HOL/ex/set.ML\<close> in
- Isabelle92 or @{cite \<open>\S18.7\<close> "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]
- \<open>\<forall>f::\<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool. \<exists>S::\<alpha> \<Rightarrow> bool. \<forall>x::\<alpha>. f x \<noteq> S\<close>}
-
- Viewing types as sets, \<open>\<alpha> \<Rightarrow> bool\<close> represents the powerset of \<open>\<alpha>\<close>. This
- version of the theorem states that for every function from \<open>\<alpha>\<close> to its
- powerset, some subset is outside its range. The Isabelle/Isar proofs below
- uses HOL's set theory, with the type \<open>\<alpha> set\<close> and the operator \<open>range :: (\<alpha> \<Rightarrow>
- \<beta>) \<Rightarrow> \<beta> set\<close>.
-\<close>
-
-theorem "\<exists>S. S \<notin> range (f :: 'a \<Rightarrow> 'a set)"
-proof
- let ?S = "{x. x \<notin> f x}"
- show "?S \<notin> range f"
- proof
- assume "?S \<in> range f"
- then obtain y where "?S = f y" ..
- then show False
- proof (rule equalityCE)
- assume "y \<in> f y"
- assume "y \<in> ?S"
- then have "y \<notin> f y" ..
- with \<open>y \<in> f y\<close> show ?thesis by contradiction
- next
- assume "y \<notin> ?S"
- assume "y \<notin> f y"
- then have "y \<in> ?S" ..
- with \<open>y \<notin> ?S\<close> show ?thesis by contradiction
- qed
- qed
-qed
-
-text \<open>
- 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.
-\<close>
-
-theorem "\<exists>S. S \<notin> range (f :: 'a \<Rightarrow> 'a set)"
- by best
-
-end
--- 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 \<open>The Drinker's Principle\<close>
-
-theory Drinker
- imports Main
-begin
-
-text \<open>
- 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.
-\<close>
-
-lemma de_Morgan:
- assumes "\<not> (\<forall>x. P x)"
- shows "\<exists>x. \<not> P x"
-proof (rule classical)
- assume "\<nexists>x. \<not> P x"
- have "\<forall>x. P x"
- proof
- fix x show "P x"
- proof (rule classical)
- assume "\<not> P x"
- then have "\<exists>x. \<not> P x" ..
- with \<open>\<nexists>x. \<not> P x\<close> show ?thesis by contradiction
- qed
- qed
- with \<open>\<not> (\<forall>x. P x)\<close> show ?thesis by contradiction
-qed
-
-theorem Drinker's_Principle: "\<exists>x. drunk x \<longrightarrow> (\<forall>x. drunk x)"
-proof cases
- assume "\<forall>x. drunk x"
- then have "drunk a \<longrightarrow> (\<forall>x. drunk x)" for a ..
- then show ?thesis ..
-next
- assume "\<not> (\<forall>x. drunk x)"
- then have "\<exists>x. \<not> drunk x" by (rule de_Morgan)
- then obtain a where "\<not> drunk a" ..
- have "drunk a \<longrightarrow> (\<forall>x. drunk x)"
- proof
- assume "drunk a"
- with \<open>\<not> drunk a\<close> show "\<forall>x. drunk x" by contradiction
- qed
- then show ?thesis ..
-qed
-
-end
--- 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 \<open>Textbook-style reasoning: the Knaster-Tarski Theorem\<close>
-
-theory Knaster_Tarski
- imports Main "HOL-Library.Lattice_Syntax"
-begin
-
-
-subsection \<open>Prose version\<close>
-
-text \<open>
- According to the textbook @{cite \<open>pages 93--94\<close> "davey-priestley"}, the
- Knaster-Tarski fixpoint theorem is as follows.\<^footnote>\<open>We have dualized the
- argument, and tuned the notation a little bit.\<close>
-
- \<^bold>\<open>The Knaster-Tarski Fixpoint Theorem.\<close> Let \<open>L\<close> be a complete lattice and
- \<open>f: L \<rightarrow> L\<close> an order-preserving map. Then \<open>\<Sqinter>{x \<in> L | f(x) \<le> x}\<close> is a fixpoint
- of \<open>f\<close>.
-
- \<^bold>\<open>Proof.\<close> Let \<open>H = {x \<in> L | f(x) \<le> x}\<close> and \<open>a = \<Sqinter>H\<close>. For all \<open>x \<in> H\<close> we have
- \<open>a \<le> x\<close>, so \<open>f(a) \<le> f(x) \<le> x\<close>. Thus \<open>f(a)\<close> is a lower bound of \<open>H\<close>, whence
- \<open>f(a) \<le> a\<close>. We now use this inequality to prove the reverse one (!) and
- thereby complete the proof that \<open>a\<close> is a fixpoint. Since \<open>f\<close> is
- order-preserving, \<open>f(f(a)) \<le> f(a)\<close>. This says \<open>f(a) \<in> H\<close>, so \<open>a \<le> f(a)\<close>.\<close>
-
-
-subsection \<open>Formal versions\<close>
-
-text \<open>
- 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.
-\<close>
-
-theorem Knaster_Tarski:
- fixes f :: "'a::complete_lattice \<Rightarrow> 'a"
- assumes "mono f"
- shows "\<exists>a. f a = a"
-proof
- let ?H = "{u. f u \<le> u}"
- let ?a = "\<Sqinter>?H"
- show "f ?a = ?a"
- proof -
- {
- fix x
- assume "x \<in> ?H"
- then have "?a \<le> x" by (rule Inf_lower)
- with \<open>mono f\<close> have "f ?a \<le> f x" ..
- also from \<open>x \<in> ?H\<close> have "\<dots> \<le> x" ..
- finally have "f ?a \<le> x" .
- }
- then have "f ?a \<le> ?a" by (rule Inf_greatest)
- {
- also presume "\<dots> \<le> f ?a"
- finally (order_antisym) show ?thesis .
- }
- from \<open>mono f\<close> and \<open>f ?a \<le> ?a\<close> have "f (f ?a) \<le> f ?a" ..
- then have "f ?a \<in> ?H" ..
- then show "?a \<le> f ?a" by (rule Inf_lower)
- qed
-qed
-
-text \<open>
- 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.
-\<close>
-
-theorem Knaster_Tarski':
- fixes f :: "'a::complete_lattice \<Rightarrow> 'a"
- assumes "mono f"
- shows "\<exists>a. f a = a"
-proof
- let ?H = "{u. f u \<le> u}"
- let ?a = "\<Sqinter>?H"
- show "f ?a = ?a"
- proof (rule order_antisym)
- show "f ?a \<le> ?a"
- proof (rule Inf_greatest)
- fix x
- assume "x \<in> ?H"
- then have "?a \<le> x" by (rule Inf_lower)
- with \<open>mono f\<close> have "f ?a \<le> f x" ..
- also from \<open>x \<in> ?H\<close> have "\<dots> \<le> x" ..
- finally show "f ?a \<le> x" .
- qed
- show "?a \<le> f ?a"
- proof (rule Inf_lower)
- from \<open>mono f\<close> and \<open>f ?a \<le> ?a\<close> have "f (f ?a) \<le> f ?a" ..
- then show "f ?a \<in> ?H" ..
- qed
- qed
-qed
-
-end
--- 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 \<open>Peirce's Law\<close>
-
-theory Peirce
- imports Main
-begin
-
-text \<open>
- We consider Peirce's Law: \<open>((A \<longrightarrow> B) \<longrightarrow> A) \<longrightarrow> A\<close>. 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>\<open>The rule involved there is negation elimination; it holds in
- intuitionistic logic as well.\<close>\<close>
-
-theorem "((A \<longrightarrow> B) \<longrightarrow> A) \<longrightarrow> A"
-proof
- assume "(A \<longrightarrow> B) \<longrightarrow> A"
- show A
- proof (rule classical)
- assume "\<not> A"
- have "A \<longrightarrow> B"
- proof
- assume A
- with \<open>\<not> A\<close> show B by contradiction
- qed
- with \<open>(A \<longrightarrow> B) \<longrightarrow> A\<close> show A ..
- qed
-qed
-
-text \<open>
- In the subsequent version the reasoning is rearranged by means of ``weak
- assumptions'' (as introduced by \<^theory_text>\<open>presume\<close>). Before assuming the negated
- goal \<open>\<not> A\<close>, its intended consequence \<open>A \<longrightarrow> B\<close> is put into place in order to
- solve the main problem. Nevertheless, we do not get anything for free, but
- have to establish \<open>A \<longrightarrow> B\<close> later on. The overall effect is that of a logical
- \<^emph>\<open>cut\<close>.
-
- Technically speaking, whenever some goal is solved by \<^theory_text>\<open>show\<close> 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>\<open>assume\<close>) are solved immediately.
-\<close>
-
-theorem "((A \<longrightarrow> B) \<longrightarrow> A) \<longrightarrow> A"
-proof
- assume "(A \<longrightarrow> B) \<longrightarrow> A"
- show A
- proof (rule classical)
- presume "A \<longrightarrow> B"
- with \<open>(A \<longrightarrow> B) \<longrightarrow> A\<close> show A ..
- next
- assume "\<not> A"
- show "A \<longrightarrow> B"
- proof
- assume A
- with \<open>\<not> A\<close> show B by contradiction
- qed
- qed
-qed
-
-text \<open>
- 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>\<open>and\<close> 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.
-\<close>
-
-end
--- 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 \<open>Export and re-import of global proof terms\<close>
--- 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
--- 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 \<open>Isabelle/ML basics\<close>
-
-theory "ML"
-imports Main
-begin
-
-section \<open>ML expressions\<close>
-
-text \<open>
- The Isabelle command \<^theory_text>\<open>ML\<close> 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.
-\<close>
-
-ML \<open>1 + 1\<close>
-
-ML \<open>val a = 1\<close>
-ML \<open>val b = 1\<close>
-ML \<open>val c = a + b\<close>
-
-
-section \<open>Antiquotations\<close>
-
-text \<open>
- There are some language extensions (via antiquotations), as explained in the
- ``Isabelle/Isar implementation manual'', chapter 0.
-\<close>
-
-ML \<open>length []\<close>
-ML \<open>\<^assert> (length [] = 0)\<close>
-
-
-text \<open>Formal entities from the surrounding context may be referenced as
- follows:\<close>
-
-term "1 + 1" \<comment> \<open>term within theory source\<close>
-
-ML \<open>\<^term>\<open>1 + 1\<close> (* term as symbolic ML datatype value *)\<close>
-
-ML \<open>\<^term>\<open>1 + (1::int)\<close>\<close>
-
-
-ML \<open>
- (* formal source with position information *)
- val s = \<open>1 + 1\<close>;
-
- (* read term via old-style string interface *)
- val t = Syntax.read_term \<^context> (Syntax.implode_input s);
-\<close>
-
-
-section \<open>Recursive ML evaluation\<close>
-
-ML \<open>
- ML \<open>ML \<open>val a = @{thm refl}\<close>\<close>;
- ML \<open>val b = @{thm sym}\<close>;
- val c = @{thm trans}
- val thms = [a, b, c];
-\<close>
-
-
-section \<open>IDE support\<close>
-
-text \<open>
- 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
-\<close>
-
-ML \<open>fn i => fn list => length list + i\<close>
-
-
-section \<open>Example: factorial and ackermann function in Isabelle/ML\<close>
-
-ML \<open>
- fun factorial 0 = 1
- | factorial n = n * factorial (n - 1)
-\<close>
-
-ML \<open>factorial 42\<close>
-ML \<open>factorial 10000 div factorial 9999\<close>
-
-text \<open>See \<^url>\<open>http://mathworld.wolfram.com/AckermannFunction.html\<close>.\<close>
-
-ML \<open>
- fun ackermann 0 n = n + 1
- | ackermann m 0 = ackermann (m - 1) 1
- | ackermann m n = ackermann (m - 1) (ackermann m (n - 1))
-\<close>
-
-ML \<open>timeit (fn () => ackermann 3 10)\<close>
-
-
-section \<open>Parallel Isabelle/ML\<close>
-
-text \<open>
- 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.
-\<close>
-
-ML \<open>
- val x = Future.fork (fn () => ackermann 3 10);
- val y = Future.fork (fn () => ackermann 3 10);
- val z = Future.join x + Future.join y
-\<close>
-
-text \<open>
- The \<^ML_structure>\<open>Par_List\<close> module provides high-level combinators for
- parallel list operations.
-\<close>
-
-ML \<open>timeit (fn () => map (fn n => ackermann 3 n) (1 upto 10))\<close>
-ML \<open>timeit (fn () => Par_List.map (fn n => ackermann 3 n) (1 upto 10))\<close>
-
-
-section \<open>Function specifications in Isabelle/HOL\<close>
-
-fun factorial :: "nat \<Rightarrow> nat"
-where
- "factorial 0 = 1"
-| "factorial (Suc n) = Suc n * factorial n"
-
-term "factorial 4" \<comment> \<open>symbolic term\<close>
-value "factorial 4" \<comment> \<open>evaluation via ML code generation in the background\<close>
-
-declare [[ML_source_trace]]
-ML \<open>\<^term>\<open>factorial 4\<close>\<close> \<comment> \<open>symbolic term in ML\<close>
-ML \<open>@{code "factorial"}\<close> \<comment> \<open>ML code from function specification\<close>
-
-
-fun ackermann :: "nat \<Rightarrow> nat \<Rightarrow> 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
-
--- 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 \<open>Finite sequences\<close>
-
-theory Seq
-imports Main
-begin
-
-datatype 'a seq = Empty | Seq 'a "'a seq"
-
-fun conc :: "'a seq \<Rightarrow> 'a seq \<Rightarrow> 'a seq"
-where
- "conc Empty ys = ys"
-| "conc (Seq x xs) ys = Seq x (conc xs ys)"
-
-fun reverse :: "'a seq \<Rightarrow> '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