1open HolKernel Parse boolLib bossLib;
2
3open pred_setTheory set_relationTheory
4open folPrenexTheory folModelsTheory folLangTheory
5
6val _ = new_theory "folProp";
7
8(* ========================================================================= *)
9(* Propositional logic as subsystem of FOL, leading to compactness.          *)
10(* ========================================================================= *)
11
12Definition pholds_def:
13  (pholds v False ��� F) ���
14  (pholds v (Pred p l) ��� v (Pred p l)) ���
15  (pholds v (IMP p q) ��� (pholds v p ��� pholds v q)) ���
16  (pholds v (FALL x p) ��� v (FALL x p))
17End
18
19Theorem PHOLDS[simp]:
20  (pholds v False ��� F) ���
21  (pholds v True ��� T) ���
22  (pholds v (Pred pnm l) ��� v (Pred pnm l)) ���
23  (pholds v (Not q) ��� ��pholds v q) ���
24  (pholds v (Or p q) ��� pholds v p ��� pholds v q) ���
25  (pholds v (And p q) ��� pholds v p ��� pholds v q) ���
26  (pholds v (Iff p q) ��� (pholds v p ��� pholds v q)) ���
27  (pholds v (IMP p q) ��� (pholds v p ��� pholds v q)) ���
28  (pholds v (Exists x p) ��� ��v (FALL x (Not p))) ���
29  (pholds v (FALL x p) ��� v (FALL x p))
30Proof
31  simp[pholds_def, Or_def, Not_def, Iff_def, And_def, Exists_def, True_def] >>
32  metis_tac[]
33QED
34
35(* ------------------------------------------------------------------------- *)
36(* Propositional satisfaction.                                               *)
37(* ------------------------------------------------------------------------- *)
38
39val _ = set_fixity "psatisfies" (Infix(NONASSOC, 450))
40
41Definition psatisfies_def:
42  v psatisfies s ��� ���p. p ��� s ��� pholds v p
43End
44
45Definition psatisfiable_def:
46  psatisfiable s ��� ���v. v psatisfies s
47End
48
49Theorem psatisfiable_mono:
50  psatisfiable a ��� b ��� a ��� psatisfiable b
51Proof
52  simp[psatisfiable_def, psatisfies_def, SUBSET_DEF] >> metis_tac[]
53QED
54
55(* ------------------------------------------------------------------------- *)
56(* Extensibility of finitely satisfiable set.                                *)
57(* ------------------------------------------------------------------------- *)
58
59Definition finsat_def:
60  finsat a ��� ���b. b ��� a ��� FINITE b ��� psatisfiable b
61End
62
63Theorem finsat_mono:
64  finsat a ��� b ��� a ��� finsat b
65Proof
66  simp[finsat_def, SUBSET_DEF]
67QED
68
69Theorem satisfiable_finsat:
70  psatisfiable s ��� finsat s
71Proof
72  rw[finsat_def] >> metis_tac[psatisfiable_mono]
73QED
74
75Theorem IN_UNCURRY:
76  x IN UNCURRY f ��� UNCURRY f x
77Proof
78  simp[IN_DEF]
79QED
80
81(* uses Zorn's Lemma *)
82Theorem FINSAT_MAX:
83  finsat a ��� ���b. a ��� b ��� finsat b ��� ���c. b ��� c ��� finsat c ��� c = b
84Proof
85  strip_tac >>
86  qspecl_then [�����(b,c). a ��� b ��� b ��� c ��� finsat c���,
87               ���{ b | a ��� b ��� finsat b}���] mp_tac
88    zorns_lemma >>
89  impl_tac
90  >- (rw[]
91      >- (rw[EXTENSION] >> metis_tac[SUBSET_REFL] (* set is nonempty *))
92      >- ((* subset is a partial order *)
93          simp[partial_order_def, domain_def, range_def, transitive_def,
94               antisym_def, reflexive_def, IN_UNCURRY] >> rw[]
95          >- (simp[Once SUBSET_DEF, PULL_EXISTS] >> metis_tac[finsat_mono])
96          >- (simp[Once SUBSET_DEF, PULL_EXISTS] >> metis_tac[SUBSET_TRANS])
97          >- metis_tac[SUBSET_TRANS]
98          >- metis_tac[SUBSET_ANTISYM])
99      >- ((* upper bounds of chain t *)
100          rename [���chain t _���, ���upper_bounds t _ ��� ������] >>
101          fs[chain_def, upper_bounds_def, IN_UNCURRY, range_def, EXTENSION] >>
102          Cases_on ���t = ������ >> simp[]
103          >- (ntac 2 (qexists_tac ���a���) >> simp[]) >> fs[EXTENSION] >>
104          qexists_tac ���BIGUNION t��� >> simp[] >>
105          ������b. FINITE b ��� b ��� BIGUNION t ��� ���U. U ��� t ��� b ��� U���
106             by (Induct_on ���FINITE��� >> simp[] >> conj_tac >- metis_tac[] >>
107                 rw[] >> fs[] >>
108                 rename [���b ��� BIGUNION chn���, ���e ��� b���, ���e ��� s1���, ���s1 ��� chn���,
109                         ���b ��� s2���, ���s2 ��� chn���] >>
110                 ���s1 ��� s2 ��� s2 ��� s1��� by metis_tac[]
111                 >- (qexists_tac���s2��� >> metis_tac[SUBSET_DEF]) >>
112                 qexists_tac���s1��� >> metis_tac[SUBSET_TRANS]) >>
113          ���finsat (BIGUNION t)���
114             by (simp[finsat_def] >> rw[] >>
115                 first_x_assum
116                   (drule_all_then (qx_choose_then ���U��� strip_assume_tac)) >>
117                 metis_tac[finsat_def]) >>
118          simp[] >> metis_tac[SUBSET_BIGUNION_I])) >>
119  simp[maximal_elements_def, IN_UNCURRY] >> metis_tac[SUBSET_TRANS]
120QED
121
122(* ------------------------------------------------------------------------- *)
123(* Compactness.                                                              *)
124(* ------------------------------------------------------------------------- *)
125
126Theorem finsat_extend:
127  finsat b ��� ���p. finsat (p INSERT b) ��� finsat (Not p INSERT b)
128Proof
129  simp[finsat_def] >> strip_tac >> CCONTR_TAC >> fs[] >>
130  rename [���pos ��� p INSERT b���, ���neg ��� Not p INSERT b���] >>
131  ���p ��� b ��� Not p ��� b��� by metis_tac[ABSORPTION] >>
132  ���p ��� pos ��� Not p ��� neg��� by (fs[SUBSET_DEF] >> metis_tac[]) >>
133  qabbrev_tac ���big = (pos DELETE p) ��� (neg DELETE Not p)��� >>
134  ���big ��� b��� by (fs[SUBSET_DEF, Abbr���big���] >> metis_tac[]) >>
135  ���FINITE big��� by simp[Abbr���big���] >> ���psatisfiable big��� by metis_tac[] >>
136  ������v. v psatisfies big��� by metis_tac[psatisfiable_def] >>
137  ���pholds v p ��� pholds v (Not p)��� by simp[]
138  >- (���v psatisfies (p INSERT big)��� by fs[psatisfies_def, DISJ_IMP_THM] >>
139      ���v psatisfies pos���
140        by (fs[Abbr���big���, SUBSET_DEF, psatisfies_def] >> metis_tac[]) >>
141      metis_tac[psatisfiable_def])
142  >- (���v psatisfies (Not p INSERT big)��� by fs[psatisfies_def, DISJ_IMP_THM] >>
143      ���v psatisfies neg���
144        by (fs[Abbr���big���, SUBSET_DEF, psatisfies_def] >> metis_tac[]) >>
145      metis_tac[psatisfiable_def])
146QED
147
148Theorem finsat_max_complete:
149  finsat b ��� (���c. b ��� c ��� finsat c ��� c = b) ��� ���p. p ��� b ��� Not p ��� b
150Proof
151  rpt strip_tac >> drule_then strip_assume_tac finsat_extend >>
152  metis_tac[IN_INSERT, SUBSET_DEF, ABSORPTION]
153QED
154
155Theorem finsat_max_complete_strong:
156  finsat b ��� (���c. b ��� c ��� finsat c ��� c = b) ��� ���p. Not p ��� b ��� p ��� b
157Proof
158  rpt strip_tac >> reverse (Cases_on ���p ��� b���) >> simp[]
159  >- metis_tac[finsat_max_complete] >>
160  strip_tac >>
161  ���{p ; Not p} ��� b ��� FINITE {p ; Not p}��� by simp[SUBSET_DEF] >>
162  ���psatisfiable {p; Not p}��� by metis_tac[finsat_def] >>
163  fs[psatisfiable_def, psatisfies_def, DISJ_IMP_THM, FORALL_AND_THM]
164QED
165
166Theorem finsat_deduction:
167  finsat b ��� (���c. b ��� c ��� finsat c ��� c = b) ���
168  ���p. p ��� b ��� ���a. FINITE a ��� a ��� b ��� ���v. (���q. q ��� a ��� pholds v q) ��� pholds v p
169Proof
170  rpt strip_tac >> eq_tac
171  >- (strip_tac >> qexists_tac ���{p}��� >> simp[SUBSET_DEF]) >>
172  strip_tac >> CCONTR_TAC >>
173  drule_all_then (strip_assume_tac o GSYM) finsat_max_complete_strong >>
174  fs[] >>
175  ���FINITE (Not p INSERT a) ��� Not p INSERT a ��� b��� by simp[SUBSET_DEF] >>
176  ���psatisfiable (Not p INSERT a)��� by metis_tac[finsat_def] >>
177  fs[psatisfiable_def, psatisfies_def, DISJ_IMP_THM, FORALL_AND_THM] >>
178  metis_tac[]
179QED
180
181Theorem finsat_consistent:
182  finsat b ��� False ��� b
183Proof
184  simp[finsat_def, psatisfiable_def, psatisfies_def] >> rpt strip_tac >>
185  first_x_assum (qspec_then ���{False}��� mp_tac) >> simp[]
186QED
187
188Theorem finsat_max_homo:
189  finsat b ��� (���c. b ��� c ��� finsat c ��� c = b) ���
190  ���p q. IMP p q ��� b ��� p ��� b ��� q ��� b
191Proof
192  rpt strip_tac >> eq_tac
193  >- (drule_all_then (rewrite_tac o Portable.single) finsat_deduction >>
194      simp[] >> disch_then (qx_choose_then ���A1��� strip_assume_tac) >>
195      disch_then (qx_choose_then ���A2��� strip_assume_tac) >>
196      qexists_tac ���A1 ��� A2��� >> simp[]) >>
197  CONV_TAC(LAND_CONV (REWR_CONV (DECIDE ���p ��� q ��� ~p ��� q���))) >>
198  drule_all_then (rewrite_tac o Portable.single o GSYM)
199    finsat_max_complete_strong >>
200  drule_all_then (rewrite_tac o Portable.single) finsat_deduction >> simp[] >>
201  disch_then (DISJ_CASES_THEN (qx_choose_then ���A��� strip_assume_tac)) >>
202  qexists_tac ���A��� >> simp[]
203QED
204
205Theorem COMPACT_PROP:
206  (���b. FINITE b ��� b ��� a ��� ���v. ���r. r ��� b ��� pholds v r) ���
207  ���v. ���r. r ��� a ��� pholds v r
208Proof
209  strip_tac >>
210  ���finsat a��� by metis_tac[finsat_def, psatisfies_def, psatisfiable_def] >>
211  drule_then (qx_choose_then ���B��� strip_assume_tac) FINSAT_MAX >>
212  qexists_tac �����p. p ��� B��� >>
213  ������r. pholds (��p. p ��� B) r ��� r ��� B��� suffices_by metis_tac[SUBSET_DEF] >>
214  Induct >> simp[finsat_consistent, finsat_max_homo]
215QED
216
217Theorem compact_finsat:
218  psatisfiable a ��� finsat a
219Proof
220  eq_tac >- (simp[finsat_def] >> metis_tac[psatisfiable_mono]) >>
221  simp[finsat_def, psatisfiable_def, psatisfies_def] >>
222  metis_tac[COMPACT_PROP]
223QED
224
225(* ------------------------------------------------------------------------- *)
226(* Important variant used in proving Uniformity for FOL.                     *)
227(* ------------------------------------------------------------------------- *)
228
229Theorem COMPACT_PROP_ALT:
230  ���a. (���v. ���p. p ��� a ��� pholds v p) ���
231      ���b. FINITE b ��� b ��� a ��� ���v. ���p. p ��� b ��� pholds v p
232Proof
233  rpt strip_tac >>
234  Q.SUBGOAL_THEN �����(���v. ���r. r ��� { Not q | q ��� a } ��� pholds v r)��� MP_TAC
235    >- simp[PULL_EXISTS] >>
236  disch_then (mp_tac o
237              MATCH_MP (GEN_ALL (CONV_RULE CONTRAPOS_CONV COMPACT_PROP))) >>
238  simp[] >>
239  disch_then (qx_choose_then ���b��� strip_assume_tac) >>
240  qexists_tac ���{ p | Not p ��� b}��� >> simp[] >> rpt conj_tac
241  >- (���IMAGE Not {p | Not p ��� b} ��� b��� by simp[SUBSET_DEF, PULL_EXISTS] >>
242      ���FINITE (IMAGE Not {p | Not p ��� b})��� by metis_tac[SUBSET_FINITE] >>
243      fs[INJECTIVE_IMAGE_FINITE])
244  >- (fs[SUBSET_DEF] >> rw[] >> res_tac >> fs[]) >>
245  fs[SUBSET_DEF] >> qx_gen_tac ���v��� >>
246  pop_assum (qspec_then ���v��� (qx_choose_then �������� strip_assume_tac)) >>
247  first_x_assum drule >> simp[PULL_EXISTS] >> rw[] >> fs[] >> metis_tac[]
248QED
249
250Theorem FINITE_DISJ_lemma:
251  ���a. FINITE a ���
252      ���ps. EVERY (��p. p ��� a) ps ���
253           ���v. pholds v (FOLDR Or False ps) ���
254               ���p. p ��� a ��� pholds v p
255Proof
256  Induct_on ���FINITE��� >> simp[] >> rw[] >>
257  rename [���p ��� a���, ���EVERY _ ps���]  >> qexists_tac ���p::ps��� >>
258  dsimp[] >> irule listTheory.MONO_EVERY >> qexists_tac �����p. p ��� a��� >>
259  simp[]
260QED
261
262Theorem COMPACT_DISJ:
263  ���a. (���v. ���p. p ��� a ��� pholds v p) ���
264      ���ps. EVERY (��p. p ��� a) ps ��� ���v. pholds v (FOLDR Or False ps)
265Proof
266  rw[] >>
267  drule_then (qx_choose_then ���b��� strip_assume_tac) COMPACT_PROP_ALT >>
268  drule_then (qx_choose_then ���ps��� strip_assume_tac) FINITE_DISJ_lemma >>
269  qexists_tac ���ps��� >> simp[] >> irule listTheory.MONO_EVERY >>
270  qexists_tac �����p. p ��� b��� >> fs[SUBSET_DEF]
271QED
272
273val _ = export_theory()
274