1(**** ML Programs from Chapter 10 of 2 3 ML for the Working Programmer, 2nd edition 4 by Lawrence C. Paulson, Computer Laboratory, University of Cambridge. 5 (Cambridge University Press, 1996) 6 7Copyright (C) 1996 by Cambridge University Press. 8Permission to copy without fee is granted provided that this copyright 9notice and the DISCLAIMER OF WARRANTY are included in any copy. 10 11DISCLAIMER OF WARRANTY. These programs are provided `as is' without 12warranty of any kind. We make no warranties, express or implied, that the 13programs are free of error, or are consistent with any particular standard 14of merchantability, or that they will meet your requirements for any 15particular application. They should not be relied upon for solving a 16problem whose incorrect solution could result in injury to a person or loss 17of property. If you do use the programs or functions in such a manner, it 18is at your own risk. The author and publisher disclaim all liability for 19direct, incidental or consequential damages resulting from your use of 20these programs or functions. 21****) 22 23 24(*TACTIC-BASED PROVER FOR CLASSICAL FIRST-ORDER LOGIC*) 25 26(*variables 27 a,b,c: string qnt: string (quantifier name) 28 i,j: int (Bound indices) 29 t,u: term p,q: form 30 x,y: any f,g: functions *) 31 32(**** Terms and Formulae ****) 33signature FOL = 34 sig 35 datatype term = Var of string 36 | Param of string * string list 37 | Bound of int 38 | Fun of string * term list 39 datatype form = Pred of string * term list 40 | Conn of string * form list 41 | Quant of string * string * form 42 type goal = form list * form list 43 val precOf: string -> int 44 val abstract: int -> term -> form -> form 45 val subst: int -> term -> form -> form 46 val termVars: term * string list -> string list 47 val goalVars: goal * string list -> string list 48 val termParams: term * (string * string list) list 49 -> (string * string list) list 50 val goalParams: goal * (string * string list) list 51 -> (string * string list) list 52 end; 53 54structure Fol : FOL = 55 struct 56 datatype term = Var of string 57 | Param of string * string list 58 | Bound of int 59 | Fun of string * term list; 60 datatype form = Pred of string * term list 61 | Conn of string * form list 62 | Quant of string * string * form; 63 64 type goal = form list * form list; 65 66 (*Replace the term u1 by u2 throughout a term t*) 67 fun replace (u1,u2) t = 68 if t=u1 then u2 else 69 case t of Fun(a,ts) => Fun(a, map (replace(u1,u2)) ts) 70 | _ => t; 71 72 (*Abstraction of a formula over the atomic term t. *) 73 fun abstract i t (Pred(a,ts)) = Pred(a, map (replace (t, Bound i)) ts) 74 | abstract i t (Conn(b,ps)) = Conn(b, map (abstract i t) ps) 75 | abstract i t (Quant(qnt,b,p)) = Quant(qnt, b, abstract (i+1) t p); 76 77 (*Replace (Bound i) by t in formula. t may contain no bound vars *) 78 fun subst i t (Pred(a,ts)) = Pred(a, map (replace (Bound i, t)) ts) 79 | subst i t (Conn(b,ps)) = Conn(b, map (subst i t) ps) 80 | subst i t (Quant(qnt,b,p)) = Quant(qnt, b, subst (i+1) t p); 81 82 (*Precedence table: used by parsing AND display! *) 83 fun precOf "~" = 4 84 | precOf "&" = 3 85 | precOf "|" = 2 86 | precOf "<->" = 1 87 | precOf "-->" = 1 88 | precOf _ = ~1 (*means not an infix*); 89 90 (*Accumulate a term function over all terms in a formula*) 91 fun accumForm f (Pred(_,ts), z) = foldr f z ts 92 | accumForm f (Conn(_,ps), z) = foldr (accumForm f) z ps 93 | accumForm f (Quant(_,_,p), z) = accumForm f (p,z); 94 95 (*Accumulate a form function over all formulae in a goal [POLYMORHPIC]*) 96 fun accumGoal f ((ps,qs), z) = foldr f (foldr f z qs) ps; 97 98 (*insertion into ordered list of strings*) 99 fun insert (a,[]) = [a] 100 | insert (a,b::bs) = case String.compare (a,b) of 101 LESS => a::b::bs 102 | EQUAL => b::bs 103 | GREATER => b::insert(a,bs); 104 105 (*Accumulate all Vars in the term (except in a Param).*) 106 fun termVars (Var a, bs) = insert(a,bs) 107 | termVars (Fun(_,ts), bs) = foldr termVars bs ts 108 | termVars (_, bs) = bs; 109 val goalVars = accumGoal (accumForm termVars); 110 111 (*Accumulate all Params*) 112 fun termParams (Param(a,bs), pairs) = (a,bs) :: pairs 113 | termParams (Fun(_,ts), pairs) = foldr termParams pairs ts 114 | termParams (_, pairs) = pairs; 115 val goalParams = accumGoal (accumForm termParams); 116 end; 117 118(**** Syntax: scanning, parsing, and display ****) 119 120structure FolKey = 121 struct val alphas = ["ALL","EX"] 122 and symbols = ["(", ")", ".", ",", "?", "~", "&", "|", 123 "<->", "-->", "|-"] 124 end; 125structure FolLex = Lexical (FolKey); 126structure FolParsing = Parsing (FolLex); 127 128 129 130 131 132(*** Parsing of First-order terms & formulae ***) 133signature PARSE_FOL = 134 sig 135 val read: string -> Fol.form 136 end; 137 138structure ParseFol : PARSE_FOL = 139 struct 140 local 141 142 open FolParsing 143 (*One or more phrases separated by commas*) 144 fun list ph = ph -- repeat ("," $-- ph) >> (op::); 145 146 (*Either (ph,...,ph) or empty. *) 147 fun pack_ ph = "(" $-- list ph -- $")" >> #1 148 || empty; 149 150 (*Make a quantifier from parsed information*) 151 fun makeQuant ((qnt,b),p) = 152 Fol.Quant(qnt, b, Fol.abstract 0 (Fol.Fun(b,[])) p); 153 154 (*Make a connective*) 155 fun makeConn a p q = Fol.Conn(a, [p,q]); 156 fun makeNeg p = Fol.Conn("~", [p]); 157 158 fun term toks = 159 ( id -- pack_ term >> Fol.Fun 160 || "?" $-- id >> Fol.Var ) toks; 161 162 fun form toks = 163 ( $"ALL" -- id -- "." $-- form >> makeQuant 164 || $"EX" -- id -- "." $-- form >> makeQuant 165 || infixes (primary, Fol.precOf, makeConn) ) toks 166 and primary toks = 167 ( "~" $-- primary >> makeNeg 168 || "(" $-- form -- $")" >> #1 169 || id -- pack_ term >> Fol.Pred ) toks; 170 in 171 val read = reader form 172 end 173 end; 174 175 176(*** Pretty Printing of terms, formulae, and goals ***) 177 178signature DISPLAY_FOL = 179 sig 180 val form: Fol.form -> unit 181 val goal: int -> Fol.goal -> unit 182 end; 183 184structure DisplayFol : DISPLAY_FOL = 185 struct 186 fun enclose sexp = Pretty.blo(1, [Pretty.str"(", sexp, Pretty.str")"]); 187 188 fun commas [] = [] 189 | commas (sexp::sexps) = Pretty.str"," :: Pretty.brk 1 :: 190 sexp :: commas sexps; 191 192 fun list (sexp::sexps) = Pretty.blo(0, sexp :: commas sexps); 193 194 fun term (Fol.Param(a,_)) = Pretty.str a 195 | term (Fol.Var a) = Pretty.str ("?"^a) 196 | term (Fol.Bound i) = Pretty.str "??UNMATCHED INDEX??" 197 | term (Fol.Fun (a,ts)) = Pretty.blo(0, [Pretty.str a, args ts]) 198 and args [] = Pretty.str"" 199 | args ts = enclose (list (map term ts)); 200 201 (*display formula in context of operator with precedence k *) 202 fun formp k (Fol.Pred (a,ts)) = Pretty.blo(0, [Pretty.str a, args ts]) 203 | formp k (Fol.Conn("~", [p])) = 204 Pretty.blo(0, [Pretty.str "~", formp (Fol.precOf "~") p]) 205 | formp k (Fol.Conn(C, [p,q])) = 206 let val pf = formp (Int.max(Fol.precOf C, k)) 207 val sexp = Pretty.blo(0, [pf p, 208 Pretty.str(" "^C), 209 Pretty.brk 1, 210 pf q]) 211 in if (Fol.precOf C <= k) then (enclose sexp) else sexp 212 end 213 | formp k (Fol.Quant(qnt,b,p)) = 214 let val q = Fol.subst 0 (Fol.Fun(b,[])) p 215 val sexp = Pretty.blo(2, 216 [Pretty.str(qnt ^ " " ^ b ^ "."), 217 Pretty.brk 1, 218 formp 0 q]) 219 in if k>0 then (enclose sexp) else sexp end 220 | formp k _ = Pretty.str"??UNKNOWN FORMULA??"; 221 222 fun formList [] = Pretty.str"empty" 223 | formList ps = list (map (formp 0) ps); 224 225 fun form p = Pretty.pr (TextIO.stdOut, formp 0 p, 50); 226 227 fun goal (n:int) (ps,qs) = 228 Pretty.pr (TextIO.stdOut, 229 Pretty.blo (4, [Pretty.str(" " ^ Int.toString n ^ ". "), 230 formList ps, 231 Pretty.brk 2, 232 Pretty.str"|- ", 233 formList qs]), 234 50); 235 end; 236 237 238(**** UNIFICATION ****) 239 240signature UNIFY = 241 sig 242 exception Failed 243 val atoms: Fol.form * Fol.form -> Fol.term StringDict.t 244 val instTerm: Fol.term StringDict.t -> Fol.term -> Fol.term 245 val instForm: Fol.term StringDict.t -> Fol.form -> Fol.form 246 val instGoal: Fol.term StringDict.t -> Fol.goal -> Fol.goal 247 end; 248 249structure Unify : UNIFY = 250 struct 251 exception Failed; 252 253 (*Naive unification of terms containing no bound variables*) 254 fun unifyLists env = 255 let fun chase (Fol.Var a) = (*Chase variable assignments*) 256 (chase(StringDict.lookup(env,a)) 257 handle StringDict.E _ => Fol.Var a) 258 | chase t = t 259 fun occurs a (Fol.Fun(_,ts)) = occsl a ts 260 | occurs a (Fol.Param(_,bs)) = occsl a (map Fol.Var bs) 261 | occurs a (Fol.Var b) = 262 (a=b) orelse (occurs a (StringDict.lookup(env,b)) 263 handle StringDict.E _ => false) 264 | occurs a _ = false 265 and occsl a = List.exists (occurs a) 266 and unify (Fol.Var a, t) = 267 if t = Fol.Var a then env 268 else if occurs a t then raise Failed 269 else StringDict.update(env,a,t) 270 | unify (t, Fol.Var a) = unify (Fol.Var a, t) 271 | unify (Fol.Param(a,_), Fol.Param(b,_)) = 272 if a=b then env else raise Failed 273 | unify (Fol.Fun(a,ts), Fol.Fun(b,us)) = 274 if a=b then unifyl(ts,us) else raise Failed 275 | unify _ = raise Failed 276 and unifyl ([],[]) = env 277 | unifyl (t::ts, u::us) = 278 unifyLists (unify (chase t, chase u)) (ts,us) 279 | unifyl _ = raise Failed 280 in unifyl end 281 282 (*Unification of atomic formulae*) 283 fun atoms (Fol.Pred(a,ts), Fol.Pred(b,us)) = 284 if a=b then unifyLists StringDict.empty (ts,us) 285 else raise Failed 286 | atoms _ = raise Failed; 287 288 (*Instantiate a term by an environment*) 289 fun instTerm env (Fol.Fun(a,ts)) = Fol.Fun(a, map (instTerm env) ts) 290 | instTerm env (Fol.Param(a,bs)) = 291 Fol.Param(a, foldr Fol.termVars [] 292 (map (instTerm env o Fol.Var) bs)) 293 | instTerm env (Fol.Var a) = (instTerm env (StringDict.lookup(env,a)) 294 handle StringDict.E _ => Fol.Var a) 295 | instTerm env t = t; 296 297 (*Instantiate a formula*) 298 fun instForm env (Fol.Pred(a,ts)) = Fol.Pred(a, map (instTerm env) ts) 299 | instForm env (Fol.Conn(b,ps)) = Fol.Conn(b, map (instForm env) ps) 300 | instForm env (Fol.Quant(qnt,b,p)) = Fol.Quant(qnt, b, instForm env p); 301 302 fun instGoal env (ps,qs) = 303 (map (instForm env) ps, map (instForm env) qs); 304 end; 305 306 307 308(**** Rules and proof states -- the abstract type "state" ****) 309 310signature RULE = 311 sig 312 type state 313 type tactic = state -> state ImpSeq.t 314 val main: state -> Fol.form 315 val subgoals: state -> Fol.goal list 316 val initial: Fol.form -> state 317 val final: state -> bool 318 val basic: int -> tactic 319 val unify: int -> tactic 320 val conjL: int -> tactic 321 val conjR: int -> tactic 322 val disjL: int -> tactic 323 val disjR: int -> tactic 324 val impL: int -> tactic 325 val impR: int -> tactic 326 val negL: int -> tactic 327 val negR: int -> tactic 328 val iffL: int -> tactic 329 val iffR: int -> tactic 330 val allL: int -> tactic 331 val allR: int -> tactic 332 val exL: int -> tactic 333 val exR: int -> tactic 334 end; 335 336 337(*Note use of :> for abstraction*) 338structure Rule :> RULE = 339 struct 340 341 (*A state contains subgoals, main goal, variable counter *) 342 datatype state = State of Fol.goal list * Fol.form * int; 343 344 type tactic = state -> state ImpSeq.t; 345 346 fun main (State(gs,p,_)) = p 347 and subgoals (State(gs,p,_)) = gs; 348 349 (*initial state has one subgoal *) 350 fun initial p = State([ ([],[p]) ], p, 0); 351 352 (*final state has no subgoals.*) 353 fun final (State(gs,_,_)) = null gs; 354 355 (*add the goals "newgs" to replace subgoal i*) 356 fun spliceGoals gs newgs i = List.take(gs,i-1) @ newgs @ List.drop(gs,i); 357 358 (*goalF maps goal -> goal list; operator makes a deterministic tactic*) 359 fun propRule goalF i (State(gs,p,n)) = 360 let val gs2 = spliceGoals gs (goalF (List.nth(gs,i-1))) i 361 in ImpSeq.fromList [State(gs2, p, n)] end 362 handle _ => ImpSeq.empty; 363 364 (*for basic sequents: with identical formulae on opposite sides*) 365 val basic = propRule 366 (fn (ps,qs) => 367 if List.exists (fn p => List.exists (fn q => p=q) qs) ps 368 then [] else raise Match); 369 370 (*Solves goal p|-q by unifying p with q. 371 Returns list of successful environments. *) 372 fun unifiable ([], _) = ImpSeq.empty 373 | unifiable (p::ps, qs) = 374 let fun find [] = unifiable (ps,qs) 375 | find (q::qs) = ImpSeq.cons(Unify.atoms(p,q), fn() => find qs) 376 handle Unify.Failed => find qs 377 in find qs end; 378 379 fun inst env (gs,p,n) = 380 State (map (Unify.instGoal env) gs, Unify.instForm env p, n); 381 382 (*for solvable goals with unifiable formulae on opposite sides*) 383 fun unify i (State(gs,p,n)) = 384 let val (ps,qs) = List.nth(gs,i-1) 385 fun next env = inst env (spliceGoals gs [] i, p, n) 386 in ImpSeq.map next (unifiable(ps,qs)) end 387 handle Subscript => ImpSeq.empty; 388 389 390 (*** Tactics for propositional rules ***) 391 392 (* return & delete first formula of the form Conn(a,_,_) *) 393 fun splitConn a qs = 394 let fun get [] = raise Match 395 | get (Fol.Conn(b,ps) :: qs) = if a=b then ps else get qs 396 | get (q::qs) = get qs; 397 fun del [] = [] 398 | del ((q as Fol.Conn(b,_)) :: qs) = if a=b then qs 399 else q :: del qs 400 | del (q::qs) = q :: del qs 401 in (get qs, del qs) end; 402 403 (*leftF transforms left-side formulae to new subgoals*) 404 fun propL a leftF = propRule (fn (ps,qs) => leftF (splitConn a ps, qs)); 405 406 (*rightF transforms right-side formulae to new subgoals*) 407 fun propR a rightF = propRule (fn (ps,qs) => rightF (ps, splitConn a qs)); 408 409 val conjL = propL "&" (fn (([p1,p2], ps), qs) => [(p1::p2::ps, qs)]); 410 411 val conjR = propR "&" 412 (fn (ps, ([q1,q2], qs)) => [(ps, q1::qs), (ps, q2::qs)]); 413 414 val disjL = propL "|" 415 (fn (([p1,p2], ps), qs) => [(p1::ps, qs), (p2::ps, qs)]); 416 417 val disjR = propR "|" (fn (ps, ([q1,q2], qs)) => [(ps, q1::q2::qs)]); 418 419 val impL = propL "-->" 420 (fn (([p1,p2], ps), qs) => [(p2::ps, qs), (ps, p1::qs)]); 421 422 val impR = propR "-->" (fn (ps, ([q1,q2], qs)) => [(q1::ps, q2::qs)]); 423 424 val negL = propL "~" (fn (([p], ps), qs) => [(ps, p::qs)]); 425 426 val negR = propR "~" (fn (ps, ([q], qs)) => [(q::ps, qs)]); 427 428 val iffL = propL "<->" 429 (fn (([p1,p2], ps), qs) => [(p1::p2::ps, qs), (ps, p1::p2::qs)]); 430 431 val iffR = propR "<->" 432 (fn (ps, ([q1,q2], qs)) => [(q1::ps, q2::qs), (q2::ps, q1::qs)]); 433 434 435 (*** Tactics for quantifier rules ***) 436 437 (* return & delete first formula of the form Quant(qnt,_,_) *) 438 fun splitQuant qnt qs = 439 let fun get [] = raise Match 440 | get ((q as Fol.Quant(qnt2,_,p)) :: qs) = if qnt=qnt2 then q 441 else get qs 442 | get (q::qs) = get qs; 443 fun del [] = [] 444 | del ((q as Fol.Quant(qnt2,_,p)) :: qs) = if qnt=qnt2 then qs 445 else q :: del qs 446 | del (q::qs) = q :: del qs 447 in (get qs, del qs) end; 448 449 fun letter n = String.substring("abcdefghijklmnopqrstuvwxyz", n, 1) 450 451 fun gensym n = (* the "_" prevents clashes with user's variable names*) 452 if n<26 then "_" ^ letter n 453 else gensym(n div 26) ^ letter(n mod 26); 454 455 fun quantRule goalF i (State(gs,p,n)) = 456 let val gs2 = spliceGoals gs (goalF (List.nth(gs,i-1), gensym n)) i 457 in ImpSeq.fromList [State(gs2, p, n+1)] end 458 handle _ => ImpSeq.empty; 459 460 val allL = quantRule (fn ((ps,qs), b) => 461 let val (qntForm as Fol.Quant(_,_,p), ps') = splitQuant "ALL" ps 462 val px = Fol.subst 0 (Fol.Var b) p 463 in [(px :: ps' @ [qntForm], qs)] end); 464 465 val allR = quantRule (fn ((ps,qs), b) => 466 let val (Fol.Quant(_,_,q), qs') = splitQuant "ALL" qs 467 val vars = Fol.goalVars ((ps,qs), []) 468 val qx = Fol.subst 0 (Fol.Param(b, vars)) q 469 in [(ps, qx::qs')] end); 470 471 val exL = quantRule (fn ((ps,qs), b) => 472 let val (Fol.Quant(_,_,p), ps') = splitQuant "EX" ps 473 val vars = Fol.goalVars ((ps,qs), []) 474 val px = Fol.subst 0 (Fol.Param(b, vars)) p 475 in [(px::ps', qs)] end); 476 477 val exR = quantRule (fn ((ps,qs), b) => 478 let val (qntForm as Fol.Quant(_,_,q), qs') = splitQuant "EX" qs 479 val qx = Fol.subst 0 (Fol.Var b) q 480 in [(ps, qx :: qs' @ [qntForm])] end); 481 482 end; 483 484 485(**** Commands to modify the top-level proof state 486 Each level of goal stack includes a proof state and alternative states, 487 the output of the tactic applied to the preceeding level. 488 EXERCISE: design and implement better undo facilities. ****) 489 490signature COMMAND = 491 sig 492 val goal: string -> unit 493 val by: Rule.tactic -> unit 494 val pr: Rule.state -> unit 495 val getState: unit -> Rule.state 496 end; 497 498structure Command : COMMAND = 499 struct 500 501 val currState = ref (Rule.initial (Fol.Pred("No goal yet!",[]))); 502 503 fun question (s,z) = " ?" :: s :: z; 504 fun printParam (a,[]) = () (*print a line of parameter table*) 505 | printParam (a,ts) = 506 print (String.concat (a :: " not in " :: 507 foldr question ["\n"] ts)); 508 509 fun printGoals (_, []) = () 510 | printGoals (n, g::gs) = (DisplayFol.goal n g; printGoals (n+1,gs)); 511 512 fun pr st = (*print a proof state*) 513 let val p = Rule.main st 514 and gs = Rule.subgoals st 515 in DisplayFol.form p; 516 if Rule.final st then print "No subgoals left!\n" 517 else (printGoals (1,gs); 518 app printParam (foldr Fol.goalParams [] gs)) 519 end; 520 521 (*print new state, then set it*) 522 fun setState state = (pr state; currState := state); 523 524 val goal = setState o Rule.initial o ParseFol.read; 525 526 fun by tac = setState (ImpSeq.hd (tac (!currState))) 527 handle ImpSeq.Empty => print "** Tactic FAILED! **\n" 528 529 fun getState() = !currState; 530 end; 531 532 533 534(*** Tacticals ***) 535infix 0 |@|; 536 537signature TACTICAL = 538 sig 539 type ('a,'b) multifun (*should be = 'a -> 'b ImpSeq.t*) 540 val -- : ('a,'b) multifun * ('b,'c) multifun -> ('a,'c) multifun 541 val || : ('a,'b) multifun * ('a,'b) multifun -> ('a,'b) multifun 542 val |@| : ('a,'b) multifun * ('a,'b) multifun -> ('a,'b) multifun 543 val all : ('a,'a) multifun 544 val no : ('a,'b) multifun 545 val try : ('a,'a) multifun -> ('a,'a) multifun 546 val repeat : ('a,'a) multifun -> ('a,'a) multifun 547 val repeatDeterm : ('a,'a) multifun -> ('a,'a) multifun 548 val depthFirst : ('a -> bool) -> ('a,'a) multifun -> ('a,'a) multifun 549 val depthIter : ('a -> bool) * int -> ('a,'a) multifun -> ('a,'a) multifun 550 val firstF : ('a -> ('b,'c)multifun) list -> 'a -> ('b,'c)multifun 551 end; 552 553structure Tactical : TACTICAL = 554 struct 555 type ('a,'b)multifun = 'a -> 'b ImpSeq.t 556 557 (*-- performs one tactic followed by another*) 558 fun (tac1 -- tac2) x = ImpSeq.concat (ImpSeq.map tac2 (tac1 x)); 559 560 (*|| commits to the first successful tactic: no backtracking. *) 561 fun (tac1 || tac2) x = 562 let val y = tac1 x 563 in if ImpSeq.null y then tac2 x else y end; 564 565 (*|@| combines the results of two tactics with backtracking.*) 566 fun (tac1 |@| tac2) x = 567 ImpSeq.concat(ImpSeq.cons(tac1 x, (*delay application of tac2!*) 568 fn()=> ImpSeq.cons(tac2 x, 569 fn()=> ImpSeq.empty))); 570 571 (*accepts all states unchanged; identity of --*) 572 fun all x = ImpSeq.fromList [x]; 573 574 (*accepts no states; identity of || and |@|*) 575 fun no x = ImpSeq.empty; 576 577 fun try tac = tac || all; 578 579 (*Performs no backtracking: quits when it gets stuck*) 580 fun repeat tac x = (tac -- repeat tac || all) x; 581 582 fun repeatDeterm tac x = 583 let fun drep x = drep (ImpSeq.hd (tac x)) 584 handle ImpSeq.Empty => x 585 in ImpSeq.fromList [drep x] end; 586 587 (*Repeats again and again until "pred" reports proof tree as satisfied*) 588 fun depthFirst pred tac x = 589 (if pred x then all 590 else tac -- depthFirst pred tac) x; 591 592 fun depthIter (pred,d) tac x = 593 let val next = ImpSeq.toList o tac 594 fun dfs i (y, sf) () = 595 if i<0 then sf() 596 else if i<d andalso pred y 597 then ImpSeq.cons(y, foldr (dfs (i-1)) sf (next y)) 598 else foldr (dfs (i-1)) sf (next y) () 599 fun deepen k = dfs k (x, fn()=> deepen (k+d)) () 600 in deepen 0 end; 601 602 fun orelseF (tac1, tac2) u = tac1 u || tac2 u; 603 604 (*For combining tactic functions*) 605 fun firstF ts = foldr orelseF (fn _ => no) ts; 606 end; 607 608 609signature TAC = 610 sig 611 val safeSteps: int -> Rule.tactic 612 val quant: int -> Rule.tactic 613 val step: int -> Rule.tactic 614 val depth: Rule.tactic 615 val depthIt: int -> Rule.tactic 616 end; 617 618structure Tac : TAC = 619 struct 620 local open Tactical Rule 621 in 622 (*Deterministic; applies one rule to the goal; no unification or variable 623 instantiation; cannot render the goal unprovable.*) 624 val safe = 625 firstF [basic, 626 conjL, disjR, impR, negL, negR, exL, allR, (*1 subgoal*) 627 conjR, disjL, impL, iffL, iffR (*2 subgoals*)]; 628 629 fun safeSteps i = safe i -- repeatDeterm (safe i); 630 631 (*expand a quantifier on the left and the right (if possible!) *) 632 fun quant i = (allL i -- try (exR i)) || exR i; 633 634 val depth = depthFirst final (safeSteps 1 || unify 1 || quant 1); 635 636 fun step i = safeSteps i || (unify i |@| allL i |@| exR i); 637 638 fun depthIt d = depthIter (final, d) (step 1); 639 end 640 end; 641 642 643