# HG changeset patch
# User nipkow
# Date 1617255303 -7200
# Node ID c72fd8f1fcebaf86006caa552590b94dd8bdfbce
# Parent  419edc7f372685fe7d421e8c7dccb2141dc69617# Parent  a3cc9fa1295df753394b606dabbb39b411857877
merged

diff -r 419edc7f3726 -r c72fd8f1fceb CONTRIBUTORS
--- a/CONTRIBUTORS	Wed Mar 31 23:45:16 2021 +0200
+++ b/CONTRIBUTORS	Thu Apr 01 07:35:03 2021 +0200
@@ -6,6 +6,9 @@
 Contributions to this Isabelle version
 --------------------------------------
 
+* March 2021: Lukas Stevens
+  New order prover
+
 * March 2021: Florian Haftmann
   Dedicated session for combinatorics.
 
diff -r 419edc7f3726 -r c72fd8f1fceb src/HOL/Analysis/Interval_Integral.thy
--- a/src/HOL/Analysis/Interval_Integral.thy	Wed Mar 31 23:45:16 2021 +0200
+++ b/src/HOL/Analysis/Interval_Integral.thy	Thu Apr 01 07:35:03 2021 +0200
@@ -438,8 +438,9 @@
     by (rule interval_integral_endpoints_reverse)
   show ?thesis
     using integrable
-    by (cases a b b c a c rule: linorder_le_cases[case_product linorder_le_cases linorder_cases])
-       (simp_all add: min_absorb1 min_absorb2 max_absorb1 max_absorb2 field_simps 1 2 3)
+    apply (cases a b b c a c rule: linorder_le_cases[case_product linorder_le_cases linorder_cases])
+    apply simp_all (* remove some looping cases *)
+    by (simp_all add: min_absorb1 min_absorb2 max_absorb1 max_absorb2 field_simps 1 2 3)
 qed
 
 lemma interval_integrable_isCont:
diff -r 419edc7f3726 -r c72fd8f1fceb src/HOL/Data_Structures/Brother12_Map.thy
--- a/src/HOL/Data_Structures/Brother12_Map.thy	Wed Mar 31 23:45:16 2021 +0200
+++ b/src/HOL/Data_Structures/Brother12_Map.thy	Thu Apr 01 07:35:03 2021 +0200
@@ -83,8 +83,11 @@
 
 lemma inorder_del:
   "t \<in> T h \<Longrightarrow> sorted1(inorder t) \<Longrightarrow> inorder(del x t) = del_list x (inorder t)"
