(*<*)
theory Tutorial = Main:
(*>*)
chapter {* Introduction *}
chapter {* Technical issues *}
section {* Source texts *}
section {* Interaction and debugging *}
section {* Step-by-step examples *}
subsection {* Summing natural numbers *}
theorem "2 * (\<Sum>i < n + 1. i) = n * (n + 1)" (is "?P n")
proof (induct n)
case 0
then show "?P 0" by simp
next
case (Suc n)
let "?S n = _" = "?P n"
have "?S (n + 1) = ?S n + 2 * (n + 1)" by simp
also have "?S n = n * (n + 1)" .
also have "\<dots> + 2 * (n + 1) = (n + 1) * (n + 2)" by simp
finally show "?P (Suc n)" by simp
qed
theorem "2 * (\<Sum>i < n + 1. i) = n * (n + 1)"
proof (induct n)
case 0
then show ?case by simp
next
case Suc
then show ?case by simp
qed
theorem "2 * (\<Sum>i < n + 1. i) = n * (n + 1)"
by (induct n) simp_all
theorem "2 * (\<Sum>i < n + 1. i) = n * (n + 1)"
apply (induct n)
apply simp_all
done
chapter {* Interaction and debugging *}
chapter {* Calculational reasoning *}
chapter {* Proof by cases and induction *}
chapter {* General natural deduction *}
chapter {* Example: FIXME *}
chapter FIXME
section {* Formal document preparation *}
subsection {* Example *}
text {*
See this very document itself.
*}
subsection {* Getting started *}
text {*
\verb"isatool mkdir Test && isatool make"
*}
section {* Human-readable proof composition in Isar *}
subsection {* Getting started *}
text {* Claim a trivial goal in order to enter proof mode @{text \<dots>} *}
lemma True
proof
txt {* After the canonical initial refinement step we are left
within an \emph{proof body}. *}
txt {* Here we may augment the present local {proof context} as we
please. *}
fix something
assume a: "anything something"
txt {* Note that the present configuration may be inspected by
several \emph{diagnostic commands}. *}
term something -- "@{term [show_types] something}"
term anything -- "@{term [show_types] anything}"
thm a -- {* @{thm a} *}
txt {* We may state local (auxiliary) results as well. *}
have True proof qed
txt {* We are now satisfied. *}
qed
subsection {* Calculational Reasoning *}
text {*
Isar is mainly about Natural Deduction, but Calculational Reasoning
turns out as a simplified instance of that, so we demonstrate it
first.
*}
subsubsection {* Transitive chains *}
text {*
Technique: establish a chain of local facts, separated by \cmd{also}
and terminated by \cmd{finally}; another goal has to follow to point
out the final result.
*}
lemma "x1 = x4"
proof - -- "do nothing yet"
have "x1 = x2" sorry
also
have "x2 = x3" sorry
also
have "x3 = x4" sorry
finally
show "x1 = x4" .
qed
text {*
This may be written more succinctly, using the special term binds
``@{text \<dots>}'' (for the right-hand side of the last statement) and
``@{text ?thesis}'' (for the original claim at the head of the
proof).
*}
lemma "x1 = x4"
proof -
have "x1 = x2" sorry
also have "\<dots> = x3" sorry
also have "\<dots> = x4" sorry
finally show ?thesis .
qed
text {*
The (implicit) forward-chaining steps involved in \cmd{also} and
\cmd{finally} are declared in the current context. The main library
of Isabelle/HOL already knows about (mixed) transitivities of @{text
"="}, @{text "<"}, @{text "\<le>"} etc.
*}
lemma "(x1::nat) < x6"
-- {* restriction to type @{typ nat} ensures that @{text "<"} is really transitive *}
proof -
have "x1 < x2" sorry
also have "\<dots> \<le> x3" sorry
also have "\<dots> = x4" sorry
also have "\<dots> < x5" sorry
also have "\<dots> = x6" sorry
finally show ?thesis .
qed
text {*
We may also calculate on propositions.
*}
lemma True
proof
have "A \<longrightarrow> B \<longrightarrow> C" sorry
also have A sorry
also have B sorry
finally have C .
qed
text {*
This is getting pretty close to Dijkstra's preferred proof style.
*}
lemma True
proof
have [trans]: "\<And>X Y Z. X \<longrightarrow> Y \<Longrightarrow> Y \<longrightarrow> Z \<Longrightarrow> X \<longrightarrow> Z" by rules
have "A \<longrightarrow> B" sorry
also have "\<dots> \<longrightarrow> C" sorry
also have "\<dots> \<longrightarrow> D" sorry
finally have "A \<longrightarrow> D" .
qed
subsubsection {* Degenerate calculations and bigstep reasoning *}
text {*
Instead of \cmd{also}/\cmd{finally} we may use degenerative steps
\cmd{moreover}/\cmd{ultimately} to accumulate facts, without
applying any forward rules yet.
*}
lemma True
proof
have A sorry
moreover have B sorry
moreover have C sorry
ultimately have A and B and C . -- "Pretty obvious, right?"
qed
text {*
Both kinds of calculational elements may be used together.
*}
lemma True
proof
assume reasoning_pattern [trans]: "A \<Longrightarrow> B \<Longrightarrow> C \<Longrightarrow> D"
have A sorry
moreover have B sorry
moreover have C sorry
finally have D .
qed
subsection {* Natural deduction *}
subsubsection {* Primitive patterns *}
text {*
The default theory context admits to perform canonical single-step
reasoning (similar to Gentzen) without further ado.
*}
lemma True
proof
have True ..
{ assume False
then have C .. }
have "\<not> A"
proof
assume A
show False sorry
qed
{ assume "\<not> A" and A
then have C .. }
have "A \<longrightarrow> B"
proof
assume A
show B sorry
qed
{ assume "A \<longrightarrow> B" and A
then have B .. }
have "A \<and> B"
proof
show A sorry
show B sorry
qed
{ assume "A \<and> B"
then have A .. }
{ assume "A \<and> B"
then have B .. }
{ assume A
then have "A \<or> B" .. }
{ assume B
then have "A \<or> B" .. }
{ assume "A \<or> B"
then have C
proof
assume A
then show ?thesis sorry
next
assume B
then show ?thesis sorry
qed }
have "\<forall>x. P x"
proof
fix x
show "P x" sorry
qed
{ assume "\<forall>x. P x"
then have "P t" .. }
have "\<exists>x. P x"
proof
show "P t" sorry
qed
{ assume "\<exists>x. P x"
then obtain x where "P x" ..
note nothing -- "relax" }
qed
text {*
Certainly, this works with derived rules for defined concepts in the
same manner. E.g.\ use the simple-typed set-theory of Isabelle/HOL. *}
lemma True
proof
have "y \<in> (\<Inter>x \<in> A. B x)"
proof
fix x
assume "x \<in> A"
show "y \<in> B x" sorry
qed
have "y \<in> (\<Union>x \<in> A. B x)"
proof
show "a \<in> A" sorry
show "y \<in> B a" sorry
qed
qed
subsubsection {* Variations in structure *}
text {*
The design of the Isar language takes the user seriously
*}
subsubsection {* Generalized elimination *}
subsubsection {* Scalable cases and induction *}
section {* Assimilating the old tactical style *}
text {*
Improper commands:
Observation: every Isar subproof may start with a ``script'' of
*}
(*<*)
end
(*>*)