# HG changeset patch # User ballarin # Date 1090849730 -7200 # Node ID 4b3d280ef06a85c1ff8881cd11fa3146363d62d8 # Parent a6cd1a4547511068a7404aa1ff21b3d2c2ba0117 New prover for transitive and reflexive-transitive closure of relations. - Code in Provers/trancl.ML - HOL: Simplifier set up to use it as solver diff -r a6cd1a454751 -r 4b3d280ef06a NEWS --- a/NEWS Thu Jul 22 19:33:12 2004 +0200 +++ b/NEWS Mon Jul 26 15:48:50 2004 +0200 @@ -6,6 +6,9 @@ *** General *** +* Provers/trancl.ML: new transitivity reasoner for transitive and + reflexive-transitive closure of relations. + * Pure: considerably improved version of 'constdefs' command. Now performs automatic type-inference of declared constants; additional support for local structure declarations (cf. locales and HOL @@ -184,6 +187,12 @@ Function 'Summation' over nat is gone, its syntax '\i hom G H" notes hom_mult [simp] = hom_mult [OF homh] @@ -553,7 +553,7 @@ lemma (in group_hom) hom_one [simp]: "h \ = \\<^bsub>H\<^esub>" proof - - have "h \ \\<^bsub>H\<^esub> \\<^bsub>H\<^esub> = h \ \\<^sub>2 h \" + have "h \ \\<^bsub>H\<^esub> \\<^bsub>H\<^esub> = h \ \\<^bsub>H\<^esub> h \" by (simp add: hom_mult [symmetric] del: hom_mult) then show ?thesis by (simp del: r_one) qed diff -r a6cd1a454751 -r 4b3d280ef06a src/HOL/Algebra/UnivPoly.thy --- a/src/HOL/Algebra/UnivPoly.thy Thu Jul 22 19:33:12 2004 +0200 +++ b/src/HOL/Algebra/UnivPoly.thy Mon Jul 26 15:48:50 2004 +0200 @@ -1162,7 +1162,7 @@ next case (Suc j) (* The following could be simplified if there was a reasoner for - total orders integrated with simip. *) + total orders integrated with simp. *) have R6: "!!i k. [| k <= j; i <= Suc j - k |] ==> g i \ carrier R" using Suc by (auto intro!: funcset_mem [OF Rg]) arith have R8: "!!i k. [| k <= Suc j; i <= k |] ==> g (k - i) \ carrier R" diff -r a6cd1a454751 -r 4b3d280ef06a src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Thu Jul 22 19:33:12 2004 +0200 +++ b/src/HOL/IsaMakefile Mon Jul 26 15:48:50 2004 +0200 @@ -78,6 +78,7 @@ $(SRC)/Provers/hypsubst.ML $(SRC)/Provers/induct_method.ML \ $(SRC)/Provers/make_elim.ML $(SRC)/Provers/order.ML \ $(SRC)/Provers/simplifier.ML $(SRC)/Provers/splitter.ML \ + $(SRC)/Provers/trancl.ML \ $(SRC)/TFL/dcterm.ML $(SRC)/TFL/post.ML $(SRC)/TFL/rules.ML \ $(SRC)/TFL/tfl.ML $(SRC)/TFL/thms.ML $(SRC)/TFL/thry.ML \ $(SRC)/TFL/usyntax.ML $(SRC)/TFL/utils.ML \ diff -r a6cd1a454751 -r 4b3d280ef06a src/HOL/MicroJava/Comp/CorrComp.thy --- a/src/HOL/MicroJava/Comp/CorrComp.thy Thu Jul 22 19:33:12 2004 +0200 +++ b/src/HOL/MicroJava/Comp/CorrComp.thy Mon Jul 26 15:48:50 2004 +0200 @@ -52,7 +52,7 @@ done theorem exec_all_refl: "exec_all G s s" -by (simp only: exec_all_def, rule rtrancl_refl) +by (simp only: exec_all_def (* CBtrancl, rule rtrancl_refl*) ) theorem exec_instr_in_exec_all: diff -r a6cd1a454751 -r 4b3d280ef06a src/HOL/MicroJava/J/WellForm.thy --- a/src/HOL/MicroJava/J/WellForm.thy Thu Jul 22 19:33:12 2004 +0200 +++ b/src/HOL/MicroJava/J/WellForm.thy Mon Jul 26 15:48:50 2004 +0200 @@ -316,7 +316,7 @@ apply( assumption) apply( fast) apply(auto dest!: wf_cdecl_supD) -apply(erule (1) converse_rtrancl_into_rtrancl) +(*CBtrancl: apply(erule (1) converse_rtrancl_into_rtrancl) *) done lemma is_type_rTI: "wf_mhead G sig rT ==> is_type G rT" diff -r a6cd1a454751 -r 4b3d280ef06a src/HOL/Transitive_Closure.thy --- a/src/HOL/Transitive_Closure.thy Thu Jul 22 19:33:12 2004 +0200 +++ b/src/HOL/Transitive_Closure.thy Mon Jul 26 15:48:50 2004 +0200 @@ -6,7 +6,9 @@ header {* Reflexive and Transitive closure of a relation *} -theory Transitive_Closure = Inductive: +theory Transitive_Closure = Inductive + +files ("../Provers/trancl.ML"): text {* @{text rtrancl} is reflexive/transitive closure, @@ -444,4 +446,62 @@ declare rtranclE [cases set: rtrancl] declare tranclE [cases set: trancl] +subsection {* Setup of transitivity reasoner *} + +use "../Provers/trancl.ML"; + +ML_setup {* + +structure Trancl_Tac = Trancl_Tac_Fun ( + struct + val r_into_trancl = thm "r_into_trancl"; + val trancl_trans = thm "trancl_trans"; + val rtrancl_refl = thm "rtrancl_refl"; + val r_into_rtrancl = thm "r_into_rtrancl"; + val trancl_into_rtrancl = thm "trancl_into_rtrancl"; + val rtrancl_trancl_trancl = thm "rtrancl_trancl_trancl"; + val trancl_rtrancl_trancl = thm "trancl_rtrancl_trancl"; + val rtrancl_trans = thm "rtrancl_trans"; +(* + fun decomp (Trueprop $ t) = + let fun dec (Const ("op :", _) $ t1 $ t2 ) = + let fun dec1 (Const ("Pair", _) $ a $ b) = (a,b); + fun dec2 (Const ("Transitive_Closure.rtrancl", _ ) $ r) = (r,"r*") + | dec2 (Const ("Transitive_Closure.trancl", _ ) $ r) = (r,"r+") + | dec2 r = (r,"r"); + val (a,b) = dec1 t1; + val (rel,r) = dec2 t2; + in Some (a,b,rel,r) end + | dec _ = None + in dec t end; +*) + fun decomp (Trueprop $ t) = + let fun dec (Const ("op :", _) $ (Const ("Pair", _) $ a $ b) $ rel ) = + let fun decr (Const ("Transitive_Closure.rtrancl", _ ) $ r) = (r,"r*") + | decr (Const ("Transitive_Closure.trancl", _ ) $ r) = (r,"r+") + | decr r = (r,"r"); + val (rel,r) = decr rel; + in Some (a,b,rel,r) end + | dec _ = None + in dec t end; + + end); (* struct *) + +simpset_ref() := simpset () + addSolver (mk_solver "Trancl" (fn _ => Trancl_Tac.trancl_tac)) + addSolver (mk_solver "Rtrancl" (fn _ => Trancl_Tac.rtrancl_tac)); + +*} + +(* Optional methods + +method_setup trancl = + {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (trancl_tac)) *} + {* simple transitivity reasoner *} +method_setup rtrancl = + {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (rtrancl_tac)) *} + {* simple transitivity reasoner *} + +*) + end diff -r a6cd1a454751 -r 4b3d280ef06a src/HOL/UNITY/Simple/Reach.thy --- a/src/HOL/UNITY/Simple/Reach.thy Thu Jul 22 19:33:12 2004 +0200 +++ b/src/HOL/UNITY/Simple/Reach.thy Mon Jul 26 15:48:50 2004 +0200 @@ -75,7 +75,7 @@ apply (unfold fixedpoint_def) apply (rule equalityI) apply (auto intro!: ext) - prefer 2 apply (blast intro: rtrancl_trans) +(* CBtrancl: prefer 2 apply (blast intro: rtrancl_trans) *) apply (erule rtrancl_induct, auto) done diff -r a6cd1a454751 -r 4b3d280ef06a src/Provers/trancl.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Provers/trancl.ML Mon Jul 26 15:48:50 2004 +0200 @@ -0,0 +1,478 @@ +(* + Title: Transitivity reasoner for partial and linear orders + Id: $Id$ + Author: Oliver Kutter + Copyright: TU Muenchen +*) + +signature TRANCL_ARITH = +sig + + (* theorems for transitive closure *) + + val r_into_trancl : thm + (* (a,b) : r ==> (a,b) : r^+ *) + val trancl_trans : thm + (* [| (a,b) : r^+ ; (b,c) : r^+ |] ==> (a,c) : r^+ *) + + (* additional theorems for reflexive-transitive closure *) + + val rtrancl_refl : thm + (* (a,a): r^* *) + val r_into_rtrancl : thm + (* (a,b) : r ==> (a,b) : r^* *) + val trancl_into_rtrancl : thm + (* (a,b) : r^+ ==> (a,b) : r^* *) + val rtrancl_trancl_trancl : thm + (* [| (a,b) : r^* ; (b,c) : r^+ |] ==> (a,c) : r^+ *) + val trancl_rtrancl_trancl : thm + (* [| (a,b) : r^+ ; (b,c) : r^* |] ==> (a,c) : r^+ *) + val rtrancl_trans : thm + (* [| (a,b) : r^* ; (b,c) : r^* |] ==> (a,c) : r^* *) + + val decomp: term -> (term * term * term * string) option + +end; + +signature TRANCL_TAC = +sig + val trancl_tac: int -> tactic; + val rtrancl_tac: int -> tactic; +end; + +functor Trancl_Tac_Fun (Cls : TRANCL_ARITH): TRANCL_TAC = +struct + + + datatype proof + = Asm of int + | Thm of proof list * thm; + + exception Cannot; + + fun prove asms = + let fun pr (Asm i) = nth_elem (i, asms) + | pr (Thm (prfs, thm)) = (map pr prfs) MRS thm + in pr end; + + +(* Internal datatype for inequalities *) +datatype rel + = R of term * term * proof (* just a unknown relation R *) + | Trans of term * term * proof (* R^+ *) + | RTrans of term * term * proof; (* R^* *) + + (* Misc functions for datatype rel *) +fun lower (R (x, _, _)) = x + | lower (Trans (x, _, _)) = x + | lower (RTrans (x,_,_)) = x; + +fun upper (R (_, y, _)) = y + | upper (Trans (_, y, _)) = y + | upper (RTrans (_,y,_)) = y; + +fun getprf (R (_, _, p)) = p +| getprf (Trans (_, _, p)) = p +| getprf (RTrans (_,_, p)) = p; + +fun mkasm_trancl Rel (t, n) = + case Cls.decomp t of + Some (x, y, rel,r) => if rel aconv Rel then + + (case r of + "r" => [Trans (x,y, Thm([Asm n], Cls.r_into_trancl))] + | "r+" => [Trans (x,y, Asm n)] + | "r*" => [] + | _ => error ("trancl_tac: unknown relation symbol")) + else [] + | None => []; + +fun mkasm_rtrancl Rel (t, n) = + case Cls.decomp t of + Some (x, y, rel, r) => if rel aconv Rel then + (case r of + "r" => [ Trans (x,y, Thm([Asm n], Cls.r_into_trancl))] + | "r+" => [ Trans (x,y, Asm n)] + | "r*" => [ RTrans(x,y, Asm n)] + | _ => error ("rtrancl_tac: unknown relation symbol" )) + else [] + | None => []; + +fun mkconcl_trancl t = + case Cls.decomp t of + Some (x, y, rel, r) => (case r of + "r+" => (rel, Trans (x,y, Asm ~1), Asm 0) + | _ => raise Cannot) + | None => raise Cannot; + +fun mkconcl_rtrancl t = + case Cls.decomp t of + Some (x, y, rel,r ) => (case r of + "r+" => (rel, Trans (x,y, Asm ~1), Asm 0) + | "r*" => (rel, RTrans (x,y, Asm ~1), Asm 0) + | _ => raise Cannot) + | None => raise Cannot; + +(* trans. cls. rules *) +fun makeStep (Trans (a,_,p), Trans(_,c,q)) = Trans (a,c, Thm ([p,q], Cls.trancl_trans)) +(* refl. + trans. cls. rules *) +| makeStep (RTrans (a,_,p), Trans(_,c,q)) = Trans (a,c, Thm ([p,q], Cls.rtrancl_trancl_trancl)) +| makeStep (Trans (a,_,p), RTrans(_,c,q)) = Trans (a,c, Thm ([p,q], Cls.trancl_rtrancl_trancl)) +| makeStep (RTrans (a,_,p), RTrans(_,c,q)) = RTrans (a,c, Thm ([p,q], Cls.rtrancl_trans)) +| makeStep (a,b) = error ("makeStep: internal error: undefined case\n"^(makestring a) ^"\n" ^ (makestring b)); + +(* ******************************************************************* *) +(* *) +(* transPath (Clslist, Cls): (rel list * rel) -> rel *) +(* *) +(* If a path represented by a list of elements of type rel is found, *) +(* this needs to be contracted to a single element of type rel. *) +(* Prior to each transitivity step it is checked whether the step is *) +(* valid. *) +(* *) +(* ******************************************************************* *) + +fun transPath ([],acc) = acc +| transPath (x::xs,acc) = transPath (xs, makeStep(acc,x)) + +(* ********************************************************************* *) +(* Graph functions *) +(* ********************************************************************* *) + +(* *********************************************************** *) +(* Functions for constructing graphs *) +(* *********************************************************** *) + +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)); + +(* ********************************************************************** *) +(* *) +(* mkGraph constructs from a list of objects of type rel a graph g *) +(* *) +(* ********************************************************************** *) + +fun mkGraph [] = ([],[]) +| mkGraph ys = + let + fun buildGraph ([],g,zs) = (g,zs) + | buildGraph (x::xs, g, zs) = + case x of (Trans (_,_,_)) => + buildGraph (xs, addEdge((upper x), [],(addEdge ((lower x),[((upper x),x)],g))), x::zs) + | _ => buildGraph (xs, addEdge((upper x), [],(addEdge ((lower x),[((upper x),x)],g))), zs) +in buildGraph (ys, [], []) end; + +(* *********************************************************************** *) +(* *) +(* adjacent g u : (''a * 'b list ) list -> ''a -> 'b list *) +(* *) +(* List of successors of u in graph g *) +(* *) +(* *********************************************************************** *) + +fun adjacent eq_comp ((v,adj)::el) u = + if eq_comp (u, v) then adj else adjacent eq_comp el u +| adjacent _ [] _ = [] + +(* *********************************************************************** *) +(* *) +(* dfs eq_comp g u v: *) +(* ('a * 'a -> bool) -> ('a *( 'a * rel) list) list -> *) +(* 'a -> 'a -> (bool * ('a * rel) list) *) +(* *) +(* Depth first search of v from u. *) +(* Returns (true, path(u, v)) if successful, otherwise (false, []). *) +(* *) +(* *********************************************************************** *) + +fun dfs eq_comp g u v = + let + val pred = ref nil; + val visited = ref nil; + + fun been_visited v = exists (fn w => eq_comp (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 eq_comp g u') + end + in + dfs_visit u; + if (been_visited v) then (true, (!pred)) else (false , []) + end; + +(* *********************************************************************** *) +(* *) +(* transpose g: *) +(* (''a * ''a list) list -> (''a * ''a list) list *) +(* *) +(* Computes transposed graph g' from g *) +(* by reversing all edges u -> v to v -> u *) +(* *) +(* *********************************************************************** *) + +fun transpose eq_comp g = + let + (* Compute list of reversed edges for each adjacency list *) + 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 + 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 eq_comp (u, 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 + +(* *********************************************************************** *) +(* *) +(* dfs_reachable eq_comp g u: *) +(* (int * int list) list -> int -> int list *) +(* *) +(* Computes list of all nodes reachable from u in g. *) +(* *) +(* *********************************************************************** *) + +fun dfs_reachable eq_comp g u = + let + (* List of vertices which have been visited. *) + val visited = ref nil; + + fun been_visited v = exists (fn w => eq_comp (w, v)) (!visited) + + fun dfs_visit g u = + let + val _ = visited := u :: !visited + val descendents = + foldr (fn ((v,l),ds) => if been_visited v then ds + else v :: dfs_visit g v @ ds) + ( ((adjacent eq_comp g u)) ,nil) + in descendents end + + in u :: dfs_visit g u end; + +(* *********************************************************************** *) +(* *) +(* dfs_term_reachable g u: *) +(* (term * term list) list -> term -> term list *) +(* *) +(* Computes list of all nodes reachable from u in g. *) +(* *) +(* *********************************************************************** *) + +fun dfs_term_reachable g u = dfs_reachable (op aconv) g u; + +(* ************************************************************************ *) +(* *) +(* findPath x y g: Term.term -> Term.term -> *) +(* (Term.term * (Term.term * rel list) list) -> *) +(* (bool, rel list) *) +(* *) +(* Searches a path from vertex x to vertex y in Graph g, returns true and *) +(* the list of edges of edges if path is found, otherwise false and nil. *) +(* *) +(* ************************************************************************ *) + +fun findPath x y g = + let + val (found, tmp) = dfs (op aconv) g x y ; + val pred = map snd tmp; + + fun path x y = + let + (* find predecessor u of node v and the edge u -> v *) + + fun lookup v [] = raise Cannot + | lookup v (e::es) = if (upper e) aconv v then e else lookup v es; + + (* traverse path backwards and return list of visited edges *) + fun rev_path v = + let val l = lookup v pred + val u = lower l; + in + if u aconv x then [l] else (rev_path u) @ [l] + end + + in rev_path y end; + + in + + + if found then ( (found, (path x y) )) else (found,[]) + + + + end; + + +fun findRtranclProof g tranclEdges subgoal = + (* simple case first *) + case subgoal of (RTrans (x,y,_)) => if x aconv y then [Thm ([], Cls.rtrancl_refl)] else ( + let val (found, path) = findPath (lower subgoal) (upper subgoal) g + in + if found then ( + let val path' = (transPath (tl path, hd path)) + in + + case path' of (Trans (_,_,p)) => [Thm ([p], Cls.trancl_into_rtrancl )] + | _ => [getprf path'] + + end + ) + else raise Cannot + end + ) + +| (Trans (x,y,_)) => ( + + let + val Vx = dfs_term_reachable g x; + val g' = transpose (op aconv) g; + val Vy = dfs_term_reachable g' y; + + fun processTranclEdges [] = raise Cannot + | processTranclEdges (e::es) = + if (upper e) mem Vx andalso (lower e) mem Vx + andalso (upper e) mem Vy andalso (lower e) mem Vy + then ( + + + if (lower e) aconv x then ( + if (upper e) aconv y then ( + [(getprf e)] + ) + else ( + let + val (found,path) = findPath (upper e) y g + in + + if found then ( + [getprf (transPath (path, e))] + ) else processTranclEdges es + + end + ) + ) + else if (upper e) aconv y then ( + let val (xufound,xupath) = findPath x (lower e) g + in + + if xufound then ( + + let val xuRTranclEdge = transPath (tl xupath, hd xupath) + val xyTranclEdge = makeStep(xuRTranclEdge,e) + + in [getprf xyTranclEdge] end + + ) else processTranclEdges es + + end + ) + else ( + + let val (xufound,xupath) = findPath x (lower e) g + val (vyfound,vypath) = findPath (upper e) y g + in + if xufound then ( + if vyfound then ( + let val xuRTranclEdge = transPath (tl xupath, hd xupath) + val vyRTranclEdge = transPath (tl vypath, hd vypath) + val xyTranclEdge = makeStep (makeStep(xuRTranclEdge,e),vyRTranclEdge) + + in [getprf xyTranclEdge] end + + ) else processTranclEdges es + ) + else processTranclEdges es + end + ) + ) + else processTranclEdges es; + in processTranclEdges tranclEdges end ) +| _ => raise Cannot + + +fun solveTrancl (asms, concl) = + let val (g,_) = mkGraph asms + in + let val (_, subgoal, _) = mkconcl_trancl concl + val (found, path) = findPath (lower subgoal) (upper subgoal) g + in + + + if found then [getprf (transPath (tl path, hd path))] + else raise Cannot + + end + end; + + + +fun solveRtrancl (asms, concl) = + let val (g,tranclEdges) = mkGraph asms + val (_, subgoal, _) = mkconcl_rtrancl concl +in + findRtranclProof g tranclEdges subgoal +end; + + +val trancl_tac = SUBGOAL (fn (A, n) => + let + val Hs = Logic.strip_assums_hyp A; + val C = Logic.strip_assums_concl A; + val (rel,subgoals, prf) = mkconcl_trancl C; + val prems = flat (ListPair.map (mkasm_trancl rel) (Hs, 0 upto (length Hs - 1))) + val prfs = solveTrancl (prems, C); + + in + METAHYPS (fn asms => + let val thms = map (prove asms) prfs + in rtac (prove thms prf) 1 end) n + end +handle Cannot => no_tac); + + + +val rtrancl_tac = SUBGOAL (fn (A, n) => + let + val Hs = Logic.strip_assums_hyp A; + val C = Logic.strip_assums_concl A; + val (rel,subgoals, prf) = mkconcl_rtrancl C; + + val prems = flat (ListPair.map (mkasm_rtrancl rel) (Hs, 0 upto (length Hs - 1))) + val prfs = solveRtrancl (prems, C); + in + METAHYPS (fn asms => + let val thms = map (prove asms) prfs + in rtac (prove thms prf) 1 end) n + end +handle Cannot => no_tac); + +end; +