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