1167465Smp(* Title: Provers/quasi.ML 259243Sobrien Author: Oliver Kutter, TU Muenchen 359243Sobrien 459243SobrienReasoner for simple transitivity and quasi orders. 559243Sobrien*) 659243Sobrien 759243Sobrien(* 859243Sobrien 959243SobrienThe package provides tactics trans_tac and quasi_tac that use 1059243Sobrienpremises of the form 1159243Sobrien 1259243Sobrien t = u, t ~= u, t < u and t <= u 1359243Sobrien 1459243Sobriento 1559243Sobrien- either derive a contradiction, in which case the conclusion can be 1659243Sobrien any term, 17100616Smp- or prove the concluson, which must be of the form t ~= u, t < u or 1859243Sobrien t <= u. 1959243Sobrien 2059243SobrienDetails: 2159243Sobrien 2259243Sobrien1. trans_tac: 2359243Sobrien Only premises of form t <= u are used and the conclusion must be of 2459243Sobrien the same form. The conclusion is proved, if possible, by a chain of 2559243Sobrien transitivity from the assumptions. 2659243Sobrien 2759243Sobrien2. quasi_tac: 2859243Sobrien <= is assumed to be a quasi order and < its strict relative, defined 2959243Sobrien as t < u == t <= u & t ~= u. Again, the conclusion is proved from 3059243Sobrien the assumptions. 3159243Sobrien Note that the presence of a strict relation is not necessary for 3259243Sobrien quasi_tac. Configure decomp_quasi to ignore < and ~=. A list of 3359243Sobrien required theorems for both situations is given below. 3459243Sobrien*) 35167465Smp 3659243Sobriensignature LESS_ARITH = 3759243Sobriensig 3859243Sobrien (* Transitivity of <= 3959243Sobrien Note that transitivities for < hold for partial orders only. *) 4059243Sobrien val le_trans: thm (* [| x <= y; y <= z |] ==> x <= z *) 41167465Smp 4259243Sobrien (* Additional theorem for quasi orders *) 43167465Smp val le_refl: thm (* x <= x *) 44167465Smp val eqD1: thm (* x = y ==> x <= y *) 45167465Smp val eqD2: thm (* x = y ==> y <= x *) 46145479Smp 4759243Sobrien (* Additional theorems for premises of the form x < y *) 4859243Sobrien val less_reflE: thm (* x < x ==> P *) 49167465Smp val less_imp_le : thm (* x < y ==> x <= y *) 50167465Smp 5159243Sobrien (* Additional theorems for premises of the form x ~= y *) 5259243Sobrien val le_neq_trans : thm (* [| x <= y ; x ~= y |] ==> x < y *) 53167465Smp val neq_le_trans : thm (* [| x ~= y ; x <= y |] ==> x < y *) 5459243Sobrien 5559243Sobrien (* Additional theorem for goals of form x ~= y *) 5659243Sobrien val less_imp_neq : thm (* x < y ==> x ~= y *) 5759243Sobrien 58167465Smp (* Analysis of premises and conclusion *) 59167465Smp (* decomp_x (`x Rel y') should yield SOME (x, Rel, y) 6059243Sobrien where Rel is one of "<", "<=", "=" and "~=", 61167465Smp other relation symbols cause an error message *) 62167465Smp (* decomp_trans is used by trans_tac, it may only return Rel = "<=" *) 63167465Smp val decomp_trans: theory -> term -> (term * string * term) option 64167465Smp (* decomp_quasi is used by quasi_tac *) 65167465Smp val decomp_quasi: theory -> term -> (term * string * term) option 6659243Sobrienend; 6759243Sobrien 68167465Smpsignature QUASI_TAC = 69167465Smpsig 70167465Smp val trans_tac: Proof.context -> int -> tactic 7159243Sobrien val quasi_tac: Proof.context -> int -> tactic 72167465Smpend; 73167465Smp 7459243Sobrienfunctor Quasi_Tac(Less: LESS_ARITH): QUASI_TAC = 7559243Sobrienstruct 7659243Sobrien 7759243Sobrien(* Internal datatype for the proof *) 7859243Sobriendatatype proof 7959243Sobrien = Asm of int 80167465Smp | Thm of proof list * thm; 8159243Sobrien 8259243Sobrienexception Cannot; 83167465Smp (* Internal exception, raised if conclusion cannot be derived from 84167465Smp assumptions. *) 8559243Sobrienexception Contr of proof; 86167465Smp (* Internal exception, raised if contradiction ( x < x ) was derived *) 87167465Smp 8859243Sobrienfun prove asms = 8959243Sobrien let 9059243Sobrien fun pr (Asm i) = nth asms i 9159243Sobrien | pr (Thm (prfs, thm)) = map pr prfs MRS thm; 9259243Sobrien in pr end; 9359243Sobrien 9459243Sobrien(* Internal datatype for inequalities *) 9559243Sobriendatatype less 9659243Sobrien = Less of term * term * proof 9759243Sobrien | Le of term * term * proof 9859243Sobrien | NotEq of term * term * proof; 9959243Sobrien 10059243Sobrien (* Misc functions for datatype less *) 10159243Sobrienfun lower (Less (x, _, _)) = x 10259243Sobrien | lower (Le (x, _, _)) = x 10359243Sobrien | lower (NotEq (x,_,_)) = x; 10459243Sobrien 10559243Sobrienfun upper (Less (_, y, _)) = y 10659243Sobrien | upper (Le (_, y, _)) = y 10759243Sobrien | upper (NotEq (_,y,_)) = y; 10859243Sobrien 10959243Sobrienfun getprf (Less (_, _, p)) = p 110167465Smp| getprf (Le (_, _, p)) = p 11159243Sobrien| getprf (NotEq (_,_, p)) = p; 11259243Sobrien 11359243Sobrien(* ************************************************************************ *) 11459243Sobrien(* *) 11559243Sobrien(* mkasm_trans sign (t, n) : theory -> (Term.term * int) -> less *) 11659243Sobrien(* *) 11759243Sobrien(* Tuple (t, n) (t an assumption, n its index in the assumptions) is *) 11859243Sobrien(* translated to an element of type less. *) 11959243Sobrien(* Only assumptions of form x <= y are used, all others are ignored *) 12059243Sobrien(* *) 12159243Sobrien(* ************************************************************************ *) 12259243Sobrien 12359243Sobrienfun mkasm_trans thy (t, n) = 12459243Sobrien case Less.decomp_trans thy t of 12559243Sobrien SOME (x, rel, y) => 12659243Sobrien (case rel of 12759243Sobrien "<=" => [Le (x, y, Asm n)] 12859243Sobrien | _ => error ("trans_tac: unknown relation symbol ``" ^ rel ^ 12959243Sobrien "''returned by decomp_trans.")) 13059243Sobrien | NONE => []; 13159243Sobrien 132167465Smp(* ************************************************************************ *) 133167465Smp(* *) 13459243Sobrien(* mkasm_quasi sign (t, n) : theory -> (Term.term * int) -> less *) 135167465Smp(* *) 136167465Smp(* Tuple (t, n) (t an assumption, n its index in the assumptions) is *) 13759243Sobrien(* translated to an element of type less. *) 13859243Sobrien(* Quasi orders only. *) 13959243Sobrien(* *) 14059243Sobrien(* ************************************************************************ *) 14159243Sobrien 14259243Sobrienfun mkasm_quasi thy (t, n) = 14359243Sobrien case Less.decomp_quasi thy t of 14459243Sobrien SOME (x, rel, y) => (case rel of 14559243Sobrien "<" => if (x aconv y) then raise Contr (Thm ([Asm n], Less.less_reflE)) 146167465Smp else [Less (x, y, Asm n)] 14759243Sobrien | "<=" => [Le (x, y, Asm n)] 14859243Sobrien | "=" => [Le (x, y, Thm ([Asm n], Less.eqD1)), 14959243Sobrien Le (y, x, Thm ([Asm n], Less.eqD2))] 150167465Smp | "~=" => if (x aconv y) then 151167465Smp raise Contr (Thm ([(Thm ([(Thm ([], Less.le_refl)) ,(Asm n)], Less.le_neq_trans))], Less.less_reflE)) 152167465Smp else [ NotEq (x, y, Asm n), 153167465Smp NotEq (y, x,Thm ( [Asm n], @{thm not_sym}))] 154167465Smp | _ => error ("quasi_tac: unknown relation symbol ``" ^ rel ^ 155167465Smp "''returned by decomp_quasi.")) 156167465Smp | NONE => []; 157167465Smp 15859243Sobrien 15959243Sobrien(* ************************************************************************ *) 16059243Sobrien(* *) 16159243Sobrien(* mkconcl_trans sign t : theory -> Term.term -> less *) 16259243Sobrien(* *) 163(* Translates conclusion t to an element of type less. *) 164(* Only for Conclusions of form x <= y or x < y. *) 165(* *) 166(* ************************************************************************ *) 167 168 169fun mkconcl_trans thy t = 170 case Less.decomp_trans thy t of 171 SOME (x, rel, y) => (case rel of 172 "<=" => (Le (x, y, Asm ~1), Asm 0) 173 | _ => raise Cannot) 174 | NONE => raise Cannot; 175 176 177(* ************************************************************************ *) 178(* *) 179(* mkconcl_quasi sign t : theory -> Term.term -> less *) 180(* *) 181(* Translates conclusion t to an element of type less. *) 182(* Quasi orders only. *) 183(* *) 184(* ************************************************************************ *) 185 186fun mkconcl_quasi thy t = 187 case Less.decomp_quasi thy t of 188 SOME (x, rel, y) => (case rel of 189 "<" => ([Less (x, y, Asm ~1)], Asm 0) 190 | "<=" => ([Le (x, y, Asm ~1)], Asm 0) 191 | "~=" => ([NotEq (x,y, Asm ~1)], Asm 0) 192 | _ => raise Cannot) 193| NONE => raise Cannot; 194 195 196(* ******************************************************************* *) 197(* *) 198(* mergeLess (less1,less2): less * less -> less *) 199(* *) 200(* Merge to elements of type less according to the following rules *) 201(* *) 202(* x <= y && y <= z ==> x <= z *) 203(* x <= y && x ~= y ==> x < y *) 204(* x ~= y && x <= y ==> x < y *) 205(* *) 206(* ******************************************************************* *) 207 208fun mergeLess (Le (x, _, p) , Le (_ , z, q)) = 209 Le (x, z, Thm ([p,q] , Less.le_trans)) 210| mergeLess (Le (x, z, p) , NotEq (x', z', q)) = 211 if (x aconv x' andalso z aconv z' ) 212 then Less (x, z, Thm ([p,q] , Less.le_neq_trans)) 213 else error "quasi_tac: internal error le_neq_trans" 214| mergeLess (NotEq (x, z, p) , Le (x' , z', q)) = 215 if (x aconv x' andalso z aconv z') 216 then Less (x, z, Thm ([p,q] , Less.neq_le_trans)) 217 else error "quasi_tac: internal error neq_le_trans" 218| mergeLess (_, _) = 219 error "quasi_tac: internal error: undefined case"; 220 221 222(* ******************************************************************** *) 223(* tr checks for valid transitivity step *) 224(* ******************************************************************** *) 225 226infix tr; 227fun (Le (_, y, _)) tr (Le (x', _, _)) = ( y aconv x' ) 228 | _ tr _ = false; 229 230(* ******************************************************************* *) 231(* *) 232(* transPath (Lesslist, Less): (less list * less) -> less *) 233(* *) 234(* If a path represented by a list of elements of type less is found, *) 235(* this needs to be contracted to a single element of type less. *) 236(* Prior to each transitivity step it is checked whether the step is *) 237(* valid. *) 238(* *) 239(* ******************************************************************* *) 240 241fun transPath ([],lesss) = lesss 242| transPath (x::xs,lesss) = 243 if lesss tr x then transPath (xs, mergeLess(lesss,x)) 244 else error "trans/quasi_tac: internal error transpath"; 245 246(* ******************************************************************* *) 247(* *) 248(* less1 subsumes less2 : less -> less -> bool *) 249(* *) 250(* subsumes checks whether less1 implies less2 *) 251(* *) 252(* ******************************************************************* *) 253 254infix subsumes; 255fun (Le (x, y, _)) subsumes (Le (x', y', _)) = 256 (x aconv x' andalso y aconv y') 257 | (Le _) subsumes (Less _) = 258 error "trans/quasi_tac: internal error: Le cannot subsume Less" 259 | (NotEq(x,y,_)) subsumes (NotEq(x',y',_)) = x aconv x' andalso y aconv y' orelse x aconv y' andalso y aconv x' 260 | _ subsumes _ = false; 261 262(* ******************************************************************* *) 263(* *) 264(* triv_solv less1 : less -> proof option *) 265(* *) 266(* Solves trivial goal x <= x. *) 267(* *) 268(* ******************************************************************* *) 269 270fun triv_solv (Le (x, x', _)) = 271 if x aconv x' then SOME (Thm ([], Less.le_refl)) 272 else NONE 273| triv_solv _ = NONE; 274 275(* ********************************************************************* *) 276(* Graph functions *) 277(* ********************************************************************* *) 278 279(* *********************************************************** *) 280(* Functions for constructing graphs *) 281(* *********************************************************** *) 282 283fun addEdge (v,d,[]) = [(v,d)] 284| addEdge (v,d,((u,dl)::el)) = if v aconv u then ((v,d@dl)::el) 285 else (u,dl):: (addEdge(v,d,el)); 286 287(* ********************************************************************** *) 288(* *) 289(* mkQuasiGraph constructs from a list of objects of type less a graph g, *) 290(* by taking all edges that are candidate for a <=, and a list neqE, by *) 291(* taking all edges that are candiate for a ~= *) 292(* *) 293(* ********************************************************************** *) 294 295fun mkQuasiGraph [] = ([],[]) 296| mkQuasiGraph lessList = 297 let 298 fun buildGraphs ([],leG, neqE) = (leG, neqE) 299 | buildGraphs (l::ls, leG, neqE) = case l of 300 (Less (x,y,p)) => 301 let 302 val leEdge = Le (x,y, Thm ([p], Less.less_imp_le)) 303 val neqEdges = [ NotEq (x,y, Thm ([p], Less.less_imp_neq)), 304 NotEq (y,x, Thm ( [Thm ([p], Less.less_imp_neq)], @{thm not_sym}))] 305 in 306 buildGraphs (ls, addEdge(y,[],(addEdge (x,[(y,leEdge)],leG))), neqEdges@neqE) 307 end 308 | (Le (x,y,p)) => buildGraphs (ls, addEdge(y,[],(addEdge (x,[(y,l)],leG))), neqE) 309 | _ => buildGraphs (ls, leG, l::neqE) ; 310 311in buildGraphs (lessList, [], []) end; 312 313(* ********************************************************************** *) 314(* *) 315(* mkGraph constructs from a list of objects of type less a graph g *) 316(* Used for plain transitivity chain reasoning. *) 317(* *) 318(* ********************************************************************** *) 319 320fun mkGraph [] = [] 321| mkGraph lessList = 322 let 323 fun buildGraph ([],g) = g 324 | buildGraph (l::ls, g) = buildGraph (ls, (addEdge ((lower l),[((upper l),l)],g))) 325 326in buildGraph (lessList, []) end; 327 328(* *********************************************************************** *) 329(* *) 330(* adjacent g u : (''a * 'b list ) list -> ''a -> 'b list *) 331(* *) 332(* List of successors of u in graph g *) 333(* *) 334(* *********************************************************************** *) 335 336fun adjacent eq_comp ((v,adj)::el) u = 337 if eq_comp (u, v) then adj else adjacent eq_comp el u 338| adjacent _ [] _ = [] 339 340(* *********************************************************************** *) 341(* *) 342(* dfs eq_comp g u v: *) 343(* ('a * 'a -> bool) -> ('a *( 'a * less) list) list -> *) 344(* 'a -> 'a -> (bool * ('a * less) list) *) 345(* *) 346(* Depth first search of v from u. *) 347(* Returns (true, path(u, v)) if successful, otherwise (false, []). *) 348(* *) 349(* *********************************************************************** *) 350 351fun dfs eq_comp g u v = 352 let 353 val pred = Unsynchronized.ref []; 354 val visited = Unsynchronized.ref []; 355 356 fun been_visited v = exists (fn w => eq_comp (w, v)) (!visited) 357 358 fun dfs_visit u' = 359 let val _ = visited := u' :: (!visited) 360 361 fun update (x,l) = let val _ = pred := (x,l) ::(!pred) in () end; 362 363 in if been_visited v then () 364 else (List.app (fn (v',l) => if been_visited v' then () else ( 365 update (v',l); 366 dfs_visit v'; ()) )) (adjacent eq_comp g u') 367 end 368 in 369 dfs_visit u; 370 if (been_visited v) then (true, (!pred)) else (false , []) 371 end; 372 373(* ************************************************************************ *) 374(* *) 375(* Begin: Quasi Order relevant functions *) 376(* *) 377(* *) 378(* ************************************************************************ *) 379 380(* ************************************************************************ *) 381(* *) 382(* findPath x y g: Term.term -> Term.term -> *) 383(* (Term.term * (Term.term * less list) list) -> *) 384(* (bool, less list) *) 385(* *) 386(* Searches a path from vertex x to vertex y in Graph g, returns true and *) 387(* the list of edges forming the path, if a path is found, otherwise false *) 388(* and nil. *) 389(* *) 390(* ************************************************************************ *) 391 392 393 fun findPath x y g = 394 let 395 val (found, tmp) = dfs (op aconv) g x y ; 396 val pred = map snd tmp; 397 398 fun path x y = 399 let 400 (* find predecessor u of node v and the edge u -> v *) 401 fun lookup v [] = raise Cannot 402 | lookup v (e::es) = if (upper e) aconv v then e else lookup v es; 403 404 (* traverse path backwards and return list of visited edges *) 405 fun rev_path v = 406 let val l = lookup v pred 407 val u = lower l; 408 in 409 if u aconv x then [l] else (rev_path u) @ [l] 410 end 411 in rev_path y end; 412 413 in 414 if found then ( 415 if x aconv y then (found,[(Le (x, y, (Thm ([], Less.le_refl))))]) 416 else (found, (path x y) )) 417 else (found,[]) 418 end; 419 420 421(* ************************************************************************ *) 422(* *) 423(* findQuasiProof (leqG, neqE) subgoal: *) 424(* (Term.term * (Term.term * less list) list) * less list -> less -> proof *) 425(* *) 426(* Constructs a proof for subgoal by searching a special path in leqG and *) 427(* neqE. Raises Cannot if construction of the proof fails. *) 428(* *) 429(* ************************************************************************ *) 430 431 432(* As the conlusion can be either of form x <= y, x < y or x ~= y we have *) 433(* three cases to deal with. Finding a transitivity path from x to y with label *) 434(* 1. <= *) 435(* This is simply done by searching any path from x to y in the graph leG. *) 436(* The graph leG contains only edges with label <=. *) 437(* *) 438(* 2. < *) 439(* A path from x to y with label < can be found by searching a path with *) 440(* label <= from x to y in the graph leG and merging the path x <= y with *) 441(* a parallel edge x ~= y resp. y ~= x to x < y. *) 442(* *) 443(* 3. ~= *) 444(* If the conclusion is of form x ~= y, we can find a proof either directly, *) 445(* if x ~= y or y ~= x are among the assumptions, or by constructing x ~= y if *) 446(* x < y or y < x follows from the assumptions. *) 447 448fun findQuasiProof (leG, neqE) subgoal = 449 case subgoal of (Le (x,y, _)) => ( 450 let 451 val (xyLefound,xyLePath) = findPath x y leG 452 in 453 if xyLefound then ( 454 let 455 val Le_x_y = (transPath (tl xyLePath, hd xyLePath)) 456 in getprf Le_x_y end ) 457 else raise Cannot 458 end ) 459 | (Less (x,y,_)) => ( 460 let 461 fun findParallelNeq [] = NONE 462 | findParallelNeq (e::es) = 463 if (x aconv (lower e) andalso y aconv (upper e)) then SOME e 464 else if (y aconv (lower e) andalso x aconv (upper e)) 465 then SOME (NotEq (x,y, (Thm ([getprf e], @{thm not_sym})))) 466 else findParallelNeq es; 467 in 468 (* test if there is a edge x ~= y respectivly y ~= x and *) 469 (* if it possible to find a path x <= y in leG, thus we can conclude x < y *) 470 (case findParallelNeq neqE of (SOME e) => 471 let 472 val (xyLeFound,xyLePath) = findPath x y leG 473 in 474 if xyLeFound then ( 475 let 476 val Le_x_y = (transPath (tl xyLePath, hd xyLePath)) 477 val Less_x_y = mergeLess (e, Le_x_y) 478 in getprf Less_x_y end 479 ) else raise Cannot 480 end 481 | _ => raise Cannot) 482 end ) 483 | (NotEq (x,y,_)) => 484 (* First check if a single premiss is sufficient *) 485 (case (find_first (fn fact => fact subsumes subgoal) neqE, subgoal) of 486 (SOME (NotEq (x, y, p)), NotEq (x', y', _)) => 487 if (x aconv x' andalso y aconv y') then p 488 else Thm ([p], @{thm not_sym}) 489 | _ => raise Cannot 490 ) 491 492 493(* ************************************************************************ *) 494(* *) 495(* End: Quasi Order relevant functions *) 496(* *) 497(* *) 498(* ************************************************************************ *) 499 500(* *********************************************************************** *) 501(* *) 502(* solveLeTrans sign (asms,concl) : *) 503(* theory -> less list * Term.term -> proof list *) 504(* *) 505(* Solves *) 506(* *) 507(* *********************************************************************** *) 508 509fun solveLeTrans thy (asms, concl) = 510 let 511 val g = mkGraph asms 512 in 513 let 514 val (subgoal, prf) = mkconcl_trans thy concl 515 val (found, path) = findPath (lower subgoal) (upper subgoal) g 516 in 517 if found then [getprf (transPath (tl path, hd path))] 518 else raise Cannot 519 end 520 end; 521 522 523(* *********************************************************************** *) 524(* *) 525(* solveQuasiOrder sign (asms,concl) : *) 526(* theory -> less list * Term.term -> proof list *) 527(* *) 528(* Find proof if possible for quasi order. *) 529(* *) 530(* *********************************************************************** *) 531 532fun solveQuasiOrder thy (asms, concl) = 533 let 534 val (leG, neqE) = mkQuasiGraph asms 535 in 536 let 537 val (subgoals, prf) = mkconcl_quasi thy concl 538 fun solve facts less = 539 (case triv_solv less of NONE => findQuasiProof (leG, neqE) less 540 | SOME prf => prf ) 541 in map (solve asms) subgoals end 542 end; 543 544(* ************************************************************************ *) 545(* *) 546(* Tactics *) 547(* *) 548(* - trans_tac *) 549(* - quasi_tac, solves quasi orders *) 550(* ************************************************************************ *) 551 552 553(* trans_tac - solves transitivity chains over <= *) 554 555fun trans_tac ctxt = SUBGOAL (fn (A, n) => fn st => 556 let 557 val thy = Proof_Context.theory_of ctxt; 558 val rfrees = map Free (Term.rename_wrt_term A (Logic.strip_params A)); 559 val Hs = map (fn H => subst_bounds (rfrees, H)) (Logic.strip_assums_hyp A); 560 val C = subst_bounds (rfrees, Logic.strip_assums_concl A); 561 val lesss = flat (map_index (mkasm_trans thy o swap) Hs); 562 val prfs = solveLeTrans thy (lesss, C); 563 564 val (subgoal, prf) = mkconcl_trans thy C; 565 in 566 Subgoal.FOCUS (fn {context = ctxt', prems, ...} => 567 let val thms = map (prove prems) prfs 568 in resolve_tac ctxt' [prove thms prf] 1 end) ctxt n st 569 end 570 handle Contr p => 571 Subgoal.FOCUS (fn {context = ctxt', prems, ...} => 572 resolve_tac ctxt' [prove prems p] 1) ctxt n st 573 | Cannot => Seq.empty); 574 575 576(* quasi_tac - solves quasi orders *) 577 578fun quasi_tac ctxt = SUBGOAL (fn (A, n) => fn st => 579 let 580 val thy = Proof_Context.theory_of ctxt 581 val rfrees = map Free (Term.rename_wrt_term A (Logic.strip_params A)); 582 val Hs = map (fn H => subst_bounds (rfrees, H)) (Logic.strip_assums_hyp A); 583 val C = subst_bounds (rfrees, Logic.strip_assums_concl A); 584 val lesss = flat (map_index (mkasm_quasi thy o swap) Hs); 585 val prfs = solveQuasiOrder thy (lesss, C); 586 val (subgoals, prf) = mkconcl_quasi thy C; 587 in 588 Subgoal.FOCUS (fn {context = ctxt', prems, ...} => 589 let val thms = map (prove prems) prfs 590 in resolve_tac ctxt' [prove thms prf] 1 end) ctxt n st 591 end 592 handle Contr p => 593 (Subgoal.FOCUS (fn {context = ctxt', prems, ...} => 594 resolve_tac ctxt' [prove prems p] 1) ctxt n st handle General.Subscript => Seq.empty) 595 | Cannot => Seq.empty 596 | General.Subscript => Seq.empty); 597 598end; 599