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