(* Title: HOL/Isar_Examples/Structured_Statements.thy
Author: Makarius
*)
section \<open>Structured statements within Isar proofs\<close>
theory Structured_Statements
imports Main
begin
subsection \<open>Introduction steps\<close>
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 \<open>If-and-only-if\<close>
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 \<open>Alternative proof, avoiding redundant copy of symmetric argument.\<close>
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 \<open>Elimination and cases\<close>
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 \<open>A\<close>
then show ?thesis \<proof>
next
case b thm \<open>B\<close>
then show ?thesis \<proof>
next
case c thm \<open>C\<close>
then show ?thesis \<proof>
next
case d thm \<open>D\<close>
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 \<open>A x\<close>
then show ?thesis \<proof>
next
case b thm \<open>B y z\<close>
then show ?thesis \<proof>
qed
end
subsection \<open>Induction\<close>
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 \<open>P n\<close>
using that \<proof>
qed
end
subsection \<open>Suffices-to-show\<close>
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" \<comment> \<open>concrete \<^term>\<open>a\<close>\<close>
\<proof>
qed
end
end
¤ Dauer der Verarbeitung: 0.21 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
