Quelle  Document.thy

theory Document
  imports Main
begin

section ‹Abstract›

text ‹
  \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
  🪙‹https://ctan.org/pkg/foiltex› for further information.
 ›


chapter ‹Introduction›

section ‹Some slide›

paragraph ‹Point 1:
  \plainstyle ABC›

text ‹
  🪙 something
  🪙 to say \dots
 ›

paragraph ‹Point 2:
  \plainstyle XYZ›

text ‹
  🪙 more
  🪙 to say \dots
 ›


section ‹Another slide›

paragraph ‹Key definitions:›

text ‹Informal bla bla.›

definition "foo = True"  🍋 ‹side remark on 🍋‹foo›\›

definition "bar = False"  🍋 ‹side remark on 🍋‹bar›\›

lemma foo unfolding foo_def ..


chapter ‹Application: Cantor's theorem›

section ‹Informal notes›

text_raw ‹\isakeeptag{proof}›
text ‹
  Cantor's Theorem states that there is no surjection from
  a set to its powerset. The proof works by diagonalization. E.g.\ see
  🪙 🪙‹http://mathworld.wolfram.com/CantorDiagonalMethod.html›
  🪙 🪙‹https://en.wikipedia.org/wiki/Cantor's_diagonal_argument›
 ›

section ‹Formal proof›

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 ‹Conclusion›

section ‹Lorem ipsum dolor›

text ‹
  🪙 Lorem ipsum dolor sit amet, consectetur adipiscing elit.
  🪙 Donec id ipsum sapien.
  🪙 Vivamus malesuada enim nibh, a tristique nisi sodales ac.
  🪙 Praesent ut sem consectetur, interdum tellus ac, sodales nulla.
 ›

end