# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1258989170 -3600
# Node ID 573e2b625e8e68d8564631fc6dcdf211264bbe1f
# Parent  cc96aaf6484c5318c564b45f3da6b73b9dc229a1
a version of inj_REPABS (needs to be looked at again later)

diff -r cc96aaf6484c -r 573e2b625e8e QuotMain.thy
--- a/QuotMain.thy	Mon Nov 23 15:08:25 2009 +0100
+++ b/QuotMain.thy	Mon Nov 23 16:12:50 2009 +0100
@@ -1380,22 +1380,13 @@
   $ (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))
-
-(* FIXME: this should be a proper test with the qcinfo *)
-fun is_lifted_const h gh = 
-  is_Const h andalso is_Const gh andalso not (h = gh)
-*}
-
+ML {* length *}
 
 ML {*
 (* bound variables need to be treated properly,  *)
 (* as the type of subterms need to be calculated *)
 
+
 fun inj_REPABS lthy (rtrm, qtrm) =
 let
   val rty = fastype_of rtrm
@@ -1413,32 +1404,34 @@
         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'))
+        val result = 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))
+        if rty = qty 
+        then result
+        else mk_repabs lthy (rty, qty) result
       end
   | _ =>
+      (* FIXME / TODO: this is a case that needs to be looked at          *)
+      (* - variables get a rep-abs insde and outside an application       *)
+      (* - constants only get a rep-abs on the outside of the application *)
+      (* - applications get a rep-abs insde and outside an application    *)
       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');
+        val rargs' = map (inj_REPABS lthy) (rargs ~~ qargs)
       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
+        if rty = qty
+        then list_comb (rhead, rargs')
+        else
+          case (rhead, qhead, length rargs') of
+            (Const _, Const _, 0) => mk_repabs lthy (rty, qty) rhead
+          | (Free  _, Free  _, 0) =>  mk_repabs lthy (rty, qty) rhead
+          | (Const _, Const _, _) =>  mk_repabs lthy (rty, qty) (list_comb (rhead, rargs')) 
+          | (Free (x, T), Free (x', T'), _) => 
+               mk_repabs lthy (rty, qty) (list_comb (mk_repabs lthy (T, T') rhead, rargs'))
+          | (Abs _, Abs _, _ ) =>
+               mk_repabs lthy (rty, qty) (list_comb (inj_REPABS lthy (rhead, qhead), rargs')) 
+          | _ => trm_lift_error lthy rtrm qtrm
       end
 end
 *}