1structure liteLib :> liteLib = 2struct 3 4open Feedback Thm Conv Abbrev; 5 6infix THENC ORELSEC |->; 7 8(*--------------------------------------------------------------------------- 9 * Fake for NJSML: it does not use Interrupt anyway so it won't ever 10 * get raised. 11 *---------------------------------------------------------------------------*) 12(* exception Interrupt; *) 13 14 15 16(*--------------------------------------------------------------------- 17 * Exceptions 18 *--------------------------------------------------------------------*) 19 20val ERR = mk_HOL_ERR "liteLib" 21 22fun STRUCT_ERR s (func,mesg) = raise Feedback.mk_HOL_ERR s func mesg 23fun STRUCT_WRAP s (func,exn) = raise Feedback.wrap_exn s func exn 24 25(*--------------------------------------------------------------------- 26 * options 27 *--------------------------------------------------------------------*) 28 29fun the (SOME x) = x 30 | the _ = failwith "the: can't take \"the\" of NONE" 31 32fun is_some (SOME x) = true 33 | is_some NONE = false 34 35fun is_none NONE = true 36 | is_none _ = false 37 38fun option_cases f e (SOME x) = f x 39 | option_cases f e NONE = e 40 41fun option_app f (SOME x) = SOME (f x) 42 | option_app f NONE = NONE 43 44 45infix 3 |> thenf orelsef; 46fun (x |> f) = f x; 47 48fun (f thenf g) x = g(f x); 49 50fun (f orelsef g) x = 51 f x handle Interrupt => raise Interrupt 52 | _ => g x; 53 54val repeat = Lib.repeat 55 56fun foldr f e L = 57 let fun itl [] = e 58 | itl (a::rst) = f (a,itl rst) 59 in itl L 60 end; 61 62fun foldl f e L = 63 let fun rev_it [] e = e 64 | rev_it (a::rst) e = rev_it rst (f (a,e)) 65 in rev_it L e 66 end; 67 68fun end_foldr f = 69 let fun endit [] = failwith "end_foldr: list too short" 70 | endit alist = 71 let val (base,ralist) = case rev alist of 72 h::t => (h,t) 73 | _ => raise Bind 74 in foldr f base (rev ralist) 75 end 76 in endit 77 end; 78 79val chop_list = Lib.split_after; 80 81fun rotl (a::rst) = rst@[a] 82 | rotl [] = failwith "rotl: empty list" 83 84fun rotr lst = 85 let val (front,last) = Lib.front_last lst 86 in last::front 87 end 88 handle HOL_ERR _ => failwith "rotr: empty list" 89 90 91fun replicate (x,n) = 92 let fun repl 0 = [] 93 | repl n = x::repl (n-1) 94 in repl n 95 end 96 97fun upto (n,m) = if n >= m then [] else n::upto (n+1,m); 98 99(* ------------------------------------------------------------------------- *) 100(* Iterative splitting (list) and stripping (tree) via destructor. *) 101(* ------------------------------------------------------------------------- *) 102 103fun splitlist dest x = 104 let val (l,r) = dest x 105 val (ls,res) = splitlist dest r 106 in (l::ls,res) 107 end 108 handle Interrupt => raise Interrupt 109 | _ => ([],x);; 110 111fun rev_splitlist dest = 112 let fun rsplist ls x = 113 let val (l,r) = dest x 114 in rsplist (r::ls) l 115 end 116 handle Interrupt => raise Interrupt 117 | _ => (x,ls) 118 in 119 fn x => rsplist [] x 120 end;; 121 122fun striplist dest = 123 let fun strip x acc = 124 let val (l,r) = dest x 125 in strip l (strip r acc) 126 end 127 handle Interrupt => raise Interrupt 128 | _ => x::acc 129 in 130 fn x => strip x [] 131 end;; 132 133 134(*--------------------------------------------------------------------* 135 * Associative list functions * 136 *--------------------------------------------------------------------*) 137 138val rev_assoc = Lib.rev_assoc; 139 140fun remove_assoc x = 141 let fun remove [] = raise ERR "" "" 142 | remove ((h as (l,r))::t) = if (x = l) then t else (h::remove t) 143 in fn l => (remove l handle HOL_ERR _ => l) 144 end; 145 146fun add_assoc (x as (l,r)) ll = x::remove_assoc l ll; 147 148(* ------------------------------------------------------------------------- *) 149(* "lazy" objects to delay calculation and avoid recalculation. *) 150(* ------------------------------------------------------------------------- *) 151 152datatype ('a,'b)Lazysum = Unrealized of ('a -> 'b) * 'a 153 | Realized of 'b; 154 155type ('a,'b)lazy = ('a,'b) Lazysum ref; 156 157fun lazy f x = ref(Realized (f x)); 158fun eager y = ref(Realized y);; 159 160fun eval r = 161 case !r of 162 Realized(y) => y 163 | Unrealized(f,x) => let val y = f(x) in (r := Realized(y); y) end;; 164 165(*-------------------------------------------------------------------* 166 * Orders * 167 *-------------------------------------------------------------------*) 168 169fun ord_of_lt lt (x,y) = 170 if lt(x, y) then LESS else 171 if lt(y,x) then GREATER else EQUAL; 172 173fun lt_of_ord ord (x,y) = (ord(x, y) = LESS); 174 175val list_ord = Lib.list_compare 176 177 178(* ===================================================================== * 179 * Basic equality reasoning including conversionals. * 180 * ===================================================================== *) 181 182(*--------------------------------------------------------------------------* 183 * General syntax for binary operators (monomorphic constructor only). * 184 * * 185 * Nb. strip_binop strips only on the right, binops strips both * 186 * left and right (alal conjuncts and disjuncts). * 187 * -------------------------------------------------------------------------*) 188 189fun mk_binop opr (l,r) = 190 Term.list_mk_comb(opr,[l,r]) handle HOL_ERR _ => failwith "mk_binop" 191 192fun list_mk_binop opr = Lib.end_itlist (Lib.curry (mk_binop opr)); 193 194fun dest_binop opr tm = 195 let val (Rator,rhs) = Term.dest_comb tm 196 val (opr',lhs) = Term.dest_comb Rator 197 in 198 if opr=opr' then (lhs,rhs) else fail() 199 end 200 handle HOL_ERR _ => failwith "dest_binop"; 201 202fun strip_binop opr = 203 let val dest = dest_binop opr 204 fun strip tm = 205 let val (l,r) = dest tm 206 val (str,rm) = strip r 207 in (l::str,rm) 208 end 209 handle HOL_ERR _ => ([],tm) 210 in strip 211 end; 212 213fun binops opr = 214 let val dest = dest_binop opr 215 fun strip tm = 216 let val (l,r) = dest tm 217 in strip l @ strip r 218 end 219 handle HOL_ERR _ => [tm] 220 in strip 221 end; 222 223fun is_binop opr = Lib.can (dest_binop opr) 224 225val is_imp = is_binop boolSyntax.implication; 226val dest_imp = dest_binop boolSyntax.implication; 227val strip_imp = splitlist dest_imp; 228 229 230(* ------------------------------------------------------------------------- *) 231(* Grabbing left operand of a binary operator (or something coextensive!) *) 232(* ------------------------------------------------------------------------- *) 233 234val lhand = Term.rand o Term.rator;; 235 236(* ------------------------------------------------------------------------- *) 237(* Like mk_comb, but instantiates type variables in rator if necessary. *) 238(* ------------------------------------------------------------------------- *) 239 240fun mk_icomb(tm1,tm2) = 241 let val ty = Lib.fst(Type.dom_rng(Term.type_of tm1)) 242 val tyins = Type.match_type ty (Term.type_of tm2) 243 in 244 Term.mk_comb(Term.inst tyins tm1, tm2) 245 end;; 246 247(* ------------------------------------------------------------------------- *) 248(* Instantiates types for constant c and iteratively makes combination. *) 249(* ------------------------------------------------------------------------- *) 250 251fun list_mk_icomb tm1 args = 252 Lib.rev_itlist (Lib.C (Lib.curry mk_icomb)) args tm1;; 253 254(* ------------------------------------------------------------------------- *) 255(* Rule allowing easy instantiation of polymorphic proformas. *) 256(* ------------------------------------------------------------------------- *) 257 258fun PINST tyin tmin = 259 let val inst_fn = Term.inst tyin 260 val tmin' = map (fn {redex,residue} => 261 {redex=inst_fn redex, residue=residue}) tmin 262 val iterm_fn = Thm.INST tmin' 263 val itype_fn = Thm.INST_TYPE tyin 264 in 265 fn th => iterm_fn (itype_fn th) handle HOL_ERR _ => failwith "PINST" 266 end; 267 268 269(* ------------------------------------------------------------------------- *) 270(* Really basic stuff for equality. *) 271(* ------------------------------------------------------------------------- *) 272 273fun MK_BINOP oper (lth,rth) = MK_COMB(AP_TERM oper lth,rth); 274 275(* ------------------------------------------------------------------------- *) 276(* Subterm conversions. *) 277(* ------------------------------------------------------------------------- *) 278 279val LAND_CONV = Conv.LAND_CONV 280val BINDER_CONV = Conv.BINDER_CONV 281 282fun COMB2_CONV lconv rconv tm = 283 let val (Rator,Rand) = Term.dest_comb tm 284 in MK_COMB(lconv Rator, rconv Rand) 285 end; 286 287val COMB_CONV = Lib.W COMB2_CONV;; 288 289fun alpha v tm = 290 let val (v0,bod) = Term.dest_abs tm 291 handle HOL_ERR _ => failwith "alpha: Not an abstraction" 292 in if v = v0 then tm else 293 if not (Lib.mem v (Term.free_vars bod)) 294 then Term.mk_abs(v, Term.subst [Lib.|->(v0,v)] bod) 295 else failwith "alpha: Invalid new variable" 296 end; 297 298 299val ABS_CONV = Conv.ABS_CONV 300 301val BODY_CONV = 302 let fun dest_quant tm = 303 let val (q,atm) = Term.dest_comb tm 304 val (v,bod) = Term.dest_abs atm 305 in ((q,v),bod) 306 end 307 val strip_quant = splitlist dest_quant 308 in fn conv => fn tm => 309 let val (quants,bod) = strip_quant tm 310 in Lib.itlist(fn (q,v) => fn th => AP_TERM q (ABS v th)) quants (conv bod) 311 end 312 end;; 313 314(* ------------------------------------------------------------------------- *) 315(* Faster depth conversions using failure rather than returning a REFL. *) 316(* ------------------------------------------------------------------------- *) 317 318val rhs = boolSyntax.rhs; 319 320infix THENQC THENCQC; 321 322fun op THENQC (conv1,conv2) tm = 323 let val th1 = conv1 tm 324 in let val th2 = conv2(rhs(concl th1)) 325 in TRANS th1 th2 326 end handle HOL_ERR _ => th1 327 end 328 handle HOL_ERR _ => conv2 tm; 329 330 331fun op THENCQC (conv1,conv2) tm = 332 let val th1 = conv1 tm 333 in let val th2 = conv2(rhs(concl th1)) 334 in TRANS th1 th2 335 end 336 handle HOL_ERR _ => th1 337 end 338 339fun REPEATQC conv tm = (conv THENCQC (REPEATQC conv)) tm;; 340 341fun COMB2_QCONV conv1 conv2 tm = 342 let val (l,r) = Term.dest_comb tm 343 in let val th1 = conv1 l 344 in let val th2 = conv2 r 345 in MK_COMB(th1,th2) 346 end 347 handle HOL_ERR _ => AP_THM th1 r 348 end 349 handle HOL_ERR _ => AP_TERM l (conv2 r) 350 end; 351 352val COMB_QCONV = Lib.W COMB2_QCONV;; 353 354fun SUB_QCONV conv tm = 355 if Term.is_abs tm then ABS_CONV conv tm 356 else COMB_QCONV conv tm;; 357 358fun ONCE_DEPTH_QCONV conv tm = 359 (conv ORELSEC (SUB_QCONV (ONCE_DEPTH_QCONV conv))) tm;; 360 361fun DEPTH_QCONV conv tm = 362 ((SUB_QCONV (DEPTH_QCONV conv)) THENQC 363 (REPEATQC conv)) tm;; 364 365fun REDEPTH_QCONV conv tm = 366 ((SUB_QCONV (REDEPTH_QCONV conv)) THENQC 367 (conv THENCQC (REDEPTH_QCONV conv))) tm;; 368 369fun TOP_DEPTH_QCONV conv tm = 370 ((REPEATQC conv) THENQC 371 (SUB_QCONV (TOP_DEPTH_QCONV conv) 372 THENCQC 373 (conv THENCQC (TOP_DEPTH_QCONV conv)))) tm;; 374 375fun TOP_SWEEP_QCONV conv tm = 376 ((REPEATQC conv) THENQC 377 (SUB_QCONV (TOP_SWEEP_QCONV conv))) tm;; 378 379(* ------------------------------------------------------------------------- *) 380(* Standard conversions. *) 381(* ------------------------------------------------------------------------- *) 382 383fun TOP_SWEEP_CONV c = TRY_CONV (TOP_SWEEP_QCONV c);; 384 385(* ------------------------------------------------------------------------- *) 386(* Apply at leaves of op-tree; NB any failures at leaves cause failure. *) 387(* ------------------------------------------------------------------------- *) 388 389local exception DEST_BINOP 390in 391fun DEPTH_BINOP_CONV oper conv tm = 392 let val (l,r) = dest_binop oper tm handle HOL_ERR _ => raise DEST_BINOP 393 val lth = DEPTH_BINOP_CONV oper conv l 394 and rth = DEPTH_BINOP_CONV oper conv r 395 in MK_COMB(AP_TERM oper lth,rth) 396 end 397 handle DEST_BINOP => conv tm 398end; 399 400 401(* ------------------------------------------------------------------------- *) 402(* Single bottom-up pass, starting at the topmost success! *) 403(* ------------------------------------------------------------------------- *) 404 405fun SINGLE_DEPTH_CONV conv tm = 406 conv tm handle HOL_ERR _ 407 => (SUB_CONV (SINGLE_DEPTH_CONV conv) 408 THENC TRY_CONV conv) tm;; 409 410(*-----------------------------------------------------------------------*) 411(* MK_ABS_CONV - Abstract a term by a variable *) 412(* MK_ABSL_CONV - Abstract a term by a set of variables *) 413(* *) 414(* [DRS 96.01.28] *) 415(*-----------------------------------------------------------------------*) 416 417fun MK_ABS_CONV var tm = 418 if (Term.is_comb tm andalso (Term.rand tm = var) 419 andalso not (Term.free_in var (Term.rator tm))) 420 then REFL tm 421 else 422 let val rhs = Term.mk_abs(var,tm) 423 val newrhs = Term.mk_comb(rhs,var) 424 in SYM (BETA_CONV newrhs) 425 end; 426 427fun MK_ABSL_CONV vars tm = 428 let val rhs = boolSyntax.list_mk_abs (vars,tm) 429 val newrhs = Term.list_mk_comb(rhs,vars) 430 val thm1 = foldr (fn (_,conv) => (RATOR_CONV conv) THENC BETA_CONV) 431 ALL_CONV vars newrhs 432 in SYM thm1 433 end; 434 435val RIGHT_BETAS = 436 Lib.rev_itlist (fn a => CONV_RULE (RAND_CONV BETA_CONV) o Lib.C AP_THM a);; 437 438fun name_of_const tm = 439 let val {Name,Thy,...} = Term.dest_thy_const tm in (Name,Thy) end; 440 441fun MK_CONJ eq1 eq2 = MK_COMB(AP_TERM boolSyntax.conjunction eq1,eq2) 442fun MK_DISJ eq1 eq2 = MK_COMB(AP_TERM boolSyntax.disjunction eq1,eq2) 443fun MK_FORALL v th = 444 let val theta = [{redex=Type.alpha, residue=Term.type_of v}] 445 in AP_TERM (Term.inst theta boolSyntax.universal) (ABS v th) 446 end; 447fun MK_EXISTS v th = 448 let val theta = [{redex=Type.alpha, residue=Term.type_of v}] 449 in AP_TERM (Term.inst theta boolSyntax.existential) (ABS v th) 450 end; 451 452fun SIMPLE_DISJ_CASES th1 th2 = 453 case (hyp th1, hyp th2) 454 of (h1::_, h2::_) => DISJ_CASES (ASSUME(boolSyntax.mk_disj(h1,h2))) th1 th2 455 | _ => raise ERR "SIMPLE_DISJ_CASES" ""; 456 457val SIMPLE_CHOOSE = Drule.SIMPLE_CHOOSE 458 459end; 460