src/HOL/Tools/Quotient/quotient_term.ML
author Christian Urban <urbanc@in.tum.de>
Fri Nov 25 00:18:59 2011 +0000 (2011-11-25)
changeset 45628 f21eb7073895
parent 45534 4ab21521b393
child 45795 2d8949268303
permissions -rw-r--r--
in a local context, also the free variable case needs to be analysed default tip
     1 (*  Title:      HOL/Tools/Quotient/quotient_term.ML
     2     Author:     Cezary Kaliszyk and Christian Urban
     3 
     4 Constructs terms corresponding to goals from lifting theorems to
     5 quotient types.
     6 *)
     7 
     8 signature QUOTIENT_TERM =
     9 sig
    10   exception LIFT_MATCH of string
    11 
    12   datatype flag = AbsF | RepF
    13 
    14   val absrep_fun: flag -> Proof.context -> typ * typ -> term
    15   val absrep_fun_chk: flag -> Proof.context -> typ * typ -> term
    16 
    17   (* Allows Nitpick to represent quotient types as single elements from raw type *)
    18   val absrep_const_chk: flag -> Proof.context -> string -> term
    19 
    20   val equiv_relation: Proof.context -> typ * typ -> term
    21   val equiv_relation_chk: Proof.context -> typ * typ -> term
    22 
    23   val regularize_trm: Proof.context -> term * term -> term
    24   val regularize_trm_chk: Proof.context -> term * term -> term
    25 
    26   val inj_repabs_trm: Proof.context -> term * term -> term
    27   val inj_repabs_trm_chk: Proof.context -> term * term -> term
    28 
    29   val derive_qtyp: Proof.context -> typ list -> typ -> typ
    30   val derive_qtrm: Proof.context -> typ list -> term -> term
    31   val derive_rtyp: Proof.context -> typ list -> typ -> typ
    32   val derive_rtrm: Proof.context -> typ list -> term -> term
    33 end;
    34 
    35 structure Quotient_Term: QUOTIENT_TERM =
    36 struct
    37 
    38 exception LIFT_MATCH of string
    39 
    40 
    41 
    42 (*** Aggregate Rep/Abs Function ***)
    43 
    44 
    45 (* The flag RepF is for types in negative position; AbsF is for types
    46    in positive position. Because of this, function types need to be
    47    treated specially, since there the polarity changes.
    48 *)
    49 
    50 datatype flag = AbsF | RepF
    51 
    52 fun negF AbsF = RepF
    53   | negF RepF = AbsF
    54 
    55 fun is_identity (Const (@{const_name id}, _)) = true
    56   | is_identity _ = false
    57 
    58 fun mk_identity ty = Const (@{const_name id}, ty --> ty)
    59 
    60 fun mk_fun_compose flag (trm1, trm2) =
    61   case flag of
    62     AbsF => Const (@{const_name comp}, dummyT) $ trm1 $ trm2
    63   | RepF => Const (@{const_name comp}, dummyT) $ trm2 $ trm1
    64 
    65 fun get_mapfun thy s =
    66   (case Quotient_Info.lookup_quotmaps_global thy s of
    67     SOME map_data => Const (#mapfun map_data, dummyT)
    68   | NONE => raise LIFT_MATCH ("No map function for type " ^ quote s ^ " found."))
    69 
    70 (* makes a Free out of a TVar *)
    71 fun mk_Free (TVar ((x, i), _)) = Free (unprefix "'" x ^ string_of_int i, dummyT)
    72 
    73 (* produces an aggregate map function for the
    74    rty-part of a quotient definition; abstracts
    75    over all variables listed in vs (these variables
    76    correspond to the type variables in rty)
    77 
    78    for example for: (?'a list * ?'b)
    79    it produces:     %a b. prod_map (map a) b
    80 *)
    81 fun mk_mapfun thy vs rty =
    82   let
    83     val vs' = map mk_Free vs
    84 
    85     fun mk_mapfun_aux rty =
    86       case rty of
    87         TVar _ => mk_Free rty
    88       | Type (_, []) => mk_identity rty
    89       | Type (s, tys) => list_comb (get_mapfun thy s, map mk_mapfun_aux tys)
    90       | _ => raise LIFT_MATCH "mk_mapfun (default)"
    91   in
    92     fold_rev Term.lambda vs' (mk_mapfun_aux rty)
    93   end
    94 
    95 (* looks up the (varified) rty and qty for
    96    a quotient definition
    97 *)
    98 fun get_rty_qty thy s =
    99   (case Quotient_Info.lookup_quotients_global thy s of
   100     SOME qdata => (#rtyp qdata, #qtyp qdata)
   101   | NONE => raise LIFT_MATCH ("No quotient type " ^ quote s ^ " found."))
   102 
   103 (* takes two type-environments and looks
   104    up in both of them the variable v, which
   105    must be listed in the environment
   106 *)
   107 fun double_lookup rtyenv qtyenv v =
   108   let
   109     val v' = fst (dest_TVar v)
   110   in
   111     (snd (the (Vartab.lookup rtyenv v')), snd (the (Vartab.lookup qtyenv v')))
   112   end
   113 
   114 (* matches a type pattern with a type *)
   115 fun match ctxt err ty_pat ty =
   116   let
   117     val thy = Proof_Context.theory_of ctxt
   118   in
   119     Sign.typ_match thy (ty_pat, ty) Vartab.empty
   120       handle Type.TYPE_MATCH => err ctxt ty_pat ty
   121   end
   122 
   123 (* produces the rep or abs constant for a qty *)
   124 fun absrep_const flag ctxt qty_str =
   125   let
   126     (* FIXME *)
   127     fun mk_dummyT (Const (c, _)) = Const (c, dummyT)
   128       | mk_dummyT (Free (c, _)) = Free (c, dummyT)
   129       | mk_dummyT _ = error "Expecting abs/rep term to be a constant or a free variable"     
   130   in
   131     case Quotient_Info.lookup_abs_rep ctxt qty_str of
   132       SOME abs_rep => 
   133         mk_dummyT (case flag of
   134           AbsF => #abs abs_rep
   135         | RepF => #rep abs_rep)
   136       | NONE => error ("No abs/rep terms for " ^ quote qty_str)
   137   end
   138   
   139 (* Lets Nitpick represent elements of quotient types as elements of the raw type *)
   140 fun absrep_const_chk flag ctxt qty_str =
   141   Syntax.check_term ctxt (absrep_const flag ctxt qty_str)
   142 
   143 fun absrep_match_err ctxt ty_pat ty =
   144   let
   145     val ty_pat_str = Syntax.string_of_typ ctxt ty_pat
   146     val ty_str = Syntax.string_of_typ ctxt ty
   147   in
   148     raise LIFT_MATCH (space_implode " "
   149       ["absrep_fun (Types ", quote ty_pat_str, "and", quote ty_str, " do not match.)"])
   150   end
   151 
   152 
   153 (** generation of an aggregate absrep function **)
   154 
   155 (* - In case of equal types we just return the identity.
   156 
   157    - In case of TFrees we also return the identity.
   158 
   159    - In case of function types we recurse taking
   160      the polarity change into account.
   161 
   162    - If the type constructors are equal, we recurse for the
   163      arguments and build the appropriate map function.
   164 
   165    - If the type constructors are unequal, there must be an
   166      instance of quotient types:
   167 
   168        - we first look up the corresponding rty_pat and qty_pat
   169          from the quotient definition; the arguments of qty_pat
   170          must be some distinct TVars
   171        - we then match the rty_pat with rty and qty_pat with qty;
   172          if matching fails the types do not correspond -> error
   173        - the matching produces two environments; we look up the
   174          assignments for the qty_pat variables and recurse on the
   175          assignments
   176        - we prefix the aggregate map function for the rty_pat,
   177          which is an abstraction over all type variables
   178        - finally we compose the result with the appropriate
   179          absrep function in case at least one argument produced
   180          a non-identity function /
   181          otherwise we just return the appropriate absrep
   182          function
   183 
   184      The composition is necessary for types like
   185 
   186         ('a list) list / ('a foo) foo
   187 
   188      The matching is necessary for types like
   189 
   190         ('a * 'a) list / 'a bar
   191 
   192      The test is necessary in order to eliminate superfluous
   193      identity maps.
   194 *)
   195 
   196 fun absrep_fun flag ctxt (rty, qty) =
   197   let
   198     val thy = Proof_Context.theory_of ctxt
   199   in
   200     if rty = qty
   201     then mk_identity rty
   202     else
   203       case (rty, qty) of
   204         (Type ("fun", [ty1, ty2]), Type ("fun", [ty1', ty2'])) =>
   205           let
   206             val arg1 = absrep_fun (negF flag) ctxt (ty1, ty1')
   207             val arg2 = absrep_fun flag ctxt (ty2, ty2')
   208           in
   209             list_comb (get_mapfun thy "fun", [arg1, arg2])
   210           end
   211   (* FIXME: use type_name antiquotation if set type becomes explicit *)
   212       | (Type ("Set.set", [ty]), Type ("Set.set", [ty'])) =>
   213           let
   214             val arg = absrep_fun (negF flag) ctxt (ty, ty')
   215           in
   216             get_mapfun thy "Set.set" $ arg
   217           end
   218       | (Type (s, tys), Type (s', tys')) =>
   219           if s = s'
   220           then
   221             let
   222               val args = map (absrep_fun flag ctxt) (tys ~~ tys')
   223             in
   224               list_comb (get_mapfun thy s, args)
   225             end
   226           else
   227             let
   228               val (rty_pat, qty_pat as Type (_, vs)) = get_rty_qty thy s'
   229               val rtyenv = match ctxt absrep_match_err rty_pat rty
   230               val qtyenv = match ctxt absrep_match_err qty_pat qty
   231               val args_aux = map (double_lookup rtyenv qtyenv) vs
   232               val args = map (absrep_fun flag ctxt) args_aux
   233             in
   234               if forall is_identity args
   235               then absrep_const flag ctxt s'
   236               else
   237                 let
   238                   val map_fun = mk_mapfun thy vs rty_pat
   239                   val result = list_comb (map_fun, args)
   240                 in
   241                   mk_fun_compose flag (absrep_const flag ctxt s', result)
   242                 end
   243             end
   244       | (TFree x, TFree x') =>
   245           if x = x'
   246           then mk_identity rty
   247           else raise (LIFT_MATCH "absrep_fun (frees)")
   248       | (TVar _, TVar _) => raise (LIFT_MATCH "absrep_fun (vars)")
   249       | _ => raise (LIFT_MATCH "absrep_fun (default)")
   250   end
   251 
   252 fun absrep_fun_chk flag ctxt (rty, qty) =
   253   absrep_fun flag ctxt (rty, qty)
   254   |> Syntax.check_term ctxt
   255 
   256 
   257 
   258 
   259 (*** Aggregate Equivalence Relation ***)
   260 
   261 
   262 (* works very similar to the absrep generation,
   263    except there is no need for polarities
   264 *)
   265 
   266 (* instantiates TVars so that the term is of type ty *)
   267 fun force_typ ctxt trm ty =
   268   let
   269     val thy = Proof_Context.theory_of ctxt
   270     val trm_ty = fastype_of trm
   271     val ty_inst = Sign.typ_match thy (trm_ty, ty) Vartab.empty
   272   in
   273     map_types (Envir.subst_type ty_inst) trm
   274   end
   275 
   276 fun is_eq (Const (@{const_name HOL.eq}, _)) = true
   277   | is_eq _ = false
   278 
   279 fun mk_rel_compose (trm1, trm2) =
   280   Const (@{const_abbrev "rel_conj"}, dummyT) $ trm1 $ trm2
   281 
   282 fun get_relmap thy s =
   283   (case Quotient_Info.lookup_quotmaps thy s of
   284     SOME map_data => Const (#relmap map_data, dummyT)
   285   | NONE => raise LIFT_MATCH ("get_relmap (no relation map function found for type " ^ s ^ ")"))
   286 
   287 fun mk_relmap ctxt vs rty =
   288   let
   289     val vs' = map (mk_Free) vs
   290 
   291     fun mk_relmap_aux rty =
   292       case rty of
   293         TVar _ => mk_Free rty
   294       | Type (_, []) => HOLogic.eq_const rty
   295       | Type (s, tys) => list_comb (get_relmap ctxt s, map mk_relmap_aux tys)
   296       | _ => raise LIFT_MATCH ("mk_relmap (default)")
   297   in
   298     fold_rev Term.lambda vs' (mk_relmap_aux rty)
   299   end
   300 
   301 fun get_equiv_rel thy s =
   302   (case Quotient_Info.lookup_quotients thy s of
   303     SOME qdata => #equiv_rel qdata
   304   | NONE => raise LIFT_MATCH ("get_quotdata (no quotient found for type " ^ s ^ ")"))
   305 
   306 fun equiv_match_err ctxt ty_pat ty =
   307   let
   308     val ty_pat_str = Syntax.string_of_typ ctxt ty_pat
   309     val ty_str = Syntax.string_of_typ ctxt ty
   310   in
   311     raise LIFT_MATCH (space_implode " "
   312       ["equiv_relation (Types ", quote ty_pat_str, "and", quote ty_str, " do not match.)"])
   313   end
   314 
   315 (* builds the aggregate equivalence relation
   316    that will be the argument of Respects
   317 *)
   318 fun equiv_relation ctxt (rty, qty) =
   319   let
   320     val thy = Proof_Context.theory_of ctxt
   321   in
   322     if rty = qty
   323     then HOLogic.eq_const rty
   324     else
   325       case (rty, qty) of
   326         (Type (s, tys), Type (s', tys')) =>
   327           if s = s'
   328           then
   329             let
   330               val args = map (equiv_relation ctxt) (tys ~~ tys')
   331             in
   332               list_comb (get_relmap ctxt s, args)
   333             end
   334           else
   335             let
   336               val (rty_pat, qty_pat as Type (_, vs)) = get_rty_qty thy s'
   337               val rtyenv = match ctxt equiv_match_err rty_pat rty
   338               val qtyenv = match ctxt equiv_match_err qty_pat qty
   339               val args_aux = map (double_lookup rtyenv qtyenv) vs
   340               val args = map (equiv_relation ctxt) args_aux
   341               val eqv_rel = get_equiv_rel ctxt s'
   342               val eqv_rel' = force_typ ctxt eqv_rel ([rty, rty] ---> @{typ bool})
   343             in
   344               if forall is_eq args
   345               then eqv_rel'
   346               else
   347                 let
   348                   val rel_map = mk_relmap ctxt vs rty_pat
   349                   val result = list_comb (rel_map, args)
   350                 in
   351                   mk_rel_compose (result, eqv_rel')
   352                 end
   353             end
   354       | _ => HOLogic.eq_const rty
   355   end
   356 
   357 fun equiv_relation_chk ctxt (rty, qty) =
   358   equiv_relation ctxt (rty, qty)
   359   |> Syntax.check_term ctxt
   360 
   361 
   362 
   363 (*** Regularization ***)
   364 
   365 (* Regularizing an rtrm means:
   366 
   367  - Quantifiers over types that need lifting are replaced
   368    by bounded quantifiers, for example:
   369 
   370       All P  ----> All (Respects R) P
   371 
   372    where the aggregate relation R is given by the rty and qty;
   373 
   374  - Abstractions over types that need lifting are replaced
   375    by bounded abstractions, for example:
   376 
   377       %x. P  ----> Ball (Respects R) %x. P
   378 
   379  - Equalities over types that need lifting are replaced by
   380    corresponding equivalence relations, for example:
   381 
   382       A = B  ----> R A B
   383 
   384    or
   385 
   386       A = B  ----> (R ===> R) A B
   387 
   388    for more complicated types of A and B
   389 
   390 
   391  The regularize_trm accepts raw theorems in which equalities
   392  and quantifiers match exactly the ones in the lifted theorem
   393  but also accepts partially regularized terms.
   394 
   395  This means that the raw theorems can have:
   396    Ball (Respects R),  Bex (Respects R), Bex1_rel (Respects R), Babs, R
   397  in the places where:
   398    All, Ex, Ex1, %, (op =)
   399  is required the lifted theorem.
   400 
   401 *)
   402 
   403 val mk_babs = Const (@{const_name Babs}, dummyT)
   404 val mk_ball = Const (@{const_name Ball}, dummyT)
   405 val mk_bex  = Const (@{const_name Bex}, dummyT)
   406 val mk_bex1_rel = Const (@{const_name Bex1_rel}, dummyT)
   407 val mk_resp = Const (@{const_name Respects}, dummyT)
   408 
   409 (* - applies f to the subterm of an abstraction,
   410      otherwise to the given term,
   411    - used by regularize, therefore abstracted
   412      variables do not have to be treated specially
   413 *)
   414 fun apply_subt f (trm1, trm2) =
   415   case (trm1, trm2) of
   416     (Abs (x, T, t), Abs (_ , _, t')) => Abs (x, T, f (t, t'))
   417   | _ => f (trm1, trm2)
   418 
   419 fun term_mismatch str ctxt t1 t2 =
   420   let
   421     val t1_str = Syntax.string_of_term ctxt t1
   422     val t2_str = Syntax.string_of_term ctxt t2
   423     val t1_ty_str = Syntax.string_of_typ ctxt (fastype_of t1)
   424     val t2_ty_str = Syntax.string_of_typ ctxt (fastype_of t2)
   425   in
   426     raise LIFT_MATCH (cat_lines [str, t1_str ^ "::" ^ t1_ty_str, t2_str ^ "::" ^ t2_ty_str])
   427   end
   428 
   429 (* the major type of All and Ex quantifiers *)
   430 fun qnt_typ ty = domain_type (domain_type ty)
   431 
   432 (* Checks that two types match, for example:
   433      rty -> rty   matches   qty -> qty *)
   434 fun matches_typ ctxt rT qT =
   435   let
   436     val thy = Proof_Context.theory_of ctxt
   437   in
   438     if rT = qT then true
   439     else
   440       (case (rT, qT) of
   441         (Type (rs, rtys), Type (qs, qtys)) =>
   442           if rs = qs then
   443             if length rtys <> length qtys then false
   444             else forall (fn x => x = true) (map2 (matches_typ ctxt) rtys qtys)
   445           else
   446             (case Quotient_Info.lookup_quotients_global thy qs of
   447               SOME quotinfo => Sign.typ_instance thy (rT, #rtyp quotinfo)
   448             | NONE => false)
   449       | _ => false)
   450   end
   451 
   452 
   453 (* produces a regularized version of rtrm
   454 
   455    - the result might contain dummyTs
   456 
   457    - for regularization we do not need any
   458      special treatment of bound variables
   459 *)
   460 fun regularize_trm ctxt (rtrm, qtrm) =
   461   (case (rtrm, qtrm) of
   462     (Abs (x, ty, t), Abs (_, ty', t')) =>
   463       let
   464         val subtrm = Abs(x, ty, regularize_trm ctxt (t, t'))
   465       in
   466         if ty = ty' then subtrm
   467         else mk_babs $ (mk_resp $ equiv_relation ctxt (ty, ty')) $ subtrm
   468       end
   469 
   470   | (Const (@{const_name Babs}, T) $ resrel $ (t as (Abs (_, ty, _))), t' as (Abs (_, ty', _))) =>
   471       let
   472         val subtrm = regularize_trm ctxt (t, t')
   473         val needres = mk_resp $ equiv_relation_chk ctxt (ty, ty')
   474       in
   475         if resrel <> needres
   476         then term_mismatch "regularize (Babs)" ctxt resrel needres
   477         else mk_babs $ resrel $ subtrm
   478       end
   479 
   480   | (Const (@{const_name All}, ty) $ t, Const (@{const_name All}, ty') $ t') =>
   481       let
   482         val subtrm = apply_subt (regularize_trm ctxt) (t, t')
   483       in
   484         if ty = ty' then Const (@{const_name All}, ty) $ subtrm
   485         else mk_ball $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
   486       end
   487 
   488   | (Const (@{const_name Ex}, ty) $ t, Const (@{const_name Ex}, ty') $ t') =>
   489       let
   490         val subtrm = apply_subt (regularize_trm ctxt) (t, t')
   491       in
   492         if ty = ty' then Const (@{const_name Ex}, ty) $ subtrm
   493         else mk_bex $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
   494       end
   495 
   496   | (Const (@{const_name Ex1}, ty) $ (Abs (_, _,
   497       (Const (@{const_name HOL.conj}, _) $ (Const (@{const_name Set.member}, _) $ _ $
   498         (Const (@{const_name Respects}, _) $ resrel)) $ (t $ _)))),
   499      Const (@{const_name Ex1}, ty') $ t') =>
   500       let
   501         val t_ = incr_boundvars (~1) t
   502         val subtrm = apply_subt (regularize_trm ctxt) (t_, t')
   503         val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty')
   504       in
   505         if resrel <> needrel
   506         then term_mismatch "regularize (Bex1)" ctxt resrel needrel
   507         else mk_bex1_rel $ resrel $ subtrm
   508       end
   509 
   510   | (Const (@{const_name Ex1}, ty) $ t, Const (@{const_name Ex1}, ty') $ t') =>
   511       let
   512         val subtrm = apply_subt (regularize_trm ctxt) (t, t')
   513       in
   514         if ty = ty' then Const (@{const_name Ex1}, ty) $ subtrm
   515         else mk_bex1_rel $ (equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
   516       end
   517 
   518   | (Const (@{const_name Ball}, ty) $ (Const (@{const_name Respects}, _) $ resrel) $ t,
   519      Const (@{const_name All}, ty') $ t') =>
   520       let
   521         val subtrm = apply_subt (regularize_trm ctxt) (t, t')
   522         val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty')
   523       in
   524         if resrel <> needrel
   525         then term_mismatch "regularize (Ball)" ctxt resrel needrel
   526         else mk_ball $ (mk_resp $ resrel) $ subtrm
   527       end
   528 
   529   | (Const (@{const_name Bex}, ty) $ (Const (@{const_name Respects}, _) $ resrel) $ t,
   530      Const (@{const_name Ex}, ty') $ t') =>
   531       let
   532         val subtrm = apply_subt (regularize_trm ctxt) (t, t')
   533         val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty')
   534       in
   535         if resrel <> needrel
   536         then term_mismatch "regularize (Bex)" ctxt resrel needrel
   537         else mk_bex $ (mk_resp $ resrel) $ subtrm
   538       end
   539 
   540   | (Const (@{const_name Bex1_rel}, ty) $ resrel $ t, Const (@{const_name Ex1}, ty') $ t') =>
   541       let
   542         val subtrm = apply_subt (regularize_trm ctxt) (t, t')
   543         val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty')
   544       in
   545         if resrel <> needrel
   546         then term_mismatch "regularize (Bex1_res)" ctxt resrel needrel
   547         else mk_bex1_rel $ resrel $ subtrm
   548       end
   549 
   550   | (* equalities need to be replaced by appropriate equivalence relations *)
   551     (Const (@{const_name HOL.eq}, ty), Const (@{const_name HOL.eq}, ty')) =>
   552         if ty = ty' then rtrm
   553         else equiv_relation ctxt (domain_type ty, domain_type ty')
   554 
   555   | (* in this case we just check whether the given equivalence relation is correct *)
   556     (rel, Const (@{const_name HOL.eq}, ty')) =>
   557       let
   558         val rel_ty = fastype_of rel
   559         val rel' = equiv_relation_chk ctxt (domain_type rel_ty, domain_type ty')
   560       in
   561         if rel' aconv rel then rtrm
   562         else term_mismatch "regularize (relation mismatch)" ctxt rel rel'
   563       end
   564 
   565   | (_, Const _) =>
   566       let
   567         val thy = Proof_Context.theory_of ctxt
   568         fun same_const (Const (s, T)) (Const (s', T')) = s = s' andalso matches_typ ctxt T T'
   569           | same_const _ _ = false
   570       in
   571         if same_const rtrm qtrm then rtrm
   572         else
   573           let
   574             val rtrm' =
   575               (case Quotient_Info.lookup_quotconsts_global thy qtrm of
   576                 SOME qconst_info => #rconst qconst_info
   577               | NONE => term_mismatch "regularize (constant not found)" ctxt rtrm qtrm)
   578           in
   579             if Pattern.matches thy (rtrm', rtrm)
   580             then rtrm else term_mismatch "regularize (constant mismatch)" ctxt rtrm qtrm
   581           end
   582       end
   583 
   584   | (((t1 as Const (@{const_name prod_case}, _)) $ Abs (v1, ty, Abs(v1', ty', s1))),
   585      ((t2 as Const (@{const_name prod_case}, _)) $ Abs (v2, _ , Abs(v2', _  , s2)))) =>
   586        regularize_trm ctxt (t1, t2) $ Abs (v1, ty, Abs (v1', ty', regularize_trm ctxt (s1, s2)))
   587 
   588   | (((t1 as Const (@{const_name prod_case}, _)) $ Abs (v1, ty, s1)),
   589      ((t2 as Const (@{const_name prod_case}, _)) $ Abs (v2, _ , s2))) =>
   590        regularize_trm ctxt (t1, t2) $ Abs (v1, ty, regularize_trm ctxt (s1, s2))
   591 
   592   | (t1 $ t2, t1' $ t2') =>
   593        regularize_trm ctxt (t1, t1') $ regularize_trm ctxt (t2, t2')
   594 
   595   | (Bound i, Bound i') =>
   596       if i = i' then rtrm
   597       else raise (LIFT_MATCH "regularize (bounds mismatch)")
   598 
   599   | _ =>
   600       let
   601         val rtrm_str = Syntax.string_of_term ctxt rtrm
   602         val qtrm_str = Syntax.string_of_term ctxt qtrm
   603       in
   604         raise (LIFT_MATCH ("regularize failed (default: " ^ rtrm_str ^ "," ^ qtrm_str ^ ")"))
   605       end)
   606 
   607 fun regularize_trm_chk ctxt (rtrm, qtrm) =
   608   regularize_trm ctxt (rtrm, qtrm)
   609   |> Syntax.check_term ctxt
   610 
   611 
   612 
   613 (*** Rep/Abs Injection ***)
   614 
   615 (*
   616 Injection of Rep/Abs means:
   617 
   618   For abstractions:
   619 
   620   * If the type of the abstraction needs lifting, then we add Rep/Abs
   621     around the abstraction; otherwise we leave it unchanged.
   622 
   623   For applications:
   624 
   625   * If the application involves a bounded quantifier, we recurse on
   626     the second argument. If the application is a bounded abstraction,
   627     we always put an Rep/Abs around it (since bounded abstractions
   628     are assumed to always need lifting). Otherwise we recurse on both
   629     arguments.
   630 
   631   For constants:
   632 
   633   * If the constant is (op =), we leave it always unchanged.
   634     Otherwise the type of the constant needs lifting, we put
   635     and Rep/Abs around it.
   636 
   637   For free variables:
   638 
   639   * We put a Rep/Abs around it if the type needs lifting.
   640 
   641   Vars case cannot occur.
   642 *)
   643 
   644 fun mk_repabs ctxt (T, T') trm =
   645   absrep_fun RepF ctxt (T, T') $ (absrep_fun AbsF ctxt (T, T') $ trm)
   646 
   647 fun inj_repabs_err ctxt msg rtrm qtrm =
   648   let
   649     val rtrm_str = Syntax.string_of_term ctxt rtrm
   650     val qtrm_str = Syntax.string_of_term ctxt qtrm
   651   in
   652     raise LIFT_MATCH (space_implode " " [msg, quote rtrm_str, "and", quote qtrm_str])
   653   end
   654 
   655 
   656 (* bound variables need to be treated properly,
   657    as the type of subterms needs to be calculated   *)
   658 fun inj_repabs_trm ctxt (rtrm, qtrm) =
   659  case (rtrm, qtrm) of
   660     (Const (@{const_name Ball}, T) $ r $ t, Const (@{const_name All}, _) $ t') =>
   661        Const (@{const_name Ball}, T) $ r $ (inj_repabs_trm ctxt (t, t'))
   662 
   663   | (Const (@{const_name Bex}, T) $ r $ t, Const (@{const_name Ex}, _) $ t') =>
   664        Const (@{const_name Bex}, T) $ r $ (inj_repabs_trm ctxt (t, t'))
   665 
   666   | (Const (@{const_name Babs}, T) $ r $ t, t' as (Abs _)) =>
   667       let
   668         val rty = fastype_of rtrm
   669         val qty = fastype_of qtrm
   670       in
   671         mk_repabs ctxt (rty, qty) (Const (@{const_name Babs}, T) $ r $ (inj_repabs_trm ctxt (t, t')))
   672       end
   673 
   674   | (Abs (x, T, t), Abs (x', T', t')) =>
   675       let
   676         val rty = fastype_of rtrm
   677         val qty = fastype_of qtrm
   678         val (y, s) = Term.dest_abs (x, T, t)
   679         val (_, s') = Term.dest_abs (x', T', t')
   680         val yvar = Free (y, T)
   681         val result = Term.lambda_name (y, yvar) (inj_repabs_trm ctxt (s, s'))
   682       in
   683         if rty = qty then result
   684         else mk_repabs ctxt (rty, qty) result
   685       end
   686 
   687   | (t $ s, t' $ s') =>
   688        (inj_repabs_trm ctxt (t, t')) $ (inj_repabs_trm ctxt (s, s'))
   689 
   690   | (Free (_, T), Free (_, T')) =>
   691         if T = T' then rtrm
   692         else mk_repabs ctxt (T, T') rtrm
   693 
   694   | (_, Const (@{const_name HOL.eq}, _)) => rtrm
   695 
   696   | (_, Const (_, T')) =>
   697       let
   698         val rty = fastype_of rtrm
   699       in
   700         if rty = T' then rtrm
   701         else mk_repabs ctxt (rty, T') rtrm
   702       end
   703 
   704   | _ => inj_repabs_err ctxt "injection (default):" rtrm qtrm
   705 
   706 fun inj_repabs_trm_chk ctxt (rtrm, qtrm) =
   707   inj_repabs_trm ctxt (rtrm, qtrm)
   708   |> Syntax.check_term ctxt
   709 
   710 
   711 
   712 (*** Wrapper for automatically transforming an rthm into a qthm ***)
   713 
   714 (* substitutions functions for r/q-types and
   715    r/q-constants, respectively
   716 *)
   717 fun subst_typ ctxt ty_subst rty =
   718   case rty of
   719     Type (s, rtys) =>
   720       let
   721         val thy = Proof_Context.theory_of ctxt
   722         val rty' = Type (s, map (subst_typ ctxt ty_subst) rtys)
   723 
   724         fun matches [] = rty'
   725           | matches ((rty, qty)::tail) =
   726               (case try (Sign.typ_match thy (rty, rty')) Vartab.empty of
   727                 NONE => matches tail
   728               | SOME inst => Envir.subst_type inst qty)
   729       in
   730         matches ty_subst
   731       end
   732   | _ => rty
   733 
   734 fun subst_trm ctxt ty_subst trm_subst rtrm =
   735   case rtrm of
   736     t1 $ t2 => (subst_trm ctxt ty_subst trm_subst t1) $ (subst_trm ctxt ty_subst trm_subst t2)
   737   | Abs (x, ty, t) => Abs (x, subst_typ ctxt ty_subst ty, subst_trm ctxt ty_subst trm_subst t)
   738   | Free(n, ty) => Free(n, subst_typ ctxt ty_subst ty)
   739   | Var(n, ty) => Var(n, subst_typ ctxt ty_subst ty)
   740   | Bound i => Bound i
   741   | Const (a, ty) =>
   742       let
   743         val thy = Proof_Context.theory_of ctxt
   744 
   745         fun matches [] = Const (a, subst_typ ctxt ty_subst ty)
   746           | matches ((rconst, qconst)::tail) =
   747               (case try (Pattern.match thy (rconst, rtrm)) (Vartab.empty, Vartab.empty) of
   748                 NONE => matches tail
   749               | SOME inst => Envir.subst_term inst qconst)
   750       in
   751         matches trm_subst
   752       end
   753 
   754 (* generate type and term substitutions out of the
   755    qtypes involved in a quotient; the direction flag
   756    indicates in which direction the substitutions work:
   757 
   758      true:  quotient -> raw
   759      false: raw -> quotient
   760 *)
   761 fun mk_ty_subst qtys direction ctxt =
   762   let
   763     val thy = Proof_Context.theory_of ctxt
   764   in
   765     Quotient_Info.dest_quotients ctxt
   766     |> map (fn x => (#rtyp x, #qtyp x))
   767     |> filter (fn (_, qty) => member (Sign.typ_instance thy o swap) qtys qty)
   768     |> map (if direction then swap else I)
   769   end
   770 
   771 fun mk_trm_subst qtys direction ctxt =
   772   let
   773     val subst_typ' = subst_typ ctxt (mk_ty_subst qtys direction ctxt)
   774     fun proper (t1, t2) = subst_typ' (fastype_of t1) = fastype_of t2
   775 
   776     val const_substs =
   777       Quotient_Info.dest_quotconsts ctxt
   778       |> map (fn x => (#rconst x, #qconst x))
   779       |> map (if direction then swap else I)
   780 
   781     val rel_substs =
   782       Quotient_Info.dest_quotients ctxt
   783       |> map (fn x => (#equiv_rel x, HOLogic.eq_const (#qtyp x)))
   784       |> map (if direction then swap else I)
   785   in
   786     filter proper (const_substs @ rel_substs)
   787   end
   788 
   789 
   790 (* derives a qtyp and qtrm out of a rtyp and rtrm,
   791    respectively
   792 *)
   793 fun derive_qtyp ctxt qtys rty =
   794   subst_typ ctxt (mk_ty_subst qtys false ctxt) rty
   795 
   796 fun derive_qtrm ctxt qtys rtrm =
   797   subst_trm ctxt (mk_ty_subst qtys false ctxt) (mk_trm_subst qtys false ctxt) rtrm
   798 
   799 (* derives a rtyp and rtrm out of a qtyp and qtrm,
   800    respectively
   801 *)
   802 fun derive_rtyp ctxt qtys qty =
   803   subst_typ ctxt (mk_ty_subst qtys true ctxt) qty
   804 
   805 fun derive_rtrm ctxt qtys qtrm =
   806   subst_trm ctxt (mk_ty_subst qtys true ctxt) (mk_trm_subst qtys true ctxt) qtrm
   807 
   808 
   809 end;