1(* Title: src/Provers/preorder.ML 2 Author: Oliver Kutter, TU Muenchen 3 4Reasoner for simple transitivity and quasi orders. 5*) 6 7(* 8 9The package provides tactics trans_tac and quasi_tac that use 10premises of the form 11 12 t = u, t ~= u, t < u and t <= u 13 14to 15- either derive a contradiction, in which case the conclusion can be 16 any term, 17- or prove the concluson, which must be of the form t ~= u, t < u or 18 t <= u. 19 20Details: 21 221. trans_tac: 23 Only premises of form t <= u are used and the conclusion must be of 24 the same form. The conclusion is proved, if possible, by a chain of 25 transitivity from the assumptions. 26 272. quasi_tac: 28 <= is assumed to be a quasi order and < its strict relative, defined 29 as t < u == t <= u & t ~= u. Again, the conclusion is proved from 30 the assumptions. 31 Note that the presence of a strict relation is not necessary for 32 quasi_tac. Configure decomp_quasi to ignore < and ~=. A list of 33 required theorems for both situations is given below. 34*) 35 36signature LESS_ARITH = 37sig 38 (* Transitivity of <= 39 Note that transitivities for < hold for partial orders only. *) 40 val le_trans: thm (* [| x <= y; y <= z |] ==> x <= z *) 41 42 (* Additional theorem for quasi orders *) 43 val le_refl: thm (* x <= x *) 44 val eqD1: thm (* x = y ==> x <= y *) 45 val eqD2: thm (* x = y ==> y <= x *) 46 47 (* Additional theorems for premises of the form x < y *) 48 val less_reflE: thm (* x < x ==> P *) 49 val less_imp_le : thm (* x < y ==> x <= y *) 50 51 (* Additional theorems for premises of the form x ~= y *) 52 val le_neq_trans : thm (* [| x <= y ; x ~= y |] ==> x < y *) 53 val neq_le_trans : thm (* [| x ~= y ; x <= y |] ==> x < y *) 54 55 (* Additional theorem for goals of form x ~= y *) 56 val less_imp_neq : thm (* x < y ==> x ~= y *) 57 58 (* Analysis of premises and conclusion *) 59 (* decomp_x (`x Rel y') should yield SOME (x, Rel, y) 60 where Rel is one of "<", "<=", "=" and "~=", 61 other relation symbols cause an error message *) 62 (* decomp_trans is used by trans_tac, it may only return Rel = "<=" *) 63 val decomp_trans: theory -> term -> (term * string * term) option 64 (* decomp_quasi is used by quasi_tac *) 65 val decomp_quasi: theory -> term -> (term * string * term) option 66end; 67 68signature QUASI_TAC = 69sig 70 val trans_tac: Proof.context -> int -> tactic 71 val quasi_tac: Proof.context -> int -> tactic 72end; 73 74functor Quasi_Tac(Less: LESS_ARITH): QUASI_TAC = 75struct 76 77(* Internal datatype for the proof *) 78datatype proof 79 = Asm of int 80 | Thm of proof list * thm; 81 82exception Cannot; 83 (* Internal exception, raised if conclusion cannot be derived from 84 assumptions. *) 85exception Contr of proof; 86 (* Internal exception, raised if contradiction ( x < x ) was derived *) 87 88fun prove asms = 89 let 90 fun pr (Asm i) = nth asms i 91 | pr (Thm (prfs, thm)) = map pr prfs MRS thm; 92 in pr end; 93 94(* Internal datatype for inequalities *) 95datatype less 96 = Less of term * term * proof 97 | Le of term * term * proof 98 | NotEq of term * term * proof; 99 100 (* Misc functions for datatype less *) 101fun lower (Less (x, _, _)) = x 102 | lower (Le (x, _, _)) = x 103 | lower (NotEq (x,_,_)) = x; 104 105fun upper (Less (_, y, _)) = y 106 | upper (Le (_, y, _)) = y 107 | upper (NotEq (_,y,_)) = y; 108 109fun getprf (Less (_, _, p)) = p 110| getprf (Le (_, _, p)) = p 111| getprf (NotEq (_,_, p)) = p; 112 113(* ************************************************************************ *) 114(* *) 115(* mkasm_trans sign (t, n) : theory -> (Term.term * int) -> less *) 116(* *) 117(* Tuple (t, n) (t an assumption, n its index in the assumptions) is *) 118(* translated to an element of type less. *) 119(* Only assumptions of form x <= y are used, all others are ignored *) 120(* *) 121(* ************************************************************************ *) 122 123fun mkasm_trans thy (t, n) = 124 case Less.decomp_trans thy t of 125 SOME (x, rel, y) => 126 (case rel of 127 "<=" => [Le (x, y, Asm n)] 128 | _ => error ("trans_tac: unknown relation symbol ``" ^ rel ^ 129 "''returned by decomp_trans.")) 130 | NONE => []; 131 132(* ************************************************************************ *) 133(* *) 134(* mkasm_quasi sign (t, n) : theory -> (Term.term * int) -> less *) 135(* *) 136(* Tuple (t, n) (t an assumption, n its index in the assumptions) is *) 137(* translated to an element of type less. *) 138(* Quasi orders only. *) 139(* *) 140(* ************************************************************************ *) 141 142fun mkasm_quasi thy (t, n) = 143 case Less.decomp_quasi thy t of 144 SOME (x, rel, y) => (case rel of 145 "<" => if (x aconv y) then raise Contr (Thm ([Asm n], Less.less_reflE)) 146 else [Less (x, y, Asm n)] 147 | "<=" => [Le (x, y, Asm n)] 148 | "=" => [Le (x, y, Thm ([Asm n], Less.eqD1)), 149 Le (y, x, Thm ([Asm n], Less.eqD2))] 150 | "~=" => if (x aconv y) then 151 raise Contr (Thm ([(Thm ([(Thm ([], Less.le_refl)) ,(Asm n)], Less.le_neq_trans))], Less.less_reflE)) 152 else [ NotEq (x, y, Asm n), 153 NotEq (y, x,Thm ( [Asm n], @{thm not_sym}))] 154 | _ => error ("quasi_tac: unknown relation symbol ``" ^ rel ^ 155 "''returned by decomp_quasi.")) 156 | NONE => []; 157 158 159(* ************************************************************************ *) 160(* *) 161(* mkconcl_trans sign t : theory -> Term.term -> less *) 162(* *) 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