(* A simple comment *) theory Demo01 imports Main begin text {* This is also a comment but it generates nice \LaTeX-text! *} text {* Note that free variables (eg x), bound variables (eg %n) and constants (eg Suc) are displayed differently. *} term "x" term "Suc x" term "Succ x" term "Suc x = Succ y" text {* Navigating in ProofGeneral Try the buttons in the tool bar: {\em next} and {\em undo} for single steps (key bindings C-c C-n and C-c C-u), {\em goto} for processing/undoing whole sections (key binding C-c C-Ret), {\em use} and {\em retract} for processing/undoing whole theories. *} text {* To display types: menu Isabelle/Isar -> Settings -> Show Types *} text {* 0 and + are overloaded: *} prop "n + n = 0" prop "(n::nat) + n = 0" prop "n + n = Suc m" text{* A bound variable: *} term "\x. x" term "\x. Suc x < y" prop "map (\n. Suc n + 1) [0, 1] = [2, 3]"; (* Try this: term "Suc n = True" Terms must be type correct! *) text {* Displaying theorems, schematic variables *} thm conjI 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]}. *} 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. *} (* More ProofGeneral: the {\em state} button shows the goal window, the {\em stop} button interrupts Isabelle during proofs (key binding C-c C-c), the {\em find} button helps you to find theorems (key binding C-c C-f). You can give a list of constant names (use patterns for mixfix syntax). It will find all theorems containing those constants. Try C-c C-f "_ + _" "_ < _" "Suc" *) 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 "y \ ?S" hence "y \ f y" by simp hence "y \ ?S" by(simp add:fy) thus False by contradiction next assume "y \ ?S" hence "y \ f y" by simp hence "y \ ?S" by(simp add:fy) thus False by contradiction qed qed qed end