Quelle  Structured_Statements.thy   Sprache: Isabelle

(*  Title:      HOL/Isar_Examples/Structured_Statements.thy
    Author:     Makarius
*)

section ‹Structured statements within Isar proofs›

theory Structured_Statements
  imports Main
begin

subsection ‹Introduction steps›

notepad
begin
  fix A B :: bool
  fix P :: "'a \ bool"

  have "A \ B"
  proof
    show B if A using that 🍋
  qed

  have "\ A"
  proof
    show False if A using that 🍋
  qed

  have "\x. P x"
  proof
    show "P x" for x 🍋
  qed
end


subsection ‹If-and-only-if›

notepad
begin
  fix A B :: bool

  have "A \ B"
  proof
    show B if A 🍋
    show A if B 🍋
  qed
next
  fix A B :: bool

  have iff_comm: "(A \ B) \ (B \ A)"
  proof
    show "B \ A" if "A \ B"
    proof
      show B using that ..
      show A using that ..
    qed
    show "A \ B" if "B \ A"
    proof
      show A using that ..
      show B using that ..
    qed
  qed

  text ‹Alternative proof, avoiding redundant copy of symmetric argument.›
  have iff_comm: "(A \ B) \ (B \ A)"
  proof
    show "B \ A" if "A \ B" for A B
    proof
      show B using that ..
      show A using that ..
    qed
    then show "A \ B" if "B \ A"
      by this (rule that)
  qed
end


subsection ‹Elimination and cases›

notepad
begin
  fix A B C D :: bool
  assume *: "A \ B \ C \ D"

  consider (a) A | (b) B | (c) C | (d) D
    using * by blast
  then have something
  proof cases
    case a  thm ‹A›
    then show ?thesis 🍋
  next
    case b  thm ‹B›
    then show ?thesis 🍋
  next
    case c  thm ‹C›
    then show ?thesis 🍋
  next
    case d  thm ‹D›
    then show ?thesis 🍋
  qed
next
  fix A :: "'a \ bool"
  fix B :: "'b \ 'c \ bool"
  assume *: "(\x. A x) \ (\y z. B y z)"

  consider (a) x where "A x" | (b) y z where "B y z"
    using * by blast
  then have something
  proof cases
    case a  thm ‹A x›
    then show ?thesis 🍋
  next
    case b  thm ‹B y z›
    then show ?thesis 🍋
  qed
end


subsection ‹Induction›

notepad
begin
  fix P :: "nat \ bool"
  fix n :: nat

  have "P n"
  proof (induct n)
    show "P 0" 🍋
    show "P (Suc n)" if "P n" for n  thm ‹P n›
      using that 🍋
  qed
end


subsection ‹Suffices-to-show›

notepad
begin
  fix A B C
  assume r: "A \ B \ C"

  have C
  proof -
    show ?thesis when A (is ?A) and B (is ?B)
      using that by (rule r)
    show ?A 🍋
    show ?B 🍋
  qed
next
  fix a :: 'a
  fix A :: "'a \ bool"
  fix C

  have C
  proof -
    show ?thesis when "A x" (is ?A) for x :: 'a \ \abstract \<^term>\x\\
      using that 🍋
    show "?A a"  🍋 ‹concrete 🍋‹a››
      🍋
  qed
end

end