1(* ===================================================================== *) 2(* FILE : boolSyntax.sml *) 3(* DESCRIPTION : Derived HOL syntax operations. Mostly translated from *) 4(* the hol88 source. *) 5(* *) 6(* AUTHORS : (c) Mike Gordon, University of Cambridge *) 7(* Konrad Slind, University of Calgary *) 8(* Modified : September 1997, Ken Larsen (functor removal) *) 9(* Modified : July 2000, Konrad Slind *) 10(* ===================================================================== *) 11 12structure boolSyntax :> boolSyntax = 13struct 14 15open Feedback Lib HolKernel boolTheory; 16 17val ERR = mk_HOL_ERR "boolSyntax" 18type goal = term list * term 19 20(*--------------------------------------------------------------------------- 21 Basic constants 22 ---------------------------------------------------------------------------*) 23 24val equality = prim_mk_const {Name = "=", Thy = "min"} 25val implication = prim_mk_const {Name = "==>", Thy = "min"} 26val select = prim_mk_const {Name = "@", Thy = "min"} 27val T = prim_mk_const {Name = "T", Thy = "bool"} 28val F = prim_mk_const {Name = "F", Thy = "bool"} 29val universal = prim_mk_const {Name = "!", Thy = "bool"} 30val existential = prim_mk_const {Name = "?", Thy = "bool"} 31val exists1 = prim_mk_const {Name = "?!", Thy = "bool"} 32val conjunction = prim_mk_const {Name = "/\\", Thy = "bool"} 33val disjunction = prim_mk_const {Name = "\\/", Thy = "bool"} 34val negation = prim_mk_const {Name = "~", Thy = "bool"} 35val conditional = prim_mk_const {Name = "COND", Thy = "bool"} 36val let_tm = prim_mk_const {Name = "LET", Thy = "bool"} 37val arb = prim_mk_const {Name = "ARB", Thy = "bool"} 38val the_value = prim_mk_const {Name = "the_value", Thy = "bool"} 39val bool_case = prim_mk_const {Name = "COND", Thy = "bool"} 40val literal_case = prim_mk_const {Name = "literal_case", Thy = "bool"} 41val bounded_tm = prim_mk_const {Name = "BOUNDED", Thy = "bool"} 42val IN_tm = prim_mk_const {Name = "IN", Thy = "bool"} 43 44(*--------------------------------------------------------------------------- 45 Derived syntax operations 46 ---------------------------------------------------------------------------*) 47 48fun mk_eq (lhs, rhs) = 49 list_mk_comb (inst [alpha |-> type_of lhs] equality, [lhs, rhs]) 50 handle HOL_ERR _ => raise ERR "mk_eq" "lhs and rhs have different types" 51 52fun mk_imp (ant, conseq) = 53 list_mk_comb (implication, [ant, conseq]) 54 handle HOL_ERR _ => raise ERR "mk_imp" "Non-boolean argument" 55 56val mk_select = mk_binder select "mk_select" 57val mk_forall = mk_binder universal "mk_forall" 58val mk_exists = mk_binder existential "mk_exists" 59val mk_exists1 = mk_binder exists1 "mk_exists1" 60 61fun mk_conj (conj1, conj2) = 62 list_mk_comb (conjunction, [conj1, conj2]) 63 handle HOL_ERR _ => raise ERR "mk_conj" "Non-boolean argument" 64 65fun mk_disj (disj1, disj2) = 66 list_mk_comb (disjunction, [disj1, disj2]) 67 handle HOL_ERR _ => raise ERR "mk_disj" "Non-boolean argument" 68 69fun mk_neg M = 70 with_exn mk_comb (negation, M) (ERR "mk_neg" "Non-boolean argument") 71 72fun mk_cond (cond, larm, rarm) = 73 list_mk_comb (inst [alpha |-> type_of larm] conditional, [cond, larm, rarm]) 74 handle HOL_ERR _ => raise ERR "mk_cond" "" 75 76fun mk_let (func, arg) = 77 let 78 val (dom, rng) = dom_rng (type_of func) 79 in 80 list_mk_comb (inst [alpha |-> dom, beta |-> rng] let_tm, [func, arg]) 81 end 82 handle HOL_ERR _ => raise ERR "mk_let" "" 83 84fun mk_bool_case (a0, a1, b) = 85 list_mk_comb (inst [alpha |-> type_of a0] bool_case, [b, a0, a1]) 86 handle HOL_ERR _ => raise ERR "mk_bool_case" "" 87 88fun mk_literal_case (func, arg) = 89 let 90 val (dom, rng) = dom_rng (type_of func) 91 in 92 list_mk_comb 93 (inst [alpha |-> dom, beta |-> rng] literal_case, [func, arg]) 94 end 95 handle HOL_ERR _ => raise ERR "mk_literal_case" "" 96 97fun mk_arb ty = inst [alpha |-> ty] arb 98 99fun mk_itself ty = inst [alpha |-> ty] the_value 100 101val mk_icomb = Lib.uncurry HolKernel.mk_monop 102 103fun mk_IN (t1, t2) = mk_comb(mk_icomb(IN_tm, t1), t2) 104 105(*--------------------------------------------------------------------------* 106 * Destructors * 107 *--------------------------------------------------------------------------*) 108 109local 110 val dest_eq_ty_err = ERR "dest_eq(_ty)" "not an \"=\"" 111 val lhs_err = ERR "lhs" "not an \"=\"" 112 val rhs_err = ERR "rhs" "not an \"=\"" 113 val lhand_err = ERR "lhand" "not a binary comb" 114 val dest_imp_err = ERR "dest_imp" "not an \"==>\"" 115 val dest_cond_err = ERR "dest_cond" "not a conditional" 116 val bool_case_err = ERR "dest_bool_case" "not a \"bool_case\"" 117 val literal_case_err = ERR "dest_literal_case" "not a \"literal_case\"" 118in 119 val dest_eq = dest_binop equality dest_eq_ty_err 120 fun dest_eq_ty M = let val (l, r) = dest_eq M in (l, r, type_of l) end 121 fun lhs M = with_exn (fst o dest_eq) M lhs_err 122 fun rhs M = with_exn (snd o dest_eq) M rhs_err 123 fun lhand M = with_exn (rand o rator) M lhand_err 124 125 val dest_neg = dest_monop negation (ERR "dest_neg" "not a negation") 126 val dest_imp_only = dest_binop implication dest_imp_err 127 fun dest_imp M = dest_imp_only M 128 handle HOL_ERR _ => (dest_neg M, F) 129 handle HOL_ERR _ => raise dest_imp_err 130 val dest_select = dest_binder select (ERR "dest_select" "not a \"@\"") 131 val dest_forall = dest_binder universal (ERR "dest_forall" "not a \"!\"") 132 val dest_exists = dest_binder existential (ERR "dest_exists" "not a \"?\"") 133 val dest_exists1 = dest_binder exists1 (ERR "dest_exists1" "not a \"?!\"") 134 val dest_conj = dest_binop conjunction (ERR "dest_conj" "not a \"/\\\"") 135 val dest_disj = dest_binop disjunction (ERR "dest_disj" "not a \"\\/\"") 136 val dest_let = dest_binop let_tm (ERR "dest_let" "not a let term") 137 val dest_IN = dest_binop IN_tm (ERR "dest_IN" "not an IN term") 138 139 fun dest_cond M = 140 let 141 val (Rator, t2) = with_exn dest_comb M dest_cond_err 142 val (b, t1) = dest_binop conditional dest_cond_err Rator 143 in 144 (b, t1, t2) 145 end 146 147 fun dest_bool_case M = 148 let 149 val (Rator, a1) = with_exn dest_comb M bool_case_err 150 val (b, a0) = dest_binop bool_case bool_case_err Rator 151 in 152 (a0, a1, b) 153 end 154 155 val dest_literal_case = dest_binop literal_case literal_case_err 156 157 fun dest_arb M = 158 if same_const M arb then type_of M else raise ERR "dest_arb" "" 159 160 fun dest_itself M = 161 if same_const M the_value 162 then hd (snd (dest_type (type_of M))) 163 else raise ERR "dest_itself" "" 164end (* local *) 165 166(*--------------------------------------------------------------------------- 167 Selectors 168 ---------------------------------------------------------------------------*) 169 170val is_eq = can dest_eq 171val is_imp = can dest_imp 172val is_imp_only = can dest_imp_only 173val is_select = can dest_select 174val is_forall = can dest_forall 175val is_exists = can dest_exists 176val is_exists1 = can dest_exists1 177val is_conj = can dest_conj 178val is_disj = can dest_disj 179val is_neg = can dest_neg 180val is_cond = can dest_cond 181val is_let = can dest_let 182val is_bool_case = can dest_bool_case 183val is_literal_case = can dest_literal_case 184val is_arb = same_const arb 185val is_the_value = same_const the_value 186val is_IN = can dest_IN 187fun is_bool_atom tm = 188 is_var tm andalso (type_of tm = bool) 189 orelse is_neg tm andalso is_var (dest_neg tm); 190 191(*---------------------------------------------------------------------------* 192 * Construction and destruction functions that deal with SML lists * 193 *---------------------------------------------------------------------------*) 194 195val list_mk_comb = HolKernel.list_mk_comb 196val list_mk_abs = HolKernel.list_mk_abs 197 198val list_mk_forall = list_mk_binder (SOME universal) 199val list_mk_exists = list_mk_binder (SOME existential) 200val list_mk_conj = list_mk_rbinop (curry mk_conj) 201val list_mk_disj = list_mk_rbinop (curry mk_disj) 202 203fun list_mk_imp (A, c) = list_mk_rbinop (curry mk_imp) (A @ [c]) 204 205fun list_mk_icomb (f, args) = List.foldl (fn (a, t) => mk_icomb (t, a)) f args 206 207val strip_comb = HolKernel.strip_comb 208val strip_abs = HolKernel.strip_abs 209val strip_forall = HolKernel.strip_binder (SOME universal) 210val strip_exists = HolKernel.strip_binder (SOME existential) 211val strip_conj = strip_binop dest_conj 212val strip_disj = strip_binop dest_disj 213 214fun dest_strip_comb t = 215 let 216 val (l, r) = strip_comb t 217 val {Thy = thy, Name = name, ...} = Term.dest_thy_const l 218 in 219 (thy ^ "$" ^ name, r) 220 end 221 222val strip_imp = 223 let 224 val desti = total dest_imp 225 fun strip A M = 226 case desti M of 227 NONE => (List.rev A, M) 228 | SOME (ant, conseq) => strip (ant :: A) conseq 229 in 230 strip [] 231 end 232 233val strip_imp_only = 234 let 235 val desti = total dest_imp_only 236 fun strip A M = 237 case desti M of 238 NONE => (List.rev A, M) 239 | SOME (ant, conseq) => strip (ant :: A) conseq 240 in 241 strip [] 242 end 243 244val strip_neg = 245 let 246 val destn = total dest_neg 247 fun strip A M = 248 case destn M of 249 NONE => (M, A) 250 | SOME N => strip (A + 1) N 251 in 252 strip 0 253 end 254 255fun gen_all tm = list_mk_forall (free_vars tm, tm) 256 257(*---------------------------------------------------------------------------* 258 * Construction and destruction of function types from/to lists of types * 259 * Michael Norrish - December 1999 * 260 *---------------------------------------------------------------------------*) 261 262val list_mk_fun = HolKernel.list_mk_fun 263val strip_fun = HolKernel.strip_fun 264 265(*--------------------------------------------------------------------------- 266 Linking definitional principles and signature operations 267 with grammars. 268 ---------------------------------------------------------------------------*) 269 270fun dest t = 271 let 272 val (lhs, rhs) = dest_eq (snd (strip_forall t)) 273 val (f, args) = strip_comb lhs 274 val f = mk_var(dest_const f) handle HOL_ERR _ => f 275 in 276 if all is_var args 277 then (args, mk_eq (f, list_mk_abs (args, rhs))) 278 else raise ERR "new_definition" "non-variable argument" 279 end 280 281fun RIGHT_BETA th = TRANS th (BETA_CONV (rhs (concl th))) 282 283fun post (V, th) = 284 let 285 fun add_var v th = RIGHT_BETA (AP_THM th v) 286 in 287 itlist GEN V (rev_itlist add_var V th) 288 end 289 290val _ = Definition.new_definition_hook := (dest, post) 291 292open Parse 293 294fun defname t = 295 let 296 val head = #1 (strip_comb (lhs (#2 (strip_forall t)))) 297 in 298 fst (dest_var head handle HOL_ERR _ => dest_const head) 299 end 300 301fun new_infixr_definition (s, t, p) = 302 Definition.new_definition (s, t) before set_fixity (defname t) (Infixr p) 303 304fun new_infixl_definition (s, t, p) = 305 Definition.new_definition (s, t) before set_fixity (defname t) (Infixl p) 306 307fun new_binder_definition (s, t) = 308 Definition.new_definition (s, t) before Parse.set_fixity (defname t) Binder 309 310fun new_type_definition (name, inhab_thm) = 311 Definition.new_type_definition (name, inhab_thm) 312 313fun new_infix (Name, Ty, Prec) = 314 Theory.new_constant (Name, Ty) 315 before Parse.add_infix (Name, Prec, Parse.RIGHT) 316 317fun new_binder (p as (Name, _)) = 318 Theory.new_constant p before set_fixity Name Binder 319 320fun new_infix_type (x as {Name, Arity, ParseName, Prec, Assoc}) = 321 let 322 val _ = Arity = 2 orelse 323 raise ERR "new_infix_type" "Infix types must have arity 2" 324 in 325 Theory.new_type (Name, Arity) 326 before Parse.add_infix_type 327 {Name = Name, ParseName = ParseName, Prec = Prec, Assoc = Assoc} 328 end 329 330(*---------------------------------------------------------------------------*) 331(* Lifter for booleans *) 332(*---------------------------------------------------------------------------*) 333 334fun lift_bool _ true = T 335 | lift_bool _ false = F 336 337(*--------------------------------------------------------------------------*) 338(* Some simple algebraic properties expressed at the term level. *) 339(*--------------------------------------------------------------------------*) 340 341val (comm_tm, assoc_tm, idem_tm, ldistrib_tm, rdistrib_tm) = 342 let 343 val f = mk_var ("f", alpha --> alpha --> alpha) 344 val g = mk_var ("g", alpha --> alpha --> alpha) 345 val g1 = mk_var ("g", alpha --> alpha) 346 val x = mk_var ("x", alpha) 347 val y = mk_var ("y", alpha) 348 val z = mk_var ("z", alpha) 349 in 350 (mk_eq (list_mk_comb (f, [x, y]), list_mk_comb (f, [y, x])), 351 mk_eq (list_mk_comb (f, [x, list_mk_comb (f, [y, z])]), 352 list_mk_comb (f, [list_mk_comb (f, [x, y]), z])), 353 mk_eq (mk_comb (g1, mk_comb (g1, x)), mk_comb (g1, x)), 354 mk_eq (list_mk_comb (f, [x, list_mk_comb (g, [y, z])]), 355 list_mk_comb (g, [list_mk_comb (f, [x, y]), 356 list_mk_comb (f, [x, z])])), 357 mk_eq (list_mk_comb (f, [list_mk_comb (g, [y, z]), x]), 358 list_mk_comb (g, [list_mk_comb (f, [y, x]), 359 list_mk_comb (f, [z, x])]))) 360 end 361 362(* ===================================================================== *) 363(* Syntactic operations on restricted quantifications. *) 364(* These ought to be generalised to all kinds of restrictions, *) 365(* but one thing at a time. *) 366(* --------------------------------------------------------------------- *) 367 368val (mk_res_forall, mk_res_exists, mk_res_exists_unique, 369 mk_res_select, mk_res_abstract) = 370 let 371 fun mk_res_quan cons s (x, t1, t2) = 372 let 373 val xty = type_of x 374 val t2_ty = type_of t2 375 val ty = (xty --> bool) --> (xty --> t2_ty) 376 --> (if cons = "RES_ABSTRACT" 377 then xty --> t2_ty 378 else if cons = "RES_SELECT" 379 then xty 380 else Type.bool) 381 in 382 mk_comb (mk_comb (mk_thy_const {Name=cons, Thy="bool", Ty=ty}, t1), 383 mk_abs (x, t2)) 384 end 385 handle _ => raise ERR "mk_res_quan" s 386 in 387 (mk_res_quan "RES_FORALL" "mk_res_forall", 388 mk_res_quan "RES_EXISTS" "mk_res_exists", 389 mk_res_quan "RES_EXISTS_UNIQUE" "mk_res_exists_unique", 390 mk_res_quan "RES_SELECT" "mk_res_select", 391 mk_res_quan "RES_ABSTRACT" "mk_res_abstract") 392 end 393 394fun list_mk_res_forall (ress, body) = 395 (itlist (fn (v, p) => fn b => mk_res_forall (v, p, b)) ress body) 396 handle _ => raise ERR "list_mk_res_forall" "" 397 398fun list_mk_res_exists (ress, body) = 399 (itlist (fn (v, p) => fn b => mk_res_exists (v, p, b)) ress body) 400 handle _ => raise ERR "list_mk_res_exists" "" 401 402val (dest_res_forall, dest_res_exists, dest_res_exists_unique, 403 dest_res_select, dest_res_abstract) = 404 let 405 fun dest_res_quan cons s = 406 let 407 val check = 408 assert (fn c => 409 let 410 val {Name, Thy, ...} = dest_thy_const c 411 in 412 Name = cons andalso Thy = "bool" 413 end) 414 in 415 fn tm => 416 let 417 val (op1, rand1) = dest_comb tm 418 val (op2, c1) = dest_comb op1 419 val _ = check op2 420 val (c2, c3) = dest_abs rand1 421 in 422 (c2, c1, c3) 423 end 424 end 425 handle _ => raise ERR "dest_res_quan" s 426 in 427 (dest_res_quan "RES_FORALL" "dest_res_forall", 428 dest_res_quan "RES_EXISTS" "dest_res_exists", 429 dest_res_quan "RES_EXISTS_UNIQUE" "dest_res_exists_unique", 430 dest_res_quan "RES_SELECT" "dest_res_select", 431 dest_res_quan "RES_ABSTRACT" "dest_res_abstract") 432 end 433 434fun strip_res_forall fm = 435 let 436 val (bv, pred, body) = dest_res_forall fm 437 val (prs, core) = strip_res_forall body 438 in 439 ((bv, pred) :: prs, core) 440 end 441 handle _ => ([], fm) 442 443fun strip_res_exists fm = 444 let 445 val (bv, pred, body) = dest_res_exists fm 446 val (prs, core) = strip_res_exists body 447 in 448 ((bv, pred) :: prs, core) 449 end 450 handle _ => ([], fm) 451 452val is_res_forall = can dest_res_forall 453val is_res_exists = can dest_res_exists 454val is_res_exists_unique = can dest_res_exists_unique 455val is_res_select = can dest_res_select 456val is_res_abstract = can dest_res_abstract 457 458fun mk n = prim_mk_const {Name = n, Thy = "bool"} 459 460val res_forall_tm = mk "RES_FORALL" 461val res_exists_tm = mk "RES_EXISTS" 462val res_exists1_tm = mk "RES_EXISTS_UNIQUE" 463val res_select_tm = mk "RES_SELECT" 464val res_abstract_tm = mk "RES_ABSTRACT" 465 466fun op~~(t1,t2) = aconv t1 t2 467fun op!~(t1,t2) = not (t1 ~~ t2) 468val ES = HOLset.empty Term.compare 469fun singt t = HOLset.add(ES, t) 470fun listset ts = HOLset.addList(ES, ts) 471fun FVLset ts = FVL ts ES 472fun FVs t = FVLset [t] 473 474(* ===================================================================== *) 475(* Type unification algorithms, and derived constructors. *) 476(* There are two versions of the algorithm: *) 477(* one performs classical unification (type_unify), and the other *) 478(* (sep_type_unify) renames all type variables to allow "unification" *) 479(* of types with type variables in common. The latter returns two *) 480(* substitutions, to be performed on the types separately *) 481(* --------------------------------------------------------------------- *) 482 483local 484 485 fun UERR s = ERR "type_unify" s 486 487 fun type_refine_subst [] tyS' = tyS' 488 | type_refine_subst tyS [] = tyS 489 | type_refine_subst tyS tyS' = 490 tyS' @ 491 (List.map (fn {redex, residue} => redex |-> type_subst tyS' residue) tyS) 492 493 fun type_new_vars vars = 494 let 495 val gvars = List.map (fn _ => gen_tyvar ()) vars 496 in 497 (gvars, ListPair.map op|->(vars,gvars), ListPair.map op|->(gvars,vars)) 498 end 499 fun is_tyvar vars ty = is_vartype ty andalso Lib.mem ty vars 500 fun find_redex r = Lib.first (fn rr as {redex, residue} => r = redex) 501 fun clean_subst s = Lib.filter (fn {redex, residue} => redex <> residue) s 502 fun maplet_map (redf, resf) {redex, residue} = (redf redex |-> resf residue) 503 fun subst_map fg = List.map (maplet_map fg) 504 505 fun solve _ sub [] = sub 506 | solve vars sub (tys :: rest) = 507 solve' vars sub (((type_subst sub) ## (type_subst sub)) tys) rest 508 and solve' vars sub (ty1, ty2) rest = 509 if is_tyvar vars ty1 then 510 if ty1 = ty2 then solve vars sub rest 511 else if type_var_in ty1 ty2 then raise UERR "occurs check" 512 else 513 (case total (find_redex ty1) sub of NONE 514 => solve vars (type_refine_subst sub [ty1 |-> ty2]) rest 515 | SOME {residue, ...} 516 => solve' vars sub (ty2, residue) rest) 517 else if is_tyvar vars ty2 then solve' vars sub (ty2, ty1) rest 518 else if is_vartype ty1 then 519 let 520 val _ = (ty1 = ty2) orelse raise UERR "(vartype, non-vartype)" 521 in 522 solve vars sub rest 523 end 524 else 525 let 526 val (ty2_n, ty2_a) = dest_type ty2 527 val (ty1_n, ty1_a) = dest_type ty1 528 val _ = (ty1_n = ty2_n) orelse 529 raise UERR "different type constructors" 530 in 531 solve vars sub (zip ty1_a ty2_a @ rest) 532 end 533 534 fun var_type_unify vars ty1 ty2 = solve' vars [] (ty1, ty2) [] 535 536 fun sep_var_type_unify (vars1, ty1) (vars2, ty2) = 537 let 538 val (gvars1, old_to_new1, new_to_old1) = type_new_vars vars1 539 val (gvars2, old_to_new2, new_to_old2) = type_new_vars vars2 540 val ty1' = type_subst old_to_new1 ty1 541 val ty2' = type_subst old_to_new2 ty2 542 val sub = var_type_unify (gvars1 @ gvars2) ty1' ty2' 543 val (sub1, sub2) = partition (C mem gvars1 o #redex) sub 544 val renaming_sub = new_to_old1 @ new_to_old2 545 in 546 (fn f => f ## f) 547 (clean_subst o subst_map ((fn x => (x,x)) 548 (type_subst renaming_sub))) (sub1, sub2) 549 end 550 551in 552 553 fun type_unify ty1 ty2 = 554 var_type_unify (union (type_vars ty1) (type_vars ty2)) ty1 ty2 555 556 fun sep_type_unify ty1 ty2 = 557 sep_var_type_unify (type_vars ty1, ty1) (type_vars ty2, ty2) 558 559 fun mk_ucomb (f, a) = 560 let 561 val fty = Term.type_of f 562 val aty = Term.type_of a 563 val (dty, rty) = dom_rng fty 564 val (dsub, asub) = sep_type_unify dty aty 565 in 566 mk_comb (Term.inst dsub f, Term.inst asub a) 567 end 568 569 fun list_mk_ucomb (f, args) = List.foldl (mk_ucomb o swap) f args 570 571 (* only generates one list *) 572 fun gen_tyvar_sigma (tys : hol_type list) = 573 map (fn ty => {redex = ty, residue = gen_tyvar()}) tys 574 fun gen_tyvarify tm = 575 Term.inst (gen_tyvar_sigma (type_vars_in_term tm)) tm 576 577 578end 579 580(* ---------------------------------------------------------------------- 581 Utility functions to help with the fact that terms are not an 582 equality type 583 ---------------------------------------------------------------------- *) 584 585local 586open Portable 587val aconv = Term.aconv 588in 589 590fun Teq tm = Term.same_const T tm 591fun Feq tm = Term.same_const F tm 592val tml_eq = list_eq aconv 593val tmp_eq = pair_eq aconv aconv 594val goal_eq = pair_eq tml_eq aconv 595val goals_eq = list_eq goal_eq 596val tmem = Lib.op_mem Term.aconv 597fun memt tlist t = Lib.op_mem Term.aconv t tlist 598val tunion = Lib.op_union Term.aconv 599fun tassoc t l = Lib.op_assoc Term.aconv t l 600 601fun tmx_eq (tm1,x1) (tm2,x2) = x1 = x2 andalso Term.aconv tm1 tm2 602fun xtm_eq (x1,tm1) (x2,tm2) = x1 = x2 andalso Term.aconv tm1 tm2 603end 604 605 606end 607