12369

1 
(* Title: FOL/ex/First_Order_Logic.thy


2 
ID: $Id$


3 
Author: Markus Wenzel, TU Munich


4 
*)


5 


6 
header {* A simple formulation of FirstOrder Logic *}


7 

16417

8 
theory First_Order_Logic imports Pure begin

12369

9 


10 
text {*


11 
The subsequent theory development illustrates singlesorted


12 
intuitionistic firstorder logic with equality, formulated within


13 
the Pure framework. Actually this is not an example of


14 
Isabelle/FOL, but of Isabelle/Pure.


15 
*}


16 


17 
subsection {* Syntax *}


18 


19 
typedecl i


20 
typedecl o


21 


22 
judgment


23 
Trueprop :: "o \<Rightarrow> prop" ("_" 5)


24 


25 


26 
subsection {* Propositional logic *}


27 

21939

28 
axiomatization


29 
false :: o ("\<bottom>") and


30 
imp :: "o \<Rightarrow> o \<Rightarrow> o" (infixr "\<longrightarrow>" 25) and


31 
conj :: "o \<Rightarrow> o \<Rightarrow> o" (infixr "\<and>" 35) and


32 
disj :: "o \<Rightarrow> o \<Rightarrow> o" (infixr "\<or>" 30)


33 
where


34 
falseE [elim]: "\<bottom> \<Longrightarrow> A" and

12369

35 

21939

36 
impI [intro]: "(A \<Longrightarrow> B) \<Longrightarrow> A \<longrightarrow> B" and


37 
mp [dest]: "A \<longrightarrow> B \<Longrightarrow> A \<Longrightarrow> B" and

12369

38 

21939

39 
conjI [intro]: "A \<Longrightarrow> B \<Longrightarrow> A \<and> B" and


40 
conjD1: "A \<and> B \<Longrightarrow> A" and


41 
conjD2: "A \<and> B \<Longrightarrow> B" and

12369

42 

21939

43 
disjE [elim]: "A \<or> B \<Longrightarrow> (A \<Longrightarrow> C) \<Longrightarrow> (B \<Longrightarrow> C) \<Longrightarrow> C" and


44 
disjI1 [intro]: "A \<Longrightarrow> A \<or> B" and

12369

45 
disjI2 [intro]: "B \<Longrightarrow> A \<or> B"


46 

21939

47 
theorem conjE [elim]:


48 
assumes "A \<and> B"


49 
obtains A and B


50 
proof


51 
from `A \<and> B` show A by (rule conjD1)


52 
from `A \<and> B` show B by (rule conjD2)

12369

53 
qed


54 

21939

55 
definition


56 
true :: o ("\<top>") where

12369

57 
"\<top> \<equiv> \<bottom> \<longrightarrow> \<bottom>"

21939

58 


59 
definition


60 
not :: "o \<Rightarrow> o" ("\<not> _" [40] 40) where

12369

61 
"\<not> A \<equiv> A \<longrightarrow> \<bottom>"

21939

62 


63 
definition


64 
iff :: "o \<Rightarrow> o \<Rightarrow> o" (infixr "\<longleftrightarrow>" 25) where

12392

65 
"A \<longleftrightarrow> B \<equiv> (A \<longrightarrow> B) \<and> (B \<longrightarrow> A)"


66 

12369

67 


68 
theorem trueI [intro]: \<top>


69 
proof (unfold true_def)


70 
show "\<bottom> \<longrightarrow> \<bottom>" ..


71 
qed


72 


73 
theorem notI [intro]: "(A \<Longrightarrow> \<bottom>) \<Longrightarrow> \<not> A"


74 
proof (unfold not_def)


75 
assume "A \<Longrightarrow> \<bottom>"

21939

76 
then show "A \<longrightarrow> \<bottom>" ..

12369

77 
qed


78 


79 
theorem notE [elim]: "\<not> A \<Longrightarrow> A \<Longrightarrow> B"


80 
proof (unfold not_def)


81 
assume "A \<longrightarrow> \<bottom>" and A

21939

