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