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