12560
|
1 |
(* Title: ZF/Induct/PropLog.thy
|
12088
|
2 |
ID: $Id$
|
|
3 |
Author: Tobias Nipkow & Lawrence C Paulson
|
|
4 |
Copyright 1993 University of Cambridge
|
12610
|
5 |
*)
|
12560
|
6 |
|
12610
|
7 |
header {* Meta-theory of propositional logic *}
|
12088
|
8 |
|
16417
|
9 |
theory PropLog imports Main begin
|
12088
|
10 |
|
12610
|
11 |
text {*
|
|
12 |
Datatype definition of propositional logic formulae and inductive
|
|
13 |
definition of the propositional tautologies.
|
|
14 |
|
|
15 |
Inductive definition of propositional logic. Soundness and
|
|
16 |
completeness w.r.t.\ truth-tables.
|
12088
|
17 |
|
12610
|
18 |
Prove: If @{text "H |= p"} then @{text "G |= p"} where @{text "G \<in>
|
|
19 |
Fin(H)"}
|
|
20 |
*}
|
|
21 |
|
|
22 |
|
|
23 |
subsection {* The datatype of propositions *}
|
12088
|
24 |
|
|
25 |
consts
|
12610
|
26 |
propn :: i
|
12088
|
27 |
|
12610
|
28 |
datatype propn =
|
|
29 |
Fls
|
|
30 |
| Var ("n \<in> nat") ("#_" [100] 100)
|
|
31 |
| Imp ("p \<in> propn", "q \<in> propn") (infixr "=>" 90)
|
|
32 |
|
12088
|
33 |
|
12610
|
34 |
subsection {* The proof system *}
|
|
35 |
|
|
36 |
consts thms :: "i => i"
|
|
37 |
syntax "_thms" :: "[i,i] => o" (infixl "|-" 50)
|
|
38 |
translations "H |- p" == "p \<in> thms(H)"
|
12088
|
39 |
|
|
40 |
inductive
|
12610
|
41 |
domains "thms(H)" \<subseteq> "propn"
|
12560
|
42 |
intros
|
|
43 |
H: "[| p \<in> H; p \<in> propn |] ==> H |- p"
|
|
44 |
K: "[| p \<in> propn; q \<in> propn |] ==> H |- p=>q=>p"
|
12610
|
45 |
S: "[| p \<in> propn; q \<in> propn; r \<in> propn |]
|
12560
|
46 |
==> H |- (p=>q=>r) => (p=>q) => p=>r"
|
|
47 |
DN: "p \<in> propn ==> H |- ((p=>Fls) => Fls) => p"
|
|
48 |
MP: "[| H |- p=>q; H |- p; p \<in> propn; q \<in> propn |] ==> H |- q"
|
|
49 |
type_intros "propn.intros"
|
12088
|
50 |
|
12560
|
51 |
declare propn.intros [simp]
|
|
52 |
|
12610
|
53 |
|
|
54 |
subsection {* The semantics *}
|
|
55 |
|
|
56 |
subsubsection {* Semantics of propositional logic. *}
|
12560
|
57 |
|
12610
|
58 |
consts
|
|
59 |
is_true_fun :: "[i,i] => i"
|
|
60 |
primrec
|
|
61 |
"is_true_fun(Fls, t) = 0"
|
|
62 |
"is_true_fun(Var(v), t) = (if v \<in> t then 1 else 0)"
|
|
63 |
"is_true_fun(p=>q, t) = (if is_true_fun(p,t) = 1 then is_true_fun(q,t) else 1)"
|
|
64 |
|
|
65 |
constdefs
|
|
66 |
is_true :: "[i,i] => o"
|
|
67 |
"is_true(p,t) == is_true_fun(p,t) = 1"
|
|
68 |
-- {* this definition is required since predicates can't be recursive *}
|
12560
|
69 |
|
|
70 |
lemma is_true_Fls [simp]: "is_true(Fls,t) <-> False"
|
12610
|
71 |
by (simp add: is_true_def)
|
12560
|
72 |
|
|
73 |
lemma is_true_Var [simp]: "is_true(#v,t) <-> v \<in> t"
|
12610
|
74 |
by (simp add: is_true_def)
|
12560
|
75 |
|
|
76 |
lemma is_true_Imp [simp]: "is_true(p=>q,t) <-> (is_true(p,t)-->is_true(q,t))"
|
12610
|
77 |
by (simp add: is_true_def)
|
|
78 |
|
|
79 |
|
|
80 |
subsubsection {* Logical consequence *}
|
|
81 |
|
|
82 |
text {*
|
|
83 |
For every valuation, if all elements of @{text H} are true then so
|
|
84 |
is @{text p}.
|
|
85 |
*}
|
|
86 |
|
|
87 |
constdefs
|
|
88 |
logcon :: "[i,i] => o" (infixl "|=" 50)
|
|
89 |
"H |= p == \<forall>t. (\<forall>q \<in> H. is_true(q,t)) --> is_true(p,t)"
|
12560
|
90 |
|
|
91 |
|
12610
|
92 |
text {*
|
|
93 |
A finite set of hypotheses from @{text t} and the @{text Var}s in
|
|
94 |
@{text p}.
|
|
95 |
*}
|
|
96 |
|
|
97 |
consts
|
|
98 |
hyps :: "[i,i] => i"
|
|
99 |
primrec
|
|
100 |
"hyps(Fls, t) = 0"
|
|
101 |
"hyps(Var(v), t) = (if v \<in> t then {#v} else {#v=>Fls})"
|
|
102 |
"hyps(p=>q, t) = hyps(p,t) \<union> hyps(q,t)"
|
|
103 |
|
|
104 |
|
|
105 |
|
|
106 |
subsection {* Proof theory of propositional logic *}
|
12560
|
107 |
|
|
108 |
lemma thms_mono: "G \<subseteq> H ==> thms(G) \<subseteq> thms(H)"
|
12610
|
109 |
apply (unfold thms.defs)
|
|
110 |
apply (rule lfp_mono)
|
|
111 |
apply (rule thms.bnd_mono)+
|
|
112 |
apply (assumption | rule univ_mono basic_monos)+
|
|
113 |
done
|
12560
|
114 |
|
|
115 |
lemmas thms_in_pl = thms.dom_subset [THEN subsetD]
|
|
116 |
|
|
117 |
inductive_cases ImpE: "p=>q \<in> propn"
|
|
118 |
|
|
119 |
lemma thms_MP: "[| H |- p=>q; H |- p |] ==> H |- q"
|
12610
|
120 |
-- {* Stronger Modus Ponens rule: no typechecking! *}
|
|
121 |
apply (rule thms.MP)
|
|
122 |
apply (erule asm_rl thms_in_pl thms_in_pl [THEN ImpE])+
|
|
123 |
done
|
12560
|
124 |
|
|
125 |
lemma thms_I: "p \<in> propn ==> H |- p=>p"
|
12610
|
126 |
-- {*Rule is called @{text I} for Identity Combinator, not for Introduction. *}
|
|
127 |
apply (rule thms.S [THEN thms_MP, THEN thms_MP])
|
|
128 |
apply (rule_tac [5] thms.K)
|
|
129 |
apply (rule_tac [4] thms.K)
|
|
130 |
apply simp_all
|
|
131 |
done
|
|
132 |
|
12560
|
133 |
|
12610
|
134 |
subsubsection {* Weakening, left and right *}
|
12560
|
135 |
|
12610
|
136 |
lemma weaken_left: "[| G \<subseteq> H; G|-p |] ==> H|-p"
|
|
137 |
-- {* Order of premises is convenient with @{text THEN} *}
|
|
138 |
by (erule thms_mono [THEN subsetD])
|
12560
|
139 |
|
12610
|
140 |
lemma weaken_left_cons: "H |- p ==> cons(a,H) |- p"
|
|
141 |
by (erule subset_consI [THEN weaken_left])
|
12560
|
142 |
|
|
143 |
lemmas weaken_left_Un1 = Un_upper1 [THEN weaken_left]
|
|
144 |
lemmas weaken_left_Un2 = Un_upper2 [THEN weaken_left]
|
|
145 |
|
|
146 |
lemma weaken_right: "[| H |- q; p \<in> propn |] ==> H |- p=>q"
|
12610
|
147 |
by (simp_all add: thms.K [THEN thms_MP] thms_in_pl)
|
12560
|
148 |
|
|
149 |
|
12610
|
150 |
subsubsection {* The deduction theorem *}
|
|
151 |
|
|
152 |
theorem deduction: "[| cons(p,H) |- q; p \<in> propn |] ==> H |- p=>q"
|
|
153 |
apply (erule thms.induct)
|
|
154 |
apply (blast intro: thms_I thms.H [THEN weaken_right])
|
|
155 |
apply (blast intro: thms.K [THEN weaken_right])
|
|
156 |
apply (blast intro: thms.S [THEN weaken_right])
|
|
157 |
apply (blast intro: thms.DN [THEN weaken_right])
|
|
158 |
apply (blast intro: thms.S [THEN thms_MP [THEN thms_MP]])
|
|
159 |
done
|
12560
|
160 |
|
|
161 |
|
12610
|
162 |
subsubsection {* The cut rule *}
|
|
163 |
|
12560
|
164 |
lemma cut: "[| H|-p; cons(p,H) |- q |] ==> H |- q"
|
12610
|
165 |
apply (rule deduction [THEN thms_MP])
|
|
166 |
apply (simp_all add: thms_in_pl)
|
|
167 |
done
|
12560
|
168 |
|
|
169 |
lemma thms_FlsE: "[| H |- Fls; p \<in> propn |] ==> H |- p"
|
12610
|
170 |
apply (rule thms.DN [THEN thms_MP])
|
|
171 |
apply (rule_tac [2] weaken_right)
|
|
172 |
apply (simp_all add: propn.intros)
|
|
173 |
done
|
12560
|
174 |
|
12610
|
175 |
lemma thms_notE: "[| H |- p=>Fls; H |- p; q \<in> propn |] ==> H |- q"
|
|
176 |
by (erule thms_MP [THEN thms_FlsE])
|
|
177 |
|
|
178 |
|
|
179 |
subsubsection {* Soundness of the rules wrt truth-table semantics *}
|
12560
|
180 |
|
12610
|
181 |
theorem soundness: "H |- p ==> H |= p"
|
|
182 |
apply (unfold logcon_def)
|
18415
|
183 |
apply (induct set: thms)
|
12610
|
184 |
apply auto
|
|
185 |
done
|
12560
|
186 |
|
12610
|
187 |
|
|
188 |
subsection {* Completeness *}
|
|
189 |
|
|
190 |
subsubsection {* Towards the completeness proof *}
|
12560
|
191 |
|
|
192 |
lemma Fls_Imp: "[| H |- p=>Fls; q \<in> propn |] ==> H |- p=>q"
|
12610
|
193 |
apply (frule thms_in_pl)
|
|
194 |
apply (rule deduction)
|
|
195 |
apply (rule weaken_left_cons [THEN thms_notE])
|
|
196 |
apply (blast intro: thms.H elim: ImpE)+
|
|
197 |
done
|
12560
|
198 |
|
|
199 |
lemma Imp_Fls: "[| H |- p; H |- q=>Fls |] ==> H |- (p=>q)=>Fls"
|
12610
|
200 |
apply (frule thms_in_pl)
|
|
201 |
apply (frule thms_in_pl [of concl: "q=>Fls"])
|
|
202 |
apply (rule deduction)
|
|
203 |
apply (erule weaken_left_cons [THEN thms_MP])
|
|
204 |
apply (rule consI1 [THEN thms.H, THEN thms_MP])
|
|
205 |
apply (blast intro: weaken_left_cons elim: ImpE)+
|
|
206 |
done
|
12560
|
207 |
|
|
208 |
lemma hyps_thms_if:
|
12610
|
209 |
"p \<in> propn ==> hyps(p,t) |- (if is_true(p,t) then p else p=>Fls)"
|
|
210 |
-- {* Typical example of strengthening the induction statement. *}
|
|
211 |
apply simp
|
|
212 |
apply (induct_tac p)
|
|
213 |
apply (simp_all add: thms_I thms.H)
|
|
214 |
apply (safe elim!: Fls_Imp [THEN weaken_left_Un1] Fls_Imp [THEN weaken_left_Un2])
|
|
215 |
apply (blast intro: weaken_left_Un1 weaken_left_Un2 weaken_right Imp_Fls)+
|
|
216 |
done
|
|
217 |
|
|
218 |
lemma logcon_thms_p: "[| p \<in> propn; 0 |= p |] ==> hyps(p,t) |- p"
|
|
219 |
-- {* Key lemma for completeness; yields a set of assumptions satisfying @{text p} *}
|
|
220 |
apply (drule hyps_thms_if)
|
|
221 |
apply (simp add: logcon_def)
|
|
222 |
done
|
|
223 |
|
|
224 |
text {*
|
|
225 |
For proving certain theorems in our new propositional logic.
|
|
226 |
*}
|
12560
|
227 |
|
12610
|
228 |
lemmas propn_SIs = propn.intros deduction
|
|
229 |
and propn_Is = thms_in_pl thms.H thms.H [THEN thms_MP]
|
|
230 |
|
|
231 |
text {*
|
|
232 |
The excluded middle in the form of an elimination rule.
|
|
233 |
*}
|
12560
|
234 |
|
12610
|
235 |
lemma thms_excluded_middle:
|
|
236 |
"[| p \<in> propn; q \<in> propn |] ==> H |- (p=>q) => ((p=>Fls)=>q) => q"
|
|
237 |
apply (rule deduction [THEN deduction])
|
|
238 |
apply (rule thms.DN [THEN thms_MP])
|
|
239 |
apply (best intro!: propn_SIs intro: propn_Is)+
|
|
240 |
done
|
12560
|
241 |
|
12610
|
242 |
lemma thms_excluded_middle_rule:
|
|
243 |
"[| cons(p,H) |- q; cons(p=>Fls,H) |- q; p \<in> propn |] ==> H |- q"
|
|
244 |
-- {* Hard to prove directly because it requires cuts *}
|
|
245 |
apply (rule thms_excluded_middle [THEN thms_MP, THEN thms_MP])
|
|
246 |
apply (blast intro!: propn_SIs intro: propn_Is)+
|
|
247 |
done
|
12560
|
248 |
|
|
249 |
|
12610
|
250 |
subsubsection {* Completeness -- lemmas for reducing the set of assumptions *}
|
12560
|
251 |
|
12610
|
252 |
text {*
|
|
253 |
For the case @{prop "hyps(p,t)-cons(#v,Y) |- p"} we also have @{prop
|
|
254 |
"hyps(p,t)-{#v} \<subseteq> hyps(p, t-{v})"}.
|
|
255 |
*}
|
12560
|
256 |
|
12610
|
257 |
lemma hyps_Diff:
|
|
258 |
"p \<in> propn ==> hyps(p, t-{v}) \<subseteq> cons(#v=>Fls, hyps(p,t)-{#v})"
|
18415
|
259 |
by (induct set: propn) auto
|
12560
|
260 |
|
12610
|
261 |
text {*
|
|
262 |
For the case @{prop "hyps(p,t)-cons(#v => Fls,Y) |- p"} we also have
|
|
263 |
@{prop "hyps(p,t)-{#v=>Fls} \<subseteq> hyps(p, cons(v,t))"}.
|
|
264 |
*}
|
12560
|
265 |
|
|
266 |
lemma hyps_cons:
|
12610
|
267 |
"p \<in> propn ==> hyps(p, cons(v,t)) \<subseteq> cons(#v, hyps(p,t)-{#v=>Fls})"
|
18415
|
268 |
by (induct set: propn) auto
|
12560
|
269 |
|
12610
|
270 |
text {* Two lemmas for use with @{text weaken_left} *}
|
12560
|
271 |
|
|
272 |
lemma cons_Diff_same: "B-C \<subseteq> cons(a, B-cons(a,C))"
|
12610
|
273 |
by blast
|
12560
|
274 |
|
|
275 |
lemma cons_Diff_subset2: "cons(a, B-{c}) - D \<subseteq> cons(a, B-cons(c,D))"
|
12610
|
276 |
by blast
|
12560
|
277 |
|
12610
|
278 |
text {*
|
|
279 |
The set @{term "hyps(p,t)"} is finite, and elements have the form
|
|
280 |
@{term "#v"} or @{term "#v=>Fls"}; could probably prove the stronger
|
|
281 |
@{prop "hyps(p,t) \<in> Fin(hyps(p,0) \<union> hyps(p,nat))"}.
|
|
282 |
*}
|
|
283 |
|
12560
|
284 |
lemma hyps_finite: "p \<in> propn ==> hyps(p,t) \<in> Fin(\<Union>v \<in> nat. {#v, #v=>Fls})"
|
18415
|
285 |
by (induct set: propn) auto
|
12560
|
286 |
|
|
287 |
lemmas Diff_weaken_left = Diff_mono [OF _ subset_refl, THEN weaken_left]
|
|
288 |
|
12610
|
289 |
text {*
|
|
290 |
Induction on the finite set of assumptions @{term "hyps(p,t0)"}. We
|
|
291 |
may repeatedly subtract assumptions until none are left!
|
|
292 |
*}
|
|
293 |
|
12560
|
294 |
lemma completeness_0_lemma [rule_format]:
|
|
295 |
"[| p \<in> propn; 0 |= p |] ==> \<forall>t. hyps(p,t) - hyps(p,t0) |- p"
|
12610
|
296 |
apply (frule hyps_finite)
|
|
297 |
apply (erule Fin_induct)
|
|
298 |
apply (simp add: logcon_thms_p Diff_0)
|
|
299 |
txt {* inductive step *}
|
|
300 |
apply safe
|
|
301 |
txt {* Case @{prop "hyps(p,t)-cons(#v,Y) |- p"} *}
|
|
302 |
apply (rule thms_excluded_middle_rule)
|
|
303 |
apply (erule_tac [3] propn.intros)
|
|
304 |
apply (blast intro: cons_Diff_same [THEN weaken_left])
|
|
305 |
apply (blast intro: cons_Diff_subset2 [THEN weaken_left]
|
|
306 |
hyps_Diff [THEN Diff_weaken_left])
|
|
307 |
txt {* Case @{prop "hyps(p,t)-cons(#v => Fls,Y) |- p"} *}
|
|
308 |
apply (rule thms_excluded_middle_rule)
|
|
309 |
apply (erule_tac [3] propn.intros)
|
|
310 |
apply (blast intro: cons_Diff_subset2 [THEN weaken_left]
|
|
311 |
hyps_cons [THEN Diff_weaken_left])
|
12560
|
312 |
apply (blast intro: cons_Diff_same [THEN weaken_left])
|
12610
|
313 |
done
|
|
314 |
|
|
315 |
|
|
316 |
subsubsection {* Completeness theorem *}
|
12560
|
317 |
|
|
318 |
lemma completeness_0: "[| p \<in> propn; 0 |= p |] ==> 0 |- p"
|
12610
|
319 |
-- {* The base case for completeness *}
|
|
320 |
apply (rule Diff_cancel [THEN subst])
|
|
321 |
apply (blast intro: completeness_0_lemma)
|
|
322 |
done
|
12560
|
323 |
|
|
324 |
lemma logcon_Imp: "[| cons(p,H) |= q |] ==> H |= p=>q"
|
12610
|
325 |
-- {* A semantic analogue of the Deduction Theorem *}
|
|
326 |
by (simp add: logcon_def)
|
12560
|
327 |
|
18415
|
328 |
lemma completeness:
|
|
329 |
"H \<in> Fin(propn) ==> p \<in> propn \<Longrightarrow> H |= p \<Longrightarrow> H |- p"
|
20503
|
330 |
apply (induct arbitrary: p set: Fin)
|
12610
|
331 |
apply (safe intro!: completeness_0)
|
|
332 |
apply (rule weaken_left_cons [THEN thms_MP])
|
|
333 |
apply (blast intro!: logcon_Imp propn.intros)
|
|
334 |
apply (blast intro: propn_Is)
|
|
335 |
done
|
12560
|
336 |
|
12610
|
337 |
theorem thms_iff: "H \<in> Fin(propn) ==> H |- p <-> H |= p \<and> p \<in> propn"
|
|
338 |
by (blast intro: soundness completeness thms_in_pl)
|
12560
|
339 |
|
12088
|
340 |
end
|