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