# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1258805675 -3600
# Node ID e755a5da14c8d9dd4c026a098bd3e1fbe8489c7d
# Parent  3d7a3a1419221bf79f761f487a9f26d76f78112f
my first version of repabs injection

diff -r 3d7a3a141922 -r e755a5da14c8 IntEx.thy
--- a/IntEx.thy	Sat Nov 21 11:16:48 2009 +0100
+++ b/IntEx.thy	Sat Nov 21 13:14:35 2009 +0100
@@ -163,22 +163,63 @@
 apply(tactic {* REGULARIZE_tac' @{context} @{thm "TrueI"} @{thm my_int_equiv} *})
 done
 
-(*
+ML {*
+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 {*
-fun inj_REPABS lthy rtrm qtrm =
+fun replace_bnd0 (trm, Abs (x, T, t)) =
+  Abs (x, T, subst_bound (trm, t))
+*}
+
+ML {*
+fun inj_REPABS_aux lthy (rtrm, qtrm) =
+let
+  val rty = fastype_of rtrm
+  val qty = fastype_of qtrm
+in
   case (rtrm, qtrm) of
     (Abs (x, T, t), Abs (x', T', t')) =>
-    if T = T'
-    then Abs (x, T, inj_REPABS lthy t t')
-    else 
-      let 
-         
-      in
+    let
+      val (y, s) = Term.dest_abs (x, T, t)
+      val (y', s') = Term.dest_abs (x', T', t')
+      val yvar = Free (y, T)
+      val res = lambda yvar (inj_REPABS_aux lthy (s, s'))
+    in
+      if T = T'
+      then res
+      else mk_repabs lthy (rty, qty) (replace_bnd0 (mk_repabs lthy (T, T') (Bound 0), res))
+    end
+  (* FIXME: Does one havae to look at the abstraction or go under the lambda. *) 
+  | (Const (@{const_name "Ball"}, T) $ r $ t, Const (@{const_name "All"}, _) $ t') =>
+      Const (@{const_name "Ball"}, T) $ r $ (inj_REPABS_aux lthy (t, t'))
+  | (Const (@{const_name "Bex"}, T) $ r $ t, Const (@{const_name "Ex"}, _) $ t') =>
+      Const (@{const_name "Bex"}, T) $ r $ (inj_REPABS_aux lthy (t, t'))
+  | (rtrm as _ $ _, qtrm as _ $ _) => 
+    let
+      val (rhead, rargs) = Term.strip_comb rtrm
+      val (qhead, qargs) = Term.strip_comb qtrm
+      val rhead' = inj_REPABS_aux lthy (rhead, qhead)
+      val rargs' = map (inj_REPABS_aux lthy) (rargs ~~ qargs)
+      val res = list_comb (rhead', rargs')
+    in
+      if rty = qty
+      then res
+      else mk_repabs lthy (rty, qty) res
+    end
+  (* FIXME: cases for frees and vars *)
+  | _ => rtrm
+end
+*}
 
-      end
-  | _ => rtrm
+
+ML {*
+fun inj_REPABS lthy (rtrm, qtrm) =
+  inj_REPABS_aux lthy (rtrm, qtrm)
+  |> Syntax.check_term lthy
 *}
-*)
 
 lemma plus_assoc_pre:
   shows "my_plus (my_plus i j) k \<approx> my_plus i (my_plus j k)"
@@ -191,15 +232,31 @@
 ML {* val test2 = lift_thm_my_int @{context} @{thm plus_assoc_pre} *}
 
 ML {*
-  val aqtrm = (prop_of (atomize_thm test2))
-  val artrm = (prop_of (atomize_thm @{thm plus_assoc_pre})) 
+  val arthm = atomize_thm @{thm plus_assoc_pre}
+  val aqthm = atomize_thm test2
+
+  val aqtrm = prop_of aqthm
+  val artrm = prop_of arthm
 *}
 
-prove {* mk_REGULARIZE_goal @{context} artrm aqtrm  *}
+prove testtest: {* mk_REGULARIZE_goal @{context} artrm aqtrm  *}
 apply(tactic {* ObjectLogic.full_atomize_tac 1 *})
 apply(tactic {* REGULARIZE_tac' @{context} @{thm "TrueI"} @{thm my_int_equiv} *})
 done
 
+ML {* @{thm testtest} OF [arthm] *}
+
+ML {* 
+  val reg_atrm = prop_of (@{thm testtest} OF [arthm]);
+*}
+
+ML {*
+inj_REPABS @{context} (reg_atrm, aqtrm)  
+|> Syntax.string_of_term @{context}
+|> writeln
+*}
+
+
 
 
 
diff -r 3d7a3a141922 -r e755a5da14c8 QuotMain.thy
--- a/QuotMain.thy	Sat Nov 21 11:16:48 2009 +0100
+++ b/QuotMain.thy	Sat Nov 21 13:14:35 2009 +0100
@@ -1282,7 +1282,7 @@
        in     
          if ty = ty'
          then Abs (x, ty, subtrm)
-         else  mk_babs $ (mk_resp $ mk_resp_arg lthy (ty, ty')) $ subtrm
+         else mk_babs $ (mk_resp $ mk_resp_arg lthy (ty, ty')) $ subtrm
        end
   | (Const (@{const_name "All"}, ty) $ t, Const (@{const_name "All"}, ty') $ t') =>
        let
@@ -1392,6 +1392,7 @@
 *}
 
 ML {*
+(* FIXME: change rel_refl rel_eqv *)
 fun REGULARIZE_tac' lthy rel_refl rel_eqv =
    (REPEAT1 o FIRST1) 
      [(K (print_tac "start")) THEN' (K no_tac),