-by(induction h arbitrary: t) (auto simp: del_list_simps inorder_n2
+  apply (induction h arbitrary: t)
+  apply (auto simp: del_list_simps inorder_n2)
+  apply (auto simp: del_list_simps inorder_n2
      inorder_split_min[OF UnI1] inorder_split_min[OF UnI2] split: option.splits)
+  done
 
 lemma inorder_delete:
   "t \<in> T h \<Longrightarrow> sorted1(inorder t) \<Longrightarrow> inorder(delete x t) = del_list x (inorder t)"
diff -r 419edc7f3726 -r c72fd8f1fceb src/HOL/Data_Structures/Brother12_Set.thy
--- a/src/HOL/Data_Structures/Brother12_Set.thy	Wed Mar 31 23:45:16 2021 +0200
+++ b/src/HOL/Data_Structures/Brother12_Set.thy	Thu Apr 01 07:35:03 2021 +0200
@@ -199,8 +199,11 @@
 
 lemma inorder_del:
   "t \<in> T h \<Longrightarrow> sorted(inorder t) \<Longrightarrow> inorder(del x t) = del_list x (inorder t)"
-by(induction h arbitrary: t) (auto simp: del_list_simps inorder_n2
+  apply (induction h arbitrary: t) 
+  apply (auto simp: del_list_simps inorder_n2 split: option.splits)
+  apply (auto simp: del_list_simps inorder_n2
      inorder_split_min[OF UnI1] inorder_split_min[OF UnI2] split: option.splits)
+  done
 
 lemma inorder_delete:
   "t \<in> T h \<Longrightarrow> sorted(inorder t) \<Longrightarrow> inorder(delete x t) = del_list x (inorder t)"
diff -r 419edc7f3726 -r c72fd8f1fceb src/HOL/Data_Structures/Selection.thy
--- a/src/HOL/Data_Structures/Selection.thy	Wed Mar 31 23:45:16 2021 +0200
+++ b/src/HOL/Data_Structures/Selection.thy	Thu Apr 01 07:35:03 2021 +0200
@@ -343,7 +343,8 @@
   have mset_eq: "mset xs = mset ls + mset es + mset gs"
     unfolding ls_def es_def gs_def by (induction xs) auto
   have length_eq: "length xs = length ls + length es + length gs"
-    unfolding ls_def es_def gs_def by (induction xs) auto
+    unfolding ls_def es_def gs_def 
+    using [[simp_depth_limit = 1]] by (induction xs) auto
   have [simp]: "select i es = x" if "i < length es" for i
   proof -
     have "select i es \<in> set (sort es)" unfolding select_def
@@ -555,7 +556,8 @@
     have tw: "(ls, es, gs) = partition3 x xs"
       unfolding partition3_def defs One_nat_def ..
     have length_eq: "length xs = nl + ne + length gs"
-      unfolding nl_def ne_def ls_def es_def gs_def by (induction xs) auto
+      unfolding nl_def ne_def ls_def es_def gs_def
+      using [[simp_depth_limit = 1]] by (induction xs) auto
     note IH = "1.IH"(2,3)[OF False x_def tw refl refl]
 
     have "mom_select k xs = (if k < nl then mom_select k ls else if k < nl + ne then x
diff -r 419edc7f3726 -r c72fd8f1fceb src/HOL/Data_Structures/Set2_Join.thy
--- a/src/HOL/Data_Structures/Set2_Join.thy	Wed Mar 31 23:45:16 2021 +0200
+++ b/src/HOL/Data_Structures/Set2_Join.thy	Thu Apr 01 07:35:03 2021 +0200
@@ -94,7 +94,27 @@
 proof(induction t arbitrary: l b r rule: tree2_induct)
   case Leaf thus ?case by simp
 next
-  case Node thus ?case by(force split!: prod.splits if_splits intro!: bst_join)
+  case (Node y a b z l c r)
+  consider (LT) l1 xin l2 where "(l1,xin,l2) = split y x" 
+    and "split \<langle>y, (a, b), z\<rangle> x = (l1, xin, join l2 a z)" and "cmp x a = LT"
+  | (GT) r1 xin r2 where "(r1,xin,r2) = split z x" 
+    and "split \<langle>y, (a, b), z\<rangle> x = (join y a r1, xin, r2)" and "cmp x a = GT"
+  | (EQ) "split \<langle>y, (a, b), z\<rangle> x = (y, True, z)" and "cmp x a = EQ"
+    by (force split: cmp_val.splits prod.splits if_splits)
+
+  thus ?case 
+  proof cases
+    case (LT l1 xin l2)
+    with Node.IH(1)[OF \<open>(l1,xin,l2) = split y x\<close>[symmetric]] Node.prems
+    show ?thesis by (force intro!: bst_join)
+  next
+    case (GT r1 xin r2)
+    with Node.IH(2)[OF \<open>(r1,xin,r2) = split z x\<close>[symmetric]] Node.prems
+    show ?thesis by (force intro!: bst_join)
+  next
+    case EQ
+    with Node.prems show ?thesis by auto
+  qed
 qed
 
 lemma split_inv: "split t x = (l,b,r) \<Longrightarrow> inv t \<Longrightarrow> inv l \<and> inv r"
diff -r 419edc7f3726 -r c72fd8f1fceb src/HOL/Library/RBT_Impl.thy
--- a/src/HOL/Library/RBT_Impl.thy	Wed Mar 31 23:45:16 2021 +0200
+++ b/src/HOL/Library/RBT_Impl.thy	Thu Apr 01 07:35:03 2021 +0200
@@ -1052,11 +1052,7 @@
 end
 
 theorem (in linorder) rbt_lookup_map: "rbt_lookup (map f t) x = map_option (f x) (rbt_lookup t x)"
-  apply(induct t)
-  apply auto
-  apply(rename_tac a b c, subgoal_tac "x = a")
-  apply auto
-  done
+  by (induct t) (auto simp: antisym_conv3)
  (* FIXME: simproc "antisym less" does not work for linorder context, only for linorder type class
     by (induct t) auto *)
 
@@ -2508,9 +2504,10 @@
 
 lemma rbt_split_min_rbt_lookup: "rbt_split_min t = (a,b,t') \<Longrightarrow> rbt_sorted t \<Longrightarrow> t \<noteq> RBT_Impl.Empty \<Longrightarrow>
   rbt_lookup t k = (if k < a then None else if k = a then Some b else rbt_lookup t' k)"
-  by (induction t arbitrary: a b t')
-     (auto simp: rbt_less_trans antisym_conv3 rbt_less_prop rbt_split_min_set rbt_lookup_rbt_join
-      rbt_split_min_rbt_sorted split!: if_splits prod.splits)
+  apply (induction t arbitrary: a b t')
+   apply(simp_all split: if_splits prod.splits)
+     apply(auto simp: rbt_less_prop rbt_split_min_set rbt_lookup_rbt_join rbt_split_min_rbt_sorted)
+  done
 
 lemma rbt_sorted_rbt_join2: "rbt_sorted l \<Longrightarrow> rbt_sorted r \<Longrightarrow>
   \<forall>x \<in> set (RBT_Impl.keys l). \<forall>y \<in> set (RBT_Impl.keys r). x < y \<Longrightarrow> rbt_sorted (rbt_join2 l r)"
@@ -2528,9 +2525,11 @@
   set (RBT_Impl.keys l) = {a \<in> set (RBT_Impl.keys t). a < x} \<and>
   set (RBT_Impl.keys r) = {a \<in> set (RBT_Impl.keys t). x < a} \<and>
   rbt_sorted l \<and> rbt_sorted r"
-  by (induction t arbitrary: l r)
-     (force simp: Let_def set_rbt_join rbt_greater_prop rbt_less_prop
-      split: if_splits prod.splits intro!: rbt_sorted_rbt_join)+
+  apply (induction t arbitrary: l r)
+   apply(simp_all split!: prod.splits if_splits)
+    apply(force simp: set_rbt_join rbt_greater_prop rbt_less_prop
+      intro: rbt_sorted_rbt_join)+
+  done
 
 lemma rbt_split_lookup: "rbt_split t x = (l,\<beta>,r) \<Longrightarrow> rbt_sorted t \<Longrightarrow>
   rbt_lookup t k = (if k < x then rbt_lookup l k else if k = x then \<beta> else rbt_lookup r k)"
@@ -2884,6 +2883,7 @@
         | Some v \<Rightarrow> (case rbt_lookup t2 k of None \<Rightarrow> Some v | _ \<Rightarrow> None))"
         using not_small rbt_lookup_iff_keys(2)[of l1] rbt_lookup_iff_keys(3)[of l1]
           rbt_lookup_iff_keys(3)[of r1] rbt_split_t1_props
+        using [[simp_depth_limit = 2]]
         by (auto simp: rbt_minus_rec.simps[of t1] Branch rbt_split_t1 rbt_lookup_join2
             minus_l1_l2(2) minus_r1_r2(2) rbt_split_lookup[OF rbt_split_t1 1(4)] lookup_l1_r1_a
             split: option.splits)
diff -r 419edc7f3726 -r c72fd8f1fceb src/HOL/Nonstandard_Analysis/Examples/NSPrimes.thy
--- a/src/HOL/Nonstandard_Analysis/Examples/NSPrimes.thy	Wed Mar 31 23:45:16 2021 +0200
+++ b/src/HOL/Nonstandard_Analysis/Examples/NSPrimes.thy	Thu Apr 01 07:35:03 2021 +0200
@@ -189,8 +189,6 @@
   apply (drule_tac x = m in spec)
   apply (drule subsetD)
    apply auto
-  apply (drule_tac x = "injf_max m E" in order_less_trans)
-   apply auto
   done
 
 lemma inj_injf_max: "\<forall>x. \<exists>y \<in> E. x < y \<Longrightarrow> inj (\<lambda>n. injf_max n E)"
diff -r 419edc7f3726 -r c72fd8f1fceb src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Wed Mar 31 23:45:16 2021 +0200
+++ b/src/HOL/Orderings.thy	Thu Apr 01 07:35:03 2021 +0200
@@ -9,7 +9,8 @@
 keywords "print_orders" :: diag
 begin
 
-ML_file \<open>~~/src/Provers/order.ML\<close>
+ML_file \<open>~~/src/Provers/order_procedure.ML\<close>
+ML_file \<open>~~/src/Provers/order_tac.ML\<close>
 
 subsection \<open>Abstract ordering\<close>
 
@@ -520,114 +521,59 @@
 subsection \<open>Reasoning tools setup\<close>
 
 ML \<open>
-signature ORDERS =
-sig
-  val print_structures: Proof.context -> unit
-  val order_tac: Proof.context -> thm list -> int -> tactic
-  val add_struct: string * term list -> string -> attribute
-  val del_struct: string * term list -> attribute
-end;
-
-structure Orders: ORDERS =
-struct
-
-(* context data *)
-
-fun struct_eq ((s1: string, ts1), (s2, ts2)) =
-  s1 = s2 andalso eq_list (op aconv) (ts1, ts2);
+structure Logic_Signature : LOGIC_SIGNATURE = struct
+  val mk_Trueprop = HOLogic.mk_Trueprop
+  val dest_Trueprop = HOLogic.dest_Trueprop
+  val Trueprop_conv = HOLogic.Trueprop_conv
+  val Not = HOLogic.Not
+  val conj = HOLogic.conj
+  val disj = HOLogic.disj
+  
+  val notI = @{thm notI}
+  val ccontr = @{thm ccontr}
+  val conjI = @{thm conjI}  
+  val conjE = @{thm conjE}
+  val disjE = @{thm disjE}
 
-structure Data = Generic_Data
-(
-  type T = ((string * term list) * Order_Tac.less_arith) list;
-    (* Order structures:
-       identifier of the structure, list of operations and record of theorems
-       needed to set up the transitivity reasoner,
-       identifier and operations identify the structure uniquely. *)
-  val empty = [];
-  val extend = I;
-  fun merge data = AList.join struct_eq (K fst) data;
-);
+  val not_not_conv = Conv.rewr_conv @{thm eq_reflection[OF not_not]}
+  val de_Morgan_conj_conv = Conv.rewr_conv @{thm eq_reflection[OF de_Morgan_conj]}
+  val de_Morgan_disj_conv = Conv.rewr_conv @{thm eq_reflection[OF de_Morgan_disj]}
+  val conj_disj_distribL_conv = Conv.rewr_conv @{thm eq_reflection[OF conj_disj_distribL]}
+  val conj_disj_distribR_conv = Conv.rewr_conv @{thm eq_reflection[OF conj_disj_distribR]}
+end
 
-fun print_structures ctxt =
+structure HOL_Base_Order_Tac = Base_Order_Tac(
+  structure Logic_Sig = Logic_Signature;
+  (* Exclude types with specialised solvers. *)
+  val excluded_types = [HOLogic.natT, HOLogic.intT, HOLogic.realT]
+)
+
+structure HOL_Order_Tac = Order_Tac(structure Base_Tac = HOL_Base_Order_Tac)
+
+fun print_orders ctxt0 =
   let
-    val structs = Data.get (Context.Proof ctxt);
+    val ctxt = Config.put show_sorts true ctxt0
+    val orders = HOL_Order_Tac.Data.get (Context.Proof ctxt)
     fun pretty_term t = Pretty.block
       [Pretty.quote (Syntax.pretty_term ctxt t), Pretty.brk 1,
         Pretty.str "::", Pretty.brk 1,
-        Pretty.quote (Syntax.pretty_typ ctxt (type_of t))];
-    fun pretty_struct ((s, ts), _) = Pretty.block
-      [Pretty.str s, Pretty.str ":", Pretty.brk 1,
-       Pretty.enclose "(" ")" (Pretty.breaks (map pretty_term ts))];
+        Pretty.quote (Syntax.pretty_typ ctxt (type_of t)), Pretty.brk 1]
+    fun pretty_order ({kind = kind, ops = ops, ...}, _) =
+      Pretty.block ([Pretty.str (@{make_string} kind), Pretty.str ":", Pretty.brk 1]
+                    @ map pretty_term ops)
   in
-    Pretty.writeln (Pretty.big_list "order structures:" (map pretty_struct structs))
-  end;
+    Pretty.writeln (Pretty.big_list "order structures:" (map pretty_order orders))
+  end
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>print_orders\<close>
     "print order structures available to transitivity reasoner"
-    (Scan.succeed (Toplevel.keep (print_structures o Toplevel.context_of)));
-
-
-(* tactics *)
+    (Scan.succeed (Toplevel.keep (print_orders o Toplevel.context_of)))
 
-fun struct_tac ((s, ops), thms) ctxt facts =
-  let
-    val [eq, le, less] = ops;
-    fun decomp thy (\<^const>\<open>Trueprop\<close> $ t) =
-          let
-            fun excluded t =
-              (* exclude numeric types: linear arithmetic subsumes transitivity *)
-              let val T = type_of t
-              in
-                T = HOLogic.natT orelse T = HOLogic.intT orelse T = HOLogic.realT
-              end;
-            fun rel (bin_op $ t1 $ t2) =
-                  if excluded t1 then NONE
-                  else if Pattern.matches thy (eq, bin_op) then SOME (t1, "=", t2)
-                  else if Pattern.matches thy (le, bin_op) then SOME (t1, "<=", t2)
-                  else if Pattern.matches thy (less, bin_op) then SOME (t1, "<", t2)
-                  else NONE
-              | rel _ = NONE;
-            fun dec (Const (\<^const_name>\<open>Not\<close>, _) $ t) =
-                  (case rel t of NONE =>
-                    NONE
-                  | SOME (t1, rel, t2) => SOME (t1, "~" ^ rel, t2))
-              | dec x = rel x;
-          in dec t end
-      | decomp _ _ = NONE;
-  in
-    (case s of
-      "order" => Order_Tac.partial_tac decomp thms ctxt facts
-    | "linorder" => Order_Tac.linear_tac decomp thms ctxt facts
-    | _ => error ("Unknown order kind " ^ quote s ^ " encountered in transitivity reasoner"))
-  end
-
-fun order_tac ctxt facts =
-  FIRST' (map (fn s => CHANGED o struct_tac s ctxt facts) (Data.get (Context.Proof ctxt)));
-
-
-(* attributes *)
-
-fun add_struct s tag =
-  Thm.declaration_attribute
-    (fn thm => Data.map (AList.map_default struct_eq (s, Order_Tac.empty TrueI) (Order_Tac.update tag thm)));
-fun del_struct s =
-  Thm.declaration_attribute
-    (fn _ => Data.map (AList.delete struct_eq s));
-
-end;
 \<close>
 
-attribute_setup order = \<open>
-  Scan.lift ((Args.add -- Args.name >> (fn (_, s) => SOME s) || Args.del >> K NONE) --|
-    Args.colon (* FIXME || Scan.succeed true *) ) -- Scan.lift Args.name --
-    Scan.repeat Args.term
-    >> (fn ((SOME tag, n), ts) => Orders.add_struct (n, ts) tag
-         | ((NONE, n), ts) => Orders.del_struct (n, ts))
-\<close> "theorems controlling transitivity reasoner"
-
 method_setup order = \<open>
-  Scan.succeed (fn ctxt => SIMPLE_METHOD' (Orders.order_tac ctxt []))
+  Scan.succeed (fn ctxt => SIMPLE_METHOD' (HOL_Order_Tac.tac [] ctxt))
 \<close> "transitivity reasoner"
 
 
@@ -636,93 +582,43 @@
 context order
 begin
 
-(* The type constraint on @{term (=}) below is necessary since the operation
-   is not a parameter of the locale. *)
-
-declare less_irrefl [THEN notE, order add less_reflE: order "(=) :: 'a \<Rightarrow> 'a \<Rightarrow> bool" "(<=)" "(<)"]
-
-declare order_refl  [order add le_refl: order "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
-
-declare less_imp_le [order add less_imp_le: order "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
-
-declare order.antisym [order add eqI: order "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
-
-declare eq_refl [order add eqD1: order "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
-
-declare sym [THEN eq_refl, order add eqD2: order "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
+lemma nless_le: "(\<not> a < b) \<longleftrightarrow> (\<not> a \<le> b) \<or> a = b"
+  using local.dual_order.order_iff_strict by blast
 
-declare less_trans [order add less_trans: order "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
-
-declare less_le_trans [order add less_le_trans: order "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
-
-declare le_less_trans [order add le_less_trans: order "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
-
-declare order_trans [order add le_trans: order "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
-
-declare le_neq_trans [order add le_neq_trans: order "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
-
-declare neq_le_trans [order add neq_le_trans: order "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
-
-declare less_imp_neq [order add less_imp_neq: order "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
-
-declare eq_neq_eq_imp_neq [order add eq_neq_eq_imp_neq: order "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
-
-declare not_sym [order add not_sym: order "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
+local_setup \<open>
+  HOL_Order_Tac.declare_order {
+    ops = {eq = @{term \<open>(=) :: 'a \<Rightarrow> 'a \<Rightarrow> bool\<close>}, le = @{term \<open>(\<le>)\<close>}, lt = @{term \<open>(<)\<close>}},
+    thms = {trans = @{thm order_trans}, refl = @{thm order_refl}, eqD1 = @{thm eq_refl},
+            eqD2 = @{thm eq_refl[OF sym]}, antisym = @{thm order_antisym}, contr = @{thm notE}},
+    conv_thms = {less_le = @{thm eq_reflection[OF less_le]},
+                 nless_le = @{thm eq_reflection[OF nless_le]}}
+  }
+\<close>
 
 end
 
 context linorder
 begin
 
-declare [[order del: order "(=) :: 'a => 'a => bool" "(<=)" "(<)"]]
-
-declare less_irrefl [THEN notE, order add less_reflE: linorder "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
-
-declare order_refl [order add le_refl: linorder "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
-
-declare less_imp_le [order add less_imp_le: linorder "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
-
-declare not_less [THEN iffD2, order add not_lessI: linorder "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
-
-declare not_le [THEN iffD2, order add not_leI: linorder "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
-
-declare not_less [THEN iffD1, order add not_lessD: linorder "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
-
-declare not_le [THEN iffD1, order add not_leD: linorder "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
-
-declare order.antisym [order add eqI: linorder "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
-
-declare eq_refl [order add eqD1: linorder "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
+lemma nle_le: "(\<not> a \<le> b) \<longleftrightarrow> b \<le> a \<and> b \<noteq> a"
+  using not_le less_le by simp
 
-declare sym [THEN eq_refl, order add eqD2: linorder "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
-
-declare less_trans [order add less_trans: linorder "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
-
-declare less_le_trans [order add less_le_trans: linorder "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
-
-declare le_less_trans [order add le_less_trans: linorder "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
-
-declare order_trans [order add le_trans: linorder "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
-
-declare le_neq_trans [order add le_neq_trans: linorder "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
-
-declare neq_le_trans [order add neq_le_trans: linorder "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
-
-declare less_imp_neq [order add less_imp_neq: linorder "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
-
-declare eq_neq_eq_imp_neq [order add eq_neq_eq_imp_neq: linorder "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
-
-declare not_sym [order add not_sym: linorder "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
+local_setup \<open>
+  HOL_Order_Tac.declare_linorder {
+    ops = {eq = @{term \<open>(=) :: 'a \<Rightarrow> 'a \<Rightarrow> bool\<close>}, le = @{term \<open>(\<le>)\<close>}, lt = @{term \<open>(<)\<close>}},
+    thms = {trans = @{thm order_trans}, refl = @{thm order_refl}, eqD1 = @{thm eq_refl},
+            eqD2 = @{thm eq_refl[OF sym]}, antisym = @{thm order_antisym}, contr = @{thm notE}},
+    conv_thms = {less_le = @{thm eq_reflection[OF less_le]},
+                 nless_le = @{thm eq_reflection[OF not_less]},
+                 nle_le = @{thm eq_reflection[OF nle_le]}}
+  }
+\<close>
 
 end
 
 setup \<open>
   map_theory_simpset (fn ctxt0 => ctxt0 addSolver
-    mk_solver "Transitivity" (fn ctxt => Orders.order_tac ctxt (Simplifier.prems_of ctxt)))
-  (*Adding the transitivity reasoners also as safe solvers showed a slight
-    speed up, but the reasoning strength appears to be not higher (at least
-    no breaking of additional proofs in the entire HOL distribution, as
-    of 5 March 2004, was observed).*)
+    mk_solver "Transitivity" (fn ctxt => HOL_Order_Tac.tac (Simplifier.prems_of ctxt) ctxt))
 \<close>
 
 ML \<open>
@@ -765,7 +661,7 @@
               | SOME thm => SOME (mk_meta_eq(thm RS @{thm linorder_class.antisym_conv3})))
             end
         | SOME thm => SOME (mk_meta_eq (thm RS @{thm antisym_conv2})))
-      end handle THM _ => NONE)
+      end handle THM _ => NONE)                           
   | _ => NONE);
 
 end;
@@ -1226,6 +1122,7 @@
     case False with \<open>x \<le> y\<close> have "x < y" by simp
     with assms strict_monoD have "f x < f y" by auto
     then show ?thesis by simp
+
   qed
 qed
 
diff -r 419edc7f3726 -r c72fd8f1fceb src/Provers/order.ML
--- a/src/Provers/order.ML	Wed Mar 31 23:45:16 2021 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,1264 +0,0 @@
-(*  Title:      Provers/order.ML
-    Author:     Oliver Kutter, TU Muenchen
-
-Transitivity reasoner for partial and linear orders.
-*)
-
-(* TODO: reduce number of input thms *)
-
-(*
-
-The package provides tactics partial_tac and linear_tac that use all
-premises of the form
-
-  t = u, t ~= u, t < u, t <= u, ~(t < u) and ~(t <= u)
-
-to
-1. either derive a contradiction,
-   in which case the conclusion can be any term,
-2. or prove the conclusion, which must be of the same form as the
-   premises (excluding ~(t < u) and ~(t <= u) for partial orders)
-
-The package is not limited to the relation <= and friends.  It can be
-instantiated to any partial and/or linear order --- for example, the
-divisibility relation "dvd".  In order to instantiate the package for
-a partial order only, supply dummy theorems to the rules for linear
-orders, and don't use linear_tac!
-
-*)
-
-signature ORDER_TAC =
-sig
-  (* Theorems required by the reasoner *)
-  type less_arith
-  val empty : thm -> less_arith
-  val update : string -> thm -> less_arith -> less_arith
-
-  (* Tactics *)
-  val partial_tac:
-    (theory -> term -> (term * string * term) option) -> less_arith ->
-    Proof.context -> thm list -> int -> tactic
-  val linear_tac:
-    (theory -> term -> (term * string * term) option) -> less_arith ->
-    Proof.context -> thm list -> int -> tactic
-end;
-
-structure Order_Tac: ORDER_TAC =
-struct
-
-(* Record to handle input theorems in a convenient way. *)
-
-type less_arith =
-  {
-    (* Theorems for partial orders *)
-    less_reflE: thm,  (* x < x ==> P *)
-    le_refl: thm,  (* x <= x *)
-    less_imp_le: thm, (* x < y ==> x <= y *)
-    eqI: thm, (* [| x <= y; y <= x |] ==> x = y *)
-    eqD1: thm, (* x = y ==> x <= y *)
-    eqD2: thm, (* x = y ==> y <= x *)
-    less_trans: thm,  (* [| x < y; y < z |] ==> x < z *)
-    less_le_trans: thm,  (* [| x < y; y <= z |] ==> x < z *)
-    le_less_trans: thm,  (* [| x <= y; y < z |] ==> x < z *)
-    le_trans: thm,  (* [| x <= y; y <= z |] ==> x <= z *)
-    le_neq_trans : thm, (* [| x <= y ; x ~= y |] ==> x < y *)
-    neq_le_trans : thm, (* [| x ~= y ; x <= y |] ==> x < y *)
-    not_sym : thm, (* x ~= y ==> y ~= x *)
-
-    (* Additional theorems for linear orders *)
-    not_lessD: thm, (* ~(x < y) ==> y <= x *)
-    not_leD: thm, (* ~(x <= y) ==> y < x *)
-    not_lessI: thm, (* y <= x  ==> ~(x < y) *)
-    not_leI: thm, (* y < x  ==> ~(x <= y) *)
-
-    (* Additional theorems for subgoals of form x ~= y *)
-    less_imp_neq : thm, (* x < y ==> x ~= y *)
-    eq_neq_eq_imp_neq : thm (* [| x = u ; u ~= v ; v = z|] ==> x ~= z *)
-  }
-
-fun empty dummy_thm =
-    {less_reflE= dummy_thm, le_refl= dummy_thm, less_imp_le= dummy_thm, eqI= dummy_thm,
-      eqD1= dummy_thm, eqD2= dummy_thm,
-      less_trans= dummy_thm, less_le_trans= dummy_thm, le_less_trans= dummy_thm,
-      le_trans= dummy_thm, le_neq_trans = dummy_thm, neq_le_trans = dummy_thm,
-      not_sym = dummy_thm,
-      not_lessD= dummy_thm, not_leD= dummy_thm, not_lessI= dummy_thm, not_leI= dummy_thm,
-      less_imp_neq = dummy_thm, eq_neq_eq_imp_neq = dummy_thm}
-
-fun change thms f =
-  let
-    val {less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans,
-      less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans,
-      not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq,
-      eq_neq_eq_imp_neq} = thms;
-    val (less_reflE', le_refl', less_imp_le', eqI', eqD1', eqD2', less_trans',
-      less_le_trans', le_less_trans', le_trans', le_neq_trans', neq_le_trans',
-      not_sym', not_lessD', not_leD', not_lessI', not_leI', less_imp_neq',
-      eq_neq_eq_imp_neq') =
-     f (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans,
-      less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans,
-      not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq,
-      eq_neq_eq_imp_neq)
-  in {less_reflE = less_reflE', le_refl= le_refl',
-      less_imp_le = less_imp_le', eqI = eqI', eqD1 = eqD1', eqD2 = eqD2',
-      less_trans = less_trans', less_le_trans = less_le_trans',
-      le_less_trans = le_less_trans', le_trans = le_trans', le_neq_trans = le_neq_trans',
-      neq_le_trans = neq_le_trans', not_sym = not_sym',
-      not_lessD = not_lessD', not_leD = not_leD', not_lessI = not_lessI',
-      not_leI = not_leI',
-      less_imp_neq = less_imp_neq', eq_neq_eq_imp_neq = eq_neq_eq_imp_neq'}
-  end;
-
-fun update "less_reflE" thm thms =
-    change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans,
-      less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans,
-      not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq,
-      eq_neq_eq_imp_neq) =>
-    (thm, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans,
-      less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans,
-      not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, eq_neq_eq_imp_neq))
-  | update "le_refl" thm thms =
-    change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans,
-      less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans,
-      not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq,
-      eq_neq_eq_imp_neq) =>
-    (less_reflE, thm, less_imp_le, eqI, eqD1, eqD2, less_trans,
-      less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans,
-      not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, eq_neq_eq_imp_neq))
-  | update "less_imp_le" thm thms =
-    change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans,
-      less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans,
-      not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq,
-      eq_neq_eq_imp_neq) =>
-    (less_reflE, le_refl, thm, eqI, eqD1, eqD2, less_trans,
-      less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans,
-      not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, eq_neq_eq_imp_neq))
-  | update "eqI" thm thms =
-    change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans,
-      less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans,
-      not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq,
-      eq_neq_eq_imp_neq) =>
-    (less_reflE, le_refl, less_imp_le, thm, eqD1, eqD2, less_trans,
-      less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans,
-      not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, eq_neq_eq_imp_neq))
-  | update "eqD1" thm thms =
-    change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans,
-      less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans,
-      not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq,
-      eq_neq_eq_imp_neq) =>
-    (less_reflE, le_refl, less_imp_le, eqI, thm, eqD2, less_trans,
-      less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans,
-      not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, eq_neq_eq_imp_neq))
-  | update "eqD2" thm thms =
-    change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans,
-      less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans,
-      not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq,
-      eq_neq_eq_imp_neq) =>
-    (less_reflE, le_refl, less_imp_le, eqI, eqD1, thm, less_trans,
-      less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans,
-      not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, eq_neq_eq_imp_neq))
-  | update "less_trans" thm thms =
-    change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans,
-      less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans,
-      not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq,
-      eq_neq_eq_imp_neq) =>
-    (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, thm,
-      less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans,
-      not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, eq_neq_eq_imp_neq))
-  | update "less_le_trans" thm thms =
-    change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans,
-      less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans,
-      not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq,
-      eq_neq_eq_imp_neq) =>
-    (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans,
-      thm, le_less_trans, le_trans, le_neq_trans, neq_le_trans,
-      not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, eq_neq_eq_imp_neq))
-  | update "le_less_trans" thm thms =
-    change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans,
-      less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans,
-      not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq,
-      eq_neq_eq_imp_neq) =>
-    (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans,
-      less_le_trans, thm, le_trans, le_neq_trans, neq_le_trans,
-      not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, eq_neq_eq_imp_neq))
-  | update "le_trans" thm thms =
-    change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans,
-      less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans,
-      not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq,
-      eq_neq_eq_imp_neq) =>
-    (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans,
-      less_le_trans, le_less_trans, thm, le_neq_trans, neq_le_trans,
-      not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, eq_neq_eq_imp_neq))
-  | update "le_neq_trans" thm thms =
-    change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans,
-      less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans,
-      not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq,
-      eq_neq_eq_imp_neq) =>
-    (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans,
-      less_le_trans, le_less_trans, le_trans, thm, neq_le_trans,
-      not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, eq_neq_eq_imp_neq))
-  | update "neq_le_trans" thm thms =
-    change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans,
-      less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans,
-      not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq,
-      eq_neq_eq_imp_neq) =>
-    (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans,
-      less_le_trans, le_less_trans, le_trans, le_neq_trans, thm,
-      not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, eq_neq_eq_imp_neq))
-  | update "not_sym" thm thms =
-    change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans,
-      less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans,
-      not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq,
-      eq_neq_eq_imp_neq) =>
-    (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans,
-      less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans,
-      thm, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, eq_neq_eq_imp_neq))
-  | update "not_lessD" thm thms =
-    change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans,
-      less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans,
-      not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq,
-      eq_neq_eq_imp_neq) =>
-    (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans,
-      less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans,
-      not_sym, thm, not_leD, not_lessI, not_leI, less_imp_neq, eq_neq_eq_imp_neq))
-  | update "not_leD" thm thms =
-    change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans,
-      less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans,
-      not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq,
-      eq_neq_eq_imp_neq) =>
-    (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans,
-      less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans,
-      not_sym, not_lessD, thm, not_lessI, not_leI, less_imp_neq, eq_neq_eq_imp_neq))
-  | update "not_lessI" thm thms =
-    change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans,
-      less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans,
-      not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq,
-      eq_neq_eq_imp_neq) =>
-    (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans,
-      less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans,
-      not_sym, not_lessD, not_leD, thm, not_leI, less_imp_neq, eq_neq_eq_imp_neq))
-  | update "not_leI" thm thms =
-    change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans,
-      less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans,
-      not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq,
-      eq_neq_eq_imp_neq) =>
-    (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans,
-      less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans,
-      not_sym, not_lessD, not_leD, not_lessI, thm, less_imp_neq, eq_neq_eq_imp_neq))
-  | update "less_imp_neq" thm thms =
-    change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans,
-      less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans,
-      not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq,
-      eq_neq_eq_imp_neq) =>
-    (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans,
-      less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans,
-      not_sym, not_lessD, not_leD, not_lessI, not_leI, thm, eq_neq_eq_imp_neq))
-  | update "eq_neq_eq_imp_neq" thm thms =
-    change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans,
-      less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans,
-      not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq,
-      eq_neq_eq_imp_neq) =>
-    (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans,
-      less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans,
-      not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, thm));
-
-(* Internal datatype for the proof *)
-datatype proof
-  = Asm of int
-  | Thm of proof list * thm;
-
-exception Cannot;
- (* Internal exception, raised if conclusion cannot be derived from
-     assumptions. *)
-exception Contr of proof;
-  (* Internal exception, raised if contradiction ( x < x ) was derived *)
-
-fun prove asms =
-  let
-    fun pr (Asm i) = nth asms i
-      | pr (Thm (prfs, thm)) = map pr prfs MRS thm;
-  in pr end;
-
-(* Internal datatype for inequalities *)
-datatype less
-   = Less  of term * term * proof
-   | Le    of term * term * proof
-   | NotEq of term * term * proof;
-
-(* Misc functions for datatype less *)
-fun lower (Less (x, _, _)) = x
-  | lower (Le (x, _, _)) = x
-  | lower (NotEq (x,_,_)) = x;
-
-fun upper (Less (_, y, _)) = y
-  | upper (Le (_, y, _)) = y
-  | upper (NotEq (_,y,_)) = y;
-
-fun getprf   (Less (_, _, p)) = p
-|   getprf   (Le   (_, _, p)) = p
-|   getprf   (NotEq (_,_, p)) = p;
-
-
-(* ************************************************************************ *)
-(*                                                                          *)
-(* mkasm_partial                                                            *)
-(*                                                                          *)
-(* Tuple (t, n) (t an assumption, n its index in the assumptions) is        *)
-(* translated to an element of type less.                                   *)
-(* Partial orders only.                                                     *)
-(*                                                                          *)
-(* ************************************************************************ *)
-
-fun mkasm_partial decomp (less_thms : less_arith) sign (n, t) =
-  case decomp sign t of
-    SOME (x, rel, y) => (case rel of
-      "<"   => if (x aconv y) then raise Contr (Thm ([Asm n], #less_reflE less_thms))
-               else [Less (x, y, Asm n)]
-    | "~<"  => []
-    | "<="  => [Le (x, y, Asm n)]
-    | "~<=" => []
-    | "="   => [Le (x, y, Thm ([Asm n], #eqD1 less_thms)),
-                Le (y, x, Thm ([Asm n], #eqD2 less_thms))]
-    | "~="  => if (x aconv y) then
-                  raise Contr (Thm ([(Thm ([(Thm ([], #le_refl less_thms)) ,(Asm n)], #le_neq_trans less_thms))], #less_reflE less_thms))
-               else [ NotEq (x, y, Asm n),
-                      NotEq (y, x,Thm ( [Asm n], #not_sym less_thms))]
-    | _     => error ("partial_tac: unknown relation symbol ``" ^ rel ^
-                 "''returned by decomp."))
-  | NONE => [];
-
-(* ************************************************************************ *)
-(*                                                                          *)
-(* mkasm_linear                                                             *)
-(*                                                                          *)
-(* Tuple (t, n) (t an assumption, n its index in the assumptions) is        *)
-(* translated to an element of type less.                                   *)
-(* Linear orders only.                                                      *)
-(*                                                                          *)
-(* ************************************************************************ *)
-
-fun mkasm_linear decomp (less_thms : less_arith) sign (n, t) =
-  case decomp sign t of
-    SOME (x, rel, y) => (case rel of
-      "<"   => if (x aconv y) then raise Contr (Thm ([Asm n], #less_reflE less_thms))
-               else [Less (x, y, Asm n)]
-    | "~<"  => [Le (y, x, Thm ([Asm n], #not_lessD less_thms))]
-    | "<="  => [Le (x, y, Asm n)]
-    | "~<=" => if (x aconv y) then
-                  raise (Contr (Thm ([Thm ([Asm n], #not_leD less_thms)], #less_reflE less_thms)))
-               else [Less (y, x, Thm ([Asm n], #not_leD less_thms))]
-    | "="   => [Le (x, y, Thm ([Asm n], #eqD1 less_thms)),
-                Le (y, x, Thm ([Asm n], #eqD2 less_thms))]
-    | "~="  => if (x aconv y) then
-                  raise Contr (Thm ([(Thm ([(Thm ([], #le_refl less_thms)) ,(Asm n)], #le_neq_trans less_thms))], #less_reflE less_thms))
-               else [ NotEq (x, y, Asm n),
-                      NotEq (y, x,Thm ( [Asm n], #not_sym less_thms))]
-    | _     => error ("linear_tac: unknown relation symbol ``" ^ rel ^
-                 "''returned by decomp."))
-  | NONE => [];
-
-(* ************************************************************************ *)
-(*                                                                          *)
-(* mkconcl_partial                                                          *)
-(*                                                                          *)
-(* Translates conclusion t to an element of type less.                      *)
-(* Partial orders only.                                                     *)
-(*                                                                          *)
-(* ************************************************************************ *)
-
-fun mkconcl_partial decomp (less_thms : less_arith) sign t =
-  case decomp sign t of
-    SOME (x, rel, y) => (case rel of
-      "<"   => ([Less (x, y, Asm ~1)], Asm 0)
-    | "<="  => ([Le (x, y, Asm ~1)], Asm 0)
-    | "="   => ([Le (x, y, Asm ~1), Le (y, x, Asm ~1)],
-                 Thm ([Asm 0, Asm 1], #eqI less_thms))
-    | "~="  => ([NotEq (x,y, Asm ~1)], Asm 0)
-    | _  => raise Cannot)
-  | NONE => raise Cannot;
-
-(* ************************************************************************ *)
-(*                                                                          *)
-(* mkconcl_linear                                                           *)
-(*                                                                          *)
-(* Translates conclusion t to an element of type less.                      *)
-(* Linear orders only.                                                      *)
-(*                                                                          *)
-(* ************************************************************************ *)
-
-fun mkconcl_linear decomp (less_thms : less_arith) sign t =
-  case decomp sign t of
-    SOME (x, rel, y) => (case rel of
-      "<"   => ([Less (x, y, Asm ~1)], Asm 0)
-    | "~<"  => ([Le (y, x, Asm ~1)], Thm ([Asm 0], #not_lessI less_thms))
-    | "<="  => ([Le (x, y, Asm ~1)], Asm 0)
-    | "~<=" => ([Less (y, x, Asm ~1)], Thm ([Asm 0], #not_leI less_thms))
-    | "="   => ([Le (x, y, Asm ~1), Le (y, x, Asm ~1)],
-                 Thm ([Asm 0, Asm 1], #eqI less_thms))
-    | "~="  => ([NotEq (x,y, Asm ~1)], Asm 0)
-    | _  => raise Cannot)
-  | NONE => raise Cannot;
-
-
-(*** The common part for partial and linear orders ***)
-
-(* Analysis of premises and conclusion: *)
-(* decomp (`x Rel y') should yield (x, Rel, y)
-     where Rel is one of "<", "<=", "~<", "~<=", "=" and "~=",
-     other relation symbols cause an error message *)
-
-fun gen_order_tac mkasm mkconcl decomp' (less_thms : less_arith) ctxt prems =
-
-let
-
-fun decomp sign t = Option.map (fn (x, rel, y) =>
-  (Envir.beta_eta_contract x, rel, Envir.beta_eta_contract y)) (decomp' sign t);
-
-(* ******************************************************************* *)
-(*                                                                     *)
-(* mergeLess                                                           *)
-(*                                                                     *)
-(* Merge two elements of type less according to the following rules    *)
-(*                                                                     *)
-(* x <  y && y <  z ==> x < z                                          *)
-(* x <  y && y <= z ==> x < z                                          *)
-(* x <= y && y <  z ==> x < z                                          *)
-(* x <= y && y <= z ==> x <= z                                         *)
-(* x <= y && x ~= y ==> x < y                                          *)
-(* x ~= y && x <= y ==> x < y                                          *)
-(* x <  y && x ~= y ==> x < y                                          *)
-(* x ~= y && x <  y ==> x < y                                          *)
-(*                                                                     *)
-(* ******************************************************************* *)
-
-fun mergeLess (Less (x, _, p) , Less (_ , z, q)) =
-      Less (x, z, Thm ([p,q] , #less_trans less_thms))
-|   mergeLess (Less (x, _, p) , Le (_ , z, q)) =
-      Less (x, z, Thm ([p,q] , #less_le_trans less_thms))
-|   mergeLess (Le (x, _, p) , Less (_ , z, q)) =
-      Less (x, z, Thm ([p,q] , #le_less_trans less_thms))
-|   mergeLess (Le (x, z, p) , NotEq (x', z', q)) =
-      if (x aconv x' andalso z aconv z' )
-      then Less (x, z, Thm ([p,q] , #le_neq_trans less_thms))
-      else error "linear/partial_tac: internal error le_neq_trans"
-|   mergeLess (NotEq (x, z, p) , Le (x' , z', q)) =
-      if (x aconv x' andalso z aconv z')
-      then Less (x, z, Thm ([p,q] , #neq_le_trans less_thms))
-      else error "linear/partial_tac: internal error neq_le_trans"
-|   mergeLess (NotEq (x, z, p) , Less (x' , z', q)) =
-      if (x aconv x' andalso z aconv z')
-      then Less ((x' , z', q))
-      else error "linear/partial_tac: internal error neq_less_trans"
-|   mergeLess (Less (x, z, p) , NotEq (x', z', q)) =
-      if (x aconv x' andalso z aconv z')
-      then Less (x, z, p)
-      else error "linear/partial_tac: internal error less_neq_trans"
-|   mergeLess (Le (x, _, p) , Le (_ , z, q)) =
-      Le (x, z, Thm ([p,q] , #le_trans less_thms))
-|   mergeLess (_, _) =
-      error "linear/partial_tac: internal error: undefined case";
-
-
-(* ******************************************************************** *)
-(* tr checks for valid transitivity step                                *)
-(* ******************************************************************** *)
-
-infix tr;
-fun (Less (_, y, _)) tr (Le (x', _, _))   = ( y aconv x' )
-  | (Le   (_, y, _)) tr (Less (x', _, _)) = ( y aconv x' )
-  | (Less (_, y, _)) tr (Less (x', _, _)) = ( y aconv x' )
-  | (Le (_, y, _))   tr (Le (x', _, _))   = ( y aconv x' )
-  | _ tr _ = false;
-
-
-(* ******************************************************************* *)
-(*                                                                     *)
-(* transPath (Lesslist, Less): (less list * less) -> less              *)
-(*                                                                     *)
-(* If a path represented by a list of elements of type less is found,  *)
-(* this needs to be contracted to a single element of type less.       *)
-(* Prior to each transitivity step it is checked whether the step is   *)
-(* valid.                                                              *)
-(*                                                                     *)
-(* ******************************************************************* *)
-
-fun transPath ([],lesss) = lesss
-|   transPath (x::xs,lesss) =
-      if lesss tr x then transPath (xs, mergeLess(lesss,x))
-      else error "linear/partial_tac: internal error transpath";
-
-(* ******************************************************************* *)
-(*                                                                     *)
-(* less1 subsumes less2 : less -> less -> bool                         *)
-(*                                                                     *)
-(* subsumes checks whether less1 implies less2                         *)
-(*                                                                     *)
-(* ******************************************************************* *)
-
-infix subsumes;
-fun (Less (x, y, _)) subsumes (Le (x', y', _)) =
-      (x aconv x' andalso y aconv y')
-  | (Less (x, y, _)) subsumes (Less (x', y', _)) =
-      (x aconv x' andalso y aconv y')
-  | (Le (x, y, _)) subsumes (Le (x', y', _)) =
-      (x aconv x' andalso y aconv y')
-  | (Less (x, y, _)) subsumes (NotEq (x', y', _)) =
-      (x aconv x' andalso y aconv y') orelse (y aconv x' andalso x aconv y')
-  | (NotEq (x, y, _)) subsumes (NotEq (x', y', _)) =
-      (x aconv x' andalso y aconv y') orelse (y aconv x' andalso x aconv y')
-  | (Le _) subsumes (Less _) =
-      error "linear/partial_tac: internal error: Le cannot subsume Less"
-  | _ subsumes _ = false;
-
-(* ******************************************************************* *)
-(*                                                                     *)
-(* triv_solv less1 : less ->  proof option                     *)
-(*                                                                     *)
-(* Solves trivial goal x <= x.                                         *)
-(*                                                                     *)
-(* ******************************************************************* *)
-
-fun triv_solv (Le (x, x', _)) =
-    if x aconv x' then  SOME (Thm ([], #le_refl less_thms))
-    else NONE
-|   triv_solv _ = NONE;
-
-(* ********************************************************************* *)
-(* Graph functions                                                       *)
-(* ********************************************************************* *)
-
-
-
-(* ******************************************************************* *)
-(*                                                                     *)
-(* General:                                                            *)
-(*                                                                     *)
-(* Inequalities are represented by various types of graphs.            *)
-(*                                                                     *)
-(* 1. (Term.term * (Term.term * less) list) list                       *)
-(*    - Graph of this type is generated from the assumptions,          *)
-(*      it does contain information on which edge stems from which     *)
-(*      assumption.                                                    *)
-(*    - Used to compute strongly connected components                  *)
-(*    - Used to compute component subgraphs                            *)
-(*    - Used for component subgraphs to reconstruct paths in components*)
-(*                                                                     *)
-(* 2. (int * (int * less) list ) list                                  *)
-(*    - Graph of this type is generated from the strong components of  *)
-(*      graph of type 1.  It consists of the strong components of      *)
-(*      graph 1, where nodes are indices of the components.            *)
-(*      Only edges between components are part of this graph.          *)
-(*    - Used to reconstruct paths between several components.          *)
-(*                                                                     *)
-(* ******************************************************************* *)
-
-
-(* *********************************************************** *)
-(* Functions for constructing graphs                           *)
-(* *********************************************************** *)
-
-fun addEdge (v,d,[]) = [(v,d)]
-|   addEdge (v,d,((u,dl)::el)) = if v aconv u then ((v,d@dl)::el)
-    else (u,dl):: (addEdge(v,d,el));
-
-(* ********************************************************************* *)
-(*                                                                       *)
-(* mkGraphs constructs from a list of objects of type less a graph g,    *)
-(* by taking all edges that are candidate for a <=, and a list neqE, by  *)
-(* taking all edges that are candiate for a ~=                           *)
-(*                                                                       *)
-(* ********************************************************************* *)
-
-fun mkGraphs [] = ([],[],[])
-|   mkGraphs lessList =
- let
-
-fun buildGraphs ([],leqG,neqG,neqE) = (leqG, neqG, neqE)
-|   buildGraphs (l::ls, leqG,neqG, neqE) = case l of
-  (Less (x,y,p)) =>
-       buildGraphs (ls, addEdge (x,[(y,(Less (x, y, p)))],leqG) ,
-                        addEdge (x,[(y,(Less (x, y, p)))],neqG), l::neqE)
-| (Le (x,y,p)) =>
-      buildGraphs (ls, addEdge (x,[(y,(Le (x, y,p)))],leqG) , neqG, neqE)
-| (NotEq  (x,y,p)) =>
-      buildGraphs (ls, leqG , addEdge (x,[(y,(NotEq (x, y, p)))],neqG), l::neqE) ;
-
-  in buildGraphs (lessList, [], [], []) end;
-
-
-(* *********************************************************************** *)
-(*                                                                         *)
-(* adjacent g u : (''a * 'b list ) list -> ''a -> 'b list                  *)
-(*                                                                         *)
-(* List of successors of u in graph g                                      *)
-(*                                                                         *)
-(* *********************************************************************** *)
-
-fun adjacent eq_comp ((v,adj)::el) u =
-    if eq_comp (u, v) then adj else adjacent eq_comp el u
-|   adjacent _  []  _ = []
-
-
-(* *********************************************************************** *)
-(*                                                                         *)
-(* transpose g:                                                            *)
-(* (''a * ''a list) list -> (''a * ''a list) list                          *)
-(*                                                                         *)
-(* Computes transposed graph g' from g                                     *)
-(* by reversing all edges u -> v to v -> u                                 *)
-(*                                                                         *)
-(* *********************************************************************** *)
-
-fun transpose eq_comp g =
-  let
-   (* Compute list of reversed edges for each adjacency list *)
-   fun flip (u,(v,l)::el) = (v,(u,l)) :: flip (u,el)
-     | flip (_,[]) = []
-
-   (* Compute adjacency list for node u from the list of edges
-      and return a likewise reduced list of edges.  The list of edges
-      is searches for edges starting from u, and these edges are removed. *)
-   fun gather (u,(v,w)::el) =
-    let
-     val (adj,edges) = gather (u,el)
-    in
-     if eq_comp (u, v) then (w::adj,edges)
-     else (adj,(v,w)::edges)
-    end
-   | gather (_,[]) = ([],[])
-
-   (* For every node in the input graph, call gather to find all reachable
-      nodes in the list of edges *)
-   fun assemble ((u,_)::el) edges =
-       let val (adj,edges) = gather (u,edges)
-       in (u,adj) :: assemble el edges
-       end
-     | assemble [] _ = []
-
-   (* Compute, for each adjacency list, the list with reversed edges,
-      and concatenate these lists. *)
-   val flipped = maps flip g
-
- in assemble g flipped end
-
-(* *********************************************************************** *)
-(*                                                                         *)
-(* scc_term : (term * term list) list -> term list list                    *)
-(*                                                                         *)
-(* The following is based on the algorithm for finding strongly connected  *)
-(* components described in Introduction to Algorithms, by Cormon, Leiserson*)
-(* and Rivest, section 23.5. The input G is an adjacency list description  *)
-(* of a directed graph. The output is a list of the strongly connected     *)
-(* components (each a list of vertices).                                   *)
-(*                                                                         *)
-(*                                                                         *)
-(* *********************************************************************** *)
-
-fun scc_term G =
-     let
-  (* Ordered list of the vertices that DFS has finished with;
-     most recently finished goes at the head. *)
-  val finish : term list Unsynchronized.ref = Unsynchronized.ref []
-
-  (* List of vertices which have been visited. *)
-  val visited : term list Unsynchronized.ref = Unsynchronized.ref []
-
-  fun been_visited v = exists (fn w => w aconv v) (!visited)
-
-  (* Given the adjacency list rep of a graph (a list of pairs),
-     return just the first element of each pair, yielding the
-     vertex list. *)
-  val members = map (fn (v,_) => v)
-
-  (* Returns the nodes in the DFS tree rooted at u in g *)
-  fun dfs_visit g u : term list =
-      let
-   val _ = visited := u :: !visited
-   val descendents =
-       List.foldr (fn ((v,l),ds) => if been_visited v then ds
-            else v :: dfs_visit g v @ ds)
-        [] (adjacent (op aconv) g u)
-      in
-   finish := u :: !finish;
-   descendents
-      end
-     in
-
-  (* DFS on the graph; apply dfs_visit to each vertex in
-     the graph, checking first to make sure the vertex is
-     as yet unvisited. *)
-  List.app (fn u => if been_visited u then ()
-        else (dfs_visit G u; ()))  (members G);
-  visited := [];
-
-  (* We don't reset finish because its value is used by
-     foldl below, and it will never be used again (even
-     though dfs_visit will continue to modify it). *)
-
-  (* DFS on the transpose. The vertices returned by
-     dfs_visit along with u form a connected component. We
-     collect all the connected components together in a
-     list, which is what is returned. *)
-  fold (fn u => fn comps =>
-      if been_visited u then comps
-      else (u :: dfs_visit (transpose (op aconv) G) u) :: comps) (!finish) []
-end;
-
-
-(* *********************************************************************** *)
-(*                                                                         *)
-(* dfs_int_reachable g u:                                                  *)
-(* (int * int list) list -> int -> int list                                *)
-(*                                                                         *)
-(* Computes list of all nodes reachable from u in g.                       *)
-(*                                                                         *)
-(* *********************************************************************** *)
-
-fun dfs_int_reachable g u =
- let
-  (* List of vertices which have been visited. *)
-  val visited : int list Unsynchronized.ref = Unsynchronized.ref []
-
-  fun been_visited v = exists (fn w => w = v) (!visited)
-
-  fun dfs_visit g u : int list =
-      let
-   val _ = visited := u :: !visited
-   val descendents =
-       List.foldr (fn ((v,l),ds) => if been_visited v then ds
-            else v :: dfs_visit g v @ ds)
-        [] (adjacent (op =) g u)
-   in  descendents end
-
- in u :: dfs_visit g u end;
-
-
-fun indexNodes IndexComp =
-    maps (fn (index, comp) => (map (fn v => (v,index)) comp)) IndexComp;
-
-fun getIndex v [] = ~1
-|   getIndex v ((v',k)::vs) = if v aconv v' then k else getIndex v vs;
-
-
-
-(* *********************************************************************** *)
-(*                                                                         *)
-(* dfs eq_comp g u v:                                                       *)
-(* ('a * 'a -> bool) -> ('a  *( 'a * less) list) list ->                   *)
-(* 'a -> 'a -> (bool * ('a * less) list)                                   *)
-(*                                                                         *)
-(* Depth first search of v from u.                                         *)
-(* Returns (true, path(u, v)) if successful, otherwise (false, []).        *)
-(*                                                                         *)
-(* *********************************************************************** *)
-
-fun dfs eq_comp g u v =
- let
-    val pred = Unsynchronized.ref [];
-    val visited = Unsynchronized.ref [];
-
-    fun been_visited v = exists (fn w => eq_comp (w, v)) (!visited)
-
-    fun dfs_visit u' =
-    let val _ = visited := u' :: (!visited)
-
-    fun update (x,l) = let val _ = pred := (x,l) ::(!pred) in () end;
-
-    in if been_visited v then ()
-    else (List.app (fn (v',l) => if been_visited v' then () else (
-       update (v',l);
-       dfs_visit v'; ()) )) (adjacent eq_comp g u')
-     end
-  in
-    dfs_visit u;
-    if (been_visited v) then (true, (!pred)) else (false , [])
-  end;
-
-
-(* *********************************************************************** *)
-(*                                                                         *)
-(* completeTermPath u v g:                                                 *)
-(* Term.term -> Term.term -> (Term.term * (Term.term * less) list) list    *)
-(* -> less list                                                            *)
-(*                                                                         *)
-(* Complete the path from u to v in graph g.  Path search is performed     *)
-(* with dfs_term g u v.  This yields for each node v' its predecessor u'   *)
-(* and the edge u' -> v'.  Allows traversing graph backwards from v and    *)
-(* finding the path u -> v.                                                *)
-(*                                                                         *)
-(* *********************************************************************** *)
-
-
-fun completeTermPath u v g  =
-  let
-   val (found, tmp) =  dfs (op aconv) g u v ;
-   val pred = map snd tmp;
-
-   fun path x y  =
-      let
-
-      (* find predecessor u of node v and the edge u -> v *)
-
-      fun lookup v [] = raise Cannot
-      |   lookup v (e::es) = if (upper e) aconv v then e else lookup v es;
-
-      (* traverse path backwards and return list of visited edges *)
-      fun rev_path v =
-       let val l = lookup v pred
-           val u = lower l;
-       in
-        if u aconv x then [l]
-        else (rev_path u) @ [l]
-       end
-     in rev_path y end;
-
-  in
-  if found then (if u aconv v then [(Le (u, v, (Thm ([], #le_refl less_thms))))]
-  else path u v ) else raise Cannot
-end;
-
-
-(* *********************************************************************** *)
-(*                                                                         *)
-(* findProof (sccGraph, neqE, ntc, sccSubgraphs) subgoal:                  *)
-(*                                                                         *)
-(* (int * (int * less) list) list * less list *  (Term.term * int) list    *)
-(* * ((term * (term * less) list) list) list -> Less -> proof              *)
-(*                                                                         *)
-(* findProof constructs from graphs (sccGraph, sccSubgraphs) and neqE a    *)
-(* proof for subgoal.  Raises exception Cannot if this is not possible.    *)
-(*                                                                         *)
-(* *********************************************************************** *)
-
-fun findProof (sccGraph, neqE, ntc, sccSubgraphs) subgoal =
-let
-
- (* complete path x y from component graph *)
- fun completeComponentPath x y predlist =
-   let
-          val xi = getIndex x ntc
-          val yi = getIndex y ntc
-
-          fun lookup k [] =  raise Cannot
-          |   lookup k ((h: int,l)::us) = if k = h then l else lookup k us;
-
-          fun rev_completeComponentPath y' =
-           let val edge = lookup (getIndex y' ntc) predlist
-               val u = lower edge
-               val v = upper edge
-           in
-             if (getIndex u ntc) = xi then
-               completeTermPath x u (nth sccSubgraphs xi) @ [edge] @
-               completeTermPath v y' (nth sccSubgraphs (getIndex y' ntc))
-             else
-              rev_completeComponentPath u @ [edge] @
-                completeTermPath v y' (nth sccSubgraphs (getIndex y' ntc))
-           end
-   in
-     if x aconv y then
-       [(Le (x, y, (Thm ([], #le_refl less_thms))))]
-     else if xi = yi then completeTermPath x y (nth sccSubgraphs xi)
-     else rev_completeComponentPath y
-   end;
-
-(* ******************************************************************* *)
-(* findLess e x y xi yi xreachable yreachable                          *)
-(*                                                                     *)
-(* Find a path from x through e to y, of weight <                      *)
-(* ******************************************************************* *)
-
- fun findLess e x y xi yi xreachable yreachable =
-  let val u = lower e
-      val v = upper e
-      val ui = getIndex u ntc
-      val vi = getIndex v ntc
-
-  in
-      if member (op =) xreachable ui andalso member (op =) xreachable vi andalso
-         member (op =) yreachable ui andalso member (op =) yreachable vi then (
-
-  (case e of (Less (_, _, _)) =>
-       let
-        val (xufound, xupred) =  dfs (op =) sccGraph xi (getIndex u ntc)
-            in
-             if xufound then (
-              let
-               val (vyfound, vypred) =  dfs (op =) sccGraph (getIndex v ntc) yi
-              in
-               if vyfound then (
-                let
-                 val xypath = (completeComponentPath x u xupred)@[e]@(completeComponentPath v y vypred)
-                 val xyLesss = transPath (tl xypath, hd xypath)
-                in
-                 if xyLesss subsumes subgoal then SOME (getprf xyLesss)
-                 else NONE
-               end)
-               else NONE
-              end)
-             else NONE
-            end
-       |  _   =>
-         let val (uvfound, uvpred) =  dfs (op =) sccGraph (getIndex u ntc) (getIndex v ntc)
-             in
-              if uvfound then (
-               let
-                val (xufound, xupred) = dfs (op =) sccGraph xi (getIndex u ntc)
-               in
-                if xufound then (
-                 let
-                  val (vyfound, vypred) =  dfs (op =) sccGraph (getIndex v ntc) yi
-                 in
-                  if vyfound then (
-                   let
-                    val uvpath = completeComponentPath u v uvpred
-                    val uvLesss = mergeLess ( transPath (tl uvpath, hd uvpath), e)
-                    val xypath = (completeComponentPath  x u xupred)@[uvLesss]@(completeComponentPath v y vypred)
-                    val xyLesss = transPath (tl xypath, hd xypath)
-                   in
-                    if xyLesss subsumes subgoal then SOME (getprf xyLesss)
-                    else NONE
-                   end )
-                  else NONE
-                 end)
-                else NONE
-               end )
-              else NONE
-             end )
-    ) else NONE
-end;
-
-
-in
-  (* looking for x <= y: any path from x to y is sufficient *)
-  case subgoal of (Le (x, y, _)) => (
-  if null sccGraph then raise Cannot else (
-   let
-    val xi = getIndex x ntc
-    val yi = getIndex y ntc
-    (* searches in sccGraph a path from xi to yi *)
-    val (found, pred) = dfs (op =) sccGraph xi yi
-   in
-    if found then (
-       let val xypath = completeComponentPath x y pred
-           val xyLesss = transPath (tl xypath, hd xypath)
-       in
-          (case xyLesss of
-            (Less (_, _, q)) => if xyLesss subsumes subgoal then (Thm ([q], #less_imp_le less_thms))
-                                else raise Cannot
-             | _   => if xyLesss subsumes subgoal then (getprf xyLesss)
-                      else raise Cannot)
-       end )
-     else raise Cannot
-   end
-    )
-   )
- (* looking for x < y: particular path required, which is not necessarily
-    found by normal dfs *)
- |   (Less (x, y, _)) => (
-  if null sccGraph then raise Cannot else (
-   let
-    val xi = getIndex x ntc
-    val yi = getIndex y ntc
-    val sccGraph_transpose = transpose (op =) sccGraph
-    (* all components that can be reached from component xi  *)
-    val xreachable = dfs_int_reachable sccGraph xi
-    (* all comonents reachable from y in the transposed graph sccGraph' *)
-    val yreachable = dfs_int_reachable sccGraph_transpose yi
-    (* for all edges u ~= v or u < v check if they are part of path x < y *)
-    fun processNeqEdges [] = raise Cannot
-    |   processNeqEdges (e::es) =
-      case  (findLess e x y xi yi xreachable yreachable) of (SOME prf) => prf
-      | _ => processNeqEdges es
-
-    in
-       processNeqEdges neqE
-    end
-  )
- )
-| (NotEq (x, y, _)) => (
-  (* if there aren't any edges that are candidate for a ~= raise Cannot *)
-  if null neqE then raise Cannot
-  (* if there aren't any edges that are candidate for <= then just search a edge in neqE that implies the subgoal *)
-  else if null sccSubgraphs then (
-     (case (find_first (fn fact => fact subsumes subgoal) neqE, subgoal) of
-       ( SOME (NotEq (x, y, p)), NotEq (x', y', _)) =>
-          if  (x aconv x' andalso y aconv y') then p
-          else Thm ([p], #not_sym less_thms)
-     | ( SOME (Less (x, y, p)), NotEq (x', y', _)) =>
-          if x aconv x' andalso y aconv y' then (Thm ([p], #less_imp_neq less_thms))
-          else (Thm ([(Thm ([p], #less_imp_neq less_thms))], #not_sym less_thms))
-     | _ => raise Cannot)
-   ) else (
-
-   let  val xi = getIndex x ntc
-        val yi = getIndex y ntc
-        val sccGraph_transpose = transpose (op =) sccGraph
-        val xreachable = dfs_int_reachable sccGraph xi
-        val yreachable = dfs_int_reachable sccGraph_transpose yi
-
-        fun processNeqEdges [] = raise Cannot
-        |   processNeqEdges (e::es) = (
-            let val u = lower e
-                val v = upper e
-                val ui = getIndex u ntc
-                val vi = getIndex v ntc
-
-            in
-                (* if x ~= y follows from edge e *)
-                if e subsumes subgoal then (
-                     case e of (Less (u, v, q)) => (
-                       if u aconv x andalso v aconv y then (Thm ([q], #less_imp_neq less_thms))
-                       else (Thm ([(Thm ([q], #less_imp_neq less_thms))], #not_sym less_thms))
-                     )
-                     |    (NotEq (u,v, q)) => (
-                       if u aconv x andalso v aconv y then q
-                       else (Thm ([q],  #not_sym less_thms))
-                     )
-                 )
-                (* if SCC_x is linked to SCC_y via edge e *)
-                 else if ui = xi andalso vi = yi then (
-                   case e of (Less (_, _,_)) => (
-                        let
-                          val xypath =
-                            completeTermPath x u (nth sccSubgraphs ui) @ [e] @
-                            completeTermPath v y (nth sccSubgraphs vi)
-                          val xyLesss = transPath (tl xypath, hd xypath)
-                        in  (Thm ([getprf xyLesss], #less_imp_neq less_thms)) end)
-                   | _ => (
-                        let
-                            val xupath = completeTermPath x u (nth sccSubgraphs ui)
-                            val uxpath = completeTermPath u x (nth sccSubgraphs ui)
-                            val vypath = completeTermPath v y (nth sccSubgraphs vi)
-                            val yvpath = completeTermPath y v (nth sccSubgraphs vi)
-                            val xuLesss = transPath (tl xupath, hd xupath)
-                            val uxLesss = transPath (tl uxpath, hd uxpath)
-                            val vyLesss = transPath (tl vypath, hd vypath)
-                            val yvLesss = transPath (tl yvpath, hd yvpath)
-                            val x_eq_u =  (Thm ([(getprf xuLesss),(getprf uxLesss)], #eqI less_thms))
-                            val v_eq_y =  (Thm ([(getprf vyLesss),(getprf yvLesss)], #eqI less_thms))
-                        in
-                           (Thm ([x_eq_u , (getprf e), v_eq_y ], #eq_neq_eq_imp_neq less_thms))
-                        end
-                        )
-                  ) else if ui = yi andalso vi = xi then (
-                     case e of (Less (_, _,_)) => (
-                        let
-                          val xypath =
-                            completeTermPath y u (nth sccSubgraphs ui) @ [e] @
-                            completeTermPath v x (nth sccSubgraphs vi)
-                          val xyLesss = transPath (tl xypath, hd xypath)
-                        in (Thm ([(Thm ([getprf xyLesss], #less_imp_neq less_thms))] , #not_sym less_thms)) end )
-                     | _ => (
-
-                        let val yupath = completeTermPath y u (nth sccSubgraphs ui)
-                            val uypath = completeTermPath u y (nth sccSubgraphs ui)
-                            val vxpath = completeTermPath v x (nth sccSubgraphs vi)
-                            val xvpath = completeTermPath x v (nth sccSubgraphs vi)
-                            val yuLesss = transPath (tl yupath, hd yupath)
-                            val uyLesss = transPath (tl uypath, hd uypath)
-                            val vxLesss = transPath (tl vxpath, hd vxpath)
-                            val xvLesss = transPath (tl xvpath, hd xvpath)
-                            val y_eq_u =  (Thm ([(getprf yuLesss),(getprf uyLesss)], #eqI less_thms))
-                            val v_eq_x =  (Thm ([(getprf vxLesss),(getprf xvLesss)], #eqI less_thms))
-                        in
-                            (Thm ([(Thm ([y_eq_u , (getprf e), v_eq_x ], #eq_neq_eq_imp_neq less_thms))], #not_sym less_thms))
-                        end
-                       )
-                  ) else (
-                       (* there exists a path x < y or y < x such that
-                          x ~= y may be concluded *)
-                        case  (findLess e x y xi yi xreachable yreachable) of
-                              (SOME prf) =>  (Thm ([prf], #less_imp_neq less_thms))
-                             | NONE =>  (
-                               let
-                                val yr = dfs_int_reachable sccGraph yi
-                                val xr = dfs_int_reachable sccGraph_transpose xi
-                               in
-                                case  (findLess e y x yi xi yr xr) of
-                                      (SOME prf) => (Thm ([(Thm ([prf], #less_imp_neq less_thms))], #not_sym less_thms))
-                                      | _ => processNeqEdges es
-                               end)
-                 ) end)
-     in processNeqEdges neqE end)
-  )
-end;
-
-
-(* ******************************************************************* *)
-(*                                                                     *)
-(* mk_sccGraphs components leqG neqG ntc :                             *)
-(* Term.term list list ->                                              *)
-(* (Term.term * (Term.term * less) list) list ->                       *)
-(* (Term.term * (Term.term * less) list) list ->                       *)
-(* (Term.term * int)  list ->                                          *)
-(* (int * (int * less) list) list   *                                  *)
-(* ((Term.term * (Term.term * less) list) list) list                   *)
-(*                                                                     *)
-(*                                                                     *)
-(* Computes, from graph leqG, list of all its components and the list  *)
-(* ntc (nodes, index of component) a graph whose nodes are the         *)
-(* indices of the components of g.  Egdes of the new graph are         *)
-(* only the edges of g linking two components. Also computes for each  *)
-(* component the subgraph of leqG that forms this component.           *)
-(*                                                                     *)
-(* For each component SCC_i is checked if there exists a edge in neqG  *)
-(* that leads to a contradiction.                                      *)
-(*                                                                     *)
-(* We have a contradiction for edge u ~= v and u < v if:               *)
-(* - u and v are in the same component,                                *)
-(* that is, a path u <= v and a path v <= u exist, hence u = v.        *)
-(* From irreflexivity of < follows u < u or v < v. Ex false quodlibet. *)
-(*                                                                     *)
-(* ******************************************************************* *)
-
-fun mk_sccGraphs _ [] _ _ = ([],[])
-|   mk_sccGraphs components leqG neqG ntc =
-    let
-    (* Liste (Index der Komponente, Komponente *)
-    val IndexComp = map_index I components;
-
-
-    fun handleContr edge g =
-       (case edge of
-          (Less  (x, y, _)) => (
-            let
-             val xxpath = edge :: (completeTermPath y x g )
-             val xxLesss = transPath (tl xxpath, hd xxpath)
-             val q = getprf xxLesss
-            in
-             raise (Contr (Thm ([q], #less_reflE less_thms )))
-            end
-          )
-        | (NotEq (x, y, _)) => (
-            let
-             val xypath = (completeTermPath x y g )
-             val yxpath = (completeTermPath y x g )
-             val xyLesss = transPath (tl xypath, hd xypath)
-             val yxLesss = transPath (tl yxpath, hd yxpath)
-             val q = getprf (mergeLess ((mergeLess (edge, xyLesss)),yxLesss ))
-            in
-             raise (Contr (Thm ([q], #less_reflE less_thms )))
-            end
-         )
-        | _ =>  error "trans_tac/handleContr: invalid Contradiction");
-
-
-    (* k is index of the actual component *)
-
-    fun processComponent (k, comp) =
-     let
-        (* all edges with weight <= of the actual component *)
-        val leqEdges = maps (adjacent (op aconv) leqG) comp;
-        (* all edges with weight ~= of the actual component *)
-        val neqEdges = map snd (maps (adjacent (op aconv) neqG) comp);
-
-       (* find an edge leading to a contradiction *)
-       fun findContr [] = NONE
-       |   findContr (e::es) =
-                    let val ui = (getIndex (lower e) ntc)
-                        val vi = (getIndex (upper e) ntc)
-                    in
-                        if ui = vi then  SOME e
-                        else findContr es
-                    end;
-
-                (* sort edges into component internal edges and
-                   edges pointing away from the component *)
-                fun sortEdges  [] (intern,extern)  = (intern,extern)
-                |   sortEdges  ((v,l)::es) (intern, extern) =
-                    let val k' = getIndex v ntc in
-                        if k' = k then
-                            sortEdges es (l::intern, extern)
-                        else sortEdges  es (intern, (k',l)::extern) end;
-
-                (* Insert edge into sorted list of edges, where edge is
-                    only added if
-                    - it is found for the first time
-                    - it is a <= edge and no parallel < edge was found earlier
-                    - it is a < edge
-                 *)
-                 fun insert (h: int,l) [] = [(h,l)]
-                 |   insert (h,l) ((k',l')::es) = if h = k' then (
-                     case l of (Less (_, _, _)) => (h,l)::es
-                     | _  => (case l' of (Less (_, _, _)) => (h,l')::es
-                              | _ => (k',l)::es) )
-                     else (k',l'):: insert (h,l) es;
-
-                (* Reorganise list of edges such that
-                    - duplicate edges are removed
-                    - if a < edge and a <= edge exist at the same time,
-                      remove <= edge *)
-                 fun reOrganizeEdges [] sorted = sorted: (int * less) list
-                 |   reOrganizeEdges (e::es) sorted = reOrganizeEdges es (insert e sorted);
-
-                 (* construct the subgraph forming the strongly connected component
-                    from the edge list *)
-                 fun sccSubGraph [] g  = g
-                 |   sccSubGraph (l::ls) g =
-                          sccSubGraph ls (addEdge ((lower l),[((upper l),l)],g))
-
-                 val (intern, extern) = sortEdges leqEdges ([], []);
-                 val subGraph = sccSubGraph intern [];
-
-     in
-         case findContr neqEdges of SOME e => handleContr e subGraph
-         | _ => ((k, (reOrganizeEdges (extern) [])), subGraph)
-     end;
-
-    val tmp =  map processComponent IndexComp
-in
-     ( (map fst tmp), (map snd tmp))
-end;
-
-
-(** Find proof if possible. **)
-
-fun gen_solve mkconcl sign (asms, concl) =
- let
-  val (leqG, neqG, neqE) = mkGraphs asms
-  val components = scc_term leqG
-  val ntc = indexNodes (map_index I components)
-  val (sccGraph, sccSubgraphs) = mk_sccGraphs components leqG neqG ntc
- in
-   let
-   val (subgoals, prf) = mkconcl decomp less_thms sign concl
-   fun solve facts less =
-      (case triv_solv less of NONE => findProof (sccGraph, neqE, ntc, sccSubgraphs) less
-      | SOME prf => prf )
-  in
-   map (solve asms) subgoals
-  end
- end;
-
-in
- SUBGOAL (fn (A, n) => fn st =>
-  let
-   val thy = Proof_Context.theory_of ctxt;
-   val rfrees = map Free (Term.rename_wrt_term A (Logic.strip_params A));
-   val Hs =
-    map Thm.prop_of prems @
-    map (fn H => subst_bounds (rfrees, H)) (Logic.strip_assums_hyp A)
-   val C = subst_bounds (rfrees, Logic.strip_assums_concl A)
-   val lesss = flat (map_index (mkasm decomp less_thms thy) Hs)
-   val prfs = gen_solve mkconcl thy (lesss, C);
-   val (subgoals, prf) = mkconcl decomp less_thms thy C;
-  in
-   Subgoal.FOCUS (fn {context = ctxt', prems = asms, ...} =>
-     let val thms = map (prove (prems @ asms)) prfs
-     in resolve_tac ctxt' [prove thms prf] 1 end) ctxt n st
-  end
-  handle Contr p =>
-      (Subgoal.FOCUS (fn {context = ctxt', prems = asms, ...} =>
-          resolve_tac ctxt' [prove asms p] 1) ctxt n st
-        handle General.Subscript => Seq.empty)
-   | Cannot => Seq.empty
-   | General.Subscript => Seq.empty)
-end;
-
-(* partial_tac - solves partial orders *)
-val partial_tac = gen_order_tac mkasm_partial mkconcl_partial;
-
-(* linear_tac - solves linear/total orders *)
-val linear_tac = gen_order_tac mkasm_linear mkconcl_linear;
-
-end;
diff -r 419edc7f3726 -r c72fd8f1fceb src/Provers/order_procedure.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Provers/order_procedure.ML	Thu Apr 01 07:35:03 2021 +0200
@@ -0,0 +1,604 @@
+structure Order_Procedure : sig
+  datatype int = Int_of_integer of IntInf.int
+  val integer_of_int : int -> IntInf.int
+  datatype 'a fm = Atom of 'a | And of 'a fm * 'a fm | Or of 'a fm * 'a fm |
+    Neg of 'a fm
+  datatype trm = Const of string | App of trm * trm | Var of int
+  datatype prf_trm = PThm of string | Appt of prf_trm * trm |
+    AppP of prf_trm * prf_trm | AbsP of trm * prf_trm | Bound of trm |
+    Conv of trm * prf_trm * prf_trm
+  datatype o_atom = EQ of int * int | LEQ of int * int | LESS of int * int
+  val lo_contr_prf : (bool * o_atom) fm -> prf_trm option
+  val po_contr_prf : (bool * o_atom) fm -> prf_trm option
+end = struct
+
+datatype int = Int_of_integer of IntInf.int;
+
+fun integer_of_int (Int_of_integer k) = k;
+
+fun equal_inta k l = (((integer_of_int k) : IntInf.int) = (integer_of_int l));
+
+type 'a equal = {equal : 'a -> 'a -> bool};
+val equal = #equal : 'a equal -> 'a -> 'a -> bool;
+
+val equal_int = {equal = equal_inta} : int equal;
+
+fun less_eq_int k l = IntInf.<= (integer_of_int k, integer_of_int l);
+
+type 'a ord = {less_eq : 'a -> 'a -> bool, less : 'a -> 'a -> bool};
+val less_eq = #less_eq : 'a ord -> 'a -> 'a -> bool;
+val less = #less : 'a ord -> 'a -> 'a -> bool;
+
+fun less_int k l = IntInf.< (integer_of_int k, integer_of_int l);
+
+val ord_int = {less_eq = less_eq_int, less = less_int} : int ord;
+
+type 'a preorder = {ord_preorder : 'a ord};
+val ord_preorder = #ord_preorder : 'a preorder -> 'a ord;
+
+type 'a order = {preorder_order : 'a preorder};
+val preorder_order = #preorder_order : 'a order -> 'a preorder;
+
+val preorder_int = {ord_preorder = ord_int} : int preorder;
+
+val order_int = {preorder_order = preorder_int} : int order;
+
+type 'a linorder = {order_linorder : 'a order};
+val order_linorder = #order_linorder : 'a linorder -> 'a order;
+
+val linorder_int = {order_linorder = order_int} : int linorder;
+
+fun eq A_ a b = equal A_ a b;
+
+fun equal_proda A_ B_ (x1, x2) (y1, y2) = eq A_ x1 y1 andalso eq B_ x2 y2;
+
+fun equal_prod A_ B_ = {equal = equal_proda A_ B_} : ('a * 'b) equal;
+
+fun less_eq_prod A_ B_ (x1, y1) (x2, y2) =
+  less A_ x1 x2 orelse less_eq A_ x1 x2 andalso less_eq B_ y1 y2;
+
+fun less_prod A_ B_ (x1, y1) (x2, y2) =
+  less A_ x1 x2 orelse less_eq A_ x1 x2 andalso less B_ y1 y2;
+
+fun ord_prod A_ B_ = {less_eq = less_eq_prod A_ B_, less = less_prod A_ B_} :
+  ('a * 'b) ord;
+
+fun preorder_prod A_ B_ =
+  {ord_preorder = ord_prod (ord_preorder A_) (ord_preorder B_)} :
+  ('a * 'b) preorder;
+
+fun order_prod A_ B_ =
+  {preorder_order = preorder_prod (preorder_order A_) (preorder_order B_)} :
+  ('a * 'b) order;
+
+fun linorder_prod A_ B_ =
+  {order_linorder = order_prod (order_linorder A_) (order_linorder B_)} :
+  ('a * 'b) linorder;
+
+datatype nat = Zero_nat | Suc of nat;
+
+datatype color = R | B;
+
+datatype ('a, 'b) rbta = Empty |
+  Branch of color * ('a, 'b) rbta * 'a * 'b * ('a, 'b) rbta;
+
+datatype ('b, 'a) rbt = RBT of ('b, 'a) rbta;
+
+datatype 'a set = Set of 'a list | Coset of 'a list;
+
+datatype 'a fm = Atom of 'a | And of 'a fm * 'a fm | Or of 'a fm * 'a fm |
+  Neg of 'a fm;
+
+datatype trm = Const of string | App of trm * trm | Var of int;
+
+datatype prf_trm = PThm of string | Appt of prf_trm * trm |
+  AppP of prf_trm * prf_trm | AbsP of trm * prf_trm | Bound of trm |
+  Conv of trm * prf_trm * prf_trm;
+
+datatype ('a, 'b) mapping = Mapping of ('a, 'b) rbt;
+
+datatype o_atom = EQ of int * int | LEQ of int * int | LESS of int * int;
+
+fun id x = (fn xa => xa) x;
+
+fun impl_of B_ (RBT x) = x;
+
+fun folda f (Branch (c, lt, k, v, rt)) x = folda f rt (f k v (folda f lt x))
+  | folda f Empty x = x;
+
+fun fold A_ x xc = folda x (impl_of A_ xc);
+
+fun gen_keys kts (Branch (c, l, k, v, r)) = gen_keys ((k, r) :: kts) l
+  | gen_keys ((k, t) :: kts) Empty = k :: gen_keys kts t
+  | gen_keys [] Empty = [];
+
+fun keysb x = gen_keys [] x;
+
+fun keys A_ x = keysb (impl_of A_ x);
+
+fun maps f [] = []
+  | maps f (x :: xs) = f x @ maps f xs;
+
+fun empty A_ = RBT Empty;
+
+fun foldl f a [] = a
+  | foldl f a (x :: xs) = foldl f (f a x) xs;
+
+fun foldr f [] = id
+  | foldr f (x :: xs) = f x o foldr f xs;
+
+fun balance (Branch (R, a, w, x, b)) s t (Branch (R, c, y, z, d)) =
+  Branch (R, Branch (B, a, w, x, b), s, t, Branch (B, c, y, z, d))
+  | balance (Branch (R, Branch (R, a, w, x, b), s, t, c)) y z Empty =
+    Branch (R, Branch (B, a, w, x, b), s, t, Branch (B, c, y, z, Empty))
+  | balance (Branch (R, Branch (R, a, w, x, b), s, t, c)) y z
+    (Branch (B, va, vb, vc, vd)) =
+    Branch
+      (R, Branch (B, a, w, x, b), s, t,
+        Branch (B, c, y, z, Branch (B, va, vb, vc, vd)))
+  | balance (Branch (R, Empty, w, x, Branch (R, b, s, t, c))) y z Empty =
+    Branch (R, Branch (B, Empty, w, x, b), s, t, Branch (B, c, y, z, Empty))
+  | balance
+    (Branch (R, Branch (B, va, vb, vc, vd), w, x, Branch (R, b, s, t, c))) y z
+    Empty =
+    Branch
+      (R, Branch (B, Branch (B, va, vb, vc, vd), w, x, b), s, t,
+        Branch (B, c, y, z, Empty))
+  | balance (Branch (R, Empty, w, x, Branch (R, b, s, t, c))) y z
+    (Branch (B, va, vb, vc, vd)) =
+    Branch
+      (R, Branch (B, Empty, w, x, b), s, t,
+        Branch (B, c, y, z, Branch (B, va, vb, vc, vd)))
+  | balance
+    (Branch (R, Branch (B, ve, vf, vg, vh), w, x, Branch (R, b, s, t, c))) y z
+    (Branch (B, va, vb, vc, vd)) =
+    Branch
+      (R, Branch (B, Branch (B, ve, vf, vg, vh), w, x, b), s, t,
+        Branch (B, c, y, z, Branch (B, va, vb, vc, vd)))
+  | balance Empty w x (Branch (R, b, s, t, Branch (R, c, y, z, d))) =
+    Branch (R, Branch (B, Empty, w, x, b), s, t, Branch (B, c, y, z, d))
+  | balance (Branch (B, va, vb, vc, vd)) w x
+    (Branch (R, b, s, t, Branch (R, c, y, z, d))) =
+    Branch
+      (R, Branch (B, Branch (B, va, vb, vc, vd), w, x, b), s, t,
+        Branch (B, c, y, z, d))
+  | balance Empty w x (Branch (R, Branch (R, b, s, t, c), y, z, Empty)) =
+    Branch (R, Branch (B, Empty, w, x, b), s, t, Branch (B, c, y, z, Empty))
+  | balance Empty w x
+    (Branch (R, Branch (R, b, s, t, c), y, z, Branch (B, va, vb, vc, vd))) =
+    Branch
+      (R, Branch (B, Empty, w, x, b), s, t,
+        Branch (B, c, y, z, Branch (B, va, vb, vc, vd)))
+  | balance (Branch (B, va, vb, vc, vd)) w x
+    (Branch (R, Branch (R, b, s, t, c), y, z, Empty)) =
+    Branch
+      (R, Branch (B, Branch (B, va, vb, vc, vd), w, x, b), s, t,
+        Branch (B, c, y, z, Empty))
+  | balance (Branch (B, va, vb, vc, vd)) w x
+    (Branch (R, Branch (R, b, s, t, c), y, z, Branch (B, ve, vf, vg, vh))) =
+    Branch
+      (R, Branch (B, Branch (B, va, vb, vc, vd), w, x, b), s, t,
+        Branch (B, c, y, z, Branch (B, ve, vf, vg, vh)))
+  | balance Empty s t Empty = Branch (B, Empty, s, t, Empty)
+  | balance Empty s t (Branch (B, va, vb, vc, vd)) =
+    Branch (B, Empty, s, t, Branch (B, va, vb, vc, vd))
+  | balance Empty s t (Branch (v, Empty, vb, vc, Empty)) =
+    Branch (B, Empty, s, t, Branch (v, Empty, vb, vc, Empty))
+  | balance Empty s t (Branch (v, Branch (B, ve, vf, vg, vh), vb, vc, Empty)) =
+    Branch
+      (B, Empty, s, t, Branch (v, Branch (B, ve, vf, vg, vh), vb, vc, Empty))
+  | balance Empty s t (Branch (v, Empty, vb, vc, Branch (B, vf, vg, vh, vi))) =
+    Branch
+      (B, Empty, s, t, Branch (v, Empty, vb, vc, Branch (B, vf, vg, vh, vi)))
+  | balance Empty s t
+    (Branch (v, Branch (B, ve, vj, vk, vl), vb, vc, Branch (B, vf, vg, vh, vi)))
+    = Branch
+        (B, Empty, s, t,
+          Branch
+            (v, Branch (B, ve, vj, vk, vl), vb, vc, Branch (B, vf, vg, vh, vi)))
+  | balance (Branch (B, va, vb, vc, vd)) s t Empty =
+    Branch (B, Branch (B, va, vb, vc, vd), s, t, Empty)
+  | balance (Branch (B, va, vb, vc, vd)) s t (Branch (B, ve, vf, vg, vh)) =
+    Branch (B, Branch (B, va, vb, vc, vd), s, t, Branch (B, ve, vf, vg, vh))
+  | balance (Branch (B, va, vb, vc, vd)) s t (Branch (v, Empty, vf, vg, Empty))
+    = Branch
+        (B, Branch (B, va, vb, vc, vd), s, t, Branch (v, Empty, vf, vg, Empty))
+  | balance (Branch (B, va, vb, vc, vd)) s t
+    (Branch (v, Branch (B, vi, vj, vk, vl), vf, vg, Empty)) =
+    Branch
+      (B, Branch (B, va, vb, vc, vd), s, t,
+        Branch (v, Branch (B, vi, vj, vk, vl), vf, vg, Empty))
+  | balance (Branch (B, va, vb, vc, vd)) s t
+    (Branch (v, Empty, vf, vg, Branch (B, vj, vk, vl, vm))) =
+    Branch
+      (B, Branch (B, va, vb, vc, vd), s, t,
+        Branch (v, Empty, vf, vg, Branch (B, vj, vk, vl, vm)))
+  | balance (Branch (B, va, vb, vc, vd)) s t
+    (Branch (v, Branch (B, vi, vn, vo, vp), vf, vg, Branch (B, vj, vk, vl, vm)))
+    = Branch
+        (B, Branch (B, va, vb, vc, vd), s, t,
+          Branch
+            (v, Branch (B, vi, vn, vo, vp), vf, vg, Branch (B, vj, vk, vl, vm)))
+  | balance (Branch (v, Empty, vb, vc, Empty)) s t Empty =
+    Branch (B, Branch (v, Empty, vb, vc, Empty), s, t, Empty)
+  | balance (Branch (v, Empty, vb, vc, Branch (B, ve, vf, vg, vh))) s t Empty =
+    Branch
+      (B, Branch (v, Empty, vb, vc, Branch (B, ve, vf, vg, vh)), s, t, Empty)
+  | balance (Branch (v, Branch (B, vf, vg, vh, vi), vb, vc, Empty)) s t Empty =
+    Branch
+      (B, Branch (v, Branch (B, vf, vg, vh, vi), vb, vc, Empty), s, t, Empty)
+  | balance
+    (Branch (v, Branch (B, vf, vg, vh, vi), vb, vc, Branch (B, ve, vj, vk, vl)))
+    s t Empty =
+    Branch
+      (B, Branch
+            (v, Branch (B, vf, vg, vh, vi), vb, vc, Branch (B, ve, vj, vk, vl)),
+        s, t, Empty)
+  | balance (Branch (v, Empty, vf, vg, Empty)) s t (Branch (B, va, vb, vc, vd))
+    = Branch
+        (B, Branch (v, Empty, vf, vg, Empty), s, t, Branch (B, va, vb, vc, vd))
+  | balance (Branch (v, Empty, vf, vg, Branch (B, vi, vj, vk, vl))) s t
+    (Branch (B, va, vb, vc, vd)) =
+    Branch
+      (B, Branch (v, Empty, vf, vg, Branch (B, vi, vj, vk, vl)), s, t,
+        Branch (B, va, vb, vc, vd))
+  | balance (Branch (v, Branch (B, vj, vk, vl, vm), vf, vg, Empty)) s t
+    (Branch (B, va, vb, vc, vd)) =
+    Branch
+      (B, Branch (v, Branch (B, vj, vk, vl, vm), vf, vg, Empty), s, t,
+        Branch (B, va, vb, vc, vd))
+  | balance
+    (Branch (v, Branch (B, vj, vk, vl, vm), vf, vg, Branch (B, vi, vn, vo, vp)))
+    s t (Branch (B, va, vb, vc, vd)) =
+    Branch
+      (B, Branch
+            (v, Branch (B, vj, vk, vl, vm), vf, vg, Branch (B, vi, vn, vo, vp)),
+        s, t, Branch (B, va, vb, vc, vd));
+
+fun rbt_ins A_ f k v Empty = Branch (R, Empty, k, v, Empty)
+  | rbt_ins A_ f k v (Branch (B, l, x, y, r)) =
+    (if less A_ k x then balance (rbt_ins A_ f k v l) x y r
+      else (if less A_ x k then balance l x y (rbt_ins A_ f k v r)
+             else Branch (B, l, x, f k y v, r)))
+  | rbt_ins A_ f k v (Branch (R, l, x, y, r)) =
+    (if less A_ k x then Branch (R, rbt_ins A_ f k v l, x, y, r)
+      else (if less A_ x k then Branch (R, l, x, y, rbt_ins A_ f k v r)
+             else Branch (R, l, x, f k y v, r)));
+
+fun paint c Empty = Empty
+  | paint c (Branch (uu, l, k, v, r)) = Branch (c, l, k, v, r);
+
+fun rbt_insert_with_key A_ f k v t = paint B (rbt_ins A_ f k v t);
+
+fun rbt_insert A_ = rbt_insert_with_key A_ (fn _ => fn _ => fn nv => nv);
+
+fun insert A_ xc xd xe =
+  RBT (rbt_insert ((ord_preorder o preorder_order o order_linorder) A_) xc xd
+        (impl_of A_ xe));
+
+fun rbt_lookup A_ Empty k = NONE
+  | rbt_lookup A_ (Branch (uu, l, x, y, r)) k =
+    (if less A_ k x then rbt_lookup A_ l k
+      else (if less A_ x k then rbt_lookup A_ r k else SOME y));
+
+fun lookup A_ x =
+  rbt_lookup ((ord_preorder o preorder_order o order_linorder) A_)
+    (impl_of A_ x);
+
+fun member A_ [] y = false
+  | member A_ (x :: xs) y = eq A_ x y orelse member A_ xs y;
+
+fun hd (x21 :: x22) = x21;
+
+fun tl [] = []
+  | tl (x21 :: x22) = x22;
+
+fun remdups A_ [] = []
+  | remdups A_ (x :: xs) =
+    (if member A_ xs x then remdups A_ xs else x :: remdups A_ xs);
+
+fun dnf_and_fm (Or (phi_1, phi_2)) psi =
+  Or (dnf_and_fm phi_1 psi, dnf_and_fm phi_2 psi)
+  | dnf_and_fm (Atom v) (Or (phi_1, phi_2)) =
+    Or (dnf_and_fm (Atom v) phi_1, dnf_and_fm (Atom v) phi_2)
+  | dnf_and_fm (And (v, va)) (Or (phi_1, phi_2)) =
+    Or (dnf_and_fm (And (v, va)) phi_1, dnf_and_fm (And (v, va)) phi_2)
+  | dnf_and_fm (Neg v) (Or (phi_1, phi_2)) =
+    Or (dnf_and_fm (Neg v) phi_1, dnf_and_fm (Neg v) phi_2)
+  | dnf_and_fm (Atom v) (Atom va) = And (Atom v, Atom va)
+  | dnf_and_fm (Atom v) (And (va, vb)) = And (Atom v, And (va, vb))
+  | dnf_and_fm (Atom v) (Neg va) = And (Atom v, Neg va)
+  | dnf_and_fm (And (v, va)) (Atom vb) = And (And (v, va), Atom vb)
+  | dnf_and_fm (And (v, va)) (And (vb, vc)) = And (And (v, va), And (vb, vc))
+  | dnf_and_fm (And (v, va)) (Neg vb) = And (And (v, va), Neg vb)
+  | dnf_and_fm (Neg v) (Atom va) = And (Neg v, Atom va)
+  | dnf_and_fm (Neg v) (And (va, vb)) = And (Neg v, And (va, vb))
+  | dnf_and_fm (Neg v) (Neg va) = And (Neg v, Neg va);
+
+fun dnf_fm (And (phi_1, phi_2)) = dnf_and_fm (dnf_fm phi_1) (dnf_fm phi_2)
+  | dnf_fm (Or (phi_1, phi_2)) = Or (dnf_fm phi_1, dnf_fm phi_2)
+  | dnf_fm (Atom v) = Atom v
+  | dnf_fm (Neg v) = Neg v;
+
+fun keysa A_ (Mapping t) = Set (keys A_ t);
+
+fun amap_fm h (Atom a) = h a
+  | amap_fm h (And (phi_1, phi_2)) = And (amap_fm h phi_1, amap_fm h phi_2)
+  | amap_fm h (Or (phi_1, phi_2)) = Or (amap_fm h phi_1, amap_fm h phi_2)
+  | amap_fm h (Neg phi) = Neg (amap_fm h phi);
+
+fun emptya A_ = Mapping (empty A_);
+
+fun lookupa A_ (Mapping t) = lookup A_ t;
+
+fun update A_ k v (Mapping t) = Mapping (insert A_ k v t);
+
+fun gen_length n (x :: xs) = gen_length (Suc n) xs
+  | gen_length n [] = n;
+
+fun size_list x = gen_length Zero_nat x;
+
+fun card A_ (Set xs) = size_list (remdups A_ xs);
+
+fun conj_list (And (phi_1, phi_2)) = conj_list phi_1 @ conj_list phi_2
+  | conj_list (Atom a) = [a];
+
+fun trm_of_fm f (Atom a) = f a
+  | trm_of_fm f (And (phi_1, phi_2)) =
+    App (App (Const "conj", trm_of_fm f phi_1), trm_of_fm f phi_2)
+  | trm_of_fm f (Or (phi_1, phi_2)) =
+    App (App (Const "disj", trm_of_fm f phi_1), trm_of_fm f phi_2)
+  | trm_of_fm f (Neg phi) = App (Const "Not", trm_of_fm f phi);
+
+fun dnf_and_fm_prf (Or (phi_1, phi_2)) psi =
+  foldl (fn a => fn b => AppP (a, b)) (PThm "then_conv")
+    [PThm "conj_disj_distribR_conv",
+      foldl (fn a => fn b => AppP (a, b)) (PThm "combination_conv")
+        [AppP (PThm "arg_conv",
+                hd [dnf_and_fm_prf phi_1 psi, dnf_and_fm_prf phi_2 psi]),
+          hd (tl [dnf_and_fm_prf phi_1 psi, dnf_and_fm_prf phi_2 psi])]]
+  | dnf_and_fm_prf (Atom v) (Or (phi_1, phi_2)) =
+    foldl (fn a => fn b => AppP (a, b)) (PThm "then_conv")
+      [PThm "conj_disj_distribL_conv",
+        foldl (fn a => fn b => AppP (a, b)) (PThm "combination_conv")
+          [AppP (PThm "arg_conv",
+                  hd [dnf_and_fm_prf (Atom v) phi_1,
+                       dnf_and_fm_prf (Atom v) phi_2]),
+            hd (tl [dnf_and_fm_prf (Atom v) phi_1,
+                     dnf_and_fm_prf (Atom v) phi_2])]]
+  | dnf_and_fm_prf (And (v, va)) (Or (phi_1, phi_2)) =
+    foldl (fn a => fn b => AppP (a, b)) (PThm "then_conv")
+      [PThm "conj_disj_distribL_conv",
+        foldl (fn a => fn b => AppP (a, b)) (PThm "combination_conv")
+          [AppP (PThm "arg_conv",
+                  hd [dnf_and_fm_prf (And (v, va)) phi_1,
+                       dnf_and_fm_prf (And (v, va)) phi_2]),
+            hd (tl [dnf_and_fm_prf (And (v, va)) phi_1,
+                     dnf_and_fm_prf (And (v, va)) phi_2])]]
+  | dnf_and_fm_prf (Neg v) (Or (phi_1, phi_2)) =
+    foldl (fn a => fn b => AppP (a, b)) (PThm "then_conv")
+      [PThm "conj_disj_distribL_conv",
+        foldl (fn a => fn b => AppP (a, b)) (PThm "combination_conv")
+          [AppP (PThm "arg_conv",
+                  hd [dnf_and_fm_prf (Neg v) phi_1,
+                       dnf_and_fm_prf (Neg v) phi_2]),
+            hd (tl [dnf_and_fm_prf (Neg v) phi_1,
+                     dnf_and_fm_prf (Neg v) phi_2])]]
+  | dnf_and_fm_prf (Atom v) (Atom va) = PThm "all_conv"
+  | dnf_and_fm_prf (Atom v) (And (va, vb)) = PThm "all_conv"
+  | dnf_and_fm_prf (Atom v) (Neg va) = PThm "all_conv"
+  | dnf_and_fm_prf (And (v, va)) (Atom vb) = PThm "all_conv"
+  | dnf_and_fm_prf (And (v, va)) (And (vb, vc)) = PThm "all_conv"
+  | dnf_and_fm_prf (And (v, va)) (Neg vb) = PThm "all_conv"
+  | dnf_and_fm_prf (Neg v) (Atom va) = PThm "all_conv"
+  | dnf_and_fm_prf (Neg v) (And (va, vb)) = PThm "all_conv"
+  | dnf_and_fm_prf (Neg v) (Neg va) = PThm "all_conv";
+
+fun dnf_fm_prf (And (phi_1, phi_2)) =
+  foldl (fn a => fn b => AppP (a, b)) (PThm "then_conv")
+    [foldl (fn a => fn b => AppP (a, b)) (PThm "combination_conv")
+       [AppP (PThm "arg_conv", hd [dnf_fm_prf phi_1, dnf_fm_prf phi_2]),
+         hd (tl [dnf_fm_prf phi_1, dnf_fm_prf phi_2])],
+      dnf_and_fm_prf (dnf_fm phi_1) (dnf_fm phi_2)]
+  | dnf_fm_prf (Or (phi_1, phi_2)) =
+    foldl (fn a => fn b => AppP (a, b)) (PThm "combination_conv")
+      [AppP (PThm "arg_conv", hd [dnf_fm_prf phi_1, dnf_fm_prf phi_2]),
+        hd (tl [dnf_fm_prf phi_1, dnf_fm_prf phi_2])]
+  | dnf_fm_prf (Atom v) = PThm "all_conv"
+  | dnf_fm_prf (Neg v) = PThm "all_conv";
+
+fun of_alist A_ xs = foldr (fn (a, b) => update A_ a b) xs (emptya A_);
+
+fun deneg (true, LESS (x, y)) =
+  And (Atom (true, LEQ (x, y)), Atom (false, EQ (x, y)))
+  | deneg (false, LESS (x, y)) = Atom (true, LEQ (y, x))
+  | deneg (false, LEQ (x, y)) =
+    And (Atom (true, LEQ (y, x)), Atom (false, EQ (y, x)))
+  | deneg (false, EQ (v, vb)) = Atom (false, EQ (v, vb))
+  | deneg (v, EQ (vb, vc)) = Atom (v, EQ (vb, vc))
+  | deneg (true, LEQ (vb, vc)) = Atom (true, LEQ (vb, vc));
+
+fun from_conj_prf trm_of_atom p (And (a, b)) =
+  foldl (fn aa => fn ba => AppP (aa, ba)) (PThm "conjE")
+    [Bound (trm_of_fm trm_of_atom (And (a, b))),
+      AbsP (trm_of_fm trm_of_atom a,
+             AbsP (trm_of_fm trm_of_atom b,
+                    from_conj_prf trm_of_atom (from_conj_prf trm_of_atom p b)
+                      a))]
+  | from_conj_prf trm_of_atom p (Atom a) = p;
+
+fun contr_fm_prf trm_of_atom contr_atom_prf (Or (c, d)) =
+  (case (contr_fm_prf trm_of_atom contr_atom_prf c,
+          contr_fm_prf trm_of_atom contr_atom_prf d)
+    of (NONE, _) => NONE | (SOME _, NONE) => NONE
+    | (SOME p1, SOME p2) =>
+      SOME (foldl (fn a => fn b => AppP (a, b)) (PThm "disjE")
+             [Bound (trm_of_fm trm_of_atom (Or (c, d))),
+               AbsP (trm_of_fm trm_of_atom c, p1),
+               AbsP (trm_of_fm trm_of_atom d, p2)]))
+  | contr_fm_prf trm_of_atom contr_atom_prf (And (a, b)) =
+    (case contr_atom_prf (conj_list (And (a, b))) of NONE => NONE
+      | SOME p => SOME (from_conj_prf trm_of_atom p (And (a, b))))
+  | contr_fm_prf trm_of_atom contr_atom_prf (Atom a) = contr_atom_prf [a];
+
+fun deless (true, LESS (x, y)) =
+  And (Atom (true, LEQ (x, y)), Atom (false, EQ (x, y)))
+  | deless (false, LESS (x, y)) =
+    Or (Atom (false, LEQ (x, y)), Atom (true, EQ (x, y)))
+  | deless (false, EQ (v, vb)) = Atom (false, EQ (v, vb))
+  | deless (false, LEQ (v, vb)) = Atom (false, LEQ (v, vb))
+  | deless (v, EQ (vb, vc)) = Atom (v, EQ (vb, vc))
+  | deless (v, LEQ (vb, vc)) = Atom (v, LEQ (vb, vc));
+
+fun deneg_prf (true, LESS (x, y)) = PThm "less_le"
+  | deneg_prf (false, LESS (x, y)) = PThm "nless_le"
+  | deneg_prf (false, LEQ (x, y)) = PThm "nle_le"
+  | deneg_prf (false, EQ (v, vb)) = PThm "all_conv"
+  | deneg_prf (v, EQ (vb, vc)) = PThm "all_conv"
+  | deneg_prf (true, LEQ (vb, vc)) = PThm "all_conv";
+
+val one_nat : nat = Suc Zero_nat;
+
+fun map_option f NONE = NONE
+  | map_option f (SOME x2) = SOME (f x2);
+
+fun deless_prf (true, LESS (x, y)) = PThm "less_le"
+  | deless_prf (false, LESS (x, y)) = PThm "nless_le"
+  | deless_prf (false, EQ (v, vb)) = PThm "all_conv"
+  | deless_prf (false, LEQ (v, vb)) = PThm "all_conv"
+  | deless_prf (v, EQ (vb, vc)) = PThm "all_conv"
+  | deless_prf (v, LEQ (vb, vc)) = PThm "all_conv";
+
+fun trm_of_oatom (EQ (x, y)) = App (App (Const "eq", Var x), Var y)
+  | trm_of_oatom (LEQ (x, y)) = App (App (Const "le", Var x), Var y)
+  | trm_of_oatom (LESS (x, y)) = App (App (Const "lt", Var x), Var y);
+
+fun minus_nat (Suc m) (Suc n) = minus_nat m n
+  | minus_nat Zero_nat n = Zero_nat
+  | minus_nat m Zero_nat = m;
+
+fun mapping_fold A_ f (Mapping t) a = fold A_ f t a;
+
+fun relcomp1_mapping A_ (B1_, B2_) x y1 pxy pm pma =
+  mapping_fold (linorder_prod B2_ B2_)
+    (fn (y2, z) => fn pyz => fn pmb =>
+      (if eq B1_ y1 y2 andalso not (eq B1_ y2 z)
+        then update (linorder_prod A_ B2_) (x, z)
+               (foldl (fn a => fn b => AppP (a, b)) (PThm "trans") [pxy, pyz])
+               pmb
+        else pmb))
+    pm pma;
+
+fun relcomp_mapping (A1_, A2_) pm1 pm2 pma =
+  mapping_fold (linorder_prod A2_ A2_)
+    (fn (x, y) => fn pxy => fn pm =>
+      (if eq A1_ x y then pm
+        else relcomp1_mapping A2_ (A1_, A2_) x y pxy pm2 pm))
+    pm1 pma;
+
+fun ntrancl_mapping (A1_, A2_) Zero_nat m = m
+  | ntrancl_mapping (A1_, A2_) (Suc k) m =
+    let
+      val trclm = ntrancl_mapping (A1_, A2_) k m;
+    in
+      relcomp_mapping (A1_, A2_) trclm m trclm
+    end;
+
+fun trancl_mapping (A1_, A2_) m =
+  ntrancl_mapping (A1_, A2_)
+    (minus_nat (card (equal_prod A1_ A1_) (keysa (linorder_prod A2_ A2_) m))
+      one_nat)
+    m;
+
+fun is_in_leq leqm l =
+  let
+    val (x, y) = l;
+  in
+    (if equal_inta x y then SOME (Appt (PThm "refl", Var x))
+      else lookupa (linorder_prod linorder_int linorder_int) leqm l)
+  end;
+
+fun is_in_eq leqm l =
+  let
+    val (x, y) = l;
+  in
+    (case (is_in_leq leqm (x, y), is_in_leq leqm (y, x)) of (NONE, _) => NONE
+      | (SOME _, NONE) => NONE
+      | (SOME p1, SOME p2) =>
+        SOME (foldl (fn a => fn b => AppP (a, b)) (PThm "antisym") [p1, p2]))
+  end;
+
+fun trm_of_oliteral (true, a) = trm_of_oatom a
+  | trm_of_oliteral (false, a) = App (Const "Not", trm_of_oatom a);
+
+fun contr1_list leqm (false, LEQ (x, y)) =
+  map_option
+    (fn a =>
+      AppP (AppP (PThm "contr", Bound (trm_of_oliteral (false, LEQ (x, y)))),
+             a))
+    (is_in_leq leqm (x, y))
+  | contr1_list leqm (false, EQ (x, y)) =
+    map_option
+      (fn a =>
+        AppP (AppP (PThm "contr", Bound (trm_of_oliteral (false, EQ (x, y)))),
+               a))
+      (is_in_eq leqm (x, y))
+  | contr1_list uu (true, va) = NONE
+  | contr1_list uu (v, LESS (vb, vc)) = NONE;
+
+fun contr_list_aux leqm [] = NONE
+  | contr_list_aux leqm (l :: ls) =
+    (case contr1_list leqm l of NONE => contr_list_aux leqm ls
+      | SOME a => SOME a);
+
+fun leq1_member_list (true, LEQ (x, y)) =
+  [((x, y), Bound (trm_of_oliteral (true, LEQ (x, y))))]
+  | leq1_member_list (true, EQ (x, y)) =
+    [((x, y), AppP (PThm "eqD1", Bound (trm_of_oliteral (true, EQ (x, y))))),
+      ((y, x), AppP (PThm "eqD2", Bound (trm_of_oliteral (true, EQ (x, y)))))]
+  | leq1_member_list (false, va) = []
+  | leq1_member_list (v, LESS (vb, vc)) = [];
+
+fun leq1_list a = maps leq1_member_list a;
+
+fun leq1_mapping a =
+  of_alist (linorder_prod linorder_int linorder_int) (leq1_list a);
+
+fun contr_list a =
+  contr_list_aux (trancl_mapping (equal_int, linorder_int) (leq1_mapping a)) a;
+
+fun contr_prf atom_conv phi =
+  contr_fm_prf trm_of_oliteral contr_list (dnf_fm (amap_fm atom_conv phi));
+
+fun amap_f_m_prf ap (Atom a) = AppP (PThm "atom_conv", ap a)
+  | amap_f_m_prf ap (And (phi_1, phi_2)) =
+    foldl (fn a => fn b => AppP (a, b)) (PThm "combination_conv")
+      [AppP (PThm "arg_conv",
+              hd [amap_f_m_prf ap phi_1, amap_f_m_prf ap phi_2]),
+        hd (tl [amap_f_m_prf ap phi_1, amap_f_m_prf ap phi_2])]
+  | amap_f_m_prf ap (Or (phi_1, phi_2)) =
+    foldl (fn a => fn b => AppP (a, b)) (PThm "combination_conv")
+      [AppP (PThm "arg_conv",
+              hd [amap_f_m_prf ap phi_1, amap_f_m_prf ap phi_2]),
+        hd (tl [amap_f_m_prf ap phi_1, amap_f_m_prf ap phi_2])]
+  | amap_f_m_prf ap (Neg phi) = AppP (PThm "arg_conv", amap_f_m_prf ap phi);
+
+fun lo_contr_prf phi =
+  map_option
+    ((fn a =>
+       Conv (trm_of_fm trm_of_oliteral phi, amap_f_m_prf deneg_prf phi, a)) o
+      (fn a =>
+        Conv (trm_of_fm trm_of_oliteral (amap_fm deneg phi),
+               dnf_fm_prf (amap_fm deneg phi), a)))
+    (contr_prf deneg phi);
+
+fun po_contr_prf phi =
+  map_option
+    ((fn a =>
+       Conv (trm_of_fm trm_of_oliteral phi, amap_f_m_prf deless_prf phi, a)) o
+      (fn a =>
+        Conv (trm_of_fm trm_of_oliteral (amap_fm deless phi),
+               dnf_fm_prf (amap_fm deless phi), a)))
+    (contr_prf deless phi);
+
+end; (*struct Order_Procedure*)
diff -r 419edc7f3726 -r c72fd8f1fceb src/Provers/order_tac.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Provers/order_tac.ML	Thu Apr 01 07:35:03 2021 +0200
@@ -0,0 +1,456 @@
+signature REIFY_TABLE =
+sig
+  type table
+  val empty : table
+  val get_var : term -> table -> (int * table)
+  val get_term : int -> table -> term option
+end
+
+structure Reifytab: REIFY_TABLE =
+struct
+  type table = (int * int Termtab.table * term Inttab.table)
+  
+  val empty = (0, Termtab.empty, Inttab.empty)
+  
+  fun get_var t (tab as (max_var, termtab, inttab)) =
+    (case Termtab.lookup termtab t of
+      SOME v => (v, tab)
+    | NONE => (max_var,
+              (max_var + 1, Termtab.update (t, max_var) termtab, Inttab.update (max_var, t) inttab))
+    )
+  
+  fun get_term v (_, _, inttab) = Inttab.lookup inttab v
+end
+
+signature LOGIC_SIGNATURE =
+sig
+  val mk_Trueprop : term -> term
+  val dest_Trueprop : term -> term
+  val Trueprop_conv : conv -> conv
+  val Not : term
+  val conj : term
+  val disj : term
+  
+  val notI : thm (* (P \<Longrightarrow> False) \<Longrightarrow> \<not> P *)
+  val ccontr : thm (* (\<not> P \<Longrightarrow> False) \<Longrightarrow> P *)
+  val conjI : thm (* P \<Longrightarrow> Q \<Longrightarrow> P \<and> Q *)
+  val conjE : thm (* P \<and> Q \<Longrightarrow> (P \<Longrightarrow> Q \<Longrightarrow> R) \<Longrightarrow> R *)
+  val disjE : thm (* P \<or> Q \<Longrightarrow> (P \<Longrightarrow> R) \<Longrightarrow> (Q \<Longrightarrow> R) \<Longrightarrow> R *)
+
+  val not_not_conv : conv (* \<not> (\<not> P) \<equiv> P *)
+  val de_Morgan_conj_conv : conv (* \<not> (P \<and> Q) \<equiv> \<not> P \<or> \<not> Q *)
+  val de_Morgan_disj_conv : conv (* \<not> (P \<or> Q) \<equiv> \<not> P \<and> \<not> Q *)
+  val conj_disj_distribL_conv : conv (* P \<and> (Q \<or> R) \<equiv> (P \<and> Q) \<or> (P \<and> R) *)
+  val conj_disj_distribR_conv : conv (* (Q \<or> R) \<and> P \<equiv> (Q \<and> P) \<or> (R \<and> P) *)
+end
+
+(* Control tracing output of the solver. *)
+val order_trace_cfg = Attrib.setup_config_bool @{binding "order_trace"} (K false)
+(* In partial orders, literals of the form \<not> x < y will force the order solver to perform case
+   distinctions, which leads to an exponential blowup of the runtime. The split limit controls
+   the number of literals of this form that are passed to the solver. 
+ *)
+val order_split_limit_cfg = Attrib.setup_config_int @{binding "order_split_limit"} (K 8)
+
+datatype order_kind = Order | Linorder
+
+type order_literal = (bool * Order_Procedure.o_atom)
+
+type order_context = {
+    kind : order_kind,
+    ops : term list, thms : (string * thm) list, conv_thms : (string * thm) list
+  }
+
+signature BASE_ORDER_TAC =
+sig
+
+  val tac :
+        (order_literal Order_Procedure.fm -> Order_Procedure.prf_trm option)
+        -> order_context -> thm list
+        -> Proof.context -> int -> tactic
+end
+
+functor Base_Order_Tac(
+  structure Logic_Sig : LOGIC_SIGNATURE; val excluded_types : typ list) : BASE_ORDER_TAC =
+struct
+  open Order_Procedure
+
+  fun expect _ (SOME x) = x
+    | expect f NONE = f ()
+
+  fun matches_skeleton t s = t = Term.dummy orelse
+    (case (t, s) of
+      (t0 $ t1, s0 $ s1) => matches_skeleton t0 s0 andalso matches_skeleton t1 s1
+    | _ => t aconv s)
+
+  fun dest_binop t =
+    let
+      val binop_skel = Term.dummy $ Term.dummy $ Term.dummy
+      val not_binop_skel = Logic_Sig.Not $ binop_skel
+    in
+      if matches_skeleton not_binop_skel t
+        then (case t of (_ $ (t1 $ t2 $ t3)) => (false, (t1, t2, t3)))
+        else if matches_skeleton binop_skel t
+          then (case t of (t1 $ t2 $ t3) => (true, (t1, t2, t3)))
+          else raise TERM ("Not a binop literal", [t])
+    end
+
+  fun find_term t = Library.find_first (fn (t', _) => t' aconv t)
+
+  fun reify_order_atom (eq, le, lt) t reifytab =
+    let
+      val (b, (t0, t1, t2)) =
+        (dest_binop t) handle TERM (_, _) => raise TERM ("Can't reify order literal", [t])
+      val binops = [(eq, EQ), (le, LEQ), (lt, LESS)]
+    in
+      case find_term t0 binops of
+        SOME (_, reified_bop) =>
+          reifytab
+          |> Reifytab.get_var t1 ||> Reifytab.get_var t2
+          |> (fn (v1, (v2, vartab')) =>
+               ((b, reified_bop (Int_of_integer v1, Int_of_integer v2)), vartab'))
+          |>> Atom
+      | NONE => raise TERM ("Can't reify order literal", [t])
+    end
+
+  fun reify consts reify_atom t reifytab =
+    let
+      fun reify' (t1 $ t2) reifytab =
+            let
+              val (t0, ts) = strip_comb (t1 $ t2)
+              val consts_of_arity = filter (fn (_, (_, ar)) => length ts = ar) consts
+            in
+              (case find_term t0 consts_of_arity of
+                SOME (_, (reified_op, _)) => fold_map reify' ts reifytab |>> reified_op
+              | NONE => reify_atom (t1 $ t2) reifytab)
+            end
+        | reify' t reifytab = reify_atom t reifytab
+    in
+      reify' t reifytab
+    end
+
+  fun list_curry0 f = (fn [] => f, 0)
+  fun list_curry1 f = (fn [x] => f x, 1)
+  fun list_curry2 f = (fn [x, y] => f x y, 2)
+
+  fun reify_order_conj ord_ops =
+    let
+      val consts = map (apsnd (list_curry2 o curry)) [(Logic_Sig.conj, And), (Logic_Sig.disj, Or)]
+    in   
+      reify consts (reify_order_atom ord_ops)
+    end
+
+  fun dereify_term consts reifytab t =
+    let
+      fun dereify_term' (App (t1, t2)) = (dereify_term' t1) $ (dereify_term' t2)
+        | dereify_term' (Const s) =
+            AList.lookup (op =) consts s
+            |> expect (fn () => raise TERM ("Const " ^ s ^ " not in", map snd consts))
+        | dereify_term' (Var v) = Reifytab.get_term (integer_of_int v) reifytab |> the
+    in
+      dereify_term' t
+    end
+
+  fun dereify_order_fm (eq, le, lt) reifytab t =
+    let
+      val consts = [
+        ("eq", eq), ("le", le), ("lt", lt),
+        ("Not", Logic_Sig.Not), ("disj", Logic_Sig.disj), ("conj", Logic_Sig.conj)
+        ]
+    in
+      dereify_term consts reifytab t
+    end
+
+  fun strip_AppP t =
+    let fun strip (AppP (f, s), ss) = strip (f, s::ss)
+          | strip x = x
+    in strip (t, []) end
+
+  fun replay_conv convs cvp =
+    let
+      val convs = convs @
+        [("all_conv", list_curry0 Conv.all_conv)] @ 
+        map (apsnd list_curry1) [
+          ("atom_conv", I),
+          ("neg_atom_conv", I),
+          ("arg_conv", Conv.arg_conv)] @
+        map (apsnd list_curry2) [
+          ("combination_conv", Conv.combination_conv),
+          ("then_conv", curry (op then_conv))]
+
+      fun lookup_conv convs c = AList.lookup (op =) convs c
+            |> expect (fn () => error ("Can't replay conversion: " ^ c))
+
+      fun rp_conv t =
+        (case strip_AppP t ||> map rp_conv of
+          (PThm c, cvs) =>
+            let val (conv, arity) = lookup_conv convs c
+            in if arity = length cvs
+              then conv cvs
+              else error ("Expected " ^ Int.toString arity ^ " arguments for conversion " ^
+                          c ^ " but got " ^ (length cvs |> Int.toString) ^ " arguments")
+            end
+        | _ => error "Unexpected constructor in conversion proof")
+    in
+      rp_conv cvp
+    end
+
+  fun replay_prf_trm replay_conv dereify ctxt thmtab assmtab p =
+    let
+      fun replay_prf_trm' _ (PThm s) =
+            AList.lookup (op =) thmtab s
+            |> expect (fn () => error ("Cannot replay theorem: " ^ s))
+        | replay_prf_trm' assmtab (Appt (p, t)) =
+            replay_prf_trm' assmtab p
+            |> Drule.infer_instantiate' ctxt [SOME (Thm.cterm_of ctxt (dereify t))]
+        | replay_prf_trm' assmtab (AppP (p1, p2)) =
+            apply2 (replay_prf_trm' assmtab) (p2, p1) |> (op COMP)
+        | replay_prf_trm' assmtab (AbsP (reified_t, p)) =
+            let
+              val t = dereify reified_t
+              val t_thm = Logic_Sig.mk_Trueprop t |> Thm.cterm_of ctxt |> Assumption.assume ctxt
+              val rp = replay_prf_trm' (Termtab.update (Thm.prop_of t_thm, t_thm) assmtab) p
+            in
+              Thm.implies_intr (Thm.cprop_of t_thm) rp
+            end
+        | replay_prf_trm' assmtab (Bound reified_t) =
+            let
+              val t = dereify reified_t |> Logic_Sig.mk_Trueprop
+            in
+              Termtab.lookup assmtab t
+              |> expect (fn () => raise TERM ("Assumption not found:", t::Termtab.keys assmtab))
+            end
+        | replay_prf_trm' assmtab (Conv (t, cp, p)) =
+            let
+              val thm = replay_prf_trm' assmtab (Bound t)
+              val conv = Logic_Sig.Trueprop_conv (replay_conv cp)
+              val conv_thm = Conv.fconv_rule conv thm
+              val conv_term = Thm.prop_of conv_thm
+            in
+              replay_prf_trm' (Termtab.update (conv_term, conv_thm) assmtab) p
+            end
+    in
+      replay_prf_trm' assmtab p
+    end
+
+  fun replay_order_prf_trm ord_ops {thms = thms, conv_thms = conv_thms, ...} ctxt reifytab assmtab =
+    let
+      val thmtab = thms @ [
+          ("conjE", Logic_Sig.conjE), ("conjI", Logic_Sig.conjI), ("disjE", Logic_Sig.disjE)
+        ]
+      val convs = map (apsnd list_curry0) (
+        map (apsnd Conv.rewr_conv) conv_thms @
+        [
+          ("not_not_conv", Logic_Sig.not_not_conv),
+          ("de_Morgan_conj_conv", Logic_Sig.de_Morgan_conj_conv),
+          ("de_Morgan_disj_conv", Logic_Sig.de_Morgan_disj_conv),
+          ("conj_disj_distribR_conv", Logic_Sig.conj_disj_distribR_conv),
+          ("conj_disj_distribL_conv", Logic_Sig.conj_disj_distribL_conv)
+        ])
+      
+      val dereify = dereify_order_fm ord_ops reifytab
+    in
+      replay_prf_trm (replay_conv convs) dereify ctxt thmtab assmtab
+    end
+
+  fun is_binop_term t =
+    let
+      fun is_included t = forall (curry (op <>) (t |> fastype_of |> domain_type)) excluded_types
+    in
+      (case dest_binop (Logic_Sig.dest_Trueprop t) of
+        (_, (binop, t1, t2)) =>
+          is_included binop andalso
+          (* Exclude terms with schematic variables since the solver can't deal with them.
+             More specifically, the solver uses Assumption.assume which does not allow schematic
+             variables in the assumed cterm.
+          *)
+          Term.add_var_names (binop $ t1 $ t2) [] = []
+      ) handle TERM (_, _) => false
+    end
+
+  fun partition_matches ctxt term_of pats ys =
+    let
+      val thy = Proof_Context.theory_of ctxt
+
+      fun find_match t env =
+        Library.get_first (try (fn pat => Pattern.match thy (pat, t) env)) pats
+      
+      fun filter_matches xs = fold (fn x => fn (mxs, nmxs, env) =>
+        case find_match (term_of x) env of
+          SOME env' => (x::mxs, nmxs, env')
+        | NONE => (mxs, x::nmxs, env)) xs ([], [], (Vartab.empty, Vartab.empty))
+
+      fun partition xs =
+        case filter_matches xs of
+          ([], _, _) => []
+        | (mxs, nmxs, env) => (env, mxs) :: partition nmxs
+    in
+      partition ys
+    end
+
+  fun limit_not_less [_, _, lt] ctxt prems =
+    let
+      val thy = Proof_Context.theory_of ctxt
+      val trace = Config.get ctxt order_trace_cfg
+      val limit = Config.get ctxt order_split_limit_cfg
+
+      fun is_not_less_term t =
+        (case dest_binop (Logic_Sig.dest_Trueprop t) of
+          (false, (t0, _, _)) => Pattern.matches thy (lt, t0)
+        | _ => false)
+        handle TERM _ => false
+
+      val not_less_prems = filter (is_not_less_term o Thm.prop_of) prems
+      val _ = if trace andalso length not_less_prems > limit
+                then tracing "order split limit exceeded"
+                else ()
+     in
+      filter_out (is_not_less_term o Thm.prop_of) prems @
+      take limit not_less_prems
+     end
+      
+  fun order_tac raw_order_proc octxt simp_prems =
+    Subgoal.FOCUS (fn {prems=prems, context=ctxt, ...} =>
+      let
+        val trace = Config.get ctxt order_trace_cfg
+
+        val binop_prems = filter (is_binop_term o Thm.prop_of) (prems @ simp_prems)
+        val strip_binop = (fn (x, _, _) => x) o snd o dest_binop
+        val binop_of = strip_binop o Logic_Sig.dest_Trueprop o Thm.prop_of
+
+        (* Due to local_setup, the operators of the order may contain schematic term and type
+           variables. We partition the premises according to distinct instances of those operators.
+         *)
+        val part_prems = partition_matches ctxt binop_of (#ops octxt) binop_prems
+          |> (case #kind octxt of
+                Order => map (fn (env, prems) =>
+                          (env, limit_not_less (#ops octxt) ctxt prems))
+              | _ => I)
+              
+        fun order_tac' (_, []) = no_tac
+          | order_tac' (env, prems) =
+            let
+              val [eq, le, lt] = #ops octxt
+              val subst_contract = Envir.eta_contract o Envir.subst_term env
+              val ord_ops = (subst_contract eq,
+                             subst_contract le,
+                             subst_contract lt)
+  
+              val _ = if trace then @{print} (ord_ops, prems) else (ord_ops, prems)
+  
+              val prems_conj_thm = foldl1 (fn (x, a) => Logic_Sig.conjI OF [x, a]) prems
+                |> Conv.fconv_rule Thm.eta_conversion 
+              val prems_conj = prems_conj_thm |> Thm.prop_of
+              val (reified_prems_conj, reifytab) =
+                reify_order_conj ord_ops (Logic_Sig.dest_Trueprop prems_conj) Reifytab.empty
+  
+              val proof = raw_order_proc reified_prems_conj
+  
+              val assmtab = Termtab.make [(prems_conj, prems_conj_thm)]
+              val replay = replay_order_prf_trm ord_ops octxt ctxt reifytab assmtab
+            in
+              case proof of
+                NONE => no_tac
+              | SOME p => SOLVED' (resolve_tac ctxt [replay p]) 1
+            end
+     in
+      FIRST (map order_tac' part_prems)
+     end)
+
+  val ad_absurdum_tac = SUBGOAL (fn (A, i) =>
+      case try (Logic_Sig.dest_Trueprop o Logic.strip_assums_concl) A of
+        SOME (nt $ _) =>
+          if nt = Logic_Sig.Not
+            then resolve0_tac [Logic_Sig.notI] i
+            else resolve0_tac [Logic_Sig.ccontr] i
+      | SOME _ => resolve0_tac [Logic_Sig.ccontr] i
+      | NONE => resolve0_tac [Logic_Sig.ccontr] i)
+
+  fun tac raw_order_proc octxt simp_prems ctxt =
+      EVERY' [
+          ad_absurdum_tac,
+          CONVERSION Thm.eta_conversion,
+          order_tac raw_order_proc octxt simp_prems ctxt
+        ]
+  
+end
+
+functor Order_Tac(structure Base_Tac : BASE_ORDER_TAC) = struct
+
+  fun order_context_eq ({kind = kind1, ops = ops1, ...}, {kind = kind2, ops = ops2, ...}) =
+    kind1 = kind2 andalso eq_list (op aconv) (ops1, ops2)
+
+  fun order_data_eq (x, y) = order_context_eq (fst x, fst y)
+  
+  structure Data = Generic_Data(
+    type T = (order_context * (order_context -> thm list -> Proof.context -> int -> tactic)) list
+    val empty = []
+    val extend = I
+    fun merge data = Library.merge order_data_eq data
+  )
+
+  fun declare (octxt as {kind = kind, raw_proc = raw_proc, ...}) lthy =
+    lthy |> Local_Theory.declaration {syntax = false, pervasive = false} (fn phi => fn context =>
+      let
+        val ops = map (Morphism.term phi) (#ops octxt)
+        val thms = map (fn (s, thm) => (s, Morphism.thm phi thm)) (#thms octxt)
+        val conv_thms = map (fn (s, thm) => (s, Morphism.thm phi thm)) (#conv_thms octxt)
+        val octxt' = {kind = kind, ops = ops, thms = thms, conv_thms = conv_thms}
+      in
+        context |> Data.map (Library.insert order_data_eq (octxt', raw_proc))
+      end)
+
+  fun declare_order {
+      ops = {eq = eq, le = le, lt = lt},
+      thms = {
+        trans = trans, (* x \<le> y \<Longrightarrow> y \<le> z \<Longrightarrow> x \<le> z *)
+        refl = refl, (* x \<le> x *)
+        eqD1 = eqD1, (* x = y \<Longrightarrow> x \<le> y *)
+        eqD2 = eqD2, (* x = y \<Longrightarrow> y \<le> x *)
+        antisym = antisym, (* x \<le> y \<Longrightarrow> y \<le> x \<Longrightarrow> x = y *)
+        contr = contr (* \<not> P \<Longrightarrow> P \<Longrightarrow> R *)
+      },
+      conv_thms = {
+        less_le = less_le, (* x < y \<equiv> x \<le> y \<and> x \<noteq> y *)
+        nless_le = nless_le (* \<not> a < b \<equiv> \<not> a \<le> b \<or> a = b *)
+      }
+    } =
+    declare {
+      kind = Order,
+      ops = [eq, le, lt],
+      thms = [("trans", trans), ("refl", refl), ("eqD1", eqD1), ("eqD2", eqD2),
+              ("antisym", antisym), ("contr", contr)],
+      conv_thms = [("less_le", less_le), ("nless_le", nless_le)],
+      raw_proc = Base_Tac.tac Order_Procedure.po_contr_prf
+     }                
+
+  fun declare_linorder {
+      ops = {eq = eq, le = le, lt = lt},
+      thms = {
+        trans = trans, (* x \<le> y \<Longrightarrow> y \<le> z \<Longrightarrow> x \<le> z *)
+        refl = refl, (* x \<le> x *)
+        eqD1 = eqD1, (* x = y \<Longrightarrow> x \<le> y *)
+        eqD2 = eqD2, (* x = y \<Longrightarrow> y \<le> x *)
+        antisym = antisym, (* x \<le> y \<Longrightarrow> y \<le> x \<Longrightarrow> x = y *)
+        contr = contr (* \<not> P \<Longrightarrow> P \<Longrightarrow> R *)
+      },
+      conv_thms = {
+        less_le = less_le, (* x < y \<equiv> x \<le> y \<and> x \<noteq> y *)
+        nless_le = nless_le, (* \<not> x < y \<equiv> y \<le> x *)
+        nle_le = nle_le (* \<not> a \<le> b \<equiv> b \<le> a \<and> b \<noteq> a *)
+      }
+    } =
+    declare {
+      kind = Linorder,
+      ops = [eq, le, lt],
+      thms = [("trans", trans), ("refl", refl), ("eqD1", eqD1), ("eqD2", eqD2),
+              ("antisym", antisym), ("contr", contr)],
+      conv_thms = [("less_le", less_le), ("nless_le", nless_le), ("nle_le", nle_le)],
+      raw_proc = Base_Tac.tac Order_Procedure.lo_contr_prf
+     }
+  
+  (* Try to solve the goal by calling the order solver with each of the declared orders. *)      
+  fun tac simp_prems ctxt =
+    let fun app_tac (octxt, tac0) = CHANGED o tac0 octxt simp_prems ctxt
+    in FIRST' (map app_tac (Data.get (Context.Proof ctxt))) end
+end