(* A simple comment *) theory week01A_demo1 imports Main begin text \This is also a comment but it generates nice \LaTeX-text!\ text \ Note that free variables (eg @{term x}), bound variables (eg @{term "\n. n"}) and constants (eg @{term Suc}) are displayed differently. \ term "x" term "Suc x" term "Succ x" term "Suc x = Succ y" term "\x. x" text \To display more types inside terms:\ declare [[show_types]] term "Suc x = Succ y" text \To switch off again:\ declare [[show_types=false]] term "Suc x = Succ y" text \0 and + are overloaded:\ prop "n + n = 0" prop "(n::nat) + n = 0" prop "(n::int) + n = 0" prop "n + n = Suc m" text\A bound variable:\ term "\x. x v" term "\x. Suc x < y" prop "map (\n. Suc n + 1) [0, 1] = [2, 3]" text \Terms must be type correct!\ term "Suc n = True" text \Displaying theorems, schematic variables\ thm conjI text \Schematic variables have question marks and can be instantiated:\ thm conjI [where ?Q = "x"] thm impI thm disjE text \ You can use \texttt{term}, \texttt{prop} and \texttt{thm} in \LaTeX sections, too! The lemma conjI is: @{thm conjI}. Nicer version, without schematic variables: @{thm conjI [no_vars]}. \ thm conjI [no_vars] text \Finding theorems\ text \Searching for constants/functions:\ find_theorems "map" text \A list of search criteria finds thms that match all of them:\ find_theorems "map" "zip" text \To search for patterns, use underscore:\ find_theorems "_ + _ = _ - _" find_theorems "_ + _" "_ < _" "Suc" text \Searching for theorem names:\ find_theorems name: "conj" text \They can all be combined, theorem names include the theory name:\ find_theorems "_ \ _" name: "HOL." -name: "conj" text \Stating theorems and a first proof\ lemma "A \ A" \ \a single line comment\ \ \note the goals window\ apply (rule impI) apply assumption done text \ A proof is a list of {\tt apply} statements, terminated by {\tt done}. {\tt apply} takes a proof method as argument (assumption, rule, etc.). It needs parentheses when the method consists of more than one word. \ text \Isabelle doesn't care if you call it lemma, theorem or corollary\ theorem "A \ A" apply (rule impI) apply assumption done corollary "A \ A" apply (rule impI) apply assumption done text \You can give it a name, too\ lemma mylemma: "A \ A" by (rule impI) text \Abandoning a proof\ lemma "P = NP" \ \this is too hard\ oops text \Isabelle forgets the lemma and you cannot use it later\ text \Faking a proof\ lemma "P \ NP" \ \have an idea, will show this later\ sorry text \ {\tt sorry} only works interactively (and in {\em quick-and-dirty-mode}), and Isabelle keeps track of what you have faked. \ text \Proof styles\ \ \automatic\ theorem Cantor: "\S. S \ range (f :: 'a \ 'a set)" by best \ \exploring, but unstructured\ theorem Cantor': "\S. S \ range (f :: 'a \ 'a set)" apply (rule_tac x = "{x. x \ f x}" in exI) apply (rule notI) apply clarsimp apply blast done \ \structured, explaining\ theorem Cantor'': "\S. S \ range (f :: 'a \ 'a set)" proof let ?S = "{x. x \ f x}" show "?S \ range f" proof assume "?S \ range f" then obtain y where fy: "?S = f y" .. show False proof cases assume yin: "y \ ?S" hence "y \ f y" by simp hence "y \ ?S" by(simp add:fy) thus False using yin by contradiction next assume yout: "y \ ?S" hence "y \ f y" by simp hence "y \ ?S" by(simp add:fy) thus False using yout by contradiction qed qed qed find_theorems "Suc (Suc _)" find_theorems "(_ + _) + _ = _ + (_ + _)" end