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