# HG changeset patch # User ballarin # Date 1091537271 -7200 # Node ID 79846e8792ebcfb3abe0ac55a1c5a19f63673f22 # Parent 04b0e943fcc96b5ef871330bc4b5d984577bcd32 New transitivity reasoners for transitivity only and quasi orders. diff -r 04b0e943fcc9 -r 79846e8792eb NEWS --- a/NEWS Tue Aug 03 13:48:00 2004 +0200 +++ b/NEWS Tue Aug 03 14:47:51 2004 +0200 @@ -6,6 +6,9 @@ *** General *** +* Provers/quasi.ML: new transitivity reasoners for transitivity only + and quasi orders. + * Provers/trancl.ML: new transitivity reasoner for transitive and reflexive-transitive closure of relations. diff -r 04b0e943fcc9 -r 79846e8792eb src/HOL/HOL.thy --- a/src/HOL/HOL.thy Tue Aug 03 13:48:00 2004 +0200 +++ b/src/HOL/HOL.thy Tue Aug 03 14:47:51 2004 +0200 @@ -986,7 +986,49 @@ ML_setup {* -structure Trans_Tac = Trans_Tac_Fun ( +(* The setting up of Quasi_Tac serves as a demo. Since there is no + class for quasi orders, the tactics Quasi_Tac.trans_tac and + Quasi_Tac.quasi_tac are not of much use. *) + +structure Quasi_Tac = Quasi_Tac_Fun ( + struct + val le_trans = thm "order_trans"; + val le_refl = thm "order_refl"; + val eqD1 = thm "order_eq_refl"; + val eqD2 = thm "sym" RS thm "order_eq_refl"; + val less_reflE = thm "order_less_irrefl" RS thm "notE"; + val less_imp_le = thm "order_less_imp_le"; + val le_neq_trans = thm "order_le_neq_trans"; + val neq_le_trans = thm "order_neq_le_trans"; + val less_imp_neq = thm "less_imp_neq"; + + fun decomp_gen sort sign (Trueprop $ t) = + let fun of_sort t = Sign.of_sort sign (type_of t, sort) + fun dec (Const ("Not", _) $ t) = ( + case dec t of + None => None + | Some (t1, rel, t2) => Some (t1, "~" ^ rel, t2)) + | dec (Const ("op =", _) $ t1 $ t2) = + if of_sort t1 + then Some (t1, "=", t2) + else None + | dec (Const ("op <=", _) $ t1 $ t2) = + if of_sort t1 + then Some (t1, "<=", t2) + else None + | dec (Const ("op <", _) $ t1 $ t2) = + if of_sort t1 + then Some (t1, "<", t2) + else None + | dec _ = None + in dec t end; + + val decomp_trans = decomp_gen ["HOL.order"]; + val decomp_quasi = decomp_gen ["HOL.order"]; + + end); (* struct *) + +structure Order_Tac = Order_Tac_Fun ( struct val less_reflE = thm "order_less_irrefl" RS thm "notE"; val le_refl = thm "order_refl"; @@ -1034,26 +1076,29 @@ end); (* struct *) simpset_ref() := simpset () - addSolver (mk_solver "Trans_linear" (fn _ => Trans_Tac.linear_tac)) - addSolver (mk_solver "Trans_partial" (fn _ => Trans_Tac.partial_tac)); + addSolver (mk_solver "Trans_linear" (fn _ => Order_Tac.linear_tac)) + addSolver (mk_solver "Trans_partial" (fn _ => Order_Tac.partial_tac)); (* Adding the transitivity reasoners also as safe solvers showed a slight speed up, but the reasoning strength appears to be not higher (at least no breaking of additional proofs in the entire HOL distribution, as of 5 March 2004, was observed). *) *} -(* Optional methods +(* Optional setup of methods *) +(* method_setup trans_partial = - {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (trans_tac_partial)) *} - {* simple transitivity reasoner *} + {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (Order_Tac.partial_tac)) *} + {* transitivity reasoner for partial orders *} method_setup trans_linear = - {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (trans_tac_linear)) *} - {* simple transitivity reasoner *} + {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (Order_Tac.linear_tac)) *} + {* transitivity reasoner for linear orders *} *) (* declare order.order_refl [simp del] order_less_irrefl [simp del] + +can currently not be removed, abel_cancel relies on it. *) subsubsection "Bounded quantifiers" diff -r 04b0e943fcc9 -r 79846e8792eb src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Tue Aug 03 13:48:00 2004 +0200 +++ b/src/HOL/IsaMakefile Tue Aug 03 14:47:51 2004 +0200 @@ -77,6 +77,7 @@ $(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML \ $(SRC)/Provers/hypsubst.ML $(SRC)/Provers/induct_method.ML \ $(SRC)/Provers/make_elim.ML $(SRC)/Provers/order.ML \ + $(SRC)/Provers/quasi.ML \ $(SRC)/Provers/simplifier.ML $(SRC)/Provers/splitter.ML \ $(SRC)/Provers/trancl.ML \ $(SRC)/TFL/dcterm.ML $(SRC)/TFL/post.ML $(SRC)/TFL/rules.ML \ diff -r 04b0e943fcc9 -r 79846e8792eb src/HOL/ROOT.ML --- a/src/HOL/ROOT.ML Tue Aug 03 13:48:00 2004 +0200 +++ b/src/HOL/ROOT.ML Tue Aug 03 14:47:51 2004 +0200 @@ -34,6 +34,7 @@ use "~~/src/Provers/Arith/cancel_numeral_factor.ML"; use "~~/src/Provers/Arith/extract_common_term.ML"; use "~~/src/Provers/Arith/cancel_div_mod.ML"; +use "~~/src/Provers/quasi.ML"; use "~~/src/Provers/order.ML"; with_path "Integ" use_thy "Main"; diff -r 04b0e943fcc9 -r 79846e8792eb src/Provers/order.ML --- a/src/Provers/order.ML Tue Aug 03 13:48:00 2004 +0200 +++ b/src/Provers/order.ML Tue Aug 03 14:47:51 2004 +0200 @@ -9,7 +9,7 @@ (* -The packages provides tactics partial_tac and linear_tac that use all +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) @@ -56,21 +56,22 @@ val eq_neq_eq_imp_neq : thm (* [| x = u ; u ~= v ; v = z|] ==> x ~= z *) (* Analysis of premises and conclusion *) - (* decomp_part is for partial_tac, decomp_lin is for linear_tac; - decomp_x (`x Rel y') should yield (x, Rel, y) + (* decomp_x (`x Rel y') should yield (x, Rel, y) where Rel is one of "<", "<=", "~<", "~<=", "=" and "~=", other relation symbols cause an error message *) + (* decomp_part is used by partial_tac *) val decomp_part: Sign.sg -> term -> (term * string * term) option + (* decomp_lin is used by linear_tac *) val decomp_lin: Sign.sg -> term -> (term * string * term) option end; -signature TRANS_TAC = +signature ORDER_TAC = sig val partial_tac: int -> tactic val linear_tac: int -> tactic end; -functor Trans_Tac_Fun (Less: LESS_ARITH): TRANS_TAC = +functor Order_Tac_Fun (Less: LESS_ARITH): ORDER_TAC = struct (* Extract subgoal with signature *) diff -r 04b0e943fcc9 -r 79846e8792eb src/Provers/quasi.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Provers/quasi.ML Tue Aug 03 14:47:51 2004 +0200 @@ -0,0 +1,598 @@ +(* + Title: Reasoner for simple transitivity and quasi orders. + Id: $Id$ + Author: Oliver Kutter + Copyright: TU Muenchen + *) + +(* + +The package provides tactics trans_tac and quasi_tac that use +premises of the form + + t = u, t ~= u, t < u and t <= u + +to +- either derive a contradiction, in which case the conclusion can be + any term, +- or prove the concluson, which must be of the form t ~= u, t < u or + t <= u. + +Details: + +1. trans_tac: + Only premises of form t <= u are used and the conclusion must be of + the same form. The conclusion is proved, if possible, by a chain of + transitivity from the assumptions. + +2. quasi_tac: + <= is assumed to be a quasi order and < its strict relative, defined + as t < u == t <= u & t ~= u. Again, the conclusion is proved from + 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. +*) + +signature LESS_ARITH = +sig + (* Transitivity of <= + 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 *) + val eqD2: thm (* x = y ==> y <= x *) + + (* Additional theorems for premises of the form x < y *) + val less_reflE: thm (* x < x ==> P *) + val less_imp_le : thm (* x < y ==> x <= y *) + + (* Additional theorems for premises of the form x ~= y *) + val le_neq_trans : thm (* [| x <= y ; x ~= y |] ==> x < y *) + val neq_le_trans : thm (* [| x ~= y ; x <= y |] ==> x < y *) + + (* Additional theorem for goals of form x ~= y *) + val less_imp_neq : thm (* x < y ==> x ~= y *) + + (* Analysis of premises and conclusion *) + (* decomp_x (`x Rel y') should yield Some (x, Rel, y) + where Rel is one of "<", "<=", "=" and "~=", + other relation symbols cause an error message *) + (* decomp_trans is used by trans_tac, it may only return Rel = "<=" *) + val decomp_trans: Sign.sg -> term -> (term * string * term) option + (* decomp_quasi is used by quasi_tac *) + val decomp_quasi: Sign.sg -> term -> (term * string * term) option +end; + +signature QUASI_TAC = +sig + val trans_tac: int -> tactic + val quasi_tac: int -> tactic +end; + +functor Quasi_Tac_Fun (Less: LESS_ARITH): QUASI_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_trans 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. *) +(* Only assumptions of form x <= y are used, all others are ignored *) +(* *) +(* ************************************************************************ *) + +fun mkasm_trans sign (t, n) = + case Less.decomp_trans sign t of + 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) : 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. *) +(* Quasi orders only. *) +(* *) +(* ************************************************************************ *) + +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)) + 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"))] + | _ => error ("quasi_tac: unknown relation symbol ``" ^ rel ^ + "''returned by decomp_quasi.")) + | None => []; + + +(* ************************************************************************ *) +(* *) +(* mkconcl_trans sign t : Sign.sg -> Term.term -> less *) +(* *) +(* Translates conclusion t to an element of type less. *) +(* Only for Conclusions of form x <= y or x < y. *) +(* *) +(* ************************************************************************ *) + + +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) + | _ => raise Cannot) + | None => raise Cannot; + + +(* ************************************************************************ *) +(* *) +(* mkconcl_quasi sign t : Sign.sg -> Term.term -> less *) +(* *) +(* Translates conclusion t to an element of type less. *) +(* Quasi orders only. *) +(* *) +(* ************************************************************************ *) + +fun mkconcl_quasi sign t = + case Less.decomp_quasi sign t of + Some (x, rel, y) => (case rel of + "<" => ([Less (x, y, Asm ~1)], Asm 0) + | "<=" => ([Le (x, y, Asm ~1)], Asm 0) + | "~=" => ([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 && x ~= y ==> x < y *) +(* x ~= y && x <= y ==> x < y *) +(* *) +(* ******************************************************************* *) + +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' ) + 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') + then Less (x, z, Thm ([p,q] , Less.neq_le_trans)) + else error "quasi_tac: internal error neq_le_trans" +| mergeLess (_, _) = + error "quasi_tac: internal error: undefined case"; + + +(* ******************************************************************** *) +(* tr checks for valid transitivity step *) +(* ******************************************************************** *) + +infix tr; +fun (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 "trans/quasi_tac: internal error transpath"; + +(* ******************************************************************* *) +(* *) +(* less1 subsumes less2 : less -> less -> bool *) +(* *) +(* subsumes checks whether less1 implies less2 *) +(* *) +(* ******************************************************************* *) + +infix subsumes; +fun (Le (x, y, _)) subsumes (Le (x', y', _)) = + (x aconv x' andalso y aconv y') + | (Le _) subsumes (Less _) = + error "trans/quasi_tac: internal error: Le cannot subsume Less" + | (NotEq(x,y,_)) subsumes (NotEq(x',y',_)) = x aconv x' andalso y aconv y' orelse x aconv y' andalso y aconv x' + | _ 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 *) +(* ********************************************************************* *) + +(* *********************************************************** *) +(* 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)); + +(* ********************************************************************** *) +(* *) +(* 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 = + let + fun buildGraphs ([],leG, neqE) = (leG, neqE) + | 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) + | _ => buildGraphs (ls, leG, l::neqE) ; + +in buildGraphs (lessList, [], []) end; + +(* ********************************************************************** *) +(* *) +(* mkGraph constructs from a list of objects of type less a graph g *) +(* Used for plain transitivity chain reasoning. *) +(* *) +(* ********************************************************************** *) + +fun mkGraph [] = [] +| mkGraph lessList = + let + fun buildGraph ([],g) = g + | buildGraph (l::ls, g) = buildGraph (ls, (addEdge ((lower l),[((upper l),l)],g))) + +in buildGraph (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 _ [] _ = [] + +(* *********************************************************************** *) +(* *) +(* 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 = ref nil; + val visited = ref nil; + + 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 (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; + +(* ************************************************************************ *) +(* *) +(* Begin: Quasi Order relevant functions *) +(* *) +(* *) +(* ************************************************************************ *) + +(* ************************************************************************ *) +(* *) +(* findPath x y g: Term.term -> Term.term -> *) +(* (Term.term * (Term.term * less list) list) -> *) +(* (bool, less list) *) +(* *) +(* Searches a path from vertex x to vertex y in Graph g, returns true and *) +(* the list of edges forming the path, if a path is found, otherwise false *) +(* and nil. *) +(* *) +(* ************************************************************************ *) + + + 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 *) + 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 x aconv y then (found,[(Le (x, y, (Thm ([], Less.le_refl))))]) + else (found, (path x y) )) + else (found,[]) + 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. *) +(* *) +(* ************************************************************************ *) + + +(* 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. <= *) +(* This is simply done by searching any path from x to y in the graph leG. *) +(* The graph leG contains only edges with label <=. *) +(* *) +(* 2. < *) +(* A path from x to y with label < can be found by searching a path with *) +(* label <= from x to y in the graph leG and merging the path x <= y with *) +(* a parallel edge x ~= y resp. y ~= x to x < y. *) +(* *) +(* 3. ~= *) +(* If the conclusion is of form x ~= y, we can find a proof either directly, *) +(* if x ~= y or y ~= x are among the assumptions, or by constructing x ~= y if *) +(* x < y or y < x follows from the assumptions. *) + +fun findQuasiProof (leG, neqE) subgoal = + case subgoal of (Le (x,y, _)) => ( + let + val (xyLefound,xyLePath) = findPath x y leG + in + if xyLefound then ( + let + val Le_x_y = (transPath (tl xyLePath, hd xyLePath)) + in getprf Le_x_y end ) + else raise Cannot + end ) + | (Less (x,y,_)) => ( + 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 ; + 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 + in + if xyLeFound then ( + 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 ) + | (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 + else Thm ([p], thm "not_sym") + | _ => raise Cannot + ) + + +(* ************************************************************************ *) +(* *) +(* End: Quasi Order relevant functions *) +(* *) +(* *) +(* ************************************************************************ *) + +(* *********************************************************************** *) +(* *) +(* solveLeTrans sign (asms,concl) : *) +(* Sign.sg -> less list * Term.term -> proof list *) +(* *) +(* Solves *) +(* *) +(* *********************************************************************** *) + +fun solveLeTrans sign (asms, concl) = + let + val g = mkGraph asms + in + let + val (subgoal, prf) = mkconcl_trans sign concl + val (found, path) = findPath (lower subgoal) (upper subgoal) g + in + if found then [getprf (transPath (tl path, hd path))] + else raise Cannot + end + end; + + +(* *********************************************************************** *) +(* *) +(* solveQuasiOrder sign (asms,concl) : *) +(* Sign.sg -> less list * Term.term -> proof list *) +(* *) +(* Find proof if possible for quasi order. *) +(* *) +(* *********************************************************************** *) + +fun solveQuasiOrder sign (asms, concl) = + let + val (leG, neqE) = mkQuasiGraph asms + in + let + val (subgoals, prf) = mkconcl_quasi sign concl + fun solve facts less = + (case triv_solv less of None => findQuasiProof (leG, neqE) less + | Some prf => prf ) + in map (solve asms) subgoals end + end; + +(* ************************************************************************ *) +(* *) +(* Tactics *) +(* *) +(* - trans_tac *) +(* - quasi_tac, solves quasi orders *) +(* ************************************************************************ *) + + +(* trans_tac - solves transitivity chains over <= *) +val trans_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_trans sign) (Hs, 0 upto (length Hs - 1))) + val prfs = solveLeTrans sign (lesss, C); + + val (subgoal, prf) = mkconcl_trans 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 +); + +(* quasi_tac - solves quasi orders *) +val quasi_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_quasi sign) (Hs, 0 upto (length Hs - 1))) + val prfs = solveQuasiOrder sign (lesss, C); + val (subgoals, prf) = mkconcl_quasi 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;