diff -r e83a6e452843 -r 6ed87b3d358c QuotMain.thy
--- a/QuotMain.thy	Fri Oct 30 15:52:47 2009 +0100
+++ b/QuotMain.thy	Fri Oct 30 16:24:07 2009 +0100
@@ -447,106 +447,6 @@
 *}
 
 ML {*
-(* trm \<Rightarrow> new_trm *)
-fun regularise trm rty rel lthy =
-  case trm of
-    Abs (x, T, t) =>
-      if (needs_lift rty T) then let
-        val ([x'], lthy2) = Variable.variant_fixes [x] lthy;
-        val v = Free (x', T);
-        val t' = subst_bound (v, t);
-        val rec_term = regularise t' rty rel lthy2;
-        val lam_term = Term.lambda_name (x, v) rec_term;
-        val sub_res_term = tyRel T rty rel lthy;
-        val respects = Const (@{const_name Respects}, (fastype_of sub_res_term) --> T --> @{typ bool});
-        val res_term = respects $ sub_res_term;
-        val ty = fastype_of trm;
-        val rabs = Const (@{const_name Babs}, (fastype_of res_term) --> ty --> ty);
-        val rabs_term = (rabs $ res_term) $ lam_term;
-      in
-        rabs_term
-      end else let
-        val ([x'], lthy2) = Variable.variant_fixes [x] lthy;
-        val v = Free (x', T);
-        val t' = subst_bound (v, t);
-        val rec_term = regularise t' rty rel lthy2;
-      in
-        Term.lambda_name (x, v) rec_term
-      end
-  | ((Const (@{const_name "All"}, at)) $ (Abs (x, T, t))) =>
-      if (needs_lift rty T) then let
-        val ([x'], lthy2) = Variable.variant_fixes [x] lthy;
-        val v = Free (x', T);
-        val t' = subst_bound (v, t);
-        val rec_term = regularise t' rty rel lthy2;
-        val lam_term = Term.lambda_name (x, v) rec_term;
-        val sub_res_term = tyRel T rty rel lthy;
-        val respects = Const (@{const_name Respects}, (fastype_of sub_res_term) --> T --> @{typ bool});
-        val res_term = respects $ sub_res_term;
-        val ty = fastype_of lam_term;
-        val rall = Const (@{const_name Ball}, (fastype_of res_term) --> ty --> @{typ bool});
-        val rall_term = (rall $ res_term) $ lam_term;
-      in
-        rall_term
-      end else let
-        val ([x'], lthy2) = Variable.variant_fixes [x] lthy;
-        val v = Free (x', T);
-        val t' = subst_bound (v, t);
-        val rec_term = regularise t' rty rel lthy2;
-        val lam_term = Term.lambda_name (x, v) rec_term
-      in
-        Const(@{const_name "All"}, at) $ lam_term
-      end
-  | ((Const (@{const_name "All"}, at)) $ P) =>
-      let
-        val (_, [al, _]) = dest_Type (fastype_of P);
-        val ([x], lthy2) = Variable.variant_fixes [""] lthy;
-        val v = (Free (x, al));
-        val abs = Term.lambda_name (x, v) (P $ v);
-      in regularise ((Const (@{const_name "All"}, at)) $ abs) rty rel lthy2 end
-  | ((Const (@{const_name "Ex"}, at)) $ (Abs (x, T, t))) =>
-      if (needs_lift rty T) then let
-        val ([x'], lthy2) = Variable.variant_fixes [x] lthy;
-        val v = Free (x', T);
-        val t' = subst_bound (v, t);
-        val rec_term = regularise t' rty rel lthy2;
-        val lam_term = Term.lambda_name (x, v) rec_term;
-        val sub_res_term = tyRel T rty rel lthy;
-        val respects = Const (@{const_name Respects}, (fastype_of sub_res_term) --> T --> @{typ bool});
-        val res_term = respects $ sub_res_term;
-        val ty = fastype_of lam_term;
-        val rall = Const (@{const_name Bex}, (fastype_of res_term) --> ty --> @{typ bool});
-        val rall_term = (rall $ res_term) $ lam_term;
-      in
-        rall_term
-      end else let
-        val ([x'], lthy2) = Variable.variant_fixes [x] lthy;
-        val v = Free (x', T);
-        val t' = subst_bound (v, t);
-        val rec_term = regularise t' rty rel lthy2;
-        val lam_term = Term.lambda_name (x, v) rec_term
-      in
-        Const(@{const_name "Ex"}, at) $ lam_term
-      end
-  | ((Const (@{const_name "Ex"}, at)) $ P) =>
-      let
-        val (_, [al, _]) = dest_Type (fastype_of P);
-        val ([x], lthy2) = Variable.variant_fixes [""] lthy;
-        val v = (Free (x, al));
-        val abs = Term.lambda_name (x, v) (P $ v);
-      in regularise ((Const (@{const_name "Ex"}, at)) $ abs) rty rel lthy2 end
-  | a $ b => (regularise a rty rel lthy) $ (regularise b rty rel lthy)
-  | _ => trm
-
-*}
-
-(* my version of regularise *)
-(****************************)
-
-(* some helper functions *)
-
-
-ML {*
 fun mk_babs ty ty' = Const (@{const_name "Babs"}, [ty' --> @{typ bool}, ty] ---> ty)
 fun mk_ball ty = Const (@{const_name "Ball"}, [ty, ty] ---> @{typ bool})
 fun mk_bex ty = Const (@{const_name "Bex"}, [ty, ty] ---> @{typ bool})
@@ -566,47 +466,51 @@
   | _ => f trm
 *}
 
-
-(* FIXME: assumes always the typ is qty! *)
 (* FIXME: if there are more than one quotient, then you have to look up the relation *)
 ML {*
-fun my_reg rel trm =
+fun my_reg lthy rel rty trm =
   case trm of
     Abs (x, T, t) =>
-       let 
-          val ty1 = fastype_of trm
-       in
-         (mk_babs ty1 T) $ (mk_resp T $ rel) $ (apply_subt (my_reg rel) trm)    
-       end
-  | Const (@{const_name "All"}, ty) $ t =>
-       let 
+       if (needs_lift rty T) then
+         let
+            val rrel = tyRel T rty rel lthy
+         in
+           (mk_babs (fastype_of trm) T) $ (mk_resp T $ rrel) $ (apply_subt (my_reg lthy rel rty) trm)
+         end
+       else
+         Abs(x, T, (apply_subt (my_reg lthy rel rty) t))
+  | Const (@{const_name "All"}, ty) $ (t as Abs (x, T, _)) =>
+       let
           val ty1 = domain_type ty
           val ty2 = domain_type ty1
+          val rrel = tyRel T rty rel lthy
        in
-         (mk_ball ty1) $ (mk_resp ty2 $ rel) $ (apply_subt (my_reg rel) t)      
+         if (needs_lift rty T) then
+           (mk_ball ty1) $ (mk_resp ty2 $ rrel) $ (apply_subt (my_reg lthy rel rty) t)
+         else
+           Const (@{const_name "All"}, ty) $ apply_subt (my_reg lthy rel rty) t
        end
-  | Const (@{const_name "Ex"}, ty) $ t =>
-       let 
+  | Const (@{const_name "Ex"}, ty) $ (t as Abs (x, T, _)) =>
+       let
           val ty1 = domain_type ty
           val ty2 = domain_type ty1
+          val rrel = tyRel T rty rel lthy
        in
-         (mk_bex ty1) $ (mk_resp ty2 $ rel) $ (apply_subt (my_reg rel) t)    
+         if (needs_lift rty T) then
+           (mk_bex ty1) $ (mk_resp ty2 $ rrel) $ (apply_subt (my_reg lthy rel rty) t)
+         else
+           Const (@{const_name "Ex"}, ty) $ apply_subt (my_reg lthy rel rty) t
        end
-  | t1 $ t2 => (my_reg rel t1) $ (my_reg rel t2)
+  | t1 $ t2 => (my_reg lthy rel rty t1) $ (my_reg lthy rel rty t2)
   | _ => trm
 *}
 
-
-(*fun prove_reg trm \<Rightarrow> thm (we might need some facts to do this)
-  trm == new_trm
-*)
-
 text {* Assumes that the given theorem is atomized *}
 ML {*
   fun build_regularize_goal thm rty rel lthy =
      Logic.mk_implies
        ((prop_of thm),
-       (regularise (prop_of thm) rty rel lthy))
+       (my_reg lthy rel rty (prop_of thm)))
 *}
 
 ML {*