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