src/HOL/Tools/Quotient/quotient_term.ML
author wenzelm
Sat Apr 16 16:15:37 2011 +0200 (2011-04-16)
changeset 42361 23f352990944
parent 41451 892e67be8304
child 44413 80d460bc6fa8
permissions -rw-r--r--
modernized structure Proof_Context;
     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   let
    67     val thy = Proof_Context.theory_of ctxt
    68     val mapfun = #mapfun (Quotient_Info.maps_lookup thy s) handle Quotient_Info.NotFound =>
    69       raise LIFT_MATCH ("No map function for type " ^ quote s ^ " found.")
    70   in
    71     Const (mapfun, dummyT)
    72   end
    73 
    74 (* makes a Free out of a TVar *)
    75 fun mk_Free (TVar ((x, i), _)) = Free (unprefix "'" x ^ string_of_int i, dummyT)
    76 
    77 (* produces an aggregate map function for the
    78    rty-part of a quotient definition; abstracts
    79    over all variables listed in vs (these variables
    80    correspond to the type variables in rty)
    81 
    82    for example for: (?'a list * ?'b)
    83    it produces:     %a b. prod_map (map a) b
    84 *)
    85 fun mk_mapfun ctxt vs rty =
    86   let
    87     val vs' = map mk_Free vs
    88 
    89     fun mk_mapfun_aux rty =
    90       case rty of
    91         TVar _ => mk_Free rty
    92       | Type (_, []) => mk_identity rty
    93       | Type (s, tys) => list_comb (get_mapfun ctxt s, map mk_mapfun_aux tys)
    94       | _ => raise LIFT_MATCH "mk_mapfun (default)"
    95   in
    96     fold_rev Term.lambda vs' (mk_mapfun_aux rty)
    97   end
    98 
    99 (* looks up the (varified) rty and qty for
   100    a quotient definition
   101 *)
   102 fun get_rty_qty ctxt s =
   103   let
   104     val thy = Proof_Context.theory_of ctxt
   105     val qdata = Quotient_Info.quotdata_lookup thy s handle Quotient_Info.NotFound =>
   106       raise LIFT_MATCH ("No quotient type " ^ quote s ^ " found.")
   107   in
   108     (#rtyp qdata, #qtyp qdata)
   109   end
   110 
   111 (* takes two type-environments and looks
   112    up in both of them the variable v, which
   113    must be listed in the environment
   114 *)
   115 fun double_lookup rtyenv qtyenv v =
   116   let
   117     val v' = fst (dest_TVar v)
   118   in
   119     (snd (the (Vartab.lookup rtyenv v')), snd (the (Vartab.lookup qtyenv v')))
   120   end
   121 
   122 (* matches a type pattern with a type *)
   123 fun match ctxt err ty_pat ty =
   124   let
   125     val thy = Proof_Context.theory_of ctxt
   126   in
   127     Sign.typ_match thy (ty_pat, ty) Vartab.empty
   128       handle Type.TYPE_MATCH => err ctxt ty_pat ty
   129   end
   130 
   131 (* produces the rep or abs constant for a qty *)
   132 fun absrep_const flag ctxt qty_str =
   133   let
   134     val qty_name = Long_Name.base_name qty_str
   135     val qualifier = Long_Name.qualifier qty_str
   136   in
   137     case flag of
   138       AbsF => Const (Long_Name.qualify qualifier ("abs_" ^ qty_name), dummyT)
   139     | RepF => Const (Long_Name.qualify qualifier ("rep_" ^ qty_name), dummyT)
   140   end
   141 
   142 (* Lets Nitpick represent elements of quotient types as elements of the raw type *)
   143 fun absrep_const_chk flag ctxt qty_str =
   144   Syntax.check_term ctxt (absrep_const flag ctxt qty_str)
   145 
   146 fun absrep_match_err ctxt ty_pat ty =
   147   let
   148     val ty_pat_str = Syntax.string_of_typ ctxt ty_pat
   149     val ty_str = Syntax.string_of_typ ctxt ty
   150   in
   151     raise LIFT_MATCH (space_implode " "
   152       ["absrep_fun (Types ", quote ty_pat_str, "and", quote ty_str, " do not match.)"])
   153   end
   154 
   155 
   156 (** generation of an aggregate absrep function **)
   157 
   158 (* - In case of equal types we just return the identity.
   159 
   160    - In case of TFrees we also return the identity.
   161 
   162    - In case of function types we recurse taking
   163      the polarity change into account.
   164 
   165    - If the type constructors are equal, we recurse for the
   166      arguments and build the appropriate map function.
   167 
   168    - If the type constructors are unequal, there must be an
   169      instance of quotient types:
   170 
   171        - we first look up the corresponding rty_pat and qty_pat
   172          from the quotient definition; the arguments of qty_pat
   173          must be some distinct TVars
   174        - we then match the rty_pat with rty and qty_pat with qty;
   175          if matching fails the types do not correspond -> error
   176        - the matching produces two environments; we look up the
   177          assignments for the qty_pat variables and recurse on the
   178          assignments
   179        - we prefix the aggregate map function for the rty_pat,
   180          which is an abstraction over all type variables
   181        - finally we compose the result with the appropriate
   182          absrep function in case at least one argument produced
   183          a non-identity function /
   184          otherwise we just return the appropriate absrep
   185          function
   186 
   187      The composition is necessary for types like
   188 
   189         ('a list) list / ('a foo) foo
   190 
   191      The matching is necessary for types like
   192 
   193         ('a * 'a) list / 'a bar
   194 
   195      The test is necessary in order to eliminate superfluous
   196      identity maps.
   197 *)
   198 
   199 fun absrep_fun flag ctxt (rty, qty) =
   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 ctxt "fun", [arg1, arg2])
   210         end
   211     | (Type (s, tys), Type (s', tys')) =>
   212         if s = s'
   213         then
   214           let
   215             val args = map (absrep_fun flag ctxt) (tys ~~ tys')
   216           in
   217             list_comb (get_mapfun ctxt s, args)
   218           end
   219         else
   220           let
   221             val (rty_pat, qty_pat as Type (_, vs)) = get_rty_qty ctxt s'
   222             val rtyenv = match ctxt absrep_match_err rty_pat rty
   223             val qtyenv = match ctxt absrep_match_err qty_pat qty
   224             val args_aux = map (double_lookup rtyenv qtyenv) vs
   225             val args = map (absrep_fun flag ctxt) args_aux
   226           in
   227             if forall is_identity args
   228             then absrep_const flag ctxt s'
   229             else
   230               let
   231                 val map_fun = mk_mapfun ctxt vs rty_pat
   232                 val result = list_comb (map_fun, args)
   233               in
   234                 mk_fun_compose flag (absrep_const flag ctxt s', result)
   235               end
   236           end
   237     | (TFree x, TFree x') =>
   238         if x = x'
   239         then mk_identity rty
   240         else raise (LIFT_MATCH "absrep_fun (frees)")
   241     | (TVar _, TVar _) => raise (LIFT_MATCH "absrep_fun (vars)")
   242     | _ => raise (LIFT_MATCH "absrep_fun (default)")
   243 
   244 fun absrep_fun_chk flag ctxt (rty, qty) =
   245   absrep_fun flag ctxt (rty, qty)
   246   |> Syntax.check_term ctxt
   247 
   248 
   249 
   250 
   251 (*** Aggregate Equivalence Relation ***)
   252 
   253 
   254 (* works very similar to the absrep generation,
   255    except there is no need for polarities
   256 *)
   257 
   258 (* instantiates TVars so that the term is of type ty *)
   259 fun force_typ ctxt trm ty =
   260   let
   261     val thy = Proof_Context.theory_of ctxt
   262     val trm_ty = fastype_of trm
   263     val ty_inst = Sign.typ_match thy (trm_ty, ty) Vartab.empty
   264   in
   265     map_types (Envir.subst_type ty_inst) trm
   266   end
   267 
   268 fun is_eq (Const (@{const_name HOL.eq}, _)) = true
   269   | is_eq _ = false
   270 
   271 fun mk_rel_compose (trm1, trm2) =
   272   Const (@{const_abbrev "rel_conj"}, dummyT) $ trm1 $ trm2
   273 
   274 fun get_relmap ctxt s =
   275   let
   276     val thy = Proof_Context.theory_of ctxt
   277     val relmap = #relmap (Quotient_Info.maps_lookup thy s) handle Quotient_Info.NotFound =>
   278       raise LIFT_MATCH ("get_relmap (no relation map function found for type " ^ s ^ ")")
   279   in
   280     Const (relmap, dummyT)
   281   end
   282 
   283 fun mk_relmap ctxt vs rty =
   284   let
   285     val vs' = map (mk_Free) vs
   286 
   287     fun mk_relmap_aux rty =
   288       case rty of
   289         TVar _ => mk_Free rty
   290       | Type (_, []) => HOLogic.eq_const rty
   291       | Type (s, tys) => list_comb (get_relmap ctxt s, map mk_relmap_aux tys)
   292       | _ => raise LIFT_MATCH ("mk_relmap (default)")
   293   in
   294     fold_rev Term.lambda vs' (mk_relmap_aux rty)
   295   end
   296 
   297 fun get_equiv_rel ctxt s =
   298   let
   299     val thy = Proof_Context.theory_of ctxt
   300   in
   301     #equiv_rel (Quotient_Info.quotdata_lookup thy s) handle Quotient_Info.NotFound =>
   302       raise LIFT_MATCH ("get_quotdata (no quotient found for type " ^ s ^ ")")
   303   end
   304 
   305 fun equiv_match_err ctxt ty_pat ty =
   306   let
   307     val ty_pat_str = Syntax.string_of_typ ctxt ty_pat
   308     val ty_str = Syntax.string_of_typ ctxt ty
   309   in
   310     raise LIFT_MATCH (space_implode " "
   311       ["equiv_relation (Types ", quote ty_pat_str, "and", quote ty_str, " do not match.)"])
   312   end
   313 
   314 (* builds the aggregate equivalence relation
   315    that will be the argument of Respects
   316 *)
   317 fun equiv_relation ctxt (rty, qty) =
   318   if rty = qty
   319   then HOLogic.eq_const rty
   320   else
   321     case (rty, qty) of
   322       (Type (s, tys), Type (s', tys')) =>
   323         if s = s'
   324         then
   325           let
   326             val args = map (equiv_relation ctxt) (tys ~~ tys')
   327           in
   328             list_comb (get_relmap ctxt s, args)
   329           end
   330         else
   331           let
   332             val (rty_pat, qty_pat as Type (_, vs)) = get_rty_qty ctxt s'
   333             val rtyenv = match ctxt equiv_match_err rty_pat rty
   334             val qtyenv = match ctxt equiv_match_err qty_pat qty
   335             val args_aux = map (double_lookup rtyenv qtyenv) vs
   336             val args = map (equiv_relation ctxt) args_aux
   337             val eqv_rel = get_equiv_rel ctxt s'
   338             val eqv_rel' = force_typ ctxt eqv_rel ([rty, rty] ---> @{typ bool})
   339           in
   340             if forall is_eq args
   341             then eqv_rel'
   342             else
   343               let
   344                 val rel_map = mk_relmap ctxt vs rty_pat
   345                 val result = list_comb (rel_map, args)
   346               in
   347                 mk_rel_compose (result, eqv_rel')
   348               end
   349           end
   350     | _ => HOLogic.eq_const rty
   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 thy rT qT =
   430   if rT = qT then true
   431   else
   432     (case (rT, qT) of
   433       (Type (rs, rtys), Type (qs, qtys)) =>
   434         if rs = qs then
   435           if length rtys <> length qtys then false
   436           else forall (fn x => x = true) (map2 (matches_typ thy) rtys qtys)
   437         else
   438           (case Quotient_Info.quotdata_lookup_raw thy qs of
   439             SOME quotinfo => Sign.typ_instance thy (rT, #rtyp quotinfo)
   440           | NONE => false)
   441     | _ => false)
   442 
   443 
   444 (* produces a regularized version of rtrm
   445 
   446    - the result might contain dummyTs
   447 
   448    - for regularization we do not need any
   449      special treatment of bound variables
   450 *)
   451 fun regularize_trm ctxt (rtrm, qtrm) =
   452   case (rtrm, qtrm) of
   453     (Abs (x, ty, t), Abs (_, ty', t')) =>
   454       let
   455         val subtrm = Abs(x, ty, regularize_trm ctxt (t, t'))
   456       in
   457         if ty = ty' then subtrm
   458         else mk_babs $ (mk_resp $ equiv_relation ctxt (ty, ty')) $ subtrm
   459       end
   460   | (Const (@{const_name Babs}, T) $ resrel $ (t as (Abs (_, ty, _))), t' as (Abs (_, ty', _))) =>
   461       let
   462         val subtrm = regularize_trm ctxt (t, t')
   463         val needres = mk_resp $ equiv_relation_chk ctxt (ty, ty')
   464       in
   465         if resrel <> needres
   466         then term_mismatch "regularize (Babs)" ctxt resrel needres
   467         else mk_babs $ resrel $ subtrm
   468       end
   469 
   470   | (Const (@{const_name All}, ty) $ t, Const (@{const_name All}, ty') $ t') =>
   471       let
   472         val subtrm = apply_subt (regularize_trm ctxt) (t, t')
   473       in
   474         if ty = ty' then Const (@{const_name All}, ty) $ subtrm
   475         else mk_ball $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
   476       end
   477 
   478   | (Const (@{const_name Ex}, ty) $ t, Const (@{const_name Ex}, ty') $ t') =>
   479       let
   480         val subtrm = apply_subt (regularize_trm ctxt) (t, t')
   481       in
   482         if ty = ty' then Const (@{const_name Ex}, ty) $ subtrm
   483         else mk_bex $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
   484       end
   485 
   486   | (Const (@{const_name Ex1}, ty) $ (Abs (_, _,
   487       (Const (@{const_name HOL.conj}, _) $ (Const (@{const_name Set.member}, _) $ _ $
   488         (Const (@{const_name Respects}, _) $ resrel)) $ (t $ _)))),
   489      Const (@{const_name Ex1}, ty') $ t') =>
   490       let
   491         val t_ = incr_boundvars (~1) t
   492         val subtrm = apply_subt (regularize_trm ctxt) (t_, t')
   493         val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty')
   494       in
   495         if resrel <> needrel
   496         then term_mismatch "regularize (Bex1)" ctxt resrel needrel
   497         else mk_bex1_rel $ resrel $ subtrm
   498       end
   499 
   500   | (Const (@{const_name Ex1}, ty) $ t, Const (@{const_name Ex1}, ty') $ t') =>
   501       let
   502         val subtrm = apply_subt (regularize_trm ctxt) (t, t')
   503       in
   504         if ty = ty' then Const (@{const_name Ex1}, ty) $ subtrm
   505         else mk_bex1_rel $ (equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
   506       end
   507 
   508   | (Const (@{const_name Ball}, ty) $ (Const (@{const_name Respects}, _) $ resrel) $ t,
   509      Const (@{const_name All}, ty') $ t') =>
   510       let
   511         val subtrm = apply_subt (regularize_trm ctxt) (t, t')
   512         val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty')
   513       in
   514         if resrel <> needrel
   515         then term_mismatch "regularize (Ball)" ctxt resrel needrel
   516         else mk_ball $ (mk_resp $ resrel) $ subtrm
   517       end
   518 
   519   | (Const (@{const_name Bex}, ty) $ (Const (@{const_name Respects}, _) $ resrel) $ t,
   520      Const (@{const_name Ex}, ty') $ t') =>
   521       let
   522         val subtrm = apply_subt (regularize_trm ctxt) (t, t')
   523         val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty')
   524       in
   525         if resrel <> needrel
   526         then term_mismatch "regularize (Bex)" ctxt resrel needrel
   527         else mk_bex $ (mk_resp $ resrel) $ subtrm
   528       end
   529 
   530   | (Const (@{const_name Bex1_rel}, ty) $ resrel $ t, Const (@{const_name Ex1}, 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 (Bex1_res)" ctxt resrel needrel
   537         else mk_bex1_rel $ resrel $ subtrm
   538       end
   539 
   540   | (* equalities need to be replaced by appropriate equivalence relations *)
   541     (Const (@{const_name HOL.eq}, ty), Const (@{const_name HOL.eq}, ty')) =>
   542         if ty = ty' then rtrm
   543         else equiv_relation ctxt (domain_type ty, domain_type ty')
   544 
   545   | (* in this case we just check whether the given equivalence relation is correct *)
   546     (rel, Const (@{const_name HOL.eq}, ty')) =>
   547       let
   548         val rel_ty = fastype_of rel
   549         val rel' = equiv_relation_chk ctxt (domain_type rel_ty, domain_type ty')
   550       in
   551         if rel' aconv rel then rtrm
   552         else term_mismatch "regularize (relation mismatch)" ctxt rel rel'
   553       end
   554 
   555   | (_, Const _) =>
   556       let
   557         val thy = Proof_Context.theory_of ctxt
   558         fun same_const (Const (s, T)) (Const (s', T')) = (s = s') andalso matches_typ thy T T'
   559           | same_const _ _ = false
   560       in
   561         if same_const rtrm qtrm then rtrm
   562         else
   563           let
   564             val rtrm' = #rconst (Quotient_Info.qconsts_lookup thy qtrm)
   565               handle Quotient_Info.NotFound =>
   566                 term_mismatch "regularize (constant not found)" ctxt rtrm qtrm
   567           in
   568             if Pattern.matches thy (rtrm', rtrm)
   569             then rtrm else term_mismatch "regularize (constant mismatch)" ctxt rtrm qtrm
   570           end
   571       end
   572 
   573   | (((t1 as Const (@{const_name prod_case}, _)) $ Abs (v1, ty, Abs(v1', ty', s1))),
   574      ((t2 as Const (@{const_name prod_case}, _)) $ Abs (v2, _ , Abs(v2', _  , s2)))) =>
   575        regularize_trm ctxt (t1, t2) $ Abs (v1, ty, Abs (v1', ty', regularize_trm ctxt (s1, s2)))
   576 
   577   | (((t1 as Const (@{const_name prod_case}, _)) $ Abs (v1, ty, s1)),
   578      ((t2 as Const (@{const_name prod_case}, _)) $ Abs (v2, _ , s2))) =>
   579        regularize_trm ctxt (t1, t2) $ Abs (v1, ty, regularize_trm ctxt (s1, s2))
   580 
   581   | (t1 $ t2, t1' $ t2') =>
   582        regularize_trm ctxt (t1, t1') $ regularize_trm ctxt (t2, t2')
   583 
   584   | (Bound i, Bound i') =>
   585       if i = i' then rtrm
   586       else raise (LIFT_MATCH "regularize (bounds mismatch)")
   587 
   588   | _ =>
   589       let
   590         val rtrm_str = Syntax.string_of_term ctxt rtrm
   591         val qtrm_str = Syntax.string_of_term ctxt qtrm
   592       in
   593         raise (LIFT_MATCH ("regularize failed (default: " ^ rtrm_str ^ "," ^ qtrm_str ^ ")"))
   594       end
   595 
   596 fun regularize_trm_chk ctxt (rtrm, qtrm) =
   597   regularize_trm ctxt (rtrm, qtrm)
   598   |> Syntax.check_term ctxt
   599 
   600 
   601 
   602 (*** Rep/Abs Injection ***)
   603 
   604 (*
   605 Injection of Rep/Abs means:
   606 
   607   For abstractions:
   608 
   609   * If the type of the abstraction needs lifting, then we add Rep/Abs
   610     around the abstraction; otherwise we leave it unchanged.
   611 
   612   For applications:
   613 
   614   * If the application involves a bounded quantifier, we recurse on
   615     the second argument. If the application is a bounded abstraction,
   616     we always put an Rep/Abs around it (since bounded abstractions
   617     are assumed to always need lifting). Otherwise we recurse on both
   618     arguments.
   619 
   620   For constants:
   621 
   622   * If the constant is (op =), we leave it always unchanged.
   623     Otherwise the type of the constant needs lifting, we put
   624     and Rep/Abs around it.
   625 
   626   For free variables:
   627 
   628   * We put a Rep/Abs around it if the type needs lifting.
   629 
   630   Vars case cannot occur.
   631 *)
   632 
   633 fun mk_repabs ctxt (T, T') trm =
   634   absrep_fun RepF ctxt (T, T') $ (absrep_fun AbsF ctxt (T, T') $ trm)
   635 
   636 fun inj_repabs_err ctxt msg rtrm qtrm =
   637   let
   638     val rtrm_str = Syntax.string_of_term ctxt rtrm
   639     val qtrm_str = Syntax.string_of_term ctxt qtrm
   640   in
   641     raise LIFT_MATCH (space_implode " " [msg, quote rtrm_str, "and", quote qtrm_str])
   642   end
   643 
   644 
   645 (* bound variables need to be treated properly,
   646    as the type of subterms needs to be calculated   *)
   647 fun inj_repabs_trm ctxt (rtrm, qtrm) =
   648  case (rtrm, qtrm) of
   649     (Const (@{const_name Ball}, T) $ r $ t, Const (@{const_name All}, _) $ t') =>
   650        Const (@{const_name Ball}, T) $ r $ (inj_repabs_trm ctxt (t, t'))
   651 
   652   | (Const (@{const_name Bex}, T) $ r $ t, Const (@{const_name Ex}, _) $ t') =>
   653        Const (@{const_name Bex}, T) $ r $ (inj_repabs_trm ctxt (t, t'))
   654 
   655   | (Const (@{const_name Babs}, T) $ r $ t, t' as (Abs _)) =>
   656       let
   657         val rty = fastype_of rtrm
   658         val qty = fastype_of qtrm
   659       in
   660         mk_repabs ctxt (rty, qty) (Const (@{const_name Babs}, T) $ r $ (inj_repabs_trm ctxt (t, t')))
   661       end
   662 
   663   | (Abs (x, T, t), Abs (x', T', t')) =>
   664       let
   665         val rty = fastype_of rtrm
   666         val qty = fastype_of qtrm
   667         val (y, s) = Term.dest_abs (x, T, t)
   668         val (_, s') = Term.dest_abs (x', T', t')
   669         val yvar = Free (y, T)
   670         val result = Term.lambda_name (y, yvar) (inj_repabs_trm ctxt (s, s'))
   671       in
   672         if rty = qty then result
   673         else mk_repabs ctxt (rty, qty) result
   674       end
   675 
   676   | (t $ s, t' $ s') =>
   677        (inj_repabs_trm ctxt (t, t')) $ (inj_repabs_trm ctxt (s, s'))
   678 
   679   | (Free (_, T), Free (_, T')) =>
   680         if T = T' then rtrm
   681         else mk_repabs ctxt (T, T') rtrm
   682 
   683   | (_, Const (@{const_name HOL.eq}, _)) => rtrm
   684 
   685   | (_, Const (_, T')) =>
   686       let
   687         val rty = fastype_of rtrm
   688       in
   689         if rty = T' then rtrm
   690         else mk_repabs ctxt (rty, T') rtrm
   691       end
   692 
   693   | _ => inj_repabs_err ctxt "injection (default):" rtrm qtrm
   694 
   695 fun inj_repabs_trm_chk ctxt (rtrm, qtrm) =
   696   inj_repabs_trm ctxt (rtrm, qtrm)
   697   |> Syntax.check_term ctxt
   698 
   699 
   700 
   701 (*** Wrapper for automatically transforming an rthm into a qthm ***)
   702 
   703 (* substitutions functions for r/q-types and
   704    r/q-constants, respectively
   705 *)
   706 fun subst_typ ctxt ty_subst rty =
   707   case rty of
   708     Type (s, rtys) =>
   709       let
   710         val thy = Proof_Context.theory_of ctxt
   711         val rty' = Type (s, map (subst_typ ctxt ty_subst) rtys)
   712 
   713         fun matches [] = rty'
   714           | matches ((rty, qty)::tail) =
   715               case try (Sign.typ_match thy (rty, rty')) Vartab.empty of
   716                 NONE => matches tail
   717               | SOME inst => Envir.subst_type inst qty
   718       in
   719         matches ty_subst
   720       end
   721   | _ => rty
   722 
   723 fun subst_trm ctxt ty_subst trm_subst rtrm =
   724   case rtrm of
   725     t1 $ t2 => (subst_trm ctxt ty_subst trm_subst t1) $ (subst_trm ctxt ty_subst trm_subst t2)
   726   | Abs (x, ty, t) => Abs (x, subst_typ ctxt ty_subst ty, subst_trm ctxt ty_subst trm_subst t)
   727   | Free(n, ty) => Free(n, subst_typ ctxt ty_subst ty)
   728   | Var(n, ty) => Var(n, subst_typ ctxt ty_subst ty)
   729   | Bound i => Bound i
   730   | Const (a, ty) =>
   731       let
   732         val thy = Proof_Context.theory_of ctxt
   733 
   734         fun matches [] = Const (a, subst_typ ctxt ty_subst ty)
   735           | matches ((rconst, qconst)::tail) =
   736               case try (Pattern.match thy (rconst, rtrm)) (Vartab.empty, Vartab.empty) of
   737                 NONE => matches tail
   738               | SOME inst => Envir.subst_term inst qconst
   739       in
   740         matches trm_subst
   741       end
   742 
   743 (* generate type and term substitutions out of the
   744    qtypes involved in a quotient; the direction flag
   745    indicates in which direction the substitutions work:
   746 
   747      true:  quotient -> raw
   748      false: raw -> quotient
   749 *)
   750 fun mk_ty_subst qtys direction ctxt =
   751   let
   752     val thy = Proof_Context.theory_of ctxt
   753   in
   754     Quotient_Info.quotdata_dest ctxt
   755     |> map (fn x => (#rtyp x, #qtyp x))
   756     |> filter (fn (_, qty) => member (Sign.typ_instance thy o swap) qtys qty)
   757     |> map (if direction then swap else I)
   758   end
   759 
   760 fun mk_trm_subst qtys direction ctxt =
   761   let
   762     val subst_typ' = subst_typ ctxt (mk_ty_subst qtys direction ctxt)
   763     fun proper (t1, t2) = subst_typ' (fastype_of t1) = fastype_of t2
   764 
   765     val const_substs =
   766       Quotient_Info.qconsts_dest ctxt
   767       |> map (fn x => (#rconst x, #qconst x))
   768       |> map (if direction then swap else I)
   769 
   770     val rel_substs =
   771       Quotient_Info.quotdata_dest ctxt
   772       |> map (fn x => (#equiv_rel x, HOLogic.eq_const (#qtyp x)))
   773       |> map (if direction then swap else I)
   774   in
   775     filter proper (const_substs @ rel_substs)
   776   end
   777 
   778 
   779 (* derives a qtyp and qtrm out of a rtyp and rtrm,
   780    respectively
   781 *)
   782 fun derive_qtyp ctxt qtys rty =
   783   subst_typ ctxt (mk_ty_subst qtys false ctxt) rty
   784 
   785 fun derive_qtrm ctxt qtys rtrm =
   786   subst_trm ctxt (mk_ty_subst qtys false ctxt) (mk_trm_subst qtys false ctxt) rtrm
   787 
   788 (* derives a rtyp and rtrm out of a qtyp and qtrm,
   789    respectively
   790 *)
   791 fun derive_rtyp ctxt qtys qty =
   792   subst_typ ctxt (mk_ty_subst qtys true ctxt) qty
   793 
   794 fun derive_rtrm ctxt qtys qtrm =
   795   subst_trm ctxt (mk_ty_subst qtys true ctxt) (mk_trm_subst qtys true ctxt) qtrm
   796 
   797 
   798 end; (* structure *)