# HG changeset patch
# User haftmann
# Date 1550255062 0
# Node ID 56d5bb8c102eb71754bcb419258b641a6edec5d7
# Parent  5929b172c6fe2483961a968cb10fdcfa1901496c
proper installation of ancient procedure for preorders

diff -r 5929b172c6fe -r 56d5bb8c102e src/HOL/Library/Preorder.thy
--- a/src/HOL/Library/Preorder.thy	Fri Feb 15 07:11:11 2019 +0000
+++ b/src/HOL/Library/Preorder.thy	Fri Feb 15 18:24:22 2019 +0000
@@ -16,13 +16,22 @@
   equiv ("'(\<approx>')") and
   equiv ("(_/ \<approx> _)"  [51, 51] 50)
 
-lemma refl [iff]: "x \<approx> x"
+lemma equivD1: "x \<le> y" if "x \<approx> y"
+  using that by (simp add: equiv_def)
+
+lemma equivD2: "y \<le> x" if "x \<approx> y"
+  using that by (simp add: equiv_def)
+
+lemma equiv_refl [iff]: "x \<approx> x"
   by (simp add: equiv_def)
 
-lemma trans: "x \<approx> y \<Longrightarrow> y \<approx> z \<Longrightarrow> x \<approx> z"
+lemma equiv_sym: "x \<approx> y \<longleftrightarrow> y \<approx> x"
+  by (auto simp add: equiv_def)
+
+lemma equiv_trans: "x \<approx> y \<Longrightarrow> y \<approx> z \<Longrightarrow> x \<approx> z"
   by (auto simp: equiv_def intro: order_trans)
 
-lemma antisym: "x \<le> y \<Longrightarrow> y \<le> x \<Longrightarrow> x \<approx> y"
+lemma equiv_antisym: "x \<le> y \<Longrightarrow> y \<le> x \<Longrightarrow> x \<approx> y"
   by (simp only: equiv_def)
 
 lemma less_le: "x < y \<longleftrightarrow> x \<le> y \<and> \<not> x \<approx> y"
@@ -31,24 +40,55 @@
 lemma le_less: "x \<le> y \<longleftrightarrow> x < y \<or> x \<approx> y"
   by (auto simp add: equiv_def less_le)
 
-lemma le_imp_less_or_eq: "x \<le> y \<Longrightarrow> x < y \<or> x \<approx> y"
+lemma le_imp_less_or_equiv: "x \<le> y \<Longrightarrow> x < y \<or> x \<approx> y"
   by (simp add: less_le)
 
-lemma less_imp_not_eq: "x < y \<Longrightarrow> x \<approx> y \<longleftrightarrow> False"
+lemma less_imp_not_equiv: "x < y \<Longrightarrow> \<not> x \<approx> y"
   by (simp add: less_le)
 
-lemma less_imp_not_eq2: "x < y \<Longrightarrow> y \<approx> x \<longleftrightarrow> False"
-  by (simp add: equiv_def less_le)
-
-lemma neq_le_trans: "\<not> a \<approx> b \<Longrightarrow> a \<le> b \<Longrightarrow> a < b"
+lemma not_equiv_le_trans: "\<not> a \<approx> b \<Longrightarrow> a \<le> b \<Longrightarrow> a < b"
   by (simp add: less_le)
 
-lemma le_neq_trans: "a \<le> b \<Longrightarrow> \<not> a \<approx> b \<Longrightarrow> a < b"
-  by (simp add: less_le)
+lemma le_not_equiv_trans: "a \<le> b \<Longrightarrow> \<not> a \<approx> b \<Longrightarrow> a < b"
+  by (rule not_equiv_le_trans)
 
 lemma antisym_conv: "y \<le> x \<Longrightarrow> x \<le> y \<longleftrightarrow> x \<approx> y"
   by (simp add: equiv_def)
 
 end
 
+thm order_trans
+
+find_theorems "?i < ?j \<Longrightarrow> ?i \<le> ?j"
+
+ML_file \<open>~~/src/Provers/preorder.ML\<close>
+
+ML \<open>
+structure Quasi = Quasi_Tac(
+struct
+
+val le_trans = @{thm order_trans};
+val le_refl = @{thm order_refl};
+val eqD1 = @{thm equivD1};
+val eqD2 = @{thm equivD2};
+val less_reflE = @{thm less_irrefl};
+val less_imp_le = @{thm less_imp_le};
+val le_neq_trans = @{thm le_not_equiv_trans};
+val neq_le_trans = @{thm not_equiv_le_trans};
+val less_imp_neq = @{thm less_imp_not_equiv};
+
+fun decomp_quasi thy (Const (@{const_name less_eq}, _) $ t1 $ t2) = SOME (t1, "<=", t2)
+  | decomp_quasi thy (Const (@{const_name less}, _) $ t1 $ t2) = SOME (t1, "<", t2)
+  | decomp_quasi thy (Const (@{const_name equiv}, _) $ t1 $ t2) = SOME (t1, "=", t2)
+  | decomp_quasi thy (Const (@{const_name Not}, _) $ (Const (@{const_name equiv}, _) $ t1 $ t2)) = SOME (t1, "~=", t2)
+  | decomp_quasi thy _ = NONE;
+
+fun decomp_trans thy t = case decomp_quasi thy t of
+    x as SOME (t1, "<=", t2) => x
+  | _ => NONE;
+
 end
+);
+\<close>
+
+end
diff -r 5929b172c6fe -r 56d5bb8c102e src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Fri Feb 15 07:11:11 2019 +0000
+++ b/src/HOL/Orderings.thy	Fri Feb 15 18:24:22 2019 +0000
@@ -10,7 +10,6 @@
 begin
 
 ML_file \<open>~~/src/Provers/order.ML\<close>
-ML_file \<open>~~/src/Provers/quasi.ML\<close>  (* FIXME unused? *)
 
 subsection \<open>Abstract ordering\<close>
 
diff -r 5929b172c6fe -r 56d5bb8c102e src/HOL/ex/Function_Growth.thy
--- a/src/HOL/ex/Function_Growth.thy	Fri Feb 15 07:11:11 2019 +0000
+++ b/src/HOL/ex/Function_Growth.thy	Fri Feb 15 18:24:22 2019 +0000
@@ -279,7 +279,7 @@
   qed
 qed
 
-declare fun_order.antisym [intro?]
+declare fun_order.equiv_antisym [intro?]
 
 
 subsection \<open>Simple examples\<close>
diff -r 5929b172c6fe -r 56d5bb8c102e src/Provers/preorder.ML
--- /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;
diff -r 5929b172c6fe -r 56d5bb8c102e src/Provers/quasi.ML
--- a/src/Provers/quasi.ML	Fri Feb 15 07:11:11 2019 +0000
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,598 +0,0 @@
-(*  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 (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;