--- a/QuotMain.thy	Mon Nov 23 13:46:14 2009 +0100
+++ b/QuotMain.thy	Mon Nov 23 13:55:31 2009 +0100
@@ -1449,6 +1449,76 @@
   end
 *}
 
+(* rep-abs injection *)
+
+ML {*
+(* FIXME: is this the right get_fun function for rep-abs injection *)
+fun mk_repabs lthy (T, T') trm = 
+  Quotient_Def.get_fun repF lthy (T, T') 
+  $ (Quotient_Def.get_fun absF lthy (T, T') $ trm)
+*}
+
+ML {*
+(* replaces a term for the bound variable, *)
+(* possible capture                        *)
+fun replace_bnd0 (trm, Abs (x, T, t)) =
+  Abs (x, T, subst_bound (trm, t))
+*}
+
+
+ML {*
+(* bound variables need to be treated properly,  *)
+(* as the type of subterms need to be calculated *)
+
+fun is_lifted_const h gh = is_Const h andalso is_Const gh andalso not (h = gh)
+
+fun inj_REPABS lthy (rtrm, qtrm) =
+let
+  val rty = fastype_of rtrm
+  val qty = fastype_of qtrm
+in
+  case (rtrm, qtrm) of
+    (Const (@{const_name "Ball"}, T) $ r $ t, Const (@{const_name "All"}, _) $ t') =>
+       Const (@{const_name "Ball"}, T) $ r $ (inj_REPABS lthy (t, t'))
+  | (Const (@{const_name "Bex"}, T) $ r $ t, Const (@{const_name "Ex"}, _) $ t') =>
+       Const (@{const_name "Bex"}, T) $ r $ (inj_REPABS lthy (t, t'))
+  | (Const (@{const_name "Babs"}, T) $ r $ t, t') =>
+       Const (@{const_name "Babs"}, T) $ r $ (inj_REPABS lthy (t, t'))
+  | (Abs (x, T, t), Abs (x', T', t')) =>
+      let
+        val (y, s) = Term.dest_abs (x, T, t)
+        val (_, s') = Term.dest_abs (x', T', t')
+        val yvar = Free (y, T)
+        val res = lambda yvar (inj_REPABS lthy (s, s'))
+      in
+        if rty = qty
+        then res
+        else if T = T'
+             then mk_repabs lthy (rty, qty) res
+             else mk_repabs lthy (rty, qty) (replace_bnd0 (mk_repabs lthy (T, T') (Bound 0), res))
+      end
+  | _ =>
+      let
+        val (rhead, rargs) = strip_comb rtrm
+        val (qhead, qargs) = strip_comb qtrm
+        (* TODO:  val rhead' = inj_REPABS lthy (rhead, qhead) *)
+        val rhead' = rhead;
+        val rargs' = map (inj_REPABS lthy) (rargs ~~ qargs);
+        val result = list_comb (rhead', rargs');
+      in
+        if rty = qty then result else
+        if (is_lifted_const rhead qhead) then mk_repabs lthy (rty, qty) result else
+        if ((Term.is_Free rhead) andalso (length rargs' > 0)) then mk_repabs lthy (rty, qty) result else
+        if rargs' = [] then rhead' else result
+      end
+end
+*}
+
+ML {*
+fun mk_inj_REPABS_goal lthy (rtrm, qtrm) =
+  Logic.mk_equals (rtrm, Syntax.check_term lthy (inj_REPABS lthy (rtrm, qtrm)))
+*}
+
 
 end