1(* 2 3 fsubty ::= TyVar of string | Top | Fun of fsubty => fsubty 4 | ForallTy of string => fsubty => fsubty 5 6 where the string in ForallTy binds in the second fsubty argument, but 7 not the first 8 9 Inductively characterise a subset of the lambda calculus terms that 10 can stand in for these types. The encoding is 11 12 CON T --> Top 13 CON F @@ t @@ LAM v t' --> ForallTy v t t' 14 VAR s --> TyVar s 15 t @@ u --> Fun t u 16 17 This theory establishes the type, along with swap functions for the type 18 and the type of "contexts", which are of type (string * type) list 19 20*) 21 22open HolKernel boolLib Parse 23 24open binderLib bossLib metisLib BasicProvers boolSimps 25 26val SUBSET_DEF = pred_setTheory.SUBSET_DEF 27 28val _ = new_theory "fsubtypes" 29 30(* establish the inductive characterisation of the encoding above *) 31val (fsubrep_rules, fsubrep_ind, fsubrep_cases) = Hol_reln` 32 fsubrep (CON T) /\ 33 (!v t t'. fsubrep t /\ fsubrep t' ==> fsubrep (CON F @@ t @@ LAM v t')) /\ 34 (!s. fsubrep (VAR s)) /\ 35 (!t u. fsubrep t /\ fsubrep u ==> fsubrep (t @@ u)) 36`; 37 38val strong_fsubrep_ind = save_thm( 39 "strong_fsubrep_ind", 40 IndDefLib.derive_strong_induction (fsubrep_rules, fsubrep_ind)); 41 42(* because this is not obviously non-overlapping, we need to prove that 43 certain patterns aren't in fsubrep by induction *) 44 45val lam_not_fsubrep0 = prove( 46 ``!t0. fsubrep t0 ==> !v t. (t0 = LAM v t) ==> F``, 47 HO_MATCH_MP_TAC fsubrep_ind THEN SRW_TAC [][]); 48val lam_not_fsubrep = save_thm( 49 "lam_not_fsubrep", 50 SIMP_RULE (srw_ss() ++ DNF_ss) [] lam_not_fsubrep0) 51val _ = export_rewrites ["lam_not_fsubrep"] 52 53val CONF_not_fsubrep = store_thm( 54 "CONF_not_fsubrep", 55 ``~(fsubrep (CON F))``, 56 ONCE_REWRITE_TAC [fsubrep_cases] THEN SRW_TAC [][]); 57val _ = export_rewrites ["CONF_not_fsubrep"] 58 59(* type can be established by showing that fsubrep is non-empty; CON T is 60 the witness *) 61val fsubty_def = new_type_definition ( 62 "fsubty", 63 prove(``?x. fsubrep x``, Q.EXISTS_TAC `CON T` THEN 64 SRW_TAC [][fsubrep_rules]) 65); 66 67val bijections_exist = 68 define_new_type_bijections {name = "bijections_exist", 69 ABS = "term2fsubty", 70 REP = "fsubty2term", 71 tyax = fsubty_def}; 72 73(* obvious facts about the bijections *) 74val fsubty2term_11 = store_thm( 75 "fsubty2term_11", 76 ``(fsubty2term ty1 = fsubty2term ty2) = (ty1 = ty2)``, 77 SRW_TAC [][EQ_IMP_THM] THEN 78 METIS_TAC [bijections_exist]); 79val _ = export_rewrites ["fsubty2term_11"] 80 81val term2fsubty_11 = store_thm( 82 "term2fsubty_11", 83 ``fsubrep t1 /\ fsubrep t2 ==> 84 ((term2fsubty t1 = term2fsubty t2) = (t1 = t2))``, 85 SRW_TAC [][EQ_IMP_THM] THEN METIS_TAC [bijections_exist]); 86 87val fsubrep_fsubty2term = store_thm( 88 "fsubrep_fsubty2term", 89 ``fsubrep (fsubty2term ty1)``, 90 METIS_TAC [bijections_exist]); 91val _ = export_rewrites ["fsubrep_fsubty2term"] 92 93 94(* define constructors *) 95val Top_def = Define`Top = term2fsubty (CON T)`; 96val TyVar_def = Define`TyVar s = term2fsubty (VAR s)`; 97val Fun_def = Define` 98 Fun ty1 ty2 = term2fsubty (fsubty2term ty1 @@ fsubty2term ty2) 99`; 100val ForallTy_def = Define` 101 ForallTy v boundty ty = 102 term2fsubty (CON F @@ fsubty2term boundty @@ LAM v (fsubty2term ty)) 103`; 104 105(* prove injectivity for the non-binder constructors *) 106val Fun_11 = store_thm( 107 "Fun_11", 108 ``(Fun ty1 ty2 = Fun ty3 ty4) = (ty1 = ty3) /\ (ty2 = ty4)``, 109 SIMP_TAC (srw_ss()) [Fun_def, EQ_IMP_THM, fsubrep_rules, term2fsubty_11]); 110val _ = export_rewrites ["Fun_11"] 111 112val TyVar_11 = store_thm( 113 "TyVar_11", 114 ``(TyVar s1 = TyVar s2) = (s1 = s2)``, 115 SIMP_TAC (srw_ss()) [TyVar_def, fsubrep_rules, term2fsubty_11]); 116val _ = export_rewrites ["TyVar_11"] 117 118(* prove distinctness *) 119val fsubty_distinct = store_thm( 120 "fsubty_distinct", 121 ``~(Top = TyVar s) /\ ~(Top = Fun ty1 ty2) /\ ~(Top = ForallTy v bnd ty) /\ 122 ~(TyVar s = Fun ty1 ty2) /\ ~(TyVar s = ForallTy v bnd ty) /\ 123 ~(Fun ty1 ty2 = ForallTy v bnd ty)``, 124 SRW_TAC [][Top_def, TyVar_def, Fun_def, ForallTy_def, 125 fsubrep_rules, term2fsubty_11] THEN 126 DISJ2_TAC THEN STRIP_TAC THEN 127 POP_ASSUM (MP_TAC o Q.AP_TERM `fsubrep`) THEN 128 SRW_TAC [][]); 129val _ = export_rewrites ["fsubty_distinct"] 130 131val forall_fsubty = prove( 132 ``(!ty. P ty) = (!t. fsubrep t ==> P (term2fsubty t))``, 133 SRW_TAC [][EQ_IMP_THM] THEN 134 `?t. (ty = term2fsubty t) /\ fsubrep t` 135 by METIS_TAC [bijections_exist] THEN 136 METIS_TAC []); 137 138val rep_abs_lemma = prove( 139 ``fsubrep t ==> (fsubty2term (term2fsubty t) = t)``, 140 METIS_TAC [bijections_exist]) 141 142(* induction principle *) 143val fsubty_ind = store_thm( 144 "fsubty_ind", 145 ``!P. 146 P Top /\ 147 (!ty1 ty2. P ty1 /\ P ty2 ==> P (Fun ty1 ty2)) /\ 148 (!s. P (TyVar s)) /\ 149 (!v bnd ty. P bnd /\ P ty ==> P (ForallTy v bnd ty)) ==> 150 !ty. P ty``, 151 SIMP_TAC (srw_ss()) 152 [forall_fsubty, Top_def, TyVar_def, Fun_def, ForallTy_def, 153 rep_abs_lemma] THEN 154 GEN_TAC THEN STRIP_TAC THEN 155 HO_MATCH_MP_TAC strong_fsubrep_ind THEN 156 METIS_TAC []); 157 158(* definition of swap *) 159val fswap_def = Define` 160 fswap x y ty = term2fsubty (swap x y (fsubty2term ty)) 161`; 162 163val fsubrep_swap = store_thm( 164 "fsubrep_swap", 165 ``!t. fsubrep t ==> !x y. fsubrep (swap x y t)``, 166 HO_MATCH_MP_TAC fsubrep_ind THEN 167 SRW_TAC [][swapTheory.swap_thm, fsubrep_rules]); 168 169val fswap_thm = store_thm( 170 "fswap_thm", 171 ``(!s. fswap x y (TyVar s) = TyVar (swapstr x y s)) /\ 172 (!ty1 ty2. fswap x y (Fun ty1 ty2) = 173 Fun (fswap x y ty1) (fswap x y ty2)) /\ 174 (fswap x y Top = Top) /\ 175 (!v bnd ty. fswap x y (ForallTy v bnd ty) = 176 ForallTy (swapstr x y v) (fswap x y bnd) (fswap x y ty))``, 177 SRW_TAC [][fswap_def, Top_def, ForallTy_def, Fun_def, TyVar_def, 178 rep_abs_lemma, fsubrep_rules, swapTheory.swap_thm, 179 fsubrep_swap]); 180val _ = export_rewrites ["fswap_thm"] 181 182val fswap_inv = store_thm( 183 "fswap_inv", 184 ``!ty x y. fswap x y (fswap x y ty) = ty``, 185 HO_MATCH_MP_TAC fsubty_ind THEN SRW_TAC [][]); 186val _ = export_rewrites ["fswap_inv"] 187 188val fswap_id = store_thm( 189 "fswap_id", 190 ``fswap x x ty = ty``, 191 SRW_TAC [][fswap_def, bijections_exist]); 192val _ = export_rewrites ["fswap_id"] 193 194val fswap_comm = store_thm( 195 "fswap_comm", 196 ``fswap y x = fswap x y``, 197 SRW_TAC [][FUN_EQ_THM, fswap_def, swapTheory.swap_comm]); 198val _ = export_rewrites ["fswap_comm"] 199 200(* define swap over contexts *) 201val ctxtswap_def = Define` 202 (ctxtswap x y [] = []) /\ 203 (ctxtswap x y (h::t) = (swapstr x y (FST h), fswap x y (SND h)) :: 204 ctxtswap x y t) 205`; 206val _ = export_rewrites ["ctxtswap_def"] 207 208val ctxtswap_inv = store_thm( 209 "ctxtswap_inv", 210 ``!G x y. ctxtswap x y (ctxtswap x y G) = G``, 211 Induct THEN SRW_TAC [][]); 212val _ = export_rewrites ["ctxtswap_inv"] 213 214val ctxtswap_id = store_thm( 215 "ctxtswap_id", 216 ``!G x y. ctxtswap x x G = G``, 217 Induct THEN SRW_TAC [][ctxtswap_def]); 218val _ = export_rewrites ["ctxtswap_id"] 219 220val MEM_ctxtswap = store_thm( 221 "MEM_ctxtswap", 222 ``!G x y v ty. MEM (v,ty) (ctxtswap x y G) = 223 MEM (swapstr x y v, fswap x y ty) G``, 224 Induct THEN ASM_SIMP_TAC (srw_ss()) [pairTheory.FORALL_PROD] THEN 225 METIS_TAC [fswap_inv]); 226val _ = export_rewrites ["MEM_ctxtswap"] 227 228val cdom_def = Define` 229 (cdom ([]: (string # fsubty) list) = {}) /\ 230 (cdom (h::t) = FST h INSERT cdom t) 231`; 232val _ = export_rewrites ["cdom_def"] 233 234val FINITE_cdom = store_thm( 235 "FINITE_cdom", 236 ``!G. FINITE (cdom G)``, 237 Induct THEN SRW_TAC [][]); 238val _ = export_rewrites ["FINITE_cdom"] 239 240val cdom_MEM = store_thm( 241 "cdom_MEM", 242 ``x IN cdom G = ?ty. MEM (x,ty) G``, 243 Induct_on `G` THEN ASM_SIMP_TAC (srw_ss()) [pairTheory.FORALL_PROD] THEN 244 METIS_TAC []); 245 246(* define fv for types *) 247val ftyFV_def = Define` 248 ftyFV ty = FV (fsubty2term ty) 249`; 250 251val ftyFV_thm = store_thm( 252 "ftyFV_thm", 253 ``(ftyFV Top = {}) /\ 254 (ftyFV (Fun ty1 ty2) = ftyFV ty1 UNION ftyFV ty2) /\ 255 (ftyFV (TyVar s) = {s}) /\ 256 (ftyFV (ForallTy v bnd ty) = ftyFV bnd UNION (ftyFV ty DELETE v))``, 257 SRW_TAC [][ftyFV_def, Top_def, Fun_def, ForallTy_def, TyVar_def, 258 rep_abs_lemma, fsubrep_rules]); 259val _ = export_rewrites ["ftyFV_thm"] 260 261(* the following is not really an injectivity result, but it seems the best 262 possible for ForallTy *) 263val ForallTy_11 = store_thm( 264 "ForallTy_11", 265 ``(ForallTy v1 bnd1 bod1 = ForallTy v2 bnd2 bod2) = 266 (bnd1 = bnd2) /\ ((v1 = v2) \/ ~(v1 IN ftyFV bod2)) /\ 267 (bod1 = fswap v1 v2 bod2)``, 268 SRW_TAC [][ftyFV_def, ftyFV_thm, fswap_def, ForallTy_def, 269 term2fsubty_11, fsubrep_rules, swapTheory.LAM_INJ_swap, 270 EQ_IMP_THM] THEN 271 ASM_SIMP_TAC (srw_ss()) [] THENL [ 272 FIRST_X_ASSUM (MP_TAC o Q.AP_TERM `term2fsubty`) THEN 273 SRW_TAC [][bijections_exist], 274 FIRST_X_ASSUM (MP_TAC o Q.AP_TERM `term2fsubty`) THEN 275 SRW_TAC [][bijections_exist], 276 SRW_TAC [][bijections_exist], 277 SRW_TAC [][rep_abs_lemma, fsubrep_fsubty2term, fsubrep_swap] 278 ]); 279 280val ForallTy_injectivity_lemma1 = store_thm( 281 "ForallTy_injectivity_lemma1", 282 ``(ForallTy x bnd1 ty1 = ForallTy y bnd2 ty2) ==> 283 (bnd1 = bnd2) /\ (ty2 = fswap x y ty1)``, 284 METIS_TAC [ForallTy_11, fswap_inv]); 285 286val ForallTy_INJ_ALPHA_FV = store_thm( 287 "ForallTy_INJ_ALPHA_FV", 288 ``(ForallTy x bnd ty1 = ForallTy y bnd ty2) /\ ~(x = y) ==> 289 ~(x IN ftyFV ty2) /\ ~(y IN ftyFV ty1)``, 290 METIS_TAC [ForallTy_11]); 291 292val ForallTy_ALPHA = store_thm( 293 "ForallTy_ALPHA", 294 ``~(u IN ftyFV ty) ==> 295 (ForallTy u bnd (fswap u v ty) = ForallTy v bnd ty)``, 296 METIS_TAC [ForallTy_11]); 297 298val fswap_fresh = store_thm( 299 "fswap_fresh", 300 ``!ty x y. ~(x IN ftyFV ty) /\ ~(y IN ftyFV ty) ==> 301 (fswap x y ty = ty)``, 302 SRW_TAC [][fswap_def, ftyFV_def, swapTheory.swap_identity, 303 bijections_exist]); 304 305val swapset_DELETE = store_thm( 306 "swapset_DELETE", 307 ``swapset x y (s1 DELETE s) = swapset x y s1 DELETE swapstr x y s``, 308 SRW_TAC [][swapTheory.swapset_def, pred_setTheory.EXTENSION]); 309 310val swapset_SUBSET = store_thm( 311 "swapset_SUBSET", 312 ``s1 SUBSET swapset x y s2 = swapset x y s1 SUBSET s2``, 313 SRW_TAC [][swapTheory.swapset_def, SUBSET_DEF] THEN 314 METIS_TAC [swapTheory.swapstr_inverse]); 315val _ = export_rewrites ["swapset_SUBSET"] 316 317val ftyFV_fswap = store_thm( 318 "ftyFV_fswap", 319 ``!ty x y. ftyFV (fswap x y ty) = swapset x y (ftyFV ty)``, 320 HO_MATCH_MP_TAC fsubty_ind THEN 321 SRW_TAC [][swapTheory.swapset_UNION, swapset_DELETE]); 322val _ = export_rewrites ["ftyFV_fswap"] 323 324val ftyFV_FINITE = store_thm( 325 "ftyFV_FINITE", 326 ``!ty. FINITE (ftyFV ty)``, 327 HO_MATCH_MP_TAC fsubty_ind THEN 328 SRW_TAC [][]); 329val _ = export_rewrites ["ftyFV_FINITE"] 330 331(* define FV for ctxts *) 332val ctxtFV_def = Define` 333 (ctxtFV [] = {}) /\ 334 (ctxtFV (h::t) = {FST h} UNION ftyFV (SND h) UNION ctxtFV t) 335`; 336val _ = export_rewrites ["ctxtFV_def"] 337 338val ctxtFV_ctxtswap = store_thm( 339 "ctxtFV_ctxtswap", 340 ``!G x y. ctxtFV (ctxtswap x y G) = swapset x y (ctxtFV G)``, 341 Induct THEN SRW_TAC [][swapTheory.swapset_UNION]); 342val _ = export_rewrites ["ctxtFV_ctxtswap"] 343 344val ctxtFV_FINITE = store_thm( 345 "ctxtFV_FINITE", 346 ``!G. FINITE (ctxtFV G)``, 347 Induct THEN SRW_TAC [][]); 348val _ = export_rewrites ["ctxtFV_FINITE"] 349 350val cdom_SUBSET_ctxtFV = store_thm( 351 "cdom_SUBSET_ctxtFV", 352 ``!G. cdom G SUBSET ctxtFV G``, 353 Induct THEN 354 FULL_SIMP_TAC (srw_ss()) [cdom_def, SUBSET_DEF] THEN 355 METIS_TAC []); 356 357val cdom_ctxtswap = store_thm( 358 "cdom_ctxtswap", 359 ``!G x y. cdom (ctxtswap x y G) = swapset x y (cdom G)``, 360 Induct THEN SRW_TAC[][]); 361val _ = export_rewrites ["cdom_ctxtswap"] 362 363val ctxtswap_fresh = store_thm( 364 "ctxtswap_fresh", 365 ``!G x y. 366 ~(x IN ctxtFV G) /\ ~(y IN ctxtFV G) ==> 367 (ctxtswap x y G = G)``, 368 Induct THEN SRW_TAC [][fswap_fresh]); 369 370(* wfctxt implements the restrictions defined on pp393-4 *) 371val wfctxt_def = Define` 372 (wfctxt [] = T) /\ 373 (wfctxt ((x,ty) :: t) = ~(x IN cdom t) /\ 374 ftyFV ty SUBSET cdom t /\ 375 wfctxt t) 376`; 377val _ = export_rewrites ["wfctxt_def"] 378 379val wfctxt_swap = store_thm( 380 "wfctxt_swap", 381 ``!G x y. wfctxt (ctxtswap x y G) = wfctxt G``, 382 Induct THEN ASM_SIMP_TAC (srw_ss()) [pairTheory.FORALL_PROD]); 383val _ = export_rewrites ["wfctxt_swap"] 384 385val wfctxt_ctxtFV_cdom = store_thm( 386 "wfctxt_ctxtFV_cdom", 387 ``!G. wfctxt G ==> (ctxtFV G = cdom G)``, 388 SIMP_TAC (srw_ss()) [pred_setTheory.EXTENSION] THEN 389 Induct THEN ASM_SIMP_TAC (srw_ss()) [pairTheory.FORALL_PROD, SUBSET_DEF] THEN 390 METIS_TAC []); 391 392val wfctxt_MEM = store_thm( 393 "wfctxt_MEM", 394 ``!G. wfctxt G /\ MEM (x,ty) G ==> 395 x IN cdom G /\ !y. y IN ftyFV ty ==> y IN cdom G``, 396 Induct THEN ASM_SIMP_TAC (srw_ss()) [pairTheory.FORALL_PROD, 397 SUBSET_DEF] THEN 398 METIS_TAC []); 399 400val fsize_def = Define` 401 fsize (t:fsubty) = size (fsubty2term t) 402`; 403 404val fsize_thm = store_thm( 405 "fsize_thm", 406 ``(fsize Top = 1) /\ 407 (fsize (TyVar s) = 1) /\ 408 (fsize (ForallTy x ty1 ty2) = fsize ty1 + fsize ty2 + 4) /\ 409 (fsize (Fun ty1 ty2) = fsize ty1 + fsize ty2 + 1)``, 410 SRW_TAC [numSimps.ARITH_ss] 411 [fsize_def,Fun_def,Top_def,ForallTy_def,TyVar_def, 412 rep_abs_lemma, fsubrep_rules, ncTheory.size_thm]); 413 414 415val _ = export_theory(); 416 417