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?);
--- 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 [
--- 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
--- 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;
--- 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;
--- 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;