--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Provers/preorder.ML Fri Feb 15 18:24:22 2019 +0000
@@ -0,0 +1,598 @@
+(* Title: src/Provers/preorder.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 (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;
+
+(* ************************************************************************ *)
+(* *)
+(* 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 (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 {context = ctxt', prems, ...} =>
+ let val thms = map (prove prems) prfs
+ in resolve_tac ctxt' [prove thms prf] 1 end) ctxt n st
+ end
+ handle Contr p =>
+ Subgoal.FOCUS (fn {context = ctxt', prems, ...} =>
+ resolve_tac ctxt' [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 {context = ctxt', prems, ...} =>
+ let val thms = map (prove prems) prfs
+ in resolve_tac ctxt' [prove thms prf] 1 end) ctxt n st
+ end
+ handle Contr p =>
+ (Subgoal.FOCUS (fn {context = ctxt', prems, ...} =>
+ resolve_tac ctxt' [prove prems p] 1) ctxt n st handle General.Subscript => Seq.empty)
+ | Cannot => Seq.empty
+ | General.Subscript => Seq.empty);
+
+end;