Add new closure solver

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/closure_procedure.ML	Mon Aug 23 13:43:02 2021 +0200
@@ -0,0 +1,919 @@
+(* Generated from Closure_Tactic.thy; DO NOT EDIT! *)
+
+structure Closure_Procedure : sig
+  datatype inta = Int_of_integer of int
+  val integer_of_int : inta -> 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 inta
+  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
+  type ('a, 'b) mapping
+  datatype closure_atom = EQ of inta * inta | In of inta * inta |
+    InTcl of inta * inta | InRtcl of inta * inta | InConv of inta * inta |
+    InReflcl of inta * inta
+  val contr_list : (bool * closure_atom) list -> prf_trm option
+  val full_contr_prf : (bool * closure_atom) fm -> prf_trm option
+end = struct
+
+datatype inta = Int_of_integer of int;
+
+fun integer_of_int (Int_of_integer k) = k;
+
+fun equal_inta k l = integer_of_int k = 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} : inta equal;
+
+fun less_eq_int k l = 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 = integer_of_int k < integer_of_int l;
+
+val ord_int = {less_eq = less_eq_int, less = less_int} : inta 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} : inta preorder;
+
+val order_int = {preorder_order = preorder_int} : inta order;
+
+type 'a linorder = {order_linorder : 'a order};
+val order_linorder = #order_linorder : 'a linorder -> 'a order;
+
+val linorder_int = {order_linorder = order_int} : inta 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 num = One | Bit0 of num | Bit1 of num;
+
+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 inta;
+
+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 closure_atom = EQ of inta * inta | In of inta * inta |
+  InTcl of inta * inta | InRtcl of inta * inta | InConv of inta * inta |
+  InReflcl of inta * inta;
+
+fun id x = (fn xa => xa) x;
+
+fun impl_of B_ (RBT x) = x;
+
+fun foldb f (Branch (c, lt, k, v, rt)) x = foldb f rt (f k v (foldb f lt x))
+  | foldb f Empty x = x;
+
+fun fold A_ x xc = foldb 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 map f [] = []
+  | map f (x21 :: x22) = f x21 :: map f x22;
+
+fun image f (Set xs) = Set (map f xs);
+
+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 membera A_ [] y = false
+  | membera A_ (x :: xs) y = eq A_ x y orelse membera A_ xs y;
+
+fun member A_ x (Coset xs) = not (membera A_ xs x)
+  | member A_ x (Set xs) = membera A_ xs x;
+
+fun filter p [] = []
+  | filter p (x :: xs) = (if p x then x :: filter p xs else filter p xs);
+
+fun less_nat m (Suc n) = less_eq_nat m n
+  | less_nat n Zero_nat = false
+and less_eq_nat (Suc m) n = less_nat m n
+  | less_eq_nat Zero_nat n = true;
+
+fun rbt_baliR t1 ab bb (Branch (R, t2, aa, ba, Branch (R, t3, a, b, t4))) =
+  Branch (R, Branch (B, t1, ab, bb, t2), aa, ba, Branch (B, t3, a, b, t4))
+  | rbt_baliR t1 ab bb (Branch (R, Branch (R, t2, aa, ba, t3), a, b, Empty)) =
+    Branch (R, Branch (B, t1, ab, bb, t2), aa, ba, Branch (B, t3, a, b, Empty))
+  | rbt_baliR t1 ab bb
+    (Branch (R, Branch (R, t2, aa, ba, t3), a, b, Branch (B, va, vb, vc, vd))) =
+    Branch
+      (R, Branch (B, t1, ab, bb, t2), aa, ba,
+        Branch (B, t3, a, b, Branch (B, va, vb, vc, vd)))
+  | rbt_baliR t1 a b Empty = Branch (B, t1, a, b, Empty)
+  | rbt_baliR t1 a b (Branch (B, va, vb, vc, vd)) =
+    Branch (B, t1, a, b, Branch (B, va, vb, vc, vd))
+  | rbt_baliR t1 a b (Branch (v, Empty, vb, vc, Empty)) =
+    Branch (B, t1, a, b, Branch (v, Empty, vb, vc, Empty))
+  | rbt_baliR t1 a b (Branch (v, Branch (B, ve, vf, vg, vh), vb, vc, Empty)) =
+    Branch (B, t1, a, b, Branch (v, Branch (B, ve, vf, vg, vh), vb, vc, Empty))
+  | rbt_baliR t1 a b (Branch (v, Empty, vb, vc, Branch (B, vf, vg, vh, vi))) =
+    Branch (B, t1, a, b, Branch (v, Empty, vb, vc, Branch (B, vf, vg, vh, vi)))
+  | rbt_baliR t1 a b
+    (Branch (v, Branch (B, ve, vj, vk, vl), vb, vc, Branch (B, vf, vg, vh, vi)))
+    = Branch
+        (B, t1, a, b,
+          Branch
+            (v, Branch (B, ve, vj, vk, vl), vb, vc,
+              Branch (B, vf, vg, vh, vi)));
+
+fun equal_color R B = false
+  | equal_color B R = false
+  | equal_color B B = true
+  | equal_color R R = true;
+
+fun bheight Empty = Zero_nat
+  | bheight (Branch (c, lt, k, v, rt)) =
+    (if equal_color c B then Suc (bheight lt) else bheight lt);
+
+fun rbt_joinR l a b r =
+  (if less_eq_nat (bheight l) (bheight r) then Branch (R, l, a, b, r)
+    else (case l
+           of Branch (R, la, ab, ba, ra) =>
+             Branch (R, la, ab, ba, rbt_joinR ra a b r)
+           | Branch (B, la, ab, ba, ra) =>
+             rbt_baliR la ab ba (rbt_joinR ra a b r)));
+
+fun rbt_baliL (Branch (R, Branch (R, t1, ab, bb, t2), aa, ba, t3)) a b t4 =
+  Branch (R, Branch (B, t1, ab, bb, t2), aa, ba, Branch (B, t3, a, b, t4))
+  | rbt_baliL (Branch (R, Empty, ab, bb, Branch (R, t2, aa, ba, t3))) a b t4 =
+    Branch (R, Branch (B, Empty, ab, bb, t2), aa, ba, Branch (B, t3, a, b, t4))
+  | rbt_baliL
+    (Branch (R, Branch (B, va, vb, vc, vd), ab, bb, Branch (R, t2, aa, ba, t3)))
+    a b t4 =
+    Branch
+      (R, Branch (B, Branch (B, va, vb, vc, vd), ab, bb, t2), aa, ba,
+        Branch (B, t3, a, b, t4))
+  | rbt_baliL Empty a b t2 = Branch (B, Empty, a, b, t2)
+  | rbt_baliL (Branch (B, va, vb, vc, vd)) a b t2 =
+    Branch (B, Branch (B, va, vb, vc, vd), a, b, t2)
+  | rbt_baliL (Branch (v, Empty, vb, vc, Empty)) a b t2 =
+    Branch (B, Branch (v, Empty, vb, vc, Empty), a, b, t2)
+  | rbt_baliL (Branch (v, Empty, vb, vc, Branch (B, ve, vf, vg, vh))) a b t2 =
+    Branch (B, Branch (v, Empty, vb, vc, Branch (B, ve, vf, vg, vh)), a, b, t2)
+  | rbt_baliL (Branch (v, Branch (B, vf, vg, vh, vi), vb, vc, Empty)) a b t2 =
+    Branch (B, Branch (v, Branch (B, vf, vg, vh, vi), vb, vc, Empty), a, b, t2)
+  | rbt_baliL
+    (Branch (v, Branch (B, vf, vg, vh, vi), vb, vc, Branch (B, ve, vj, vk, vl)))
+    a b t2 =
+    Branch
+      (B, Branch
+            (v, Branch (B, vf, vg, vh, vi), vb, vc, Branch (B, ve, vj, vk, vl)),
+        a, b, t2);
+
+fun rbt_joinL l a b r =
+  (if less_eq_nat (bheight r) (bheight l) then Branch (R, l, a, b, r)
+    else (case r
+           of Branch (R, la, ab, ba, ra) =>
+             Branch (R, rbt_joinL l a b la, ab, ba, ra)
+           | Branch (B, la, ab, ba, ra) =>
+             rbt_baliL (rbt_joinL l a b la) ab ba ra));
+
+fun rbt_join l a b r =
+  let
+    val bhl = bheight l;
+    val bhr = bheight r;
+  in
+    (if less_nat bhr bhl then paint B (rbt_joinR l a b r)
+      else (if less_nat bhl bhr then paint B (rbt_joinL l a b r)
+             else Branch (B, l, a, b, r)))
+  end;
+
+fun rbt_split A_ Empty k = (Empty, (NONE, Empty))
+  | rbt_split A_ (Branch (uu, l, a, b, r)) x =
+    (if less A_ x a then let
+                           val (l1, (beta, l2)) = rbt_split A_ l x;
+                         in
+                           (l1, (beta, rbt_join l2 a b r))
+                         end
+      else (if less A_ a x then let
+                                  val (r1, (beta, r2)) = rbt_split A_ r x;
+                                in
+                                  (rbt_join l a b r1, (beta, r2))
+                                end
+             else (l, (SOME b, r))));
+
+fun plus_nat (Suc m) n = plus_nat m (Suc n)
+  | plus_nat Zero_nat n = n;
+
+val one_nat : nat = Suc Zero_nat;
+
+fun nat_of_num (Bit1 n) = let
+                            val m = nat_of_num n;
+                          in
+                            Suc (plus_nat m m)
+                          end
+  | nat_of_num (Bit0 n) = let
+                            val m = nat_of_num n;
+                          in
+                            plus_nat m m
+                          end
+  | nat_of_num One = one_nat;
+
+fun small_rbt t = less_nat (bheight t) (nat_of_num (Bit0 (Bit0 One)));
+
+fun flip_rbt t1 t2 = less_nat (bheight t2) (bheight t1);
+
+fun rbt_union_swap_rec A_ f gamma t1 t2 =
+  let
+    val (gammaa, (t2a, t1a)) =
+      (if flip_rbt t2 t1 then (not gamma, (t1, t2)) else (gamma, (t2, t1)));
+    val fa = (if gammaa then (fn k => fn v => fn va => f k va v) else f);
+  in
+    (if small_rbt t2a then foldb (rbt_insert_with_key A_ fa) t2a t1a
+      else (case t1a of Empty => t2a
+             | Branch (_, l1, a, b, r1) =>
+               let
+                 val (l2, (beta, r2)) = rbt_split A_ t2a a;
+               in
+                 rbt_join (rbt_union_swap_rec A_ f gammaa l1 l2) a
+                   (case beta of NONE => b | SOME c => fa a b c)
+                   (rbt_union_swap_rec A_ f gammaa r1 r2)
+               end))
+  end;
+
+fun rbt_union_with_key A_ f t1 t2 =
+  paint B (rbt_union_swap_rec A_ f false t1 t2);
+
+fun rbt_union_with B_ f = rbt_union_with_key B_ (fn _ => f);
+
+fun combine A_ xc xd xe =
+  RBT (rbt_union_with ((ord_preorder o preorder_order o order_linorder) A_) xc
+        (impl_of A_ xd) (impl_of A_ xe));
+
+fun hd (x21 :: x22) = x21;
+
+fun remdups A_ [] = []
+  | remdups A_ (x :: xs) =
+    (if membera 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 folda A_ f (Mapping t) a = fold A_ f t a;
+
+fun keysa A_ (Mapping t) = Set (keys A_ t);
+
+fun rbt_bulkload A_ xs = foldr (fn (a, b) => rbt_insert A_ a b) xs Empty;
+
+fun bulkload A_ xa =
+  RBT (rbt_bulkload ((ord_preorder o preorder_order o order_linorder) A_) xa);
+
+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 map_filter f [] = []
+  | map_filter f (x :: xs) =
+    (case f x of NONE => map_filter f xs | SOME y => y :: map_filter f 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 combinea B_ f (Mapping t1) (Mapping t2) = Mapping (combine B_ f t1 t2);
+
+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", 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", 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", 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", 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", 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", 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 tabulate A_ ks f = Mapping (bulkload A_ (map (fn k => (k, f k)) ks));
+
+fun the (SOME x2) = x2;
+
+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 ordered_keys A_ (Mapping t) = keys A_ t;
+
+fun fst (x1, x2) = x1;
+
+fun map_option f NONE = NONE
+  | map_option f (SOME x2) = SOME (f x2);
+
+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 insort_key B_ f x [] = [x]
+  | insort_key B_ f x (y :: ys) =
+    (if less_eq ((ord_preorder o preorder_order o order_linorder) B_) (f x)
+          (f y)
+      then x :: y :: ys else y :: insort_key B_ f x ys);
+
+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", 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", 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 trm_of_closure_atom (EQ (x, y)) = App (App (Const "eq", Var x), Var y)
+  | trm_of_closure_atom (In (x, y)) = App (App (Const "in", Var x), Var y)
+  | trm_of_closure_atom (InTcl (x, y)) =
+    App (App (Const "in_trancl", Var x), Var y)
+  | trm_of_closure_atom (InRtcl (x, y)) =
+    App (App (Const "in_rtrancl", Var x), Var y)
+  | trm_of_closure_atom (InReflcl (x, y)) =
+    App (App (Const "in_reflcl", Var x), Var y)
+  | trm_of_closure_atom (InConv (x, y)) =
+    App (App (Const "in_converse", Var x), Var y);
+
+fun trm_of_closure_literal (true, a) = trm_of_closure_atom a
+  | trm_of_closure_literal (false, a) =
+    App (Const "Not", trm_of_closure_atom a);
+
+fun eq1_member_list (true, EQ (x, y)) =
+  [((x, y), Bound (trm_of_closure_literal (true, EQ (x, y)))),
+    ((y, x),
+      AppP (PThm "eq_sym", Bound (trm_of_closure_literal (true, EQ (x, y)))))]
+  | eq1_member_list (false, va) = []
+  | eq1_member_list (v, In (vb, vc)) = []
+  | eq1_member_list (v, InTcl (vb, vc)) = []
+  | eq1_member_list (v, InRtcl (vb, vc)) = []
+  | eq1_member_list (v, InConv (vb, vc)) = []
+  | eq1_member_list (v, InReflcl (vb, vc)) = [];
+
+fun eq1_list x = maps eq1_member_list x;
+
+fun is_in_eq eqm =
+  (fn (x, y) =>
+    (if equal_inta x y then SOME (Appt (PThm "eq_refl", Var x))
+      else lookupa (linorder_prod linorder_int linorder_int) eqm (x, y)));
+
+fun insort_insert_key (B1_, B2_) f x xs =
+  (if member B1_ (f x) (image f (Set xs)) then xs else insort_key B2_ f x xs);
+
+fun veq_list (A1_, A2_) eqm x =
+  insort_insert_key (A1_, A2_) (fn xa => xa) x
+    (map_filter (fn xa => (if let
+                                val (_, z) = xa;
+                              in
+                                eq A1_ z x
+                              end
+                            then SOME (fst xa) else NONE))
+      (ordered_keys (linorder_prod A2_ A2_) eqm));
+
+fun veq_rep_mapping eqm [] = emptya linorder_int
+  | veq_rep_mapping eqm (v :: vs) =
+    let
+      val veqs = veq_list (equal_int, linorder_int) eqm v;
+    in
+      combinea linorder_int (fn x => fn _ => x)
+        (tabulate linorder_int veqs
+          (fn x => (hd veqs, the (is_in_eq eqm (hd veqs, x)))))
+        (veq_rep_mapping eqm (filter (not o membera equal_int veqs) vs))
+    end;
+
+fun contr1_list is_in_eq is_in_in1 is_in_tcl (false, EQ (x, y)) =
+  map_option
+    (fn p2 =>
+      foldl (fn a => fn b => AppP (a, b)) (PThm "contr")
+        [Bound (trm_of_closure_literal (false, EQ (x, y))), p2])
+    (is_in_eq (x, y))
+  | contr1_list is_in_eq is_in_in1 is_in_tcl (false, In (x, y)) =
+    map_option
+      (fn p2 =>
+        foldl (fn a => fn b => AppP (a, b)) (PThm "contr")
+          [Bound (trm_of_closure_literal (false, In (x, y))), p2])
+      (is_in_in1 (x, y))
+  | contr1_list is_in_eq is_in_in1 is_in_tcl (false, InTcl (x, y)) =
+    map_option
+      (fn p2 =>
+        foldl (fn a => fn b => AppP (a, b)) (PThm "contr")
+          [Bound (trm_of_closure_literal (false, InTcl (x, y))), p2])
+      (is_in_tcl (x, y))
+  | contr1_list is_in_eq is_in_in1 is_in_tcl (false, InRtcl (x, y)) =
+    (case is_in_eq (x, y)
+      of NONE =>
+        map_option
+          (fn p2 =>
+            foldl (fn a => fn b => AppP (a, b)) (PThm "contr")
+              [AppP (PThm "not_rtrancl_into_not_trancl",
+                      Bound (trm_of_closure_literal (false, InRtcl (x, y)))),
+                p2])
+          (is_in_tcl (x, y))
+      | SOME p =>
+        SOME (foldl (fn a => fn b => AppP (a, b)) (PThm "contr")
+               [Bound (trm_of_closure_literal (false, InRtcl (x, y))),
+                 AppP (PThm "rtrancl_refl", p)]))
+  | contr1_list is_in_eq is_in_in1 is_in_tcl (true, va) = NONE
+  | contr1_list is_in_eq is_in_in1 is_in_tcl (v, InConv (vb, vc)) = NONE
+  | contr1_list is_in_eq is_in_in1 is_in_tcl (v, InReflcl (vb, vc)) = NONE;
+
+fun contr_list_aux is_in_eq is_in_in1 is_in_tcl [] = NONE
+  | contr_list_aux is_in_eq is_in_in1 is_in_tcl (l :: ls) =
+    (case contr1_list is_in_eq is_in_in1 is_in_tcl l
+      of NONE => contr_list_aux is_in_eq is_in_in1 is_in_tcl ls
+      | SOME a => SOME a);
+
+fun relcomp1_mapping B_ (C1_, C2_) combine x y1 pxy pm pma =
+  folda (linorder_prod C2_ C2_)
+    (fn (y2, z) => fn pyz => fn pmb =>
+      (if eq C1_ y1 y2 andalso not (eq C1_ y2 z)
+        then update (linorder_prod B_ C2_) (x, z) (combine pxy pyz) pmb
+        else pmb))
+    pm pma;
+
+fun relcomp_mapping (B1_, B2_) combine pm1 pm2 pma =
+  folda (linorder_prod B2_ B2_)
+    (fn (x, y) => fn pxy => fn pm =>
+      (if eq B1_ x y then pm
+        else relcomp1_mapping B2_ (B1_, B2_) combine x y pxy pm2 pm))
+    pm1 pma;
+
+fun ntrancl_mapping (B1_, B2_) combine Zero_nat m = m
+  | ntrancl_mapping (B1_, B2_) combine (Suc k) m =
+    let
+      val trclm = ntrancl_mapping (B1_, B2_) combine k m;
+    in
+      relcomp_mapping (B1_, B2_) combine trclm m trclm
+    end;
+
+fun trancl_mapping (B1_, B2_) combine m =
+  ntrancl_mapping (B1_, B2_) combine
+    (minus_nat (card (equal_prod B1_ B1_) (keysa (linorder_prod B2_ B2_) m))
+      one_nat)
+    m;
+
+fun tcl1_member_list veqrm l =
+  (case l of (true, EQ (_, _)) => []
+    | (true, In (x, y)) =>
+      let
+        val (rep_x, prep_x) = the (lookupa linorder_int veqrm x);
+        val (rep_y, prep_y) = the (lookupa linorder_int veqrm y);
+        val p =
+          foldl (fn a => fn b => AppP (a, b)) (PThm "eq_in_trancl")
+            [prep_x, prep_y,
+              AppP (PThm "r_into_trancl",
+                     Bound (trm_of_closure_literal (true, In (x, y))))];
+      in
+        [((rep_x, rep_y), p)]
+      end
+    | (true, InTcl (x, y)) =>
+      let
+        val (rep_x, prep_x) = the (lookupa linorder_int veqrm x);
+        val (rep_y, prep_y) = the (lookupa linorder_int veqrm y);
+        val p =
+          foldl (fn a => fn b => AppP (a, b)) (PThm "eq_in_trancl")
+            [prep_x, prep_y,
+              Bound (trm_of_closure_literal (true, InTcl (x, y)))];
+      in
+        [((rep_x, rep_y), p)]
+      end
+    | (true, InRtcl (_, _)) => [] | (true, InConv (_, _)) => []
+    | (true, InReflcl (_, _)) => [] | (false, _) => []);
+
+fun tcl1_mapping A_ veqrm a =
+  of_alist (linorder_prod A_ A_) (maps (tcl1_member_list veqrm) a);
+
+fun tcl_mapping (A1_, A2_) veqrm a =
+  trancl_mapping (A1_, A2_)
+    (fn p1 => fn p2 =>
+      foldl (fn aa => fn b => AppP (aa, b)) (PThm "trancl_trans") [p1, p2])
+    (tcl1_mapping A2_ veqrm a);
+
+fun in1_member_list veqrm l =
+  (case l of (true, EQ (_, _)) => []
+    | (true, In (x, y)) =>
+      let
+        val (rep_x, prep_x) = the (lookupa linorder_int veqrm x);
+        val (rep_y, prep_y) = the (lookupa linorder_int veqrm y);
+      in
+        [((rep_x, rep_y),
+           foldl (fn a => fn b => AppP (a, b)) (PThm "eq_in")
+             [prep_x, prep_y,
+               Bound (trm_of_closure_literal (true, In (x, y)))])]
+      end
+    | (true, InTcl (_, _)) => [] | (true, InRtcl (_, _)) => []
+    | (true, InConv (_, _)) => [] | (true, InReflcl (_, _)) => []
+    | (false, _) => []);
+
+fun in1_mapping A_ veqrm a =
+  of_alist (linorder_prod A_ A_) (maps (in1_member_list veqrm) a);
+
+fun vars_list (uu, EQ (x, y)) = [x, y]
+  | vars_list (uv, In (x, y)) = [x, y]
+  | vars_list (uw, InTcl (x, y)) = [x, y]
+  | vars_list (ux, InRtcl (x, y)) = [x, y]
+  | vars_list (uy, InConv (x, y)) = [x, y]
+  | vars_list (uz, InReflcl (x, y)) = [x, y];
+
+fun varss_list x = (remdups equal_int o maps vars_list) x;
+
+fun eq1_mapping a =
+  of_alist (linorder_prod linorder_int linorder_int) (eq1_list a);
+
+fun eq_mapping a =
+  trancl_mapping (equal_int, linorder_int)
+    (fn p1 => fn p2 =>
+      foldl (fn aa => fn b => AppP (aa, b)) (PThm "eq_trans") [p1, p2])
+    (eq1_mapping a);
+
+fun is_in_tcl A_ B_ veqrm tclm =
+  (fn (x, y) =>
+    (case (lookupa A_ veqrm x, lookupa A_ veqrm y) of (NONE, _) => NONE
+      | (SOME (_, _), NONE) => NONE
+      | (SOME (rep_x, prep_x), SOME (rep_y, prep_y)) =>
+        map_option
+          (fn p3 =>
+            foldl (fn a => fn b => AppP (a, b)) (PThm "eq_in_trancl")
+              [AppP (PThm "eq_sym", prep_x), AppP (PThm "eq_sym", prep_y), p3])
+          (lookupa (linorder_prod B_ B_) tclm (rep_x, rep_y))));
+
+fun is_in_in1 A_ B_ veqrm in1m =
+  (fn (x, y) =>
+    (case (lookupa A_ veqrm x, lookupa A_ veqrm y) of (NONE, _) => NONE
+      | (SOME (_, _), NONE) => NONE
+      | (SOME (rep_x, prep_x), SOME (rep_y, prep_y)) =>
+        map_option
+          (fn p3 =>
+            foldl (fn a => fn b => AppP (a, b)) (PThm "eq_in")
+              [AppP (PThm "eq_sym", prep_x), AppP (PThm "eq_sym", prep_y), p3])
+          (lookupa (linorder_prod B_ B_) in1m (rep_x, rep_y))));
+
+fun contr_list a =
+  let
+    val eqm = eq_mapping a;
+    val isineq = is_in_eq (eq_mapping a);
+    val veq_repm = veq_rep_mapping eqm (varss_list a);
+    val in1m = in1_mapping linorder_int veq_repm a;
+    val isin1 = is_in_in1 linorder_int linorder_int veq_repm in1m;
+    val tclm = tcl_mapping (equal_int, linorder_int) veq_repm a;
+    val isintcl = is_in_tcl linorder_int linorder_int veq_repm tclm;
+  in
+    contr_list_aux isineq isin1 isintcl a
+  end;
+
+fun contr_prf atom_conv phi =
+  contr_fm_prf trm_of_closure_literal contr_list
+    (dnf_fm (amap_fm atom_conv phi));
+
+fun normalise (true, InRtcl (x, y)) =
+  Or (Atom (true, EQ (x, y)),
+       And (Atom (false, EQ (x, y)), Atom (true, InTcl (x, y))))
+  | normalise (true, InReflcl (x, y)) =
+    Or (Atom (true, EQ (x, y)),
+         And (Atom (false, EQ (x, y)), Atom (true, In (x, y))))
+  | normalise (false, InReflcl (x, y)) =
+    And (Atom (false, EQ (x, y)), Atom (false, In (x, y)))
+  | normalise (b, InConv (x, y)) = Atom (b, In (y, x))
+  | normalise (false, EQ (v, vb)) = Atom (false, EQ (v, vb))
+  | normalise (false, In (v, vb)) = Atom (false, In (v, vb))
+  | normalise (false, InTcl (v, vb)) = Atom (false, InTcl (v, vb))
+  | normalise (false, InRtcl (v, vb)) = Atom (false, InRtcl (v, vb))
+  | normalise (v, EQ (vb, vc)) = Atom (v, EQ (vb, vc))
+  | normalise (v, In (vb, vc)) = Atom (v, In (vb, vc))
+  | normalise (v, InTcl (vb, vc)) = Atom (v, InTcl (vb, vc));
+
+fun normalise_prf (true, InRtcl (x, y)) = PThm "rtrancl_eq_or_trancl_conv"
+  | normalise_prf (true, InReflcl (x, y)) = PThm "reflcl_eq_or_in_conv"
+  | normalise_prf (false, InReflcl (x, y)) = PThm "not_reflcl_eq_and_in_conv"
+  | normalise_prf (true, InConv (x, y)) = PThm "in_converse_conv"
+  | normalise_prf (false, InConv (x, y)) = PThm "not_in_converse_conv"
+  | normalise_prf (false, EQ (v, vb)) = PThm "all_conv"
+  | normalise_prf (false, In (v, vb)) = PThm "all_conv"
+  | normalise_prf (false, InTcl (v, vb)) = PThm "all_conv"
+  | normalise_prf (false, InRtcl (v, vb)) = PThm "all_conv"
+  | normalise_prf (v, EQ (vb, vc)) = PThm "all_conv"
+  | normalise_prf (v, In (vb, vc)) = PThm "all_conv"
+  | normalise_prf (v, InTcl (vb, vc)) = PThm "all_conv";
+
+fun full_contr_prf phi =
+  map_option
+    ((fn a =>
+       Conv (trm_of_fm trm_of_closure_literal phi,
+              amap_f_m_prf normalise_prf phi, a)) o
+      (fn a =>
+        Conv (trm_of_fm trm_of_closure_literal (amap_fm normalise phi),
+               dnf_fm_prf (amap_fm normalise phi), a)))
+    (contr_prf normalise phi);
+
+end; (*struct Closure_Procedure*)

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/closure_tac.ML	Mon Aug 23 13:43:02 2021 +0200
@@ -0,0 +1,301 @@
+signature CLOSURE_TAC_ARGS =
+sig
+  val mk_rel_typ : typ -> typ
+
+  val in_pat : term -> term -> term -> term
+  val in_trancl_pat : term -> term -> term -> term
+  val in_rtrancl_pat : term -> term -> term -> term
+  val in_reflcl_pat : term -> term -> term -> term
+  val in_converse_pat : term -> term -> term -> term
+
+  val r_into_trancl_thm : thm
+  val trancl_trans_thm : thm
+  val eq_in_thm : thm
+  val eq_in_trancl_thm : thm
+  val rtrancl_refl_thm : thm
+  val not_rtrancl_into_not_trancl_thm : thm
+
+  val rtrancl_eq_or_trancl_conv : conv
+  val reflcl_eq_or_in_conv : conv
+  val not_reflcl_eq_and_in_conv : conv
+  val in_converse_conv : conv
+  val not_in_converse_conv : conv
+end
+
+functor Closure_Tac(Closure_Tac_Args : CLOSURE_TAC_ARGS) =
+struct
+
+open Closure_Procedure
+open Closure_Tac_Args
+
+fun expect _ (SOME x) = x
+  | expect f NONE = f ()
+
+fun find_term t = Library.find_first (fn (t', _) => t' aconv t)
+
+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 dereify_closure_fm r reifytab t =
+  let
+    fun dereify_term' (App (App (Const "in", t1), t2)) =
+          in_pat (dereify_term' t1) (dereify_term' t2) r
+      | dereify_term' (App (App (Const "in_trancl", t1), t2)) =
+          in_trancl_pat (dereify_term' t1) (dereify_term' t2) r
+      | dereify_term' (App (App (Const "in_rtrancl", t1), t2)) =
+          in_rtrancl_pat (dereify_term' t1) (dereify_term' t2) r
+      | dereify_term' (App (App (Const "in_reflcl", t1), t2)) =
+          in_reflcl_pat (dereify_term' t1) (dereify_term' t2) r
+      | dereify_term' (App (App (Const "in_converse", t1), t2)) =
+          in_converse_pat (dereify_term' t1) (dereify_term' t2) r
+      | dereify_term' (App (App (Const "eq", t1), t2)) =
+          HOLogic.mk_eq (dereify_term' t1, dereify_term' t2)
+      | dereify_term' (App (t1, t2)) = dereify_term' t1 $ dereify_term' t2
+      | dereify_term' (Const "Not") = HOLogic.Not
+      | dereify_term' (Const "conj") = HOLogic.conj
+      | dereify_term' (Const "disj") = HOLogic.disj
+      | dereify_term' (Const c) = error ("Unexpected constant " ^ c)
+      | dereify_term' (Var v) = Reifytab.get_term (integer_of_int v) reifytab |> the
+  in
+    dereify_term' 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 = HOLogic.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 |> HOLogic.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 = HOLogic.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_closure_prf_trm ctxt r reifytab assmtab =
+  let
+    val thmtab =
+      [ ("conjE", @{thm conjE}), ("conjI", @{thm conjI}), ("disjE", @{thm disjE})
+      , ("eq_trans", @{thm HOL.trans}), ("eq_refl", @{thm HOL.refl}), ("eq_sym", @{thm HOL.sym})
+      , ("r_into_trancl", r_into_trancl_thm), ("trancl_trans", trancl_trans_thm)
+      , ("eq_in", eq_in_thm), ("eq_in_trancl", eq_in_trancl_thm)
+      , ("rtrancl_refl", rtrancl_refl_thm)
+      , ("not_rtrancl_into_not_trancl", not_rtrancl_into_not_trancl_thm)
+      , ("contr", @{thm notE})
+      ]
+    val convs = map (apsnd list_curry0) (
+        [ ("rtrancl_eq_or_trancl_conv", rtrancl_eq_or_trancl_conv)
+        , ("reflcl_eq_or_in_conv", reflcl_eq_or_in_conv)
+        , ("not_reflcl_eq_and_in_conv", not_reflcl_eq_and_in_conv)
+        , ("in_converse_conv", in_converse_conv)
+        , ("not_in_converse_conv", not_in_converse_conv)
+        ] @
+        map (apsnd (Conv.rewr_conv o (fn thm => @{thm eq_reflection} OF [thm])))
+          [ ("not_not_conv", @{thm not_not})
+          , ("de_Morgan_conj_conv", @{thm de_Morgan_conj})
+          , ("de_Morgan_disj_conv", @{thm de_Morgan_disj})
+          , ("conj_disj_distribR_conv", @{thm conj_disj_distribR})
+          , ("conj_disj_distribL_conv", @{thm conj_disj_distribL})
+          ])
+    
+    val dereify = dereify_closure_fm r reifytab
+  in
+    replay_prf_trm (replay_conv convs) dereify ctxt thmtab assmtab
+  end
+
+fun partition_matches ctxt dummys pats term_of ts =
+  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 delete_dummys tab = fold Vartab.delete_safe dummys tab
+    fun filter_matches xs = fold (fn x => fn (mxs, nmxs, env) =>
+        case find_match (term_of x) env of
+          SOME (tyenv', tenv') => (x::mxs, nmxs, (delete_dummys tyenv', delete_dummys tenv'))
+        | 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 ts
+  end
+
+fun reify ctxt pats atom_pats atom_ctor t reifytab =
+  let
+    val thy = Proof_Context.theory_of ctxt
+    fun try_match pat t = try (Pattern.match thy (pat, t)) (Vartab.empty, Vartab.empty)
+    fun get_first_match pats t =
+      Library.get_first (fn (pat, vars, ctor) => Option.map (pair (vars, ctor)) (try_match pat t)) pats 
+    val _ = fold
+  in
+    case get_first_match pats t of
+      SOME ((vars, ctor), env) =>
+        let
+          val ts = map (snd o the o Vartab.lookup (snd env)) vars
+          val (rts, reifytab') = fold_rev (fn t => fn (rts, reifytab) =>
+                                            reify ctxt pats atom_pats atom_ctor t reifytab
+                                          |>> (fn rt => rt :: rts)) ts ([], reifytab)
+        in
+          (ctor rts, reifytab')
+        end
+    | NONE =>
+        case get_first_match atom_pats t of
+          SOME ((vars, ctor), env) =>
+            let
+              val ts = map (snd o the o Vartab.lookup (snd env)) vars 
+              val (rvs, reifytab') = fold_rev (fn t => fn (rvs, reifytab) => Reifytab.get_var t reifytab
+                                               |>> (fn rv => rv :: rvs)) ts ([], reifytab)
+            in
+              (atom_ctor (ctor (map Int_of_integer rvs)), reifytab')
+            end
+        | NONE => raise TERM ("Can't reify term", [t])
+  end
+
+local
+  val aty = TVar (("'a", 0), ["HOL.type"])
+  val xn = ("x", 0)
+  val yn = ("y", 0)
+  val x = Term.Var (xn, aty)
+  val y = Term.Var (yn, aty)
+  val r = Term.Var (("r", 0), mk_rel_typ aty)
+
+  val closure_pats' = [ in_trancl_pat x y r, in_rtrancl_pat x y r
+                      , in_reflcl_pat x y r, in_converse_pat x y r]
+  val closure_pats = closure_pats' @ map HOLogic.mk_not closure_pats'
+  val eq_pat = HOLogic.mk_eq (x, y)
+  fun rem_pats r = [ eq_pat, HOLogic.mk_not eq_pat, in_pat x y r, HOLogic.mk_not (in_pat x y r) ]
+in
+
+  fun reify_closure_conj ctxt r =
+    let
+      val pats = [ (@{term conj} $ x $ y, [xn, yn], (fn [x, y] => And (x, y))) ]
+      val atom_pats = [ (eq_pat, [xn, yn], (fn [x, y] => (true, EQ (x, y))))
+                      , (in_trancl_pat x y r, [xn, yn], (fn [x, y] => (true, InTcl (x, y))))
+                      , (in_rtrancl_pat x y r, [xn, yn], (fn [x, y] => (true, InRtcl (x, y))))
+                      , (in_reflcl_pat x y r, [xn, yn], (fn [x, y] => (true, InReflcl (x, y))))
+                      , (in_converse_pat x y r, [xn, yn], (fn [x, y] => (true, InConv (x, y))))
+                      , (in_pat x y r, [xn, yn], (fn [x, y] => (true, In (x, y))))
+                      ]
+      fun negate_pat (pat, vars, ctor) = (HOLogic.mk_not pat, vars, ctor #>> not)
+    in
+      reify ctxt pats (atom_pats @ map negate_pat atom_pats) Atom
+    end
+
+  fun closure_tac simp_prems = Subgoal.FOCUS (fn {prems=prems, context=ctxt, ...} =>
+    let
+      fun is_atomic p = case Thm.prop_of p of tp $ _ => tp = HOLogic.Trueprop | _ => false
+      val prems = filter (fn p => null (Term.add_vars (Thm.prop_of p) []) andalso is_atomic p)
+                         (simp_prems @ prems)
+      val part_prems = partition_matches ctxt (map (fst o Term.dest_Var) [x, y]) closure_pats
+                                         (HOLogic.dest_Trueprop o Thm.prop_of) prems
+
+      fun closure_tac' (_, []) = no_tac
+        | closure_tac' (env, matched_prems) =
+          let
+            val thy = Proof_Context.theory_of ctxt
+            val r = Vartab.lookup (snd env) (fst (Term.dest_Var r)) |> the |> snd
+
+            fun try_match pats t =
+              Library.get_first (fn pat => try (Pattern.match thy (pat, t)) env) pats
+            fun try_match_thm pats p = try_match pats (HOLogic.dest_Trueprop (Thm.prop_of p))
+            val prems = matched_prems @
+                        filter (Option.isSome o try_match_thm (rem_pats r)) prems
+
+            val prems_conj_thm = foldl1 (fn (x, a) => @{thm conjI} OF [x, a]) prems
+              |> Conv.fconv_rule Thm.eta_conversion 
+            val prems_conj = Thm.prop_of prems_conj_thm
+            val (reified_prems_conj, reifytab) =
+              reify_closure_conj ctxt r (HOLogic.dest_Trueprop prems_conj) Reifytab.empty
+
+            val proof = Closure_Procedure.full_contr_prf reified_prems_conj
+
+            val assmtab = Termtab.make [(prems_conj, prems_conj_thm)]
+            val replay = replay_closure_prf_trm ctxt r reifytab assmtab
+          in
+            case proof of
+              NONE => no_tac
+            | SOME p => SOLVED' (resolve_tac ctxt [replay p]) 1
+          end
+    in
+      FIRST (map closure_tac' part_prems)
+    end)
+end
+
+val ad_absurdum_tac = SUBGOAL (fn (A, i) =>
+    case try (HOLogic.dest_Trueprop o Logic.strip_assums_concl) A of
+      SOME (nt $ _) =>
+        if nt = HOLogic.Not
+          then resolve0_tac [@{thm notI}] i
+          else resolve0_tac [@{thm ccontr}] i
+    | _ => resolve0_tac [@{thm ccontr}] i)
+
+fun tac simp_prems ctxt =
+  EVERY' [ad_absurdum_tac, CONVERSION Thm.eta_conversion, closure_tac simp_prems ctxt]
+
+end
\ No newline at end of file

--- a/src/HOL/Transitive_Closure.thy	Fri Sep 03 17:10:04 2021 +0200
+++ b/src/HOL/Transitive_Closure.thy	Mon Aug 23 13:43:02 2021 +0200
@@ -1275,64 +1275,99 @@
 
 subsection \<open>Setup of transitivity reasoner\<close>
 
+ML_file \<open>~~/src/HOL/Tools/closure_procedure.ML\<close>
+ML_file \<open>~~/src/HOL/Tools/closure_tac.ML\<close>
+
+lemma not_rtrancl_into_not_trancl: "(x, y) \<notin> r\<^sup>* \<Longrightarrow> (x, y) \<notin> r\<^sup>+"
+  using trancl_into_rtrancl by fast
+
+lemma reflcl_eq_or_in: "(x, y) \<in> r\<^sup>= \<longleftrightarrow> x = y \<or> x \<noteq> y \<and> (x, y) \<in> r"
+  by auto
+
+lemma not_reflcl_eq_and_in: "(x, y) \<notin> r\<^sup>= \<longleftrightarrow> x \<noteq> y \<and> (x, y) \<notin> r"
+  by auto
+
+lemma not_in_converse: "(x, y) \<notin> r\<inverse> \<longleftrightarrow> (y, x) \<notin> r"
+  using converse_iff by blast
+
+lemma not_rtranclp_into_not_tranclp: "\<not> r\<^sup>*\<^sup>* x y \<Longrightarrow> \<not> r\<^sup>+\<^sup>+ x y"
+  using tranclp_into_rtranclp by fast
+
+lemma rtranclp_eq_or_tranclp: "r\<^sup>*\<^sup>* x y \<longleftrightarrow> x = y \<or> x \<noteq> y \<and> r\<^sup>+\<^sup>+ x y"
+  using rtranclp.rtrancl_refl tranclp_into_rtranclp by (auto dest: rtranclpD)
+
+lemma reflclp_eq_or_in: "r\<^sup>=\<^sup>= x y \<longleftrightarrow> x = y \<or> x \<noteq> y \<and> r x y"
+  by auto
+
+lemma not_reflclp_eq_and_in: "\<not> r\<^sup>=\<^sup>= x y  \<longleftrightarrow> x \<noteq> y \<and> \<not> r x y"
+  by auto
+
+lemma not_in_conversep: "\<not> r\<inverse>\<inverse> x y \<longleftrightarrow> \<not> r y x"
+  using conversep_iff by blast
+
 ML \<open>
-structure Trancl_Tac = Trancl_Tac
-(
-  val r_into_trancl = @{thm trancl.r_into_trancl};
-  val trancl_trans  = @{thm trancl_trans};
-  val rtrancl_refl = @{thm rtrancl.rtrancl_refl};
-  val r_into_rtrancl = @{thm r_into_rtrancl};
-  val trancl_into_rtrancl = @{thm trancl_into_rtrancl};
-  val rtrancl_trancl_trancl = @{thm rtrancl_trancl_trancl};
-  val trancl_rtrancl_trancl = @{thm trancl_rtrancl_trancl};
-  val rtrancl_trans = @{thm rtrancl_trans};
+  local
+    fun mk_closure_type r = Term.fastype_of r --> Term.fastype_of r
+  
+    fun mk_Id ty = Const (@{const_name Id}, ty)
+    fun mk_eq ty = Const (@{const_name HOL.eq}, ty)
+    fun mk_reflcl mk_Id r =
+      let val r_ty = Term.fastype_of r
+      in Const (@{const_name sup}, r_ty --> r_ty --> r_ty) $ r $ mk_Id r_ty end
+  in
+    structure Closure_Tac_Rel = Closure_Tac(
+      fun mk_rel_typ ty = HOLogic.mk_prodT (ty, ty) |> HOLogic.mk_setT
 
-  fun decomp (\<^const>\<open>Trueprop\<close> $ t) =
-        let
-          fun dec (Const (\<^const_name>\<open>Set.member\<close>, _) $ (Const (\<^const_name>\<open>Pair\<close>, _) $ a $ b) $ rel) =
-              let
-                fun decr (Const (\<^const_name>\<open>rtrancl\<close>, _ ) $ r) = (r,"r*")
-                  | decr (Const (\<^const_name>\<open>trancl\<close>, _ ) $ r)  = (r,"r+")
-                  | decr r = (r,"r");
-                val (rel,r) = decr (Envir.beta_eta_contract rel);
-              in SOME (a,b,rel,r) end
-          | dec _ =  NONE
-        in dec t end
-    | decomp _ = NONE;
-);
+      fun in_pat x y r = HOLogic.mk_mem (HOLogic.mk_prod (x, y), r)
+      fun in_trancl_pat x y r = in_pat x y (Const (@{const_name trancl}, mk_closure_type r) $ r)
+      fun in_rtrancl_pat x y r = in_pat x y (Const (@{const_name rtrancl}, mk_closure_type r) $ r)
+      fun in_reflcl_pat x y r = in_pat x y (mk_reflcl mk_Id r)
+      fun in_converse_pat x y r = in_pat x y (Const (@{const_name converse}, Term.fastype_of r))
+  
+      val r_into_trancl_thm = @{thm r_into_trancl}
+      val trancl_trans_thm = @{thm trancl_trans}
+      val eq_in_thm = @{lemma \<open>v = x \<Longrightarrow> w = y \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> (v, w) \<in> r\<close> by simp}
+      val eq_in_trancl_thm = @{lemma \<open>v = x \<Longrightarrow> w = y \<Longrightarrow> (x, y) \<in> r\<^sup>+ \<Longrightarrow> (v, w) \<in> r\<^sup>+\<close> by simp}
+      val rtrancl_refl_thm = @{lemma \<open>x = y \<Longrightarrow> (x, y) \<in> r\<^sup>*\<close> by simp}
+      val not_rtrancl_into_not_trancl_thm = @{thm not_rtrancl_into_not_trancl}
+
+      val rtrancl_eq_or_trancl_conv = Conv.rewr_conv @{thm eq_reflection[OF rtrancl_eq_or_trancl]}
+      val reflcl_eq_or_in_conv = Conv.rewr_conv @{thm eq_reflection[OF reflcl_eq_or_in]}
+      val not_reflcl_eq_and_in_conv = Conv.rewr_conv @{thm eq_reflection[OF not_reflcl_eq_and_in]}
+      val in_converse_conv = Conv.rewr_conv @{thm eq_reflection[OF converse_iff]}
+      val not_in_converse_conv = Conv.rewr_conv @{thm eq_reflection[OF not_in_converse]}
+    );
 
-structure Tranclp_Tac = Trancl_Tac
-(
-  val r_into_trancl = @{thm tranclp.r_into_trancl};
-  val trancl_trans  = @{thm tranclp_trans};
-  val rtrancl_refl = @{thm rtranclp.rtrancl_refl};
-  val r_into_rtrancl = @{thm r_into_rtranclp};
-  val trancl_into_rtrancl = @{thm tranclp_into_rtranclp};
-  val rtrancl_trancl_trancl = @{thm rtranclp_tranclp_tranclp};
-  val trancl_rtrancl_trancl = @{thm tranclp_rtranclp_tranclp};
-  val rtrancl_trans = @{thm rtranclp_trans};
+    structure Closure_Tac_Pred = Closure_Tac(
+      fun mk_rel_typ ty = ty --> ty --> HOLogic.boolT
 
-  fun decomp (\<^const>\<open>Trueprop\<close> $ t) =
-        let
-          fun dec (rel $ a $ b) =
-            let
-              fun decr (Const (\<^const_name>\<open>rtranclp\<close>, _ ) $ r) = (r,"r*")
-                | decr (Const (\<^const_name>\<open>tranclp\<close>, _ ) $ r)  = (r,"r+")
-                | decr r = (r,"r");
-              val (rel,r) = decr rel;
-            in SOME (a, b, rel, r) end
-          | dec _ =  NONE
-        in dec t end
-    | decomp _ = NONE;
-);
+      fun in_pat x y r = r $ x $ y
+      fun in_trancl_pat x y r = in_pat x y (Const (@{const_name tranclp}, mk_closure_type r) $ r)
+      fun in_rtrancl_pat x y r = in_pat x y (Const (@{const_name rtranclp}, mk_closure_type r) $ r)
+      fun in_reflcl_pat x y r = in_pat x y (mk_reflcl mk_eq r)
+      fun in_converse_pat x y r = in_pat x y (Const (@{const_name conversep}, mk_closure_type r) $ r)
+  
+      val r_into_trancl_thm = @{thm tranclp.r_into_trancl}
+      val trancl_trans_thm = @{thm tranclp_trans}
+      val eq_in_thm = @{lemma \<open>v = x \<Longrightarrow> w = y \<Longrightarrow> r x y \<Longrightarrow> r v w\<close> by simp}
+      val eq_in_trancl_thm = @{lemma \<open>v = x \<Longrightarrow> w = y \<Longrightarrow> r\<^sup>+\<^sup>+ x y \<Longrightarrow> r\<^sup>+\<^sup>+ v w\<close> by simp}
+      val rtrancl_refl_thm = @{lemma \<open>x = y \<Longrightarrow> r\<^sup>*\<^sup>* x y\<close> by simp}
+      val not_rtrancl_into_not_trancl_thm = @{thm not_rtranclp_into_not_tranclp}
+
+      val rtrancl_eq_or_trancl_conv = Conv.rewr_conv @{thm eq_reflection[OF rtranclp_eq_or_tranclp]}
+      val reflcl_eq_or_in_conv = Conv.rewr_conv @{thm eq_reflection[OF reflclp_eq_or_in]}
+      val not_reflcl_eq_and_in_conv = Conv.rewr_conv @{thm eq_reflection[OF not_reflclp_eq_and_in]}
+      val in_converse_conv = Conv.rewr_conv @{thm eq_reflection[OF conversep_iff]}
+      val not_in_converse_conv = Conv.rewr_conv @{thm eq_reflection[OF not_in_conversep]}
+    );
+  end
 \<close>
 
 setup \<open>
   map_theory_simpset (fn ctxt => ctxt
-    addSolver (mk_solver "Trancl" Trancl_Tac.trancl_tac)
-    addSolver (mk_solver "Rtrancl" Trancl_Tac.rtrancl_tac)
-    addSolver (mk_solver "Tranclp" Tranclp_Tac.trancl_tac)
-    addSolver (mk_solver "Rtranclp" Tranclp_Tac.rtrancl_tac))
+    addSolver (mk_solver "RTrancl" (Closure_Tac_Rel.tac (Simplifier.prems_of ctxt)))
+    addSolver (mk_solver "RTranclp" (Closure_Tac_Pred.tac (Simplifier.prems_of ctxt)))
+  )
 \<close>
 
 lemma transp_rtranclp [simp]: "transp R\<^sup>*\<^sup>*"
@@ -1340,17 +1375,11 @@
 
 text \<open>Optional methods.\<close>
 
-method_setup trancl =
-  \<open>Scan.succeed (SIMPLE_METHOD' o Trancl_Tac.trancl_tac)\<close>
-  \<open>simple transitivity reasoner\<close>
 method_setup rtrancl =
-  \<open>Scan.succeed (SIMPLE_METHOD' o Trancl_Tac.rtrancl_tac)\<close>
+  \<open>Scan.succeed (SIMPLE_METHOD' o Closure_Tac_Rel.tac [])\<close>
   \<open>simple transitivity reasoner\<close>
-method_setup tranclp =
-  \<open>Scan.succeed (SIMPLE_METHOD' o Tranclp_Tac.trancl_tac)\<close>
-  \<open>simple transitivity reasoner (predicate version)\<close>
 method_setup rtranclp =
-  \<open>Scan.succeed (SIMPLE_METHOD' o Tranclp_Tac.rtrancl_tac)\<close>
+  \<open>Scan.succeed (SIMPLE_METHOD' o Closure_Tac_Pred.tac [])\<close>
   \<open>simple transitivity reasoner (predicate version)\<close>
 
 end