(* Title: Provers/quasi.ML
Author: Oliver Kutter, TU Muenchen
Reasoner for simple transitivity and quasi orders.
*)
(*
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: theory -> term -> (term * string * term) option
(* decomp_quasi is used by quasi_tac *)
val decomp_quasi: theory -> term -> (term * string * term) option
end;
signature QUASI_TAC =
sig
val trans_tac: Proof.context -> int -> tactic
val quasi_tac: Proof.context -> int -> tactic
end;
functor Quasi_Tac(Less: LESS_ARITH): QUASI_TAC =
struct
(* 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_trans sign (t, n) : theory -> (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 thy (t, n) =
case Less.decomp_trans thy 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) : theory -> (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 thy (t, n) =
case Less.decomp_quasi thy 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 : theory -> 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 thy t =
case Less.decomp_trans thy 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 : theory -> Term.term -> less *)
(* *)
(* Translates conclusion t to an element of type less. *)
(* Quasi orders only. *)
(* *)
(* ************************************************************************ *)
fun mkconcl_quasi thy t =
case Less.decomp_quasi thy 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 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 = 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 (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) : *)
(* theory -> less list * Term.term -> proof list *)
(* *)
(* Solves *)
(* *)
(* *********************************************************************** *)
fun solveLeTrans thy (asms, concl) =
let
val g = mkGraph asms
in
let
val (subgoal, prf) = mkconcl_trans thy 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) : *)
(* theory -> less list * Term.term -> proof list *)
(* *)
(* Find proof if possible for quasi order. *)
(* *)
(* *********************************************************************** *)
fun solveQuasiOrder thy (asms, concl) =
let
val (leG, neqE) = mkQuasiGraph asms
in
let
val (subgoals, prf) = mkconcl_quasi thy 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 <= *)
fun trans_tac ctxt = 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 (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_trans thy o swap) Hs);
val prfs = solveLeTrans thy (lesss, C);
val (subgoal, prf) = mkconcl_trans thy C;
in
Subgoal.FOCUS (fn {prems, ...} =>
let val thms = map (prove prems) prfs
in rtac (prove thms prf) 1 end) ctxt n st
end
handle Contr p => Subgoal.FOCUS (fn {prems, ...} => rtac (prove prems p) 1) ctxt n st
| Cannot => Seq.empty);
(* quasi_tac - solves quasi orders *)
fun quasi_tac ctxt = 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 (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_quasi thy o swap) Hs);
val prfs = solveQuasiOrder thy (lesss, C);
val (subgoals, prf) = mkconcl_quasi thy C;
in
Subgoal.FOCUS (fn {prems, ...} =>
let val thms = map (prove prems) prfs
in rtac (prove thms prf) 1 end) ctxt n st
end
handle Contr p =>
(Subgoal.FOCUS (fn {prems, ...} => rtac (prove prems p) 1) ctxt n st
handle General.Subscript => Seq.empty)
| Cannot => Seq.empty
| General.Subscript => Seq.empty);
end;