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