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