Quelle  Document.thy   Sprache: unbekannt

theory Document
  imports Main
begin

section ‹Some section›

subsection ‹Some subsection›

subsection ‹Some subsubsection›

subsubsection ‹Some subsubsubsection›

paragraph ‹A paragraph.›

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


paragraph ‹Another paragraph.›

text ‹See also cite‹‹\S3› in "isabelle-system"›.›


section ‹Formal proof of Cantor's theorem›

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

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


subsection ‹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. Quisque vel diam at
 risus tempus tempor eget a tortor. Suspendisse potenti. Nulla erat lacus,
 dignissim sed volutpat nec, feugiat non leo. Nunc blandit et justo sed
 venenatis. Donec scelerisque placerat magna, et congue nulla convallis vel.
 Cras tristique dolor consequat dolor tristique rutrum. Suspendisse ultrices
 sem nibh, et suscipit felis ultricies at. Aliquam venenatis est vel nulla
 efficitur ornare. Lorem ipsum dolor sit amet, consectetur adipiscing elit.
 ›

end