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