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