Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Structured_Statements.thy Sprache: Isabelle

Original von: Isabelle^©

(*  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.7 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.