# HG changeset patch
# User wenzelm
# Date 1007563485 -3600
# Node ID 2e4fb29496b0849b50079f5343398968adf9a636
# Parent  45dc2986aeb4a9651376fa8eb3ae6fb47cb13f20
iff;

diff -r 45dc2986aeb4 -r 2e4fb29496b0 src/FOL/ex/First_Order_Logic.thy
--- 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 *}