(* Title: Provers/order.ML Author: Oliver Kutter, TU Muenchen Transitivity reasoner for partial and linear orders. *) (* TODO: reduce number of input thms *) (* The package 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 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 ORDER_TAC = sig (* Theorems required by the reasoner *) type less_arith val empty : thm -> less_arith val update : string -> thm -> less_arith -> less_arith (* Tactics *) val partial_tac: (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 -> Proof.context -> thm list -> int -> tactic end; structure Order_Tac: ORDER_TAC = struct (* Record to handle input theorems in a convenient way. *) type less_arith = { (* Theorems for partial orders *) less_reflE: thm, (* x < x ==> P *) le_refl: thm, (* x <= x *) less_imp_le: thm, (* x < y ==> x <= y *) eqI: thm, (* [| x <= y; y <= x |] ==> x = y *) eqD1: thm, (* x = y ==> x <= y *) eqD2: thm, (* x = y ==> y <= x *) less_trans: thm, (* [| x < y; y < z |] ==> x < z *) less_le_trans: thm, (* [| x < y; y <= z |] ==> x < z *) le_less_trans: thm, (* [| x <= y; y < z |] ==> x < z *) le_trans: thm, (* [| x <= y; y <= z |] ==> x <= z *) le_neq_trans : thm, (* [| x <= y ; x ~= y |] ==> x < y *) neq_le_trans : thm, (* [| x ~= y ; x <= y |] ==> x < y *) not_sym : thm, (* x ~= y ==> y ~= x *) (* Additional theorems for linear orders *) not_lessD: thm, (* ~(x < y) ==> y <= x *) not_leD: thm, (* ~(x <= y) ==> y < x *) not_lessI: thm, (* y <= x ==> ~(x < y) *) not_leI: thm, (* y < x ==> ~(x <= y) *) (* Additional theorems for subgoals of form x ~= y *) less_imp_neq : thm, (* x < y ==> x ~= y *) eq_neq_eq_imp_neq : thm (* [| x = u ; u ~= v ; v = z|] ==> x ~= z *) } fun empty dummy_thm = {less_reflE= dummy_thm, le_refl= dummy_thm, less_imp_le= dummy_thm, eqI= dummy_thm, eqD1= dummy_thm, eqD2= dummy_thm, less_trans= dummy_thm, less_le_trans= dummy_thm, le_less_trans= dummy_thm, le_trans= dummy_thm, le_neq_trans = dummy_thm, neq_le_trans = dummy_thm, not_sym = dummy_thm, not_lessD= dummy_thm, not_leD= dummy_thm, not_lessI= dummy_thm, not_leI= dummy_thm, less_imp_neq = dummy_thm, eq_neq_eq_imp_neq = dummy_thm} fun change thms f = let val {less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans, 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, eq_neq_eq_imp_neq} = thms; val (less_reflE', le_refl', less_imp_le', eqI', eqD1', eqD2', less_trans', 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', eq_neq_eq_imp_neq') = f (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans, 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, eq_neq_eq_imp_neq) in {less_reflE = less_reflE', le_refl= le_refl', less_imp_le = less_imp_le', eqI = eqI', eqD1 = eqD1', eqD2 = eqD2', less_trans = less_trans', less_le_trans = less_le_trans', le_less_trans = le_less_trans', le_trans = le_trans', le_neq_trans = le_neq_trans', neq_le_trans = neq_le_trans', not_sym = not_sym', not_lessD = not_lessD', not_leD = not_leD', not_lessI = not_lessI', not_leI = not_leI', less_imp_neq = less_imp_neq', eq_neq_eq_imp_neq = eq_neq_eq_imp_neq'} end; fun update "less_reflE" thm thms = change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans, 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, eq_neq_eq_imp_neq) => (thm, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans, 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, eq_neq_eq_imp_neq)) | update "le_refl" thm thms = change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans, 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, eq_neq_eq_imp_neq) => (less_reflE, thm, less_imp_le, eqI, eqD1, eqD2, less_trans, 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, eq_neq_eq_imp_neq)) | update "less_imp_le" thm thms = change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans, 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, eq_neq_eq_imp_neq) => (less_reflE, le_refl, thm, eqI, eqD1, eqD2, less_trans, 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, eq_neq_eq_imp_neq)) | update "eqI" thm thms = change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans, 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, eq_neq_eq_imp_neq) => (less_reflE, le_refl, less_imp_le, thm, eqD1, eqD2, less_trans, 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, eq_neq_eq_imp_neq)) | update "eqD1" thm thms = change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans, 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, eq_neq_eq_imp_neq) => (less_reflE, le_refl, less_imp_le, eqI, thm, eqD2, less_trans, 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, eq_neq_eq_imp_neq)) | update "eqD2" thm thms = change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans, 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, eq_neq_eq_imp_neq) => (less_reflE, le_refl, less_imp_le, eqI, eqD1, thm, less_trans, 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, eq_neq_eq_imp_neq)) | update "less_trans" thm thms = change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans, 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, eq_neq_eq_imp_neq) => (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, thm, 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, eq_neq_eq_imp_neq)) | update "less_le_trans" thm thms = change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans, 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, eq_neq_eq_imp_neq) => (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans, thm, le_less_trans, le_trans, le_neq_trans, neq_le_trans, not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, eq_neq_eq_imp_neq)) | update "le_less_trans" thm thms = change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans, 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, eq_neq_eq_imp_neq) => (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans, less_le_trans, thm, le_trans, le_neq_trans, neq_le_trans, not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, eq_neq_eq_imp_neq)) | update "le_trans" thm thms = change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans, 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, eq_neq_eq_imp_neq) => (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans, less_le_trans, le_less_trans, thm, le_neq_trans, neq_le_trans, not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, eq_neq_eq_imp_neq)) | update "le_neq_trans" thm thms = change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans, 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, eq_neq_eq_imp_neq) => (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans, less_le_trans, le_less_trans, le_trans, thm, neq_le_trans, not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, eq_neq_eq_imp_neq)) | update "neq_le_trans" thm thms = change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans, 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, eq_neq_eq_imp_neq) => (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans, less_le_trans, le_less_trans, le_trans, le_neq_trans, thm, not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, eq_neq_eq_imp_neq)) | update "not_sym" thm thms = change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans, 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, eq_neq_eq_imp_neq) => (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans, less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans, thm, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, eq_neq_eq_imp_neq)) | update "not_lessD" thm thms = change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans, 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, eq_neq_eq_imp_neq) => (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans, less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans, not_sym, thm, not_leD, not_lessI, not_leI, less_imp_neq, eq_neq_eq_imp_neq)) | update "not_leD" thm thms = change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans, 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, eq_neq_eq_imp_neq) => (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans, less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans, not_sym, not_lessD, thm, not_lessI, not_leI, less_imp_neq, eq_neq_eq_imp_neq)) | update "not_lessI" thm thms = change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans, 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, eq_neq_eq_imp_neq) => (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans, less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans, not_sym, not_lessD, not_leD, thm, not_leI, less_imp_neq, eq_neq_eq_imp_neq)) | update "not_leI" thm thms = change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans, 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, eq_neq_eq_imp_neq) => (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans, less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans, not_sym, not_lessD, not_leD, not_lessI, thm, less_imp_neq, eq_neq_eq_imp_neq)) | update "less_imp_neq" thm thms = change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans, 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, eq_neq_eq_imp_neq) => (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans, less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans, not_sym, not_lessD, not_leD, not_lessI, not_leI, thm, eq_neq_eq_imp_neq)) | update "eq_neq_eq_imp_neq" thm thms = change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans, 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, eq_neq_eq_imp_neq) => (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans, 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)); (* 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 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 | 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 *) (* *) (* 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 decomp (less_thms : less_arith) sign (n, t) = 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)) 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 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))] | _ => error ("partial_tac: unknown relation symbol ``" ^ rel ^ "''returned by decomp.")) | NONE => []; (* ************************************************************************ *) (* *) (* mkasm_linear *) (* *) (* 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 decomp (less_thms : less_arith) sign (n, t) = 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)) 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))] | "=" => [Le (x, y, Thm ([Asm n], #eqD1 less_thms)), Le (y, x, Thm ([Asm n], #eqD2 less_thms))] | "~=" => 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))] | _ => error ("linear_tac: unknown relation symbol ``" ^ rel ^ "''returned by decomp.")) | NONE => []; (* ************************************************************************ *) (* *) (* mkconcl_partial *) (* *) (* Translates conclusion t to an element of type less. *) (* Partial orders only. *) (* *) (* ************************************************************************ *) fun mkconcl_partial decomp (less_thms : less_arith) sign t = case decomp 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], #eqI less_thms)) | "~=" => ([NotEq (x,y, Asm ~1)], Asm 0) | _ => raise Cannot) | NONE => raise Cannot; (* ************************************************************************ *) (* *) (* mkconcl_linear *) (* *) (* Translates conclusion t to an element of type less. *) (* Linear orders only. *) (* *) (* ************************************************************************ *) fun mkconcl_linear decomp (less_thms : less_arith) sign t = case decomp 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], #not_lessI less_thms)) | "<=" => ([Le (x, y, Asm ~1)], Asm 0) | "~<=" => ([Less (y, x, Asm ~1)], Thm ([Asm 0], #not_leI less_thms)) | "=" => ([Le (x, y, Asm ~1), Le (y, x, Asm ~1)], Thm ([Asm 0, Asm 1], #eqI less_thms)) | "~=" => ([NotEq (x,y, Asm ~1)], Asm 0) | _ => raise Cannot) | NONE => raise Cannot; (*** The common part for partial and linear orders ***) (* Analysis of premises and conclusion: *) (* decomp (`x Rel y') should yield (x, Rel, y) where Rel is one of "<", "<=", "~<", "~<=", "=" and "~=", other relation symbols cause an error message *) fun gen_order_tac mkasm mkconcl decomp' (less_thms : less_arith) ctxt prems = let fun decomp sign t = Option.map (fn (x, rel, y) => (Envir.beta_eta_contract x, rel, Envir.beta_eta_contract y)) (decomp' sign t); (* ******************************************************************* *) (* *) (* mergeLess *) (* *) (* Merge two 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_trans less_thms)) | mergeLess (Less (x, _, p) , Le (_ , z, q)) = Less (x, z, Thm ([p,q] , #less_le_trans less_thms)) | 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' ) 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') 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') 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] , #le_trans less_thms)) | 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 option *) (* *) (* Solves trivial goal x <= x. *) (* *) (* ******************************************************************* *) fun triv_solv (Le (x, x', _)) = if x aconv x' then SOME (Thm ([], #le_refl less_thms)) else NONE | triv_solv _ = NONE; (* ********************************************************************* *) (* Graph functions *) (* ********************************************************************* *) (* ******************************************************************* *) (* *) (* General: *) (* *) (* Inequalities are represented by various types of graphs. *) (* *) (* 1. (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 compute strongly connected components *) (* - Used to compute component subgraphs *) (* - Used for component subgraphs to reconstruct paths in components*) (* *) (* 2. (int * (int * less) list ) list *) (* - Graph of this type is generated from the strong components of *) (* graph of type 1. It consists of the strong components of *) (* graph 1, where nodes are indices of the components. *) (* Only edges between components are part of this graph. *) (* - Used to reconstruct paths between several components. *) (* *) (* ******************************************************************* *) (* *********************************************************** *) (* Functions for constructing graphs *) (* *********************************************************** *) fun addEdge (v,d,[]) = [(v,d)] | addEdge (v,d,((u,dl)::el)) = if v aconv u then ((v,d@dl)::el) else (u,dl):: (addEdge(v,d,el)); (* ********************************************************************* *) (* *) (* 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 = 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) | (Le (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; (* *********************************************************************** *) (* *) (* adjacent g u : (''a * 'b list ) list -> ''a -> 'b list *) (* *) (* List of successors of u in graph g *) (* *) (* *********************************************************************** *) fun adjacent eq_comp ((v,adj)::el) u = if eq_comp (u, v) then adj else adjacent eq_comp el u | adjacent _ [] _ = [] (* *********************************************************************** *) (* *) (* transpose g: *) (* (''a * ''a list) list -> (''a * ''a list) list *) (* *) (* Computes transposed graph g' from g *) (* by reversing all edges u -> v to v -> u *) (* *) (* *********************************************************************** *) fun transpose eq_comp g = let (* Compute list of reversed edges for each adjacency list *) fun flip (u,(v,l)::el) = (v,(u,l)) :: flip (u,el) | flip (_,[]) = [] (* Compute adjacency list for node u from the list of edges and return a likewise reduced list of edges. The list of edges is searches for edges starting from u, and these edges are removed. *) fun gather (u,(v,w)::el) = let val (adj,edges) = gather (u,el) in if eq_comp (u, v) then (w::adj,edges) else (adj,(v,w)::edges) end | gather (_,[]) = ([],[]) (* 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 [] _ = [] (* Compute, for each adjacency list, the list with reversed edges, and concatenate these lists. *) val flipped = maps flip g 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 Unsynchronized.ref = Unsynchronized.ref [] (* List of vertices which have been visited. *) val visited : term list Unsynchronized.ref = Unsynchronized.ref [] 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 = List.foldr (fn ((v,l),ds) => if been_visited v then ds else v :: dfs_visit g v @ ds) [] (adjacent (op aconv) g u) 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. *) List.app (fn u => if been_visited u then () else (dfs_visit G u; ())) (members G); visited := []; (* We don't reset finish because its value is used by foldl 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. *) fold (fn u => fn comps => if been_visited u then comps else (u :: dfs_visit (transpose (op aconv) G) u) :: comps) (!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 Unsynchronized.ref = Unsynchronized.ref [] fun been_visited v = exists (fn w => w = v) (!visited) fun dfs_visit g u : int list = let val _ = visited := u :: !visited val descendents = List.foldr (fn ((v,l),ds) => if been_visited v then ds else v :: dfs_visit g v @ ds) [] (adjacent (op =) g u) in descendents end in u :: dfs_visit g u end; fun indexNodes IndexComp = maps (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; (* *********************************************************************** *) (* *) (* dfs eq_comp g u v: *) (* ('a * 'a -> bool) -> ('a *( 'a * less) list) 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 val pred = Unsynchronized.ref []; val visited = Unsynchronized.ref []; fun been_visited v = exists (fn w => eq_comp (w, v)) (!visited) fun dfs_visit u' = let val _ = visited := u' :: (!visited) fun update (x,l) = let val _ = pred := (x,l) ::(!pred) in () end; in if been_visited v then () else (List.app (fn (v',l) => if been_visited v' then () else ( update (v',l); dfs_visit v'; ()) )) (adjacent eq_comp g u') end in dfs_visit u; if (been_visited v) then (true, (!pred)) else (false , []) end; (* *********************************************************************** *) (* *) (* 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, 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 = 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 ([], #le_refl less_thms))))] else path u v ) else raise Cannot end; (* *********************************************************************** *) (* *) (* findProof (sccGraph, neqE, ntc, sccSubgraphs) subgoal: *) (* *) (* (int * (int * less) list) list * less list * (Term.term * int) list *) (* * ((term * (term * less) list) list) list -> Less -> proof *) (* *) (* findProof constructs from graphs (sccGraph, sccSubgraphs) and neqE a *) (* 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 (nth sccSubgraphs xi) @ [edge] @ completeTermPath v y' (nth sccSubgraphs (getIndex y' ntc)) else rev_completeComponentPath u @ [edge] @ completeTermPath v y' (nth sccSubgraphs (getIndex y' ntc)) end in if x aconv y then [(Le (x, y, (Thm ([], #le_refl less_thms))))] else if xi = yi then completeTermPath x y (nth sccSubgraphs xi) 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 member (op =) xreachable ui andalso member (op =) xreachable vi andalso member (op =) yreachable ui andalso member (op =) yreachable vi then ( (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) 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) 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, _)) => ( 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 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) 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 val xi = getIndex x ntc val yi = getIndex y ntc val sccGraph_transpose = transpose (op =) sccGraph (* all components that can be reached from component xi *) val xreachable = dfs_int_reachable sccGraph xi (* 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 | _ => processNeqEdges es in processNeqEdges neqE end ) ) | (NotEq (x, y, _)) => ( (* if there aren't any edges that are candidate for a ~= raise Cannot *) if null neqE then raise Cannot (* if there aren't any edges that are candidate for <= then just search a edge in neqE that implies the subgoal *) else if null sccSubgraphs then ( (case (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 (Thm ([p], #less_imp_neq less_thms)) else (Thm ([(Thm ([p], #less_imp_neq less_thms))], #not_sym less_thms)) | _ => raise Cannot) ) else ( let val xi = getIndex x ntc val yi = getIndex y ntc 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)) ) ) (* 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 (nth sccSubgraphs ui) @ [e] @ completeTermPath v y (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 (nth sccSubgraphs ui) val uxpath = completeTermPath u x (nth sccSubgraphs ui) val vypath = completeTermPath v y (nth sccSubgraphs vi) val yvpath = completeTermPath y v (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 (nth sccSubgraphs ui) @ [e] @ completeTermPath v x (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 (nth sccSubgraphs ui) val uypath = completeTermPath u y (nth sccSubgraphs ui) val vxpath = completeTermPath v x (nth sccSubgraphs vi) val xvpath = completeTermPath x v (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)) | 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)) | _ => processNeqEdges es end) ) end) in processNeqEdges neqE end) ) end; (* ******************************************************************* *) (* *) (* mk_sccGraphs components leqG neqG ntc : *) (* Term.term list list -> *) (* (Term.term * (Term.term * less) list) list -> *) (* (Term.term * (Term.term * less) list) list -> *) (* (Term.term * int) list -> *) (* (int * (int * less) list) list * *) (* ((Term.term * (Term.term * less) list) list) list *) (* *) (* *) (* Computes, from graph leqG, 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. Also computes for each *) (* component the subgraph of leqG that forms this component. *) (* *) (* For each component SCC_i is checked if there exists a edge in neqG *) (* that 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 mk_sccGraphs _ [] _ _ = ([],[]) | mk_sccGraphs components leqG neqG ntc = let (* Liste (Index der Komponente, Komponente *) val IndexComp = map_index I components; 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 ) | (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 *) val leqEdges = maps (adjacent (op aconv) leqG) comp; (* all edges with weight ~= of the actual component *) val neqEdges = map snd (maps (adjacent (op aconv) neqG) comp); (* 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 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 - 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); (* 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 ([], []); val subGraph = sccSubGraph intern []; 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; (** Find proof if possible. **) fun gen_solve mkconcl sign (asms, concl) = let val (leqG, neqG, neqE) = mkGraphs asms val components = scc_term leqG val ntc = indexNodes (map_index I components) val (sccGraph, sccSubgraphs) = mk_sccGraphs components leqG neqG ntc in 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 | SOME prf => prf ) in map (solve asms) subgoals end end; in SUBGOAL (fn (A, n) => fn st => let val thy = Proof_Context.theory_of ctxt; val rfrees = map Free (Term.rename_wrt_term A (Logic.strip_params A)); val Hs = map Thm.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 = flat (map_index (mkasm decomp less_thms thy) Hs) val prfs = gen_solve mkconcl thy (lesss, C); val (subgoals, prf) = mkconcl decomp less_thms thy C; in Subgoal.FOCUS (fn {context = ctxt', prems = asms, ...} => let val thms = map (prove (prems @ asms)) prfs in resolve_tac ctxt' [prove thms prf] 1 end) ctxt n st end handle Contr p => (Subgoal.FOCUS (fn {context = ctxt', prems = asms, ...} => resolve_tac ctxt' [prove asms p] 1) ctxt n st handle General.Subscript => Seq.empty) | Cannot => Seq.empty | General.Subscript => Seq.empty) end; (* partial_tac - solves partial orders *) val partial_tac = gen_order_tac mkasm_partial mkconcl_partial; (* linear_tac - solves linear/total orders *) val linear_tac = gen_order_tac mkasm_linear mkconcl_linear; end;