Theory Structured_Statements

(*  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 \<proof>
  qed

  have "¬ A"
  proof
    show False if A using that \<proof>
  qed

  have "∀x. P x"
  proof
    show "P x" for x \<proof>
  qed
end


subsection ‹If-and-only-if›

notepad
begin
  fix A B :: bool

  have "A ⟷ B"
  proof
    show B if A \<proof>
    show A if B \<proof>
  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 \<proof>
  next
    case b  thm ‹B›
    then show ?thesis \<proof>
  next
    case c  thm ‹C›
    then show ?thesis \<proof>
  next
    case d  thm ‹D›
    then show ?thesis \<proof>
  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 \<proof>
  next
    case b  thm ‹B y z›
    then show ?thesis \<proof>
  qed
end


subsection ‹Induction›

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

  have "P n"
  proof (induct n)
    show "P 0" \<proof>
    show "P (Suc n)" if "P n" for n  thm ‹P n›
      using that \<proof>
  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 \<proof>
    show ?B \<proof>
  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 \<proof>
    show "?A a"  ― ‹concrete \<^term>‹a››
      \<proof>
  qed
end

end