(* 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 ("\")
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 ("\")
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
¤ Dauer der Verarbeitung: 0.2 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.
|
