1(* ===================================================================== *) 2(* FILE : barendregt.sml *) 3(* VERSION : 1.0 *) 4(* DESCRIPTION : Tactics for working with substitutions naively. *) 5(* *) 6(* AUTHOR : Peter Vincent Homeier *) 7(* DATE : September 3, 2000 *) 8(* COPYRIGHT : Copyright (c) 2000 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 67 68(* 69val (asl,gl) = top_goal(); 70*) 71 72 73fun TACTIC_ERR{function,message} = 74 Feedback.HOL_ERR{origin_structure = "Tactic", 75 origin_function = function, 76 message = message}; 77 78fun failwith function = 79 ( (* if debug_fail then 80 print_string ("Failure in Cond_rewrite: "^function^"\n") 81 else (); *) 82 raise TACTIC_ERR{function = function,message = ""}); 83 84 85fun mk_subst l = map (fn (residue:'a, redex:'b) => 86 {redex=redex,residue=residue}) l; 87val INST_TY_TERM = (Drule.INST_TY_TERM) o (mk_subst##mk_subst); 88fun dest_subst l = map (fn {residue,redex} => (residue:'a, redex:'b)) l; 89 90 91 92val get_shift_matches = (dest_subst##dest_subst) o 93 (Term.match_term ���Lam x t :'a term���); 94(* 95val get_shift_matches = Psyntax.match_term ���Lam x t :'a term���; 96*) 97 98(* SEARCH_matches applies the function f to every subterm of the 99 given term tm, except to variables or constants, for which 100 SEARCH_matches always raises an exception. 101 The return value is a list of 'a objects, as produced by f 102 for every subterm of tm, all collected into one list. 103*) 104fun SEARCH_matches (f:term->'a list) tm = 105 ( (* if debug_matches then (print_string "SEARCH_matches: "; 106 print_term tm; print_newline()) else (); *) 107 if is_comb tm then 108 (let val {Rator,Rand} = Rsyntax.dest_comb tm 109 val m1 = (f Rator handle _ => []) 110 val m2 = (f Rand handle _ => []) 111 in append m1 m2 112 end) 113 else 114 if is_abs tm then 115 let val {Bvar,Body} = Rsyntax.dest_abs tm in 116 (f Body handle _ => []) 117 end 118 else failwith "SEARCH_matches"); 119 120(* 121fun SUB_matches (f:term->'a) tm = 122 ( (* if debug_matches then (print_string "SUB_matches: "; 123 print_term tm; print_newline()) else (); *) 124 if is_comb tm then 125 (let val {Rator,Rand} = Rsyntax.dest_comb tm in 126 (f Rator handle _ => f Rand) 127 end) 128 else 129 if is_abs tm then 130 let val {Bvar,Body} = Rsyntax.dest_abs tm in 131 f Body 132 end 133 else failwith "SUB_matches"); 134 135fun ONCE_DEPTH_matches (f:term->'a) tm = 136 ( (* if debug_matches then 137 (print_string "ONCE_DEPTH_matches: "; print_term tm; print_newline()) 138 else (); *) 139 (f tm handle _ => (SUB_matches (ONCE_DEPTH_matches f) tm))); 140*) 141 142fun ALL_DEPTH_matches (f:term->'a) tm = 143 ( (* if debug_matches then 144 (print_string "ONCE_DEPTH_matches: "; print_term tm; print_newline()) 145 else (); *) 146 ([f tm] handle _ => (SEARCH_matches (ALL_DEPTH_matches f) tm))); 147 148 149fun remove_s_matches matches = 150 let val (terms_list,types_list) = matches; 151 val nsterms = filter (fn (f,s) => not (#Name(dest_var s) = "s")) 152 terms_list 153 in 154 (nsterms,([]:(hol_type * hol_type) list)) 155 end; 156 157 158(* ------------------------------------------------------------------ *) 159(* Need to group together matches which have the same "x" match; *) 160(* for each such group, we should compute a variant of the x once, *) 161(* and then use the same variant x' for each of the new shifted *) 162(* bodies of the SIGMA expressions. This ensures that SIGMA *) 163(* expressions which had identical bound variables before, still *) 164(* have identical bound variables afterwards. This is important. *) 165(* ------------------------------------------------------------------ *) 166 167fun find_x (match::matches) = 168 let val (l,r) = match in 169 if r = ���x:var��� then l else find_x matches 170 end 171 | find_x [] = ���x:var���; 172 173fun find_t (match::matches) = 174 let val (l,r) = match in 175 if r = ���t:'a term��� then l else find_t matches 176 end 177 | find_t [] = ���t:'a term���; 178 179fun sort_matches matchesl = 180 let val (mtermsl,_) = split matchesl 181 val xtms = map find_x mtermsl 182 val dist_xtms = mk_set xtms 183 val xs_termsl = zip xtms mtermsl 184 val xmgroups = map (fn dx => filter (fn (x,matches) => (x = dx)) 185 xs_termsl) 186 dist_xtms 187 val mgroups = map (map snd) xmgroups 188 val t's = map (map find_t) mgroups 189 val mtygroups = map (map (fn tms => 190 (tms, ([]:(hol_type * hol_type) list)))) 191 mgroups 192 val tmgroups = zip (zip dist_xtms t's) mtygroups 193 in 194 tmgroups 195 end; 196 197 198 199val EVERY_LENGTH_LEMMA = TAC_PROOF(([], 200 ���!os (a:'a) as. 201 (LENGTH os = LENGTH (CONS a as)) ==> 202 (?(o':'b) os'. (LENGTH os' = LENGTH as) /\ (os = CONS o' os'))���), 203 LIST_INDUCT_TAC 204 THEN REWRITE_TAC[LENGTH,arithmeticTheory.SUC_NOT] 205 THEN REWRITE_TAC[prim_recTheory.INV_SUC_EQ,CONS_11] 206 THEN REPEAT GEN_TAC THEN STRIP_TAC 207 THEN EXISTS_TAC ���h:'b��� 208 THEN EXISTS_TAC ���os:'b list��� 209 THEN ASM_REWRITE_TAC[] 210 ); 211 212val NIL_LENGTH_LEMMA = TAC_PROOF(([], 213 ���!os:'b list. 214 (LENGTH os = LENGTH ([]:'a list)) ==> 215 (os = [])���), 216 REWRITE_TAC[LENGTH,LENGTH_NIL] 217 ); 218 219fun REPEAT_N 0 tac = ALL_TAC 220 | REPEAT_N n tac = (tac THEN REPEAT_N (n-1) tac); 221 222 223 224fun make_new_objects thm = 225 let val cn = concl thm 226 val rhs = #rhs(dest_eq cn) 227 val lst = #Rand(dest_comb rhs) 228 fun length_list lst = 229 if lst = ���[]:obj list��� then 0 230 else 1 + length_list (#Rand(dest_comb lst)) 231 val n = length_list lst 232 fun make_one 0 thm = thm 233 | make_one n thm = thm 234 in 235 (make_one n thm; n) 236 end; 237 238 239(* 240fun MAKE_CLEAN_VAR_THM free_vrs matches = 241 let val (terms_list,types_list) = matches; 242 val ftm = foldr (fn (x,s) => 243 if type_of x = (==`:var`==) 244 then ���^x INSERT ^s��� 245 else if type_of x = (==`:var list`==) 246 then ���SL ^x UNION ^s��� 247 else if type_of x = (==`:var set`==) 248 then ���^x UNION ^s��� 249 else if type_of x = (==`:'a term`==) 250 then ���(FV ^x) UNION ^s��� 251 else s) 252 ���{}:var set��� 253 free_vrs; 254 val sterms = (ftm, ���s:var set���)::terms_list; 255 val smatches = (sterms,([]:(hol_type * hol_type) list)); 256 val sigma_thm = INST_TY_TERM smatches (SPEC_ALL SIGMA_CLEAN_VAR); 257 in 258 REWRITE_RULE[FINITE_EMPTY,FINITE_INSERT,FINITE_UNION, 259 FINITE_FV_object,IN,IN_UNION,DE_MORGAN_THM] 260 sigma_thm 261 end; 262*) 263 264 265fun MAKE_LIST_CLEAN_VAR_THM free_vrs (x, os) = 266 let val ftm = foldr (fn (x,s) => 267 if type_of x = (==`:var`==) 268 then ���^x INSERT ^s��� 269 else if type_of x = (==`:var list`==) 270 then ���SL ^x UNION ^s��� 271 else if type_of x = (==`:var set`==) 272 then ���^x UNION ^s��� 273 else if type_of x = (==`:'a term`==) 274 then ���(FV ^x) UNION ^s��� 275 else s) 276 ���{}:var set��� 277 free_vrs; 278 val mk_term_list = foldr (fn (a,os) => ���CONS ^a ^os���) 279 ���[]:'a term list��� 280 val os_tm = mk_term_list os 281 val lambda_thm = SPECL[ftm,x,os_tm] LAMBDA_LIST_CLEAN_VAR 282 val exists_list_thm = 283 REWRITE_RULE[FINITE_EMPTY,FINITE_INSERT,FINITE_UNION, 284 FINITE_FV,IN,IN_UNION,DE_MORGAN_THM] 285 lambda_thm 286 val os' = foldr (fn (v,l) => (Term.variant (l @ free_vrs) v)::l) 287 [] os 288 val os'_tm = mk_term_list os' 289 val {Bvar=zvar, Body=body1} = dest_exists (concl exists_list_thm) 290 val {Rator=exists_binder, Rand=body2} = dest_comb body1 291 val os'_vr = #Bvar(dest_abs body2) 292 val exists_tm1 = beta_conv (mk_comb{Rator=body2, Rand=os'_tm}) 293 val exists_tm2 = foldr (fn (o1,tm) => mk_exists{Bvar=o1, Body=tm}) 294 exists_tm1 os' 295 val exists_tm = mk_exists{Bvar=zvar, Body=exists_tm2} 296 val exists_thm = TAC_PROOF (([],exists_tm), 297 STRIP_ASSUME_TAC exists_list_thm 298 THEN ASSUM_LIST (fn asl1 => 299 EXISTS_TAC (#Rand (dest_comb (#Rator(dest_comb 300 (#Rand(dest_comb (concl (hd (rev asl1)))))))))) 301 THEN REPEAT 302 (POP_ASSUM (fn lth => 303 STRIP_ASSUME_TAC (MATCH_MP EVERY_LENGTH_LEMMA lth)) 304 THEN FIRST_ASSUM (fn eth => 305 EXISTS_TAC 306 (#Rand (dest_comb (#Rator(dest_comb 307 (#rhs(dest_eq (concl eth)))))))) 308 THEN POP_ASSUM REWRITE_ALL_THM) 309 THEN POP_ASSUM (REWRITE_ALL_THM o MATCH_MP NIL_LENGTH_LEMMA) 310 THEN ASM_REWRITE_TAC[LENGTH] 311 ) 312 in 313 BETA_RULE (REWRITE_RULE[EVERY_DEF,MAP2,combinTheory.I_THM] exists_thm) 314 end; 315 316 317val MAKE_SIMPLE_SUBST_TAC = 318 DEP_REWRITE_TAC[LAMBDA_SUBST_SIMPLE] 319 THEN CONJ_TAC 320 THENL 321 [ ASM_REWRITE_TAC[termTheory.BV_subst_def,pairTheory.FST,IN] 322 THEN REPEAT (CHANGED_TAC 323 (ASM_REWRITE_TAC[IN_DIFF,IN,FV_term,FV_term_subst] 324 THEN DEP_REWRITE_TAC[NOT_IN_FV_subst,NOT_IN_FV_subst2])) 325 THEN ASM_REWRITE_TAC[], 326 327 ALL_TAC 328 ]; 329 330 331(* 332val SHIFT_LAMBDA_TAC :tactic = fn (asl,gl) => 333 let val matches = ONCE_DEPTH_matches get_shift_matches gl; 334 val free_vrs = mk_set (append (free_vars gl) 335 (flatten (map free_vars asl))); 336 val lambda_thm = MAKE_CLEAN_VAR_THM free_vrs matches 337 in 338 (STRIP_ASSUME_TAC lambda_thm 339 THEN FIRST_ASSUM REWRITE_THM 340 THEN UNDISCH_LAST_TAC 341 THEN FIRST_ASSUM (fn hght => EVERY_ASSUM (fn th => 342 ASSUME_TAC (MATCH_MP th hght) 343 handle _ => ALL_TAC)) 344 THEN DISCH_TAC) (asl,gl) 345 end; 346*) 347 348val SHIFT_LAMBDAS_TAC :tactic = fn (asl,gl) => 349 let val matchesl = mk_set (ALL_DEPTH_matches get_shift_matches gl); 350 val match_groups = sort_matches matchesl 351 val (tags,groups) = split match_groups 352 (* val (xs,bodies) = split tags *) 353 val free_vrs = mk_set (append (free_vars gl) 354 (flatten (map free_vars asl))); 355 val lambda_thms = map (MAKE_LIST_CLEAN_VAR_THM free_vrs) tags 356 val t_lambda_thms = zip tags lambda_thms 357 (* val lambda_thm = map (MAKE_CLEAN_VAR_THM free_vrs) matchesl *) 358 in 359 if matchesl = [] then 360 ONCE_REWRITE_TAC[SUB_term] (asl,gl) 361 else 362 (EVERY (map (fn ((x,os),lambda_thm) => 363 let val n = length os in 364 STRIP_ASSUME_TAC lambda_thm 365 THEN POP_ASSUM (fn th => ALL_TAC) 366 THEN REPEAT_N n 367 (FIRST_ASSUM REWRITE_THM THEN UNDISCH_LAST_TAC) 368 THEN REPEAT_N n UNDISCH_LAST_TAC (* the HEIGHT = HEIGHT asms *) 369 THEN REPEAT_N n 370 (DISCH_THEN (fn hght => 371 EVERY_ASSUM (fn th => 372 ASSUME_TAC (MATCH_MP th hght) 373 handle _ => ALL_TAC) 374 THEN ASSUME_TAC hght)) 375 THEN REPEAT_N n DISCH_TAC 376 end) 377 t_lambda_thms) ) 378 (* above is tactic, applied to: *) 379 (asl,gl) 380 end; 381 382 383(* ================================================================== *) 384(* End of local declarations. *) 385(* Beginning of exported declarations. *) 386(* ================================================================== *) 387 388in 389 390 391val SHIFT_LAMBDAS_TAC = SHIFT_LAMBDAS_TAC; 392 393 394val MAKE_SIMPLE_SUBST_TAC = MAKE_SIMPLE_SUBST_TAC; 395 396val SIMPLE_SUBST_TAC = 397 SHIFT_LAMBDAS_TAC THEN MAKE_SIMPLE_SUBST_TAC; 398 399 400end (* of local declaration block *) 401 402end; (* of structure barendregt *) 403 404 405(* TEST EXAMPLES: 406 407load "MutualIndThen"; 408open MutualIndThen; 409 410(* Barendregt's Substitution Lemma, 2.1.16, page 27: *) 411 412val BARENDREGT_SUBSTITUTION_LEMMA = TAC_PROOF 413 (([], 414 ���!(M:'a term) N L x y. 415 ~(x = y) /\ ~(x IN FV L) ==> 416 (((M <[ [x,N]) <[ [y,L]) = 417 ((M <[ [y,L]) <[ [x, (N <[ [y,L])]))���), 418 MUTUAL_INDUCT_THEN term_height_induct ASSUME_TAC 419 THENL 420 [ (* Con case *) 421 REPEAT STRIP_TAC 422 THEN REWRITE_TAC[SUB_term,SUB], 423 424 (* Var case *) 425 REPEAT STRIP_TAC 426 THEN REWRITE_TAC[SUB_term,SUB] 427 THEN COND_CASES_TAC 428 THENL 429 [ ASM_REWRITE_TAC[SUB_term,SUB], 430 431 REWRITE_TAC[SUB_term,SUB] 432 THEN COND_CASES_TAC 433 THENL 434 [ IMP_RES_THEN REWRITE_THM subst_EMPTY, 435 436 ASM_REWRITE_TAC[SUB_term,SUB] 437 ] 438 ], 439 440 (* App case *) 441 REPEAT STRIP_TAC 442 THEN RES_TAC 443 THEN ASM_REWRITE_TAC[SUB_term], 444 445 (* Lam case *) 446 REPEAT STRIP_TAC 447 THEN SIMPLE_SUBST_TAC 448 THEN DEP_ASM_REWRITE_TAC[] 449 ] 450 ); 451 452*) 453