1open HolKernel boolLib Parse bossLib
2
3open binderLib
4open nomdatatype
5open nomsetTheory
6open generic_termsTheory
7open lcsymtacs
8open boolSimps
9open pred_setTheory
10
11fun Save_thm (nm, th) = save_thm(nm,th) before export_rewrites [nm]
12fun Store_thm(nm,t,tac) = store_thm(nm,t,tac) before export_rewrites [nm]
13
14val _ = new_theory "foltypes"
15
16val _ = set_fixity "=" (Infix(NONASSOC, 450))
17
18val tyname = "foterm"
19
20val _ = Hol_datatype `
21  ftm_discriminator = ftmFN of string | ftmRN of string | ftmF | ftmIMP |
22                      ftmALL
23`;
24
25val [gvar,glam] = genind_rules |> SPEC_ALL |> CONJUNCTS
26
27val vp = ``(��n u:unit. n = 0)``
28val lp = ``
29  (��n d:ftm_discriminator tns uns.
30     n = 0 ��� (���s. d = ftmFN s) ��� (���i. MEM i uns ��� i = 0) ��� tns = [] ���
31     n = 1 ��� (���s. d = ftmRN s) ��� (���i. MEM i uns ��� i = 0) ��� tns = [] ���
32     n = 1 ��� d = ftmF ��� uns = [] ��� tns = [] ���
33     n = 1 ��� d = ftmIMP ��� uns = [1;1] ��� tns = [] ���
34     n = 1 ��� d = ftmALL ��� uns = [] ��� tns = [1])
35``
36
37val {term_ABS_pseudo11, term_REP_11, genind_term_REP, genind_exists,
38     termP, absrep_id = term_absrep_id,
39     repabs_pseudo_id = term_repabs_pseudo_id,
40     term_REP_t, term_ABS_t,
41     newty = term_ty, ...} =
42    new_type_step1 tyname 0 {vp=vp, lp = lp}
43
44val VAR_t = mk_var("VAR", ``:string -> ^term_ty``)
45val VAR_def = new_definition(
46  "VAR_def",
47  ``^VAR_t s = ^term_ABS_t (GVAR s ())``);
48val VAR_termP = prove(
49  mk_comb(termP, VAR_def |> SPEC_ALL |> concl |> rhs |> rand),
50  srw_tac[][genind_rules]);
51val VAR_t = defined_const VAR_def
52
53val FN_t = mk_var("FN", ``:string -> ^term_ty list -> ^term_ty``)
54val FN_def = new_definition(
55  "FN_def",
56  ``^FN_t s args =
57    ^term_ABS_t (GLAM ARB (ftmFN s) [] (MAP ^term_REP_t args))``);
58val FN_termP = prove(
59  ``^termP (GLAM x (ftmFN s) [] (MAP ^term_REP_t args))``,
60  match_mp_tac glam >> srw_tac [][genind_term_REP] >>
61  qexists_tac `GENLIST (��n. 0) (LENGTH args)` >>
62  simp[listTheory.MEM_GENLIST,
63       listTheory.LIST_REL_EL_EQN, listTheory.EL_MAP, genind_term_REP])
64val FN_t = defined_const FN_def
65
66val FN_def' = prove(
67  ``^term_ABS_t (GLAM v (ftmFN s) [] (MAP ^term_REP_t args)) = ^FN_t s args``,
68  srw_tac[][FN_def, GLAM_NIL_EQ, term_ABS_pseudo11, FN_termP]);
69
70val tm_cons_info = [{con_termP = VAR_termP, con_def = VAR_def},
71                    {con_termP = FN_termP, con_def = SYM FN_def'}]
72val tpm_name_pfx = "t"
73
74val {tpm_thm = tpm_thm0, term_REP_tpm, t_pmact_t, tpm_t} =
75    define_permutation { name_pfx = "t", name = tyname,
76                         term_REP_t = term_REP_t,
77                         term_ABS_t = term_ABS_t, absrep_id = term_absrep_id,
78                         repabs_pseudo_id = term_repabs_pseudo_id,
79                         cons_info = tm_cons_info, newty = term_ty,
80                         genind_term_REP = genind_term_REP}
81
82val tpm_thm = save_thm(
83  "tpm_thm",
84  tpm_thm0 |> SIMP_RULE bool_ss [listpm_MAP, listTheory.MAP_MAP_o,
85                                 combinTheory.o_DEF, SYM term_REP_tpm]
86           |> REWRITE_RULE [GSYM combinTheory.o_DEF,
87                            GSYM listTheory.MAP_MAP_o]
88           |> REWRITE_RULE [FN_def']);
89
90val forms_exist = prove(
91  ``���x. genind ^vp ^lp 1 x``,
92  qexists_tac `GLAM ARB (ftmRN s) [] []` >>
93  match_mp_tac glam >> simp[] >> qexists_tac `[]` >> simp[]);
94
95val {absrep_id = form_absrep_id, newty = form_ty,
96     repabs_pseudo_id = form_repabs_pseudo_id, termP = formP, termP_exists,
97     termP_term_REP = formP_form_REP,
98     term_ABS_t = form_ABS_t, term_ABS_pseudo11 = form_ABS_pseudo11,
99     term_REP_t = form_REP_t,
100     term_REP_11 = form_REP_11} =
101    newtypeTools.rich_new_type ("form", forms_exist)
102
103val ALL_t = mk_var("ALL", ``:string -> ^form_ty -> ^form_ty``)
104val ALL_def = new_definition(
105  "ALL_def",
106  ``^ALL_t s body =
107    ^form_ABS_t (GLAM s ftmALL [^form_REP_t body] [])``);
108val ALL_formP = prove(
109  mk_comb(formP, ALL_def |> SPEC_ALL |> concl |> rhs |> rand),
110  match_mp_tac glam >> simp[formP_form_REP]);
111val ALL_t = defined_const ALL_def
112
113val REL_t = mk_var("REL", ``:string -> ^term_ty list -> ^form_ty``)
114val REL_def = new_definition(
115  "REL_def",
116  ``^REL_t s args =
117    ^form_ABS_t (GLAM ARB (ftmRN s) [] (MAP ^term_REP_t args))``);
118val REL_formP = prove(
119  ``^formP (GLAM v (ftmRN s) [] (MAP ^term_REP_t args))``,
120  match_mp_tac glam >> simp[genind_term_REP] >>
121  qexists_tac `GENLIST (\n. 0) (LENGTH args)` >>
122  simp[listTheory.MEM_GENLIST,
123       listTheory.LIST_REL_EL_EQN, listTheory.EL_MAP, genind_term_REP])
124val REL_t = defined_const REL_def
125val REL_def' = prove(
126  ``^form_ABS_t (GLAM v (ftmRN s) [] (MAP ^term_REP_t args)) = ^REL_t s args``,
127  srw_tac[][REL_def, GLAM_NIL_EQ, form_ABS_pseudo11, REL_formP]);
128
129val FALSE_t = mk_var("FALSE", ``:^form_ty``)
130val FALSE_def = new_definition(
131  "FALSE_def",
132  ``^FALSE_t = ^form_ABS_t (GLAM ARB ftmF [] [])``);
133val FALSE_formP = prove(
134  ``^formP (GLAM v ftmF [] [])``,
135  match_mp_tac glam >> simp[]);
136val FALSE_t = defined_const FALSE_def
137val FALSE_def' = prove(
138  ``^form_ABS_t (GLAM v ftmF [] []) = ^FALSE_t``,
139  srw_tac[][FALSE_def, GLAM_NIL_EQ, form_ABS_pseudo11, FALSE_formP])
140
141val IMP_t = mk_var("IMP", ``:^form_ty -> ^form_ty -> ^form_ty``)
142val IMP_def = new_definition("IMP_def",
143  ``^IMP_t f1 f2 =
144    ^form_ABS_t (GLAM ARB ftmIMP [] [^form_REP_t f1; ^form_REP_t f2])``);
145val IMP_formP = prove(
146  ``^formP (GLAM v ftmIMP [] [^form_REP_t f1; ^form_REP_t f2])``,
147  match_mp_tac glam >> simp[formP_form_REP]);
148val IMP_t = defined_const IMP_def
149val IMP_def' = prove(
150  ``^form_ABS_t (GLAM v ftmIMP [] [^form_REP_t f1; ^form_REP_t f2]) =
151    ^IMP_t f1 f2``,
152  rw[IMP_def, GLAM_NIL_EQ, form_ABS_pseudo11, IMP_formP]);
153
154val fm_cons_info = [{con_termP = REL_formP, con_def = GSYM REL_def'},
155                    {con_termP = ALL_formP, con_def = ALL_def},
156                    {con_termP = FALSE_formP, con_def = GSYM FALSE_def'},
157                    {con_termP = IMP_formP, con_def = GSYM IMP_def'}]
158val tpm_name_pfx = "f"
159
160val {tpm_thm = fpm_thm0, term_REP_tpm = form_REP_fpm, t_pmact_t = f_pmact_t,
161     tpm_t = fpm_t} =
162    define_permutation { name_pfx = "f", name = "form",
163                         term_REP_t = form_REP_t,
164                         term_ABS_t = form_ABS_t, absrep_id = form_absrep_id,
165                         repabs_pseudo_id = form_repabs_pseudo_id,
166                         cons_info = fm_cons_info, newty = form_ty,
167                         genind_term_REP = formP_form_REP}
168
169val fpm_thm = save_thm(
170  "fpm_thm",
171  fpm_thm0 |> SIMP_RULE bool_ss [listpm_MAP, listTheory.MAP_MAP_o,
172                                 combinTheory.o_DEF, SYM term_REP_tpm]
173           |> REWRITE_RULE [GSYM combinTheory.o_DEF,
174                            GSYM listTheory.MAP_MAP_o]
175           |> REWRITE_RULE [REL_def'])
176
177(* support *)
178val term_REP_eqv = prove(
179   ``support (fn_pmact ^t_pmact_t gt_pmact) ^term_REP_t {}`` ,
180   srw_tac [][support_def, fnpm_def, FUN_EQ_THM, term_REP_tpm, pmact_sing_inv]);
181
182val supp_term_REP = prove(
183  ``supp (fn_pmact ^t_pmact_t gt_pmact) ^term_REP_t = {}``,
184  REWRITE_TAC [GSYM SUBSET_EMPTY] >>
185  MATCH_MP_TAC (GEN_ALL supp_smallest) >>
186  srw_tac [][term_REP_eqv])
187
188val tpm_def' =
189    term_REP_tpm |> AP_TERM term_ABS_t |> PURE_REWRITE_RULE [term_absrep_id]
190
191val t = mk_var("t", term_ty)
192val supptpm_support = prove(
193  ``support ^t_pmact_t ^t (supp gt_pmact (^term_REP_t ^t))``,
194  srw_tac [][support_def, tpm_def', supp_fresh, term_absrep_id]);
195
196val supptpm_apart = prove(
197  ``x ��� supp gt_pmact (^term_REP_t ^t) ��� y ��� supp gt_pmact (^term_REP_t ^t) ���
198    ^tpm_t [(x,y)] ^t ��� ^t``,
199  srw_tac [][tpm_def']>>
200  DISCH_THEN (MP_TAC o AP_TERM term_REP_t) >>
201  srw_tac [][term_repabs_pseudo_id, genind_gtpm_eqn, genind_term_REP,
202             supp_apart]);
203
204val supp_tpm = prove(
205  ``supp ^t_pmact_t ^t = supp gt_pmact (^term_REP_t ^t)``,
206  match_mp_tac (GEN_ALL supp_unique_apart) >>
207  srw_tac [][supptpm_support, supptpm_apart, FINITE_GFV])
208
209val supp_tpml = prove(
210  ``supp (list_pmact ^t_pmact_t) ts = GFVl (MAP foterm_REP ts)``,
211  Induct_on `ts` >> simp[supp_tpm]);
212
213val _ = overload_on ("tFV", ``supp ^t_pmact_t``)
214val _ = overload_on ("tFVl", ``supp (list_pmact ^t_pmact_t)``)
215
216val FINITE_tFV = store_thm(
217  "FINITE_tFV",
218  ``FINITE (tFV t)``,
219  srw_tac [][supp_tpm, FINITE_GFV]);
220val _ = export_rewrites ["FINITE_tFV"]
221
222fun supp_clause repabs_pseudo_id {con_termP, con_def} = let
223  open pred_setTheory
224  val t = mk_comb(``supp ^t_pmact_t``, lhand (concl (SPEC_ALL con_def)))
225in
226  t |> REWRITE_CONV [supp_tpm, con_def, MATCH_MP repabs_pseudo_id con_termP,
227                     GFV_thm]
228    |> REWRITE_RULE [supp_listpm, EMPTY_DELETE, UNION_EMPTY]
229    |> REWRITE_RULE [GSYM supp_tpm, GSYM supp_tpml]
230    |> GEN_ALL
231end
232
233val tFV_thm = Save_thm(
234  "tFV_thm",
235  LIST_CONJ (map (supp_clause term_repabs_pseudo_id) tm_cons_info))
236
237val form_REP_eqv = prove(
238   ``support (fn_pmact ^f_pmact_t gt_pmact) ^form_REP_t {}`` ,
239   srw_tac [][support_def, fnpm_def, FUN_EQ_THM, form_REP_fpm, pmact_sing_inv]);
240
241val supp_form_REP = prove(
242  ``supp (fn_pmact ^f_pmact_t gt_pmact) ^form_REP_t = {}``,
243  REWRITE_TAC [GSYM SUBSET_EMPTY] >> MATCH_MP_TAC (GEN_ALL supp_smallest) >>
244  srw_tac [][form_REP_eqv])
245
246val fpm_def' =
247    form_REP_fpm |> AP_TERM form_ABS_t |> PURE_REWRITE_RULE [form_absrep_id]
248
249val t = mk_var("f", form_ty)
250val supptpm_support = prove(
251  ``support ^f_pmact_t ^t (supp gt_pmact (^form_REP_t ^t))``,
252  srw_tac [][support_def, fpm_def', supp_fresh, form_absrep_id]);
253
254val supptpm_apart = prove(
255  ``x ��� supp gt_pmact (^form_REP_t ^t) ��� y ��� supp gt_pmact (^form_REP_t ^t) ���
256    ^fpm_t [(x,y)] ^t ��� ^t``,
257  srw_tac [][fpm_def']>>
258  DISCH_THEN (MP_TAC o AP_TERM form_REP_t) >>
259  srw_tac [][form_repabs_pseudo_id, genind_gtpm_eqn, formP_form_REP,
260             supp_apart]);
261
262val supp_tpm = prove(
263  ``supp ^f_pmact_t ^t = supp gt_pmact (^form_REP_t ^t)``,
264  match_mp_tac (GEN_ALL supp_unique_apart) >>
265  srw_tac [][supptpm_support, supptpm_apart, FINITE_GFV])
266
267val _ = overload_on ("fFV", ``supp ^f_pmact_t``)
268
269val FINITE_fFV = store_thm(
270  "FINITE_fFV",
271  ``FINITE (fFV f)``,
272  srw_tac [][supp_tpm, FINITE_GFV]);
273val _ = export_rewrites ["FINITE_fFV"]
274
275fun supp_clause repabs_pseudo_id {con_termP, con_def} = let
276  open pred_setTheory
277  val t = mk_comb(``supp ^f_pmact_t``, lhand (concl (SPEC_ALL con_def)))
278in
279  t |> REWRITE_CONV [supp_tpm, con_def, MATCH_MP repabs_pseudo_id con_termP,
280                     GFV_thm]
281    |> REWRITE_RULE [supp_listpm, EMPTY_DELETE, UNION_EMPTY]
282    |> REWRITE_RULE [GSYM supp_tpm, GSYM supp_tpml]
283    |> GEN_ALL
284end
285
286val fFV_thm = Save_thm(
287  "fFV_thm",
288  LIST_CONJ (map (supp_clause form_repabs_pseudo_id) fm_cons_info))
289
290val LIST_REL_CONS1 = listTheory.LIST_REL_CONS1
291val LIST_REL_NIL = listTheory.LIST_REL_NIL
292
293val term_ind0 =
294    bvc_genind
295        |> INST_TYPE [alpha |-> ``:ftm_discriminator``, beta |-> ``:unit``]
296        |> Q.INST [`vp` |-> `^vp`, `lp` |-> `^lp`]
297        |> Q.SPEC `��n t0 x. (n = 0) ��� Q t0 x`
298        |> Q.INST [`Q` |-> `��t. P (foterm_ABS t)`]
299        |> SPEC_ALL
300        |> UNDISCH_ALL |> SIMP_RULE std_ss []
301        |> SPECL [``0n``, ``foterm_REP ft``]
302        |> SIMP_RULE std_ss [genind_term_REP, term_absrep_id]
303        |> Q.GEN `ft` |> DISCH_ALL
304        |> SIMP_RULE std_ss [LEFT_AND_OVER_OR, DISJ_IMP_THM, LIST_REL_CONS1,
305                             LIST_REL_NIL,
306                             RIGHT_AND_OVER_OR, FORALL_AND_THM, GSYM VAR_def,
307                             oneTheory.FORALL_ONE]
308        |> Q.INST [`P` |-> `��t x. Q t`, `fv` |-> `��x. {}`]
309        |> SIMP_RULE (srw_ss()) [] |> Q.GEN `Q`
310
311val foterm_ind = store_thm(
312  "foterm_ind",
313  ``!P.
314      (���s. P (VAR s)) ���
315      (���s ts. (���t. MEM t ts ��� P t) ��� P (FN s ts)) ���
316      ���ft. P ft``,
317  rpt gen_tac >> strip_tac >> match_mp_tac term_ind0 >> simp[] >>
318  rw[listTheory.LIST_REL_EL_EQN] >>
319  `���i. i < LENGTH uns ��� EL i uns = 0` by metis_tac [listTheory.MEM_EL] >>
320  fs[] >>
321  `���ts. us = MAP foterm_REP ts`
322     by (qexists_tac `MAP foterm_ABS us` >>
323         simp[listTheory.MAP_MAP_o] >>
324         match_mp_tac listTheory.LIST_EQ >> simp[listTheory.EL_MAP] >>
325         qx_gen_tac `i` >> rw[] >> ONCE_REWRITE_TAC [EQ_SYM_EQ] >>
326         match_mp_tac term_repabs_pseudo_id >> metis_tac[]) >>
327  simp[FN_def'] >> first_x_assum match_mp_tac >>
328  rw[] >> qpat_x_assum `���n. n < LENGTH uns ��� PP ��� QQ` mp_tac >>
329  simp[listTheory.EL_MAP, term_absrep_id] >>
330  `���n. n < LENGTH ts ��� t = EL n ts` by metis_tac[listTheory.MEM_EL] >>
331  simp[])
332
333val GFVl_thm = prove(
334  ``GFVl [] = {} ��� GFVl (g::gs) = GFV g ��� GFVl gs``,
335  rw[EXTENSION, IN_GFVl] >> metis_tac[]);
336
337val formP_eq = prove(
338  ``^formP g <=> ���f. g = form_REP f``,
339  rw[EQ_IMP_THM] >> rw[formP_form_REP] >> qexists_tac `form_ABS g` >>
340  rw[form_repabs_pseudo_id]);
341
342val fof_ind0 =
343    bvc_genind
344        |> INST_TYPE [alpha |-> ``:ftm_discriminator``, beta |-> ``:unit``]
345        |> Q.INST [`vp` |-> `^vp`, `lp` |-> `^lp`]
346        |> Q.SPEC `��n t0 x. (n = 1) ��� Q t0 x`
347        |> Q.INST [`Q` |-> `��t. P (form_ABS t)`]
348        |> SPEC_ALL
349        |> UNDISCH_ALL |> SIMP_RULE std_ss []
350        |> SPECL [``1n``, ``form_REP f``]
351        |> SIMP_RULE std_ss [formP_form_REP, form_absrep_id]
352        |> Q.GEN `f` |> DISCH_ALL
353        |> SIMP_RULE std_ss [LEFT_AND_OVER_OR, DISJ_IMP_THM, LIST_REL_CONS1,
354                             LIST_REL_NIL,
355                             RIGHT_AND_OVER_OR, FORALL_AND_THM, GSYM VAR_def,
356                             oneTheory.FORALL_ONE, formP_eq]
357        |> CONV_RULE (LAND_CONV
358                      (SIMP_CONV (std_ss ++ DNF_ss) [IMP_def', GFVl_thm]))
359        |> SIMP_RULE (srw_ss()) [FALSE_def', form_absrep_id, GSYM ALL_def,
360                                 IMP_def']
361        |> GEN_ALL
362
363val fof_ind = store_thm(
364  "fof_ind",
365  ``���P fv.
366      (���x. FINITE (fv x)) ��� (���x ts s. P (REL s ts) x) ���
367      (���x. P FALSE x) ���
368      (���f1 f2 x. (���x. P f1 x) ��� (���x. P f2 x) ��� P (IMP f1 f2) x) ���
369      (���v x f. v ��� fv x ��� (���x. P f x) ��� P (ALL v f) x)
370     ���
371      ���f x. P f x``,
372  rpt gen_tac >> strip_tac >> match_mp_tac fof_ind0 >> qexists_tac `fv` >>
373  simp[] >> rpt strip_tac >>
374  `���ts. MAP foterm_REP ts = us`
375     by (qexists_tac `MAP foterm_ABS us` >> simp[listTheory.MAP_MAP_o] >>
376         match_mp_tac listTheory.LIST_EQ >> simp[] >>
377         qpat_x_assum `LIST_REL RR XX YY` mp_tac >>
378         simp[listTheory.LIST_REL_EL_EQN, listTheory.EL_MAP] >>
379         rw[] >> match_mp_tac term_repabs_pseudo_id >>
380         asm_simp_tac (srw_ss() ++ DNF_ss) [] >>
381         fs[IMP_CONJ_THM, FORALL_AND_THM] >>
382         `���i. i < LENGTH uns ��� EL i uns = 0`
383           by metis_tac [listTheory.MEM_EL] >>
384         fs[]) >>
385  rw[REL_def']);
386
387val fof_indX = save_thm(
388  "fof_indX",
389  fof_ind |> Q.SPEC `��f x. Q f` |> Q.SPEC `��x. X` |> SIMP_RULE (srw_ss()) []
390          |> Q.INST [`Q` |-> `P`] |> Q.GEN `X` |> Q.GEN `P`)
391
392val ALL_eq_thm = save_thm(
393  "ALL_eq_thm",
394  ``ALL v1 f1 = ALL v2 f2``
395    |> SIMP_CONV (srw_ss()) [ALL_def, ALL_formP, form_ABS_pseudo11,
396                             GLAM_eq_thm, form_REP_11, GSYM form_REP_fpm,
397                             GSYM supp_tpm]
398    |> GENL [``v1:string``, ``v2:string``, ``f1:form``, ``f2:form``]);
399
400val (_, repty) = dom_rng (type_of term_REP_t)
401val repty' = ty_antiq repty
402val tlf = ``��(v:string)
403             (d:ftm_discriminator)
404             (ds1:(�� -> ��) list) (ds2:(�� -> ��) list)
405             (ts1 : ^repty' list) (ts2: ^repty' list) (p:��).
406               case d of ftmFN s => f s (MAP foterm_ABS ts2)
407                                        (MAP (��r. r p) ds2) : 'a``
408
409val vf = ``��(s:string) u:unit p:��. vv s p:��``
410
411val termP0 = prove(
412  ``genind ^vp ^lp n t <=> (n = 0) ��� ^termP t ��� (n = 1) ��� ^formP t``,
413  eq_tac >> simp_tac (srw_ss()) [DISJ_IMP_THM] >>
414  strip_tac >> qsuff_tac `n = 0 ��� n = 1` >- (strip_tac >> rw[]) >>
415  pop_assum mp_tac >>
416  Q.ISPEC_THEN `t` STRUCT_CASES_TAC gterm_cases >>
417  rw[genind_GVAR, genind_GLAM_eqn]);
418
419val termP_term_REP = prove(
420  ``^termP gt ��� (���t. gt = ^term_REP_t t)``,
421  rw[EQ_IMP_THM] >> rw[genind_term_REP] >> qexists_tac `^term_ABS_t gt` >>
422  rw[term_repabs_pseudo_id]);
423
424fun select_exconjs is thm = let
425  val (v, body) = dest_exists (concl thm)
426  val bodyth = ASSUME body
427  val allcs = CONJUNCTS bodyth
428  val cs = map (fn i => List.nth(allcs, i)) is
429  val body' = LIST_CONJ cs
430  val exbody = EXISTS (mk_exists(v, concl body'), v) body'
431in
432  CHOOSE (v, thm) exbody
433end
434
435val tm_recursion0 =
436  parameter_gtm_recursion
437    |> INST_TYPE [alpha |-> ``:ftm_discriminator``, beta |-> ``:unit``,
438                  gamma |-> alpha]
439    |> Q.INST [`lf` |-> `^tlf`, `lp` |-> `^lp`, `vp` |-> `^vp`, `vf` |-> `^vf`]
440    |> ONCE_REWRITE_RULE [termP0]
441    |> SIMP_RULE bool_ss [DISJ_IMP_THM, FORALL_AND_THM, genind_GVAR,
442                          genind_GLAM_eqn, termP_term_REP]
443    |> SIMP_RULE std_ss []
444    |> CONV_RULE (RAND_CONV (SIMP_CONV (srw_ss() ++ DNF_ss) []))
445    |> UNDISCH_ALL
446    |> select_exconjs [0,1,6]
447
448
449val _ = export_theory()
450