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