1open HolKernel Parse boolLib bossLib; 2 3open listTheory pred_setTheory 4open folLangTheory 5 6val _ = new_theory "folModels"; 7 8val MAP_CONG' = REWRITE_RULE [GSYM AND_IMP_INTRO] MAP_CONG 9 10val _ = Datatype��� 11 model = <| Dom : �� set ; Fun : num -> �� list -> �� ; 12 Pred : num -> �� list -> bool |> 13���; 14 15Definition valuation_def: 16 valuation M v ��� ���n. v n ��� M.Dom 17End 18 19Theorem upd_valuation[simp]: 20 valuation M v ��� a ��� M.Dom ��� valuation M v���x ��� a��� 21Proof 22 simp[valuation_def, combinTheory.APPLY_UPDATE_THM] >> rw[] >> rw[] 23QED 24 25Definition termval_def[simp]: 26 (termval M v (V x) = v x) ��� 27 (termval M v (Fn f l) = M.Fun f (MAP (termval M v) l)) 28Termination 29 WF_REL_TAC ���measure (term_size o SND o SND)��� >> simp[] 30End 31 32Definition holds_def: 33 (holds M v False ��� F) ��� 34 (holds M v (Pred a l) ��� M.Pred a (MAP (termval M v) l)) ��� 35 (holds M v (IMP f1 f2) ��� (holds M v f1 ��� holds M v f2)) ��� 36 (holds M v (FALL x f) ��� ���a. a ��� M.Dom ��� holds M v���x ��� a��� f) 37End 38 39Definition hold_def: 40 hold M v fms ��� ���p. p ��� fms ��� holds M v p 41End 42 43Definition satisfies_def: 44 (satisfies) M fms ��� ���v p. valuation M v ��� p ��� fms ��� holds M v p 45End 46 47val _ = set_fixity "satisfies" (Infix(NONASSOC, 450)) 48 49Theorem satisfies_SING[simp]: 50 M satisfies {p} ��� ���v. valuation M v ��� holds M v p 51Proof 52 simp[satisfies_def] 53QED 54 55Theorem HOLDS[simp]: 56 (holds M v False ��� F) ��� 57 (holds M v True ��� T) ��� 58 (holds M v (Pred a l) ��� M.Pred a (MAP (termval M v) l)) ��� 59 (holds M v (Not p) ��� ~holds M v p) ��� 60 (holds M v (Or p q) ��� holds M v p ��� holds M v q) ��� 61 (holds M v (And p q) ��� holds M v p ��� holds M v q) ��� 62 (holds M v (Iff p q) ��� (holds M v p ��� holds M v q)) ��� 63 (holds M v (IMP p q) ��� (holds M v p ��� holds M v q)) ��� 64 (holds M v (FALL x p) ��� ���a. a ��� M.Dom ��� holds M v���x ��� a��� p) ��� 65 (holds M v (Exists x p) ��� ���a. a ��� M.Dom ��� holds M v���x ��� a��� p) 66Proof 67 simp[holds_def, True_def, Not_def, Exists_def, Or_def, And_def, Iff_def] >> 68 metis_tac[] 69QED 70 71Theorem termval_valuation: 72 ���t M v1 v2. 73 (���x. x ��� FVT t ��� (v1 x = v2 x)) ��� 74 (termval M v1 t = termval M v2 t) 75Proof 76 ho_match_mp_tac term_induct >> simp[MEM_MAP, PULL_EXISTS] >> 77 rpt strip_tac >> AP_TERM_TAC >> 78 irule MAP_CONG >> simp[] >> rpt strip_tac >> first_x_assum irule >> 79 metis_tac[] 80QED 81 82Theorem holds_valuation: 83 ���M p v1 v2. 84 (���x. x ��� FV p ��� (v1 x = v2 x)) ��� 85 (holds M v1 p ��� holds M v2 p) 86Proof 87 Induct_on ���p��� >> simp[MEM_MAP, PULL_EXISTS] 88 >- (rpt strip_tac >> AP_TERM_TAC >> irule MAP_CONG >> simp[] >> 89 rpt strip_tac >> irule termval_valuation >> metis_tac[]) 90 >- metis_tac[] 91 >- (rpt strip_tac >> AP_TERM_TAC >> ABS_TAC >> AP_TERM_TAC >> 92 first_x_assum irule >> rpt strip_tac >> 93 rename [���var ��� FV fm���, ���_ ��� u ��� a ������] >> 94 Cases_on ���var = u��� >> simp[combinTheory.UPDATE_APPLY]) 95QED 96 97Definition interpretation_def: 98 interpretation (fns,preds : (num # num) set) M ��� 99 ���f l. (f, LENGTH l) ��� fns ��� (���x. MEM x l ��� x ��� M.Dom) ��� 100 M.Fun f l ��� M.Dom 101End 102 103Definition satisfiable_def: 104 satisfiable (:��) fms ��� 105 ���M:�� model. M.Dom ��� ��� ��� interpretation (language fms) M ��� M satisfies fms 106End 107 108Definition ffinsat_def: 109 ffinsat (:��) s ��� ���t. FINITE t ��� t ��� s ��� satisfiable (:��) t 110End 111 112Definition valid_def: 113 valid (:��) fms ��� 114 ���M:�� model. interpretation (language fms) M ��� M.Dom ��� ��� ��� M satisfies fms 115End 116 117Definition entails_def: 118 entails (:��) �� p ��� 119 ���M:�� model v. 120 valuation M v ��� 121 interpretation (language (p INSERT ��)) M ��� M.Dom ��� ��� ��� hold M v �� ��� 122 holds M v p 123End 124 125Definition equivalent_def: 126 equivalent (:��) p q ��� 127 ���M:�� model v. holds M v p ��� holds M v q 128End 129 130Theorem interpretation_termval: 131 ���t M v (preds:(num # num)set). 132 interpretation (term_functions t,preds) M ��� valuation M v ��� 133 termval M v t ��� M.Dom 134Proof 135 simp[interpretation_def] >> ho_match_mp_tac term_induct >> rpt strip_tac 136 >- fs[valuation_def] >> 137 fs[MEM_MAP, PULL_EXISTS] >> 138 first_assum irule >> simp[MEM_MAP, PULL_EXISTS] >> 139 rpt strip_tac >> first_x_assum irule >> simp[] >> rpt strip_tac >> 140 last_x_assum irule >> simp[] >> metis_tac[] 141QED 142 143Theorem interpretation_sublang: 144 fns2 ��� fns1 ��� interpretation (fns1,preds1) M ��� interpretation (fns2,preds2) M 145Proof 146 simp[SUBSET_DEF, interpretation_def] 147QED 148 149Theorem termsubst_termval: 150 (M.Fun = Fn) ��� ���t v. termsubst v t = termval M v t 151Proof 152 strip_tac >> ho_match_mp_tac term_induct >> simp[Cong MAP_CONG'] 153QED 154 155Theorem termval_triv: 156 (M.Fun = Fn) ��� ���t. termval M V t = t 157Proof 158 strip_tac >> ho_match_mp_tac term_induct >> simp[Cong MAP_CONG'] 159QED 160 161Theorem termval_termsubst: 162 ���t v i. termval M v (termsubst i t) = termval M (termval M v o i) t 163Proof 164 ho_match_mp_tac term_induct >> 165 simp[MAP_MAP_o, combinTheory.o_ABS_R, Cong MAP_CONG'] 166QED 167 168Theorem holds_formsubst : 169 ���v i. holds M v (formsubst i p) ��� holds M (termval M v o i) p 170Proof 171 Induct_on ���p��� >> simp[MAP_MAP_o, termval_termsubst, Cong MAP_CONG'] >> 172 rpt gen_tac >> 173 ho_match_mp_tac 174 (METIS_PROVE [] ��� 175 (���a. P a ��� (Q a ��� R a)) ��� ((���a. P a ��� Q a) ��� (���a. P a ��� R a)) 176 ���) >> 177 qx_gen_tac ���a��� >> strip_tac >> csimp[combinTheory.UPDATE_APPLY] >> 178 reverse COND_CASES_TAC >> simp[] 179 >- (irule holds_valuation >> rw[] >> 180 simp[combinTheory.APPLY_UPDATE_THM] >> rw[combinTheory.UPDATE_APPLY] >> 181 irule termval_valuation >> metis_tac[combinTheory.APPLY_UPDATE_THM]) >> 182 fs[] >> Q.MATCH_GOALSUB_ABBREV_TAC ���VARIANT (FV f)��� >> 183 irule holds_valuation >> qx_gen_tac ���u��� >> strip_tac >> simp[] >> 184 rw[combinTheory.APPLY_UPDATE_THM] >> 185 irule termval_valuation >> qx_gen_tac ���uu��� >> strip_tac >> 186 rw[combinTheory.APPLY_UPDATE_THM] >> 187 rename [���VARIANT (FV f) ��� FVT (i u)���] >> 188 ���FVT (i u) ��� FV f��� suffices_by metis_tac[FV_FINITE, VARIANT_NOTIN_SUBSET] >> 189 simp[formsubst_FV, Abbr���f���, SUBSET_DEF] >> 190 metis_tac[combinTheory.APPLY_UPDATE_THM] 191QED 192 193Theorem holds_formsubst1: 194 holds M �� (formsubst V��� x ��� t ��� p) ��� holds M ����� x ��� termval M �� t��� p 195Proof 196 simp[holds_formsubst] >> irule holds_valuation >> 197 rw[combinTheory.APPLY_UPDATE_THM] 198QED 199 200Theorem holds_rename: 201 holds M �� (formsubst V��� x ��� V y ��� p) ��� holds M ����� x ��� �� y ��� p 202Proof 203 simp[holds_formsubst1] 204QED 205 206Theorem holds_alpha_forall: 207 y ��� FV (FALL x p) ��� 208 (holds M v (FALL y (formsubst V��� x ��� V y��� p)) ��� 209 holds M v (FALL x p)) 210Proof 211 simp[combinTheory.APPLY_UPDATE_ID, DISJ_IMP_THM, holds_formsubst1, 212 combinTheory.UPDATE_APPLY, combinTheory.UPDATE_EQ] >> strip_tac >> 213 AP_TERM_TAC >> ABS_TAC >> AP_TERM_TAC >> 214 irule holds_valuation >> rpt strip_tac >> 215 rw[combinTheory.APPLY_UPDATE_THM] >> fs[] 216QED 217 218Theorem holds_alpha_exists: 219 y ��� FV (Exists x p) ��� 220 (holds M v (Exists y (formsubst V��� x ��� V y��� p)) ��� 221 holds M v (Exists x p)) 222Proof 223 simp[combinTheory.APPLY_UPDATE_ID, DISJ_IMP_THM, holds_formsubst1, 224 combinTheory.UPDATE_APPLY, combinTheory.UPDATE_EQ] >> strip_tac >> 225 AP_TERM_TAC >> ABS_TAC >> AP_TERM_TAC >> 226 irule holds_valuation >> rpt strip_tac >> 227 rw[combinTheory.APPLY_UPDATE_THM] >> fs[] 228QED 229 230Theorem termval_functions: 231 ���t. (���f zs. (f,LENGTH zs) ��� term_functions t ��� (M.Fun f zs = M'.Fun f zs)) ��� 232 ���v. termval M v t = termval M' v t 233Proof 234 ho_match_mp_tac term_induct >> 235 simp[MEM_MAP, PULL_EXISTS, DISJ_IMP_THM, FORALL_AND_THM] >> rw[] >> 236 AP_TERM_TAC >> irule MAP_CONG' >> rw[] >> 237 first_x_assum irule >> metis_tac[] 238QED 239 240Theorem holds_functions: 241 (M2.Dom = M1.Dom) ��� (���P zs. M2.Pred P zs ��� M1.Pred P zs) ��� 242 (���f zs. (f,LENGTH zs) ��� form_functions p ��� (M2.Fun f zs = M1.Fun f zs)) 243 ��� 244 ���v. holds M2 v p ��� holds M1 v p 245Proof 246 Induct_on ���p��� >> simp[MEM_MAP,PULL_EXISTS] >> rw[] >> AP_TERM_TAC >> 247 irule MAP_CONG' >> rw[] >> metis_tac[termval_functions] 248QED 249 250Theorem holds_predicates: 251 (M2.Dom = M1.Dom) ��� (���f zs. M2.Fun f zs = M1.Fun f zs) ��� 252 (���P zs. (P,LENGTH zs) ��� form_predicates p ��� (M2.Pred P zs ��� M1.Pred P zs)) 253��� 254 ���v. holds M2 v p ��� holds M1 v p 255Proof 256 Induct_on ���p��� >> rw[] >> AP_TERM_TAC >> irule MAP_CONG' >> rw[] >> 257 irule termval_functions >> simp[] 258QED 259 260Theorem holds_uclose: 261 (���v. valuation M v ��� holds M v (FALL x p)) ��� 262 (M.Dom = ���) ��� ���v. valuation M v ��� holds M v p 263Proof 264 simp[] >> Cases_on ���M.Dom = ������ >> simp[] >> 265 metis_tac[combinTheory.APPLY_UPDATE_ID, upd_valuation, valuation_def] 266QED 267 268Theorem copy_models: 269 INJ f ����(:��) ����(:��) ��� 270 (���Ms : �� model. 271 Ms.Dom ��� ��� ��� interpretation (language s) Ms ��� Ms satisfies s) ��� 272 (���Mt : �� model. 273 Mt.Dom ��� ��� ��� interpretation (language s) Mt ��� Mt satisfies s) 274Proof 275 rw[INJ_IFF] >> 276 qabbrev_tac ���f' = ��b. @a. f a = b��� >> 277 ������a. f' (f a) = a��� by simp[Abbr���f'���] >> 278 qexists_tac ���<| Dom := { f d | d ��� Ms.Dom }; 279 Fun := ��g zs. f (Ms.Fun g (MAP f' zs)); 280 Pred := ��p zs. Ms.Pred p (MAP f' zs) |>��� >> 281 rw[] 282 >- (fs[EXTENSION] >> metis_tac[]) 283 >- (fs[interpretation_def, language_def] >> rw[] >> first_x_assum irule >> 284 simp[MEM_MAP, PULL_EXISTS] >> metis_tac[]) >> 285 simp[satisfies_def] >> rpt gen_tac >> 286 qmatch_abbrev_tac ���valuation Mt v ��� _ ��� _��� >> 287 ������t v. valuation Mt v ��� (termval Mt v t = f (termval Ms (f' o v) t))��� 288 by (Induct >> simp[Cong MAP_CONG'] 289 >- (simp[valuation_def] >> 290 ���Mt.Dom = {f d | d ��� Ms.Dom}��� by simp[Abbr���Mt���] >> simp[] >> 291 metis_tac[]) >> 292 simp[Abbr���Mt���, MAP_MAP_o, combinTheory.o_ABS_R]) >> 293 ������k v m:num->��. f' o m��� k ��� f v ��� = (f' o m)��� k ��� v ������ 294 by (simp[combinTheory.APPLY_UPDATE_THM, FUN_EQ_THM] >> rw[]) >> 295 ������p v. valuation Mt v ��� (holds Mt v p ��� holds Ms (f' o v) p)��� 296 by (Induct >> simp[Cong MAP_CONG'] 297 >- simp[Abbr���Mt���, MAP_MAP_o, combinTheory.o_ABS_R] >> 298 rw[Abbr���Mt���, PULL_EXISTS]) >> 299 simp[] >> fs[satisfies_def] >> rw[] >> first_x_assum irule >> 300 fs[valuation_def] >> fs[Abbr���Mt���] >> metis_tac[] 301QED 302 303 304 305 306 307val _ = export_theory(); 308