diff -r 54f186bb5e3e -r 3b21b24a5fb6 Quot/quotient_term.ML
--- a/Quot/quotient_term.ML	Tue Dec 22 22:10:48 2009 +0100
+++ b/Quot/quotient_term.ML	Wed Dec 23 10:31:54 2009 +0100
@@ -21,10 +21,13 @@
 
 exception LIFT_MATCH of string
 
-(* Calculates the aggregate abs and rep functions for a given type; *) 
-(* repF is for constants' arguments; absF is for constants;         *)
-(* function types need to be treated specially, since repF and absF *)
-(* change                                                           *)
+(*******************************)
+(* Aggregate Rep/Abs Functions *)
+(*******************************)
+
+(* The flag repF is for types in negative position, while absF is   *) 
+(* for types in positive position. Because of this, function types  *)
+(* need to be treated specially, since there the polarity changes.  *)
 
 datatype flag = absF | repF
 
@@ -38,19 +41,19 @@
     absF => Const (@{const_name "comp"}, dummyT) $ trm1 $ trm2
   | repF => Const (@{const_name "comp"}, dummyT) $ trm2 $ trm1
 
-fun absrep_fun_aux lthy s fs =
+fun get_map ctxt ty_str =
 let
-  val thy = ProofContext.theory_of lthy
-  val exc = LIFT_MATCH (space_implode " " ["absrep_fun_aux: no map for type", quote s, "."])
-  val info = maps_lookup thy s handle NotFound => raise exc
+  val thy = ProofContext.theory_of ctxt
+  val exc = LIFT_MATCH (space_implode " " ["absrep_fun: no map for type", quote ty_str, "."])
+  val info = maps_lookup thy ty_str handle NotFound => raise exc
 in
-  list_comb (Const (#mapfun info, dummyT), fs)
+  Const (#mapfun info, dummyT)
 end
 
-fun get_const flag lthy _ qty =
+fun get_absrep_const flag ctxt _ qty =
 (* FIXME: check here that the type-constructors of _ and qty are related *)
 let
-  val thy = ProofContext.theory_of lthy
+  val thy = ProofContext.theory_of ctxt
   val qty_name = Long_Name.base_name (fst (dest_Type qty))
 in
   case flag of
@@ -58,41 +61,42 @@
   | repF => Const (Sign.full_bname thy ("rep_" ^ qty_name), dummyT)
 end
 
-fun absrep_fun flag lthy (rty, qty) =
+fun absrep_fun flag ctxt (rty, qty) =
   if rty = qty then mk_identity qty else
   case (rty, qty) of
     (Type ("fun", [ty1, ty2]), Type ("fun", [ty1', ty2'])) =>
-     let
-       val fs_ty1 = absrep_fun (negF flag) lthy (ty1, ty1')
-       val fs_ty2 = absrep_fun flag lthy (ty2, ty2')
-     in
-       absrep_fun_aux lthy "fun" [fs_ty1, fs_ty2]
-     end
+      let
+        val arg1 = absrep_fun (negF flag) ctxt (ty1, ty1')
+        val arg2 = absrep_fun flag ctxt (ty2, ty2')
+      in
+        list_comb (get_map ctxt "fun", [arg1, arg2])
+      end
   | (Type (s, _), Type (s', [])) =>
-     if s = s'
-     then mk_identity qty
-     else get_const flag lthy rty qty
+      if s = s'
+      then mk_identity qty
+      else get_absrep_const flag ctxt rty qty
   | (Type (s, tys), Type (s', tys')) =>
-     let
-        val args = map (absrep_fun flag lthy) (tys ~~ tys')
-     in
+      let
+        val args = map (absrep_fun flag ctxt) (tys ~~ tys')
+        val result = list_comb (get_map ctxt s, args)
+      in
         if s = s'
-        then absrep_fun_aux lthy s args
-        else mk_compose flag (get_const flag lthy rty qty, absrep_fun_aux lthy s args)
-     end
+        then result
+        else mk_compose flag (get_absrep_const flag ctxt rty qty, result)
+      end
   | (TFree x, TFree x') =>
-     if x = x'
-     then mk_identity qty
-     else raise (LIFT_MATCH "absrep_fun (frees)")
+      if x = x'
+      then mk_identity qty
+      else raise (LIFT_MATCH "absrep_fun (frees)")
   | (TVar _, TVar _) => raise (LIFT_MATCH "absrep_fun (vars)")
   | _ => raise (LIFT_MATCH "absrep_fun (default)")
 
-fun absrep_fun_chk flag lthy (rty, qty) =
-  absrep_fun flag lthy (rty, qty)
-  |> Syntax.check_term lthy
+fun absrep_fun_chk flag ctxt (rty, qty) =
+  absrep_fun flag ctxt (rty, qty)
+  |> Syntax.check_term ctxt
 
-(*
-Regularizing an rtrm means:
+
+(* Regularizing an rtrm means:
  
  - Quantifiers over types that need lifting are replaced 
    by bounded quantifiers, for example:
@@ -120,9 +124,9 @@
 
 (* builds the aggregate equivalence relation *)
 (* that will be the argument of Respects     *)
-fun mk_resp_arg lthy (rty, qty) =
+fun mk_resp_arg ctxt (rty, qty) =
 let
-  val thy = ProofContext.theory_of lthy
+  val thy = ProofContext.theory_of ctxt
 in  
   if rty = qty
   then HOLogic.eq_const rty
@@ -134,7 +138,7 @@
          let
            val exc = LIFT_MATCH ("mk_resp_arg (no map function found for type " ^ s) 
            val map_info = maps_lookup thy s handle NotFound => raise exc
-           val args = map (mk_resp_arg lthy) (tys ~~ tys')
+           val args = map (mk_resp_arg ctxt) (tys ~~ tys')
          in
            list_comb (Const (#relfun map_info, dummyT), args) 
          end  
@@ -180,43 +184,43 @@
 (* - for regularisation we do not need any      *)
 (*   special treatment of bound variables       *)
 
-fun regularize_trm lthy (rtrm, qtrm) =
+fun regularize_trm ctxt (rtrm, qtrm) =
   case (rtrm, qtrm) of
     (Abs (x, ty, t), Abs (_, ty', t')) =>
        let
-         val subtrm = Abs(x, ty, regularize_trm lthy (t, t'))
+         val subtrm = Abs(x, ty, regularize_trm ctxt (t, t'))
        in
          if ty = ty' then subtrm
-         else mk_babs $ (mk_resp $ mk_resp_arg lthy (ty, ty')) $ subtrm
+         else mk_babs $ (mk_resp $ mk_resp_arg ctxt (ty, ty')) $ subtrm
        end
 
   | (Const (@{const_name "All"}, ty) $ t, Const (@{const_name "All"}, ty') $ t') =>
        let
-         val subtrm = apply_subt (regularize_trm lthy) (t, t')
+         val subtrm = apply_subt (regularize_trm ctxt) (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
+         else mk_ball $ (mk_resp $ mk_resp_arg ctxt (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_trm lthy) (t, t')
+         val subtrm = apply_subt (regularize_trm ctxt) (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
+         else mk_bex $ (mk_resp $ mk_resp_arg ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
        end
 
   | (* equalities need to be replaced by appropriate equivalence relations *) 
     (Const (@{const_name "op ="}, ty), Const (@{const_name "op ="}, ty')) =>
          if ty = ty' then rtrm
-         else mk_resp_arg lthy (domain_type ty, domain_type ty') 
+         else mk_resp_arg ctxt (domain_type ty, domain_type ty') 
 
   | (* in this case we just check whether the given equivalence relation is correct *) 
     (rel, Const (@{const_name "op ="}, ty')) =>
        let 
          val exc = LIFT_MATCH "regularise (relation mismatch)"
          val rel_ty = (fastype_of rel) handle TERM _ => raise exc 
-         val rel' = mk_resp_arg lthy (domain_type rel_ty, domain_type ty') 
+         val rel' = mk_resp_arg ctxt (domain_type rel_ty, domain_type ty') 
        in 
          if rel' aconv rel then rtrm else raise exc
        end  
@@ -241,8 +245,8 @@
          if same_name rtrm qtrm then rtrm
          else 
            let 
-             val thy = ProofContext.theory_of lthy
-             val qtrm_str = Syntax.string_of_term lthy qtrm
+             val thy = ProofContext.theory_of ctxt
+             val qtrm_str = Syntax.string_of_term ctxt qtrm
              val exc1 = LIFT_MATCH ("regularize (constant " ^ qtrm_str ^ " not found)")
              val exc2 = LIFT_MATCH ("regularize (constant " ^ qtrm_str ^ " mismatch)")
              val rtrm' = (#rconst (qconsts_lookup thy qtrm)) handle NotFound => raise exc1
@@ -253,7 +257,7 @@
        end 
 
   | (t1 $ t2, t1' $ t2') =>
-       (regularize_trm lthy (t1, t1')) $ (regularize_trm lthy (t2, t2'))
+       (regularize_trm ctxt (t1, t1')) $ (regularize_trm ctxt (t2, t2'))
 
   | (Bound i, Bound i') =>
        if i = i' then rtrm 
@@ -261,15 +265,15 @@
 
   | _ =>
        let 
-         val rtrm_str = Syntax.string_of_term lthy rtrm
-         val qtrm_str = Syntax.string_of_term lthy qtrm
+         val rtrm_str = Syntax.string_of_term ctxt rtrm
+         val qtrm_str = Syntax.string_of_term ctxt qtrm
        in
          raise (LIFT_MATCH ("regularize failed (default: " ^ rtrm_str ^ "," ^ qtrm_str ^ ")"))
        end
 
-fun regularize_trm_chk lthy (rtrm, qtrm) =
-  regularize_trm lthy (rtrm, qtrm) 
-  |> Syntax.check_term lthy
+fun regularize_trm_chk ctxt (rtrm, qtrm) =
+  regularize_trm ctxt (rtrm, qtrm) 
+  |> Syntax.check_term ctxt
 
 (*
 Injection of Rep/Abs means:
@@ -299,27 +303,27 @@
   Vars case cannot occur.
 *)
 
-fun mk_repabs lthy (T, T') trm = 
-  absrep_fun repF lthy (T, T') $ (absrep_fun absF lthy (T, T') $ trm)
+fun mk_repabs ctxt (T, T') trm = 
+  absrep_fun repF ctxt (T, T') $ (absrep_fun absF ctxt (T, T') $ trm)
 
 
 (* bound variables need to be treated properly,     *)
 (* as the type of subterms needs to be calculated   *)
 
-fun inj_repabs_trm lthy (rtrm, qtrm) =
+fun inj_repabs_trm ctxt (rtrm, qtrm) =
  case (rtrm, qtrm) of
     (Const (@{const_name "Ball"}, T) $ r $ t, Const (@{const_name "All"}, _) $ t') =>
-       Const (@{const_name "Ball"}, T) $ r $ (inj_repabs_trm lthy (t, t'))
+       Const (@{const_name "Ball"}, T) $ r $ (inj_repabs_trm ctxt (t, t'))
 
   | (Const (@{const_name "Bex"}, T) $ r $ t, Const (@{const_name "Ex"}, _) $ t') =>
-       Const (@{const_name "Bex"}, T) $ r $ (inj_repabs_trm lthy (t, t'))
+       Const (@{const_name "Bex"}, T) $ r $ (inj_repabs_trm ctxt (t, t'))
 
   | (Const (@{const_name "Babs"}, T) $ r $ t, t' as (Abs _)) =>
       let
         val rty = fastype_of rtrm
         val qty = fastype_of qtrm
       in
-        mk_repabs lthy (rty, qty) (Const (@{const_name "Babs"}, T) $ r $ (inj_repabs_trm lthy (t, t')))
+        mk_repabs ctxt (rty, qty) (Const (@{const_name "Babs"}, T) $ r $ (inj_repabs_trm ctxt (t, t')))
       end
 
   | (Abs (x, T, t), Abs (x', T', t')) =>
@@ -329,18 +333,18 @@
         val (y, s) = Term.dest_abs (x, T, t)
         val (_, s') = Term.dest_abs (x', T', t')
         val yvar = Free (y, T)
-        val result = Term.lambda_name (y, yvar) (inj_repabs_trm lthy (s, s'))
+        val result = Term.lambda_name (y, yvar) (inj_repabs_trm ctxt (s, s'))
       in
         if rty = qty then result
-        else mk_repabs lthy (rty, qty) result
+        else mk_repabs ctxt (rty, qty) result
       end
 
   | (t $ s, t' $ s') =>  
-       (inj_repabs_trm lthy (t, t')) $ (inj_repabs_trm lthy (s, s'))
+       (inj_repabs_trm ctxt (t, t')) $ (inj_repabs_trm ctxt (s, s'))
 
   | (Free (_, T), Free (_, T')) => 
         if T = T' then rtrm 
-        else mk_repabs lthy (T, T') rtrm
+        else mk_repabs ctxt (T, T') rtrm
 
   | (_, Const (@{const_name "op ="}, _)) => rtrm
 
@@ -349,14 +353,14 @@
         val rty = fastype_of rtrm
       in 
         if rty = T' then rtrm
-        else mk_repabs lthy (rty, T') rtrm
+        else mk_repabs ctxt (rty, T') rtrm
       end   
   
   | _ => raise (LIFT_MATCH "injection (default)")
 
-fun inj_repabs_trm_chk lthy (rtrm, qtrm) =
-  inj_repabs_trm lthy (rtrm, qtrm) 
-  |> Syntax.check_term lthy
+fun inj_repabs_trm_chk ctxt (rtrm, qtrm) =
+  inj_repabs_trm ctxt (rtrm, qtrm) 
+  |> Syntax.check_term ctxt
 
 end; (* structure *)