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