doc-src/IsarTut/Tutorial/Tutorial.thy

added nat_split

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