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