src/HOL/Tools/Quotient/quotient_term.ML
author kuncar
Fri Mar 23 22:00:17 2012 +0100 (2012-03-23)
changeset 47106 dfa5ed8d94b4
parent 47096 3ea48c19673e
child 47308 9caab698dbe4
permissions -rw-r--r--
use Thm.transfer for thms stored in generic context data storage
     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 get_rel_from_quot_thm: thm -> term
    24   val prove_quot_theorem: Proof.context -> typ * typ -> thm
    25 
    26   val regularize_trm: Proof.context -> term * term -> term
    27   val regularize_trm_chk: Proof.context -> term * term -> term
    28 
    29   val inj_repabs_trm: Proof.context -> term * term -> term
    30   val inj_repabs_trm_chk: Proof.context -> term * term -> term
    31 
    32   val derive_qtyp: Proof.context -> typ list -> typ -> typ
    33   val derive_qtrm: Proof.context -> typ list -> term -> term
    34   val derive_rtyp: Proof.context -> typ list -> typ -> typ
    35   val derive_rtrm: Proof.context -> typ list -> term -> term
    36 end;
    37 
    38 structure Quotient_Term: QUOTIENT_TERM =
    39 struct
    40 
    41 exception LIFT_MATCH of string
    42 
    43 
    44 
    45 (*** Aggregate Rep/Abs Function ***)
    46 
    47 
    48 (* The flag RepF is for types in negative position; AbsF is for types
    49    in positive position. Because of this, function types need to be
    50    treated specially, since there the polarity changes.
    51 *)
    52 
    53 datatype flag = AbsF | RepF
    54 
    55 fun negF AbsF = RepF
    56   | negF RepF = AbsF
    57 
    58 fun is_identity (Const (@{const_name id}, _)) = true
    59   | is_identity _ = false
    60 
    61 fun mk_identity ty = Const (@{const_name id}, ty --> ty)
    62 
    63 fun mk_fun_compose flag (trm1, trm2) =
    64   case flag of
    65     AbsF => Const (@{const_name comp}, dummyT) $ trm1 $ trm2
    66   | RepF => Const (@{const_name comp}, dummyT) $ trm2 $ trm1
    67 
    68 fun get_mapfun_data ctxt s =
    69   (case Symtab.lookup (Enriched_Type.entries ctxt) s of
    70     SOME [map_data] => (case try dest_Const (#mapper map_data) of
    71       SOME (c, _) => (Const (c, dummyT), #variances map_data)
    72     | NONE => raise LIFT_MATCH ("map function for type " ^ quote s ^ " is not a constant."))
    73   | SOME _ => raise LIFT_MATCH ("map function for type " ^ quote s ^ " is non-singleton entry.")
    74   | NONE => raise LIFT_MATCH ("No map function for type " ^ quote s ^ " found.")) 
    75 
    76 fun defined_mapfun_data ctxt s =
    77   Symtab.defined (Enriched_Type.entries ctxt) s
    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 fun get_equiv_rel thy s =
   283   (case Quotient_Info.lookup_quotients thy s of
   284     SOME qdata => #equiv_rel qdata
   285   | NONE => raise LIFT_MATCH ("get_equiv_rel (no quotient found for type " ^ s ^ ")"))
   286 
   287 fun equiv_match_err ctxt ty_pat ty =
   288   let
   289     val ty_pat_str = Syntax.string_of_typ ctxt ty_pat
   290     val ty_str = Syntax.string_of_typ ctxt ty
   291   in
   292     raise LIFT_MATCH (space_implode " "
   293       ["equiv_relation (Types ", quote ty_pat_str, "and", quote ty_str, " do not match.)"])
   294   end
   295 
   296 (* builds the aggregate equivalence relation
   297    that will be the argument of Respects
   298 *)
   299 fun equiv_relation ctxt (rty, qty) =
   300   if rty = qty
   301   then HOLogic.eq_const rty
   302   else
   303     case (rty, qty) of
   304       (Type (s, tys), Type (s', tys')) =>
   305         if s = s'
   306         then
   307           let
   308             val args = map (equiv_relation ctxt) (tys ~~ tys')
   309           in
   310             list_comb (get_relmap ctxt s, args)
   311           end
   312         else
   313           let
   314             val (Type (_, rtys), qty_pat) = get_rty_qty ctxt s'
   315             val qtyenv = match ctxt equiv_match_err qty_pat qty
   316             val rtys' = map (Envir.subst_type qtyenv) rtys
   317             val args = map (equiv_relation ctxt) (tys ~~ rtys')
   318             val eqv_rel = get_equiv_rel ctxt s'
   319             val eqv_rel' = force_typ ctxt eqv_rel ([rty, rty] ---> @{typ bool})
   320           in
   321             if forall is_eq args
   322             then eqv_rel'
   323             else
   324               let
   325                 val result = list_comb (get_relmap ctxt s, args)
   326               in
   327                 mk_rel_compose (result, eqv_rel')
   328               end
   329           end
   330     | _ => HOLogic.eq_const rty
   331 
   332 
   333 fun equiv_relation_chk ctxt (rty, qty) =
   334   equiv_relation ctxt (rty, qty)
   335   |> Syntax.check_term ctxt
   336 
   337 (* generation of the Quotient theorem  *)
   338 
   339 exception CODE_GEN of string
   340 
   341 fun get_quot_thm ctxt s =
   342   let
   343     val thy = Proof_Context.theory_of ctxt
   344   in
   345     (case Quotient_Info.lookup_quotients ctxt s of
   346       SOME qdata => Thm.transfer thy (#quot_thm qdata)
   347     | NONE => raise CODE_GEN ("No quotient type " ^ quote s ^ " found."))
   348   end
   349 
   350 fun get_rel_quot_thm ctxt s =
   351    let
   352     val thy = Proof_Context.theory_of ctxt
   353   in
   354     (case Quotient_Info.lookup_quotmaps ctxt s of
   355       SOME map_data => Thm.transfer thy (#quot_thm map_data)
   356     | NONE => raise CODE_GEN ("get_relmap (no relation map function found for type " ^ s ^ ")"))
   357   end
   358 
   359 fun is_id_quot thm = (prop_of thm = prop_of @{thm identity_quotient})
   360 
   361 infix 0 MRSL
   362 
   363 fun ants MRSL thm = fold (fn rl => fn thm => rl RS thm) ants thm
   364 
   365 exception NOT_IMPL of string
   366 
   367 fun get_rel_from_quot_thm quot_thm = 
   368   let
   369     val (_ $ rel $ _ $ _) = (HOLogic.dest_Trueprop o prop_of) quot_thm
   370   in
   371     rel
   372   end
   373 
   374 fun mk_quot_thm_compose (rel_quot_thm, quot_thm) = 
   375   let
   376     val quot_thm_rel = get_rel_from_quot_thm quot_thm
   377   in
   378     if is_eq quot_thm_rel then [rel_quot_thm, quot_thm] MRSL @{thm OOO_eq_quotient}
   379     else raise NOT_IMPL "nested quotients: not implemented yet"
   380   end
   381 
   382 fun prove_quot_theorem ctxt (rty, qty) =
   383   if rty = qty
   384   then @{thm identity_quotient}
   385   else
   386     case (rty, qty) of
   387       (Type (s, tys), Type (s', tys')) =>
   388         if s = s'
   389         then
   390           let
   391             val args = map (prove_quot_theorem ctxt) (tys ~~ tys')
   392           in
   393             args MRSL (get_rel_quot_thm ctxt s)
   394           end
   395         else
   396           let
   397             val (Type (_, rtys), qty_pat) = get_rty_qty ctxt s'
   398             val qtyenv = match ctxt equiv_match_err qty_pat qty
   399             val rtys' = map (Envir.subst_type qtyenv) rtys
   400             val args = map (prove_quot_theorem ctxt) (tys ~~ rtys')
   401             val quot_thm = get_quot_thm ctxt s'
   402           in
   403             if forall is_id_quot args
   404             then
   405               quot_thm
   406             else
   407               let
   408                 val rel_quot_thm = args MRSL (get_rel_quot_thm ctxt s)
   409               in
   410                 mk_quot_thm_compose (rel_quot_thm, quot_thm)
   411              end
   412           end
   413     | _ => @{thm identity_quotient}
   414 
   415 
   416 
   417 (*** Regularization ***)
   418 
   419 (* Regularizing an rtrm means:
   420 
   421  - Quantifiers over types that need lifting are replaced
   422    by bounded quantifiers, for example:
   423 
   424       All P  ----> All (Respects R) P
   425 
   426    where the aggregate relation R is given by the rty and qty;
   427 
   428  - Abstractions over types that need lifting are replaced
   429    by bounded abstractions, for example:
   430 
   431       %x. P  ----> Ball (Respects R) %x. P
   432 
   433  - Equalities over types that need lifting are replaced by
   434    corresponding equivalence relations, for example:
   435 
   436       A = B  ----> R A B
   437 
   438    or
   439 
   440       A = B  ----> (R ===> R) A B
   441 
   442    for more complicated types of A and B
   443 
   444 
   445  The regularize_trm accepts raw theorems in which equalities
   446  and quantifiers match exactly the ones in the lifted theorem
   447  but also accepts partially regularized terms.
   448 
   449  This means that the raw theorems can have:
   450    Ball (Respects R),  Bex (Respects R), Bex1_rel (Respects R), Babs, R
   451  in the places where:
   452    All, Ex, Ex1, %, (op =)
   453  is required the lifted theorem.
   454 
   455 *)
   456 
   457 val mk_babs = Const (@{const_name Babs}, dummyT)
   458 val mk_ball = Const (@{const_name Ball}, dummyT)
   459 val mk_bex  = Const (@{const_name Bex}, dummyT)
   460 val mk_bex1_rel = Const (@{const_name Bex1_rel}, dummyT)
   461 val mk_resp = Const (@{const_name Respects}, dummyT)
   462 
   463 (* - applies f to the subterm of an abstraction,
   464      otherwise to the given term,
   465    - used by regularize, therefore abstracted
   466      variables do not have to be treated specially
   467 *)
   468 fun apply_subt f (trm1, trm2) =
   469   case (trm1, trm2) of
   470     (Abs (x, T, t), Abs (_ , _, t')) => Abs (x, T, f (t, t'))
   471   | _ => f (trm1, trm2)
   472 
   473 fun term_mismatch str ctxt t1 t2 =
   474   let
   475     val t1_str = Syntax.string_of_term ctxt t1
   476     val t2_str = Syntax.string_of_term ctxt t2
   477     val t1_ty_str = Syntax.string_of_typ ctxt (fastype_of t1)
   478     val t2_ty_str = Syntax.string_of_typ ctxt (fastype_of t2)
   479   in
   480     raise LIFT_MATCH (cat_lines [str, t1_str ^ "::" ^ t1_ty_str, t2_str ^ "::" ^ t2_ty_str])
   481   end
   482 
   483 (* the major type of All and Ex quantifiers *)
   484 fun qnt_typ ty = domain_type (domain_type ty)
   485 
   486 (* Checks that two types match, for example:
   487      rty -> rty   matches   qty -> qty *)
   488 fun matches_typ ctxt rT qT =
   489   let
   490     val thy = Proof_Context.theory_of ctxt
   491   in
   492     if rT = qT then true
   493     else
   494       (case (rT, qT) of
   495         (Type (rs, rtys), Type (qs, qtys)) =>
   496           if rs = qs then
   497             if length rtys <> length qtys then false
   498             else forall (fn x => x = true) (map2 (matches_typ ctxt) rtys qtys)
   499           else
   500             (case Quotient_Info.lookup_quotients_global thy qs of
   501               SOME quotinfo => Sign.typ_instance thy (rT, #rtyp quotinfo)
   502             | NONE => false)
   503       | _ => false)
   504   end
   505 
   506 
   507 (* produces a regularized version of rtrm
   508 
   509    - the result might contain dummyTs
   510 
   511    - for regularization we do not need any
   512      special treatment of bound variables
   513 *)
   514 fun regularize_trm ctxt (rtrm, qtrm) =
   515   (case (rtrm, qtrm) of
   516     (Abs (x, ty, t), Abs (_, ty', t')) =>
   517       let
   518         val subtrm = Abs(x, ty, regularize_trm ctxt (t, t'))
   519       in
   520         if ty = ty' then subtrm
   521         else mk_babs $ (mk_resp $ equiv_relation ctxt (ty, ty')) $ subtrm
   522       end
   523 
   524   | (Const (@{const_name Babs}, T) $ resrel $ (t as (Abs (_, ty, _))), t' as (Abs (_, ty', _))) =>
   525       let
   526         val subtrm = regularize_trm ctxt (t, t')
   527         val needres = mk_resp $ equiv_relation_chk ctxt (ty, ty')
   528       in
   529         if resrel <> needres
   530         then term_mismatch "regularize (Babs)" ctxt resrel needres
   531         else mk_babs $ resrel $ subtrm
   532       end
   533 
   534   | (Const (@{const_name All}, ty) $ t, Const (@{const_name All}, ty') $ t') =>
   535       let
   536         val subtrm = apply_subt (regularize_trm ctxt) (t, t')
   537       in
   538         if ty = ty' then Const (@{const_name All}, ty) $ subtrm
   539         else mk_ball $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
   540       end
   541 
   542   | (Const (@{const_name Ex}, ty) $ t, Const (@{const_name Ex}, ty') $ t') =>
   543       let
   544         val subtrm = apply_subt (regularize_trm ctxt) (t, t')
   545       in
   546         if ty = ty' then Const (@{const_name Ex}, ty) $ subtrm
   547         else mk_bex $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
   548       end
   549 
   550   | (Const (@{const_name Ex1}, ty) $ (Abs (_, _,
   551       (Const (@{const_name HOL.conj}, _) $ (Const (@{const_name Set.member}, _) $ _ $
   552         (Const (@{const_name Respects}, _) $ resrel)) $ (t $ _)))),
   553      Const (@{const_name Ex1}, ty') $ t') =>
   554       let
   555         val t_ = incr_boundvars (~1) t
   556         val subtrm = apply_subt (regularize_trm ctxt) (t_, t')
   557         val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty')
   558       in
   559         if resrel <> needrel
   560         then term_mismatch "regularize (Bex1)" ctxt resrel needrel
   561         else mk_bex1_rel $ resrel $ subtrm
   562       end
   563 
   564   | (Const (@{const_name Ex1}, ty) $ t, Const (@{const_name Ex1}, ty') $ t') =>
   565       let
   566         val subtrm = apply_subt (regularize_trm ctxt) (t, t')
   567       in
   568         if ty = ty' then Const (@{const_name Ex1}, ty) $ subtrm
   569         else mk_bex1_rel $ (equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
   570       end
   571 
   572   | (Const (@{const_name Ball}, ty) $ (Const (@{const_name Respects}, _) $ resrel) $ t,
   573      Const (@{const_name All}, ty') $ t') =>
   574       let
   575         val subtrm = apply_subt (regularize_trm ctxt) (t, t')
   576         val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty')
   577       in
   578         if resrel <> needrel
   579         then term_mismatch "regularize (Ball)" ctxt resrel needrel
   580         else mk_ball $ (mk_resp $ resrel) $ subtrm
   581       end
   582 
   583   | (Const (@{const_name Bex}, ty) $ (Const (@{const_name Respects}, _) $ resrel) $ t,
   584      Const (@{const_name Ex}, ty') $ t') =>
   585       let
   586         val subtrm = apply_subt (regularize_trm ctxt) (t, t')
   587         val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty')
   588       in
   589         if resrel <> needrel
   590         then term_mismatch "regularize (Bex)" ctxt resrel needrel
   591         else mk_bex $ (mk_resp $ resrel) $ subtrm
   592       end
   593 
   594   | (Const (@{const_name Bex1_rel}, ty) $ resrel $ t, Const (@{const_name Ex1}, ty') $ t') =>
   595       let
   596         val subtrm = apply_subt (regularize_trm ctxt) (t, t')
   597         val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty')
   598       in
   599         if resrel <> needrel
   600         then term_mismatch "regularize (Bex1_res)" ctxt resrel needrel
   601         else mk_bex1_rel $ resrel $ subtrm
   602       end
   603 
   604   | (* equalities need to be replaced by appropriate equivalence relations *)
   605     (Const (@{const_name HOL.eq}, ty), Const (@{const_name HOL.eq}, ty')) =>
   606         if ty = ty' then rtrm
   607         else equiv_relation ctxt (domain_type ty, domain_type ty')
   608 
   609   | (* in this case we just check whether the given equivalence relation is correct *)
   610     (rel, Const (@{const_name HOL.eq}, ty')) =>
   611       let
   612         val rel_ty = fastype_of rel
   613         val rel' = equiv_relation_chk ctxt (domain_type rel_ty, domain_type ty')
   614       in
   615         if rel' aconv rel then rtrm
   616         else term_mismatch "regularize (relation mismatch)" ctxt rel rel'
   617       end
   618 
   619   | (_, Const _) =>
   620       let
   621         val thy = Proof_Context.theory_of ctxt
   622         fun same_const (Const (s, T)) (Const (s', T')) = s = s' andalso matches_typ ctxt T T'
   623           | same_const _ _ = false
   624       in
   625         if same_const rtrm qtrm then rtrm
   626         else
   627           let
   628             val rtrm' =
   629               (case Quotient_Info.lookup_quotconsts_global thy qtrm of
   630                 SOME qconst_info => #rconst qconst_info
   631               | NONE => term_mismatch "regularize (constant not found)" ctxt rtrm qtrm)
   632           in
   633             if Pattern.matches thy (rtrm', rtrm)
   634             then rtrm else term_mismatch "regularize (constant mismatch)" ctxt rtrm qtrm
   635           end
   636       end
   637 
   638   | (((t1 as Const (@{const_name prod_case}, _)) $ Abs (v1, ty, Abs(v1', ty', s1))),
   639      ((t2 as Const (@{const_name prod_case}, _)) $ Abs (v2, _ , Abs(v2', _  , s2)))) =>
   640        regularize_trm ctxt (t1, t2) $ Abs (v1, ty, Abs (v1', ty', regularize_trm ctxt (s1, s2)))
   641 
   642   | (((t1 as Const (@{const_name prod_case}, _)) $ Abs (v1, ty, s1)),
   643      ((t2 as Const (@{const_name prod_case}, _)) $ Abs (v2, _ , s2))) =>
   644        regularize_trm ctxt (t1, t2) $ Abs (v1, ty, regularize_trm ctxt (s1, s2))
   645 
   646   | (t1 $ t2, t1' $ t2') =>
   647        regularize_trm ctxt (t1, t1') $ regularize_trm ctxt (t2, t2')
   648 
   649   | (Bound i, Bound i') =>
   650       if i = i' then rtrm
   651       else raise (LIFT_MATCH "regularize (bounds mismatch)")
   652 
   653   | _ =>
   654       let
   655         val rtrm_str = Syntax.string_of_term ctxt rtrm
   656         val qtrm_str = Syntax.string_of_term ctxt qtrm
   657       in
   658         raise (LIFT_MATCH ("regularize failed (default: " ^ rtrm_str ^ "," ^ qtrm_str ^ ")"))
   659       end)
   660 
   661 fun regularize_trm_chk ctxt (rtrm, qtrm) =
   662   regularize_trm ctxt (rtrm, qtrm)
   663   |> Syntax.check_term ctxt
   664 
   665 
   666 
   667 (*** Rep/Abs Injection ***)
   668 
   669 (*
   670 Injection of Rep/Abs means:
   671 
   672   For abstractions:
   673 
   674   * If the type of the abstraction needs lifting, then we add Rep/Abs
   675     around the abstraction; otherwise we leave it unchanged.
   676 
   677   For applications:
   678 
   679   * If the application involves a bounded quantifier, we recurse on
   680     the second argument. If the application is a bounded abstraction,
   681     we always put an Rep/Abs around it (since bounded abstractions
   682     are assumed to always need lifting). Otherwise we recurse on both
   683     arguments.
   684 
   685   For constants:
   686 
   687   * If the constant is (op =), we leave it always unchanged.
   688     Otherwise the type of the constant needs lifting, we put
   689     and Rep/Abs around it.
   690 
   691   For free variables:
   692 
   693   * We put a Rep/Abs around it if the type needs lifting.
   694 
   695   Vars case cannot occur.
   696 *)
   697 
   698 fun mk_repabs ctxt (T, T') trm =
   699   absrep_fun ctxt RepF (T, T') $ (absrep_fun ctxt AbsF (T, T') $ trm)
   700 
   701 fun inj_repabs_err ctxt msg rtrm qtrm =
   702   let
   703     val rtrm_str = Syntax.string_of_term ctxt rtrm
   704     val qtrm_str = Syntax.string_of_term ctxt qtrm
   705   in
   706     raise LIFT_MATCH (space_implode " " [msg, quote rtrm_str, "and", quote qtrm_str])
   707   end
   708 
   709 
   710 (* bound variables need to be treated properly,
   711    as the type of subterms needs to be calculated   *)
   712 fun inj_repabs_trm ctxt (rtrm, qtrm) =
   713  case (rtrm, qtrm) of
   714     (Const (@{const_name Ball}, T) $ r $ t, Const (@{const_name All}, _) $ t') =>
   715        Const (@{const_name Ball}, T) $ r $ (inj_repabs_trm ctxt (t, t'))
   716 
   717   | (Const (@{const_name Bex}, T) $ r $ t, Const (@{const_name Ex}, _) $ t') =>
   718        Const (@{const_name Bex}, T) $ r $ (inj_repabs_trm ctxt (t, t'))
   719 
   720   | (Const (@{const_name Babs}, T) $ r $ t, t' as (Abs _)) =>
   721       let
   722         val rty = fastype_of rtrm
   723         val qty = fastype_of qtrm
   724       in
   725         mk_repabs ctxt (rty, qty) (Const (@{const_name Babs}, T) $ r $ (inj_repabs_trm ctxt (t, t')))
   726       end
   727 
   728   | (Abs (x, T, t), Abs (x', T', t')) =>
   729       let
   730         val rty = fastype_of rtrm
   731         val qty = fastype_of qtrm
   732         val (y, s) = Term.dest_abs (x, T, t)
   733         val (_, s') = Term.dest_abs (x', T', t')
   734         val yvar = Free (y, T)
   735         val result = Term.lambda_name (y, yvar) (inj_repabs_trm ctxt (s, s'))
   736       in
   737         if rty = qty then result
   738         else mk_repabs ctxt (rty, qty) result
   739       end
   740 
   741   | (t $ s, t' $ s') =>
   742        (inj_repabs_trm ctxt (t, t')) $ (inj_repabs_trm ctxt (s, s'))
   743 
   744   | (Free (_, T), Free (_, T')) =>
   745         if T = T' then rtrm
   746         else mk_repabs ctxt (T, T') rtrm
   747 
   748   | (_, Const (@{const_name HOL.eq}, _)) => rtrm
   749 
   750   | (_, Const (_, T')) =>
   751       let
   752         val rty = fastype_of rtrm
   753       in
   754         if rty = T' then rtrm
   755         else mk_repabs ctxt (rty, T') rtrm
   756       end
   757 
   758   | _ => inj_repabs_err ctxt "injection (default):" rtrm qtrm
   759 
   760 fun inj_repabs_trm_chk ctxt (rtrm, qtrm) =
   761   inj_repabs_trm ctxt (rtrm, qtrm)
   762   |> Syntax.check_term ctxt
   763 
   764 
   765 
   766 (*** Wrapper for automatically transforming an rthm into a qthm ***)
   767 
   768 (* substitutions functions for r/q-types and
   769    r/q-constants, respectively
   770 *)
   771 fun subst_typ ctxt ty_subst rty =
   772   case rty of
   773     Type (s, rtys) =>
   774       let
   775         val thy = Proof_Context.theory_of ctxt
   776         val rty' = Type (s, map (subst_typ ctxt ty_subst) rtys)
   777 
   778         fun matches [] = rty'
   779           | matches ((rty, qty)::tail) =
   780               (case try (Sign.typ_match thy (rty, rty')) Vartab.empty of
   781                 NONE => matches tail
   782               | SOME inst => subst_typ ctxt ty_subst (Envir.subst_type inst qty))
   783       in
   784         matches ty_subst
   785       end
   786   | _ => rty
   787 
   788 fun subst_trm ctxt ty_subst trm_subst rtrm =
   789   case rtrm of
   790     t1 $ t2 => (subst_trm ctxt ty_subst trm_subst t1) $ (subst_trm ctxt ty_subst trm_subst t2)
   791   | Abs (x, ty, t) => Abs (x, subst_typ ctxt ty_subst ty, subst_trm ctxt ty_subst trm_subst t)
   792   | Free(n, ty) => Free(n, subst_typ ctxt ty_subst ty)
   793   | Var(n, ty) => Var(n, subst_typ ctxt ty_subst ty)
   794   | Bound i => Bound i
   795   | Const (a, ty) =>
   796       let
   797         val thy = Proof_Context.theory_of ctxt
   798 
   799         fun matches [] = Const (a, subst_typ ctxt ty_subst ty)
   800           | matches ((rconst, qconst)::tail) =
   801               (case try (Pattern.match thy (rconst, rtrm)) (Vartab.empty, Vartab.empty) of
   802                 NONE => matches tail
   803               | SOME inst => subst_trm ctxt ty_subst trm_subst (Envir.subst_term inst qconst))
   804       in
   805         matches trm_subst
   806       end
   807 
   808 (* generate type and term substitutions out of the
   809    qtypes involved in a quotient; the direction flag
   810    indicates in which direction the substitutions work:
   811 
   812      true:  quotient -> raw
   813      false: raw -> quotient
   814 *)
   815 fun mk_ty_subst qtys direction ctxt =
   816   let
   817     val thy = Proof_Context.theory_of ctxt
   818   in
   819     Quotient_Info.dest_quotients ctxt
   820     |> map (fn x => (#rtyp x, #qtyp x))
   821     |> filter (fn (_, qty) => member (Sign.typ_instance thy o swap) qtys qty)
   822     |> map (if direction then swap else I)
   823   end
   824 
   825 fun mk_trm_subst qtys direction ctxt =
   826   let
   827     val subst_typ' = subst_typ ctxt (mk_ty_subst qtys direction ctxt)
   828     fun proper (t1, t2) = subst_typ' (fastype_of t1) = fastype_of t2
   829 
   830     val const_substs =
   831       Quotient_Info.dest_quotconsts ctxt
   832       |> map (fn x => (#rconst x, #qconst x))
   833       |> map (if direction then swap else I)
   834 
   835     val rel_substs =
   836       Quotient_Info.dest_quotients ctxt
   837       |> map (fn x => (#equiv_rel x, HOLogic.eq_const (#qtyp x)))
   838       |> map (if direction then swap else I)
   839   in
   840     filter proper (const_substs @ rel_substs)
   841   end
   842 
   843 
   844 (* derives a qtyp and qtrm out of a rtyp and rtrm,
   845    respectively
   846 *)
   847 fun derive_qtyp ctxt qtys rty =
   848   subst_typ ctxt (mk_ty_subst qtys false ctxt) rty
   849 
   850 fun derive_qtrm ctxt qtys rtrm =
   851   subst_trm ctxt (mk_ty_subst qtys false ctxt) (mk_trm_subst qtys false ctxt) rtrm
   852 
   853 (* derives a rtyp and rtrm out of a qtyp and qtrm,
   854    respectively
   855 *)
   856 fun derive_rtyp ctxt qtys qty =
   857   subst_typ ctxt (mk_ty_subst qtys true ctxt) qty
   858 
   859 fun derive_rtrm ctxt qtys qtrm =
   860   subst_trm ctxt (mk_ty_subst qtys true ctxt) (mk_trm_subst qtys true ctxt) qtrm
   861 
   862 
   863 end;