1 (* Title: FOL/ex/First_Order_Logic.thy |
1 (* Title: FOL/ex/First_Order_Logic.thy |
2 Author: Markus Wenzel, TU Munich |
2 Author: Makarius |
3 *) |
3 *) |
4 |
4 |
5 section \<open>A simple formulation of First-Order Logic\<close> |
5 section \<open>A simple formulation of First-Order Logic\<close> |
6 |
6 |
7 theory First_Order_Logic imports Pure begin |
|
8 |
|
9 text \<open> |
7 text \<open> |
10 The subsequent theory development illustrates single-sorted |
8 The subsequent theory development illustrates single-sorted intuitionistic |
11 intuitionistic first-order logic with equality, formulated within |
9 first-order logic with equality, formulated within the Pure framework. So |
12 the Pure framework. Actually this is not an example of |
10 this is strictly speaking an example of Isabelle/Pure, not Isabelle/FOL. |
13 Isabelle/FOL, but of Isabelle/Pure. |
|
14 \<close> |
11 \<close> |
15 |
12 |
16 subsection \<open>Syntax\<close> |
13 theory First_Order_Logic |
|
14 imports Pure |
|
15 begin |
|
16 |
|
17 subsection \<open>Abstract syntax\<close> |
17 |
18 |
18 typedecl i |
19 typedecl i |
19 typedecl o |
20 typedecl o |
20 |
21 |
21 judgment |
22 judgment Trueprop :: "o \<Rightarrow> prop" ("_" 5) |
22 Trueprop :: "o \<Rightarrow> prop" ("_" 5) |
|
23 |
23 |
24 |
24 |
25 subsection \<open>Propositional logic\<close> |
25 subsection \<open>Propositional logic\<close> |
26 |
26 |
27 axiomatization |
27 axiomatization false :: o ("\<bottom>") |
28 false :: o ("\<bottom>") and |
28 where falseE [elim]: "\<bottom> \<Longrightarrow> A" |
29 imp :: "o \<Rightarrow> o \<Rightarrow> o" (infixr "\<longrightarrow>" 25) and |
|
30 conj :: "o \<Rightarrow> o \<Rightarrow> o" (infixr "\<and>" 35) and |
|
31 disj :: "o \<Rightarrow> o \<Rightarrow> o" (infixr "\<or>" 30) |
|
32 where |
|
33 falseE [elim]: "\<bottom> \<Longrightarrow> A" and |
|
34 |
29 |
35 impI [intro]: "(A \<Longrightarrow> B) \<Longrightarrow> A \<longrightarrow> B" and |
|
36 mp [dest]: "A \<longrightarrow> B \<Longrightarrow> A \<Longrightarrow> B" and |
|
37 |
30 |
38 conjI [intro]: "A \<Longrightarrow> B \<Longrightarrow> A \<and> B" and |
31 axiomatization imp :: "o \<Rightarrow> o \<Rightarrow> o" (infixr "\<longrightarrow>" 25) |
39 conjD1: "A \<and> B \<Longrightarrow> A" and |
32 where impI [intro]: "(A \<Longrightarrow> B) \<Longrightarrow> A \<longrightarrow> B" |
40 conjD2: "A \<and> B \<Longrightarrow> B" and |
33 and mp [dest]: "A \<longrightarrow> B \<Longrightarrow> A \<Longrightarrow> B" |
41 |
34 |
42 disjE [elim]: "A \<or> B \<Longrightarrow> (A \<Longrightarrow> C) \<Longrightarrow> (B \<Longrightarrow> C) \<Longrightarrow> C" and |
35 |
43 disjI1 [intro]: "A \<Longrightarrow> A \<or> B" and |
36 axiomatization conj :: "o \<Rightarrow> o \<Rightarrow> o" (infixr "\<and>" 35) |
44 disjI2 [intro]: "B \<Longrightarrow> A \<or> B" |
37 where conjI [intro]: "A \<Longrightarrow> B \<Longrightarrow> A \<and> B" |
|
38 and conjD1: "A \<and> B \<Longrightarrow> A" |
|
39 and conjD2: "A \<and> B \<Longrightarrow> B" |
45 |
40 |
46 theorem conjE [elim]: |
41 theorem conjE [elim]: |
47 assumes "A \<and> B" |
42 assumes "A \<and> B" |
48 obtains A and B |
43 obtains A and B |
49 proof |
44 proof |
50 from \<open>A \<and> B\<close> show A by (rule conjD1) |
45 from \<open>A \<and> B\<close> show A |
51 from \<open>A \<and> B\<close> show B by (rule conjD2) |
46 by (rule conjD1) |
|
47 from \<open>A \<and> B\<close> show B |
|
48 by (rule conjD2) |
52 qed |
49 qed |
|
50 |
|
51 |
|
52 axiomatization disj :: "o \<Rightarrow> o \<Rightarrow> o" (infixr "\<or>" 30) |
|
53 where disjE [elim]: "A \<or> B \<Longrightarrow> (A \<Longrightarrow> C) \<Longrightarrow> (B \<Longrightarrow> C) \<Longrightarrow> C" |
|
54 and disjI1 [intro]: "A \<Longrightarrow> A \<or> B" |
|
55 and disjI2 [intro]: "B \<Longrightarrow> A \<or> B" |
|
56 |
53 |
57 |
54 definition true :: o ("\<top>") |
58 definition true :: o ("\<top>") |
55 where "\<top> \<equiv> \<bottom> \<longrightarrow> \<bottom>" |
59 where "\<top> \<equiv> \<bottom> \<longrightarrow> \<bottom>" |
56 |
60 |
|
61 theorem trueI [intro]: \<top> |
|
62 unfolding true_def .. |
|
63 |
|
64 |
57 definition not :: "o \<Rightarrow> o" ("\<not> _" [40] 40) |
65 definition not :: "o \<Rightarrow> o" ("\<not> _" [40] 40) |
58 where "\<not> A \<equiv> A \<longrightarrow> \<bottom>" |
66 where "\<not> A \<equiv> A \<longrightarrow> \<bottom>" |
59 |
67 |
60 definition iff :: "o \<Rightarrow> o \<Rightarrow> o" (infixr "\<longleftrightarrow>" 25) |
|
61 where "A \<longleftrightarrow> B \<equiv> (A \<longrightarrow> B) \<and> (B \<longrightarrow> A)" |
|
62 |
|
63 |
|
64 theorem trueI [intro]: \<top> |
|
65 proof (unfold true_def) |
|
66 show "\<bottom> \<longrightarrow> \<bottom>" .. |
|
67 qed |
|
68 |
|
69 theorem notI [intro]: "(A \<Longrightarrow> \<bottom>) \<Longrightarrow> \<not> A" |
68 theorem notI [intro]: "(A \<Longrightarrow> \<bottom>) \<Longrightarrow> \<not> A" |
70 proof (unfold not_def) |
69 unfolding not_def .. |
71 assume "A \<Longrightarrow> \<bottom>" |
|
72 then show "A \<longrightarrow> \<bottom>" .. |
|
73 qed |
|
74 |
70 |
75 theorem notE [elim]: "\<not> A \<Longrightarrow> A \<Longrightarrow> B" |
71 theorem notE [elim]: "\<not> A \<Longrightarrow> A \<Longrightarrow> B" |
76 proof (unfold not_def) |
72 unfolding not_def |
|
73 proof - |
77 assume "A \<longrightarrow> \<bottom>" and A |
74 assume "A \<longrightarrow> \<bottom>" and A |
78 then have \<bottom> .. |
75 then have \<bottom> .. |
79 then show B .. |
76 then show B .. |
80 qed |
77 qed |
81 |
78 |
82 theorem iffI [intro]: "(A \<Longrightarrow> B) \<Longrightarrow> (B \<Longrightarrow> A) \<Longrightarrow> A \<longleftrightarrow> B" |
79 |
83 proof (unfold iff_def) |
80 definition iff :: "o \<Rightarrow> o \<Rightarrow> o" (infixr "\<longleftrightarrow>" 25) |
84 assume "A \<Longrightarrow> B" then have "A \<longrightarrow> B" .. |
81 where "A \<longleftrightarrow> B \<equiv> (A \<longrightarrow> B) \<and> (B \<longrightarrow> A)" |
85 moreover assume "B \<Longrightarrow> A" then have "B \<longrightarrow> A" .. |
82 |
86 ultimately show "(A \<longrightarrow> B) \<and> (B \<longrightarrow> A)" .. |
83 theorem iffI [intro]: |
|
84 assumes "A \<Longrightarrow> B" |
|
85 and "B \<Longrightarrow> A" |
|
86 shows "A \<longleftrightarrow> B" |
|
87 unfolding iff_def |
|
88 proof |
|
89 from \<open>A \<Longrightarrow> B\<close> show "A \<longrightarrow> B" .. |
|
90 from \<open>B \<Longrightarrow> A\<close> show "B \<longrightarrow> A" .. |
87 qed |
91 qed |
88 |
92 |
89 theorem iff1 [elim]: "A \<longleftrightarrow> B \<Longrightarrow> A \<Longrightarrow> B" |
93 theorem iff1 [elim]: |
90 proof (unfold iff_def) |
94 assumes "A \<longleftrightarrow> B" and A |
91 assume "(A \<longrightarrow> B) \<and> (B \<longrightarrow> A)" |
95 shows B |
|
96 proof - |
|
97 from \<open>A \<longleftrightarrow> B\<close> have "(A \<longrightarrow> B) \<and> (B \<longrightarrow> A)" |
|
98 unfolding iff_def . |
92 then have "A \<longrightarrow> B" .. |
99 then have "A \<longrightarrow> B" .. |
93 then show "A \<Longrightarrow> B" .. |
100 from this and \<open>A\<close> show B .. |
94 qed |
101 qed |
95 |
102 |
96 theorem iff2 [elim]: "A \<longleftrightarrow> B \<Longrightarrow> B \<Longrightarrow> A" |
103 theorem iff2 [elim]: |
97 proof (unfold iff_def) |
104 assumes "A \<longleftrightarrow> B" and B |
98 assume "(A \<longrightarrow> B) \<and> (B \<longrightarrow> A)" |
105 shows A |
|
106 proof - |
|
107 from \<open>A \<longleftrightarrow> B\<close> have "(A \<longrightarrow> B) \<and> (B \<longrightarrow> A)" |
|
108 unfolding iff_def . |
99 then have "B \<longrightarrow> A" .. |
109 then have "B \<longrightarrow> A" .. |
100 then show "B \<Longrightarrow> A" .. |
110 from this and \<open>B\<close> show A .. |
101 qed |
111 qed |
102 |
112 |
103 |
113 |
104 subsection \<open>Equality\<close> |
114 subsection \<open>Equality\<close> |
105 |
115 |
106 axiomatization |
116 axiomatization equal :: "i \<Rightarrow> i \<Rightarrow> o" (infixl "=" 50) |
107 equal :: "i \<Rightarrow> i \<Rightarrow> o" (infixl "=" 50) |
117 where refl [intro]: "x = x" |
108 where |
118 and subst: "x = y \<Longrightarrow> P x \<Longrightarrow> P y" |
109 refl [intro]: "x = x" and |
|
110 subst: "x = y \<Longrightarrow> P x \<Longrightarrow> P y" |
|
111 |
119 |
112 theorem trans [trans]: "x = y \<Longrightarrow> y = z \<Longrightarrow> x = z" |
120 theorem trans [trans]: "x = y \<Longrightarrow> y = z \<Longrightarrow> x = z" |
113 by (rule subst) |
121 by (rule subst) |
114 |
122 |
115 theorem sym [sym]: "x = y \<Longrightarrow> y = x" |
123 theorem sym [sym]: "x = y \<Longrightarrow> y = x" |
116 proof - |
124 proof - |
117 assume "x = y" |
125 assume "x = y" |
118 from this and refl show "y = x" by (rule subst) |
126 from this and refl show "y = x" |
|
127 by (rule subst) |
119 qed |
128 qed |
120 |
129 |
121 |
130 |
122 subsection \<open>Quantifiers\<close> |
131 subsection \<open>Quantifiers\<close> |
123 |
132 |
124 axiomatization |
133 axiomatization All :: "(i \<Rightarrow> o) \<Rightarrow> o" (binder "\<forall>" 10) |
125 All :: "(i \<Rightarrow> o) \<Rightarrow> o" (binder "\<forall>" 10) and |
134 where allI [intro]: "(\<And>x. P x) \<Longrightarrow> \<forall>x. P x" |
126 Ex :: "(i \<Rightarrow> o) \<Rightarrow> o" (binder "\<exists>" 10) |
135 and allD [dest]: "\<forall>x. P x \<Longrightarrow> P a" |
127 where |
136 |
128 allI [intro]: "(\<And>x. P x) \<Longrightarrow> \<forall>x. P x" and |
137 axiomatization Ex :: "(i \<Rightarrow> o) \<Rightarrow> o" (binder "\<exists>" 10) |
129 allD [dest]: "\<forall>x. P x \<Longrightarrow> P a" and |
138 where exI [intro]: "P a \<Longrightarrow> \<exists>x. P x" |
130 exI [intro]: "P a \<Longrightarrow> \<exists>x. P x" and |
139 and exE [elim]: "\<exists>x. P x \<Longrightarrow> (\<And>x. P x \<Longrightarrow> C) \<Longrightarrow> C" |
131 exE [elim]: "\<exists>x. P x \<Longrightarrow> (\<And>x. P x \<Longrightarrow> C) \<Longrightarrow> C" |
|
132 |
140 |
133 |
141 |
134 lemma "(\<exists>x. P (f x)) \<longrightarrow> (\<exists>y. P y)" |
142 lemma "(\<exists>x. P (f x)) \<longrightarrow> (\<exists>y. P y)" |
135 proof |
143 proof |
136 assume "\<exists>x. P (f x)" |
144 assume "\<exists>x. P (f x)" |
137 then show "\<exists>y. P y" |
145 then obtain x where "P (f x)" .. |
138 proof |
146 then show "\<exists>y. P y" .. |
139 fix x assume "P (f x)" |
|
140 then show ?thesis .. |
|
141 qed |
|
142 qed |
147 qed |
143 |
148 |
144 lemma "(\<exists>x. \<forall>y. R x y) \<longrightarrow> (\<forall>y. \<exists>x. R x y)" |
149 lemma "(\<exists>x. \<forall>y. R x y) \<longrightarrow> (\<forall>y. \<exists>x. R x y)" |
145 proof |
150 proof |
146 assume "\<exists>x. \<forall>y. R x y" |
151 assume "\<exists>x. \<forall>y. R x y" |
147 then show "\<forall>y. \<exists>x. R x y" |
152 then obtain x where "\<forall>y. R x y" .. |
|
153 show "\<forall>y. \<exists>x. R x y" |
148 proof |
154 proof |
149 fix x assume a: "\<forall>y. R x y" |
155 fix y |
150 show ?thesis |
156 from \<open>\<forall>y. R x y\<close> have "R x y" .. |
151 proof |
157 then show "\<exists>x. R x y" .. |
152 fix y from a have "R x y" .. |
|
153 then show "\<exists>x. R x y" .. |
|
154 qed |
|
155 qed |
158 qed |
156 qed |
159 qed |
157 |
160 |
158 end |
161 end |