src/HOL/Tools/Quotient/quotient_term.ML
changeset 35222 4f1fba00f66d
child 35402 115a5a95710a
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Tools/Quotient/quotient_term.ML	Fri Feb 19 13:54:19 2010 +0100
     1.3 @@ -0,0 +1,786 @@
     1.4 +(*  Title:      quotient_term.thy
     1.5 +    Author:     Cezary Kaliszyk and Christian Urban
     1.6 +
     1.7 +    Constructs terms corresponding to goals from
     1.8 +    lifting theorems to quotient types.
     1.9 +*)
    1.10 +
    1.11 +signature QUOTIENT_TERM =
    1.12 +sig
    1.13 +  exception LIFT_MATCH of string
    1.14 +
    1.15 +  datatype flag = AbsF | RepF
    1.16 +
    1.17 +  val absrep_fun: flag -> Proof.context -> typ * typ -> term
    1.18 +  val absrep_fun_chk: flag -> Proof.context -> typ * typ -> term
    1.19 +
    1.20 +  (* Allows Nitpick to represent quotient types as single elements from raw type *)
    1.21 +  val absrep_const_chk: flag -> Proof.context -> string -> term
    1.22 +
    1.23 +  val equiv_relation: Proof.context -> typ * typ -> term
    1.24 +  val equiv_relation_chk: Proof.context -> typ * typ -> term
    1.25 +
    1.26 +  val regularize_trm: Proof.context -> term * term -> term
    1.27 +  val regularize_trm_chk: Proof.context -> term * term -> term
    1.28 +
    1.29 +  val inj_repabs_trm: Proof.context -> term * term -> term
    1.30 +  val inj_repabs_trm_chk: Proof.context -> term * term -> term
    1.31 +
    1.32 +  val quotient_lift_const: string * term -> local_theory -> term
    1.33 +  val quotient_lift_all: Proof.context -> term -> term
    1.34 +end;
    1.35 +
    1.36 +structure Quotient_Term: QUOTIENT_TERM =
    1.37 +struct
    1.38 +
    1.39 +open Quotient_Info;
    1.40 +
    1.41 +exception LIFT_MATCH of string
    1.42 +
    1.43 +
    1.44 +
    1.45 +(*** Aggregate Rep/Abs Function ***)
    1.46 +
    1.47 +
    1.48 +(* The flag RepF is for types in negative position; AbsF is for types
    1.49 +   in positive position. Because of this, function types need to be
    1.50 +   treated specially, since there the polarity changes.
    1.51 +*)
    1.52 +
    1.53 +datatype flag = AbsF | RepF
    1.54 +
    1.55 +fun negF AbsF = RepF
    1.56 +  | negF RepF = AbsF
    1.57 +
    1.58 +fun is_identity (Const (@{const_name "id"}, _)) = true
    1.59 +  | is_identity _ = false
    1.60 +
    1.61 +fun mk_identity ty = Const (@{const_name "id"}, ty --> ty)
    1.62 +
    1.63 +fun mk_fun_compose flag (trm1, trm2) =
    1.64 +  case flag of
    1.65 +    AbsF => Const (@{const_name "comp"}, dummyT) $ trm1 $ trm2
    1.66 +  | RepF => Const (@{const_name "comp"}, dummyT) $ trm2 $ trm1
    1.67 +
    1.68 +fun get_mapfun ctxt s =
    1.69 +let
    1.70 +  val thy = ProofContext.theory_of ctxt
    1.71 +  val exn = LIFT_MATCH ("No map function for type " ^ quote s ^ " found.")
    1.72 +  val mapfun = #mapfun (maps_lookup thy s) handle Quotient_Info.NotFound => raise exn
    1.73 +in
    1.74 +  Const (mapfun, dummyT)
    1.75 +end
    1.76 +
    1.77 +(* makes a Free out of a TVar *)
    1.78 +fun mk_Free (TVar ((x, i), _)) = Free (unprefix "'" x ^ string_of_int i, dummyT)
    1.79 +
    1.80 +(* produces an aggregate map function for the
    1.81 +   rty-part of a quotient definition; abstracts
    1.82 +   over all variables listed in vs (these variables
    1.83 +   correspond to the type variables in rty)
    1.84 +
    1.85 +   for example for: (?'a list * ?'b)
    1.86 +   it produces:     %a b. prod_map (map a) b
    1.87 +*)
    1.88 +fun mk_mapfun ctxt vs rty =
    1.89 +let
    1.90 +  val vs' = map (mk_Free) vs
    1.91 +
    1.92 +  fun mk_mapfun_aux rty =
    1.93 +    case rty of
    1.94 +      TVar _ => mk_Free rty
    1.95 +    | Type (_, []) => mk_identity rty
    1.96 +    | Type (s, tys) => list_comb (get_mapfun ctxt s, map mk_mapfun_aux tys)
    1.97 +    | _ => raise LIFT_MATCH "mk_mapfun (default)"
    1.98 +in
    1.99 +  fold_rev Term.lambda vs' (mk_mapfun_aux rty)
   1.100 +end
   1.101 +
   1.102 +(* looks up the (varified) rty and qty for
   1.103 +   a quotient definition
   1.104 +*)
   1.105 +fun get_rty_qty ctxt s =
   1.106 +let
   1.107 +  val thy = ProofContext.theory_of ctxt
   1.108 +  val exn = LIFT_MATCH ("No quotient type " ^ quote s ^ " found.")
   1.109 +  val qdata = (quotdata_lookup thy s) handle Quotient_Info.NotFound => raise exn
   1.110 +in
   1.111 +  (#rtyp qdata, #qtyp qdata)
   1.112 +end
   1.113 +
   1.114 +(* takes two type-environments and looks
   1.115 +   up in both of them the variable v, which
   1.116 +   must be listed in the environment
   1.117 +*)
   1.118 +fun double_lookup rtyenv qtyenv v =
   1.119 +let
   1.120 +  val v' = fst (dest_TVar v)
   1.121 +in
   1.122 +  (snd (the (Vartab.lookup rtyenv v')), snd (the (Vartab.lookup qtyenv v')))
   1.123 +end
   1.124 +
   1.125 +(* matches a type pattern with a type *)
   1.126 +fun match ctxt err ty_pat ty =
   1.127 +let
   1.128 +  val thy = ProofContext.theory_of ctxt
   1.129 +in
   1.130 +  Sign.typ_match thy (ty_pat, ty) Vartab.empty
   1.131 +  handle MATCH_TYPE => err ctxt ty_pat ty
   1.132 +end
   1.133 +
   1.134 +(* produces the rep or abs constant for a qty *)
   1.135 +fun absrep_const flag ctxt qty_str =
   1.136 +let
   1.137 +  val thy = ProofContext.theory_of ctxt
   1.138 +  val qty_name = Long_Name.base_name qty_str
   1.139 +in
   1.140 +  case flag of
   1.141 +    AbsF => Const (Sign.full_bname thy ("abs_" ^ qty_name), dummyT)
   1.142 +  | RepF => Const (Sign.full_bname thy ("rep_" ^ qty_name), dummyT)
   1.143 +end
   1.144 +
   1.145 +(* Lets Nitpick represent elements of quotient types as elements of the raw type *)
   1.146 +fun absrep_const_chk flag ctxt qty_str =
   1.147 +  Syntax.check_term ctxt (absrep_const flag ctxt qty_str)
   1.148 +
   1.149 +fun absrep_match_err ctxt ty_pat ty =
   1.150 +let
   1.151 +  val ty_pat_str = Syntax.string_of_typ ctxt ty_pat
   1.152 +  val ty_str = Syntax.string_of_typ ctxt ty
   1.153 +in
   1.154 +  raise LIFT_MATCH (space_implode " "
   1.155 +    ["absrep_fun (Types ", quote ty_pat_str, "and", quote ty_str, " do not match.)"])
   1.156 +end
   1.157 +
   1.158 +
   1.159 +(** generation of an aggregate absrep function **)
   1.160 +
   1.161 +(* - In case of equal types we just return the identity.
   1.162 +
   1.163 +   - In case of TFrees we also return the identity.
   1.164 +
   1.165 +   - In case of function types we recurse taking
   1.166 +     the polarity change into account.
   1.167 +
   1.168 +   - If the type constructors are equal, we recurse for the
   1.169 +     arguments and build the appropriate map function.
   1.170 +
   1.171 +   - If the type constructors are unequal, there must be an
   1.172 +     instance of quotient types:
   1.173 +
   1.174 +       - we first look up the corresponding rty_pat and qty_pat
   1.175 +         from the quotient definition; the arguments of qty_pat
   1.176 +         must be some distinct TVars
   1.177 +       - we then match the rty_pat with rty and qty_pat with qty;
   1.178 +         if matching fails the types do not correspond -> error
   1.179 +       - the matching produces two environments; we look up the
   1.180 +         assignments for the qty_pat variables and recurse on the
   1.181 +         assignments
   1.182 +       - we prefix the aggregate map function for the rty_pat,
   1.183 +         which is an abstraction over all type variables
   1.184 +       - finally we compose the result with the appropriate
   1.185 +         absrep function in case at least one argument produced
   1.186 +         a non-identity function /
   1.187 +         otherwise we just return the appropriate absrep
   1.188 +         function
   1.189 +
   1.190 +     The composition is necessary for types like
   1.191 +
   1.192 +        ('a list) list / ('a foo) foo
   1.193 +
   1.194 +     The matching is necessary for types like
   1.195 +
   1.196 +        ('a * 'a) list / 'a bar
   1.197 +
   1.198 +     The test is necessary in order to eliminate superfluous
   1.199 +     identity maps.
   1.200 +*)
   1.201 +
   1.202 +fun absrep_fun flag ctxt (rty, qty) =
   1.203 +  if rty = qty
   1.204 +  then mk_identity rty
   1.205 +  else
   1.206 +    case (rty, qty) of
   1.207 +      (Type ("fun", [ty1, ty2]), Type ("fun", [ty1', ty2'])) =>
   1.208 +        let
   1.209 +          val arg1 = absrep_fun (negF flag) ctxt (ty1, ty1')
   1.210 +          val arg2 = absrep_fun flag ctxt (ty2, ty2')
   1.211 +        in
   1.212 +          list_comb (get_mapfun ctxt "fun", [arg1, arg2])
   1.213 +        end
   1.214 +    | (Type (s, tys), Type (s', tys')) =>
   1.215 +        if s = s'
   1.216 +        then
   1.217 +           let
   1.218 +             val args = map (absrep_fun flag ctxt) (tys ~~ tys')
   1.219 +           in
   1.220 +             list_comb (get_mapfun ctxt s, args)
   1.221 +           end
   1.222 +        else
   1.223 +           let
   1.224 +             val (rty_pat, qty_pat as Type (_, vs)) = get_rty_qty ctxt s'
   1.225 +             val rtyenv = match ctxt absrep_match_err rty_pat rty
   1.226 +             val qtyenv = match ctxt absrep_match_err qty_pat qty
   1.227 +             val args_aux = map (double_lookup rtyenv qtyenv) vs
   1.228 +             val args = map (absrep_fun flag ctxt) args_aux
   1.229 +             val map_fun = mk_mapfun ctxt vs rty_pat
   1.230 +             val result = list_comb (map_fun, args)
   1.231 +           in
   1.232 +             if forall is_identity args
   1.233 +             then absrep_const flag ctxt s'
   1.234 +             else mk_fun_compose flag (absrep_const flag ctxt s', result)
   1.235 +           end
   1.236 +    | (TFree x, TFree x') =>
   1.237 +        if x = x'
   1.238 +        then mk_identity rty
   1.239 +        else raise (LIFT_MATCH "absrep_fun (frees)")
   1.240 +    | (TVar _, TVar _) => raise (LIFT_MATCH "absrep_fun (vars)")
   1.241 +    | _ => raise (LIFT_MATCH "absrep_fun (default)")
   1.242 +
   1.243 +fun absrep_fun_chk flag ctxt (rty, qty) =
   1.244 +  absrep_fun flag ctxt (rty, qty)
   1.245 +  |> Syntax.check_term ctxt
   1.246 +
   1.247 +
   1.248 +
   1.249 +
   1.250 +(*** Aggregate Equivalence Relation ***)
   1.251 +
   1.252 +
   1.253 +(* works very similar to the absrep generation,
   1.254 +   except there is no need for polarities
   1.255 +*)
   1.256 +
   1.257 +(* instantiates TVars so that the term is of type ty *)
   1.258 +fun force_typ ctxt trm ty =
   1.259 +let
   1.260 +  val thy = ProofContext.theory_of ctxt
   1.261 +  val trm_ty = fastype_of trm
   1.262 +  val ty_inst = Sign.typ_match thy (trm_ty, ty) Vartab.empty
   1.263 +in
   1.264 +  map_types (Envir.subst_type ty_inst) trm
   1.265 +end
   1.266 +
   1.267 +fun is_eq (Const (@{const_name "op ="}, _)) = true
   1.268 +  | is_eq _ = false
   1.269 +
   1.270 +fun mk_rel_compose (trm1, trm2) =
   1.271 +  Const (@{const_name "rel_conj"}, dummyT) $ trm1 $ trm2
   1.272 +
   1.273 +fun get_relmap ctxt s =
   1.274 +let
   1.275 +  val thy = ProofContext.theory_of ctxt
   1.276 +  val exn = LIFT_MATCH ("get_relmap (no relation map function found for type " ^ s ^ ")")
   1.277 +  val relmap = #relmap (maps_lookup thy s) handle Quotient_Info.NotFound => raise exn
   1.278 +in
   1.279 +  Const (relmap, dummyT)
   1.280 +end
   1.281 +
   1.282 +fun mk_relmap ctxt vs rty =
   1.283 +let
   1.284 +  val vs' = map (mk_Free) vs
   1.285 +
   1.286 +  fun mk_relmap_aux rty =
   1.287 +    case rty of
   1.288 +      TVar _ => mk_Free rty
   1.289 +    | Type (_, []) => HOLogic.eq_const rty
   1.290 +    | Type (s, tys) => list_comb (get_relmap ctxt s, map mk_relmap_aux tys)
   1.291 +    | _ => raise LIFT_MATCH ("mk_relmap (default)")
   1.292 +in
   1.293 +  fold_rev Term.lambda vs' (mk_relmap_aux rty)
   1.294 +end
   1.295 +
   1.296 +fun get_equiv_rel ctxt s =
   1.297 +let
   1.298 +  val thy = ProofContext.theory_of ctxt
   1.299 +  val exn = LIFT_MATCH ("get_quotdata (no quotient found for type " ^ s ^ ")")
   1.300 +in
   1.301 +  #equiv_rel (quotdata_lookup thy s) handle Quotient_Info.NotFound => raise exn
   1.302 +end
   1.303 +
   1.304 +fun equiv_match_err ctxt ty_pat ty =
   1.305 +let
   1.306 +  val ty_pat_str = Syntax.string_of_typ ctxt ty_pat
   1.307 +  val ty_str = Syntax.string_of_typ ctxt ty
   1.308 +in
   1.309 +  raise LIFT_MATCH (space_implode " "
   1.310 +    ["equiv_relation (Types ", quote ty_pat_str, "and", quote ty_str, " do not match.)"])
   1.311 +end
   1.312 +
   1.313 +(* builds the aggregate equivalence relation
   1.314 +   that will be the argument of Respects
   1.315 +*)
   1.316 +fun equiv_relation ctxt (rty, qty) =
   1.317 +  if rty = qty
   1.318 +  then HOLogic.eq_const rty
   1.319 +  else
   1.320 +    case (rty, qty) of
   1.321 +      (Type (s, tys), Type (s', tys')) =>
   1.322 +       if s = s'
   1.323 +       then
   1.324 +         let
   1.325 +           val args = map (equiv_relation ctxt) (tys ~~ tys')
   1.326 +         in
   1.327 +           list_comb (get_relmap ctxt s, args)
   1.328 +         end
   1.329 +       else
   1.330 +         let
   1.331 +           val (rty_pat, qty_pat as Type (_, vs)) = get_rty_qty ctxt s'
   1.332 +           val rtyenv = match ctxt equiv_match_err rty_pat rty
   1.333 +           val qtyenv = match ctxt equiv_match_err qty_pat qty
   1.334 +           val args_aux = map (double_lookup rtyenv qtyenv) vs
   1.335 +           val args = map (equiv_relation ctxt) args_aux
   1.336 +           val rel_map = mk_relmap ctxt vs rty_pat
   1.337 +           val result = list_comb (rel_map, args)
   1.338 +           val eqv_rel = get_equiv_rel ctxt s'
   1.339 +           val eqv_rel' = force_typ ctxt eqv_rel ([rty, rty] ---> @{typ bool})
   1.340 +         in
   1.341 +           if forall is_eq args
   1.342 +           then eqv_rel'
   1.343 +           else mk_rel_compose (result, eqv_rel')
   1.344 +         end
   1.345 +      | _ => HOLogic.eq_const rty
   1.346 +
   1.347 +fun equiv_relation_chk ctxt (rty, qty) =
   1.348 +  equiv_relation ctxt (rty, qty)
   1.349 +  |> Syntax.check_term ctxt
   1.350 +
   1.351 +
   1.352 +
   1.353 +(*** Regularization ***)
   1.354 +
   1.355 +(* Regularizing an rtrm means:
   1.356 +
   1.357 + - Quantifiers over types that need lifting are replaced
   1.358 +   by bounded quantifiers, for example:
   1.359 +
   1.360 +      All P  ----> All (Respects R) P
   1.361 +
   1.362 +   where the aggregate relation R is given by the rty and qty;
   1.363 +
   1.364 + - Abstractions over types that need lifting are replaced
   1.365 +   by bounded abstractions, for example:
   1.366 +
   1.367 +      %x. P  ----> Ball (Respects R) %x. P
   1.368 +
   1.369 + - Equalities over types that need lifting are replaced by
   1.370 +   corresponding equivalence relations, for example:
   1.371 +
   1.372 +      A = B  ----> R A B
   1.373 +
   1.374 +   or
   1.375 +
   1.376 +      A = B  ----> (R ===> R) A B
   1.377 +
   1.378 +   for more complicated types of A and B
   1.379 +
   1.380 +
   1.381 + The regularize_trm accepts raw theorems in which equalities
   1.382 + and quantifiers match exactly the ones in the lifted theorem
   1.383 + but also accepts partially regularized terms.
   1.384 +
   1.385 + This means that the raw theorems can have:
   1.386 +   Ball (Respects R),  Bex (Respects R), Bex1_rel (Respects R), Babs, R
   1.387 + in the places where:
   1.388 +   All, Ex, Ex1, %, (op =)
   1.389 + is required the lifted theorem.
   1.390 +
   1.391 +*)
   1.392 +
   1.393 +val mk_babs = Const (@{const_name Babs}, dummyT)
   1.394 +val mk_ball = Const (@{const_name Ball}, dummyT)
   1.395 +val mk_bex  = Const (@{const_name Bex}, dummyT)
   1.396 +val mk_bex1_rel = Const (@{const_name Bex1_rel}, dummyT)
   1.397 +val mk_resp = Const (@{const_name Respects}, dummyT)
   1.398 +
   1.399 +(* - applies f to the subterm of an abstraction,
   1.400 +     otherwise to the given term,
   1.401 +   - used by regularize, therefore abstracted
   1.402 +     variables do not have to be treated specially
   1.403 +*)
   1.404 +fun apply_subt f (trm1, trm2) =
   1.405 +  case (trm1, trm2) of
   1.406 +    (Abs (x, T, t), Abs (_ , _, t')) => Abs (x, T, f (t, t'))
   1.407 +  | _ => f (trm1, trm2)
   1.408 +
   1.409 +fun term_mismatch str ctxt t1 t2 =
   1.410 +let
   1.411 +  val t1_str = Syntax.string_of_term ctxt t1
   1.412 +  val t2_str = Syntax.string_of_term ctxt t2
   1.413 +  val t1_ty_str = Syntax.string_of_typ ctxt (fastype_of t1)
   1.414 +  val t2_ty_str = Syntax.string_of_typ ctxt (fastype_of t2)
   1.415 +in
   1.416 +  raise LIFT_MATCH (cat_lines [str, t1_str ^ "::" ^ t1_ty_str, t2_str ^ "::" ^ t2_ty_str])
   1.417 +end
   1.418 +
   1.419 +(* the major type of All and Ex quantifiers *)
   1.420 +fun qnt_typ ty = domain_type (domain_type ty)
   1.421 +
   1.422 +(* Checks that two types match, for example:
   1.423 +     rty -> rty   matches   qty -> qty *)
   1.424 +fun matches_typ thy rT qT =
   1.425 +  if rT = qT then true else
   1.426 +  case (rT, qT) of
   1.427 +    (Type (rs, rtys), Type (qs, qtys)) =>
   1.428 +      if rs = qs then
   1.429 +        if length rtys <> length qtys then false else
   1.430 +        forall (fn x => x = true) (map2 (matches_typ thy) rtys qtys)
   1.431 +      else
   1.432 +        (case Quotient_Info.quotdata_lookup_raw thy qs of
   1.433 +          SOME quotinfo => Sign.typ_instance thy (rT, #rtyp quotinfo)
   1.434 +        | NONE => false)
   1.435 +  | _ => false
   1.436 +
   1.437 +
   1.438 +(* produces a regularized version of rtrm
   1.439 +
   1.440 +   - the result might contain dummyTs
   1.441 +
   1.442 +   - for regularisation we do not need any
   1.443 +     special treatment of bound variables
   1.444 +*)
   1.445 +fun regularize_trm ctxt (rtrm, qtrm) =
   1.446 +  case (rtrm, qtrm) of
   1.447 +    (Abs (x, ty, t), Abs (_, ty', t')) =>
   1.448 +       let
   1.449 +         val subtrm = Abs(x, ty, regularize_trm ctxt (t, t'))
   1.450 +       in
   1.451 +         if ty = ty' then subtrm
   1.452 +         else mk_babs $ (mk_resp $ equiv_relation ctxt (ty, ty')) $ subtrm
   1.453 +       end
   1.454 +  | (Const (@{const_name "Babs"}, T) $ resrel $ (t as (Abs (_, ty, _))), t' as (Abs (_, ty', _))) =>
   1.455 +       let
   1.456 +         val subtrm = regularize_trm ctxt (t, t')
   1.457 +         val needres = mk_resp $ equiv_relation_chk ctxt (ty, ty')
   1.458 +       in
   1.459 +         if resrel <> needres
   1.460 +         then term_mismatch "regularize (Babs)" ctxt resrel needres
   1.461 +         else mk_babs $ resrel $ subtrm
   1.462 +       end
   1.463 +
   1.464 +  | (Const (@{const_name "All"}, ty) $ t, Const (@{const_name "All"}, ty') $ t') =>
   1.465 +       let
   1.466 +         val subtrm = apply_subt (regularize_trm ctxt) (t, t')
   1.467 +       in
   1.468 +         if ty = ty' then Const (@{const_name "All"}, ty) $ subtrm
   1.469 +         else mk_ball $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
   1.470 +       end
   1.471 +
   1.472 +  | (Const (@{const_name "Ex"}, ty) $ t, Const (@{const_name "Ex"}, ty') $ t') =>
   1.473 +       let
   1.474 +         val subtrm = apply_subt (regularize_trm ctxt) (t, t')
   1.475 +       in
   1.476 +         if ty = ty' then Const (@{const_name "Ex"}, ty) $ subtrm
   1.477 +         else mk_bex $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
   1.478 +       end
   1.479 +
   1.480 +  | (Const (@{const_name "Ex1"}, ty) $ (Abs (_, _,
   1.481 +      (Const (@{const_name "op &"}, _) $ (Const (@{const_name "op :"}, _) $ _ $
   1.482 +        (Const (@{const_name "Respects"}, _) $ resrel)) $ (t $ _)))),
   1.483 +     Const (@{const_name "Ex1"}, ty') $ t') =>
   1.484 +       let
   1.485 +         val t_ = incr_boundvars (~1) t
   1.486 +         val subtrm = apply_subt (regularize_trm ctxt) (t_, t')
   1.487 +         val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty')
   1.488 +       in
   1.489 +         if resrel <> needrel
   1.490 +         then term_mismatch "regularize (Bex1)" ctxt resrel needrel
   1.491 +         else mk_bex1_rel $ resrel $ subtrm
   1.492 +       end
   1.493 +
   1.494 +  | (Const (@{const_name "Ex1"}, ty) $ t, Const (@{const_name "Ex1"}, ty') $ t') =>
   1.495 +       let
   1.496 +         val subtrm = apply_subt (regularize_trm ctxt) (t, t')
   1.497 +       in
   1.498 +         if ty = ty' then Const (@{const_name "Ex1"}, ty) $ subtrm
   1.499 +         else mk_bex1_rel $ (equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
   1.500 +       end
   1.501 +
   1.502 +  | (Const (@{const_name "Ball"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t,
   1.503 +     Const (@{const_name "All"}, ty') $ t') =>
   1.504 +       let
   1.505 +         val subtrm = apply_subt (regularize_trm ctxt) (t, t')
   1.506 +         val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty')
   1.507 +       in
   1.508 +         if resrel <> needrel
   1.509 +         then term_mismatch "regularize (Ball)" ctxt resrel needrel
   1.510 +         else mk_ball $ (mk_resp $ resrel) $ subtrm
   1.511 +       end
   1.512 +
   1.513 +  | (Const (@{const_name "Bex"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t,
   1.514 +     Const (@{const_name "Ex"}, ty') $ t') =>
   1.515 +       let
   1.516 +         val subtrm = apply_subt (regularize_trm ctxt) (t, t')
   1.517 +         val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty')
   1.518 +       in
   1.519 +         if resrel <> needrel
   1.520 +         then term_mismatch "regularize (Bex)" ctxt resrel needrel
   1.521 +         else mk_bex $ (mk_resp $ resrel) $ subtrm
   1.522 +       end
   1.523 +
   1.524 +  | (Const (@{const_name "Bex1_rel"}, ty) $ resrel $ t, Const (@{const_name "Ex1"}, ty') $ t') =>
   1.525 +       let
   1.526 +         val subtrm = apply_subt (regularize_trm ctxt) (t, t')
   1.527 +         val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty')
   1.528 +       in
   1.529 +         if resrel <> needrel
   1.530 +         then term_mismatch "regularize (Bex1_res)" ctxt resrel needrel
   1.531 +         else mk_bex1_rel $ resrel $ subtrm
   1.532 +       end
   1.533 +
   1.534 +  | (* equalities need to be replaced by appropriate equivalence relations *)
   1.535 +    (Const (@{const_name "op ="}, ty), Const (@{const_name "op ="}, ty')) =>
   1.536 +         if ty = ty' then rtrm
   1.537 +         else equiv_relation ctxt (domain_type ty, domain_type ty')
   1.538 +
   1.539 +  | (* in this case we just check whether the given equivalence relation is correct *)
   1.540 +    (rel, Const (@{const_name "op ="}, ty')) =>
   1.541 +       let
   1.542 +         val rel_ty = fastype_of rel
   1.543 +         val rel' = equiv_relation_chk ctxt (domain_type rel_ty, domain_type ty')
   1.544 +       in
   1.545 +         if rel' aconv rel then rtrm
   1.546 +         else term_mismatch "regularise (relation mismatch)" ctxt rel rel'
   1.547 +       end
   1.548 +
   1.549 +  | (_, Const _) =>
   1.550 +       let
   1.551 +         val thy = ProofContext.theory_of ctxt
   1.552 +         fun same_const (Const (s, T)) (Const (s', T')) = (s = s') andalso matches_typ thy T T'
   1.553 +           | same_const _ _ = false
   1.554 +       in
   1.555 +         if same_const rtrm qtrm then rtrm
   1.556 +         else
   1.557 +           let
   1.558 +             val rtrm' = #rconst (qconsts_lookup thy qtrm)
   1.559 +               handle Quotient_Info.NotFound => term_mismatch "regularize(constant notfound)" ctxt rtrm qtrm
   1.560 +           in
   1.561 +             if Pattern.matches thy (rtrm', rtrm)
   1.562 +             then rtrm else term_mismatch "regularize(constant mismatch)" ctxt rtrm qtrm
   1.563 +           end
   1.564 +       end
   1.565 +
   1.566 +  | (((t1 as Const (@{const_name "split"}, _)) $ Abs (v1, ty, Abs(v1', ty', s1))),
   1.567 +     ((t2 as Const (@{const_name "split"}, _)) $ Abs (v2, _ , Abs(v2', _  , s2)))) =>
   1.568 +       regularize_trm ctxt (t1, t2) $ Abs (v1, ty, Abs (v1', ty', regularize_trm ctxt (s1, s2)))
   1.569 +
   1.570 +  | (((t1 as Const (@{const_name "split"}, _)) $ Abs (v1, ty, s1)),
   1.571 +     ((t2 as Const (@{const_name "split"}, _)) $ Abs (v2, _ , s2))) =>
   1.572 +       regularize_trm ctxt (t1, t2) $ Abs (v1, ty, regularize_trm ctxt (s1, s2))
   1.573 +
   1.574 +  | (t1 $ t2, t1' $ t2') =>
   1.575 +       regularize_trm ctxt (t1, t1') $ regularize_trm ctxt (t2, t2')
   1.576 +
   1.577 +  | (Bound i, Bound i') =>
   1.578 +       if i = i' then rtrm
   1.579 +       else raise (LIFT_MATCH "regularize (bounds mismatch)")
   1.580 +
   1.581 +  | _ =>
   1.582 +       let
   1.583 +         val rtrm_str = Syntax.string_of_term ctxt rtrm
   1.584 +         val qtrm_str = Syntax.string_of_term ctxt qtrm
   1.585 +       in
   1.586 +         raise (LIFT_MATCH ("regularize failed (default: " ^ rtrm_str ^ "," ^ qtrm_str ^ ")"))
   1.587 +       end
   1.588 +
   1.589 +fun regularize_trm_chk ctxt (rtrm, qtrm) =
   1.590 +  regularize_trm ctxt (rtrm, qtrm)
   1.591 +  |> Syntax.check_term ctxt
   1.592 +
   1.593 +
   1.594 +
   1.595 +(*** Rep/Abs Injection ***)
   1.596 +
   1.597 +(*
   1.598 +Injection of Rep/Abs means:
   1.599 +
   1.600 +  For abstractions:
   1.601 +
   1.602 +  * If the type of the abstraction needs lifting, then we add Rep/Abs
   1.603 +    around the abstraction; otherwise we leave it unchanged.
   1.604 +
   1.605 +  For applications:
   1.606 +
   1.607 +  * If the application involves a bounded quantifier, we recurse on
   1.608 +    the second argument. If the application is a bounded abstraction,
   1.609 +    we always put an Rep/Abs around it (since bounded abstractions
   1.610 +    are assumed to always need lifting). Otherwise we recurse on both
   1.611 +    arguments.
   1.612 +
   1.613 +  For constants:
   1.614 +
   1.615 +  * If the constant is (op =), we leave it always unchanged.
   1.616 +    Otherwise the type of the constant needs lifting, we put
   1.617 +    and Rep/Abs around it.
   1.618 +
   1.619 +  For free variables:
   1.620 +
   1.621 +  * We put a Rep/Abs around it if the type needs lifting.
   1.622 +
   1.623 +  Vars case cannot occur.
   1.624 +*)
   1.625 +
   1.626 +fun mk_repabs ctxt (T, T') trm =
   1.627 +  absrep_fun RepF ctxt (T, T') $ (absrep_fun AbsF ctxt (T, T') $ trm)
   1.628 +
   1.629 +fun inj_repabs_err ctxt msg rtrm qtrm =
   1.630 +let
   1.631 +  val rtrm_str = Syntax.string_of_term ctxt rtrm
   1.632 +  val qtrm_str = Syntax.string_of_term ctxt qtrm
   1.633 +in
   1.634 +  raise LIFT_MATCH (space_implode " " [msg, quote rtrm_str, "and", quote qtrm_str])
   1.635 +end
   1.636 +
   1.637 +
   1.638 +(* bound variables need to be treated properly,
   1.639 +   as the type of subterms needs to be calculated   *)
   1.640 +fun inj_repabs_trm ctxt (rtrm, qtrm) =
   1.641 + case (rtrm, qtrm) of
   1.642 +    (Const (@{const_name "Ball"}, T) $ r $ t, Const (@{const_name "All"}, _) $ t') =>
   1.643 +       Const (@{const_name "Ball"}, T) $ r $ (inj_repabs_trm ctxt (t, t'))
   1.644 +
   1.645 +  | (Const (@{const_name "Bex"}, T) $ r $ t, Const (@{const_name "Ex"}, _) $ t') =>
   1.646 +       Const (@{const_name "Bex"}, T) $ r $ (inj_repabs_trm ctxt (t, t'))
   1.647 +
   1.648 +  | (Const (@{const_name "Babs"}, T) $ r $ t, t' as (Abs _)) =>
   1.649 +      let
   1.650 +        val rty = fastype_of rtrm
   1.651 +        val qty = fastype_of qtrm
   1.652 +      in
   1.653 +        mk_repabs ctxt (rty, qty) (Const (@{const_name "Babs"}, T) $ r $ (inj_repabs_trm ctxt (t, t')))
   1.654 +      end
   1.655 +
   1.656 +  | (Abs (x, T, t), Abs (x', T', t')) =>
   1.657 +      let
   1.658 +        val rty = fastype_of rtrm
   1.659 +        val qty = fastype_of qtrm
   1.660 +        val (y, s) = Term.dest_abs (x, T, t)
   1.661 +        val (_, s') = Term.dest_abs (x', T', t')
   1.662 +        val yvar = Free (y, T)
   1.663 +        val result = Term.lambda_name (y, yvar) (inj_repabs_trm ctxt (s, s'))
   1.664 +      in
   1.665 +        if rty = qty then result
   1.666 +        else mk_repabs ctxt (rty, qty) result
   1.667 +      end
   1.668 +
   1.669 +  | (t $ s, t' $ s') =>
   1.670 +       (inj_repabs_trm ctxt (t, t')) $ (inj_repabs_trm ctxt (s, s'))
   1.671 +
   1.672 +  | (Free (_, T), Free (_, T')) =>
   1.673 +        if T = T' then rtrm
   1.674 +        else mk_repabs ctxt (T, T') rtrm
   1.675 +
   1.676 +  | (_, Const (@{const_name "op ="}, _)) => rtrm
   1.677 +
   1.678 +  | (_, Const (_, T')) =>
   1.679 +      let
   1.680 +        val rty = fastype_of rtrm
   1.681 +      in
   1.682 +        if rty = T' then rtrm
   1.683 +        else mk_repabs ctxt (rty, T') rtrm
   1.684 +      end
   1.685 +
   1.686 +  | _ => inj_repabs_err ctxt "injection (default):" rtrm qtrm
   1.687 +
   1.688 +fun inj_repabs_trm_chk ctxt (rtrm, qtrm) =
   1.689 +  inj_repabs_trm ctxt (rtrm, qtrm)
   1.690 +  |> Syntax.check_term ctxt
   1.691 +
   1.692 +
   1.693 +
   1.694 +(*** Wrapper for automatically transforming an rthm into a qthm ***)
   1.695 +
   1.696 +(* subst_tys takes a list of (rty, qty) substitution pairs
   1.697 +   and replaces all occurences of rty in the given type
   1.698 +   by appropriate qty, with substitution *)
   1.699 +fun subst_ty thy ty (rty, qty) r =
   1.700 +  if r <> NONE then r else
   1.701 +  case try (Sign.typ_match thy (rty, ty)) Vartab.empty of
   1.702 +    SOME inst => SOME (Envir.subst_type inst qty)
   1.703 +  | NONE => NONE
   1.704 +fun subst_tys thy substs ty =
   1.705 +  case fold (subst_ty thy ty) substs NONE of
   1.706 +    SOME ty => ty
   1.707 +  | NONE =>
   1.708 +      (case ty of
   1.709 +        Type (s, tys) => Type (s, map (subst_tys thy substs) tys)
   1.710 +      | x => x)
   1.711 +
   1.712 +(* subst_trms takes a list of (rtrm, qtrm) substitution pairs
   1.713 +   and if the given term matches any of the raw terms it
   1.714 +   returns the appropriate qtrm instantiated. If none of
   1.715 +   them matched it returns NONE. *)
   1.716 +fun subst_trm thy t (rtrm, qtrm) s =
   1.717 +  if s <> NONE then s else
   1.718 +    case try (Pattern.match thy (rtrm, t)) (Vartab.empty, Vartab.empty) of
   1.719 +      SOME inst => SOME (Envir.subst_term inst qtrm)
   1.720 +    | NONE => NONE;
   1.721 +fun subst_trms thy substs t = fold (subst_trm thy t) substs NONE
   1.722 +
   1.723 +(* prepares type and term substitution pairs to be used by above
   1.724 +   functions that let replace all raw constructs by appropriate
   1.725 +   lifted counterparts. *)
   1.726 +fun get_ty_trm_substs ctxt =
   1.727 +let
   1.728 +  val thy = ProofContext.theory_of ctxt
   1.729 +  val quot_infos  = Quotient_Info.quotdata_dest ctxt
   1.730 +  val const_infos = Quotient_Info.qconsts_dest ctxt
   1.731 +  val ty_substs = map (fn ri => (#rtyp ri, #qtyp ri)) quot_infos
   1.732 +  val const_substs = map (fn ci => (#rconst ci, #qconst ci)) const_infos
   1.733 +  fun rel_eq rel = HOLogic.eq_const (subst_tys thy ty_substs (domain_type (fastype_of rel)))
   1.734 +  val rel_substs = map (fn ri => (#equiv_rel ri, rel_eq (#equiv_rel ri))) quot_infos
   1.735 +in
   1.736 +  (ty_substs, const_substs @ rel_substs)
   1.737 +end
   1.738 +
   1.739 +fun quotient_lift_const (b, t) ctxt =
   1.740 +let
   1.741 +  val thy = ProofContext.theory_of ctxt
   1.742 +  val (ty_substs, _) = get_ty_trm_substs ctxt;
   1.743 +  val (_, ty) = dest_Const t;
   1.744 +  val nty = subst_tys thy ty_substs ty;
   1.745 +in
   1.746 +  Free(b, nty)
   1.747 +end
   1.748 +
   1.749 +(*
   1.750 +Takes a term and
   1.751 +
   1.752 +* replaces raw constants by the quotient constants
   1.753 +
   1.754 +* replaces equivalence relations by equalities
   1.755 +
   1.756 +* replaces raw types by the quotient types
   1.757 +
   1.758 +*)
   1.759 +
   1.760 +fun quotient_lift_all ctxt t =
   1.761 +let
   1.762 +  val thy = ProofContext.theory_of ctxt
   1.763 +  val (ty_substs, substs) = get_ty_trm_substs ctxt
   1.764 +  fun lift_aux t =
   1.765 +    case subst_trms thy substs t of
   1.766 +      SOME x => x
   1.767 +    | NONE =>
   1.768 +      (case t of
   1.769 +        a $ b => lift_aux a $ lift_aux b
   1.770 +      | Abs(a, ty, s) =>
   1.771 +          let
   1.772 +            val (y, s') = Term.dest_abs (a, ty, s)
   1.773 +            val nty = subst_tys thy ty_substs ty
   1.774 +          in
   1.775 +            Abs(y, nty, abstract_over (Free (y, nty), lift_aux s'))
   1.776 +          end
   1.777 +      | Free(n, ty) => Free(n, subst_tys thy ty_substs ty)
   1.778 +      | Var(n, ty) => Var(n, subst_tys thy ty_substs ty)
   1.779 +      | Bound i => Bound i
   1.780 +      | Const(s, ty) => Const(s, subst_tys thy ty_substs ty))
   1.781 +in
   1.782 +  lift_aux t
   1.783 +end
   1.784 +
   1.785 +
   1.786 +end; (* structure *)
   1.787 +
   1.788 +
   1.789 +