# HG changeset patch # User ballarin # Date 1078744663 -3600 # Node ID 4392cb82018b4bb115201f13ff60dd5e31d5b3d2 # Parent 24724afce166d111e7a907039292a9e1f6ba888a Bug-fixes for transitivity reasoner. diff -r 24724afce166 -r 4392cb82018b src/HOL/Library/Multiset.thy --- a/src/HOL/Library/Multiset.thy Mon Mar 08 12:16:57 2004 +0100 +++ b/src/HOL/Library/Multiset.thy Mon Mar 08 12:17:43 2004 +0100 @@ -801,7 +801,6 @@ apply (rule one_step_implies_mult) apply (simp only: trans_def) apply auto - apply (blast intro: order_less_trans) done theorem union_upper1: "A <= A + (B::'a::order multiset)" diff -r 24724afce166 -r 4392cb82018b src/Provers/order.ML --- a/src/Provers/order.ML Mon Mar 08 12:16:57 2004 +0100 +++ b/src/Provers/order.ML Mon Mar 08 12:17:43 2004 +0100 @@ -5,7 +5,7 @@ Copyright: TU Muenchen *) -(* TODO: reduce number of input thms, reduce code duplication *) +(* TODO: reduce number of input thms *) (* @@ -73,7 +73,6 @@ struct (* Extract subgoal with signature *) - fun SUBGOAL goalfun i st = goalfun (List.nth(prems_of st, i-1), i, sign_of_thm st) st handle Subscript => Seq.empty; @@ -84,7 +83,7 @@ | Thm of proof list * thm; exception Cannot; - (* Internal exception, raised if conclusion cannot be derived from + (* Internal exception, raised if conclusion cannot be derived from assumptions. *) exception Contr of proof; (* Internal exception, raised if contradiction ( x < x ) was derived *) @@ -99,7 +98,6 @@ = Less of term * term * proof | Le of term * term * proof | NotEq of term * term * proof; - (* Misc functions for datatype less *) fun lower (Less (x, _, _)) = x @@ -114,7 +112,6 @@ | getprf (Le (_, _, p)) = p | getprf (NotEq (_,_, p)) = p; - (* ************************************************************************ *) (* *) (* mkasm_partial sign (t, n) : Sign.sg -> (Term.term * int) -> less *) @@ -138,13 +135,11 @@ | "~=" => if (x aconv y) then raise Contr (Thm ([(Thm ([(Thm ([], Less.le_refl)) ,(Asm n)], Less.le_neq_trans))], Less.less_reflE)) else [ NotEq (x, y, Asm n), - NotEq (y, x,Thm ( [Asm n], thm "not_sym"))] (* Le (x, x, Thm ([],Less.le_refl))]*) + NotEq (y, x,Thm ( [Asm n], thm "not_sym"))] | _ => error ("partial_tac: unknown relation symbol ``" ^ rel ^ "''returned by decomp_part.")) | None => []; - - (* ************************************************************************ *) (* *) (* mkasm_linear sign (t, n) : Sign.sg -> (Term.term * int) -> less *) @@ -175,7 +170,6 @@ "''returned by decomp_lin.")) | None => []; - (* ************************************************************************ *) (* *) (* mkconcl_partial sign t : Sign.sg -> Term.term -> less *) @@ -196,7 +190,6 @@ | _ => raise Cannot) | None => raise Cannot; - (* ************************************************************************ *) (* *) (* mkconcl_linear sign t : Sign.sg -> Term.term -> less *) @@ -219,8 +212,6 @@ | _ => raise Cannot) | None => raise Cannot; - - (* ******************************************************************* *) (* *) (* mergeLess (less1,less2): less * less -> less *) @@ -342,33 +333,21 @@ (* *) (* Inequalities are represented by various types of graphs. *) (* *) -(* 1. (Term.term * Term.term list) list *) -(* - Graph of this type is generated from the assumptions, *) -(* does not contain information on which edge stems from which *) -(* assumption. *) -(* - Used to compute strong components. *) -(* *) -(* 2. (Term.term * (Term.term * less) list) list *) +(* 1. (Term.term * (Term.term * less) list) list *) (* - Graph of this type is generated from the assumptions, *) (* it does contain information on which edge stems from which *) (* assumption. *) -(* - Used to reconstruct paths. *) +(* - Used to compute strongly connected components *) +(* - Used to compute component subgraphs *) +(* - Used for component subgraphs to reconstruct paths in components*) (* *) -(* 3. (int * (int * less) list ) list *) +(* 2. (int * (int * less) list ) list *) (* - Graph of this type is generated from the strong components of *) -(* graph of type 2. It consists of the strong components of *) -(* graph 2, where nodes are indices of the components. *) +(* graph of type 1. It consists of the strong components of *) +(* graph 1, where nodes are indices of the components. *) (* Only edges between components are part of this graph. *) (* - Used to reconstruct paths between several components. *) (* *) -(* 4. (int * int list) list *) -(* - Graph of this type is generated from graph of type 3, but *) -(* edge information of type less is removed. *) -(* - Used to *) -(* - Compute transposed graphs of type 4. *) -(* - Compute list of components reachable from a component. *) -(* *) -(* *) (* ******************************************************************* *) @@ -376,104 +355,48 @@ (* Functions for constructing graphs *) (* *********************************************************** *) -fun addLessEdge (v,d,[]) = [(v,d)] -| addLessEdge (v,d,((u,dl)::el)) = if v aconv u then ((v,d@dl)::el) - else (u,dl):: (addLessEdge(v,d,el)); - -fun addTermEdge (v,u,[]) = [(v,[u])] -| addTermEdge (v,u,((x,adj)::el)) = if v aconv x then (v,u::adj)::el - else (x,adj) :: addTermEdge (v,u,el); +fun addEdge (v,d,[]) = [(v,d)] +| addEdge (v,d,((u,dl)::el)) = if v aconv u then ((v,d@dl)::el) + else (u,dl):: (addEdge(v,d,el)); (* ********************************************************************* *) (* *) -(* buildGraphs constructs three graphs from a list of type less: *) -(* g1: graph for the <= relation *) -(* g2: graph for the <= relation with additional information for *) -(* proof reconstruction *) -(* neqEdges: all edges that are candidates for a ~= *) +(* mkGraphs constructs from a list of objects of type less a graph g, *) +(* by taking all edges that are candidate for a <=, and a list neqE, by *) +(* taking all edges that are candiate for a ~= *) (* *) (* ********************************************************************* *) +fun mkGraphs [] = ([],[],[]) +| mkGraphs lessList = + let -fun buildGraphs ([],g1,g2,neqEdges) = (g1, g2, neqEdges) -| buildGraphs (l::ls,g1,g2,neqEdges) = case l of -(Less (x,y,p)) =>( - let val g1' = addTermEdge (x,y,g1) - and g2' = addLessEdge (x,[(y,(Less (x, y, p)))],g2) - in buildGraphs (ls,g1',g2',l::neqEdges) end) +fun buildGraphs ([],leqG,neqG,neqE) = (leqG, neqG, neqE) +| buildGraphs (l::ls, leqG,neqG, neqE) = case l of + (Less (x,y,p)) => + buildGraphs (ls, addEdge (x,[(y,(Less (x, y, p)))],leqG) , + addEdge (x,[(y,(Less (x, y, p)))],neqG), l::neqE) | (Le (x,y,p)) => -( let val g1' = addTermEdge (x,y,g1) - and g2' = addLessEdge (x,[(y,(Le (x, y,p)))],g2) - in buildGraphs (ls,g1',g2',neqEdges) end) -| (NotEq (x,y,p)) => ( buildGraphs (ls,g1,g2,l::neqEdges) ) + buildGraphs (ls, addEdge (x,[(y,(Le (x, y,p)))],leqG) , neqG, neqE) +| (NotEq (x,y,p)) => + buildGraphs (ls, leqG , addEdge (x,[(y,(NotEq (x, y, p)))],neqG), l::neqE) ; + + in buildGraphs (lessList, [], [], []) end; (* *********************************************************************** *) (* *) -(* adjacent_term g u : (Term.term * 'a list ) list -> Term.term -> 'a list *) -(* *) -(* *) -(* *********************************************************************** *) - -fun adjacent_term ((v,adj)::el) u = - if u aconv v then adj else adjacent_term el u -| adjacent_term nil _ = [] - -(* *********************************************************************** *) -(* *) -(* adjacent_term g u : (''a * 'b list ) list -> ''a -> 'b list *) +(* adjacent g u : (''a * 'b list ) list -> ''a -> 'b list *) (* *) (* List of successors of u in graph g *) (* *) (* *********************************************************************** *) -fun adjacent ((v,adj)::el) u = - if u = v then adj else adjacent el u -| adjacent nil _ = [] +fun adjacent eq_comp ((v,adj)::el) u = + if eq_comp (u, v) then adj else adjacent eq_comp el u +| adjacent _ [] _ = [] - -(* *********************************************************************** *) -(* *) -(* transpose_term g: *) -(* (Term.term * Term.term list) list -> (Term.term * Term.term list) list *) -(* *) -(* Computes transposed graph g' from g *) -(* by reversing all edges u -> v to v -> u *) -(* *) -(* *********************************************************************** *) - - fun transpose_term g = - let - (* Compute list of reversed edges for each adjacency list *) - fun flip (u,v::el) = (v,u) :: flip (u,el) - | flip (_,nil) = nil - - (* Compute adjacency list for node u from the list of edges - and return a likewise reduced list of edges. The list of edges - is searches for edges starting from u, and these edges are removed. *) - fun gather (u,(v,w)::el) = - let - val (adj,edges) = gather (u,el) - in - if u aconv v then (w::adj,edges) - else (adj,(v,w)::edges) - end - | gather (_,nil) = (nil,nil) - - (* For every node in the input graph, call gather to find all reachable - nodes in the list of edges *) - fun assemble ((u,_)::el) edges = - let val (adj,edges) = gather (u,edges) - in (u,adj) :: assemble el edges - end - | assemble nil _ = nil - - (* Compute, for each adjacency list, the list with reversed edges, - and concatenate these lists. *) - val flipped = foldr (op @) ((map flip g),nil) - - in assemble g flipped end - + (* *********************************************************************** *) (* *) (* transpose g: *) @@ -484,10 +407,10 @@ (* *) (* *********************************************************************** *) -fun transpose g = +fun transpose eq_comp g = let (* Compute list of reversed edges for each adjacency list *) - fun flip (u,v::el) = (v,u) :: flip (u,el) + fun flip (u,(v,l)::el) = (v,(u,l)) :: flip (u,el) | flip (_,nil) = nil (* Compute adjacency list for node u from the list of edges @@ -497,7 +420,7 @@ let val (adj,edges) = gather (u,el) in - if u = v then (w::adj,edges) + if eq_comp (u, v) then (w::adj,edges) else (adj,(v,w)::edges) end | gather (_,nil) = (nil,nil) @@ -516,16 +439,19 @@ in assemble g flipped end - -(* scc_term : (term * term list) list -> term list list *) +(* *********************************************************************** *) +(* *) +(* scc_term : (term * term list) list -> term list list *) +(* *) +(* The following is based on the algorithm for finding strongly connected *) +(* components described in Introduction to Algorithms, by Cormon, Leiserson*) +(* and Rivest, section 23.5. The input G is an adjacency list description *) +(* of a directed graph. The output is a list of the strongly connected *) +(* components (each a list of vertices). *) +(* *) +(* *) +(* *********************************************************************** *) -(* The following is based on the algorithm for finding strongly - connected components described in Introduction to Algorithms, - by Cormon, Leiserson, and Rivest, section 23.5. The input G - is an adjacency list description of a directed graph. The - output is a list of the strongly connected components (each a - list of vertices). *) - fun scc_term G = let (* Ordered list of the vertices that DFS has finished with; @@ -547,9 +473,9 @@ let val _ = visited := u :: !visited val descendents = - foldr (fn (v,ds) => if been_visited v then ds + foldr (fn ((v,l),ds) => if been_visited v then ds else v :: dfs_visit g v @ ds) - ((adjacent_term g u) ,nil) + ((adjacent (op aconv) g u) ,nil) in finish := u :: !finish; descendents @@ -564,7 +490,7 @@ visited := nil; (* We don't reset finish because its value is used by - revfold below, and it will never be used again (even + foldl below, and it will never be used again (even though dfs_visit will continue to modify it). *) (* DFS on the transpose. The vertices returned by @@ -573,7 +499,7 @@ list, which is what is returned. *) foldl (fn (comps,u) => if been_visited u then comps - else ((u :: dfs_visit (transpose_term G) u) :: comps)) (nil,(!finish)) + else ((u :: dfs_visit (transpose (op aconv) G) u) :: comps)) (nil,(!finish)) end; @@ -586,7 +512,6 @@ (* *) (* *********************************************************************** *) - fun dfs_int_reachable g u = let (* List of vertices which have been visited. *) @@ -598,16 +523,16 @@ let val _ = visited := u :: !visited val descendents = - foldr (fn (v,ds) => if been_visited v then ds + foldr (fn ((v,l),ds) => if been_visited v then ds else v :: dfs_visit g v @ ds) - ( ((adjacent g u)) ,nil) + ( ((adjacent (op =) g u)) ,nil) in descendents end in u :: dfs_visit g u end; fun indexComps components = - ListPair.map (fn (a,b) => (b,a)) (components, 0 upto (length components -1)); + ListPair.map (fn (a,b) => (a,b)) (0 upto (length components -1), components); fun indexNodes IndexComp = flat (map (fn (index, comp) => (map (fn v => (v,index)) comp)) IndexComp); @@ -616,113 +541,35 @@ | getIndex v ((v',k)::vs) = if v aconv v' then k else getIndex v vs; -(* ***************************************************************** *) -(* *) -(* evalcompgraph components g ntc : *) -(* Term.term list list -> *) -(* (Term.term * (Term.term * less) list) list -> *) -(* (Term.term * int) list -> (int * (int * less) list) list *) -(* *) -(* *) -(* Computes, from graph g, list of all its components and the list *) -(* ntc (nodes, index of component) a graph whose nodes are the *) -(* indices of the components of g. Egdes of the new graph are *) -(* only the edges of g linking two components. *) -(* *) -(* ***************************************************************** *) - -fun evalcompgraph components g ntc = - let - (* Liste (Index der Komponente, Komponente *) - val IndexComp = indexComps components; - - (* Compute new graph with the property that it only contains edges - between components. *) - - (* k is index of current start component. *) - - fun processComponent (k, comp) = - let - (* all edges pointing away from the component *) - (* (Term.term * less) list *) - val allEdges = flat (map (adjacent_term g) comp); - - (* choose those edges pointing to nodes outside - the current component *) - - fun selectEdges [] = [] - | selectEdges ((v,l)::es) = let val k' = getIndex v ntc in - if k' = k then selectEdges es else (k', l) :: (selectEdges es) end; - - (* Insert edge into sorted list of edges, where edge is - only added if - - it is found for the first time - - it is a <= edge and no parallel < edge was found earlier - - it is a < edge - *) - - fun insert (h,l) [] = [(h,l)] - | insert (h,l) ((k',l')::es) = if h = k' then ( - case l of (Less (_, _, _)) => (h,l)::es - | _ => (case l' of (Less (_, _, _)) => (h,l')::es - | _ => (k',l)::es) ) - else (k',l'):: insert (h,l) es; - - (* Reorganise list of edges such that - - duplicate edges are removed - - if a < edge and a <= edge exist at the same time, - remove <= edge *) - - fun sortEdges [] sorted = sorted: (int * less) list - | sortEdges (e::es) sorted = sortEdges es (insert e sorted); - - in - (k, (sortEdges (selectEdges allEdges) [])) - end; - - -in map processComponent IndexComp end; - -(* Remove ``less'' edge info from graph *) -(* type ('a * ('a * less) list) list *) -fun stripOffLess g = map (fn (v, desc) => (v,map (fn (u,l) => u) desc)) g; - - (* *********************************************************************** *) (* *) -(* dfs_term g u v: *) -(* (Term.term *(Term.term * less) list) list -> *) -(* Term.term -> Term.term -> (bool * less list) *) +(* dfs eq_comp g u v: *) +(* ('a * 'a -> bool) -> ('a *( 'a * less) list) list -> *) +(* 'a -> 'a -> (bool * ('a * less) list) *) (* *) (* Depth first search of v from u. *) (* Returns (true, path(u, v)) if successful, otherwise (false, []). *) (* *) (* *********************************************************************** *) - -fun dfs_term g u v = +fun dfs eq_comp g u v = let -(* TODO: this comment is unclear *) - (* Liste der gegangenen Kanten, - die Kante e die zum Vorgaenger eines Knoten u gehoert ist jene - für die gilt (upper e) = u *) - val pred : less list ref = ref nil; - val visited: term list ref = ref nil; + val pred = ref nil; + val visited = ref nil; - fun been_visited v = exists (fn w => w aconv v) (!visited) + fun been_visited v = exists (fn w => eq_comp (w, v)) (!visited) fun dfs_visit u' = let val _ = visited := u' :: (!visited) - fun update l = let val _ = pred := l ::(!pred) in () end; + fun update (x,l) = let val _ = pred := (x,l) ::(!pred) in () end; in if been_visited v then () - else (app (fn (v',l) => if been_visited v' then () else ( - update l; - dfs_visit v'; ()) )) (adjacent_term g u') - end - + else (app (fn (v',l) => if been_visited v' then () else ( + update (v',l); + dfs_visit v'; ()) )) (adjacent eq_comp g u') + end in dfs_visit u; if (been_visited v) then (true, (!pred)) else (false , []) @@ -743,11 +590,11 @@ (* *********************************************************************** *) -fun completeTermPath u v g = +fun completeTermPath u v g = let + val (found, tmp) = dfs (op aconv) g u v ; + val pred = map snd tmp; - val (found, pred) = dfs_term g u v; - fun path x y = let @@ -771,56 +618,20 @@ else path u v ) else raise Cannot end; - + (* *********************************************************************** *) (* *) -(* dfs_int g u v: *) -(* (int *(int * less) list) list -> int -> int *) -(* -> (bool *(int* less) list) *) -(* *) -(* Depth first search of v from u. *) -(* Returns (true, path(u, v)) if successful, otherwise (false, []). *) +(* findProof (sccGraph, neqE, ntc, sccSubgraphs) subgoal: *) (* *) -(* *********************************************************************** *) - -fun dfs_int g u v = - let - val pred : (int * less ) list ref = ref nil; - val visited: int list ref = ref nil; - - fun been_visited v = exists (fn w => w = v) (!visited) - - fun dfs_visit u' = - let val _ = visited := u' :: (!visited) - - fun update (x,l) = let val _ = pred := (x,l) ::(!pred) in () end; - - in if been_visited v then () - else (app (fn (v',l) => if been_visited v' then () else ( - update (v',l); - dfs_visit v'; ()) )) (adjacent g u') - - end - - in - dfs_visit u; - if (been_visited v) then (true, (!pred)) else (false , []) - end; - - -(* *********************************************************************** *) +(* (int * (int * less) list) list * less list * (Term.term * int) list *) +(* * ((term * (term * less) list) list) list -> Less -> proof *) (* *) -(* findProof (g2, cg2, neqEdges, components, ntc) subgoal: *) -(* (Term.term * (Term.term * less) list) list * *) -(* (int * (int * less) list) list * less list * Term.term list list *) -(* * ( (Term.term * int) -> proof *) -(* *) -(* findProof constructs from graphs (g2, cg2) and neqEdges a proof for *) -(* subgoal. Raises exception Cannot if this is not possible. *) +(* findProof constructs from graphs (sccGraph, sccSubgraphs) and neqE a *) +(* proof for subgoal. Raises exception Cannot if this is not possible. *) (* *) (* *********************************************************************** *) -fun findProof (g2, cg2, neqEdges, components, ntc ) subgoal = +fun findProof (sccGraph, neqE, ntc, sccSubgraphs) subgoal = let (* complete path x y from component graph *) @@ -838,13 +649,15 @@ val v = upper edge in if (getIndex u ntc) = xi then - (completeTermPath x u g2)@[edge]@(completeTermPath v y' g2) - else (rev_completeComponentPath u)@[edge]@(completeTermPath v y' g2) + (completeTermPath x u (nth_elem(xi, sccSubgraphs)) )@[edge] + @(completeTermPath v y' (nth_elem((getIndex y' ntc),sccSubgraphs)) ) + else (rev_completeComponentPath u)@[edge] + @(completeTermPath v y' (nth_elem((getIndex y' ntc),sccSubgraphs)) ) end in if x aconv y then [(Le (x, y, (Thm ([], Less.le_refl))))] - else ( if xi = yi then completeTermPath x y g2 + else ( if xi = yi then completeTermPath x y (nth_elem(xi, sccSubgraphs)) else rev_completeComponentPath y ) end; @@ -854,23 +667,23 @@ (* Find a path from x through e to y, of weight < *) (* ******************************************************************* *) - fun findLess e x y xi yi Xreachable Yreachable = + fun findLess e x y xi yi xreachable yreachable = let val u = lower e val v = upper e val ui = getIndex u ntc val vi = getIndex v ntc in - if ui mem Xreachable andalso vi mem Xreachable andalso - ui mem Yreachable andalso vi mem Yreachable then ( + if ui mem xreachable andalso vi mem xreachable andalso + ui mem yreachable andalso vi mem yreachable then ( (case e of (Less (_, _, _)) => let - val (xufound, xupred) = dfs_int cg2 xi (getIndex u ntc) + val (xufound, xupred) = dfs (op =) sccGraph xi (getIndex u ntc) in if xufound then ( let - val (vyfound, vypred) = dfs_int cg2 (getIndex v ntc) yi + val (vyfound, vypred) = dfs (op =) sccGraph (getIndex v ntc) yi in if vyfound then ( let @@ -885,15 +698,15 @@ else None end | _ => - let val (xufound, xupred) = dfs_int cg2 xi (getIndex u ntc) + let val (uvfound, uvpred) = dfs (op =) sccGraph (getIndex u ntc) (getIndex v ntc) in - if xufound then ( + if uvfound then ( let - val (uvfound, uvpred) = dfs_int cg2 (getIndex u ntc) (getIndex v ntc) + val (xufound, xupred) = dfs (op =) sccGraph xi (getIndex u ntc) in - if uvfound then ( + if xufound then ( let - val (vyfound, vypred) = dfs_int cg2 (getIndex v ntc) yi + val (vyfound, vypred) = dfs (op =) sccGraph (getIndex v ntc) yi in if vyfound then ( let @@ -918,13 +731,12 @@ in (* looking for x <= y: any path from x to y is sufficient *) case subgoal of (Le (x, y, _)) => ( - + if sccGraph = [] then raise Cannot else ( let val xi = getIndex x ntc val yi = getIndex y ntc - (* sucht im Komponentengraphen einen Weg von der Komponente in der x liegt - zu der in der y liegt *) - val (found, pred) = dfs_int cg2 xi yi + (* searches in sccGraph a path from xi to yi *) + val (found, pred) = dfs (op =) sccGraph xi yi in if found then ( let val xypath = completeComponentPath x y pred @@ -938,20 +750,20 @@ end ) else raise Cannot end - + ) ) (* looking for x < y: particular path required, which is not necessarily found by normal dfs *) | (Less (x, y, _)) => ( + if sccGraph = [] then raise Cannot else ( let val xi = getIndex x ntc val yi = getIndex y ntc - val cg2' = stripOffLess cg2 - val cg2'_transpose = transpose cg2' - (* alle von x aus erreichbaren Komponenten *) - val xreachable = dfs_int_reachable cg2' xi - (* all comonents reachable from y in the transposed graph cg2' *) - val yreachable = dfs_int_reachable cg2'_transpose yi + val sccGraph_transpose = transpose (op =) sccGraph + (* all components that can be reached from component xi *) + val xreachable = dfs_int_reachable sccGraph xi + (* all comonents reachable from y in the transposed graph sccGraph' *) + val yreachable = dfs_int_reachable sccGraph_transpose yi (* for all edges u ~= v or u < v check if they are part of path x < y *) fun processNeqEdges [] = raise Cannot | processNeqEdges (e::es) = @@ -959,18 +771,30 @@ | _ => processNeqEdges es in - processNeqEdges neqEdges + processNeqEdges neqE end - + ) ) | (NotEq (x, y, _)) => ( - - let val xi = getIndex x ntc + (* if there aren't any edges that are candidate for a ~= raise Cannot *) + if neqE = [] then raise Cannot + (* if there aren't any edges that are candidate for <= then just search a edge in neqE that implies the subgoal *) + else if sccSubgraphs = [] then ( + (case (Library.find_first (fn fact => fact subsumes subgoal) neqE, subgoal) of + ( Some (NotEq (x, y, p)), NotEq (x', y', _)) => + if (x aconv x' andalso y aconv y') then p + else Thm ([p], thm "not_sym") + | ( Some (Less (x, y, p)), NotEq (x', y', _)) => + if x aconv x' andalso y aconv y' then (Thm ([p], Less.less_imp_neq)) + else (Thm ([(Thm ([p], Less.less_imp_neq))], thm "not_sym")) + | _ => raise Cannot) + ) else ( + + let val xi = getIndex x ntc val yi = getIndex y ntc - val cg2' = stripOffLess cg2 - val cg2'_transpose = transpose cg2' - val xreachable = dfs_int_reachable cg2' xi - val yreachable = dfs_int_reachable cg2'_transpose yi + val sccGraph_transpose = transpose (op =) sccGraph + val xreachable = dfs_int_reachable sccGraph xi + val yreachable = dfs_int_reachable sccGraph_transpose yi fun processNeqEdges [] = raise Cannot | processNeqEdges (e::es) = ( @@ -981,7 +805,7 @@ in (* if x ~= y follows from edge e *) - if e subsumes subgoal then ( + if e subsumes subgoal then ( case e of (Less (u, v, q)) => ( if u aconv x andalso v aconv y then (Thm ([q], Less.less_imp_neq)) else (Thm ([(Thm ([q], Less.less_imp_neq))], thm "not_sym")) @@ -994,14 +818,15 @@ (* if SCC_x is linked to SCC_y via edge e *) else if ui = xi andalso vi = yi then ( case e of (Less (_, _,_)) => ( - let val xypath = (completeTermPath x u g2) @ [e] @ (completeTermPath v y g2) + let val xypath = (completeTermPath x u (nth_elem(ui, sccSubgraphs)) ) @ [e] @ (completeTermPath v y (nth_elem(vi, sccSubgraphs)) ) val xyLesss = transPath (tl xypath, hd xypath) in (Thm ([getprf xyLesss], Less.less_imp_neq)) end) | _ => ( - let val xupath = completeTermPath x u g2 - val uxpath = completeTermPath u x g2 - val vypath = completeTermPath v y g2 - val yvpath = completeTermPath y v g2 + let + val xupath = completeTermPath x u (nth_elem(ui, sccSubgraphs)) + val uxpath = completeTermPath u x (nth_elem(ui, sccSubgraphs)) + val vypath = completeTermPath v y (nth_elem(vi, sccSubgraphs)) + val yvpath = completeTermPath y v (nth_elem(vi, sccSubgraphs)) val xuLesss = transPath (tl xupath, hd xupath) val uxLesss = transPath (tl uxpath, hd uxpath) val vyLesss = transPath (tl vypath, hd vypath) @@ -1014,15 +839,15 @@ ) ) else if ui = yi andalso vi = xi then ( case e of (Less (_, _,_)) => ( - let val xypath = (completeTermPath y u g2) @ [e] @ (completeTermPath v x g2) + let val xypath = (completeTermPath y u (nth_elem(ui, sccSubgraphs)) ) @ [e] @ (completeTermPath v x (nth_elem(vi, sccSubgraphs)) ) val xyLesss = transPath (tl xypath, hd xypath) in (Thm ([(Thm ([getprf xyLesss], Less.less_imp_neq))] , thm "not_sym")) end ) | _ => ( - let val yupath = completeTermPath y u g2 - val uypath = completeTermPath u y g2 - val vxpath = completeTermPath v x g2 - val xvpath = completeTermPath x v g2 + let val yupath = completeTermPath y u (nth_elem(ui, sccSubgraphs)) + val uypath = completeTermPath u y (nth_elem(ui, sccSubgraphs)) + val vxpath = completeTermPath v x (nth_elem(vi, sccSubgraphs)) + val xvpath = completeTermPath x v (nth_elem(vi, sccSubgraphs)) val yuLesss = transPath (tl yupath, hd yupath) val uyLesss = transPath (tl uypath, hd uypath) val vxLesss = transPath (tl vxpath, hd vxpath) @@ -1040,43 +865,58 @@ (Some prf) => (Thm ([prf], Less.less_imp_neq)) | None => ( let - val yr = dfs_int_reachable cg2' yi - val xr = dfs_int_reachable cg2'_transpose xi + val yr = dfs_int_reachable sccGraph yi + val xr = dfs_int_reachable sccGraph_transpose xi in case (findLess e y x yi xi yr xr) of (Some prf) => (Thm ([(Thm ([prf], Less.less_imp_neq))], thm "not_sym")) | _ => processNeqEdges es end) ) end) - in processNeqEdges neqEdges end + in processNeqEdges neqE end) ) end; -(* *********************************************************************** *) -(* *) -(* checkComponents g components ntc neqEdges: *) -(* (Term.term * (Term.term * less) list) list -> Term.term list list -> *) -(* (Term.term * int) -> less list -> bool *) -(* *) -(* For each edge in the list neqEdges check if it leads to a contradiction.*) -(* We have a contradiction for edge u ~= v and u < v if: *) -(* - u and v are in the same component, *) -(* that is, a path u <= v and a path v <= u exist, hence u = v. *) -(* From irreflexivity of < follows u < u or v < v. Ex false quodlibet. *) -(* *) -(* *) -(* *********************************************************************** *) +(* ******************************************************************* *) +(* *) +(* mk_sccGraphs components leqG neqG ntc : *) +(* Term.term list list -> *) +(* (Term.term * (Term.term * less) list) list -> *) +(* (Term.term * (Term.term * less) list) list -> *) +(* (Term.term * int) list -> *) +(* (int * (int * less) list) list * *) +(* ((Term.term * (Term.term * less) list) list) list *) +(* *) +(* *) +(* Computes, from graph leqG, list of all its components and the list *) +(* ntc (nodes, index of component) a graph whose nodes are the *) +(* indices of the components of g. Egdes of the new graph are *) +(* only the edges of g linking two components. Also computes for each *) +(* component the subgraph of leqG that forms this component. *) +(* *) +(* For each component SCC_i is checked if there exists a edge in neqG *) +(* that leads to a contradiction. *) +(* *) +(* We have a contradiction for edge u ~= v and u < v if: *) +(* - u and v are in the same component, *) +(* that is, a path u <= v and a path v <= u exist, hence u = v. *) +(* From irreflexivity of < follows u < u or v < v. Ex false quodlibet. *) +(* *) +(* ******************************************************************* *) +fun mk_sccGraphs _ [] _ _ = ([],[]) +| mk_sccGraphs components leqG neqG ntc = + let + (* Liste (Index der Komponente, Komponente *) + val IndexComp = indexComps components; -fun checkComponents g components ntc neqEdges = - let - (* Construct proof by contradiction for edge *) - fun handleContr edge = + + fun handleContr edge g = (case edge of (Less (x, y, _)) => ( let - val xxpath = edge :: (completeTermPath y x g) + val xxpath = edge :: (completeTermPath y x g ) val xxLesss = transPath (tl xxpath, hd xxpath) val q = getprf xxLesss in @@ -1085,8 +925,8 @@ ) | (NotEq (x, y, _)) => ( let - val xypath = (completeTermPath x y g) - val yxpath = (completeTermPath y x g) + val xypath = (completeTermPath x y g ) + val yxpath = (completeTermPath y x g ) val xyLesss = transPath (tl xypath, hd xypath) val yxLesss = transPath (tl yxpath, hd yxpath) val q = getprf (mergeLess ((mergeLess (edge, xyLesss)),yxLesss )) @@ -1094,21 +934,75 @@ raise (Contr (Thm ([q], Less.less_reflE ))) end ) - | _ => error "trans_tac/checkCompoents/handleContr: invalid Contradiction"); + | _ => error "trans_tac/handleContr: invalid Contradiction"); + + + (* k is index of the actual component *) + + fun processComponent (k, comp) = + let + (* all edges with weight <= of the actual component *) + val leqEdges = flat (map (adjacent (op aconv) leqG) comp); + (* all edges with weight ~= of the actual component *) + val neqEdges = map snd (flat (map (adjacent (op aconv) neqG) comp)); - (* Check each edge in neqEdges for contradiction. - If there is a contradiction, call handleContr, otherwise do nothing. *) - fun checkNeqEdges [] = () - | checkNeqEdges (e::es) = - (case e of (Less (u, v, _)) => - if (getIndex u ntc) = (getIndex v ntc) then handleContr e g - else checkNeqEdges es - | (NotEq (u, v, _)) => - if (getIndex u ntc) = (getIndex v ntc) then handleContr e g - else checkNeqEdges es - | _ => checkNeqEdges es) - - in if g = [] then () else checkNeqEdges neqEdges end; + (* find an edge leading to a contradiction *) + fun findContr [] = None + | findContr (e::es) = + let val ui = (getIndex (lower e) ntc) + val vi = (getIndex (upper e) ntc) + in + if ui = vi then Some e + else findContr es + end; + + (* sort edges into component internal edges and + edges pointing away from the component *) + fun sortEdges [] (intern,extern) = (intern,extern) + | sortEdges ((v,l)::es) (intern, extern) = + let val k' = getIndex v ntc in + if k' = k then + sortEdges es (l::intern, extern) + else sortEdges es (intern, (k',l)::extern) end; + + (* Insert edge into sorted list of edges, where edge is + only added if + - it is found for the first time + - it is a <= edge and no parallel < edge was found earlier + - it is a < edge + *) + fun insert (h,l) [] = [(h,l)] + | insert (h,l) ((k',l')::es) = if h = k' then ( + case l of (Less (_, _, _)) => (h,l)::es + | _ => (case l' of (Less (_, _, _)) => (h,l')::es + | _ => (k',l)::es) ) + else (k',l'):: insert (h,l) es; + + (* Reorganise list of edges such that + - duplicate edges are removed + - if a < edge and a <= edge exist at the same time, + remove <= edge *) + fun reOrganizeEdges [] sorted = sorted: (int * less) list + | reOrganizeEdges (e::es) sorted = reOrganizeEdges es (insert e sorted); + + (* construct the subgraph forming the strongly connected component + from the edge list *) + fun sccSubGraph [] g = g + | sccSubGraph (l::ls) g = + sccSubGraph ls (addEdge ((lower l),[((upper l),l)],g)) + + val (intern, extern) = sortEdges leqEdges ([], []); + val subGraph = sccSubGraph intern []; + + in + case findContr neqEdges of Some e => handleContr e subGraph + | _ => ((k, (reOrganizeEdges (extern) [])), subGraph) + end; + + val tmp = map processComponent IndexComp +in + ( (map fst tmp), (map snd tmp)) +end; (* *********************************************************************** *) (* *) @@ -1121,17 +1015,15 @@ fun solvePartialOrder sign (asms, concl) = let - val (g1, g2, neqEdges) = buildGraphs (asms, [], [],[]) - val components = scc_term g1 + val (leqG, neqG, neqE) = mkGraphs asms + val components = scc_term leqG val ntc = indexNodes (indexComps components) - val cg2 = evalcompgraph components g2 ntc + val (sccGraph, sccSubgraphs) = mk_sccGraphs components leqG neqG ntc in - (* Check for contradiction within assumptions *) - checkComponents g2 components ntc neqEdges; - let + let val (subgoals, prf) = mkconcl_partial sign concl fun solve facts less = - (case triv_solv less of None => findProof (g2, cg2, neqEdges, components, ntc) less + (case triv_solv less of None => findProof (sccGraph, neqE, ntc, sccSubgraphs ) less | Some prf => prf ) in map (solve asms) subgoals @@ -1149,25 +1041,22 @@ fun solveTotalOrder sign (asms, concl) = let - val (g1, g2, neqEdges) = buildGraphs (asms, [], [],[]) - val components = scc_term g1 + val (leqG, neqG, neqE) = mkGraphs asms + val components = scc_term leqG val ntc = indexNodes (indexComps components) - val cg2 = evalcompgraph components g2 ntc + val (sccGraph, sccSubgraphs) = mk_sccGraphs components leqG neqG ntc in - checkComponents g2 components ntc neqEdges; - let + let val (subgoals, prf) = mkconcl_linear sign concl fun solve facts less = - (case triv_solv less of None => findProof (g2, cg2, neqEdges, components, ntc) less + (case triv_solv less of None => findProof (sccGraph, neqE, ntc, sccSubgraphs) less | Some prf => prf ) in map (solve asms) subgoals end end; - -(* partial_tac - solves linear/total orders *) - +(* partial_tac - solves partial orders *) val partial_tac = SUBGOAL (fn (A, n, sign) => let val rfrees = map Free (rename_wrt_term A (Logic.strip_params A)) @@ -1186,7 +1075,6 @@ ); (* linear_tac - solves linear/total orders *) - val linear_tac = SUBGOAL (fn (A, n, sign) => let val rfrees = map Free (rename_wrt_term A (Logic.strip_params A)) @@ -1204,4 +1092,3 @@ | Cannot => no_tac); end; -