Quelle Document.thy Sprache: Isabelle

theory Document
  imports Main
begin

section \<open>Abstract\<close>

text \<open>
  \small
  Isabelle is a formal document preparation system. This example shows how to
  use it together with Foil{\TeX} to produce slides in {\LaTeX}. See
  \<^url>\<open>https://ctan.org/pkg/foiltex\<close> for further information.
\<close>

chapter \<open>Introduction\<close>

section \<open>Some slide\<close>

paragraph \<open>Point 1:
  \plainstyle ABC\<close>

text \<open>
  \<^item> something
  \<^item> to say \dots
\<close>

paragraph \<open>Point 2:
  \plainstyle XYZ\<close>

text \<open>
  \<^item> more
  \<^item> to say \dots
\<close>

section \<open>Another slide\<close>

paragraph \<open>Key definitions:\<close>

text \<open>Informal bla bla.\<close>

definition "foo = True"  \<comment> \<open>side remark on \<^const>\<open>foo\<close>\<close>

definition "bar = False"  \<comment> \<open>side remark on \<^const>\<open>bar\<close>\<close>

lemma foo unfolding foo_def ..

chapter \<open>Application: Cantor's theorem\<close>

section \<open>Informal notes\<close>

text_raw \<open>\isakeeptag{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>

section \<open>Formal proof\<close>

theorem Cantor: "\f :: 'a \ 'a set. \A. \x. A = f x"
proof
  assume "\f :: 'a \ 'a set. \A. \x. A = f x"
  then obtain f :: "'a \ 'a set" where *: "\A. \x. A = f x" ..
  let ?D = "{x. x \ f x}"
  from * obtain a where "?D = f a" by blast
  moreover have "a \ ?D \ a \ f a" by blast
  ultimately show False by blast
qed

chapter \<open>Conclusion\<close>

section \<open>Lorem ipsum dolor\<close>

text \<open>
  \<^item> Lorem ipsum dolor sit amet, consectetur adipiscing elit.
  \<^item> Donec id ipsum sapien.
  \<^item> Vivamus malesuada enim nibh, a tristique nisi sodales ac.
  \<^item> Praesent ut sem consectetur, interdum tellus ac, sodales nulla.
\<close>

end

quality100%

¤ Dauer der Verarbeitung: 0.4 Sekunden ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.