(* 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