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