82 
then have \<bottom> .. then show B ..

12369

83 
qed


84 

12392

85 
theorem iffI [intro]: "(A \<Longrightarrow> B) \<Longrightarrow> (B \<Longrightarrow> A) \<Longrightarrow> A \<longleftrightarrow> B"


86 
proof (unfold iff_def)

21939

87 
assume "A \<Longrightarrow> B" then have "A \<longrightarrow> B" ..


88 
moreover assume "B \<Longrightarrow> A" then have "B \<longrightarrow> A" ..

12392

89 
ultimately show "(A \<longrightarrow> B) \<and> (B \<longrightarrow> A)" ..


90 
qed


91 


92 
theorem iff1 [elim]: "A \<longleftrightarrow> B \<Longrightarrow> A \<Longrightarrow> B"


93 
proof (unfold iff_def)


94 
assume "(A \<longrightarrow> B) \<and> (B \<longrightarrow> A)"

21939

95 
then have "A \<longrightarrow> B" ..


96 
then show "A \<Longrightarrow> B" ..

12392

97 
qed


98 


99 
theorem iff2 [elim]: "A \<longleftrightarrow> B \<Longrightarrow> B \<Longrightarrow> A"


100 
proof (unfold iff_def)


101 
assume "(A \<longrightarrow> B) \<and> (B \<longrightarrow> A)"

21939

102 
then have "B \<longrightarrow> A" ..


103 
then show "B \<Longrightarrow> A" ..

12392

104 
qed


105 

12369

106 


107 
subsection {* Equality *}


108 

21939

109 
axiomatization


110 
equal :: "i \<Rightarrow> i \<Rightarrow> o" (infixl "=" 50)


111 
where


112 
refl [intro]: "x = x" and

12369

113 
subst: "x = y \<Longrightarrow> P(x) \<Longrightarrow> P(y)"


114 


115 
theorem trans [trans]: "x = y \<Longrightarrow> y = z \<Longrightarrow> x = z"


116 
by (rule subst)


117 


118 
theorem sym [sym]: "x = y \<Longrightarrow> y = x"


119 
proof 


120 
assume "x = y"


121 
from this and refl show "y = x" by (rule subst)


122 
qed


123 


124 


125 
subsection {* Quantifiers *}


126 

21939

127 
axiomatization


128 
All :: "(i \<Rightarrow> o) \<Rightarrow> o" (binder "\<forall>" 10) and


129 
Ex :: "(i \<Rightarrow> o) \<Rightarrow> o" (binder "\<exists>" 10)


130 
where


131 
allI [intro]: "(\<And>x. P(x)) \<Longrightarrow> \<forall>x. P(x)" and


132 
allD [dest]: "\<forall>x. P(x) \<Longrightarrow> P(a)" and


133 
exI [intro]: "P(a) \<Longrightarrow> \<exists>x. P(x)" and

12369

134 
exE [elim]: "\<exists>x. P(x) \<Longrightarrow> (\<And>x. P(x) \<Longrightarrow> C) \<Longrightarrow> C"


135 


136 


137 
lemma "(\<exists>x. P(f(x))) \<longrightarrow> (\<exists>y. P(y))"


138 
proof


139 
assume "\<exists>x. P(f(x))"

21939

140 
then show "\<exists>y. P(y)"

12369

141 
proof


142 
fix x assume "P(f(x))"

21939

143 
then show ?thesis ..

12369

144 
qed


145 
qed


146 


147 
lemma "(\<exists>x. \<forall>y. R(x, y)) \<longrightarrow> (\<forall>y. \<exists>x. R(x, y))"


148 
proof


149 
assume "\<exists>x. \<forall>y. R(x, y)"

21939

150 
then show "\<forall>y. \<exists>x. R(x, y)"

12369

151 
proof


152 
fix x assume a: "\<forall>y. R(x, y)"


153 
show ?thesis


154 
proof


155 
fix y from a have "R(x, y)" ..

21939

156 
then show "\<exists>x. R(x, y)" ..

12369

157 
qed


158 
qed


159 
qed


160 


161 
end
