author wenzelm Wed, 05 Dec 2001 15:44:45 +0100 changeset 12392 2e4fb29496b0 parent 12391 45dc2986aeb4 child 12393 03c55bb0ee92
iff;
```--- a/src/FOL/ex/First_Order_Logic.thy	Wed Dec 05 15:36:48 2001 +0100
+++ b/src/FOL/ex/First_Order_Logic.thy	Wed Dec 05 15:44:45 2001 +0100
@@ -62,6 +62,9 @@
"\<top> \<equiv> \<bottom> \<longrightarrow> \<bottom>"
not :: "o \<Rightarrow> o"    ("\<not> _" [40] 40)
"\<not> A \<equiv> A \<longrightarrow> \<bottom>"
+  iff :: "o \<Rightarrow> o \<Rightarrow> o"    (infixr "\<longleftrightarrow>" 25)
+  "A \<longleftrightarrow> B \<equiv> (A \<longrightarrow> B) \<and> (B \<longrightarrow> A)"
+

theorem trueI [intro]: \<top>
proof (unfold true_def)
@@ -80,6 +83,27 @@
hence \<bottom> .. thus B ..
qed

+theorem iffI [intro]: "(A \<Longrightarrow> B) \<Longrightarrow> (B \<Longrightarrow> A) \<Longrightarrow> A \<longleftrightarrow> B"
+proof (unfold iff_def)
+  assume "A \<Longrightarrow> B" hence "A \<longrightarrow> B" ..
+  moreover assume "B \<Longrightarrow> A" hence "B \<longrightarrow> A" ..
+  ultimately show "(A \<longrightarrow> B) \<and> (B \<longrightarrow> A)" ..
+qed
+
+theorem iff1 [elim]: "A \<longleftrightarrow> B \<Longrightarrow> A \<Longrightarrow> B"
+proof (unfold iff_def)
+  assume "(A \<longrightarrow> B) \<and> (B \<longrightarrow> A)"
+  hence "A \<longrightarrow> B" ..
+  thus "A \<Longrightarrow> B" ..
+qed
+
+theorem iff2 [elim]: "A \<longleftrightarrow> B \<Longrightarrow> B \<Longrightarrow> A"
+proof (unfold iff_def)
+  assume "(A \<longrightarrow> B) \<and> (B \<longrightarrow> A)"
+  hence "B \<longrightarrow> A" ..
+  thus "B \<Longrightarrow> A" ..
+qed
+

subsection {* Equality *}
```