--- a/QuotMain.thy	Thu Nov 19 14:17:10 2009 +0100
+++ b/QuotMain.thy	Fri Nov 20 13:03:01 2009 +0100
@@ -331,7 +331,7 @@
        end
   | Const (@{const_name "op ="}, ty) $ t =>
       if needs_lift rty (fastype_of t) then
-        (tyRel (fastype_of t) rty rel lthy) $ t
+        (tyRel (fastype_of t) rty rel lthy) $ t   (* FIXME: t should be regularised too *)
       else Const (@{const_name "op ="}, ty) $ (my_reg lthy rel rty t)
   | t1 $ t2 => (my_reg lthy rel rty t1) $ (my_reg lthy rel rty t2)
   | _ => trm
@@ -1144,19 +1144,112 @@
   end
 *}
 
+(******************************************)
+(* version with explicit qtrm             *)
+(******************************************)
+
+(* exception for when qtrm and rtrm do not match *)
+ML {* exception LIFT_MATCH of string *}
+
 ML {*
-fun my_lift qtrm rthm lthy =
+fun mk_resp_arg lthy (rty, qty) =
 let
   val thy = ProofContext.theory_of lthy
+in  
+  case (rty, qty) of
+    (Type (s, tys), Type (s', tys')) =>
+       if s = s' 
+       then let
+              val SOME map_info = maps_lookup thy s
+              val args = map (mk_resp_arg lthy) (tys ~~tys')
+            in
+              list_comb (Const (#relfun map_info, dummyT), args) 
+            end  
+       else let  
+              val SOME qinfo = quotdata_lookup_thy thy s'
+            in
+              #rel qinfo
+            end
+    | _ => HOLogic.eq_const dummyT
+end
+*}
 
-  val a_rthm = atomize_thm rthm
-  val a_qtrm = ObjectLogic.atomize_term thy qtrm
+ML {*
+val mk_babs = Const (@{const_name "Babs"}, dummyT)
+val mk_ball = Const (@{const_name "Ball"}, dummyT)
+val mk_bex  = Const (@{const_name "Bex"}, dummyT)
+val mk_resp = Const (@{const_name Respects}, dummyT)
+*}
+
+ML {*
+(* applies f to the subterm of an abstractions, otherwise to the given term *)
+(* abstracted variables do not have to be treated specially *)
+fun apply_subt f trm1 trm2 =
+  case (trm1, trm2) of
+    (Abs (x, T, t), Abs (x', T', t')) => Abs (x, T, f t t')
+  | _ => f trm1 trm2
+
+fun qnt_typ ty = domain_type (domain_type ty)
+*}
 
-  val _ = Syntax.string_of_term lthy (prop_of a_rthm) |> writeln
-  val _ = Syntax.string_of_term lthy a_qtrm |> writeln
-in
-  (a_rthm, a_qtrm)
-end
+ML {*
+fun REGULARIZE_aux lthy rtrm qtrm =
+  case (rtrm, qtrm) of
+    (Abs (x, T, t), Abs (x', T', t')) =>
+       let
+         val subtrm = REGULARIZE_aux lthy t t'
+       in     
+         if T = T'
+         then Abs (x, T, subtrm)
+         else  mk_babs $ (mk_resp $ mk_resp_arg lthy (T, T')) $ subtrm
+       end
+  | (Const (@{const_name "All"}, ty) $ t, Const (@{const_name "All"}, ty') $ t') =>
+       let
+         val subtrm = apply_subt (REGULARIZE_aux lthy) t t'
+       in
+         if ty = ty'
+         then Const (@{const_name "All"}, ty) $ subtrm
+         else mk_ball $ (mk_resp $ mk_resp_arg lthy (qnt_typ ty, qnt_typ ty')) $ subtrm
+       end
+  | (Const (@{const_name "Ex"}, ty) $ t, Const (@{const_name "Ex"}, ty') $ t') =>
+       let
+         val subtrm = apply_subt (REGULARIZE_aux lthy) t t'
+       in
+         if ty = ty'
+         then Const (@{const_name "Ex"}, ty) $ subtrm
+         else mk_bex $ (mk_resp $ mk_resp_arg lthy (qnt_typ ty, qnt_typ ty')) $ subtrm
+       end
+  (* FIXME: why is there a case for equality? is it correct? *)
+  | (Const (@{const_name "op ="}, ty) $ t, Const (@{const_name "op ="}, ty') $ t') =>
+       let
+         val subtrm = REGULARIZE_aux lthy t t'
+       in
+         if ty = ty'
+         then Const (@{const_name "op ="}, ty) $ subtrm
+         else mk_resp_arg lthy (ty, ty') $ subtrm
+       end 
+  | (t1 $ t2, t1' $ t2') =>
+       (REGULARIZE_aux lthy t1 t1') $ (REGULARIZE_aux lthy t2 t2')
+  | (Free (x, ty), Free (x', ty')) =>
+       if x = x' 
+       then rtrm 
+       else raise LIFT_MATCH "quotient and lifted theorem do not match"
+  | (Bound i, Bound i') =>
+       if i = i' 
+       then rtrm 
+       else raise LIFT_MATCH "quotient and lifted theorem do not match"
+  | (Const (s, ty), Const (s', ty')) =>
+       if s = s' andalso ty = ty'
+       then rtrm
+       else rtrm (* FIXME: check correspondence according to definitions *) 
+  | _ => raise LIFT_MATCH "quotient and lifted theorem do not match"
+*}
+
+ML {*
+fun REGULARIZE_trm lthy rtrm qtrm =
+  REGULARIZE_aux lthy rtrm qtrm
+  |> Syntax.check_term lthy
+  
 *}
 
 end