--- a/QuotMain.thy	Sun Nov 29 09:38:07 2009 +0100
+++ b/QuotMain.thy	Sun Nov 29 17:47:37 2009 +0100
@@ -136,9 +136,6 @@
 
 end
 
-lemma tst: "EQUIV bla"
-sorry
-
 lemma equiv_trans2:
   assumes e: "EQUIV R"
   and     ac: "R a c"
@@ -235,8 +232,6 @@
 
 section {* Debugging infrastructure for testing tactics *}
 
-
-
 ML {*
 fun my_print_tac ctxt s i thm =
 let
@@ -263,6 +258,7 @@
 fun NDT ctxt s tac thm = tac thm  
 *}
 
+
 section {*  Infrastructure about definitions *}
 
 (* Does the same as 'subst' in a given theorem *)
@@ -347,6 +343,64 @@
   end
 *}
 
+section {* Infrastructure for special quotient identity *}
+
+definition
+  "qid TYPE('a) TYPE('b) x \<equiv> x"
+
+ML {*
+fun get_typ1 (Type ("itself", [T])) = T 
+fun get_typ2 (Const ("TYPE", T)) = get_typ1 T
+fun get_tys (Const (@{const_name "qid"},_) $ ty1 $ ty2) =
+  (get_typ2 ty1, get_typ2 ty2)
+
+fun is_qid (Const (@{const_name "qid"},_) $ _ $ _) = true
+  | is_qid _ = false
+
+
+fun mk_itself ty = Type ("itself", [ty])
+fun mk_TYPE ty = Const ("TYPE", mk_itself ty)
+fun mk_qid (rty, qty, trm) = 
+  Const (@{const_name "qid"}, [mk_itself rty, mk_itself qty, dummyT] ---> dummyT) 
+    $ mk_TYPE rty $ mk_TYPE qty $ trm
+*}
+
+ML {*
+fun insertion_aux rtrm qtrm =
+  case (rtrm, qtrm) of
+    (Abs (x, ty, t), Abs (x', ty', t')) =>
+       let
+         val (y, s) = Term.dest_abs (x, ty, t)
+         val (_, s') = Term.dest_abs (x', ty', t')
+         val yvar = Free (y, ty)
+         val result = Term.lambda_name (y, yvar) (insertion_aux s s')
+       in     
+         if ty = ty'
+         then result
+         else mk_qid (ty, ty', result)
+       end
+  | (t1 $ t2, t1' $ t2') =>
+       let 
+         val rty = fastype_of rtrm
+         val qty = fastype_of qtrm 
+         val subtrm1 = insertion_aux t1 t1' 
+         val subtrm2 = insertion_aux t2 t2'
+       in
+         if rty = qty
+         then subtrm1 $ subtrm2
+         else mk_qid (rty, qty, subtrm1 $ subtrm2)
+       end
+  | (Free (_, ty), Free (_, ty')) =>
+       if ty = ty'
+       then rtrm 
+       else mk_qid (ty, ty', rtrm)
+  | (Const (s, ty), Const (s', ty')) =>
+       if s = s' andalso ty = ty'
+       then rtrm
+       else mk_qid (ty, ty', rtrm) 
+  | (_, _) => raise (LIFT_MATCH "insertion")
+*}
+
 section {* Regularization *} 
 
 (*
@@ -470,10 +524,9 @@
        end 
   | (t1 $ t2, t1' $ t2') =>
        (regularize_trm lthy t1 t1') $ (regularize_trm lthy t2 t2')
-  | (Free (x, ty), Free (x', ty')) =>
-       if x = x' 
-       then rtrm     (* FIXME: check whether types corresponds *)
-       else raise (LIFT_MATCH "regularize (frees)")
+  | (Free (x, ty), Free (x', ty')) => 
+       (* this case cannot arrise as we start with two fully atomized terms *)
+       raise (LIFT_MATCH "regularize (frees)")
   | (Bound i, Bound i') =>
        if i = i' 
        then rtrm 
@@ -734,7 +787,7 @@
         val (y, s) = Term.dest_abs (x, T, t)
         val (_, s') = Term.dest_abs (x', T', t')
         val yvar = Free (y, T)
-        val result = lambda yvar (inj_repabs_trm lthy (s, s'))
+        val result = Term.lambda_name (y, yvar) (inj_repabs_trm lthy (s, s'))
       in
         if rty = qty 
         then result
@@ -790,7 +843,6 @@
   handle _ => no_tac)
 *}
 
-
 ML {*
 fun quotient_tac quot_thms =
   REPEAT_ALL_NEW (FIRST'