summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Mon, 08 Jun 2020 21:38:41 +0200 | |

changeset 71925 | bf085daea304 |

parent 71924 | e5df9c8d9d4b |

child 71926 | bee83c9d3306 |

clarified sessions: "Notable Examples in Isabelle/HOL";

--- 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