1open HolKernel Parse boolLib bossLib; 2 3open pred_setTheory listTheory nlistTheory 4 5val _ = new_theory "folLang"; 6 7Theorem MAP_CONG' = REWRITE_RULE [GSYM AND_IMP_INTRO] MAP_CONG 8 9 10Definition LIST_UNION_def[simp]: 11 (LIST_UNION [] = ���) ��� 12 (LIST_UNION (h::t) = h ��� LIST_UNION t) 13End 14 15Theorem IN_LIST_UNION[simp]: 16 x ��� LIST_UNION l ��� ���s. MEM s l ��� x ��� s 17Proof 18 Induct_on ���l��� >> simp[] >> metis_tac[] 19QED 20 21Theorem FINITE_LIST_UNION[simp]: 22 FINITE (LIST_UNION sets) ��� ���s. MEM s sets ��� FINITE s 23Proof 24 Induct_on ���sets��� >> simp[] >> metis_tac[] 25QED 26 27Datatype: term = V num | Fn num (term list) 28End 29 30val term_size_def = DB.fetch "-" "term_size_def" 31val _ = export_rewrites ["term_size_def"] 32 33Theorem term_size_lemma[simp]: 34 ���x l a. MEM a l ��� term_size a < 1 + (x + term1_size l) 35Proof 36 rpt gen_tac >> Induct_on ���l��� >> simp[] >> rpt strip_tac >> simp[] >> 37 res_tac >> simp[] 38QED 39 40Theorem term_induct: 41 ���P. (���v. P (V v)) ��� (���n ts. (���t. MEM t ts ��� P t) ��� P (Fn n ts)) ��� 42 ���t. P t 43Proof 44 rpt strip_tac >> 45 qspecl_then [���P���, �����ts. ���t. MEM t ts ��� P t���] 46 (assume_tac o SIMP_RULE bool_ss []) 47 (TypeBase.induction_of ���:term���) >> rfs[] >> 48 fs[DISJ_IMP_THM, FORALL_AND_THM] 49QED 50 51val _ = TypeBase.update_induction term_induct 52 53Definition tswap_def[simp]: 54 (tswap x y (V v) = if v = x then V y else if v = y then V x else V v) ��� 55 (tswap x y (Fn f ts) = Fn f (MAP (tswap x y) ts)) 56Termination 57 WF_REL_TAC ���measure (term_size o SND o SND)��� >> simp[] 58End 59 60Definition FVT_def[simp]: 61 (FVT (V v) = {v}) ��� 62 (FVT (Fn s ts) = LIST_UNION (MAP FVT ts)) 63Termination 64 WF_REL_TAC ���measure term_size��� >> simp[] 65End 66 67Theorem FVT_FINITE[simp]: 68 ���t. FINITE (FVT t) 69Proof 70 ho_match_mp_tac term_induct >> simp[MEM_MAP, PULL_EXISTS] 71QED 72 73Theorem tswap_inv[simp]: 74 ���t. tswap x y (tswap x y t) = t 75Proof 76 ho_match_mp_tac term_induct >> rw[] >> simp[MAP_MAP_o, Cong MAP_CONG'] 77QED 78 79Theorem tswap_id[simp]: 80 ���t. tswap x x t = t 81Proof 82 ho_match_mp_tac term_induct >> rw[] >> simp[MAP_MAP_o, Cong MAP_CONG'] 83QED 84 85Theorem tswap_supp_id[simp]: 86 ���t. x ��� FVT t ��� y ��� FVT t ��� (tswap x y t = t) 87Proof 88 ho_match_mp_tac term_induct >> rw[] >> fs[MAP_MAP_o, MEM_MAP] >> 89 simp[LIST_EQ_REWRITE, EL_MAP] >> rw[] >> first_x_assum irule >> 90 metis_tac[MEM_EL] 91QED 92 93Definition termsubst_def[simp]: 94 (termsubst v (V x) = v x) ��� 95 (termsubst v (Fn f l) = Fn f (MAP (termsubst v) l)) 96Termination 97 WF_REL_TAC ���measure (term_size o SND)��� >> simp[] 98End 99 100Theorem termsubst_termsubst: 101 ���t i j. termsubst j (termsubst i t) = termsubst (termsubst j o i) t 102Proof 103 ho_match_mp_tac term_induct >> 104 simp[MAP_MAP_o, combinTheory.o_ABS_R, Cong MAP_CONG'] 105QED 106 107Theorem termsubst_triv[simp]: 108 ���t. termsubst V t = t 109Proof 110 ho_match_mp_tac term_induct >> simp[Cong MAP_CONG'] 111QED 112 113Theorem termsubst_valuation: 114 ���t v1 v2. (���x. x ��� FVT t ��� (v1 x = v2 x)) ��� (termsubst v1 t = termsubst v2 t) 115Proof 116 ho_match_mp_tac term_induct >> simp[MEM_MAP, PULL_EXISTS] >> rpt strip_tac >> 117 irule MAP_CONG' >> simp[] >> rpt strip_tac >> first_x_assum irule >> 118 metis_tac[] 119QED 120 121Theorem termsubst_fvt: 122 ���t i. FVT (termsubst i t) = { x | ���y. y ��� FVT t ��� x ��� FVT (i y) } 123Proof 124 ho_match_mp_tac term_induct >> 125 simp[MAP_MAP_o, combinTheory.o_ABS_R, MEM_MAP, PULL_EXISTS] >> rpt strip_tac>> 126 simp[Once EXTENSION,MEM_MAP,PULL_EXISTS] >> csimp[] >> metis_tac[] 127QED 128 129Theorem freshsubst_tswap: 130 ���t. y ��� FVT t ��� (termsubst V��� x ��� V y ��� t = tswap x y t) 131Proof 132 ho_match_mp_tac term_induct >> simp[MEM_MAP,combinTheory.APPLY_UPDATE_THM] >> 133 rpt strip_tac >- (COND_CASES_TAC >> fs[]) >> 134 irule MAP_CONG' >> simp[] >> metis_tac[] 135QED 136 137Datatype: 138 form = False 139 | Pred num (term list) 140 | IMP form form 141 | FALL num form 142End 143 144Definition Not_def: 145 Not f = IMP f False 146End 147 148Definition True_def: 149 True = Not False 150End 151 152Definition Or_def: 153 Or p q = IMP (IMP p q) q 154End 155 156Definition And_def: 157 And p q = Not (Or (Not p) (Not q)) 158End 159 160Definition Iff_def: 161 Iff p q = And (IMP p q) (IMP q p) 162End 163 164Definition Exists_def: 165 Exists x p = Not (FALL x (Not p)) 166End 167 168Definition term_functions_def[simp]: 169 (term_functions (V v) = ���) ��� 170 (term_functions (Fn f args) = 171 (f, LENGTH args) INSERT LIST_UNION (MAP term_functions args)) 172Termination 173 WF_REL_TAC ���measure term_size��� >> simp[] 174End 175 176Definition form_functions_def[simp]: 177 (form_functions False = ���) ��� 178 (form_functions (Pred n ts) = LIST_UNION (MAP term_functions ts)) ��� 179 (form_functions (IMP f1 f2) = form_functions f1 ��� form_functions f2) ��� 180 (form_functions (FALL x f) = form_functions f) 181End 182 183Definition form_predicates[simp]: 184 (form_predicates False = ���) ��� 185 (form_predicates (Pred n ts) = {(n,LENGTH ts)}) ��� 186 (form_predicates (IMP f1 f2) = form_predicates f1 ��� form_predicates f2) ��� 187 (form_predicates (FALL x f) = form_predicates f) 188End 189 190Theorem form_functions_Exists[simp]: 191 form_functions (Exists x p) = form_functions p 192Proof 193 simp[Exists_def, Not_def] 194QED 195 196Theorem form_predicates_Exists[simp]: 197 form_predicates (Exists x p) = form_predicates p 198Proof 199 simp[Exists_def, Not_def] 200QED 201 202Definition functions_def: 203 functions fms = BIGUNION{form_functions f | f ��� fms} 204End 205 206Definition predicates_def: 207 predicates fms = BIGUNION {form_predicates f | f ��� fms} 208End 209 210Definition language_def: 211 language fms = (functions fms, predicates fms) 212End 213 214Theorem functions_SING[simp]: 215 functions {f} = form_functions f 216Proof 217 simp[functions_def, Once EXTENSION] 218QED 219 220Theorem language_SING: 221 language {p} = (form_functions p, form_predicates p) 222Proof 223 simp[functions_def, language_def, predicates_def] >> simp[Once EXTENSION] 224QED 225 226Definition FV_def[simp]: 227 (FV False = ���) ��� 228 (FV (Pred _ ts) = LIST_UNION (MAP FVT ts)) ��� 229 (FV (IMP f1 f2) = FV f1 ��� FV f2) ��� 230 (FV (FALL x f) = FV f DELETE x) 231End 232 233Theorem FV_extras[simp]: 234 (FV True = ���) ��� 235 (FV (Not p) = FV p) ��� 236 (FV (And p q) = FV p ��� FV q) ��� 237 (FV (Or p q) = FV p ��� FV q) ��� 238 (FV (Iff p q) = FV p ��� FV q) ��� 239 (FV (Exists x p) = FV p DELETE x) 240Proof 241 simp[Exists_def, And_def, Or_def, Iff_def, True_def, Not_def] >> 242 simp[EXTENSION] >> metis_tac[] 243QED 244 245Theorem language_FALL[simp]: 246 language {FALL x p} = language {p} 247Proof 248 simp[language_def, predicates_def, EXTENSION] 249QED 250 251Theorem language_Exists[simp]: 252 language {Exists x p} = language {p} 253Proof 254 simp[language_def, predicates_def, EXTENSION, Exists_def, Not_def] 255QED 256 257Definition BV_def[simp]: 258 (BV False = ���) ��� 259 (BV (Pred _ _) = ���) ��� 260 (BV (IMP f1 f2) = BV f1 ��� BV f2) ��� 261 (BV (FALL x f) = x INSERT BV f) 262End 263 264Theorem FV_FINITE[simp]: 265 ���f. FINITE (FV f) 266Proof 267 Induct >> simp[MEM_MAP,PULL_EXISTS] 268QED 269 270Theorem BV_FINITE[simp]: 271 ���f. FINITE (BV f) 272Proof 273 Induct >> simp[] 274QED 275 276Definition VARIANT_def : 277 VARIANT s = MAX_SET s + 1 278End 279 280Theorem VARIANT_FINITE: 281 ���s. FINITE s ��� VARIANT s ��� s 282Proof 283 simp[VARIANT_def] >> rpt strip_tac >> drule_all in_max_set >> simp[] 284QED 285 286Theorem VARIANT_THM[simp]: 287 VARIANT (FV t) ��� FV t 288Proof 289 simp[VARIANT_FINITE] 290QED 291 292Definition formsubst_def[simp]: 293 (formsubst v False = False) ��� 294 (formsubst v (Pred p l) = Pred p (MAP (termsubst v) l)) ��� 295 (formsubst v (IMP f1 f2) = IMP (formsubst v f1) (formsubst v f2)) ��� 296 (formsubst v (FALL u f) = 297 let v' = v��� u ��� V u ��� ; 298 z = if ���y. y ��� FV (FALL u f) ��� u ��� FVT (v' y) then 299 VARIANT (FV (formsubst v' f)) 300 else u 301 in 302 FALL z (formsubst v��� u ��� V z ��� f)) 303End 304 305Theorem formsubst_triv[simp]: 306 formsubst V p = p 307Proof 308 Induct_on ���p��� >> simp[Cong MAP_CONG', combinTheory.APPLY_UPDATE_ID] 309QED 310 311Theorem formsubst_valuation: 312 ���v1 v2. (���x. x ��� FV p ��� (v1 x = v2 x)) ��� (formsubst v1 p = formsubst v2 p) 313Proof 314 Induct_on ���p��� >> simp[MEM_MAP, PULL_EXISTS, Cong MAP_CONG'] 315 >- (rw[] >> irule MAP_CONG' >> simp[] >> metis_tac[termsubst_valuation]) >> 316 csimp[combinTheory.UPDATE_APPLY] >> rpt gen_tac >> strip_tac >> 317 reverse COND_CASES_TAC >> simp[] 318 >- (first_x_assum irule >> simp[combinTheory.APPLY_UPDATE_THM]) >> 319 rename [���VARIANT (FV (formsubst v1��� k ��� V k��� form))���] >> 320 ���formsubst v1���k ��� V k��� form = formsubst v2���k ��� V k��� form��� 321 by (first_x_assum irule >> simp[combinTheory.APPLY_UPDATE_THM]) >> 322 simp[] >> 323 first_x_assum irule >> simp[combinTheory.APPLY_UPDATE_THM] 324QED 325 326Theorem formsubst_FV : 327 ���i. FV (formsubst i p) = { x | ���y. y ��� FV p ��� x ��� FVT (i y) } 328Proof 329 Induct_on ���p��� >> 330 simp[MEM_MAP, PULL_EXISTS, MAP_MAP_o, Cong MAP_CONG', termsubst_fvt] 331 >- (simp[Once EXTENSION, MEM_MAP, PULL_EXISTS] >> metis_tac[]) 332 >- (simp[Once EXTENSION] >> metis_tac[]) >> 333 csimp[combinTheory.UPDATE_APPLY] >> rpt gen_tac >> 334 reverse COND_CASES_TAC 335 >- (simp[Once EXTENSION] >> fs[] >> 336 simp[combinTheory.APPLY_UPDATE_THM] >> qx_gen_tac ���u��� >> eq_tac >> 337 simp[PULL_EXISTS] >> qx_gen_tac ���v��� >- (rw[] >> metis_tac[]) >> 338 metis_tac[]) >> 339 simp[Once EXTENSION, EQ_IMP_THM, PULL_EXISTS, FORALL_AND_THM] >> 340 qmatch_goalsub_abbrev_tac ���i ��� n ��� V var������ >> rw[] 341 >- (rename [���x ��� FVT (i ��� n ��� V var ��� y)���] >> 342 ���y ��� n��� by (strip_tac >> fs[combinTheory.UPDATE_APPLY]) >> 343 fs[combinTheory.UPDATE_APPLY] >> metis_tac[]) >> 344 asm_simp_tac (srw_ss() ++ boolSimps.CONJ_ss ++ boolSimps.COND_elim_ss) 345 [combinTheory.APPLY_UPDATE_THM] >> 346 simp[GSYM PULL_EXISTS] >> conj_tac >- metis_tac[] >> 347 simp[Abbr���var���] >> 348 last_assum (fn th => REWRITE_TAC [GSYM th]) >> 349 qmatch_abbrev_tac���x <> VARIANT (FV f)��� >> 350 ���x ��� FV f��� suffices_by metis_tac[VARIANT_THM] >> 351 simp[Abbr���f���] >> metis_tac[combinTheory.APPLY_UPDATE_THM] 352QED 353 354Theorem VARIANT_NOTIN_SUBSET: 355 FINITE s ��� t ��� s ��� VARIANT s ��� t 356Proof 357 simp[VARIANT_def] >> strip_tac >> DEEP_INTRO_TAC MAX_SET_ELIM >> simp[] >> 358 rw[] >> fs[] >> metis_tac [DECIDE ���~(x + 1 ��� x)���, SUBSET_DEF] 359QED 360 361Theorem formsubst_rename: 362 FV (formsubst V��� x ��� V y��� p) DELETE y = (FV p DELETE x) DELETE y 363Proof 364 simp_tac (srw_ss() ++ boolSimps.COND_elim_ss ++ boolSimps.CONJ_ss) 365 [formsubst_FV, EXTENSION, combinTheory.APPLY_UPDATE_THM] >> 366 metis_tac[] 367QED 368 369Theorem term_functions_termsubst: 370 ���t i. term_functions (termsubst i t) = 371 term_functions t ��� { x | ���y. y ��� FVT t ��� x ��� term_functions (i y) } 372Proof 373 ho_match_mp_tac term_induct >> 374 simp[MAP_MAP_o, combinTheory.o_ABS_R, MEM_MAP, PULL_EXISTS, Cong MAP_CONG'] >> 375 rpt strip_tac >> simp[Once EXTENSION] >> simp[MEM_MAP, PULL_EXISTS] >> 376 metis_tac[] 377QED 378 379Theorem form_functions_formsubst: 380 ���i. form_functions (formsubst i p) = 381 form_functions p ��� { x | ���y. y ��� FV p ��� x ��� term_functions (i y) } 382Proof 383 Induct_on ���p��� >> 384 simp[MAP_MAP_o, combinTheory.o_ABS_R, Cong MAP_CONG', 385 term_functions_termsubst, MEM_MAP, PULL_EXISTS] 386 >- (simp[Once EXTENSION,MEM_MAP, PULL_EXISTS] >> metis_tac[]) 387 >- (simp[Once EXTENSION] >> metis_tac[]) 388 >- (csimp[combinTheory.APPLY_UPDATE_THM] >> 389 simp_tac (srw_ss() ++ boolSimps.COND_elim_ss ++ boolSimps.CONJ_ss) [] >> 390 simp[Once EXTENSION] >> metis_tac[]) 391QED 392 393 394Theorem form_functions_formsubst1[simp]: 395 x ��� FV p ��� 396 (form_functions (formsubst V��� x ��� t ��� p) = 397 form_functions p ��� term_functions t) 398Proof 399 simp_tac(srw_ss() ++ boolSimps.CONJ_ss ++ boolSimps.COND_elim_ss) 400 [combinTheory.APPLY_UPDATE_THM,form_functions_formsubst, 401 term_functions_termsubst] 402QED 403 404Theorem form_predicates_formsubst[simp]: 405 ���i. form_predicates (formsubst i p) = form_predicates p 406Proof Induct_on ���p��� >> simp[] 407QED 408 409Theorem formsubst_14b[simp]: 410 x ��� FV p ��� (formsubst V��� x ��� t ��� p = p) 411Proof 412 strip_tac >> 413 ���formsubst V���x ��� t��� p = formsubst V p��� suffices_by simp[] >> 414 irule formsubst_valuation >> 415 asm_simp_tac(srw_ss() ++ boolSimps.COND_elim_ss ++ boolSimps.CONJ_ss) 416 [combinTheory.APPLY_UPDATE_THM] 417QED 418 419Theorem formsubst_language_rename: 420 language {formsubst V��� x ��� V y ��� p} = language {p} 421Proof 422 simp[language_SING] >> Cases_on ���x ��� FV p��� >> simp[] 423QED 424 425(* show countability via G��delization *) 426Definition num_of_term_def[simp]: 427 num_of_term (V x) = 0 ��� x ��� 428 num_of_term (Fn f l) = 1 ��� (f ��� nlist_of (MAP num_of_term l)) 429Termination 430 WF_REL_TAC ���measure term_size��� >> simp[] 431End 432 433Theorem num_of_term_11[simp]: 434 ���t1 t2. num_of_term t1 = num_of_term t2 ��� t1 = t2 435Proof 436 Induct >> simp[] >> Cases_on ���t2��� >> 437 csimp[LIST_EQ_REWRITE, rich_listTheory.EL_MEM, EL_MAP] 438QED 439 440Definition term_of_num_def: 441 term_of_num n = @t. n = num_of_term t 442End 443 444Theorem TERM_OF_NUM[simp]: 445 term_of_num(num_of_term t) = t 446Proof 447 simp[term_of_num_def] 448QED 449 450Theorem countable_terms[simp]: 451 countable ����(:term) 452Proof 453 simp[countable_def, INJ_DEF] >> qexists_tac���num_of_term��� >> simp[] 454QED 455 456Theorem INFINITE_terms[simp]: 457 INFINITE ����(:term) 458Proof 459 simp[INFINITE_INJ_NOT_SURJ] >> qexists_tac �����t. Fn 0 [t]��� >> 460 simp[INJ_DEF, SURJ_DEF] >> qexists_tac ���V 0��� >> simp[] 461QED 462 463Definition num_of_form_def[simp]: 464 num_of_form False = 0 ��� 0 ��� 465 num_of_form (Pred p l) = 1 ��� (p ��� nlist_of (MAP num_of_term l)) ��� 466 num_of_form (IMP p1 p2) = 2 ��� (num_of_form p1 ��� num_of_form p2) ��� 467 num_of_form (FALL x p) = 3 ��� (x ��� num_of_form p) 468End 469 470Theorem num_of_form_11[simp]: 471 ���p1 p2. num_of_form p1 = num_of_form p2 ��� p1 = p2 472Proof 473 Induct >> simp[] >> Cases_on ���p2��� >> simp[INJ_MAP_EQ_IFF, INJ_DEF] 474QED 475 476Theorem countable_forms[simp]: 477 countable ����(:form) 478Proof 479 simp[countable_def, INJ_DEF] >> qexists_tac���num_of_form��� >> simp[] 480QED 481 482Theorem INFINITE_forms[simp]: 483 INFINITE ����(:form) 484Proof 485 simp[INFINITE_INJ_NOT_SURJ] >> qexists_tac �����p. IMP p False��� >> 486 simp[INJ_DEF, SURJ_DEF] >> qexists_tac ���False��� >> simp[] 487QED 488 489Definition form_of_num_def: 490 form_of_num n = @f. num_of_form f = n 491End 492 493Theorem FORM_OF_NUM[simp]: 494 form_of_num (num_of_form p) = p 495Proof 496 simp[form_of_num_def] 497QED 498 499 500 501val _ = export_theory(); 502