New prover for transitive and reflexive-transitive closure of relations.
- Code in Provers/trancl.ML
- HOL: Simplifier set up to use it as solver
1.1 --- a/NEWS Thu Jul 22 19:33:12 2004 +0200
1.2 +++ b/NEWS Mon Jul 26 15:48:50 2004 +0200
1.3 @@ -6,6 +6,9 @@
1.4
1.5 *** General ***
1.6
1.7 +* Provers/trancl.ML: new transitivity reasoner for transitive and
1.8 + reflexive-transitive closure of relations.
1.9 +
1.10 * Pure: considerably improved version of 'constdefs' command. Now
1.11 performs automatic type-inference of declared constants; additional
1.12 support for local structure declarations (cf. locales and HOL
1.13 @@ -184,6 +187,12 @@
1.14 Function 'Summation' over nat is gone, its syntax '\<Sum>i<k. e'
1.15 now translates into 'setsum' as above.
1.16
1.17 +* Simplifier:
1.18 + - Is now set up to reason about transitivity chains involving "trancl" (r^+)
1.19 + and "rtrancl" (r^*) by setting up tactics provided by Provers/trancl.ML
1.20 + as additional solvers.
1.21 + - INCOMPATIBILITY: old proofs break occasionally. Typically, this is
1.22 + because simplification now solves more goals than previously.
1.23
1.24 *** HOLCF ***
1.25
2.1 --- a/src/HOL/Algebra/Group.thy Thu Jul 22 19:33:12 2004 +0200
2.2 +++ b/src/HOL/Algebra/Group.thy Mon Jul 26 15:48:50 2004 +0200
2.3 @@ -540,7 +540,7 @@
2.4
2.5
2.6 text{*Basis for homomorphism proofs: we assume two groups @{term G} and
2.7 - @term{H}, with a homomorphism @{term h} between them*}
2.8 + @{term H}, with a homomorphism @{term h} between them*}
2.9 locale group_hom = group G + group H + var h +
2.10 assumes homh: "h \<in> hom G H"
2.11 notes hom_mult [simp] = hom_mult [OF homh]
2.12 @@ -553,7 +553,7 @@
2.13 lemma (in group_hom) hom_one [simp]:
2.14 "h \<one> = \<one>\<^bsub>H\<^esub>"
2.15 proof -
2.16 - have "h \<one> \<otimes>\<^bsub>H\<^esub> \<one>\<^bsub>H\<^esub> = h \<one> \<otimes>\<^sub>2 h \<one>"
2.17 + have "h \<one> \<otimes>\<^bsub>H\<^esub> \<one>\<^bsub>H\<^esub> = h \<one> \<otimes>\<^bsub>H\<^esub> h \<one>"
2.18 by (simp add: hom_mult [symmetric] del: hom_mult)
2.19 then show ?thesis by (simp del: r_one)
2.20 qed
3.1 --- a/src/HOL/Algebra/UnivPoly.thy Thu Jul 22 19:33:12 2004 +0200
3.2 +++ b/src/HOL/Algebra/UnivPoly.thy Mon Jul 26 15:48:50 2004 +0200
3.3 @@ -1162,7 +1162,7 @@
3.4 next
3.5 case (Suc j)
3.6 (* The following could be simplified if there was a reasoner for
3.7 - total orders integrated with simip. *)
3.8 + total orders integrated with simp. *)
3.9 have R6: "!!i k. [| k <= j; i <= Suc j - k |] ==> g i \<in> carrier R"
3.10 using Suc by (auto intro!: funcset_mem [OF Rg]) arith
3.11 have R8: "!!i k. [| k <= Suc j; i <= k |] ==> g (k - i) \<in> carrier R"
4.1 --- a/src/HOL/IsaMakefile Thu Jul 22 19:33:12 2004 +0200
4.2 +++ b/src/HOL/IsaMakefile Mon Jul 26 15:48:50 2004 +0200
4.3 @@ -78,6 +78,7 @@
4.4 $(SRC)/Provers/hypsubst.ML $(SRC)/Provers/induct_method.ML \
4.5 $(SRC)/Provers/make_elim.ML $(SRC)/Provers/order.ML \
4.6 $(SRC)/Provers/simplifier.ML $(SRC)/Provers/splitter.ML \
4.7 + $(SRC)/Provers/trancl.ML \
4.8 $(SRC)/TFL/dcterm.ML $(SRC)/TFL/post.ML $(SRC)/TFL/rules.ML \
4.9 $(SRC)/TFL/tfl.ML $(SRC)/TFL/thms.ML $(SRC)/TFL/thry.ML \
4.10 $(SRC)/TFL/usyntax.ML $(SRC)/TFL/utils.ML \
5.1 --- a/src/HOL/MicroJava/Comp/CorrComp.thy Thu Jul 22 19:33:12 2004 +0200
5.2 +++ b/src/HOL/MicroJava/Comp/CorrComp.thy Mon Jul 26 15:48:50 2004 +0200
5.3 @@ -52,7 +52,7 @@
5.4 done
5.5
5.6 theorem exec_all_refl: "exec_all G s s"
5.7 -by (simp only: exec_all_def, rule rtrancl_refl)
5.8 +by (simp only: exec_all_def (* CBtrancl, rule rtrancl_refl*) )
5.9
5.10
5.11 theorem exec_instr_in_exec_all:
6.1 --- a/src/HOL/MicroJava/J/WellForm.thy Thu Jul 22 19:33:12 2004 +0200
6.2 +++ b/src/HOL/MicroJava/J/WellForm.thy Mon Jul 26 15:48:50 2004 +0200
6.3 @@ -316,7 +316,7 @@
6.4 apply( assumption)
6.5 apply( fast)
6.6 apply(auto dest!: wf_cdecl_supD)
6.7 -apply(erule (1) converse_rtrancl_into_rtrancl)
6.8 +(*CBtrancl: apply(erule (1) converse_rtrancl_into_rtrancl) *)
6.9 done
6.10
6.11 lemma is_type_rTI: "wf_mhead G sig rT ==> is_type G rT"
7.1 --- a/src/HOL/Transitive_Closure.thy Thu Jul 22 19:33:12 2004 +0200
7.2 +++ b/src/HOL/Transitive_Closure.thy Mon Jul 26 15:48:50 2004 +0200
7.3 @@ -6,7 +6,9 @@
7.4
7.5 header {* Reflexive and Transitive closure of a relation *}
7.6
7.7 -theory Transitive_Closure = Inductive:
7.8 +theory Transitive_Closure = Inductive
7.9 +
7.10 +files ("../Provers/trancl.ML"):
7.11
7.12 text {*
7.13 @{text rtrancl} is reflexive/transitive closure,
7.14 @@ -444,4 +446,62 @@
7.15 declare rtranclE [cases set: rtrancl]
7.16 declare tranclE [cases set: trancl]
7.17
7.18 +subsection {* Setup of transitivity reasoner *}
7.19 +
7.20 +use "../Provers/trancl.ML";
7.21 +
7.22 +ML_setup {*
7.23 +
7.24 +structure Trancl_Tac = Trancl_Tac_Fun (
7.25 + struct
7.26 + val r_into_trancl = thm "r_into_trancl";
7.27 + val trancl_trans = thm "trancl_trans";
7.28 + val rtrancl_refl = thm "rtrancl_refl";
7.29 + val r_into_rtrancl = thm "r_into_rtrancl";
7.30 + val trancl_into_rtrancl = thm "trancl_into_rtrancl";
7.31 + val rtrancl_trancl_trancl = thm "rtrancl_trancl_trancl";
7.32 + val trancl_rtrancl_trancl = thm "trancl_rtrancl_trancl";
7.33 + val rtrancl_trans = thm "rtrancl_trans";
7.34 +(*
7.35 + fun decomp (Trueprop $ t) =
7.36 + let fun dec (Const ("op :", _) $ t1 $ t2 ) =
7.37 + let fun dec1 (Const ("Pair", _) $ a $ b) = (a,b);
7.38 + fun dec2 (Const ("Transitive_Closure.rtrancl", _ ) $ r) = (r,"r*")
7.39 + | dec2 (Const ("Transitive_Closure.trancl", _ ) $ r) = (r,"r+")
7.40 + | dec2 r = (r,"r");
7.41 + val (a,b) = dec1 t1;
7.42 + val (rel,r) = dec2 t2;
7.43 + in Some (a,b,rel,r) end
7.44 + | dec _ = None
7.45 + in dec t end;
7.46 +*)
7.47 + fun decomp (Trueprop $ t) =
7.48 + let fun dec (Const ("op :", _) $ (Const ("Pair", _) $ a $ b) $ rel ) =
7.49 + let fun decr (Const ("Transitive_Closure.rtrancl", _ ) $ r) = (r,"r*")
7.50 + | decr (Const ("Transitive_Closure.trancl", _ ) $ r) = (r,"r+")
7.51 + | decr r = (r,"r");
7.52 + val (rel,r) = decr rel;
7.53 + in Some (a,b,rel,r) end
7.54 + | dec _ = None
7.55 + in dec t end;
7.56 +
7.57 + end); (* struct *)
7.58 +
7.59 +simpset_ref() := simpset ()
7.60 + addSolver (mk_solver "Trancl" (fn _ => Trancl_Tac.trancl_tac))
7.61 + addSolver (mk_solver "Rtrancl" (fn _ => Trancl_Tac.rtrancl_tac));
7.62 +
7.63 +*}
7.64 +
7.65 +(* Optional methods
7.66 +
7.67 +method_setup trancl =
7.68 + {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (trancl_tac)) *}
7.69 + {* simple transitivity reasoner *}
7.70 +method_setup rtrancl =
7.71 + {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (rtrancl_tac)) *}
7.72 + {* simple transitivity reasoner *}
7.73 +
7.74 +*)
7.75 +
7.76 end
8.1 --- a/src/HOL/UNITY/Simple/Reach.thy Thu Jul 22 19:33:12 2004 +0200
8.2 +++ b/src/HOL/UNITY/Simple/Reach.thy Mon Jul 26 15:48:50 2004 +0200
8.3 @@ -75,7 +75,7 @@
8.4 apply (unfold fixedpoint_def)
8.5 apply (rule equalityI)
8.6 apply (auto intro!: ext)
8.7 - prefer 2 apply (blast intro: rtrancl_trans)
8.8 +(* CBtrancl: prefer 2 apply (blast intro: rtrancl_trans) *)
8.9 apply (erule rtrancl_induct, auto)
8.10 done
8.11
9.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
9.2 +++ b/src/Provers/trancl.ML Mon Jul 26 15:48:50 2004 +0200
9.3 @@ -0,0 +1,478 @@
9.4 +(*
9.5 + Title: Transitivity reasoner for partial and linear orders
9.6 + Id: $Id$
9.7 + Author: Oliver Kutter
9.8 + Copyright: TU Muenchen
9.9 +*)
9.10 +
9.11 +signature TRANCL_ARITH =
9.12 +sig
9.13 +
9.14 + (* theorems for transitive closure *)
9.15 +
9.16 + val r_into_trancl : thm
9.17 + (* (a,b) : r ==> (a,b) : r^+ *)
9.18 + val trancl_trans : thm
9.19 + (* [| (a,b) : r^+ ; (b,c) : r^+ |] ==> (a,c) : r^+ *)
9.20 +
9.21 + (* additional theorems for reflexive-transitive closure *)
9.22 +
9.23 + val rtrancl_refl : thm
9.24 + (* (a,a): r^* *)
9.25 + val r_into_rtrancl : thm
9.26 + (* (a,b) : r ==> (a,b) : r^* *)
9.27 + val trancl_into_rtrancl : thm
9.28 + (* (a,b) : r^+ ==> (a,b) : r^* *)
9.29 + val rtrancl_trancl_trancl : thm
9.30 + (* [| (a,b) : r^* ; (b,c) : r^+ |] ==> (a,c) : r^+ *)
9.31 + val trancl_rtrancl_trancl : thm
9.32 + (* [| (a,b) : r^+ ; (b,c) : r^* |] ==> (a,c) : r^+ *)
9.33 + val rtrancl_trans : thm
9.34 + (* [| (a,b) : r^* ; (b,c) : r^* |] ==> (a,c) : r^* *)
9.35 +
9.36 + val decomp: term -> (term * term * term * string) option
9.37 +
9.38 +end;
9.39 +
9.40 +signature TRANCL_TAC =
9.41 +sig
9.42 + val trancl_tac: int -> tactic;
9.43 + val rtrancl_tac: int -> tactic;
9.44 +end;
9.45 +
9.46 +functor Trancl_Tac_Fun (Cls : TRANCL_ARITH): TRANCL_TAC =
9.47 +struct
9.48 +
9.49 +
9.50 + datatype proof
9.51 + = Asm of int
9.52 + | Thm of proof list * thm;
9.53 +
9.54 + exception Cannot;
9.55 +
9.56 + fun prove asms =
9.57 + let fun pr (Asm i) = nth_elem (i, asms)
9.58 + | pr (Thm (prfs, thm)) = (map pr prfs) MRS thm
9.59 + in pr end;
9.60 +
9.61 +
9.62 +(* Internal datatype for inequalities *)
9.63 +datatype rel
9.64 + = R of term * term * proof (* just a unknown relation R *)
9.65 + | Trans of term * term * proof (* R^+ *)
9.66 + | RTrans of term * term * proof; (* R^* *)
9.67 +
9.68 + (* Misc functions for datatype rel *)
9.69 +fun lower (R (x, _, _)) = x
9.70 + | lower (Trans (x, _, _)) = x
9.71 + | lower (RTrans (x,_,_)) = x;
9.72 +
9.73 +fun upper (R (_, y, _)) = y
9.74 + | upper (Trans (_, y, _)) = y
9.75 + | upper (RTrans (_,y,_)) = y;
9.76 +
9.77 +fun getprf (R (_, _, p)) = p
9.78 +| getprf (Trans (_, _, p)) = p
9.79 +| getprf (RTrans (_,_, p)) = p;
9.80 +
9.81 +fun mkasm_trancl Rel (t, n) =
9.82 + case Cls.decomp t of
9.83 + Some (x, y, rel,r) => if rel aconv Rel then
9.84 +
9.85 + (case r of
9.86 + "r" => [Trans (x,y, Thm([Asm n], Cls.r_into_trancl))]
9.87 + | "r+" => [Trans (x,y, Asm n)]
9.88 + | "r*" => []
9.89 + | _ => error ("trancl_tac: unknown relation symbol"))
9.90 + else []
9.91 + | None => [];
9.92 +
9.93 +fun mkasm_rtrancl Rel (t, n) =
9.94 + case Cls.decomp t of
9.95 + Some (x, y, rel, r) => if rel aconv Rel then
9.96 + (case r of
9.97 + "r" => [ Trans (x,y, Thm([Asm n], Cls.r_into_trancl))]
9.98 + | "r+" => [ Trans (x,y, Asm n)]
9.99 + | "r*" => [ RTrans(x,y, Asm n)]
9.100 + | _ => error ("rtrancl_tac: unknown relation symbol" ))
9.101 + else []
9.102 + | None => [];
9.103 +
9.104 +fun mkconcl_trancl t =
9.105 + case Cls.decomp t of
9.106 + Some (x, y, rel, r) => (case r of
9.107 + "r+" => (rel, Trans (x,y, Asm ~1), Asm 0)
9.108 + | _ => raise Cannot)
9.109 + | None => raise Cannot;
9.110 +
9.111 +fun mkconcl_rtrancl t =
9.112 + case Cls.decomp t of
9.113 + Some (x, y, rel,r ) => (case r of
9.114 + "r+" => (rel, Trans (x,y, Asm ~1), Asm 0)
9.115 + | "r*" => (rel, RTrans (x,y, Asm ~1), Asm 0)
9.116 + | _ => raise Cannot)
9.117 + | None => raise Cannot;
9.118 +
9.119 +(* trans. cls. rules *)
9.120 +fun makeStep (Trans (a,_,p), Trans(_,c,q)) = Trans (a,c, Thm ([p,q], Cls.trancl_trans))
9.121 +(* refl. + trans. cls. rules *)
9.122 +| makeStep (RTrans (a,_,p), Trans(_,c,q)) = Trans (a,c, Thm ([p,q], Cls.rtrancl_trancl_trancl))
9.123 +| makeStep (Trans (a,_,p), RTrans(_,c,q)) = Trans (a,c, Thm ([p,q], Cls.trancl_rtrancl_trancl))
9.124 +| makeStep (RTrans (a,_,p), RTrans(_,c,q)) = RTrans (a,c, Thm ([p,q], Cls.rtrancl_trans))
9.125 +| makeStep (a,b) = error ("makeStep: internal error: undefined case\n"^(makestring a) ^"\n" ^ (makestring b));
9.126 +
9.127 +(* ******************************************************************* *)
9.128 +(* *)
9.129 +(* transPath (Clslist, Cls): (rel list * rel) -> rel *)
9.130 +(* *)
9.131 +(* If a path represented by a list of elements of type rel is found, *)
9.132 +(* this needs to be contracted to a single element of type rel. *)
9.133 +(* Prior to each transitivity step it is checked whether the step is *)
9.134 +(* valid. *)
9.135 +(* *)
9.136 +(* ******************************************************************* *)
9.137 +
9.138 +fun transPath ([],acc) = acc
9.139 +| transPath (x::xs,acc) = transPath (xs, makeStep(acc,x))
9.140 +
9.141 +(* ********************************************************************* *)
9.142 +(* Graph functions *)
9.143 +(* ********************************************************************* *)
9.144 +
9.145 +(* *********************************************************** *)
9.146 +(* Functions for constructing graphs *)
9.147 +(* *********************************************************** *)
9.148 +
9.149 +fun addEdge (v,d,[]) = [(v,d)]
9.150 +| addEdge (v,d,((u,dl)::el)) = if v aconv u then ((v,d@dl)::el)
9.151 + else (u,dl):: (addEdge(v,d,el));
9.152 +
9.153 +(* ********************************************************************** *)
9.154 +(* *)
9.155 +(* mkGraph constructs from a list of objects of type rel a graph g *)
9.156 +(* *)
9.157 +(* ********************************************************************** *)
9.158 +
9.159 +fun mkGraph [] = ([],[])
9.160 +| mkGraph ys =
9.161 + let
9.162 + fun buildGraph ([],g,zs) = (g,zs)
9.163 + | buildGraph (x::xs, g, zs) =
9.164 + case x of (Trans (_,_,_)) =>
9.165 + buildGraph (xs, addEdge((upper x), [],(addEdge ((lower x),[((upper x),x)],g))), x::zs)
9.166 + | _ => buildGraph (xs, addEdge((upper x), [],(addEdge ((lower x),[((upper x),x)],g))), zs)
9.167 +in buildGraph (ys, [], []) end;
9.168 +
9.169 +(* *********************************************************************** *)
9.170 +(* *)
9.171 +(* adjacent g u : (''a * 'b list ) list -> ''a -> 'b list *)
9.172 +(* *)
9.173 +(* List of successors of u in graph g *)
9.174 +(* *)
9.175 +(* *********************************************************************** *)
9.176 +
9.177 +fun adjacent eq_comp ((v,adj)::el) u =
9.178 + if eq_comp (u, v) then adj else adjacent eq_comp el u
9.179 +| adjacent _ [] _ = []
9.180 +
9.181 +(* *********************************************************************** *)
9.182 +(* *)
9.183 +(* dfs eq_comp g u v: *)
9.184 +(* ('a * 'a -> bool) -> ('a *( 'a * rel) list) list -> *)
9.185 +(* 'a -> 'a -> (bool * ('a * rel) list) *)
9.186 +(* *)
9.187 +(* Depth first search of v from u. *)
9.188 +(* Returns (true, path(u, v)) if successful, otherwise (false, []). *)
9.189 +(* *)
9.190 +(* *********************************************************************** *)
9.191 +
9.192 +fun dfs eq_comp g u v =
9.193 + let
9.194 + val pred = ref nil;
9.195 + val visited = ref nil;
9.196 +
9.197 + fun been_visited v = exists (fn w => eq_comp (w, v)) (!visited)
9.198 +
9.199 + fun dfs_visit u' =
9.200 + let val _ = visited := u' :: (!visited)
9.201 +
9.202 + fun update (x,l) = let val _ = pred := (x,l) ::(!pred) in () end;
9.203 +
9.204 + in if been_visited v then ()
9.205 + else (app (fn (v',l) => if been_visited v' then () else (
9.206 + update (v',l);
9.207 + dfs_visit v'; ()) )) (adjacent eq_comp g u')
9.208 + end
9.209 + in
9.210 + dfs_visit u;
9.211 + if (been_visited v) then (true, (!pred)) else (false , [])
9.212 + end;
9.213 +
9.214 +(* *********************************************************************** *)
9.215 +(* *)
9.216 +(* transpose g: *)
9.217 +(* (''a * ''a list) list -> (''a * ''a list) list *)
9.218 +(* *)
9.219 +(* Computes transposed graph g' from g *)
9.220 +(* by reversing all edges u -> v to v -> u *)
9.221 +(* *)
9.222 +(* *********************************************************************** *)
9.223 +
9.224 +fun transpose eq_comp g =
9.225 + let
9.226 + (* Compute list of reversed edges for each adjacency list *)
9.227 + fun flip (u,(v,l)::el) = (v,(u,l)) :: flip (u,el)
9.228 + | flip (_,nil) = nil
9.229 +
9.230 + (* Compute adjacency list for node u from the list of edges
9.231 + and return a likewise reduced list of edges. The list of edges
9.232 + is searches for edges starting from u, and these edges are removed. *)
9.233 + fun gather (u,(v,w)::el) =
9.234 + let
9.235 + val (adj,edges) = gather (u,el)
9.236 + in
9.237 + if eq_comp (u, v) then (w::adj,edges)
9.238 + else (adj,(v,w)::edges)
9.239 + end
9.240 + | gather (_,nil) = (nil,nil)
9.241 +
9.242 + (* For every node in the input graph, call gather to find all reachable
9.243 + nodes in the list of edges *)
9.244 + fun assemble ((u,_)::el) edges =
9.245 + let val (adj,edges) = gather (u,edges)
9.246 + in (u,adj) :: assemble el edges
9.247 + end
9.248 + | assemble nil _ = nil
9.249 +
9.250 + (* Compute, for each adjacency list, the list with reversed edges,
9.251 + and concatenate these lists. *)
9.252 + val flipped = foldr (op @) ((map flip g),nil)
9.253 +
9.254 + in assemble g flipped end
9.255 +
9.256 +(* *********************************************************************** *)
9.257 +(* *)
9.258 +(* dfs_reachable eq_comp g u: *)
9.259 +(* (int * int list) list -> int -> int list *)
9.260 +(* *)
9.261 +(* Computes list of all nodes reachable from u in g. *)
9.262 +(* *)
9.263 +(* *********************************************************************** *)
9.264 +
9.265 +fun dfs_reachable eq_comp g u =
9.266 + let
9.267 + (* List of vertices which have been visited. *)
9.268 + val visited = ref nil;
9.269 +
9.270 + fun been_visited v = exists (fn w => eq_comp (w, v)) (!visited)
9.271 +
9.272 + fun dfs_visit g u =
9.273 + let
9.274 + val _ = visited := u :: !visited
9.275 + val descendents =
9.276 + foldr (fn ((v,l),ds) => if been_visited v then ds
9.277 + else v :: dfs_visit g v @ ds)
9.278 + ( ((adjacent eq_comp g u)) ,nil)
9.279 + in descendents end
9.280 +
9.281 + in u :: dfs_visit g u end;
9.282 +
9.283 +(* *********************************************************************** *)
9.284 +(* *)
9.285 +(* dfs_term_reachable g u: *)
9.286 +(* (term * term list) list -> term -> term list *)
9.287 +(* *)
9.288 +(* Computes list of all nodes reachable from u in g. *)
9.289 +(* *)
9.290 +(* *********************************************************************** *)
9.291 +
9.292 +fun dfs_term_reachable g u = dfs_reachable (op aconv) g u;
9.293 +
9.294 +(* ************************************************************************ *)
9.295 +(* *)
9.296 +(* findPath x y g: Term.term -> Term.term -> *)
9.297 +(* (Term.term * (Term.term * rel list) list) -> *)
9.298 +(* (bool, rel list) *)
9.299 +(* *)
9.300 +(* Searches a path from vertex x to vertex y in Graph g, returns true and *)
9.301 +(* the list of edges of edges if path is found, otherwise false and nil. *)
9.302 +(* *)
9.303 +(* ************************************************************************ *)
9.304 +
9.305 +fun findPath x y g =
9.306 + let
9.307 + val (found, tmp) = dfs (op aconv) g x y ;
9.308 + val pred = map snd tmp;
9.309 +
9.310 + fun path x y =
9.311 + let
9.312 + (* find predecessor u of node v and the edge u -> v *)
9.313 +
9.314 + fun lookup v [] = raise Cannot
9.315 + | lookup v (e::es) = if (upper e) aconv v then e else lookup v es;
9.316 +
9.317 + (* traverse path backwards and return list of visited edges *)
9.318 + fun rev_path v =
9.319 + let val l = lookup v pred
9.320 + val u = lower l;
9.321 + in
9.322 + if u aconv x then [l] else (rev_path u) @ [l]
9.323 + end
9.324 +
9.325 + in rev_path y end;
9.326 +
9.327 + in
9.328 +
9.329 +
9.330 + if found then ( (found, (path x y) )) else (found,[])
9.331 +
9.332 +
9.333 +
9.334 + end;
9.335 +
9.336 +
9.337 +fun findRtranclProof g tranclEdges subgoal =
9.338 + (* simple case first *)
9.339 + case subgoal of (RTrans (x,y,_)) => if x aconv y then [Thm ([], Cls.rtrancl_refl)] else (
9.340 + let val (found, path) = findPath (lower subgoal) (upper subgoal) g
9.341 + in
9.342 + if found then (
9.343 + let val path' = (transPath (tl path, hd path))
9.344 + in
9.345 +
9.346 + case path' of (Trans (_,_,p)) => [Thm ([p], Cls.trancl_into_rtrancl )]
9.347 + | _ => [getprf path']
9.348 +
9.349 + end
9.350 + )
9.351 + else raise Cannot
9.352 + end
9.353 + )
9.354 +
9.355 +| (Trans (x,y,_)) => (
9.356 +
9.357 + let
9.358 + val Vx = dfs_term_reachable g x;
9.359 + val g' = transpose (op aconv) g;
9.360 + val Vy = dfs_term_reachable g' y;
9.361 +
9.362 + fun processTranclEdges [] = raise Cannot
9.363 + | processTranclEdges (e::es) =
9.364 + if (upper e) mem Vx andalso (lower e) mem Vx
9.365 + andalso (upper e) mem Vy andalso (lower e) mem Vy
9.366 + then (
9.367 +
9.368 +
9.369 + if (lower e) aconv x then (
9.370 + if (upper e) aconv y then (
9.371 + [(getprf e)]
9.372 + )
9.373 + else (
9.374 + let
9.375 + val (found,path) = findPath (upper e) y g
9.376 + in
9.377 +
9.378 + if found then (
9.379 + [getprf (transPath (path, e))]
9.380 + ) else processTranclEdges es
9.381 +
9.382 + end
9.383 + )
9.384 + )
9.385 + else if (upper e) aconv y then (
9.386 + let val (xufound,xupath) = findPath x (lower e) g
9.387 + in
9.388 +
9.389 + if xufound then (
9.390 +
9.391 + let val xuRTranclEdge = transPath (tl xupath, hd xupath)
9.392 + val xyTranclEdge = makeStep(xuRTranclEdge,e)
9.393 +
9.394 + in [getprf xyTranclEdge] end
9.395 +
9.396 + ) else processTranclEdges es
9.397 +
9.398 + end
9.399 + )
9.400 + else (
9.401 +
9.402 + let val (xufound,xupath) = findPath x (lower e) g
9.403 + val (vyfound,vypath) = findPath (upper e) y g
9.404 + in
9.405 + if xufound then (
9.406 + if vyfound then (
9.407 + let val xuRTranclEdge = transPath (tl xupath, hd xupath)
9.408 + val vyRTranclEdge = transPath (tl vypath, hd vypath)
9.409 + val xyTranclEdge = makeStep (makeStep(xuRTranclEdge,e),vyRTranclEdge)
9.410 +
9.411 + in [getprf xyTranclEdge] end
9.412 +
9.413 + ) else processTranclEdges es
9.414 + )
9.415 + else processTranclEdges es
9.416 + end
9.417 + )
9.418 + )
9.419 + else processTranclEdges es;
9.420 + in processTranclEdges tranclEdges end )
9.421 +| _ => raise Cannot
9.422 +
9.423 +
9.424 +fun solveTrancl (asms, concl) =
9.425 + let val (g,_) = mkGraph asms
9.426 + in
9.427 + let val (_, subgoal, _) = mkconcl_trancl concl
9.428 + val (found, path) = findPath (lower subgoal) (upper subgoal) g
9.429 + in
9.430 +
9.431 +
9.432 + if found then [getprf (transPath (tl path, hd path))]
9.433 + else raise Cannot
9.434 +
9.435 + end
9.436 + end;
9.437 +
9.438 +
9.439 +
9.440 +fun solveRtrancl (asms, concl) =
9.441 + let val (g,tranclEdges) = mkGraph asms
9.442 + val (_, subgoal, _) = mkconcl_rtrancl concl
9.443 +in
9.444 + findRtranclProof g tranclEdges subgoal
9.445 +end;
9.446 +
9.447 +
9.448 +val trancl_tac = SUBGOAL (fn (A, n) =>
9.449 + let
9.450 + val Hs = Logic.strip_assums_hyp A;
9.451 + val C = Logic.strip_assums_concl A;
9.452 + val (rel,subgoals, prf) = mkconcl_trancl C;
9.453 + val prems = flat (ListPair.map (mkasm_trancl rel) (Hs, 0 upto (length Hs - 1)))
9.454 + val prfs = solveTrancl (prems, C);
9.455 +
9.456 + in
9.457 + METAHYPS (fn asms =>
9.458 + let val thms = map (prove asms) prfs
9.459 + in rtac (prove thms prf) 1 end) n
9.460 + end
9.461 +handle Cannot => no_tac);
9.462 +
9.463 +
9.464 +
9.465 +val rtrancl_tac = SUBGOAL (fn (A, n) =>
9.466 + let
9.467 + val Hs = Logic.strip_assums_hyp A;
9.468 + val C = Logic.strip_assums_concl A;
9.469 + val (rel,subgoals, prf) = mkconcl_rtrancl C;
9.470 +
9.471 + val prems = flat (ListPair.map (mkasm_rtrancl rel) (Hs, 0 upto (length Hs - 1)))
9.472 + val prfs = solveRtrancl (prems, C);
9.473 + in
9.474 + METAHYPS (fn asms =>
9.475 + let val thms = map (prove asms) prfs
9.476 + in rtac (prove thms prf) 1 end) n
9.477 + end
9.478 +handle Cannot => no_tac);
9.479 +
9.480 +end;
9.481 +