1open HolKernel Parse boolLib bossLib;
2
3open pred_setTheory listTheory
4open boolSimps combinTheory
5open folLangTheory folModelsTheory
6
7val _ = new_theory "folPrenex";
8
9Definition qfree_def:
10  (qfree False ��� T) ���
11  (qfree (Pred _ _) ��� T) ���
12  (qfree (IMP f1 f2) ��� qfree f1 ��� qfree f2) ���
13  (qfree (FALL _ _) ��� F)
14End
15
16Theorem QFREE[simp]:
17  (qfree False ��� T) ���
18  (qfree True ��� T) ���
19  (qfree (Pred n ts) ��� T) ���
20  (qfree (Not p) ��� qfree p) ���
21  (qfree (Or p q) ��� qfree p ��� qfree q) ���
22  (qfree (And p q) ��� qfree p ��� qfree q) ���
23  (qfree (Iff p q) ��� qfree p ��� qfree q) ���
24  (qfree (IMP p q) ��� qfree p ��� qfree q) ���
25  (qfree (FALL n p) ��� F) ���
26  (qfree (Exists n p) ��� F)
27Proof
28  simp[qfree_def, Exists_def, And_def, Or_def, True_def, Not_def, Iff_def] >>
29  metis_tac[]
30QED
31
32Theorem qfree_formsubst[simp]:
33  qfree (formsubst i p) ��� qfree p
34Proof
35  Induct_on ���p��� >> simp[]
36QED
37
38Theorem qfree_bv_empty:
39  qfree p ��� (BV p = ���)
40Proof
41  Induct_on ���p��� >> simp[]
42QED
43
44val (prenex_rules, prenex_ind, prenex_cases) = Hol_reln���
45  (���p. qfree p ��� prenex p) ���
46  (���x p. prenex p ��� prenex (FALL x p)) ���
47  (���x p. prenex p ��� prenex (Exists x p))
48���;
49
50val (universal_rules, universal_ind, universal_cases) = Hol_reln���
51  (���p. qfree p ��� universal p) ���
52  (���x p. universal p ��� universal (FALL x p))
53���;
54
55Theorem prenex_INDUCT_NOT:
56  ���P. (���p. qfree p ��� P p) ���
57      (���x p. P p ��� P (FALL x p)) ���
58      (���p. P p ��� P (Not p))
59    ���
60      ���p. prenex p ��� P p
61Proof
62  ntac 2 strip_tac >> Induct_on ���prenex��� >> simp[Exists_def]
63QED
64
65Theorem universal_prenex:
66  ���p. universal p ��� prenex p
67Proof
68  Induct_on ���universal��� >> simp[prenex_rules]
69QED
70
71Theorem Exists_eqns[simp]:
72  Exists x p ��� Or q r ���
73  Exists x p ��� Iff q r ���
74  Exists x p ��� And q r ���
75  Exists x p ��� FALL y q ���
76  Exists x p ��� Pred n ts ���
77  ((Exists x p = IMP q r) ��� (q = FALL x (IMP p False)) ��� (r = False)) ���
78  ((Exists x p = Exists y q) ��� (x = y) ��� (p = q))
79Proof
80  simp[And_def, Or_def, Iff_def, Exists_def, Not_def] >> metis_tac[]
81QED
82
83Theorem PRENEX[simp]:
84  (prenex False ��� T) ���
85  (prenex True ��� T) ���
86  (prenex (Pred n ts) ��� T) ���
87  (prenex (Not p) ��� qfree p ��� ���x q. (Not p = Exists x q) ��� prenex q) ���
88  (prenex (Or p q) ��� qfree p ��� qfree q) ���
89  (prenex (And p q) ��� qfree p ��� qfree q) ���
90  (prenex (IMP p q) ��� qfree p ��� qfree q ���
91                      ���x r. (IMP p q = Exists x r) ��� prenex r) ���
92  (prenex (Iff p q) ��� qfree p ��� qfree q) ���
93  (prenex (FALL x p) ��� prenex p) ���
94  (prenex (Exists x p) ��� prenex p)
95Proof
96  rpt conj_tac >>
97  simp[SimpLHS, Once prenex_cases] >>
98  simp[And_def, Or_def, Iff_def, Not_def]
99QED
100
101Theorem formsubst_EQ[simp]:
102  (���i p. (formsubst i p = False) ��� (p = False)) ���
103  (���i p. (False = formsubst i p) ��� (p = False)) ���
104  (���i p n ts. (formsubst i p = Pred n ts) ��� ���ts0. (p = Pred n ts0) ���
105                                       (ts = MAP (termsubst i) ts0)) ���
106  (���i p q r. (formsubst i p = IMP q r) ���
107             ���q0 r0. (p = IMP q0 r0) ��� (q = formsubst i q0) ���
108                     (r = formsubst i r0)) ���
109  (���i p q. (formsubst i p = Not q) ��� ���q0. (p = Not q0) ��� (q = formsubst i q0))
110Proof
111  csimp[Not_def] >> rw[] >> Cases_on ���p��� >> simp[] >> metis_tac[]
112QED
113
114Theorem formsubst_Not[simp]:
115  formsubst i (Not p) = Not (formsubst i p)
116Proof
117  rw[Not_def]
118QED
119
120Theorem Not_11[simp]:
121  (Not p = Not q) ��� (p = q)
122Proof
123  rw[Not_def]
124QED
125
126Theorem formsubst_EQ_FALL:
127  (���x q. formsubst i p = FALL x q) ��� (���x q. p = FALL x q)
128Proof
129  Cases_on ���p��� >> simp[]
130QED
131
132Theorem formsubst_EQ_Exists:
133  (���x q. formsubst i p = Exists x q) ��� (���x q. p = Exists x q)
134Proof
135  Cases_on ���p��� >> simp[] >>
136  rename [���subf2 = False���, ���formsubst i subf1 = FALL _ _���] >>
137  Cases_on ���subf2 = False��� >> simp[] >>
138  Cases_on ���subf1��� >> simp[]
139QED
140
141Theorem prenex_formsubst[simp]:
142  prenex (formsubst i p) ��� prenex p
143Proof
144  ���(���p. prenex p ��� ���i. prenex (formsubst i p)) ���
145   (���p. prenex p ��� ���i q. (p = formsubst i q) ��� prenex q)���
146    suffices_by metis_tac[] >>
147  conj_tac >> Induct_on ���prenex��� >> simp[] >> rw[]
148  >- metis_tac[qfree_formsubst, prenex_rules]
149  >- simp[Exists_def]
150  >- metis_tac[qfree_formsubst, prenex_rules]
151  >- (rename [���FALL n p = formsubst i q���] >>
152      ������m r. q = FALL m r��� by metis_tac[formsubst_EQ_FALL] >> rw[] >> fs[] >>
153      metis_tac[])
154  >- (rename [���Exists n p = formsubst i q���] >>
155      ������m r. q = Exists m r��� by metis_tac[formsubst_EQ_Exists] >> rw[] >>
156      fs[Exists_def] >> metis_tac[])
157QED
158
159Definition size_def:
160  (size False = 1) ���
161  (size (Pred _ _) = 1) ���
162  (size (IMP q r) = 1 + size q + size r) ���
163  (size (FALL _ q) = 1 + size q)
164End
165
166Theorem SIZE[simp]:
167  (size False = 1) ���
168  (size True = 3) ���
169  (size (Pred n ts) = 1) ���
170  (size (Not p) = 2 + size p) ���
171  (size (Or p q) = size p + 2 * size q + 2) ���
172  (size (And p q) = size p + 2 * size q + 10) ���
173  (size (Iff p q) = 3 * size p + 3 * size q + 13) ���
174  (size (IMP p q) = size p + size q + 1) ���
175  (size (FALL x p) = 1 + size p) ���
176  (size (Exists x p) = 5 + size p)
177Proof
178  simp[And_def, Or_def, Iff_def, size_def, Exists_def, Not_def, True_def]
179QED
180
181Theorem size_formsubst[simp]:
182  ���i. size (formsubst i p) = size p
183Proof
184  Induct_on ���p��� >> simp[]
185QED
186
187Definition PPAT_def:
188  PPAT A B C p =
189    case some (x,q). p = Exists x q of
190        SOME (x,q) => B x q
191      | NONE =>
192        case p of
193            FALL x q => A x q
194          | _ => C p
195End
196
197Theorem PPAT[simp]:
198  (PPAT A B C (FALL x p) = A x p) ���
199  (PPAT A B C (Exists x p) = B x p) ���
200  ((!x q. p ��� FALL x q) ��� (���x q. p ��� Exists x q) ��� (PPAT A B C p = C p))
201Proof
202  simp[PPAT_def, pairTheory.ELIM_UNCURRY]>>
203  ������a b. (��y. (a:num = FST y) ��� (b:form = SND y)) = (��p. p = (a,b))���
204     by simp[FUN_EQ_THM, pairTheory.FORALL_PROD, EQ_SYM_EQ] >>
205  simp[] >>
206  Cases_on ���p��� >> simp[Exists_def]
207QED
208
209Theorem PPAT_CONG[defncong]:
210  ���A1 A2 B1 B2 C1 C2 q q'.
211    (���x p. size p < size q ��� (A1 x p = A2 x p)) ���
212    (���x p. size p < size q ��� (B1 x p = B2 x p)) ��� (���p. C1 p = C2 p) ���
213    (q = q') ���
214    (PPAT A1 B1 C1 q = PPAT A2 B2 C2 q')
215Proof
216  rw[] >>
217  Cases_on ������n p0. q = Exists n p0��� >> fs[] >>
218  Cases_on ���q��� >> simp[]
219QED
220
221Definition prenexR_def:
222  prenexR p q =
223    PPAT
224      (��x q0. let y = VARIANT (FV p ��� FV(FALL x q0))
225              in
226                FALL y (prenexR p (formsubst V���x ��� V y��� q0)))
227      (��x q0. let y = VARIANT (FV p ��� FV(Exists x q0))
228              in
229                Exists y (prenexR p (formsubst V���x ��� V y��� q0)))
230      (��q. IMP p q)
231      q
232Termination
233  WF_REL_TAC ���measure (size o SND)��� >> simp[]
234End
235
236Theorem prenexR_thm[simp]:
237  (prenexR p (FALL x q) = let y = VARIANT (FV p ��� FV (FALL x q))
238                          in
239                            FALL y (prenexR p (formsubst V���x ��� V y��� q))) ���
240  (prenexR p (Exists x q) = let y = VARIANT (FV p ��� FV(Exists x q))
241                            in
242                              Exists y (prenexR p (formsubst V���x ��� V y��� q))) ���
243  (qfree q ��� (prenexR p q = IMP p q))
244Proof
245  rpt conj_tac >> simp[SimpLHS, Once prenexR_def] >> simp[] >> strip_tac >>
246  ���(���x r. q ��� FALL x r) ��� (���x r. q ��� Exists x r)���
247     by (rpt strip_tac >> fs[]) >>
248  simp[]
249QED
250
251Definition prenexL_def:
252  prenexL p q =
253    PPAT (��x p0. let y = VARIANT (FV (FALL x p0) ��� FV q)
254                 in
255                   Exists y (prenexL (formsubst V���x ��� V y��� p0) q))
256         (��x p0. let y = VARIANT (FV (Exists x p0) ��� FV q)
257                 in
258                   FALL y (prenexL (formsubst V���x ��� V y��� p0) q))
259         (��p. prenexR p q) p
260Termination
261  WF_REL_TAC ���measure (size o FST)��� >> simp[]
262End
263
264Theorem prenexL_thm[simp]:
265  (prenexL (FALL x p) q = let y = VARIANT (FV (FALL x p) ��� FV q)
266                          in
267                            Exists y (prenexL (formsubst V���x ��� V y��� p) q)) ���
268  (prenexL (Exists x p) q = let y = VARIANT (FV (Exists x p) ��� FV q)
269                            in
270                              FALL y (prenexL (formsubst V���x ��� V y��� p) q)) ���
271  (qfree p ��� (prenexL p q = prenexR p q))
272Proof
273  rpt conj_tac >> simp[Once prenexL_def, SimpLHS] >> simp[] >> strip_tac >>
274  ���(���x r. p ��� FALL x r) ��� (���x r. p ��� Exists x r)���
275     by (rpt strip_tac >> fs[]) >>
276  simp[]
277QED
278
279Definition Prenex_def[simp]:
280  (Prenex False = False) ���
281  (Prenex (Pred n ts) = Pred n ts) ���
282  (Prenex (IMP f1 f2) = prenexL (Prenex f1) (Prenex f2)) ���
283  (Prenex (FALL x f) = FALL x (Prenex f))
284End
285
286Theorem prenexR_language[simp]:
287  ���p. language {prenexR p q} = language {IMP p q}
288Proof
289  completeInduct_on ���size q��� >> fs[PULL_FORALL, language_SING] >> rpt gen_tac >>
290  disch_then SUBST_ALL_TAC >>
291  Cases_on ������x q0. q = Exists x q0��� >> fs[]
292  >- (simp[Exists_def, Not_def, form_functions_formsubst] >>
293      simp_tac (srw_ss() ++ COND_elim_ss) [combinTheory.APPLY_UPDATE_THM]) >>
294  Cases_on ������x q0. q = FALL x q0��� >> fs[]
295  >- simp_tac (srw_ss() ++ COND_elim_ss)
296       [form_functions_formsubst,combinTheory.APPLY_UPDATE_THM] >>
297  conj_tac >> simp[Once prenexR_def]
298QED
299
300Theorem prenexL_language[simp]:
301  ���q. language {prenexL p q} = language {IMP p q}
302Proof
303  completeInduct_on ���size p��� >> fs[PULL_FORALL] >> rpt gen_tac >>
304  disch_then SUBST_ALL_TAC >>
305  Cases_on ������x p0. p = Exists x p0��� >> fs[] >> fs[]
306  >- (fs[Exists_def, Not_def, form_functions_formsubst, language_SING] >>
307      simp_tac (srw_ss() ++ COND_elim_ss) [combinTheory.APPLY_UPDATE_THM]) >>
308  Cases_on ������x p0. p = FALL x p0��� >> fs[]
309  >- full_simp_tac (srw_ss() ++ COND_elim_ss)
310       [language_SING,form_functions_formsubst,APPLY_UPDATE_THM,Exists_def,
311        Not_def] >>
312  simp[Once prenexL_def]
313QED
314
315Theorem prenex_lemma_forall:
316  P ��� (FV f1 = FV f2) ��� (language {f1} = language {f2}) ���
317  (���M:�� model v. M.Dom ��� ��� ��� (holds M v f1 ��� holds M v f2)) ���
318  P ��� (FV (FALL z f1) = FV (FALL z f2)) ���
319  (language {FALL z f1} = language {FALL z f2}) ���
320  ���M:�� model v. M.Dom ��� ��� ��� (holds M v (FALL z f1) ��� holds M v (FALL z f2))
321Proof
322  rw[language_SING]
323QED
324
325Theorem prenex_lemma_exists:
326  P ��� (FV f1 = FV f2) ��� (language {f1} = language {f2}) ���
327  (���M:�� model v. M.Dom ��� ��� ��� (holds M v f1 ��� holds M v f2)) ���
328  P ��� (FV (Exists z f1) = FV (Exists z f2)) ���
329  (language {Exists z f1} = language {Exists z f2}) ���
330  ���M:�� model v. M.Dom ��� ��� ��� (holds M v (Exists z f1) ��� holds M v (Exists z f2))
331Proof
332  rw[language_SING, Exists_def, Not_def]
333QED
334
335Theorem prenex_rename1[simp]:
336  ���f x y. prenex (formsubst V���x ��� V y��� f) ��� prenex f
337Proof
338  completeInduct_on ���size f��� >> fs[PULL_FORALL]
339QED
340
341Theorem tfresh_rename_inverts:
342  ���t x y. y ��� FVT t ��� (termsubst V���y ��� V x��� (termsubst V���x ��� V y��� t) = t)
343Proof
344  ho_match_mp_tac term_induct >> simp[] >> rw[MEM_MAP, MAP_MAP_o]
345  >- rw[combinTheory.APPLY_UPDATE_THM] >>
346  irule EQ_TRANS >> qexists_tac ���MAP I ts��� >> reverse conj_tac
347  >- simp[] >>
348  irule listTheory.MAP_CONG >> simp[] >> qx_gen_tac ���t0��� >> strip_tac >>
349  first_x_assum irule >> metis_tac[]
350QED
351
352Theorem holds_nonFV:
353  v ��� FV f ��� (holds M i��� v ��� t ��� f ��� holds M i f)
354Proof
355  strip_tac >> irule holds_valuation >>
356  simp[combinTheory.APPLY_UPDATE_THM] >> rw[] >> fs[]
357QED
358
359Theorem prenexR_FV[simp]:
360  FV (prenexR p q) = FV p ��� FV q
361Proof
362  completeInduct_on ���size q��� >> fs[PULL_FORALL] >> rw[] >>
363  Cases_on ������v q0. q = Exists v q0��� >> fs[]
364  >- (simp_tac (srw_ss() ++ COND_elim_ss)
365       [EXTENSION, formsubst_FV, termsubst_fvt, APPLY_UPDATE_THM] >>
366      qmatch_goalsub_abbrev_tac ���VARIANT s��� >>
367      qabbrev_tac ���vv = VARIANT s��� >>
368      ���vv ��� s��� by simp[Abbr���vv���, Abbr���s���, VARIANT_FINITE] >>
369      Q.UNABBREV_TAC ���s��� >> fs[] >> gen_tac >>
370      eq_tac >> rw[] >> simp[] >> fs[] >> metis_tac[]) >>
371  Cases_on ������v q0. q = FALL v q0��� >> fs[]
372  >- (simp_tac (srw_ss() ++ COND_elim_ss)
373       [EXTENSION, formsubst_FV, termsubst_fvt, APPLY_UPDATE_THM] >>
374      qmatch_goalsub_abbrev_tac ���VARIANT s��� >>
375      qabbrev_tac ���vv = VARIANT s��� >>
376      ���vv ��� s��� by simp[Abbr���vv���, Abbr���s���, VARIANT_FINITE] >>
377      Q.UNABBREV_TAC ���s��� >> fs[] >> gen_tac >>
378      eq_tac >> rw[] >> simp[] >> fs[] >> metis_tac[]) >>
379  simp[prenexR_def]
380QED
381
382Theorem prenexR_prenex:
383  qfree p ��� prenex q ��� prenex (prenexR p q)
384Proof
385  completeInduct_on ���size q��� >> fs[PULL_FORALL] >> gen_tac >>
386  disch_then SUBST_ALL_TAC >>
387  simp[Once prenex_cases, SimpLHS] >> dsimp[]
388QED
389
390Theorem prenexR_holds:
391  ���M v. M.Dom ��� ��� ��� (holds M v (prenexR p q) ��� holds M v (IMP p q))
392Proof
393  completeInduct_on ���size q��� >> fs[PULL_FORALL] >> rw[] >>
394  Cases_on ������v q0. q = Exists v q0��� >> fs[] >> fs[]
395  >- (qmatch_goalsub_abbrev_tac ���VARIANT ss��� >>
396      ���VARIANT ss ��� ss��� by simp[VARIANT_FINITE, Abbr���ss���] >>
397      qabbrev_tac ���vv = VARIANT ss��� >>
398      rename [���holds M vln��� vv ��� _ ��� f1���, ���formsubst _ f2���] >>
399      ���vv ��� FV f1��� by fs[Abbr���ss���] >>
400      ������t. holds M vln���vv ��� t��� f1 ��� holds M vln f1���
401          by (gen_tac >> irule holds_valuation >>
402              metis_tac[combinTheory.APPLY_UPDATE_THM]) >>
403      simp[] >> Cases_on ���holds M vln f1��� >> simp[]
404      >- (AP_TERM_TAC >> ABS_TAC >>
405          rename [���d ��� M.Dom���] >> Cases_on ���d ��� M.Dom��� >>
406          simp[holds_formsubst] >> irule holds_valuation >>
407          rw[combinTheory.APPLY_UPDATE_THM] >> fs[Abbr���ss���] >> metis_tac[]) >>
408      metis_tac[MEMBER_NOT_EMPTY]) >>
409  Cases_on ������v q0. q = FALL v q0��� >> fs[] >> fs[]
410  >- (qmatch_goalsub_abbrev_tac ���VARIANT ss��� >>
411      ���VARIANT ss ��� ss��� by simp[VARIANT_FINITE, Abbr���ss���] >>
412      qabbrev_tac ���vv = VARIANT ss��� >>
413      rename [���holds M vln��� vv ��� _ ��� f1���, ���formsubst V���v��� ��� V vv��� f2���] >>
414      ���vv ��� FV f1��� by fs[Abbr���ss���] >>
415      ������d. holds M vln���vv ��� d��� f1 ��� holds M vln f1���
416        by (gen_tac >> irule holds_valuation >> simp[APPLY_UPDATE_THM] >>
417            metis_tac[]) >>
418      simp[] >> Cases_on ���holds M vln f1��� >> simp[holds_formsubst] >>
419      AP_TERM_TAC >> ABS_TAC >> rename [���d ��� M.Dom���] >> Cases_on ���d ��� M.Dom��� >>
420      simp[] >> irule holds_valuation >> simp[APPLY_UPDATE_THM] >>
421      rw[APPLY_UPDATE_THM] >> fs[Abbr���ss���] >> metis_tac[]) >>
422  simp[Once prenexR_def]
423QED
424
425Theorem prenexL_FV[simp]:
426  FV (prenexL p q) = FV p ��� FV q
427Proof
428  completeInduct_on ���size p��� >> fs[PULL_FORALL] >> rw[] >>
429  Cases_on ������v p1. p = Exists v p1��� >> fs[]
430  >- (qmatch_goalsub_abbrev_tac ���VARIANT ss��� >>
431      ���VARIANT ss ��� ss��� by fs[Abbr���ss���, VARIANT_FINITE] >>
432      simp[formsubst_FV, combinTheory.APPLY_UPDATE_THM] >>
433      simp[EXTENSION] >> qx_gen_tac ���n��� >> eq_tac >>
434      asm_simp_tac(srw_ss() ++ COND_elim_ss) [] >> rw[]
435      >- simp[Abbr���ss���]
436      >- simp[Abbr���ss���]
437      >- (dsimp[] >> fs[Abbr���ss���])
438      >- metis_tac[]) >>
439  Cases_on ������v p1. p = FALL v p1��� >> fs[]
440  >- (qmatch_goalsub_abbrev_tac ���VARIANT ss��� >>
441      ���VARIANT ss ��� ss��� by fs[Abbr���ss���, VARIANT_FINITE] >>
442      simp[formsubst_FV, combinTheory.APPLY_UPDATE_THM] >>
443      simp[EXTENSION] >> qx_gen_tac ���n��� >> eq_tac >>
444      asm_simp_tac(srw_ss() ++ COND_elim_ss) [] >> rw[]
445      >- simp[Abbr���ss���]
446      >- simp[Abbr���ss���]
447      >- (dsimp[] >> fs[Abbr���ss���])
448      >- metis_tac[]) >>
449  simp[prenexL_def]
450QED
451
452Theorem prenexL_prenex[simp]:
453  prenex p ��� prenex q ��� prenex (prenexL p q)
454Proof
455  completeInduct_on ���size p��� >> fs[PULL_FORALL] >> rw[] >>
456  Cases_on ������v p0. p = Exists v p0��� >> fs[] >>
457  Cases_on ������v p0. p = FALL v p0��� >> fs[] >> fs[] >>
458  simp[prenexL_def] >>
459  ���qfree p��� suffices_by metis_tac[prenexR_prenex] >>
460  Q.UNDISCH_THEN ���prenex p��� mp_tac >> simp[Once prenex_cases]
461QED
462
463Theorem prenexL_holds[simp]:
464   ���M vln. M.Dom ��� ��� ��� (holds M vln (prenexL p q) ��� holds M vln (IMP p q))
465Proof
466  completeInduct_on ���size p��� >> fs[PULL_FORALL] >> rw[] >>
467  Cases_on ������v p0. p = Exists v p0��� >> fs[]
468  >- (qmatch_goalsub_abbrev_tac ���VARIANT ss��� >>
469      ���VARIANT ss ��� ss��� by simp[VARIANT_FINITE, Abbr���ss���] >>
470      ������d. holds M vln��� VARIANT ss ��� d��� q ��� holds M vln q���
471        by (gen_tac >> irule holds_valuation >> rw[APPLY_UPDATE_THM] >>
472            fs[Abbr���ss���]) >> simp[PULL_EXISTS] >>
473      AP_TERM_TAC >> ABS_TAC >> rename [���d ��� M.Dom���] >> Cases_on ���d ��� M.Dom��� >>
474      simp[] >> AP_THM_TAC >> AP_TERM_TAC >>
475      simp[holds_formsubst] >> irule holds_valuation >> rw[APPLY_UPDATE_THM] >>
476      fs[Abbr���ss���] >> metis_tac[]) >>
477  Cases_on ������v p0. p = FALL v p0��� >> fs[]
478  >- (qmatch_goalsub_abbrev_tac ���VARIANT ss��� >>
479      ���VARIANT ss ��� ss��� by simp[VARIANT_FINITE, Abbr���ss���] >>
480      simp[GSYM LEFT_EXISTS_IMP_THM] >>
481      ������d. holds M vln��� VARIANT ss ��� d ��� q ��� holds M vln q���
482        by (gen_tac >> irule holds_nonFV >> fs[Abbr���ss���]) >>
483      simp[] >> Cases_on ���holds M vln q��� >> simp[]
484      >- metis_tac[MEMBER_NOT_EMPTY] >>
485      AP_TERM_TAC >> ABS_TAC >> rename [���d ��� M.Dom���] >> Cases_on ���d ��� M.Dom��� >>
486      simp[] >> simp[holds_formsubst] >> irule holds_valuation >>
487      rw[APPLY_UPDATE_THM] >> fs[Abbr���ss���] >> metis_tac[]) >>
488  simp[Once prenexL_def, prenexR_holds]
489QED
490
491Theorem prenex_Prenex[simp]:
492  prenex (Prenex f)
493Proof
494  Induct_on ���f��� >> simp[]
495QED
496
497Theorem FV_Prenex[simp]:
498  FV (Prenex f) = FV f
499Proof
500  Induct_on ���f��� >> simp[]
501QED
502
503Theorem holds_Prenex[simp]:
504  ���vln. M.Dom ��� ��� ��� (holds M vln (Prenex f) ��� holds M vln f)
505Proof
506  Induct_on ���f��� >> simp[prenexL_holds]
507QED
508
509Theorem language_Prenex[simp]:
510  language {Prenex f} = language {f}
511Proof
512  Induct_on ���f��� >> simp[] >> fs[language_SING]
513QED
514
515Theorem form_functions_prenexR[simp]:
516  ���f1 f2. form_functions (prenexR f1 f2) = form_functions f1 ��� form_functions f2
517Proof
518  ho_match_mp_tac prenexR_ind >> rpt strip_tac >> simp[Once prenexR_def] >>
519  Cases_on������x f2'. f2 = Exists x f2'��� >>
520  full_simp_tac (srw_ss() ++ COND_elim_ss)
521    [form_functions_formsubst, combinTheory.APPLY_UPDATE_THM] >>
522  Cases_on ������x f2'. f2 = FALL x f2'��� >>
523  full_simp_tac (srw_ss() ++ COND_elim_ss)
524    [form_functions_formsubst, combinTheory.APPLY_UPDATE_THM]
525QED
526
527Theorem form_functions_prenexL[simp]:
528  ���f1 f2. form_functions (prenexL f1 f2) = form_functions f1 ��� form_functions f2
529Proof
530  ho_match_mp_tac prenexL_ind >> rpt strip_tac >>
531  simp[Once prenexL_def] >>
532  Cases_on������x f1'. f1 = Exists x f1'��� >>
533  full_simp_tac (srw_ss() ++ COND_elim_ss)
534    [form_functions_formsubst, combinTheory.APPLY_UPDATE_THM] >>
535  Cases_on ������x f1'. f1 = FALL x f1'��� >>
536  full_simp_tac (srw_ss() ++ COND_elim_ss)
537    [form_functions_formsubst, combinTheory.APPLY_UPDATE_THM]
538QED
539
540Theorem form_functions_Prenex[simp]:
541  form_functions (Prenex f) = form_functions f
542Proof
543  Induct_on ���f��� >> simp[]
544QED
545
546Theorem form_predicates_prenexR[simp]:
547  ���f1 f2.
548    form_predicates (prenexR f1 f2) = form_predicates f1 ��� form_predicates f2
549Proof
550  ho_match_mp_tac prenexR_ind >> rpt strip_tac >>
551  simp[Once prenexR_def] >>
552  Cases_on������x f2'. f2 = Exists x f2'��� >> fs [] >>
553  Cases_on ������x f2'. f2 = FALL x f2'��� >> fs []
554QED
555
556Theorem form_predicates_prenexL[simp]:
557  ���f1 f2.
558    form_predicates (prenexL f1 f2) = form_predicates f1 ��� form_predicates f2
559Proof
560  ho_match_mp_tac prenexL_ind >> rpt strip_tac >>
561  simp[Once prenexL_def] >>
562  Cases_on������x f1'. f1 = Exists x f1'��� >> fs [] >>
563  Cases_on ������x f1'. f1 = FALL x f1'��� >> fs []
564QED
565
566Theorem form_predicates_Prenex[simp]:
567  form_predicates (Prenex p) = form_predicates p
568Proof
569  Induct_on ���p��� >> simp[]
570QED
571
572
573val _ = export_theory();
574