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