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 


28 
consts


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


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


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


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


33 


34 
axioms


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


36 


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


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


39 


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


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


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


43 


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


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


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


47 


48 
theorem conjE [elim]: "A \<and> B \<Longrightarrow> (A \<Longrightarrow> B \<Longrightarrow> C) \<Longrightarrow> C"


49 
proof 


50 
assume ab: "A \<and> B"


51 
assume r: "A \<Longrightarrow> B \<Longrightarrow> C"


52 
show C


53 
proof (rule r)


54 
from ab show A by (rule conjD1)


55 
from ab show B by (rule conjD2)


56 
qed


57 
qed


58 


59 
constdefs


60 
true :: o ("\<top>")


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


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


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

12392

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


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>"


76 
thus "A \<longrightarrow> \<bottom>" ..


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


82 
hence \<bottom> .. thus B ..


83 
qed


84 

12392

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


86 
proof (unfold iff_def)


87 
assume "A \<Longrightarrow> B" hence "A \<longrightarrow> B" ..


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


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)"


95 
hence "A \<longrightarrow> B" ..


96 
thus "A \<Longrightarrow> B" ..


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)"


102 
hence "B \<longrightarrow> A" ..


103 
thus "B \<Longrightarrow> A" ..


104 
qed


105 

12369

106 


107 
subsection {* Equality *}


108 


109 
consts


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


111 


112 
axioms


113 
refl [intro]: "x = x"


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


115 


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


117 
by (rule subst)


118 


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


120 
proof 


121 
assume "x = y"


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


123 
qed


124 


125 


126 
subsection {* Quantifiers *}


127 


128 
consts


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


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


131 


132 
axioms


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


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


135 


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


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


138 


139 


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


141 
proof


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


143 
thus "\<exists>y. P(y)"


144 
proof


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


146 
thus ?thesis ..


147 
qed


148 
qed


149 


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


151 
proof


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


153 
thus "\<forall>y. \<exists>x. R(x, y)"


154 
proof


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


156 
show ?thesis


157 
proof


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


159 
thus "\<exists>x. R(x, y)" ..


160 
qed


161 
qed


162 
qed


163 


164 
end
