src/HOL/Tools/Quotient/quotient_term.ML
author Christian Urban <urbanc@in.tum.de>
Tue Aug 24 22:38:45 2010 +0800 (2010-08-24)
changeset 38694 9db37e912ee4
parent 38624 9bb0016f7e60
child 38718 c7cbbb18eabe
permissions -rw-r--r--
use matching of types than just equality - this is needed in nominal to cope with type variables
     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 open Quotient_Info;
    39 
    40 exception LIFT_MATCH of string
    41 
    42 
    43 
    44 (*** Aggregate Rep/Abs Function ***)
    45 
    46 
    47 (* The flag RepF is for types in negative position; AbsF is for types
    48    in positive position. Because of this, function types need to be
    49    treated specially, since there the polarity changes.
    50 *)
    51 
    52 datatype flag = AbsF | RepF
    53 
    54 fun negF AbsF = RepF
    55   | negF RepF = AbsF
    56 
    57 fun is_identity (Const (@{const_name id}, _)) = true
    58   | is_identity _ = false
    59 
    60 fun mk_identity ty = Const (@{const_name id}, ty --> ty)
    61 
    62 fun mk_fun_compose flag (trm1, trm2) =
    63   case flag of
    64     AbsF => Const (@{const_name comp}, dummyT) $ trm1 $ trm2
    65   | RepF => Const (@{const_name comp}, dummyT) $ trm2 $ trm1
    66 
    67 fun get_mapfun ctxt s =
    68 let
    69   val thy = ProofContext.theory_of ctxt
    70   val exn = LIFT_MATCH ("No map function for type " ^ quote s ^ " found.")
    71   val mapfun = #mapfun (maps_lookup thy s) handle Quotient_Info.NotFound => raise exn
    72 in
    73   Const (mapfun, dummyT)
    74 end
    75 
    76 (* makes a Free out of a TVar *)
    77 fun mk_Free (TVar ((x, i), _)) = Free (unprefix "'" x ^ string_of_int i, dummyT)
    78 
    79 (* produces an aggregate map function for the
    80    rty-part of a quotient definition; abstracts
    81    over all variables listed in vs (these variables
    82    correspond to the type variables in rty)
    83 
    84    for example for: (?'a list * ?'b)
    85    it produces:     %a b. prod_map (map a) b
    86 *)
    87 fun mk_mapfun ctxt vs rty =
    88 let
    89   val vs' = map mk_Free vs
    90 
    91   fun mk_mapfun_aux rty =
    92     case rty of
    93       TVar _ => mk_Free rty
    94     | Type (_, []) => mk_identity rty
    95     | Type (s, tys) => list_comb (get_mapfun ctxt s, map mk_mapfun_aux tys)
    96     | _ => raise LIFT_MATCH "mk_mapfun (default)"
    97 in
    98   fold_rev Term.lambda vs' (mk_mapfun_aux rty)
    99 end
   100 
   101 (* looks up the (varified) rty and qty for
   102    a quotient definition
   103 *)
   104 fun get_rty_qty ctxt s =
   105 let
   106   val thy = ProofContext.theory_of ctxt
   107   val exn = LIFT_MATCH ("No quotient type " ^ quote s ^ " found.")
   108   val qdata = quotdata_lookup thy s handle Quotient_Info.NotFound => raise exn
   109 in
   110   (#rtyp qdata, #qtyp qdata)
   111 end
   112 
   113 (* takes two type-environments and looks
   114    up in both of them the variable v, which
   115    must be listed in the environment
   116 *)
   117 fun double_lookup rtyenv qtyenv v =
   118 let
   119   val v' = fst (dest_TVar v)
   120 in
   121   (snd (the (Vartab.lookup rtyenv v')), snd (the (Vartab.lookup qtyenv v')))
   122 end
   123 
   124 (* matches a type pattern with a type *)
   125 fun match ctxt err ty_pat ty =
   126 let
   127   val thy = ProofContext.theory_of ctxt
   128 in
   129   Sign.typ_match thy (ty_pat, ty) Vartab.empty
   130   handle MATCH_TYPE => err ctxt ty_pat ty
   131 end
   132 
   133 (* produces the rep or abs constant for a qty *)
   134 fun absrep_const flag ctxt qty_str =
   135 let
   136   val qty_name = Long_Name.base_name qty_str
   137   val qualifier = Long_Name.qualifier qty_str
   138 in
   139   case flag of
   140     AbsF => Const (Long_Name.qualify qualifier ("abs_" ^ qty_name), dummyT)
   141   | RepF => Const (Long_Name.qualify qualifier ("rep_" ^ qty_name), dummyT)
   142 end
   143 
   144 (* Lets Nitpick represent elements of quotient types as elements of the raw type *)
   145 fun absrep_const_chk flag ctxt qty_str =
   146   Syntax.check_term ctxt (absrep_const flag ctxt qty_str)
   147 
   148 fun absrep_match_err ctxt ty_pat ty =
   149 let
   150   val ty_pat_str = Syntax.string_of_typ ctxt ty_pat
   151   val ty_str = Syntax.string_of_typ ctxt ty
   152 in
   153   raise LIFT_MATCH (space_implode " "
   154     ["absrep_fun (Types ", quote ty_pat_str, "and", quote ty_str, " do not match.)"])
   155 end
   156 
   157 
   158 (** generation of an aggregate absrep function **)
   159 
   160 (* - In case of equal types we just return the identity.
   161 
   162    - In case of TFrees we also return the identity.
   163 
   164    - In case of function types we recurse taking
   165      the polarity change into account.
   166 
   167    - If the type constructors are equal, we recurse for the
   168      arguments and build the appropriate map function.
   169 
   170    - If the type constructors are unequal, there must be an
   171      instance of quotient types:
   172 
   173        - we first look up the corresponding rty_pat and qty_pat
   174          from the quotient definition; the arguments of qty_pat
   175          must be some distinct TVars
   176        - we then match the rty_pat with rty and qty_pat with qty;
   177          if matching fails the types do not correspond -> error
   178        - the matching produces two environments; we look up the
   179          assignments for the qty_pat variables and recurse on the
   180          assignments
   181        - we prefix the aggregate map function for the rty_pat,
   182          which is an abstraction over all type variables
   183        - finally we compose the result with the appropriate
   184          absrep function in case at least one argument produced
   185          a non-identity function /
   186          otherwise we just return the appropriate absrep
   187          function
   188 
   189      The composition is necessary for types like
   190 
   191         ('a list) list / ('a foo) foo
   192 
   193      The matching is necessary for types like
   194 
   195         ('a * 'a) list / 'a bar
   196 
   197      The test is necessary in order to eliminate superfluous
   198      identity maps.
   199 *)
   200 
   201 fun absrep_fun flag ctxt (rty, qty) =
   202   if rty = qty
   203   then mk_identity rty
   204   else
   205     case (rty, qty) of
   206       (Type ("fun", [ty1, ty2]), Type ("fun", [ty1', ty2'])) =>
   207         let
   208           val arg1 = absrep_fun (negF flag) ctxt (ty1, ty1')
   209           val arg2 = absrep_fun flag ctxt (ty2, ty2')
   210         in
   211           list_comb (get_mapfun ctxt "fun", [arg1, arg2])
   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 ctxt s, args)
   220            end
   221         else
   222            let
   223              val (rty_pat, qty_pat as Type (_, vs)) = get_rty_qty ctxt 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 ctxt 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 
   246 fun absrep_fun_chk flag ctxt (rty, qty) =
   247   absrep_fun flag ctxt (rty, qty)
   248   |> Syntax.check_term ctxt
   249 
   250 
   251 
   252 
   253 (*** Aggregate Equivalence Relation ***)
   254 
   255 
   256 (* works very similar to the absrep generation,
   257    except there is no need for polarities
   258 *)
   259 
   260 (* instantiates TVars so that the term is of type ty *)
   261 fun force_typ ctxt trm ty =
   262 let
   263   val thy = ProofContext.theory_of ctxt
   264   val trm_ty = fastype_of trm
   265   val ty_inst = Sign.typ_match thy (trm_ty, ty) Vartab.empty
   266 in
   267   map_types (Envir.subst_type ty_inst) trm
   268 end
   269 
   270 fun is_eq (Const (@{const_name "op ="}, _)) = true
   271   | is_eq _ = false
   272 
   273 fun mk_rel_compose (trm1, trm2) =
   274   Const (@{const_abbrev "rel_conj"}, dummyT) $ trm1 $ trm2
   275 
   276 fun get_relmap ctxt s =
   277 let
   278   val thy = ProofContext.theory_of ctxt
   279   val exn = LIFT_MATCH ("get_relmap (no relation map function found for type " ^ s ^ ")")
   280   val relmap = #relmap (maps_lookup thy s) handle Quotient_Info.NotFound => raise exn
   281 in
   282   Const (relmap, dummyT)
   283 end
   284 
   285 fun mk_relmap ctxt vs rty =
   286 let
   287   val vs' = map (mk_Free) vs
   288 
   289   fun mk_relmap_aux rty =
   290     case rty of
   291       TVar _ => mk_Free rty
   292     | Type (_, []) => HOLogic.eq_const rty
   293     | Type (s, tys) => list_comb (get_relmap ctxt s, map mk_relmap_aux tys)
   294     | _ => raise LIFT_MATCH ("mk_relmap (default)")
   295 in
   296   fold_rev Term.lambda vs' (mk_relmap_aux rty)
   297 end
   298 
   299 fun get_equiv_rel ctxt s =
   300 let
   301   val thy = ProofContext.theory_of ctxt
   302   val exn = LIFT_MATCH ("get_quotdata (no quotient found for type " ^ s ^ ")")
   303 in
   304   #equiv_rel (quotdata_lookup thy s) handle Quotient_Info.NotFound => raise exn
   305 end
   306 
   307 fun equiv_match_err ctxt ty_pat ty =
   308 let
   309   val ty_pat_str = Syntax.string_of_typ ctxt ty_pat
   310   val ty_str = Syntax.string_of_typ ctxt ty
   311 in
   312   raise LIFT_MATCH (space_implode " "
   313     ["equiv_relation (Types ", quote ty_pat_str, "and", quote ty_str, " do not match.)"])
   314 end
   315 
   316 (* builds the aggregate equivalence relation
   317    that will be the argument of Respects
   318 *)
   319 fun equiv_relation ctxt (rty, qty) =
   320   if rty = qty
   321   then HOLogic.eq_const rty
   322   else
   323     case (rty, qty) of
   324       (Type (s, tys), Type (s', tys')) =>
   325        if s = s'
   326        then
   327          let
   328            val args = map (equiv_relation ctxt) (tys ~~ tys')
   329          in
   330            list_comb (get_relmap ctxt s, args)
   331          end
   332        else
   333          let
   334            val (rty_pat, qty_pat as Type (_, vs)) = get_rty_qty ctxt s'
   335            val rtyenv = match ctxt equiv_match_err rty_pat rty
   336            val qtyenv = match ctxt equiv_match_err qty_pat qty
   337            val args_aux = map (double_lookup rtyenv qtyenv) vs
   338            val args = map (equiv_relation ctxt) args_aux
   339            val eqv_rel = get_equiv_rel ctxt s'
   340            val eqv_rel' = force_typ ctxt eqv_rel ([rty, rty] ---> @{typ bool})
   341          in
   342            if forall is_eq args
   343            then eqv_rel'
   344            else 
   345              let 
   346                val rel_map = mk_relmap ctxt vs rty_pat
   347                val result = list_comb (rel_map, args)
   348              in
   349                mk_rel_compose (result, eqv_rel')
   350              end
   351          end
   352       | _ => HOLogic.eq_const rty
   353 
   354 fun equiv_relation_chk ctxt (rty, qty) =
   355   equiv_relation ctxt (rty, qty)
   356   |> Syntax.check_term ctxt
   357 
   358 
   359 
   360 (*** Regularization ***)
   361 
   362 (* Regularizing an rtrm means:
   363 
   364  - Quantifiers over types that need lifting are replaced
   365    by bounded quantifiers, for example:
   366 
   367       All P  ----> All (Respects R) P
   368 
   369    where the aggregate relation R is given by the rty and qty;
   370 
   371  - Abstractions over types that need lifting are replaced
   372    by bounded abstractions, for example:
   373 
   374       %x. P  ----> Ball (Respects R) %x. P
   375 
   376  - Equalities over types that need lifting are replaced by
   377    corresponding equivalence relations, for example:
   378 
   379       A = B  ----> R A B
   380 
   381    or
   382 
   383       A = B  ----> (R ===> R) A B
   384 
   385    for more complicated types of A and B
   386 
   387 
   388  The regularize_trm accepts raw theorems in which equalities
   389  and quantifiers match exactly the ones in the lifted theorem
   390  but also accepts partially regularized terms.
   391 
   392  This means that the raw theorems can have:
   393    Ball (Respects R),  Bex (Respects R), Bex1_rel (Respects R), Babs, R
   394  in the places where:
   395    All, Ex, Ex1, %, (op =)
   396  is required the lifted theorem.
   397 
   398 *)
   399 
   400 val mk_babs = Const (@{const_name Babs}, dummyT)
   401 val mk_ball = Const (@{const_name Ball}, dummyT)
   402 val mk_bex  = Const (@{const_name Bex}, dummyT)
   403 val mk_bex1_rel = Const (@{const_name Bex1_rel}, dummyT)
   404 val mk_resp = Const (@{const_name Respects}, dummyT)
   405 
   406 (* - applies f to the subterm of an abstraction,
   407      otherwise to the given term,
   408    - used by regularize, therefore abstracted
   409      variables do not have to be treated specially
   410 *)
   411 fun apply_subt f (trm1, trm2) =
   412   case (trm1, trm2) of
   413     (Abs (x, T, t), Abs (_ , _, t')) => Abs (x, T, f (t, t'))
   414   | _ => f (trm1, trm2)
   415 
   416 fun term_mismatch str ctxt t1 t2 =
   417 let
   418   val t1_str = Syntax.string_of_term ctxt t1
   419   val t2_str = Syntax.string_of_term ctxt t2
   420   val t1_ty_str = Syntax.string_of_typ ctxt (fastype_of t1)
   421   val t2_ty_str = Syntax.string_of_typ ctxt (fastype_of t2)
   422 in
   423   raise LIFT_MATCH (cat_lines [str, t1_str ^ "::" ^ t1_ty_str, t2_str ^ "::" ^ t2_ty_str])
   424 end
   425 
   426 (* the major type of All and Ex quantifiers *)
   427 fun qnt_typ ty = domain_type (domain_type ty)
   428 
   429 (* Checks that two types match, for example:
   430      rty -> rty   matches   qty -> qty *)
   431 fun matches_typ thy rT qT =
   432   if rT = qT then true else
   433   case (rT, qT) of
   434     (Type (rs, rtys), Type (qs, qtys)) =>
   435       if rs = qs then
   436         if length rtys <> length qtys then false else
   437         forall (fn x => x = true) (map2 (matches_typ thy) rtys qtys)
   438       else
   439         (case Quotient_Info.quotdata_lookup_raw thy qs of
   440           SOME quotinfo => Sign.typ_instance thy (rT, #rtyp quotinfo)
   441         | NONE => false)
   442   | _ => false
   443 
   444 
   445 (* produces a regularized version of rtrm
   446 
   447    - the result might contain dummyTs
   448 
   449    - for regularisation we do not need any
   450      special treatment of bound variables
   451 *)
   452 fun regularize_trm ctxt (rtrm, qtrm) =
   453   case (rtrm, qtrm) of
   454     (Abs (x, ty, t), Abs (_, ty', t')) =>
   455        let
   456          val subtrm = Abs(x, ty, regularize_trm ctxt (t, t'))
   457        in
   458          if ty = ty' then subtrm
   459          else mk_babs $ (mk_resp $ equiv_relation ctxt (ty, ty')) $ subtrm
   460        end
   461   | (Const (@{const_name Babs}, T) $ resrel $ (t as (Abs (_, ty, _))), t' as (Abs (_, ty', _))) =>
   462        let
   463          val subtrm = regularize_trm ctxt (t, t')
   464          val needres = mk_resp $ equiv_relation_chk ctxt (ty, ty')
   465        in
   466          if resrel <> needres
   467          then term_mismatch "regularize (Babs)" ctxt resrel needres
   468          else mk_babs $ resrel $ subtrm
   469        end
   470 
   471   | (Const (@{const_name All}, ty) $ t, Const (@{const_name All}, ty') $ t') =>
   472        let
   473          val subtrm = apply_subt (regularize_trm ctxt) (t, t')
   474        in
   475          if ty = ty' then Const (@{const_name All}, ty) $ subtrm
   476          else mk_ball $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
   477        end
   478 
   479   | (Const (@{const_name Ex}, ty) $ t, Const (@{const_name Ex}, ty') $ t') =>
   480        let
   481          val subtrm = apply_subt (regularize_trm ctxt) (t, t')
   482        in
   483          if ty = ty' then Const (@{const_name Ex}, ty) $ subtrm
   484          else mk_bex $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
   485        end
   486 
   487   | (Const (@{const_name Ex1}, ty) $ (Abs (_, _,
   488       (Const (@{const_name "op &"}, _) $ (Const (@{const_name Set.member}, _) $ _ $
   489         (Const (@{const_name Respects}, _) $ resrel)) $ (t $ _)))),
   490      Const (@{const_name Ex1}, ty') $ t') =>
   491        let
   492          val t_ = incr_boundvars (~1) t
   493          val subtrm = apply_subt (regularize_trm ctxt) (t_, t')
   494          val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty')
   495        in
   496          if resrel <> needrel
   497          then term_mismatch "regularize (Bex1)" ctxt resrel needrel
   498          else mk_bex1_rel $ resrel $ subtrm
   499        end
   500 
   501   | (Const (@{const_name Ex1}, ty) $ t, Const (@{const_name Ex1}, ty') $ t') =>
   502        let
   503          val subtrm = apply_subt (regularize_trm ctxt) (t, t')
   504        in
   505          if ty = ty' then Const (@{const_name Ex1}, ty) $ subtrm
   506          else mk_bex1_rel $ (equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
   507        end
   508 
   509   | (Const (@{const_name Ball}, ty) $ (Const (@{const_name Respects}, _) $ resrel) $ t,
   510      Const (@{const_name All}, ty') $ t') =>
   511        let
   512          val subtrm = apply_subt (regularize_trm ctxt) (t, t')
   513          val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty')
   514        in
   515          if resrel <> needrel
   516          then term_mismatch "regularize (Ball)" ctxt resrel needrel
   517          else mk_ball $ (mk_resp $ resrel) $ subtrm
   518        end
   519 
   520   | (Const (@{const_name Bex}, ty) $ (Const (@{const_name Respects}, _) $ resrel) $ t,
   521      Const (@{const_name Ex}, ty') $ t') =>
   522        let
   523          val subtrm = apply_subt (regularize_trm ctxt) (t, t')
   524          val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty')
   525        in
   526          if resrel <> needrel
   527          then term_mismatch "regularize (Bex)" ctxt resrel needrel
   528          else mk_bex $ (mk_resp $ resrel) $ subtrm
   529        end
   530 
   531   | (Const (@{const_name Bex1_rel}, ty) $ resrel $ t, Const (@{const_name Ex1}, ty') $ t') =>
   532        let
   533          val subtrm = apply_subt (regularize_trm ctxt) (t, t')
   534          val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty')
   535        in
   536          if resrel <> needrel
   537          then term_mismatch "regularize (Bex1_res)" ctxt resrel needrel
   538          else mk_bex1_rel $ resrel $ subtrm
   539        end
   540 
   541   | (* equalities need to be replaced by appropriate equivalence relations *)
   542     (Const (@{const_name "op ="}, ty), Const (@{const_name "op ="}, ty')) =>
   543          if ty = ty' then rtrm
   544          else equiv_relation ctxt (domain_type ty, domain_type ty')
   545 
   546   | (* in this case we just check whether the given equivalence relation is correct *)
   547     (rel, Const (@{const_name "op ="}, ty')) =>
   548        let
   549          val rel_ty = fastype_of rel
   550          val rel' = equiv_relation_chk ctxt (domain_type rel_ty, domain_type ty')
   551        in
   552          if rel' aconv rel then rtrm
   553          else term_mismatch "regularise (relation mismatch)" ctxt rel rel'
   554        end
   555 
   556   | (_, Const _) =>
   557        let
   558          val thy = ProofContext.theory_of ctxt
   559          fun same_const (Const (s, T)) (Const (s', T')) = (s = s') andalso matches_typ thy T T'
   560            | same_const _ _ = false
   561        in
   562          if same_const rtrm qtrm then rtrm
   563          else
   564            let
   565              val rtrm' = #rconst (qconsts_lookup thy qtrm)
   566                handle Quotient_Info.NotFound => term_mismatch "regularize(constant notfound)" 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 "op ="}, _)) => 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 = ProofContext.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 = ProofContext.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 = ProofContext.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 *)