--- a/src/Provers/linorder.ML Thu Feb 19 10:41:32 2004 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,214 +0,0 @@
-(*
- Title: Transitivity reasoner for linear orders
- Id: $Id$
- Author: Clemens Ballarin, started 8 November 2002
- Copyright: TU Muenchen
-*)
-
-(***
-This is a very simple package for transitivity reasoning over linear orders.
-Simple means exponential time (and space) in the number of premises.
-Should be replaced by a graph-theoretic algorithm.
-
-The package provides a tactic trans_tac that uses all premises of the form
-
- t = u, t < u, t <= u, ~(t < u) and ~(t <= u)
-
-to
-1. either derive a contradiction,
- in which case the conclusion can be any term,
-2. or prove the conclusion, which must be of the same form as the premises.
-
-To get rid of ~= in the premises, it is advisable to use an elimination
-rule of the form
-
- [| t ~= u; t < u ==> P; u < t ==> P |] ==> P.
-
-The package is implemented as an ML functor and thus not limited to the
-relation <= and friends. It can be instantiated to any total order ---
-for example, the divisibility relation "dvd".
-***)
-
-(*** Credits ***
-
-This package is closely based on a (no longer used) transitivity reasoner for
-the natural numbers, which was written by Tobias Nipkow.
-
-****************)
-
-signature LESS_ARITH =
-sig
- val less_reflE: thm (* x < x ==> P *)
- val le_refl: thm (* x <= x *)
- val less_imp_le: thm (* x < y ==> x <= y *)
- val not_lessI: thm (* y <= x ==> ~(x < y) *)
- val not_leI: thm (* y < x ==> ~(x <= y) *)
- val not_lessD: thm (* ~(x < y) ==> y <= x *)
- val not_leD: thm (* ~(x <= y) ==> y < x *)
- val eqI: thm (* [| x <= y; y <= x |] ==> x = y *)
- val eqD1: thm (* x = y ==> x <= y *)
- val eqD2: thm (* x = y ==> y <= x *)
- val less_trans: thm (* [| x <= y; y <= z |] ==> x <= z *)
- val less_le_trans: thm (* [| x <= y; y < z |] ==> x < z *)
- val le_less_trans: thm (* [| x < y; y <= z |] ==> x < z *)
- val le_trans: thm (* [| x < y; y < z |] ==> x < z *)
- val decomp: term -> (term * string * term) option
- (* decomp (`x Rel y') should yield (x, Rel, y)
- where Rel is one of "<", "<=", "~<", "~<=", "=" and "~="
- other relation symbols are ignored *)
-end;
-
-signature TRANS_TAC =
-sig
- val trans_tac: int -> tactic
-end;
-
-functor Trans_Tac_Fun (Less: LESS_ARITH): TRANS_TAC =
-struct
-
-(*** Proof objects ***)
-
-datatype proof
- = Asm of int
- | Thm of proof list * thm;
-
-(* Turn proof objects into theorems *)
-
-fun prove asms =
- let fun pr (Asm i) = nth_elem (i, asms)
- | pr (Thm (prfs, thm)) = (map pr prfs) MRS thm
- in pr end;
-
-(*** Exceptions ***)
-
-exception Contr of proof; (* Raised when contradiction is found *)
-
-exception Cannot; (* Raised when goal cannot be proved *)
-
-(*** Internal representation of inequalities ***)
-
-datatype less
- = Less of term * term * proof
- | Le of term * term * proof;
-
-fun lower (Less (x, _, _)) = x
- | lower (Le (x, _, _)) = x;
-
-fun upper (Less (_, y, _)) = y
- | upper (Le (_, y, _)) = y;
-
-infix subsumes;
-
-fun (Less (x, y, _)) subsumes (Le (x', y', _)) = (x = x' andalso y = y')
- | (Less (x, y, _)) subsumes (Less (x', y', _)) = (x = x' andalso y = y')
- | (Le (x, y, _)) subsumes (Le (x', y', _)) = (x = x' andalso y = y')
- | _ subsumes _ = false;
-
-fun trivial (Le (x, x', _)) = (x = x')
- | trivial _ = false;
-
-(*** Transitive closure ***)
-
-fun add new =
- let fun adds([], news) = new::news
- | adds(old::olds, news) = if new subsumes old then adds(olds, news)
- else adds(olds, old::news)
- in adds end;
-
-fun ctest (less as Less (x, x', p)) =
- if x = x' then raise Contr (Thm ([p], Less.less_reflE))
- else less
- | ctest less = less;
-
-fun mktrans (Less (x, _, p), Less (_, z, q)) =
- Less (x, z, Thm([p, q], Less.less_trans))
- | mktrans (Less (x, _, p), Le (_, z, q)) =
- Less (x, z, Thm([p, q], Less.less_le_trans))
- | mktrans (Le (x, _, p), Less (_, z, q)) =
- Less (x, z, Thm([p, q], Less.le_less_trans))
- | mktrans (Le (x, _, p), Le (_, z, q)) =
- Le (x, z, Thm([p, q], Less.le_trans));
-
-fun trans new olds =
- let fun tr (news, old) =
- if upper old = lower new then mktrans (old, new)::news
- else if upper new = lower old then mktrans (new, old)::news
- else news
- in foldl tr ([], olds) end;
-
-fun close1 olds new =
- if trivial new orelse exists (fn old => old subsumes new) olds then olds
- else let val news = trans new olds
- in close (add new (olds, [])) news end
-and close olds [] = olds
- | close olds (new::news) = close (close1 olds (ctest new)) news;
-
-(*** Solving and proving goals ***)
-
-(* Recognise and solve trivial goal *)
-
-fun triv_sol (Le (x, x', _)) =
- if x = x' then Some (Thm ([], Less.le_refl))
- else None
- | triv_sol _ = None;
-
-(* Solve less starting from facts *)
-
-fun solve facts less =
- case triv_sol less of
- None => (case (Library.find_first (fn fact => fact subsumes less) facts, less) of
- (None, _) => raise Cannot
- | (Some (Less (_, _, p)), Less _) => p
- | (Some (Le (_, _, p)), Less _) =>
- error "trans_tac/solve: internal error: le cannot subsume less"
- | (Some (Less (_, _, p)), Le _) => Thm ([p], Less.less_imp_le)
- | (Some (Le (_, _, p)), Le _) => p)
- | Some prf => prf;
-
-(* Turn term t into Less or Le; n is position of t in list of assumptions *)
-
-fun mkasm (t, n) =
- case Less.decomp t of
- Some (x, rel, y) => (case rel of
- "<" => [Less (x, y, Asm n)]
- | "~<" => [Le (y, x, Thm ([Asm n], Less.not_lessD))]
- | "<=" => [Le (x, y, Asm n)]
- | "~<=" => [Less (y, x, Thm ([Asm n], Less.not_leD))]
- | "=" => [Le (x, y, Thm ([Asm n], Less.eqD1)),
- Le (x, y, Thm ([Asm n], Less.eqD1))]
- | "~=" => []
- | _ => error ("trans_tac/mkasm: unknown relation " ^ rel))
- | None => [];
-
-(* Turn goal t into a pair (goals, proof) where goals is a list of
- Le/Less-subgoals to solve, and proof the validation that proves the concl t
- Asm ~1 is dummy (denotes a goal)
-*)
-
-fun mkconcl t =
- case Less.decomp t of
- Some (x, rel, y) => (case rel of
- "<" => ([Less (x, y, Asm ~1)], Asm 0)
- | "~<" => ([Le (y, x, Asm ~1)], Thm ([Asm 0], Less.not_lessI))
- | "<=" => ([Le (x, y, Asm ~1)], Asm 0)
- | "~<=" => ([Less (y, x, Asm ~1)], Thm ([Asm 0], Less.not_leI))
- | "=" => ([Le (x, y, Asm ~1), Le (y, x, Asm ~1)],
- Thm ([Asm 0, Asm 1], Less.eqI))
- | _ => raise Cannot)
- | None => raise Cannot;
-
-val trans_tac = SUBGOAL (fn (A, n) =>
- let val Hs = Logic.strip_assums_hyp A
- val C = Logic.strip_assums_concl A
- val lesss = flat (ListPair.map mkasm (Hs, 0 upto (length Hs - 1)))
- val clesss = close [] lesss
- val (subgoals, prf) = mkconcl C
- val prfs = map (solve clesss) subgoals
- in METAHYPS (fn asms =>
- let val thms = map (prove 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);
-
-end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Provers/order.ML Thu Feb 19 15:57:34 2004 +0100
@@ -0,0 +1,1207 @@
+(*
+ Title: Transitivity reasoner for partial and linear orders
+ Id: $Id$
+ Author: Oliver Kutter
+ Copyright: TU Muenchen
+*)
+
+(* TODO: reduce number of input thms, reduce code duplication *)
+
+(*
+
+The packages provides tactics partial_tac and linear_tac that use all
+premises of the form
+
+ t = u, t ~= u, t < u, t <= u, ~(t < u) and ~(t <= u)
+
+to
+1. either derive a contradiction,
+ in which case the conclusion can be any term,
+2. or prove the conclusion, which must be of the same form as the
+ premises (excluding ~(t < u) and ~(t <= u) for partial orders)
+
+The package is implemented as an ML functor and thus not limited to the
+relation <= and friends. It can be instantiated to any partial and/or
+linear order --- for example, the divisibility relation "dvd". In
+order to instantiate the package for a partial order only, supply
+dummy theorems to the rules for linear orders, and don't use
+linear_tac!
+
+*)
+
+signature LESS_ARITH =
+sig
+ (* Theorems for partial orders *)
+ val less_reflE: thm (* x < x ==> P *)
+ val le_refl: thm (* x <= x *)
+ val less_imp_le: thm (* x < y ==> x <= y *)
+ val eqI: thm (* [| x <= y; y <= x |] ==> x = y *)
+ val eqD1: thm (* x = y ==> x <= y *)
+ val eqD2: thm (* x = y ==> y <= x *)
+ val less_trans: thm (* [| x <= y; y <= z |] ==> x <= z *)
+ val less_le_trans: thm (* [| x <= y; y < z |] ==> x < z *)
+ val le_less_trans: thm (* [| x < y; y <= z |] ==> x < z *)
+ val le_trans: thm (* [| x < y; y < z |] ==> x < z *)
+ val le_neq_trans : thm (* [| x <= y ; x ~= y |] ==> x < y *)
+ val neq_le_trans : thm (* [| x ~= y ; x <= y |] ==> x < y *)
+
+ (* Additional theorems for linear orders *)
+ val not_lessD: thm (* ~(x < y) ==> y <= x *)
+ val not_leD: thm (* ~(x <= y) ==> y < x *)
+ val not_lessI: thm (* y <= x ==> ~(x < y) *)
+ val not_leI: thm (* y < x ==> ~(x <= y) *)
+
+ (* Additional theorems for subgoals of form x ~= y *)
+ val less_imp_neq : thm (* x < y ==> x ~= y *)
+ val eq_neq_eq_imp_neq : thm (* [| x = u ; u ~= v ; v = z|] ==> x ~= z *)
+
+ (* Analysis of premises and conclusion *)
+ (* decomp_x (`x Rel y') should yield (x, Rel, y)
+ where Rel is one of "<", "<=", "~<", "~<=", "=" and "~=",
+ other relation symbols cause an error message *)
+ val decomp_part: Sign.sg -> term -> (term * string * term) option
+ val decomp_lin: Sign.sg -> term -> (term * string * term) option
+end;
+
+signature TRANS_TAC =
+sig
+ val partial_tac: int -> tactic
+ val linear_tac: int -> tactic
+end;
+
+functor Trans_Tac_Fun (Less: LESS_ARITH): TRANS_TAC =
+struct
+
+(* Extract subgoal with signature *)
+
+fun SUBGOAL goalfun i st =
+ goalfun (List.nth(prems_of st, i-1), i, sign_of_thm st) st
+ handle Subscript => Seq.empty;
+
+(* Internal datatype for the proof *)
+datatype proof
+ = 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 =
+ let fun pr (Asm i) = nth_elem (i, asms)
+ | pr (Thm (prfs, thm)) = (map pr prfs) MRS thm
+ in pr end;
+
+(* Internal datatype for inequalities *)
+datatype less
+ = Less of term * term * proof
+ | Le of term * term * proof
+ | NotEq of term * term * proof;
+
+
+(* Misc functions for datatype less *)
+fun lower (Less (x, _, _)) = x
+ | lower (Le (x, _, _)) = x
+ | lower (NotEq (x,_,_)) = x;
+
+fun upper (Less (_, y, _)) = y
+ | upper (Le (_, y, _)) = y
+ | upper (NotEq (_,y,_)) = y;
+
+fun getprf (Less (_, _, p)) = p
+| getprf (Le (_, _, p)) = p
+| getprf (NotEq (_,_, p)) = p;
+
+
+(* ************************************************************************ *)
+(* *)
+(* mkasm_partial sign (t, n) : Sign.sg -> (Term.term * int) -> less *)
+(* *)
+(* Tuple (t, n) (t an assumption, n its index in the assumptions) is *)
+(* translated to an element of type less. *)
+(* Partial orders only. *)
+(* *)
+(* ************************************************************************ *)
+
+fun mkasm_partial sign (t, n) =
+ case Less.decomp_part sign t of
+ Some (x, rel, y) => (case rel of
+ "<" => 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
+ raise Contr (Thm ([(Thm ([(Thm ([], Less.le_refl)) ,(Asm n)], Less.le_neq_trans))], Less.less_reflE))
+ else [ NotEq (x, y, Asm n),
+ NotEq (y, x,Thm ( [Asm n], thm "not_sym"))] (* Le (x, x, Thm ([],Less.le_refl))]*)
+ | _ => error ("partial_tac: unknown relation symbol ``" ^ rel ^
+ "''returned by decomp_part."))
+ | None => [];
+
+
+
+(* ************************************************************************ *)
+(* *)
+(* mkasm_linear sign (t, n) : Sign.sg -> (Term.term * int) -> less *)
+(* *)
+(* Tuple (t, n) (t an assumption, n its index in the assumptions) is *)
+(* translated to an element of type less. *)
+(* Linear orders only. *)
+(* *)
+(* ************************************************************************ *)
+
+fun mkasm_linear sign (t, n) =
+ case Less.decomp_lin sign t of
+ Some (x, rel, y) => (case rel of
+ "<" => if (x aconv y) then raise Contr (Thm ([Asm n], Less.less_reflE))
+ else [Less (x, y, Asm n)]
+ | "~<" => [Le (y, x, Thm ([Asm n], Less.not_lessD))]
+ | "<=" => [Le (x, y, Asm n)]
+ | "~<=" => if (x aconv y) then
+ raise (Contr (Thm ([Thm ([Asm n], Less.not_leD)], Less.less_reflE)))
+ else [Less (y, x, Thm ([Asm n], Less.not_leD))]
+ | "=" => [Le (x, y, Thm ([Asm n], Less.eqD1)),
+ Le (y, x, Thm ([Asm n], Less.eqD2))]
+ | "~=" => 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"))]
+ | _ => error ("linear_tac: unknown relation symbol ``" ^ rel ^
+ "''returned by decomp_lin."))
+ | None => [];
+
+
+(* ************************************************************************ *)
+(* *)
+(* mkconcl_partial sign t : Sign.sg -> Term.term -> less *)
+(* *)
+(* Translates conclusion t to an element of type less. *)
+(* Partial orders only. *)
+(* *)
+(* ************************************************************************ *)
+
+fun mkconcl_partial sign t =
+ case Less.decomp_part sign t of
+ Some (x, rel, y) => (case rel of
+ "<" => ([Less (x, y, Asm ~1)], Asm 0)
+ | "<=" => ([Le (x, y, Asm ~1)], Asm 0)
+ | "=" => ([Le (x, y, Asm ~1), Le (y, x, Asm ~1)],
+ Thm ([Asm 0, Asm 1], Less.eqI))
+ | "~=" => ([NotEq (x,y, Asm ~1)], Asm 0)
+ | _ => raise Cannot)
+ | None => raise Cannot;
+
+
+(* ************************************************************************ *)
+(* *)
+(* mkconcl_linear sign t : Sign.sg -> Term.term -> less *)
+(* *)
+(* Translates conclusion t to an element of type less. *)
+(* Linear orders only. *)
+(* *)
+(* ************************************************************************ *)
+
+fun mkconcl_linear sign t =
+ case Less.decomp_lin sign t of
+ Some (x, rel, y) => (case rel of
+ "<" => ([Less (x, y, Asm ~1)], Asm 0)
+ | "~<" => ([Le (y, x, Asm ~1)], Thm ([Asm 0], Less.not_lessI))
+ | "<=" => ([Le (x, y, Asm ~1)], Asm 0)
+ | "~<=" => ([Less (y, x, Asm ~1)], Thm ([Asm 0], Less.not_leI))
+ | "=" => ([Le (x, y, Asm ~1), Le (y, x, Asm ~1)],
+ Thm ([Asm 0, Asm 1], Less.eqI))
+ | "~=" => ([NotEq (x,y, Asm ~1)], Asm 0)
+ | _ => raise Cannot)
+ | None => raise Cannot;
+
+
+
+(* ******************************************************************* *)
+(* *)
+(* mergeLess (less1,less2): less * less -> less *)
+(* *)
+(* Merge to elements of type less according to the following rules *)
+(* *)
+(* x < y && y < z ==> x < z *)
+(* x < y && y <= z ==> x < z *)
+(* x <= y && y < z ==> x < z *)
+(* x <= y && y <= z ==> x <= z *)
+(* x <= y && x ~= y ==> x < y *)
+(* x ~= y && x <= y ==> x < y *)
+(* x < y && x ~= y ==> x < y *)
+(* x ~= y && x < y ==> x < y *)
+(* *)
+(* ******************************************************************* *)
+
+fun mergeLess (Less (x, _, p) , Less (_ , z, q)) =
+ Less (x, z, Thm ([p,q] , Less.less_trans))
+| mergeLess (Less (x, _, p) , Le (_ , z, q)) =
+ Less (x, z, Thm ([p,q] , Less.less_le_trans))
+| mergeLess (Le (x, _, p) , Less (_ , z, q)) =
+ Less (x, z, Thm ([p,q] , Less.le_less_trans))
+| mergeLess (Le (x, z, p) , NotEq (x', z', q)) =
+ if (x aconv x' andalso z aconv z' )
+ then Less (x, z, Thm ([p,q] , Less.le_neq_trans))
+ 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')
+ then Less (x, z, Thm ([p,q] , Less.neq_le_trans))
+ 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')
+ 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')
+ then Less (x, z, p)
+ else error "linear/partial_tac: internal error less_neq_trans"
+| mergeLess (Le (x, _, p) , Le (_ , z, q)) =
+ Le (x, z, Thm ([p,q] , Less.le_trans))
+| mergeLess (_, _) =
+ error "linear/partial_tac: internal error: undefined case";
+
+
+(* ******************************************************************** *)
+(* tr checks for valid transitivity step *)
+(* ******************************************************************** *)
+
+infix tr;
+fun (Less (_, y, _)) tr (Le (x', _, _)) = ( y aconv x' )
+ | (Le (_, y, _)) tr (Less (x', _, _)) = ( y aconv x' )
+ | (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 *)
+(* *)
+(* If a path represented by a list of elements of type less is found, *)
+(* this needs to be contracted to a single element of type less. *)
+(* Prior to each transitivity step it is checked whether the step is *)
+(* valid. *)
+(* *)
+(* ******************************************************************* *)
+
+fun transPath ([],lesss) = lesss
+| 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 *)
+(* *)
+(* subsumes checks whether less1 implies less2 *)
+(* *)
+(* ******************************************************************* *)
+
+infix subsumes;
+fun (Less (x, y, _)) subsumes (Le (x', y', _)) =
+ (x aconv x' andalso y aconv y')
+ | (Less (x, y, _)) subsumes (Less (x', y', _)) =
+ (x aconv x' andalso y aconv y')
+ | (Le (x, y, _)) subsumes (Le (x', y', _)) =
+ (x aconv x' andalso y aconv y')
+ | (Less (x, y, _)) subsumes (NotEq (x', y', _)) =
+ (x aconv x' andalso y aconv y') orelse (y aconv x' andalso x aconv y')
+ | (NotEq (x, y, _)) subsumes (NotEq (x', y', _)) =
+ (x aconv x' andalso y aconv y') orelse (y aconv x' andalso x aconv y')
+ | (Le _) subsumes (Less _) =
+ error "linear/partial_tac: internal error: Le cannot subsume Less"
+ | _ subsumes _ = false;
+
+(* ******************************************************************* *)
+(* *)
+(* triv_solv less1 : less -> proof Library.option *)
+(* *)
+(* Solves trivial goal x <= x. *)
+(* *)
+(* ******************************************************************* *)
+
+fun triv_solv (Le (x, x', _)) =
+ if x aconv x' then Some (Thm ([], Less.le_refl))
+ else None
+| triv_solv _ = None;
+
+(* ********************************************************************* *)
+(* Graph functions *)
+(* ********************************************************************* *)
+
+
+
+(* ******************************************************************* *)
+(* *)
+(* General: *)
+(* *)
+(* Inequalities are represented by various types of graphs. *)
+(* *)
+(* 1. (Term.term * Term.term list) list *)
+(* - Graph of this type is generated from the assumptions, *)
+(* does not contain information on which edge stems from which *)
+(* assumption. *)
+(* - Used to compute strong components. *)
+(* *)
+(* 2. (Term.term * (Term.term * less) list) list *)
+(* - Graph of this type is generated from the assumptions, *)
+(* it does contain information on which edge stems from which *)
+(* assumption. *)
+(* - Used to reconstruct paths. *)
+(* *)
+(* 3. (int * (int * less) list ) list *)
+(* - Graph of this type is generated from the strong components of *)
+(* graph of type 2. It consists of the strong components of *)
+(* graph 2, where nodes are indices of the components. *)
+(* Only edges between components are part of this graph. *)
+(* - Used to reconstruct paths between several components. *)
+(* *)
+(* 4. (int * int list) list *)
+(* - Graph of this type is generated from graph of type 3, but *)
+(* edge information of type less is removed. *)
+(* - Used to *)
+(* - Compute transposed graphs of type 4. *)
+(* - Compute list of components reachable from a component. *)
+(* *)
+(* *)
+(* ******************************************************************* *)
+
+
+(* *********************************************************** *)
+(* Functions for constructing graphs *)
+(* *********************************************************** *)
+
+fun addLessEdge (v,d,[]) = [(v,d)]
+| addLessEdge (v,d,((u,dl)::el)) = if v aconv u then ((v,d@dl)::el)
+ else (u,dl):: (addLessEdge(v,d,el));
+
+fun addTermEdge (v,u,[]) = [(v,[u])]
+| addTermEdge (v,u,((x,adj)::el)) = if v aconv x then (v,u::adj)::el
+ else (x,adj) :: addTermEdge (v,u,el);
+
+(* ********************************************************************* *)
+(* *)
+(* buildGraphs constructs three graphs from a list of type less: *)
+(* g1: graph for the <= relation *)
+(* g2: graph for the <= relation with additional information for *)
+(* proof reconstruction *)
+(* neqEdges: all edges that are candidates for a ~= *)
+(* *)
+(* ********************************************************************* *)
+
+
+fun buildGraphs ([],g1,g2,neqEdges) = (g1, g2, neqEdges)
+| buildGraphs (l::ls,g1,g2,neqEdges) = case l of
+(Less (x,y,p)) =>(
+ let val g1' = addTermEdge (x,y,g1)
+ and g2' = addLessEdge (x,[(y,(Less (x, y, p)))],g2)
+ in buildGraphs (ls,g1',g2',l::neqEdges) end)
+| (Le (x,y,p)) =>
+( let val g1' = addTermEdge (x,y,g1)
+ and g2' = addLessEdge (x,[(y,(Le (x, y,p)))],g2)
+ in buildGraphs (ls,g1',g2',neqEdges) end)
+| (NotEq (x,y,p)) => ( buildGraphs (ls,g1,g2,l::neqEdges) )
+
+
+(* *********************************************************************** *)
+(* *)
+(* adjacent_term g u : (Term.term * 'a list ) list -> Term.term -> 'a list *)
+(* *)
+(* *)
+(* *********************************************************************** *)
+
+fun adjacent_term ((v,adj)::el) u =
+ if u aconv v then adj else adjacent_term el u
+| adjacent_term nil _ = []
+
+(* *********************************************************************** *)
+(* *)
+(* adjacent_term g u : (''a * 'b list ) list -> ''a -> 'b list *)
+(* *)
+(* List of successors of u in graph g *)
+(* *)
+(* *********************************************************************** *)
+
+fun adjacent ((v,adj)::el) u =
+ if u = v then adj else adjacent el u
+| adjacent nil _ = []
+
+
+(* *********************************************************************** *)
+(* *)
+(* transpose_term g: *)
+(* (Term.term * Term.term list) list -> (Term.term * Term.term list) list *)
+(* *)
+(* Computes transposed graph g' from g *)
+(* by reversing all edges u -> v to v -> u *)
+(* *)
+(* *********************************************************************** *)
+
+ fun transpose_term g =
+ let
+ (* Compute list of reversed edges for each adjacency list *)
+ fun flip (u,v::el) = (v,u) :: flip (u,el)
+ | flip (_,nil) = nil
+
+ (* Compute adjacency list for node u from the list of edges
+ and return a likewise reduced list of edges. The list of edges
+ is searches for edges starting from u, and these edges are removed. *)
+ fun gather (u,(v,w)::el) =
+ let
+ val (adj,edges) = gather (u,el)
+ in
+ if u aconv v then (w::adj,edges)
+ else (adj,(v,w)::edges)
+ end
+ | gather (_,nil) = (nil,nil)
+
+ (* For every node in the input graph, call gather to find all reachable
+ nodes in the list of edges *)
+ fun assemble ((u,_)::el) edges =
+ let val (adj,edges) = gather (u,edges)
+ in (u,adj) :: assemble el edges
+ end
+ | assemble nil _ = nil
+
+ (* Compute, for each adjacency list, the list with reversed edges,
+ and concatenate these lists. *)
+ val flipped = foldr (op @) ((map flip g),nil)
+
+ in assemble g flipped end
+
+(* *********************************************************************** *)
+(* *)
+(* transpose g: *)
+(* (''a * ''a list) list -> (''a * ''a list) list *)
+(* *)
+(* Computes transposed graph g' from g *)
+(* by reversing all edges u -> v to v -> u *)
+(* *)
+(* *********************************************************************** *)
+
+fun transpose g =
+ let
+ (* Compute list of reversed edges for each adjacency list *)
+ fun flip (u,v::el) = (v,u) :: flip (u,el)
+ | flip (_,nil) = nil
+
+ (* Compute adjacency list for node u from the list of edges
+ and return a likewise reduced list of edges. The list of edges
+ is searches for edges starting from u, and these edges are removed. *)
+ fun gather (u,(v,w)::el) =
+ let
+ val (adj,edges) = gather (u,el)
+ in
+ if u = v then (w::adj,edges)
+ else (adj,(v,w)::edges)
+ end
+ | gather (_,nil) = (nil,nil)
+
+ (* For every node in the input graph, call gather to find all reachable
+ nodes in the list of edges *)
+ fun assemble ((u,_)::el) edges =
+ let val (adj,edges) = gather (u,edges)
+ in (u,adj) :: assemble el edges
+ end
+ | assemble nil _ = nil
+
+ (* Compute, for each adjacency list, the list with reversed edges,
+ and concatenate these lists. *)
+ val flipped = foldr (op @) ((map flip g),nil)
+
+ in assemble g flipped end
+
+
+(* 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). *)
+
+fun scc_term G =
+ let
+ (* Ordered list of the vertices that DFS has finished with;
+ most recently finished goes at the head. *)
+ val finish : term list ref = ref nil
+
+ (* 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
+ vertex list. *)
+ val members = map (fn (v,_) => v)
+
+ (* Returns the nodes in the DFS tree rooted at u in g *)
+ fun dfs_visit g u : term list =
+ let
+ val _ = visited := u :: !visited
+ val descendents =
+ foldr (fn (v,ds) => if been_visited v then ds
+ else v :: dfs_visit g v @ ds)
+ ((adjacent_term g u) ,nil)
+ in
+ finish := u :: !finish;
+ descendents
+ end
+ in
+
+ (* DFS on the graph; apply dfs_visit to each vertex in
+ the graph, checking first to make sure the vertex is
+ as yet unvisited. *)
+ app (fn u => if been_visited u then ()
+ else (dfs_visit G u; ())) (members G);
+ visited := nil;
+
+ (* We don't reset finish because its value is used by
+ revfold below, and it will never be used again (even
+ though dfs_visit will continue to modify it). *)
+
+ (* DFS on the transpose. The vertices returned by
+ dfs_visit along with u form a connected component. We
+ collect all the connected components together in a
+ list, which is what is returned. *)
+ foldl (fn (comps,u) =>
+ if been_visited u then comps
+ else ((u :: dfs_visit (transpose_term G) u) :: comps)) (nil,(!finish))
+end;
+
+
+(* *********************************************************************** *)
+(* *)
+(* dfs_int_reachable g u: *)
+(* (int * int list) list -> int -> int list *)
+(* *)
+(* Computes list of all nodes reachable from u in g. *)
+(* *)
+(* *********************************************************************** *)
+
+
+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 =
+ let
+ val _ = visited := u :: !visited
+ val descendents =
+ foldr (fn (v,ds) => if been_visited v then ds
+ else v :: dfs_visit g v @ ds)
+ ( ((adjacent g u)) ,nil)
+ in descendents end
+
+ in u :: dfs_visit g u end;
+
+
+fun indexComps components =
+ ListPair.map (fn (a,b) => (b,a)) (components, 0 upto (length components -1));
+
+fun indexNodes IndexComp =
+ flat (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;
+
+
+(* ***************************************************************** *)
+(* *)
+(* evalcompgraph components g ntc : *)
+(* Term.term list list -> *)
+(* (Term.term * (Term.term * less) list) list -> *)
+(* (Term.term * int) list -> (int * (int * less) list) list *)
+(* *)
+(* *)
+(* Computes, from graph g, list of all its components and the list *)
+(* ntc (nodes, index of component) a graph whose nodes are the *)
+(* indices of the components of g. Egdes of the new graph are *)
+(* only the edges of g linking two components. *)
+(* *)
+(* ***************************************************************** *)
+
+fun evalcompgraph components g ntc =
+ let
+ (* Liste (Index der Komponente, Komponente *)
+ val IndexComp = indexComps components;
+
+ (* Compute new graph with the property that it only contains edges
+ between components. *)
+
+ (* k is index of current start component. *)
+
+ fun processComponent (k, comp) =
+ let
+ (* all edges pointing away from the component *)
+ (* (Term.term * less) list *)
+ val allEdges = flat (map (adjacent_term g) comp);
+
+ (* choose those edges pointing to nodes outside
+ the current component *)
+
+ fun selectEdges [] = []
+ | selectEdges ((v,l)::es) = let val k' = getIndex v ntc in
+ if k' = k then selectEdges es else (k', l) :: (selectEdges es) end;
+
+ (* Insert edge into sorted list of edges, where edge is
+ only added if
+ - it is found for the first time
+ - it is a <= edge and no parallel < edge was found earlier
+ - it is a < edge
+ *)
+
+ fun insert (h,l) [] = [(h,l)]
+ | insert (h,l) ((k',l')::es) = if h = k' then (
+ case l of (Less (_, _, _)) => (h,l)::es
+ | _ => (case l' of (Less (_, _, _)) => (h,l')::es
+ | _ => (k',l)::es) )
+ else (k',l'):: insert (h,l) es;
+
+ (* Reorganise list of edges such that
+ - duplicate edges are removed
+ - if a < edge and a <= edge exist at the same time,
+ remove <= edge *)
+
+ fun sortEdges [] sorted = sorted: (int * less) list
+ | sortEdges (e::es) sorted = sortEdges es (insert e sorted);
+
+ in
+ (k, (sortEdges (selectEdges allEdges) []))
+ end;
+
+
+in map processComponent IndexComp end;
+
+(* Remove ``less'' edge info from graph *)
+(* type ('a * ('a * less) list) list *)
+fun stripOffLess g = map (fn (v, desc) => (v,map (fn (u,l) => u) desc)) g;
+
+
+
+(* *********************************************************************** *)
+(* *)
+(* dfs_term g u v: *)
+(* (Term.term *(Term.term * less) list) list -> *)
+(* Term.term -> Term.term -> (bool * less list) *)
+(* *)
+(* Depth first search of v from u. *)
+(* Returns (true, path(u, v)) if successful, otherwise (false, []). *)
+(* *)
+(* *********************************************************************** *)
+
+
+fun dfs_term g u v =
+ let
+(* TODO: this comment is unclear *)
+ (* Liste der gegangenen Kanten,
+ die Kante e die zum Vorgaenger eines Knoten u gehoert ist jene
+ für die gilt (upper e) = u *)
+ val pred : less list ref = ref nil;
+ val visited: term list ref = ref nil;
+
+ fun been_visited v = exists (fn w => w aconv v) (!visited)
+
+ fun dfs_visit u' =
+ let val _ = visited := u' :: (!visited)
+
+ fun update l = let val _ = pred := l ::(!pred) in () end;
+
+ in if been_visited v then ()
+ else (app (fn (v',l) => if been_visited v' then () else (
+ update l;
+ dfs_visit v'; ()) )) (adjacent_term g u')
+ end
+
+ 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 *)
+(* -> less list *)
+(* *)
+(* Complete the path from u to v in graph g. Path search is performed *)
+(* with dfs_term g u v. This yields for each node v' its predecessor u' *)
+(* and the edge u' -> v'. Allows traversing graph backwards from v and *)
+(* finding the path u -> v. *)
+(* *)
+(* *********************************************************************** *)
+
+
+fun completeTermPath u v g =
+ let
+
+ val (found, pred) = dfs_term g u v;
+
+ fun path x y =
+ let
+
+ (* find predecessor u of node v and the edge u -> v *)
+
+ fun lookup v [] = raise Cannot
+ | lookup v (e::es) = if (upper e) aconv v then e else lookup v es;
+
+ (* traverse path backwards and return list of visited edges *)
+ fun rev_path v =
+ let val l = lookup v pred
+ val u = lower l;
+ in
+ if u aconv x then [l]
+ else (rev_path u) @ [l]
+ end
+ in rev_path y end;
+
+ in
+ if found then (if u aconv v then [(Le (u, v, (Thm ([], Less.le_refl))))]
+ else path u v ) else raise Cannot
+end;
+
+
+(* *********************************************************************** *)
+(* *)
+(* dfs_int g u v: *)
+(* (int *(int * less) list) list -> int -> int *)
+(* -> (bool *(int* less) list) *)
+(* *)
+(* Depth first search of v from u. *)
+(* Returns (true, path(u, v)) if successful, otherwise (false, []). *)
+(* *)
+(* *********************************************************************** *)
+
+fun dfs_int g u v =
+ let
+ val pred : (int * less ) list ref = ref nil;
+ val visited: int list ref = ref nil;
+
+ fun been_visited v = exists (fn w => w = v) (!visited)
+
+ fun dfs_visit u' =
+ let val _ = visited := u' :: (!visited)
+
+ fun update (x,l) = let val _ = pred := (x,l) ::(!pred) in () end;
+
+ in if been_visited v then ()
+ else (app (fn (v',l) => if been_visited v' then () else (
+ update (v',l);
+ dfs_visit v'; ()) )) (adjacent g u')
+
+ end
+
+ in
+ dfs_visit u;
+ if (been_visited v) then (true, (!pred)) else (false , [])
+ end;
+
+
+(* *********************************************************************** *)
+(* *)
+(* findProof (g2, cg2, neqEdges, components, ntc) subgoal: *)
+(* (Term.term * (Term.term * less) list) list * *)
+(* (int * (int * less) list) list * less list * Term.term list list *)
+(* * ( (Term.term * int) -> proof *)
+(* *)
+(* findProof constructs from graphs (g2, cg2) and neqEdges a proof for *)
+(* subgoal. Raises exception Cannot if this is not possible. *)
+(* *)
+(* *********************************************************************** *)
+
+fun findProof (g2, cg2, neqEdges, components, ntc ) 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,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 g2)@[edge]@(completeTermPath v y' g2)
+ else (rev_completeComponentPath u)@[edge]@(completeTermPath v y' g2)
+ end
+ in
+ if x aconv y then
+ [(Le (x, y, (Thm ([], Less.le_refl))))]
+ else ( if xi = yi then completeTermPath x y g2
+ 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
+ val v = upper e
+ val ui = getIndex u ntc
+ val vi = getIndex v ntc
+
+ in
+ if ui mem Xreachable andalso vi mem Xreachable andalso
+ ui mem Yreachable andalso vi mem Yreachable then (
+
+ (case e of (Less (_, _, _)) =>
+ let
+ val (xufound, xupred) = dfs_int cg2 xi (getIndex u ntc)
+ in
+ if xufound then (
+ let
+ val (vyfound, vypred) = dfs_int cg2 (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 (xufound, xupred) = dfs_int cg2 xi (getIndex u ntc)
+ in
+ if xufound then (
+ let
+ val (uvfound, uvpred) = dfs_int cg2 (getIndex u ntc) (getIndex v ntc)
+ in
+ if uvfound then (
+ let
+ val (vyfound, vypred) = dfs_int cg2 (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 )
+ ) else None
+end;
+
+
+in
+ (* looking for x <= y: any path from x to y is sufficient *)
+ case subgoal of (Le (x, y, _)) => (
+
+ let
+ val xi = getIndex x ntc
+ val yi = getIndex y ntc
+ (* sucht im Komponentengraphen einen Weg von der Komponente in der x liegt
+ zu der in der y liegt *)
+ val (found, pred) = dfs_int cg2 xi yi
+ 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.less_imp_le))
+ else raise Cannot
+ | _ => if xyLesss subsumes subgoal then (getprf xyLesss)
+ 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, _)) => (
+ let
+ val xi = getIndex x ntc
+ val yi = getIndex y ntc
+ val cg2' = stripOffLess cg2
+ val cg2'_transpose = transpose cg2'
+ (* alle von x aus erreichbaren Komponenten *)
+ val xreachable = dfs_int_reachable cg2' xi
+ (* all comonents reachable from y in the transposed graph cg2' *)
+ val yreachable = dfs_int_reachable cg2'_transpose yi
+ (* 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
+ | _ => processNeqEdges es
+
+ in
+ processNeqEdges neqEdges
+ end
+
+ )
+| (NotEq (x, y, _)) => (
+
+ let val xi = getIndex x ntc
+ val yi = getIndex y ntc
+ val cg2' = stripOffLess cg2
+ val cg2'_transpose = transpose cg2'
+ val xreachable = dfs_int_reachable cg2' xi
+ val yreachable = dfs_int_reachable cg2'_transpose yi
+
+ 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.less_imp_neq))
+ else (Thm ([(Thm ([q], Less.less_imp_neq))], thm "not_sym"))
+ )
+ | (NotEq (u,v, q)) => (
+ if u aconv x andalso v aconv y then q
+ else (Thm ([q], thm "not_sym"))
+ )
+ )
+ (* if SCC_x is linked to SCC_y via edge e *)
+ else if ui = xi andalso vi = yi then (
+ case e of (Less (_, _,_)) => (
+ let val xypath = (completeTermPath x u g2) @ [e] @ (completeTermPath v y g2)
+ val xyLesss = transPath (tl xypath, hd xypath)
+ in (Thm ([getprf xyLesss], Less.less_imp_neq)) end)
+ | _ => (
+ let val xupath = completeTermPath x u g2
+ val uxpath = completeTermPath u x g2
+ val vypath = completeTermPath v y g2
+ val yvpath = completeTermPath y v g2
+ 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)], Less.eqI))
+ val v_eq_y = (Thm ([(getprf vyLesss),(getprf yvLesss)], Less.eqI))
+ in
+ (Thm ([x_eq_u , (getprf e), v_eq_y ], Less.eq_neq_eq_imp_neq))
+ end
+ )
+ ) else if ui = yi andalso vi = xi then (
+ case e of (Less (_, _,_)) => (
+ let val xypath = (completeTermPath y u g2) @ [e] @ (completeTermPath v x g2)
+ val xyLesss = transPath (tl xypath, hd xypath)
+ in (Thm ([(Thm ([getprf xyLesss], Less.less_imp_neq))] , thm "not_sym")) end )
+ | _ => (
+
+ let val yupath = completeTermPath y u g2
+ val uypath = completeTermPath u y g2
+ val vxpath = completeTermPath v x g2
+ val xvpath = completeTermPath x v g2
+ 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)], Less.eqI))
+ val v_eq_x = (Thm ([(getprf vxLesss),(getprf xvLesss)], Less.eqI))
+ in
+ (Thm ([(Thm ([y_eq_u , (getprf e), v_eq_x ], Less.eq_neq_eq_imp_neq))], thm "not_sym"))
+ 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.less_imp_neq))
+ | None => (
+ let
+ val yr = dfs_int_reachable cg2' yi
+ val xr = dfs_int_reachable cg2'_transpose xi
+ in
+ case (findLess e y x yi xi yr xr) of
+ (Some prf) => (Thm ([(Thm ([prf], Less.less_imp_neq))], thm "not_sym"))
+ | _ => processNeqEdges es
+ end)
+ ) end)
+ in processNeqEdges neqEdges end
+ )
+end;
+
+
+(* *********************************************************************** *)
+(* *)
+(* checkComponents g components ntc neqEdges: *)
+(* (Term.term * (Term.term * less) list) list -> Term.term list list -> *)
+(* (Term.term * int) -> less list -> bool *)
+(* *)
+(* For each edge in the list neqEdges check if it leads to a contradiction.*)
+(* We have a contradiction for edge u ~= v and u < v if: *)
+(* - u and v are in the same component, *)
+(* that is, a path u <= v and a path v <= u exist, hence u = v. *)
+(* From irreflexivity of < follows u < u or v < v. Ex false quodlibet. *)
+(* *)
+(* *)
+(* *********************************************************************** *)
+
+
+fun checkComponents g components ntc neqEdges =
+ let
+ (* Construct proof by contradiction for edge *)
+ fun handleContr edge =
+ (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.less_reflE )))
+ 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.less_reflE )))
+ end
+ )
+ | _ => error "trans_tac/checkCompoents/handleContr: invalid Contradiction");
+
+ (* Check each edge in neqEdges for contradiction.
+ If there is a contradiction, call handleContr, otherwise do nothing. *)
+ fun checkNeqEdges [] = ()
+ | checkNeqEdges (e::es) =
+ (case e of (Less (u, v, _)) =>
+ if (getIndex u ntc) = (getIndex v ntc) then handleContr e g
+ else checkNeqEdges es
+ | (NotEq (u, v, _)) =>
+ if (getIndex u ntc) = (getIndex v ntc) then handleContr e g
+ else checkNeqEdges es
+ | _ => checkNeqEdges es)
+
+ in if g = [] then () else checkNeqEdges neqEdges end;
+
+(* *********************************************************************** *)
+(* *)
+(* solvePartialOrder sign (asms,concl) : *)
+(* Sign.sg -> less list * Term.term -> proof list *)
+(* *)
+(* Find proof if possible for partial orders. *)
+(* *)
+(* *********************************************************************** *)
+
+fun solvePartialOrder sign (asms, concl) =
+ let
+ val (g1, g2, neqEdges) = buildGraphs (asms, [], [],[])
+ val components = scc_term g1
+ val ntc = indexNodes (indexComps components)
+ val cg2 = evalcompgraph components g2 ntc
+ in
+ (* Check for contradiction within assumptions *)
+ checkComponents g2 components ntc neqEdges;
+ let
+ val (subgoals, prf) = mkconcl_partial sign concl
+ fun solve facts less =
+ (case triv_solv less of None => findProof (g2, cg2, neqEdges, components, ntc) less
+ | Some prf => prf )
+ in
+ map (solve asms) subgoals
+ end
+ end;
+
+(* *********************************************************************** *)
+(* *)
+(* solveTotalOrder sign (asms,concl) : *)
+(* Sign.sg -> less list * Term.term -> proof list *)
+(* *)
+(* Find proof if possible for linear orders. *)
+(* *)
+(* *********************************************************************** *)
+
+fun solveTotalOrder sign (asms, concl) =
+ let
+ val (g1, g2, neqEdges) = buildGraphs (asms, [], [],[])
+ val components = scc_term g1
+ val ntc = indexNodes (indexComps components)
+ val cg2 = evalcompgraph components g2 ntc
+ in
+ checkComponents g2 components ntc neqEdges;
+ let
+ val (subgoals, prf) = mkconcl_linear sign concl
+ fun solve facts less =
+ (case triv_solv less of None => findProof (g2, cg2, neqEdges, components, ntc) less
+ | Some prf => prf )
+ in
+ map (solve asms) subgoals
+ end
+ end;
+
+
+(* partial_tac - solves linear/total orders *)
+
+val partial_tac = SUBGOAL (fn (A, n, sign) =>
+ let
+ val rfrees = map Free (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_partial sign) (Hs, 0 upto (length Hs - 1)))
+ val prfs = solvePartialOrder sign (lesss, C);
+ val (subgoals, prf) = mkconcl_partial sign C;
+ in
+ METAHYPS (fn asms =>
+ let val thms = map (prove 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
+ );
+
+(* linear_tac - solves linear/total orders *)
+
+val linear_tac = SUBGOAL (fn (A, n, sign) =>
+ let
+ val rfrees = map Free (rename_wrt_term A (Logic.strip_params A))
+ 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_linear sign) (Hs, 0 upto (length Hs - 1)))
+ val prfs = solveTotalOrder sign (lesss, C);
+ val (subgoals, prf) = mkconcl_linear sign C;
+ in
+ METAHYPS (fn asms =>
+ let val thms = map (prove 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);
+
+end;
+