# HG changeset patch # User wenzelm # Date 1248640111 -7200 # Node ID 87806301a813ed117bb7215f7305fbea22ee6ee1 # Parent 6a6827bad05f446d4dbb9295c38659854e40748a replaced old METAHYPS by FOCUS; eliminated homegrown SUBGOAL combinator -- beware of exception Subscript in body; modernized functor names; minimal tuning of sources; reactivated dead quasi.ML (ever used?); diff -r 6a6827bad05f -r 87806301a813 src/HOL/Orderings.thy --- a/src/HOL/Orderings.thy Sun Jul 26 22:24:13 2009 +0200 +++ b/src/HOL/Orderings.thy Sun Jul 26 22:28:31 2009 +0200 @@ -6,7 +6,9 @@ theory Orderings imports HOL -uses "~~/src/Provers/order.ML" +uses + "~~/src/Provers/order.ML" + "~~/src/Provers/quasi.ML" (* FIXME unused? *) begin subsection {* Quasi orders *} @@ -289,7 +291,7 @@ sig val print_structures: Proof.context -> unit val setup: theory -> theory - val order_tac: thm list -> Proof.context -> int -> tactic + val order_tac: Proof.context -> thm list -> int -> tactic end; structure Orders: ORDERS = @@ -329,7 +331,7 @@ (** Method **) -fun struct_tac ((s, [eq, le, less]), thms) prems = +fun struct_tac ((s, [eq, le, less]), thms) ctxt prems = let fun decomp thy (@{const Trueprop} $ t) = let @@ -354,13 +356,13 @@ | decomp thy _ = NONE; in case s of - "order" => Order_Tac.partial_tac decomp thms prems - | "linorder" => Order_Tac.linear_tac decomp thms prems + "order" => Order_Tac.partial_tac decomp thms ctxt prems + | "linorder" => Order_Tac.linear_tac decomp thms ctxt prems | _ => error ("Unknown kind of order `" ^ s ^ "' encountered in transitivity reasoner.") end -fun order_tac prems ctxt = - FIRST' (map (fn s => CHANGED o struct_tac s prems) (Data.get (Context.Proof ctxt))); +fun order_tac ctxt prems = + FIRST' (map (fn s => CHANGED o struct_tac s ctxt prems) (Data.get (Context.Proof ctxt))); (** Attribute **) @@ -394,7 +396,7 @@ (** Setup **) val setup = - Method.setup @{binding order} (Scan.succeed (SIMPLE_METHOD' o order_tac [])) + Method.setup @{binding order} (Scan.succeed (fn ctxt => SIMPLE_METHOD' (order_tac ctxt []))) "transitivity reasoner" #> attrib_setup; @@ -532,7 +534,7 @@ Simplifier.simproc thy name raw_ts proc) procs)) thy; fun add_solver name tac = Simplifier.map_simpset (fn ss => ss addSolver - mk_solver' name (fn ss => tac (Simplifier.prems_of_ss ss) (Simplifier.the_context ss))); + mk_solver' name (fn ss => tac (Simplifier.the_context ss) (Simplifier.prems_of_ss ss))); in add_simprocs [ diff -r 6a6827bad05f -r 87806301a813 src/HOL/Transitive_Closure.thy --- a/src/HOL/Transitive_Closure.thy Sun Jul 26 22:24:13 2009 +0200 +++ b/src/HOL/Transitive_Closure.thy Sun Jul 26 22:28:31 2009 +0200 @@ -811,16 +811,16 @@ ML {* -structure Trancl_Tac = Trancl_Tac_Fun ( - struct - val r_into_trancl = @{thm trancl.r_into_trancl}; - val trancl_trans = @{thm trancl_trans}; - val rtrancl_refl = @{thm rtrancl.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}; +structure Trancl_Tac = Trancl_Tac +( + val r_into_trancl = @{thm trancl.r_into_trancl}; + val trancl_trans = @{thm trancl_trans}; + val rtrancl_refl = @{thm rtrancl.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 (@{const Trueprop} $ t) = let fun dec (Const ("op :", _) $ (Const ("Pair", _) $ a $ b) $ rel ) = @@ -832,19 +832,18 @@ | dec _ = NONE in dec t end | decomp _ = NONE; - - end); +); -structure Tranclp_Tac = Trancl_Tac_Fun ( - struct - val r_into_trancl = @{thm tranclp.r_into_trancl}; - val trancl_trans = @{thm tranclp_trans}; - val rtrancl_refl = @{thm rtranclp.rtrancl_refl}; - val r_into_rtrancl = @{thm r_into_rtranclp}; - val trancl_into_rtrancl = @{thm tranclp_into_rtranclp}; - val rtrancl_trancl_trancl = @{thm rtranclp_tranclp_tranclp}; - val trancl_rtrancl_trancl = @{thm tranclp_rtranclp_tranclp}; - val rtrancl_trans = @{thm rtranclp_trans}; +structure Tranclp_Tac = Trancl_Tac +( + val r_into_trancl = @{thm tranclp.r_into_trancl}; + val trancl_trans = @{thm tranclp_trans}; + val rtrancl_refl = @{thm rtranclp.rtrancl_refl}; + val r_into_rtrancl = @{thm r_into_rtranclp}; + val trancl_into_rtrancl = @{thm tranclp_into_rtranclp}; + val rtrancl_trancl_trancl = @{thm rtranclp_tranclp_tranclp}; + val trancl_rtrancl_trancl = @{thm tranclp_rtranclp_tranclp}; + val rtrancl_trans = @{thm rtranclp_trans}; fun decomp (@{const Trueprop} $ t) = let fun dec (rel $ a $ b) = @@ -856,31 +855,31 @@ | dec _ = NONE in dec t end | decomp _ = NONE; - - end); +); *} declaration {* fn _ => Simplifier.map_ss (fn ss => ss - addSolver (mk_solver "Trancl" (fn _ => Trancl_Tac.trancl_tac)) - addSolver (mk_solver "Rtrancl" (fn _ => Trancl_Tac.rtrancl_tac)) - addSolver (mk_solver "Tranclp" (fn _ => Tranclp_Tac.trancl_tac)) - addSolver (mk_solver "Rtranclp" (fn _ => Tranclp_Tac.rtrancl_tac))) + addSolver (mk_solver' "Trancl" (Trancl_Tac.trancl_tac o Simplifier.the_context)) + addSolver (mk_solver' "Rtrancl" (Trancl_Tac.rtrancl_tac o Simplifier.the_context)) + addSolver (mk_solver' "Tranclp" (Tranclp_Tac.trancl_tac o Simplifier.the_context)) + addSolver (mk_solver' "Rtranclp" (Tranclp_Tac.rtrancl_tac o Simplifier.the_context))) *} -(* Optional methods *) + +text {* Optional methods. *} method_setup trancl = - {* Scan.succeed (K (SIMPLE_METHOD' Trancl_Tac.trancl_tac)) *} + {* Scan.succeed (SIMPLE_METHOD' o Trancl_Tac.trancl_tac) *} {* simple transitivity reasoner *} method_setup rtrancl = - {* Scan.succeed (K (SIMPLE_METHOD' Trancl_Tac.rtrancl_tac)) *} + {* Scan.succeed (SIMPLE_METHOD' o Trancl_Tac.rtrancl_tac) *} {* simple transitivity reasoner *} method_setup tranclp = - {* Scan.succeed (K (SIMPLE_METHOD' Tranclp_Tac.trancl_tac)) *} + {* Scan.succeed (SIMPLE_METHOD' o Tranclp_Tac.trancl_tac) *} {* simple transitivity reasoner (predicate version) *} method_setup rtranclp = - {* Scan.succeed (K (SIMPLE_METHOD' Tranclp_Tac.rtrancl_tac)) *} + {* Scan.succeed (SIMPLE_METHOD' o Tranclp_Tac.rtrancl_tac) *} {* simple transitivity reasoner (predicate version) *} end diff -r 6a6827bad05f -r 87806301a813 src/Provers/order.ML --- a/src/Provers/order.ML Sun Jul 26 22:24:13 2009 +0200 +++ b/src/Provers/order.ML Sun Jul 26 22:28:31 2009 +0200 @@ -35,9 +35,11 @@ (* Tactics *) val partial_tac: - (theory -> term -> (term * string * term) option) -> less_arith -> thm list -> int -> tactic + (theory -> term -> (term * string * term) option) -> less_arith -> + Proof.context -> thm list -> int -> tactic val linear_tac: - (theory -> term -> (term * string * term) option) -> less_arith -> thm list -> int -> tactic + (theory -> term -> (term * string * term) option) -> less_arith -> + Proof.context -> thm list -> int -> tactic end; structure Order_Tac: ORDER_TAC = @@ -259,34 +261,28 @@ less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans, not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, thm)); - -(* Extract subgoal with signature *) -fun SUBGOAL goalfun i st = - goalfun (List.nth(prems_of st, i-1), i, Thm.theory_of_thm st) st - handle Subscript => Seq.empty; - (* Internal datatype for the proof *) datatype proof - = Asm of int - | Thm of proof list * thm; - + = Asm of int + | Thm of proof list * thm; + exception Cannot; (* Internal exception, raised if conclusion cannot be derived from assumptions. *) exception Contr of proof; (* Internal exception, raised if contradiction ( x < x ) was derived *) -fun prove asms = +fun prove asms = let fun pr (Asm i) = List.nth (asms, i) | pr (Thm (prfs, thm)) = (map pr prfs) MRS thm in pr end; (* Internal datatype for inequalities *) -datatype less - = Less of term * term * proof +datatype less + = Less of term * term * proof | Le of term * term * proof - | NotEq of term * term * proof; - + | NotEq of term * term * proof; + (* Misc functions for datatype less *) fun lower (Less (x, _, _)) = x | lower (Le (x, _, _)) = x @@ -314,17 +310,17 @@ fun mkasm_partial decomp (less_thms : less_arith) sign (t, n) = case decomp sign t of SOME (x, rel, y) => (case rel of - "<" => if (x aconv y) then raise Contr (Thm ([Asm n], #less_reflE less_thms)) + "<" => if (x aconv y) then raise Contr (Thm ([Asm n], #less_reflE less_thms)) else [Less (x, y, Asm n)] | "~<" => [] | "<=" => [Le (x, y, Asm n)] - | "~<=" => [] + | "~<=" => [] | "=" => [Le (x, y, Thm ([Asm n], #eqD1 less_thms)), Le (y, x, Thm ([Asm n], #eqD2 less_thms))] - | "~=" => if (x aconv y) then + | "~=" => if (x aconv y) then raise Contr (Thm ([(Thm ([(Thm ([], #le_refl less_thms)) ,(Asm n)], #le_neq_trans less_thms))], #less_reflE less_thms)) else [ NotEq (x, y, Asm n), - NotEq (y, x,Thm ( [Asm n], #not_sym less_thms))] + NotEq (y, x,Thm ( [Asm n], #not_sym less_thms))] | _ => error ("partial_tac: unknown relation symbol ``" ^ rel ^ "''returned by decomp.")) | NONE => []; @@ -338,23 +334,23 @@ (* Linear orders only. *) (* *) (* ************************************************************************ *) - + fun mkasm_linear decomp (less_thms : less_arith) sign (t, n) = case decomp sign t of SOME (x, rel, y) => (case rel of - "<" => if (x aconv y) then raise Contr (Thm ([Asm n], #less_reflE less_thms)) + "<" => if (x aconv y) then raise Contr (Thm ([Asm n], #less_reflE less_thms)) else [Less (x, y, Asm n)] | "~<" => [Le (y, x, Thm ([Asm n], #not_lessD less_thms))] | "<=" => [Le (x, y, Asm n)] - | "~<=" => if (x aconv y) then - raise (Contr (Thm ([Thm ([Asm n], #not_leD less_thms)], #less_reflE less_thms))) - else [Less (y, x, Thm ([Asm n], #not_leD less_thms))] + | "~<=" => if (x aconv y) then + raise (Contr (Thm ([Thm ([Asm n], #not_leD less_thms)], #less_reflE less_thms))) + else [Less (y, x, Thm ([Asm n], #not_leD less_thms))] | "=" => [Le (x, y, Thm ([Asm n], #eqD1 less_thms)), Le (y, x, Thm ([Asm n], #eqD2 less_thms))] - | "~=" => if (x aconv y) then + | "~=" => if (x aconv y) then raise Contr (Thm ([(Thm ([(Thm ([], #le_refl less_thms)) ,(Asm n)], #le_neq_trans less_thms))], #less_reflE less_thms)) else [ NotEq (x, y, Asm n), - NotEq (y, x,Thm ( [Asm n], #not_sym less_thms))] + NotEq (y, x,Thm ( [Asm n], #not_sym less_thms))] | _ => error ("linear_tac: unknown relation symbol ``" ^ rel ^ "''returned by decomp.")) | NONE => []; @@ -409,7 +405,7 @@ where Rel is one of "<", "<=", "~<", "~<=", "=" and "~=", other relation symbols cause an error message *) -fun gen_order_tac mkasm mkconcl decomp' (less_thms : less_arith) prems = +fun gen_order_tac mkasm mkconcl decomp' (less_thms : less_arith) ctxt prems = let @@ -440,19 +436,19 @@ | mergeLess (Le (x, _, p) , Less (_ , z, q)) = Less (x, z, Thm ([p,q] , #le_less_trans less_thms)) | mergeLess (Le (x, z, p) , NotEq (x', z', q)) = - if (x aconv x' andalso z aconv z' ) + if (x aconv x' andalso z aconv z' ) then Less (x, z, Thm ([p,q] , #le_neq_trans less_thms)) else error "linear/partial_tac: internal error le_neq_trans" | mergeLess (NotEq (x, z, p) , Le (x' , z', q)) = - if (x aconv x' andalso z aconv z') + if (x aconv x' andalso z aconv z') then Less (x, z, Thm ([p,q] , #neq_le_trans less_thms)) else error "linear/partial_tac: internal error neq_le_trans" | mergeLess (NotEq (x, z, p) , Less (x' , z', q)) = - if (x aconv x' andalso z aconv z') + if (x aconv x' andalso z aconv z') then Less ((x' , z', q)) else error "linear/partial_tac: internal error neq_less_trans" | mergeLess (Less (x, z, p) , NotEq (x', z', q)) = - if (x aconv x' andalso z aconv z') + if (x aconv x' andalso z aconv z') then Less (x, z, p) else error "linear/partial_tac: internal error less_neq_trans" | mergeLess (Le (x, _, p) , Le (_ , z, q)) = @@ -471,8 +467,8 @@ | (Less (_, y, _)) tr (Less (x', _, _)) = ( y aconv x' ) | (Le (_, y, _)) tr (Le (x', _, _)) = ( y aconv x' ) | _ tr _ = false; - - + + (* ******************************************************************* *) (* *) (* transPath (Lesslist, Less): (less list * less) -> less *) @@ -488,7 +484,7 @@ | transPath (x::xs,lesss) = if lesss tr x then transPath (xs, mergeLess(lesss,x)) else error "linear/partial_tac: internal error transpath"; - + (* ******************************************************************* *) (* *) (* less1 subsumes less2 : less -> less -> bool *) @@ -496,7 +492,7 @@ (* subsumes checks whether less1 implies less2 *) (* *) (* ******************************************************************* *) - + infix subsumes; fun (Less (x, y, _)) subsumes (Le (x', y', _)) = (x aconv x' andalso y aconv y') @@ -554,7 +550,7 @@ (* *) (* ******************************************************************* *) - + (* *********************************************************** *) (* Functions for constructing graphs *) (* *********************************************************** *) @@ -562,27 +558,27 @@ 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)); - + (* ********************************************************************* *) (* *) -(* mkGraphs constructs from a list of objects of type less a graph g, *) +(* 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 = +| mkGraphs lessList = let 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) +| 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)) => - buildGraphs (ls, addEdge (x,[(y,(Le (x, y,p)))],leqG) , neqG, neqE) -| (NotEq (x,y,p)) => + 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; @@ -595,12 +591,12 @@ (* List of successors of u in graph g *) (* *) (* *********************************************************************** *) - -fun adjacent eq_comp ((v,adj)::el) u = + +fun adjacent eq_comp ((v,adj)::el) u = if eq_comp (u, v) then adj else adjacent eq_comp el u -| adjacent _ [] _ = [] - - +| adjacent _ [] _ = [] + + (* *********************************************************************** *) (* *) (* transpose g: *) @@ -616,7 +612,7 @@ (* 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. *) @@ -640,19 +636,19 @@ (* Compute, for each adjacency list, the list with reversed edges, and concatenate these lists. *) val flipped = List.foldr (op @) nil (map flip g) - - in assemble g flipped end - + + in assemble g flipped end + (* *********************************************************************** *) -(* *) +(* *) (* 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). *) -(* *) +(* components (each a list of vertices). *) +(* *) (* *) (* *********************************************************************** *) @@ -664,11 +660,11 @@ (* List of vertices which have been visited. *) val visited : term list ref = ref nil - + fun been_visited v = exists (fn w => w aconv v) (!visited) - + (* Given the adjacency list rep of a graph (a list of pairs), - return just the first element of each pair, yielding the + return just the first element of each pair, yielding the vertex list. *) val members = map (fn (v,_) => v) @@ -701,7 +697,7 @@ dfs_visit along with u form a connected component. We collect all the connected components together in a list, which is what is returned. *) - Library.foldl (fn (comps,u) => + Library.foldl (fn (comps,u) => if been_visited u then comps else ((u :: dfs_visit (transpose (op aconv) G) u) :: comps)) (nil,(!finish)) end; @@ -710,17 +706,17 @@ (* *********************************************************************** *) (* *) (* dfs_int_reachable g u: *) -(* (int * int list) list -> int -> int list *) +(* (int * int list) list -> int -> int list *) (* *) (* Computes list of all nodes reachable from u in g. *) (* *) (* *********************************************************************** *) -fun dfs_int_reachable g u = +fun dfs_int_reachable g u = let (* List of vertices which have been visited. *) val visited : int list ref = ref nil - + fun been_visited v = exists (fn w => w = v) (!visited) fun dfs_visit g u : int list = @@ -731,59 +727,59 @@ else v :: dfs_visit g v @ ds) nil (adjacent (op =) g u) in descendents end - + in u :: dfs_visit g u end; - -fun indexComps components = + +fun indexComps components = ListPair.map (fn (a,b) => (a,b)) (0 upto (length components -1), components); -fun indexNodes IndexComp = +fun indexNodes IndexComp = List.concat (map (fn (index, comp) => (map (fn v => (v,index)) comp)) IndexComp); - + fun getIndex v [] = ~1 -| getIndex v ((v',k)::vs) = if v aconv v' then k else getIndex v vs; - +| getIndex v ((v',k)::vs) = if v aconv v' then k else getIndex v vs; + (* *********************************************************************** *) (* *) (* dfs eq_comp g u v: *) (* ('a * 'a -> bool) -> ('a *( 'a * less) list) list -> *) -(* 'a -> 'a -> (bool * ('a * less) 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 eq_comp g u v = - let +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' = + + 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 () + + in if been_visited v then () else (app (fn (v',l) => if been_visited v' then () else ( - update (v',l); + 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 , []) + in + dfs_visit u; + if (been_visited v) then (true, (!pred)) else (false , []) end; - + (* *********************************************************************** *) (* *) (* completeTermPath u v g: *) -(* Term.term -> Term.term -> (Term.term * (Term.term * less) list) list *) +(* Term.term -> Term.term -> (Term.term * (Term.term * less) list) list *) (* -> less list *) (* *) (* Complete the path from u to v in graph g. Path search is performed *) @@ -793,36 +789,36 @@ (* *) (* *********************************************************************** *) - -fun completeTermPath u v g = - let + +fun completeTermPath u v g = + let val (found, tmp) = dfs (op aconv) g u v ; 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 = + (* 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] + else (rev_path u) @ [l] end in rev_path y end; - - in + + in if found then (if u aconv v then [(Le (u, v, (Thm ([], #le_refl less_thms))))] else path u v ) else raise Cannot -end; +end; - + (* *********************************************************************** *) (* *) (* findProof (sccGraph, neqE, ntc, sccSubgraphs) subgoal: *) @@ -834,133 +830,133 @@ (* proof for subgoal. Raises exception Cannot if this is not possible. *) (* *) (* *********************************************************************** *) - + fun findProof (sccGraph, neqE, ntc, sccSubgraphs) subgoal = let - + (* complete path x y from component graph *) - fun completeComponentPath x y predlist = - let - val xi = getIndex x ntc - val yi = getIndex y ntc - - fun lookup k [] = raise Cannot - | lookup k ((h: int,l)::us) = if k = h then l else lookup k us; - - fun rev_completeComponentPath y' = - let val edge = lookup (getIndex y' ntc) predlist - val u = lower edge - val v = upper edge - in - if (getIndex u ntc) = xi then - (completeTermPath x u (List.nth(sccSubgraphs, xi)) )@[edge] - @(completeTermPath v y' (List.nth(sccSubgraphs, getIndex y' ntc)) ) - else (rev_completeComponentPath u)@[edge] - @(completeTermPath v y' (List.nth(sccSubgraphs, getIndex y' ntc)) ) + fun completeComponentPath x y predlist = + let + val xi = getIndex x ntc + val yi = getIndex y ntc + + fun lookup k [] = raise Cannot + | lookup k ((h: int,l)::us) = if k = h then l else lookup k us; + + fun rev_completeComponentPath y' = + let val edge = lookup (getIndex y' ntc) predlist + val u = lower edge + val v = upper edge + in + if (getIndex u ntc) = xi then + (completeTermPath x u (List.nth(sccSubgraphs, xi)) )@[edge] + @(completeTermPath v y' (List.nth(sccSubgraphs, getIndex y' ntc)) ) + else (rev_completeComponentPath u)@[edge] + @(completeTermPath v y' (List.nth(sccSubgraphs, getIndex y' ntc)) ) end - in - if x aconv y then + in + if x aconv y then [(Le (x, y, (Thm ([], #le_refl less_thms))))] else ( if xi = yi then completeTermPath x y (List.nth(sccSubgraphs, xi)) - else rev_completeComponentPath y ) + else rev_completeComponentPath y ) end; -(* ******************************************************************* *) +(* ******************************************************************* *) (* findLess e x y xi yi xreachable yreachable *) (* *) (* Find a path from x through e to y, of weight < *) -(* ******************************************************************* *) - - fun findLess e x y xi yi xreachable yreachable = - let val u = lower e +(* ******************************************************************* *) + + 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 + + in + if ui mem xreachable andalso vi mem xreachable andalso ui mem yreachable andalso vi mem yreachable then ( - - (case e of (Less (_, _, _)) => + + (case e of (Less (_, _, _)) => let val (xufound, xupred) = dfs (op =) sccGraph xi (getIndex u ntc) - in - if xufound then ( - let - val (vyfound, vypred) = dfs (op =) sccGraph (getIndex v ntc) yi - in - if vyfound then ( - let - val xypath = (completeComponentPath x u xupred)@[e]@(completeComponentPath v y vypred) - val xyLesss = transPath (tl xypath, hd xypath) - in - if xyLesss subsumes subgoal then SOME (getprf xyLesss) + in + if xufound then ( + let + val (vyfound, vypred) = dfs (op =) sccGraph (getIndex v ntc) yi + in + if vyfound then ( + let + val xypath = (completeComponentPath x u xupred)@[e]@(completeComponentPath v y vypred) + val xyLesss = transPath (tl xypath, hd xypath) + in + if xyLesss subsumes subgoal then SOME (getprf xyLesss) else NONE - end) - else NONE - end) - else NONE - end - | _ => - let val (uvfound, uvpred) = dfs (op =) sccGraph (getIndex u ntc) (getIndex v ntc) - in - if uvfound then ( - let - val (xufound, xupred) = dfs (op =) sccGraph xi (getIndex u ntc) - in - if xufound then ( - let - val (vyfound, vypred) = dfs (op =) sccGraph (getIndex v ntc) yi - in - if vyfound then ( - let - val uvpath = completeComponentPath u v uvpred - val uvLesss = mergeLess ( transPath (tl uvpath, hd uvpath), e) - val xypath = (completeComponentPath x u xupred)@[uvLesss]@(completeComponentPath v y vypred) - val xyLesss = transPath (tl xypath, hd xypath) - in - if xyLesss subsumes subgoal then SOME (getprf xyLesss) + end) + else NONE + end) + else NONE + end + | _ => + let val (uvfound, uvpred) = dfs (op =) sccGraph (getIndex u ntc) (getIndex v ntc) + in + if uvfound then ( + let + val (xufound, xupred) = dfs (op =) sccGraph xi (getIndex u ntc) + in + if xufound then ( + let + val (vyfound, vypred) = dfs (op =) sccGraph (getIndex v ntc) yi + in + if vyfound then ( + let + val uvpath = completeComponentPath u v uvpred + val uvLesss = mergeLess ( transPath (tl uvpath, hd uvpath), e) + val xypath = (completeComponentPath x u xupred)@[uvLesss]@(completeComponentPath v y vypred) + val xyLesss = transPath (tl xypath, hd xypath) + in + if xyLesss subsumes subgoal then SOME (getprf xyLesss) else NONE - end ) - else NONE - end) - else NONE - end ) - else NONE - end ) + end ) + else NONE + end) + else NONE + end ) + else NONE + end ) ) else NONE -end; - - +end; + + in (* looking for x <= y: any path from x to y is sufficient *) case subgoal of (Le (x, y, _)) => ( - if null sccGraph then raise Cannot else ( - let + if null sccGraph then raise Cannot else ( + let val xi = getIndex x ntc val yi = getIndex y ntc (* searches in sccGraph a path from xi to yi *) val (found, pred) = dfs (op =) sccGraph xi yi - in + in if found then ( - let val xypath = completeComponentPath x y pred - val xyLesss = transPath (tl xypath, hd xypath) - in - (case xyLesss of - (Less (_, _, q)) => if xyLesss subsumes subgoal then (Thm ([q], #less_imp_le less_thms)) - else raise Cannot - | _ => if xyLesss subsumes subgoal then (getprf xyLesss) - else raise Cannot) + let val xypath = completeComponentPath x y pred + val xyLesss = transPath (tl xypath, hd xypath) + in + (case xyLesss of + (Less (_, _, q)) => if xyLesss subsumes subgoal then (Thm ([q], #less_imp_le less_thms)) + else raise Cannot + | _ => if xyLesss subsumes subgoal then (getprf xyLesss) + else raise Cannot) end ) - else raise Cannot - end + else raise Cannot + end ) ) (* looking for x < y: particular path required, which is not necessarily found by normal dfs *) | (Less (x, y, _)) => ( if null sccGraph then raise Cannot else ( - let + let val xi = getIndex x ntc val yi = getIndex y ntc val sccGraph_transpose = transpose (op =) sccGraph @@ -969,13 +965,13 @@ (* 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) = - case (findLess e x y xi yi xreachable yreachable) of (SOME prf) => prf + fun processNeqEdges [] = raise Cannot + | processNeqEdges (e::es) = + case (findLess e x y xi yi xreachable yreachable) of (SOME prf) => prf | _ => processNeqEdges es - - in - processNeqEdges neqE + + in + processNeqEdges neqE end ) ) @@ -986,99 +982,99 @@ else if null 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], #not_sym less_thms) - | ( SOME (Less (x, y, p)), NotEq (x', y', _)) => + if (x aconv x' andalso y aconv y') then p + else Thm ([p], #not_sym less_thms) + | ( SOME (Less (x, y, p)), NotEq (x', y', _)) => if x aconv x' andalso y aconv y' then (Thm ([p], #less_imp_neq less_thms)) else (Thm ([(Thm ([p], #less_imp_neq less_thms))], #not_sym less_thms)) - | _ => raise Cannot) + | _ => raise Cannot) ) else ( - - let val xi = getIndex x ntc + + let val xi = getIndex x ntc val yi = getIndex y ntc - val sccGraph_transpose = transpose (op =) sccGraph + 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) = ( - let val u = lower e - val v = upper e - val ui = getIndex u ntc - val vi = getIndex v ntc - - in - (* if x ~= y follows from edge e *) - if e subsumes subgoal then ( - case e of (Less (u, v, q)) => ( - if u aconv x andalso v aconv y then (Thm ([q], #less_imp_neq less_thms)) - else (Thm ([(Thm ([q], #less_imp_neq less_thms))], #not_sym less_thms)) - ) - | (NotEq (u,v, q)) => ( - if u aconv x andalso v aconv y then q - else (Thm ([q], #not_sym less_thms)) - ) - ) + val yreachable = dfs_int_reachable sccGraph_transpose yi + + fun processNeqEdges [] = raise Cannot + | processNeqEdges (e::es) = ( + let val u = lower e + val v = upper e + val ui = getIndex u ntc + val vi = getIndex v ntc + + in + (* if x ~= y follows from edge e *) + if e subsumes subgoal then ( + case e of (Less (u, v, q)) => ( + if u aconv x andalso v aconv y then (Thm ([q], #less_imp_neq less_thms)) + else (Thm ([(Thm ([q], #less_imp_neq less_thms))], #not_sym less_thms)) + ) + | (NotEq (u,v, q)) => ( + if u aconv x andalso v aconv y then q + else (Thm ([q], #not_sym less_thms)) + ) + ) (* if SCC_x is linked to SCC_y via edge e *) - else if ui = xi andalso vi = yi then ( + else if ui = xi andalso vi = yi then ( case e of (Less (_, _,_)) => ( - let val xypath = (completeTermPath x u (List.nth(sccSubgraphs, ui)) ) @ [e] @ (completeTermPath v y (List.nth(sccSubgraphs, vi)) ) - val xyLesss = transPath (tl xypath, hd xypath) - in (Thm ([getprf xyLesss], #less_imp_neq less_thms)) end) - | _ => ( - let - val xupath = completeTermPath x u (List.nth(sccSubgraphs, ui)) - val uxpath = completeTermPath u x (List.nth(sccSubgraphs, ui)) - val vypath = completeTermPath v y (List.nth(sccSubgraphs, vi)) - val yvpath = completeTermPath y v (List.nth(sccSubgraphs, vi)) - val xuLesss = transPath (tl xupath, hd xupath) - val uxLesss = transPath (tl uxpath, hd uxpath) - val vyLesss = transPath (tl vypath, hd vypath) - val yvLesss = transPath (tl yvpath, hd yvpath) - val x_eq_u = (Thm ([(getprf xuLesss),(getprf uxLesss)], #eqI less_thms)) - val v_eq_y = (Thm ([(getprf vyLesss),(getprf yvLesss)], #eqI less_thms)) - in - (Thm ([x_eq_u , (getprf e), v_eq_y ], #eq_neq_eq_imp_neq less_thms)) - end - ) - ) else if ui = yi andalso vi = xi then ( - case e of (Less (_, _,_)) => ( - let val xypath = (completeTermPath y u (List.nth(sccSubgraphs, ui)) ) @ [e] @ (completeTermPath v x (List.nth(sccSubgraphs, vi)) ) - val xyLesss = transPath (tl xypath, hd xypath) - in (Thm ([(Thm ([getprf xyLesss], #less_imp_neq less_thms))] , #not_sym less_thms)) end ) - | _ => ( - - let val yupath = completeTermPath y u (List.nth(sccSubgraphs, ui)) - val uypath = completeTermPath u y (List.nth(sccSubgraphs, ui)) - val vxpath = completeTermPath v x (List.nth(sccSubgraphs, vi)) - val xvpath = completeTermPath x v (List.nth(sccSubgraphs, vi)) - val yuLesss = transPath (tl yupath, hd yupath) - val uyLesss = transPath (tl uypath, hd uypath) - val vxLesss = transPath (tl vxpath, hd vxpath) - val xvLesss = transPath (tl xvpath, hd xvpath) - val y_eq_u = (Thm ([(getprf yuLesss),(getprf uyLesss)], #eqI less_thms)) - val v_eq_x = (Thm ([(getprf vxLesss),(getprf xvLesss)], #eqI less_thms)) - in - (Thm ([(Thm ([y_eq_u , (getprf e), v_eq_x ], #eq_neq_eq_imp_neq less_thms))], #not_sym less_thms)) - end - ) - ) else ( + let val xypath = (completeTermPath x u (List.nth(sccSubgraphs, ui)) ) @ [e] @ (completeTermPath v y (List.nth(sccSubgraphs, vi)) ) + val xyLesss = transPath (tl xypath, hd xypath) + in (Thm ([getprf xyLesss], #less_imp_neq less_thms)) end) + | _ => ( + let + val xupath = completeTermPath x u (List.nth(sccSubgraphs, ui)) + val uxpath = completeTermPath u x (List.nth(sccSubgraphs, ui)) + val vypath = completeTermPath v y (List.nth(sccSubgraphs, vi)) + val yvpath = completeTermPath y v (List.nth(sccSubgraphs, vi)) + val xuLesss = transPath (tl xupath, hd xupath) + val uxLesss = transPath (tl uxpath, hd uxpath) + val vyLesss = transPath (tl vypath, hd vypath) + val yvLesss = transPath (tl yvpath, hd yvpath) + val x_eq_u = (Thm ([(getprf xuLesss),(getprf uxLesss)], #eqI less_thms)) + val v_eq_y = (Thm ([(getprf vyLesss),(getprf yvLesss)], #eqI less_thms)) + in + (Thm ([x_eq_u , (getprf e), v_eq_y ], #eq_neq_eq_imp_neq less_thms)) + end + ) + ) else if ui = yi andalso vi = xi then ( + case e of (Less (_, _,_)) => ( + let val xypath = (completeTermPath y u (List.nth(sccSubgraphs, ui)) ) @ [e] @ (completeTermPath v x (List.nth(sccSubgraphs, vi)) ) + val xyLesss = transPath (tl xypath, hd xypath) + in (Thm ([(Thm ([getprf xyLesss], #less_imp_neq less_thms))] , #not_sym less_thms)) end ) + | _ => ( + + let val yupath = completeTermPath y u (List.nth(sccSubgraphs, ui)) + val uypath = completeTermPath u y (List.nth(sccSubgraphs, ui)) + val vxpath = completeTermPath v x (List.nth(sccSubgraphs, vi)) + val xvpath = completeTermPath x v (List.nth(sccSubgraphs, vi)) + val yuLesss = transPath (tl yupath, hd yupath) + val uyLesss = transPath (tl uypath, hd uypath) + val vxLesss = transPath (tl vxpath, hd vxpath) + val xvLesss = transPath (tl xvpath, hd xvpath) + val y_eq_u = (Thm ([(getprf yuLesss),(getprf uyLesss)], #eqI less_thms)) + val v_eq_x = (Thm ([(getprf vxLesss),(getprf xvLesss)], #eqI less_thms)) + in + (Thm ([(Thm ([y_eq_u , (getprf e), v_eq_x ], #eq_neq_eq_imp_neq less_thms))], #not_sym less_thms)) + end + ) + ) else ( (* there exists a path x < y or y < x such that x ~= y may be concluded *) - case (findLess e x y xi yi xreachable yreachable) of - (SOME prf) => (Thm ([prf], #less_imp_neq less_thms)) + case (findLess e x y xi yi xreachable yreachable) of + (SOME prf) => (Thm ([prf], #less_imp_neq less_thms)) | NONE => ( - let - 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_imp_neq less_thms))], #not_sym less_thms)) + let + 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_imp_neq less_thms))], #not_sym less_thms)) | _ => processNeqEdges es - end) - ) end) + end) + ) end) in processNeqEdges neqE end) - ) + ) end; @@ -1110,115 +1106,115 @@ (* ******************************************************************* *) fun mk_sccGraphs _ [] _ _ = ([],[]) -| mk_sccGraphs components leqG neqG ntc = +| mk_sccGraphs components leqG neqG ntc = let (* Liste (Index der Komponente, Komponente *) val IndexComp = indexComps components; - - fun handleContr edge g = - (case edge of + + fun handleContr edge g = + (case edge of (Less (x, y, _)) => ( - let - val xxpath = edge :: (completeTermPath y x g ) - val xxLesss = transPath (tl xxpath, hd xxpath) - val q = getprf xxLesss - in - raise (Contr (Thm ([q], #less_reflE less_thms ))) - end - ) + let + val xxpath = edge :: (completeTermPath y x g ) + val xxLesss = transPath (tl xxpath, hd xxpath) + val q = getprf xxLesss + in + raise (Contr (Thm ([q], #less_reflE less_thms ))) + end + ) | (NotEq (x, y, _)) => ( - let - 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 )) - in - raise (Contr (Thm ([q], #less_reflE less_thms ))) - end - ) - | _ => 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 *) + let + 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 )) + in + raise (Contr (Thm ([q], #less_reflE less_thms ))) + end + ) + | _ => 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 = List.concat (map (adjacent (op aconv) leqG) comp); - (* all edges with weight ~= of the actual component *) + (* all edges with weight ~= of the actual component *) val neqEdges = map snd (List.concat (map (adjacent (op aconv) neqG) comp)); - (* find an edge leading to a contradiction *) + (* 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 + | 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: int,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 + fun insert (h: int,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); - + 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 ([], []); + 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 + + 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; + | _ => ((k, (reOrganizeEdges (extern) [])), subGraph) + end; + + val tmp = map processComponent IndexComp +in + ( (map fst tmp), (map snd tmp)) +end; (** Find proof if possible. **) fun gen_solve mkconcl sign (asms, concl) = - let + let val (leqG, neqG, neqE) = mkGraphs asms - val components = scc_term leqG + val components = scc_term leqG val ntc = indexNodes (indexComps components) val (sccGraph, sccSubgraphs) = mk_sccGraphs components leqG neqG ntc in - let + let val (subgoals, prf) = mkconcl decomp less_thms sign concl fun solve facts less = (case triv_solv less of NONE => findProof (sccGraph, neqE, ntc, sccSubgraphs) less @@ -1229,24 +1225,25 @@ end; in - - SUBGOAL (fn (A, n, sign) => - let - val rfrees = map Free (Term.rename_wrt_term A (Logic.strip_params A)) - val Hs = map prop_of prems @ map (fn H => subst_bounds (rfrees, H)) (Logic.strip_assums_hyp A) - val C = subst_bounds (rfrees, Logic.strip_assums_concl A) - val lesss = List.concat (ListPair.map (mkasm decomp less_thms sign) (Hs, 0 upto (length Hs - 1))) - val prfs = gen_solve mkconcl sign (lesss, C); - val (subgoals, prf) = mkconcl decomp less_thms sign C; - in - METAHYPS (fn asms => - let val thms = map (prove (prems @ asms)) prfs - in rtac (prove thms prf) 1 end) n - end - handle Contr p => METAHYPS (fn asms => rtac (prove asms p) 1) n - | Cannot => no_tac - ) - + SUBGOAL (fn (A, n) => fn st => + let + val thy = ProofContext.theory_of ctxt; + val rfrees = map Free (Term.rename_wrt_term A (Logic.strip_params A)); + val Hs = map prop_of prems @ map (fn H => subst_bounds (rfrees, H)) (Logic.strip_assums_hyp A) + val C = subst_bounds (rfrees, Logic.strip_assums_concl A) + val lesss = List.concat (ListPair.map (mkasm decomp less_thms thy) (Hs, 0 upto (length Hs - 1))) + val prfs = gen_solve mkconcl thy (lesss, C); + val (subgoals, prf) = mkconcl decomp less_thms thy C; + in + FOCUS (fn {prems = asms, ...} => + let val thms = map (prove (prems @ asms)) prfs + in rtac (prove thms prf) 1 end) ctxt n st + end + handle Contr p => + (FOCUS (fn {prems = asms, ...} => rtac (prove asms p) 1) ctxt n st + handle Subscript => Seq.empty) + | Cannot => Seq.empty + | Subscript => Seq.empty) end; (* partial_tac - solves partial orders *) @@ -1255,5 +1252,4 @@ (* linear_tac - solves linear/total orders *) val linear_tac = gen_order_tac mkasm_linear mkconcl_linear; - end; diff -r 6a6827bad05f -r 87806301a813 src/Provers/quasi.ML --- a/src/Provers/quasi.ML Sun Jul 26 22:24:13 2009 +0200 +++ b/src/Provers/quasi.ML Sun Jul 26 22:28:31 2009 +0200 @@ -3,10 +3,10 @@ Reasoner for simple transitivity and quasi orders. *) -(* - +(* + The package provides tactics trans_tac and quasi_tac that use -premises of the form +premises of the form t = u, t ~= u, t < u and t <= u @@ -29,15 +29,15 @@ the assumptions. Note that the presence of a strict relation is not necessary for quasi_tac. Configure decomp_quasi to ignore < and ~=. A list of - required theorems for both situations is given below. + required theorems for both situations is given below. *) signature LESS_ARITH = sig (* Transitivity of <= - Note that transitivities for < hold for partial orders only. *) + Note that transitivities for < hold for partial orders only. *) val le_trans: thm (* [| x <= y; y <= z |] ==> x <= z *) - + (* Additional theorem for quasi orders *) val le_refl: thm (* x <= x *) val eqD1: thm (* x = y ==> x <= y *) @@ -64,41 +64,36 @@ val decomp_quasi: theory -> term -> (term * string * term) option end; -signature QUASI_TAC = +signature QUASI_TAC = sig - val trans_tac: int -> tactic - val quasi_tac: int -> tactic + val trans_tac: Proof.context -> int -> tactic + val quasi_tac: Proof.context -> int -> tactic end; -functor Quasi_Tac_Fun (Less: LESS_ARITH): QUASI_TAC = +functor Quasi_Tac(Less: LESS_ARITH): QUASI_TAC = struct -(* Extract subgoal with signature *) -fun SUBGOAL goalfun i st = - goalfun (List.nth(prems_of st, i-1), i, Thm.theory_of_thm st) st - handle Subscript => Seq.empty; - (* Internal datatype for the proof *) datatype proof - = Asm of int - | Thm of proof list * thm; - + = Asm of int + | Thm of proof list * thm; + exception Cannot; (* Internal exception, raised if conclusion cannot be derived from assumptions. *) exception Contr of proof; (* Internal exception, raised if contradiction ( x < x ) was derived *) -fun prove asms = +fun prove asms = let fun pr (Asm i) = List.nth (asms, i) | pr (Thm (prfs, thm)) = (map pr prfs) MRS thm in pr end; (* Internal datatype for inequalities *) -datatype less - = Less of term * term * proof +datatype less + = Less of term * term * proof | Le of term * term * proof - | NotEq of term * term * proof; + | NotEq of term * term * proof; (* Misc functions for datatype less *) fun lower (Less (x, _, _)) = x @@ -125,13 +120,13 @@ fun mkasm_trans sign (t, n) = case Less.decomp_trans sign t of - SOME (x, rel, y) => + SOME (x, rel, y) => (case rel of "<=" => [Le (x, y, Asm n)] | _ => error ("trans_tac: unknown relation symbol ``" ^ rel ^ "''returned by decomp_trans.")) | NONE => []; - + (* ************************************************************************ *) (* *) (* mkasm_quasi sign (t, n) : theory -> (Term.term * int) -> less *) @@ -145,15 +140,15 @@ fun mkasm_quasi sign (t, n) = case Less.decomp_quasi sign t of SOME (x, rel, y) => (case rel of - "<" => if (x aconv y) then raise Contr (Thm ([Asm n], Less.less_reflE)) + "<" => if (x aconv y) then raise Contr (Thm ([Asm n], Less.less_reflE)) else [Less (x, y, Asm n)] | "<=" => [Le (x, y, Asm n)] | "=" => [Le (x, y, Thm ([Asm n], Less.eqD1)), Le (y, x, Thm ([Asm n], Less.eqD2))] - | "~=" => if (x aconv y) then + | "~=" => 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"))] + NotEq (y, x,Thm ( [Asm n], thm "not_sym"))] | _ => error ("quasi_tac: unknown relation symbol ``" ^ rel ^ "''returned by decomp_quasi.")) | NONE => []; @@ -168,15 +163,15 @@ (* *) (* ************************************************************************ *) - + fun mkconcl_trans sign t = case Less.decomp_trans sign t of SOME (x, rel, y) => (case rel of - "<=" => (Le (x, y, Asm ~1), Asm 0) + "<=" => (Le (x, y, Asm ~1), Asm 0) | _ => raise Cannot) | NONE => raise Cannot; - - + + (* ************************************************************************ *) (* *) (* mkconcl_quasi sign t : theory -> Term.term -> less *) @@ -194,8 +189,8 @@ | "~=" => ([NotEq (x,y, Asm ~1)], Asm 0) | _ => raise Cannot) | NONE => raise Cannot; - - + + (* ******************************************************************* *) (* *) (* mergeLess (less1,less2): less * less -> less *) @@ -211,11 +206,11 @@ fun mergeLess (Le (x, _, p) , Le (_ , z, q)) = Le (x, z, Thm ([p,q] , Less.le_trans)) | mergeLess (Le (x, z, p) , NotEq (x', z', q)) = - if (x aconv x' andalso z aconv z' ) + if (x aconv x' andalso z aconv z' ) then Less (x, z, Thm ([p,q] , Less.le_neq_trans)) else error "quasi_tac: internal error le_neq_trans" | mergeLess (NotEq (x, z, p) , Le (x' , z', q)) = - if (x aconv x' andalso z aconv z') + if (x aconv x' andalso z aconv z') then Less (x, z, Thm ([p,q] , Less.neq_le_trans)) else error "quasi_tac: internal error neq_le_trans" | mergeLess (_, _) = @@ -229,7 +224,7 @@ infix tr; fun (Le (_, y, _)) tr (Le (x', _, _)) = ( y aconv x' ) | _ tr _ = false; - + (* ******************************************************************* *) (* *) (* transPath (Lesslist, Less): (less list * less) -> less *) @@ -245,7 +240,7 @@ | transPath (x::xs,lesss) = if lesss tr x then transPath (xs, mergeLess(lesss,x)) else error "trans/quasi_tac: internal error transpath"; - + (* ******************************************************************* *) (* *) (* less1 subsumes less2 : less -> less -> bool *) @@ -253,7 +248,7 @@ (* subsumes checks whether less1 implies less2 *) (* *) (* ******************************************************************* *) - + infix subsumes; fun (Le (x, y, _)) subsumes (Le (x', y', _)) = (x aconv x' andalso y aconv y') @@ -271,7 +266,7 @@ (* ******************************************************************* *) fun triv_solv (Le (x, x', _)) = - if x aconv x' then SOME (Thm ([], Less.le_refl)) + if x aconv x' then SOME (Thm ([], Less.le_refl)) else NONE | triv_solv _ = NONE; @@ -286,33 +281,33 @@ 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)); - + (* ********************************************************************** *) (* *) -(* mkQuasiGraph constructs from a list of objects of type less a graph g, *) +(* mkQuasiGraph 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 mkQuasiGraph [] = ([],[]) -| mkQuasiGraph lessList = +| mkQuasiGraph lessList = let fun buildGraphs ([],leG, neqE) = (leG, neqE) - | buildGraphs (l::ls, leG, neqE) = case l of + | buildGraphs (l::ls, leG, neqE) = case l of (Less (x,y,p)) => - let - val leEdge = Le (x,y, Thm ([p], Less.less_imp_le)) - val neqEdges = [ NotEq (x,y, Thm ([p], Less.less_imp_neq)), - NotEq (y,x, Thm ( [Thm ([p], Less.less_imp_neq)], thm "not_sym"))] - in - buildGraphs (ls, addEdge(y,[],(addEdge (x,[(y,leEdge)],leG))), neqEdges@neqE) - end - | (Le (x,y,p)) => buildGraphs (ls, addEdge(y,[],(addEdge (x,[(y,l)],leG))), neqE) + let + val leEdge = Le (x,y, Thm ([p], Less.less_imp_le)) + val neqEdges = [ NotEq (x,y, Thm ([p], Less.less_imp_neq)), + NotEq (y,x, Thm ( [Thm ([p], Less.less_imp_neq)], thm "not_sym"))] + in + buildGraphs (ls, addEdge(y,[],(addEdge (x,[(y,leEdge)],leG))), neqEdges@neqE) + end + | (Le (x,y,p)) => buildGraphs (ls, addEdge(y,[],(addEdge (x,[(y,l)],leG))), neqE) | _ => buildGraphs (ls, leG, l::neqE) ; in buildGraphs (lessList, [], []) end; - + (* ********************************************************************** *) (* *) (* mkGraph constructs from a list of objects of type less a graph g *) @@ -321,11 +316,11 @@ (* ********************************************************************** *) fun mkGraph [] = [] -| mkGraph lessList = +| mkGraph lessList = let fun buildGraph ([],g) = g - | buildGraph (l::ls, g) = buildGraph (ls, (addEdge ((lower l),[((upper l),l)],g))) - + | buildGraph (l::ls, g) = buildGraph (ls, (addEdge ((lower l),[((upper l),l)],g))) + in buildGraph (lessList, []) end; (* *********************************************************************** *) @@ -335,42 +330,42 @@ (* List of successors of u in graph g *) (* *) (* *********************************************************************** *) - -fun adjacent eq_comp ((v,adj)::el) u = + +fun adjacent eq_comp ((v,adj)::el) u = if eq_comp (u, v) then adj else adjacent eq_comp el u -| adjacent _ [] _ = [] +| adjacent _ [] _ = [] (* *********************************************************************** *) (* *) (* dfs eq_comp g u v: *) (* ('a * 'a -> bool) -> ('a *( 'a * less) list) list -> *) -(* 'a -> 'a -> (bool * ('a * less) 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 eq_comp g u v = - let +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' = + + 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 () + + in if been_visited v then () else (app (fn (v',l) => if been_visited v' then () else ( - update (v',l); + 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 , []) + in + dfs_visit u; + if (been_visited v) then (true, (!pred)) else (false , []) end; (* ************************************************************************ *) @@ -393,8 +388,8 @@ (* ************************************************************************ *) - fun findPath x y g = - let + fun findPath x y g = + let val (found, tmp) = dfs (op aconv) g x y ; val pred = map snd tmp; @@ -403,38 +398,38 @@ (* 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 + + (* 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 + if u aconv x then [l] else (rev_path u) @ [l] + end in rev_path y end; - - in + + in if found then ( if x aconv y then (found,[(Le (x, y, (Thm ([], Less.le_refl))))]) - else (found, (path x y) )) + else (found, (path x y) )) else (found,[]) - end; - - -(* ************************************************************************ *) + end; + + +(* ************************************************************************ *) (* *) (* findQuasiProof (leqG, neqE) subgoal: *) (* (Term.term * (Term.term * less list) list) * less list -> less -> proof *) (* *) (* Constructs a proof for subgoal by searching a special path in leqG and *) -(* neqE. Raises Cannot if construction of the proof fails. *) +(* neqE. Raises Cannot if construction of the proof fails. *) (* *) -(* ************************************************************************ *) +(* ************************************************************************ *) (* As the conlusion can be either of form x <= y, x < y or x ~= y we have *) (* three cases to deal with. Finding a transitivity path from x to y with label *) -(* 1. <= *) +(* 1. <= *) (* This is simply done by searching any path from x to y in the graph leG. *) (* The graph leG contains only edges with label <=. *) (* *) @@ -450,54 +445,54 @@ fun findQuasiProof (leG, neqE) subgoal = case subgoal of (Le (x,y, _)) => ( - let - val (xyLefound,xyLePath) = findPath x y leG + let + val (xyLefound,xyLePath) = findPath x y leG in if xyLefound then ( - let + let val Le_x_y = (transPath (tl xyLePath, hd xyLePath)) in getprf Le_x_y end ) else raise Cannot end ) | (Less (x,y,_)) => ( - let + let fun findParallelNeq [] = NONE | findParallelNeq (e::es) = if (x aconv (lower e) andalso y aconv (upper e)) then SOME e else if (y aconv (lower e) andalso x aconv (upper e)) then SOME (NotEq (x,y, (Thm ([getprf e], thm "not_sym")))) - else findParallelNeq es ; + else findParallelNeq es ; in (* test if there is a edge x ~= y respectivly y ~= x and *) (* if it possible to find a path x <= y in leG, thus we can conclude x < y *) - (case findParallelNeq neqE of (SOME e) => - let - val (xyLeFound,xyLePath) = findPath x y leG + (case findParallelNeq neqE of (SOME e) => + let + val (xyLeFound,xyLePath) = findPath x y leG in if xyLeFound then ( - let + let val Le_x_y = (transPath (tl xyLePath, hd xyLePath)) val Less_x_y = mergeLess (e, Le_x_y) in getprf Less_x_y end ) else raise Cannot - end - | _ => raise Cannot) + end + | _ => raise Cannot) end ) - | (NotEq (x,y,_)) => + | (NotEq (x,y,_)) => (* First check if a single premiss is sufficient *) (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 + if (x aconv x' andalso y aconv y') then p else Thm ([p], thm "not_sym") - | _ => raise Cannot + | _ => raise Cannot ) - -(* ************************************************************************ *) -(* *) -(* End: Quasi Order relevant functions *) -(* *) -(* *) -(* ************************************************************************ *) + +(* ************************************************************************ *) +(* *) +(* End: Quasi Order relevant functions *) +(* *) +(* *) +(* ************************************************************************ *) (* *********************************************************************** *) (* *) @@ -509,14 +504,14 @@ (* *********************************************************************** *) fun solveLeTrans sign (asms, concl) = - let + let val g = mkGraph asms in - let + let val (subgoal, prf) = mkconcl_trans sign concl - val (found, path) = findPath (lower subgoal) (upper subgoal) g + val (found, path) = findPath (lower subgoal) (upper subgoal) g in - if found then [getprf (transPath (tl path, hd path))] + if found then [getprf (transPath (tl path, hd path))] else raise Cannot end end; @@ -532,10 +527,10 @@ (* *********************************************************************** *) fun solveQuasiOrder sign (asms, concl) = - let + let val (leG, neqE) = mkQuasiGraph asms in - let + let val (subgoals, prf) = mkconcl_quasi sign concl fun solve facts less = (case triv_solv less of NONE => findQuasiProof (leG, neqE) less @@ -543,54 +538,56 @@ in map (solve asms) subgoals end end; -(* ************************************************************************ *) -(* *) +(* ************************************************************************ *) +(* *) (* Tactics *) (* *) -(* - trans_tac *) -(* - quasi_tac, solves quasi orders *) -(* ************************************************************************ *) +(* - trans_tac *) +(* - quasi_tac, solves quasi orders *) +(* ************************************************************************ *) (* trans_tac - solves transitivity chains over <= *) -val trans_tac = SUBGOAL (fn (A, n, sign) => + +fun trans_tac ctxt = SUBGOAL (fn (A, n) => let - val rfrees = map Free (Term.rename_wrt_term A (Logic.strip_params A)) - val Hs = map (fn H => subst_bounds (rfrees, H)) (Logic.strip_assums_hyp A) - val C = subst_bounds (rfrees, Logic.strip_assums_concl A) - val lesss = List.concat (ListPair.map (mkasm_trans sign) (Hs, 0 upto (length Hs - 1))) - val prfs = solveLeTrans sign (lesss, C); - - val (subgoal, prf) = mkconcl_trans sign C; + val thy = ProofContext.theory_of ctxt; + val rfrees = map Free (Term.rename_wrt_term A (Logic.strip_params A)); + val Hs = map (fn H => subst_bounds (rfrees, H)) (Logic.strip_assums_hyp A); + val C = subst_bounds (rfrees, Logic.strip_assums_concl A); + val lesss = List.concat (ListPair.map (mkasm_trans thy) (Hs, 0 upto (length Hs - 1))); + val prfs = solveLeTrans thy (lesss, C); + + val (subgoal, prf) = mkconcl_trans thy C; in - - METAHYPS (fn asms => - let val thms = map (prove asms) prfs - in rtac (prove thms prf) 1 end) n - + FOCUS (fn {prems, ...} => + let val thms = map (prove prems) prfs + in rtac (prove thms prf) 1 end) ctxt n end - handle Contr p => METAHYPS (fn asms => rtac (prove asms p) 1) n - | Cannot => no_tac -); + handle Contr p => FOCUS (fn {prems, ...} => rtac (prove prems p) 1) ctxt n + | Cannot => no_tac); + (* quasi_tac - solves quasi orders *) -val quasi_tac = SUBGOAL (fn (A, n, sign) => + +fun quasi_tac ctxt = SUBGOAL (fn (A, n) => fn st => let - val rfrees = map Free (Term.rename_wrt_term A (Logic.strip_params A)) - val Hs = map (fn H => subst_bounds (rfrees, H)) (Logic.strip_assums_hyp A) - val C = subst_bounds (rfrees, Logic.strip_assums_concl A) - val lesss = List.concat (ListPair.map (mkasm_quasi sign) (Hs, 0 upto (length Hs - 1))) - val prfs = solveQuasiOrder sign (lesss, C); - val (subgoals, prf) = mkconcl_quasi sign C; + val thy = ProofContext.theory_of ctxt; + val rfrees = map Free (Term.rename_wrt_term A (Logic.strip_params A)); + val Hs = map (fn H => subst_bounds (rfrees, H)) (Logic.strip_assums_hyp A); + val C = subst_bounds (rfrees, Logic.strip_assums_concl A); + val lesss = flat (ListPair.map (mkasm_quasi thy) (Hs, 0 upto (length Hs - 1))); + val prfs = solveQuasiOrder thy (lesss, C); + val (subgoals, prf) = mkconcl_quasi thy C; in - - METAHYPS (fn asms => - let val thms = map (prove asms) prfs - in rtac (prove thms prf) 1 end) n - + FOCUS (fn {prems, ...} => + let val thms = map (prove prems) prfs + in rtac (prove thms prf) 1 end) ctxt n st end - handle Contr p => METAHYPS (fn asms => rtac (prove asms p) 1) n - | Cannot => no_tac -); - + handle Contr p => + (FOCUS (fn {prems, ...} => rtac (prove prems p) 1) ctxt n st + handle Subscript => Seq.empty) + | Cannot => Seq.empty + | Subscript => Seq.empty); + end; diff -r 6a6827bad05f -r 87806301a813 src/Provers/trancl.ML --- a/src/Provers/trancl.ML Sun Jul 26 22:24:13 2009 +0200 +++ b/src/Provers/trancl.ML Sun Jul 26 22:28:31 2009 +0200 @@ -26,7 +26,7 @@ *) -signature TRANCL_ARITH = +signature TRANCL_ARITH = sig (* theorems for transitive closure *) @@ -63,25 +63,25 @@ "r": the relation itself, "r^+": transitive closure of the relation, "r^*": reflexive-transitive closure of the relation - *) + *) - val decomp: term -> (term * term * term * string) option + val decomp: term -> (term * term * term * string) option end; -signature TRANCL_TAC = +signature TRANCL_TAC = sig - val trancl_tac: int -> tactic; - val rtrancl_tac: int -> tactic; + val trancl_tac: Proof.context -> int -> tactic + val rtrancl_tac: Proof.context -> int -> tactic end; -functor Trancl_Tac_Fun (Cls : TRANCL_ARITH): TRANCL_TAC = +functor Trancl_Tac(Cls: TRANCL_ARITH): TRANCL_TAC = struct - + datatype proof - = Asm of int - | Thm of proof list * thm; + = Asm of int + | Thm of proof list * thm; exception Cannot; (* internal exception: raised if no proof can be found *) @@ -89,7 +89,7 @@ (Envir.beta_eta_contract x, Envir.beta_eta_contract y, Envir.beta_eta_contract rel, r)) (Cls.decomp t); -fun prove thy r asms = +fun prove thy r asms = let fun inst thm = let val SOME (_, _, r', _) = decomp (concl_of thm) @@ -98,12 +98,12 @@ | pr (Thm (prfs, thm)) = map pr prfs MRS inst thm in pr end; - + (* Internal datatype for inequalities *) -datatype rel +datatype rel = Trans of term * term * proof (* R^+ *) | RTrans of term * term * proof; (* R^* *) - + (* Misc functions for datatype rel *) fun lower (Trans (x, _, _)) = x | lower (RTrans (x,_,_)) = x; @@ -112,8 +112,8 @@ | upper (RTrans (_,y,_)) = y; fun getprf (Trans (_, _, p)) = p -| getprf (RTrans (_,_, p)) = p; - +| getprf (RTrans (_,_, p)) = p; + (* ************************************************************************ *) (* *) (* mkasm_trancl Rel (t,n): term -> (term , int) -> rel list *) @@ -127,16 +127,16 @@ fun mkasm_trancl Rel (t, n) = case decomp t of - SOME (x, y, rel,r) => if rel aconv Rel then - + 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 [] + else [] | NONE => []; - + (* ************************************************************************ *) (* *) (* mkasm_rtrancl Rel (t,n): term -> (term , int) -> rel list *) @@ -156,7 +156,7 @@ | "r+" => [ Trans (x,y, Asm n)] | "r*" => [ RTrans(x,y, Asm n)] | _ => error ("rtrancl_tac: unknown relation symbol" )) - else [] + else [] | NONE => []; (* ************************************************************************ *) @@ -204,7 +204,7 @@ 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 (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)); (* ******************************************************************* *) @@ -220,7 +220,7 @@ fun transPath ([],acc) = acc | transPath (x::xs,acc) = transPath (xs, makeStep(acc,x)) - + (* ********************************************************************* *) (* Graph functions *) (* ********************************************************************* *) @@ -232,7 +232,7 @@ 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 *) @@ -241,13 +241,13 @@ (* ********************************************************************** *) fun mkGraph [] = ([],[]) -| mkGraph ys = +| 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) + | 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; (* *********************************************************************** *) @@ -257,42 +257,42 @@ (* List of successors of u in graph g *) (* *) (* *********************************************************************** *) - -fun adjacent eq_comp ((v,adj)::el) u = + +fun adjacent eq_comp ((v,adj)::el) u = if eq_comp (u, v) then adj else adjacent eq_comp el u -| adjacent _ [] _ = [] +| adjacent _ [] _ = [] (* *********************************************************************** *) (* *) (* dfs eq_comp g u v: *) (* ('a * 'a -> bool) -> ('a *( 'a * rel) list) list -> *) -(* 'a -> 'a -> (bool * ('a * rel) 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 +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' = + + 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 () + + in if been_visited v then () else (app (fn (v',l) => if been_visited v' then () else ( - update (v',l); + 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 , []) + in + dfs_visit u; + if (been_visited v) then (true, (!pred)) else (false , []) end; (* *********************************************************************** *) @@ -310,7 +310,7 @@ (* 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. *) @@ -334,23 +334,23 @@ (* Compute, for each adjacency list, the list with reversed edges, and concatenate these lists. *) val flipped = List.foldr (op @) nil (map flip g) - - in assemble g flipped end - + + in assemble g flipped end + (* *********************************************************************** *) (* *) (* dfs_reachable eq_comp g u: *) -(* (int * int list) list -> int -> int list *) +(* (int * int list) list -> int -> int list *) (* *) (* Computes list of all nodes reachable from u in g. *) (* *) (* *********************************************************************** *) -fun dfs_reachable eq_comp g u = +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 = @@ -361,13 +361,13 @@ else v :: dfs_visit g v @ ds) nil (adjacent eq_comp g u) in descendents end - + in u :: dfs_visit g u end; (* *********************************************************************** *) (* *) (* dfs_term_reachable g u: *) -(* (term * term list) list -> term -> term list *) +(* (term * term list) list -> term -> term list *) (* *) (* Computes list of all nodes reachable from u in g. *) (* *) @@ -375,45 +375,45 @@ 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) -> *) +(* (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 if path is found, otherwise false and nil. *) (* *) -(* ************************************************************************ *) - -fun findPath x y g = - let +(* ************************************************************************ *) + +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 *) - + (* 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 - + + (* 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 + + in + - if found then ( (found, (path x y) )) else (found,[]) - - + + end; @@ -426,143 +426,142 @@ (* *) (* ************************************************************************ *) -fun findRtranclProof g tranclEdges subgoal = +fun findRtranclProof g tranclEdges subgoal = 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 + 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 + 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) = + | 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 + 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 ( - 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; + 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) = + +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 + else raise Cannot end end; - -fun solveRtrancl (asms, concl) = + +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) => fn st => + + +fun trancl_tac ctxt = SUBGOAL (fn (A, n) => let - val thy = theory_of_thm st; + val thy = ProofContext.theory_of ctxt; val Hs = Logic.strip_assums_hyp A; val C = Logic.strip_assums_concl A; - val (rel,subgoals, prf) = mkconcl_trancl C; - val prems = List.concat (ListPair.map (mkasm_trancl rel) (Hs, 0 upto (length Hs - 1))) + 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 thy rel asms) prfs - in rtac (prove thy rel thms prf) 1 end) n st + FOCUS (fn {prems, ...} => + let val thms = map (prove thy rel prems) prfs + in rtac (prove thy rel thms prf) 1 end) ctxt n end -handle Cannot => no_tac st); + handle Cannot => no_tac); - - -val rtrancl_tac = SUBGOAL (fn (A, n) => fn st => + +fun rtrancl_tac ctxt = SUBGOAL (fn (A, n) => fn st => let - val thy = theory_of_thm st; + val thy = ProofContext.theory_of ctxt; val Hs = Logic.strip_assums_hyp A; val C = Logic.strip_assums_concl A; - val (rel,subgoals, prf) = mkconcl_rtrancl C; + val (rel, subgoals, prf) = mkconcl_rtrancl C; - val prems = List.concat (ListPair.map (mkasm_rtrancl rel) (Hs, 0 upto (length Hs - 1))) + 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 thy rel asms) prfs - in rtac (prove thy rel thms prf) 1 end) n st + FOCUS (fn {prems, ...} => + let val thms = map (prove thy rel prems) prfs + in rtac (prove thy rel thms prf) 1 end) ctxt n st end -handle Cannot => no_tac st); + handle Cannot => Seq.empty | Subscript => Seq.empty); end;