Theory Structured_Statements

theory Structured_Statements
imports Main
```(*  Title:      HOL/Isar_Examples/Structured_Statements.thy
Author:     Makarius
*)

section ‹Structured statements within Isar proofs›

theory Structured_Statements
imports Main
begin

subsection ‹Introduction steps›

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›

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›

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›

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›

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
```