Quelle First_Order_Logic.thy Sprache: Isabelle

(*  Title:      Pure/Examples/First_Order_Logic.thy
    Author:     Makarius
*)

section \<open>A simple formulation of First-Order Logic\<close>

text \<open>
  The subsequent theory development illustrates single-sorted intuitionistic
  first-order logic with equality, formulated within the Pure framework.
\<close>

theory First_Order_Logic
  imports Pure
begin

subsection \<open>Abstract syntax\<close>

typedecl i
typedecl o

judgment Trueprop :: "o \ prop" (\_\ 5)

subsection \<open>Propositional logic\<close>

axiomatization false :: o  (\<open>\<bottom>\<close>)
  where falseE [elim]: "\ \ A"

axiomatization imp :: "o \ o \ o" (infixr \\\ 25)
  where impI [intro]: "(A \ B) \ A \ B"
    and mp [dest]: "A \ B \ A \ B"

axiomatization conj :: "o \ o \ o" (infixr \\\ 35)
  where conjI [intro]: "A \ B \ A \ B"
    and conjD1: "A \ B \ A"
    and conjD2: "A \ B \ B"

theorem conjE [elim]:
  assumes "A \ B"
  obtains A and B
proof
  from \<open>A \<and> B\<close> show A
    by (rule conjD1)
  from \<open>A \<and> B\<close> show B
    by (rule conjD2)
qed

axiomatization disj :: "o \ o \ o" (infixr \\\ 30)
  where disjE [elim]: "A \ B \ (A \ C) \ (B \ C) \ C"
    and disjI1 [intro]: "A \ A \ B"
    and disjI2 [intro]: "B \ A \ B"

definition true :: o  (\<open>\<top>\<close>)
  where "\ \ \ \ \"

theorem trueI [intro]: \<top>
  unfolding true_def ..

definition not :: "o \ o" (\\ _\ [40] 40)
  where "\ A \ A \ \"

theorem notI [intro]: "(A \ \) \ \ A"
  unfolding not_def ..

theorem notE [elim]: "\ A \ A \ B"
  unfolding not_def
proof -
  assume "A \ \" and A
  then have \<bottom> ..
  then show B ..
qed

definition iff :: "o \ o \ o" (infixr \\\ 25)
  where "A \ B \ (A \ B) \ (B \ A)"

theorem iffI [intro]:
  assumes "A \ B"
    and "B \ A"
  shows "A \ B"
  unfolding iff_def
proof
  from \<open>A \<Longrightarrow> B\<close> show "A \<longrightarrow> B" ..
  from \<open>B \<Longrightarrow> A\<close> show "B \<longrightarrow> A" ..
qed

theorem iff1 [elim]:
  assumes "A \ B" and A
  shows B
proof -
  from \<open>A \<longleftrightarrow> B\<close> have "(A \<longrightarrow> B) \<and> (B \<longrightarrow> A)"
    unfolding iff_def .
  then have "A \ B" ..
  from this and \<open>A\<close> show B ..
qed

theorem iff2 [elim]:
  assumes "A \ B" and B
  shows A
proof -
  from \<open>A \<longleftrightarrow> B\<close> have "(A \<longrightarrow> B) \<and> (B \<longrightarrow> A)"
    unfolding iff_def .
  then have "B \ A" ..
  from this and \<open>B\<close> show A ..
qed

subsection \<open>Equality\<close>

axiomatization equal :: "i \ i \ o" (infixl \=\ 50)
  where refl [intro]: "x = x"
    and subst: "x = y \ P x \ P y"

theorem trans [trans]: "x = y \ y = z \ x = z"
  by (rule subst)

theorem sym [sym]: "x = y \ y = x"
proof -
  assume "x = y"
  from this and refl show "y = x"
    by (rule subst)
qed

subsection \<open>Quantifiers\<close>

axiomatization All :: "(i \ o) \ o" (binder \\\ 10)
  where allI [intro]: "(\x. P x) \ \x. P x"
    and allD [dest]: "\x. P x \ P a"

axiomatization Ex :: "(i \ o) \ o" (binder \\\ 10)
  where exI [intro]: "P a \ \x. P x"
    and exE [elim]: "\x. P x \ (\x. P x \ C) \ C"

lemma "(\x. P (f x)) \ (\y. P y)"
proof
  assume "\x. P (f x)"
  then obtain x where "P (f x)" ..
  then show "\y. P y" ..
qed

lemma "(\x. \y. R x y) \ (\y. \x. R x y)"
proof
  assume "\x. \y. R x y"
  then obtain x where "\y. R x y" ..
  show "\y. \x. R x y"
  proof
    fix y
    from \<open>\<forall>y. R x y\<close> have "R x y" ..
    then show "\x. R x y" ..
  qed
qed

end

quality99%

¤ Dauer der Verarbeitung: 0.19 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.