Theory Document

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 \<^const>‹foo››

definition "bar = False"  ― ‹side remark on \<^const>‹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