1(* ===================================================================== *) 2(* FILE : barendregt.sml *) 3(* VERSION : 2.0 *) 4(* DESCRIPTION : Tactics for working with substitutions naively. *) 5(* *) 6(* AUTHOR : Peter Vincent Homeier *) 7(* DATE : May 30, 2004 *) 8(* COPYRIGHT : Copyright (c) 2004 by Peter Vincent Homeier *) 9(* *) 10(* ===================================================================== *) 11 12 13structure barendregt :> barendregt = 14struct 15 16open HolKernel Parse boolLib; 17infix THEN THENL THENC ORELSE ORELSEC THEN_TCL ORELSE_TCL ## |->; 18infixr -->; 19 20(* 21type term = Term.term 22type thm = Thm.thm; 23*) 24 25 26 27local 28 29 30(* In interactive sessions, do: 31 32app load ["pairTheory", 33 "listLib", "numTheory", "Num_induct", 34 "pred_setTheory", "pred_setLib", 35 "mutualLib", "ind_defLib", "bossLib", 36 "ind_rel", "dep_rewrite", 37 "more_listTheory", "more_setTheory", "variableTheory", 38 "termTheory", "alphaTheory", "liftTheory" 39 ]; 40 41*) 42 43 44open pred_setTheory more_setTheory; 45open listTheory; 46open liftTheory; 47open dep_rewrite; 48open Rsyntax; 49 50 51val LIST_INDUCT_TAC = 52 INDUCT_THEN list_induction ASSUME_TAC; 53 54val REWRITE_THM = fn th => REWRITE_TAC[th]; 55val UNDISCH_LAST_TAC = POP_ASSUM MP_TAC; 56 57fun REWRITE_ASSUM_TAC rths :tactic = 58 RULE_ASSUM_TAC (REWRITE_RULE rths); 59 60fun REWRITE_ALL_TAC rths :tactic = 61 REWRITE_TAC rths THEN 62 REWRITE_ASSUM_TAC rths; 63 64val REWRITE_ALL_THM = fn th => REWRITE_ALL_TAC[th]; 65 66 67val dict = ty_antiq( ==`:(string # method) list`== ); 68val entry = ty_antiq( ==`:string # method`== ); 69 70 71(* 72val (asl,gl) = top_goal(); 73*) 74 75 76fun TACTIC_ERR{function,message} = 77 Feedback.HOL_ERR{origin_structure = "Tactic", 78 origin_function = function, 79 message = message}; 80 81fun failwith function = 82 ( (* if debug_fail then 83 print_string ("Failure in Cond_rewrite: "^function^"\n") 84 else (); *) 85 raise TACTIC_ERR{function = function,message = ""}); 86 87 88fun mk_subst l = map (fn (residue:'a, redex:'b) => 89 {redex=redex,residue=residue}) l; 90val INST_TY_TERM = (Drule.INST_TY_TERM) o (mk_subst##mk_subst); 91fun dest_subst l = map (fn {residue,redex} => (residue:'a, redex:'b)) l; 92 93 94 95val get_shift_matches = (dest_subst##dest_subst) o 96 (Term.match_term ���SIGMA x a���); 97(* 98val get_shift_matches = Psyntax.match_term ���SIGMA x a���; 99*) 100 101(* SEARCH_matches applies the function f to every subterm of the 102 given term tm, except to variables or constants, for which 103 SEARCH_matches always raises an exception. 104 The return value is a list of 'a objects, as produced by f 105 for every subterm of tm, all collected into one list. 106*) 107fun SEARCH_matches (f:term->'a list) tm = 108 ( (* if debug_matches then (print_string "SEARCH_matches: "; 109 print_term tm; print_newline()) else (); *) 110 if is_comb tm then 111 (let val {Rator,Rand} = Rsyntax.dest_comb tm 112 val m1 = (f Rator handle _ => []) 113 val m2 = (f Rand handle _ => []) 114 in append m1 m2 115 end) 116 else 117 if is_abs tm then 118 let val {Bvar,Body} = Rsyntax.dest_abs tm in 119 (f Body handle _ => []) 120 end 121 else failwith "SEARCH_matches"); 122 123(* 124fun SUB_matches (f:term->'a) tm = 125 ( (* if debug_matches then (print_string "SUB_matches: "; 126 print_term tm; print_newline()) else (); *) 127 if is_comb tm then 128 (let val {Rator,Rand} = Rsyntax.dest_comb tm in 129 (f Rator handle _ => f Rand) 130 end) 131 else 132 if is_abs tm then 133 let val {Bvar,Body} = Rsyntax.dest_abs tm in 134 f Body 135 end 136 else failwith "SUB_matches"); 137 138fun ONCE_DEPTH_matches (f:term->'a) tm = 139 ( (* if debug_matches then 140 (print_string "ONCE_DEPTH_matches: "; print_term tm; print_newline()) 141 else (); *) 142 (f tm handle _ => (SUB_matches (ONCE_DEPTH_matches f) tm))); 143*) 144 145fun ALL_DEPTH_matches (f:term->'a) tm = 146 ( (* if debug_matches then 147 (print_string "ONCE_DEPTH_matches: "; print_term tm; print_newline()) 148 else (); *) 149 ([f tm] handle _ => (SEARCH_matches (ALL_DEPTH_matches f) tm))); 150 151 152fun remove_s_matches matches = 153 let val (terms_list,types_list) = matches; 154 val nsterms = filter (fn (f,s) => not (#Name(dest_var s) = "s")) 155 terms_list 156 in 157 (nsterms,([]:(hol_type * hol_type) list)) 158 end; 159 160 161(* ------------------------------------------------------------------ *) 162(* Need to group together matches which have the same "x" match; *) 163(* for each such group, we should compute a variant of the x once, *) 164(* and then use the same variant x' for each of the new shifted *) 165(* bodies of the SIGMA expressions. This ensures that SIGMA *) 166(* expressions which had identical bound variables before, still *) 167(* have identical bound variables afterwards. This is important. *) 168(* ------------------------------------------------------------------ *) 169 170fun find_x (match::matches) = 171 let val (l,r) = match in 172 if r = ���x:var��� then l else find_x matches 173 end 174 | find_x [] = ���x:var���; 175 176fun find_a (match::matches) = 177 let val (l,r) = match in 178 if r = ���a:obj��� then l else find_a matches 179 end 180 | find_a [] = ���a:obj���; 181 182fun sort_matches matchesl = 183 let val (mtermsl,_) = split matchesl 184 val xtms = map find_x mtermsl 185 val dist_xtms = mk_set xtms 186 val xs_termsl = zip xtms mtermsl 187 val xmgroups = map (fn dx => filter (fn (x,matches) => (x = dx)) 188 xs_termsl) 189 dist_xtms 190 val mgroups = map (map snd) xmgroups 191 val t's = map (map find_a) mgroups 192 val mtygroups = map (map (fn tms => 193 (tms, ([]:(hol_type * hol_type) list)))) 194 mgroups 195 val tmgroups = zip (zip dist_xtms t's) mtygroups 196 in 197 tmgroups 198 end; 199 200 201 202val EVERY_LENGTH_LEMMA = TAC_PROOF(([], 203 ���!os (a:'a) as. 204 (LENGTH os = LENGTH (CONS a as)) ==> 205 (?(o':'b) os'. (LENGTH os' = LENGTH as) /\ (os = CONS o' os'))���), 206 LIST_INDUCT_TAC 207 THEN REWRITE_TAC[LENGTH,arithmeticTheory.SUC_NOT] 208 THEN REWRITE_TAC[prim_recTheory.INV_SUC_EQ,CONS_11] 209 THEN REPEAT GEN_TAC THEN STRIP_TAC 210 THEN EXISTS_TAC ���h:'b��� 211 THEN EXISTS_TAC ���os:'b list��� 212 THEN ASM_REWRITE_TAC[] 213 ); 214 215val NIL_LENGTH_LEMMA = TAC_PROOF(([], 216 ���!os:'b list. 217 (LENGTH os = LENGTH ([]:'a list)) ==> 218 (os = [])���), 219 REWRITE_TAC[LENGTH,LENGTH_NIL] 220 ); 221 222fun REPEAT_N 0 tac = ALL_TAC 223 | REPEAT_N n tac = (tac THEN REPEAT_N (n-1) tac); 224 225 226 227fun make_new_objects thm = 228 let val cn = concl thm 229 val rhs = #rhs(dest_eq cn) 230 val lst = #Rand(dest_comb rhs) 231 fun length_list lst = 232 if lst = ���[]:obj list��� then 0 233 else 1 + length_list (#Rand(dest_comb lst)) 234 val n = length_list lst 235 fun make_one 0 thm = thm 236 | make_one n thm = thm 237 in 238 (make_one n thm; n) 239 end; 240 241 242(* 243fun MAKE_CLEAN_VAR_THM free_vrs matches = 244 let val (terms_list,types_list) = matches; 245 val ftm = foldr (fn (x,s) => 246 if type_of x = (==`:var`==) 247 then ���^x INSERT ^s��� 248 else if type_of x = (==`:var list`==) 249 then ���SL ^x UNION ^s��� 250 else if type_of x = (==`:var set`==) 251 then ���^x UNION ^s��� 252 else if type_of x = (==`:obj`==) 253 then ���(FV_obj ^x) UNION ^s��� 254 else if type_of x = (==`:(string # method) list`==) 255 then ���(FV_dict ^x) UNION ^s��� 256 else if type_of x = (==`:string # method`==) 257 then ���(FV_entry ^x) UNION ^s��� 258 else if type_of x = (==`:method`==) 259 then ���(FV_method ^x) UNION ^s��� 260 else s) 261 ���{}:var set��� 262 free_vrs; 263 val sterms = (ftm, ���s:var set���)::terms_list; 264 val smatches = (sterms,([]:(hol_type * hol_type) list)); 265 val sigma_thm = INST_TY_TERM smatches (SPEC_ALL SIGMA_CLEAN_VAR); 266 in 267 REWRITE_RULE[FINITE_EMPTY,FINITE_INSERT,FINITE_UNION, 268 FINITE_FV_object,IN,IN_UNION,DE_MORGAN_THM] 269 sigma_thm 270 end; 271*) 272 273 274fun MAKE_LIST_CLEAN_VAR_THM free_vrs (x, os) = 275 let val ftm = foldr (fn (x,s) => 276 if type_of x = (==`:var`==) 277 then ���^x INSERT ^s��� 278 else if type_of x = (==`:var list`==) 279 then ���SL ^x UNION ^s��� 280 else if type_of x = (==`:var set`==) 281 then ���^x UNION ^s��� 282 else if type_of x = (==`:obj`==) 283 then ���(FV_obj ^x) UNION ^s��� 284 else if type_of x = (==`:(string # method) list`==) 285 then ���(FV_dict ^x) UNION ^s��� 286 else if type_of x = (==`:string # method`==) 287 then ���(FV_entry ^x) UNION ^s��� 288 else if type_of x = (==`:method`==) 289 then ���(FV_method ^x) UNION ^s��� 290 else s) 291 ���{}:var set��� 292 free_vrs; 293 val mk_obj_list = foldr (fn (a,os) => ���CONS ^a ^os���) 294 ���[]:obj list��� 295 val os_tm = mk_obj_list os 296 val sigma_thm = SPECL[ftm,x,os_tm] SIGMA_LIST_CLEAN_VAR 297 val exists_list_thm = 298 REWRITE_RULE[FINITE_EMPTY,FINITE_INSERT,FINITE_UNION, 299 FINITE_FV_object,IN,IN_UNION,DE_MORGAN_THM] 300 sigma_thm 301 val os' = foldr (fn (v,l) => (Term.variant (l @ free_vrs) v)::l) 302 [] os 303 val os'_tm = mk_obj_list os' 304 val {Bvar=zvar, Body=body1} = dest_exists (concl exists_list_thm) 305 val {Rator=exists_binder, Rand=body2} = dest_comb body1 306 val os'_vr = #Bvar(dest_abs body2) 307 val exists_tm1 = beta_conv (mk_comb{Rator=body2, Rand=os'_tm}) 308 val exists_tm2 = foldr (fn (o1,tm) => mk_exists{Bvar=o1, Body=tm}) 309 exists_tm1 os' 310 val exists_tm = mk_exists{Bvar=zvar, Body=exists_tm2} 311 val exists_thm = TAC_PROOF (([],exists_tm), 312 STRIP_ASSUME_TAC exists_list_thm 313 THEN ASSUM_LIST (fn asl1 => 314 EXISTS_TAC (#Rand (dest_comb (#Rator(dest_comb 315 (#Rand(dest_comb (concl (hd (rev asl1)))))))))) 316 THEN REPEAT 317 (POP_ASSUM (fn lth => 318 STRIP_ASSUME_TAC (MATCH_MP EVERY_LENGTH_LEMMA lth)) 319 THEN FIRST_ASSUM (fn eth => 320 EXISTS_TAC 321 (#Rand (dest_comb (#Rator(dest_comb 322 (#rhs(dest_eq (concl eth)))))))) 323 THEN POP_ASSUM REWRITE_ALL_THM) 324 THEN POP_ASSUM (REWRITE_ALL_THM o MATCH_MP NIL_LENGTH_LEMMA) 325 THEN ASM_REWRITE_TAC[LENGTH] 326 ) 327 in 328 BETA_RULE (REWRITE_RULE[EVERY_DEF,MAP2,combinTheory.I_THM] exists_thm) 329 end; 330 331 332val MAKE_SIMPLE_SUBST_TAC = 333 DEP_REWRITE_TAC[SIGMA_SUBST_SIMPLE] 334 THEN CONJ_TAC 335 THENL 336 [ ASM_REWRITE_TAC[objectTheory.BV_subst_def,pairTheory.FST,IN] 337 THEN REPEAT (CHANGED_TAC 338 (ASM_REWRITE_TAC[IN_DIFF,IN,FV_object,FV_object_subst] 339 THEN DEP_REWRITE_TAC[NOT_IN_FV_subst])) 340 THEN ASM_REWRITE_TAC[], 341 342 ALL_TAC 343 ]; 344 345 346(* 347val SHIFT_SIGMA_TAC :tactic = fn (asl,gl) => 348 let val matches = ONCE_DEPTH_matches get_shift_matches gl; 349 val free_vrs = mk_set (append (free_vars gl) 350 (flatten (map free_vars asl))); 351 val sigma_thm = MAKE_CLEAN_VAR_THM free_vrs matches 352 in 353 (STRIP_ASSUME_TAC sigma_thm 354 THEN FIRST_ASSUM REWRITE_THM 355 THEN UNDISCH_LAST_TAC 356 THEN FIRST_ASSUM (fn hght => EVERY_ASSUM (fn th => 357 ASSUME_TAC (MATCH_MP th hght) 358 handle _ => ALL_TAC)) 359 THEN DISCH_TAC) (asl,gl) 360 end; 361*) 362 363val SHIFT_SIGMAS_TAC :tactic = fn (asl,gl) => 364 let val matchesl = mk_set (ALL_DEPTH_matches get_shift_matches gl); 365 val match_groups = sort_matches matchesl 366 val (tags,groups) = split match_groups 367 (* val (xs,bodies) = split tags *) 368 val free_vrs = mk_set (append (free_vars gl) 369 (flatten (map free_vars asl))); 370 val sigma_thms = map (MAKE_LIST_CLEAN_VAR_THM free_vrs) tags 371 val t_sigma_thms = zip tags sigma_thms 372 (* val sigma_thm = map (MAKE_CLEAN_VAR_THM free_vrs) matchesl *) 373 in 374 if matchesl = [] then 375 ONCE_REWRITE_TAC[SUB_object] (asl,gl) 376 else 377 (EVERY (map (fn ((x,os),sigma_thm) => 378 let val n = length os in 379 STRIP_ASSUME_TAC sigma_thm 380 THEN POP_ASSUM (fn th => ALL_TAC) 381 THEN REPEAT_N n 382 (FIRST_ASSUM REWRITE_THM THEN UNDISCH_LAST_TAC) 383 THEN REPEAT_N n UNDISCH_LAST_TAC (* the HEIGHT = HEIGHT asms *) 384 THEN REPEAT_N n 385 (DISCH_THEN (fn hght => 386 EVERY_ASSUM (fn th => 387 ASSUME_TAC (MATCH_MP th hght) 388 handle _ => ALL_TAC) 389 THEN ASSUME_TAC hght)) 390 THEN REPEAT_N n DISCH_TAC 391 end) 392 t_sigma_thms) 393 THEN MAKE_SIMPLE_SUBST_TAC) 394 (* above is tactic, applied to: *) 395 (asl,gl) 396 end; 397 398 399(* ================================================================== *) 400(* End of local declarations. *) 401(* Beginning of exported declarations. *) 402(* ================================================================== *) 403 404in 405 406(* 407val SHIFT_SIGMAS_TAC = SHIFT_SIGMAS_TAC; 408*) 409 410val MAKE_SIMPLE_SUBST_TAC = MAKE_SIMPLE_SUBST_TAC; 411 412val SIMPLE_SUBST_TAC = 413 SHIFT_SIGMAS_TAC; 414 415 416end (* of local declaration block *) 417 418end; (* of structure barendregt *) 419 420 421(* TEST EXAMPLES: 422 423load "MutualIndThen"; 424open MutualIndThen; 425 426(* Barendregt's Substitution Lemma, 2.1.16, page 27: *) 427 428val BARENDREGHT_SUBSTITUTION_LEMMA = TAC_PROOF 429 (([], 430 ���(!M N L x y. 431 ~(x = y) /\ ~(x IN FV_obj L) ==> 432 (((M <[ [x,N]) <[ [y,L]) = 433 ((M <[ [y,L]) <[ [x, (N <[ [y,L])]))) /\ 434 (!M N L x y. 435 ~(x = y) /\ ~(x IN FV_obj L) ==> 436 (((M <[ [x,N]) <[ [y,L]) = 437 ((M <[ [y,L]) <[ [x, (N <[ [y,L])]))) /\ 438 (!M N L x y. 439 ~(x = y) /\ ~(x IN FV_obj L) ==> 440 (((M <[ [x,N]) <[ [y,L]) = 441 ((M <[ [y,L]) <[ [x, (N <[ [y,L])]))) /\ 442 (!M N L x y. 443 ~(x = y) /\ ~(x IN FV_obj L) ==> 444 (((M <[ [x,N]) <[ [y,L]) = 445 ((M <[ [y,L]) <[ [x, (N <[ [y,L])])))���), 446 MUTUAL_INDUCT_THEN object_height_induct ASSUME_TAC 447 THENL 448 [ REPEAT STRIP_TAC 449 THEN REWRITE_TAC[SUB_object,SUB] 450 THEN COND_CASES_TAC 451 THENL 452 [ POP_ASSUM REWRITE_ALL_THM 453 THEN EVERY_ASSUM (REWRITE_THM o GSYM) 454 THEN REWRITE_TAC[SUB_object,SUB], 455 456 REWRITE_TAC[SUB_object,SUB] 457 THEN COND_CASES_TAC 458 THENL 459 [ IMP_RES_THEN REWRITE_THM subst_EMPTY, 460 461 ASM_REWRITE_TAC[SUB_object,SUB] 462 ] 463 ], 464 465 REPEAT STRIP_TAC 466 THEN RES_TAC 467 THEN ASM_REWRITE_TAC[SUB_object], 468 469 REPEAT STRIP_TAC 470 THEN RES_TAC 471 THEN ASM_REWRITE_TAC[SUB_object], 472 473 REPEAT STRIP_TAC 474 THEN RES_TAC 475 THEN ASM_REWRITE_TAC[SUB_object], 476 477 REPEAT STRIP_TAC 478 THEN RES_TAC 479 THEN ASM_REWRITE_TAC[SUB_object], 480 481 REPEAT STRIP_TAC 482 THEN RES_TAC 483 THEN ASM_REWRITE_TAC[SUB_object], 484 485 REPEAT STRIP_TAC 486 THEN RES_TAC 487 THEN ASM_REWRITE_TAC[SUB_object], 488 489 REPEAT STRIP_TAC 490 THEN SHIFT_SIGMAS_TAC 491 THEN MAKE_SIMPLE_SUBST_TAC 492 THEN DEP_ASM_REWRITE_TAC[] 493 ] 494 ); 495 496*) 497